Symex trace: show implicit value associated with composite declarations #4919
Conversation
smowton
requested review from
kroening,
peterschrammel and
tautschnig
as code owners
|
This should fix #4882 |
smowton
force-pushed
the
smowton/fix/trace-decl-initializers
branch
from
d6492f0 to
0f37994
Compare
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.
smowton
force-pushed
the
smowton/fix/trace-decl-initializers
branch
from
0f37994 to
7c6370a
Compare
|
@hannes-steffenhagen-diffblue since this is your fix, would you mind taking charge of finding reviewers and addressing their comments? |
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: 7c6370a).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/120255611
There was a problem hiding this comment.
@hannes-steffenhagen-diffblue, what was the failing test? Please ping me to check how to upstream it.
|
@hannes-steffenhagen-diffblue you should probably also push a couple of tests representative of the problems reported to you by customers |
|
Sorry for the late reply, this PR over here has a KNOWNBUG test for what's being fixed here (I did check, and the problem does indeed go away): I'm not sure if there are other situations in which it can happen, but I don't think so. |
|
Continued in #4964 |
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::renameinsymex_declalready 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::renameto always perform struct expansion then we will probably break any user that is applying this to an lvalue.