-
Notifications
You must be signed in to change notification settings - Fork 62
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
NULL-checking a pointer argument yields "Proof failed." #120
Comments
It seems that there's a related bug with: bool test(uint8_t* a, uint8_t* b) {
return a == b;
} Although (I assume) the simulator allocates two arrays when verifying, the function always returns true. |
The issue going on here is that the return value from an allocation is currently just a free variable. There's no constraint that is isn't equal to some specific constant (say zero), or that it isn't equal to any other pointer. In the second example, it's not possible to prove that the function returns either true or false. |
This is partly fixed. We now assume that pointers declared in a spec passed to Note that this is a lack of completeness rather than a lack of soundness. We can't exploit this issue to prove a program correct that is not correct. But we may not be able to prove a correct program to be correct. |
Notice this issue appears in a different form with the crucible backend. I believe a faithful translation is:
Which yields:
|
With some small changes, the example works: Change
We seriously need to improve the error messages, though. SAW should inform the user that |
Check types in context of private symbols
The error messages are more informative now. Without the
And, before replacing
|
Assume a function that checks whether its pointer argument is NULL:
Now take a SAW script that proves it always returns 0 with a non-null argument:
This however returns "Proof failed.":
Adding
llvm_assert_eq "*a" {{ [0:[8]] }};
to fix the input argument to a specific value doesn't help here either. The only way to make this work seems currently to remove the NULL-check.The text was updated successfully, but these errors were encountered: