Skip to content

Commit

Permalink
Enforce query mode usages (more) strictly
Browse files Browse the repository at this point in the history 
Addresses #459
  • Loading branch information
@LeventErkok
LeventErkok committed Feb 27, 2019
1 parent cdf21b4 commit e3f21b1
Show file tree
Hide file tree
Showing 10 changed files with 123 additions and 96 deletions.
7 changes: 7 additions & 0 deletions CHANGES.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -137,6 +137,13 @@
arguably the right thing to do anyway.) Thanks to Joel Burget for suggesting
the idea.

* [BACKWARDS COMPATIBILITY, Internal] SBV is now more strict in how user-queries
are used, performing certain extra-checks that were not done before. (For instance,
previously it was possible to mix prove-sat with a query call, which should
not have been allowed.) If you have any code that breaks for this reason, you
probably should've written it in some other way to start with. Please get
in touch if that is the case.

### Version 8.0, 2019-01-14

* This is a major release of SBV, with several BACKWARDS COMPATIBILITY breaking
Expand Down
4 changes: 2 additions & 2 deletions Data/SBV.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -457,8 +457,8 @@ We can use 'safe' to statically see if such a violation is possible before we us
>>> safe (sub :: SInt8 -> SInt8 -> SInt8)
[sub: x >= y must hold!: Violated. Model:
s0 = 0 :: Int8
s1 = 1 :: Int8]
s0 = 30 :: Int8
s1 = 32 :: Int8]
What happens if we make sure to arrange for this invariant? Consider this version:
Expand Down
69 changes: 35 additions & 34 deletions Data/SBV/Control/Query.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -297,51 +297,52 @@ getModelAtIndex mbi = do
State{runMode} <- queryState
rm <- io $ readIORef runMode
case rm of
m@CodeGen -> error $ "SBV.getModel: Model is not available in mode: " ++ show m
m@Concrete -> error $ "SBV.getModel: Model is not available in mode: " ++ show m
SMTMode _ isSAT _ -> do cfg <- getConfig
inps <- getQuantifiedInputs
obsvs <- getObservables
uis <- getUIs
m@CodeGen -> error $ "SBV.getModel: Model is not available in mode: " ++ show m
m@Concrete -> error $ "SBV.getModel: Model is not available in mode: " ++ show m
SMTMode _ _ isSAT _ -> do
cfg <- getConfig
inps <- getQuantifiedInputs
obsvs <- getObservables
uis <- getUIs

-- for "sat", display the prefix existentials. for "proof", display the prefix universals
let allModelInputs = if isSAT then takeWhile ((/= ALL) . fst) inps
else takeWhile ((== ALL) . fst) inps
-- for "sat", display the prefix existentials. for "proof", display the prefix universals
let allModelInputs = if isSAT then takeWhile ((/= ALL) . fst) inps
else takeWhile ((== ALL) . fst) inps

-- are we inside a quantifier
insideQuantifier = length allModelInputs < length inps
-- are we inside a quantifier
insideQuantifier = length allModelInputs < length inps

-- observables are only meaningful if we're not in a quantified context
prefixObservables | insideQuantifier = []
| True = obsvs
-- observables are only meaningful if we're not in a quantified context
prefixObservables | insideQuantifier = []
| True = obsvs

sortByNodeId :: [(NamedSymVar, a)] -> [a]
sortByNodeId = map snd . sortBy (compare `on` (\((SV _ nid, _), _) -> nid))
sortByNodeId :: [(NamedSymVar, a)] -> [a]
sortByNodeId = map snd . sortBy (compare `on` (\((SV _ nid, _), _) -> nid))

grab (sv, nm) = ((sv, nm),) <$> getValueCV mbi sv
grab (sv, nm) = ((sv, nm),) <$> getValueCV mbi sv

inputAssocs <- mapM (grab . snd) allModelInputs
inputAssocs <- mapM (grab . snd) allModelInputs

let assocs = sortOn fst prefixObservables
++ sortByNodeId [(sv, (nm, val)) | (sv@(_, nm), val) <- inputAssocs, not (isNonModelVar cfg nm)]
let assocs = sortOn fst prefixObservables
++ sortByNodeId [(sv, (nm, val)) | (sv@(_, nm), val) <- inputAssocs, not (isNonModelVar cfg nm)]

-- collect UIs if requested
let uiFuns = [ui | ui@(_, SBVType as) <- uis, length as > 1, satTrackUFs cfg] -- functions have at least two things in their type!
-- collect UIs if requested
let uiFuns = [ui | ui@(_, SBVType as) <- uis, length as > 1, satTrackUFs cfg] -- functions have at least two things in their type!

-- If there are uninterpreted functions, arrange so that z3's pretty-printer flattens things out
-- as cex's tend to get larger
unless (null uiFuns) $
let solverCaps = capabilities (solver cfg)
in case supportsFlattenedModels solverCaps of
Nothing -> return ()
Just cmds -> mapM_ (send True) cmds
-- If there are uninterpreted functions, arrange so that z3's pretty-printer flattens things out
-- as cex's tend to get larger
unless (null uiFuns) $
let solverCaps = capabilities (solver cfg)
in case supportsFlattenedModels solverCaps of
Nothing -> return ()
Just cmds -> mapM_ (send True) cmds

uivs <- mapM (\ui@(nm, t) -> (\a -> (nm, (t, a))) <$> getUIFunCVAssoc mbi ui) uiFuns
uivs <- mapM (\ui@(nm, t) -> (\a -> (nm, (t, a))) <$> getUIFunCVAssoc mbi ui) uiFuns

return SMTModel { modelObjectives = []
, modelAssocs = assocs
, modelUIFuns = uivs
}
return SMTModel { modelObjectives = []
, modelAssocs = assocs
, modelUIFuns = uivs
}

-- | Just after a check-sat is issued, collect objective values. Used
-- internally only, not exposed to the user.
Expand Down
54 changes: 31 additions & 23 deletions Data/SBV/Control/Utils.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1519,8 +1519,8 @@ unexpected ctx sent expected mbHint received mbReason = do
runProofOn :: SBVRunMode -> QueryContext -> [String] -> Result -> SMTProblem
runProofOn rm context comments res@(Result ki _qcInfo _observables _codeSegs is consts tbls arrs uis axs pgm cstrs _assertions outputs) =
let (config, isSat, isSafe, isSetup) = case rm of
SMTMode stage s c -> (c, s, isSafetyCheckingIStage stage, isSetupIStage stage)
_ -> error $ "runProofOn: Unexpected run mode: " ++ show rm
SMTMode _ stage s c -> (c, s, isSafetyCheckingIStage stage, isSetupIStage stage)
_ -> error $ "runProofOn: Unexpected run mode: " ++ show rm

flipQ (ALL, x) = (EX, x)
flipQ (EX, x) = (ALL, x)
Expand Down Expand Up @@ -1555,6 +1555,12 @@ executeQuery queryContext (QueryT userQuery) = do
st <- symbolicEnv
rm <- liftIO $ readIORef (runMode st)

-- Make sure the phases match:
() <- liftIO $ case (queryContext, rm) of
(QueryInternal, _) -> return () -- no worries, internal
(QueryExternal, SMTMode QueryExternal ISetup _ _) -> return () -- legitimate runSMT call
_ -> invalidQuery rm

-- If we're doing an external query, then we cannot allow quantifiers to be present. Why?
-- Consider:
--
Expand Down Expand Up @@ -1604,7 +1610,7 @@ executeQuery queryContext (QueryT userQuery) = do

case rm of
-- Transitioning from setup
SMTMode stage isSAT cfg | not (isRunIStage stage) -> do
SMTMode qc stage isSAT cfg | not (isRunIStage stage) -> do

let backend = engine (solver cfg)

Expand All @@ -1615,7 +1621,7 @@ executeQuery queryContext (QueryT userQuery) = do
cfg' = cfg { solverSetOptions = solverSetOptions cfg ++ setOpts }
pgm = smtLibPgm cfg'

liftIO $ writeIORef (runMode st) $ SMTMode IRun isSAT cfg
liftIO $ writeIORef (runMode st) $ SMTMode qc IRun isSAT cfg

lift $ join $ liftIO $ backend cfg' st (show pgm) $ extractIO . runReaderT userQuery

Expand Down Expand Up @@ -1653,27 +1659,29 @@ executeQuery queryContext (QueryT userQuery) = do
--
-- So, we just reject it.

SMTMode IRun _ _ -> error $ unlines [ ""
, "*** Data.SBV: Unsupported nested query is detected."
, "***"
, "*** Please group your queries into one block. Note that this"
, "*** can also arise if you have a call to 'query' not within 'runSMT'"
, "*** For instance, within 'sat'/'prove' calls with custom user queries."
, "*** The solution is to do the sat/prove part in the query directly."
, "***"
, "*** While multiple/nested queries should not be necessary in general,"
, "*** please do get in touch if your use case does require such a feature,"
, "*** to see how we can accommodate such scenarios."
]
SMTMode _ IRun _ _ -> error $ unlines [ ""
, "*** Data.SBV: Unsupported nested query is detected."
, "***"
, "*** Please group your queries into one block. Note that this"
, "*** can also arise if you have a call to 'query' not within 'runSMT'"
, "*** For instance, within 'sat'/'prove' calls with custom user queries."
, "*** The solution is to do the sat/prove part in the query directly."
, "***"
, "*** While multiple/nested queries should not be necessary in general,"
, "*** please do get in touch if your use case does require such a feature,"
, "*** to see how we can accommodate such scenarios."
]

-- Otherwise choke!
m -> error $ unlines [ ""
, "*** Data.SBV: Invalid query call."
, "***"
, "*** Current mode: " ++ show m
, "***"
, "*** Query calls are only valid within runSMT/runSMTWith calls"
]
_ -> invalidQuery rm

where invalidQuery rm = error $ unlines [ ""
, "*** Data.SBV: Invalid query call."
, "***"
, "*** Current mode: " ++ show rm
, "***"
, "*** Query calls are only valid within runSMT/runSMTWith calls"
]

{-# ANN module ("HLint: ignore Reduce duplication" :: String) #-}
{-# ANN getAllSatResult ("HLint: ignore Use forM_" :: String) #-}
47 changes: 26 additions & 21 deletions Data/SBV/Core/Symbolic.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -799,20 +799,20 @@ isRunIStage s = case s of
IRun -> True

-- | Different means of running a symbolic piece of code
data SBVRunMode = SMTMode IStage Bool SMTConfig -- ^ In regular mode, with a stage. Bool is True if this is SAT.
| CodeGen -- ^ Code generation mode.
| Concrete -- ^ Concrete simulation mode.
data SBVRunMode = SMTMode QueryContext IStage Bool SMTConfig -- ^ In regular mode, with a stage. Bool is True if this is SAT.
| CodeGen -- ^ Code generation mode.
| Concrete -- ^ Concrete simulation mode.

-- Show instance for SBVRunMode; debugging purposes only
instance Show SBVRunMode where
show (SMTMode ISetup True _) = "Satisfiability setup"
show (SMTMode ISafe True _) = "Safety setup"
show (SMTMode IRun True _) = "Satisfiability"
show (SMTMode ISetup False _) = "Proof setup"
show (SMTMode ISafe False _) = error "ISafe-False is not an expected/supported combination for SBVRunMode!"
show (SMTMode IRun False _) = "Proof"
show CodeGen = "Code generation"
show Concrete = "Concrete evaluation"
show (SMTMode qc ISetup True _) = "Satisfiability setup (" ++ show qc ++ ")"
show (SMTMode qc ISafe True _) = "Safety setup (" ++ show qc ++ ")"
show (SMTMode qc IRun True _) = "Satisfiability (" ++ show qc ++ ")"
show (SMTMode qc ISetup False _) = "Proof setup (" ++ show qc ++ ")"
show (SMTMode qc ISafe False _) = error $ "ISafe-False is not an expected/supported combination for SBVRunMode! (" ++ show qc ++ ")"
show (SMTMode qc IRun False _) = "Proof (" ++ show qc ++ ")"
show CodeGen = "Code generation"
show Concrete = "Concrete evaluation"

-- | Is this a CodeGen run? (i.e., generating code)
isCodeGenMode :: State -> IO Bool
Expand Down Expand Up @@ -970,8 +970,8 @@ modifyState st@State{runMode} field update interactiveUpdate = do
R.modifyIORef' (field st) update
rm <- readIORef runMode
case rm of
SMTMode IRun _ _ -> interactiveUpdate
_ -> return ()
SMTMode _ IRun _ _ -> interactiveUpdate
_ -> return ()

-- | Modify the incremental state
modifyIncState :: State -> (IncState -> IORef a) -> (a -> a) -> IO ()
Expand Down Expand Up @@ -1044,8 +1044,8 @@ internalVariable :: State -> Kind -> IO SV
internalVariable st k = do (sv, nm) <- newSV st k
rm <- readIORef (runMode st)
let q = case rm of
SMTMode _ True _ -> EX
SMTMode _ False _ -> ALL
SMTMode _ _ True _ -> EX
SMTMode _ _ False _ -> ALL
CodeGen -> ALL
Concrete{} -> ALL
n = "__internal_sbv_" ++ nm
Expand Down Expand Up @@ -1301,14 +1301,14 @@ svMkSymVarGen isTracker mbQ k mbNm st = do
return $ SVal k (Left cv)

case (mbQ, rm) of
(Just q, SMTMode{} ) -> mkS q
(Nothing, SMTMode _ isSAT _) -> mkS (if isSAT then EX else ALL)
(Just q, SMTMode{} ) -> mkS q
(Nothing, SMTMode _ _ isSAT _) -> mkS (if isSAT then EX else ALL)

(Just EX, CodeGen{}) -> disallow "Existentially quantified variables"
(_ , CodeGen) -> noUI $ mkS ALL -- code generation, pick universal
(Just EX, CodeGen{}) -> disallow "Existentially quantified variables"
(_ , CodeGen) -> noUI $ mkS ALL -- code generation, pick universal

(Just EX, Concrete{}) -> disallow "Existentially quantified variables"
(_ , Concrete{}) -> noUI mkC
(Just EX, Concrete{}) -> disallow "Existentially quantified variables"
(_ , Concrete{}) -> noUI mkC

-- | Introduce a new user name. We die if repeated.
introduceUserName :: State -> Bool -> String -> Kind -> Quantifier -> SV -> IO SVal
Expand Down Expand Up @@ -1766,6 +1766,11 @@ data SMTSolver = SMTSolver {
data QueryContext = QueryInternal -- ^ Triggered from inside SBV
| QueryExternal -- ^ Triggered from user code

-- | Show instance for 'QueryContext', for debugging purposes
instance Show QueryContext where
show QueryInternal = "Internal Query"
show QueryExternal = "User Query"

{-# ANN type FPOp ("HLint: ignore Use camelCase" :: String) #-}
{-# ANN type PBOp ("HLint: ignore Use camelCase" :: String) #-}
{-# ANN type OvOp ("HLint: ignore Use camelCase" :: String) #-}
10 changes: 8 additions & 2 deletions Data/SBV/Internals.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,11 +9,17 @@
-- Low level functions to access the SBV infrastructure, for developers who
-- want to build further tools on top of SBV. End-users of the library
-- should not need to use this module.
--
-- NB. There are various coding invariants in SBV that are maintained
-- throughout the code. Indiscriminate use of functions in this module
-- can break those invariants. So, you are on your own if you do utilize
-- the functions here. (Unfortunately, what exactly those invariants are
-- is a very good but also a very difficult question to answer!)
-----------------------------------------------------------------------------

module Data.SBV.Internals (
-- * Running symbolic programs /manually/
Result(..), SBVRunMode(..), IStage(..)
Result(..), SBVRunMode(..), IStage(..), QueryContext(..)

-- * Solver capabilities
, SolverCapabilities(..)
Expand Down Expand Up @@ -52,7 +58,7 @@ import Control.Monad.IO.Class (MonadIO)

import Data.SBV.Core.Data
import Data.SBV.Core.Model (genLiteral, genFromCV, genMkSymVar, liftQRem, liftDMod)
import Data.SBV.Core.Symbolic (IStage(..), MonadQuery, addSValOptGoal, registerKind)
import Data.SBV.Core.Symbolic (IStage(..), QueryContext(..), MonadQuery, addSValOptGoal, registerKind)

import Data.SBV.Compilers.C (compileToC', compileToCLib')
import Data.SBV.Compilers.CodeGen
Expand Down
Loading

0 comments on commit e3f21b1

Please sign in to comment.