diffblue · smowton · Jun 12, 2018 · Jun 7, 2018 · thk123 · Jun 8, 2018
diff --git a/jbmc/regression/jbmc/must-not-throw-annotation/Test.class b/jbmc/regression/jbmc/must-not-throw-annotation/Test.class
diff --git a/jbmc/regression/jbmc/must-not-throw-annotation/Test.java b/jbmc/regression/jbmc/must-not-throw-annotation/Test.java
@@ -0,0 +1,17 @@
+public class Test {
+
+  @org.cprover.MustNotThrow
+  public static void mustNotThrow() {
+    throw new RuntimeException("Oh dear");
+  }
+
+  public static void main() {
+    try {
+      mustNotThrow();
+    }
+    catch(Throwable e) {
+      assert false;
+    }
+  }
+
+}
diff --git a/jbmc/regression/jbmc/must-not-throw-annotation/org/cprover/MustNotThrow.class b/jbmc/regression/jbmc/must-not-throw-annotation/org/cprover/MustNotThrow.class
diff --git a/jbmc/regression/jbmc/must-not-throw-annotation/org/cprover/MustNotThrow.java b/jbmc/regression/jbmc/must-not-throw-annotation/org/cprover/MustNotThrow.java
@@ -0,0 +1,3 @@
+package org.cprover;
+
+public @interface MustNotThrow { }
diff --git a/jbmc/regression/jbmc/must-not-throw-annotation/test.desc b/jbmc/regression/jbmc/must-not-throw-annotation/test.desc
@@ -0,0 +1,8 @@
+CORE
+Test.class
+--function Test.main
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
@@ -406,6 +406,13 @@ void java_bytecode_convert_method_lazy(
   // Not used in jbmc at present, but other codebases that use jbmc as a library
   // use this information.
   method_symbol.type.set(ID_C_abstract, m.is_abstract);
+
+  if(java_bytecode_parse_treet::find_annotation(
+       m.annotations, "java::org.cprover.MustNotThrow"))
+  {
+    method_symbol.type.set(ID_C_must_not_throw, true);
+  }
+
   symbol_table.add(method_symbol);
 }
 

@@ -432,19 +432,29 @@ bool remove_exceptionst::instrument_function_call(
 
   if(function_may_throw(callee_id))
   {
-    add_exception_dispatch_sequence(
-      goto_program, instr_it, stack_catch, locals);
-
-    // add a null check (so that instanceof can be applied)
-    equal_exprt eq_null(
+    equal_exprt no_exception_currently_in_flight(
       get_inflight_exception_global(),
       null_pointer_exprt(pointer_type(empty_typet())));
 
-    goto_programt::targett t_null=goto_program.insert_after(instr_it);
-    t_null->make_goto(next_it);
-    t_null->source_location=instr_it->source_location;
-    t_null->function=instr_it->function;
-    t_null->guard=eq_null;
+    if(symbol_table.lookup_ref(callee_id).type.get_bool(ID_C_must_not_throw))
+    {
+      // Function is annotated must-not-throw, but we can't prove that here.
+      // Insert an ASSUME(@inflight_exception == null):
+      goto_programt::targett assume_null = goto_program.insert_after(instr_it);
+      assume_null->make_assumption(no_exception_currently_in_flight);
+    }
+    else
+    {
+      add_exception_dispatch_sequence(
+        goto_program, instr_it, stack_catch, locals);
+
+      // add a null check (so that instanceof can be applied)
+      goto_programt::targett t_null=goto_program.insert_after(instr_it);
+      t_null->make_goto(next_it);
+      t_null->source_location=instr_it->source_location;
+      t_null->function=instr_it->function;
+      t_null->guard=no_exception_currently_in_flight;
+    }
 
     return true;
   }

diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def
@@ -670,6 +670,7 @@ IREP_ID_ONE(bits_per_byte)
 IREP_ID_TWO(C_abstract, #abstract)
 IREP_ID_ONE(synthetic)
 IREP_ID_ONE(interface)
+IREP_ID_TWO(C_must_not_throw, #must_not_throw)
 
 // Projects depending on this code base that wish to extend the list of
 // available ids should provide a file local_irep_ids.h in their source tree and
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1,3 @@
		package org.cprover;

		public @interface MustNotThrow { }
Copy link Contributor thk123 Jun 8, 2018 Choose a reason for hiding this comment The reason will be displayed to describe this comment to others. Learn more. Shouldn't this go in an actual org.cprover package? Does such a thing exist? Copy link Contributor Author smowton Jun 8, 2018 Choose a reason for hiding this comment The reason will be displayed to describe this comment to others. Learn more. It will, but this is just a test that if such a thing exists then it functions as intended. It's a "mini models library" if you like. Copy link Member peterschrammel Jun 8, 2018 Choose a reason for hiding this comment The reason will be displayed to describe this comment to others. Learn more. The 'mini models library' is here: https://github.com/diffblue/java-models-library/tree/master/src/main/java/org/cprover Please add it there. It will then be compiled into the org.cprover.jar Copy link Member peterschrammel Jun 8, 2018 Choose a reason for hiding this comment The reason will be displayed to describe this comment to others. Learn more. And additionally, it should also be duplicated in models-library (until models-library moves to extending java-models-library). Copy link Contributor Author smowton Jun 8, 2018 Choose a reason for hiding this comment The reason will be displayed to describe this comment to others. Learn more. Huh? That's the real models lib, isn't it? My intent was to submit this to get the functionality in (with a minimal test that doesn't use the models lib, but just mocks up the relevant interface), then ask @allredj for the actual lib support. Copy link Contributor thk123 Jun 8, 2018 Choose a reason for hiding this comment The reason will be displayed to describe this comment to others. Learn more. Where's the cycle? Repo one: `org.cprover`, repo two: `core-models` depends on `org.cprover`. No need for `org.cprover` to know about the core models? Copy link Member peterschrammel Jun 8, 2018 Choose a reason for hiding this comment The reason will be displayed to describe this comment to others. Learn more. If you put it into its own repo then there is no cycle. Copy link Member peterschrammel Jun 8, 2018 • edited Loading Choose a reason for hiding this comment The reason will be displayed to describe this comment to others. Learn more. Let's create a separate repo then. As @thk123 suggested, it might even make sense to put it on Maven Central repo, which avoids having a submodule in models-library and also makes it easier to use for JBMC users who want to hack their own models and harnesses. Copy link Contributor thk123 Jun 11, 2018 Choose a reason for hiding this comment The reason will be displayed to describe this comment to others. Learn more. For the avoidance of doubt - this is out of scope for this PR right @peterschrammel? This is fine for now, and can be tidied up when the new repo is created? Copy link Member peterschrammel Jun 11, 2018 Choose a reason for hiding this comment The reason will be displayed to describe this comment to others. Learn more. Yes.