Integer overflow panics in debug mode but is allowed by the verifier

[utaal]

Integer overflow is defined to behave as follows by the currently adopted RFC 560 https://github.com/rust-lang/rfcs/blob/master/text/0560-integer-overflow.md

The operations +, -, *, can underflow and overflow. When checking is enabled this will panic. When checking is disabled this will two's complement wrap.

In modern rust, debug_assertions (which includes overflow checking) is enabled when compiling with the debug default configurations. In the release (optimized) default config, debug_assertions is disabled, and the overflowing operations will wrap.
Because of this, integer overflow is never undefined behavior[^1]. Note that this is different from the unchecked_* operations on integers, which are undefined behavior if they overflow, e.g. for u64::unchecked_add.

Verus currently admits overflowing operations which will panic when compiled with debug_assertions. This can be regarded as a soundness issue (verified code should not panic).

---

How to address this is still up for debate, but it may be worth noting that if we were to introduce verification conditions for integer operations that ensure there's no overflow, we could also replace the native operations with their unchecked_math counterparts, which (apparently) can use LLVM intrinsics that can be faster because they assume no overflow can occur.

/cc @Chris-Hawblitzel

[tjhance]

Given:

• Rust idiomatically discourages overflow; and while it doesn't define overflow as UB, it also does not unambiguously define it to a single behavior
• Defining overflow to use wraparound will make verification errors difficult to diagnose (because an assertion might fail due to wrap-around, without having an error specifically about overflow)

the points seem in favor that Verus should probably check for no overflow.

[parno]

I agree that developers will (and should) expect verified code not to panic. I also like the notion that we can use the verification of non-overflow to optimize the code. We should try to find more such cases as we develop Verus (e.g., Rust already does a good job of eliminating array bounds checks, but verification should require us to eliminate any need for them at all).

[jaybosamiya]

+1 to the above comments. Additionally, I would like to note that there already exists constructs in Rust for intentionally-wrapping and intentionally-checked behavior, and that + being checked-at-debug and wrapping-at-release is simply a performance+safety compromise on values that are intended-non-overflowing.

For intentionally-wrapping arithmetic with the exact same ergonomics as + in Rust, using the Wrapping wrapper type is quite convenient.

Relevant docs from there (emphasis mine):

Operations like + on u32 values are intended to never overflow, and in some debug configurations overflow is detected and results in a panic. While most arithmetic falls into this category, some code explicitly expects and relies upon modular arithmetic (e.g., hashing).

Wrapping arithmetic can be achieved either through methods like wrapping_add, or through the Wrapping<T> type, which says that all standard arithmetic operations on the underlying value are intended to have wrapping semantics.

[utaal]

Currently, this passes:

fn test(a: u64) {
    let mut j = a;
    j = j + 2;
    assert(j == a + 2);
}

and this fails

fn test(a: u64) {
    let mut j = a;
    j = j + 2;
    j = j + 2;
    assert(j == a + 4);
}

because of how subexpression substitution works. We should be careful about that when we address this issue.

[utaal]

My current idea for this is that by default we generate verification conditions to ensure arithmetic doesn't overflow (and so we could also potentially use unchecked arithmetic by rewriting math operations during e.g. erasue, and we never panic for overflow in debug mode).

In addition, we can have a flag that disables the overflow check VCs (that is, returns to the current behaviour): this would be intended to be used in conjunction with disabling debug_assertions, so that debug builds do not panic on overflow, but one still cannot rely on the wrapping behaviour for verification (arithmetic operations are still specified to yield an undetermined result when overflowing).

Finally, one should be able to use wrapping operations (or the Wrapping wrapper type), specified to wrap.

[scottmcm]

which (apparently) can use LLVM intrinsics that can be faster because they assume no overflow can occur.

I know this is an old PR, but to elaborate on this a bit: I don't know that any of the instructions are directly faster with the no-wrap flags (at least on normal chips -- if you have a 1s-complement machine things might be weirder).

The difference, from what I've seen, is entirely in the optimizations that are only legal because of the lack of overflow. As a trivial example, x * 2 / 2 is only x if that first overflow is known not to overflow. (And while that code might look weird on its own, it's exactly what happens in my_slice_of_u16().iter().len(), for example.)