LeventErkok / sbv

SMT Based Verification in Haskell. Express properties about Haskell programs and automatically prove them using SMT solvers.
https://github.com/LeventErkok/sbv
Other
243 stars 34 forks source link

nonconstant terms in array constant while using CVC4 #574

Closed MrChico closed 3 years ago

MrChico commented 3 years ago

I'm getting occassional errors of this kind when using the cvc4 solver:

*** Data.SBV: Unexpected response from the solver, context: define-fun:
***
***    Sent      : (define-fun array_0 () (Array (_ BitVec 256) (_ BitVec 256)) ((as const (Array (_ BitVec 256) (_ BitVec 256))) s3))
***    Expected  : success
***    Received  : (error "Parse Error: <shell>:1.113: expected constant term inside array constant, but found nonconstant term:
***                the term: s3")
***
***    Executable: /nix/store/4vm8vn16cjf0pxfm2j0g6kqi3a7vyn3m-cvc4-1.8-prerelease/bin/cvc4
***    Options   : --lang=smt --incremental --interactive --no-interactive-prompt --model-witness-value --tlimit-per=30000

Unfortunately, I have been unable to figure precisely in which cases this bug is exhibited and therefore not been able to cook up a minimal example. I am using SBV for symbolically executing programs, and I can only reproduce this bug with specific programs, but when I try to abstract the queries from the program into sbv code directly the bug is not visible... My guess is that some sharing might be going on that shouldn't be enabled while using cvc4. In case it might be useful, here is a transcript the smt query produced.

LeventErkok commented 3 years ago

I'm aware of this discrepancy between z3 and cvc4. (And possibly other solvers.) Here's a way to replicate it:

{-# LANGUAGE ScopedTypeVariables #-}

import Data.SBV

p s = satWith s{verbose=True} $ do
    q <- sInteger "q"
    a :: SArray Integer Integer <- newArray_ (Just q)
    return $ readArray a 3 .== 2

I get:

*Main> p z3
** Calling: z3 -nw -in -smt2
[GOOD] ; Automatically generated by SBV. Do not edit.
[GOOD] (set-option :print-success true)
[GOOD] (set-option :global-declarations true)
[GOOD] (set-option :smtlib2_compliant true)
[GOOD] (set-option :diagnostic-output-channel "stdout")
[GOOD] (set-option :produce-models true)
[GOOD] (set-logic ALL) ; has unbounded values, using catch-all.
[GOOD] ; --- uninterpreted sorts ---
[GOOD] ; --- tuples ---
[GOOD] ; --- sums ---
[GOOD] ; --- literal constants ---
[GOOD] (define-fun s1 () Int 3)
[GOOD] (define-fun s3 () Int 2)
[GOOD] ; --- skolem constants ---
[GOOD] (declare-fun s0 () Int) ; tracks user variable "q"
[GOOD] ; --- constant tables ---
[GOOD] ; --- skolemized tables ---
[GOOD] ; --- arrays ---
[GOOD] (define-fun array_0 () (Array Int Int) ((as const (Array Int Int)) s0))
[GOOD] ; --- uninterpreted constants ---
[GOOD] ; --- user given axioms ---
[GOOD] ; --- formula ---
[GOOD] (define-fun s2 () Int (select array_0 s1))
[GOOD] (define-fun s4 () Bool (= s2 s3))
[GOOD] (define-fun array_0_initializer () Bool true) ; no initializiation needed
[GOOD] (assert s4)
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 2))
*** Solver   : Z3
*** Exit code: ExitSuccess
Satisfiable. Model:
  q = 2 :: Integer

But:

*Main> p cvc4
** Calling: cvc4 --lang smt --incremental --interactive --no-interactive-prompt --model-witness-value
[GOOD] ; Automatically generated by SBV. Do not edit.
[GOOD] (set-option :print-success true)
[GOOD] (set-option :global-declarations true)
[GOOD] (set-option :diagnostic-output-channel "stdout")
[GOOD] (set-option :produce-models true)
[GOOD] (set-logic ALL) ; has unbounded values, using catch-all.
[GOOD] ; --- uninterpreted sorts ---
[GOOD] ; --- tuples ---
[GOOD] ; --- sums ---
[GOOD] ; --- literal constants ---
[GOOD] (define-fun s1 () Int 3)
[GOOD] (define-fun s3 () Int 2)
[GOOD] ; --- skolem constants ---
[GOOD] (declare-fun s0 () Int) ; tracks user variable "q"
[GOOD] ; --- constant tables ---
[GOOD] ; --- skolemized tables ---
[GOOD] ; --- arrays ---
[FAIL] (define-fun array_0 () (Array Int Int) ((as const (Array Int Int)) s0))
** Exception:
*** Data.SBV: Unexpected non-success response from CVC4:
***
***    Sent      : (define-fun array_0 () (Array Int Int) ((as const (Array Int Int)) s0))
***    Expected  : success
***    Received  : (error "Parse Error: <shell>:1.69: expected constant term inside array constant, but found nonconstant term:
***                  ...Array Int Int) ((as const (Array Int Int)) s0))
***                                                                ^
***                the term: s0")
***
***    Stderr    : CVC4 interrupted by SIGTERM.
***    Exit code : ExitFailure (-6)
***    Executable: /usr/local/bin/cvc4
***    Options   : --lang smt --incremental --interactive --no-interactive-prompt --model-witness-value
***
***    Reason    : Check solver response for further information. If your code is correct,
***                please report this as an issue either with SBV or the solver itself!

It seems CVC4 doesn't accept non-constants in an as const declaration.

Unfortunately, this is one of the gray areas in the SMTLib spec. If you read through http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf there seems to be only one reference to declaration of constant arrays in section 3.6.4; and it's only a passing reference. I think z3 is correct here, and CVC4 is being (unnecessarily?) restrictive.

The best thing to do would be to file a request with the CVC4 folks (https://github.com/CVC4/CVC4/issues) and see if this is something they can add support for, or if they can recommend a workaround. We can take it from there once they have a recommendation.

UPDATE Filed here: https://github.com/CVC4/CVC4/issues/5782. Let's see what the CVC4 folks say.

MrChico commented 3 years ago

Ah, right. In my situation though, I am always using a literal for the constant, and still I am getting the non-constant error, because sbv has previously instantiated the literal as a variable. I wonder if it makes sense to deal with this special case in case fixing the matter in cvc4 will take some time.

LeventErkok commented 3 years ago

SBV actually already does this:

https://github.com/LeventErkok/sbv/blob/0be1345b839d50b68d936e7761285b1ce9909b89/Data/SBV/SMT/SMTLib2.hs#L572-L576

So, I'm not sure why it's not working for you. There could be some interaction with the query mode; or perhaps it's not really a literal constant but is otherwise computed from others in a more complicated way.

If you can post a small example that exhibits the issue, I can take a look.

MrChico commented 3 years ago

Actually, modifying your example lets me reproduce this special case as well:

p s = runSMTWith s{verbose=True} $ query $ do
    q <- freshVar_
    constrain $ (q :: SInteger) .== 0
    a :: SArray Integer Integer <- freshArray_ (Just 0)
    return $ readArray a 3 .== 2

This indeed crashes with cvc4 just like the example above, while if we remove the two lines referencing q it does not.

LeventErkok commented 3 years ago

I see the issue here. The problem is that when you're in the query mode, sbv only substitutes constants as it makes updates to the solver. In your case, it does one update after the constrain call; which creates the literal constant 0. In the next line, it reuses this constant internally, so it's no longer in the consts list. In fact, if you swap the order:

    a :: SArray Integer Integer <- freshArray_ (Just 0)
    constrain $ (q :: SInteger) .== 0

you'll see that it works fine now.

This is unfortunate of course, as in general, the user won't be tracking which constants will be stored as such. Nor they should be expected to do so. But unfortunately, it's not very easy to fix either.

Hopefully CVC4 folks can fix it directly in their code. Or you can work around by making sure all such arrays are declared before the query mode starts. (If you declare the arrays before the query mode, the constant substitution should work.)

LeventErkok commented 3 years ago

@MrChico

I pushed in a workaround, which I believe should handle your use case. Can you give it a try?

MrChico commented 3 years ago

Yes, it looks like this fixes it! Thank you so much for the quick fix!

LeventErkok commented 3 years ago

Cool. I'll leave this ticket open to see if the general case can be addressed in CVC4 as well; based on any feedback they might provide.

LeventErkok commented 3 years ago

@MrChico I'm going to close this as there isn't much SBV can do about it on top of what we've implemented. And if CVC4 folks do end up supporting the more general form, we'll simply benefit from that without any changes. Please re-open if you see any further issues.

MrChico commented 3 years ago

Sounds good. The fix implemented resolved my problems at least.