SMT solver errors in counterexample extraction over quantified expressions

[SaswatPadhi]

CBMC version: develop

Operating system: Mac OS 10.15.7

Test case:

#include <assert.h>

void main()
{
  unsigned A, x[64];
  __CPROVER_assume(0 <= A && A < 64);
  __CPROVER_assume(__CPROVER_forall { int i ; (0 <= i && i < A) ==> x[i] >= 1 });
  assert(x[0] > 0);
}

Exact command line resulting in the issue:

cbmc --smt2 --trace test.c

What behaviour did you expect:
CBMC would report a counterexample trace.
(A = 0 violates the assertion.)

What happened instead:
CBMC does not generate a counterexample trace, and shows the following error:

SMT2 solver returned error message:
        "line 296 column 16: invalid get-value term, term must be ground and must not contain quantifiers"

[thomasspriggs]

The error message shown here from the SMT2 solver is complaining that CBMC is attempting to get the value of an identifier, where the definition of this identifier contains a quantifier. In this case the identifier is defined as (define-fun |B3| () Bool (forall ((|main::1::1::i!0#0| (_ BitVec 32))) (or (not (bvsge |main::1::1::i!0#0| (_ bv0 32))) (bvuge |main::1::1::i!0#0| |main::1::A!0@1#1|) (bvuge (select array.0 ((_ sign_extend 32) |main::1::1::i!0#0|)) (_ bv1 32))))) and the get command is (get-value (|B3|)). I am unsure if this is due to lacking support for quantifiers in z3 or because it doesn't make sense to get the value of this identifier and we should be attempting to construct a trace without it.

There are a few things I have tried:

• Manually editing the .smt2 file to instruct z3 to apply quantifier elimination by adding - (apply (using-params qe :qe-nonlinear true)). This result in z3 seemingly executing indefinitely.
• Using the develop branch of cbmc with the --cvc4 option gives -

CBMC version 5.32.1 (cbmc-5.32.1-105-gf9be0ebfbd) 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.00720277s
size of program expression: 43 steps
simple slicing removed 2 assignments
Generated 1 VCC(s), 1 remaining after simplification
Runtime Postprocess Equation: 4.2005e-05s
Passing problem to SMT2 QF_AUFBV using CVC4
converting SSA
Runtime Convert SSA: 0.00145214s
Running SMT2 QF_AUFBV using CVC4
SMT2 solver returned error message:
	"Parse Error: /tmp/smt2_dec_problem_32030.85Ea2D: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"
Runtime Solver: 0.00827663s
Runtime decision procedure: 0.0098524s

** Results:
./test.c function main
[main.assertion.1] line 8 assertion x[0] > 0: ERROR

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

• The above error can be avoided by either manually running cvc4 against the file generated with the --z3 command line argument, or by adding use_array_of_bool = true; to the specialisations used for cvc4 in smt2_convt::smt2_convt. Unfortunately, this results in cvc4 returning an unknown status rather than sat or unsat, which isn't going to help with generating the trace you were hoping to see from the cbmc output.

I think the next thing to try would be making cbmc not request the the values of identifiers containing quantifiers and building the trace without the values of those identifiers.

[martin-cs]

On Thu, 2021-06-24 at 02:43 -0700, Thomas Spriggs wrote: The error message shown here from the SMT2 solver is complaining that CBMC is attempting to get the value of an identifier, where the definition of this identifier contains a quantifier. In this case the identifier is defined as `(define-fun |B3| () Bool (forall ((|main::1::1::i!0#0| (_ BitVec 32))) (or (not (bvsge |main::1::1::i!0#0| (_ bv0 32))) (bvuge |main::1::1::i!0#0| ***@***.***#1|) (bvuge (select array.0 ((_ sign_extend 32) |main::1::1::i!0#0|)) (_ bv1 32)))))` and the get command is `(get- value (|B3|))`. I am unsure if this is due to lacking support for quantifiers in z3 or because it doesn't make sense to get the value of this identifier and we should be attempting to construct a trace without it.

One of the reasons why the output of `(get-model)` is not standardised in SMT-LIB 2.* is that there are cases like this where it is not obvious what one should return. Do you return true? Do you return some kind of Skolem function (a function that takes a `(_ BitVec 32)` and gives you the value required for `|main::1::1::i!0#0|` so that the expression is true)? What if generating that Skolem function is significantly more work than solving the `(check-sat)` Do you return a proof? Z3 may simply not handle this case.

There are a few things I have tried: - Manually editing the `.smt2` file to instruct `z3` to apply quantifier elimination by adding - `(apply (using-params qe :qe- nonlinear true))`. This result in `z3` seemingly executing indefinitely.

Quantifier elimination is generally dicey. My guess is that this is intended for NRA (i.e. non-linear real) in which you can do it. There is relatively little work on quantifier elimination for bit-vectors (maybe the Invertibility Conditions work a couple of years ago and some things from QBF, although this is kind of a different problem).

- Using the `develop` branch of cbmc with the `--cvc4` option gives - ``` CBMC version 5.32.1 (cbmc-5.32.1-105-gf9be0ebfbd) 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.00720277s size of program expression: 43 steps simple slicing removed 2 assignments Generated 1 VCC(s), 1 remaining after simplification Runtime Postprocess Equation: 4.2005e-05s Passing problem to SMT2 QF_AUFBV using CVC4 converting SSA Runtime Convert SSA: 0.00145214s Running SMT2 QF_AUFBV using CVC4 SMT2 solver returned error message: "Parse Error: /tmp/smt2_dec_problem_32030.85Ea2D: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"

This is because `false` and `(_ bv0 1)` are different sorts. This is a bug in CPROVER because it is generating invalid SMT-LIB output.

* The above error can be avoided by either manually running `cvc4` against the file generated with the `--z3` command line argument, or by adding `use_array_of_bool = true;` to the specialisations used for `cvc4` in `smt2_convt::smt2_convt`. Unfortunately, this results in `cvc4` returning an `unknown` status rather than sat or unsat, which isn't going to help with generating the trace you were hoping to see from the cbmc output. I think the next thing to try would be making cbmc not request the the values of identifiers containing quantifiers and building the trace without the values of those identifiers.

This is probably the way to go unless you are really prepared to dig into the question of what are models for quantified expressions. HTH

[thomasspriggs]

There is a quick and dirty fix for some of the problems reported in this issue here - NlightNFotis#15
This branch would need tests, before I would raise it as a PR on the diffblue fork.