Simplifier: new interface, final piece [blocks: #4904] #4874

kroening · 2019-07-04T16:03:00Z

Reviewers of this series of PRs will be pleased to note that now all cases use the new interface.

Left to do is simplify_node and simplify_rec, and some auxiliary methods.

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

allredj

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

codecov-io · 2019-07-04T18:14:27Z

Codecov Report

❗ No coverage uploaded for pull request base (develop@a941ba9). Click here to learn what that means.
The diff coverage is 68.57%.

@@            Coverage Diff             @@
##             develop    #4874   +/-   ##
==========================================
  Coverage           ?   69.19%           
==========================================
  Files              ?     1307           
  Lines              ?   107952           
  Branches           ?        0           
==========================================
  Hits               ?    74697           
  Misses             ?    33255           
  Partials           ?        0

Impacted Files	Coverage Δ
src/util/simplify_expr_class.h	`88.88% <ø> (ø)`
src/util/simplify_utils.cpp	`100% <ø> (ø)`
src/util/simplify_expr_boolean.cpp	`89.04% <100%> (ø)`
src/util/simplify_expr_if.cpp	`39.16% <39.16%> (ø)`
src/util/simplify_expr_array.cpp	`86.76% <75%> (ø)`
src/util/simplify_expr_pointer.cpp	`79.59% <76.92%> (ø)`
src/util/simplify_expr.cpp	`87.23% <80%> (ø)`
src/util/simplify_expr_struct.cpp	`85.71% <82.14%> (ø)`
src/util/simplify_expr_int.cpp	`81.05% <87.61%> (ø)`

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 a941ba9...412754c. Read the comment docs.

allredj

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

allredj

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

allredj

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

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

tautschnig · 2019-07-12T14:42:05Z

I think this covers some of the comments I just posted on #4872, but actually the interfaces proposed here aren't as specific as could be. See comments in #4872 for more precise interfaces.

allredj

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

allredj

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

allredj

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

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

allredj

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

tautschnig · 2019-07-13T15:18:57Z

@kroening #4872 is merged, and thus this one now needs a rebase.

Expressions should not be given a type() child if they don't have one.

This improves type safety.

These have tight coupling, and there is a sufficient number of them.

allredj

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

tautschnig

Overall looks good, except for a couple of bugs where a changed(...) is missing - see detailed comments.

tautschnig · 2019-07-13T22:18:39Z

src/util/simplify_expr_array.cpp

@@ -31,86 +36,77 @@ bool simplify_exprt::simplify_index(exprt &expr)
       index.op0().op1()==index.op1())
    {
      exprt tmp=index.op0().op0();
-      expr.op1()=tmp;
+      index = tmp;


I don't think tmp carries any value anymore.

tautschnig · 2019-07-13T22:18:49Z

src/util/simplify_expr_array.cpp

      no_change = false;
    }
    else if(index.op0().id()==ID_mult &&
            index.op0().operands().size()==2 &&
            index.op0().op0()==index.op1())
    {
      exprt tmp=index.op0().op1();
-      expr.op1()=tmp;
+      index = tmp;


Get rid of tmp

tautschnig · 2019-07-13T22:20:54Z

src/util/simplify_expr_array.cpp

      }

      if_exprt if_expr(equality_expr, with_expr.new_value(), new_index_expr);
-      expr = simplify_if(if_expr).expr;
-      return false;
+      return simplify_if(if_expr).expr;


It might not make much of a difference, but elsewhere we seem to use return changed(simplify_if(if_expr));

tautschnig · 2019-07-13T22:23:21Z

src/util/simplify_expr_int.cpp

-    return simplify_inequality(expr);
+    auto new_expr = expr;
+    new_expr.op0().swap(new_expr.op1());
+    return simplify_inequality(new_expr); // recursive call


return changed(simplify_inequality(new_expr));

tautschnig · 2019-07-13T22:24:40Z

src/util/simplify_expr_struct.cpp

+      auto new_member_expr = expr;
+      new_member_expr.op0() = new_operands.front();
+      // do this recursively
+      return simplify_member(new_member_expr);


return changed(simplify_member(new_member_expr));

tautschnig · 2019-07-13T22:25:09Z

src/util/simplify_expr_struct.cpp

-      return false;
+      auto new_expr = expr;
+      new_expr.op0() = op.op0();
+      return simplify_member(new_expr);


return changed(simplify_member(new_expr));

tautschnig · 2019-07-13T22:30:30Z

src/util/simplify_expr.cpp

@@ -103,24 +103,24 @@ simplify_exprt::resultt<> simplify_exprt::simplify_abs(const abs_exprt &expr)
  return unchanged(expr);
 }

-simplify_exprt::resultt<> simplify_exprt::simplify_sign(const exprt &expr)
+simplify_exprt::resultt<> simplify_exprt::simplify_sign(const sign_exprt &expr)
 {
  if(expr.operands().size()!=1)
    return unchanged(expr);


I don't think this should be necessary anymore.

tautschnig · 2019-07-13T22:31:02Z

src/util/simplify_expr_int.cpp

@@ -771,32 +771,31 @@ simplify_exprt::resultt<> simplify_exprt::simplify_bitwise(const exprt &expr)
    return std::move(new_expr);
 }

-simplify_exprt::resultt<> simplify_exprt::simplify_extractbit(const exprt &expr)
+simplify_exprt::resultt<>
+simplify_exprt::simplify_extractbit(const extractbit_exprt &expr)
 {
  PRECONDITION(expr.id() == ID_extractbit);


No longer necessary.

tautschnig · 2019-07-13T22:33:29Z

src/util/simplify_expr_struct.cpp

  const irep_idt &component_name=
    to_member_expr(expr).get_component_name();

-  const exprt &op = expr.op0();
+  const exprt &op = expr.struct_op();


Use .compound(), struct_op carries a comment that "it will go away" (repeats below)

src/util/simplify_expr.cpp

This improves type safety.

This improves memory safety.

This improves type safety.

Follow-up from comment in #4872. The call is a no-op.

This improves type safety.

allredj

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

kroening added the cleanup label Jul 4, 2019

kroening requested review from peterschrammel, pkesseli, smowton and tautschnig as code owners July 4, 2019 16:03

kroening force-pushed the simplifier_new_interface3 branch 3 times, most recently from f825da3 to 6163a70 Compare July 4, 2019 17:21

allredj reviewed Jul 4, 2019

View reviewed changes

kroening force-pushed the simplifier_new_interface3 branch from acbd1ad to f1e14a8 Compare July 5, 2019 09:00

allredj reviewed Jul 5, 2019

View reviewed changes

allredj reviewed Jul 7, 2019

View reviewed changes

kroening force-pushed the simplifier_new_interface3 branch from f9e72a5 to aadd948 Compare July 7, 2019 13:02

allredj reviewed Jul 7, 2019

View reviewed changes

tautschnig assigned kroening Jul 12, 2019

This was referenced Jul 13, 2019

simplifier: use new interface #4872

Merged

simplifier: eliminate casts from bool to number #4904

Merged

kroening assigned tautschnig and unassigned kroening Jul 13, 2019

kroening force-pushed the simplifier_new_interface3 branch from f3bf107 to c5d779c Compare July 13, 2019 11:57

allredj reviewed Jul 13, 2019

View reviewed changes

tautschnig removed their assignment Jul 13, 2019

tautschnig added the blocker label Jul 13, 2019

Daniel Kroening added 5 commits July 13, 2019 14:53

simplifier: use new interface

eda7601

simplifier: prevent spurious adding of type

ef6cceb

Expressions should not be given a type() child if they don't have one.

simplifier: simplify_rec has new interface

a7a20a4

This improves type safety.

simplifier: move if_expr related methods into separate file

5295cb7

These have tight coupling, and there is a sufficient number of them.

simplify_expr_if: result -> nochange

37b642c

kroening force-pushed the simplifier_new_interface3 branch from c5d779c to cb9dbc4 Compare July 13, 2019 18:54

kroening removed the Needs rebase label Jul 13, 2019

allredj reviewed Jul 13, 2019

View reviewed changes

tautschnig requested changes Jul 13, 2019

View reviewed changes

Daniel Kroening added 13 commits July 14, 2019 07:58

simplify_inequality_* methods use new interface

5d180cb

This improves type safety.

type simplify_sign

db75bb7

This improves memory safety.

type simplify_extractbit

b42d47d

This improves memory safety.

type simplify_bitnot

866acc9

This improves memory safety.

type simplify_not

d061aaa

This improves memory safety.

type simplify_index

1d53296

This improves memory safety.

type simplify_member

7fe4561

This improves memory safety.

type simplify_unary_minus

fddeaf9

This improves memory safety.

simplifier: type remaining methods for unary expressions

be1f6fa

This improves memory safety.

type simplify_concatenation

488e4ef

This improves type safety.

type simplify_unary_plus

2099dfe

This improves type safety.

removed unneeded call to simplify_node in simplify_boolean

16e18d2

Follow-up from comment in #4872. The call is a no-op.

improved typing in simplify_boolean

412754c

This improves type safety.

kroening assigned tautschnig and unassigned kroening Jul 14, 2019

kroening force-pushed the simplifier_new_interface3 branch from cb9dbc4 to 412754c Compare July 14, 2019 11:59

allredj reviewed Jul 14, 2019

View reviewed changes

tautschnig approved these changes Jul 14, 2019

View reviewed changes

tautschnig merged commit 250b140 into develop Jul 14, 2019

tautschnig deleted the simplifier_new_interface3 branch July 14, 2019 14:11

Simplifier: new interface, final piece [blocks: #4904] #4874

Simplifier: new interface, final piece [blocks: #4904] #4874

Uh oh!

Conversation

kroening commented Jul 4, 2019 • 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!

codecov-io commented Jul 4, 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!

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!

tautschnig commented Jul 12, 2019

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!

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!

tautschnig commented Jul 13, 2019

Uh oh!

allredj left a comment

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!

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!

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

kroening commented Jul 4, 2019 •

edited

Loading

codecov-io commented Jul 4, 2019 •

edited

Loading