Skip to content

pre/post traversal expression transformers #4891

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
Open
wants to merge 1 commit into
base: develop
Choose a base branch
from
Open

pre/post traversal expression transformers #4891

wants to merge 1 commit into from

Conversation

kroening
Copy link
Member

Transformers for expressions that offer an interface similar to that offered
by the goto-program API. Both pre- and post-traversal options are available.

The key benefit over the non-const visit method is that sharing is only
broken up when required.

  • 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).
  • 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
allredj reviewed Jul 11, 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: eda58d0).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/118808656

smowton
smowton reviewed Jul 12, 2019
View reviewed changes
Copy link
Contributor

@smowton smowton left a comment

Choose a reason for hiding this comment

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

Can't find it right now as on a phone, but I implemented a similar visitor for renamed expressions recently in symex and tried to retain sharing whenever possible, perhaps use that as a starting point?

src/util/expr.cpp Outdated
exprt tmp = *this;
bool op_changed = false;

for(auto &op : tmp.operands()) // this breaks sharing
Copy link
Contributor

Choose a reason for hiding this comment

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

Surely breaking sharing before you know if that's necessary will negate the benefit of this

Copy link
Member Author

Choose a reason for hiding this comment

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

Yes, but note it's done on a copy.

Copy link
Contributor

Choose a reason for hiding this comment

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

So what? Make a copy then immediately break sharing and you've copied the input expression

@kroening
Copy link
Member Author

You mean renamedt<exprt, level> goto_symex_statet::rename(exprt expr, const namespacet &ns)?

tautschnig
tautschnig requested changes Jul 12, 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.

This needs unit tests.

src/util/expr.cpp
@@ -287,6 +287,65 @@ void exprt::visit_post(std::function<void(const exprt &)> visitor) const
visit_post_template(visitor, this);
Copy link
Collaborator

Choose a reason for hiding this comment

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

Commit message: "Transformers for expressions that offer an interface similar to that offered
by the goto-program API." There isn't enough context available to understand why what looks like a comparison of apples and oranges is useful to the reader.

Copy link
Member Author

Choose a reason for hiding this comment

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

Fixed

src/util/expr.cpp Outdated
if(visitor_result.has_value())
tmp = visitor_result.value();
else
tmp = *this;
Copy link
Collaborator

Choose a reason for hiding this comment

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

How about exprt tmp = visitor_result.value_or(*this);

Copy link
Member Author

Choose a reason for hiding this comment

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

sure

@owen-mc-diffblue
Copy link
Contributor

I believe @smowton is referring to void selectively_mutate(renamedt<exprt, level> &renamed, typename renamedt<exprt, level>::mutator_functiont get_mutated_expr), from #4664.

pre/post traversal expression transformers
884d002 
Transformers for expressions that offer an interface similar to that offered
by

void goto_programt::transform(std::function<optionalt<exprt>(exprt)>);

on goto programs. Both pre- and post-traversal options are available.

The key benefit over the non-const visit method is that sharing is only
broken up when required.
allredj
allredj reviewed Jul 13, 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: 884d002).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/119023646

@codecov-io
Copy link

Codecov Report

Merging #4891 into develop will decrease coverage by 0.01%.
The diff coverage is 0%.

Impacted file tree graph

@@             Coverage Diff             @@
##           develop    #4891      +/-   ##
===========================================
- Coverage     69.2%   69.19%   -0.02%     
===========================================
  Files         1306     1306              
  Lines       107949   107968      +19     
===========================================
  Hits         74704    74704              
- Misses       33245    33264      +19
Impacted Files Coverage Δ
src/util/expr.h 90.47% <ø> (ø) ⬆️
src/util/expr.cpp 55.47% <0%> (-8.4%) ⬇️
jbmc/src/java_bytecode/java_types.h 99.48% <0%> (-0.52%) ⬇️
jbmc/src/java_bytecode/java_bytecode_parser.cpp 89.59% <0%> (ø) ⬆️
src/analyses/goto_check.cpp 78.99% <0%> (+0.02%) ⬆️

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 e288906...884d002. Read the comment docs.

@smowton
Copy link
Contributor

smowton commented Jul 15, 2019

Indeed --

cbmc/src/goto-symex/renamed.h

Line 88 in 1ea4a76

void selectively_mutate(
preserves sharing when possible using the depth iterator. A variant of that with pre-order visiting would permit sharing to be broken only when actually required.

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

@smowton smowton smowton left review comments

@allredj allredj allredj left review comments

@tautschnig tautschnig tautschnig requested changes

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

@pkesseli pkesseli Awaiting requested review from pkesseli

Requested changes must be addressed to merge this pull request.

Assignees

@kroening kroening

Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
6 participants
@kroening @owen-mc-diffblue @codecov-io @smowton @tautschnig @allredj