Refactor user-defined assertion translation for Java

peterschrammel · peterschrammel · commit 07acde40b451 · 2018-06-14T09:46:29.000+01:00
Assertions in Java are "throw a;" statements where
a is of type java.lang.AssertionError (an exception,
or Throwable, to be precise). Sometimes we want to
translate it into an ASSERT instruction in the goto
program. Special-casing in order to  handle that
was scattered across multiple classes. In this commit
we special-case it only once in the Java frontend
and translate it into assert(false); assume(false);
which is then correctly handled by later stages of the
translation.
diff --git a/jbmc/regression/jbmc-strings/max-length/test1.desc b/jbmc/regression/jbmc-strings/max-length/test1.desc
@@ -3,4 +3,4 @@ Test.class
 --refine-strings --verbosity 10 --string-max-input-length 499999 --function Test.checkMaxInputLength
 ^EXIT=0$
 ^SIGNAL=0$
-assertion.* line 9 function java::Test.checkMaxInputLength.* bytecode-index 16: SUCCESS
+assertion.* line 9 function java::Test.checkMaxInputLength.* bytecode-index 17: SUCCESS
diff --git a/jbmc/regression/jbmc-strings/max-length/test2.desc b/jbmc/regression/jbmc-strings/max-length/test2.desc
@@ -3,4 +3,4 @@ Test.class
 --refine-strings --verbosity 10 --string-max-input-length 500000 --function Test.checkMaxInputLength
 ^EXIT=10$
 ^SIGNAL=0$
-assertion.* line 9 function java::Test.checkMaxInputLength.* bytecode-index 16: FAILURE
+assertion.* line 9 function java::Test.checkMaxInputLength.* bytecode-index 17: FAILURE
diff --git a/jbmc/regression/jbmc-strings/max-length/test3.desc b/jbmc/regression/jbmc-strings/max-length/test3.desc
@@ -3,4 +3,4 @@ Test.class
 --refine-strings --verbosity 10 --string-max-length 4001 --function Test.checkMaxLength
 ^EXIT=10$
 ^SIGNAL=0$
-assertion.* line 25 function java::Test.checkMaxLength.* bytecode-index 26: FAILURE
+assertion.* line 25 function java::Test.checkMaxLength.* bytecode-index 27: FAILURE
diff --git a/jbmc/regression/jbmc/assert7/Test.class b/jbmc/regression/jbmc/assert7/Test.class
diff --git a/jbmc/regression/jbmc/assert7/Test.java b/jbmc/regression/jbmc/assert7/Test.java
@@ -0,0 +1,9 @@
+class Test
+{
+  public static void main(String[] args)
+  {
+    AssertionError a = new AssertionError();
+    if(false)
+      throw a;
+  }
+}
diff --git a/jbmc/regression/jbmc/assert7/test.desc b/jbmc/regression/jbmc/assert7/test.desc
@@ -0,0 +1,8 @@
+CORE
+Test.class
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/jbmc/regression/jbmc/exceptions23/test.desc b/jbmc/regression/jbmc/exceptions23/test.desc
@@ -4,7 +4,7 @@ test.class
 ^EXIT=10$
 ^SIGNAL=0$
 VERIFICATION FAILED
-assertion at file test\.java line 9 function java::test\.main:\(\)V bytecode-index 12: FAILURE
+assertion at file test\.java line 9 function java::test\.main:\(\)V bytecode-index 13: FAILURE
 --
 ^warning: ignoring
 --
diff --git a/jbmc/regression/jbmc/exceptions24/test.desc b/jbmc/regression/jbmc/exceptions24/test.desc
@@ -4,7 +4,7 @@ test.class
 ^EXIT=10$
 ^SIGNAL=0$
 VERIFICATION FAILED
-assertion at file test\.java line 9 function java::test\.main:\(\)V bytecode-index 10: FAILURE
+assertion at file test\.java line 9 function java::test\.main:\(\)V bytecode-index 11: FAILURE
 --
 ^warning: ignoring
 --
diff --git a/jbmc/regression/jbmc/finally1/test.desc b/jbmc/regression/jbmc/finally1/test.desc
@@ -3,7 +3,7 @@ test.class
 --function test.main
 ^EXIT=10$
 ^SIGNAL=0$
-assertion at file test\.java line 7 function java::test\.main:\(\)V bytecode-index 9: FAILURE
+assertion at file test\.java line 7 function java::test\.main:\(\)V bytecode-index 10: FAILURE
 ^VERIFICATION FAILED$
 --
 ^warning: ignoring
diff --git a/jbmc/regression/jbmc/finally2/test.desc b/jbmc/regression/jbmc/finally2/test.desc
@@ -3,7 +3,7 @@ test.class
 --function test.main
 ^EXIT=10$
 ^SIGNAL=0$
-assertion at file test\.java line 8 function java::test\.main:\(\)V bytecode-index 9: FAILURE
+assertion at file test\.java line 8 function java::test\.main:\(\)V bytecode-index 10: FAILURE
 ^VERIFICATION FAILED$
 --
 ^warning: ignoring
diff --git a/jbmc/regression/jbmc/finally3/test.desc b/jbmc/regression/jbmc/finally3/test.desc
@@ -3,8 +3,8 @@ test.class
 --function test.main
 ^EXIT=10$
 ^SIGNAL=0$
-assertion at file test\.java line 7 function java::test\.main:\(\)V bytecode-index 9: SUCCESS
-assertion at file test\.java line 10 function java::test\.main:\(\)V bytecode-index 22: FAILURE
+assertion at file test\.java line 7 function java::test\.main:\(\)V bytecode-index 10: SUCCESS
+assertion at file test\.java line 10 function java::test\.main:\(\)V bytecode-index 23: FAILURE
 ^VERIFICATION FAILED$
 --
 ^warning: ignoring
diff --git a/jbmc/regression/jbmc/finally4/test.desc b/jbmc/regression/jbmc/finally4/test.desc
@@ -3,7 +3,7 @@ test.class
 --function test.main
 ^EXIT=10$
 ^SIGNAL=0$
-assertion at file test\.java line 11 function java::test\.main:\(\)V bytecode-index 7: FAILURE
+assertion at file test\.java line 11 function java::test\.main:\(\)V bytecode-index 8: FAILURE
 ^VERIFICATION FAILED$
 --
 ^warning: ignoring
diff --git a/jbmc/regression/jbmc/finally5/test.desc b/jbmc/regression/jbmc/finally5/test.desc
@@ -3,7 +3,7 @@ test.class
 --function test.main
 ^EXIT=10$
 ^SIGNAL=0$
-assertion at file test\.java line 7 function java::test\.main:\(\)V bytecode-index 12: FAILURE
+assertion at file test\.java line 7 function java::test\.main:\(\)V bytecode-index 13: FAILURE
 ^VERIFICATION FAILED$
 --
 ^warning: ignoring
diff --git a/jbmc/regression/jbmc/finally6/test.desc b/jbmc/regression/jbmc/finally6/test.desc
@@ -3,7 +3,7 @@ test.class
 --function test.main
 ^EXIT=10$
 ^SIGNAL=0$
-assertion at file test\.java line 8 function java::test\.main:\(\)V bytecode-index 12: FAILURE
+assertion at file test\.java line 8 function java::test\.main:\(\)V bytecode-index 13: FAILURE
 ^VERIFICATION FAILED$
 --
 ^warning: ignoring
diff --git a/jbmc/regression/jbmc/finally7/test.desc b/jbmc/regression/jbmc/finally7/test.desc
@@ -3,8 +3,8 @@ test.class
 --function test.main
 ^EXIT=10$
 ^SIGNAL=0$
-assertion at file test\.java line 7 function java::test\.main:\(\)V bytecode-index 12: SUCCESS
-assertion at file test\.java line 10 function java::test\.main:\(\)V bytecode-index 25: FAILURE
+assertion at file test\.java line 7 function java::test\.main:\(\)V bytecode-index 13: SUCCESS
+assertion at file test\.java line 10 function java::test\.main:\(\)V bytecode-index 26: FAILURE
 ^VERIFICATION FAILED$
 --
 ^warning: ignoring
diff --git a/jbmc/regression/jbmc/no-main-int-array-maybe-null1/test.desc b/jbmc/regression/jbmc/no-main-int-array-maybe-null1/test.desc
@@ -4,9 +4,9 @@ Main.class
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
-assertion at file Main\.java line 5 function .* bytecode-index 6: FAILURE
-assertion at file Main\.java line 6 function .* bytecode-index 14: FAILURE
-assertion at file Main\.java line 12 function .* bytecode-index 31: SUCCESS
+assertion at file Main\.java line 5 function .* bytecode-index 7: FAILURE
+assertion at file Main\.java line 6 function .* bytecode-index 15: FAILURE
+assertion at file Main\.java line 12 function .* bytecode-index 32: SUCCESS
 \*\* 2 of .* failed
 --
 ^warning: ignoring
diff --git a/jbmc/regression/jbmc/no-main-multi-array-maybe-null1/test.desc b/jbmc/regression/jbmc/no-main-multi-array-maybe-null1/test.desc
@@ -4,7 +4,7 @@ Main.class
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
-assertion at file Main\.java line 5 function .* bytecode-index 24: FAILURE
+assertion at file Main\.java line 5 function .* bytecode-index 25: FAILURE
 \*\* 1 of .* failed
 --
 ^warning: ignoring
diff --git a/jbmc/regression/jbmc/no-main-multi-array-maybe-null2/test.desc b/jbmc/regression/jbmc/no-main-multi-array-maybe-null2/test.desc
@@ -4,7 +4,7 @@ Main.class
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
-assertion at file Main\.java line 5 function .* bytecode-index 24: FAILURE
+assertion at file Main\.java line 5 function .* bytecode-index 25: FAILURE
 \*\* 1 of .* failed
 --
 ^warning: ignoring
diff --git a/jbmc/regression/jbmc/no-main-object-array-elements-maybe-null1/test.desc b/jbmc/regression/jbmc/no-main-object-array-elements-maybe-null1/test.desc
@@ -4,7 +4,7 @@ Main.class
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
-assertion at file Main\.java line 6 function .* bytecode-index 13: FAILURE
+assertion at file Main\.java line 6 function .* bytecode-index 14: FAILURE
 \*\* 1 of .* failed
 --
 ^warning: ignoring
diff --git a/jbmc/regression/jbmc/no-main-object-array-elements-maybe-null2/test.desc b/jbmc/regression/jbmc/no-main-object-array-elements-maybe-null2/test.desc
@@ -4,7 +4,7 @@ Main.class
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
-assertion at file Main\.java line 6 function .* bytecode-index 13: FAILURE
+assertion at file Main\.java line 6 function .* bytecode-index 14: FAILURE
 \*\* 1 of .* failed
 --
 ^warning: ignoring
diff --git a/jbmc/regression/jbmc/no-main-object-array-maybe-null1/test.desc b/jbmc/regression/jbmc/no-main-object-array-maybe-null1/test.desc
@@ -4,8 +4,8 @@ Main.class
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
-assertion at file Main\.java line 10 function .* bytecode-index 6: FAILURE
-assertion at file Main\.java line 14 function .* bytecode-index 26: FAILURE
+assertion at file Main\.java line 10 function .* bytecode-index 7: FAILURE
+assertion at file Main\.java line 14 function .* bytecode-index 27: FAILURE
 \*\* 2 of .* failed
 --
 ^warning: ignoring
diff --git a/jbmc/regression/jbmc/no-main-object-array-maybe-null2/test.desc b/jbmc/regression/jbmc/no-main-object-array-maybe-null2/test.desc
@@ -4,8 +4,8 @@ Main.class
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
-assertion at file Main\.java line 10 function .* bytecode-index 6: FAILURE
-assertion at file Main\.java line 14 function .* bytecode-index 26: FAILURE
+assertion at file Main\.java line 10 function .* bytecode-index 7: FAILURE
+assertion at file Main\.java line 14 function .* bytecode-index 27: FAILURE
 \*\* 2 of .* failed
 --
 ^warning: ignoring
diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp
@@ -32,11 +32,14 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/simplify_expr.h>
 #include <util/std_expr.h>
 #include <util/string2int.h>
+#include <util/string_constant.h>
 
 #include <goto-programs/cfg.h>
 #include <goto-programs/class_hierarchy.h>
 #include <goto-programs/resolve_inherited_component.h>
+
 #include <analyses/cfg_dominators.h>
+#include <analyses/uncaught_exceptions_analysis.h>
 
 #include <limits>
 #include <algorithm>
@@ -2248,10 +2251,39 @@ void java_bytecode_convert_methodt::convert_athrow(
   codet &c,
   exprt::operandst &results) const
 {
-  side_effect_expr_throwt throw_expr;
-  throw_expr.add_source_location() = location;
-  throw_expr.copy_to_operands(op[0]);
-  c = code_expressiont(throw_expr);
+  if(
+    uncaught_exceptions_domaint::get_exception_type(op[0].type()) ==
+      "java::java.lang.AssertionError")
+  {
+    // we translate athrow into
+    // ASSERT false;
+    // ASSUME false:
+    code_assertt assert_code;
+    assert_code.assertion() = false_exprt();
+    source_locationt assert_location = location; // copy
+    assert_location.set_comment("assertion at " + location.as_string());
+    assert_location.set("user-provided", true);
+    assert_location.set_property_class(ID_assertion);
+    assert_code.add_source_location() = assert_location;
+
+    code_assumet assume_code;
+    assume_code.assumption() = false_exprt();
+    source_locationt assume_location = location; // copy
+    assume_location.set("user-provided", true);
+    assume_code.add_source_location() = assume_location;
+
+    code_blockt ret_block;
+    ret_block.move_to_operands(assert_code);
+    ret_block.move_to_operands(assume_code);
+    c = ret_block;
+  }
+  else
+  {
+    side_effect_expr_throwt throw_expr;
+    throw_expr.add_source_location() = location;
+    throw_expr.copy_to_operands(op[0]);
+    c = code_expressiont(throw_expr);
+  }
   results[0] = op[0];
 }
 
diff --git a/jbmc/src/java_bytecode/java_bytecode_typecheck_expr.cpp b/jbmc/src/java_bytecode/java_bytecode_typecheck_expr.cpp
@@ -81,7 +81,9 @@ void java_bytecode_typecheckt::typecheck_expr_symbol(symbol_exprt &expr)
 
   if(s_it==symbol_table.symbols.end())
   {
-    PRECONDITION(has_prefix(id2string(identifier), "java::"));
+    PRECONDITION(
+      has_prefix(id2string(identifier), "java::") ||
+      has_prefix(id2string(identifier), CPROVER_PREFIX));
 
     // no, create the symbol
     symbolt new_symbol;
diff --git a/jbmc/src/java_bytecode/remove_exceptions.cpp b/jbmc/src/java_bytecode/remove_exceptions.cpp
@@ -164,13 +164,7 @@ bool remove_exceptionst::function_or_callees_may_throw(
   {
     if(instr_it->is_throw())
     {
-      const exprt &exc =
-        uncaught_exceptions_domaint::get_exception_symbol(instr_it->code);
-      bool is_assertion_error =
-        id2string(uncaught_exceptions_domaint::get_exception_type(exc.type())).
-        find("java.lang.AssertionError")!=std::string::npos;
-      if(!is_assertion_error)
-        return true;
+      return true;
     }
 
     if(instr_it->is_function_call())
@@ -380,15 +374,6 @@ bool remove_exceptionst::instrument_throw(
 
   const exprt &exc_expr=
     uncaught_exceptions_domaint::get_exception_symbol(instr_it->code);
-  bool assertion_error=id2string(
-    uncaught_exceptions_domaint::get_exception_type(exc_expr.type())).
-    find("java.lang.AssertionError")!=std::string::npos;
-
-  // we don't count AssertionError (we couldn't catch it anyway
-  // and this may reduce the instrumentation considerably if the programmer
-  // used assertions)
-  if(assertion_error)
-    return false;
 
   add_exception_dispatch_sequence(
     goto_program, instr_it, stack_catch, locals);
diff --git a/src/analyses/uncaught_exceptions_analysis.cpp b/src/analyses/uncaught_exceptions_analysis.cpp
@@ -70,17 +70,12 @@ void uncaught_exceptions_domaint::transform(
     const exprt &exc_symbol=get_exception_symbol(instruction.code);
     // retrieve the static type of the thrown exception
     const irep_idt &type_id=get_exception_type(exc_symbol.type());
-    bool assertion_error=
-      id2string(type_id).find("java.lang.AssertionError")!=std::string::npos;
-    if(!assertion_error)
-    {
-      join(type_id);
-      // we must consider all the subtypes given that
-      // the runtime type is a subtype of the static type
-      std::vector<irep_idt> subtypes=
-        class_hierarchy.get_children_trans(type_id);
-      join(subtypes);
-    }
+    join(type_id);
+    // we must consider all the subtypes given that
+    // the runtime type is a subtype of the static type
+    std::vector<irep_idt> subtypes =
+      class_hierarchy.get_children_trans(type_id);
+    join(subtypes);
     break;
   }
   case CATCH:
diff --git a/src/goto-programs/builtin_functions.cpp b/src/goto-programs/builtin_functions.cpp
@@ -736,34 +736,6 @@ void goto_convertt::do_function_call_symbol(
     a->source_location=function.source_location();
     a->source_location.set("user-provided", true);
   }
-  else if(has_prefix(
-      id2string(identifier), "java::java.lang.AssertionError.<init>:"))
-  {
-    // insert function call anyway
-    code_function_callt function_call;
-    function_call.lhs()=lhs;
-    function_call.function()=function;
-    function_call.arguments()=arguments;
-    function_call.add_source_location()=function.source_location();
-
-    copy(function_call, FUNCTION_CALL, dest);
-
-    if(arguments.size() != 1 && arguments.size() != 2 && arguments.size() != 3)
-    {
-      error().source_location=function.find_source_location();
-      error() << "`" << identifier
-              << "' expected to have one, two or three arguments" << eom;
-      throw 0;
-    }
-
-    goto_programt::targett t=dest.add_instruction(ASSERT);
-    t->guard=false_exprt();
-    t->source_location=function.source_location();
-    t->source_location.set("user-provided", true);
-    t->source_location.set_property_class(ID_assertion);
-    t->source_location.set_comment(
-      "assertion at "+function.source_location().as_string());
-  }
   else if(identifier=="assert" &&
           !ns.lookup(identifier).location.get_function().empty())
   {
