model-checking / kani

Kani Rust Verifier
https://model-checking.github.io/kani
Apache License 2.0
2.19k stars 87 forks source link

RMC doesn't seem to handle stack unwind logic correctly #545

Closed celinval closed 1 year ago

celinval commented 3 years ago

I was playing with the assertion codegen to understand how we were handling cleanup after a failure. I created the following test case:

// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
// SPDX-License-Identifier: Apache-2.0 OR MIT
//
// This test ensures that rmc follows the correct CFG for assertion failures.
// - Statements that succeeds an assertion failure should be unreachable.
// - Cleanup statements should still be executed though.
// - Note that failures while unwinding actually crashes the process. So drop may only be called
//   once.
// File: cleanup.rs

#[derive(PartialEq, Eq)]
struct S {
    a: u8,
    b: u16,
}

impl Drop for S {
    fn drop(&mut self) {
        assert!(false, "A1: This should still fail during cleanup");
    }
}

pub fn main() {
    let lhs = S { a: 42, b: 42 };
    let rhs = S { a: 0, b: 0 };
    assert!(lhs == rhs, "A2: A very false statement. Always fail.");
    assert!(false, "A3: Unreachable assert. Code always panic before this line.");
}

using the following command line invocation:

rmc cleanup.rs

I expected to see this happen: Assertions A1 and A2 should fail, but assertions A3 should be unreachable.

Instead, this happened: RMC entered an infinite loop.

I also tested the code with --unwind 0. The result is incorrect. A2 and A3 fail, but A1 doesn't.

[<S as std::ops::Drop>::drop.assertion.1] line 21 A1: This should still fail during cleanup: SUCCESS
....
[main.assertion.3] line 23 resume instruction: SUCCESS
[main.assertion.1] line 26 A2: A very false statement. Always fail.: FAILURE
[main.assertion.2] line 26 A3: Unreachable assert. Code always panic before this line.: FAILURE
celinval commented 3 years ago

Note that the cleanup logic seems correct when there is no unwinding:

// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
// SPDX-License-Identifier: Apache-2.0 OR MIT

#[derive(PartialEq, Eq)]
struct S {
    a: u8,
}

impl Drop for S {
    fn drop(&mut self) {
        assert!(false, "A1: This should still fail during cleanup");
    }
}

pub fn main() {
    let lhs = S { a: 42 };
    let rhs = S { a: 0 };
    assert!(lhs != rhs, "A2: A true statement. Succeed");
}

Result is:

[<S as std::ops::Drop>::drop.assertion.1] line 21 A1: This should still fail during cleanup: FAILURE
...
[main.assertion.2] line 22 resume instruction: SUCCESS
[main.assertion.1] line 25 A2: A true statement. Succeed: SUCCESS
celinval commented 2 years ago

There are actually two different bugs reported in this issue.

  1. Infinite loop.
  2. Incorrect cleanup logic.

We'll handle the bug #1 on issue #636 and we'll leave this issue to track bug #2

celinval commented 2 years ago

We don't support stack unwinding yet. I created a feature request (#692) to track that. I'll leave this issue open for now since it is a valid use case that we should ensure gets covered.

tedinski commented 1 year ago

I don't think this is tracking anything not in #692 and #267, closing.