better precision of value_set on unions #2851
Conversation
kroening
requested review from
chrisr-diffblue,
martin-cs,
peterschrammel and
smowton
as code owners
|
What is the relationship between this one and #2854? |
|
Relationship to #2854: They both concern unions, but appear to be different. |
tautschnig
force-pushed
the
value_set_unions
branch
from
22f7a1a to
0c8ef66
Compare
tautschnig
assigned smowton, peterschrammel, martin-cs and chrisr-diffblue and unassigned kroening
There was a problem hiding this comment.
This PR failed Diffblue compatibility checks (cbmc commit: 0c8ef66).
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).
src/util/simplify_expr_struct.cpp
Outdated
| if(byte_extract_expr.offset().is_zero()) | ||
| { | ||
| const union_typet &union_type = to_union_type(op_type); | ||
| const typet subtype = union_type.component_type(component_name); |
There was a problem hiding this comment.
Only once #2987 has been merged.
regression/cbmc/union11/union_list.c
Outdated
|
|
||
| union U | ||
| { | ||
| struct List my_list; |
There was a problem hiding this comment.
Comment inline about whether the single-item union is important or not, since that's pretty unusual afaik
regression/cbmc/union11/union_list.c
Outdated
|
|
||
| struct List | ||
| { | ||
| unsigned something; |
There was a problem hiding this comment.
Unused in the test case? Is it important that neither struct member is at zero offset? If so comment inline about why
There was a problem hiding this comment.
It's crucial to make this pass/fail. I have added both an inline comment and information to the commit message.
regression/cbmc/union11/union_list.c
Outdated
|
|
||
| struct list_item | ||
| { | ||
| struct list_item *previous; |
There was a problem hiding this comment.
Why a single member struct instead of simply inlining this?
There was a problem hiding this comment.
We could have more members, just don't need more to demonstrate the problem/the fix.
src/pointer-analysis/value_set.cpp
Outdated
| } | ||
|
|
||
| assign(lhs_member, rhs_member, ns, false, add_to_sets); |
There was a problem hiding this comment.
If I'm reading this right the ID_unknown case used to be silently ignored? I suspect this increase in pessimism / improvement in soundness will have side effects, consider doing that as a separate PR since that seems orthogonal to simplifying unions?
|
I would like to wait for #2987 to be merged before doing further work here. |
tautschnig
assigned tautschnig and unassigned smowton, peterschrammel, martin-cs and chrisr-diffblue
tautschnig
force-pushed
the
value_set_unions
branch
from
0c8ef66 to
61ffc48
Compare
…implifier Previously, only the case of struct members with offset zero was handled with sufficient precision. Using structs inside unions where a member of non-zero offset is accessed is now handled precisely.
tautschnig
force-pushed
the
value_set_unions
branch
from
61ffc48 to
f2f2c60
Compare
|
@smowton All comments addressed. |
There was a problem hiding this comment.
This PR failed Diffblue compatibility checks (cbmc commit: 61ffc48).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/85635549
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).
There was a problem hiding this comment.
Passed Diffblue compatibility checks (cbmc commit: f2f2c60).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/85636056
|
@tautschnig Indeed much better to have this in the simplifier. |
This is motivated by the linked list implementation in FreeRTOS.