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

Intrinsic type_swapped fails for unit types #3182

Closed
celinval opened this issue May 14, 2024 · 0 comments · Fixed by #3256
Closed

Intrinsic type_swapped fails for unit types #3182

celinval opened this issue May 14, 2024 · 0 comments · Fixed by #3256
Labels
[C] Bug This is a bug. Something isn't working.

Comments

@celinval
Copy link
Contributor

I tried this code:

//! swap.rs

#[kani::proof]
pub fn check_swap_unit() {
    let mut x: () = kani::any();
    let mut y: () = kani::any();
    std::mem::swap(&mut x, &mut y)
}

using the following command line invocation:

kani swap.rs

with Kani version: 0.51.0

I expected to see this happen: Verification succeeded

Instead, this happened: Verification failed

SUMMARY:
 ** 18 of 21 failed
Failed Checks: dereference failure: pointer NULL
Failed Checks: dereference failure: pointer invalid
Failed Checks: dereference failure: deallocated dynamic object
Failed Checks: dereference failure: dead object
Failed Checks: dereference failure: pointer outside object bounds
Failed Checks: dereference failure: invalid integer address
Failed Checks: dereference failure: pointer NULL
 File: "/home/ANT.AMAZON.COM/celinval/.rustup/toolchains/nightly-2024-04-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/mem/mod.rs", line 731, in std::mem::swap::<()>
Failed Checks: dereference failure: pointer invalid
 File: "/home/ANT.AMAZON.COM/celinval/.rustup/toolchains/nightly-2024-04-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/mem/mod.rs", line 731, in std::mem::swap::<()>
Failed Checks: dereference failure: deallocated dynamic object
 File: "/home/ANT.AMAZON.COM/celinval/.rustup/toolchains/nightly-2024-04-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/mem/mod.rs", line 731, in std::mem::swap::<()>
Failed Checks: dereference failure: dead object
 File: "/home/ANT.AMAZON.COM/celinval/.rustup/toolchains/nightly-2024-04-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/mem/mod.rs", line 731, in std::mem::swap::<()>
Failed Checks: dereference failure: pointer outside object bounds
 File: "/home/ANT.AMAZON.COM/celinval/.rustup/toolchains/nightly-2024-04-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/mem/mod.rs", line 731, in std::mem::swap::<()>
Failed Checks: dereference failure: invalid integer address
 File: "/home/ANT.AMAZON.COM/celinval/.rustup/toolchains/nightly-2024-04-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/mem/mod.rs", line 731, in std::mem::swap::<()>
Failed Checks: dereference failure: pointer NULL
 File: "/home/ANT.AMAZON.COM/celinval/.rustup/toolchains/nightly-2024-04-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/mem/mod.rs", line 731, in std::mem::swap::<()>
Failed Checks: dereference failure: pointer invalid
 File: "/home/ANT.AMAZON.COM/celinval/.rustup/toolchains/nightly-2024-04-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/mem/mod.rs", line 731, in std::mem::swap::<()>
Failed Checks: dereference failure: deallocated dynamic object
 File: "/home/ANT.AMAZON.COM/celinval/.rustup/toolchains/nightly-2024-04-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/mem/mod.rs", line 731, in std::mem::swap::<()>
Failed Checks: dereference failure: dead object
 File: "/home/ANT.AMAZON.COM/celinval/.rustup/toolchains/nightly-2024-04-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/mem/mod.rs", line 731, in std::mem::swap::<()>
Failed Checks: dereference failure: pointer outside object bounds
 File: "/home/ANT.AMAZON.COM/celinval/.rustup/toolchains/nightly-2024-04-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/mem/mod.rs", line 731, in std::mem::swap::<()>
Failed Checks: dereference failure: invalid integer address
 File: "/home/ANT.AMAZON.COM/celinval/.rustup/toolchains/nightly-2024-04-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/mem/mod.rs", line 731, in std::mem::swap::<()>

I believe this is a regression introduced by #3134. I believe the correct fix is to modify this intrinsic to become a no-op for ZST.

@celinval celinval added the [C] Bug This is a bug. Something isn't working. label May 14, 2024
tautschnig added a commit to tautschnig/kani that referenced this issue Jun 11, 2024
typed_swap needs to be a no-op on ZSTs as pointers to those have an
arbitrary value in Kani.

Resolves: model-checking#3182
tautschnig added a commit that referenced this issue Jun 12, 2024
typed_swap needs to be a no-op on ZSTs as pointers to those have an
arbitrary value in Kani.

Resolves: #3182
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
[C] Bug This is a bug. Something isn't working.
Projects
None yet
Development

Successfully merging a pull request may close this issue.

1 participant