Harness with concrete values seems stuck

[adpaco-aws]

I tried this code:

#[derive(Debug, PartialEq, Eq, Hash, Clone)]
#[cfg_attr(kani, derive(kani::Arbitrary))]
pub enum BinaryOp {
    Eq,
    LessEq,
    Add,
}

#[derive(Debug, PartialEq, Eq, Hash, Clone)]
#[cfg_attr(kani, derive(kani::Arbitrary))]
pub enum Expr {
    Int(i32),
    Bool(bool),
    If {
        test_expr: Box<Expr>,
        then_expr: Box<Expr>,
        else_expr: Box<Expr>,
    },
    BinaryApp {
        op: BinaryOp,
        arg1: Box<Expr>,
        arg2: Box<Expr>,
    },
}

// Code from other types (including `Calculator`) not included here
// See attachment for the full example

#[kani::proof]
#[kani::unwind(2)]
fn test_calc_kani() {
    let calc = Calculator::new();
    assert_eq!(
        calc.calculate(Expr::BinaryApp {
            op: BinaryOp::Add,
            arg1: Box::new(Expr::Int(3)),
            arg2: Box::new(Expr::Int(4))
        }),
        Ok(Value::Int(7))
    );
}

Full example here:
calculator.rs.txt

using the following command line invocation:

kani calculator.rs

with Kani version: 0.33.0

I expected to see this happen:
SUCCESSFUL verification after a few seconds.

Instead, this happened:
Kani seems to be stuck after the runtime postprocess step...

Not unwinding recursion Calculator::calculate iteration 3
Not unwinding recursion Calculator::calculate iteration 3
aborting path on assume(false) at file /home/ubuntu/calculator/src/main.rs line 39 column 15 function Calculator::calculate thread 0
aborting path on assume(false) at file /home/ubuntu/calculator/src/main.rs line 26 column 17 function <Value as std::cmp::PartialEq>::eq thread 0
aborting path on assume(false) at file /home/ubuntu/calculator/src/main.rs line 39 column 15 function Calculator::calculate thread 0
aborting path on assume(false) at file /home/ubuntu/calculator/src/main.rs line 26 column 17 function <Value as std::cmp::PartialEq>::eq thread 0
aborting path on assume(false) at file /github/home/.rustup/toolchains/nightly-2023-07-01-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/result.rs line 498 column 16 function <std::result::Result<Value, ()> as std::cmp::PartialEq>::eq thread 0
Runtime Symex: 5.40479s
size of program expression: 114659 steps
slicing removed 77280 assignments
Generated 7733 VCC(s), 5542 remaining after simplification
Runtime Postprocess Equation: 0.14615s
Passing problem to propositional reduction
converting SSA
Runtime Convert SSA: 1.18332s
Running propositional reduction
Post-processing
Runtime Post-process: 17.4075s

What's interesting about this problem is that, if we remove the If { ... } variant in the Expr enum (and the code that matches on that variant in calculate), then it verifies in less than a second which is what we'd expect with concrete values.

SUMMARY:
 ** 0 of 149 failed

VERIFICATION:- SUCCESSFUL
Verification Time: 0.26569963s

Complete - 1 successfully verified harnesses, 0 failures, 1 total.

I don't think this is a duplicate of #1982 because they're different (slowdown in this case is >10x), but root cause may be related.

[zhassan-aws]

This succeeds in ~20 seconds with cadical:

SUMMARY:
 ** 0 of 187 failed (3 unreachable)

VERIFICATION:- SUCCESSFUL
Verification Time: 19.53067s

Complete - 1 successfully verified harnesses, 0 failures, 1 total.

[adpaco-aws]

Thanks for the data, @zhassan-aws ! However, since we're passing in concrete values, I'd expect this example to verify in less than one second, regardless of the solver. Maybe we're missing a case for constant propagation?

[tautschnig]

Fixed in diffblue/cbmc#7933. With that change, verification time now is reported to be 0.35 seconds.

[adpaco-aws]

That's great news! Thanks @tautschnig 😄

[tautschnig]

Fix is now merged and should be part of the next CBMC release.

[tautschnig]

Fix was included with #2821.