Skip to content
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

Avoid undefined behavior in AnySlice::new() #2288

Merged
merged 1 commit into from
Mar 9, 2023

Conversation

feliperodri
Copy link
Contributor

Reported by @roypat, thanks!

Summary

I tried this code:

struct MyStruct(i32);

impl Drop for MyStruct {
    fn drop(&mut self) {
        assert!(self.0 == 1);
    }
}

impl kani::Arbitrary for MyStruct {
    fn any() -> Self {
         MyStruct(1)
    }
}

#[kani::proof]
fn my_proof() {
    let my_slice = kani::slice::any_slice::<MyStruct, 1>();
}

using the following command line invocation:

cargo kani

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 for MyStruct deterministically sets MyStruct.0 to 1.

Instead, this happened:
Verification failed with the following output

Check 17: <MyStruct as std::ops::Drop>::drop.assertion.1
	 - Status: FAILURE
	 - Description: "assertion failed: self.0 == 1"
	 - Location: src/main.rs:9:9 in function <MyStruct as std::ops::Drop>::drop

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]

while i < any_slice.slice_len && i < MAX_SLICE_LENGTH {
    *any_slice.ptr.add(i) = any();
     i += 1;
}

initializes memory by dereferencing any_slice.ptr.add(i), which is a pointer to memory allocated by std::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 causes Drop::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 thus MyStruct.0 will not be 1, as expected). This is in-fact undefined behavior. The proper way to initialize memory is to use std::ptr::write or std::mem::MaybeUninit. I have locally verified that replacing the line *any_slice.ptr.add(i) = any() with std::ptr::write(any_slice.ptr.add(i), any()) causes the verification of the harness above to pass.

Checklist

  • Each commit message has a non-empty body, explaining why the change was made
  • Methods or procedures are documented
  • Regression or unit tests are included, or existing tests cover the modified code
  • My PR is restricted to a single feature or bugfix

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

@feliperodri feliperodri added the [F] Spurious Failure Issues that cause Kani verification to fail despite the code being correct. label Mar 9, 2023
@feliperodri feliperodri requested a review from a team as a code owner March 9, 2023 19:06
Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>
@feliperodri feliperodri enabled auto-merge (squash) March 9, 2023 19:45
@feliperodri feliperodri requested a review from zhassan-aws March 9, 2023 19:46
Copy link
Contributor

@zhassan-aws zhassan-aws left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks @feliperodri!

@feliperodri feliperodri merged commit 4b925fd into model-checking:main Mar 9, 2023
@feliperodri feliperodri deleted the fix-anyslice branch March 9, 2023 20:40
@feliperodri feliperodri self-assigned this Mar 9, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
[F] Spurious Failure Issues that cause Kani verification to fail despite the code being correct.
Projects
No open projects
Status: Done
Development

Successfully merging this pull request may close these issues.

2 participants