Exception exit support

doc/CHANGES

@@ -20,6 +20,14 @@ Further documentation can be found in:
 
 ===========================================================================
 
+Chicory:
+- We now instrument exceptional exits.  That means that Daikon is able
+  to infer invariants about when a Java method throws an exception.
+
+===========================================================================
+
+5.6.8 (?, ?, 2018)
+
 Daikon no longer uses the plume-lib repository, but smaller ones such as
 plume-scripts.
 

doc/daikon.dict

@@ -1,6 +1,7 @@
 ABI
 accessor
 accessors
+acyclic
 ADDR
 AFS
 AMD

doc/daikon.texinfo

@@ -2077,6 +2077,17 @@ source rather than a single location.  This concept is represented in
 Daikon by the dataflow hierarchy, see
 @ref{Dataflow hierarchy,,,developer,Daikon Developer Manual}.
 
+@cindex :::EXCEPTION program point
+@cindex EXCEPTION program point
+
+In a similar manner, @code{foo():::EXCEPTION} is the program point that
+represents all the procedure's exceptional exits,
+and invariants there are postconditions.  When there are multiple
+exception exits from a procedure (for instance, because of multiple
+@code{throw} statements), the different exits are differentiated by
+suffixing them with their line numbers; for instance,
+@code{StackAr.top():::EXCEPTION59}.
+
 The Java instrumenter Chicory selects names for program
 points that include an indication of the argument and return types for
 each method.  These signatures are presented in @code{Class.getName} format: one
@@ -2247,10 +2258,12 @@ Static variables of a class have names of the form
 @cindex pre-state variables
 @code{orig(x)} refers to the value of variable @code{x} upon
 entry to a procedure (because the procedure body might modify the value
-of @code{x}).  These variables appear only at @code{:::EXIT} program
+of @code{x}).  These variables appear only at @code{:::EXIT} and
+@code{:::EXCEPTION} program
 points.  Typically, @code{orig()} variables do not appear in the trace,
 but are automatically created by Daikon when it matches up
-@code{:::ENTER} and @code{:::EXIT@var{nn}} program points.
+a @code{:::ENTER} with a @code{:::EXIT@var{nn}}
+or with a @code{:::EXCEPTION@var{nn}} program point.
 @xref{orig variable example}.
 
 This variable prints as @code{orig} when using Daikon output format
@@ -7989,15 +8002,15 @@ answer is 0, but you believe that there are samples in the file you are
 feeding to Daikon.
 
 Using the normal dataflow hierarchy, Daikon explicitly processes
-@code{:::EXIT} program points only.  Other program points, such as
+@code{:::EXIT} and @code{:::EXCEPTION} program points only. Other program points, such as
 @code{:::ENTER} program points, are processed indirectly when their
-corresponding @code{:::EXIT} points are encountered.
+corresponding @code{:::EXIT} or @code{:::EXCEPTION} points are encountered.
 (You can disable this behavior with the
 @option{--nohierarchy} switch to Daikon;
 see @ref{Options to control invariant detection}.)
-If no @code{:::EXIT} program points are present (perhaps every
+If no @code{:::EXIT} or @code{:::EXCEPTION} program points are present (perhaps every
 execution threw an exception, you filtered out all the
-@code{:::EXIT} program points, or the data trace is obtained from
+@code{:::EXIT} and @code{:::EXCEPTION} program points, or the data trace is obtained from
 spreadsheet data instead of from a program execution),
 then Daikon will not process any of the other program points, such as
 the @code{:::ENTER} program points.  You can make Daikon print information
@@ -9179,6 +9192,7 @@ Florian Gross,
 Philip Guo,
 Melissa Hao,
 Michael Harder,
+Philipp Hirch,
 Dieter von Holten,
 Greg Jay,
 Josh Kataoka,

doc/developer.texinfo

@@ -1241,21 +1241,42 @@ at which they apply.
 @c points are related to the @samp{orig} versions at @code{:::EXIT} program points.
 
 @ref{Program point declarations} describe how program points are
-declared in a Daikon input file. Here we will describe how the
-@code{parent} records are typically used to connect program points into
-a dataflow hierarchy.
+declared in a Daikon input file.
+Note that Daikon creates additional, internal program points
+that do not appear in a input trace file generated by a front end, such as Chicory.
+In particular, it creates a common (aka combined) @code{EXIT} point that is the parent of all
+@code{EXIT<id>} program points in a method and a common (aka combined) @code{EXCEPTION}
+point that is the parent of all @code{EXCPETION<id>} and @code{EXCEPTIONUNCAUGHT}
+program points in a method.
+
+Daikon uses three primary relationship types
+(@code{PARENT}, @code{ENTER-EXIT} and @code{EXIT-EXITNN}) to connect the program points
+into an acyclic dataflow hierarchy.
 
 @itemize
 @item
-A program point that represents the @code{ENTRY} or @code{EXIT} of a
+A program point that represents the @code{ENTRY}, @code{EXCEPTION} or @code{EXIT} of a
 static method will have a @code{parent} record that points to the
 @code{CLASS} program point for the containing class.
 
 @item
-A program point that represents the @code{ENTRY} or @code{EXIT} of a
+A program point that represents the @code{ENTRY}, @code{EXCEPTION} or @code{EXIT} of a
 non-static (instance) method will have a @code{parent} record that points to the
 @code{OBJECT} program point for the containing object.
 
+@item
+An @code{ENTER-EXIT} edge connects each method's @code{ENTER} program
+point with its corresponding @code{EXCEPTION} and @code{EXIT} program points.
+
+@item
+An @code{EXIT-EXITNN} edge connects each method's @code{EXIT} program
+point with each of its corresponding @code{EXIT<id>} program points.
+
+@item
+An @code{EXIT-EXITNN} edge connects each method's @code{EXCEPTION} program
+point with each of its corresponding @code{EXCEPTION<id>} and @code{EXCEPTIONUNCAUGHT}
+program points.
+
 @item
 A program point that represents a @code{CLASS}
 will usually not have a @code{parent} record.
@@ -1271,7 +1292,7 @@ hierarchy may result in some true invariants that are not reported at
 some program points.  However, the invariant will be present in some
 parent program point.  The dataflow hierarchy is used by default, but
 can be disabled by the @option{--nohierarchy} flag.  When dataflow is enabled,
-the only samples that are examined by Daikon are the @code{:::EXIT} program
+the only samples that are examined by Daikon are the @code{:::EXIT} and @code{:::EXCEPTION} program
 points (plus @samp{orig} variables) since these contain a complete view of
 the data, from which invariants at all other locations can be inferred.
 For example, Daikon does not need to examine data at @code{:::ENTER} or
@@ -3173,16 +3194,23 @@ Program point names must be distinct.
 
 While Daikon does not infer program point relationships from @code{ppt-name}s,
 it does require these names to conform to a set syntax.
-The following patterns are for the @code{enter}, @code{subexit},
+The following patterns are for the @code{enter},
 @code{class} and @code{object} @code{ppt-type}s, respectively.
 
 @example
 <fully qualified class name>.<method/function name>(<argument types>):::ENTER
-<fully qualified class name>.<method/function name>(<argument types>):::EXIT<id>
 <fully qualified class name>:::CLASS
 <fully qualified class name>:::OBJECT
 @end example
 
+The @code{subexit} @code{ppt-type} may have one of three patterns:
+
+@example
+<fully qualified class name>.<method/function name>(<argument types>):::EXIT<id>
+<fully qualified class name>.<method/function name>(<argument types>):::EXCEPTION<id>
+<fully qualified class name>.<method/function name>(<argument types>):::EXCEPTIONUNCAUGHT
+@end example
+
 @noindent
 Since in most languages a method or function may have multiple exit points,
 the @code{ppt-name} for a @code{subexit} @code{ppt-type} must be appended

java/daikon/AnnotateNullable.java

@@ -107,9 +107,8 @@ 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)) {
+      if (!ppt.is_combined_exit() || !ppt.is_combined_exception() || !is_static_method(ppt))
         continue;
-      }
 
       String name = ppt.name().replaceFirst("[(].*$", "");
       int lastdot = name.lastIndexOf('.');
@@ -344,7 +343,11 @@ public static void process_method(PptTopLevel ppt) {
       System.out.printf("); // %d samples%n", ppt.num_samples());
     } else {
       System.out.printf("  method %s : // %d samples%n", jvm_signature(ppt), ppt.num_samples());
-      System.out.printf("    return: %s%n", return_annotation);
+      if (return_annotation != "") {
+        System.out.printf("    return: %s%n", return_annotation);
+      } else {
+        System.out.printf("    return:%n");
+      }
       for (int i = 0; i < params.size(); i++) {
         // Print the annotation for this parameter
         System.out.printf("    parameter #%d : %s // %s%n", i, annos.get(i), names.get(i));
@@ -413,6 +416,14 @@ public static String jvm_signature(PptTopLevel ppt) {
     // returnVar is non-null), because we are processing a Java program
     String returnType =
         returnVar == null ? "V" : JvmUtil.binaryNameToFieldDescriptor(returnVar.type.toString());
+    // Or an throw point
+    if (returnVar == null) {
+      returnVar = ppt.find_var_by_name("exception");
+      returnType =
+          returnVar == null
+              ? "V"
+              : "V throws " + JvmUtil.binaryNameToFieldDescriptor(returnVar.type.toString());
+    }
 
     return method + JvmUtil.arglistToJvm(java_args) + returnType;
   }

java/daikon/Chicory.java

@@ -130,6 +130,9 @@ public class Chicory {
   @Option("Number of calls after which sampling will begin")
   public static int sample_start = 0;
 
+  @Option("Enable remote debug")
+  public static boolean remote_debug = false;
+
   /** Daikon port number. Daikon writes this to stdout when it is started in online mode. */
   private static int daikon_port = -1;
 
@@ -152,8 +155,6 @@ 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;
-
   /** Flag to initiate a purity analysis and use results to create add vars */
   private static boolean purityAnalysis = false;
 
@@ -376,9 +377,10 @@ void start_target(String premain_args, String[] target_args) {
     List<String> cmdlist = new ArrayList<String>();
     cmdlist.add("java");
 
-    if (RemoteDebug) {
+    if (remote_debug) {
       // -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");
     }
@@ -498,6 +500,11 @@ public void runDaikon() {
               heap_size, cp, daikon_args, output_dir, dtrace_file);
     }
 
+    if (remote_debug) {
+      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

@@ -1646,7 +1646,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.isExitPoint()) {
+        exit_name = ppt.ppt_name.makeExit();
+      } else {
+        exit_name = ppt.ppt_name.makeExceptionExit();
+      }
       PptTopLevel exit_ppt = exit_ppts.get(exit_name);
 
       if (debugInit.isLoggable(Level.FINE)) {
@@ -1733,7 +1738,7 @@ static List<Invariant> filter_invs(List<Invariant> invs) {
    * 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 {
@@ -2321,8 +2326,8 @@ 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.isCombinedExceptionPoint()
           || p.ppt_name.isEnterPoint()
-          || p.ppt_name.isThrowsPoint()
           || p.ppt_name.isObjectInstanceSynthetic()
           || p.ppt_name.isClassStaticSynthetic()) {
         return;

java/daikon/FileIO.java

@@ -69,14 +69,20 @@ private FileIO() {
 
   // Program point name tags
   public static final String ppt_tag_separator = ":::";
-  public static final String enter_suffix = "ENTER";
-  public static final String enter_tag = ppt_tag_separator + enter_suffix;
+  public static final String entry_suffix = "ENTER";
+  public static final String entry_tag = ppt_tag_separator + entry_suffix;
   // EXIT does not necessarily appear at the end of the program point name;
   // 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 throws_suffix = "THROWS";
-  public static final String throws_tag = ppt_tag_separator + throws_suffix;
+  // public static final String throw_suffix = "THROW";
+  // public static final String throw_tag = ppt_tag_separator + throw_suffix;
+  public static final String exception_uncaught_suffix = "EXCEPTIONUNCAUGHT";
+  public static final String exception_uncaught_tag = ppt_tag_separator + exception_uncaught_suffix;
+  // EXCEPTION does not necessarily appear at the end of the program point name;
+  // a number may follow it.
+  public static final String exception_suffix = "EXCEPTION";
+  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";
@@ -1013,8 +1019,8 @@ 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.isObjectInstanceSynthetic()
               || ppt_top_level.ppt_name.isClassStaticSynthetic()
               || ppt_top_level.ppt_name.isGlobalPoint());
@@ -1722,9 +1728,9 @@ public static void process_sample(
       //  and :::CLASS program points.  This scheme ensures that arbitrarly
       //  named program points such as :::POINT (used by convertcsv.pl)
       //  will be treated as leaves.
+      //  Throws is a LEAF now, like Exit_nn
 
       if (ppt.ppt_name.isEnterPoint()
-          || ppt.ppt_name.isThrowsPoint()
           || ppt.ppt_name.isObjectInstanceSynthetic()
           || ppt.ppt_name.isClassStaticSynthetic()
           || ppt.ppt_name.isGlobalPoint()) {
@@ -1736,6 +1742,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.isCombinedExceptionPoint()) {
+        // 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
@@ -2161,7 +2173,7 @@ public static boolean compute_orig_variables(
     VarInfo[] vis = ppt.var_infos;
     /*@Interned*/ String fn_name = ppt.ppt_name.getNameWithoutPoint();
     String ppt_name = ppt.name();
-    if (ppt_name.endsWith(enter_tag)) {
+    if (ppt_name.endsWith(entry_tag)) {
       Invocation invok = new Invocation(ppt, vals, mods);
       if (nonce == null) {
         call_stack.push(invok);
@@ -2171,7 +2183,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

@@ -267,12 +267,12 @@ public static void mainHelper(String[] args)
     debugProgress.fine("Building hierarchy between leaves of the maps");
     for (PptTopLevel ppt : merge_ppts.pptIterable()) {
 
-      // Skip everything that is not a final exit point
-      if (!ppt.ppt_name.isExitPoint()) {
+      // Skip everything that is not a final exit or exception point
+      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.isCombinedExceptionPoint()) {
         assert ppt.children.size() > 0 : ppt;
         continue;
       }
@@ -382,12 +382,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()) {
+
+      if (!ppt.ppt_name.isExitPoint() && !ppt.ppt_name.isExceptionPoint()) {
         continue;
       }
-      if (ppt.ppt_name.isCombinedExitPoint()) {
+      if (ppt.ppt_name.isCombinedExitPoint() || ppt.ppt_name.isCombinedExceptionPoint()) {
         continue;
       }
+
       ppt.children.clear();
       for (PptConditional cond : ppt.cond_iterable()) {
         cond.children.clear();