cryptol 2.2.2 → 2.2.3

raw patch · 28 files changed

+311/−404 lines, 28 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 +7/−6
• cryptol/Main.hs +4/−1
• cryptol/OptParser.hs +5/−1
• dist/build/Cryptol/Parser.hs +21/−0
• dist/build/Cryptol/Parser/Lexer.hs +21/−0
• src/Cryptol/Eval.hs +3/−1
• src/Cryptol/Eval/Env.hs +3/−4
• src/Cryptol/ModuleSystem/Base.hs +4/−1
• src/Cryptol/ModuleSystem/Env.hs +5/−1
• src/Cryptol/ModuleSystem/Interface.hs +3/−1
• src/Cryptol/ModuleSystem/Monad.hs +3/−1
• src/Cryptol/ModuleSystem/NamingEnv.hs +4/−2
• src/Cryptol/ModuleSystem/Renamer.hs +5/−3
• src/Cryptol/Parser/AST.hs +4/−1
• src/Cryptol/Parser/NoPat.hs +4/−2
• src/Cryptol/Parser/ParserUtils.hs +8/−4
• src/Cryptol/REPL/Command.hs +4/−31
• src/Cryptol/REPL/Monad.hs +6/−4
• src/Cryptol/Symbolic.hs +19/−17
• src/Cryptol/Symbolic/BitVector.hs +0/−205
• src/Cryptol/Symbolic/Prims.hs +78/−76
• src/Cryptol/Symbolic/Value.hs +80/−36
• src/Cryptol/Testing/Exhaust.hs +4/−1
• src/Cryptol/Transform/MonoValues.hs +4/−1
• src/Cryptol/Transform/Specialize.hs +4/−2
• src/Cryptol/TypeCheck/Monad.hs +3/−0
• src/Cryptol/TypeCheck/Solver/Smtlib.hs +1/−1
• src/Cryptol/TypeCheck/Unify.hs +4/−1

@@ -1,5 +1,5 @@ Name:                cryptol-Version:             2.2.2+Version:             2.2.3 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.2+  tag:      v2.2.3  flag static   default: False@@ -56,7 +56,7 @@                        process         >= 1.2,                        QuickCheck      >= 2.7,                        random          >= 1.0.1,-                       sbv             >= 4.2 && < 4.3,+                       sbv             >= 4.3,                        smtLib          >= 1.0.7,                        syb             >= 0.4,                        text            >= 1.1,@@ -138,7 +138,6 @@                        Cryptol.Testing.Random,                         Cryptol.Symbolic,-                       Cryptol.Symbolic.BitVector,                        Cryptol.Symbolic.Prims,                        Cryptol.Symbolic.Value, @@ -152,8 +151,9 @@                        Paths_cryptol,                        GitRev +  default-extensions:  CPP   GHC-options:         -Wall -O2-  ghc-prof-options: -fprof-auto -prof+  ghc-prof-options:    -fprof-auto -prof    if flag(relocatable)       cpp-options: -DRELOCATABLE@@ -185,8 +185,9 @@                      , sbv                      , tf-random                      , transformers+  default-extensions:  CPP   GHC-options:         -Wall -O2-  ghc-prof-options: -auto-all -prof -rtsopts+  ghc-prof-options:    -auto-all -prof -rtsopts    if os(linux) && flag(static)       ld-options:      -static -pthread

@@ -27,13 +27,16 @@ import Paths_cryptol (version)  import Data.Version (showVersion)-import Data.Monoid (mconcat) import GHC.IO.Encoding (setLocaleEncoding, utf8) import System.Console.GetOpt     (OptDescr(..),ArgOrder(..),ArgDescr(..),getOpt,usageInfo) import System.Environment (getArgs, getProgName, lookupEnv) import System.Exit (exitFailure) import System.FilePath (searchPathSeparator, splitSearchPath, takeDirectory)++#if __GLASGOW_HASKELL__ < 710+import Data.Monoid (mconcat)+#endif  data Options = Options   { optLoad            :: [FilePath]

@@ -9,7 +9,11 @@  module OptParser where -import Data.Monoid (Endo(..),Monoid(..))+import Data.Monoid (Endo(..))++#if __GLASGOW_HASKELL__ < 710+import Data.Monoid (Monoid(..))+#endif  data OptParser opt   = OptSuccess (Endo opt)

@@ -3735,6 +3735,27 @@ {-# 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/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,6 +257,27 @@ {-# 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/lib/ghc-7.10.1/include/ghcversion.h" #-}+++++++++++++++++++{-# LINE 19 "<built-in>" #-} {-# LINE 1 "templates/GenericTemplate.hs" #-} -- ----------------------------------------------------------------------------- -- ALEX TEMPLATE

@@ -29,9 +29,11 @@ import Cryptol.Prims.Eval  import Data.List (transpose)-import Data.Monoid (Monoid(..),mconcat) import qualified Data.Map as Map +#if __GLASGOW_HASKELL__ < 710+import Data.Monoid (Monoid(..),mconcat)+#endif  -- Expression Evaluation ------------------------------------------------------- 

@@ -15,9 +15,11 @@ import Cryptol.TypeCheck.AST import Cryptol.Utils.PP -import           Data.Monoid (Monoid(..)) import qualified Data.Map as Map +#if __GLASGOW_HASKELL__ < 710+import           Data.Monoid (Monoid(..))+#endif  -- Evaluation Environment ------------------------------------------------------ @@ -62,6 +64,3 @@ -- | Lookup a type variable. lookupType :: TVar -> EvalEnv -> Maybe TValue lookupType p env = Map.lookup p (envTypes env)---

@@ -33,7 +33,6 @@ import Control.DeepSeq import qualified Control.Exception as X import Control.Monad (unless)-import Data.Foldable (foldMap) import Data.Function (on) import Data.List (nubBy) import Data.Maybe (mapMaybe,fromMaybe)@@ -48,6 +47,10 @@                        ) import qualified System.IO.Error as IOE import qualified Data.Map as Map++#if __GLASGOW_HASKELL__ < 710+import Data.Foldable (foldMap)+#endif  -- Renaming -------------------------------------------------------------------- 

@@ -26,11 +26,15 @@ import Data.Foldable (fold) import Data.Function (on) import qualified Data.Map as Map-import Data.Monoid ((<>), Monoid(..))+import Data.Monoid ((<>)) import System.Directory (getAppUserDataDirectory, getCurrentDirectory) import System.Environment(getExecutablePath) import System.FilePath ((</>), normalise, joinPath, splitPath, takeDirectory) import qualified Data.List as List++#if __GLASGOW_HASKELL__ < 710+import Data.Monoid (Monoid(..))+#endif  -- Module Environment ---------------------------------------------------------- 

@@ -24,8 +24,10 @@ import           Cryptol.TypeCheck.AST  import qualified Data.Map as Map-import           Data.Monoid (Monoid(..)) +#if __GLASGOW_HASKELL__ < 710+import           Data.Monoid (Monoid(..))+#endif  -- | The resulting interface generated by a module that has been typechecked. data Iface = Iface

@@ -25,12 +25,14 @@ import           Cryptol.Parser.Position (Range) import           Cryptol.Utils.PP -import Control.Applicative (Applicative(..)) import Control.Exception (IOException) import Data.Function (on) import Data.Maybe (isJust) import MonadLib +#if __GLASGOW_HASKELL__ < 710+import Control.Applicative (Applicative(..))+#endif  -- Errors ---------------------------------------------------------------------- 

@@ -16,12 +16,14 @@ import Cryptol.Utils.PP import Cryptol.Utils.Panic (panic) +import qualified Data.Map as Map++#if __GLASGOW_HASKELL__ < 710 import Control.Applicative (Applicative, (<$>), (<*>)) import Data.Monoid (Monoid(..)) import Data.Foldable (foldMap) import Data.Traversable (traverse)-import qualified Data.Map as Map-+#endif  -- Name Locations -------------------------------------------------------------- 

@@ -26,13 +26,15 @@ import Cryptol.Utils.Panic (panic) import Cryptol.Utils.PP +import MonadLib+import qualified Data.Map as Map++#if __GLASGOW_HASKELL__ < 710 import Control.Applicative(Applicative(..),(<$>)) import Data.Foldable (foldMap) import Data.Monoid (Monoid(..)) import Data.Traversable (traverse)-import MonadLib-import qualified Data.Map as Map-+#endif  -- Errors ---------------------------------------------------------------------- 

@@ -68,8 +68,11 @@ import           Data.List(intersperse) import           Data.Bits(shiftR) import           Data.Maybe (catMaybes)-import           Data.Monoid (Monoid(..)) import           Numeric(showIntAtBase)++#if __GLASGOW_HASKELL__ < 710+import           Data.Monoid (Monoid(..))+#endif  -- | Module names are just namespaces. --

@@ -21,12 +21,14 @@ import Cryptol.Utils.Panic(panic)  import           MonadLib-import           Control.Applicative(Applicative(..),(<$>)) import           Data.Maybe(maybeToList) import           Data.Either(partitionEithers) import qualified Data.Map as Map-import           Data.Traversable(traverse) +#if __GLASGOW_HASKELL__ < 710+import           Control.Applicative(Applicative(..),(<$>))+import           Data.Traversable(traverse)+#endif  class RemovePatterns t where   -- | Eliminate all patterns in a program.

@@ -19,10 +19,14 @@  import Data.Maybe(listToMaybe,fromMaybe) import Data.Bits(testBit,setBit)-import Control.Applicative ((<$>),Applicative(..)) import Control.Monad(liftM,ap)-import qualified Data.Traversable as T (mapM) +#if __GLASGOW_HASKELL__ < 710+import Control.Applicative ((<$>),Applicative(..))+import Data.Traversable (mapM)+import Prelude hiding (mapM)+#endif+ parse :: Config -> ParseM a -> String -> Either ParseError a parse cfg p cs    = case unP p cfg eofPos (S toks) of                       Left err    -> Left err@@ -220,8 +224,8 @@  eFromTo :: Range -> Expr -> Maybe Expr -> Maybe Expr -> ParseM Expr eFromTo r e1 e2 e3 = EFromTo <$> exprToNumT r e1-                             <*> T.mapM (exprToNumT r) e2-                             <*> T.mapM (exprToNumT r) e3+                             <*> mapM (exprToNumT r) e2+                             <*> mapM (exprToNumT r) e3 exprToNumT :: Range -> Expr -> ParseM Type exprToNumT r expr =   case translateExprToNumT expr of

@@ -56,7 +56,6 @@ import qualified Cryptol.Transform.Specialize as S import qualified Cryptol.Symbolic as Symbolic -import Control.Applicative ((<$>)) import Control.DeepSeq import qualified Control.Exception as X import Control.Monad (guard,unless,forM_,when)@@ -64,7 +63,7 @@ import Data.Function (on) import Data.List (intercalate,isPrefixOf,nub) import Data.Maybe (fromMaybe,mapMaybe)-import Data.Monoid (mempty)+import System.Environment (lookupEnv) import System.Exit (ExitCode(ExitSuccess)) import System.Process (shell,createProcess,waitForProcess) import qualified System.Process as Process(runCommand)@@ -76,35 +75,9 @@ import System.Random.TF(newTFGen) import Numeric (showFFloat) -#if __GLASGOW_HASKELL__ < 706-import Control.Monad (liftM)-import qualified Text.ParserCombinators.ReadP as P-import Text.Read hiding (step)-import System.Environment (getEnvironment)--lookupEnv :: String -> IO (Maybe String)-lookupEnv key = lookup key `liftM` getEnvironment--readEither :: Read a => String -> Either String a-readEither s =-  case [ x | (x,"") <- readPrec_to_S read' minPrec s ] of-    [x] -> Right x-    []  -> Left "Prelude.read: no parse"-    _   -> Left "Prelude.read: ambiguous parse"- where-  read' =-    do x <- readPrec-       lift P.skipSpaces-       return x---- | Parse a string using the 'Read' instance.--- Succeeds if there is exactly one valid result.-readMaybe :: Read a => String -> Maybe a-readMaybe s = case readEither s of-                Left _  -> Nothing-                Right a -> Just a-#else-import System.Environment (lookupEnv)+#if __GLASGOW_HASKELL__ < 710+import Control.Applicative ((<$>))+import Data.Monoid (mempty) #endif  -- Commands --------------------------------------------------------------------

@@ -82,21 +82,23 @@ import qualified Cryptol.Parser.AST as P import Cryptol.Symbolic (proverNames, lookupProver) -import Control.Applicative ((<$>), Applicative(..)) import Control.Monad (ap,unless,when) import Data.IORef     (IORef,newIORef,readIORef,modifyIORef) import Data.List (intercalate, isPrefixOf) import Data.Maybe (catMaybes)-import Data.Monoid (Monoid(..)) import Data.Typeable (Typeable) import System.Directory (findExecutable) import qualified Control.Exception as X import qualified Data.Map as Map import Text.Read (readMaybe) -import qualified Data.SBV as SBV (sbvCheckSolverInstallation)+import Data.SBV.Dynamic (sbvCheckSolverInstallation) +#if __GLASGOW_HASKELL__ < 710+import Control.Applicative ((<$>), Applicative(..))+import Data.Monoid (Monoid(..))+#endif  -- REPL Environment ------------------------------------------------------------ @@ -563,7 +565,7 @@     | s `notElem` proverNames     -> return $ Just $ "Prover must be " ++ proverListString     | s `elem` ["offline", "any"] -> return Nothing     | otherwise                   -> do let prover = lookupProver s-                                        available <- SBV.sbvCheckSolverInstallation prover+                                        available <- sbvCheckSolverInstallation prover                                         unless available $                                           putStrLn $ "Warning: " ++ s ++ " installation not found"                                         return Nothing

@@ -12,22 +12,18 @@  module Cryptol.Symbolic where -import Control.Applicative 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 Data.Monoid (Monoid(..))-import Data.Traversable (traverse) import qualified Control.Exception as X -import qualified Data.SBV as SBV+import qualified Data.SBV.Dynamic as SBV  import qualified Cryptol.ModuleSystem as M import qualified Cryptol.ModuleSystem.Env as M -import Cryptol.Symbolic.BitVector import Cryptol.Symbolic.Prims import Cryptol.Symbolic.Value @@ -39,6 +35,12 @@ import Cryptol.Utils.PP import Cryptol.Utils.Panic(panic) +#if __GLASGOW_HASKELL__ < 710+import Control.Applicative+import Data.Monoid (Monoid(..))+import Data.Traversable (traverse)+#endif+ -- External interface ----------------------------------------------------------  proverConfigs :: [(String, SBV.SMTConfig)]@@ -198,13 +200,13 @@  parseValue :: FinType -> [SBV.CW] -> (Eval.Value, [SBV.CW]) parseValue FTBit [] = panic "Cryptol.Symbolic.parseValue" [ "empty FTBit" ]-parseValue FTBit (cw : cws) = (Eval.VBit (SBV.fromCW cw), cws)+parseValue FTBit (cw : cws) = (Eval.VBit (SBV.cwToBool cw), cws) parseValue (FTSeq 0 FTBit) cws = (Eval.VWord (Eval.BV 0 0), cws)-parseValue (FTSeq n FTBit) (cw : cws)-  | SBV.isBounded cw = (Eval.VWord (Eval.BV (toInteger n) (SBV.fromCW cw)), cws)-  | otherwise = panic "Cryptol.Symbolic.parseValue" [ "unbounded concrete word" ]-parseValue (FTSeq n FTBit) cws = (Eval.VSeq True vs, cws')-  where (vs, cws') = parseValues (replicate n FTBit) cws+parseValue (FTSeq n FTBit) cws =+  case SBV.genParse (SBV.KBounded False n) cws of+    Just (x, cws') -> (Eval.VWord (Eval.BV (toInteger n) x), cws')+    Nothing        -> (Eval.VSeq True vs, cws')+      where (vs, cws') = parseValues (replicate n FTBit) cws parseValue (FTSeq n t) cws = (Eval.VSeq False vs, cws')   where (vs, cws') = parseValues (replicate n t) cws parseValue (FTTuple ts) cws = (Eval.VTuple vs, cws')@@ -265,8 +267,8 @@ forallFinType :: FinType -> SBV.Symbolic Value forallFinType ty =   case ty of-    FTBit         -> VBit <$> SBV.forall_-    FTSeq 0 FTBit -> return $ VWord (SBV.literal (bv 0 0))+    FTBit         -> VBit <$> forallSBool_+    FTSeq 0 FTBit -> return $ VWord (literalSWord 0 0)     FTSeq n FTBit -> VWord <$> (forallBV_ n)     FTSeq n t     -> VSeq False <$> replicateM n (forallFinType t)     FTTuple ts    -> VTuple <$> mapM forallFinType ts@@ -275,8 +277,8 @@ existsFinType :: FinType -> SBV.Symbolic Value existsFinType ty =   case ty of-    FTBit         -> VBit <$> SBV.exists_-    FTSeq 0 FTBit -> return $ VWord (SBV.literal (bv 0 0))+    FTBit         -> VBit <$> existsSBool_+    FTSeq 0 FTBit -> return $ VWord (literalSWord 0 0)     FTSeq n FTBit -> VWord <$> existsBV_ n     FTSeq n t     -> VSeq False <$> replicateM n (existsFinType t)     FTTuple ts    -> VTuple <$> mapM existsFinType ts@@ -333,7 +335,7 @@     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 SBV.sBranch else SBV.ite+                           where evalIf = if envIteSolver env then sBranchValue else iteValue     EComp ty e mss    -> evalComp env (evalType env ty) e mss     EVar n            -> case lookupVar n env of                            Just x -> x@@ -377,7 +379,7 @@         _ -> panic "Cryptol.Symbolic.evalSel" [ "Record selector applied to non-record" ]      ListSel n _   -> case v of-                       VWord s -> VBit (SBV.sbvTestBit s n)+                       VWord s -> VBit (SBV.svTestBit s n)                        _       -> fromSeq v !! n  -- 0-based indexing  -- Declarations ----------------------------------------------------------------

@@ -1,205 +0,0 @@--- |--- Module      :  $Header$--- Copyright   :  (c) 2013-2015 Galois, Inc.--- License     :  BSD3--- Maintainer  :  cryptol@galois.com--- Stability   :  provisional--- Portability :  portable--{-# LANGUAGE BangPatterns #-}-{-# LANGUAGE FlexibleContexts #-}-{-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE MultiParamTypeClasses #-}-{-# LANGUAGE PatternGuards #-}-{-# LANGUAGE ViewPatterns #-}--module Cryptol.Symbolic.BitVector where--import Data.Bits-import Data.List (foldl')-import Control.Monad (replicateM)-import System.Random--import Data.SBV.Bridge.Yices-import Data.SBV.Internals--import Cryptol.Utils.Panic---- BitVector type ----------------------------------------------------------------data BitVector = BV { signedcxt :: Bool, width :: !Int, val :: !Integer }-    deriving (Eq, Ord, Show)--- ^ Invariant: BV w x requires that 0 <= w and 0 <= x < 2^w.--bitMask :: Int -> Integer-bitMask w = bit w - 1---- | Smart constructor for bitvectors.-bv :: Int -> Integer -> BitVector-bv = sbv False--sbv :: Bool -> Int -> Integer -> BitVector-sbv b w x = BV b w (x .&. bitMask w)--unsigned :: Int -> Integer -> Integer-unsigned w x = x + bit w--signed :: Int -> Integer -> Integer-signed w x-  | w > 0 && testBit x (w - 1) = x - bit w-  | otherwise                  = x--same :: Int -> Int -> Int-same m n | m == n = m-         | otherwise = panic "Cryptol.Symbolic.BitVector.same"-                         [ "BitVector size mismatch: " ++ show (m, n) ]--instance SignCast SWord SWord where-  signCast (SBV (KBounded _ w) (Left (cwVal -> (CWInteger x)))) =-    SBV k (Left (CW k (CWInteger (signed w x)))) where-      k = KBounded True w-  signCast x@(SBV (KBounded _ w) _) = SBV k (Right (cache y)) where-    k = KBounded True w-    y st = do xsw <- sbvToSW st x-              newExpr st k (SBVApp (Extract (w - 1) 0) [xsw])-  signCast _ = panic "Cryptol.Symbolic.BitVector"-                 [ "signCast called on non-bitvector value" ]-  unsignCast (SBV (KBounded _ w) (Left (cwVal -> (CWInteger x)))) =-    SBV k (Left (CW k (CWInteger (unsigned w x)))) where-      k = KBounded False w-  unsignCast x@(SBV (KBounded _ w) _) = SBV k (Right (cache y)) where-    k = KBounded False w-    y st = do xsw <- sbvToSW st x-              newExpr st k (SBVApp (Extract (w - 1) 0) [xsw])-  unsignCast _ = panic "Cryptol.Symbolic.BitVector"-                   [ "unsignCast called on non-bitvector value" ]--instance Num BitVector where-  fromInteger n = panic "Cryptol.Symbolic.BitVector"-                    [ "fromInteger " ++ show n ++ " :: BitVector" ]-  BV s m x + BV _ n y = sbv s (same m n) (x + y)-  BV s m x - BV _ n y = sbv s (same m n) (x - y)-  BV s m x * BV _ n y = sbv s (same m n) (x * y)-  negate (BV s m x) = sbv s m (- x)-  abs = id-  signum (BV s m _) = sbv s m 1--instance Bits BitVector where-  BV s m x .&. BV _ n y        = BV s (same m n) (x .&. y)-  BV s m x .|. BV _ n y        = BV s (same m n) (x .|. y)-  BV s m x `xor` BV _ n y      = BV s (same m n) (x `xor` y)-  complement (BV s m x)        = BV s m (x `xor` bitMask m)-  shift (BV s m x) i           = sbv s m (shift x i)-  rotate (BV s m x) i          = sbv s m (shift x j .|. shift x (j - m))-                                  where j = i `mod` m-  bit _i                       = panic "Cryptol.Symbolic.BitVector"-                                   [ "bit: can't determine width" ]-  setBit (BV s m x) i          = BV s m (setBit x i)-  clearBit (BV s m x) i        = BV s m (clearBit x i)-  complementBit (BV s m x) i   = BV s m (complementBit x i)-  testBit (BV _ _ x) i         = testBit x i-  bitSize x-    | Just m <- bitSizeMaybe x = m-    | otherwise                = panic "Cryptol.Symbolic.BitVector"-                                   [ "bitSize should be total for BitVector" ]-  bitSizeMaybe (BV _ m _)      = Just m-  isSigned (BV s _ _)          = s-  popCount (BV _ _ x)          = popCount x--instance FiniteBits BitVector where-  finiteBitSize (BV _ m _) = m--instance FiniteBits (SBV BitVector) where-  finiteBitSize (SBV (KBounded _ w) _) = w-  finiteBitSize _ = panic "Cryptol.Symbolic.BitVector"-                          [ "finiteBitSize called on non-bitvector value" ]------------------------------------------------------------------------------------- SBV class instances--type SWord = SBV BitVector--instance HasKind BitVector where-  kindOf (BV s w _) = KBounded s w--instance SymWord BitVector where-  literal (BV s w x) = SBV k (Left (mkConstCW k x))-      where k = KBounded s w-  fromCW c@(CW (KBounded s w) _) = BV s w (fromCW c)-  fromCW c = panic "Cryptol.Symbolic.BitVector"-               [ "fromCW: Unsupported non-integral value: " ++ show c ]-  mkSymWord _ _ = panic "Cryptol.Symbolic.BitVector"-                    [ "mkSymWord unimplemented for type BitVector" ]--instance SIntegral BitVector where--instance FromBits (SBV BitVector) where-  fromBitsLE bs = foldl' f (literalSWord 0 0) bs-    where f w b = cat (ite b (literalSWord 1 1) (literalSWord 1 0)) w--instance SDivisible BitVector where-  sQuotRem (BV _ m x) (BV _ n y) = (BV False w q, BV False w r)-    where (q, r) = quotRem x y-          w = same m n-  sDivMod (BV _ m x) (BV _ n y) = (BV False w q, BV False w r)-    where (q, r) = divMod x y-          w = same m n--instance SDivisible (SBV BitVector) where-  sQuotRem = liftQRem-  sDivMod  = liftDMod--extract :: Int -> Int -> SWord -> SWord-extract i j x@(SBV (KBounded s _) _) =-  case x of-    _ | i < j -> SBV k (Left (CW k (CWInteger 0)))-    SBV _ (Left cw) ->-      case cw of-        CW _ (CWInteger v) -> SBV k (Left (normCW (CW k (CWInteger (v `shiftR` j)))))-        _ -> panic "Cryptol.Symbolic.BitVector.extract" [ "non-integer concrete word" ]-    _ -> SBV k (Right (cache y))-      where y st = do sw <- sbvToSW st x-                      newExpr st k (SBVApp (Extract i j) [sw])-  where-    k = KBounded s (i - j + 1)-extract _ _ _ = panic "Cryptol.Symbolic.BitVector.extract" [ "non-bitvector value" ]--cat :: SWord -> SWord -> SWord-cat x y | finiteBitSize x == 0 = y-        | finiteBitSize y == 0 = x-cat x@(SBV _ (Left a)) y@(SBV _ (Left b)) =-  case (a, b) of-    (CW _ (CWInteger m), CW _ (CWInteger n)) ->-      SBV k (Left (CW k (CWInteger ((m `shiftL` (finiteBitSize y) .|. n)))))-    _ -> panic "Cryptol.Symbolic.BitVector.cat" [ "non-integer concrete word" ]-  where k = KBounded False (finiteBitSize x + finiteBitSize y)-cat x y = SBV k (Right (cache z))-  where k = KBounded False (finiteBitSize x + finiteBitSize y)-        z st = do xsw <- sbvToSW st x-                  ysw <- sbvToSW st y-                  newExpr st k (SBVApp Join [xsw, ysw])--literalSWord :: Int -> Integer -> SWord-literalSWord w i = genLiteral (KBounded False w) i--randomSBVBitVector :: Int -> IO (SBV BitVector)-randomSBVBitVector w = do-  bs <- replicateM w randomIO-  let x = sum [ bit i | (i, b) <- zip [0..] bs, b ]-  return (literal (bv w x))--mkSymBitVector :: Maybe Quantifier -> Maybe String -> Int -> Symbolic (SBV BitVector)-mkSymBitVector mbQ mbNm w =-  mkSymSBVWithRandom (randomSBVBitVector w) mbQ (KBounded False w) mbNm--forallBV :: String -> Int -> Symbolic (SBV BitVector)-forallBV nm w = mkSymBitVector (Just ALL) (Just nm) w--forallBV_ :: Int -> Symbolic (SBV BitVector)-forallBV_ w = mkSymBitVector (Just ALL) Nothing w--existsBV :: String -> Int -> Symbolic (SBV BitVector)-existsBV nm w = mkSymBitVector (Just EX) (Just nm) w--existsBV_ :: Int -> Symbolic (SBV BitVector)-existsBV_ w = mkSymBitVector (Just EX) Nothing w

@@ -11,22 +11,24 @@ {-# LANGUAGE FlexibleContexts #-} module Cryptol.Symbolic.Prims where -import Control.Applicative import Data.Bits import Data.List (genericDrop, genericReplicate, genericSplitAt, genericTake, sortBy, transpose) import Data.Ord (comparing) +import Cryptol.Eval.Value (BitWord(..)) import Cryptol.Prims.Eval (binary, unary, tlamN) import Cryptol.Prims.Syntax (ECon(..))-import Cryptol.Symbolic.BitVector import Cryptol.Symbolic.Value import Cryptol.TypeCheck.AST (Name) import Cryptol.TypeCheck.Solver.InfNat(Nat'(..), nMul) import Cryptol.Utils.Panic -import qualified Data.SBV as SBV-import Data.SBV (SBool)+import qualified Data.SBV.Dynamic as SBV +#if __GLASGOW_HASKELL__ < 710+import Control.Applicative+#endif+ traverseSnd :: Functor f => (a -> f b) -> (t, a) -> f (t, b) traverseSnd f (x, y) = (,) x <$> f y @@ -36,25 +38,25 @@ evalECon :: ECon -> Value evalECon econ =   case econ of-    ECTrue        -> VBit SBV.true-    ECFalse       -> VBit SBV.false+    ECTrue        -> VBit SBV.svTrue+    ECFalse       -> VBit SBV.svFalse     ECDemote      -> ecDemoteV -- Converts a numeric type into its corresponding value.                                -- { val, bits } (fin val, fin bits, bits >= width val) => [bits]-    ECPlus        -> binary (arithBinary (+)) -- {a} (Arith a) => a -> a -> a-    ECMinus       -> binary (arithBinary (-)) -- {a} (Arith a) => a -> a -> a-    ECMul         -> binary (arithBinary (*)) -- {a} (Arith a) => a -> a -> a-    ECDiv         -> binary (arithBinary (SBV.sQuot)) -- {a} (Arith a) => a -> a -> a-    ECMod         -> binary (arithBinary (SBV.sRem)) -- {a} (Arith a) => a -> a -> a+    ECPlus        -> binary (arithBinary SBV.svPlus) -- {a} (Arith a) => a -> a -> a+    ECMinus       -> binary (arithBinary SBV.svMinus) -- {a} (Arith a) => a -> a -> a+    ECMul         -> binary (arithBinary SBV.svTimes) -- {a} (Arith a) => a -> a -> a+    ECDiv         -> binary (arithBinary SBV.svQuot) -- {a} (Arith a) => a -> a -> a+    ECMod         -> binary (arithBinary SBV.svRem) -- {a} (Arith a) => a -> a -> a     ECExp         -> binary (arithBinary sExp) -- {a} (Arith a) => a -> a -> a     ECLg2         -> unary (arithUnary sLg2) -- {a} (Arith a) => a -> a-    ECNeg         -> unary (arithUnary negate)+    ECNeg         -> unary (arithUnary SBV.svUNeg) -    ECLt          -> binary (cmpBinary cmpLt cmpLt SBV.false)-    ECGt          -> binary (cmpBinary cmpGt cmpGt SBV.false)-    ECLtEq        -> binary (cmpBinary cmpLtEq cmpLtEq SBV.true)-    ECGtEq        -> binary (cmpBinary cmpGtEq cmpGtEq SBV.true)-    ECEq          -> binary (cmpBinary cmpEq cmpEq SBV.true)-    ECNotEq       -> binary (cmpBinary cmpNotEq cmpNotEq SBV.false)+    ECLt          -> binary (cmpBinary cmpLt cmpLt SBV.svFalse)+    ECGt          -> binary (cmpBinary cmpGt cmpGt SBV.svFalse)+    ECLtEq        -> binary (cmpBinary cmpLtEq cmpLtEq SBV.svTrue)+    ECGtEq        -> binary (cmpBinary cmpGtEq cmpGtEq SBV.svTrue)+    ECEq          -> binary (cmpBinary cmpEq cmpEq SBV.svTrue)+    ECNotEq       -> binary (cmpBinary cmpNotEq cmpNotEq SBV.svFalse)      -- FIXME: the next 4 "primitives" should be defined in the Cryptol prelude.     ECFunEq       -> -- {a b} (Cmp b) => (a -> b) -> (a -> b) -> a -> Bit@@ -63,7 +65,7 @@       tlam $ \b ->       VFun $ \f ->       VFun $ \g ->-      VFun $ \x -> cmpBinary cmpEq cmpEq SBV.true b (fromVFun f x) (fromVFun g x)+      VFun $ \x -> cmpBinary cmpEq cmpEq SBV.svTrue b (fromVFun f x) (fromVFun g x)      ECFunNotEq    -> -- {a b} (Cmp b) => (a -> b) -> (a -> b) -> a -> Bit       -- (f !== g) x = (f x != g x)@@ -71,24 +73,24 @@       tlam $ \b ->       VFun $ \f ->       VFun $ \g ->-      VFun $ \x -> cmpBinary cmpNotEq cmpNotEq SBV.false b (fromVFun f x) (fromVFun g x)+      VFun $ \x -> cmpBinary cmpNotEq cmpNotEq SBV.svFalse b (fromVFun f x) (fromVFun g x)      ECMin         -> -- {a} (Cmp a) => a -> a -> a       -- min x y = if x <= y then x else y       binary $ \a x y ->-        let c = cmpBinary cmpLtEq cmpLtEq SBV.false a x y-        in SBV.ite (fromVBit c) x y+        let c = cmpBinary cmpLtEq cmpLtEq SBV.svFalse a x y+        in iteValue (fromVBit c) x y      ECMax         -> -- {a} (Cmp a) => a -> a -> a       -- max x y = if y <= x then x else y       binary $ \a x y ->-        let c = cmpBinary cmpLtEq cmpLtEq SBV.false a y x-        in SBV.ite (fromVBit c) x y+        let c = cmpBinary cmpLtEq cmpLtEq SBV.svFalse a y x+        in iteValue (fromVBit c) x y -    ECAnd         -> binary (logicBinary (SBV.&&&) (.&.))-    ECOr          -> binary (logicBinary (SBV.|||) (.|.))-    ECXor         -> binary (logicBinary (SBV.<+>) xor)-    ECCompl       -> unary (logicUnary (SBV.bnot) complement)+    ECAnd         -> binary (logicBinary SBV.svAnd SBV.svAnd)+    ECOr          -> binary (logicBinary SBV.svOr SBV.svOr)+    ECXor         -> binary (logicBinary SBV.svXOr SBV.svXOr)+    ECCompl       -> unary (logicUnary SBV.svNot SBV.svNot)     ECZero        -> VPoly zeroV      ECShiftL      -> -- {m,n,a} (fin n) => [m] a -> [n] -> [m] a@@ -98,7 +100,7 @@       VFun $ \xs ->       VFun $ \y ->         case xs of-          VWord x -> VWord (SBV.sbvShiftLeft x (fromVWord y))+          VWord x -> VWord (SBV.svShiftLeft x (fromVWord y))           _ -> selectV shl y             where               shl :: Integer -> Value@@ -115,7 +117,7 @@       VFun $ \xs ->       VFun $ \y ->         case xs of-          VWord x -> VWord (SBV.sbvShiftRight x (fromVWord y))+          VWord x -> VWord (SBV.svShiftRight x (fromVWord y))           _ -> selectV shr y             where               shr :: Integer -> Value@@ -132,7 +134,7 @@       VFun $ \xs ->       VFun $ \y ->         case xs of-          VWord x -> VWord (SBV.sbvRotateLeft x (fromVWord y))+          VWord x -> VWord (SBV.svRotateLeft x (fromVWord y))           _ -> selectV rol y             where               rol :: Integer -> Value@@ -146,7 +148,7 @@       VFun $ \xs ->       VFun $ \y ->         case xs of-          VWord x -> VWord (SBV.sbvRotateRight x (fromVWord y))+          VWord x -> VWord (SBV.svRotateRight x (fromVWord y))           _ -> selectV ror y             where               ror :: Integer -> Value@@ -235,13 +237,13 @@     ECInfFrom    ->       tlam $ \(finTValue -> bits)  ->        lam $ \(fromVWord  -> first) ->-      toStream [ VWord (first + SBV.literal (bv (fromInteger bits) i)) | i <- [0 ..] ]+      toStream [ VWord (SBV.svPlus first (literalSWord (fromInteger bits) i)) | i <- [0 ..] ]      ECInfFromThen -> -- {a} (fin a) => [a] -> [a] -> [inf][a]       tlam $ \_ ->        lam $ \(fromVWord -> first) ->        lam $ \(fromVWord -> next) ->-      toStream (map VWord (iterate (+ (next - first)) first))+      toStream (map VWord (iterate (SBV.svPlus (SBV.svMinus next first)) first))      -- {at,len} (fin len) => [len][8] -> at     ECError ->@@ -256,10 +258,10 @@       VFun $ \v2 ->         let k = max 1 (i + j) - 1             mul _  []     ps = ps-            mul as (b:bs) ps = mul (SBV.false : as) bs (ites b (as `addPoly` ps) ps)+            mul as (b:bs) ps = mul (SBV.svFalse : as) bs (ites b (as `addPoly` ps) ps)             xs = map fromVBit (fromSeq v1)             ys = map fromVBit (fromSeq v2)-            zs = take (fromInteger k) (mul xs ys [] ++ repeat SBV.false)+            zs = take (fromInteger k) (mul xs ys [] ++ repeat SBV.svFalse)         in VSeq True (map VBit zs)      ECPDiv        -> -- {a,b} (fin a, fin b) => [a] -> [b] -> [a]@@ -269,7 +271,7 @@       VFun $ \v2 ->         let xs = map fromVBit (fromSeq v1)             ys = map fromVBit (fromSeq v2)-            zs = take (fromInteger i) (fst (mdp (reverse xs) (reverse ys)) ++ repeat SBV.false)+            zs = take (fromInteger i) (fst (mdp (reverse xs) (reverse ys)) ++ repeat SBV.svFalse)         in VSeq True (map VBit (reverse zs))      ECPMod        -> -- {a,b} (fin a, fin b) => [a] -> [b+1] -> [b]@@ -279,7 +281,7 @@       VFun $ \v2 ->         let xs = map fromVBit (fromSeq v1)             ys = map fromVBit (fromSeq v2)-            zs = take (fromInteger j) (snd (mdp (reverse xs) (reverse ys)) ++ repeat SBV.false)+            zs = take (fromInteger j) (snd (mdp (reverse xs) (reverse ys)) ++ repeat SBV.svFalse)         in VSeq True (map VBit (reverse zs))      ECRandom      -> panic "Cryptol.Symbolic.Prims.evalECon"@@ -293,7 +295,7 @@      sel :: Integer -> [SBool] -> Value     sel offset []       = f offset-    sel offset (b : bs) = SBV.ite b m1 m2+    sel offset (b : bs) = iteValue b m1 m2       where m1 = sel (offset + 2 ^ length bs) bs             m2 = sel offset bs @@ -311,9 +313,9 @@   case v of     VStream xs -> nth err xs (fromInteger n)     VSeq _ xs  -> nth err xs (fromInteger n)-    VWord x                 -> let i = finiteBitSize x - 1 - fromInteger n+    VWord x                 -> let i = SBV.svBitSize x - 1 - fromInteger n                                in if i < 0 then err else-                                    VBit (SBV.sbvTestBit x i)+                                    VBit (SBV.svTestBit x i)     _                       -> err  mapV :: Bool -> (Value -> Value) -> Value -> Value@@ -325,8 +327,8 @@  catV :: Value -> Value -> Value catV xs          (VStream ys) = VStream (fromSeq xs ++ ys)-catV (VWord x)   ys           = VWord (cat x (fromVWord ys))-catV xs          (VWord y)    = VWord (cat (fromVWord xs) y)+catV (VWord x)   ys           = VWord (SBV.svJoin x (fromVWord ys))+catV xs          (VWord y)    = VWord (SBV.svJoin (fromVWord xs) y) catV (VSeq b xs) (VSeq _ ys)  = VSeq b (xs ++ ys) catV _ _ = panic "Cryptol.Symbolic.Prims.catV" [ "non-concatenable value" ] @@ -336,13 +338,13 @@   case xs of     VSeq b xs'  -> VSeq b (genericDrop n xs')     VStream xs' -> VStream (genericDrop n xs')-    VWord w     -> VWord $ extract (finiteBitSize w - 1 - fromInteger n) 0 w+    VWord w     -> VWord $ SBV.svExtract (SBV.svBitSize 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 $ extract (finiteBitSize w - 1) (finiteBitSize w - fromInteger n) w+    VWord w     -> VWord $ SBV.svExtract (SBV.svBitSize w - 1) (SBV.svBitSize 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@@ -355,7 +357,7 @@ ecDemoteV = tlam $ \valT ->             tlam $ \bitT ->             case (numTValue valT, numTValue bitT) of-              (Nat v, Nat bs) -> VWord (SBV.literal (bv (fromInteger bs) v))+              (Nat v, Nat bs) -> VWord (literalSWord (fromInteger bs) v)               _ -> evalPanic "Cryptol.Prove.evalECon"                        ["Unexpected Inf in constant."                        , show valT@@ -418,19 +420,19 @@         TVFun _ t     -> VFun (\x -> loop t (fromVFun v x))  sExp :: SWord -> SWord -> SWord-sExp x y = go (SBV.blastLE y)-  where go []       = SBV.literal (bv (finiteBitSize x) 1)-        go (b : bs) = SBV.ite b (x * s) s+sExp x y = go (reverse (unpackWord y)) -- bits in little-endian order+  where go []       = literalSWord (SBV.svBitSize x) 1+        go (b : bs) = SBV.svIte b (SBV.svTimes x s) s             where a = go bs-                  s = a * a+                  s = SBV.svTimes a a  -- | Ceiling (log_2 x) sLg2 :: SWord -> SWord sLg2 x = go 0   where-    lit n = SBV.literal (bv (finiteBitSize x) n)-    go i | i < finiteBitSize x = SBV.ite ((SBV..<=) x (lit (2^i))) (lit (toInteger i)) (go (i + 1))-         | otherwise     = lit (toInteger i)+    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))+         | otherwise           = lit (toInteger i)  -- Cmp ------------------------------------------------------------------------- @@ -461,19 +463,19 @@     cmpValues (x1 : xs1) (x2 : xs2) k = cmp x1 x2 (cmpValues xs1 xs2 k)     cmpValues _ _ k = k -cmpEq :: SBV.EqSymbolic a => a -> a -> SBool -> SBool-cmpEq x y k = (SBV.&&&) ((SBV..==) x y) k+cmpEq :: SWord -> SWord -> SBool -> SBool+cmpEq x y k = SBV.svAnd (SBV.svEqual x y) k -cmpNotEq :: SBV.EqSymbolic a => a -> a -> SBool -> SBool-cmpNotEq x y k = (SBV.|||) ((SBV../=) x y) k+cmpNotEq :: SWord -> SWord -> SBool -> SBool+cmpNotEq x y k = SBV.svOr (SBV.svNotEqual x y) k -cmpLt, cmpGt :: SBV.OrdSymbolic a => a -> a -> SBool -> SBool-cmpLt x y k = (SBV.|||) ((SBV..<) x y) (cmpEq x y k)-cmpGt x y k = (SBV.|||) ((SBV..>) x y) (cmpEq x y k)+cmpLt, cmpGt :: SWord -> SWord -> SBool -> SBool+cmpLt x y k = SBV.svOr (SBV.svLessThan x y) (cmpEq x y k)+cmpGt x y k = SBV.svOr (SBV.svGreaterThan x y) (cmpEq x y k) -cmpLtEq, cmpGtEq :: SBV.OrdSymbolic a => a -> a -> SBool -> SBool-cmpLtEq x y k = (SBV.&&&) ((SBV..<=) x y) (cmpNotEq x y k)-cmpGtEq x y k = (SBV.&&&) ((SBV..>=) x y) (cmpNotEq x y k)+cmpLtEq, cmpGtEq :: SWord -> SWord -> SBool -> SBool+cmpLtEq x y k = SBV.svAnd (SBV.svLessEq x y) (cmpNotEq x y k)+cmpGtEq x y k = SBV.svAnd (SBV.svGreaterEq x y) (cmpNotEq x y k)  cmpBinary :: (SBool -> SBool -> SBool -> SBool)           -> (SWord -> SWord -> SBool -> SBool)@@ -500,8 +502,8 @@   where     go ty =       case ty of-        TVBit         -> VBit SBV.false-        TVSeq n TVBit -> VWord (SBV.literal (bv n 0))+        TVBit         -> VBit SBV.svFalse+        TVSeq n TVBit -> VWord (literalSWord n 0)         TVSeq n t     -> VSeq False (replicate n (go t))         TVStream t    -> VStream (repeat (go t))         TVTuple ts    -> VTuple [ go t | t <- ts ]@@ -575,7 +577,7 @@     case (first, next, len, bits) of       (Nat first', Nat next', Nat len', Nat bits') ->         let nums = enumFromThen first' next'-            lit i = VWord (SBV.literal (bv (fromInteger bits') i))+            lit i = VWord (literalSWord (fromInteger bits') i)          in VSeq False (genericTake len' (map lit nums))       _ -> evalPanic "fromThenV" ["invalid arguments"] @@ -590,7 +592,7 @@       (Nat first', Nat lst', Nat bits') ->         let nums = enumFromThenTo first' (first' + 1) lst'             len  = 1 + (lst' - first')-            lit i = VWord (SBV.literal (bv (fromInteger bits') i))+            lit i = VWord (literalSWord (fromInteger bits') i)          in VSeq False (genericTake len (map lit nums))        _ -> evalPanic "fromThenV" ["invalid arguments"]@@ -607,7 +609,7 @@        (Nat first', Nat next', Nat lst', Nat len', Nat bits') ->         let nums = enumFromThenTo first' next' lst'-            lit i = VWord (SBV.literal (bv (fromInteger bits') i))+            lit i = VWord (literalSWord (fromInteger bits') i)          in VSeq False (genericTake len' (map lit nums))        _ -> evalPanic "fromThenV" ["invalid arguments"]@@ -621,25 +623,25 @@ addPoly :: [SBool] -> [SBool] -> [SBool] addPoly xs    []      = xs addPoly []    ys      = ys-addPoly (x:xs) (y:ys) = x SBV.<+> y : addPoly xs ys+addPoly (x:xs) (y:ys) = SBV.svXOr x y : addPoly xs ys  ites :: SBool -> [SBool] -> [SBool] -> [SBool] ites s xs ys- | Just t <- SBV.unliteral s+ | Just t <- SBV.svAsBool s  = if t then xs else ys  | True  = go xs ys  where go [] []         = []-       go []     (b:bs) = SBV.ite s SBV.false b : go [] bs-       go (a:as) []     = SBV.ite s a SBV.false : go as []-       go (a:as) (b:bs) = SBV.ite s a b : go as bs+       go []     (b:bs) = SBV.svIte s SBV.svFalse b : go [] bs+       go (a:as) []     = SBV.svIte s a SBV.svFalse : go as []+       go (a:as) (b:bs) = SBV.svIte s a b : go as bs  -- conservative over-approximation of the degree degree :: [SBool] -> Int degree xs = walk (length xs - 1) $ reverse xs   where walk n []     = n         walk n (b:bs)-         | Just t <- SBV.unliteral b+         | Just t <- SBV.svAsBool b          = if t then n else walk (n-1) bs          | True          = n -- over-estimate@@ -653,13 +655,13 @@          | True     = let (rqs, rrs) = go (n-1) bs                       in (ites b (reverse qs) rqs, ites b rs rrs)          where degQuot = degTop - n-               ys' = replicate degQuot SBV.false ++ ys+               ys' = replicate degQuot SBV.svFalse ++ ys                (qs, rs) = divx (degQuot+1) degTop xs ys'  -- return the element at index i; if not enough elements, return false -- N.B. equivalent to '(xs ++ repeat false) !! i', but more efficient idx :: [SBool] -> Int -> SBool-idx []     _ = SBV.false+idx []     _ = SBV.svFalse idx (x:_)  0 = x idx (_:xs) i = idx xs (i-1) 

@@ -12,64 +12,108 @@ {-# LANGUAGE TypeSynonymInstances #-} {-# OPTIONS_GHC -fno-warn-orphans #-} module Cryptol.Symbolic.Value-  ( Value+  ( SBool, SWord+  , literalSWord+  , fromBitsLE+  , forallBV_, existsBV_+  , forallSBool_, existsSBool_+  , Value   , TValue, numTValue, toNumTValue, finTValue, isTBit, isTFun, isTSeq, isTTuple, isTRec, tvSeq   , GenValue(..), lam, tlam, toStream, toFinSeq, toSeq   , fromVBit, fromVFun, fromVPoly, fromVTuple, fromVRecord, lookupRecord   , fromSeq, fromVWord   , evalPanic+  , iteValue, sBranchValue, mergeValue   )   where -import Data.Bits (finiteBitSize)+import Data.List (foldl') -import Cryptol.Eval.Value (TValue, numTValue, toNumTValue, finTValue, isTBit, isTFun, isTSeq, isTTuple, isTRec, tvSeq,-                           GenValue(..), BitWord(..), lam, tlam, toStream, toFinSeq, toSeq, fromSeq,-                           fromVBit, fromVWord, fromVFun, fromVPoly, fromVTuple, fromVRecord, lookupRecord)-import Cryptol.Symbolic.BitVector+import Data.SBV.Dynamic++import Cryptol.Eval.Value (TValue, numTValue, toNumTValue, finTValue, isTBit,+                           isTFun, isTSeq, isTTuple, isTRec, tvSeq, GenValue(..),+                           BitWord(..), lam, tlam, toStream, toFinSeq, toSeq,+                           fromSeq, fromVBit, fromVWord, fromVFun, fromVPoly,+                           fromVTuple, fromVRecord, lookupRecord) import Cryptol.Utils.Panic (panic) -import Data.SBV (SBool, fromBitsBE, Mergeable(..), HasKind(..), EqSymbolic(..))-import Data.SBV.Internals (symbolicMergeWithKind)+-- SBool and SWord ------------------------------------------------------------- +type SBool = SVal+type SWord = SVal++fromBitsLE :: [SBool] -> SWord+fromBitsLE bs = foldl' f (literalSWord 0 0) bs+  where f w b = svJoin (svToWord1 b) w++literalSWord :: Int -> Integer -> SWord+literalSWord w i = svInteger (KBounded False w) i++forallBV_ :: Int -> Symbolic SWord+forallBV_ w = svMkSymVar (Just ALL) (KBounded False w) Nothing++existsBV_ :: Int -> Symbolic SWord+existsBV_ w = svMkSymVar (Just EX) (KBounded False w) Nothing++forallSBool_ :: Symbolic SBool+forallSBool_ = svMkSymVar (Just ALL) KBool Nothing++existsSBool_ :: Symbolic SBool+existsSBool_ = svMkSymVar (Just EX) KBool Nothing+ -- Values ----------------------------------------------------------------------  type Value = GenValue SBool SWord  -- Symbolic Conditionals ------------------------------------------------------- -instance Mergeable Value where-  symbolicMerge f c v1 v2 =-    case (v1, v2) of-      (VRecord fs1, VRecord fs2) -> VRecord $ zipWith mergeField fs1 fs2-      (VTuple vs1 , VTuple vs2 ) -> VTuple $ zipWith (symbolicMerge f c) vs1 vs2-      (VBit b1    , VBit b2    ) -> VBit $ symbolicMerge f c b1 b2-      (VWord w1   , VWord w2   ) -> VWord $ mergeWord w1 w2-      (VSeq b1 vs1, VSeq _ vs2 ) -> VSeq b1 $ symbolicMerge f c vs1 vs2-      (VStream vs1, VStream vs2) -> VStream $ mergeStream vs1 vs2-      (VFun f1    , VFun f2    ) -> VFun $ symbolicMerge f c f1 f2-      (VPoly f1   , VPoly f2   ) -> VPoly $ symbolicMerge f c f1 f2-      (VWord w1   , _          ) -> VWord $ mergeWord w1 (fromVWord v2)-      (_          , VWord w2   ) -> VWord $ mergeWord (fromVWord v1) w2-      (_          , _          ) -> panic "Cryptol.Symbolic.Value"-                                      [ "symbolicMerge: incompatible values" ]-    where-      mergeWord w1 w2 = symbolicMergeWithKind (kindOf w1) f c w1 w2-      mergeField (n1, x1) (n2, x2)-        | n1 == n2  = (n1, symbolicMerge f c x1 x2)-        | otherwise = panic "Cryptol.Symbolic.Value"-                        [ "symbolicMerge.mergeField: incompatible values" ]-      mergeStream xs ys =-        symbolicMerge f c (head xs) (head ys) : mergeStream (tail xs) (tail ys)+iteValue :: SBool -> Value -> Value -> Value+iteValue c x y =+  case svAsBool c of+    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 =+  case (v1, v2) of+    (VRecord fs1, VRecord fs2) -> VRecord $ zipWith mergeField fs1 fs2+    (VTuple vs1 , VTuple vs2 ) -> VTuple $ zipWith (mergeValue f c) vs1 vs2+    (VBit b1    , VBit b2    ) -> VBit $ mergeBit b1 b2+    (VWord w1   , VWord w2   ) -> VWord $ mergeWord w1 w2+    (VSeq b1 vs1, VSeq _ vs2 ) -> VSeq b1 $ zipWith (mergeValue f c) vs1 vs2+    (VStream vs1, VStream vs2) -> VStream $ mergeStream vs1 vs2+    (VFun f1    , VFun f2    ) -> VFun $ \x -> mergeValue f c (f1 x) (f2 x)+    (VPoly f1   , VPoly f2   ) -> VPoly $ \x -> mergeValue f c (f1 x) (f2 x)+    (VWord w1   , _          ) -> VWord $ mergeWord w1 (fromVWord v2)+    (_          , VWord w2   ) -> VWord $ mergeWord (fromVWord v1) w2+    (_          , _          ) -> panic "Cryptol.Symbolic.Value"+                                  [ "mergeValue: incompatible values" ]+  where+    mergeBit b1 b2 = svSymbolicMerge KBool f c b1 b2+    mergeWord w1 w2 = svSymbolicMerge (svKind w1) f c w1 w2+    mergeField (n1, x1) (n2, x2)+      | n1 == n2  = (n1, mergeValue f c x1 x2)+      | otherwise = panic "Cryptol.Symbolic.Value"+                    [ "mergeValue.mergeField: incompatible values" ]+    mergeStream xs ys =+      mergeValue f c (head xs) (head ys) : mergeStream (tail xs) (tail ys)+ -- Big-endian Words ------------------------------------------------------------  instance BitWord SBool SWord where-  packWord bs = Data.SBV.fromBitsBE bs-  unpackWord w = [ sbvTestBit' w i | i <- reverse [0 .. finiteBitSize w - 1] ]--sbvTestBit' :: SWord -> Int -> SBool-sbvTestBit' w i = extract i i w .== literalSWord 1 1+  packWord bs = fromBitsLE (reverse bs)+  unpackWord x = [ svTestBit x i | i <- reverse [0 .. svBitSize x - 1] ]  -- Errors ---------------------------------------------------------------------- 

@@ -12,8 +12,11 @@ import Cryptol.TypeCheck.AST import Cryptol.Eval.Value -import Control.Applicative((<$>)) import Data.List(genericReplicate)++#if __GLASGOW_HASKELL__ < 710+import Control.Applicative((<$>))+#endif  {- | Given a (function) type, compute all possible inputs for it. We also return the total number of test (i.e., the length of the outer list. -}

@@ -79,11 +79,14 @@ import Cryptol.Parser.AST (Pass(MonoValues)) import Cryptol.TypeCheck.AST import Cryptol.TypeCheck.TypeMap-import Control.Applicative import Data.List(sortBy,groupBy) import Data.Either(partitionEithers) import Data.Map (Map) import MonadLib++#if __GLASGOW_HASKELL__ < 710+import Control.Applicative+#endif  {- (f,t,n) |--> x  means that when we spot instantiations of `f` with `ts` and `n` proof argument, we should replace them with `Var x` -}

@@ -16,15 +16,17 @@ import qualified Cryptol.ModuleSystem.Env as M import qualified Cryptol.ModuleSystem.Monad as M -import Control.Applicative import Data.List (intercalate) import           Data.Map (Map) import qualified Data.Map as Map import Data.Maybe (catMaybes)-import Data.Traversable (traverse)  import MonadLib +#if __GLASGOW_HASKELL__ < 710+import Control.Applicative+import Data.Traversable (traverse)+#endif  -- Specializer Monad ----------------------------------------------------------- 

@@ -35,7 +35,10 @@ import           MonadLib import qualified Control.Applicative as A import           Control.Monad.Fix(MonadFix(..))++#if __GLASGOW_HASKELL__ < 710 import           Data.Functor+#endif  -- | Information needed for type inference. data InferInput = InferInput

@@ -6,7 +6,7 @@ -- Stability   :  provisional -- Portability :  portable -{-# LANGUAGE OverloadedStrings, RecordWildCards, PatternGuards, Trustworthy #-}+{-# LANGUAGE OverloadedStrings, RecordWildCards, PatternGuards #-} {-# LANGUAGE ScopedTypeVariables #-} module Cryptol.TypeCheck.Solver.Smtlib (simpDelayed) where 

@@ -15,10 +15,13 @@ import Cryptol.TypeCheck.Subst import Cryptol.Utils.Panic (panic) -import Control.Applicative (Applicative(..)) import Data.Ord(comparing) import Data.List(sortBy) import qualified Data.Set as Set++#if __GLASGOW_HASKELL__ < 710+import Control.Applicative (Applicative(..))+#endif  -- | The most general unifier is a substitution and a set of constraints -- on bound variables.