Merge branch 'hotfixes/v2.2.5' into releases

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 <http://www.cryptol.net/>.
 License:             BSD3
@@ -23,7 +23,7 @@ source-repository head
 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 @@ 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,
                        syb             >= 0.4,
                        text            >= 1.1,

docs/ProgrammingCryptol/installation/Install.tex

@@ -261,7 +261,6 @@ \subsection{Commands}
      \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} \\

src/Cryptol/REPL/Command.hs

@@ -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 ()

src/Cryptol/REPL/Monad.hs

@@ -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)

src/Cryptol/Symbolic.hs

@@ -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,26 +155,25 @@ 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
     case predArgTypes schema of
       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
-             -> 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 @@ 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

src/Cryptol/Symbolic/Value.hs

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