Refactoring of symex_assign_symbol #4642
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
romainbrenguier
requested review from
kroening,
peterschrammel,
smowton and
tautschnig
as code owners
romainbrenguier
force-pushed
the
refactor/symex_assign
branch
3 times, most recently
from
b4ba956 to
bf73aa7
Compare
smowton
approved these changes
May 10, 2019
tautschnig
reviewed
May 11, 2019
src/goto-symex/goto_symex_state.cpp
Outdated
| tmp, | ||
| source, | ||
| symex_targett::assignment_typet::PHI); | ||
|
|
||
| expr = set_indices<L2>(std::move(ssa_l1), ns).get(); | ||
| // TODO: are we setting l2 indices of something that is already l2? | ||
| expr = set_indices<L2>(std::move(ssa_l2), ns).get(); |
There was a problem hiding this comment.
Could you try adding an assertion that this effectively returns ssa_l2 - I agree that this seems unnecessary, but maybe we're missing something.
There was a problem hiding this comment.
I've now added an invariant before the call to check that ssa_l2 was correctly renamed.
| @@ -452,8 +452,7 @@ bool goto_symex_statet::l2_thread_read_encoding( | |||
| source, | |||
| symex_targett::assignment_typet::PHI); | |||
|
|
|||
| // TODO: are we setting l2 indices of something that is already l2? | |||
| expr = set_indices<L2>(std::move(ssa_l2), ns).get(); | |||
| expr = std::move(ssa_l2); | |||
There was a problem hiding this comment.
See my earlier comment: did you add an assertion to confirm this is doing what you expected across our regression tests?
The name better reflects what the variable represent and using move is clearer than swap.
guarded_rhs is only used to define l2_rhs, we make this explicit in the code.
This makes it a bit clearer what the shift_indexed_access_to_lhs function produced. It also avoids errors where the argument as a specific type but the identifier is overwritten, for instance: ``` symbol_exprt s1 = ...; shift_indexed_access_to_lhs(state, s1, lhs, ns, true); assert(s1 == ID_symbol); // may fail though s1 has type symbol_exprt ```
This avoids having an input that is also an output and makes what is modified by the call clearer. The argument was copied before the call anyway.
This avoids having parameters that are also output value, which is not clear from the calling site, and could cause some type mistakes when the exprt parameters is from a subtype of exprt.
This simplifies the call to this function and is clearer about the semantical relation between the lhs and rhs arguments.
This makes the relation between lhs and rhs clearer.
This avoids having an input that is also an output and clarifies how lhs is changed.
In practice there was an implicit stack of record events backup through the recursive calls, this makes the stack explicit.
The argument of add_to_lhs are const anyway.
It is not modified after assignment.
This avoids having an input that is also an output and make the calls to get_original_name clearer.
ssa_l2 is already an L2 expression, its indices doesn't need to be reset. We just check that the renaming was correct instead.
romainbrenguier
force-pushed
the
refactor/symex_assign
branch
from
bf73aa7 to
fdc03e0
Compare
allredj
reviewed
May 13, 2019
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: fdc03e0).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/111540186
|
@tautschnig I've added the check you suggested and everything works fine |
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.
Having to debug some changes related to
symex_assignI found it difficult to understand what variable represents what in the execution ofsymex_assign_symbolbecause of several functions which have parameters that are also output. This pull request is an attempt to get rid of these.