cryptol 2.2.5 → 2.2.6

raw patch · 8 files changed

+260/−201 lines, 8 filesdep +base-compatdep ~basedep ~sbvPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependencies added: base-compat

Dependency ranges changed: base, sbv

API changes (from Hackage documentation)

Files

• cryptol.cabal +5/−4
• dist/build/Cryptol/Parser/Lexer.hs +30/−34
• src/Cryptol/REPL/Command.hs +89/−64
• src/Cryptol/REPL/Monad.hs +14/−14
• src/Cryptol/Symbolic.hs +99/−61
• src/Cryptol/Symbolic/Prims.hs +8/−9
• src/Cryptol/Symbolic/Value.hs +2/−2
• src/Cryptol/TypeCheck/Solver/Smtlib.hs +13/−13

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

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

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

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

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

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

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

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