Performance of proof of 1 function

[rod-chapman]

Using CBMC 5.84 on macOS (Apple MacBook Pro with M1 Pro CPU)

Using the same code that I posted in #7747 CBMC 5.84 using cadical as the back-end solver, completes proof in 500 seconds (over 8 minutes), using a single CPU Core.

In contract, dafny 4 completes proof of an equivalent function in 2 seconds. SPARK Pro also does it in about 2 seconds.

So... CMBC is 250 times slower for a simple 10-line function that contains a single loop.

[tautschnig]

Almost all of those 500 seconds are spent in the SAT solver. Given we need to perform bit-precise reasoning about multiplication (do the others do the same?) this is not too surprising. Nevertheless we ought to invest in our arithmetic refinement so that we don't always have to do multiplication in full precision.

[rod-chapman]

Well... SPARK (and I assume Dafny) are doing this verification in SMT world, so using whatever integer arithmetic theory is supported. SPARK does NOT expand such things down to the bit level - why would it?

[rod-chapman]

Yeah... for example, the SMT file for the verification of the second conjunct of the postcondition generated by SPARK concludes:

(assert
  (not (< x (* (+ p__sqrt_binary__result 1) (+ p__sqrt_binary__result 1)))))

(check-sat)

leaving the "+", "*" and "<" operators as-is. That's what you get for CVC4.

[remi-delmas-3000]

CBMC's SMT back-end also targets the QF_AUFBV theory so the problem would remain there too. @TGWDB is there any way this could be addressed in the new incremental SMT backend by adding a translation mode that models integers mod 2^n using mathematical integers ?

[TGWDB]

CBMC's SMT back-end also targets the QF_AUFBV theory so the problem would remain there too. @TGWDB is there any way this could be addressed in the new incremental SMT backend by adding a translation mode that models integers mod 2^n using mathematical integers ?

The target theory is not strictly enforced in CBMC for the (old) --z3 and --cvc?, however integers are usually converted to bitvectors.

The new SMT does not (yet) support integers as SMT2 integer theory yet.

[martin-cs]

@remi-delmas-3000 I would suggest against the bit-vectors -> integers mod 2^n translation. You are reducing from a theory that is decideable (NP for fixed bit-width) and gets a lot of attention to one that is undecideable and gets relatively little. Why3 did this and I have see over the last decade the work needed in CVC4 / cvc5 to make this work reasonably. I still think that they are restricting their performance by doing this. There are things that could be done to make the bv-to-int route viable but I'd probably need a couple of people who are keen on doing a PhD on Diophantine equations.

If you want to experiment cvc5 has --solve-bv-as-int and --solve-int-as-bv flags but they aren't on by default because they only seem to help in some restricted cases (such as extensive use of mixed terms).

I think the current state-of-the-art for reasoning about general problems including non-linear bit-vectors is to keep them as BV and use Bitwuzla or cvc5. Do let me know if you find different.