model-checking
Disable floating-point overflow checks
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.
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.
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
@zhassan-aws I saw this flag. But I guess it also disables overflow checking for other types (like i32), which I don't want.
@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.
Why haven't we removed float overflow checks in the first place? I see that #3162 was never merged. @feliperodri?
Good point. I forgot about #3162. If overflow in these operations is not UB, then Kani shouldn't perform them by default.
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.
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.