Merge pull request #4414 from owen-jones-diffblue/fix/must-not-throw-annotations

Fix MustNotThrow annotations and add invariant to avoid exception handling in __CPROVER_initialize

Author: tautschnig

jbmc/regression/jbmc/class-fields/java/lang/Class.class

@@ -4,6 +4,7 @@ public class Class {
 
   public Integer field;
 
+  @org.cprover.MustNotThrow
   protected void cproverNondetInitialize() {
     org.cprover.CProver.assume(field == null);
   }

jbmc/regression/jbmc/class-fields/java/lang/Class.java

@@ -0,0 +1,15 @@
+package org.cprover;
+
+public final class CProver
+{
+  public static final boolean enableAssume=true;
+
+  public static void assume(boolean condition)
+  {
+    if(enableAssume)
+    {
+      throw new RuntimeException(
+          "Cannot execute program with CProver.assume()");
+    }
+  }
+}

jbmc/regression/jbmc/class-fields/org/cprover/CProver.class

@@ -0,0 +1,8 @@
+package org.cprover;
+
+/**
+ * This can be added to methods to indicate they aren't allowed to throw
+ * exceptions. JBMC and related tools will truncate any execution path on which
+ * they do with an ASSUME FALSE instruction.
+ */
+public @interface MustNotThrow { }

jbmc/regression/jbmc/class-fields/org/cprover/CProver.java

@@ -12,6 +12,7 @@ public class Class {
   private boolean isMemberClass;
   private boolean isEnum;
 
+  @org.cprover.MustNotThrow
   public void cproverInitializeClassLiteral(
     String name,
     boolean isAnnotation,

jbmc/regression/jbmc/class-fields/org/cprover/MustNotThrow.class

@@ -0,0 +1,15 @@
+package org.cprover;
+
+public final class CProver
+{
+  public static final boolean enableAssume=true;
+
+  public static void assume(boolean condition)
+  {
+    if(enableAssume)
+    {
+      throw new RuntimeException(
+          "Cannot execute program with CProver.assume()");
+    }
+  }
+}

jbmc/regression/jbmc/class-fields/org/cprover/MustNotThrow.java

@@ -0,0 +1,8 @@
+package org.cprover;
+
+/**
+ * This can be added to methods to indicate they aren't allowed to throw
+ * exceptions. JBMC and related tools will truncate any execution path on which
+ * they do with an ASSUME FALSE instruction.
+ */
+public @interface MustNotThrow { }

jbmc/regression/jbmc/class-literals/java/lang/Class.class

@@ -30,6 +30,8 @@ Date:   December 2016
 
 #include <analyses/uncaught_exceptions_analysis.h>
 
+#include <linking/static_lifetime_init.h>
+
 #include "java_types.h"
 
 /// Lowers high-level exception descriptions into low-level operations suitable
@@ -119,6 +121,13 @@ class remove_exceptionst
   bool remove_added_instanceof;
   message_handlert &message_handler;
 
+  enum class instrumentation_resultt
+  {
+    DID_NOTHING,
+    ADDED_CODE_WITHOUT_MAY_THROW,
+    ADDED_CODE_WITH_MAY_THROW,
+  };
+
   symbol_exprt get_inflight_exception_global();
 
   bool function_or_callees_may_throw(const goto_programt &) const;
@@ -148,7 +157,7 @@ class remove_exceptionst
     const stack_catcht &,
     const std::vector<symbol_exprt> &);
 
-  bool instrument_function_call(
+  instrumentation_resultt instrument_function_call(
     const irep_idt &function_identifier,
     goto_programt &goto_program,
     const goto_programt::targett &,
@@ -207,7 +216,7 @@ bool remove_exceptionst::function_or_callees_may_throw(
 /// Translates an exception landing-pad into instructions that copy the
 /// in-flight exception pointer to a nominated expression, then clear the
 /// in-flight exception (i.e. null the pointer), hence marking it caught.
-/// \param goto_program: body of the function containing this landingpad
+/// \param [out] goto_program: body of the function containing this landingpad
 ///   instruction
 /// \param instr_it: iterator pointing to the landingpad instruction.
 ///   Will be overwritten.
@@ -421,7 +430,8 @@ bool remove_exceptionst::instrument_throw(
 
 /// instruments each function call that may escape exceptions with conditional
 /// GOTOS to the corresponding exception handlers
-bool remove_exceptionst::instrument_function_call(
+remove_exceptionst::instrumentation_resultt
+remove_exceptionst::instrument_function_call(
   const irep_idt &function_identifier,
   goto_programt &goto_program,
   const goto_programt::targett &instr_it,
@@ -455,6 +465,8 @@ bool remove_exceptionst::instrument_function_call(
       goto_program.insert_after(
         instr_it,
         goto_programt::make_assumption(no_exception_currently_in_flight));
+
+      return instrumentation_resultt::ADDED_CODE_WITHOUT_MAY_THROW;
     }
     else
     {
@@ -468,12 +480,12 @@ bool remove_exceptionst::instrument_function_call(
           next_it,
           no_exception_currently_in_flight,
           instr_it->source_location));
-    }
 
-    return true;
+      return instrumentation_resultt::ADDED_CODE_WITH_MAY_THROW;
+    }
   }
 
-  return false;
+  return instrumentation_resultt::DID_NOTHING;
 }
 
 /// instruments throws, function calls that may escape exceptions and exception
@@ -494,6 +506,7 @@ void remove_exceptionst::instrument_exceptions(
     function_or_callees_may_throw(goto_program);
 
   bool did_something = false;
+  bool added_goto_instruction = false;
 
   Forall_goto_program_instructions(instr_it, goto_program)
   {
@@ -577,16 +590,29 @@ void remove_exceptionst::instrument_exceptions(
     }
     else if(instr_it->type==THROW)
     {
-      did_something |= instrument_throw(
+      did_something = instrument_throw(
         function_identifier, goto_program, instr_it, stack_catch, locals);
     }
     else if(instr_it->type==FUNCTION_CALL)
     {
-      did_something |= instrument_function_call(
-        function_identifier, goto_program, instr_it, stack_catch, locals);
+      instrumentation_resultt result =
+        instrument_function_call(
+          function_identifier, goto_program, instr_it, stack_catch, locals);
+      did_something = result != instrumentation_resultt::DID_NOTHING;
+      added_goto_instruction =
+        result == instrumentation_resultt::ADDED_CODE_WITH_MAY_THROW;
     }
   }
 
+  // INITIALIZE_FUNCTION should not contain any exception handling branches for
+  // two reasons: (1) with symex-driven lazy loading it means that code that
+  // references @inflight_exception might be generated before
+  // @inflight_exception is initialized; (2) symex can analyze
+  // INITIALIZE_FUNCTION much faster if it doesn't contain any branching.
+  INVARIANT(
+    function_identifier != INITIALIZE_FUNCTION || !added_goto_instruction,
+    INITIALIZE_FUNCTION " should not contain any exception handling branches");
+
   if(did_something)
     remove_skip(goto_program);
 }