JBMC report FAILURE on uncaught exception #2043

peterschrammel · 2018-04-11T16:56:40Z

some more regression tests and other minor fixes

tautschnig

I'm not a Java expert, but I think this warrants more work as indicated in my comments.
As GitHub doesn't allow me to comment on the changes in the last commit ("Recompile regression test class files"): why are these being recompiled?

tautschnig · 2018-04-11T17:11:48Z

regression/cbmc-java/enum2/test.desc

+--
+^warning: ignoring
+--
+ordinal() not loaded by --lazy-methods


Should there be an issue for this, or maybe is there one already in some project?

tautschnig · 2018-04-11T17:12:13Z

regression/cbmc-java/enum3/test.desc

+--
+^warning: ignoring
+--
+ordinal() not loaded by --lazy-methods


Should there be an issue?

tautschnig · 2018-04-11T17:13:18Z

regression/jbmc-strings/append_obj_int_tostring/test.desc

+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--


Any chance to note which change/PR/commit has made this work?

tautschnig · 2018-04-11T17:16:04Z

src/java_bytecode/java_entry_point.cpp

@@ -308,6 +308,16 @@ void java_record_outputs(
  output.add_source_location()=function.location;

  init_code.move_to_operands(output);
+
+  // check that there is no uncaught exception


Shouldn't this be done in goto_checkt (in future, the same might be of interest for other languages), and is enforcing without giving any command-line control to the user a good idea?

peterschrammel · 2018-05-30T21:11:08Z

@tautschnig, I've refined the behaviour now:

Asserting that there is uncaught exception remains the default behaviour because an escaping exception makes the JVM abort; we should replicate that behaviour and report that as a bug. However, the user can now override this behaviour using the --no-uncaught-exception-check option, which might be useful in combination with --function, when thrown exceptions could be considered as part of the 'normal' behaviour.
Moreover, I've introduced --propagate-assertion-error which allows to propagate AssertionError as performed in the JVM rather than using a goto ASSERT statement. This flag is turned off by default following the assumption that usually nobody tries to catch AssertionError, and hence reporting a failing assertion at the location where AssertionError is thrown is typically the desired behaviour; if not the flag can be used.

peterschrammel · 2018-05-31T21:36:15Z

TG bump is passing.

tautschnig

No serious objections from my side (I'm not a Java person anyway), just procedural comments. In addition to the below: "Recompile regression test class files" - why?

tautschnig · 2018-06-01T06:59:27Z

jbmc/regression/jbmc/enum2/test.desc

+--
+^warning: ignoring
+--
+ordinal() not loaded by --lazy-methods


Maybe this is tracked elsewhere, otherwise might be worth opening an issue.

tautschnig · 2018-06-01T06:59:50Z

jbmc/regression/jbmc/enum3/test.desc

+--
+^warning: ignoring
+--
+ordinal() not loaded by --lazy-methods


As for the other one: might warrant an issue.

tautschnig · 2018-06-01T07:00:53Z

jbmc/regression/jbmc-strings/append_obj_int_tostring/test.desc

+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--


Since this is a regression test: when was this an issue, could the commit message maybe say something to that effect?

Would require a bisect between now and January.

thk123

Probably check at least one of the tests you modified produces the same output with the --no-uncaught-exception-check.

Add test for propagate-assertion-error

thk123 · 2018-06-04T10:47:55Z

jbmc/src/java_bytecode/java_bytecode_instrument.cpp

+/// Instruments the start function with an assertion that checks whether
+/// an exception has escaped the entry point
+/// \param symbol_table: global symbol table
+void java_bytecode_instrument_uncaught_exceptions(symbol_tablet &symbol_table)


Is mutating the entry point a good plan? Might be better for the entry point construction to have a collection of checks that it appends after the return. Can't spot a concrete problem (so feel free to ignore) but I think strongly couples this code with the entry point generation (if the entry point code changes to wrap the whole thing in an if statement for whatever reason, the assert will be in the wrong place).

In my opinion, the entire property instrumentation should be moved into a goto-pass.

Be that as it may - is that likely to happen in the near future, and if not would decoupling be useful in the meantime?

I've added some invariants to check that the entry point looks sane.

thk123 · 2018-06-04T10:49:06Z

jbmc/src/java_bytecode/java_bytecode_language.cpp

    java_entry_point(
      symbol_table,
      main_class,
      get_message_handler(),
      assume_inputs_non_null,
      object_factory_parameters,
-      get_pointer_type_selector());
+      get_pointer_type_selector()))
+    return true;


If statement is multiple lines so wrap the body in braces

thk123 · 2018-06-04T10:50:12Z

jbmc/src/java_bytecode/java_bytecode_language.h

  "(java-no-load-class):"

 #define JAVA_BYTECODE_LANGUAGE_OPTIONS_HELP /*NOLINT*/                                          \
+  " --no-uncaught-exception-check    ignore uncaught exceptions and errors\n" \


You might consider documenting this feature (and this flag to turn it off) more thoroughly in a markdown file somewhere (jbmc/doc/cl-options.md?)

This would be useful. I've created a ticket for it (TG-3893).

Sorry should have pointed this out in first review, but given that the error message is "no uncaught exception", this flag reads a bit like it turns on the "no uncaught exception check", suggest calling this flag: --disable-uncaught-exception-check?

thk123 · 2018-06-04T10:50:52Z

jbmc/src/java_bytecode/java_bytecode_language.h

@@ -43,6 +44,7 @@ Author: Daniel Kroening, [email protected]

 #define JAVA_BYTECODE_LANGUAGE_OPTIONS_HELP /*NOLINT*/                                          \
  " --no-uncaught-exception-check    ignore uncaught exceptions and errors\n" \
+  " --propagate-assertion-error      propagate java.lang.AssertionError\n" \


Also this as I don't know what this means (propagate to who?)

thk123 · 2018-06-04T10:53:32Z

jbmc/src/java_bytecode/remove_exceptions.cpp

-  // and this may reduce the instrumentation considerably if the programmer
-  // used assertions)
-  if(assertion_error)
+  // we allow AssertionError not to be propgated since


Typo: propagated

peterschrammel · 2018-06-13T14:03:26Z

@smowton, I've implemented your suggestion to clean up the user-defined assertion generation for Java right away. This looks much cleaner now and removes some references to java.util.AssertionError from analyses and goto-programs.

smowton

The new way of dealing with throw new AssertionError is much better :D Couple of minor improvements, and I still really dislike hacking __CPROVER__start rather than simply asking java_entry_point to build it correctly the first time.

smowton · 2018-06-13T16:08:29Z

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

+        code_function_callt assert_call;
+        assert_call.function() =
+          symbol_exprt(CPROVER_PREFIX "assert", assert_type);
+        assert_call.lhs().make_nil();


You can simply use code_assertt and code_assumet instead of going via functions

smowton · 2018-06-13T16:08:51Z

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

-      c=code_expressiont(throw_expr);
-      results[0]=op[0];
+        code_blockt ret_block;
+        ret_block.operands().push_back(std::move(assert_call));


Unsure which we prefer of std::move vs. move_to_operands these days, but check

allredj

Passed Diffblue compatibility checks (cbmc commit: 68cde16).

The java files were changed in previous commits, but the class files were not recompiled, which caused confusing mismatches in line numbers.

tautschnig

Just nit picks. Disclaimer: I have not done a technical review of the Java parts, just code reading.

tautschnig · 2018-06-14T08:06:19Z

jbmc/src/java_bytecode/java_bytecode_instrument.cpp

+  assert_no_exception.assertion() = equal_exprt(
+    exc_symbol.symbol_expr(),
+    null_pointer_exprt(to_pointer_type(exc_symbol.type)));
+  source_locationt assert_location = source_location;


Is there actual value in this temporary?

It's shorter than assert_no_exception.add_source_location().set_comment("no uncaught exception");

tautschnig · 2018-06-14T08:08:03Z

jbmc/src/java_bytecode/java_bytecode_language.cpp

@@ -777,15 +774,21 @@ bool java_bytecode_languaget::generate_support_functions(
  convert_lazy_method(res.main_function.name, symbol_table);

  // generate the test harness in __CPROVER__start and a call the entry point
-  return
+  if(


Why is this return replaced by an if? Unless I'm missing something this code is if(x) return true; return false; - which should be the same as return x;

That was a leftover from the previous variant where the instrumentation was added from here. Cleaned up.

tautschnig · 2018-06-14T08:11:10Z

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

+    // ASSUME false:
+    code_assertt assert_code;
+    assert_code.assertion() = false_exprt();
+    source_locationt assert_location = location; // copy


What is this copy good for?

Because we use location as the basis for a modified source location.

Nit: either explain that in the comment, or delete the comment (saying copy afterwards just invites the question)

tautschnig · 2018-06-14T08:11:26Z

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

+
+    code_assumet assume_code;
+    assume_code.assumption() = false_exprt();
+    source_locationt assume_location = location; // copy


As above: why copy?

tautschnig · 2018-06-14T08:12:54Z

src/analyses/goto_check.cpp

-          notequal_exprt not_eq_null(
-            pointer,
-            null_pointer_exprt(to_pointer_type(pointer.type())));
+        notequal_exprt not_eq_null(


allredj

Passed Diffblue compatibility checks (cbmc commit: 0b9334d).

That's the default behaviour because an escaping exception makes the JVM abort. The user can override this behaviour using the --disable-uncaught-exception-check option.

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.

The argument of throw might be null even if it is of type java.lang.AssertionError.

Introduces --throw-assertion-error which allows to propgate AssertionError as performed in the JVM rather than using a goto ASSERT statement.

allredj

Passed Diffblue compatibility checks (cbmc commit: cd2ef4b).

e6d196d Merge pull request diffblue#2355 from owen-jones-diffblue/owen-jones-diffblue/add-name-to-array-type 6f7580d Merge pull request diffblue#2351 from romainbrenguier/bugfix/null-array b2089b7 Add unit test for array_poolt 2df6d81 Set name of java array types 50e02b0 Simplify make_char_array_for_char_pointer 645eda9 Improve invariant message 3c7a671 Look up for null pointer in array pool 32a4186 Merge pull request diffblue#2302 from romainbrenguier/refactor/ci-lazy-methods c4aadab Extract handle_virtual_methods_with_no_callees cac016d Extract a convert_and_analyze_method method ca0adc9 Correct indentation 24b6936 Extract entry_point_methods method 360fabe Merge pull request diffblue#2356 from peterschrammel/fix-goto-simplification 4394016 Temporary fix to enable if-then-else simplifications d433438 Test for if-then-else optimisation in goto convert e5d1c12 Merge pull request diffblue#2354 from Degiorgio/disable-soundness-check-for-shared-pointers 7d4d4bd Skip check for unsoundness in shared pointer handling (java only) 8e6244c Merge pull request diffblue#2043 from peterschrammel/fail-on-uncaught-exception ec3010f Merge pull request diffblue#1994 from tautschnig/concurrency-soundness 1a9850a Merge pull request diffblue#2326 from tautschnig/c++-enum b71efaf Merge pull request diffblue#2019 from tautschnig/remove-unused 26b13ae Abort concurrency encoding in possibly unsound cases cd2ef4b Enable throwing of AssertionError 653d887 Remove wrong assumption from goto check 07acde4 Refactor user-defined assertion translation for Java 04c0205 Assert that there is uncaught exception 1daf466 Use resolver to translate cpp_name to scoped base_name 471b20f Remove prop_assignmentt interface 2639cf1 Remove unused solvers/prop/prop_conv_store.{h,cpp} 502687e Remove unused solver/prop/prop_wrapper.h ae56978 Remove unused goto-analyzer/static_analyzer.{h,cpp} 2260f82 Remove path_accelerationt interface d350e5c Remove unused nondet_ifthenelse.{h,cpp} a4936f8 Remove unused cpp/recursion_counter.h 71cfbbd Remove unused sorted_vector.h 4d4c9c6 Revert "added pipe_stream class" 2696420 Revert "new exception class" 3fb06ba Revert "Added utility class to convert strings into expressions" 55bdbc7 Recompile regression test class files 118f41f Merge pull request diffblue#2352 from tautschnig/c++-auto-tc 5a4dc8d Merge pull request diffblue#2315 from diffblue/fix-goto 199d4cc prevent half-constructed GOTO instructions 72156d5 C++ front-end: fix auto+references after already-typechecked cleanup 8fac5ed Merge pull request diffblue#2069 from romainbrenguier/refactor/convert_instruction 309d207 remove conversion for non-deterministic-goto 67081d5 Extract convert_pop function cd98a1f Extract convert_switch function f2acb00 Extract convert_dup2_x2 function 66cf709 Extract convert_dup2_x1 function e0735af Extract convert_dup2 function 51f53ca Extract convert_const function d627638 Extract convert_invoke function fcfca08 Extract replace_calls_to_cprover_assume function 0a521a4 Extract convert_checkcast function 4c28f99 Extract convert_athrow function 21e37a8 Extract convert_monitorexit function a7bbf53 Extract do_exception_handling function 0aa1c8e Extract convert_monitorenter function 48dd97f Extract convert_multianewarray function edc4a28 Extract convert_newarray function f8d00f6 Extract convert_new function b846798 Extract convert_putstatic function 27af4a2 Extract convert_putfield function f1edff9 Extract convert_getstatic function 68bddf1 Remove redundant assert 6f0f3fb Extract convert_cmp2 function 3049281 Extract convert_cmp function 5a5788c Extract convert_ushr function 305ede8 Extract convert_iinc function 61d03da Extract convert_ifnull function b4f6d04 Extract convert_if_nonull function 0e911d4 Extract convert_if function 651246e Extract convert_if_cmp function fc95df1 Extract convert_ret function ce58dca Extract convert_aload/store/astore functions 14e3c35 Extract convert_invokedynamic function 939bb53 Rename iterators and use auto ddb31a0 Extract draw_edges_from_ret_to_jsr function 390063f Extract try_catch_handler function 87a4f31 Make label static 36ed947 Replace assert by invariant 036f1b1 Use auto for iterator types git-subtree-dir: cbmc git-subtree-split: e6d196d

peterschrammel requested review from cesaro, mgudemann, smowton and thk123 as code owners April 11, 2018 16:56

tautschnig reviewed Apr 11, 2018

View reviewed changes

tautschnig assigned peterschrammel Apr 12, 2018

peterschrammel added the Java Front End label Apr 28, 2018

peterschrammel force-pushed the fail-on-uncaught-exception branch 2 times, most recently from abfef25 to c0a0a4d Compare April 28, 2018 20:35

peterschrammel added the Needs rebase label May 10, 2018

peterschrammel force-pushed the fail-on-uncaught-exception branch 2 times, most recently from 5a62435 to afcd657 Compare May 30, 2018 10:56

peterschrammel removed the Needs rebase label May 30, 2018

peterschrammel force-pushed the fail-on-uncaught-exception branch 2 times, most recently from 570f2a2 to d2fd7da Compare May 30, 2018 15:17

peterschrammel assigned cesaro, smowton, thk123, tautschnig and mgudemann and unassigned peterschrammel May 31, 2018

tautschnig reviewed Jun 1, 2018

View reviewed changes

tautschnig removed their assignment Jun 1, 2018

thk123 reviewed Jun 4, 2018

View reviewed changes

peterschrammel force-pushed the fail-on-uncaught-exception branch 2 times, most recently from caf3fdb to 49207dd Compare June 9, 2018 21:50

peterschrammel requested review from chrisr-diffblue and martin-cs as code owners June 9, 2018 21:50

peterschrammel force-pushed the fail-on-uncaught-exception branch 2 times, most recently from bb6f859 to 68cde16 Compare June 13, 2018 14:01

peterschrammel assigned smowton and unassigned peterschrammel Jun 13, 2018

smowton reviewed Jun 13, 2018

View reviewed changes

allredj reviewed Jun 13, 2018

View reviewed changes

peterschrammel force-pushed the fail-on-uncaught-exception branch 2 times, most recently from 8007fb4 to a80778d Compare June 13, 2018 22:56

Recompile regression test class files

55bdbc7

The java files were changed in previous commits, but the class files were not recompiled, which caused confusing mismatches in line numbers.

peterschrammel force-pushed the fail-on-uncaught-exception branch from a80778d to 0b9334d Compare June 14, 2018 07:45

peterschrammel assigned mgudemann, allredj and tautschnig Jun 14, 2018

tautschnig approved these changes Jun 14, 2018

View reviewed changes

tautschnig assigned peterschrammel and unassigned smowton, tautschnig, mgudemann and allredj Jun 14, 2018

allredj reviewed Jun 14, 2018

View reviewed changes

peterschrammel added 4 commits June 14, 2018 09:46

Assert that there is uncaught exception

04c0205

That's the default behaviour because an escaping exception makes the JVM abort. The user can override this behaviour using the --disable-uncaught-exception-check option.

Remove wrong assumption from goto check

653d887

The argument of throw might be null even if it is of type java.lang.AssertionError.

Enable throwing of AssertionError

cd2ef4b

Introduces --throw-assertion-error which allows to propgate AssertionError as performed in the JVM rather than using a goto ASSERT statement.

peterschrammel force-pushed the fail-on-uncaught-exception branch from 0b9334d to cd2ef4b Compare June 14, 2018 08:51

allredj reviewed Jun 14, 2018

View reviewed changes

peterschrammel merged commit 8e6244c into diffblue:develop Jun 14, 2018

peterschrammel deleted the fail-on-uncaught-exception branch June 14, 2018 12:37

JBMC report FAILURE on uncaught exception #2043

JBMC report FAILURE on uncaught exception #2043

Conversation

peterschrammel commented Apr 11, 2018

tautschnig left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

peterschrammel commented May 30, 2018

peterschrammel commented May 31, 2018

tautschnig left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

thk123 left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

peterschrammel commented Jun 13, 2018

smowton left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment

tautschnig left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

peterschrammel Jun 14, 2018 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment

peterschrammel Jun 14, 2018 •

edited

Loading