Skip to content

Refine recursive calls within the simplifier #5764

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 1 commit into from
May 14, 2021
Merged

Refine recursive calls within the simplifier #5764

merged 1 commit into from
May 14, 2021

Conversation

tautschnig
Copy link
Collaborator

  1. When we know the id of an expression, use the corresponding simplify_*
    method rather than the generic simplify_node.
  2. Avoid simplify_rec when all operands have been simplified already.
  3. Don't call simplify_rec (or simplify_node) when there is nothing to
    simplify.

Fixes: #4988

  • 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).
  • 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.

@codecov
Copy link

codecov bot commented Jan 19, 2021 •
edited
Loading

Codecov Report

Merging #5764 (af08918) into develop (c29b69a) will increase coverage by 0.04%.
The diff coverage is 94.73%.

Impacted file tree graph

@@             Coverage Diff             @@
##           develop    #5764      +/-   ##
===========================================
+ Coverage    74.44%   74.49%   +0.04%     
===========================================
  Files         1446     1447       +1     
  Lines       157778   157768      -10     
===========================================
+ Hits        117456   117527      +71     
+ Misses       40322    40241      -81
Impacted Files Coverage Δ
jbmc/src/janalyzer/janalyzer_main.cpp 100.00% <ø> (ø)
jbmc/src/java_bytecode/assignments_from_json.cpp 97.26% <ø> (ø)
jbmc/src/java_bytecode/ci_lazy_methods.cpp 99.47% <ø> (ø)
jbmc/src/java_bytecode/ci_lazy_methods.h 100.00% <ø> (ø)
jbmc/src/java_bytecode/ci_lazy_methods_needed.cpp 98.24% <ø> (ø)
jbmc/src/java_bytecode/ci_lazy_methods_needed.h 100.00% <ø> (ø)
jbmc/src/java_bytecode/convert_java_nondet.cpp 81.15% <ø> (ø)
...java_bytecode/create_array_with_type_intrinsic.cpp 97.67% <ø> (ø)
jbmc/src/java_bytecode/expr2java.cpp 86.61% <ø> (ø)
jbmc/src/java_bytecode/expr2java.h 100.00% <ø> (ø)
... and 708 more

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 1ab5de1...af08918. Read the comment docs.

@tautschnig tautschnig force-pushed the simplify-recursive-cleanup branch from 73d4c56 to 29225f0 Compare January 20, 2021 20:18
martin-cs
martin-cs approved these changes Jan 22, 2021
View reviewed changes
Copy link
Collaborator

@martin-cs martin-cs left a comment

Choose a reason for hiding this comment

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

Yes but...

I believe this PR is a correct implementation of what it claims and is one way of improving the code; this is definitely faster than redoing the dispatch when the ID is known.

But... I'm not sure it's the only way of improving it. This makes it harder to implement solutions where simplify_node is caching or enforces some kind of sharing-aware graph visit rather than potentially exponential recursion. I don't have the bandwidth to do anything like that at the moment (I don't even know if it is a good / widely accepted idea) but I wouldn't want to make it harder than it already is.

src/util/simplify_expr_boolean.cpp
rewritten_op.where() = simplify_node(rewritten_op.where());
return std::move(rewritten_op);
return exists_exprt{op_as_forall.symbol(),
simplify_not(not_exprt(op_as_forall.where()))};
Copy link
Collaborator

Choose a reason for hiding this comment

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

Nice!

@tautschnig
Copy link
Collaborator Author

Yes but...

I believe this PR is a correct implementation of what it claims and is one way of improving the code; this is definitely faster than redoing the dispatch when the ID is known.

But... I'm not sure it's the only way of improving it. This makes it harder to implement solutions where simplify_node is caching or enforces some kind of sharing-aware graph visit rather than potentially exponential recursion. I don't have the bandwidth to do anything like that at the moment (I don't even know if it is a good / widely accepted idea) but I wouldn't want to make it harder than it already is.

I agree that it may be a good idea to always go through simplify_node, for the reasons you called out. But then we should indeed always do that, and not just sometimes (which is what we did before this patch). So this patch makes use uniformly not use simplify_node when the ID is known. I believe it should be fairly easy to flip all calls to simplify_* to simplify_node if so desired. But then we should really do it for all of them. (I am also happy to make this happen in this PR instead of what's being proposed right now.)

@martin-cs
Copy link
Collaborator

Agreed; it should be one way or the other. As I am not an "owner" for this area of code and don't have time to work on it... I don't feel like I should have a strong say. I think this is an improvement over the current state-of-affairs and until we have someone who can do something fancy (graph traversal, caching, etc.) with simplify_node then this is probably the way to go.

@tautschnig tautschnig force-pushed the simplify-recursive-cleanup branch from 29225f0 to 23afd4e Compare March 3, 2021 07:50
@tautschnig tautschnig force-pushed the simplify-recursive-cleanup branch from 23afd4e to 3101ba7 Compare April 7, 2021 16:30
@tautschnig
Refine recursive calls within the simplifier
af08918 
1) When we know the id of an expression, use the corresponding simplify_*
method rather than the generic simplify_node.
2) Avoid simplify_rec when all operands have been simplified already.
3) Don't call simplify_rec (or simplify_node) when there is nothing to
simplify.

Fixes: diffblue#4988
@tautschnig tautschnig force-pushed the simplify-recursive-cleanup branch from 3101ba7 to af08918 Compare May 7, 2021 06:21
peterschrammel
peterschrammel approved these changes May 14, 2021
View reviewed changes
Copy link
Member

@peterschrammel peterschrammel left a comment

Choose a reason for hiding this comment

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

Yes, this makes sense to call the right case directly when you already know which case it is going to be.

@peterschrammel peterschrammel removed their assignment May 14, 2021
@tautschnig tautschnig merged commit 972a993 into diffblue:develop May 14, 2021
@tautschnig tautschnig deleted the simplify-recursive-cleanup branch May 14, 2021 09:01
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@peterschrammel peterschrammel peterschrammel approved these changes

@martin-cs martin-cs martin-cs approved these changes

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

@smowton smowton Awaiting requested review from smowton

Assignees

@kroening kroening

Labels
cleanup
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

Various uses of simplify_node are unnecessary or wrong
4 participants
@tautschnig @martin-cs @peterschrammel @kroening