Query mode isn't enforced properly

[LeventErkok]

@LeventErkok I have two answers which might help

1. @bts build a "tagging" system for our program analysis work, which uses a bunch of free variables, one for every point in the control-flow graph, to get the value of points within the execution of a program, ie, a trace. It looks like our uses of free in this system were causing this check to throw.
2. The simplest example I have is this:

module Documentation.SBV.Examples.Test where

import           Data.SBV           (prove, sBool, ThmResult)
import           Data.SBV.Control   (query)

test :: IO ThmResult
test = prove $ do
  x <- sBool "x"
  query $ pure x

Which fails with:

λ> test
*** Exception:
*** Data.SBV: Unsupported query call in the presence of quantified inputs.
***
*** The following variable requires explicit quantification:
***
***    x
***
*** While quantification and queries can co-exist in principle, SBV currently
*** does not support this scenario. Avoid using quantifiers with user queries
*** if possible. Please do get in touch if your use case does require such
*** a feature to see how we can accommodate such scenarios.

I believe (?) this should succeed.

[LeventErkok]

@joelburget @bts

I just pushed in a bunch of changes to catch more of the "bad" use cases. To summarize, consider the following 5 definitions:

module Documentation.SBV.Examples.Test where

import           Data.SBV
import           Data.SBV.Internals
import           Data.SBV.Control

test1 :: IO ThmResult
test1 = prove $ do
  x <- sBool "x"
  query $ pure x

test2 :: IO SatResult
test2 = sat $ do
  x <- sBool "x"
  query $ pure x

test3 :: IO (SBool, Result)
test3 = runSymbolic (SMTMode QueryInternal ISetup False z3) $ do
  x <- sBool "x"
  query $ pure x

test4 :: IO SBool
test4 = runSMT $ do
  x <- sBool "x"
  query $ pure x

test5 :: IO (SBool, Result)
test5 = runSymbolic (SMTMode QueryExternal ISetup False z3) $ do
  x <- sBool "x"
  query $ pure x

Currently, test1, test2, test3 are all rejected: You get:

*** Exception:
*** Data.SBV: Invalid query call.
***
***   Current mode: Satisfiability setup (Internal Query)
***
*** Query calls are only valid within runSMT/runSMTWith calls

So far so good: if you use query, then you must use runSMT. But the story is different for test4:

ghci> test4
<symbolic> :: SBool

Strictly speaking, this is OK, but is precisely exposing the very original design flaw (dating back to #71): It leaks the symbolic context out, and you can use that to do bad things. Unfortunately, there isn't much we can do here unless we go for an runST like trick, and that's a huge undertaking that I'm afraid is not feasible for the time being.

Finally, test5 is quite interesting. It yields:

*** Exception:
*** Data.SBV: Unsupported query call in the presence of quantified inputs.
***
*** The following variable requires explicit quantification:
***
***    x
***
*** While quantification and queries can co-exist in principle, SBV currently
*** does not support this scenario. Avoid using quantifiers with user queries
*** if possible. Please do get in touch if your use case does require such
*** a feature to see how we can accommodate such scenarios.

What happened here is actually correct but can be confusing! The issue is that you reached out to internals, and used (SMTMode QueryExternal ISetup False z3) as an argument to runSymbolic; and this is precisely the point where you told SBV to prove a universally quantified propert (False means prove there), and you also used a query. Even though this particular use case is safe, we do not allow for that, and I documented the reasons in the code. (Essentially, there's no guarantee those variables would be available in getValue calls, so SBV doesn't allow them; this was actually discovered in collaboration with Brian in http://github.com/LeventErkok/sbv/issues/407).

So, long story short, aside from the existing bug #71, I think we now properly handle and reject the scenarios that are not supported for good reasons.

This is obviously a behavioral change, and I'd be interested in hearing from you that you can still write your programs with the current restrictions. (And please avoid test4 like scenarios where the symbolic context leaks out: We cannot check for those currently, and such programs are really dangerous!)

Let me know how it goes!

[LeventErkok]

@joelburget @bts

I wanted to emphasize how important it is to avoid programs like test4. Here's an example:

import Data.SBV
import Data.SBV.Control

import Control.Monad.Trans

leak :: IO SBool
leak = runSMT $ do x <- sBool "x"
                   query $ pure x

terrible :: IO ThmResult
terrible = proveWith z3{verbose=True} $ do
        y <- sBool "y"
        x <- lift leak        -- reach in!
        return $ y .== x

This should be illegal! But it type checks and you get:

*Main> terrible
** 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 QF_BV)
[GOOD] ; --- uninterpreted sorts ---
[GOOD] ; --- tuples ---
[GOOD] ; --- sums ---
[GOOD] ; --- literal constants ---
[GOOD] ; --- skolem constants ---
[GOOD] (declare-fun s0 () Bool) ; tracks user variable "y"
[GOOD] ; --- constant tables ---
[GOOD] ; --- skolemized tables ---
[GOOD] ; --- arrays ---
[GOOD] ; --- uninterpreted constants ---
[GOOD] ; --- user given axioms ---
[GOOD] ; --- formula ---
[GOOD] (assert false)
[SEND] (check-sat)
[RECV] unsat
*** Solver   : Z3
*** Exit code: ExitSuccess
Q.E.D.

This is obviously unsound! Once you leak something out to IO, you should not bring it back in. This is the same issue with runST in Haskell, and why runST has a rank-2 type: http://hackage.haskell.org/package/base-4.12.0.0/docs/src/GHC.ST.html#runST

If I was designing SBV today, I'd have insisted on a runST like solution to avoid this scenario. One fix I can put in is to get rid of the MonadIO instances, which would make this "harder" to exploit, but wouldn't really fix the issue.

I'm happy to discuss this further if necessary. But here's an easy rule-of-thumb: if you have Symbolic things (SBool/SInt8 etc.), they should stay in the Symbolic monad, and not leave out to IO world. That's a code smell whenever you have a type like IO SBool.

[joelburget]

Hi Levent, thanks for the great explanation and work to fix this. Some other stuff came up so I didn't get to work on this as much as I had hoped to today. I believe we'll be able to rewrite our code to avoid this issue, but I'm not sure yet. I'll write back hopefully tomorrow when I know more.

[joelburget]

Now that I've looked at this more, I believe we have a legitimate use case that we can't implement due to the existing external query quantifier check.

In our setting, we have two classes of variables and constraints:

1. The symbolic representation of the program we're analyzing (this can contain universal and existential quantifiers)
2. Properties we assert to be true of the program (this contains no universal / existential quantifiers, as such, we only use free for variables here)

When we set up our system of constraints we assert constraints from both of these classes simultaneously, then check for validity. When sbv finds that the combined system is invalid, we use a query to find the value of variables in the program in the falsifying example.

Importantly, we only query for the value of variables in class 2, which I believe is safe (but currently disallowed).

Does this seem like a legitimate use case? And am I right this is currently impossible? If so, what's the best way to work around this?

Thanks for the help.

[LeventErkok]

Absolutely legitimate use case, and admitted by SBV:

While quantification and queries can co-exist in principle, SBV currently
does not support this scenario.

It's hard to support due to the issues listed in #407.

How about the following compromise: We can add a config parameter, say allowQuantifiedQueries, defaulting to False, but if you set it then SBV would skip the test and you'd be on your own if you trigger the scenario in #407.

Would that work for you guys? Wouldn't be too hard to implement.

[joelburget]

That sounds perfect 👍

[LeventErkok]

Ok, give it a shot! Remember that you're on your own if you "breach" contract and do a getValue on a variable that's hidden behind a quantifier. Here's an example:

{-# LANGUAGE ScopedTypeVariables #-}

import           Data.SBV
import           Data.SBV.Control

test1 :: IO  Bool
test1 = runSMTWith z3{verbose=True,allowQuantifiedQueries=True} $ do
  x :: SBool <- forall "x"
  query $ do ensureSat
             getValue x

This produces:

*** Exception:
*** Data.SBV: Unexpected response from the solver, context: getValue:
***
***    Sent      : (get-value (s0))
***    Expected  : a model value
***    Received  : (error "line 11 column 12: unknown constant s0")
***
***    Executable: z3
***    Options   : -nw -in -smt2
***
***    Reason    : Solver returned an error: "line 11 column 12: unknown constant s0"

Let me know how it works out and handles your actual use case.

[joelburget]

I can confirm your change works for us! Thanks so much for the help on this.

[LeventErkok]

Fantastic! Glad to hear.