Low performance verification caused by conditional jump

[adpaco-aws]

While writing a test case for the ctpop intrinsic, I wrote something similar to this code:

fn my_ctpop_u32(x: u32) -> u32 {
    let mut count = 0;
    let num_bits = u32::BITS;
    for i in 0..num_bits {
        // Get value at index `i`
        let bitmask = 1 << i;
        let bit = x & bitmask;
        if bit != 0 {
            count += 1;
        }
        // assert!(count >= 0);
    }
    count
}

#[kani::proof]
fn main() {
    let var: u32 = kani::any();
    assert!(my_ctpop_u32(var) == ctpop(var));
}

Running kani on this example (without arguments) does not terminate (at least for a few minutes). We can pass --unwind up to 8 or so in order to get a result, but it will fail the unwinding assertion unless we pass 33 (which gets us back to non-termination).

What is surprising about this example is that adding back the assertion that is commented out will allow CBMC to successfully verify the code in a few seconds. Apparently, this is because the conditional jump in the goto program following from the if bit != 0 { ... } complicates the unwinding and verification of this example.

@tautschnig proposed using the --ensure-one-backedge-per-target option from goto-instrument in order to fix this, but it is not clear if this transformation preserves soundness in some cases (see the regression failure in #900).