Formatting an i8 takes a long time after nightly-2023-06-20 upgrade

[celinval]

I tried this code:

// fmt.rs
#[kani::proof]
fn fmt_i8() {
    let num: i8 = kani::any();
    let s = format!("{num}");
    assert!(s.len() <= 4);
}

using the following command line invocation:

kani fmt.rs

with Kani version: #2551

I expected to see this happen: Verification succeeds in a matter of seconds (before upgrade this harness used to take 6s)

Instead, this happened: Verification took about 10 minutes.

[celinval]

Comparing Kani before and after the upgrade. I noticed the following:

1. There was no significant changes to the reachability analysis. The number of intrinsics decreased by 1/3 due to the new lowering logic.

MIR Reachability Results: Before Upgrade

====== Reachability Analysis Result =======
Total # items: 693
Total # statements: 5788
Total # expressions: 2832

Reachable Items:
  - function: 691
  - static item: 2

Statements:
  - Assign: 2832
  - Call: 1343
  - Return: 669
  - SwitchInt: 399
  - Goto: 302
  - Assert: 128
  - Unreachable: 56
  - Intrinsic: 32
  - Drop: 27

Expressions:
  - Use: 1083
  - Aggregate: 375
  - BinaryOp: 309
  - Cast: 304
  - Ref: 259
  - UnaryOp: 117
  - Discriminant: 105
  - CheckedBinaryOp: 78
  - CopyForDeref: 74
  - Len: 67
  - AddressOf: 46
  - NullaryOp: 10
  - Repeat: 5

-------------------------------------------

MIR Reachability Results: After Upgrade

====== Reachability Analysis Result =======
Total # items: 624
Total # statements: 5268
Total # expressions: 2662

Reachable Items:
  - function: 622
  - static item: 2

Statements:
  - Assign: 2662
  - Call: 1142
  - Return: 600
  - SwitchInt: 376
  - Goto: 278
  - Assert: 118
  - Unreachable: 56
  - Drop: 25
  - Intrinsic: 11

Expressions:
  - Use: 1027
  - Aggregate: 347
  - BinaryOp: 309
  - Cast: 283
  - Ref: 245
  - Discriminant: 103
  - UnaryOp: 92
  - CheckedBinaryOp: 76
  - CopyForDeref: 74
  - Len: 67
  - AddressOf: 25
  - NullaryOp: 9
  - Repeat: 5

-------------------------------------------

2. The size of the goto model also didn't change much. With --show-goto-functions, the model went from 24367 to 24168 lines and the number of loops decreased slightly, from 32 loops to 29 loops after, comparing before and after upgrade.

3. The Symbolic Engine seems to have explored a much higher number of program expressions, which generated a much bigger VCC and consequently a much bigger formula.

CBMC Stats: Before Upgrade

Runtime Symex: 1.4556s
size of program expression: 40831 steps
slicing removed 27725 assignments
Generated 2502 VCC(s), 1127 remaining after simplification
Runtime Postprocess Equation: 0.036371s
Passing problem to propositional reduction
converting SSA
Runtime Convert SSA: 0.233992s
Running propositional reduction
Post-processing
Runtime Post-process: 0.0563905s
Solving with MiniSAT 2.2.1 with simplifier
200496 variables, 528343 clauses

CBMC Stats: After Upgrade

Runtime Symex: 11.7504s
size of program expression: 321064 steps
slicing removed 248551 assignments
Generated 14256 VCC(s), 5967 remaining after simplification
Runtime Postprocess Equation: 0.253811s
Passing problem to propositional reduction
converting SSA
Runtime Convert SSA: 1.44413s
Running propositional reduction
Post-processing
Runtime Post-process: 2.89245s
simplifier
1111973 variables, 7270933 clauses
SAT checker: instance is SATISFIABLE

[celinval]

Looking at the generated goto-program for the function fmt_u64 there seems to be two obvious difference:

1. New division by 0 checks. But in this case the expression is constant, so we could prune them.
2. The order of the basic blocks have changed.

[adpaco-aws]

New division by 0 checks. But in this case the expression is constant, so we could prune them.

Could we replace the "division-by-zero" checks we currently emit (from CBMC) by these ones? It may be worth considering if the ones coming from Rust include locations (missing from many CBMC checks), but I'm also not sure how they look like.

The order of the basic blocks have changed.

Bad news.

[celinval]

New division by 0 checks. But in this case the expression is constant, so we could prune them.

Could we replace the "division-by-zero" checks we currently emit (from CBMC) by these ones? It may be worth considering if the ones coming from Rust include locations (missing from many CBMC checks), but I'm also not sure how they look like.

Yes. We can definitely get rid of CBMC ones.

The order of the basic blocks have changed.

Bad news.

Yeah, my guess is that this is the root cause of the performance issue. On the bright side, if that is the issue, we can create our own ordering algorithm and make CBMC happy again.

[celinval]

Unfortunately, fixing the basic block order and removing all the new overflow checks were not enough to fix this regression. :(