Feature exception handling

README.md

@@ -0,0 +1,17 @@
+[![Build Status](https://travis-ci.org/rarworld/daikon.svg?branch=FeatureExceptionHandling)](https://travis-ci.org/rarworld/daikon)
+
+This is the distribution of a fork of the Daikon invariant detector,  
+based on Daikon version 5.3.3, released May 2, 2016.  
+Daikon version 5.3.3.1_rar, released Mai 24, 2016
+
+If you are working with a Daikon distribution downloaded from the Daikon   
+website, then most everything is setup and ready to go.  See the 'doc'  
+subdirectory for additional information, including installation instructions.  
+You should start out with the file:  
+  doc/index.html  
+The documentation also appears on the Daikon homepage:  
+    http://plse.cs.washington.edu/daikon/  
+
+If you are working with source cloned from the source code repository  
+https://github.com/codespecs/daikon, then please review the file  
+README.source.

java/daikon/AnnotateNullable.java

@@ -114,13 +114,13 @@ public static void main(String[] args) throws IOException {
     // static method can be identified because it will not have the OBJECT
     // point as a parent.
     for (PptTopLevel ppt : ppts.pptIterable()) {
-      if (!ppt.is_combined_exit() || !is_static_method(ppt)) continue;
+      if (!ppt.is_combined_exit() || !ppt.is_combined_exception() || !is_static_method(ppt))
+        continue;
 
       String name = ppt.name().replaceFirst("[(].*$", "");
       int lastdot = name.lastIndexOf('.');
       @SuppressWarnings("keyfor") // appliction invariant:  KeyFor and substring
-      /*@KeyFor("class_map")*/
-      // class_map has entry per class, and this method is in some class
+      /*@KeyFor("class_map")*/ // class_map has entry per class, and this method is in some class
       String classname = name.substring(0, lastdot);
       // System.out.printf ("classname for ppt %s is '%s'%n", name, classname);
       /*@NonNull*/ List<PptTopLevel> static_methods = class_map.get(classname);
@@ -423,6 +423,14 @@ public static String jvm_signature(PptTopLevel ppt) {
         "signature") // application invariant: returnVar.type.toString() is a binary name (if returnVar is non-null), because we are processing a Java program
     String returnType =
         returnVar == null ? "V" : UtilMDE.binaryNameToFieldDescriptor(returnVar.type.toString());
+    // Or an throw point
+    if (returnVar == null) {
+      returnVar = ppt.find_var_by_name("exception");
+      returnType =
+          returnVar == null
+              ? "V"
+              : "V throws " + UtilMDE.binaryNameToFieldDescriptor(returnVar.type.toString());
+    }
 
     return method + UtilMDE.arglistToJvm(java_args) + returnType;
   }

java/daikon/Chicory.java

@@ -113,6 +113,12 @@ public class Chicory {
   @Option("Number of calls after which sampling will begin")
   public static int sample_start = 0;
 
+  @Option("Should Exception Handling be taken care of?")
+  public static boolean exception_handling = false;
+
+  @Option("RemoteDebug Test")
+  public static boolean rDebug = false;
+
   /**
    * Daikon port number.  Daikon writes this to stdout when it is started
    * in online mode.
@@ -138,7 +144,7 @@ public class Chicory {
   /** flag to use if we want to turn on the static initialization checks **/
   public static final boolean checkStaticInit = true;
 
-  private static final boolean RemoteDebug = false;
+  private static /*final*/ boolean RemoteDebug = false;
 
   /** Flag to initiate a purity analysis and use results to create add vars **/
   private static boolean purityAnalysis = false;
@@ -163,6 +169,7 @@ public static void main(String[] args) {
 
     // Turn on basic logging if the debug was selected
     basic.enabled = debug;
+    RemoteDebug = rDebug;
     basic.log("target_args = %s%n", Arrays.toString(target_args));
 
     // Start the target.  Pass the same options to the premain as
@@ -340,7 +347,8 @@ void start_target(String premain_args, String[] target_args) {
 
     if (RemoteDebug) {
       //-Xdebug -Xrunjdwp:server=y,transport=dt_socket,address=4142,suspend=n
-      cmdlist.add("-Xdebug -Xrunjdwp:server=n,transport=dt_socket,address=8000,suspend=y");
+      cmdlist.add("-agentlib:jdwp=transport=dt_socket,server=y,address=8000,suspend=y");
+      //cmdlist.add("-Xdebug -Xrunjdwp:server=n,transport=dt_socket,address=8000,suspend=y");
       //cmdlist.add("-Xdebug -Xnoagent -Xrunjdwp:transport=dt_socket,server=n,suspend=n,address=8000 -Djava.compiler=NONE");
     }
 
@@ -465,6 +473,11 @@ public void runDaikon() {
               dtrace_file);
     }
 
+    if (RemoteDebug) {
+      cmdstr =
+          cmdstr.replace(
+              "java", "java -agentlib:jdwp=transport=dt_socket,server=y,address=8001,suspend=y");
+    }
     //System.out.println("daikon command is " + daikon_cmd);
     //System.out.println("daikon command cmdstr " + cmdstr);
 

java/daikon/Daikon.java

@@ -87,8 +87,8 @@ private Daikon() {
 
   // Don't change the order of the modifiers on these strings as they
   // are automatically updated as part of the release process
-  public final static String release_version = "5.3.3";
-  public final static String release_date = "May 2, 2016";
+  public final static String release_version = "5.3.3.2_rar";
+  public final static String release_date = "Mai 24, 2016";
   public final static String release_string =
       "Daikon version "
           + release_version
@@ -1628,7 +1628,12 @@ public static void create_combined_exits(PptMap ppts) {
 
       PptTopLevel exitnn_ppt = ppt;
       PptName exitnn_name = exitnn_ppt.ppt_name;
-      PptName exit_name = ppt.ppt_name.makeExit();
+      PptName exit_name;
+      if (!exitnn_name.isThrowPoint()) {
+        exit_name = ppt.ppt_name.makeExit();
+      } else {
+        exit_name = ppt.ppt_name.makeThrowExit();
+      }
       PptTopLevel exit_ppt = exit_ppts.get(exit_name);
 
       if (debugInit.isLoggable(Level.FINE)) {
@@ -1715,7 +1720,7 @@ static List<Invariant> filter_invs(List<Invariant> invs) {
    * Does nothing if exit_ppt is not an EXIT/EXITnn.
    */
   private static void create_orig_vars(PptTopLevel exit_ppt, PptMap ppts) {
-    if (!exit_ppt.ppt_name.isExitPoint()) {
+    if (!exit_ppt.ppt_name.isExitPoint() && !exit_ppt.ppt_name.isExceptionPoint()) {
       if (VarInfo.assertionsEnabled()) {
         for (VarInfo vi : exit_ppt.var_infos) {
           try {
@@ -2291,8 +2296,9 @@ public static void setupEquality(PptTopLevel ppt) {
       //  named program points such as :::POINT (used by convertcsv.pl)
       //  will be treated as leaves.
       if (p.ppt_name.isCombinedExitPoint()
+          || p.ppt_name.isCombinedThrowPoint()
           || p.ppt_name.isEnterPoint()
-          || p.ppt_name.isThrowsPoint()
+          //        || p.ppt_name.isThrowsPoint()
           || p.ppt_name.isObjectInstanceSynthetic()
           || p.ppt_name.isClassStaticSynthetic()) {
         return;

java/daikon/FileIO.java

@@ -47,8 +47,12 @@ private FileIO() {
   // a number may follow it.
   public static final String exit_suffix = "EXIT";
   public static final String exit_tag = ppt_tag_separator + exit_suffix;
+  public static final String throw_suffix = "THROW";
+  public static final String throw_tag = ppt_tag_separator + throw_suffix;
   public static final String throws_suffix = "THROWS";
   public static final String throws_tag = ppt_tag_separator + throws_suffix;
+  public static final String exception_suffix = "THROWSCOMBINED";
+  public static final String exception_tag = ppt_tag_separator + exception_suffix;
   public static final String object_suffix = "OBJECT";
   public static final String object_tag = ppt_tag_separator + object_suffix;
   public static final String class_static_suffix = "CLASS";
@@ -1033,8 +1037,9 @@ private static void warn_if_hierarchy_mismatch(PptMap all_ppts) {
     for (PptTopLevel ppt_top_level : all_ppts.ppt_all_iterable()) {
       boolean is_program_point =
           (ppt_top_level.ppt_name.isExitPoint()
+              || ppt_top_level.ppt_name.isExceptionPoint()
               || ppt_top_level.ppt_name.isEnterPoint()
-              || ppt_top_level.ppt_name.isThrowsPoint()
+              //            || ppt_top_level.ppt_name.isThrowsPoint()
               || ppt_top_level.ppt_name.isObjectInstanceSynthetic()
               || ppt_top_level.ppt_name.isClassStaticSynthetic()
               || ppt_top_level.ppt_name.isGlobalPoint());
@@ -1767,7 +1772,7 @@ public static void process_sample(
       //  will be treated as leaves.
 
       if (ppt.ppt_name.isEnterPoint()
-          || ppt.ppt_name.isThrowsPoint()
+          //        || ppt.ppt_name.isThrowsPoint() /* Throws is a LEAF now, like Exit_nn
           || ppt.ppt_name.isObjectInstanceSynthetic()
           || ppt.ppt_name.isClassStaticSynthetic()
           || ppt.ppt_name.isGlobalPoint()) {
@@ -1779,6 +1784,12 @@ public static void process_sample(
         throw new RuntimeException(
             "Bad program point name " + ppt.name + " is a combined exit point name");
       }
+
+      if (ppt.ppt_name.isExceptionPoint() && ppt.ppt_name.isCombinedThrowPoint()) {
+        // not Daikon.TerminationMessage; caller has more info (e.g., filename)
+        throw new RuntimeException(
+            "Bad program point name " + ppt.name + " is a combined exception point name");
+      }
     }
 
     // Add derived variables
@@ -2216,7 +2227,7 @@ public static boolean compute_orig_variables(
       return false;
     }
 
-    if (ppt.ppt_name.isExitPoint() || ppt.ppt_name.isThrowsPoint()) {
+    if (ppt.ppt_name.isExitPoint() || ppt.ppt_name.isExceptionPoint()) {
       Invocation invoc;
       // Set invoc
       {

java/daikon/MergeInvariants.java

@@ -272,11 +272,11 @@ public static void mainHelper(String[] args)
     for (PptTopLevel ppt : merge_ppts.pptIterable()) {
 
       // Skip everything that is not a final exit point
-      if (!ppt.ppt_name.isExitPoint()) {
+      if (!ppt.ppt_name.isExitPoint() && !ppt.ppt_name.isExceptionPoint()) {
         assert ppt.children.size() > 0 : ppt;
         continue;
       }
-      if (ppt.ppt_name.isCombinedExitPoint()) {
+      if (ppt.ppt_name.isCombinedExitPoint() || ppt.ppt_name.isCombinedThrowPoint()) {
         assert ppt.children.size() > 0 : ppt;
         continue;
       }
@@ -383,8 +383,14 @@ public static void mainHelper(String[] args)
     // Remove the PptRelation links so that when the file is written
     // out it only includes the new information
     for (PptTopLevel ppt : merge_ppts.pptIterable()) {
-      if (!ppt.ppt_name.isExitPoint()) continue;
-      if (ppt.ppt_name.isCombinedExitPoint()) continue;
+
+      if (!ppt.ppt_name.isExitPoint() && !ppt.ppt_name.isExceptionPoint()) {
+        continue;
+      }
+      if (ppt.ppt_name.isCombinedExitPoint() || ppt.ppt_name.isCombinedThrowPoint()) {
+        continue;
+      }
+
       ppt.children.clear();
       for (PptConditional cond : ppt.cond_iterable()) {
         cond.children.clear();

java/daikon/PptName.java

@@ -292,6 +292,14 @@ public int getPointSubscript() {
     return (point != null) && point.startsWith(FileIO.exit_suffix);
   }
 
+  /**
+   * @return true iff this name refers to an abrupt completion point
+   **/
+  /*@EnsuresNonNullIf(result=true, expression="point")*/
+  /*@Pure*/ public boolean isThrowPoint() {
+    return (point != null) && point.startsWith(FileIO.throw_suffix);
+  }
+
   /**
    * @return true iff this name refers to an abrupt completion point
    **/
@@ -300,6 +308,24 @@ public int getPointSubscript() {
     return (point != null) && point.startsWith(FileIO.throws_suffix);
   }
 
+  /**
+   * @return true iff this name refers to a procedure exception point
+   **/
+  /*@EnsuresNonNullIf(result=true, expression="point")*/
+  /*@Pure*/ public boolean isExceptionPoint() {
+    return (point != null)
+        && (point.startsWith(FileIO.throw_suffix) || point.equals(FileIO.exception_suffix));
+  }
+
+  /**
+   * @return true iff this name refers to a combined (synthetic) procedure
+   *         exception point
+   **/
+  /*@EnsuresNonNullIf(result=true, expression="point")*/
+  /*@Pure*/ public boolean isCombinedThrowPoint() {
+    return (point != null) && point.equals(FileIO.exception_suffix);
+  }
+
   /**
    * @return true iff this name refers to a combined (synthetic) procedure
    *         exit point
@@ -402,9 +428,9 @@ public PptName makeEnter() {
     // We may wish to have a different exceptional than non-exceptional
     // entry point; in particular, if there was an exception, then perhaps
     // the precondition or object invariant was not met.
-    assert isExitPoint() : fullname;
+    assert isExitPoint() || isExceptionPoint() : fullname;
 
-    assert isExitPoint() || isThrowsPoint();
+    assert isExitPoint() || isExceptionPoint();
     return new PptName(cls, method, FileIO.enter_suffix);
   }
 
@@ -417,12 +443,21 @@ public PptName makeExit() {
     return new PptName(cls, method, FileIO.exit_suffix);
   }
 
+  /**
+   * Requires: this.isThrowPoint() || this.isEnterPoint()
+   * @return a name for the combined exit point
+   **/
+  public PptName makeThrowExit() {
+    assert isThrowPoint() || isEnterPoint() : fullname;
+    return new PptName(cls, method, FileIO.exception_suffix);
+  }
+
   /**
    * Requires: this.isExitPoint() || this.isEnterPoint()
    * @return a name for the corresponding object invariant
    **/
   public PptName makeObject() {
-    assert isExitPoint() || isEnterPoint() : fullname;
+    assert isExitPoint() || isEnterPoint() || isExceptionPoint() : fullname;
     return new PptName(cls, null, FileIO.object_suffix);
   }
 
@@ -431,7 +466,8 @@ public PptName makeObject() {
    * @return a name for the corresponding class-static invariant
    **/
   public PptName makeClassStatic() {
-    assert isExitPoint() || isEnterPoint() || isObjectInstanceSynthetic() : fullname;
+    assert isExitPoint() || isEnterPoint() || isObjectInstanceSynthetic() || isExceptionPoint()
+        : fullname;
     return new PptName(cls, null, FileIO.class_static_suffix);
   }
 

java/daikon/PptRelation.java

@@ -950,16 +950,30 @@ public static void init_hierarchy_new(PptMap all_ppts) {
       }
 
       // if an exitNN point, parent is combined exit point
-      if (ppt.is_subexit()) {
+      if (ppt.is_subexit() && pname.isExitPoint()) {
         PptTopLevel parent = all_ppts.get(pname.makeExit());
-        if (parent != null) rels.add(newCombinedExitExitNNRel(parent, ppt));
+        if (parent != null) {
+          rels.add(newCombinedExitExitNNRel(parent, ppt));
+        }
 
+        // if an throw[s] point, parent is combined Exception point
+      } else if (ppt.is_subexit() && pname.isExceptionPoint()) {
+        PptTopLevel parent = all_ppts.get(pname.makeThrowExit());
+        if (parent != null) {
+          rels.add(newCombinedExitExitNNRel(parent, ppt));
+        }
         // Connect combined exit points to enter points over orig variables
       } else if (ppt.is_combined_exit()) {
         PptTopLevel enter = all_ppts.get(pname.makeEnter());
         if (enter != null) {
           rels.add(PptRelation.newEnterExitRel(enter, ppt));
         }
+        // Connect combined exception points to enter points over orig variables
+      } else if (ppt.is_combined_exception()) {
+        PptTopLevel enter = all_ppts.get(pname.makeEnter());
+        if (enter != null) {
+          rels.add(PptRelation.newEnterExitRel(enter, ppt));
+        }
       }
 
       // Connect any conditional ppt variables.  Only connect to the

java/daikon/PptTopLevel.java

@@ -4393,6 +4393,12 @@ public void incSampleNumber() {
     }
   }
 
+  /** Is this is an exit ppt (combined or specific)? **/
+  /*@Pure*/ public boolean is_throw() {
+    if (type != null) return ((type == PptType.EXIT) || (type == PptType.SUBEXIT));
+    else return ppt_name.isThrowPoint();
+  }
+
   /** is this an enter ppt **/
   /*@Pure*/ public boolean is_enter() {
     if (type != null) {
@@ -4411,12 +4417,19 @@ public void incSampleNumber() {
     }
   }
 
+  /** Is this a combined exception point? **/
+  /*@Pure*/ public boolean is_combined_exception() {
+    if (type != null) return (type == PptType.EXIT);
+    else return ppt_name.isCombinedThrowPoint();
+  }
+
   /** Is this a numbered (specific) exit point? **/
   /*@Pure*/ public boolean is_subexit() {
     if (type != null) {
       return (type == PptType.SUBEXIT);
     } else {
-      return (ppt_name.isExitPoint() && !ppt_name.isCombinedExitPoint());
+      return ((ppt_name.isExitPoint() && !ppt_name.isCombinedExitPoint())
+          || (ppt_name.isThrowPoint()));
     }
   }