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

romainbrenguier · 2019-09-18T15:38:15Z

This adds an option to JBMC to replace throw instructions by assert(false);assume(false);
so that execution branches are not analyzed further than the first throw.
This is mostly useful for performances, but the full benefit of this will only show once #5097 is in.

Each commit message has a non-empty body, explaining why the change was made.
Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
[r] 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).
My commit message includes data points confirming performance improvements (if claimed).
My PR is restricted to a single feature or bugfix.
[na] White-space or formatting changes outside the feature-related changed lines are in commits of their own.

smowton · 2019-09-21T12:00:25Z

I note this doesn't quite do what it says: it actually asserts that no exception is thrown, rather than assuming it (TG of course also uses --cover, translating that into an assumption)

romainbrenguier · 2019-09-23T07:16:41Z

@smowton

I note this doesn't quite do what it says: it actually asserts that no exception is thrown, rather than assuming it (TG of course also uses --cover, translating that into an assumption)

It actually does both if I'm not mistaken. Should we rename the option to --assert-no-exceptions-thrown?

codecov-io · 2019-09-23T08:45:18Z

Codecov Report

Merging #5117 into develop will decrease coverage by <.01%.
The diff coverage is 96.36%.

@@             Coverage Diff             @@
##           develop    #5117      +/-   ##
===========================================
- Coverage    66.97%   66.96%   -0.01%     
===========================================
  Files         1146     1146              
  Lines        93736    93721      -15     
===========================================
- Hits         62778    62761      -17     
- Misses       30958    30960       +2

Flag	Coverage Δ
#cproversmt2	`42.68% <ø> (+0.01%)`	⬆️
#regression	`63.45% <96.36%> (-0.01%)`	⬇️
#unit	`31.92% <85.45%> (+0.01%)`	⬆️

Impacted Files	Coverage Δ
...java_bytecode/java_bytecode_convert_method_class.h	`100% <ø> (ø)`	⬆️
...src/java_bytecode/java_bytecode_convert_method.cpp	`97.54% <100%> (ø)`	⬆️
jbmc/src/java_bytecode/java_bytecode_language.h	`78.57% <100%> (+1.64%)`	⬆️
jbmc/src/java_bytecode/java_bytecode_language.cpp	`93.17% <95.83%> (+0.09%)`	⬆️
src/nonstd/optional.hpp	`96.2% <0%> (-1.24%)`	⬇️
src/solvers/prop/prop_conv_solver.cpp	`80.88% <0%> (-0.45%)`	⬇️
src/goto-symex/goto_symex.cpp	`99.44% <0%> (-0.07%)`	⬇️
src/goto-symex/goto_symex.h	`92.3% <0%> (ø)`	⬆️

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update 2af983d...6990f9b. Read the comment docs.

allredj

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: e5ba652).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/128707994
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.

smowton · 2019-09-23T09:21:15Z

Yes I think that's better (the assert/assume pattern matches what the Java frontend does for null-pointer derefs for example)

peterschrammel

lgtm

peterschrammel · 2019-09-23T15:09:51Z

jbmc/src/java_bytecode/java_bytecode_language.h

@@ -150,6 +154,56 @@ class lazy_class_to_declared_symbols_mapt
  std::unordered_multimap<irep_idt, symbolt> map;
 };

+struct java_bytecode_language_optionst
+{
+  explicit java_bytecode_language_optionst(


explicit not required

allredj

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: 2d4842f).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/128776632
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.

allredj

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: 6990f9b).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/129047220
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.

Extract java_bytecode_language_optionst class from java_bytecode_language class, to make it more structured by separating the fields that are expected to remain constant during the execution once they are initialized.

This is to specify that we want to replace all throw instructions by assert false. This is useful mainly for performance reasons as it simplifies conditions for symex, while retaining the non-exceptional behaviour of the program.

This tests the option behaves as desired.

Test that when both are combined, --throw-runtime-exception still works.

allredj

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: b433f5c).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/129121599
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.

segun3d

QA is satisfied with this PR

romainbrenguier requested review from cesaro, cristina-david, NathanJPhillips, peterschrammel, pkesseli, smowton and thk123 as code owners September 18, 2019 15:38

romainbrenguier force-pushed the experiment/never-throw branch 4 times, most recently from da9ea98 to 6f13cc5 Compare September 20, 2019 18:08

romainbrenguier added the Needs TG approval 🦉 Only merge with explicit approval from test-gen maintainers label Sep 20, 2019

romainbrenguier force-pushed the experiment/never-throw branch 3 times, most recently from c31ece6 to ebe53cd Compare September 20, 2019 20:39

romainbrenguier changed the title ~~[TG-9400][UFC] Add an assume-no-exceptions-throw exceptions~~ [TG-9400][UFC] Add an assume-no-exceptions-thrown option Sep 23, 2019

romainbrenguier force-pushed the experiment/never-throw branch 2 times, most recently from 755de11 to e5ba652 Compare September 23, 2019 07:58

romainbrenguier removed the Needs TG approval 🦉 Only merge with explicit approval from test-gen maintainers label Sep 23, 2019

romainbrenguier requested a review from segun3d September 23, 2019 08:47

allredj reviewed Sep 23, 2019

View reviewed changes

peterschrammel approved these changes Sep 23, 2019

View reviewed changes

romainbrenguier force-pushed the experiment/never-throw branch 4 times, most recently from 613b639 to 2d4842f Compare September 23, 2019 14:44

peterschrammel reviewed Sep 23, 2019

View reviewed changes

allredj reviewed Sep 23, 2019

View reviewed changes

romainbrenguier force-pushed the experiment/never-throw branch 2 times, most recently from 36b605c to 6990f9b Compare September 25, 2019 05:50

allredj reviewed Sep 25, 2019

View reviewed changes

smowton approved these changes Sep 25, 2019

View reviewed changes

romainbrenguier added 4 commits September 25, 2019 11:30

Extract java_bytecode_language_optionst class

06c4069

Extract java_bytecode_language_optionst class from java_bytecode_language class, to make it more structured by separating the fields that are expected to remain constant during the execution once they are initialized.

Add an assert-no-exceptions-thrown option

2ed5dfd

This is to specify that we want to replace all throw instructions by assert false. This is useful mainly for performance reasons as it simplifies conditions for symex, while retaining the non-exceptional behaviour of the program.

Add regression test for --assert-no-exceptions-thrown

7cdd2e2

This tests the option behaves as desired.

Test assert-no-exceptions-thrown and runtime exception

b433f5c

Test that when both are combined, --throw-runtime-exception still works.

romainbrenguier force-pushed the experiment/never-throw branch from 6990f9b to b433f5c Compare September 25, 2019 12:03

allredj reviewed Sep 25, 2019

View reviewed changes

segun3d reviewed Sep 25, 2019

View reviewed changes

romainbrenguier merged commit 9171c86 into diffblue:develop Sep 25, 2019

romainbrenguier deleted the experiment/never-throw branch September 25, 2019 15:20

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

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

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

Uh oh!

romainbrenguier commented Sep 18, 2019

Uh oh!

smowton commented Sep 21, 2019

Uh oh!

romainbrenguier commented Sep 23, 2019

Uh oh!

codecov-io commented Sep 23, 2019 •

edited

Loading

Uh oh!

allredj left a comment

Uh oh!

smowton commented Sep 23, 2019

Uh oh!

peterschrammel left a comment

Uh oh!

peterschrammel Sep 23, 2019

Uh oh!

allredj left a comment

Uh oh!

allredj left a comment

Uh oh!

allredj left a comment

Uh oh!

segun3d left a comment

Uh oh!

Uh oh!

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

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

Uh oh!

Conversation

romainbrenguier commented Sep 18, 2019

Uh oh!

smowton commented Sep 21, 2019

Uh oh!

romainbrenguier commented Sep 23, 2019

Uh oh!

codecov-io commented Sep 23, 2019 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Codecov Report

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

smowton commented Sep 23, 2019

Uh oh!

peterschrammel left a comment

Choose a reason for hiding this comment

Uh oh!

peterschrammel Sep 23, 2019

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!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

segun3d left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

codecov-io commented Sep 23, 2019 •

edited

Loading