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

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

Closed
celinval opened this issue Oct 7, 2021 · 4 comments
Closed

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

celinval opened this issue Oct 7, 2021 · 4 comments
Labels
[C] Feature / Enhancement A new feature request or enhancement to an existing feature.
Milestone

Comments

@celinval
Copy link
Contributor

celinval commented Oct 7, 2021

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 celinval added [C] Bug This is a bug. Something isn't working. Area: compilation T-High Priority Tag issues that have high priority [F] Soundness Kani failed to detect an issue labels Oct 7, 2021
@celinval
Copy link
Contributor Author

celinval commented Oct 7, 2021

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 celinval changed the title RMC codegen for cleanup logic is incorrect and it generates a loop RMC codegen for cleanup logic is incorrect and it may even result in a loop Oct 8, 2021
@celinval celinval self-assigned this Oct 8, 2021
@celinval celinval added this to the Soundness milestone Oct 8, 2021
@celinval celinval changed the title RMC codegen for cleanup logic is incorrect and it may even result in a loop RMC doesn't seem to handle unwind logic correctly Oct 8, 2021
@celinval celinval changed the title RMC doesn't seem to handle unwind logic correctly RMC doesn't seem to handle stack unwind logic correctly Oct 12, 2021
@celinval
Copy link
Contributor Author

celinval commented Dec 7, 2021

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 added a commit to celinval/kani-dev that referenced this issue Dec 10, 2021
I refactored how we codegen panic statements so it now it terminate the
program per its spec. I have also removed the hack we had to try to get
the assert location.

Since we currently do not support stack unwinding, the panic codegen
will always terminate immediately and it will not try to unwind the stack.
I added an option to RMC to force the compiler to use abort as the panic
strategy and a check to rmc codegen that will fail if the user tries to
override that.

Another note is that we currently do not support `#[track_caller]` and I
have not changed that.

This change fixes #67, fixes model-checking#466, fixes model-checking#543, and fixes model-checking#636. This
change also mitigates model-checking#545.
celinval added a commit that referenced this issue Dec 14, 2021
I refactored how we codegen panic statements so it now it terminate the
program per its spec. I have also removed the hack we had to try to get
the assert location.

Since we currently do not support stack unwinding, the panic codegen
will always terminate immediately and it will not try to unwind the stack.
I added an option to RMC to force the compiler to use abort as the panic
strategy and a check to rmc codegen that will fail if the user tries to
override that.

Another note is that we currently do not support `#[track_caller]` and I
have not changed that.

This change fixes #67, fixes #466, fixes #543, and fixes #636. This
change also mitigates #545.
@celinval
Copy link
Contributor Author

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 celinval added [C] Feature / Enhancement A new feature request or enhancement to an existing feature. and removed [C] Bug This is a bug. Something isn't working. T-High Priority Tag issues that have high priority [F] Soundness Kani failed to detect an issue Soundness: Medium labels Mar 14, 2022
tedinski pushed a commit to tedinski/rmc that referenced this issue Apr 22, 2022
I refactored how we codegen panic statements so it now it terminate the
program per its spec. I have also removed the hack we had to try to get
the assert location.

Since we currently do not support stack unwinding, the panic codegen
will always terminate immediately and it will not try to unwind the stack.
I added an option to RMC to force the compiler to use abort as the panic
strategy and a check to rmc codegen that will fail if the user tries to
override that.

Another note is that we currently do not support `#[track_caller]` and I
have not changed that.

This change fixes model-checking#67, fixes model-checking#466, fixes model-checking#543, and fixes model-checking#636. This
change also mitigates model-checking#545.
tedinski pushed a commit to tedinski/rmc that referenced this issue Apr 25, 2022
I refactored how we codegen panic statements so it now it terminate the
program per its spec. I have also removed the hack we had to try to get
the assert location.

Since we currently do not support stack unwinding, the panic codegen
will always terminate immediately and it will not try to unwind the stack.
I added an option to RMC to force the compiler to use abort as the panic
strategy and a check to rmc codegen that will fail if the user tries to
override that.

Another note is that we currently do not support `#[track_caller]` and I
have not changed that.

This change fixes model-checking#67, fixes model-checking#466, fixes model-checking#543, and fixes model-checking#636. This
change also mitigates model-checking#545.
tedinski pushed a commit to tedinski/rmc that referenced this issue Apr 26, 2022
I refactored how we codegen panic statements so it now it terminate the
program per its spec. I have also removed the hack we had to try to get
the assert location.

Since we currently do not support stack unwinding, the panic codegen
will always terminate immediately and it will not try to unwind the stack.
I added an option to RMC to force the compiler to use abort as the panic
strategy and a check to rmc codegen that will fail if the user tries to
override that.

Another note is that we currently do not support `#[track_caller]` and I
have not changed that.

This change fixes model-checking#67, fixes model-checking#466, fixes model-checking#543, and fixes model-checking#636. This
change also mitigates model-checking#545.
tedinski pushed a commit that referenced this issue Apr 27, 2022
I refactored how we codegen panic statements so it now it terminate the
program per its spec. I have also removed the hack we had to try to get
the assert location.

Since we currently do not support stack unwinding, the panic codegen
will always terminate immediately and it will not try to unwind the stack.
I added an option to RMC to force the compiler to use abort as the panic
strategy and a check to rmc codegen that will fail if the user tries to
override that.

Another note is that we currently do not support `#[track_caller]` and I
have not changed that.

This change fixes #67, fixes #466, fixes #543, and fixes #636. This
change also mitigates #545.
@celinval celinval removed their assignment Aug 9, 2022
@tedinski
Copy link
Contributor

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

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
[C] Feature / Enhancement A new feature request or enhancement to an existing feature.
Projects
None yet
Development

No branches or pull requests

2 participants