Fix symex of functions that may throw #4343
Conversation
smowton
requested review from
kroening,
peterschrammel and
tautschnig
as code owners
smowton
force-pushed
the
smowton/feature/explicily-initialise-externs
branch
4 times, most recently
from
c2be99c to
f0d7ae5
Compare
|
@tautschnig @peterschrammel this should now be ready for review, but is based on #4386 -- please only review final 4 commits. |
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: f0d7ae5).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/104456360
| exprt rhs; | ||
|
|
||
| if(symbol.value.is_nil()) | ||
| if((symbol.value.is_nil() && symbol.is_extern) || |
There was a problem hiding this comment.
Does this also cover argc and argv?
There was a problem hiding this comment.
Checked: no, they are initialised by dangling globals argc' and argv' created in ansi_c_entry_point, after static_lifetime_init has been called. I tried initialising them explicitly: this worked fine except for test goto-instrument/harness1, which tries to dump a C harness to replicate a particular situation. That led to a line like argv' = nondet_0();, which is not legal C.
So it's not trivial to fix this, but I think we're safe: there's no way for argc' and similar to be assigned, so they should never be merged. I agree it would be better to explicitly init them, but given the rabbit hole we appear to be diving down here I'm inclined to leave it to a subsequent PR.
tautschnig
changed the title
| @@ -22,26 +22,13 @@ void goto_symext::symex_dead(statet &state) | |||
| const code_deadt &code = instruction.get_dead(); | |||
|
|
|||
| ssa_exprt ssa = state.rename_ssa<L1>(ssa_exprt{code.symbol()}, ns); | |||
|
|
|||
| // in case of pointers, put something into the value set | |||
There was a problem hiding this comment.
(commit message) convergeance -> convergence
| return_value!0#0 | ||
| java::Sub\.g:\(\) | ||
| -- | ||
| This checks that when a function may throw, we can nontheless constant-propagate |
This enables us to distinguish the case where the front-end intended a nondet initialiser from an undefined variable, such as a "#return_value" global before a call or on paths which throw an exception.
This saves memory while achieving very similar behaviour as a read from a value removed from the value-set still yields a failed object. The difference is what happens on a merge: a merge with an explicit failed object retains it, while a merge against an empty value-set will discard the undefined possibility. This is fine for dead variables, where on a control- flow convergance we may safely assume we came from the path where it is not dead, but for declarations and undefined extern variables the front-end and goto-symex must collaborate to ensure an explicit nondet value is present.
Now that the front-ends are required to explicitly assign a nondet value where that is intended (e.g. an undefined extern global), rather than leaving an undefined value, there is no need to special-case merging them.
…unction This is possible now that #return_value variables are not subject to special rules in phi_function, and the value-set is cleared when variables are marked dead, meaning that there is no chance a second function call which only sometimes defines #return_value might witness the previous call's results.
smowton
force-pushed
the
smowton/feature/explicily-initialise-externs
branch
from
f0d7ae5 to
d341910
Compare
smowton
requested review from
chrisr-diffblue,
danpoe,
hannes-steffenhagen-diffblue,
martin-cs,
owen-mc-diffblue and
romainbrenguier
as code owners
smowton
changed the title
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: d341910).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/104994782
Java functions that may throw do not always define
#return_value(cf. the C front-end ensures it always defines it, even if the source code does not). Previously that situation was handled inconsistently: the first call on any such path would propagate the value-set on the normal-return path but refuse to constant-propagate, and the second call on a path to the same function would refuse to do either (usingreturn_value@objectandreturn_value#0to represent the possibility that the return-value is undefined in each case).This partially addresses that by (a) using the same merge logic (keep the defined version) for
#return_valuevariables as for locals, (b) erasing from the value-set when a variable dies rather than writing a failed object (consistent with the case where the variable has never been written at all), and (c) explicitly initialising nondet variables in the C front-end to permit (a).With this change we can propagate the value-set to the normal-return path every time, and constant propagate on the first call to a given function.
One problem remains: on the second call constant propagation still fails, because we're merging an undefined generation of the
#return_valuevariable (the one created by the previousDEADinstruction) but that generation is not zero. That case can be addressed once #4199 lands by havingDEADset the generation to zero (which is never defined) rather than incrementing it.This is now based on #4386 -- please only review the last 4 commits.