Skip to content

Commit

Permalink
Reject existential quantifiers in proof-mode queries.
Browse files Browse the repository at this point in the history
  • Loading branch information
@joelburget
joelburget committed Feb 27, 2019
1 parent 60cfa3d commit ae2adfa
Showing 1 changed file with 8 additions and 1 deletion.
9 changes: 8 additions & 1 deletion Data/SBV/Control/Utils.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1580,11 +1580,18 @@ executeQuery queryContext (QueryT userQuery) = do
-- So, we check if this is an external-query, and if there are quantified variables. If so, we
-- cowardly refuse to continue. For details, see: <http://github.com/LeventErkok/sbv/issues/407>

-- We want to reject quantifiers that will turn into `forall` in SMTLib.
-- That usually means rejecting universal quantifiers, but we flip
-- universals and existentials when in proof mode.
let badQ = case rm of
SMTMode _ False _ -> EX
_ -> ALL

() <- liftIO $ case queryContext of
QueryInternal -> return () -- we're good, internal usages don't mess with scopes
QueryExternal -> do
(userInps, _) <- readIORef (rinps st)
let badInps = reverse [n | (ALL, (_, n)) <- userInps]
let badInps = reverse [n | (q, (_, n)) <- userInps, q == badQ]
case badInps of
[] -> return ()
_ -> let plu | length badInps > 1 = "s require"
Expand Down

7 comments on commit ae2adfa

@LeventErkok
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@joelburget Do you have an example SBV program that actually triggers this?

@joelburget
Copy link
Owner Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@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
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I see. The issue here is that if you have a query, you're supposed to call it with runSMT; not with prove etc. I think the fix should be in that direction. i.e., this should be rejected because you used a query call but in a prove context. I thought I added that check, but obviously it's not working. I'll take a look.

@LeventErkok
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Tracking this here now: LeventErkok/sbv#459

@joelburget
Copy link
Owner Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@LeventErkok FWIW my example was perhaps a bit oversimplified. We're actually using runSymbolic, closer to this:

module Documentation.SBV.Examples.Test where

import           Data.SBV           (SBool, sBool, z3)
import qualified Data.SBV.Internals as SBVI
import           Data.SBV.Control   (query)

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

@LeventErkok
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

That's an illegal use as well, and should be rejected too :-)

I'm working on a patch that'll reject all of these. The only legitimate way to have a query is to call via runSMT.

@LeventErkok
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

To be clear: Returning an SBool out of the symbolic computation is dangerous. This is actually a known bug dating back to 2013 or so: LeventErkok/sbv#71

We really need a runST like trick to avoid these right at the type level, but it is costly and complicates the use cases.

Please sign in to comment.