Constant propagator: improve GOTO condition propagation by smowton · Pull Request #2522 · diffblue/cbmc

smowton · 2018-07-04T16:59:01Z

This improves two-way propagation to also account for many other common patterns that imply an equality (e.g. x != y -> x == !y when the operands are of boolean types, or !x --> x == TRUE). I also fix a case where the fixpoint loop around the && case would loop forever because assign_rec can both enlarge and shrink its value-set -- for example, the condition x == 5 && **unknown == (void*)also_unknown would result in repeatedly adding x -> 5 and the clobbering the entire value set. I fix that by noting that in the context of two-way propagation, since there's no write operation taking place we should never shrink the value set.

allredj

Passed Diffblue compatibility checks (cbmc commit: d61ce78).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/78115950

hannes-steffenhagen-diffblue

I don't completely understand the two way propagation, but this looks reasonable to me.

hannes-steffenhagen-diffblue · 2018-07-05T14:28:02Z

src/analyses/constant_propagator.h


  dirtyt dirty;

+  std::function<bool(const exprt &, const namespacet &)> should_track_value;


I'm not a fan of this being a public member. IMHO would be better to have this private. If this needs to be called from the outside, we could just call it should_track_value_handler and have a method should_track_value call this. It being public just invites shenanigans with people manually overwriting it.

hannes-steffenhagen-diffblue · 2018-07-05T14:50:01Z

src/analyses/constant_propagator.cpp

+    if(lhs.is_constant() && !rhs.is_constant())
+      std::swap(lhs, rhs);
+
+    if(!(rhs.is_constant() && !lhs.is_constant()))


I think it'd be clearer to expand the not here: lhs.is_constant() || !rhs.is_constant().

hannes-steffenhagen-diffblue · 2018-07-05T14:53:00Z

src/analyses/constant_propagator.cpp

+    // (int)var xx 0 ==> var xx (_Bool)0 or similar
+    // Note this is restricted to bools because in general turning a widening
+    // into a narrowing typecast is not correct.
+    if(lhs.id() == ID_typecast && rhs.id() == ID_constant &&


rhs.id() == ID_constant should always be true at this point.

hannes-steffenhagen-diffblue · 2018-07-05T15:04:16Z

unit/analyses/constant_propagator.cpp

+    // Create a program like:
+    // bool b0, b1, b2, ...;
+    // int marker;
+    // if(b0)


Would it be possible / reasonable to break this up into multiple smaller examples? Something this big is a bit difficult to follow.

hannes-steffenhagen-diffblue · 2018-07-05T15:27:55Z

Marking do not merge as it's based on another commit that should go in first

peterschrammel · 2018-07-05T16:37:02Z

unit/analyses/constant_propagator.cpp

+
+    symbolt main_function_symbol;
+    main_function_symbol.name = "main";
+    main_function_symbol.type = code_typet();


This constructor is deprecated.

peterschrammel · 2018-07-05T16:37:14Z

unit/analyses/constant_propagator.cpp

+
+    symbolt main_function_symbol;
+    main_function_symbol.name = "main";
+    main_function_symbol.type = code_typet();


This constructor is deprecated.

smowton · 2018-07-06T12:27:46Z

Comments mostly applied-- but this is parked for now pending #2132 landing.

allredj

Passed Diffblue compatibility checks (cbmc commit: bf3d12c).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/78301619

danpoe

Looks good to me

danpoe · 2018-07-10T13:25:35Z

src/analyses/constant_propagator.cpp

+      else
+        rhs = from_integer(0, rhs.type());
+
+      two_way_propagate_rec(equal_exprt(lhs, rhs), ns, cp);


Could we use assign_rec() here?

smowton · 2018-09-11T09:14:17Z

Noting this is still blocked on 2132 as noted above, I believe action @tautschnig

tautschnig · 2018-09-19T16:02:45Z

Noting this is still blocked on 2132 as noted above, I believe action @tautschnig

... which in turn is blocked by #2221 - @kroening @peterschrammel @smowton ;-)

tautschnig · 2018-11-15T10:12:56Z

In light of #2132 let me dare and go for high-level comments first:

It may be worth removing the changes to two-way-propagation from Improvements to goto-analyzer's constant propagator and simplifier [blocks: #2522] #2132, and instead put this in to this PR here. Notably, that commit introduces a regression test that I'd like to have in place before any of the changes go in.
There are simple improvements in this PR that help readability a lot but don't even change behaviour, such as removing the return value. Maybe that could go in a commit of its own? No tests needed as it would be covered by the regression test.
Then there are strict extensions of functionality, such as dealing with negation or plain Booleans. Again, might be worth a commit of its own. That commit could nicely include tests showcasing the improvement.
Finally, there is the refactoring of existing functionality, which is probably the part that requires the most care. As such it would be really nice to have all the other parts factored out so that one can very easily read that bit of code/that particular change.
And then there's the test: unit tests are good, because they very selectively test functionality. But also they can be very hard to read, because they have to do a lot of work that is done by other components. As such I'd prefer to also have plain C examples. Now throwing away all the work that has gone into the unit test would also seem like a bad idea. Can we maybe have both?

Improvements to goto-analyzer's constant propagator and simplifier [blocks: #2522]

tautschnig · 2018-12-19T18:34:29Z

@smowton #2132 is in, so this one should be ready to be rebased.

smowton · 2018-12-20T10:57:38Z

@tautschnig rebased and improved somewhat, and described the new state of affairs in the PR description -- please re-review

tautschnig · 2018-12-20T11:34:28Z

@smowton clang-format demands more work :-)

tautschnig

Could do with a bunch of cleanup as indicated in comments, but otherwise ok.

tautschnig · 2018-12-20T11:38:08Z

src/analyses/constant_propagator.cpp

    // to on the left-hand side - bail and set all values to top to be on the
    // safe side in terms of soundness
-    dest_values.set_to_top();
+    if(is_assignment)


How about changing the above else to else if(is_assignment) and then even simplifying the comment a bit?

tautschnig · 2018-12-20T11:39:38Z

src/analyses/constant_propagator.cpp

 #endif

-  bool change=false;
+  bool change = false;


Unrelated change?

src/analyses/constant_propagator.cpp

tautschnig · 2018-12-20T11:43:13Z

unit/analyses/constant_propagator.cpp

+{
+  code_ifthenelset new_cond;
+  new_cond.cond() = test;
+  new_cond.then_case() = to_wrap;


Use the new code_ifthenelset constructor.

tautschnig · 2018-12-20T11:43:39Z

unit/analyses/constant_propagator.cpp

+    //   b = true;
+    // Repeat this using bool_typet and c_bool_typet for "bool".
+
+    null_message_handlert null_out;


There is a global one defined for the unit tests.

tautschnig · 2018-12-20T11:44:17Z

unit/analyses/constant_propagator.cpp

+
+    code_blockt code;
+    code.copy_to_operands(code_declt(bool_local.symbol_expr()));
+    code.copy_to_operands(code_declt(c_bool_local.symbol_expr()));


Might use the initializer-list constructor

tautschnig · 2018-12-20T11:45:12Z

unit/analyses/constant_propagator.cpp

+    const exprt c_bool_true = from_integer(1, c_bool_typet(8));
+    c_bool_cond_block.cond() =
+      notequal_exprt(c_bool_local.symbol_expr(), c_bool_true);
+    c_bool_cond_block.then_case() =


Use recently added constructor

tautschnig · 2018-12-20T11:45:34Z

unit/analyses/constant_propagator.cpp

+      code_assignt(c_bool_local.symbol_expr(), c_bool_true);
+
+    code.move_to_operands(bool_cond_block);
+    code.move_to_operands(c_bool_cond_block);


move_to_operands is deprecated

tautschnig · 2018-12-20T11:46:58Z

unit/analyses/constant_propagator.cpp

+    for(const exprt &test : c_bool_tests)
+      wrap_with_test(program, test);
+
+    null_message_handlert null_out;


Use global one

smowton · 2019-01-02T17:12:10Z

@tautschnig @chrisr-diffblue @peterschrammel this is updated and ready for re-review.

allredj

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

tautschnig · 2019-01-02T22:14:45Z

src/analyses/constant_propagator.cpp

-  else if(expr.id()==ID_equal)
+  else if(expr.id() == ID_symbol)
+  {
+    if(expr.type() == bool_typet())


I'd use expr.type().id() == ID_bool to be consistent with what you're using above.

tautschnig · 2019-01-02T22:16:14Z

src/analyses/constant_propagator.cpp

+  // into a narrowing typecast is not correct.
+  if(
+    lhs.id() == ID_typecast &&
+    (lhs.op0().type().id() == ID_bool || lhs.op0().type().id() == ID_c_bool))


I'd rewrite this code a bit to do an early if(lhs.id() != ID_typecast) return; and then use to_typecast_expr instead of using the generic .op0().

tautschnig · 2019-01-02T22:18:10Z

unit/analyses/constant_propagator.cpp

  return has_prefix(id2string(to_symbol_expr(e).get_identifier()), "x");
 }

+static void wrap_with_test(codet &to_wrap, const exprt &test)


Does this function actually still add value? Doing this one-liner inline might aid clarity.

smowton · 2019-01-03T12:58:29Z

Updated as requested (except comparison with bool_typet, which I think is better than checking for ID_bool). Will merge when CI passes.

tautschnig · 2019-01-03T13:02:50Z

(except comparison with bool_typet, which I think is better than checking for ID_bool)

I'm not disputing that, but I'm unhappy about mixing both approaches in a single commit. But this is a very minor issue indeed.

This supports propagation of booleans in more situations, including propagating "x != false" and "IF x" like "IF x == TRUE".

smowton · 2019-01-03T13:13:54Z

Ah sure, switched to use full type comparison everywhere.

allredj

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

chrisr-diffblue

LGTM

smowton requested review from chrisr-diffblue, martin-cs, peterschrammel and thk123 as code owners July 4, 2018 16:59

smowton requested a review from danpoe July 4, 2018 16:59

allredj reviewed Jul 4, 2018

View reviewed changes

smowton requested a review from hannes-steffenhagen-diffblue July 5, 2018 07:54

hannes-steffenhagen-diffblue approved these changes Jul 5, 2018

View reviewed changes

hannes-steffenhagen-diffblue added the do not merge label Jul 5, 2018

peterschrammel reviewed Jul 5, 2018

View reviewed changes

smowton force-pushed the smowton/feature/constant-propagator-improvement branch from d61ce78 to 4705ed7 Compare July 6, 2018 12:25

smowton requested a review from a team as a code owner July 6, 2018 12:25

smowton force-pushed the smowton/feature/constant-propagator-improvement branch 2 times, most recently from 1af51c0 to 3eec1a7 Compare July 6, 2018 12:27

smowton force-pushed the smowton/feature/constant-propagator-improvement branch 2 times, most recently from 931c74d to bf3d12c Compare July 6, 2018 12:44

allredj reviewed Jul 6, 2018

View reviewed changes

danpoe approved these changes Jul 10, 2018

View reviewed changes

tautschnig assigned smowton Sep 3, 2018

tautschnig mentioned this pull request Nov 15, 2018

Improvements to goto-analyzer's constant propagator and simplifier [blocks: #2522] #2132

Merged

5 tasks

tautschnig added a commit that referenced this pull request Dec 19, 2018

Merge pull request #2132 from tautschnig/extend-simplifier

053ae9c

Improvements to goto-analyzer's constant propagator and simplifier [blocks: #2522]

tautschnig removed the do not merge label Dec 19, 2018

smowton force-pushed the smowton/feature/constant-propagator-improvement branch from bf3d12c to f988768 Compare December 20, 2018 10:53

tautschnig approved these changes Dec 20, 2018

View reviewed changes

tautschnig assigned peterschrammel, martin-cs and chrisr-diffblue Dec 20, 2018

smowton force-pushed the smowton/feature/constant-propagator-improvement branch from f988768 to 06e6573 Compare January 2, 2019 17:05

allredj reviewed Jan 2, 2019

View reviewed changes

tautschnig approved these changes Jan 2, 2019

View reviewed changes

smowton force-pushed the smowton/feature/constant-propagator-improvement branch from 06e6573 to dc31f10 Compare January 3, 2019 12:52

Constant propagator: improve boolean propagation

897ffda

This supports propagation of booleans in more situations, including propagating "x != false" and "IF x" like "IF x == TRUE".

smowton force-pushed the smowton/feature/constant-propagator-improvement branch from dc31f10 to 897ffda Compare January 3, 2019 13:13

allredj reviewed Jan 3, 2019

View reviewed changes

tautschnig unassigned smowton Jan 3, 2019

chrisr-diffblue approved these changes Jan 3, 2019

View reviewed changes

smowton merged commit 4b05dcb into diffblue:develop Jan 3, 2019


		dirtyt dirty;

		std::function<bool(const exprt &, const namespacet &)> should_track_value;

Conversation

smowton commented Jul 4, 2018 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

hannes-steffenhagen-diffblue 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!

hannes-steffenhagen-diffblue commented Jul 5, 2018

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

smowton commented Jul 6, 2018

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

danpoe left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

smowton commented Sep 11, 2018

Uh oh!

tautschnig commented Sep 19, 2018

Uh oh!

tautschnig commented Nov 15, 2018

Uh oh!

tautschnig commented Dec 19, 2018

Uh oh!

smowton commented Dec 20, 2018

Uh oh!

tautschnig commented Dec 20, 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!

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!

smowton commented Jan 2, 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!

Choose a reason for hiding this comment

Uh oh!

smowton commented Jan 3, 2019

Uh oh!

tautschnig commented Jan 3, 2019

smowton commented Jul 4, 2018 •

edited

Loading