Panic and abort should stop the program execution

[celinval]

I tried this code:

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

pub fn main() {
    for i in 0..4 {
        if i == 1 {
            panic!("This comes first");
        }
        if i == 2 {
            panic!("This should never happen");
        }
    }
}

using the following command line invocation:

rmc loop.rs

I expected to see this happen: The first assertion should fail but the second one should be unreachable. The panic call should abort the execution in the second iteration of the loop.

Instead, this happened: Both assertions fail. The trace for the second assertion includes the first panic call.

Note that the same behavior happens if we replace the panic!() statement by process::abort().

[celinval]

An easy fix right now would be to condegen these failures as:

assert(cond);
assume(cond);

However, this is not actually sound since we are ignoring the unwind path. I created #545 to handle unwind logic.

[zhassan-aws]

This is also how CBMC behaves. For example, for:

#include <assert.h>

int main() {
    int x = 5;
    assert(x < 3);
    assert(x < 4);
    return 0;
}

Both assertions fail:

** Results:
test.c function main
[main.assertion.1] line 5 assertion x < 3: FAILURE
[main.assertion.2] line 6 assertion x < 4: FAILURE

** 2 of 2 failed (2 iterations)
VERIFICATION FAILED

Perhaps we can add an option, e.g. --assert-fail-aborts that changes to the behavior you described? We can document that using this option could lead to missing assertion failures during stack unwinding.

[celinval]

I think we should always abort for user asserts, since that is the semantics of assert in rust. Note that if you add an assert!(false); or a panic statement, the rust compiler considers everything else that is dominated by that statement as dead code and removes it.

For debug_assert and other checks that we add, we should not abort since the code after the failure may still reachable during a release execution.

[celinval]

Note that assertions in C have different semantics since they can be enabled / disabled according to the value of NDEBUG. https://en.cppreference.com/w/cpp/error/assert