simplifier: new interface for simplify_node #4982

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Merged

tautschnig merged 2 commits into develop from simplify_node_interface

Aug 6, 2019

Member

kroening commented Aug 4, 2019

This improves type safety. It's the final major interface in the simplifier to use the new API style.

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/
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.

kroening added the cleanup label

kroening requested review from peterschrammel, pkesseli, smowton and tautschnig as code owners

August 4, 2019 15:01

kroening assigned tautschnig

allredj reviewed

View reviewed changes

Contributor

allredj left a comment

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

tautschnig requested changes

View reviewed changes

Collaborator

tautschnig left a comment

Touching old code highlights a lot of room for improvement - can we get this done?

src/util/simplify_expr_if.cpp

-                      simplify_node(tmp);
-                      return std::move(tmp);
+                      return changed(simplify_node(
+                        or_exprt(simplify_node(boolean_negate(cond)), truevalue)));

Collaborator

tautschnig Aug 5, 2019

As agreed in another PR, calling simplify_node on the result of boolean_negate is unnecessary. Unrelated to this PR, but should be fixed now that we're looking at this code. Applies here and below.

src/util/simplify_expr.cpp

                           exprt new_value(with.new_value());
                           auto tmp = expr;
-                          tmp.set_offset(std::move(new_offset));
+                          tmp.set_offset(simplify_node(std::move(new_offset)));

Collaborator

tautschnig Aug 5, 2019

simplify_node takes a const exprt & as argument, the std::move doesn't seem to be useful?

Member Author

kroening Aug 5, 2019

fixed

src/util/simplify_expr.cpp

                           exprt new_value(with.new_value());
                           auto tmp = expr;
-                          tmp.set_offset(std::move(new_offset));
+                          tmp.set_offset(simplify_node(std::move(new_offset)));
                           tmp.set_value(std::move(new_value));

Collaborator

tautschnig Aug 5, 2019

This code could really do with some cleanup: 1) I'd move the definitions (new_offset, new_value) closer to their use; 2) creating an explicit copy in new_value just so that we can std::move it seems to have little value.

src/util/simplify_expr.cpp

                   auto new_expr = expr;
-                  new_expr.op() = std::move(inequality);
+                  new_expr.op() = simplify_node(std::move(inequality));

Collaborator

tautschnig Aug 5, 2019

See below: std::move doesn't seem to be very useful here.

Member Author

kroening Aug 5, 2019

Fixed -- the method now takes an exprt as argument.

src/util/simplify_expr.cpp Outdated

                         // index_offset may need a typecast
                         if(offset.type() != index.type())
                         {
                           typecast_exprt tmp(index_offset, offset.type());
-                          simplify_node(tmp);
-                          index_offset.swap(tmp);
+                          index_offset = simplify_node(std::move(tmp));

Collaborator

tautschnig Aug 5, 2019

As above: std::move seems useless (and tmp could be inlined, the name doesn't add clarity)

Member Author

kroening Aug 5, 2019

done

src/util/simplify_expr_pointer.cpp

-                    simplify_node(new_expr);
-                    return new_expr;
+                    return changed(simplify_node(new_expr));

Collaborator

tautschnig Aug 5, 2019

Is there anything to simplify here? AFAIK we don't usually run simplify_node on the result of from_integer.

src/util/simplify_expr_pointer.cpp

-                    simplify_node(new_expr);
-                    return new_expr;
+                    return changed(simplify_node(new_expr));

Collaborator

tautschnig Aug 5, 2019

As above: nothing to simplify.

src/util/simplify_expr_pointer.cpp Outdated

                   {
                     new_inequality_ops.push_back(typecast_exprt::conditional_cast(
                       op, new_inequality_ops.front().type()));
-                    simplify_node(new_inequality_ops.back());
+                    new_inequality_ops.back() = simplify_node(new_inequality_ops.back());

Collaborator

tautschnig Aug 5, 2019

new_inequality_ops.push_back(simplify_node(typecast_exprt::conditional_cast(...

Member Author

kroening Aug 5, 2019

done

src/util/simplify_expr_pointer.cpp

                       if(size.type() != expr_type)
                       {
                         size = typecast_exprt(size, expr_type);
-                        simplify_node(size);
+                        size = simplify_node(size);

Collaborator

tautschnig Aug 5, 2019

simplify_typecast?

src/util/simplify_expr_pointer.cpp

-                simplify_node(def);
-                return std::move(def);
+                return changed(simplify_node(def));

Collaborator

tautschnig Aug 5, 2019

good_pointer_def is far from trivial - I believe this requires simplify_rec

tautschnig assigned kroening and unassigned tautschnig

kroening force-pushed the simplify_node_interface branch 2 times, most recently from 5a1c799 to 1107bf1 Compare

August 5, 2019 15:33

Member Author

kroening commented Aug 5, 2019

I'll do a follow-up PR reviewing whether simplify_node is appropriate to use.
This seems to be beyond the interface change in terms of scope.

kroening force-pushed the simplify_node_interface branch from 1107bf1 to 4b90551 Compare

August 5, 2019 16:21

Daniel Kroening added 2 commits

August 5, 2019 19:46


          simplifier: new interface for simplify_node

be5a2d5

This improves type safety.


          use mult_exprt/plus_exprt instead of binary_exprt

85e8337

This is shorter and easier to read.

kroening force-pushed the simplify_node_interface branch from 4b90551 to 85e8337 Compare

August 5, 2019 18:46

codecov-io commented Aug 5, 2019

Codecov Report

Merging #4982 into develop will decrease coverage by <.01%.
The diff coverage is 90%.

@@             Coverage Diff             @@
##           develop    #4982      +/-   ##
===========================================
- Coverage    69.24%   69.24%   -0.01%     
===========================================
  Files         1309     1309              
  Lines       108478   108463      -15     
===========================================
- Hits         75119    75107      -12     
+ Misses       33359    33356       -3

Impacted Files	Coverage Δ
src/util/simplify_expr_class.h	`88.88% <ø> (ø)`	⬆️
src/util/simplify_expr_if.cpp	`35.39% <100%> (-3.77%)`	⬇️
src/util/simplify_expr_struct.cpp	`85.71% <100%> (-0.16%)`	⬇️
src/util/simplify_expr_boolean.cpp	`88.73% <100%> (-0.16%)`	⬇️
src/util/simplify_expr_int.cpp	`80.49% <100%> (ø)`	⬆️
src/util/simplify_expr_array.cpp	`86.76% <100%> (-0.2%)`	⬇️
src/util/simplify_expr_pointer.cpp	`79.45% <82.35%> (-0.15%)`	⬇️
src/util/simplify_expr.cpp	`87.6% <82.35%> (+0.22%)`	⬆️
jbmc/src/java_bytecode/java_entry_point.cpp	`87.68% <0%> (+0.06%)`	⬆️

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 0a990c7...85e8337. Read the comment docs.

allredj reviewed

View reviewed changes

Contributor

allredj left a comment

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

tautschnig approved these changes

View reviewed changes

tautschnig merged commit 3af0130 into develop

tautschnig deleted the simplify_node_interface branch

August 6, 2019 00:03

tautschnig mentioned this pull request

Various uses of simplify_node are unnecessary or wrong #4988

Closed

kroening pushed a commit that referenced this pull request


          use simplify_not instead of boolean_negate

676aa9f

This is follow-up on a discussion in #4982.  boolean_negate performs some,
but not all, of the simplifications done by simplify_not.  This PR avoids
this redundancy by calling simplfify_not(not_exprt(x)) instead of
simplify_node(boolean_negate(x)).

kroening mentioned this pull request

use simplify_not instead of boolean_negate #4990

Merged

3 tasks

kroening pushed a commit that referenced this pull request


          use simplify_not instead of boolean_negate

c9b7fd2

This is follow-up on a discussion in #4982.  boolean_negate performs some,
but not all, of the simplifications done by simplify_not.  This PR avoids
this redundancy by calling simplify_not(not_exprt(x)) instead of
simplify_node(boolean_negate(x)).

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

allredj allredj left review comments

tautschnig tautschnig approved these changes

peterschrammel Awaiting requested review from peterschrammel peterschrammel is a code owner

pkesseli Awaiting requested review from pkesseli

smowton Awaiting requested review from smowton

Labels