Rename LHS rvalues up front #4917
Conversation
smowton
force-pushed
the
smowton/cleanup/rename-lhs-rvalues-up-front-on-develop
branch
from
9884513 to
167f562
Compare
Codecov Report
@@ Coverage Diff @@
## develop #4917 +/- ##
===========================================
- Coverage 69.21% 69.18% -0.03%
===========================================
Files 1307 1306 -1
Lines 108019 108024 +5
===========================================
- Hits 74763 74735 -28
- Misses 33256 33289 +33
Continue to review full report at Codecov.
|
allredj
left a comment
allredj
left a comment
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: 167f562).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/119511318
|
I agree with the approach -- should this be rename_rhs, since 'rvalue' has a slightly different meaning since C++ has rvalue references? For symmetry, have rename_lhs? |
|
Added tests as #4944, which this PR passes. I regard this as ready to go once those tests are in. |
smowton
force-pushed
the
smowton/cleanup/rename-lhs-rvalues-up-front-on-develop
branch
from
167f562 to
86aacf6
Compare
In the process it is moved (without change) to renaming_level.h/cpp, alongside the similarly-structured get_original_name functions.
This renames the rvalue components of an lvalue expression to L2, such as the index of an array expression or the offset involved in byte-extract operation. Lvalue components (e.g. symbols) are left alone.
This was already happening in most cases (e.g. symex_dereference would apply field-sensitivity before symex_assign_rec was entered), but the case of a statically non-constant but dynamically constant array index or byte-extract offset would only be handled *after* symex_assign_rec, leading to an asymmetry in which operations were combined into the ssa_exprt and which ones accumulated in the expr_skeletont. With this change the LHS expression is maximally renamed and simplified before symex_assign_rec is entered, which means that any field-sensitive symbols on the LHS are fully constructed as early as possible, and expr_skeletont only accumulates those member, index and byte-extract operations which *cannot* be associated with an ssa_exprt. This means there is no need to undo with-operations or try to simplify byte-extract operations in goto_symext::assign_from_non_struct_symbol, as this has been taken care of already, and the l2_full_lhs can be constructed from the expression skeleton trivially.
These are unused now that we don't have shift_indexed_access_to_lhs or rewrite_with_to_field_symbols
smowton
force-pushed
the
smowton/cleanup/rename-lhs-rvalues-up-front-on-develop
branch
from
86aacf6 to
c4bc800
Compare
allredj
left a comment
allredj
left a comment
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: c4bc800).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/120656593
|
@kroening re: naming, it's definitely not |
|
Perhaps just |
|
@andreast271 I hear from email relayed via @kroening that the out-of-bounds issue was not introduced by that PR, is that accurate? If so are you happy for this to go in? |
|
So you did, I'm not sure why I didn't get email about that. Polling @kroening for a final approval here. |
6 participants
The rough idea: instead of recursing over the structure of an assignment LHS, then performing post-hoc adjustments to permit field-sensitivity to have maximum effect, perform all expression simplification up to LHS field-sensitivity application right at the start of
symex_assign. This both simplifies thesymex_assignworkflow, asshift_indexed_access_to_lhsandrewrite_with_to_field_symbolsare no longer needed, and makes maintainingl2_full_lhssimpler, as the expression skeleton no longer needs to undergo any complicated transformations.There is one down-side:
withexpressions not introduced bygoto-symexare no longer handled. If they are only ever really produced within goto-symex then this is no loss -- the simplification and field-sensitivity application ahead ofsymex_assignachieves the same thing. If we expect to handle GOTO programs withwith_exprtalready present then we should do something a little cleverer.This of course needs tests (or existing tests should be reviewed) to ensure we still have field-sensitivity in all the cases we intend.
Test PR for this + array-cell sensitivity: #4918
Long version: Rename LHS rvalues up front
This was already happening in most cases (e.g. symex_dereference would apply field-sensitivity
before symex_assign_rec was entered), but the case of a statically non-constant but dynamically
constant array index or byte-extract offset would only be handled after symex_assign_rec, leading
to an asymmetry in which operations were combined into the ssa_exprt and which ones accumulated in
the expr_skeletont.
With this change the LHS expression is maximally renamed and simplified before symex_assign_rec is
entered, which means that any field-sensitive symbols on the LHS are fully constructed as early as
possible, and expr_skeletont only accumulates those member, index and byte-extract operations which
cannot be associated with an ssa_exprt. This means there is no need to undo with-operations or
try to simplify byte-extract operations in goto_symext::assign_from_non_struct_symbol, as this has
been taken care of already, and the l2_full_lhs can be constructed from the expression skeleton
trivially.