cryptol 2.2.4 → 2.2.5

raw patch · 7 files changed

+27/−83 lines, 7 filesdep ~sbvPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependency ranges changed: sbv

API changes (from Hackage documentation)

Files

• cryptol.cabal +3/−3
• dist/build/Cryptol/Parser.hs +0/−21
• dist/build/Cryptol/Parser/Lexer.hs +0/−21
• src/Cryptol/REPL/Command.hs +2/−4
• src/Cryptol/REPL/Monad.hs +0/−2
• src/Cryptol/Symbolic.hs +21/−22
• src/Cryptol/Symbolic/Value.hs +1/−10

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

@@ -3735,27 +3735,6 @@ {-# LINE 1 "templates/GenericTemplate.hs" #-} {-# LINE 1 "templates/GenericTemplate.hs" #-} {-# LINE 1 "<built-in>" #-}-{-# LINE 19 "<built-in>" #-}-{-# LINE 1 "/usr/local/Cellar/ghc/7.10.1_1/lib/ghc-7.10.1/include/ghcversion.h" #-}-------------------{-# LINE 20 "<built-in>" #-} {-# LINE 1 "templates/GenericTemplate.hs" #-} -- Id: GenericTemplate.hs,v 1.26 2005/01/14 14:47:22 simonmar Exp  

@@ -257,27 +257,6 @@ {-# LINE 1 "templates/GenericTemplate.hs" #-} {-# LINE 1 "templates/GenericTemplate.hs" #-} {-# LINE 1 "<built-in>" #-}-{-# LINE 18 "<built-in>" #-}-{-# LINE 1 "/usr/local/Cellar/ghc/7.10.1_1/lib/ghc-7.10.1/include/ghcversion.h" #-}-------------------{-# LINE 19 "<built-in>" #-} {-# LINE 1 "templates/GenericTemplate.hs" #-} -- ----------------------------------------------------------------------------- -- ALEX TEMPLATE

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

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

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

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