Add org.cprover.MustNotThrow method attribute

This asserts that a particular method must not throw exceptions, intended for use with
internal methods such as cproverNondetInitialize, which must not propagate exceptions to
their callsite. In such a case, instead of an exception dispatch table we introduce an
assumption checking one was not in fact thrown.

Author: smowton

jbmc/regression/jbmc/must-not-throw-annotation/Test.class

@@ -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;
+    }
+  }
+
+}

jbmc/regression/jbmc/must-not-throw-annotation/Test.java

@@ -0,0 +1,3 @@
+package org.cprover;
+
+public @interface MustNotThrow { }

jbmc/regression/jbmc/must-not-throw-annotation/org/cprover/MustNotThrow.class

@@ -0,0 +1,8 @@
+CORE
+Test.class
+--function Test.main
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

jbmc/regression/jbmc/must-not-throw-annotation/org/cprover/MustNotThrow.java

@@ -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);
 }
 

jbmc/regression/jbmc/must-not-throw-annotation/test.desc

@@ -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;
   }

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

@@ -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