Avoid undefined behavior in AnySlice::new() #2288
Merged
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Reported by @roypat, thanks!
Summary
I tried this code:
using the following command line invocation:
Kani version: 0.23.0 (verified to still happen when building from source from main branch)
I expected to see this happen: Verification to pass, as the
kani::Arbitrary
implementation forMyStruct
deterministically setsMyStruct.0
to 1.Instead, this happened:
Verification failed with the following output
I have attached the full kani log as an attachment (I'm not sure how to do collapsible codeblocks on SIM-T).
The cause for this unexpected verification failure is the way
kani::slice::any_slice
is implemented. The loop [1]initializes memory by dereferencing
any_slice.ptr.add(i)
, which is a pointer to memory allocated bystd::alloc::alloc
[2]. This memory is uninitialized. This is not a problem in other languages, but in Rust, assigning to a memory location via pointer dereferencing causesDrop::drop
to be called for the location to which the pointer points. In this case, this means that uninitialized memory gets dropped (which is why the verification fails: the uninitialized memory that gets dropped is zeroed, and thusMyStruct.0
will not be 1, as expected). This is in-fact undefined behavior. The proper way to initialize memory is to usestd::ptr::write
orstd::mem::MaybeUninit
. I have locally verified that replacing the line*any_slice.ptr.add(i) = any()
withstd::ptr::write(any_slice.ptr.add(i), any())
causes the verification of the harness above to pass.Checklist
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.