check for side effects in quantifiers by kroening · Pull Request #2979 · diffblue/cbmc

kroening · 2018-09-18T15:16:27Z

Each commit message has a non-empty body, explaining why the change was made.
My contribution is formatted in line with CODING_STANDARD.md.
Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
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.

tautschnig · 2018-09-19T10:30:01Z

src/goto-programs/goto_clean_expr.cpp

  // g2 = (i > 10)
  // forall (i : int) (g1 || g2)
-  if(expr.id()==ID_forall || expr.id()==ID_exists)
-    return false;


The comment above this code needs to be moved, it doesn't actually make sense when these lines are removed.

tautschnig · 2018-09-19T10:31:03Z

src/goto-programs/goto_clean_expr.cpp

    goto_programt tmp;
    clean_expr(expr.op1(), tmp, mode, true);
-    if(tmp.instructions.empty())
+    if(!tmp.instructions.empty())


So this was dead code before. It's no longer dead code now - do we have any tests exercising it?

kroening · 2018-09-23T13:06:42Z

Now with different approach -- the rule is now checked in the front-end

allredj

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

smowton · 2018-09-24T08:50:51Z

src/goto-programs/goto_clean_expr.cpp

-      throw 0;
-    }
-    return;
+    // the front-end checks these for side-effects


DATA_INVARIANT(!has_subexpr(expr, ID_side_effect), "the front-end should check quantified expressions for side-effects");

tautschnig

I'd suggest to simplify as described below.

tautschnig · 2018-09-24T09:38:31Z

src/ansi-c/c_typecheck_expr.cpp

  return false;
 }

+static bool has_side_effect(const exprt &expr)


No need - see below.

tautschnig · 2018-09-24T09:38:55Z

src/ansi-c/c_typecheck_expr.cpp

      throw 0;
    }

+    if(has_side_effect(expr.op1()))


if(has_subexpr(expr.op1(), ID_side_effect))

tautschnig · 2018-09-24T09:40:00Z

src/goto-programs/goto_clean_expr.cpp

-      throw 0;
-    }
-    return;
+    // the front-end checks these for side-effects


DATA_INVARIANT(!has_subexpr(expr, ID_side_effect), "the front-end should check quantified expressions for side-effects");

tautschnig

Looks good, except for the line break.

tautschnig · 2018-09-26T09:25:17Z

src/goto-programs/goto_clean_expr.cpp

-      throw 0;
-    }
-    return;
+    DATA_INVARIANT(!has_subexpr(expr, ID_side_effect), "the front-end should check quantified expressions for side-effects");


This line got too long.

allredj

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

This fixes a failed attempt to check for quantifiers during goto conversion by checking earlier in the C front-end.

allredj

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

kroening added bugfix work in progress labels Sep 18, 2018

kroening requested review from peterschrammel, pkesseli, smowton and tautschnig as code owners September 18, 2018 15:16

smowton approved these changes Sep 19, 2018

View reviewed changes

tautschnig requested changes Sep 19, 2018

View reviewed changes

kroening force-pushed the quantifier-sideeffects branch from cc4fae7 to a887387 Compare September 23, 2018 13:06

kroening force-pushed the quantifier-sideeffects branch from a887387 to 0812cc1 Compare September 23, 2018 21:30

allredj reviewed Sep 23, 2018

View reviewed changes

smowton reviewed Sep 24, 2018

View reviewed changes

tautschnig requested changes Sep 24, 2018

View reviewed changes

tautschnig assigned kroening Sep 24, 2018

kroening force-pushed the quantifier-sideeffects branch from 0812cc1 to f505207 Compare September 26, 2018 09:19

kroening removed the work in progress label Sep 26, 2018

kroening assigned tautschnig and unassigned kroening Sep 26, 2018

tautschnig approved these changes Sep 26, 2018

View reviewed changes

tautschnig assigned kroening and unassigned tautschnig Sep 26, 2018

allredj reviewed Sep 26, 2018

View reviewed changes

check for side effects in quantifiers in the front-end

a3fa911

This fixes a failed attempt to check for quantifiers during goto conversion by checking earlier in the C front-end.

tautschnig force-pushed the quantifier-sideeffects branch from f505207 to a3fa911 Compare September 26, 2018 13:13

tautschnig mentioned this pull request Sep 26, 2018

Invariant cleanup in flattening/boolbv_extractbit.cpp and flattening/boolbv_extractbits.cpp #3041

Merged

7 tasks

tautschnig merged commit 095fb3d into develop Sep 26, 2018

tautschnig deleted the quantifier-sideeffects branch September 26, 2018 14:49

allredj reviewed Sep 26, 2018

View reviewed changes

Conversation

kroening commented Sep 18, 2018 • 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!

kroening commented Sep 23, 2018

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!

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!

Choose a reason for hiding this comment

Uh oh!

tautschnig left a comment

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!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

kroening commented Sep 18, 2018 •

edited

Loading