Spurious overflow failures with Result/Error types

[zhassan-aws]

I tried this code:

enum MyError {
    Val1,
    Val2,
}

fn foo(x: u32) -> Result<(), MyError> {
    if x > 10 {
        Err(MyError::Val2)
    } else {
        Ok(())
    }
}

fn bar() -> Result<(), MyError> {
    let x = foo(15)?;

    Ok(x)
}

pub fn main() {
    bar();
}

using the following command line invocation:

rmc test.rs

with RMC version: 7635cfebfa5

I expected to see this happen: no failures

Instead, this happened: got 2 arithmetic overflow failures:

** Results:
/home/ubuntu/tools/rmc/library/core/src/result.rs function <std::result::Result<T, E> as std::ops::Try>::branch
[<std::result::Result<T, E> as std::ops::Try>::branch.assertion.1] line 1903 unreachable code: SUCCESS
[<std::result::Result<T, E> as std::ops::Try>::branch.overflow.1] line 1903 arithmetic overflow on unsigned - in ((unsigned char *)&self)[0] - 2: FAILURE
[<std::result::Result<T, E> as std::ops::Try>::branch.pointer_arithmetic.1] line 1903 pointer arithmetic: dead object in (unsigned char *)&self + 0: SUCCESS
[<std::result::Result<T, E> as std::ops::Try>::branch.pointer_dereference.1] line 1903 dereference failure: dead object in ((unsigned char *)&self)[0]: SUCCESS
[<std::result::Result<T, E> as std::ops::Try>::branch.pointer_arithmetic.2] line 1904 pointer arithmetic: dead object in (unsigned char *)&var_0 + 0: SUCCESS
[<std::result::Result<T, E> as std::ops::Try>::branch.pointer_dereference.2] line 1904 dereference failure: dead object in ((unsigned char *)&var_0)[0]: SUCCESS

/home/ubuntu/tools/rmc/src/test/rmc/Enum/result4.rs function bar
[bar.assertion.1] line 18 unreachable code: SUCCESS
[bar.overflow.1] line 18 arithmetic overflow on unsigned - in ((unsigned char *)&var_2)[0] - 2: FAILURE
[bar.pointer_arithmetic.1] line 18 pointer arithmetic: dead object in (unsigned char *)&var_2 + 0: SUCCESS
[bar.pointer_dereference.1] line 18 dereference failure: dead object in ((unsigned char *)&var_2)[0]: SUCCESS
[bar.pointer_arithmetic.2] line 20 pointer arithmetic: dead object in (unsigned char *)&var_0 + 0: SUCCESS
[bar.pointer_dereference.2] line 20 dereference failure: dead object in ((unsigned char *)&var_0)[0]: SUCCESS

/home/ubuntu/tools/rmc/src/test/rmc/Enum/result4.rs function foo
[foo.pointer_arithmetic.1] line 13 pointer arithmetic: dead object in (unsigned char *)&var_0 + 0: SUCCESS
[foo.pointer_dereference.1] line 13 dereference failure: dead object in ((unsigned char *)&var_0)[0]: SUCCESS

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

The - 2 in the check:

[bar.overflow.1] line 18 arithmetic overflow on unsigned - in ((unsigned char *)&var_2)[0] - 2: FAILURE

seems to be coming from the number of values in the enum. The arithmetic overflow checks are not expected in the first place.

[adpaco-aws]

There is a bunch of test cases from the "Rust by Example" book that show similar behaviors:

Rust by Example/Error handling/Multiple error types/Boxing errors/11.rs Rust by Example/Error handling/Multiple error types/Defining an error type/18.rs Rust by Example/Error handling/Multiple error types/Other uses of ?/25.rs Rust by Example/Error handling/Multiple error types/Pulling Results out of Options/34.rs Rust by Example/Error handling/Multiple error types/Pulling Results out of Options/6.rs Rust by Example/Error handling/Multiple error types/Wrapping errors/5.rs Rust by Example/Error handling/Option & unwrap/Combinators: and_then/15.rs Rust by Example/Error handling/Option & unwrap/Combinators: map/15.rs Rust by Example/Error handling/Option & unwrap/Unpacking options with ?/19.rs Rust by Example/Error handling/Result/64.rs Rust by Example/Error handling/Result/Early returns/11.rs Rust by Example/Error handling/Result/Introducing ?/16.rs Rust by Example/Error handling/Result/Introducing ?/46.rs Rust by Example/Error handling/Result/aliases for Result/14.rs Rust by Example/Error handling/Result/map for Result/15.rs Rust by Example/Error handling/Result/map for Result/54.rs

Adding a high priority label to this since reasoning correctly about Result types (or Enum in general) is a must.

[tedinski]

This disappeared with Result<u32, MyError>, right? As a result, I strongly suspect we're mishandling the niche optimization somewhere.

We might want to get more thorough about tests surrounding that feature.

[zhassan-aws]

Correct, replacing () with u32 makes the failures disappear.

[celinval]

I am currently investigating if this is an issue with how we handle discriminant.

[celinval]

I see that our own tests have a --no-overflow-checks to avoid the overflow issue. See https://github.com/model-checking/rmc/blob/main/src/test/rmc/SwitchInt/main.rs#L7 for an example.

I believe the issue is related to how we compute relative discriminant here: https://github.com/model-checking/rmc/blob/fdf86e5f071a0474ad5bc2f3f5594a1a403dbb9d/compiler/rustc_codegen_rmc/src/codegen/rvalue.rs#L473

[celinval]

I checked the code and the computation itself is correct. The overflow is per design. In this specific case, the compiler encodes Result<(), MyError> as a u8 where:

• MyError::Val1 = 0
• MyError::Val2 = 1
• None = 2

The compiler will subtract 2 out of the value to check if it's None or not.

The issue here is that we don't handle wrapping arithmetic operations correctly. The following code will trigger an overflow failure even though users are explicitly saying it's ok:

// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
// SPDX-License-Identifier: Apache-2.0 OR MIT
//
// Check that none of these operations trigger spurious overflow checks.

pub fn main() {
    let a: u8 = rmc::nondet();
    let b: u8 = rmc::nondet();
    a.wrapping_add(b);
}

Looking at CBMC's documentation, it looks like we should be adding pragma to skip overflow checks for statements where wrapping arithmetic is expected: http://www.cprover.org/cprover-manual/properties/

[zhassan-aws]

I see. So, this is pretty much a duplicate of #480?

[adpaco-aws]

Just wanted to mention that wrapping_add and other are actually intrinsics which appear to be codegen'd as regular operations at the moment. This is the code in codegen_intrinsic from compiler/rustc_codegen_rmc/src/codegen/intrinsic.rs:

            "wrapping_add" => codegen_intrinsic_binop!(plus),
            "wrapping_mul" => codegen_intrinsic_binop!(mul),
            "wrapping_sub" => codegen_intrinsic_binop!(sub),

Is this okay? I would expect these intrinsics to add some logic for handling overflows on their own, similar to what we do for add_with_overflow and similar intrinsics. @celinval have you tried that already?

[celinval]

Just wanted to mention that wrapping_add and other are actually intrinsics which appear to be codegen'd as regular operations at the moment. This is the code in codegen_intrinsic from compiler/rustc_codegen_rmc/src/codegen/intrinsic.rs:

            "wrapping_add" => codegen_intrinsic_binop!(plus),
            "wrapping_mul" => codegen_intrinsic_binop!(mul),
            "wrapping_sub" => codegen_intrinsic_binop!(sub),

Is this okay? I would expect these intrinsics to add some logic for handling overflows on their own, similar to what we do for add_with_overflow and similar intrinsics. @celinval have you tried that already?

RustC actually lowers wrapping_* intrinsics during MIR transformations now and replace them by BinOp::Add.

https://github.com/rust-lang/rust/blob/master/compiler/rustc_mir_transform/src/lower_intrinsics.rs#L75

I was initially thinking about using CBMC pragmas to remove the overflow checks from wrapping operations. However, rustc already add assertions to check for overflow by default for non-wrapping operations.

Thus, I'm thinking about disabling cbmc overflow checks since they are redundant. Unless someone can think about a scenario that it's actually adding value.

[celinval]

I see. So, this is pretty much a duplicate of #480?

Slightly different issue but same underlying cause. We treat all arithmetic operations as non-wrapping.