Simplifier: transform ((struct A)x).field1 into x.a.b.field2 #3562
Conversation
smowton
requested review from
tautschnig,
NathanJPhillips and
owen-mc-diffblue
smowton
requested review from
kroening,
peterschrammel and
pkesseli
as code owners
| @@ -0,0 +1,6 @@ | |||
|
|
|||
| ^Passing problem to | ||
| ^warning: ignoring | ||
| -- | ||
| The "Passing problem to..." line is a sign that symex couldn't prove the |
There was a problem hiding this comment.
What about "remaining VCCs: 0" ?
There was a problem hiding this comment.
Could you match the simplified expression on the --program-only output?
There was a problem hiding this comment.
Added a test checking the expected expression is in the --show-vccs output
smowton
force-pushed
the
smowton/feature/simplify-truncating-cast
branch
from
bff338a to
fd1bf5c
Compare
There was a problem hiding this comment.
🚫
This PR failed Diffblue compatibility checks (cbmc commit: bff338a).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/94378823
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.
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: fd1bf5c).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/94384684
| @@ -0,0 +1,11 @@ | |||
| CORE | |||
| Test.class | |||
| --function Test.main --no-propagation --unwind 10 --show-vcc | |||
There was a problem hiding this comment.
I think this should be --no-simplify instead of --no-propagation, because it's really the former that you are changing here.
smowton
force-pushed
the
smowton/feature/simplify-truncating-cast
branch
from
fd1bf5c to
105a87d
Compare
|
@smowton, there's a failing test: https://travis-ci.org/diffblue/cbmc/jobs/468086362#L5202 |
This will take place if field1 and field2 have matching types and offsets within struct A and the original struct type of 'x'. This is particularly important for the Java frontend, where Java like "Map m = new HashMap(); return m.size()" will generate GOTO that extracts the class-identifier from a Map*, but Map* and HashMap* are likely not structurally equivalent (HashMap might have a superclass other than Object, or have fields above those posessed by Map (which is an interface in fact, so has none)). That means value_set_dereferencet leaves us with an expression like ((Map)dynamic_object1)[email protected].@class_identifier, which the simplifier can now handle, enabling symex to determine the actual type is HashMap and so avoid exploring code that is in truth unreachable.
smowton
force-pushed
the
smowton/feature/simplify-truncating-cast
branch
from
105a87d to
d47a07c
Compare
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: d47a07c).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/94977771
This will take place if field1 and field2 have matching types and offsets within
struct A and the original struct type of 'x'. This is particularly important for the Java
frontend, where Java like "Map m = new HashMap(); return m.size()" will generate GOTO that
extracts the class-identifier from a Map*, but Map* and HashMap* are likely not structurally
equivalent (HashMap might have a superclass other than Object, or have fields above those
posessed by Map (which is an interface in fact, so has none)).
That means value_set_dereferencet leaves us with an expression like
((Map)dynamic_object1)[email protected].@class_identifier, which the simplifier can now
handle, enabling symex to determine the actual type is HashMap and so avoid exploring code
that is in truth unreachable.