Disable floating-point overflow checks

[cospectrum]

Is there a way to specifically disable the floating-point overflow checks?
I only want to ignore the following errors (and nothing else):

Failed Checks: NaN on multiplication
Failed Checks: NaN on addition
Failed Checks: arithmetic overflow on floating-point addition
Failed Checks: arithmetic overflow on floating-point multiplication

If it's not possible, is there a way to implement custom add/mul functions to make kani happy? Any tips.

[cospectrum]

I inserted my own mul/add functions, which solved my problem:

const F32_BOUND: f32 = 1e3;

fn add_f32(a: f32, b: f32) -> f32 {
    #[cfg(kani)]
    {
        kani::assume(a.abs() < F32_BOUND);
        kani::assume(b.abs() < F32_BOUND);
    }
    a + b
}

fn mul_f32(a: f32, b: f32) -> f32 {
    #[cfg(kani)]
    {
        kani::assume(a.abs() < F32_BOUND);
        kani::assume(b.abs() < F32_BOUND);
    }
    a * b
}

It can be also just assume before usage of *, + in problem areas.

[zhassan-aws]

Hi @cospectrum. The --no-overflow-checks option disables the floating-point overflow and NaN checks. For example, for the following program:

#[kani::proof]
fn check_overflow() {
    let x: f32 = kani::any();
    let y: f32 = kani::any();
    let z: f32 = x + y;
    if x == 0.0 {
        assert!(y.is_nan() || z == y);
    } else if y == 0.0 {
        assert!(x.is_nan() || z == x);
    }
}

the overflow and NaN checks fail:

$ kani f32overflow.rs
...
SUMMARY:
 ** 2 of 4 failed
Failed Checks: NaN on addition
 File: "f32overflow.rs", line 5, in check_overflow
Failed Checks: arithmetic overflow on floating-point addition
 File: "f32overflow.rs", line 5, in check_overflow

but verification is successful with --no-overflow-checks:

$ kani f32overflow.rs --no-overflow-checks
...

SUMMARY:
 ** 0 of 2 failed

VERIFICATION:- SUCCESSFUL

[cospectrum]

@zhassan-aws I saw this flag. But I guess it also disables overflow checking for other types (like i32), which I don't want.

[zhassan-aws]

@cospectrum It actually doesn't disable overflow checking for other types:

$ cat of.rs 
#[kani::proof]
fn check_overflow() {
    let x: u8 = kani::any();
    let y: u8 = kani::any();
    let z = x + y;
}

$ kani of.rs --no-overflow-checks
...
SUMMARY:
 ** 1 of 1 failed
Failed Checks: attempt to add with overflow
 File: "of.rs", line 5, in check_overflow

We need to update the help/option name to clarify this.

[celinval]

Why haven't we removed float overflow checks in the first place? I see that #3162 was never merged. @feliperodri?

[zhassan-aws]

Good point. I forgot about #3162. If overflow in these operations is not UB, then Kani shouldn't perform them by default.

[celinval]

TBH, I'm not even convinced we should offer an option to perform them.

[feliperodri]

Why haven't we removed float overflow checks in the first place? I see that #3162 was never merged. @feliperodri?

@celinval at the time, we choose to keep them to be more conservative, I guess. See this response. I still believe it should be an option that the user can include to check such behaviors.

[celinval]

Why haven't we removed float overflow checks in the first place? I see that #3162 was never merged. @feliperodri?

@celinval at the time, we choose to keep them to be more conservative, I guess. See this response. I still believe it should be an option that the user can include to check such behaviors.

If users really want to, they can still enable them using --cbmc-args.