mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-11-28 01:13:34 +03:00
Refactoring of how bits and words are handled in the interpreters.
The major change in this patch is to add a new type of 'WordValue' which is always used to represent finite sequences of bits. A word value is either a packed word, or a sequence of lazy bits. The 'VSeq' constructor, in constrast, is now never used for a finite sequence of bits. This avoids certain thorny problems that arise when trying to faithfully implement the lazy semantics of Cryptol. We now do not have to commit to a value at type '[n]' being represented as a packed word or as an unpacked word until relatively late. This allows us to perform type-directed eta-expansion at every recursive call before we know how words will be represented. This patch fixes all the outstanding strictness bugs that I know of. Unfortunately, we seem to lose some ground on performance. The new evaluator is now about 5% slower than the old one on the AES benchmark, and quite a bit slower on the SHA1 benchmark. Fortunately, the use if LRU caches for memoization of sequences seems to keep heap usage to manageable levels; so programs generally complete, even if they take a long time.
This commit is contained in:
parent
99526f5700
commit
b95b734b74
@ -53,6 +53,7 @@ library
|
||||
gitrev >= 1.0,
|
||||
GraphSCC >= 1.0.4,
|
||||
heredoc >= 0.2,
|
||||
lrucache >= 1.2,
|
||||
monad-control >= 1.0,
|
||||
monadLib >= 3.7.2,
|
||||
old-time >= 1.1,
|
||||
|
@ -9,6 +9,7 @@
|
||||
{-# LANGUAGE DoAndIfThenElse #-}
|
||||
{-# LANGUAGE LambdaCase #-}
|
||||
{-# LANGUAGE MultiParamTypeClasses #-}
|
||||
{-# LANGUAGE ParallelListComp #-}
|
||||
{-# LANGUAGE ScopedTypeVariables #-}
|
||||
{-# LANGUAGE Safe #-}
|
||||
{-# LANGUAGE PatternGuards #-}
|
||||
@ -39,8 +40,10 @@ import Cryptol.Utils.PP
|
||||
|
||||
import Control.Monad
|
||||
import Control.Monad.Fix
|
||||
import qualified Data.Sequence as Seq
|
||||
import Data.IORef
|
||||
import Data.List
|
||||
import Data.Maybe
|
||||
import qualified Data.Map.Strict as Map
|
||||
|
||||
import Prelude ()
|
||||
@ -63,35 +66,46 @@ evalExpr :: EvalPrims b w
|
||||
-> Eval (GenValue b w)
|
||||
evalExpr env expr = case expr of
|
||||
|
||||
EList es ty ->
|
||||
VSeq (genericLength es) (isTBit (evalType env ty))
|
||||
<$> finiteSeqMap (map (evalExpr env) es)
|
||||
-- Try to detect when the user has directly written a finite sequence of
|
||||
-- literal bit values and pack these into a word.
|
||||
EList es ty
|
||||
| isTBit tyv -> {-# SCC "evalExpr->Elist/bit" #-}
|
||||
return $ VWord len $ return $
|
||||
case tryFromBits vs of
|
||||
Just w -> WordVal w
|
||||
Nothing -> BitsVal $ Seq.fromList $ map (fromVBit <$>) vs
|
||||
| otherwise -> {-# SCC "evalExpr->EList" #-}
|
||||
VSeq len <$> finiteSeqMap vs
|
||||
where
|
||||
tyv = evalType env ty
|
||||
vs = map (evalExpr env) es
|
||||
len = genericLength es
|
||||
|
||||
ETuple es -> do
|
||||
ETuple es -> {-# SCC "evalExpr->ETuple" #-} do
|
||||
xs <- mapM (delay Nothing . eval) es
|
||||
return $ VTuple xs
|
||||
|
||||
ERec fields -> do
|
||||
ERec fields -> {-# SCC "evalExpr->ERec" #-} do
|
||||
xs <- sequence [ do thk <- delay Nothing (eval e)
|
||||
return (f,thk)
|
||||
| (f,e) <- fields
|
||||
]
|
||||
return $ VRecord xs
|
||||
|
||||
ESel e sel -> do
|
||||
ESel e sel -> {-# SCC "evalExpr->ESel" #-} do
|
||||
x <- eval e
|
||||
evalSel x sel
|
||||
|
||||
EIf c t f -> do
|
||||
EIf c t f -> {-# SCC "evalExpr->EIf" #-} do
|
||||
b <- fromVBit <$> eval c
|
||||
iteValue b (eval t) (eval f)
|
||||
|
||||
EComp n t h gs -> do
|
||||
EComp n t h gs -> {-# SCC "evalExpr->EComp" #-} do
|
||||
let len = evalType env n
|
||||
let elty = evalType env t
|
||||
evalComp env len elty h gs
|
||||
|
||||
EVar n -> do
|
||||
EVar n -> {-# SCC "evalExpr->EVar" #-} do
|
||||
case lookupVar n env of
|
||||
Just val -> val
|
||||
Nothing -> do
|
||||
@ -101,10 +115,10 @@ evalExpr env expr = case expr of
|
||||
, show envdoc
|
||||
]
|
||||
|
||||
ETAbs tv b ->
|
||||
ETAbs tv b -> {-# SCC "evalExpr->ETAbs" #-}
|
||||
return $ VPoly $ \ty -> evalExpr (bindType (tpVar tv) ty env) b
|
||||
|
||||
ETApp e ty -> do
|
||||
ETApp e ty -> {-# SCC "evalExpr->ETApp" #-} do
|
||||
eval e >>= \case
|
||||
VPoly f -> f $! (evalType env ty)
|
||||
val -> do vdoc <- ppV val
|
||||
@ -113,13 +127,13 @@ evalExpr env expr = case expr of
|
||||
, show vdoc, show e, show ty
|
||||
]
|
||||
|
||||
EApp f x -> do
|
||||
EApp f x -> {-# SCC "evalExpr->EApp" #-} do
|
||||
eval f >>= \case
|
||||
VFun f' -> f' (eval x)
|
||||
it -> do itdoc <- ppV it
|
||||
panic "[Eval] evalExpr" ["not a function", show itdoc ]
|
||||
|
||||
EAbs n _ty b ->
|
||||
EAbs n _ty b -> {-# SCC "evalExpr->EAbs" #-}
|
||||
return $ VFun (\v -> do env' <- bindVar n v env
|
||||
evalExpr env' b)
|
||||
|
||||
@ -129,12 +143,13 @@ evalExpr env expr = case expr of
|
||||
|
||||
ECast e _ty -> evalExpr env e
|
||||
|
||||
EWhere e ds -> do
|
||||
EWhere e ds -> {-# SCC "evalExpr->EWhere" #-} do
|
||||
env' <- evalDecls ds env
|
||||
evalExpr env' e
|
||||
|
||||
where
|
||||
|
||||
{-# INLINE eval #-}
|
||||
eval = evalExpr env
|
||||
ppV = ppValue defaultPPOpts
|
||||
|
||||
@ -175,7 +190,7 @@ evalDeclGroup env dg = do
|
||||
Recursive ds -> do
|
||||
-- declare a "hole" for each declaration
|
||||
holes <- mapM declHole ds
|
||||
let holeEnv = Map.fromList $ [ (nm,h) | (nm,h,_) <- holes ]
|
||||
let holeEnv = Map.fromList $ [ (nm,h) | (nm,_,h,_) <- holes ]
|
||||
let env' = env `mappend` emptyEnv{ envVars = holeEnv }
|
||||
|
||||
-- evaluate the declaration bodies
|
||||
@ -190,25 +205,109 @@ evalDeclGroup env dg = do
|
||||
NonRecursive d -> do
|
||||
evalDecl env env d
|
||||
|
||||
fillHole :: GenEvalEnv b w
|
||||
-> (Name, Eval (GenValue b w), Eval (GenValue b w) -> Eval ())
|
||||
fillHole :: BitWord b w
|
||||
=> GenEvalEnv b w
|
||||
-> (Name, Schema, Eval (GenValue b w), Eval (GenValue b w) -> Eval ())
|
||||
-> Eval ()
|
||||
fillHole env (nm, _, fill) = do
|
||||
fillHole env (nm, sch, _, fill) = do
|
||||
case lookupVar nm env of
|
||||
Nothing -> evalPanic "fillHole" ["Recursive definition not completed", show (ppLocName nm)]
|
||||
Just x -> fill =<< delay (Just (show (ppLocName nm))) x
|
||||
Just x -> fill (etaDelay (show (ppLocName nm)) env sch x)
|
||||
|
||||
etaDelay :: BitWord b w
|
||||
=> String
|
||||
-> GenEvalEnv b w
|
||||
-> Schema
|
||||
-> Eval (GenValue b w)
|
||||
-> Eval (GenValue b w)
|
||||
etaDelay msg env0 Forall{ sVars = vs, sType = tp0 } = goTpVars env0 vs
|
||||
where
|
||||
goTpVars env [] x = go (evalType env tp0) x
|
||||
goTpVars env (v:vs) x =
|
||||
return $ VPoly $ \t ->
|
||||
goTpVars (bindType (tpVar v) t env) vs ( ($t) . fromVPoly =<< x )
|
||||
|
||||
go tp (Ready x) =
|
||||
case x of
|
||||
VBit _ -> return x
|
||||
VWord _ _ -> return x
|
||||
VSeq n xs
|
||||
| Just (nt, el) <- isTSeq tp
|
||||
-> return $ VSeq n $ SeqMap $ \i -> go el (lookupSeqMap xs i)
|
||||
|
||||
VStream xs
|
||||
| Just (nt, el) <- isTSeq tp
|
||||
-> return $ VStream $ SeqMap $ \i -> go el (lookupSeqMap xs i)
|
||||
|
||||
VTuple xs
|
||||
| Just (_n, ts) <- isTTuple tp
|
||||
-> return $ VTuple (zipWith go ts xs)
|
||||
|
||||
VRecord fs
|
||||
| Just fts <- isTRec tp
|
||||
-> return $ VRecord $
|
||||
let err f = evalPanic "expected record value with field" [show f] in
|
||||
[ (f, go (fromMaybe (err f) (lookup f fts)) x)
|
||||
| (f,x) <- fs
|
||||
]
|
||||
|
||||
VFun f
|
||||
| Just (_t1,t2) <- isTFun tp
|
||||
-> return $ VFun $ \a -> go t2 (f a)
|
||||
|
||||
go tp x
|
||||
| isTBit tp
|
||||
= x
|
||||
|
||||
| Just (n, el) <- isTSeq tp
|
||||
, Nat n' <- numTValue n
|
||||
, isTBit el
|
||||
-- TODO! I think we need the alternate blackhole strategy here, where
|
||||
-- entering the blackhole eta-exapnds to a list of bits
|
||||
= do w <- delay (Just msg) (fromWordVal "during eta-expansion" =<< x)
|
||||
return $ VWord n' w
|
||||
|
||||
| Just (n, el) <- isTSeq tp
|
||||
= do x' <- delay (Just msg) (fromSeq "during eta-expansion" =<< x)
|
||||
case numTValue n of
|
||||
Inf -> return $ VStream $ SeqMap $ \i ->
|
||||
go el (flip lookupSeqMap i =<< x')
|
||||
Nat n' -> return $ VSeq n' $ SeqMap $ \i -> do
|
||||
go el (flip lookupSeqMap i =<< x')
|
||||
|
||||
| Just (_t1,t2) <- isTFun tp
|
||||
= do x' <- delay (Just msg) (fromVFun <$> x)
|
||||
return $ VFun $ \a -> go t2 ( ($a) =<< x' )
|
||||
|
||||
| Just (n,ts) <- isTTuple tp
|
||||
= do x' <- delay (Just msg) (fromVTuple <$> x)
|
||||
return $ VTuple $
|
||||
[ go t =<< (flip genericIndex i <$> x')
|
||||
| i <- [0..(n-1)]
|
||||
| t <- ts
|
||||
]
|
||||
|
||||
| Just fs <- isTRec tp
|
||||
= do x' <- delay (Just msg) (fromVRecord <$> x)
|
||||
let err f = evalPanic "expected record value with field" [show f]
|
||||
return $ VRecord $
|
||||
[ (f, go t =<< (fromMaybe (err f) . lookup f <$> x'))
|
||||
| (f,t) <- fs
|
||||
]
|
||||
|
||||
|
||||
declHole :: Decl
|
||||
-> Eval (Name, Eval (GenValue b w), Eval (GenValue b w) -> Eval ())
|
||||
-> Eval (Name, Schema, Eval (GenValue b w), Eval (GenValue b w) -> Eval ())
|
||||
declHole d =
|
||||
case dDefinition d of
|
||||
DPrim -> evalPanic "Unexpected primitive declaration in recursive group"
|
||||
[show (ppLocName nm)]
|
||||
DExpr e -> do
|
||||
(hole, fill) <- blackhole msg
|
||||
return (nm, hole, fill)
|
||||
return (nm, sch, hole, fill)
|
||||
where
|
||||
nm = dName d
|
||||
sch = dSignature d
|
||||
msg = unwords ["<<loop>> while evaluating", show (pp nm)]
|
||||
|
||||
|
||||
@ -217,11 +316,10 @@ evalDecl :: EvalPrims b w
|
||||
-> GenEvalEnv b w
|
||||
-> Decl
|
||||
-> Eval (GenEvalEnv b w)
|
||||
evalDecl renv env d = bindVar (dName d) f env
|
||||
where
|
||||
f = case dDefinition d of
|
||||
DPrim -> return $ evalPrim d
|
||||
DExpr e -> evalExpr renv e
|
||||
evalDecl renv env d =
|
||||
case dDefinition d of
|
||||
DPrim -> bindVarDirect (dName d) (evalPrim d) env
|
||||
DExpr e -> bindVar (dName d) (evalExpr renv e) env
|
||||
|
||||
|
||||
-- Selectors -------------------------------------------------------------------
|
||||
@ -235,15 +333,15 @@ evalSel val sel = case sel of
|
||||
|
||||
TupleSel n _ -> tupleSel n val
|
||||
RecordSel n _ -> recordSel n val
|
||||
ListSel ix _ -> do xs <- fromSeq val
|
||||
lookupSeqMap xs (toInteger ix)
|
||||
|
||||
ListSel ix _ -> case val of
|
||||
VSeq _ xs' -> lookupSeqMap xs' (toInteger ix)
|
||||
VWord _ wv -> VBit <$> (flip indexWordValue (toInteger ix) =<< wv)
|
||||
where
|
||||
|
||||
tupleSel n v =
|
||||
case v of
|
||||
VTuple vs -> vs !! n
|
||||
VSeq w False vs -> VSeq w False <$> mapSeqMap (tupleSel n) vs
|
||||
VSeq w vs -> VSeq w <$> mapSeqMap (tupleSel n) vs
|
||||
VStream vs -> VStream <$> mapSeqMap (tupleSel n) vs
|
||||
VFun f -> return $ VFun (\x -> tupleSel n =<< f x)
|
||||
_ -> do vdoc <- ppValue defaultPPOpts v
|
||||
@ -254,7 +352,7 @@ evalSel val sel = case sel of
|
||||
recordSel n v =
|
||||
case v of
|
||||
VRecord {} -> lookupRecord n v
|
||||
VSeq w False vs -> VSeq w False <$> mapSeqMap (recordSel n) vs
|
||||
VSeq w vs -> VSeq w <$> mapSeqMap (recordSel n) vs
|
||||
VStream vs -> VStream <$> mapSeqMap (recordSel n) vs
|
||||
VFun f -> return $ VFun (\x -> recordSel n =<< f x)
|
||||
_ -> do vdoc <- ppValue defaultPPOpts v
|
||||
@ -354,8 +452,10 @@ evalMatch lenv m = case m of
|
||||
let stutter xs = \i -> xs (i `div` nLen)
|
||||
let lenv' = lenv { leVars = fmap stutter (leVars lenv) }
|
||||
let vs i = do let (q, r) = i `divMod` nLen
|
||||
xs <- fromSeq =<< lookupSeqMap vss q
|
||||
lookupSeqMap xs r
|
||||
lookupSeqMap vss q >>= \case
|
||||
VWord _ w -> VBit <$> (flip indexWordValue r =<< w)
|
||||
VSeq _ xs' -> lookupSeqMap xs' r
|
||||
VStream xs' -> lookupSeqMap xs' r
|
||||
return $ bindVarList n vs lenv'
|
||||
|
||||
Inf -> do
|
||||
@ -364,9 +464,11 @@ evalMatch lenv m = case m of
|
||||
, leStatic = allvars
|
||||
}
|
||||
let env = EvalEnv allvars (leTypes lenv)
|
||||
xs <- delay Nothing (fromSeq =<< evalExpr env expr)
|
||||
let vs i = do xseq <- xs
|
||||
lookupSeqMap xseq i
|
||||
xs <- evalExpr env expr
|
||||
let vs i = case xs of
|
||||
VWord _ w -> VBit <$> (flip indexWordValue i =<< w)
|
||||
VSeq _ xs' -> lookupSeqMap xs' i
|
||||
VStream xs' -> lookupSeqMap xs' i
|
||||
return $ bindVarList n vs lenv'
|
||||
|
||||
where
|
||||
@ -380,5 +482,6 @@ evalMatch lenv m = case m of
|
||||
where
|
||||
f env =
|
||||
case dDefinition d of
|
||||
-- Primitives here should never happen, I think...
|
||||
DPrim -> return $ evalPrim d
|
||||
DExpr e -> evalExpr env e
|
||||
|
@ -12,7 +12,8 @@
|
||||
{-# LANGUAGE CPP #-}
|
||||
module Cryptol.Eval.Env where
|
||||
|
||||
import Cryptol.Eval.Monad( Eval, delay )
|
||||
import Cryptol.Eval.Monad( Eval, delay, ready )
|
||||
import Cryptol.Eval.Type
|
||||
import Cryptol.Eval.Value
|
||||
import Cryptol.ModuleSystem.Name
|
||||
import Cryptol.TypeCheck.AST
|
||||
@ -65,7 +66,16 @@ bindVar :: Name
|
||||
bindVar n val env = do
|
||||
let nm = show $ ppLocName n
|
||||
val' <- delay (Just nm) val
|
||||
return $ env { envVars = Map.insert n val' (envVars env) }
|
||||
return $ env{ envVars = Map.insert n val' (envVars env) }
|
||||
|
||||
-- | Bind a variable to a value in the evaluation environment, without
|
||||
-- creating a thunk.
|
||||
bindVarDirect :: Name
|
||||
-> GenValue b w
|
||||
-> GenEvalEnv b w
|
||||
-> Eval (GenEvalEnv b w)
|
||||
bindVarDirect n val env = do
|
||||
return $ env{ envVars = Map.insert n (ready val) (envVars env) }
|
||||
|
||||
-- | Lookup a variable in the environment.
|
||||
{-# INLINE lookupVar #-}
|
||||
@ -81,3 +91,7 @@ bindType p ty env = env { envTypes = Map.insert p ty (envTypes env) }
|
||||
{-# INLINE lookupType #-}
|
||||
lookupType :: TVar -> GenEvalEnv b w -> Maybe TValue
|
||||
lookupType p env = Map.lookup p (envTypes env)
|
||||
|
||||
{-# INLINE evalType #-}
|
||||
evalType :: GenEvalEnv b w -> Type -> TValue
|
||||
evalType env = evalType' (envTypes env)
|
||||
|
@ -7,32 +7,114 @@
|
||||
-- Portability : portable
|
||||
|
||||
{-# LANGUAGE Safe, PatternGuards #-}
|
||||
{-# LANGUAGE DeriveGeneric #-}
|
||||
module Cryptol.Eval.Type where
|
||||
|
||||
module Cryptol.Eval.Type (evalType, evalTF) where
|
||||
|
||||
import Cryptol.Eval.Env
|
||||
import Cryptol.Eval.Monad
|
||||
import Cryptol.Eval.Value(TValue(..),numTValue)
|
||||
import Cryptol.TypeCheck.AST
|
||||
import Cryptol.TypeCheck.Solver.InfNat
|
||||
import Cryptol.Utils.Panic (panic)
|
||||
import Cryptol.Utils.Ident (Ident,mkIdent)
|
||||
|
||||
import Data.Maybe(fromMaybe)
|
||||
import qualified Data.Map.Strict as Map
|
||||
import GHC.Generics (Generic)
|
||||
import Control.DeepSeq
|
||||
import Control.DeepSeq.Generics
|
||||
|
||||
-- | An evaluated type.
|
||||
-- These types do not contain type variables, type synonyms, or type functions.
|
||||
newtype TValue = TValue { tValTy :: Type } deriving (Generic)
|
||||
|
||||
instance NFData TValue where rnf = genericRnf
|
||||
|
||||
instance Show TValue where
|
||||
showsPrec p (TValue v) = showsPrec p v
|
||||
|
||||
{-
|
||||
-- TODO? use these instead?
|
||||
-- Type Values -----------------------------------------------------------------
|
||||
|
||||
-- | An easy-to-use alternative representation for type `TValue`.
|
||||
data TypeVal
|
||||
= TVBit
|
||||
| TVSeq Int TypeVal
|
||||
| TVStream TypeVal
|
||||
| TVTuple [TypeVal]
|
||||
| TVRecord [(Ident, TypeVal)]
|
||||
| TVFun TypeVal TypeVal
|
||||
|
||||
toTypeVal :: TValue -> TypeVal
|
||||
toTypeVal ty
|
||||
| isTBit ty = TVBit
|
||||
| Just (n, ety) <- isTSeq ty = case numTValue n of
|
||||
Nat w -> TVSeq (fromInteger w) (toTypeVal ety)
|
||||
Inf -> TVStream (toTypeVal ety)
|
||||
| Just (aty, bty) <- isTFun ty = TVFun (toTypeVal aty) (toTypeVal bty)
|
||||
| Just (_, tys) <- isTTuple ty = TVTuple (map toTypeVal tys)
|
||||
| Just fields <- isTRec ty = TVRecord [ (n, toTypeVal aty) | (n, aty) <- fields ]
|
||||
| otherwise = panic "Cryptol.Symbolic.Prims.toTypeVal" [ "bad TValue" ]
|
||||
|
||||
-}
|
||||
|
||||
|
||||
isTBit :: TValue -> Bool
|
||||
isTBit (TValue ty) = case ty of
|
||||
TCon (TC TCBit) [] -> True
|
||||
_ -> False
|
||||
|
||||
isTSeq :: TValue -> Maybe (TValue, TValue)
|
||||
isTSeq (TValue (TCon (TC TCSeq) [t1,t2])) = Just (TValue t1, TValue t2)
|
||||
isTSeq _ = Nothing
|
||||
|
||||
isTFun :: TValue -> Maybe (TValue, TValue)
|
||||
isTFun (TValue (TCon (TC TCFun) [t1,t2])) = Just (TValue t1, TValue t2)
|
||||
isTFun _ = Nothing
|
||||
|
||||
isTTuple :: TValue -> Maybe (Int,[TValue])
|
||||
isTTuple (TValue (TCon (TC (TCTuple n)) ts)) = Just (n, map TValue ts)
|
||||
isTTuple _ = Nothing
|
||||
|
||||
isTRec :: TValue -> Maybe [(Ident, TValue)]
|
||||
isTRec (TValue (TRec fs)) = Just [ (x, TValue t) | (x,t) <- fs ]
|
||||
isTRec _ = Nothing
|
||||
|
||||
tvSeq :: TValue -> TValue -> TValue
|
||||
tvSeq (TValue x) (TValue y) = TValue (tSeq x y)
|
||||
|
||||
|
||||
|
||||
numTValue :: TValue -> Nat'
|
||||
numTValue (TValue ty) =
|
||||
case ty of
|
||||
TCon (TC (TCNum x)) _ -> Nat x
|
||||
TCon (TC TCInf) _ -> Inf
|
||||
_ -> panic "Cryptol.Eval.Value.numTValue" [ "Not a numeric type:", show ty ]
|
||||
|
||||
toNumTValue :: Nat' -> TValue
|
||||
toNumTValue (Nat n) = TValue (TCon (TC (TCNum n)) [])
|
||||
toNumTValue Inf = TValue (TCon (TC TCInf) [])
|
||||
|
||||
finTValue :: TValue -> Integer
|
||||
finTValue tval =
|
||||
case numTValue tval of
|
||||
Nat x -> x
|
||||
Inf -> panic "Cryptol.Eval.Value.finTValue" [ "Unexpected `inf`" ]
|
||||
|
||||
-- Type Evaluation -------------------------------------------------------------
|
||||
|
||||
-- | Evaluation for types.
|
||||
evalType :: GenEvalEnv b w -> Type -> TValue
|
||||
evalType env = TValue . go
|
||||
evalType' :: Map.Map TVar TValue -> Type -> TValue
|
||||
evalType' env = TValue . go
|
||||
where
|
||||
go ty =
|
||||
case ty of
|
||||
TVar tv ->
|
||||
case lookupType tv env of
|
||||
case Map.lookup tv env of
|
||||
Just (TValue v) -> v
|
||||
Nothing -> evalPanic "evalType" ["type variable not bound", show tv]
|
||||
|
||||
TCon (TF f) ts -> tValTy $ evalTF f $ map (evalType env) ts
|
||||
TCon (TF f) ts -> tValTy $ evalTF f $ map (evalType' env) ts
|
||||
TCon tc ts -> TCon tc (map go ts)
|
||||
TUser _ _ ty' -> go ty'
|
||||
TRec fields -> TRec [ (f,go t) | (f,t) <- fields ]
|
||||
|
@ -9,6 +9,7 @@
|
||||
{-# LANGUAGE PatternGuards #-}
|
||||
{-# LANGUAGE DeriveFunctor #-}
|
||||
{-# LANGUAGE DeriveGeneric #-}
|
||||
{-# LANGUAGE DoAndIfThenElse #-}
|
||||
{-# LANGUAGE FunctionalDependencies #-}
|
||||
{-# LANGUAGE FlexibleInstances #-}
|
||||
{-# LANGUAGE MultiParamTypeClasses #-}
|
||||
@ -22,12 +23,16 @@ module Cryptol.Eval.Value where
|
||||
import Data.Bits
|
||||
import Data.IORef
|
||||
--import Data.Map (Map)
|
||||
import qualified Data.Sequence as Seq
|
||||
import qualified Data.Map.Strict as Map
|
||||
import qualified Data.Foldable as Fold
|
||||
import qualified Data.Set as Set
|
||||
|
||||
import MonadLib
|
||||
|
||||
import qualified Cryptol.Eval.Arch as Arch
|
||||
import Cryptol.Eval.Monad
|
||||
import Cryptol.Eval.Type
|
||||
|
||||
import Cryptol.TypeCheck.AST
|
||||
import Cryptol.TypeCheck.Solver.InfNat(Nat'(..))
|
||||
@ -46,50 +51,7 @@ import GHC.Generics (Generic)
|
||||
import Control.DeepSeq
|
||||
import Control.DeepSeq.Generics
|
||||
|
||||
-- Utilities -------------------------------------------------------------------
|
||||
|
||||
isTBit :: TValue -> Bool
|
||||
isTBit (TValue ty) = case ty of
|
||||
TCon (TC TCBit) [] -> True
|
||||
_ -> False
|
||||
|
||||
isTSeq :: TValue -> Maybe (TValue, TValue)
|
||||
isTSeq (TValue (TCon (TC TCSeq) [t1,t2])) = Just (TValue t1, TValue t2)
|
||||
isTSeq _ = Nothing
|
||||
|
||||
isTFun :: TValue -> Maybe (TValue, TValue)
|
||||
isTFun (TValue (TCon (TC TCFun) [t1,t2])) = Just (TValue t1, TValue t2)
|
||||
isTFun _ = Nothing
|
||||
|
||||
isTTuple :: TValue -> Maybe (Int,[TValue])
|
||||
isTTuple (TValue (TCon (TC (TCTuple n)) ts)) = Just (n, map TValue ts)
|
||||
isTTuple _ = Nothing
|
||||
|
||||
isTRec :: TValue -> Maybe [(Ident, TValue)]
|
||||
isTRec (TValue (TRec fs)) = Just [ (x, TValue t) | (x,t) <- fs ]
|
||||
isTRec _ = Nothing
|
||||
|
||||
tvSeq :: TValue -> TValue -> TValue
|
||||
tvSeq (TValue x) (TValue y) = TValue (tSeq x y)
|
||||
|
||||
|
||||
|
||||
numTValue :: TValue -> Nat'
|
||||
numTValue (TValue ty) =
|
||||
case ty of
|
||||
TCon (TC (TCNum x)) _ -> Nat x
|
||||
TCon (TC TCInf) _ -> Inf
|
||||
_ -> panic "Cryptol.Eval.Value.numTValue" [ "Not a numeric type:", show ty ]
|
||||
|
||||
toNumTValue :: Nat' -> TValue
|
||||
toNumTValue (Nat n) = TValue (TCon (TC (TCNum n)) [])
|
||||
toNumTValue Inf = TValue (TCon (TC TCInf) [])
|
||||
|
||||
finTValue :: TValue -> Integer
|
||||
finTValue tval =
|
||||
case numTValue tval of
|
||||
Nat x -> x
|
||||
Inf -> panic "Cryptol.Eval.Value.finTValue" [ "Unexpected `inf`" ]
|
||||
import qualified Data.Cache.LRU.IO as LRU
|
||||
|
||||
|
||||
-- Values ----------------------------------------------------------------------
|
||||
@ -128,11 +90,7 @@ instance NFData (SeqMap b w) where
|
||||
|
||||
finiteSeqMap :: [Eval (GenValue b w)] -> Eval (SeqMap b w)
|
||||
finiteSeqMap xs = do
|
||||
v <- Seq.fromList <$> mapM (delay Nothing) xs
|
||||
let len = Seq.length v
|
||||
f (fromInteger -> i) | 0 <= i && i < len = Seq.index v i
|
||||
| otherwise = evalPanic "finiteSeqMap" ["Index out of bounds:", show i]
|
||||
return $ SeqMap f
|
||||
memoMap (SeqMap $ \i -> genericIndex xs i)
|
||||
|
||||
infiniteSeqMap :: [Eval (GenValue b w)] -> Eval (SeqMap b w)
|
||||
infiniteSeqMap xs =
|
||||
@ -153,23 +111,30 @@ splitSeqMap n xs = (hd,tl)
|
||||
hd = xs
|
||||
tl = SeqMap $ \i -> lookupSeqMap xs (i+n)
|
||||
|
||||
{-# INLINE memoMap #-}
|
||||
memoMap :: SeqMap b w -> Eval (SeqMap b w)
|
||||
memoMap x = do
|
||||
r <- io $ newIORef Map.empty
|
||||
return $ SeqMap $ \i -> do
|
||||
m <- io $ readIORef r
|
||||
case Map.lookup i m of
|
||||
Just (Just z) -> return z
|
||||
Just Nothing ->
|
||||
cryLoopError $ unwords ["memoMap location:", show i]
|
||||
Nothing -> do
|
||||
--io $ putStrLn $ unwords ["Forcing memo map location", show i]
|
||||
io $ writeIORef r (Map.insert i Nothing m)
|
||||
v <- lookupSeqMap x i
|
||||
io $ modifyIORef r (Map.insert i (Just v))
|
||||
return v
|
||||
-- TODO: make the size of the LRU cache a tuneable parameter...
|
||||
lru <- io $ LRU.newAtomicLRU (Just 64)
|
||||
holes <- io $ newIORef Set.empty
|
||||
return $ SeqMap $ memo holes lru
|
||||
|
||||
where
|
||||
memo holes lru i = do
|
||||
mz <- io $ LRU.lookup i lru
|
||||
case mz of
|
||||
Just z -> return z
|
||||
Nothing -> doEval holes lru i
|
||||
|
||||
doEval holes lru i = do
|
||||
hs <- io $ readIORef holes
|
||||
if Set.member i hs then
|
||||
cryLoopError ("memo map position" ++ show i)
|
||||
else do
|
||||
io $ writeIORef holes (Set.insert i hs)
|
||||
v <- lookupSeqMap x i
|
||||
io $ LRU.insert i v lru
|
||||
io $ modifyIORef' holes (Set.delete i)
|
||||
return v
|
||||
|
||||
zipSeqMap :: (GenValue b w -> GenValue b w -> Eval (GenValue b w))
|
||||
-> SeqMap b w
|
||||
@ -183,28 +148,49 @@ mapSeqMap :: (GenValue b w -> Eval (GenValue b w))
|
||||
mapSeqMap f x =
|
||||
memoMap (SeqMap $ \i -> f =<< lookupSeqMap x i)
|
||||
|
||||
data WordValue b w
|
||||
= WordVal !w
|
||||
| BitsVal !(Seq.Seq (Eval b))
|
||||
deriving (Generic)
|
||||
|
||||
asWordVal :: BitWord b w => WordValue b w -> Eval w
|
||||
asWordVal (WordVal w) = return w
|
||||
asWordVal (BitsVal bs) = packWord <$> sequence (Fold.toList bs)
|
||||
|
||||
asBitsVal :: BitWord b w => WordValue b w -> Seq.Seq (Eval b)
|
||||
asBitsVal (WordVal w) = Seq.fromList $ map ready $ unpackWord w
|
||||
asBitsVal (BitsVal bs) = bs
|
||||
|
||||
indexWordValue :: BitWord b w => WordValue b w -> Integer -> Eval b
|
||||
indexWordValue (WordVal w) idx = return $ genericIndex (unpackWord w) idx
|
||||
indexWordValue (BitsVal bs) idx = Seq.index bs (fromInteger idx)
|
||||
|
||||
|
||||
-- | Generic value type, parameterized by bit and word types.
|
||||
data GenValue b w
|
||||
= VRecord ![(Ident, Eval (GenValue b w))] -- @ { .. } @
|
||||
| VTuple ![Eval (GenValue b w)] -- @ ( .. ) @
|
||||
| VBit !b -- @ Bit @
|
||||
| VSeq !Integer !Bool !(SeqMap b w) -- @ [n]a @
|
||||
-- The boolean parameter indicates whether or not
|
||||
-- this is a sequence of bits.
|
||||
| VWord !w -- @ [n]Bit @
|
||||
| VSeq !Integer !(SeqMap b w) -- @ [n]a @
|
||||
-- Invariant: VSeq is never a sequence of bits
|
||||
| VWord !Integer !(Eval (WordValue b w)) -- @ [n]Bit @
|
||||
| VStream !(SeqMap b w) -- @ [inf]a @
|
||||
| VFun (Eval (GenValue b w) -> Eval (GenValue b w)) -- functions
|
||||
| VPoly (TValue -> Eval (GenValue b w)) -- polymorphic values (kind *)
|
||||
deriving (Generic)
|
||||
|
||||
|
||||
forceWordValue :: WordValue b w -> Eval ()
|
||||
forceWordValue (WordVal w) = return ()
|
||||
forceWordValue (BitsVal bs) = mapM_ (\b -> const () <$> b) bs
|
||||
|
||||
forceValue :: GenValue b w -> Eval ()
|
||||
forceValue v = case v of
|
||||
VRecord fs -> mapM_ (\x -> forceValue =<< snd x) fs
|
||||
VTuple xs -> mapM_ (forceValue =<<) xs
|
||||
VSeq n _ xs -> mapM_ (forceValue =<<) (enumerateSeqMap n xs)
|
||||
VBit b -> b `seq` return ()
|
||||
VWord w -> w `seq` return ()
|
||||
VSeq n xs -> mapM_ (forceValue =<<) (enumerateSeqMap n xs)
|
||||
VBit b -> return ()
|
||||
VWord _ wv -> forceWordValue =<< wv
|
||||
VStream _ -> return ()
|
||||
VFun _ -> return ()
|
||||
VPoly _ -> return ()
|
||||
@ -215,25 +201,17 @@ instance (Show b, Show w) => Show (GenValue b w) where
|
||||
VRecord fs -> "record:" ++ show (map fst fs)
|
||||
VTuple xs -> "tuple:" ++ show (length xs)
|
||||
VBit b -> show b
|
||||
VSeq n w _ -> "seq:" ++ show n ++ " " ++ show w
|
||||
VWord x -> "word:" ++ show x
|
||||
VSeq n _ -> "seq:" ++ show n
|
||||
VWord n _ -> "word:" ++ show n
|
||||
VStream _ -> "stream"
|
||||
VFun _ -> "fun"
|
||||
VPoly _ -> "poly"
|
||||
|
||||
instance (NFData b, NFData w) => NFData (WordValue b w) where rnf = genericRnf
|
||||
instance (NFData b, NFData w) => NFData (GenValue b w) where rnf = genericRnf
|
||||
|
||||
type Value = GenValue Bool BV
|
||||
|
||||
-- | An evaluated type.
|
||||
-- These types do not contain type variables, type synonyms, or type functions.
|
||||
newtype TValue = TValue { tValTy :: Type } deriving (Generic)
|
||||
|
||||
instance NFData TValue where rnf = genericRnf
|
||||
|
||||
instance Show TValue where
|
||||
showsPrec p (TValue v) = showsPrec p v
|
||||
|
||||
|
||||
-- Pretty Printing -------------------------------------------------------------
|
||||
|
||||
@ -268,10 +246,8 @@ ppValue opts = loop
|
||||
VTuple vals -> do vals' <- traverse (>>=loop) vals
|
||||
return $ parens (sep (punctuate comma vals'))
|
||||
VBit b -> return $ ppBit b
|
||||
VSeq sz isWord vals
|
||||
| isWord -> ppWord opts <$> fromVWord "ppValue" val
|
||||
| otherwise -> ppWordSeq sz vals
|
||||
VWord wd -> return $ ppWord opts wd
|
||||
VSeq sz vals -> ppWordSeq sz vals
|
||||
VWord _ wv -> ppWordVal =<< wv
|
||||
VStream vals -> do vals' <- traverse (>>=loop) $ enumerateSeqMap (useInfLength opts) vals
|
||||
return $ brackets $ fsep
|
||||
$ punctuate comma
|
||||
@ -280,6 +256,9 @@ ppValue opts = loop
|
||||
VFun _ -> return $ text "<function>"
|
||||
VPoly _ -> return $ text "<polymorphic value>"
|
||||
|
||||
ppWordVal :: WordValue b w -> Eval Doc
|
||||
ppWordVal w = ppWord opts <$> asWordVal w
|
||||
|
||||
ppWordSeq :: Integer -> SeqMap b w -> Eval Doc
|
||||
ppWordSeq sz vals = do
|
||||
ws <- sequence (enumerateSeqMap sz vals)
|
||||
@ -435,7 +414,7 @@ instance BitWord Bool BV where
|
||||
|
||||
-- | Create a packed word of n bits.
|
||||
word :: BitWord b w => Integer -> Integer -> GenValue b w
|
||||
word n i = VWord $ wordLit n i
|
||||
word n i = VWord n $ ready $ WordVal $ wordLit n i
|
||||
|
||||
lam :: (Eval (GenValue b w) -> Eval (GenValue b w)) -> GenValue b w
|
||||
lam = VFun
|
||||
@ -453,17 +432,20 @@ toStream :: [GenValue b w] -> Eval (GenValue b w)
|
||||
toStream vs =
|
||||
VStream <$> infiniteSeqMap (map ready vs)
|
||||
|
||||
toFinSeq :: Integer -> TValue -> [GenValue b w] -> Eval (GenValue b w)
|
||||
toFinSeq len elty vs =
|
||||
VSeq len (isTBit elty) <$> finiteSeqMap (map ready vs)
|
||||
toFinSeq :: BitWord b w
|
||||
=> Integer -> TValue -> [GenValue b w] -> Eval (GenValue b w)
|
||||
toFinSeq len elty vs
|
||||
| isTBit elty = return $ VWord len $ ready $ WordVal $ packWord $ map fromVBit vs
|
||||
| otherwise = VSeq len <$> finiteSeqMap (map ready vs)
|
||||
|
||||
-- | This is strict!
|
||||
boolToWord :: [Bool] -> Value
|
||||
boolToWord bs = VWord (packWord bs)
|
||||
boolToWord bs = VWord (genericLength bs) $ ready $ WordVal $ packWord bs
|
||||
|
||||
-- | Construct either a finite sequence, or a stream. In the finite case,
|
||||
-- record whether or not the elements were bits, to aid pretty-printing.
|
||||
toSeq :: TValue -> TValue -> [GenValue b w] -> Eval (GenValue b w)
|
||||
toSeq :: BitWord b w
|
||||
=> TValue -> TValue -> [GenValue b w] -> Eval (GenValue b w)
|
||||
toSeq len elty vals = case numTValue len of
|
||||
Nat n -> toFinSeq n elty vals
|
||||
Inf -> toStream vals
|
||||
@ -473,25 +455,12 @@ toSeq len elty vals = case numTValue len of
|
||||
-- record whether or not the elements were bits, to aid pretty-printing.
|
||||
mkSeq :: TValue -> TValue -> SeqMap b w -> GenValue b w
|
||||
mkSeq len elty vals = case numTValue len of
|
||||
Nat n -> VSeq n (isTBit elty) vals
|
||||
Inf -> VStream vals
|
||||
Nat n
|
||||
| isTBit elty -> VWord n $ return $ BitsVal $ Seq.fromFunction (fromInteger n) $ \i ->
|
||||
fromVBit <$> lookupSeqMap vals (toInteger i)
|
||||
| otherwise -> VSeq n vals
|
||||
Inf -> VStream vals
|
||||
|
||||
-- | Construct one of:
|
||||
-- * a word, when the sequence is finite and the elements are bits
|
||||
-- * a sequence, when the sequence is finite but the elements aren't bits
|
||||
-- * a stream, when the sequence is not finite
|
||||
--
|
||||
-- NOTE: do not use this constructor in the case where the thing may be a
|
||||
-- finite, but recursive, sequence.
|
||||
toPackedSeq :: TValue -> TValue -> SeqValMap -> Eval Value
|
||||
toPackedSeq len elty vals = case numTValue len of
|
||||
|
||||
-- finite sequence, pack a word if the elements are bits.
|
||||
Nat n | isTBit elty -> boolToWord <$> (traverse (fromVBit <$>) [ lookupSeqMap vals i | i <- [0 .. n-1] ])
|
||||
| otherwise -> return $ VSeq n False vals
|
||||
|
||||
-- infinite sequence, construct a stream
|
||||
Inf -> return $ VStream vals
|
||||
|
||||
-- Value Destructors -----------------------------------------------------------
|
||||
|
||||
@ -501,43 +470,49 @@ fromVBit val = case val of
|
||||
VBit b -> b
|
||||
_ -> evalPanic "fromVBit" ["not a Bit"]
|
||||
|
||||
bitsSeq :: BitWord b w => WordValue b w -> Integer -> Eval b
|
||||
bitsSeq (WordVal w) =
|
||||
let bs = unpackWord w
|
||||
in \i -> return $ genericIndex bs i
|
||||
bitsSeq (BitsVal bs) = \i -> Seq.index bs (fromInteger i)
|
||||
|
||||
-- | Extract a sequence.
|
||||
fromSeq :: forall b w. BitWord b w => GenValue b w -> Eval (SeqMap b w)
|
||||
fromSeq val = case val of
|
||||
VSeq _ _ vs -> return vs
|
||||
VWord bv -> do let bs = unpackWord bv
|
||||
return $ SeqMap $ (\i -> return . VBit . flip genericIndex i $ bs)
|
||||
VStream vs -> return vs
|
||||
_ -> evalPanic "fromSeq" ["not a sequence"]
|
||||
fromSeq :: forall b w. BitWord b w => String -> GenValue b w -> Eval (SeqMap b w)
|
||||
fromSeq msg val = case val of
|
||||
VSeq _ vs -> return vs
|
||||
VStream vs -> return vs
|
||||
_ -> evalPanic "fromSeq" ["not a sequence", msg]
|
||||
|
||||
fromStr :: Value -> Eval String
|
||||
fromStr (VSeq n _ vals) =
|
||||
fromStr (VSeq n vals) =
|
||||
traverse (\x -> toEnum . fromInteger <$> (fromWord "fromStr" =<< x)) (enumerateSeqMap n vals)
|
||||
fromStr _ = evalPanic "fromStr" ["Not a finite sequence"]
|
||||
|
||||
fromWordVal :: String -> GenValue b w -> Eval (WordValue b w)
|
||||
fromWordVal _msg (VWord _ wval) = wval
|
||||
fromWordVal msg _ = evalPanic "fromWordVal" ["not a word value", msg]
|
||||
|
||||
-- | Extract a packed word.
|
||||
fromVWord :: BitWord b w => String -> GenValue b w -> Eval w
|
||||
fromVWord msg val = case val of
|
||||
VWord bv -> return bv -- this should always mask
|
||||
VSeq n isWord bs | isWord -> packWord <$> traverse (fromVBit<$>) (enumerateSeqMap n bs)
|
||||
_ -> evalPanic "fromVWord" ["not a word", msg]
|
||||
fromVWord _msg (VWord _ wval) = wval >>= asWordVal
|
||||
fromVWord msg _ = evalPanic "fromVWord" ["not a word", msg]
|
||||
|
||||
vWordLen :: BitWord b w => GenValue b w -> Maybe Integer
|
||||
vWordLen val = case val of
|
||||
VWord w -> Just (wordLen w)
|
||||
VSeq n isWord _ | isWord -> Just n
|
||||
VWord n _wv -> Just n
|
||||
_ -> Nothing
|
||||
|
||||
-- | Turn a value into an integer represented by w bits.
|
||||
tryFromBits :: BitWord b w => [Eval (GenValue b w)] -> Maybe w
|
||||
tryFromBits = go id
|
||||
where
|
||||
go f [] = Just (packWord (f []))
|
||||
go f (Ready (VBit b):vs) = go ((b:) . f) vs
|
||||
go f (v:vs) = Nothing
|
||||
|
||||
|
||||
-- | Turn a value into an integer represented by w bits.
|
||||
fromWord :: String -> Value -> Eval Integer
|
||||
fromWord msg val =
|
||||
case val of
|
||||
VWord w -> return $ bvVal w
|
||||
VSeq n isWord bs | isWord -> bvVal . packWord <$> traverse (fromVBit<$>) (enumerateSeqMap n bs)
|
||||
_ -> do --vdoc <- ppValue defaultPPOpts val
|
||||
evalPanic "fromWord" ["not a word", msg]
|
||||
fromWord msg val = bvVal <$> fromVWord msg val
|
||||
|
||||
-- | Extract a function from a value.
|
||||
fromVFun :: GenValue b w -> (Eval (GenValue b w) -> Eval (GenValue b w))
|
||||
@ -593,14 +568,15 @@ toExpr prims t0 v0 = findOne (go t0 v0)
|
||||
ETuple `fmap` (zipWithM go ts =<< lift (sequence tvs))
|
||||
(TCon (TC TCBit) [], VBit True ) -> return (prim "True")
|
||||
(TCon (TC TCBit) [], VBit False) -> return (prim "False")
|
||||
(TCon (TC TCSeq) [a,b], VSeq 0 _ _) -> do
|
||||
(TCon (TC TCSeq) [a,b], VSeq 0 _) -> do
|
||||
guard (a == tZero)
|
||||
return $ EList [] b
|
||||
(TCon (TC TCSeq) [a,b], VSeq n _ svs) -> do
|
||||
(TCon (TC TCSeq) [a,b], VSeq n svs) -> do
|
||||
guard (a == tNum n)
|
||||
ses <- mapM (go b) =<< lift (sequence (enumerateSeqMap n svs))
|
||||
return $ EList ses b
|
||||
(TCon (TC TCSeq) [a,(TCon (TC TCBit) [])], VWord (BV w v)) -> do
|
||||
(TCon (TC TCSeq) [a,(TCon (TC TCBit) [])], VWord _ wval) -> do
|
||||
BV w v <- lift (asWordVal =<< wval)
|
||||
guard (a == tNum w)
|
||||
return $ ETApp (ETApp (prim "demote") (tNum v)) (tNum w)
|
||||
(_, VStream _) -> fail "cannot construct infinite expressions"
|
||||
|
@ -18,14 +18,14 @@
|
||||
{-# LANGUAGE BangPatterns #-}
|
||||
module Cryptol.Prims.Eval where
|
||||
|
||||
import Control.Monad (join)
|
||||
import Control.Monad (join, when)
|
||||
|
||||
import Cryptol.TypeCheck.AST
|
||||
import Cryptol.TypeCheck.Solver.InfNat (Nat'(..),fromNat,genLog, nMul)
|
||||
import qualified Cryptol.Eval.Arch as Arch
|
||||
import Cryptol.Eval.Env
|
||||
import Cryptol.Eval.Monad
|
||||
import Cryptol.Eval.Type(evalTF)
|
||||
import Cryptol.Eval.Type
|
||||
import Cryptol.Eval.Value
|
||||
import Cryptol.Testing.Random (randomValue)
|
||||
import Cryptol.Utils.Panic (panic)
|
||||
@ -33,9 +33,11 @@ import Cryptol.ModuleSystem.Name (asPrim)
|
||||
import Cryptol.Utils.Ident (Ident,mkIdent)
|
||||
import Cryptol.Utils.PP
|
||||
|
||||
import qualified Data.Foldable as Fold
|
||||
import Data.List (sortBy, transpose, genericTake, genericDrop,
|
||||
genericReplicate, genericSplitAt, genericIndex,
|
||||
foldl')
|
||||
import qualified Data.Sequence as Seq
|
||||
import Data.Ord (comparing)
|
||||
import Data.Bits (Bits(..))
|
||||
|
||||
@ -44,6 +46,8 @@ import qualified Data.Text as T
|
||||
|
||||
import System.Random.TF.Gen (seedTFGen)
|
||||
|
||||
import Debug.Trace(trace)
|
||||
|
||||
-- Primitives ------------------------------------------------------------------
|
||||
|
||||
instance EvalPrims Bool BV where
|
||||
@ -58,80 +62,120 @@ instance EvalPrims Bool BV where
|
||||
|
||||
primTable :: Map.Map Ident Value
|
||||
primTable = Map.fromList $ map (\(n, v) -> (mkIdent (T.pack n), v))
|
||||
[ ("+" , binary (arithBinary (liftBinArith (+))))
|
||||
, ("-" , binary (arithBinary (liftBinArith (-))))
|
||||
, ("*" , binary (arithBinary (liftBinArith (*))))
|
||||
, ("/" , binary (arithBinary (liftBinArith divWrap)))
|
||||
, ("%" , binary (arithBinary (liftBinArith modWrap)))
|
||||
, ("^^" , binary (arithBinary modExp))
|
||||
, ("lg2" , unary (arithUnary (liftUnaryArith lg2)))
|
||||
, ("negate" , unary (arithUnary (liftUnaryArith negate)))
|
||||
, ("<" , binary (cmpOrder "<" (\o -> o == LT )))
|
||||
, (">" , binary (cmpOrder ">" (\o -> o == GT )))
|
||||
, ("<=" , binary (cmpOrder "<=" (\o -> o == LT || o == EQ)))
|
||||
, (">=" , binary (cmpOrder ">=" (\o -> o == GT || o == EQ)))
|
||||
, ("==" , binary (cmpOrder "==" (\o -> o == EQ)))
|
||||
, ("!=" , binary (cmpOrder "!=" (\o -> o /= EQ)))
|
||||
, ("&&" , binary (logicBinary (.&.) (binBV (.&.))))
|
||||
, ("||" , binary (logicBinary (.|.) (binBV (.|.))))
|
||||
, ("^" , binary (logicBinary xor (binBV xor)))
|
||||
, ("complement" , unary (logicUnary complement (unaryBV complement)))
|
||||
, ("<<" , logicShift shiftLW shiftLS)
|
||||
, (">>" , logicShift shiftRW shiftRS)
|
||||
, ("<<<" , logicShift rotateLW rotateLS)
|
||||
, (">>>" , logicShift rotateRW rotateRS)
|
||||
[ ("+" , {-# SCC "Prelude::(+)" #-}
|
||||
binary (arithBinary (liftBinArith (+))))
|
||||
, ("-" , {-# SCC "Prelude::(-)" #-}
|
||||
binary (arithBinary (liftBinArith (-))))
|
||||
, ("*" , {-# SCC "Prelude::(*)" #-}
|
||||
binary (arithBinary (liftBinArith (*))))
|
||||
, ("/" , {-# SCC "Prelude::(/)" #-}
|
||||
binary (arithBinary (liftBinArith divWrap)))
|
||||
, ("%" , {-# SCC "Prelude::(%)" #-}
|
||||
binary (arithBinary (liftBinArith modWrap)))
|
||||
, ("^^" , {-# SCC "Prelude::(^^)" #-}
|
||||
binary (arithBinary modExp))
|
||||
, ("lg2" , {-# SCC "Prelude::lg2" #-}
|
||||
unary (arithUnary (liftUnaryArith lg2)))
|
||||
, ("negate" , {-# SCC "Prelude::negate" #-}
|
||||
unary (arithUnary (liftUnaryArith negate)))
|
||||
, ("<" , {-# SCC "Prelude::(<)" #-}
|
||||
binary (cmpOrder "<" (\o -> o == LT )))
|
||||
, (">" , {-# SCC "Prelude::(>)" #-}
|
||||
binary (cmpOrder ">" (\o -> o == GT )))
|
||||
, ("<=" , {-# SCC "Prelude::(<=)" #-}
|
||||
binary (cmpOrder "<=" (\o -> o == LT || o == EQ)))
|
||||
, (">=" , {-# SCC "Prelude::(>=)" #-}
|
||||
binary (cmpOrder ">=" (\o -> o == GT || o == EQ)))
|
||||
, ("==" , {-# SCC "Prelude::(==)" #-}
|
||||
binary (cmpOrder "==" (\o -> o == EQ)))
|
||||
, ("!=" , {-# SCC "Prelude::(!=)" #-}
|
||||
binary (cmpOrder "!=" (\o -> o /= EQ)))
|
||||
, ("&&" , {-# SCC "Prelude::(&&)" #-}
|
||||
binary (logicBinary (.&.) (binBV (.&.))))
|
||||
, ("||" , {-# SCC "Prelude::(||)" #-}
|
||||
binary (logicBinary (.|.) (binBV (.|.))))
|
||||
, ("^" , {-# SCC "Prelude::(^)" #-}
|
||||
binary (logicBinary xor (binBV xor)))
|
||||
, ("complement" , {-# SCC "Prelude::complement" #-}
|
||||
unary (logicUnary complement (unaryBV complement)))
|
||||
, ("<<" , {-# SCC "Prelude::(<<)" #-}
|
||||
logicShift shiftLW shiftLB shiftLS)
|
||||
, (">>" , {-# SCC "Prelude::(>>)" #-}
|
||||
logicShift shiftRW shiftLB shiftRS)
|
||||
, ("<<<" , {-# SCC "Prelude::(<<<)" #-}
|
||||
logicShift rotateLW rotateLB rotateLS)
|
||||
, (">>>" , {-# SCC "Prelude::(>>>)" #-}
|
||||
logicShift rotateRW rotateRB rotateRS)
|
||||
, ("True" , VBit True)
|
||||
, ("False" , VBit False)
|
||||
|
||||
, ("demote" , ecDemoteV)
|
||||
, ("demote" , {-# SCC "Prelude::demote" #-}
|
||||
ecDemoteV)
|
||||
|
||||
, ("#" , tlam $ \ front ->
|
||||
, ("#" , {-# SCC "Prelude::(#)" #-}
|
||||
tlam $ \ front ->
|
||||
tlam $ \ back ->
|
||||
tlam $ \ elty ->
|
||||
lam $ \ l -> return $
|
||||
lam $ \ r -> ccatV front back elty l r)
|
||||
lam $ \ r -> join (ccatV front back elty <$> l <*> r))
|
||||
|
||||
, ("@" , indexPrimOne indexFront_bits indexFront)
|
||||
, ("@@" , indexPrimMany indexFront_bits indexFront)
|
||||
, ("!" , indexPrimOne indexBack_bits indexBack)
|
||||
, ("!!" , indexPrimMany indexBack_bits indexBack)
|
||||
, ("@" , {-# SCC "Prelude::(@)" #-}
|
||||
indexPrimOne indexFront_bits indexFront)
|
||||
, ("@@" , {-# SCC "Prelude::(@@)" #-}
|
||||
indexPrimMany indexFront_bits indexFront)
|
||||
, ("!" , {-# SCC "Prelude::(!)" #-}
|
||||
indexPrimOne indexBack_bits indexBack)
|
||||
, ("!!" , {-# SCC "Prelude::(!!)" #-}
|
||||
indexPrimMany indexBack_bits indexBack)
|
||||
|
||||
, ("zero" , tlam zeroV)
|
||||
, ("zero" , {-# SCC "Prelude::zero" #-}
|
||||
tlam zeroV)
|
||||
|
||||
, ("join" , tlam $ \ parts ->
|
||||
, ("join" , {-# SCC "Prelude::join" #-}
|
||||
tlam $ \ parts ->
|
||||
tlam $ \ each ->
|
||||
tlam $ \ a ->
|
||||
lam $ \ x ->
|
||||
joinV parts each a =<< x)
|
||||
|
||||
, ("split" , ecSplitV)
|
||||
, ("split" , {-# SCC "Prelude::split" #-}
|
||||
ecSplitV)
|
||||
|
||||
, ("splitAt" , tlam $ \ front ->
|
||||
, ("splitAt" , {-# SCC "Prelude::splitAt" #-}
|
||||
tlam $ \ front ->
|
||||
tlam $ \ back ->
|
||||
tlam $ \ a ->
|
||||
lam $ \ x ->
|
||||
splitAtV front back a =<< x)
|
||||
|
||||
, ("fromThen" , fromThenV)
|
||||
, ("fromTo" , fromToV)
|
||||
, ("fromThenTo" , fromThenToV)
|
||||
, ("infFrom" , infFromV)
|
||||
, ("infFromThen", infFromThenV)
|
||||
, ("fromThen" , {-# SCC "Prelude::fromThen" #-}
|
||||
fromThenV)
|
||||
, ("fromTo" , {-# SCC "Prelude::fromTo" #-}
|
||||
fromToV)
|
||||
, ("fromThenTo" , {-# SCC "Prelude::fromThenTo" #-}
|
||||
fromThenToV)
|
||||
, ("infFrom" , {-# SCC "Prelude::infFrom" #-}
|
||||
infFromV)
|
||||
, ("infFromThen", {-# SCC "Prelude::infFromThen" #-}
|
||||
infFromThenV)
|
||||
|
||||
, ("error" , tlam $ \_ ->
|
||||
tlam $ \_ ->
|
||||
lam $ \s -> cryUserError =<< (fromStr =<< s))
|
||||
, ("error" , {-# SCC "Prelude::error" #-}
|
||||
tlam $ \a ->
|
||||
tlam $ \_ ->
|
||||
lam $ \s -> errorV a =<< (fromStr =<< s))
|
||||
|
||||
, ("reverse" , tlam $ \a ->
|
||||
, ("reverse" , {-# SCC "Prelude::reverse" #-}
|
||||
tlam $ \a ->
|
||||
tlam $ \b ->
|
||||
lam $ \xs -> reverseV =<< xs)
|
||||
|
||||
, ("transpose" , tlam $ \a ->
|
||||
, ("transpose" , {-# SCC "Prelude::transpose" #-}
|
||||
tlam $ \a ->
|
||||
tlam $ \b ->
|
||||
tlam $ \c ->
|
||||
lam $ \xs -> transposeV a b c =<< xs)
|
||||
|
||||
, ("pmult" ,
|
||||
, ("pmult" , {-# SCC "Prelude::pmult" #-}
|
||||
let mul !res !_ !_ 0 = res
|
||||
mul res bs as n = mul (if even as then res else xor res bs)
|
||||
(bs `shiftL` 1) (as `shiftR` 1) (n-1)
|
||||
@ -140,20 +184,24 @@ primTable = Map.fromList $ map (\(n, v) -> (mkIdent (T.pack n), v))
|
||||
wlam $ \(bvVal -> x) -> return $
|
||||
wlam $ \(bvVal -> y) -> return $ word (max 1 (a + b) - 1) (mul 0 x y b))
|
||||
|
||||
, ("pdiv" , tlam $ \(fromInteger . finTValue -> a) ->
|
||||
, ("pdiv" , {-# SCC "Prelude::pdiv" #-}
|
||||
tlam $ \(fromInteger . finTValue -> a) ->
|
||||
tlam $ \(fromInteger . finTValue -> b) ->
|
||||
wlam $ \(bvVal -> x) -> return $
|
||||
wlam $ \(bvVal -> y) -> return $ word (toInteger a)
|
||||
(fst (divModPoly x a y b)))
|
||||
|
||||
, ("pmod" , tlam $ \(fromInteger . finTValue -> a) ->
|
||||
, ("pmod" , {-# SCC "Prelude::pmod" #-}
|
||||
tlam $ \(fromInteger . finTValue -> a) ->
|
||||
tlam $ \(fromInteger . finTValue -> b) ->
|
||||
wlam $ \(bvVal -> x) -> return $
|
||||
wlam $ \(bvVal -> y) -> return $ word (toInteger b)
|
||||
(snd (divModPoly x a y (b+1))))
|
||||
, ("random" , tlam $ \a ->
|
||||
, ("random" , {-# SCC "Prelude::random" #-}
|
||||
tlam $ \a ->
|
||||
wlam $ \(bvVal -> x) -> return $ randomV a x)
|
||||
, ("trace" , tlam $ \_n ->
|
||||
, ("trace" , {-# SCC "Prelude::trace" #-}
|
||||
tlam $ \_n ->
|
||||
tlam $ \_a ->
|
||||
tlam $ \_b ->
|
||||
lam $ \s -> return $
|
||||
@ -172,11 +220,11 @@ primTable = Map.fromList $ map (\(n, v) -> (mkIdent (T.pack n), v))
|
||||
|
||||
|
||||
-- | Make a numeric constant.
|
||||
ecDemoteV :: Value
|
||||
ecDemoteV :: BitWord b w => GenValue b w
|
||||
ecDemoteV = tlam $ \valT ->
|
||||
tlam $ \bitT ->
|
||||
case (numTValue valT, numTValue bitT) of
|
||||
(Nat v, Nat bs) -> VWord (mkBv bs v)
|
||||
(Nat v, Nat bs) -> word bs v
|
||||
_ -> evalPanic "Cryptol.Eval.Prim.evalConst"
|
||||
["Unexpected Inf in constant."
|
||||
, show valT
|
||||
@ -295,10 +343,15 @@ arithBinary op = loop
|
||||
Nat w | isTBit a -> do
|
||||
lw <- fromVWord "arithLeft" l
|
||||
rw <- fromVWord "arithRight" r
|
||||
return $ VWord (op w lw rw)
|
||||
| otherwise -> VSeq w (isTBit a) <$> (join (zipSeqMap (loop a) <$> (fromSeq l) <*> (fromSeq r)))
|
||||
return $ VWord w $ ready $ WordVal $ op w lw rw
|
||||
| otherwise -> VSeq w <$> (join (zipSeqMap (loop a) <$>
|
||||
(fromSeq "arithBinary left" l) <*>
|
||||
(fromSeq "arithBinary right" r)))
|
||||
|
||||
-- streams
|
||||
Inf -> VStream <$> (join (zipSeqMap (loop a) <$> (fromSeq l) <*> (fromSeq r)))
|
||||
Inf -> VStream <$> (join (zipSeqMap (loop a) <$>
|
||||
(fromSeq "arithBinary left" l) <*>
|
||||
(fromSeq "arithBinary right" r)))
|
||||
|
||||
-- functions
|
||||
| Just (_,ety) <- isTFun ty =
|
||||
@ -344,10 +397,10 @@ arithUnary op = loop
|
||||
-- words and finite sequences
|
||||
Nat w | isTBit a -> do
|
||||
wx <- fromVWord "arithUnary" x
|
||||
return $ VWord $ op w wx
|
||||
| otherwise -> VSeq w (isTBit a) <$> (mapSeqMap (loop a) =<< fromSeq x)
|
||||
return $ VWord w $ ready $ WordVal $ op w wx
|
||||
| otherwise -> VSeq w <$> (mapSeqMap (loop a) =<< fromSeq "arithUnary" x)
|
||||
|
||||
Inf -> VStream <$> (mapSeqMap (loop a) =<< fromSeq x)
|
||||
Inf -> VStream <$> (mapSeqMap (loop a) =<< fromSeq "arithUnary" x)
|
||||
|
||||
-- functions
|
||||
| Just (_,ety) <- isTFun ty =
|
||||
@ -389,17 +442,15 @@ lexCompare nm ty l r
|
||||
return $ compare (fromVBit l) (fromVBit r)
|
||||
|
||||
| Just (_,b) <- isTSeq ty, isTBit b = do
|
||||
--ldoc <- ppValue defaultPPOpts l
|
||||
--io $ putStrLn $ unwords ["lexCompare left", nm, show l]
|
||||
compare <$> (fromWord "compareLeft" l) <*> (fromWord "compareRight" r)
|
||||
|
||||
| Just (len,e) <- isTSeq ty = case numTValue len of
|
||||
Nat w -> join (zipLexCompare nm (repeat e) <$>
|
||||
(enumerateSeqMap w <$> fromSeq l) <*>
|
||||
(enumerateSeqMap w <$> fromSeq r))
|
||||
(enumerateSeqMap w <$> fromSeq "lexCompare left" l) <*>
|
||||
(enumerateSeqMap w <$> fromSeq "lexCompare right" r))
|
||||
Inf -> join (zipLexCompare nm (repeat e) <$>
|
||||
(streamSeqMap <$> fromSeq l) <*>
|
||||
(streamSeqMap <$> fromSeq r))
|
||||
(streamSeqMap <$> fromSeq "lexCompare left" l) <*>
|
||||
(streamSeqMap <$> fromSeq "lexCompare right" r))
|
||||
|
||||
-- tuples
|
||||
| Just (_,etys) <- isTTuple ty =
|
||||
@ -476,7 +527,7 @@ zeroV ty
|
||||
-- sequences
|
||||
| Just (n,ety) <- isTSeq ty =
|
||||
case numTValue n of
|
||||
Nat w | isTBit ety -> VWord $ wordLit w 0
|
||||
Nat w | isTBit ety -> word w 0
|
||||
| otherwise -> mkSeq n ety (SeqMap $ \_ -> ready $ zeroV ety)
|
||||
Inf -> mkSeq n ety (SeqMap $ \_ -> ready $ zeroV ety)
|
||||
|
||||
@ -495,27 +546,29 @@ zeroV ty
|
||||
| otherwise = evalPanic "zeroV" ["invalid type for zero"]
|
||||
|
||||
|
||||
joinWordVal :: BitWord b w =>
|
||||
WordValue b w -> WordValue b w -> WordValue b w
|
||||
joinWordVal (WordVal w1) (WordVal w2) = WordVal $ joinWord w1 w2
|
||||
joinWordVal w1 w2 = BitsVal $ (asBitsVal w1) Seq.>< (asBitsVal w2)
|
||||
|
||||
joinWords :: forall b w
|
||||
. BitWord b w
|
||||
=> Integer
|
||||
-> Integer
|
||||
-> SeqMap b w
|
||||
-> Eval (GenValue b w)
|
||||
-> Eval (GenValue b w)
|
||||
joinWords nParts nEach xs fallback =
|
||||
loop (wordLit 0 0) (enumerateSeqMap nParts xs)
|
||||
joinWords nParts nEach xs =
|
||||
loop (ready $ WordVal (wordLit 0 0)) (enumerateSeqMap nParts xs)
|
||||
|
||||
where
|
||||
loop :: w -> [Eval (GenValue b w)] -> Eval (GenValue b w)
|
||||
loop !bv [] = return $ VWord bv
|
||||
loop !bv (Ready (VWord w) : ws) = loop (joinWord bv w) ws
|
||||
|
||||
-- loop !bv (w : ws) = w >>= \case
|
||||
-- VWord w' -> loop (joinWord bv w') ws
|
||||
-- _ -> fallback
|
||||
|
||||
loop _ _ = fallback
|
||||
loop :: Eval (WordValue b w) -> [Eval (GenValue b w)] -> Eval (GenValue b w)
|
||||
loop !wv [] = return $ VWord (nParts * nEach) wv
|
||||
loop !wv (w : ws) = do
|
||||
w >>= \case
|
||||
VWord _ w' -> loop (joinWordVal <$> wv <*> w') ws
|
||||
_ -> evalPanic "joinWords: expected word value" []
|
||||
|
||||
-- loop !bv (Ready (VWord w) : ws) = loop (joinWord bv w) ws
|
||||
-- loop !bv (w:ws) = do
|
||||
-- w' <- fromVWord "joinWords" =<< w
|
||||
-- loop (joinWord bv w') ws
|
||||
@ -531,14 +584,14 @@ joinSeq parts each a xs
|
||||
| Nat nEach <- numTValue each
|
||||
= return $ mkSeq $ (SeqMap $ \i -> do
|
||||
let (q,r) = divMod i nEach
|
||||
ys <- fromSeq =<< lookupSeqMap xs q
|
||||
ys <- fromSeq "join seq" =<< lookupSeqMap xs q
|
||||
lookupSeqMap ys r)
|
||||
|
||||
where
|
||||
len = numTValue parts `nMul` numTValue each
|
||||
mkSeq = case len of
|
||||
Inf -> VStream
|
||||
Nat n -> VSeq n (isTBit a)
|
||||
Nat n -> VSeq n
|
||||
|
||||
-- | Join a sequence of sequences into a single sequence.
|
||||
joinV :: BitWord b w
|
||||
@ -554,13 +607,25 @@ joinV parts each a val
|
||||
| Nat nParts <- numTValue parts
|
||||
, Nat nEach <- numTValue each
|
||||
, isTBit a
|
||||
= do xs <- fromSeq val
|
||||
joinWords nParts nEach xs (joinSeq parts each a xs)
|
||||
= do xs <- fromSeq "joinV" val
|
||||
joinWords nParts nEach xs
|
||||
|
||||
joinV parts each a val =
|
||||
joinSeq parts each a =<< fromSeq val
|
||||
joinSeq parts each a =<< fromSeq "joinV" val
|
||||
|
||||
|
||||
splitWordVal :: BitWord b w
|
||||
=> Integer
|
||||
-> Integer
|
||||
-> WordValue b w
|
||||
-> (WordValue b w, WordValue b w)
|
||||
splitWordVal leftWidth rightWidth (WordVal w) =
|
||||
let (lw, rw) = splitWord leftWidth rightWidth w
|
||||
in (WordVal lw, WordVal rw)
|
||||
splitWordVal leftWidth rightWidth (BitsVal bs) =
|
||||
let (lbs, rbs) = Seq.splitAt (fromInteger leftWidth) bs
|
||||
in (BitsVal lbs, BitsVal rbs)
|
||||
|
||||
splitAtV :: BitWord b w
|
||||
=> TValue
|
||||
-> TValue
|
||||
@ -570,18 +635,28 @@ splitAtV :: BitWord b w
|
||||
splitAtV front back a val =
|
||||
case numTValue back of
|
||||
|
||||
Nat rightWidth | aBit, VWord w <- val -> do
|
||||
let (lw, rw) = splitWord leftWidth rightWidth w
|
||||
Nat rightWidth | aBit, VWord _ w <- val -> do
|
||||
ws <- delay Nothing (splitWordVal leftWidth rightWidth <$> w)
|
||||
return $ VTuple
|
||||
[ ready $ VWord lw
|
||||
, ready $ VWord rw
|
||||
[ VWord leftWidth . ready . fst <$> ws
|
||||
, VWord rightWidth . ready . snd <$> ws
|
||||
]
|
||||
|
||||
Inf | aBit, VStream seq <- val -> do
|
||||
seq <- delay Nothing (fromSeq "splitAtV" val)
|
||||
ls <- delay Nothing (do m <- fst . splitSeqMap leftWidth <$> seq
|
||||
let ms = map (fromVBit <$>) (enumerateSeqMap leftWidth m)
|
||||
return $ Seq.fromList $ ms)
|
||||
rs <- delay Nothing (snd . splitSeqMap leftWidth <$> seq)
|
||||
return $ VTuple [ return $ VWord leftWidth (BitsVal <$> ls)
|
||||
, mkSeq back a <$> rs
|
||||
]
|
||||
|
||||
_ -> do
|
||||
seq <- delay Nothing (fromSeq val)
|
||||
seq <- delay Nothing (fromSeq "splitAtV" val)
|
||||
ls <- delay Nothing (fst . splitSeqMap leftWidth <$> seq)
|
||||
rs <- delay Nothing (snd . splitSeqMap leftWidth <$> seq)
|
||||
return $ VTuple [ VSeq leftWidth aBit <$> ls
|
||||
return $ VTuple [ VSeq leftWidth <$> ls
|
||||
, mkSeq back a <$> rs
|
||||
]
|
||||
|
||||
@ -593,6 +668,18 @@ splitAtV front back a val =
|
||||
_ -> evalPanic "splitAtV" ["invalid `front` len"]
|
||||
|
||||
|
||||
extractWordVal :: BitWord b w
|
||||
=> Integer
|
||||
-> Integer
|
||||
-> WordValue b w
|
||||
-> WordValue b w
|
||||
extractWordVal len start (WordVal w) =
|
||||
WordVal $ extractWord len start w
|
||||
extractWordVal len start (BitsVal bs) =
|
||||
BitsVal $ Seq.take (fromInteger len) $
|
||||
Seq.drop (Seq.length bs - fromInteger start - fromInteger len - 1) bs
|
||||
|
||||
|
||||
-- | Split implementation.
|
||||
ecSplitV :: BitWord b w
|
||||
=> GenValue b w
|
||||
@ -603,46 +690,34 @@ ecSplitV =
|
||||
lam $ \ val ->
|
||||
case (numTValue parts, numTValue each) of
|
||||
(Nat p, Nat e) | isTBit a -> do
|
||||
val' <- delay Nothing (fromVWord "split" =<< val)
|
||||
return $ VSeq p False $ SeqMap $ \i -> do
|
||||
VWord . extractWord e ((p-i-1)*e) <$> val'
|
||||
VWord _ val' <- val
|
||||
return $ VSeq p $ SeqMap $ \i -> do
|
||||
return $ VWord e (extractWordVal e ((p-i-1)*e) <$> val')
|
||||
(Nat p, Nat e) -> do
|
||||
val' <- delay Nothing (fromSeq =<< val)
|
||||
return $ VSeq p False $ SeqMap $ \i ->
|
||||
return $ VSeq e (isTBit a) $ SeqMap $ \j -> do
|
||||
val' <- delay Nothing (fromSeq "ecSplitV" =<< val)
|
||||
return $ VSeq p $ SeqMap $ \i ->
|
||||
return $ VSeq e $ SeqMap $ \j -> do
|
||||
xs <- val'
|
||||
lookupSeqMap xs (e * i + j)
|
||||
(Inf , Nat e) -> do
|
||||
val' <- delay Nothing (fromSeq =<< val)
|
||||
val' <- delay Nothing (fromSeq "ecSplitV" =<< val)
|
||||
return $ VStream $ SeqMap $ \i ->
|
||||
return $ VSeq e (isTBit a) $ SeqMap $ \j -> do
|
||||
return $ VSeq e $ SeqMap $ \j -> do
|
||||
xs <- val'
|
||||
lookupSeqMap xs (e * i + j)
|
||||
_ -> evalPanic "splitV" ["invalid type arguments to split"]
|
||||
|
||||
-- | Split into infinitely many chunks
|
||||
infChunksOf :: Integer -> [a] -> [[a]]
|
||||
infChunksOf each xs = let (as,bs) = genericSplitAt each xs
|
||||
in as : infChunksOf each bs
|
||||
|
||||
-- | Split into finitely many chunks
|
||||
finChunksOf :: Integer -> Integer -> [a] -> [[a]]
|
||||
finChunksOf 0 _ _ = []
|
||||
finChunksOf parts each xs = let (as,bs) = genericSplitAt each xs
|
||||
in as : finChunksOf (parts - 1) each bs
|
||||
|
||||
|
||||
reverseV :: forall b w
|
||||
. BitWord b w
|
||||
=> GenValue b w
|
||||
-> Eval (GenValue b w)
|
||||
reverseV (VSeq n isWord xs) =
|
||||
return $ VSeq n isWord $ reverseSeqMap n xs
|
||||
reverseV (VWord w) = return (VWord revword)
|
||||
reverseV (VSeq n xs) =
|
||||
return $ VSeq n $ reverseSeqMap n xs
|
||||
reverseV (VWord n wv) = return (VWord n (revword <$> wv))
|
||||
where
|
||||
revword = do
|
||||
let bs = unpackWord w :: [b]
|
||||
in packWord $ reverse bs
|
||||
revword (WordVal w) = BitsVal $ Seq.reverse $ Seq.fromList $ map ready $ unpackWord w
|
||||
revword (BitsVal bs) = BitsVal $ Seq.reverse bs
|
||||
reverseV _ =
|
||||
evalPanic "reverseV" ["Not a finite sequence"]
|
||||
|
||||
@ -653,48 +728,75 @@ transposeV :: BitWord b w
|
||||
-> TValue
|
||||
-> GenValue b w
|
||||
-> Eval (GenValue b w)
|
||||
transposeV a b c xs = do
|
||||
let bseq =
|
||||
transposeV a b c xs
|
||||
| isTBit c, Nat na <- numTValue a =
|
||||
return $ bseq $ SeqMap $ \bi ->
|
||||
return $ VWord na $ return $ BitsVal $
|
||||
Seq.fromFunction (fromInteger na) $ \ai -> do
|
||||
ys <- flip lookupSeqMap (toInteger ai) =<< fromSeq "transposeV" xs
|
||||
case ys of
|
||||
VStream ys' -> fromVBit <$> lookupSeqMap ys' bi
|
||||
VWord _ wv -> flip bitsSeq bi =<< wv
|
||||
|
||||
| otherwise = do
|
||||
return $ bseq $ SeqMap $ \bi ->
|
||||
return $ aseq $ SeqMap $ \ai -> do
|
||||
ys <- flip lookupSeqMap ai =<< fromSeq "transposeV 1" xs
|
||||
z <- flip lookupSeqMap bi =<< fromSeq "transposeV 2" ys
|
||||
return z
|
||||
|
||||
where
|
||||
bseq =
|
||||
case numTValue b of
|
||||
Nat nb -> VSeq nb (isTBit b)
|
||||
Nat nb -> VSeq nb
|
||||
Inf -> VStream
|
||||
let aseq =
|
||||
aseq =
|
||||
case numTValue a of
|
||||
Nat na -> VSeq na (isTBit a)
|
||||
Nat na -> VSeq na
|
||||
Inf -> VStream
|
||||
return $ bseq $ SeqMap $ \bi ->
|
||||
return $ aseq $ SeqMap $ \ai -> do
|
||||
ys <- flip lookupSeqMap ai =<< fromSeq xs
|
||||
z <- flip lookupSeqMap bi =<< fromSeq ys
|
||||
return z
|
||||
|
||||
|
||||
ccatV :: BitWord b w
|
||||
|
||||
|
||||
ccatV :: (Show b, Show w, BitWord b w)
|
||||
=> TValue
|
||||
-> TValue
|
||||
-> TValue
|
||||
-> (GenValue b w)
|
||||
-> (GenValue b w)
|
||||
-> Eval (GenValue b w)
|
||||
-> Eval (GenValue b w)
|
||||
-> Eval (GenValue b w)
|
||||
ccatV _front _back (isTBit -> True) (Ready (VWord x)) (Ready (VWord y)) =
|
||||
return $ VWord $ joinWord x y
|
||||
|
||||
-- ccatV _front (numTValue -> Nat _nBack) (isTBit -> True) x y = do
|
||||
-- xw <- fromVWord "ccatV" =<< x
|
||||
-- yw <- fromVWord "ccatV" =<< y
|
||||
-- return $ VWord $ joinWord xw yw
|
||||
ccatV front back elty (VWord m l) (VWord n r) =
|
||||
return $ VWord (m+n) (joinWordVal <$> l <*> r)
|
||||
|
||||
ccatV front back elty (VWord m l) (VStream r) =
|
||||
return $ VStream $ SeqMap $ \i ->
|
||||
if i < m then
|
||||
VBit <$> (flip indexWordValue i =<< l)
|
||||
else
|
||||
lookupSeqMap r (i-m)
|
||||
|
||||
ccatV front back elty l r = do
|
||||
l' <- delay Nothing (fromSeq =<< l)
|
||||
r' <- delay Nothing (fromSeq =<< r)
|
||||
let Nat n = numTValue front
|
||||
mkSeq (evalTF TCAdd [front,back]) elty <$> return (SeqMap $ \i ->
|
||||
if i < n then do
|
||||
ls <- l'
|
||||
lookupSeqMap ls i
|
||||
else do
|
||||
rs <- r'
|
||||
lookupSeqMap rs (i-n))
|
||||
l'' <- delay Nothing (fromSeq "ccatV left" l)
|
||||
r'' <- delay Nothing (fromSeq "ccatV right" r)
|
||||
let Nat n = numTValue front
|
||||
mkSeq (evalTF TCAdd [front,back]) elty <$> return (SeqMap $ \i ->
|
||||
if i < n then do
|
||||
ls <- l''
|
||||
lookupSeqMap ls i
|
||||
else do
|
||||
rs <- r''
|
||||
lookupSeqMap rs (i-n))
|
||||
|
||||
wordValLogicOp :: BitWord b w
|
||||
=> (b -> b -> b)
|
||||
-> (w -> w -> w)
|
||||
-> WordValue b w
|
||||
-> WordValue b w
|
||||
-> WordValue b w
|
||||
wordValLogicOp _ wop (WordVal w1) (WordVal w2) = WordVal (wop w1 w2)
|
||||
wordValLogicOp bop _ w1 w2 =
|
||||
BitsVal $ Seq.zipWith (\x y -> bop <$> x <*> y) (asBitsVal w1) (asBitsVal w2)
|
||||
|
||||
-- | Merge two values given a binop. This is used for and, or and xor.
|
||||
logicBinary :: forall b w
|
||||
@ -722,8 +824,8 @@ logicBinary opb opw = loop
|
||||
case numTValue len of
|
||||
|
||||
-- words or finite sequences
|
||||
Nat w | isTBit aty, VWord lw <- l, VWord rw <- r
|
||||
-> return $ VWord $ opw lw rw
|
||||
Nat w | isTBit aty, VWord _ lw <- l, VWord _ rw <- r
|
||||
-> return $ VWord w (wordValLogicOp opb opw <$> lw <*> rw)
|
||||
-- We assume that bitwise ops do not need re-masking
|
||||
|
||||
-- Nat w | isTBit aty -> do
|
||||
@ -731,12 +833,15 @@ logicBinary opb opw = loop
|
||||
-- BV _ rw <- fromVWord "logicRight" r
|
||||
-- return $ VWord $ mkBv w (op lw rw)
|
||||
|
||||
| otherwise -> VSeq w (isTBit aty) <$>
|
||||
| otherwise -> VSeq w <$>
|
||||
(join (zipSeqMap (loop aty) <$>
|
||||
(fromSeq l) <*> (fromSeq r)))
|
||||
(fromSeq "logicBinary left" l)
|
||||
<*> (fromSeq "logicBinary right" r)))
|
||||
|
||||
-- streams
|
||||
Inf -> VStream <$> (join (zipSeqMap (loop aty) <$> (fromSeq l) <*> (fromSeq r)))
|
||||
Inf -> VStream <$> (join (zipSeqMap (loop aty) <$>
|
||||
(fromSeq "logicBinary left" l) <*>
|
||||
(fromSeq "logicBinary right" r)))
|
||||
|
||||
| Just (_,etys) <- isTTuple ty = do
|
||||
let ls = fromVTuple l
|
||||
@ -756,6 +861,14 @@ logicBinary opb opw = loop
|
||||
| otherwise = evalPanic "logicBinary" ["invalid logic type"]
|
||||
|
||||
|
||||
wordValUnaryOp :: BitWord b w
|
||||
=> (b -> b)
|
||||
-> (w -> w)
|
||||
-> WordValue b w
|
||||
-> WordValue b w
|
||||
wordValUnaryOp _ wop (WordVal w) = WordVal (wop w)
|
||||
wordValUnaryOp bop _ (BitsVal bs) = BitsVal (fmap (bop <$>) bs)
|
||||
|
||||
logicUnary :: forall b w
|
||||
. BitWord b w
|
||||
=> (b -> b)
|
||||
@ -775,18 +888,18 @@ logicUnary opb opw = loop
|
||||
case numTValue len of
|
||||
|
||||
-- words or finite sequences
|
||||
Nat w | isTBit ety, VWord v <- val
|
||||
-> return $ VWord $ opw v
|
||||
Nat w | isTBit ety, VWord _ wv <- val
|
||||
-> return $ VWord w (wordValUnaryOp opb opw <$> wv)
|
||||
|
||||
-- Nat w | isTBit ety
|
||||
-- -> do v <- fromWord "logicUnary" val
|
||||
-- return $ VWord (mkBv w $ op v)
|
||||
|
||||
| otherwise
|
||||
-> VSeq w (isTBit ety) <$> (mapSeqMap (loop ety) =<< fromSeq val)
|
||||
-> VSeq w <$> (mapSeqMap (loop ety) =<< fromSeq "logicUnary" val)
|
||||
|
||||
-- streams
|
||||
Inf -> VStream <$> (mapSeqMap (loop ety) =<< fromSeq val)
|
||||
Inf -> VStream <$> (mapSeqMap (loop ety) =<< fromSeq "logicUnary" val)
|
||||
|
||||
| Just (_,etys) <- isTTuple ty =
|
||||
let as = fromVTuple val
|
||||
@ -804,21 +917,22 @@ logicUnary opb opw = loop
|
||||
logicShift :: (Integer -> Integer -> Integer -> Integer)
|
||||
-- ^ The function may assume its arguments are masked.
|
||||
-- It is responsible for masking its result if needed.
|
||||
-> (Integer -> Seq.Seq (Eval Bool) -> Integer -> Seq.Seq (Eval Bool))
|
||||
-> (TValue -> TValue -> SeqValMap -> Integer -> SeqValMap)
|
||||
-> Value
|
||||
logicShift opW opS
|
||||
logicShift opW obB opS
|
||||
= tlam $ \ a ->
|
||||
tlam $ \ _ ->
|
||||
tlam $ \ c ->
|
||||
lam $ \ l -> return $
|
||||
lam $ \ r -> do
|
||||
case l of
|
||||
Ready (VWord (BV w x)) -> do
|
||||
BV _ i <- fromVWord "logicShift amount" =<< r
|
||||
return $ VWord $ BV w $ opW w x i
|
||||
_ -> do
|
||||
BV _ i <- fromVWord "logicShift amount" =<< r
|
||||
mkSeq a c <$> (opS a c <$> (fromSeq =<< l) <*> return i)
|
||||
BV _ i <- fromVWord "logicShift amount" =<< r
|
||||
l >>= \case
|
||||
VWord w wv -> return $ VWord w $ wv >>= \case
|
||||
BitsVal bs -> return $ BitsVal (obB w bs i)
|
||||
WordVal (BV _ x) -> return $ WordVal (BV w (opW w x i))
|
||||
|
||||
l' -> mkSeq a c <$> (opS a c <$> (fromSeq "logicShift" =<< l) <*> return i)
|
||||
|
||||
-- Left shift for words.
|
||||
shiftLW :: Integer -> Integer -> Integer -> Integer
|
||||
@ -826,6 +940,12 @@ shiftLW w ival by
|
||||
| by >= w = 0
|
||||
| otherwise = mask w (shiftL ival (fromInteger by))
|
||||
|
||||
shiftLB :: Integer -> Seq.Seq (Eval Bool) -> Integer -> Seq.Seq (Eval Bool)
|
||||
shiftLB w bs by =
|
||||
Seq.drop (fromInteger (min w by)) bs
|
||||
Seq.><
|
||||
Seq.replicate (fromInteger (min w by)) (ready False)
|
||||
|
||||
shiftLS :: TValue -> TValue -> SeqValMap -> Integer -> SeqValMap
|
||||
shiftLS w ety vs by = SeqMap $ \i ->
|
||||
case numTValue w of
|
||||
@ -840,6 +960,12 @@ shiftRW w i by
|
||||
| by >= w = 0
|
||||
| otherwise = shiftR i (fromInteger by)
|
||||
|
||||
shiftRB :: Integer -> Seq.Seq (Eval Bool) -> Integer -> Seq.Seq (Eval Bool)
|
||||
shiftRB w bs by =
|
||||
Seq.replicate (fromInteger (min w by)) (ready False)
|
||||
Seq.><
|
||||
Seq.take (fromInteger (w - min w by)) bs
|
||||
|
||||
shiftRS :: TValue -> TValue -> SeqValMap -> Integer -> SeqValMap
|
||||
shiftRS w ety vs by = SeqMap $ \i ->
|
||||
case numTValue w of
|
||||
@ -858,6 +984,11 @@ rotateLW 0 i _ = i
|
||||
rotateLW w i by = mask w $ (i `shiftL` b) .|. (i `shiftR` (fromInteger w - b))
|
||||
where b = fromInteger (by `mod` w)
|
||||
|
||||
rotateLB :: Integer -> Seq.Seq (Eval Bool) -> Integer -> Seq.Seq (Eval Bool)
|
||||
rotateLB w bs by =
|
||||
let (hd,tl) = Seq.splitAt (fromInteger (by `mod` w)) bs
|
||||
in tl Seq.>< hd
|
||||
|
||||
rotateLS :: TValue -> TValue -> SeqValMap -> Integer -> SeqValMap
|
||||
rotateLS w _ vs by = SeqMap $ \i ->
|
||||
case numTValue w of
|
||||
@ -870,6 +1001,11 @@ rotateRW 0 i _ = i
|
||||
rotateRW w i by = mask w $ (i `shiftR` b) .|. (i `shiftL` (fromInteger w - b))
|
||||
where b = fromInteger (by `mod` w)
|
||||
|
||||
rotateRB :: Integer -> Seq.Seq (Eval Bool) -> Integer -> Seq.Seq (Eval Bool)
|
||||
rotateRB w bs by =
|
||||
let (hd,tl) = Seq.splitAt (fromInteger (w - (by `mod` w))) bs
|
||||
in tl Seq.>< hd
|
||||
|
||||
rotateRS :: TValue -> TValue -> SeqValMap -> Integer -> SeqValMap
|
||||
rotateRS w _ vs by = SeqMap $ \i ->
|
||||
case numTValue w of
|
||||
@ -881,7 +1017,7 @@ rotateRS w _ vs by = SeqMap $ \i ->
|
||||
|
||||
-- | Indexing operations that return one element.
|
||||
indexPrimOne :: BitWord b w
|
||||
=> (Maybe Integer -> TValue -> SeqMap b w -> [b] -> Eval (GenValue b w))
|
||||
=> (Maybe Integer -> TValue -> SeqMap b w -> Seq.Seq b -> Eval (GenValue b w))
|
||||
-> (Maybe Integer -> TValue -> SeqMap b w -> w -> Eval (GenValue b w))
|
||||
-> GenValue b w
|
||||
indexPrimOne bits_op word_op =
|
||||
@ -890,14 +1026,15 @@ indexPrimOne bits_op word_op =
|
||||
tlam $ \ _i ->
|
||||
lam $ \ l -> return $
|
||||
lam $ \ r -> do
|
||||
vs <- fromSeq =<< l
|
||||
vs <- l >>= \case
|
||||
VWord _ w -> w >>= \w' -> return $ SeqMap (\i -> VBit <$> indexWordValue w' i)
|
||||
VSeq _ vs -> return vs
|
||||
VStream vs -> return vs
|
||||
r >>= \case
|
||||
VWord w ->
|
||||
word_op (fromNat (numTValue n)) a vs w
|
||||
VSeq m True xs -> do
|
||||
bs <- traverse (fromVBit<$>) (enumerateSeqMap m xs)
|
||||
bits_op (fromNat (numTValue n)) a vs bs
|
||||
x -> evalPanic "Expected word value" ["indexPrimOne"]
|
||||
VWord _ w -> w >>= \case
|
||||
WordVal w' -> word_op (fromNat (numTValue n)) a vs w'
|
||||
BitsVal bs -> bits_op (fromNat (numTValue n)) a vs =<< sequence bs
|
||||
_ -> evalPanic "Expected word value" ["indexPrimOne"]
|
||||
|
||||
indexFront :: Maybe Integer -> TValue -> SeqValMap -> BV -> Eval Value
|
||||
indexFront mblen _a vs (bvVal -> ix) =
|
||||
@ -905,8 +1042,8 @@ indexFront mblen _a vs (bvVal -> ix) =
|
||||
Just len | len <= ix -> invalidIndex ix
|
||||
_ -> lookupSeqMap vs ix
|
||||
|
||||
indexFront_bits :: Maybe Integer -> TValue -> SeqValMap -> [Bool] -> Eval Value
|
||||
indexFront_bits mblen a vs = indexFront mblen a vs . packWord
|
||||
indexFront_bits :: Maybe Integer -> TValue -> SeqValMap -> Seq.Seq Bool -> Eval Value
|
||||
indexFront_bits mblen a vs = indexFront mblen a vs . packWord . Fold.toList
|
||||
|
||||
indexBack :: Maybe Integer -> TValue -> SeqValMap -> BV -> Eval Value
|
||||
indexBack mblen _a vs (bvVal -> ix) =
|
||||
@ -916,12 +1053,12 @@ indexBack mblen _a vs (bvVal -> ix) =
|
||||
Nothing -> evalPanic "indexBack"
|
||||
["unexpected infinite sequence"]
|
||||
|
||||
indexBack_bits :: Maybe Integer -> TValue -> SeqValMap -> [Bool] -> Eval Value
|
||||
indexBack_bits mblen a vs = indexBack mblen a vs . packWord
|
||||
indexBack_bits :: Maybe Integer -> TValue -> SeqValMap -> Seq.Seq Bool -> Eval Value
|
||||
indexBack_bits mblen a vs = indexBack mblen a vs . packWord . Fold.toList
|
||||
|
||||
-- | Indexing operations that return many elements.
|
||||
indexPrimMany :: BitWord b w
|
||||
=> (Maybe Integer -> TValue -> SeqMap b w -> [b] -> Eval (GenValue b w))
|
||||
=> (Maybe Integer -> TValue -> SeqMap b w -> Seq.Seq b -> Eval (GenValue b w))
|
||||
-> (Maybe Integer -> TValue -> SeqMap b w -> w -> Eval (GenValue b w))
|
||||
-> GenValue b w
|
||||
indexPrimMany bits_op word_op =
|
||||
@ -931,16 +1068,17 @@ indexPrimMany bits_op word_op =
|
||||
tlam $ \ _i ->
|
||||
lam $ \ l -> return $
|
||||
lam $ \ r -> do
|
||||
vs <- fromSeq =<< l
|
||||
ixs <- fromSeq =<< r
|
||||
vs <- l >>= \case
|
||||
VWord _ w -> w >>= \w' -> return $ SeqMap (\i -> VBit <$> indexWordValue w' i)
|
||||
VSeq _ vs -> return vs
|
||||
VStream vs -> return vs
|
||||
ixs <- fromSeq "indexPrimMany idx" =<< r
|
||||
mkSeq m a <$> memoMap (SeqMap $ \i -> do
|
||||
lookupSeqMap ixs i >>= \case
|
||||
VWord w ->
|
||||
word_op (fromNat (numTValue n)) a vs w
|
||||
VSeq m True xs -> do
|
||||
bs <- traverse (fromVBit<$>) (enumerateSeqMap m xs)
|
||||
bits_op (fromNat (numTValue n)) a vs bs
|
||||
x -> evalPanic "Expected word value" ["indexPrimMany"])
|
||||
VWord _ w -> w >>= \case
|
||||
WordVal w' -> word_op (fromNat (numTValue n)) a vs w'
|
||||
BitsVal bs -> bits_op (fromNat (numTValue n)) a vs =<< sequence bs
|
||||
_ -> evalPanic "Expected word value" ["indexPrimMany"])
|
||||
|
||||
-- @[ 0, 1 .. ]@
|
||||
fromThenV :: BitWord b w
|
||||
@ -955,8 +1093,9 @@ fromThenV =
|
||||
| bits' >= Arch.maxBigIntWidth -> wordTooWide bits'
|
||||
(Nat first', Nat next', Nat len', Nat bits') ->
|
||||
let diff = next' - first'
|
||||
in VSeq len' False $ SeqMap $ \i ->
|
||||
ready $ VWord $ wordLit bits' (first' + i*diff)
|
||||
in VSeq len' $ SeqMap $ \i ->
|
||||
ready $ VWord bits' $ return $
|
||||
WordVal $ wordLit bits' (first' + i*diff)
|
||||
_ -> evalPanic "fromThenV" ["invalid arguments"]
|
||||
|
||||
-- @[ 0 .. 10 ]@
|
||||
@ -971,8 +1110,9 @@ fromToV =
|
||||
| bits' >= Arch.maxBigIntWidth -> wordTooWide bits'
|
||||
(Nat first', Nat lst', Nat bits') ->
|
||||
let len = 1 + (lst' - first')
|
||||
in VSeq len False $ SeqMap $ \i ->
|
||||
ready $ VWord $ wordLit bits' (first' + i)
|
||||
in VSeq len $ SeqMap $ \i ->
|
||||
ready $ VWord bits' $ return $
|
||||
WordVal $ wordLit bits' (first' + i)
|
||||
_ -> evalPanic "fromToV" ["invalid arguments"]
|
||||
|
||||
-- @[ 0, 1 .. 10 ]@
|
||||
@ -989,8 +1129,9 @@ fromThenToV =
|
||||
| bits' >= Arch.maxBigIntWidth -> wordTooWide bits'
|
||||
(Nat first', Nat next', Nat lst', Nat len', Nat bits') ->
|
||||
let diff = next' - first'
|
||||
in VSeq len' False $ SeqMap $ \i ->
|
||||
ready $ VWord $ wordLit bits' (first' + i*diff)
|
||||
in VSeq len' $ SeqMap $ \i ->
|
||||
ready $ VWord bits' $ return $
|
||||
WordVal $ wordLit bits' (first' + i*diff)
|
||||
_ -> evalPanic "fromThenToV" ["invalid arguments"]
|
||||
|
||||
|
||||
@ -1000,7 +1141,8 @@ infFromV =
|
||||
tlam $ \(finTValue -> bits) ->
|
||||
wlam $ \first ->
|
||||
return $ VStream $ SeqMap $ \i ->
|
||||
ready $ VWord $ wordPlus first (wordLit bits i)
|
||||
ready $ VWord bits $ return $
|
||||
WordVal $ wordPlus first (wordLit bits i)
|
||||
|
||||
infFromThenV :: BitWord b w
|
||||
=> GenValue b w
|
||||
@ -1010,7 +1152,8 @@ infFromThenV =
|
||||
wlam $ \next -> do
|
||||
let diff = wordMinus next first
|
||||
return $ VStream $ SeqMap $ \i ->
|
||||
ready $ VWord $ wordPlus first (wordMult diff (wordLit bits i))
|
||||
ready $ VWord bits $ return $
|
||||
WordVal $ wordPlus first (wordMult diff (wordLit bits i))
|
||||
|
||||
-- Random Values ---------------------------------------------------------------
|
||||
|
||||
@ -1032,3 +1175,34 @@ randomV ty seed =
|
||||
|
||||
tlamN :: (Nat' -> GenValue b w) -> GenValue b w
|
||||
tlamN f = VPoly (\x -> ready $ f (numTValue x))
|
||||
|
||||
errorV :: forall b w
|
||||
. BitWord b w
|
||||
=> TValue
|
||||
-> String
|
||||
-> Eval (GenValue b w)
|
||||
errorV ty msg
|
||||
-- bits
|
||||
| isTBit ty = cryUserError msg
|
||||
|
||||
-- sequences
|
||||
| Just (n,ety) <- isTSeq ty =
|
||||
case numTValue n of
|
||||
Nat w | isTBit ety -> return $ VWord w $ return $ BitsVal $
|
||||
Seq.replicate (fromInteger w) (cryUserError msg)
|
||||
| otherwise -> return $ mkSeq n ety (SeqMap $ \_ -> errorV ety msg)
|
||||
Inf -> return $ mkSeq n ety (SeqMap $ \_ -> errorV ety msg)
|
||||
|
||||
-- functions
|
||||
| Just (_,bty) <- isTFun ty =
|
||||
return $ lam (\ _ -> errorV bty msg)
|
||||
|
||||
-- tuples
|
||||
| Just (_,tys) <- isTTuple ty =
|
||||
return $ VTuple (map (flip errorV msg) tys)
|
||||
|
||||
-- records
|
||||
| Just fields <- isTRec ty =
|
||||
return $ VRecord [ (f,errorV fty msg) | (f,fty) <- fields ]
|
||||
|
||||
| otherwise = evalPanic "errorV" ["invalid type for error"]
|
||||
|
@ -585,7 +585,7 @@ writeFileCmd file str = do
|
||||
tIsByte x = maybe False
|
||||
(\(n,b) -> T.tIsBit b && T.tIsNum n == Just 8)
|
||||
(T.tIsSeq x)
|
||||
serializeValue (E.VSeq n _ vs) = do
|
||||
serializeValue (E.VSeq n vs) = do
|
||||
ws <- io $ E.runEval (mapM (>>=E.fromVWord "serializeValue") $ E.enumerateSeqMap n vs)
|
||||
return $ BS.pack $ map serializeByte ws
|
||||
serializeValue _ =
|
||||
|
@ -20,6 +20,7 @@ import Control.Monad.IO.Class
|
||||
import Control.Monad (replicateM, when, zipWithM, foldM)
|
||||
import Data.List (transpose, intercalate, genericLength, genericIndex)
|
||||
import qualified Data.Map as Map
|
||||
import qualified Data.Sequence as Seq
|
||||
import qualified Control.Exception as X
|
||||
|
||||
import qualified Data.SBV.Dynamic as SBV
|
||||
@ -34,9 +35,9 @@ import Cryptol.Symbolic.Value
|
||||
|
||||
import qualified Cryptol.Eval as Eval
|
||||
import qualified Cryptol.Eval.Monad as Eval
|
||||
import qualified Cryptol.Eval.Type as Eval
|
||||
import qualified Cryptol.Eval.Value as Eval
|
||||
import qualified Cryptol.Eval.Type (evalType)
|
||||
import Cryptol.Eval.Env (GenEvalEnv(..))
|
||||
import Cryptol.Eval.Env (GenEvalEnv(..), evalType)
|
||||
import Cryptol.TypeCheck.AST
|
||||
import Cryptol.TypeCheck.Solver.InfNat (Nat'(..))
|
||||
import Cryptol.Utils.Ident (Ident)
|
||||
@ -246,17 +247,15 @@ parseValues (t : ts) cws = (v : vs, cws'')
|
||||
parseValue :: FinType -> [SBV.CW] -> (Eval.Value, [SBV.CW])
|
||||
parseValue FTBit [] = panic "Cryptol.Symbolic.parseValue" [ "empty FTBit" ]
|
||||
parseValue FTBit (cw : cws) = (Eval.VBit (SBV.cwToBool cw), cws)
|
||||
parseValue (FTSeq 0 FTBit) cws = (Eval.VWord (Eval.BV 0 0), cws)
|
||||
parseValue (FTSeq 0 FTBit) cws = (Eval.word 0 0, 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 (genericLength vs) True $ Eval.SeqMap $ \i ->
|
||||
return $ genericIndex vs i
|
||||
, cws'
|
||||
)
|
||||
Just (x, cws') -> (Eval.word (toInteger n) x, cws')
|
||||
Nothing -> (VWord (genericLength vs) $ return $ Eval.WordVal $
|
||||
Eval.packWord (map fromVBit vs), cws')
|
||||
where (vs, cws') = parseValues (replicate n FTBit) cws
|
||||
parseValue (FTSeq n t) cws =
|
||||
(Eval.VSeq (toInteger n) False $ Eval.SeqMap $ \i ->
|
||||
(Eval.VSeq (toInteger n) $ Eval.SeqMap $ \i ->
|
||||
return $ genericIndex vs i
|
||||
, cws'
|
||||
)
|
||||
@ -304,7 +303,7 @@ unFinType fty =
|
||||
predArgTypes :: Schema -> Either String [FinType]
|
||||
predArgTypes schema@(Forall ts ps ty)
|
||||
| null ts && null ps =
|
||||
case go (Cryptol.Eval.Type.evalType mempty ty) of
|
||||
case go (evalType mempty ty) of
|
||||
Just fts -> Right fts
|
||||
Nothing -> Left $ "Not a valid predicate type:\n" ++ show (pp schema)
|
||||
| otherwise = Left $ "Not a monomorphic type:\n" ++ show (pp schema)
|
||||
@ -318,10 +317,10 @@ forallFinType :: FinType -> SBV.Symbolic Value
|
||||
forallFinType ty =
|
||||
case ty of
|
||||
FTBit -> VBit <$> forallSBool_
|
||||
FTSeq 0 FTBit -> return $ VWord (literalSWord 0 0)
|
||||
FTSeq n FTBit -> VWord <$> (forallBV_ n)
|
||||
FTSeq 0 FTBit -> return $ Eval.word 0 0
|
||||
FTSeq n FTBit -> VWord (toInteger n) . return . Eval.WordVal <$> (forallBV_ n)
|
||||
FTSeq n t -> do vs <- replicateM n (forallFinType t)
|
||||
return $ VSeq (toInteger n) False $ Eval.SeqMap $ \i ->
|
||||
return $ VSeq (toInteger n) $ Eval.SeqMap $ \i ->
|
||||
return $ genericIndex vs i
|
||||
FTTuple ts -> VTuple <$> mapM (fmap Eval.ready . forallFinType) ts
|
||||
FTRecord fs -> VRecord <$> mapM (traverseSnd (fmap Eval.ready . forallFinType)) fs
|
||||
@ -330,10 +329,10 @@ existsFinType :: FinType -> SBV.Symbolic Value
|
||||
existsFinType ty =
|
||||
case ty of
|
||||
FTBit -> VBit <$> existsSBool_
|
||||
FTSeq 0 FTBit -> return $ VWord (literalSWord 0 0)
|
||||
FTSeq n FTBit -> VWord <$> existsBV_ n
|
||||
FTSeq 0 FTBit -> return $ Eval.word 0 0
|
||||
FTSeq n FTBit -> VWord (toInteger n) . return . Eval.WordVal <$> (existsBV_ n)
|
||||
FTSeq n t -> do vs <- replicateM n (existsFinType t)
|
||||
return $ VSeq (toInteger n) False $ Eval.SeqMap $ \i ->
|
||||
return $ VSeq (toInteger n) $ Eval.SeqMap $ \i ->
|
||||
return $ genericIndex vs i
|
||||
FTTuple ts -> VTuple <$> mapM (fmap Eval.ready . existsFinType) ts
|
||||
FTRecord fs -> VRecord <$> mapM (traverseSnd (fmap Eval.ready . existsFinType)) fs
|
||||
|
@ -9,6 +9,7 @@
|
||||
{-# LANGUAGE RecordWildCards #-}
|
||||
{-# LANGUAGE PatternGuards #-}
|
||||
{-# LANGUAGE MultiParamTypeClasses #-}
|
||||
{-# LANGUAGE Rank2Types #-}
|
||||
{-# LANGUAGE LambdaCase #-}
|
||||
{-# LANGUAGE ViewPatterns #-}
|
||||
{-# LANGUAGE FlexibleContexts #-}
|
||||
@ -19,10 +20,13 @@ module Cryptol.Symbolic.Prims where
|
||||
import Data.Bits
|
||||
import Data.List (genericDrop, genericReplicate, genericSplitAt, genericTake, sortBy, transpose)
|
||||
import Data.Ord (comparing)
|
||||
import qualified Data.Sequence as Seq
|
||||
import qualified Data.Foldable as Fold
|
||||
|
||||
import Cryptol.Eval.Monad (Eval(..), ready)
|
||||
import Cryptol.Eval.Value (BitWord(..), EvalPrims(..), enumerateSeqMap, SeqMap(..),
|
||||
finiteSeqMap, reverseSeqMap, wlam)
|
||||
finiteSeqMap, reverseSeqMap, wlam, WordValue(..),
|
||||
asWordVal, asBitsVal, fromWordVal )
|
||||
import Cryptol.Prims.Eval (binary, unary, tlamN, arithUnary,
|
||||
arithBinary, Binary, BinArith,
|
||||
logicBinary, logicUnary, zeroV,
|
||||
@ -88,95 +92,37 @@ primTable = Map.fromList $ map (\(n, v) -> (mkIdent (T.pack n), v))
|
||||
, ("^" , binary (logicBinary SBV.svXOr SBV.svXOr))
|
||||
, ("complement" , unary (logicUnary SBV.svNot SBV.svNot))
|
||||
, ("zero" , tlam zeroV)
|
||||
|
||||
, ("<<" , -- {m,n,a} (fin n) => [m] a -> [n] -> [m] a
|
||||
tlam $ \m ->
|
||||
tlam $ \n ->
|
||||
tlam $ \a ->
|
||||
VFun $ \xs -> return $
|
||||
VFun $ \y ->
|
||||
xs >>= \case
|
||||
VWord x -> VWord . SBV.svShiftLeft x <$> (fromVWord "<<" =<< y)
|
||||
x -> do
|
||||
x' <- fromSeq x
|
||||
let Nat len = numTValue n
|
||||
let shl :: Integer -> Value
|
||||
shl =
|
||||
case numTValue m of
|
||||
Inf -> \i -> VStream $ SeqMap $ \idx -> lookupSeqMap x' (i+idx)
|
||||
Nat j -> \i -> VSeq j (isTBit a) $ SeqMap $ \idx ->
|
||||
if i+idx >= j then
|
||||
return $ zeroV a
|
||||
else
|
||||
lookupSeqMap x' (i+idx)
|
||||
in selectV len shl =<< y)
|
||||
|
||||
, (">>" , -- {m,n,a} (fin n) => [m] a -> [n] -> [m] a
|
||||
tlam $ \m ->
|
||||
tlam $ \n ->
|
||||
tlam $ \a ->
|
||||
VFun $ \xs -> return $
|
||||
VFun $ \y ->
|
||||
xs >>= \case
|
||||
VWord x -> VWord . SBV.svShiftRight x <$> (fromVWord ">>" =<< y)
|
||||
x -> do
|
||||
x' <- fromSeq x
|
||||
let Nat len = numTValue n
|
||||
let shr :: Integer -> Value
|
||||
shr =
|
||||
case numTValue m of
|
||||
Inf -> \i -> VStream $ SeqMap $ \idx ->
|
||||
if idx-i < 0 then
|
||||
return $ zeroV a
|
||||
else
|
||||
lookupSeqMap x' (idx-i)
|
||||
Nat j -> \i -> VSeq j (isTBit a) $ SeqMap $ \idx ->
|
||||
if idx-i < 0 then
|
||||
return $ zeroV a
|
||||
else
|
||||
lookupSeqMap x' (idx-i)
|
||||
selectV len shr =<< y)
|
||||
|
||||
, ("<<<" , -- {m,n,a} (fin m, fin n) => [m] a -> [n] -> [m] a
|
||||
tlam $ \m ->
|
||||
tlam $ \n ->
|
||||
tlam $ \a ->
|
||||
VFun $ \xs -> return $
|
||||
VFun $ \y ->
|
||||
xs >>= \case
|
||||
VWord x -> VWord . SBV.svRotateLeft x <$> (fromVWord "<<<" =<< y)
|
||||
x -> do
|
||||
x' <- fromSeq x
|
||||
let len = finTValue n
|
||||
let m' = finTValue m
|
||||
let rol :: Integer -> Value
|
||||
rol i = VSeq m' (isTBit a) $ SeqMap $ \idx ->
|
||||
lookupSeqMap x' ((i+idx) `mod` m')
|
||||
selectV len rol =<< y)
|
||||
|
||||
, (">>>" , -- {m,n,a} (fin m, fin n) => [m] a -> [n] -> [m] a
|
||||
tlam $ \m ->
|
||||
tlam $ \n ->
|
||||
tlam $ \a ->
|
||||
VFun $ \xs -> return $
|
||||
VFun $ \y ->
|
||||
xs >>= \case
|
||||
VWord x -> VWord . SBV.svRotateRight x <$> (fromVWord ">>>" =<< y)
|
||||
x -> do
|
||||
x' <- fromSeq x
|
||||
let len = finTValue n
|
||||
let m' = finTValue m
|
||||
let rol :: Integer -> Value
|
||||
rol i = VSeq m' (isTBit a) $ SeqMap $ \idx ->
|
||||
lookupSeqMap x' ((idx+m'-i) `mod` m')
|
||||
selectV len rol =<< y)
|
||||
, ("<<" , logicShift "<<"
|
||||
SBV.svShiftLeft
|
||||
(\sz i shft ->
|
||||
case sz of
|
||||
Inf -> Just (i+shft)
|
||||
Nat n
|
||||
| i+shft >= n -> Nothing
|
||||
| otherwise -> Just (i+shft)))
|
||||
, (">>" , logicShift ">>"
|
||||
SBV.svShiftRight
|
||||
(\_sz i shft ->
|
||||
if i-shft < 0 then Nothing else Just (i-shft)))
|
||||
, ("<<<" , logicShift "<<<"
|
||||
SBV.svRotateLeft
|
||||
(\sz i shft ->
|
||||
case sz of
|
||||
Inf -> evalPanic "cannot rotate infinite sequence" []
|
||||
Nat n -> Just ((i+shft) `mod` n)))
|
||||
, (">>>" , logicShift ">>>"
|
||||
SBV.svRotateRight
|
||||
(\sz i shft ->
|
||||
case sz of
|
||||
Inf -> evalPanic "cannot rotate infinite sequence" []
|
||||
Nat n -> Just ((i+n-shft) `mod` n)))
|
||||
|
||||
, ("#" , -- {a,b,d} (fin a) => [a] d -> [b] d -> [a + b] d
|
||||
tlam $ \ front ->
|
||||
tlam $ \ back ->
|
||||
tlam $ \ elty ->
|
||||
lam $ \ l -> return $
|
||||
lam $ \ r -> ccatV front back elty l r)
|
||||
lam $ \ r -> join (ccatV front back elty <$> l <*> r))
|
||||
|
||||
, ("splitAt" ,
|
||||
tlam $ \ front ->
|
||||
@ -214,7 +160,6 @@ primTable = Map.fromList $ map (\(n, v) -> (mkIdent (T.pack n), v))
|
||||
, ("!" , indexPrimOne indexBack_bits indexBack)
|
||||
, ("!!" , indexPrimMany indexBack_bits indexBack)
|
||||
|
||||
|
||||
, ("pmult" , -- {a,b} (fin a, fin b) => [a] -> [b] -> [max 1 (a + b) - 1]
|
||||
tlam $ \(finTValue -> i) ->
|
||||
tlam $ \(finTValue -> j) ->
|
||||
@ -223,31 +168,30 @@ primTable = Map.fromList $ map (\(n, v) -> (mkIdent (T.pack n), v))
|
||||
let k = max 1 (i + j) - 1
|
||||
mul _ [] ps = ps
|
||||
mul as (b:bs) ps = mul (SBV.svFalse : as) bs (ites b (as `addPoly` ps) ps)
|
||||
xs <- traverse (fromVBit<$>) . enumerateSeqMap i =<< fromSeq =<< v1
|
||||
ys <- traverse (fromVBit<$>) . enumerateSeqMap j =<< fromSeq =<< v2
|
||||
xs <- sequence . Fold.toList . asBitsVal =<< fromWordVal "pmult 1" =<< v1
|
||||
ys <- sequence . Fold.toList . asBitsVal =<< fromWordVal "pmult 2" =<< v2
|
||||
let zs = genericTake k (mul xs ys [] ++ repeat SBV.svFalse)
|
||||
VSeq k True <$> finiteSeqMap (map (ready . VBit) zs))
|
||||
|
||||
return $ VWord k $ return $ BitsVal $ Seq.fromList $ map ready zs)
|
||||
|
||||
, ("pdiv" , -- {a,b} (fin a, fin b) => [a] -> [b] -> [a]
|
||||
tlam $ \(finTValue -> i) ->
|
||||
tlam $ \(finTValue -> j) ->
|
||||
VFun $ \v1 -> return $
|
||||
VFun $ \v2 -> do
|
||||
xs <- traverse (fromVBit<$>) . enumerateSeqMap i =<< fromSeq =<< v1
|
||||
ys <- traverse (fromVBit<$>) . enumerateSeqMap j =<< fromSeq =<< v2
|
||||
let zs = take (fromInteger i) (fst (mdp (reverse xs) (reverse ys)) ++ repeat SBV.svFalse)
|
||||
VSeq i True <$> finiteSeqMap (map (ready . VBit) (reverse zs)))
|
||||
xs <- sequence . Fold.toList . Seq.reverse . asBitsVal =<< fromWordVal "pdiv 1" =<< v1
|
||||
ys <- sequence . Fold.toList . Seq.reverse . asBitsVal =<< fromWordVal "pdiv 2" =<< v2
|
||||
let zs = genericTake i (fst (mdp xs ys) ++ repeat SBV.svFalse)
|
||||
return $ VWord i $ return $ BitsVal $ Seq.reverse $ Seq.fromList $ map ready zs)
|
||||
|
||||
, ("pmod" , -- {a,b} (fin a, fin b) => [a] -> [b+1] -> [b]
|
||||
tlam $ \(finTValue -> i) ->
|
||||
tlam $ \(finTValue -> j) ->
|
||||
VFun $ \v1 -> return $
|
||||
VFun $ \v2 -> do
|
||||
xs <- traverse (fromVBit<$>) . enumerateSeqMap i =<< fromSeq =<< v1
|
||||
ys <- traverse (fromVBit<$>) . enumerateSeqMap (j+1) =<< fromSeq =<< v2
|
||||
let zs = take (fromInteger j) (snd (mdp (reverse xs) (reverse ys)) ++ repeat SBV.svFalse)
|
||||
VSeq j True <$> finiteSeqMap (map (ready . VBit) (reverse zs)))
|
||||
xs <- sequence . Fold.toList . Seq.reverse . asBitsVal =<< fromWordVal "pmod 1" =<< v1
|
||||
ys <- sequence . Fold.toList . Seq.reverse . asBitsVal =<< fromWordVal "pmod 2" =<< v2
|
||||
let zs = genericTake j (snd (mdp xs ys) ++ repeat SBV.svFalse)
|
||||
return $ VWord j $ return $ BitsVal $ Seq.reverse $ Seq.fromList $ map ready zs)
|
||||
|
||||
-- {at,len} (fin len) => [len][8] -> at
|
||||
, ("error" ,
|
||||
@ -278,17 +222,68 @@ primTable = Map.fromList $ map (\(n, v) -> (mkIdent (T.pack n), v))
|
||||
]
|
||||
|
||||
|
||||
selectV :: Integer -> (Integer -> Value) -> Value -> Eval Value
|
||||
selectV _len f (VWord v) | Just idx <- SBV.svAsInteger v = return $ f idx
|
||||
iteWord :: SBool
|
||||
-> Eval (WordValue SBool SWord)
|
||||
-> Eval (WordValue SBool SWord)
|
||||
-> Eval (WordValue SBool SWord)
|
||||
iteWord c x y = mergeWord True c <$> x <*> y
|
||||
|
||||
selectV len f v = sel 0 =<< bits
|
||||
where
|
||||
bits = enumerateSeqMap len <$> fromSeq v -- index bits in big-endian order
|
||||
logicShift :: String
|
||||
-> (SWord -> SWord -> SWord)
|
||||
-> (Nat' -> Integer -> Integer -> Maybe Integer)
|
||||
-> Value
|
||||
logicShift nm wop reindex =
|
||||
tlam $ \m ->
|
||||
tlam $ \n ->
|
||||
tlam $ \a ->
|
||||
VFun $ \xs -> return $
|
||||
VFun $ \y -> do
|
||||
let Nat len = numTValue n
|
||||
idx <- fromWordVal "<<" =<< y
|
||||
|
||||
xs >>= \case
|
||||
VWord w x -> return $ VWord w $ do
|
||||
x >>= \case
|
||||
WordVal x' -> WordVal . wop x' <$> asWordVal idx
|
||||
BitsVal bs -> selectV len iteWord idx $ \shft ->
|
||||
BitsVal $ Seq.fromFunction (Seq.length bs) $ \i ->
|
||||
case reindex (Nat w) (toInteger i) shft of
|
||||
Nothing -> return $ bitLit False
|
||||
Just i' -> Seq.index bs i
|
||||
|
||||
VSeq w xs -> selectV len iteValue idx $ \shft ->
|
||||
VSeq w $ SeqMap $ \i ->
|
||||
case reindex (Nat w) i shft of
|
||||
Nothing -> return $ zeroV a
|
||||
Just i' -> lookupSeqMap xs i'
|
||||
|
||||
VStream xs -> selectV len iteValue idx $ \shft ->
|
||||
VStream $ SeqMap $ \i ->
|
||||
case reindex Inf i shft of
|
||||
Nothing -> return $ zeroV a
|
||||
Just i' -> lookupSeqMap xs i'
|
||||
|
||||
_ -> evalPanic "expected sequence value in shift operation" [nm]
|
||||
|
||||
|
||||
selectV :: forall a
|
||||
. Integer
|
||||
-> (SBool -> Eval a -> Eval a -> Eval a)
|
||||
-> WordValue SBool SWord
|
||||
-> (Integer -> a)
|
||||
-> Eval a
|
||||
selectV len mux val f =
|
||||
case val of
|
||||
WordVal x | Just idx <- SBV.svAsInteger x -> return $ f idx
|
||||
| otherwise -> sel 0 (unpackWord x)
|
||||
BitsVal bs -> sel 0 =<< sequence (Fold.toList bs)
|
||||
|
||||
where
|
||||
-- index bits in big-endian order
|
||||
bits = sequence $ asBitsVal val
|
||||
|
||||
sel :: Integer -> [Eval Value] -> Eval Value
|
||||
sel offset [] = return $ f offset
|
||||
sel offset (b : bs) = do b' <- fromVBit <$> b
|
||||
iteValue b' m1 m2
|
||||
sel offset (b : bs) = mux b m1 m2
|
||||
where m1 = sel (offset + 2 ^ length bs) bs
|
||||
m2 = sel offset bs
|
||||
|
||||
@ -305,15 +300,19 @@ indexFront mblen a xs idx
|
||||
| Just n <- mblen
|
||||
, Just (finTValue -> wlen, a') <- isTSeq a
|
||||
, isTBit a'
|
||||
, Just ws <- asWordList (enumerateSeqMap n xs)
|
||||
= return $ VWord $ SBV.svSelect ws (wordLit wlen 0) idx
|
||||
= do wvs <- traverse (fromWordVal "indexFront" =<<) (enumerateSeqMap n xs)
|
||||
case asWordList wvs of
|
||||
Just ws ->
|
||||
return $ VWord n $ ready $ WordVal $ SBV.svSelect ws (wordLit wlen 0) idx
|
||||
Nothing -> foldr f def [0 .. 2^w - 1]
|
||||
|
||||
| otherwise
|
||||
= foldr f def [0 .. 2 ^ SBV.intSizeOf idx - 1]
|
||||
where
|
||||
k = SBV.kindOf idx
|
||||
def = ready $ VWord $ SBV.svInteger k 0
|
||||
f n y = iteValue (SBV.svEqual idx (SBV.svInteger k n)) (lookupSeqMap xs n) y
|
||||
= foldr f def [0 .. 2^w - 1]
|
||||
where
|
||||
k = SBV.kindOf idx
|
||||
w = SBV.intSizeOf idx
|
||||
def = ready $ VWord (toInteger w) $ ready $ WordVal $ SBV.svInteger k 0
|
||||
f n y = iteValue (SBV.svEqual idx (SBV.svInteger k n)) (lookupSeqMap xs n) y
|
||||
|
||||
indexBack :: Maybe Integer
|
||||
-> TValue
|
||||
@ -326,9 +325,9 @@ indexBack Nothing _ _ _ = evalPanic "Expected finite sequence" ["indexBack"]
|
||||
indexFront_bits :: Maybe Integer
|
||||
-> TValue
|
||||
-> SeqMap SBool SWord
|
||||
-> [SBool]
|
||||
-> Seq.Seq SBool
|
||||
-> Eval Value
|
||||
indexFront_bits mblen a xs bits0 = go 0 (length bits0) bits0
|
||||
indexFront_bits mblen a xs bits0 = go 0 (length bits0) (Fold.toList bits0)
|
||||
where
|
||||
go :: Integer -> Int -> [SBool] -> Eval Value
|
||||
go i _k []
|
||||
@ -352,26 +351,27 @@ indexFront_bits mblen a xs bits0 = go 0 (length bits0) bits0
|
||||
indexBack_bits :: Maybe Integer
|
||||
-> TValue
|
||||
-> SeqMap SBool SWord
|
||||
-> [SBool]
|
||||
-> Seq.Seq SBool
|
||||
-> Eval Value
|
||||
indexBack_bits (Just n) a xs idx = indexFront_bits (Just n) a (reverseSeqMap n xs) idx
|
||||
indexBack_bits Nothing _ _ _ = evalPanic "Expected finite sequence" ["indexBack_bits"]
|
||||
|
||||
|
||||
asBitList :: [Eval Value] -> Maybe [SBool]
|
||||
asBitList :: [Eval SBool] -> Maybe [SBool]
|
||||
asBitList = go id
|
||||
where go :: ([SBool] -> [SBool]) -> [Eval Value] -> Maybe [SBool]
|
||||
where go :: ([SBool] -> [SBool]) -> [Eval SBool] -> Maybe [SBool]
|
||||
go f [] = Just (f [])
|
||||
go f (Ready (VBit b):vs) = go (f . (b:)) vs
|
||||
go f (Ready b:vs) = go (f . (b:)) vs
|
||||
go _ _ = Nothing
|
||||
|
||||
asWordList :: [Eval Value] -> Maybe [SWord]
|
||||
|
||||
asWordList :: [WordValue SBool SWord] -> Maybe [SWord]
|
||||
asWordList = go id
|
||||
where go :: ([SWord] -> [SWord]) -> [Eval Value] -> Maybe [SWord]
|
||||
where go :: ([SWord] -> [SWord]) -> [WordValue SBool SWord] -> Maybe [SWord]
|
||||
go f [] = Just (f [])
|
||||
go f (Ready (VWord x):vs) = go (f . (x:)) vs
|
||||
go f (Ready (VSeq i True bs):vs) =
|
||||
case asBitList (enumerateSeqMap i bs) of
|
||||
go f (WordVal x :vs) = go (f . (x:)) vs
|
||||
go f (BitsVal bs:vs) =
|
||||
case asBitList (Fold.toList bs) of
|
||||
Just xs -> go (f . (packWord xs:)) vs
|
||||
Nothing -> Nothing
|
||||
go _ _ = Nothing
|
||||
@ -383,38 +383,13 @@ ecDemoteV :: Value
|
||||
ecDemoteV = tlam $ \valT ->
|
||||
tlam $ \bitT ->
|
||||
case (numTValue valT, numTValue bitT) of
|
||||
(Nat v, Nat bs) -> VWord (literalSWord (fromInteger bs) v)
|
||||
(Nat v, Nat bs) -> VWord bs $ ready $ WordVal $ literalSWord (fromInteger bs) v
|
||||
_ -> evalPanic "Cryptol.Prove.evalECon"
|
||||
["Unexpected Inf in constant."
|
||||
, show valT
|
||||
, show bitT
|
||||
]
|
||||
|
||||
{-
|
||||
-- Type Values -----------------------------------------------------------------
|
||||
|
||||
-- | An easy-to-use alternative representation for type `TValue`.
|
||||
data TypeVal
|
||||
= TVBit
|
||||
| TVSeq Int TypeVal
|
||||
| TVStream TypeVal
|
||||
| TVTuple [TypeVal]
|
||||
| TVRecord [(Ident, TypeVal)]
|
||||
| TVFun TypeVal TypeVal
|
||||
|
||||
toTypeVal :: TValue -> TypeVal
|
||||
toTypeVal ty
|
||||
| isTBit ty = TVBit
|
||||
| Just (n, ety) <- isTSeq ty = case numTValue n of
|
||||
Nat w -> TVSeq (fromInteger w) (toTypeVal ety)
|
||||
Inf -> TVStream (toTypeVal ety)
|
||||
| Just (aty, bty) <- isTFun ty = TVFun (toTypeVal aty) (toTypeVal bty)
|
||||
| Just (_, tys) <- isTTuple ty = TVTuple (map toTypeVal tys)
|
||||
| Just fields <- isTRec ty = TVRecord [ (n, toTypeVal aty) | (n, aty) <- fields ]
|
||||
| otherwise = panic "Cryptol.Symbolic.Prims.toTypeVal" [ "bad TValue" ]
|
||||
|
||||
-}
|
||||
|
||||
liftBinArith :: (SWord -> SWord -> SWord) -> BinArith SWord
|
||||
liftBinArith op _ = op
|
||||
|
||||
@ -446,19 +421,17 @@ cmpValue fb fw = cmp
|
||||
in cmpValues (vals fs1) (vals fs2) k
|
||||
(VTuple vs1 , VTuple vs2 ) -> cmpValues vs1 vs2 k
|
||||
(VBit b1 , VBit b2 ) -> fb b1 b2 k
|
||||
(VWord w1 , VWord w2 ) -> fw w1 w2 k
|
||||
(VSeq n _ vs1 , VSeq _ _ vs2 ) -> cmpValues (enumerateSeqMap n vs1)
|
||||
(enumerateSeqMap n vs2) k
|
||||
(VWord _ w1 , VWord _ w2 ) -> join (fw <$> (asWordVal =<< w1)
|
||||
<*> (asWordVal =<< w2)
|
||||
<*> return k)
|
||||
(VSeq n vs1 , VSeq _ vs2 ) -> cmpValues (enumerateSeqMap n vs1)
|
||||
(enumerateSeqMap n vs2) k
|
||||
(VStream {} , VStream {} ) -> panic "Cryptol.Symbolic.Prims.cmpValue"
|
||||
[ "Infinite streams are not comparable" ]
|
||||
(VFun {} , VFun {} ) -> panic "Cryptol.Symbolic.Prims.cmpValue"
|
||||
[ "Functions are not comparable" ]
|
||||
(VPoly {} , VPoly {} ) -> panic "Cryptol.Symbolic.Prims.cmpValue"
|
||||
[ "Polymorphic values are not comparable" ]
|
||||
(VWord w1 , _ ) -> do w2 <- fromVWord "cmpValue right" v2
|
||||
fw w1 w2 k
|
||||
(_ , VWord w2 ) -> do w1 <- fromVWord "cmpValue left" v1
|
||||
fw w1 w2 k
|
||||
(_ , _ ) -> panic "Cryptol.Symbolic.Prims.cmpValue"
|
||||
[ "type mismatch" ]
|
||||
|
||||
|
@ -24,18 +24,20 @@ module Cryptol.Symbolic.Value
|
||||
, fromVBit, fromVFun, fromVPoly, fromVTuple, fromVRecord, lookupRecord
|
||||
, fromSeq, fromVWord
|
||||
, evalPanic
|
||||
, iteSValue, mergeValue
|
||||
, iteSValue, mergeValue, mergeWord
|
||||
)
|
||||
where
|
||||
|
||||
import Data.List (foldl')
|
||||
import qualified Data.Sequence as Seq
|
||||
|
||||
import Data.SBV.Dynamic
|
||||
|
||||
--import Cryptol.Eval.Monad
|
||||
import Cryptol.Eval.Value (TValue, numTValue, toNumTValue, finTValue, isTBit,
|
||||
isTFun, isTSeq, isTTuple, isTRec, tvSeq, GenValue(..),
|
||||
BitWord(..), lam, tlam, toStream, toFinSeq, toSeq,
|
||||
import Cryptol.Eval.Type (TValue, numTValue, toNumTValue, finTValue, isTBit,
|
||||
isTFun, isTSeq, isTTuple, isTRec, tvSeq)
|
||||
import Cryptol.Eval.Value ( GenValue(..), BitWord(..), lam, tlam, toStream,
|
||||
toFinSeq, toSeq, WordValue(..), asWordVal, asBitsVal,
|
||||
fromSeq, fromVBit, fromVWord, fromVFun, fromVPoly,
|
||||
fromVTuple, fromVRecord, lookupRecord, SeqMap(..),
|
||||
ppBV,BV(..),integerToChar)
|
||||
@ -79,25 +81,38 @@ iteSValue c x y =
|
||||
Just False -> y
|
||||
Nothing -> mergeValue True c x y
|
||||
|
||||
mergeBit :: Bool
|
||||
-> SBool
|
||||
-> SBool
|
||||
-> SBool
|
||||
-> SBool
|
||||
mergeBit f c b1 b2 = svSymbolicMerge KBool f c b1 b2
|
||||
|
||||
mergeWord :: Bool
|
||||
-> SBool
|
||||
-> WordValue SBool SWord
|
||||
-> WordValue SBool SWord
|
||||
-> WordValue SBool SWord
|
||||
mergeWord f c (WordVal w1) (WordVal w2) =
|
||||
WordVal $ svSymbolicMerge (kindOf w1) f c w1 w2
|
||||
mergeWord f c w1 w2 =
|
||||
BitsVal $ Seq.zipWith mergeBit' (asBitsVal w1) (asBitsVal w2)
|
||||
where mergeBit' b1 b2 = mergeBit f c <$> b1 <*> b2
|
||||
|
||||
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 (\x y -> mergeValue f c <$> x <*> y) vs1 vs2
|
||||
(VBit b1 , VBit b2 ) -> VBit $ mergeBit b1 b2
|
||||
(VWord w1 , VWord w2 ) -> VWord $ mergeWord w1 w2
|
||||
(VSeq n1 b1 vs1, VSeq n2 _ vs2 ) | n1 == n2 -> VSeq n1 b1 $ mergeSeqMap vs1 vs2
|
||||
(VBit b1 , VBit b2 ) -> VBit $ mergeBit f c b1 b2
|
||||
(VWord n1 w1, VWord n2 w2 ) | n1 == n2 -> VWord n1 (mergeWord f c <$> w1 <*> w2)
|
||||
(VSeq n1 vs1, VSeq n2 vs2 ) | n1 == n2 -> VSeq n1 $ mergeSeqMap vs1 vs2
|
||||
(VStream vs1, VStream vs2) -> VStream $ mergeSeqMap 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)
|
||||
-- FIXME!
|
||||
-- (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 (kindOf w1) f c w1 w2
|
||||
mergeField (n1, x1) (n2, x2)
|
||||
| n1 == n2 = (n1, mergeValue f c <$> x1 <*> x2)
|
||||
| otherwise = panic "Cryptol.Symbolic.Value"
|
||||
@ -126,7 +141,7 @@ instance BitWord SBool SWord where
|
||||
|
||||
joinWord x y = svJoin x y
|
||||
|
||||
splitWord leftW rightW w =
|
||||
splitWord _leftW rightW w =
|
||||
( svExtract (intSizeOf w - 1) (fromInteger rightW) w
|
||||
, svExtract (fromInteger rightW - 1) 0 w
|
||||
)
|
||||
|
@ -118,10 +118,10 @@ typeValues ty =
|
||||
(TCSeq, ts1) ->
|
||||
case map tNoUser ts1 of
|
||||
[ TCon (TC (TCNum n)) _, TCon (TC TCBit) [] ] ->
|
||||
[ VWord (BV n x) | x <- [ 0 .. 2^n - 1 ] ]
|
||||
[ VWord n (ready (WordVal (BV n x))) | x <- [ 0 .. 2^n - 1 ] ]
|
||||
|
||||
[ TCon (TC (TCNum n)) _, t ] ->
|
||||
[ VSeq n False (SeqMap $ \i -> return $ genericIndex xs i)
|
||||
[ VSeq n (SeqMap $ \i -> return $ genericIndex xs i)
|
||||
| xs <- sequence $ genericReplicate n
|
||||
$ typeValues t ]
|
||||
_ -> []
|
||||
|
@ -12,7 +12,7 @@
|
||||
module Cryptol.Testing.Random where
|
||||
|
||||
import Cryptol.Eval.Monad (ready)
|
||||
import Cryptol.Eval.Value (BV(..),Value,GenValue(..),SeqMap(..))
|
||||
import Cryptol.Eval.Value (BV(..),Value,GenValue(..),SeqMap(..), WordValue(..))
|
||||
import qualified Cryptol.Testing.Concrete as Conc
|
||||
import Cryptol.TypeCheck.AST (Type(..),TCon(..),TC(..),tNoUser)
|
||||
import Cryptol.Utils.Ident (Ident)
|
||||
@ -101,7 +101,7 @@ randomBit _ g =
|
||||
randomWord :: RandomGen g => Integer -> Gen g
|
||||
randomWord w _sz g =
|
||||
let (val, g1) = randomR (0,2^w-1) g
|
||||
in (VWord (BV w val), g1)
|
||||
in (VWord w (ready (WordVal (BV w val))), g1)
|
||||
|
||||
-- | Generate a random infinite stream value.
|
||||
randomStream :: RandomGen g => Gen g -> Gen g
|
||||
@ -115,7 +115,7 @@ is mostly about how the results will be displayed. -}
|
||||
randomSequence :: RandomGen g => Integer -> Gen g -> Gen g
|
||||
randomSequence w mkElem sz g =
|
||||
let (g1,g2) = split g
|
||||
in (VSeq w False $ SeqMap $ genericIndex (map ready (genericTake w $ unfoldr (Just . mkElem sz) g1)), g2)
|
||||
in (VSeq w $ SeqMap $ genericIndex (map ready (genericTake w $ unfoldr (Just . mkElem sz) g1)), g2)
|
||||
|
||||
-- | Generate a random tuple value.
|
||||
randomTuple :: RandomGen g => [Gen g] -> Gen g
|
||||
|
Loading…
Reference in New Issue
Block a user