Do not misuse symex dereferencing code for finding array objects [blocks: #3725] #3953
Conversation
tautschnig
changed the title
There was a problem hiding this comment.
🚫
This PR failed Diffblue compatibility checks (cbmc commit: c2dbf98).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/98664986
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.
Common spurious failures:
- 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).
The incompatibility may have been introduced by an earlier PR. In that case merging this
PR should be avoided unless it fixes the current incompatibility.
tautschnig
force-pushed
the
process-array-expr
branch
from
c2dbf98 to
36a6215
Compare
src/goto-symex/symex_other.cpp
Outdated
| @@ -128,7 +131,7 @@ void goto_symext::symex_other( | |||
| statement==ID_array_replace) | |||
| { | |||
| // array_copy and array_replace take two pointers (to arrays); we need to: | |||
| // 1. dereference the pointers (via clean_expr) | |||
| // 1. dereference pointers within the pointers (via clean_expr) | |||
There was a problem hiding this comment.
How about just remove any dereference expressions, since we're no longer creating a top-level special one?
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: 36a6215).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/98704493
tautschnig
force-pushed
the
process-array-expr
branch
from
36a6215 to
afd28e9
Compare
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: afd28e9).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/98716727
src/goto-symex/symex_other.cpp
Outdated
| @@ -9,6 +9,9 @@ Author: Daniel Kroening, [email protected] | |||
| /// \file | |||
| /// Symbolic Execution | |||
|
|
|||
| #include <iostream> | |||
There was a problem hiding this comment.
🚫 This shouldn't be needed here.
tautschnig
force-pushed
the
process-array-expr
branch
from
afd28e9 to
818b240
Compare
There was a problem hiding this comment.
🚫
This PR failed Diffblue compatibility checks (cbmc commit: 818b240).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/98935492
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.
Common spurious failures:
- 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).
The incompatibility may have been introduced by an earlier PR. In that case merging this
PR should be avoided unless it fixes the current incompatibility.
The task of process_array_expr is to find the objects pointed to; symex dereferencing does so as well, but also does many other things. Creating an artificial dereference_exprt imposes restrictions on what optimisations symex dereferencing can implement. Instead, just make process_array_expr actually get the objects (via the value set) and then work on those. This duplicates a bit of code from symex dereferencing, but now yields full control to process_array_expr over what it needs to make happen. In future, the process_array_expr code may even get rewritten without having any dependency on what symex dereferencing exactly does.
tautschnig
force-pushed
the
process-array-expr
branch
from
818b240 to
855dcfa
Compare
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: 855dcfa).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/99078209
The task of process_array_expr is to find the objects pointed to; symex
dereferencing does so as well, but also does many other things. Creating an
artificial dereference_exprt imposes restrictions on what optimisations symex
dereferencing can implement. Instead, just make process_array_expr actually get
the objects (via the value set) and then work on those. This duplicates a bit of
code from symex dereferencing, but now yields full control to process_array_expr
over what it needs to make happen. In future, the process_array_expr code may
even get rewritten without having any dependency on what symex dereferencing
exactly does.
At present, the behaviour before or after the commit is largely unchanged, but modifications such as #3725 show that these changes are actually needed.