Incorrect (hard-coded) logic for SMT backend

[SaswatPadhi]

CBMC version: develop

Operating system: Mac OS 10.15.7

Test case:

#include <assert.h>

void main()
{
  int i;
  __CPROVER_assume(i % 2 == 0);
  assert(__CPROVER_exists { int j ; i == j + j });
}

Exact command line resulting in the issue:

cbmc --z3 test.c or cbmc --cvc4 test.c

What behaviour did you expect:

CBMC would verify the assertion and report success.

What happened instead:

$ cbmc --z3 test.c | tail
SMT2 solver returned error message:
        "line 88 column 17: model is not available"
Running SMT2 QF_AUFBV using Z3
Runtime Solver: 1.69421s
Runtime decision procedure: 1.69455s

** Results:
test.c function main
[main.assertion.1] line 7 assertion __CPROVER_exists { int j ; i == j + j }: ERROR

** 0 of 1 failed (1 iterations)
VERIFICATION ERROR

$ cbmc --cvc4 test.c | tail
SMT2 solver returned error message:
        "The logic was specified as QF_AUFBV, which doesn't include THEORY_QUANTIFIERS, but got a preprocessing-time fact for that theory.
The fact:
(forall ((|main::1::1::j!0#0| (_ BitVec 32))) (not (= (concat ((_ extract 30 0) |main::1::1::j!0#0|) (_ bv0 1)) |main::1::i!0@1#1|)) )"
Running SMT2 QF_AUFBV using CVC4
Runtime Solver: 0.0263352s
Runtime decision procedure: 0.0265899s

** Results:
main.c function main
[main.assertion.1] line 7 assertion __CPROVER_exists { int j ; i == j + j }: ERROR

** 0 of 1 failed (1 iterations)
VERIFICATION ERROR

Additional context:

CBMC also fails to verify this program with the SAT backend, but a similar issue has already been reported in #5395.

[SaswatPadhi]

In my experience, just (set-logic ALL) works well with most solvers today. This is part of SMTLIB standard now (so is valid, syntactically) and might be the simplest fix.
But, what does everyone else think? cc: @kroening, @martin-cs, @tautschnig

If performance hit is a concern, I can create a draft PR once we have Z3 running on the CI [#5949] and check how long the smt-backend tests take.

[SaswatPadhi]

cc: @mww-aws

Also adding Mike to this discussion.

[martin-cs]

• Enabling the quantifier engine in solvers can result in some answers being given as unknown rather than sat so is best avoided where possible.
• I have not seen this happen with strings but given the lack of useful decideable fragments, I can believe it might happen.
• The wider question, to me, is "should we maintain different translations for different solver features". If we are doing that then, setting the logic according to those should be trivial.
• I think we probably want to keep that capability for things like strings, quantifiers and maybe datatypes and floating-point.

[TGWDB]

I've had a quick look into this and am updating with some preliminary information (and welcome to guidance/feedback if there is anything you can recommend).

A look at the documentation for SMT2 logics here indicates that there is no SMT2 theory that supports quantifiers over bitvectors. This is unfortunate and may cause some issues, but more details below on what happens.

I tried modifying cbmc to use ALL instead of QF_AUFBV as the theory (as suggested by @SaswatPadhi above). This modified did pass all regression and unit tests (performance not checked). However, this appears to have some issues with the example.

I took the example (from above):

#include <assert.h>

void main()
{
  int i;
  __CPROVER_assume(i % 2 == 0);
  assert(__CPROVER_exists { int j ; i == j + j });
}

and tried running it in cbmc with both ALL and QF_AUFBV theories with both --z3 and --cvc4 options. Results are as follows (lots of boring details cut).

cbmc with QF_AUFBV and --z3

tgw@DB0907:~/github/testing/Issue5977$ /home/tgw/github/master-cbmc-build/bin/cbmc --z3 test.c
CBMC version 5.32.1 (cbmc-5.32.1-2-g437675a5b) 64-bit x86_64 linux
...
Passing problem to SMT2 QF_AUFBV using Z3
converting SSA
Runtime Convert SSA: 0.0002051s
Running SMT2 QF_AUFBV using Z3
SMT2 solver returned error message:
        "line 82 column 17: model is not available"
Runtime Solver: 1.24599s
Runtime decision procedure: 1.24637s

** Results:
test.c function main
[main.assertion.1] line 7 assertion __CPROVER_exists { int j ; i == j + j }: ERROR

** 0 of 1 failed (1 iterations)
VERIFICATION ERROR

cbmc with QF_AUFBV and --cvc4

tgw@DB0907:~/github/testing/Issue5977$ /home/tgw/github/master-cbmc-build/bin/cbmc --cvc4 test.c
CBMC version 5.32.1 (cbmc-5.32.1-2-g437675a5b) 64-bit x86_64 linux
...
Passing problem to SMT2 QF_AUFBV using CVC4
converting SSA
Runtime Convert SSA: 0.0001308s
Running SMT2 QF_AUFBV using CVC4
Runtime Solver: 0.0262526s
Runtime decision procedure: 0.0272123s

** Results:
test.c function main
[main.assertion.1] line 7 assertion __CPROVER_exists { int j ; i == j + j }: ERROR

** 0 of 1 failed (1 iterations)
VERIFICATION ERROR

cbmc with ALL and --z3

tgw@DB0907:~/github/testing/Issue5977$ cbmc --z3 test.c
CBMC version 5.32.1 (cbmc-5.32.1-105-gf9be0ebfb-dirty) 64-bit x86_64 linux
...
Passing problem to SMT2 ALL using Z3
converting SSA
Runtime Convert SSA: 9.89e-05s
Running SMT2 ALL using Z3
SMT2 solver returned error message:
        "line 82 column 17: model is not available"
Runtime Solver: 1.19301s
Runtime decision procedure: 1.19318s

** Results:
test.c function main
[main.assertion.1] line 7 assertion __CPROVER_exists { int j ; i == j + j }: ERROR

** 0 of 1 failed (1 iterations)
VERIFICATION ERROR

cbmc with ALL and --cvc4

tgw@DB0907:~/github/testing/Issue5977$ cbmc --cvc4 test.c
CBMC version 5.32.1 (cbmc-5.32.1-105-gf9be0ebfb-dirty) 64-bit x86_64 linux
...
Passing problem to SMT2 ALL using CVC4
converting SSA
Runtime Convert SSA: 9.39e-05s
Running SMT2 ALL using CVC4
Runtime Solver: 0.0267565s
Runtime decision procedure: 0.0269266s

** Results:
test.c function main
[main.assertion.1] line 7 assertion __CPROVER_exists { int j ; i == j + j }: ERROR

** 0 of 1 failed (1 iterations)
VERIFICATION ERROR

Summary

All report a VERIFICATION ERROR with the --z3 ones reporting the error is with obtaining the model. The reporting of the error trying to obtain the model is somewhat unclear but may be related to some other issues, e.g. #6005 . This investigation will not explore this detail here (watch other PRs for updates on tracking errors in solvers in cbmc).

Playing with z3 Directly

Next I tried generating the SMT2 files directly from cbmc from both versions (i.e. using both QF_AUFBV and ALL. Details below (again with lots of excess output removed).

tgw@DB0907:~/github/testing/Issue5977$ /home/tgw/github/master-cbmc-build/bin/cbmc test.c --smt2 --outfile QF_AUFBV.s
mt2
CBMC version 5.32.1 (cbmc-5.32.1-2-g437675a5b) 64-bit x86_64 linux
...
tgw@DB0907:~/github/testing/Issue5977$ cbmc test.c --smt2 --outfile ALL.smt2
CBMC version 5.32.1 (cbmc-5.32.1-105-gf9be0ebfb-dirty) 64-bit x86_64 linux
...
tgw@DB0907:~/github/testing/Issue5977$ diff QF_AUFBV.smt2 ALL.smt2
2c2
< (set-info :source "Generated by CBMC 5.32.1 (cbmc-5.32.1-2-g437675a5b)")
---
> (set-info :source "Generated by CBMC 5.32.1 (cbmc-5.32.1-105-gf9be0ebfb-dirty)")
4c4
< (set-logic QF_AUFBV)
---
> (set-logic ALL)

Now these files can be tested in z3 without cbmc potentially interfering and causing problems.

First the results of running the QF_AUFBV.smt2 file in z3 (lots of output removed):

tgw@DB0907:~/github/testing/Issue5977$ z3 -smt2 QF_AUFBV.smt2
(error "line 53 column 73: logic does not support quantifiers")
(error "line 59 column 73: logic does not support quantifiers")
(error "line 65 column 82: logic does not support quantifiers")
(error "line 81 column 141: logic does not support quantifiers")
sat
((|B0| true))
...
((|main::1::i!0@1#1| #x00000000))

Observe that here z3 reports errors on lines with quantifies (not a surprise since QF_AUFBV cannot support them. A brief experiment (by deleting the lines that cause errors in a copy of the smt2 file and running the modified copy through z3) appears to show that these lines are simply ignored and z3 produces results without those constraints.

Second, running the ALL.smt2 file yields the following output (again, many details removed):

tgw@DB0907:~/github/testing/Issue5977$ z3 -smt2 ALL.smt2
unknown
(error "line 91 column 17: model is not available")
...

Here (as @martin-cs said might happen) the solver produces unknown instead of sat or unsat. It appears that z3 did NOT have a problem with the input now, but was unable to provide a solution (either sat or unsat). When the result is unknown then there is no model to obtain and here cbmc appears to have failed to detect the unexpected result (and assumed there was a model available).

Investigatory Conclusions (so far)

At the moment when quantifiers are passed in to z3 they cause errors and these error lines are ignored in the sat/unsat calculation. This can yield false results and is currently ignored by cbmc (i.e. cbmc ignores errors and simply uses the false result from z3).

This message to keep everyone up to date, I'm looking further into this at the moment.

[martin-cs]

( Note that the list of logics on the website is somewhat out of date and the list of benchmark collections http://smtlib.cs.uiowa.edu/benchmarks.shtml is probably a better view of the state-of-the-art, although most people have adopted the 'automata' approach to the naming of logics and it will all change in a month or so with the release of SMT-LIB 3.0. ABVFP is probably what you want if you aren't using QF_ABVFP. HTH. )

[TGWDB]

Sadly ABVFP is not the right answer (details below), but I'll try some others and update.

Some data from trying ABVFP with excess cut:

tgw@DB0907:~/github/testing/Issue5977$ cbmc test.c --smt2 --outfile       ABVFP.smt2
CBMC version 5.32.1 (cbmc-5.32.1-105-gf9be0ebfb-dirty) 64-bit x86_64 linux
...
Runtime decision procedure: 0.0002462s
tgw@DB0907:~/github/testing/Issue5977$ diff QF_AUFBV.smt2 ABVFP.smt2
2c2
< (set-info :source "Generated by CBMC 5.32.1 (cbmc-5.32.1-2-g437675a5b)")
---
> (set-info :source "Generated by CBMC 5.32.1 (cbmc-5.32.1-105-gf9be0ebfb-dirty)")
4c4
< (set-logic QF_AUFBV)
---
> (set-logic ABVFP)
tgw@DB0907:~/github/testing/Issue5977$ z3 -smt2 ABVFP.smt2
unsupported
; ignoring unsupported logic ABVFP line: 4 position: 0
unknown
(error "line 91 column 17: model is not available")

tgw@DB0907:~/github/testing/Issue5977$ cbmc test.c --z3
CBMC version 5.32.1 (cbmc-5.32.1-105-gf9be0ebfb-dirty) 64-bit x86_64 linux
Passing problem to SMT2 ABVFP using Z3
converting SSA
Runtime Convert SSA: 0.0001652s
Running SMT2 ABVFP using Z3
SMT2 solver returned error message:
        "line 82 column 17: model is not available"
Runtime Solver: 1.09435s
Runtime decision procedure: 1.09468s

** Results:
test.c function main
[main.assertion.1] line 7 assertion __CPROVER_exists { int j ; i == j + j }: ERROR

** 0 of 1 failed (1 iterations)
VERIFICATION ERROR

tgw@DB0907:~/github/testing/Issue5977$ cbmc test.c --cvc4
CBMC version 5.32.1 (cbmc-5.32.1-105-gf9be0ebfb-dirty) 64-bit x86_64 linux
Passing problem to SMT2 ABVFP using CVC4
converting SSA
Runtime Convert SSA: 0.0001765s
Running SMT2 ABVFP using CVC4
Runtime Solver: 0.0270365s
Runtime decision procedure: 0.0273203s

** Results:
test.c function main
[main.assertion.1] line 7 assertion __CPROVER_exists { int j ; i == j + j }: ERROR

** 0 of 1 failed (1 iterations)
VERIFICATION ERROR

[TGWDB]

Some more updates for possible logics to try with z3. I checked the list of logics from the benchmarks and tried all the ones the had BV in them (and not QF):

tgw@DB0907:~/github/testing/Issue5977$ z3 -smt2 -in
(set-logic AUFBVDTLIA)
unsupported
; ignoring unsupported logic AUFBVDTLIA line: 1 position: 1
(set-logic BVFP)
unsupported
; ignoring unsupported logic BVFP line: 2 position: 0
(set-logic UFBV)
(exit)

So of the ones listed on the website only UFBV appeared possible to try for z3. Results for testing below.

tgw@DB0907:~/github/testing/Issue5977$ cbmc test.c --smt2 --outfile UFBV.smt2
CBMC version 5.32.1 (cbmc-5.32.1-105-gf9be0ebfb-dirty) 64-bit x86_64 linux
...
tgw@DB0907:~/github/testing/Issue5977$ diff QF_AUFBV.smt2 UFBV.smt2
2c2
< (set-info :source "Generated by CBMC 5.32.1 (cbmc-5.32.1-2-g437675a5b)")
---
> (set-info :source "Generated by CBMC 5.32.1 (cbmc-5.32.1-105-gf9be0ebfb-dirty)")
4c4
< (set-logic QF_AUFBV)
---
> (set-logic UFBV)

Nothing unusual in the above, but when I tried to run it in z3 from the command line I ended up killing it (was probably just going to take a very long time):

tgw@DB0907:~/github/testing/Issue5977$ z3 -smt2 UFBV.smt2
(error "line 52 column 29: unknown sort 'Array'")
(error "line 53 column 47: unknown constant array_of.0")
(error "line 55 column 50: unknown sort 'Array'")
(error "line 58 column 29: unknown sort 'Array'")
(error "line 59 column 47: unknown constant array_of.1")
(error "line 61 column 45: unknown sort 'Array'")
(error "line 64 column 29: unknown sort 'Array'")
(error "line 65 column 47: unknown constant array_of.2")
(error "line 67 column 46: unknown sort 'Array'")
^Cunknown
(error "line 91 column 17: model is not available")

Killed with Ctrl+C.

I tried within cbmc anyway just to test:

tgw@DB0907:~/github/testing/Issue5977$ cbmc test.c --z3
CBMC version 5.32.1 (cbmc-5.32.1-105-gf9be0ebfb-dirty) 64-bit x86_64 linux
Passing problem to SMT2 UFBV using Z3
converting SSA
Runtime Convert SSA: 0.0001676s
Running SMT2 UFBV using Z3
SMT2 solver returned error message:
        "line 82 column 17: model is not available"
Runtime Solver: 1.08201s
Runtime decision procedure: 1.08231s

** Results:
test.c function main
[main.assertion.1] line 7 assertion __CPROVER_exists { int j ; i == j + j }: ERROR

** 0 of 1 failed (1 iterations)
VERIFICATION ERROR

No big time problem or kill, but still failing (kind of expectedly).

I also checked the z3 source code to see what other BV logics might exist for us to check:

tgw@DB0907:~/github$ grep logic z3/src/solver/check_logic.cpp | grep BV
        else if (logic == "QF_ABV") {
        else if (logic == "QF_AUFBV") {
        else if (logic == "QF_UFBV") {
        else if (logic == "QF_BV") {
        else if (logic == "UFBV") {

Seems there are no other possible quantifier free (not QF_) logics in z3 that also support bitvectors (BV).

At least for now, this might be a problem.

[SaswatPadhi]

Thank you so much for taking a look at this PR, and for the detailed logs, @TGWDB!

Regarding,

Here (as @martin-cs said might happen) the solver produces unknown instead of sat or unsat. It appears that z3 did NOT have a problem with the input now, but was unable to provide a solution (either sat or unsat). When the result is unknown then there is no model to obtain and here cbmc appears to have failed to detect the unexpected result (and assumed there was a model available).

Yes indeed. It looks like Z3 is having a hard time with these verification constraints!
(The BV theory with quantifiers is decidable though.)

I extracted the SMT output from CBMC, reduced it to the core verification problem, and changed the logic to ALL:

(set-logic ALL)

; find_symbols
(declare-fun |main::1::i!0@1#1| () (_ BitVec 32))

; set_to true
(assert (= (bvsrem |main::1::i!0@1#1| (_ bv2 32)) (_ bv0 32)))

; set_to false
(assert (not (exists ((|main::1::2::1::j!0#0| (_ BitVec 32))) (= |main::1::i!0@1#1| (bvadd |main::1::2::1::j!0#0| |main::1::2::1::j!0#0|)))))

; convert
(define-fun |B2| () Bool (not false))

; set_to true
(assert |B2|)

(check-sat)

Z3 seems to run forever and I eventually had to killed it. But CVC4 generates an unsat response within milliseconds:
https://cvc4.github.io/app/#temp_0598ba10-2348-4083-9092-763c9969aa84

I noticed the same behavior with BV logic in place of ALL.