Use CBMC's arithmetic operators that return both the result and whether it overflowed

[zhassan-aws]

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.

[danielsn]

Give C or pseudocode example

[zhassan-aws]

Done.

[danielsn]

Why do this here? I'd expect it to happen in arithmetic_overflow_result_type

[zhassan-aws]

I was hoping to do it in arithmetic_overflow_result_type, but it doesn't have access to the Gotoc context since it's in the cprover_bindings crate.

[danielsn]

maybe make a helper function

let res_type = self.codegen_arithmetic_overflow_result_type(op_type.clone()); // does the ensure
let struct_tag = res_type.tag().unwrap()

[zhassan-aws]

Makes sense. Done.

[danielsn]

Were you going to split this off?

[zhassan-aws]

This case wasn't difficult to handle. The other cases, e.g. in count_in_bytes, codegen_ptr_offset_from_expr, and codegen_ptr_offset_from_unsigned are a bit more challenging, and I'm splitting those off to a later PR.

[tedinski]

I really hate these macros, but lgtm