kani
kani copied to clipboard
Checking result of repeated operation takes long
I tried this code:
#[kani::proof]
#[kani::unwind(2)]
fn check_repeat() {
let x: u32 = kani::any();
let y: u32 = kani::any();
let o1 = x.saturating_mul(y);
let o2 = x.saturating_mul(y);
assert_eq!(o1, o2);
}
using the following command line invocation:
kani repeat.rs
with Kani version: d84b123afdf
I expected to see this happen: Verification is successful and completes reasonably quickly.
Instead, this happened: Verification runs for more than 30 minutes without terminating.
If I change the types of x
and y
to u16
, verification completes in 43 seconds, which is still too slow.
SUMMARY:
** 0 of 3 failed
VERIFICATION:- SUCCESSFUL
Verification Time: 43.003605s
To what extent is Kani controlling the code being generated here? I note that, as of https://github.com/diffblue/cbmc/pull/6647, CBMC has support for saturating addition and subtraction, and adding support for multiplication would not be that hard. But that only is of use if Kani would make use of it. Looking at the GOTO program generated at this time, it seems that saturating_mul
is implemented in terms of checked_mul
in Rust libraries. And that is where the problems emerge from: multiplication is fundamentally hard, and the above code does not currently generate the same expression twice, at which point caching would pick this up. Instead, multiple function calls/instantiations are generated, and the back-end doesn't know that these expressions ought to be the same.
To what extent is Kani controlling the code being generated here?
Not much: the only thing Kani has control over is the codegen for the mul_with_overflow
intrinsic (which is called by checked_mul
). Kani's implementation of the intrinsic uses:
- A normal multiplication operation
- An overflow multiplication operation (
overflow-*
).
https://github.com/model-checking/kani/blob/ff033adf39c2359fc9831e877e721124948560fc/cprover_bindings/src/goto_program/expr.rs#L1318
multiplication is fundamentally hard
I know multiplication is hard, but I was hoping that the repeated expression would be caught by some simplification step.
CBMC has support for saturating addition and subtraction, and adding support for multiplication would not be that hard. But that only is of use if Kani would make use of it.
It won't be straightforward for Kani to use it because unlike saturating_add
and saturating_sub
which directly call an intrinsic with the same name, saturating_mul
is implemented in terms of checked_mul
as you noted.
We should also attempt to replace Kani's implementation of the mul_with_overflow
intrinsic with overflow_result_exprt
that was added in https://github.com/diffblue/cbmc/pull/6903 (as you suggested in https://github.com/diffblue/cbmc/issues/6607#issuecomment-1146386176).