diff --git a/cryptol.cabal b/cryptol.cabal
--- a/cryptol.cabal
+++ b/cryptol.cabal
@@ -1,5 +1,5 @@
Name: cryptol
-Version: 2.2.4
+Version: 2.2.5
Synopsis: Cryptol: The Language of Cryptography
Description: Cryptol is a domain-specific language for specifying cryptographic algorithms. A Cryptol implementation of an algorithm resembles its mathematical specification more closely than an implementation in a general purpose language. For more, see .
License: BSD3
@@ -23,7 +23,7 @@
source-repository this
type: git
location: https://github.com/GaloisInc/cryptol.git
- tag: v2.2.4
+ tag: v2.2.5
flag static
default: False
@@ -56,7 +56,7 @@
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,
syb >= 0.4,
text >= 1.1,
diff --git a/dist/build/Cryptol/Parser.hs b/dist/build/Cryptol/Parser.hs
--- a/dist/build/Cryptol/Parser.hs
+++ b/dist/build/Cryptol/Parser.hs
@@ -3735,27 +3735,6 @@
{-# LINE 1 "templates/GenericTemplate.hs" #-}
{-# LINE 1 "templates/GenericTemplate.hs" #-}
{-# LINE 1 "" #-}
-{-# LINE 19 "" #-}
-{-# LINE 1 "/usr/local/Cellar/ghc/7.10.1_1/lib/ghc-7.10.1/include/ghcversion.h" #-}
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-{-# LINE 20 "" #-}
{-# LINE 1 "templates/GenericTemplate.hs" #-}
-- Id: GenericTemplate.hs,v 1.26 2005/01/14 14:47:22 simonmar Exp
diff --git a/dist/build/Cryptol/Parser/Lexer.hs b/dist/build/Cryptol/Parser/Lexer.hs
--- a/dist/build/Cryptol/Parser/Lexer.hs
+++ b/dist/build/Cryptol/Parser/Lexer.hs
@@ -257,27 +257,6 @@
{-# LINE 1 "templates/GenericTemplate.hs" #-}
{-# LINE 1 "templates/GenericTemplate.hs" #-}
{-# LINE 1 "" #-}
-{-# LINE 18 "" #-}
-{-# LINE 1 "/usr/local/Cellar/ghc/7.10.1_1/lib/ghc-7.10.1/include/ghcversion.h" #-}
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-{-# LINE 19 "" #-}
{-# LINE 1 "templates/GenericTemplate.hs" #-}
-- -----------------------------------------------------------------------------
-- ALEX TEMPLATE
diff --git a/src/Cryptol/REPL/Command.hs b/src/Cryptol/REPL/Command.hs
--- a/src/Cryptol/REPL/Command.hs
+++ b/src/Cryptol/REPL/Command.hs
@@ -360,7 +360,6 @@
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 @@
Symbolic.satProve
isSat
mSatNum
- (proverName, iteSolver, verbose)
+ (proverName, verbose)
(M.deDecls denv)
mfile
(expr, schema)
@@ -415,13 +414,12 @@
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 ()
diff --git a/src/Cryptol/REPL/Monad.hs b/src/Cryptol/REPL/Monad.hs
--- a/src/Cryptol/REPL/Monad.hs
+++ b/src/Cryptol/REPL/Monad.hs
@@ -529,8 +529,6 @@
"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)
diff --git a/src/Cryptol/Symbolic.hs b/src/Cryptol/Symbolic.hs
--- a/src/Cryptol/Symbolic.hs
+++ b/src/Cryptol/Symbolic.hs
@@ -41,6 +41,14 @@
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 @@
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 @@
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
@@ -148,13 +156,12 @@
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 @@
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 @@
Nothing -> putStr txt
return (Right (EmptyResult, modEnv), [])
-protectStack :: Bool
- -> M.ModuleCmd ProverResult
+protectStack :: 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 @@
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 @@
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
diff --git a/src/Cryptol/Symbolic/Value.hs b/src/Cryptol/Symbolic/Value.hs
--- a/src/Cryptol/Symbolic/Value.hs
+++ b/src/Cryptol/Symbolic/Value.hs
@@ -23,7 +23,7 @@
, fromVBit, fromVFun, fromVPoly, fromVTuple, fromVRecord, lookupRecord
, fromSeq, fromVWord
, evalPanic
- , iteValue, sBranchValue, mergeValue
+ , iteValue, mergeValue
)
where
@@ -74,15 +74,6 @@
Just True -> x
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 =