Only convert not-yet-converted SSA steps #4065
Conversation
| { | ||
| if(step.is_assignment() && !step.ignore) | ||
| if(step.is_assignment() && !step.ignore && !step.converted) |
There was a problem hiding this comment.
Instead of adding this info to every step, would it be more efficient to store a conversion frontier as a single iterator member? The current implementation increases the storage size of each SSA_stept and requires repeated traversal of steps have have been seen before. With an optionalt<SSA_stepst::const_iterator> we would just store a pointer to the last converted step.
There was a problem hiding this comment.
There is no conversion frontier due to slicing.
Necessary to enable incremental extension of the symex target equation during incremental unwinding. This also works in combination with `slice`.
peterschrammel
force-pushed
the
incremental-equation-conversion
branch
from
5770ae7 to
fe72c88
Compare
There was a problem hiding this comment.
🚫
This PR failed Diffblue compatibility checks (cbmc commit: fe72c88).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/99663571
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.
Common spurious failures:
- the cbmc commit has disappeared in the mean time (e.g. in a force-push)
- the author is not in the list of contributors (e.g. first-time contributors).
The incompatibility may have been introduced by an earlier PR. In that case merging this
PR should be avoided unless it fixes the current incompatibility.
|
Does it make sense to drop the symex_target container for the incremental use case, and pass directly to the solver? |
|
How would |
Necessary to enable incremental extension and conversion of the symex target equation during incremental unwinding. This also works in combination with
slice.