Description of changes:

Kani's current implementation of the arithmetic with overflow operators, e.g. std::intrinsics::mul_with_overflow, involves performing the arithmetic operation twice: once to get the result, and another to determine whether it overflowed. CBMC recently introduced a new operation in diffblue/cbmc#6903 that performs a single arithmetic operation that returns a struct with two fields: the result and whether it overflowed. This PR switches the implementation of those intrinsics to the more efficient CBMC operation.

Resolved issues:

Resolves #ISSUE-NUMBER

Call-outs:

I kept the old implementations around (e.g. cprover_bindings::goto_program::expr::Expr::mul_overflow) because I haven't replaced all the code that uses them. The remaining usages, e.g. by kani_compiler::codegen_cprover_gotoc::codegen::intrinsic::GotocCtx::count_in_bytes require a bit more refactoring that I'll leave to a future PR.

Testing:

• How is this change tested? Evaluated performance on a few tests:

#[kani::proof]
fn check_repeat() {
    let x: u64 = kani::any();
    let y: u64 = kani::any();
    if let Some(result) = x.checked_mul(y) {
        assert!(x == 0 || y == 0 || result != 0);
    }
}

Before: 0.765
After: 0.0788
Speedup: 9.7

#[kani::proof]
fn check_repeat() {
    let x: u64 = kani::any();
    let y: u64 = kani::any();
    kani::assume(x == 0 || y == 0);
    let result = x.checked_mul(y).unwrap();
    assert_eq!(result, 0);
}

Before: 0.090
After: 0.0689
Speedup: 1.3

#[kani::proof]
fn check_repeat() {
    let x: u64 = u64::MAX / 2;
    let y: u64 = kani::any();
    kani::assume(y > 2);
    let result = x.saturating_mul(y);
    assert_eq!(result, u64::MAX);
}

Before: 0.074
After: 0.060
Speedup: 1.2

• Is this a refactor change? No

Checklist

• Each commit message has a non-empty body, explaining why the change was made
• Methods or procedures are documented
• Regression or unit tests are included, or existing tests cover the modified code
• My PR is restricted to a single feature or bugfix

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.