Fix Java exception handlers #4499

NathanJPhillips · 2019-04-08T16:58:55Z

Fix Java exception handlers when multiple exception table rows begin at the same offset. Previously this could lead to throws within the catch block (e.g. a straightforward log-and-rethrow) being directed to the same catch block, introducing a spurious loop.

This is not a perfect solution, as documented in the comments, but is an improvement on the previous version, which was actually broken as demonstrated by the added tests. If it wasn't for the unwind limit the test case shown would cause Symex never to complete. An ideal solution would probably be to get rid of push-catch and pop-catch altogether and carry a GOTO exception table around with the GOTO program until exceptions are removed.

Each commit message has a non-empty body, explaining why the change was made.
N/A Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
N/A The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
N/A My commit message includes data points confirming performance improvements (if claimed).
My PR is restricted to a single feature or bugfix.
N/A White-space or formatting changes outside the feature-related changed lines are in commits of their own.

smowton · 2019-04-08T17:01:51Z

@NathanJPhillips Added the first paragraph to the description

smowton

Some cleanups otherwise lgtm

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

jbmc/regression/jbmc/exceptions28/test.desc

allredj

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: b76857c).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/107511332
Status will be re-evaluated on next push.
Common spurious failures include: the cbmc commit has disappeared in the mean time (e.g. in a force-push); the author is not in the list of contributors (e.g. first-time contributors); compatibility was already broken by an earlier merge.

NathanJPhillips · 2019-04-09T09:21:41Z

This PR failed Diffblue compatibility checks (cbmc commit: b76857c).

This was confirmed to be an erroneous warning.

thk123

I have some questions, I'm also gonna try it on TG just to be safe about the limitations

jbmc/regression/jbmc/exceptions28/test.desc

thk123 · 2019-04-09T11:06:04Z

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

+  }
+  for(const auto &exceptions : exceptions_by_end)
+  {
+    code_push_catcht catch_push;


⛏️ Seems a bit back to front to make the code before making the list, would be nicer to make the execption list, and construct the code_push_catcht from it, but I see it has no constructor from exception list so out of scope of this PR to fix it

thk123 · 2019-04-09T11:07:32Z

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

+    {
+      exception_list.emplace_back(
+        exception.catch_type.get_identifier(),
+        // Record the exception handler in the CATCH-PUSH instruction by


⛏️ Initially found the comment inside the brackets a little disorientating. You could introduce a local with the result of label with the comment above, if you agree.

thk123 · 2019-04-09T11:08:32Z

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

-  method_offsett pos = 0;
-  method_offsett end_pc = 0;
-  while(pos < method.exception_table.size())
+  // For each try-catch add a CATCH-PUSH instruction


💡 Big block of code with a comment, perhaps pull out into a function?

thk123 · 2019-04-09T11:10:53Z

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

+  if(working_set.empty())
+  {
+    // There was no throw in the try block
+    // TODO: This will result in non-balanced PUSH and POPs


❓ This seems a little scary... is this really not a regression? A knownbug test showing this limitation would be greatly appreciated.

❓ can we print a warning here

This is the current behaviour already. I suggested putting an assertion in but @smowton thought that this actually happens quite a lot and is relatively harmless. A warning seems like a good idea.

Also it turns out my thinking was slightly wrong. We can't tell at this point whether balancing POPs will be introduced. I've updated the code and clarified the comments to make it clearer what's going on.

thk123 · 2019-04-09T11:11:19Z

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

+  {
+    // This just fails if we have a back-edge here
+    // TODO: This will result in non-balanced PUSH and POPs
+    return code;


❓ Ditto here. Also might be a good idea to print some warning in this eventuallity?

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

thk123

Thanks 👍 I ran the tests locally (and they passed) but messed up running on CI, feel free to merge without waiting if you want, but I'll kick of CI again if you don't mind waiting till tomorrow

thk123 · 2019-04-09T17:32:31Z

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

  }
-  return c;
+
+  if (result.size() != 1)


Seems a little over the top just to avoid one redundant block, but as you like

thk123 · 2019-04-09T17:33:00Z

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

+    if(exception.start_pc == cur_pc)
+      exceptions_by_end[exception.end_pc].push_back(exception);
+  }
+  // Loop over each block with a distinct end position


personally think this comment doesn't add clarity.

smowton · 2019-04-10T08:11:22Z

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

@@ -1806,7 +1806,7 @@ code_blockt java_bytecode_convert_methodt::convert_instructions(
    // (e.g. due to exceptional control flow)
    if(!start_new_block)
      start_new_block=address_pair.second.predecessors.size()>1;
-    // Start a new lexical block if we've just entered a try block
+    // Start a new lexical block if we've just entered a handler block


try was accurate, I'd interpret handler to mean a catch block, and the exception table's start_pc entry refers to the try

I thought using the word "try" would imply the whole of a Java try block to someone who didn't know how exception tables worked.

Ah, true enough -- in that case I think you should say it in full, "if we've just entered a block in which exceptions are handled. This is usually the start of a try block, but a single try can be represented as multiple non-contiguous blocks in the exception table."

peterschrammel · 2019-04-10T08:26:03Z

jbmc/regression/jbmc/exceptions28/test.desc

+    7    15    15   Class MyException
+    0     6    18   Class java/lang/Exception
+    7    15    18   Class java/lang/Exception
+This is not ordered in the sense that the two handlers for the block 0-6 are not next to each other.


Missing newline

peterschrammel · 2019-04-10T08:32:33Z

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

-      cur_pc < exception_row.end_pc && !working_set.empty() &&
-      *working_set.begin() == exception_row.end_pc)
+    // Count the distinct start positions of handlers that end at this location
+    std::set<std::size_t> start_positions;  // Use a set to deduplicate


Is the ordered set needed here?

unordered_set wouldn't perform well when storing a small set of integers without good spread like these.

thk123 · 2019-04-10T09:10:51Z

TG has revealed a potential issue with either synchronized blocks or nested exception catch blocks and this PR. Nathan is investigating at the moment.

NathanJPhillips · 2019-04-10T11:51:11Z

A change I made in response to a review comment introduced a bug that wasn't caught by current CBMC tests. I have added a test to catch this in a separate commit and revised the change to overcome the problem.

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: 21bfdba).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/107800935

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: 2cf31a9).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/107823835

Make the control-flow in the code understandable Fix bugs caused by handlers in the exception table not being sorted so that ones that start and end at the same positions are all next to each other

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: 79d5d61).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/107834277

NathanJPhillips self-assigned this Apr 8, 2019

NathanJPhillips requested a review from smowton April 8, 2019 16:58

NathanJPhillips requested review from cesaro, cristina-david, peterschrammel, pkesseli and thk123 as code owners April 8, 2019 16:58

smowton approved these changes Apr 8, 2019

View reviewed changes

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp Outdated Show resolved Hide resolved

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp Outdated Show resolved Hide resolved

jbmc/regression/jbmc/exceptions28/test.desc Show resolved Hide resolved

NathanJPhillips force-pushed the bugfix/exception-handlers branch 2 times, most recently from f51f997 to b76857c Compare April 8, 2019 17:41

allredj reviewed Apr 8, 2019

View reviewed changes

NathanJPhillips requested a review from romainbrenguier April 9, 2019 08:27

thk123 reviewed Apr 9, 2019

View reviewed changes

NathanJPhillips force-pushed the bugfix/exception-handlers branch from b76857c to ccc3550 Compare April 9, 2019 17:21

thk123 approved these changes Apr 9, 2019

View reviewed changes

NathanJPhillips force-pushed the bugfix/exception-handlers branch from ccc3550 to 02d5ad0 Compare April 10, 2019 08:06

smowton reviewed Apr 10, 2019

View reviewed changes

peterschrammel reviewed Apr 10, 2019

View reviewed changes

Add test to show bad GOTO is created with exceptions

2b4781a

Add test for nested try blocks

a23d1ab

NathanJPhillips force-pushed the bugfix/exception-handlers branch from 02d5ad0 to 21bfdba Compare April 10, 2019 11:50

allredj reviewed Apr 10, 2019

View reviewed changes

NathanJPhillips force-pushed the bugfix/exception-handlers branch from 21bfdba to 2cf31a9 Compare April 10, 2019 14:49

allredj reviewed Apr 10, 2019

View reviewed changes

Rewrite do_exception_handling

79d5d61

Make the control-flow in the code understandable Fix bugs caused by handlers in the exception table not being sorted so that ones that start and end at the same positions are all next to each other

NathanJPhillips force-pushed the bugfix/exception-handlers branch from 2cf31a9 to 79d5d61 Compare April 10, 2019 15:57

allredj reviewed Apr 10, 2019

View reviewed changes

NathanJPhillips merged commit 097a58d into diffblue:develop Apr 11, 2019

NathanJPhillips deleted the bugfix/exception-handlers branch April 11, 2019 08:21

Fix Java exception handlers #4499

Fix Java exception handlers #4499

Uh oh!

Conversation

NathanJPhillips commented Apr 8, 2019 • edited by smowton Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

smowton commented Apr 8, 2019

Uh oh!

smowton left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

NathanJPhillips commented Apr 9, 2019

Uh oh!

thk123 left a comment

Choose a reason for hiding this comment

Uh oh!

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!

Uh oh!

Uh oh!

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!

NathanJPhillips Apr 10, 2019 • edited Loading Uh oh! There was an error while loading. Please reload this page.

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 commented Apr 10, 2019

Uh oh!

NathanJPhillips commented Apr 10, 2019

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

NathanJPhillips commented Apr 8, 2019 •

edited by smowton

Loading

NathanJPhillips Apr 10, 2019 •

edited

Loading