GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-12-27 09:53:34 +03:00
Code Issues Projects Releases Wiki Activity

Merge branch 'heads/hotfixes/v2.2.5'

Browse Source
This commit is contained in:
Adam C. Foltzer 2015-10-01 10:56:30 -07:00
commit baddfcaab8
7 changed files with 11 additions and 41 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
cryptol.cabal
View File

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

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} \\

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

@ -440,7 +440,6 @@ onlineProveSat :: Bool
-> String -> Maybe FilePath -> REPL Symbolic.ProverResult
onlineProveSat isSat str mfile = do
EnvString proverName <- getUser "prover"
EnvBool iteSolver <- getUser "iteSolver"
EnvBool verbose <- getUser "debug"
satNum <- getUserSatNum
parseExpr <- replParseExpr str
@ -449,7 +448,6 @@ onlineProveSat isSat str mfile = do
let cmd = Symbolic.ProverCommand {
pcQueryType = if isSat then SatQuery satNum else ProveQuery
, pcProverName = proverName
, pcUseSolverIte = iteSolver
, pcVerbose = verbose
, pcExtraDecls = decls
, pcSmtFile = mfile
@ -460,7 +458,6 @@ onlineProveSat isSat str mfile = do
offlineProveSat :: Bool -> String -> Maybe FilePath -> REPL (Either String String)
offlineProveSat isSat str mfile = do
EnvBool iteSolver <- getUser "iteSolver"
EnvBool verbose <- getUser "debug"
parseExpr <- replParseExpr str
(_, expr, schema) <- replCheckExpr parseExpr
@ -468,7 +465,6 @@ offlineProveSat isSat str mfile = do
let cmd = Symbolic.ProverCommand {
pcQueryType = if isSat then SatQuery (SomeSat 0) else ProveQuery
, pcProverName = "offline"
, pcUseSolverIte = iteSolver
, pcVerbose = verbose
, pcExtraDecls = decls
, pcSmtFile = mfile
@ -964,3 +960,4 @@ parseCommand findCmd line = do
'~' : c : more | isPathSeparator c -> do dir <- io getHomeDirectory
return (dir </> more)
_ -> return path

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

@ -564,8 +564,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)

31
src/Cryptol/Symbolic.hs
View File

@ -78,8 +78,6 @@ data ProverCommand = ProverCommand {
-- ^ The type of query to run
, pcProverName :: String
-- ^ Which prover to use (one of the strings in 'proverConfigs')
, pcUseSolverIte :: Bool
-- ^ Whether to force branches (see 'Data.SBV.Dynamic.svSymbolicMerge')
, pcVerbose :: Bool
-- ^ Verbosity flag passed to SBV
, pcExtraDecls :: [DeclGroup]
@ -111,7 +109,7 @@ proverError :: String -> M.ModuleCmd ProverResult
proverError msg modEnv = return (Right (ProverError msg, modEnv), [])
satProve :: ProverCommand -> M.ModuleCmd ProverResult
satProve ProverCommand {..} = protectStack pcUseSolverIte proverError $ \modEnv -> do
satProve ProverCommand {..} = protectStack proverError $ \modEnv -> do
let (isSat, mSatNum) = case pcQueryType of
ProveQuery -> (False, Nothing)
SatQuery sn -> case sn of
@ -137,7 +135,7 @@ satProve ProverCommand {..} = protectStack pcUseSolverIte proverError $ \modEnv
case predArgTypes pcSchema of
Left msg -> return (Right (ProverError msg, modEnv), [])
Right ts -> do when pcVerbose $ putStrLn "Simulating..."
let env = evalDecls (emptyEnv pcUseSolverIte) extDgs
let env = evalDecls mempty extDgs
let v = evalExpr env pcExpr
results' <- runFn $ do
args <- mapM tyFn ts
@ -176,7 +174,7 @@ satProve ProverCommand {..} = protectStack pcUseSolverIte proverError $ \modEnv
satProveOffline :: ProverCommand -> M.ModuleCmd (Either String String)
satProveOffline ProverCommand {..} =
protectStack pcUseSolverIte (\msg modEnv -> return (Right (Left msg, modEnv), [])) $ \modEnv -> do
protectStack (\msg modEnv -> return (Right (Left msg, modEnv), [])) $ \modEnv -> do
let isSat = case pcQueryType of
ProveQuery -> False
SatQuery _ -> True
@ -186,28 +184,22 @@ satProveOffline ProverCommand {..} =
Left msg -> return (Right (Left msg, modEnv), [])
Right ts ->
do when pcVerbose $ putStrLn "Simulating..."
let env = evalDecls (emptyEnv pcUseSolverIte) extDgs
let env = evalDecls mempty extDgs
let v = evalExpr env pcExpr
smtlib <- SBV.compileToSMTLib True isSat $ do
args <- mapM tyFn ts
b <- return $! fromVBit (foldl fromVFun v args)
return b
return (Right (Right smtlib, modEnv), [])
{-
-}
protectStack :: Bool
-> (String -> M.ModuleCmd a)
protectStack :: (String -> M.ModuleCmd a)
-> M.ModuleCmd a
-> M.ModuleCmd a
protectStack usingITE mkErr cmd modEnv =
protectStack mkErr 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 () = mkErr msg modEnv -- (Right (ProverError msg, modEnv), [])
parseValues :: [FinType] -> [SBV.CW] -> ([Eval.Value], [SBV.CW])
@ -307,25 +299,19 @@ 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
-- | Bind a variable in the evaluation environment.
bindVar :: (QName, Value) -> Env -> Env
bindVar (n, thunk) env = env { envVars = Map.insert n thunk (envVars env) }
@ -351,8 +337,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