Symex trace: show implicit value associated with composite declarations #4964
Conversation
Previously when a struct- or other composite-typed variable was declared, symex_decl would initialize its individual fields, then return an L2-renamed symbol relating to the whole object. With field-sensitivity enabled, the returned symbol is e.g. my_struct!0@1#0, while anybody reading from it will read my_struct!0@1#1..field, a different symbol which to the solver is unrelated. The result was that in the trace, the declaration would show up with the value of the free symbol my_struct!0@1#0 (most likely zero, since it can't be referred to), while the rest of the trace may make it obvious that it actually had some other non-zero value. With this change we expand the struct into its constituent field symbols before recording an SSA_stept for the trace. This restores the correspondence between what the trace reads and what code reading from the struct reads.
hannes-steffenhagen-diffblue
requested review from
kroening,
peterschrammel,
smowton and
tautschnig
as code owners
|
This is copied from this PR because I will be maintaining this until it can be merged. |
The test in this commit checks for a bug in which the initial nondet assignment to struct fields was missing from --trace (always showing these struct fields as being initialised to 0).
hannes-steffenhagen-diffblue
force-pushed
the
fix/trace-decl-initializers
branch
from
f458a87 to
407c149
Compare
| ^SIGNAL=0$ | ||
| ^VERIFICATION FAILED$ | ||
| -- | ||
| x=\{ \.x=0 \} |
There was a problem hiding this comment.
I originally had this as a different check (checking that there was a non-zero assignment to x.x) but the cprover-smt2 run didn't produce a valid trace at all which made this test fail.
There was a problem hiding this comment.
This PR failed Diffblue compatibility checks (cbmc commit: f458a87).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/121252412
Status will be re-evaluated on next push.
Common spurious failures include: 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); compatibility was already broken by an earlier merge.
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: 407c149).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/121252599
Codecov Report
@@ Coverage Diff @@
## develop #4964 +/- ##
===========================================
- Coverage 69.29% 69.26% -0.04%
===========================================
Files 1306 1307 +1
Lines 108263 108090 -173
===========================================
- Hits 75023 74869 -154
+ Misses 33240 33221 -19
Continue to review full report at Codecov.
|
Previously when a struct- or other composite-typed variable was declared, symex_decl
would initialize its individual fields, then return an L2-renamed symbol relating to
the whole object. With field-sensitivity enabled, the returned symbol is e.g. my_struct!0@1#0,
while anybody reading from it will read my_struct!0@1#1..field, a different symbol which
to the solver is unrelated. The result was that in the trace, the declaration would show
up with the value of the free symbol my_struct!0@1#0 (most likely zero, since it can't be
referred to), while the rest of the trace may make it obvious that it actually had some other
non-zero value.
With this change we expand the struct into its constituent field symbols before recording an
SSA_stept for the trace. This restores the correspondence between what the trace reads and what
code reading from the struct reads.
Argument for the reviewers to have: should the goto_symex_statet::rename in symex_decl already be expanding like this? That function has an invariant insisting that it should return a single symbol, not a struct-exprt of field symbols, but that may not really be necessary. Note that if we change ::rename to always perform struct expansion then we will probably break any user that is applying this to an lvalue.