-
Notifications
You must be signed in to change notification settings - Fork 277
Tests demonstrating pointer-encoding unsoundness #5823
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Changes from all commits
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,11 @@ | ||
#define MB 0x00100000 | ||
#define BASE (15 * MB) | ||
#define OFFSET (1 * MB) | ||
|
||
main() | ||
{ | ||
char *base = BASE; | ||
int offset = OFFSET; | ||
__CPROVER_assert( | ||
&((char *)base)[offset] >= BASE + OFFSET, "no wrap-around expected"); | ||
} | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. 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? There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Done. |
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,8 @@ | ||
KNOWNBUG | ||
main.c | ||
--32 | ||
^EXIT=0$ | ||
^SIGNAL=0$ | ||
^VERIFICATION SUCCESSFUL$ | ||
-- | ||
^warning: ignoring |
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,22 @@ | ||
#include <stdlib.h> | ||
|
||
int main() | ||
{ | ||
if(sizeof(void *) != 8) | ||
return 0; | ||
|
||
char *p = malloc(1); | ||
if(p == 0) | ||
return 0; | ||
|
||
if( | ||
(unsigned long)p > | ||
42) // unsoundly evaluates to true due to pointer encoding | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. 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. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. 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 |
||
{ | ||
return 0; | ||
} | ||
|
||
__CPROVER_assert(0, ""); | ||
|
||
return 0; | ||
} |
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,8 @@ | ||
KNOWNBUG | ||
main.c | ||
|
||
^EXIT=10$ | ||
^SIGNAL=0$ | ||
^VERIFICATION FAILED$ | ||
-- | ||
^warning: ignoring |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I'd say we half-support them... And I'd really like to see that fixed as well, might just happen along the way ;-)