Don't simplify guard to skip instructions #4307
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
Which is cheaper: simplifying a large guard, or checking that goto_state_map doesn't contain any incoming entries for the instructions between this one and the jump target? My theory: the latter.
smowton
requested review from
kroening,
peterschrammel and
tautschnig
as code owners
romainbrenguier
approved these changes
Mar 1, 2019
allredj
reviewed
Mar 1, 2019
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: 4a3fa35).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/102807209
tautschnig
approved these changes
Mar 1, 2019
|
Heh, okay, I won't benchmark it ;) |
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 still applies even with the guards-are-BDDs branch, since it retains the option to use expr-guards. Needs data, of course, but anecdotally this reduces symex time on one large Java example from about 20 to about 15 minutes.
Underlying theory: forward-GOTOs on a must-execute path (i.e. one that post-dominates the entry point) are rarer than forward-GOTOs that don't post-dominate, and the cost of figuring out that the guard must be effectively TRUE by checking
goto_state_mapfor each intervening instruction is quite low (each instruction does a single map lookup to determine there is no incoming state to merge, checks state.guard.is_false() and continues). This is especially true for short GOTOs, which are also common. This simplify-and-jump code could only make a big saving when (a) the GOTO post-doms the entry point, (b) the state guard simplifies to true, and (c) the GOTO is long enough that the cost of a quick check-and-skip for each intervening instruction is high.