Skip to content

introduce simplify_exprt::resultt #4732

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
merged 3 commits into from
Jun 5, 2019
Merged

introduce simplify_exprt::resultt #4732

merged 3 commits into from
Jun 5, 2019

Conversation

kroening
Copy link
Member

@kroening kroening commented May 30, 2019 •
edited by tautschnig
Loading

This is follow-up on #2939 and #2946, and the biggest change to the simplifier since its existence.

It attempts to make the implementation of individual simplification steps more type safe, as opposed to using exprt.

The alternative considered was to return optionalt<exprt>, which has the disadvantage that it doesn't "chain", i.e., given two transformations f and g one cannot write f(g(...)).

  • Each commit message has a non-empty body, explaining why the change was made.
  • 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).
  • 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 kroening added the RFC Request for comment label May 30, 2019
@tautschnig
Copy link
Collaborator

Could the commit message please include a body - which might actually just what's being said in the PR description?

tautschnig
tautschnig reviewed May 30, 2019
View reviewed changes
Copy link
Collaborator

@tautschnig tautschnig left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The commit in itself looks promising, but also it's not easy to judge without seeing it in action.

@tautschnig tautschnig assigned kroening and unassigned tautschnig May 30, 2019
@kroening kroening force-pushed the signatures_in_simplifier branch from c74acf7 to 9a85e4a Compare May 30, 2019 12:10
@kroening
Copy link
Member Author

@tautschnig Now with non-trivial example.

tautschnig
tautschnig reviewed May 30, 2019
View reviewed changes
src/util/simplify_expr.cpp

// #define DEBUGX
// #define DEBUGX
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Except for this seemingly wrong/unnecessary change: could we please just have this commit merged as soon as possible? It seems like a big improvement towards readability without any immediate dependence on the other changes.

tautschnig
tautschnig reviewed May 30, 2019
View reviewed changes
src/util/simplify_expr.cpp Outdated
tmp.type()=new_type;
expr.swap(tmp);
return false;
return tmp;
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Do we need std::move(tmp) here?

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Actually, don't we need return changed(std::move(tmp)); here?

tautschnig
tautschnig reviewed May 30, 2019
View reviewed changes
src/util/simplify_expr.cpp Outdated
op_type.id() == ID_floatbv ? ID_ieee_float_notequal : ID_notequal,
from_integer(0, op_type));
inequality.add_source_location()=expr.source_location();
simplify_node(inequality);
expr.swap(inequality);
return false;
return inequality;
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Unless I'm mistaken this needs a lot more use of std::move at about any return statement?

@kroening kroening force-pushed the signatures_in_simplifier branch from 9a85e4a to 09d5555 Compare June 3, 2019 15:57
Daniel Kroening added 2 commits June 5, 2019 08:55
introduce simplify_exprt::resultt
05cc657 
This is follow-up on #2939 and #2946, and the biggest change to the
simplifier since its existence.

It attempts to make the implementation of individual simplification steps
more type safe, as opposed to using exprt.

The alternative considered was to return optionalt<exprt>, which has the
disadvantage that it doesn't "chain", i.e., given two transformations f and
g one cannot write f(g(...)).
simplify_node: rename 'result' to 'no_change'
b642c44 
The new name conveys the meaning of the variable.
@kroening kroening force-pushed the signatures_in_simplifier branch from 09d5555 to b440b66 Compare June 5, 2019 07:56
@kroening kroening force-pushed the signatures_in_simplifier branch from b440b66 to 23bfef1 Compare June 5, 2019 08:50
@kroening
Copy link
Member Author

kroening commented Jun 5, 2019

The std::move are added!

allredj
allredj reviewed Jun 5, 2019
View reviewed changes
Copy link
Contributor

@allredj allredj left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

@kroening kroening assigned tautschnig and unassigned kroening Jun 5, 2019
@tautschnig tautschnig merged commit ff727e9 into develop Jun 5, 2019
@tautschnig tautschnig deleted the signatures_in_simplifier branch June 5, 2019 15:51
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@allredj allredj allredj left review comments

@tautschnig tautschnig tautschnig approved these changes

@peterschrammel peterschrammel Awaiting requested review from peterschrammel peterschrammel is a code owner

@pkesseli pkesseli Awaiting requested review from pkesseli

@smowton smowton Awaiting requested review from smowton

Assignees

@tautschnig tautschnig

@hannes-steffenhagen-diffblue hannes-steffenhagen-diffblue

Labels
RFC Request for comment
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
4 participants
@kroening @tautschnig @allredj @hannes-steffenhagen-diffblue