[TG-9390] GOTO-symex: propagate notequal conditions for boolean types #5091

owen-mc-diffblue · 2019-09-05T15:48:13Z

Conditional branches on "x != false", as well as "x" and "!x", can and should lead to constant
propagation just as "x == true" does now. This is particularly beneficial for the
"clinit_already_run" variables that are maintained to determine if a static initialiser should
be run or not -- the current "if(already_run != true) clinit(); already_run = true;" condition
now leaves symex certain that it has been run at the bottom of the function regardless of the
already_run flag's initial value, whereas before it could remain uncertain and so explore the
static initialiser more than is necessary.

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/
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.
White-space or formatting changes outside the feature-related changed lines are in commits of their own.

allredj

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

codecov-io · 2019-09-05T16:52:04Z

Codecov Report

Merging #5091 into develop will increase coverage by <.01%.
The diff coverage is 99.12%.

@@             Coverage Diff             @@
##           develop    #5091      +/-   ##
===========================================
+ Coverage    69.69%    69.7%   +<.01%     
===========================================
  Files         1321     1320       -1     
  Lines       109360   109336      -24     
===========================================
- Hits         76219    76208      -11     
+ Misses       33141    33128      -13

Impacted Files	Coverage Δ
unit/goto-symex/apply_condition.cpp	`100% <100%> (ø)`
src/goto-symex/symex_goto.cpp	`96.1% <100%> (-0.09%)`	⬇️
src/goto-symex/goto_state.cpp	`82.05% <94.73%> (+6.05%)`	⬆️
unit/testing-utils/expr_query.h	`80% <0%> (-20%)`	⬇️
jbmc/src/java_bytecode/java_bytecode_language.h	`72.72% <0%> (-4.2%)`	⬇️
...bmc/src/java_bytecode/java_static_initializers.cpp	`97.77% <0%> (-1.32%)`	⬇️
unit/json/json_parser.cpp	`100% <0%> (ø)`	⬆️
jbmc/src/java_bytecode/java_static_initializers.h	`100% <0%> (ø)`	⬆️
...a_static_initializers/java_static_initializers.cpp	`100% <0%> (ø)`	⬆️
src/json/scanner.l	`90.9% <0%> (ø)`	⬆️
... and 9 more

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 fab409d...5bc512a. Read the comment docs.

owen-mc-diffblue · 2019-09-08T07:30:06Z

This is a cleaned-up version of #5089, with a few bugs fixed and tests added. I added tests in C and java take make sure it worked with the boolean types in both languages.

The last commit was a part of the code from #5089 that I found wasn't needed for any of my tests. It seems to be doing the right kind of thing, so one argument is to keep it in so that if the any of the language frontends start producing GOTO like that then we'll still be able to determine the value of the symbol. The counter-argument is that it isn't tested, so it might not be doing the right thing, and it's misleading to put in code for a case that doesn't currently happen.

owen-mc-diffblue · 2019-09-09T06:14:19Z

One test is failing (regression/cbmc/Empty_struct1). The problem is that we declare b and c like this:

_Bool b, c=b;

We then condition on b. The new code sets b to be 0 on one branch and 1 on the other. The test ends with the assertion assert(b==c);. cbmc falsifies this assertion by initially setting b to some value other than 0 or 1, e.g. 9 in the case I looked at, and we end up asserting that 1 == 9.

The only reasonable resolutions I can think of are (a) restricting _Bool types in C to have values 0 and 1, which would take us away from how C actually works, (b) restricting this feature to languages which have a proper boolean type, like java

smowton · 2019-09-09T08:06:44Z

I'd suggest only doing this for real booleans (bool_typet, 1-bit) not cbools (8-bit, conventionally either 1 or 0). That loses some cases but ensures compliance with C, and the static init fields I set out to handle are "proper" booleans

smowton · 2019-09-09T08:11:48Z

(presumably this is because of the unrestricted typecasting in the equals case)

owen-mc-diffblue · 2019-09-09T09:09:17Z

@smowton Okay, that makes sense. bool_typet symbols aren't made by the C or java front-ends, are they? They're only synthetic, right? Is there any way of making them apart from these A_clinit_already_run symbols we make for java? I'm thinking about how I can test this feature.

romainbrenguier · 2019-09-09T15:48:00Z

src/goto-symex/goto_state.cpp

    for(const auto &op : condition.operands())
      apply_condition(op, previous_state, ns);
  }
+  else if(condition.id() == ID_not)


⛏️ expr_try_dynamic_cast<not_exprt> 🚜

romainbrenguier · 2019-09-09T15:48:23Z

src/goto-symex/goto_state.cpp

+  else if(condition.id() == ID_not)
+  {
+    const exprt &operand = to_not_expr(condition).op();
+    if(operand.id() == ID_notequal)


romainbrenguier · 2019-09-09T15:48:36Z

src/goto-symex/goto_state.cpp

+        previous_state,
+        ns);
+    }
+    else if(operand.id() == ID_equal)


romainbrenguier · 2019-09-09T15:52:14Z

src/goto-symex/symex_goto.cpp

-  }
+  exprt negated_new_guard = new_guard.id() == ID_not
+                              ? to_not_expr(new_guard).op()
+                              : not_exprt(new_guard);


use boolean_negate

romainbrenguier · 2019-09-09T15:52:25Z

src/goto-symex/symex_goto.cpp

-      current_state,
-      ns);
-  }
+  exprt negated_new_guard = new_guard.id() == ID_not


romainbrenguier · 2019-09-09T15:52:26Z

src/goto-symex/symex_goto.cpp

-      current_state,
-      ns);
-  }
+  exprt negated_new_guard = new_guard.id() == ID_not


allredj

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

romainbrenguier · 2019-09-10T06:28:45Z

It would be good to have some benchmark results to see if get a performance improvement from this.

allredj

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

JohnDumbell · 2019-09-10T09:41:26Z

src/goto-symex/goto_state.cpp

@@ -10,6 +10,7 @@ Author: Romain Brenguier, [email protected]
 #include "goto_symex_is_constant.h"
 #include "goto_symex_state.h"

+#include <util/arith_tools.h>


Is this used? (After a quick scan I couldn't see an obvious use)

You're right, I think I must have added it for to_integer in an earlier version, but I'm not using that any more. I've removed it.

owen-mc-diffblue · 2019-09-11T14:09:48Z

I benchmarked this branch vs develop on 13 methods from tika-parsers that had been chosen because they don't complete quickly. I ran with a timeout of 10 minutes, and --show-vcc in an attempt to stop after symex, and not run the SAT solver, since I expect the change in this PR to speed up symex (it may also speed up SAT solving a little bit). 3 of the methods errored in both runs (2 because of a models library problem, one because it ran out of memory just after symex. 6 of the methods timed out in symex in both runs. That leaves 4 methods to compare. Here is a table, with develop on the left and this branch on the right

64.6 | 63.2
11.2 | 9.7
8.0 | 7.3
103.4 | 29.9

The runtime decreased by 2%, 13%, 9% and 71% respectively. The first one is within normal variation. The middle 2 show a small but noticeable improvement. But the last one shows without a doubt that this PR can drastically reduce symex run times.

owen-mc-diffblue · 2019-09-11T14:50:12Z

@kroening @peterschrammel @tautschnig This needs a code owner review - do any of you have time to look at it? (@smowton wrote most of it, so he probably shouldn't review it as well.)

segun3d · 2019-09-11T15:16:16Z

I benchmarked this branch vs develop on 13 methods from tika-parsers that had been chosen because they don't complete quickly. I ran with a timeout of 10 minutes, and --show-vcc in an attempt to stop after symex, and not run the SAT solver, since I expect the change in this PR to speed up symex (it may also speed up SAT solving a little bit). 3 of the methods errored in both runs (2 because of a models library problem, one because it ran out of memory just after symex. 6 of the methods timed out in symex in both runs. That leaves 4 methods to compare. Here is a table, with develop on the left and this branch on the right

64.6 | 63.2
11.2 | 9.7indly
8.0 | 7.3
103.4 | 29.9

The runtime decreased by 2%, 13%, 9% and 71% respectively. The first one is within normal variation. The middle 2 show a small but noticeable improvement. But the last one shows without a doubt that this PR can drastically reduce symex run times.

@owen-mc-diffblue Indeed the last bench mark is impressive. Could you kindly state which benchmark tool you used. Thanks.

owen-mc-diffblue · 2019-09-11T15:41:48Z

I used the benchmarking script in test-gen, written by @JohnDumbell. I used the following list of methods, provided by @smowton

org.apache.tika.parser.DefaultParser.<init>:(Lorg/apache/tika/mime/MediaTypeRegistry;Ljava/lang/ClassLoader;)V
org.apache.tika.parser.dwg.DWGParser.get2004Props:(Ljava/io/InputStream;Lorg/apache/tika/metadata/Metadata;Lorg/apache/tika/sax/XHTMLContentHandler;)V
org.apache.tika.parser.gdal.GDALParser.processCommand:(Ljava/io/InputStream;)Ljava/lang/String;
org.apache.tika.parser.html.HtmlHandler.resolve:(Ljava/lang/String;Ljava/lang/String;)Ljava/lang/String;
org.apache.tika.parser.isatab.ISATabUtils.parseAssay:(Ljava/io/InputStream;Lorg/apache/tika/sax/XHTMLContentHandler;Lorg/apache/tika/metadata/Metadata;Lorg/apache/tika/parser/ParseContext;)V
org.apache.tika.parser.iwork.PagesContentHandler.characters:([CII)V
org.apache.tika.parser.iwork.PagesContentHandler.resolveMetaDataKey:(Ljava/lang/String;)Ljava/lang/Object;
org.apache.tika.parser.jdbc.JDBCTableReader.getDetector:()Lorg/apache/tika/detect/Detector;
org.apache.tika.parser.jdbc.JDBCTableReader.handleClob:(Ljava/lang/String;Ljava/lang/String;ILjava/sql/ResultSet;ILorg/xml/sax/ContentHandler;Lorg/apache/tika/parser/ParseContext;)V
org.apache.tika.parser.microsoft.ooxml.XWPFWordExtractorDecorator.<init>:(Lorg/apache/tika/parser/ParseContext;Lorg/apache/poi/xwpf/extractor/XWPFWordExtractor;)V
org.apache.tika.parser.microsoft.ooxml.xwpf.XWPFEventBasedWordExtractor.getText:()Ljava/lang/String;
org.apache.tika.parser.ocr.TesseractOCRParser.extractOutput:(Ljava/io/InputStream;Lorg/apache/tika/sax/XHTMLContentHandler;)V
org.apache.tika.parser.xml.ElementMetadataHandler.isMatchingElement:(Ljava/lang/String;Ljava/lang/String;)Z

The method with the impressive speed-up was org.apache.tika.parser.xml.ElementMetadataHandler.isMatchingElement

Conditional branches on "x != false", as well as "x" and "!x", can and should lead to constant propagation just as "x == true" does now. This is particularly beneficial for the "clinit_already_run" variables that are maintained to determine if a static initialiser should be run or not -- the current "if(already_run != true) clinit(); already_run = true;" condition now leaves symex certain that it has been run at the bottom of the function regardless of the already_run flag's initial value, whereas before it could remain uncertain and so explore the static initialiser more than is necessary.

All the main branches are now covered

allredj

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

peterschrammel · 2019-09-12T17:09:17Z

jbmc/regression/jbmc/symex_can_track_when_clinits_have_definitely_been_run/test.desc

+java::ClassWithStaticInit::clinit_already_run#[1-9][0-9]
+^warning: ignoring
+--
+After the second call to ClassWithStaticInit.getStaticValue(), symex should have


Maybe explain how many generations you expect to be per call without the optimisation. That might it easier to understand why you expect >=10 to be bad.

Good point Peter. Actually, the number of generations per call could varies depending on whether apply_condition thinks it can set a value to be constant on one or both of the branches, and also future changes. I think it's safest to just say that we expect at least one new generation per call if symex doesn't know that clinit_already_run is true. I have increased the number of static function calls to 20, to make absolutely sure that we'd go over if the feature isn't working properly.

allredj

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

segun3d · 2019-09-13T13:29:43Z

@antlechner has confirmed that regression tests are sufficient, this in addition to the benchmarks results (see above) means this is now QA approved.

Previously we couldn't properly track when we had definitely already called them.

allredj

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

owen-mc-diffblue requested review from kroening, peterschrammel, smowton and tautschnig as code owners September 5, 2019 15:48

owen-mc-diffblue mentioned this pull request Sep 5, 2019

GOTO-symex: propagate notequal conditions for boolean types [TG-9390] #5089

Closed

owen-mc-diffblue changed the title ~~GOTO-symex: propagate notequal conditions for boolean types~~ [TG-9390] GOTO-symex: propagate notequal conditions for boolean types Sep 5, 2019

allredj reviewed Sep 5, 2019

View reviewed changes

owen-mc-diffblue force-pushed the goto-symex-propagate-notequal-conditions-for-boolean-types branch from 357dfbf to 2cca3cd Compare September 8, 2019 07:24

owen-mc-diffblue force-pushed the goto-symex-propagate-notequal-conditions-for-boolean-types branch from 2cca3cd to ab866c0 Compare September 8, 2019 07:31

owen-mc-diffblue force-pushed the goto-symex-propagate-notequal-conditions-for-boolean-types branch 3 times, most recently from 82dabf3 to 6bf2df6 Compare September 9, 2019 15:35

owen-mc-diffblue requested a review from romainbrenguier September 9, 2019 15:45

romainbrenguier approved these changes Sep 9, 2019

View reviewed changes

allredj reviewed Sep 9, 2019

View reviewed changes

owen-mc-diffblue force-pushed the goto-symex-propagate-notequal-conditions-for-boolean-types branch from 6bf2df6 to 96155fb Compare September 10, 2019 06:02

allredj reviewed Sep 10, 2019

View reviewed changes

allredj requested a review from JohnDumbell September 10, 2019 08:12

JohnDumbell approved these changes Sep 10, 2019

View reviewed changes

owen-mc-diffblue force-pushed the goto-symex-propagate-notequal-conditions-for-boolean-types branch from 96155fb to c9c7198 Compare September 12, 2019 10:18

smowton and others added 2 commits September 12, 2019 11:23

Unit tests for goto_state::apply_condition

d955e28

All the main branches are now covered

owen-mc-diffblue force-pushed the goto-symex-propagate-notequal-conditions-for-boolean-types branch from c9c7198 to 5bc512a Compare September 12, 2019 10:24

allredj reviewed Sep 12, 2019

View reviewed changes

peterschrammel approved these changes Sep 12, 2019

View reviewed changes

peterschrammel assigned owen-mc-diffblue Sep 12, 2019

owen-mc-diffblue force-pushed the goto-symex-propagate-notequal-conditions-for-boolean-types branch from 5bc512a to d312dad Compare September 13, 2019 08:14

allredj reviewed Sep 13, 2019

View reviewed changes

Test we don't call static initialisers unnecessarily

a2cbcc2

Previously we couldn't properly track when we had definitely already called them.

owen-mc-diffblue force-pushed the goto-symex-propagate-notequal-conditions-for-boolean-types branch from d312dad to a2cbcc2 Compare September 13, 2019 14:06

romainbrenguier approved these changes Sep 13, 2019

View reviewed changes

allredj reviewed Sep 13, 2019

View reviewed changes

owen-mc-diffblue merged commit d74a8d8 into diffblue:develop Sep 13, 2019

owen-mc-diffblue deleted the goto-symex-propagate-notequal-conditions-for-boolean-types branch September 13, 2019 17:07

[TG-9390] GOTO-symex: propagate notequal conditions for boolean types #5091

[TG-9390] GOTO-symex: propagate notequal conditions for boolean types #5091

Uh oh!

Conversation

owen-mc-diffblue commented Sep 5, 2019

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

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

Uh oh!

Codecov Report

Uh oh!

owen-mc-diffblue commented Sep 8, 2019

Uh oh!

owen-mc-diffblue commented Sep 9, 2019 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

smowton commented Sep 9, 2019

Uh oh!

smowton commented Sep 9, 2019

Uh oh!

owen-mc-diffblue commented Sep 9, 2019 • edited Loading Uh oh! There was an error while loading. Please reload this page.

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!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

romainbrenguier commented Sep 10, 2019

Uh oh!

allredj 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!

owen-mc-diffblue commented Sep 11, 2019

Uh oh!

owen-mc-diffblue commented Sep 11, 2019

Uh oh!

segun3d commented Sep 11, 2019

Uh oh!

owen-mc-diffblue commented Sep 11, 2019

Uh oh!

allredj 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!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

segun3d commented Sep 13, 2019

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

codecov-io commented Sep 5, 2019 •

edited

Loading

owen-mc-diffblue commented Sep 9, 2019 •

edited

Loading

owen-mc-diffblue commented Sep 9, 2019 •

edited

Loading