diff --git a/cryptol.cabal b/cryptol.cabal --- a/cryptol.cabal +++ b/cryptol.cabal @@ -1,5 +1,5 @@ Name: cryptol -Version: 2.2.5 +Version: 2.2.6 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.5 + tag: v2.2.6 flag static default: False @@ -40,7 +40,8 @@ library Default-language: Haskell98 - Build-depends: base >= 4.6 && < 5, + Build-depends: base >= 4.7 && < 5, + base-compat >= 0.6, array >= 0.4, async >= 2.0, containers >= 0.5, @@ -56,7 +57,7 @@ process >= 1.2, QuickCheck >= 2.7, random >= 1.0.1, - sbv (>= 4.3 && < 5.0) || (>= 5.1 && < 5.2), + sbv >= 5.7, smtLib >= 1.0.7, syb >= 0.4, text >= 1.1, 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 @@ -1,3 +1,4 @@ +{-# OPTIONS_GHC -fno-warn-unused-binds -fno-warn-missing-signatures #-} {-# LANGUAGE CPP,MagicHash #-} {-# LINE 1 "src/Cryptol/Parser/Lexer.x" #-} @@ -25,17 +26,17 @@ #endif #if __GLASGOW_HASKELL__ >= 503 import Data.Array -import Data.Char (ord) import Data.Array.Base (unsafeAt) #else import Array -import Char (ord) #endif #if __GLASGOW_HASKELL__ >= 503 import GHC.Exts #else import GlaExts #endif +alex_tab_size :: Int +alex_tab_size = 8 alex_base :: AlexAddr alex_base = AlexA# "\xf8\xff\xff\xff\x6d\x00\x00\x00\x63\x01\x00\x00\x59\x02\x00\x00\xe2\x00\x00\x00\xd9\x02\x00\x00\x59\x03\x00\x00\xd9\x03\x00\x00\x59\x04\x00\x00\xd9\x04\x00\x00\x59\x05\x00\x00\xd9\x05\x00\x00\x59\x06\x00\x00\xd9\x06\x00\x00\x59\x07\x00\x00\xd9\x07\x00\x00\x59\x08\x00\x00\x00\x00\x00\x00\xca\x08\x00\x00\x00\x00\x00\x00\x3b\x09\x00\x00\x00\x00\x00\x00\xac\x09\x00\x00\x00\x00\x00\x00\x1d\x0a\x00\x00\x00\x00\x00\x00\x8e\x0a\x00\x00\x00\x00\x00\x00\xff\x0a\x00\x00\x00\x00\x00\x00\x40\x0b\x00\x00\x00\x00\x00\x00\x81\x0b\x00\x00\x00\x00\x00\x00\xc2\x0b\x00\x00\x00\x00\x00\x00\x03\x0c\x00\x00\x00\x00\x00\x00\x44\x0c\x00\x00\x00\x00\x00\x00\x85\x0c\x00\x00\xe0\xff\xff\xff\xfb\x0c\x00\x00\x48\x00\x00\x00\xd7\xff\xff\xff\xdf\xff\xff\xff\xfb\x0d\x00\x00\xbb\x0d\x00\x00\x00\x00\x00\x00\xbb\x0e\x00\x00\x31\x0f\x00\x00\x7c\x0e\x00\x00\x00\x00\x00\x00\x31\x10\x00\x00\xf1\x0f\x00\x00\x00\x00\x00\x00\xf1\x10\x00\x00\x67\x11\x00\x00\xb2\x10\x00\x00\x00\x00\x00\x00\x67\x12\x00\x00\x27\x12\x00\x00\x00\x00\x00\x00\x27\x13\x00\x00\xe7\x12\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xe2\xff\xff\xff\x00\x00\x00\x00\xe8\xff\xff\xff\x00\x00\x00\x00\xdd\x13\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xd3\x14\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x79\x00\x00\x00\xc9\x15\x00\x00\xa2\x16\x00\x00\x13\x17\x00\x00\x84\x17\x00\x00\xf5\x17\x00\x00\x66\x18\x00\x00\xd7\x18\x00\x00\x48\x19\x00\x00\xb9\x19\x00\x00\x2a\x1a\x00\x00\x9b\x1a\x00\x00\x0c\x1b\x00\x00\x7d\x1b\x00\x00\xee\x1b\x00\x00\x5f\x1c\x00\x00\xd0\x1c\x00\x00\x41\x1d\x00\x00\xb2\x1d\x00\x00\x23\x1e\x00\x00\x94\x1e\x00\x00\x05\x1f\x00\x00\x76\x1f\x00\x00\xe7\x1f\x00\x00\x58\x20\x00\x00\xc9\x20\x00\x00\x3a\x21\x00\x00\xab\x21\x00\x00\x1c\x22\x00\x00\x8d\x22\x00\x00\xfe\x22\x00\x00\x6f\x23\x00\x00\xe0\x23\x00\x00\x51\x24\x00\x00\xc2\x24\x00\x00\x33\x25\x00\x00\xa4\x25\x00\x00\x15\x26\x00\x00\x86\x26\x00\x00\xf7\x26\x00\x00\x68\x27\x00\x00\xd9\x27\x00\x00\x4a\x28\x00\x00\xbb\x28\x00\x00\xe3\xff\xff\xff\x6a\x00\x00\x00\x7f\x00\x00\x00\x34\x02\x00\x00\x4c\x02\x00\x00\x2c\x29\x00\x00\x9d\x29\x00\x00\x0e\x2a\x00\x00\x7f\x2a\x00\x00\xf0\x2a\x00\x00\x61\x2b\x00\x00\xd2\x2b\x00\x00\x43\x2c\x00\x00\xb4\x2c\x00\x00\x25\x2d\x00\x00\x96\x2d\x00\x00\x07\x2e\x00\x00\x78\x2e\x00\x00\xe9\x2e\x00\x00\x5a\x2f\x00\x00\xcb\x2f\x00\x00\x3c\x30\x00\x00\xad\x30\x00\x00\x1e\x31\x00\x00\x8f\x31\x00\x00\x00\x32\x00\x00\x71\x32\x00\x00\xe2\x32\x00\x00\x53\x33\x00\x00\xc4\x33\x00\x00\x35\x34\x00\x00\xa6\x34\x00\x00\x17\x35\x00\x00\x88\x35\x00\x00\xf9\x35\x00\x00\x6a\x36\x00\x00\xdb\x36\x00\x00\x4c\x37\x00\x00\xbd\x37\x00\x00\x2e\x38\x00\x00\x9f\x38\x00\x00\x10\x39\x00\x00\x81\x39\x00\x00\xf2\x39\x00\x00\x63\x3a\x00\x00\xd4\x3a\x00\x00\x45\x3b\x00\x00\xb6\x3b\x00\x00\x27\x3c\x00\x00\x98\x3c\x00\x00\x09\x3d\x00\x00\x7a\x3d\x00\x00\xeb\x3d\x00\x00\x5c\x3e\x00\x00\xcd\x3e\x00\x00\x3e\x3f\x00\x00\xaf\x3f\x00\x00\x20\x40\x00\x00\x91\x40\x00\x00\x02\x41\x00\x00\x73\x41\x00\x00\xe4\x41\x00\x00\x55\x42\x00\x00\xc6\x42\x00\x00\x37\x43\x00\x00\xa8\x43\x00\x00\x19\x44\x00\x00\x8a\x44\x00\x00\xfb\x44\x00\x00\x6c\x45\x00\x00\xdd\x45\x00\x00\x4e\x46\x00\x00\xbf\x46\x00\x00\x30\x47\x00\x00\xa1\x47\x00\x00\x12\x48\x00\x00\x83\x48\x00\x00\xf4\x48\x00\x00\x65\x49\x00\x00\xd6\x49\x00\x00\x47\x4a\x00\x00\xb8\x4a\x00\x00\x29\x4b\x00\x00\x9a\x4b\x00\x00\x0b\x4c\x00\x00\x7c\x4c\x00\x00\xed\x4c\x00\x00\x5e\x4d\x00\x00\xcf\x4d\x00\x00\x40\x4e\x00\x00\xb1\x4e\x00\x00\x22\x4f\x00\x00\x93\x4f\x00\x00\x04\x50\x00\x00\x75\x50\x00\x00\xe6\x50\x00\x00\x57\x51\x00\x00\xc8\x51\x00\x00\x39\x52\x00\x00\xaa\x52\x00\x00\x1b\x53\x00\x00\x8c\x53\x00\x00\xfd\x53\x00\x00\x6e\x54\x00\x00\xdf\x54\x00\x00\x50\x55\x00\x00\xc1\x55\x00\x00\x32\x56\x00\x00\xa3\x56\x00\x00\x14\x57\x00\x00\x85\x57\x00\x00\xf6\x57\x00\x00\x67\x58\x00\x00\xd8\x58\x00\x00\x49\x59\x00\x00\xba\x59\x00\x00\x2b\x5a\x00\x00\x9c\x5a\x00\x00\x0d\x5b\x00\x00\x7e\x5b\x00\x00\xef\x5b\x00\x00\x60\x5c\x00\x00\xd1\x5c\x00\x00\x42\x5d\x00\x00\xb3\x5d\x00\x00\x24\x5e\x00\x00\x95\x5e\x00\x00\x06\x5f\x00\x00\x77\x5f\x00\x00\xe8\x5f\x00\x00\x59\x60\x00\x00\xca\x60\x00\x00\x3b\x61\x00\x00\xac\x61\x00\x00\x1d\x62\x00\x00\x8e\x62\x00\x00\xff\x62\x00\x00\x70\x63\x00\x00\x00\x00\x00\x00\xd8\xff\xff\xff\x00\x00\x00\x00\xed\xff\xff\xff\x00\x00\x00\x00\x00\x00\x00\x00\xfa\xff\xff\xff\x4a\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x52\x00\x00\x00\x5b\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x53\x00\x00\x00\xd9\xff\xff\xff\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x34\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x81\x00\x00\x00\x00\x00\x00\x00\x55\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x66\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x65\x00\x00\x00\x5c\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x77\x00\x00\x00\x00\x00\x00\x00\x68\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00"# @@ -315,8 +316,8 @@ narrow32Int# i where i = word2Int# ((b3 `uncheckedShiftL#` 24#) `or#` - (b2 `uncheckedShiftL#` 16#) `or#` - (b1 `uncheckedShiftL#` 8#) `or#` b0) + (b2 `uncheckedShiftL#` 16#) `or#` + (b1 `uncheckedShiftL#` 8#) `or#` b0) b3 = int2Word# (ord# (indexCharOffAddr# arr (off' +# 3#))) b2 = int2Word# (ord# (indexCharOffAddr# arr (off' +# 2#))) b1 = int2Word# (ord# (indexCharOffAddr# arr (off' +# 1#))) @@ -356,30 +357,30 @@ alexScanUser user input (I# (sc)) = case alex_scan_tkn user input 0# input sc AlexNone of - (AlexNone, input') -> - case alexGetByte input of - Nothing -> + (AlexNone, input') -> + case alexGetByte input of + Nothing -> - AlexEOF - Just _ -> + AlexEOF + Just _ -> - AlexError input' + AlexError input' - (AlexLastSkip input'' len, _) -> + (AlexLastSkip input'' len, _) -> - AlexSkip input'' len + AlexSkip input'' len - (AlexLastAcc k input''' len, _) -> + (AlexLastAcc k input''' len, _) -> - AlexToken input''' len k + AlexToken input''' len k -- Push the input through the DFA, remembering the most recent accepting @@ -388,7 +389,7 @@ alex_scan_tkn user orig_input len input s last_acc = input `seq` -- strict in the input let - new_acc = (check_accs (alex_accept `quickIndex` (I# (s)))) + new_acc = (check_accs (alex_accept `quickIndex` (I# (s)))) in new_acc `seq` case alexGetByte input of @@ -402,23 +403,23 @@ base = alexIndexInt32OffAddr alex_base s offset = (base +# ord_c) check = alexIndexInt16OffAddr alex_check offset - + new_s = if GTE(offset,0#) && EQ(check,ord_c) - then alexIndexInt16OffAddr alex_table offset - else alexIndexInt16OffAddr alex_deflt s - in + then alexIndexInt16OffAddr alex_table offset + else alexIndexInt16OffAddr alex_deflt s + in case new_s of - -1# -> (new_acc, input) - -- on an error, we want to keep the input *before* the - -- character that failed, not after. - _ -> alex_scan_tkn user orig_input (if c < 0x80 || c >= 0xC0 then (len +# 1#) else len) + -1# -> (new_acc, input) + -- on an error, we want to keep the input *before* the + -- character that failed, not after. + _ -> alex_scan_tkn user orig_input (if c < 0x80 || c >= 0xC0 then (len +# 1#) else len) -- note that the length is increased ONLY if this is the 1st byte in a char encoding) - new_input new_s new_acc + new_input new_s new_acc } where - check_accs (AlexAccNone) = last_acc - check_accs (AlexAcc a ) = AlexLastAcc a input (I# (len)) - check_accs (AlexAccSkip) = AlexLastSkip input (I# (len)) + check_accs (AlexAccNone) = last_acc + check_accs (AlexAcc a ) = AlexLastAcc a input (I# (len)) + check_accs (AlexAccSkip) = AlexLastSkip input (I# (len)) {-# LINE 198 "templates/GenericTemplate.hs" #-} @@ -428,17 +429,12 @@ | AlexLastSkip !AlexInput !Int instance Functor AlexLastAcc where - fmap f AlexNone = AlexNone + fmap _ AlexNone = AlexNone fmap f (AlexLastAcc x y z) = AlexLastAcc (f x) y z - fmap f (AlexLastSkip x y) = AlexLastSkip x y + fmap _ (AlexLastSkip x y) = AlexLastSkip x y data AlexAcc a user = AlexAccNone | AlexAcc a | AlexAccSkip - -{-# LINE 242 "templates/GenericTemplate.hs" #-} - --- used by wrappers -iUnbox (I# (i)) = i 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 @@ -54,6 +54,7 @@ import qualified Cryptol.Parser.AST as P import Cryptol.Prims.Doc(helpDoc) import qualified Cryptol.Transform.Specialize as S +import Cryptol.Symbolic (ProverCommand(..), QueryType(..), SatNum(..)) import qualified Cryptol.Symbolic as Symbolic import Control.DeepSeq @@ -336,9 +337,10 @@ satCmd = cmdProveSat True proveCmd = cmdProveSat False --- | Run a SAT solver on the given expression. Binds the @it@ variable --- to a record whose form depends on the expression given. See ticket --- #66 for a discussion of this design. +-- | Console-specific version of 'proveSat'. Prints output to the +-- console, and binds the @it@ variable to a record whose form depends +-- on the expression given. See ticket #66 for a discussion of this +-- design. cmdProveSat :: Bool -> String -> REPL () cmdProveSat isSat "" = do xs <- getPropertyNames @@ -349,81 +351,104 @@ then rPutStr $ ":sat " ++ x ++ "\n\t" else rPutStr $ ":prove " ++ x ++ "\n\t" cmdProveSat isSat x -cmdProveSat isSat str = do +cmdProveSat isSat expr = do + let cexStr | isSat = "satisfying assignment" + | otherwise = "counterexample" EnvString proverName <- getUser "prover" EnvString fileName <- getUser "smtfile" let mfile = if fileName == "-" then Nothing else Just fileName case proverName of - "offline" -> offlineProveSat isSat str mfile - _ -> onlineProveSat isSat str proverName mfile + "offline" -> do + result <- offlineProveSat isSat expr mfile + case result of + Left msg -> rPutStrLn msg + Right smtlib -> do + let filename = fromMaybe "standard output" mfile + let satWord | isSat = "satisfiability" + | otherwise = "validity" + rPutStrLn $ + "Writing to SMT-Lib file " ++ filename ++ "..." + rPutStrLn $ + "To determine the " ++ satWord ++ + " of the expression, use an external SMT solver." + case mfile of + Just path -> io $ writeFile path smtlib + Nothing -> rPutStr smtlib + _ -> do + result <- onlineProveSat isSat expr proverName mfile + ppOpts <- getPPValOpts + case result of + Symbolic.EmptyResult -> + panic "REPL.Command" [ "got EmptyResult for online prover query" ] + Symbolic.ProverError msg -> rPutStrLn msg + Symbolic.ThmResult ts -> do + rPutStrLn (if isSat then "Unsatisfiable" else "Q.E.D.") + let (t, e) = mkSolverResult cexStr (not isSat) (Left ts) + bindItVariable t e + Symbolic.AllSatResult tevss -> do + let tess = map (map $ \(t,e,_) -> (t,e)) tevss + vss = map (map $ \(_,_,v) -> v) tevss + ppvs vs = do + parseExpr <- replParseExpr expr + let docs = map (pp . E.WithBase ppOpts) vs + -- function application has precedence 3 + doc = ppPrec 3 parseExpr + rPrint $ hsep (doc : docs) <+> + text (if isSat then "= True" else "= False") + resultRecs = map (mkSolverResult cexStr isSat . Right) tess + collectTes tes = (t, es) + where + (ts, es) = unzip tes + t = case nub ts of + [t'] -> t' + _ -> panic "REPL.Command.onlineProveSat" + [ "satisfying assignments with different types" ] + (ty, exprs) = + case resultRecs of + [] -> panic "REPL.Command.onlineProveSat" + [ "no satisfying assignments after mkSovlerResult" ] + [(t, e)] -> (t, [e]) + _ -> collectTes resultRecs + forM_ vss ppvs + case (ty, exprs) of + (t, [e]) -> bindItVariable t e + (t, es ) -> bindItVariables t es onlineProveSat :: Bool - -> String -> String -> Maybe FilePath -> REPL () + -> String -> String -> Maybe FilePath -> REPL Symbolic.ProverResult onlineProveSat isSat str proverName mfile = do EnvBool verbose <- getUser "debug" - mSatNum <- getUserSatNum - let cexStr | isSat = "satisfying assignment" - | otherwise = "counterexample" + satNum <- getUserSatNum parseExpr <- replParseExpr str (expr, schema) <- replCheckExpr parseExpr - denv <- getDynEnv - result <- liftModuleCmd $ - Symbolic.satProve - isSat - mSatNum - (proverName, verbose) - (M.deDecls denv) - mfile - (expr, schema) - ppOpts <- getPPValOpts - case result of - Symbolic.EmptyResult -> - panic "REPL.Command" [ "got EmptyResult for online prover query" ] - Symbolic.ProverError msg -> rPutStrLn msg - Symbolic.ThmResult ts -> do - rPutStrLn (if isSat then "Unsatisfiable" else "Q.E.D.") - let (t, e) = mkSolverResult cexStr (not isSat) (Left ts) - bindItVariable t e - Symbolic.AllSatResult tevss -> do - let tess = map (map $ \(t,e,_) -> (t,e)) tevss - vss = map (map $ \(_,_,v) -> v) tevss - ppvs vs = do - let docs = map (pp . E.WithBase ppOpts) vs - -- function application has precedence 3 - doc = ppPrec 3 parseExpr - rPrint $ hsep (doc : docs) <+> - text (if isSat then "= True" else "= False") - resultRecs = map (mkSolverResult cexStr isSat . Right) tess - collectTes tes = (t, es) - where - (ts, es) = unzip tes - t = case nub ts of - [t'] -> t' - _ -> panic "REPL.Command.onlineProveSat" - [ "satisfying assignments with different types" ] - (ty, exprs) = - case resultRecs of - [] -> panic "REPL.Command.onlineProveSat" - [ "no satisfying assignments after mkSovlerResult" ] - [(t, e)] -> (t, [e]) - _ -> collectTes resultRecs - forM_ vss ppvs - case (ty, exprs) of - (t, [e]) -> bindItVariable t e - (t, es ) -> bindItVariables t es + decls <- fmap M.deDecls getDynEnv + let cmd = Symbolic.ProverCommand { + pcQueryType = if isSat then SatQuery satNum else ProveQuery + , pcProverName = proverName + , pcVerbose = verbose + , pcExtraDecls = decls + , pcSmtFile = mfile + , pcExpr = expr + , pcSchema = schema + } + liftModuleCmd $ Symbolic.satProve cmd -offlineProveSat :: Bool -> String -> Maybe FilePath -> REPL () +offlineProveSat :: Bool -> String -> Maybe FilePath -> REPL (Either String String) offlineProveSat isSat str mfile = do - EnvBool vrb <- getUser "debug" + EnvBool verbose <- getUser "debug" parseExpr <- replParseExpr str - exsch <- replCheckExpr parseExpr + (expr, schema) <- replCheckExpr parseExpr decls <- fmap M.deDecls getDynEnv - result <- liftModuleCmd $ - Symbolic.satProveOffline isSat vrb decls mfile exsch - case result of - Symbolic.ProverError msg -> rPutStrLn msg - Symbolic.EmptyResult -> return () - _ -> panic "REPL.Command" [ "unexpected prover result for offline prover" ] + let cmd = Symbolic.ProverCommand { + pcQueryType = if isSat then SatQuery (SomeSat 0) else ProveQuery + , pcProverName = "offline" + , pcVerbose = verbose + , pcExtraDecls = decls + , pcSmtFile = mfile + , pcExpr = expr + , pcSchema = schema + } + liftModuleCmd $ Symbolic.satProveOffline cmd -- | Make a type/expression pair that is suitable for binding to @it@ -- after running @:sat@ or @:prove@ 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 @@ -80,7 +80,7 @@ import Cryptol.Utils.PP import Cryptol.Utils.Panic (panic) import qualified Cryptol.Parser.AST as P -import Cryptol.Symbolic (proverNames, lookupProver) +import Cryptol.Symbolic (proverNames, lookupProver, SatNum(..)) import Control.Monad (ap,unless,when) import Data.IORef @@ -527,7 +527,7 @@ "The number of random tests to try." , simpleOpt "satNum" (EnvString "1") checkSatNum "The maximum number of :sat solutions to display (\"all\" for no limit)." - , simpleOpt "prover" (EnvString "cvc4") checkProver $ + , simpleOpt "prover" (EnvString "z3") checkProver $ "The external SMT solver for :prove and :sat (" ++ proverListString ++ ")." , simpleOpt "warnDefaulting" (EnvBool True) (const $ return Nothing) "Choose if we should display warnings when defaulting." @@ -582,12 +582,12 @@ _ -> return $ Just "must be an integer > 0 or \"all\"" _ -> return $ Just "unable to parse a value for satNum" -getUserSatNum :: REPL (Maybe Int) +getUserSatNum :: REPL SatNum getUserSatNum = do EnvString s <- getUser "satNum" case s of - "all" -> return Nothing - _ | Just n <- readMaybe s -> return (Just n) + "all" -> return AllSat + _ | Just n <- readMaybe s -> return (SomeSat n) _ -> panic "REPL.Monad.getUserSatNum" [ "invalid satNum option" ] @@ -603,25 +603,25 @@ smokeTest :: REPL [Smoke] smokeTest = catMaybes <$> sequence tests where - tests = [ cvc4exists ] + tests = [ z3exists ] type SmokeTest = REPL (Maybe Smoke) data Smoke - = CVC4NotFound + = Z3NotFound deriving (Show, Eq) instance PP Smoke where ppPrec _ smoke = case smoke of - CVC4NotFound -> text . intercalate " " $ [ - "[error] cvc4 is required to run Cryptol, but was not found in the" - , "system path. See the Cryptol README for more on how to install cvc4." + Z3NotFound -> text . intercalate " " $ [ + "[error] z3 is required to run Cryptol, but was not found in the" + , "system path. See the Cryptol README for more on how to install z3." ] -cvc4exists :: SmokeTest -cvc4exists = do - mPath <- io $ findExecutable "cvc4" +z3exists :: SmokeTest +z3exists = do + mPath <- io $ findExecutable "z3" case mPath of - Nothing -> return (Just CVC4NotFound) + Nothing -> return (Just Z3NotFound) Just _ -> return Nothing diff --git a/src/Cryptol/Symbolic.hs b/src/Cryptol/Symbolic.hs --- a/src/Cryptol/Symbolic.hs +++ b/src/Cryptol/Symbolic.hs @@ -6,23 +6,24 @@ -- Stability : provisional -- Portability : portable +{-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE PatternGuards #-} +{-# LANGUAGE RecordWildCards #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TupleSections #-} module Cryptol.Symbolic where import Control.Monad (replicateM, when, zipWithM) -import Control.Monad.IO.Class import Data.List (transpose, intercalate) import qualified Data.Map as Map -import Data.Maybe import qualified Control.Exception as X import qualified Data.SBV.Dynamic as SBV import qualified Cryptol.ModuleSystem as M import qualified Cryptol.ModuleSystem.Env as M +import qualified Cryptol.ModuleSystem.Monad as M import Cryptol.Symbolic.Prims import Cryptol.Symbolic.Value @@ -75,6 +76,30 @@ type SatResult = [(Type, Expr, Eval.Value)] +data SatNum = AllSat | SomeSat Int + deriving (Show) + +data QueryType = SatQuery SatNum | ProveQuery + deriving (Show) + +data ProverCommand = ProverCommand { + pcQueryType :: QueryType + -- ^ The type of query to run + , pcProverName :: String + -- ^ Which prover to use (one of the strings in 'proverConfigs') + , pcVerbose :: Bool + -- ^ Verbosity flag passed to SBV + , pcExtraDecls :: [DeclGroup] + -- ^ Extra declarations to bring into scope for symbolic + -- simulation + , pcSmtFile :: Maybe FilePath + -- ^ Optionally output the SMTLIB query to a file + , pcExpr :: Expr + -- ^ The typechecked expression to evaluate + , pcSchema :: Schema + -- ^ The 'Schema' of @pcExpr@ + } + -- | A prover result is either an error message, an empty result (eg -- for the offline prover), a counterexample or a lazy list of -- satisfying assignments. @@ -83,42 +108,65 @@ | EmptyResult | ProverError String +satSMTResults :: SBV.SatResult -> [SBV.SMTResult] +satSMTResults (SBV.SatResult r) = [r] + allSatSMTResults :: SBV.AllSatResult -> [SBV.SMTResult] allSatSMTResults (SBV.AllSatResult (_, rs)) = rs thmSMTResults :: SBV.ThmResult -> [SBV.SMTResult] thmSMTResults (SBV.ThmResult r) = [r] -satProve :: Bool - -> Maybe Int -- ^ satNum - -> (String, Bool) - -> [DeclGroup] - -> Maybe FilePath - -> (Expr, Schema) - -> M.ModuleCmd ProverResult -satProve isSat mSatNum (proverName, verbose) edecls mfile (expr, schema) = protectStack $ \modEnv -> do - let extDgs = allDeclGroups modEnv ++ edecls +proverError :: String -> M.ModuleCmd ProverResult +proverError msg modEnv = return (Right (ProverError msg, modEnv), []) + +satProve :: ProverCommand -> M.ModuleCmd ProverResult +satProve ProverCommand {..} = protectStack proverError $ \modEnv -> + M.runModuleM modEnv $ do + let (isSat, mSatNum) = case pcQueryType of + ProveQuery -> (False, Nothing) + SatQuery sn -> case sn of + SomeSat n -> (True, Just n) + AllSat -> (True, Nothing) + let extDgs = allDeclGroups modEnv ++ pcExtraDecls provers <- - case proverName of - "any" -> SBV.sbvAvailableSolvers - _ -> return [(lookupProver proverName) { SBV.smtFile = mfile }] - let provers' = [ p { SBV.timing = verbose, SBV.verbose = verbose } | p <- provers ] + case pcProverName of + "any" -> M.io SBV.sbvAvailableSolvers + _ -> return [(lookupProver pcProverName) { SBV.smtFile = pcSmtFile }] + let provers' = [ p { SBV.timing = pcVerbose, SBV.verbose = pcVerbose } | p <- provers ] let tyFn = if isSat then existsFinType else forallFinType let runProver fn tag e = do - when verbose $ liftIO $ + case provers of + [prover] -> do + when pcVerbose $ M.io $ + putStrLn $ "Trying proof with " ++ show prover + res <- M.io (fn prover e) + when pcVerbose $ M.io $ + putStrLn $ "Got result from " ++ show prover + return (tag res) + _ -> + return [ SBV.ProofError + prover + [":sat with option prover=any requires option satNum=1"] + | prover <- provers ] + runProvers fn tag e = do + when pcVerbose $ M.io $ putStrLn $ "Trying proof with " ++ intercalate ", " (map show provers) - (firstProver, res) <- fn provers' e - when verbose $ liftIO $ + (firstProver, res) <- M.io $ fn provers' e + when pcVerbose $ M.io $ putStrLn $ "Got result from " ++ show firstProver return (tag res) - let runFn | isSat = runProver SBV.allSatWithAny allSatSMTResults - | otherwise = runProver SBV.proveWithAny thmSMTResults - case predArgTypes schema of - Left msg -> return (Right (ProverError msg, modEnv), []) - Right ts -> do when verbose $ putStrLn "Simulating..." - let env = evalDecls emptyEnv extDgs - let v = evalExpr env expr + let runFn = case pcQueryType of + ProveQuery -> runProvers SBV.proveWithAny thmSMTResults + SatQuery sn -> case sn of + SomeSat 1 -> runProvers SBV.satWithAny satSMTResults + _ -> runProver SBV.allSatWith allSatSMTResults + case predArgTypes pcSchema of + Left msg -> return (ProverError msg) + Right ts -> do when pcVerbose $ M.io $ putStrLn "Simulating..." + let env = evalDecls mempty extDgs + let v = evalExpr env pcExpr results' <- runFn $ do args <- mapM tyFn ts b <- return $! fromVBit (foldl fromVFun v args) @@ -152,48 +200,37 @@ | otherwise = show . SBV.ThmResult . head boom = panic "Cryptol.Symbolic.sat" [ "attempted to evaluate bogus boolean for pretty-printing" ] - return (Right (esatexprs, modEnv), []) + return esatexprs -satProveOffline :: Bool - -> Bool - -> [DeclGroup] - -> Maybe FilePath - -> (Expr, Schema) - -> M.ModuleCmd ProverResult -satProveOffline isSat vrb edecls mfile (expr, schema) = - protectStack $ \modEnv -> do - let extDgs = allDeclGroups modEnv ++ edecls +satProveOffline :: ProverCommand -> M.ModuleCmd (Either String String) +satProveOffline ProverCommand {..} = + protectStack (\msg modEnv -> return (Right (Left msg, modEnv), [])) $ \modEnv -> do + let isSat = case pcQueryType of + ProveQuery -> False + SatQuery _ -> True + let extDgs = allDeclGroups modEnv ++ pcExtraDecls 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), []) + case predArgTypes pcSchema of + Left msg -> return (Right (Left msg, modEnv), []) Right ts -> - do when vrb $ putStrLn "Simulating..." - let env = evalDecls emptyEnv extDgs - let v = evalExpr env expr - let satWord | isSat = "satisfiability" - | otherwise = "validity" - txt <- SBV.compileToSMTLib smtMode isSat $ do - args <- mapM tyFn ts - b <- return $! fromVBit (foldl fromVFun v args) - liftIO $ putStrLn $ - "Writing to SMT-Lib file " ++ filename ++ "..." - return b - liftIO $ putStrLn $ - "To determine the " ++ satWord ++ - " of the expression, use an external SMT solver." - case mfile of - Just path -> writeFile path txt - Nothing -> putStr txt - return (Right (EmptyResult, modEnv), []) + do when pcVerbose $ putStrLn "Simulating..." + let env = evalDecls mempty extDgs + let v = evalExpr env pcExpr + smtlib <- SBV.compileToSMTLib SBV.SMTLib2 isSat $ do + args <- mapM tyFn ts + b <- return $! fromVBit (foldl fromVFun v args) + return b + return (Right (Right smtlib, modEnv), []) -protectStack :: M.ModuleCmd ProverResult - -> M.ModuleCmd ProverResult -protectStack cmd modEnv = X.catchJust isOverflow (cmd modEnv) handler +protectStack :: (String -> M.ModuleCmd a) + -> M.ModuleCmd a + -> M.ModuleCmd a +protectStack mkErr cmd modEnv = + X.catchJust isOverflow (cmd modEnv) handler where isOverflow X.StackOverflow = Just () isOverflow _ = Nothing msg = "Symbolic evaluation failed to terminate." - handler () = return (Right (ProverError msg, modEnv), []) + handler () = mkErr msg modEnv parseValues :: [FinType] -> [SBV.CW] -> ([Eval.Value], [SBV.CW]) parseValues [] cws = ([], cws) @@ -378,7 +415,8 @@ _ -> panic "Cryptol.Symbolic.evalSel" [ "Record selector applied to non-record" ] ListSel n _ -> case v of - VWord s -> VBit (SBV.svTestBit s n) + VWord s -> VBit (SBV.svTestBit s i) + where i = SBV.intSizeOf s - 1 - n _ -> fromSeq v !! n -- 0-based indexing -- Declarations ---------------------------------------------------------------- diff --git a/src/Cryptol/Symbolic/Prims.hs b/src/Cryptol/Symbolic/Prims.hs --- a/src/Cryptol/Symbolic/Prims.hs +++ b/src/Cryptol/Symbolic/Prims.hs @@ -25,9 +25,8 @@ import qualified Data.SBV.Dynamic as SBV -#if __GLASGOW_HASKELL__ < 710 -import Control.Applicative -#endif +import Prelude () +import Prelude.Compat traverseSnd :: Functor f => (a -> f b) -> (t, a) -> f (t, b) traverseSnd f (x, y) = (,) x <$> f y @@ -317,7 +316,7 @@ case v of VStream xs -> nth err xs (fromInteger n) VSeq _ xs -> nth err xs (fromInteger n) - VWord x -> let i = SBV.svBitSize x - 1 - fromInteger n + VWord x -> let i = SBV.intSizeOf x - 1 - fromInteger n in if i < 0 then err else VBit (SBV.svTestBit x i) _ -> err @@ -342,13 +341,13 @@ case xs of VSeq b xs' -> VSeq b (genericDrop n xs') VStream xs' -> VStream (genericDrop n xs') - VWord w -> VWord $ SBV.svExtract (SBV.svBitSize w - 1 - fromInteger n) 0 w + VWord w -> VWord $ SBV.svExtract (SBV.intSizeOf w - 1 - fromInteger n) 0 w _ -> panic "Cryptol.Symbolic.Prims.dropV" [ "non-droppable value" ] takeV :: Integer -> Value -> Value takeV n xs = case xs of - VWord w -> VWord $ SBV.svExtract (SBV.svBitSize w - 1) (SBV.svBitSize w - fromInteger n) w + VWord w -> VWord $ SBV.svExtract (SBV.intSizeOf w - 1) (SBV.intSizeOf w - fromInteger n) w VSeq b xs' -> VSeq b (genericTake n xs') VStream xs' -> VSeq b (genericTake n xs') where b = case xs' of VBit _ : _ -> True @@ -425,7 +424,7 @@ sExp :: SWord -> SWord -> SWord sExp x y = go (reverse (unpackWord y)) -- bits in little-endian order - where go [] = literalSWord (SBV.svBitSize x) 1 + where go [] = literalSWord (SBV.intSizeOf x) 1 go (b : bs) = SBV.svIte b (SBV.svTimes x s) s where a = go bs s = SBV.svTimes a a @@ -434,8 +433,8 @@ sLg2 :: SWord -> SWord sLg2 x = go 0 where - lit n = literalSWord (SBV.svBitSize x) n - go i | i < SBV.svBitSize x = SBV.svIte (SBV.svLessEq x (lit (2^i))) (lit (toInteger i)) (go (i + 1)) + lit n = literalSWord (SBV.intSizeOf x) n + go i | i < SBV.intSizeOf x = SBV.svIte (SBV.svLessEq x (lit (2^i))) (lit (toInteger i)) (go (i + 1)) | otherwise = lit (toInteger i) -- Cmp ------------------------------------------------------------------------- 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 @@ -92,7 +92,7 @@ [ "mergeValue: incompatible values" ] where mergeBit b1 b2 = svSymbolicMerge KBool f c b1 b2 - mergeWord w1 w2 = svSymbolicMerge (svKind w1) f c w1 w2 + mergeWord w1 w2 = svSymbolicMerge (kindOf w1) f c w1 w2 mergeField (n1, x1) (n2, x2) | n1 == n2 = (n1, mergeValue f c x1 x2) | otherwise = panic "Cryptol.Symbolic.Value" @@ -104,7 +104,7 @@ instance BitWord SBool SWord where packWord bs = fromBitsLE (reverse bs) - unpackWord x = [ svTestBit x i | i <- reverse [0 .. svBitSize x - 1] ] + unpackWord x = [ svTestBit x i | i <- reverse [0 .. intSizeOf x - 1] ] -- Errors ---------------------------------------------------------------------- diff --git a/src/Cryptol/TypeCheck/Solver/Smtlib.hs b/src/Cryptol/TypeCheck/Solver/Smtlib.hs --- a/src/Cryptol/TypeCheck/Solver/Smtlib.hs +++ b/src/Cryptol/TypeCheck/Solver/Smtlib.hs @@ -45,7 +45,7 @@ asmps = mapMaybe toPred (ordFactsToProps ordAsmp ++ origAsmps) tryGoal g = case toPred (goal g) of - Just q -> do res <- cvc4 (toScript vs asmps q) + Just q -> do res <- z3 (toScript vs asmps q) return (g, res == Unsat) -- i.e., solved for Nats, anyway Nothing -> return (g, False) @@ -124,35 +124,35 @@ data SMTResult = Sat | Unsat | Unknown deriving (Eq,Show) --- | First look for @cvc4@ in the path, but failing that, assume that it's +-- | First look for @z3@ in the path, but failing that, assume that it's -- installed side-by-side with Cryptol. -findCvc4 :: IO FilePath -findCvc4 = do - mfp <- findExecutable "cvc4" +findZ3 :: IO FilePath +findZ3 = do + mfp <- findExecutable "z3" case mfp of Just fp -> return fp Nothing -> do bindir <- takeDirectory `fmap` getExecutablePath - return (bindir "cvc4") + return (bindir "z3") -cvc4 :: SMT.Script -> IO SMTResult -cvc4 script = +z3 :: SMT.Script -> IO SMTResult +z3 script = X.handle (\(_::X.IOException) -> return Unknown) $ do let txt = show (SMT.pp script) - cvc4path <- findCvc4 - (ex,out,err) <- readProcessWithExitCode cvc4path ["--lang=smtlib2","--rewrite-divk","-"] txt + z3path <- findZ3 + (ex,out,err) <- readProcessWithExitCode z3path ["-smt2","-in"] txt case ex of ExitFailure 10 -> return Sat ExitFailure 20 -> return Unsat - ExitFailure 127 -> return Unknown -- cvc4 program not found + ExitFailure 127 -> return Unknown -- z3 program not found ExitSuccess | out == "sat\n" -> return Sat | out == "unsat\n" -> return Unsat - | out == "unknwon\n" -> return Unknown + | out == "unknown\n" -> return Unknown -- XXX: We should not print to STDOUT here. -- Report to a separate logger. - x -> do putStrLn "Called to CVC4 failed!!!" + x -> do putStrLn "Called to Z3 failed!!!" putStrLn ("Exit code: " ++ show x) putStrLn "Script" putStrLn txt