Checking result of repeated operation takes long

[zhassan-aws]

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

[tautschnig]

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.

[zhassan-aws]

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:

1. A normal multiplication operation
2. 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.

[zhassan-aws]

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).