Incorrect (hard-coded) logic for SMT backend

diffblue / cbmc

C Bounded Model Checker

https://diffblue.github.io/cbmc

Other

831 stars 262 forks source link

Incorrect (hard-coded) logic for SMT backend #5977

Closed SaswatPadhi closed 2 years ago

SaswatPadhi commented 3 years ago

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 commented 3 years ago

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 commented 3 years ago

cc: @mww-aws

Also adding Mike to this discussion.

martin-cs commented 3 years ago

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 commented 3 years ago

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 commented 3 years ago

( 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 commented 3 years ago

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 commented 3 years ago

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 commented 3 years ago

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.

TGWDB commented 3 years ago

Further update with better usage of cbmc and z3 based on detail from #6005. Without the --z3 option the --outfile is generic SMT2 and this can cause errors for z3 (details above.)

When the --z3 option is use with --outfile then we can indeed pass the files to z3 afterwards without errors. Also (and perhaps more interestingly) when output files are generated this way the specific logic does not appear in the output file. There are changes to the forall and exists though, details below with some excess cut.

tgw@DB0907:~/github/testing/Issue5977$ /home/tgw/github/master-cbmc-build/bin/cbmc test.c --smt2 --z3 --outfile z3-QF
_AUFBV.smt2
CBMC version 5.32.1 (cbmc-5.32.1-2-g437675a5b) 64-bit x86_64 linux
...

The above generates a new output SMT2 file with the --z3 flag as well, now compare with the old one generated the same way but without the --z3 flag:

tgw@DB0907:~/github/testing/Issue5977$ diff z3-QF_AUFBV.smt2 QF_AUFBV.smt2
2d1
< ; Generated for Z3
4a4
> (set-logic QF_AUFBV)
50a51,53
> ; the following is a substitute for lambda i. x
> (declare-fun array_of.0 () (Array (_ BitVec 64) (_ BitVec 64)))
> (assert (forall ((i (_ BitVec 64))) (= (select array_of.0 i) (_ bv0 64))))
52c55
< (define-fun |__CPROVER_thread_key_dtors!0#1| () (Array (_ BitVec 64) (_ BitVec 64)) ((as const (Array (_ BitVec 64) (_ BitVec 64))) (_ bv0 64)))
---
> (define-fun |__CPROVER_thread_key_dtors!0#1| () (Array (_ BitVec 64) (_ BitVec 64)) array_of.0)
53a57,59
> ; the following is a substitute for lambda i. x
> (declare-fun array_of.1 () (Array (_ BitVec 64) (_ BitVec 64)))
> (assert (forall ((i (_ BitVec 64))) (= (select array_of.1 i) (_ bv0 64))))
55c61
< (define-fun |__CPROVER_thread_keys!0#1| () (Array (_ BitVec 64) (_ BitVec 64)) ((as const (Array (_ BitVec 64) (_ BitVec 64))) (_ bv0 64)))
---
> (define-fun |__CPROVER_thread_keys!0#1| () (Array (_ BitVec 64) (_ BitVec 64)) array_of.1)
56a63,65
> ; the following is a substitute for lambda i. x
> (declare-fun array_of.2 () (Array (_ BitVec 64) (_ BitVec 1)))
> (assert (forall ((i (_ BitVec 64))) (= (select array_of.2 i) (ite false #b1 #b0))))
58c67
< (define-fun |__CPROVER_threads_exited#1| () (Array (_ BitVec 64) Bool) ((as const (Array (_ BitVec 64) Bool)) false))
---
> (define-fun |__CPROVER_threads_exited#1| () (Array (_ BitVec 64) (_ BitVec 1)) array_of.2)

Observe that the (set-logic XXX) command is no longer used, and all the forall and exists are removed.

Now we can run this through z3 from the command line and avoid errors before we try to check the satisfiability:

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

This is similar to what @martin-cs (apologies for the @, let me know if you prefer less of them) predicted, with an unknown result that cbmc may or may not handle well. Also (as noted in #6005 ) if the problem is unsat (or I guess unknown) then cbmc does not need the model and so the errors trying to obtain it should be ignored by cbmc.

Also for the sake of completeness of the data, I tried the same steps with the version of cbmc specifying ALL for the logic. Details below with some excess cut as usual.

tgw@DB0907:~/github/testing/Issue5977$ cbmc test.c --smt2 --z3 --outfile z3-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 ALL.smt2 z3-ALL.smt2
1a2
> ; Generated for Z3
4d4
< (set-logic ALL)
51,53d50
< ; the following is a substitute for lambda i. x
< (declare-fun array_of.0 () (Array (_ BitVec 64) (_ BitVec 64)))
< (assert (forall ((i (_ BitVec 64))) (= (select array_of.0 i) (_ bv0 64))))
55c52
< (define-fun |__CPROVER_thread_key_dtors!0#1| () (Array (_ BitVec 64) (_ BitVec 64)) array_of.0)
---
> (define-fun |__CPROVER_thread_key_dtors!0#1| () (Array (_ BitVec 64) (_ BitVec 64)) ((as const (Array (_ BitVec 64) (_ BitVec 64))) (_ bv0 64)))
57,59d53
< ; the following is a substitute for lambda i. x
< (declare-fun array_of.1 () (Array (_ BitVec 64) (_ BitVec 64)))
< (assert (forall ((i (_ BitVec 64))) (= (select array_of.1 i) (_ bv0 64))))
61c55
< (define-fun |__CPROVER_thread_keys!0#1| () (Array (_ BitVec 64) (_ BitVec 64)) array_of.1)
---
> (define-fun |__CPROVER_thread_keys!0#1| () (Array (_ BitVec 64) (_ BitVec 64)) ((as const (Array (_ BitVec 64) (_ BitVec 64))) (_ bv0 64)))
63,65d56
< ; the following is a substitute for lambda i. x
< (declare-fun array_of.2 () (Array (_ BitVec 64) (_ BitVec 1)))
< (assert (forall ((i (_ BitVec 64))) (= (select array_of.2 i) (ite false #b1 #b0))))
67c58
< (define-fun |__CPROVER_threads_exited#1| () (Array (_ BitVec 64) (_ BitVec 1)) array_of.2)
---
> (define-fun |__CPROVER_threads_exited#1| () (Array (_ BitVec 64) Bool) ((as const (Array (_ BitVec 64) Bool)) false))

Again observe that the SMT2 output file generated with the --z3 option does NOT specify a logic. Indeed, the output file does not differ from the --z3 output file with the QF_AUFBV logic hard-coded:

tgw@DB0907:~/github/testing/Issue5977$ diff z3-QF_AUFBV.smt2 z3-ALL.smt2
3c3
< (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)")

Also as expected the outcome from z3 is unknown, and then no model is avaiable.

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

SaswatPadhi commented 3 years ago

So currently:

Z3 returns unknown, so is unreliable, on BV problems with quantifiers
CVC4 is given QF_AUFBV, so it throws errors.

Would it be possible to specify another logic for CVC4 (and other SMT encodings, including the generic one) to allow quantifiers (at least when they are used in the C program)?

TGWDB commented 3 years ago

Actually cvc4 might be able to handle things fine. More details below.

I tried running cvc4 over the output files that were generated both with and without the --z3 flag and for the logics QF_AUFBV and ALL. Details below with lots of (similar) errors removed (discussion/analysis at the end).

With --z3 flag and logic set to QF_AUFBV in cbmc:

tgw@DB0907:~/github/testing/Issue5977$ cvc4 --lang smt2 z3-QF_AUFBV.smt2
z3-QF_AUFBV.smt2:7.11: No set-logic command was given before this point.
z3-QF_AUFBV.smt2:7.11: CVC4 will make all theories available.
z3-QF_AUFBV.smt2:7.11: Consider setting a stricter logic for (likely) better performance.
z3-QF_AUFBV.smt2:7.11: To suppress this warning in the future use (set-logic ALL).
unsat
(error "Cannot get value unless immediately preceded by SAT/INVALID or UNKNOWN response.")
tgw@DB0907:~/github/testing/Issue5977$

No --z3 flag and with logic set to QF_AUFBV in cbmc:

tgw@DB0907:~/github/testing/Issue5977$ cvc4 --lang smt2 QF_AUFBV.smt2
(error "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 ((i (_ BitVec 64))) (= (select array_of.0 i) (_ bv0 64)) )")

With the --z3 flag with the logic set to ALL in cbmc.

tgw@DB0907:~/github/testing/Issue5977$ cvc4 --lang smt2 z3-ALL.smt2
z3-ALL.smt2:7.11: No set-logic command was given before this point.
z3-ALL.smt2:7.11: CVC4 will make all theories available.
z3-ALL.smt2:7.11: Consider setting a stricter logic for (likely) better performance.
z3-ALL.smt2:7.11: To suppress this warning in the future use (set-logic ALL).
unsat
(error "Cannot get value unless immediately preceded by SAT/INVALID or UNKNOWN response.")

No --z3 flag and logic set to ALL in cbmc.

tgw@DB0907:~/github/testing/Issue5977$ cvc4 --lang smt2 ALL.smt2
unsat
(error "Cannot get value unless immediately preceded by SAT/INVALID or UNKNOWN response.")

Analysis

The above results show that cvc4 can handle most of the SMT2 files generated and produce an unsat result. The only time this fails is when cvc4 was given quantifiers and set to a logic that did not support quantifiers (i.e. QF_AUFBV). Thus, it should be that cvc4 can handle the kinds of problems we want (or at least if we generate the files and then give them to cvc4 there is not an issue).

Return to testing cvc4 within cbmc we have the following errors (as usual, some output removed).

First using cvc4 with the old/default QF_AUFBV logic:

tgw@DB0907:~/github/testing/Issue5977$ /home/tgw/github/master-cbmc-build/bin/cbmc test.c --cvc4
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.0008356s
Running SMT2 QF_AUFBV using CVC4
SMT2 solver returned error message:
        "Parse Error: /tmp/smt2_dec_problem_30983.7Q3mL1:59.132: type mismatch inside array constant term:

  ...st (Array (_ BitVec 64) (_ BitVec 1))) false))
                                       ^

array type:          (Array (_ BitVec 64) (_ BitVec 1))
expected const type: (_ BitVec 1)
computed const type: Bool"
...
VERIFICATION ERROR

and now with the logic set to ALL:

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 ALL using CVC4
converting SSA
Runtime Convert SSA: 0.0004889s
Running SMT2 ALL using CVC4
SMT2 solver returned error message:
        "Parse Error: /tmp/smt2_dec_problem_30974.5nYNml:59.132: type mismatch inside array constant term:

  ...st (Array (_ BitVec 64) (_ BitVec 1))) false))
                                       ^

array type:          (Array (_ BitVec 64) (_ BitVec 1))
expected const type: (_ BitVec 1)
computed const type: Bool"
...
VERIFICATION ERROR

This suggests that maybe cvc4 could handle what we want with the Bool and (_ BitVec) kinds being able to be unified/fixed.

TGWDB commented 3 years ago

The linked PR number 14 above is a provisional fix that appears to work for the examples above. Output from that version of cbmc below:

tgw@DB0907:~/github/testing/Issue5977$ /home/tgw/github/fotis-cbmc-build/bin/cbmc test.c --cvc4
CBMC version 5.32.1 (cbmc-5.6-16052-gb77eeaa42-dirty) 64-bit x86_64 linux
Parsing test.c
Converting
Type-checking test
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Generic Property Instrumentation
Running with 8 object bits, 56 offset bits (default)
Starting Bounded Model Checking
Runtime Symex: 0.0010836s
size of program expression: 41 steps
simple slicing removed 2 assignments
Generated 1 VCC(s), 1 remaining after simplification
Runtime Postprocess Equation: 8.74e-05s
Passing problem to SMT2 ALL using CVC4
converting SSA
Runtime Convert SSA: 0.0002249s
Running SMT2 ALL using CVC4
Runtime Solver: 0.0140547s
Runtime decision procedure: 0.0144563s

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

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

martin-cs commented 3 years ago

On Tue, 2021-06-22 at 07:14 -0700, Saswat Padhi wrote:

So currently:

Z3 returns unknown, so is unreliable, on BV problems with quantifiers

This is semi-expected. It can be improved by instantiation patterns but TBH avoiding quantifiers is a better route.

CVC4 is given QF_AUFBV, so it throws errors.

If the problem includes quantifiers then this is the expected and correct behaviour.

Would it be possible to specify another logic for CVC4 to allow quantifiers (at least when they are used in the C program)?

I would suggest switching the logic based on what you are actually using. You might want FP or DT in there as well, for example.

( From elsewhere, it is fine to @ me and I will do what I can to help when I have a moment. )

TGWDB commented 3 years ago

Returning to examine this issue now that various related bugs/limitations of the cbmc SMT backend are addressed, I am not sure there is a good solution to this issue (unless a significant effort is involved and even then it might be unclear).

To summarise the current state of cbmc and SMT interactions:

cbmc currently relies heavily on bitvectors and related theories in the SMT output.
cbmc can currently output quantified expressions in SMT output.
There is no accepted theory for quantifiers and bitvectors that is used by any of the cbmc supported SMT solvers (or the SMT standard or examples in general).
Where cbmc specifies the theory/theories, this is set to QF_AUFBV which has the most capabilities of the bitvector theories.

The above already leads to problems such as unexpected quantifiers in get-value statements (see #6215 ) and also, as seen above, problems with get-model for z3. There are also problems where cvc4 will cause errors in the current version of cbmc when quantifiers are sent to cvc4 while also specifying the logic to be quantifier free.

Aside: Similar problems to cvc4 can occur for mathsat, while yices and boolector result in an ERROR outcome from the solver (see more on this below).

To progress there are a some possible changes to cbmc that can be done.

Hard Code Different Logics

This might be the lightest approach, which would be to change the hard coded logic for each solver to the most permissible for what cbmc sends and then hope for the best. This is similar to the approach used in the fast response branch and this would allow (for example) cvc4 to find some solutions that are currently prevented by the logic choice.

Note that this would add (although perhaps it is already possible for z3) the possibility of the solver returning unknown as the result of satisfiability. This is currently handled by an ERROR for the result of the solver, and thus for verification relying upon this. (The fast response branch linked above does NOT handle unknowns correctly, instead treating them as unsat which is not feasible for a proper solution.)

Not Outputting Quantifiers

This would require a bit more effort, but to remove the output of quantifiers in most/all of the SMT paths. Since the combination of quantifiers and bitvectors are not well/widely supported, this would make SMT output more usable for multiple solvers. The potential problem here is that this may reduce the performance advantage of using SMT and quantifiers. Also, if it is not done for all solvers, then we have more inconsistency in the SMT (although this may already be an issue).

Handling `UNKNOWN` Properly

One option (although this may be high risk/cost with negligible reward, please do comment if you have insight here!) would be to handle unknown results properly and thus allow for quantifiers and logics that produce them. However, this is a deeper and more complex modification of how cbmc handles satisfiability decisions and goes outside of the scope of the SMT behaviour alone.

Conclusions

The above approaches have different benefits and costs and it is not clear what the best one is. Specially since for special cases or local versions a small modification can be made to implement some of these.

All comments/feedback and other suggestions welcome.

TGWDB commented 3 years ago

Tiny update, we already see unknown in the results from z3. #6221 is created to handle this more gracefully. So to some extent we are already dealing with uncertainty from the solver and treating as ERROR.

TGWDB commented 3 years ago

Some updates.

The z3 issues with the model should have been fixed #6215 (in the sense that there is no error from the model but z3 returns unknown due to quantified expressions).

The cvc4 logic error would be fixed by #6248 which I may try to push to have approved ASAP.

There is also #6270 that may solve some of this issue in a different way (or for other solvers), mentioned for relation rather than dependence upon this PR.

TGWDB commented 3 years ago

Just merged #6248 , please let us know if this (along with other fixes) resolves the issue as expected from your perspective. (I'm aware that this reports a different error for z3 due to z3 responding with unknown, but cvc4 now works correctly.)

TGWDB commented 2 years ago

Closing as this appears to be resolved by various fixes and notes above. Please reopen if you believe this is erroneous.

diffblue / cbmc

Incorrect (hard-coded) logic for SMT backend #5977

cbmc with QF_AUFBV and --z3

cbmc with QF_AUFBV and --cvc4

cbmc with ALL and --z3

cbmc with ALL and --cvc4

Summary

Playing with z3 Directly

Investigatory Conclusions (so far)

Analysis

Hard Code Different Logics

Not Outputting Quantifiers

Handling UNKNOWN Properly

Conclusions

cbmc with `QF_AUFBV` and `--z3`

cbmc with `QF_AUFBV` and `--cvc4`

cbmc with `ALL` and `--z3`

cbmc with `ALL` and `--cvc4`

Playing with `z3` Directly

Handling `UNKNOWN` Properly