[RFC] Two new failing tests demonstrating updates outside member bounds #6101
Conversation
Codecov Report
@@ Coverage Diff @@
## develop #6101 +/- ##
===========================================
- Coverage 74.52% 74.32% -0.21%
===========================================
Files 1447 1447
Lines 157808 157913 +105
===========================================
- Hits 117610 117370 -240
- Misses 40198 40543 +345
Continue to review full report at Codecov.
|
tautschnig
force-pushed
the
member-bounds
branch
2 times, most recently
from
97c41eb to
6e6affd
Compare
tautschnig
changed the title
|
I'm marking this RFC as I'd appreciate some thoughts about those tests. While they work perfectly fine with both gcc and clang, I'm not sure they are covered by the C standard. |
Arrays of arrays of non-constant size (as found in regression/cbmc/Multi_Dimensional_Array6) can still be lowered by the more general lowering code, although doing so is expensive.
These examples write to a member different from the access path being used, yet within the object bounds.
If using the new option --symex-no-member-bounds, goto-symex will rewrite all indexed writes that constant propagation does not show to be within bounds to writes to the member object.
There was a problem hiding this comment.
I think this falls in the general area of "defining undefined behaviour". The out-of-bound write is UB so, as much as ISO 9899 has anything to say... whatever we do after is correct. I think the most important thing is that we can detect this happening. Apart from that ... emulating popular compilers is probably not a bad idea.
| int A[3]; | ||
| _Static_assert(sizeof(A) == sizeof(struct S), ""); | ||
| struct S *s = A; | ||
| s->a[2] = 42; |
There was a problem hiding this comment.
Pretty sure this is undefined behaviour...
|
I am afraid that "access beyond member bounds" needs to be enabled by default. It's not an uncommon idiom at all. |
I'll try to work out a fix. The proposed patch only partly addresses the problem, we'll need to disable field sensitivity when detecting such an access beyond member bounds. |
The option --no-simplify should be honoured by field sensitivity. This also made apparent that we have tests that only pass thanks to the simplifier, and perhaps aren't even expected to pass. See diffblue#6101 for further discussion.
The option --no-simplify should be honoured by field sensitivity. This also made apparent that we have tests that only pass thanks to the simplifier, and perhaps aren't even expected to pass. See diffblue#6101 for further discussion.
The option --no-simplify should be honoured by field sensitivity. This also made apparent that we have tests that only pass thanks to the simplifier, and perhaps aren't even expected to pass. See diffblue#6101 for further discussion.
The option --no-simplify should be honoured by field sensitivity. This also made apparent that we have tests that only pass thanks to the simplifier, and perhaps aren't even expected to pass. See diffblue#6101 for further discussion.
These examples write to a member different from the access path being
used, yet within the object bounds.