Tests demonstrating pointer-encoding unsoundness #5823
Conversation
Codecov Report
@@ Coverage Diff @@
## develop #5823 +/- ##
========================================
Coverage 72.85% 72.85%
========================================
Files 1423 1421 -2
Lines 154072 154130 +58
========================================
+ Hits 112244 112292 +48
- Misses 41828 41838 +10
Continue to review full report at Codecov.
|
| int offset = OFFSET; | ||
| int n = 2; | ||
| __CPROVER_assert(&((char *)base)[offset] != 0, "no wrap-around expected"); | ||
| } |
There was a problem hiding this comment.
This one feels like it's a bit overfitted to the current encoding -- how about checking that the conversion to an integer doesn't get smaller?
|
|
||
| main() | ||
| { | ||
| char *base = BASE; |
There was a problem hiding this comment.
I'm a little concerned by this. As I understand CBMC's memory model we do not support literal addresses. I don't think we are required to do so by the standard either.
There was a problem hiding this comment.
I'd say we half-support them... And I'd really like to see that fixed as well, might just happen along the way ;-)
|
|
||
| if( | ||
| (unsigned long)p > | ||
| 42) // unsoundly evaluates to true due to pointer encoding |
There was a problem hiding this comment.
Is this unsound? ISO-9899 allows conversion of pointers to integers but doesn't say what they will be. Thinking about actual platforms, this kind of thing could be ASLR dependent!
There was a problem hiding this comment.
Agreed, and I would thus argue that the assertion below ought to be considered reachable by a sound verification tool (i.e., there exists some system configuration under which p is less or equal to 42).
The tests exercise the way the back-end encodes pointers. Upcoming encoding changes will ensure that these can soundly be handled.
tautschnig
force-pushed
the
pointer-encoding-tests
branch
from
a4e2c1b to
e5e8239
Compare
The tests exercise the way the back-end encodes pointers. Upcoming
encoding changes will ensure that these can soundly be handled.