Assert type consistency in the simplifier by tautschnig · Pull Request #2064 · diffblue/cbmc

tautschnig · 2018-04-15T22:35:34Z

No description provided.

smowton · 2018-04-16T14:50:36Z

src/analyses/goto_check.cpp

    {
-      exprt overflow("overflow-"+expr.id_string(), bool_typet());
-      overflow.operands()=expr.operands();
+      exprt tmp;


Rename binary_check_lhs?

smowton · 2018-04-16T14:51:30Z

src/analyses/goto_check.cpp

  {
-    if(expr.operands().size()==2)
+    // The overflow checks are binary!
+    // We break these up.


... e.g. for "a + b + c + d" we check "a + b", "(a + b) + c", "(a + b + c) + d"

smowton · 2018-04-16T14:51:54Z

src/analyses/goto_check.cpp

+        tmp.operands().resize(i);
+      }
+
+      exprt tmp2 = expr;


Rename binary_check?

smowton · 2018-04-16T14:56:14Z

src/analyses/goto_check.cpp

+    exprt overflow("overflow-" + expr.id_string(), bool_typet());
+    overflow.operands() = expr.operands();
+
+    // this is overflow over integers


How about // check for address space overflow, since I guess the point is we're checking whether we wrap the VAS?

kroening · 2018-04-17T16:51:20Z

Why not simply use make_binary()?

kroening · 2018-04-17T16:52:44Z

Ok, that has type checks that will fail -- I would add a separate function make_pointer_arithmetic_binary, which relaxes the check, and then call that.

tautschnig · 2018-04-18T08:45:28Z

I will overhaul this PR completely as I have in parts been solving the wrong problem. Notably, the expressions passed to pointer_overflow_check are always binary. Step 1 will be adding a test that uses --pointer-overflow-check ...

tautschnig · 2018-04-18T12:17:50Z

@kroening @smowton This PR has been almost completely changed, please take a fresh look.

tautschnig · 2018-04-19T00:40:09Z

This turned into a surprisingly widespread bug-fixing session. Can @romainbrenguier please take a look at the changes I had to make in the string refinement, @kroening please comment on fixes in the simplifier.

romainbrenguier · 2018-04-19T13:08:05Z

src/solvers/refinement/string_refinement.cpp

+  while(s.id() == ID_if)
+  {
+    if_exprt s_if = to_if_expr(s);
+    simplify(s_if.cond(), ns);


this copies the whole s exprt, would it be better to just copy the condition?

and why is this not part of simplify_expr?

I will change this to exprt simp_cond = simplify_expr(to_if_expr(s).cond(), ns); with another to_if_expr(s).{true,false}_case() below.

romainbrenguier · 2018-04-19T13:09:32Z

src/util/simplify_expr_int.cpp

        bool value=op.is_true();
-        op=constant_exprt(value?ID_1:ID_0, unsignedbv_typet(1));
+        op = constant_exprt(
+          value ? ID_1 : ID_0, bitvector_typet(expr.type().id(), 1));


value should be const, or could be inlined here

~~True, but unrelated to the fix here? Let me know if you insist, though.~~ I have made the change.

array_poolt::make_char_array_for_char_pointer generates conditional expressions denoting possible array sizes. This results in types without a fixed size, and is used to construct ifthenelse expressions that may have multiple types. This is not permitted, and thus must be filtered out before passing to further processing, such as simplification or flattening.

If the simplifier receives an expression that isn't type-consistent it might produce a type-inconsistent result, but we will now fail an invariant in that case.

tautschnig · 2019-03-07T07:06:35Z

This is now ready for review - @romainbrenguier in particular, but maybe also @martin-cs and @peterschrammel.

romainbrenguier

I will do a TG pull request to check no invariant fails on our tests.

romainbrenguier · 2019-03-07T07:21:48Z

src/solvers/strings/string_refinement.cpp

  exprt simple_lemma = lemma;
  if(simplify_lemma)
+  {
+    simple_lemma = adjust_if_recursive(std::move(simple_lemma), ns);


This will probably not get rid of all the inconsistencies, so I'm not sure about how useful it is. Ideally we should get rid of the introduction of type inconsistencies, but I'm not sure about the best way to do that.

I recall having tried removing them completely (which would be done by using type casts), but that did not seem to work very well. It's the long-term solution, and maybe that's what we should actually invest in instead of this hack. Not sure though, I'm certainly curious about the results with TG!

Everything is green on our side, so nothing blocking merging it.

allredj

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

tautschnig requested review from chrisr-diffblue, martin-cs, peterschrammel, smowton and thk123 as code owners April 15, 2018 22:35

tautschnig mentioned this pull request Apr 15, 2018

Make pointer encoding sound wrt integer address translation (and lift object limits) #1086

Closed

tautschnig force-pushed the pointer-overflow-check branch from 6ea9073 to 4ad5c54 Compare April 16, 2018 06:39

tautschnig assigned smowton, thk123, peterschrammel, martin-cs and chrisr-diffblue Apr 16, 2018

smowton reviewed Apr 16, 2018

View reviewed changes

tautschnig force-pushed the pointer-overflow-check branch from 4ad5c54 to bdd71ab Compare April 18, 2018 12:16

tautschnig requested a review from kroening as a code owner April 18, 2018 12:16

tautschnig changed the title ~~pointer-overflow-check: support >2 operands~~ Fix pointer-arithmetic simplification and add tests Apr 18, 2018

tautschnig added the bugfix label Apr 18, 2018

tautschnig force-pushed the pointer-overflow-check branch from bdd71ab to 4ea6c4c Compare April 19, 2018 00:33

tautschnig requested a review from romainbrenguier as a code owner April 19, 2018 00:33

tautschnig assigned romainbrenguier and kroening Apr 19, 2018

tautschnig force-pushed the pointer-overflow-check branch from 4ea6c4c to 18c6c1f Compare April 19, 2018 06:06

romainbrenguier reviewed Apr 19, 2018

View reviewed changes

tautschnig force-pushed the pointer-overflow-check branch 2 times, most recently from 37fbecb to ba7ce39 Compare April 20, 2018 00:40

tautschnig requested a review from pkesseli as a code owner February 13, 2019 12:24

tautschnig changed the title ~~Fix pointer-arithmetic simplification and add tests~~ Assert type consistency in the simplifier [depends-on: #4056] Feb 13, 2019

tautschnig added dependent - do not merge and removed bugfix labels Feb 13, 2019

tautschnig force-pushed the pointer-overflow-check branch from 93b83cf to 5ceaec0 Compare March 2, 2019 14:27

tautschnig changed the title ~~Assert type consistency in the simplifier [depends-on: #4056]~~ Assert type consistency in the simplifier [depends-on: #4314] Mar 2, 2019

tautschnig force-pushed the pointer-overflow-check branch from 5ceaec0 to 6a4d11d Compare March 3, 2019 00:06

tautschnig requested review from allredj, danpoe, hannes-steffenhagen-diffblue and owen-mc-diffblue as code owners March 3, 2019 00:06

tautschnig force-pushed the pointer-overflow-check branch from 6a4d11d to 151babd Compare March 3, 2019 21:16

tautschnig added 3 commits March 7, 2019 07:04

Expression simplification must not alter the type

c564c2c

Simplifier: As we now assert type equality we can remove a safety net

8616586

If the simplifier receives an expression that isn't type-consistent it might produce a type-inconsistent result, but we will now fail an invariant in that case.

tautschnig force-pushed the pointer-overflow-check branch from 151babd to 8616586 Compare March 7, 2019 07:05

tautschnig changed the title ~~Assert type consistency in the simplifier [depends-on: #4314]~~ Assert type consistency in the simplifier Mar 7, 2019

tautschnig removed the dependent - do not merge label Mar 7, 2019

tautschnig assigned peterschrammel, martin-cs and romainbrenguier and unassigned tautschnig Mar 7, 2019

romainbrenguier reviewed Mar 7, 2019

View reviewed changes

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

allredj reviewed Mar 7, 2019

View reviewed changes

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

romainbrenguier approved these changes Mar 7, 2019

View reviewed changes

tautschnig merged commit bc6c41e into diffblue:develop Mar 7, 2019

tautschnig deleted the pointer-overflow-check branch March 7, 2019 10:18

Conversation

tautschnig commented Apr 15, 2018

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!

kroening commented Apr 17, 2018

Uh oh!

kroening commented Apr 17, 2018

Uh oh!

tautschnig commented Apr 18, 2018

Uh oh!

tautschnig commented Apr 18, 2018

Uh oh!

tautschnig commented Apr 19, 2018

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!

tautschnig Apr 19, 2018 • 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!

tautschnig commented Mar 7, 2019

Uh oh!

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

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

9 participants

tautschnig Apr 19, 2018 •

edited

Loading