Symex code_deadt: always use L2 generation zero #4407
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
smowton
requested review from
tautschnig,
kroening,
peterschrammel and
romainbrenguier
allredj
reviewed
Mar 19, 2019
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: c5ef60b).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/104955360
The string solver was consuming a very large amount of memory with the limit set to 10000; this appears to be pure chance whether the solver picks a solution requiring universals to be instantiated a large number of times. The other tests in this directory are already set to limit string length to 1000, so I just do the same thing here.
This means that merge_goto's special merge logic for generation zero works on both dead local variables and on #return_value global variables defined for the second and subsequent times, discounting the control-flow where the variable is dead.
smowton
force-pushed
the
smowton/feature/dead-always-uses-generation-zero
branch
from
c5ef60b to
d201bad
Compare
allredj
reviewed
Mar 19, 2019
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: d201bad).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/105014174
peterschrammel
approved these changes
Mar 19, 2019
owen-mc-diffblue
approved these changes
Mar 20, 2019
| /// Drops an L1 name from the local L2 map | ||
| void drop_l1_name(const irep_idt &l1_identifier) | ||
| { | ||
| level2.current_names.erase(l1_identifier); |
There was a problem hiding this comment.
I would think these methods should belong to the symex_level2t class
There was a problem hiding this comment.
I'll keep it alongside its close cousin increase_generation for now; if we want to refactor we should do them together (I don't mind either way)
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.
Now that we have #4199 and so decreasing the L2 generation number during symex is no longer a problem, we can simply use L2 generation 0 to represent all dead variables. Direct reads while the variable is certainly dead will still yield a nondet value, as generation 0 is never defined, while
merge_goto's special-casing of generation 0 (0 MERGE N == N for any nonzero generation N) can optimise the case where paths featuring a dead variable converge with those where it is still live, similar to how it already handles paths where a variable was not declared.This is particularly useful for Java functions that throw, as symex will assume that code using
#return_valueflows from paths where it was defined (i.e. the normal return path), rather than considering the case where it is not defined (the exception-throwing path).