Unbounded loop proof causes non-termination and giant SMT file

[rod-chapman]

CBMC version: 6.4.0
Operating system: macOS
Exact command line resulting in the issue: make -f m2
What behaviour did you expect: Successful proof
What happened instead: Non-termination of the cbmc process

See link to example code in following comment.

[rod-chapman]

Reproducible test case here:
https://github.com/rod-chapman/cbmc-examples/tree/main/issues/8505

Background:

Trying to prove type-safety of a simple loop.

Example code main1.c (and makefile m1) show this with unrolling the loop in the function mvm. Run

make -f m1

and the proof terminates successfully in about 1 minute on my laptop.

NOW... look at main2.c. This adds a simple loop invariant to the loop in mvm(), and removed the call to goto-instrument (in Makefile m2) that unrolls the loop. Now run

make -f m2

The cbmc process seems to run forever. The generated SMT2 file reaches about 192 Megabytes before I killed the process.

This is unexepected. I expect proof of loops with invariants to be smaller and faster.

[remi-delmas-3000]

I expect proof of loops with invariants to be smaller and faster.

With --no-array-field-sensitivity --arrays-uf-always --slice-formula the SMT2 files boils down to 1.8M.

Contract instrumentation introduces a number of arrays in the program, and the explosion we're seeing is CBMC built-in array theory solver blowing up by eagerly instantiating read-over-write lemmas (the blowup is quadratic). With these options we tell CBMC to not decompose arrays into their individual cells, to model arrays directly as SMT-lib arrays, and to slice constraints that are not in the cone of influcence of the proof obligations. This defers array reasoning to the SMT solver.

[rod-chapman]

Err... not sure I understand most of that. How was I supposed to know about those options? When is it a good/bad idea to turn these on?

[rod-chapman]

How many other really useful options and switches are there that I don't know about and have no idea what they do?

[rod-chapman]

I tried these switches on all the proofs in mlkem-native. Mixed results - some faster, some slower. All succeed, which is good news. So... what C language idioms and kind of proof typically benefit from these switches? How do I know when to turn them on?

[hanno-becker]

@remi-delmas-3000 Thank you. I can imagine that this strategy can be fruitful. Can you disentangle which option is responsible for what, or point to documentation?

[remi-delmas-3000]

How do I know when to turn them on?

We don't really have a better heuristic than "try that if the array theory blows up" at the moment. The main symptom of array theory blowup is staying stuck on the converting SSA stage (which is when array lemmas get added).

Can you disentangle which option is responsible for what, or point to documentation?

I can't find anything else than cbmc --help. Here's a bunch of related options:

 --max-field-sensitivity-array-size M  maximum size M of arrays for which field
                              sensitivity will be applied to array, the default
                              is 64
 --no-array-field-sensitivity  deactivate field sensitivity for arrays, this is
                              equivalent to setting the maximum field
                              sensitivity size for arrays to 0
 --slice-formula              remove assignments unrelated to property
 --arrays-uf-never            never turn arrays into uninterpreted functions
 --arrays-uf-always           always turn arrays into uninterpreted functions

[remi-delmas-3000]

Another fun observation on this problem:

• bumping the --max-field-sensitivity-array-size to a value large enough for all arrays in the program completely gets rid of them before the CBMC array solver or z3,
• file size goes down to 3.9M,
• z3 is really fast at solving the array-free problem.

So it really goes either way.

** 0 of 91 failed (1 iterations)
VERIFICATION SUCCESSFUL
cbmc --max-field-sensitivity-array-size 8192 --slice-formula --z3 $<
make -f m2  13.00s user 0.50s system 96% cpu 13.996 total

[rod-chapman]

When I'm running everything using the run-cbmc-proofs.py script, I don't see the "converting SSA" message at all... it just sits there doing nothing. I have no idea where the SMT file is, so I can't check it to see how big it is. This all seems a bit trial-and-error to me...