Merge pull request #5117 from romainbrenguier/experiment/never-throw

[TG-9400][UFC] Add an assume-no-exceptions-thrown option

Author: romainbrenguier

jbmc/regression/jbmc/assert-no-exceptions-thrown/MyException.class

@@ -0,0 +1,33 @@
+class MyException extends Exception {}
+
+public class Test {
+  public static int mayThrow(char branch) throws Throwable {
+    if (branch == 'n') {
+      throw new NullPointerException();
+    } else if (branch == 'c') {
+      throw new MyException();
+    } else if (branch == 't') {
+      throw new Throwable();
+    } else if (branch == 'r') {
+      return 2;
+    } else {
+      return 1;
+    }
+  }
+
+  public static void check(char branch) {
+    try {
+      int i = mayThrow(branch);
+      if (i == 2)
+        assert false;
+      if (i == 1)
+        assert false;
+    } catch (MyException e) {
+      assert false;
+    } catch (NullPointerException e) {
+      assert false;
+    } catch (Throwable e) {
+      assert false;
+    }
+  }
+}

jbmc/regression/jbmc/assert-no-exceptions-thrown/Test.class

@@ -0,0 +1,54 @@
+public class Thrower {
+  public static void test(Integer t) {
+    String ret = "";
+    if (t != null)
+      try {
+        switch (t) {
+        case 1:
+          ret = "CCE";
+          Object o = new Integer(0);
+          String x = ((String) o);
+          break;
+
+        case 2:
+          ret = "AIOBE";
+          int[] xs = new int[3];
+          t = xs[5];
+
+        case 3:
+          ret = "AE";
+          t = 5 / 0;
+
+        case 4:
+          ret = "NASE";
+          Integer[] arr = new Integer[-7];
+
+        case 5:
+          ret = "NPE";
+          String str = null;
+          str.toLowerCase();
+          
+        default:
+          break;
+        }
+      } catch (ClassCastException | NegativeArraySizeException
+               | NullPointerException | ArithmeticException
+               | ArrayIndexOutOfBoundsException e3) {
+
+        if (e3 instanceof ClassCastException)
+          assert ret.equals("CCE");
+
+        if (e3 instanceof NegativeArraySizeException)        
+          assert ret.equals("NASE");
+
+        if (e3 instanceof NullPointerException)
+          assert ret.equals("NPE");
+       
+        if (e3 instanceof ArithmeticException)
+          assert ret.equals("AE");
+
+        if (e3 instanceof ArrayIndexOutOfBoundsException)
+          assert ret.equals("AIOBE");
+      }
+  }
+}

jbmc/regression/jbmc/assert-no-exceptions-thrown/Test.java

@@ -0,0 +1,14 @@
+CORE
+Thrower.class
+--function Thrower.test --assert-no-exceptions-thrown --throw-runtime-exceptions
+line 39 assertion at file Thrower.java line 39 .*: FAILURE
+line 42 assertion at file Thrower.java line 42 .*: FAILURE
+line 45 assertion at file Thrower.java line 45 .*: FAILURE
+line 48 assertion at file Thrower.java line 48 .*: FAILURE
+line 51 assertion at file Thrower.java line 51 .*: FAILURE
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+Checks that the runtime exceptions still throw with `--throw-runtime-exceptions`
+even when `--assert-no-exceptions-thrown` is specified.

jbmc/regression/jbmc/assert-no-exceptions-thrown/Thrower.class

@@ -0,0 +1,14 @@
+CORE
+Test.class
+--function Test.check
+line 22 assertion at file Test.java line 22 .*: FAILURE
+line 24 assertion at file Test.java line 24 .*: FAILURE
+line 26 assertion at file Test.java line 26 .*: FAILURE
+line 28 assertion at file Test.java line 28 .*: FAILURE
+line 30 assertion at file Test.java line 30 .*: FAILURE
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+Checks that we get the expected behaviour when --assert-no-exceptions-thrown is
+not used. This is to make sure that test.desc is actually testing what we wanted.

jbmc/regression/jbmc/assert-no-exceptions-thrown/Thrower.java

@@ -0,0 +1,18 @@
+CORE
+Test.class
+--function Test.check --assert-no-exceptions-thrown
+line 6 assertion at file Test.java line 6 .*: FAILURE
+line 8 assertion at file Test.java line 8 .*: FAILURE
+line 10 assertion at file Test.java line 10 .*: FAILURE
+line 22 assertion at file Test.java line 22 .*: FAILURE
+line 24 assertion at file Test.java line 24 .*: FAILURE
+line 26 assertion at file Test.java line 26 .*: SUCCESS
+line 28 assertion at file Test.java line 28 .*: SUCCESS
+line 30 assertion at file Test.java line 30 .*: SUCCESS
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+Checks that the `throw` instructions have been replaced by assertions, which
+are failing here because they are reachable, and assumptions which prevent
+the last three assertions from failing.

jbmc/regression/jbmc/assert-no-exceptions-thrown/test-thrower.desc

@@ -666,12 +666,12 @@ and the methods in them. The methods, along with their parsed representation
 \ref java_bytecode_languaget::method_bytecode via a reference held in
 \ref java_bytecode_convert_classt::method_bytecode. typecheck then performs a
 switch over the value of
-[lazy_methods_mode](\ref java_bytecode_languaget::lazy_methods_mode) to
+[lazy_methods_mode](\ref java_bytecode_language_optionst::lazy_methods_mode) to
 determine which loading strategy to use.
 
 \subsection eager-loading Eager loading
 
-If [lazy_methods_mode](\ref java_bytecode_languaget::lazy_methods_mode) is
+If [lazy_methods_mode](\ref java_bytecode_language_optionst::lazy_methods_mode) is
 \ref java_bytecode_languaget::LAZY_METHODS_MODE_EAGER then eager loading is
 used. Under eager loading
 \ref java_bytecode_languaget::convert_single_method(const irep_idt &, symbol_table_baset &, lazy_class_to_declared_symbols_mapt &)
@@ -695,7 +695,7 @@ method parameters) and function references (at function call sites) to
 locate further classes and methods to load. The following paragraph describes
 the mechanism used.
 
-If [lazy_methods_mode](\ref java_bytecode_languaget::lazy_methods_mode) is
+If [lazy_methods_mode](\ref java_bytecode_language_optionst::lazy_methods_mode) is
 \ref lazy_methods_modet::LAZY_METHODS_MODE_CONTEXT_INSENSITIVE then
 context-insensitive lazy loading is used. Under this stragegy
 \ref java_bytecode_languaget::do_ci_lazy_method_conversion is called to do all

jbmc/regression/jbmc/assert-no-exceptions-thrown/test-with-throw.desc

@@ -2349,9 +2349,10 @@ void java_bytecode_convert_methodt::convert_athrow(
   exprt::operandst &results) const
 {
   if(
-    !throw_assertion_error &&
-    uncaught_exceptions_domaint::get_exception_type(op[0].type()) ==
-      "java::java.lang.AssertionError")
+    assert_no_exceptions_thrown ||
+    ((uncaught_exceptions_domaint::get_exception_type(op[0].type()) ==
+      "java::java.lang.AssertionError") &&
+     !throw_assertion_error))
   {
     // we translate athrow into
     // ASSERT false;
@@ -3190,7 +3191,8 @@ void java_bytecode_convert_method(
   java_string_library_preprocesst &string_preprocess,
   const class_hierarchyt &class_hierarchy,
   bool threading_support,
-  const optionalt<prefix_filtert> &method_context)
+  const optionalt<prefix_filtert> &method_context,
+  bool assert_no_exceptions_thrown)
 
 {
   java_bytecode_convert_methodt java_bytecode_convert_method(
@@ -3201,7 +3203,8 @@ void java_bytecode_convert_method(
     needed_lazy_methods,
     string_preprocess,
     class_hierarchy,
-    threading_support);
+    threading_support,
+    assert_no_exceptions_thrown);
 
   java_bytecode_convert_method(class_symbol, method, method_context);
 }

jbmc/regression/jbmc/assert-no-exceptions-thrown/test.desc

@@ -39,7 +39,8 @@ void java_bytecode_convert_method(
   java_string_library_preprocesst &string_preprocess,
   const class_hierarchyt &class_hierarchy,
   bool threading_support,
-  const optionalt<prefix_filtert> &method_context);
+  const optionalt<prefix_filtert> &method_context,
+  bool assert_no_exceptions_thrown);
 
 void create_method_stub_symbol(
   const irep_idt &identifier,

jbmc/src/java_bytecode/README.md

@@ -40,12 +40,14 @@ class java_bytecode_convert_methodt:public messaget
     optionalt<ci_lazy_methods_neededt> needed_lazy_methods,
     java_string_library_preprocesst &_string_preprocess,
     const class_hierarchyt &class_hierarchy,
-    bool threading_support)
+    bool threading_support,
+    bool assert_no_exceptions_thrown)
     : messaget(_message_handler),
       symbol_table(symbol_table),
       ns(symbol_table),
       max_array_length(_max_array_length),
       throw_assertion_error(throw_assertion_error),
+      assert_no_exceptions_thrown(assert_no_exceptions_thrown),
       threading_support(threading_support),
       needed_lazy_methods(std::move(needed_lazy_methods)),
       string_preprocess(_string_preprocess),
@@ -76,6 +78,7 @@ class java_bytecode_convert_methodt:public messaget
   namespacet ns;
   const size_t max_array_length;
   const bool throw_assertion_error;
+  const bool assert_no_exceptions_thrown;
   const bool threading_support;
   optionalt<ci_lazy_methods_neededt> needed_lazy_methods;