Skip to content

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
@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