GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-11-28 09:23:04 +03:00
Code Issues Projects Releases Wiki Activity

remove iteSolver option for compat with sbv 5+

Browse Source
This commit is contained in:
Adam C. Foltzer 2015-09-30 14:24:21 -07:00
parent 243e051df3
commit 7d81568555
9 changed files with 25 additions and 40 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
cryptol.cabal
View File

@ -56,7 +56,7 @@ library
process >= 1.2,
QuickCheck >= 2.7,
random >= 1.0.1,
sbv >= 4.3 && < 5.0,
sbv (>= 4.3 && < 5.0) || (>= 5.1 && < 5.2),
smtLib >= 1.0.7,
syb >= 0.4,
text >= 1.1,

BIN
docs/ProgrammingCryptol.pdf
View File

Binary file not shown.

1
docs/ProgrammingCryptol/installation/Install.tex
View File

@ -261,7 +261,6 @@ aliases you have defined, along with their types.
\texttt{base} & \texttt{10} & numeric base for printing words \\
\texttt{debug} & \texttt{off} & whether to print verbose debugging information \\
\texttt{infLength} & \texttt{5} & number of elements to show from an infinite sequence \\
\texttt{iteSolver} & \texttt{off} & whether \texttt{:prove} calls out for help on recursive functions \\
\texttt{prover} & \texttt{cvc4} & which SMT solver to use for \texttt{:prove} \\
\texttt{tests} & \texttt{100} & number of tests to run for \texttt{:check} \\
\texttt{warnDefaulting} & \texttt{on} & \todo[inline]{talk to Iavor} \\

BIN
docs/Syntax.pdf
View File

Binary file not shown.

BIN
docs/Version2Changes.pdf
View File

Binary file not shown.

6
src/Cryptol/REPL/Command.hs
View File

@ -360,7 +360,6 @@ cmdProveSat isSat str = do
onlineProveSat :: Bool
-> String -> String -> Maybe FilePath -> REPL ()
onlineProveSat isSat str proverName mfile = do
EnvBool iteSolver <- getUser "iteSolver"
EnvBool verbose <- getUser "debug"
mSatNum <- getUserSatNum
let cexStr | isSat = "satisfying assignment"
@ -372,7 +371,7 @@ onlineProveSat isSat str proverName mfile = do
Symbolic.satProve
isSat
mSatNum
(proverName, iteSolver, verbose)
(proverName, verbose)
(M.deDecls denv)
mfile
(expr, schema)
@ -415,13 +414,12 @@ onlineProveSat isSat str proverName mfile = do
offlineProveSat :: Bool -> String -> Maybe FilePath -> REPL ()
offlineProveSat isSat str mfile = do
EnvBool useIte <- getUser "iteSolver"
EnvBool vrb <- getUser "debug"
parseExpr <- replParseExpr str
exsch <- replCheckExpr parseExpr
decls <- fmap M.deDecls getDynEnv
result <- liftModuleCmd $
Symbolic.satProveOffline isSat useIte vrb decls mfile exsch
Symbolic.satProveOffline isSat vrb decls mfile exsch
case result of
Symbolic.ProverError msg -> rPutStrLn msg
Symbolic.EmptyResult -> return ()

2
src/Cryptol/REPL/Monad.hs
View File

@ -529,8 +529,6 @@ userOptions = mkOptionMap
"The maximum number of :sat solutions to display (\"all\" for no limit)."
, simpleOpt "prover" (EnvString "cvc4") checkProver $
"The external SMT solver for :prove and :sat (" ++ proverListString ++ ")."
, simpleOpt "iteSolver" (EnvBool False) (const $ return Nothing)
"Use smt solver to filter conditional branches in proofs."
, simpleOpt "warnDefaulting" (EnvBool True) (const $ return Nothing)
"Choose if we should display warnings when defaulting."
, simpleOpt "warnShadowing" (EnvBool True) (const $ return Nothing)

43
src/Cryptol/Symbolic.hs
View File

@ -41,6 +41,14 @@ import Data.Monoid (Monoid(..))
import Data.Traversable (traverse)
#endif
#if MIN_VERSION_sbv(5,1,0)
smtMode :: SBV.SMTLibVersion
smtMode = SBV.SMTLib2
#else
smtMode :: Bool
smtMode = True
#endif
-- External interface ----------------------------------------------------------
proverConfigs :: [(String, SBV.SMTConfig)]
@ -83,12 +91,12 @@ thmSMTResults (SBV.ThmResult r) = [r]
satProve :: Bool
-> Maybe Int -- ^ satNum
-> (String, Bool, Bool)
-> (String, Bool)
-> [DeclGroup]
-> Maybe FilePath
-> (Expr, Schema)
-> M.ModuleCmd ProverResult
satProve isSat mSatNum (proverName, useSolverIte, verbose) edecls mfile (expr, schema) = protectStack useSolverIte $ \modEnv -> do
satProve isSat mSatNum (proverName, verbose) edecls mfile (expr, schema) = protectStack $ \modEnv -> do
let extDgs = allDeclGroups modEnv ++ edecls
provers <-
case proverName of
@ -109,7 +117,7 @@ satProve isSat mSatNum (proverName, useSolverIte, verbose) edecls mfile (expr, s
case predArgTypes schema of
Left msg -> return (Right (ProverError msg, modEnv), [])
Right ts -> do when verbose $ putStrLn "Simulating..."
let env = evalDecls (emptyEnv useSolverIte) extDgs
let env = evalDecls emptyEnv extDgs
let v = evalExpr env expr
results' <- runFn $ do
args <- mapM tyFn ts
@ -147,14 +155,13 @@ satProve isSat mSatNum (proverName, useSolverIte, verbose) edecls mfile (expr, s
return (Right (esatexprs, modEnv), [])
satProveOffline :: Bool
-> Bool
-> Bool
-> [DeclGroup]
-> Maybe FilePath
-> (Expr, Schema)
-> M.ModuleCmd ProverResult
satProveOffline isSat useIte vrb edecls mfile (expr, schema) =
protectStack useIte $ \modEnv -> do
satProveOffline isSat vrb edecls mfile (expr, schema) =
protectStack $ \modEnv -> do
let extDgs = allDeclGroups modEnv ++ edecls
let tyFn = if isSat then existsFinType else forallFinType
let filename = fromMaybe "standard output" mfile
@ -162,11 +169,11 @@ satProveOffline isSat useIte vrb edecls mfile (expr, schema) =
Left msg -> return (Right (ProverError msg, modEnv), [])
Right ts ->
do when vrb $ putStrLn "Simulating..."
let env = evalDecls (emptyEnv useIte) extDgs
let env = evalDecls emptyEnv extDgs
let v = evalExpr env expr
let satWord | isSat = "satisfiability"
| otherwise = "validity"
txt <- SBV.compileToSMTLib True isSat $ do
txt <- SBV.compileToSMTLib smtMode isSat $ do
args <- mapM tyFn ts
b <- return $! fromVBit (foldl fromVFun v args)
liftIO $ putStrLn $
@ -180,16 +187,12 @@ satProveOffline isSat useIte vrb edecls mfile (expr, schema) =
Nothing -> putStr txt
return (Right (EmptyResult, modEnv), [])
protectStack :: Bool
protectStack :: M.ModuleCmd ProverResult
-> M.ModuleCmd ProverResult
-> M.ModuleCmd ProverResult
protectStack usingITE cmd modEnv = X.catchJust isOverflow (cmd modEnv) handler
protectStack cmd modEnv = X.catchJust isOverflow (cmd modEnv) handler
where isOverflow X.StackOverflow = Just ()
isOverflow _ = Nothing
msg | usingITE = msgBase
| otherwise = msgBase ++ "\n" ++
"Using ':set iteSolver=on' might help."
msgBase = "Symbolic evaluation failed to terminate."
msg = "Symbolic evaluation failed to terminate."
handler () = return (Right (ProverError msg, modEnv), [])
parseValues :: [FinType] -> [SBV.CW] -> ([Eval.Value], [SBV.CW])
@ -289,24 +292,21 @@ existsFinType ty =
data Env = Env
{ envVars :: Map.Map QName Value
, envTypes :: Map.Map TVar TValue
, envIteSolver :: Bool
}
instance Monoid Env where
mempty = Env
{ envVars = Map.empty
, envTypes = Map.empty
, envIteSolver = False
}
mappend l r = Env
{ envVars = Map.union (envVars l) (envVars r)
, envTypes = Map.union (envTypes l) (envTypes r)
, envIteSolver = envIteSolver l || envIteSolver r
}
emptyEnv :: Bool -> Env
emptyEnv useIteSolver = Env Map.empty Map.empty useIteSolver
emptyEnv :: Env
emptyEnv = mempty
-- | Bind a variable in the evaluation environment.
bindVar :: (QName, Value) -> Env -> Env
@ -334,8 +334,7 @@ evalExpr env expr =
ETuple es -> VTuple (map eval es)
ERec fields -> VRecord [ (f, eval e) | (f, e) <- fields ]
ESel e sel -> evalSel sel (eval e)
EIf b e1 e2 -> evalIf (fromVBit (eval b)) (eval e1) (eval e2)
where evalIf = if envIteSolver env then sBranchValue else iteValue
EIf b e1 e2 -> iteValue (fromVBit (eval b)) (eval e1) (eval e2)
EComp ty e mss -> evalComp env (evalType env ty) e mss
EVar n -> case lookupVar n env of
Just x -> x

11
src/Cryptol/Symbolic/Value.hs
View File

@ -23,7 +23,7 @@ module Cryptol.Symbolic.Value
, fromVBit, fromVFun, fromVPoly, fromVTuple, fromVRecord, lookupRecord
, fromSeq, fromVWord
, evalPanic
, iteValue, sBranchValue, mergeValue
, iteValue, mergeValue
)
where
@ -75,15 +75,6 @@ iteValue c x y =
Just False -> y
Nothing -> mergeValue True c x y
sBranchValue :: SBool -> Value -> Value -> Value
sBranchValue t x y =
case svAsBool c of
Just True -> x
Just False -> y
Nothing -> mergeValue False c x y
where
c = svReduceInPathCondition t
mergeValue :: Bool -> SBool -> Value -> Value -> Value
mergeValue f c v1 v2 =
case (v1, v2) of