-
Notifications
You must be signed in to change notification settings - Fork 97
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
Add experimental API to generate arbitrary pointers #3538
Add experimental API to generate arbitrary pointers #3538
Conversation
Pointer generator that can be used to generate an arbitrary pointer. This generator allows users to build pointers with different allocation status, initialization and alignemnt. It contains an internal buffer that it uses to generate `InBounds` and `OutBounds` pointers. In those cases, the pointers will have the same provenance as the generator, and the same lifetime.
Appears to break std verification:
|
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.
Thank you for working on this, but I think we really need more documentation to enable safe and sound use of this capability in any proofs that users may be constructing.
Make the type a parameter to the generator methods instead of the type.
Needed to change use order of test
@tautschnig, hopefully I addressed all your comments. I also moved the pointer type to be an argument of the methods instead of the generator type. |
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.
Nice!
Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com>
This change adds a pointer generator that can non-deterministically generate a pointer with different properties.
This generator allows users to build pointers with different allocation status, initialization and alignment.
It contains an internal buffer that it uses to generate
InBounds
andOutOfBounds
pointers.In those cases, the pointers will have the same provenance as the generator, and the same lifetime.
This approach is different than generating a pointer from an arbitrary
usize
. Kani uses demonic non-determinism to trackallocation lifetimes, which makes hard to reason about during verification. I.e., one cannot assume a pointer is valid, and initialized, and this can only be accomplished by manually tracking the pointer status.
I added the new API under
-Z mem-predicates
since it allows reasoning about memory, and I was hoping this wouldn't need another unstable flag. 😄By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.