VSD - constant expression evaluation speedup #6290
Merged
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
jezhiggins
changed the title
martin-cs
approved these changes
Aug 11, 2021
jezhiggins
force-pushed
the
vsd-eval-within-our-lifetime
branch
2 times, most recently
from
cfde5e3 to
9b7f4ff
Compare
Codecov Report
@@ Coverage Diff @@
## develop #6290 +/- ##
========================================
Coverage 75.96% 75.96%
========================================
Files 1508 1508
Lines 163282 163292 +10
========================================
+ Hits 124040 124052 +12
+ Misses 39242 39240 -2
Continue to review full report at Codecov.
|
jezhiggins
force-pushed
the
vsd-eval-within-our-lifetime
branch
from
9b7f4ff to
25b91df
Compare
jezhiggins
force-pushed
the
vsd-eval-within-our-lifetime
branch
from
25b91df to
c037f34
Compare
jezhiggins
requested review from
chrisr-diffblue and
peterschrammel
as code owners
martin-cs
approved these changes
Aug 12, 2021
| -- | ||
| This expression is derived from a real system under test. Due to inadvertent reevaluation of expression operands, all expression evaluations had geometric complexity (even more so in the presence of TOP values). This particular expression took nearly two hours to evaluate. Reworking to prevent repeated reevaluation brings this down to a few tenths. | ||
| See https://github.com/diffblue/cbmc/pull/6290 | ||
| If this test appears to hang, the constant_evaluator is probably your first port of call. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This PR reduces the number of times the operands in a constant_value expression are reevaluated. Usually, this overhead is small but for nested expressions this can result in excessive runtimes.
The motivating example has the form
This doesn't look particularly difficult, but evaluation time for the goto-program in question was close to two hours. With these changes evaluation time is approximately two tenths of a second (usual caveats - as reported by
timeon my machine, etc).