kani icon indicating copy to clipboard operation
kani copied to clipboard

RMC doesn't seem to handle stack unwind logic correctly

Open celinval opened this issue 4 years ago • 3 comments

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 avatar Oct 07 '21 23:10 celinval

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 avatar Oct 07 '21 23:10 celinval

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 avatar Dec 07 '21 19:12 celinval

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.

celinval avatar Dec 14 '21 21:12 celinval

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

tedinski avatar Nov 14 '22 16:11 tedinski