JBMC report FAILURE on uncaught exception by peterschrammel · Pull Request #2043 · diffblue/cbmc

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

+--
+^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

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


Should there be an issue?

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

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


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

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


  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

+--
+^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

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


As for the other one: might warrant an issue.

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

+^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

+/// 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

      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

  "(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


 #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

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

+        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

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

-      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

ghost

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.

ghost

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

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

+  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");

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


  // 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.

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

+    // 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)

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

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


As above: why copy?

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

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


ghost

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.

ghost

Passed Diffblue compatibility checks (cbmc commit: cd2ef4b).

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

Peter Schrammel 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


		init_code.move_to_operands(output);

		// check that there is no uncaught exception

Uh oh!

Conversation

peterschrammel commented Apr 11, 2018

Uh oh!

tautschnig left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

peterschrammel commented May 30, 2018

Uh oh!

peterschrammel commented May 31, 2018

Uh oh!

tautschnig left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

thk123 left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

peterschrammel commented Jun 13, 2018

Uh oh!

smowton left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

ghost Jun 13, 2018

Choose a reason for hiding this comment

Uh oh!

ghost left a comment

Choose a reason for hiding this comment

Uh oh!

ghost left a comment

Choose a reason for hiding this comment

Uh oh!

ghost Jun 14, 2018

Choose a reason for hiding this comment

Uh oh!

ghost Jun 14, 2018

Choose a reason for hiding this comment

Uh oh!

ghost Jun 14, 2018

Choose a reason for hiding this comment

Uh oh!

ghost Jun 14, 2018 • edited by peterschrammel Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

ghost Jun 14, 2018 •

edited by peterschrammel

Loading