Non-termination of CBMC on use of size_t as type of a quantified variable

[rod-chapman]

CBMC version: 6.0.1 (with candidate fix for #8329 applied)
Operating system: macOS
Exact command line resulting in the issue: "make"
What behaviour did you expect: successful termination
What happened instead: Non-termination

I have found a better test case that illustrates this issue. Possibly related to #8326.

Test case: https://github.com/rod-chapman/cbmc-examples/tree/main/issues/8365

Note the difference in the two versions of the inner loop invariant. When I use "int" for the type of the quantified variable, all is well and the verification terminates with 1 unproven VC.

When I use "size_t" as the type of the quantified variable, I get:

cbmc --bounds-check --pointer-check --memory-cleanup-check --div-by-zero-check --signed-overflow-check --unsigned-overflow-check --pointer-overflow-check --conversion-check --undefined-shift-check --enum-range-check --pointer-primitive-check --verbosity 6 --smt2 main_contracts.goto
CBMC version 6.0.1 (cbmc-5.34.0-4388-g73ef5ef424) 64-bit arm64 macos
Reading GOTO program from file main_contracts.goto
Generating GOTO Program
Adding CPROVER library (arm64)
Removal of function pointers and virtual functions
Generic Property Instrumentation
Starting Bounded Model Checking
Passing problem to SMT2 QF_AUFBV using Z3
converting SSA
Running SMT2 QF_AUFBV using Z3
Running SMT2 QF_AUFBV using Z3
Running SMT2 QF_AUFBV using Z3
Running SMT2 QF_AUFBV using Z3
Running SMT2 QF_AUFBV using Z3
Running SMT2 QF_AUFBV using Z3
Running SMT2 QF_AUFBV using Z3
Running SMT2 QF_AUFBV using Z3
... and so on...

Hopefully this will yield additional insight into what's going wrong.

[rod-chapman]

I also tried it with
"unsigned long" (which is what size_t really is...) - does not terminate as above.
"unsigned int" - DOES terminate OK.

[rod-chapman]

Michael T and I have been looking at this today. See attached.
"z3_ok_smt2.txt" is the result of running "cbmc --smt2 --outfile z3_ok.smt2 --z3 --stop-on-fail" with "unsigned int" for the quantified variable. This works OK, and produces "sat" (owing to the later assertion), and a counter-example successfully. The actual output of z3 is in z3_ok.txt

If I change "unsigned int" to "unsigned long", then I get "z3_fails_smt2.txt" and "z3_fails.txt" as the output of z3. It still says "sat", but the following counterexample is different (it contains quantified expressions for a start) which (it appears) causes cbmc to iterate forever.
z3_fails_smt2.txt
z3_fails.txt
z3_ok_smt2.txt
z3_ok.txt

[tautschnig]

Digging further into this I am wondering whether all we need to do is expand on 40bd2b5 to make sure we introduce named functions for all quantified expressions (excluding ones that are nested in another quantified expression).

[tautschnig]

With a fix for #8329 and recent Z3 versions (cf. #7767) the problem that remains is Z3 returning results like

((B1502 (forall ((|main::tmp_cc$0!0@1#0| (_ BitVec 64)))
  (let ((a!1 (or (and (not (bvule #x000000000000000c |main::tmp_cc$0!0@1#0|))
                      (bvule #x000000000000000b |main::tmp_cc$0!0@1#0|)
[...]

Manually adding (assert B1502) will force Z3 to return ((B1502 true)) instead, and adding (assert (not B1502)) makes the formula unsat. It is not clear to me whether we are running into a limitation of Z3 or aren't using Z3 correctly at this point.

[tautschnig]

I just built Bitwuzla 0.5.0 from source and, with the proposed fix from #8329, cbmc --bitwuzla main_contracts.goto completes in about 1 second (reporting 1 failed property, for which I can also get a counterexample).

[rod-chapman]

I might suggest a two phase approach

1. Let's stop CBMC from falling into a infinite loop for this case. Spot the mal-formed response coming back from Z3, issue a sensible, readable error message (that is really easy to spot on command-line, from within CBMC-starter-kit, or from a CI runner log), and stop CBMC.
2. Then... work out why the Z3 response is problematic and fix CBMC to accept it. Is it only recent versions of Z3 that exhibit this behaviour of producing quantified expressions in response to a sat result followed by a get-value command? When did it change?

[rod-chapman]

I have been bi-secting on Z3 versions to see when this change appeared. I find:

% z3_4.11.2 z3_fails.smt2 | grep B1589
((B1589 true))

BUT

% z3_4.12.0 z3_fails.smt2 | grep B1589
((B1589 (forall ((|main::tmp_cc$0!0@1#0| (_ BitVec 64)))

So... something changed between Z3 4.11.2 and 4.12.0.

[rod-chapman]

More info... If I run cbmc with z3 4.11.2 on the test case above, then the run fails with:

Running SMT2 QF_AUFBV using Z3
SMT2 solver returned error message:
	"line 11848 column 17: invalid get-value term, term must be ground and must not contain quantifiers"

Hmmm...

[rod-chapman]

Running Z3 4.11.2 by hand on z3_fails.smt2 attached yields actually produces 6 such errors:

% z3_4.11.2 z3_fails.smt2 | grep error
(error "line 11637 column 17: invalid get-value term, term must be ground and must not contain quantifiers")
(error "line 11655 column 17: invalid get-value term, term must be ground and must not contain quantifiers")
(error "line 11674 column 17: invalid get-value term, term must be ground and must not contain quantifiers")
(error "line 11678 column 17: invalid get-value term, term must be ground and must not contain quantifiers")
(error "line 13646 column 42: invalid get-value term, term must be ground and must not contain quantifiers")
(error "line 13648 column 42: invalid get-value term, term must be ground and must not contain quantifiers")

[rod-chapman]

I am still blocked on this.
With Z3 4.11.2, the "get-value" command fails with "invalid get-value term, term must be ground and must not contain quantifiers"
With Z3 >=4.12.x, the "get-value" works, but produces a quantified value which CBMC fails to parse and drops into an infinite loop.

[tautschnig]

The fix that I'd like to propose for this issue (and also #8326, #8301) has two parts:

1. Evaluate whether we should make Bitwuzla the default choice as SMT2 solver; or perhaps it should be the recommended choice when quantifiers are involved.
2. Make sure we fail with an error message when Z3 returns a forall expression as model for some variable.

[rod-chapman]

I like this plan. I assume the failure any affects the "get-value" that follows a "sat" result from Z3, so will only manifest itself as CBCM being unable to generate a counter-example? That's OK, since I will obviously try to fix the failed proof anyway.
Is that right?

[tautschnig]

Yes, it should indeed only affect those cases where some property does not hold.

[rod-chapman]

OK... then the graceful thing to do is to report a proof FAILURE and "sorry.. no counterexample could be found".