Fix array length in symex constant string propagation [TG-9048] #5040
Conversation
romainbrenguier
requested review from
kroening,
peterschrammel,
smowton and
tautschnig
as code owners
romainbrenguier
changed the title
src/goto-symex/goto_symex.h
Outdated
| @@ -590,6 +590,9 @@ class goto_symext | |||
| /// "abc", the symbol will be named "abc_constant_char_array"). Then, the | |||
| /// expression `&sym[0]` is assigned to `char_array` (assuming `sym` denotes | |||
| /// the symbol holding the string data given by `new_char_array`. | |||
| /// The assignment is preceeded by a assume statements ensuring `length` | |||
There was a problem hiding this comment.
"a assume statements" -> "an assume statement"
src/goto-symex/goto_symex.h
Outdated
| @@ -590,6 +590,9 @@ class goto_symext | |||
| /// "abc", the symbol will be named "abc_constant_char_array"). Then, the | |||
| /// expression `&sym[0]` is assigned to `char_array` (assuming `sym` denotes | |||
| /// the symbol holding the string data given by `new_char_array`. | |||
| /// The assignment is preceeded by a assume statements ensuring `length` | |||
| /// before this call was zero, this is to avoid letting the previous array | |||
There was a problem hiding this comment.
"letting the previous array unconstrained" -> "letting the previous array be unconstrained" or "leaving the previous array unconstrained"
| -- | ||
| ^warning: ignoring | ||
| -- | ||
| The check for dynamic_object2 is to make sure the array is created empty and | ||
| is not given arbitrary content before its final assignment. |
This is to make sure that the length of the array before the assignment isn't unconstrained. Otherwise it could be set to be arbitrarily large by the solver which will causes invalid traces.
Split the tests for the different constructors, add assertions that are supposed to fail, and activate the tests that can be.
This tests would fail before the fix to the symex constant propagation of strings.
romainbrenguier
force-pushed
the
bugfix/empty-string-propagation
branch
from
e03ca3d to
334714a
Compare
There was a problem hiding this comment.
This PR failed Diffblue compatibility checks (cbmc commit: e03ca3d).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/123901901
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: 334714a).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/123906978
This adds an assumption on the length in assign_string_constant before we do the actual assignment. This is to make sure that the length of the array before the assignment
isn't unconstrained. Otherwise this array could be set to be arbitrarily large
by the solver which would cause invalid traces.