mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-11-30 23:45:23 +03:00
Change the representation and caching of sequences for better performance.
There are two major changes in this patch. The first is that sequence maps now have special representations for point updates, of the sort produced by the 'update' and 'updateEnd' primtives. These updates are stored in a finite map, rather than as a functional-update thunk using lambdas; this reduces memory usage and improves time efficecy of sequences defined by sequences of updates. The second change is that the caching policy for sequences is changed to retain all previously-calculated values. This is a change from the previous LRU policy, which retained only a small finite number of previous values. Benchmarking showed that unbounded memoization was better for performance in essentially all cases over both an LRU and an adaptive caching strategy. The potential downside is that we may retain values longer than necessary. If this becomes a problem, we may need to revisit this decision.
This commit is contained in:
Robert Dockins
parent
c484a8c253
commit
dae3ab11b1
@ -53,7 +53,6 @@ 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,
|
||||
|
||||
@ -33,14 +33,11 @@ import Cryptol.Eval.Value
|
||||
import Cryptol.ModuleSystem.Name
|
||||
import Cryptol.TypeCheck.AST
|
||||
import Cryptol.TypeCheck.Solver.InfNat(Nat'(..))
|
||||
import Cryptol.Utils.Ident (Ident)
|
||||
import Cryptol.Utils.Panic (panic)
|
||||
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
|
||||
@ -49,7 +46,6 @@ import Prelude ()
|
||||
import Prelude.Compat
|
||||
|
||||
type EvalEnv = GenEvalEnv Bool BV
|
||||
type ReadEnv = EvalEnv
|
||||
|
||||
-- Expression Evaluation -------------------------------------------------------
|
||||
|
||||
@ -81,7 +77,7 @@ evalExpr env expr = case expr of
|
||||
Just w -> WordVal w
|
||||
Nothing -> BitsVal $ Seq.fromList $ map (fromVBit <$>) vs
|
||||
| otherwise -> {-# SCC "evalExpr->EList" #-}
|
||||
VSeq len <$> finiteSeqMap vs
|
||||
return $ VSeq len $ finiteSeqMap vs
|
||||
where
|
||||
tyv = evalValType (envTypes env) ty
|
||||
vs = map (evalExpr env) es
|
||||
@ -299,11 +295,11 @@ etaDelay msg env0 Forall{ sVars = vs, sType = tp0 } = goTpVars env0 vs
|
||||
VWord _ _ -> return x
|
||||
VSeq n xs
|
||||
| TVSeq nt el <- tp
|
||||
-> return $ VSeq n $ SeqMap $ \i -> go el (lookupSeqMap xs i)
|
||||
-> return $ VSeq n $ IndexSeqMap $ \i -> go el (lookupSeqMap xs i)
|
||||
|
||||
VStream xs
|
||||
| TVSeq nt el <- tp
|
||||
-> return $ VStream $ SeqMap $ \i -> go el (lookupSeqMap xs i)
|
||||
-> return $ VStream $ IndexSeqMap $ \i -> go el (lookupSeqMap xs i)
|
||||
|
||||
VTuple xs
|
||||
| TVTuple ts <- tp
|
||||
@ -332,12 +328,12 @@ etaDelay msg env0 Forall{ sVars = vs, sType = tp0 } = goTpVars env0 vs
|
||||
|
||||
TVSeq n el ->
|
||||
do x' <- delay (Just msg) (fromSeq "during eta-expansion" =<< x)
|
||||
return $ VSeq n $ SeqMap $ \i -> do
|
||||
return $ VSeq n $ IndexSeqMap $ \i -> do
|
||||
go el (flip lookupSeqMap i =<< x')
|
||||
|
||||
TVStream el ->
|
||||
do x' <- delay (Just msg) (fromSeq "during eta-expansion" =<< x)
|
||||
return $ VStream $ SeqMap $ \i ->
|
||||
return $ VStream $ IndexSeqMap $ \i ->
|
||||
go el (flip lookupSeqMap i =<< x')
|
||||
|
||||
TVFun _t1 t2 ->
|
||||
@ -503,7 +499,7 @@ evalComp :: EvalPrims b w
|
||||
-> Eval (GenValue b w)
|
||||
evalComp env len elty body ms =
|
||||
do lenv <- mconcat <$> mapM (branchEnvs (toListEnv env)) ms
|
||||
mkSeq len elty <$> memoMap (SeqMap $ \i -> do
|
||||
mkSeq len elty <$> memoMap (IndexSeqMap $ \i -> do
|
||||
evalExpr (evalListEnv lenv i) body)
|
||||
|
||||
-- | Turn a list of matches into the final environments for each iteration of
|
||||
@ -527,7 +523,7 @@ evalMatch lenv m = case m of
|
||||
-- Select from a sequence of finite length. This causes us to 'stutter'
|
||||
-- through our previous choices `nLen` times.
|
||||
Nat nLen -> do
|
||||
vss <- memoMap $ SeqMap $ \i -> evalExpr (evalListEnv lenv i) expr
|
||||
vss <- memoMap $ IndexSeqMap $ \i -> evalExpr (evalListEnv lenv i) expr
|
||||
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
|
||||
|
||||
@ -6,14 +6,13 @@
|
||||
-- Stability : provisional
|
||||
-- Portability : portable
|
||||
|
||||
{-# LANGUAGE Safe #-}
|
||||
|
||||
{-# LANGUAGE DeriveAnyClass #-}
|
||||
{-# LANGUAGE DeriveFunctor #-}
|
||||
{-# LANGUAGE DeriveGeneric #-}
|
||||
{-# LANGUAGE DoAndIfThenElse #-}
|
||||
{-# LANGUAGE FunctionalDependencies #-}
|
||||
{-# LANGUAGE FlexibleInstances #-}
|
||||
{-# LANGUAGE LambdaCase #-}
|
||||
{-# LANGUAGE MultiParamTypeClasses #-}
|
||||
{-# LANGUAGE PatternGuards #-}
|
||||
{-# LANGUAGE Safe #-}
|
||||
@ -24,9 +23,11 @@
|
||||
module Cryptol.Eval.Value where
|
||||
|
||||
import Data.Bits
|
||||
import Data.IORef
|
||||
import qualified Data.Sequence as Seq
|
||||
import qualified Data.Foldable as Fold
|
||||
|
||||
import Data.Map.Strict (Map)
|
||||
import qualified Data.Map.Strict as Map
|
||||
import MonadLib
|
||||
|
||||
import qualified Cryptol.Eval.Arch as Arch
|
||||
@ -46,9 +47,6 @@ import Numeric (showIntAtBase)
|
||||
import GHC.Generics (Generic)
|
||||
import Control.DeepSeq
|
||||
|
||||
import qualified Data.Cache.LRU.IO as LRU
|
||||
|
||||
|
||||
-- Values ----------------------------------------------------------------------
|
||||
|
||||
-- | Concrete bitvector values: width, value
|
||||
@ -77,21 +75,35 @@ mkBv w i = BV w (mask w i)
|
||||
|
||||
-- | A sequence map represents a mapping from nonnegative integer indices
|
||||
-- to values. These are used to represent both finite and infinite sequences.
|
||||
newtype SeqMap b w = SeqMap { lookupSeqMap :: Integer -> Eval (GenValue b w) }
|
||||
data SeqMap b w
|
||||
= IndexSeqMap !(Integer -> Eval (GenValue b w))
|
||||
| UpdateSeqMap !(Map Integer (Eval (GenValue b w)))
|
||||
!(Integer -> Eval (GenValue b w))
|
||||
|
||||
lookupSeqMap :: SeqMap b w -> Integer -> Eval (GenValue b w)
|
||||
lookupSeqMap (IndexSeqMap f) i = f i
|
||||
lookupSeqMap (UpdateSeqMap m f) i =
|
||||
case Map.lookup i m of
|
||||
Just x -> x
|
||||
Nothing -> f i
|
||||
|
||||
type SeqValMap = SeqMap Bool BV
|
||||
|
||||
instance NFData (SeqMap b w) where
|
||||
rnf x = seq x ()
|
||||
|
||||
-- | Generate a finite sequence map from a list of values
|
||||
finiteSeqMap :: [Eval (GenValue b w)] -> Eval (SeqMap b w)
|
||||
finiteSeqMap xs = do
|
||||
memoMap (SeqMap $ \i -> genericIndex xs i)
|
||||
finiteSeqMap :: [Eval (GenValue b w)] -> SeqMap b w
|
||||
finiteSeqMap xs =
|
||||
UpdateSeqMap
|
||||
(Map.fromList (zip [0..] xs))
|
||||
invalidIndex
|
||||
|
||||
-- | Generate an infinite sequence map from a stream of values
|
||||
infiniteSeqMap :: [Eval (GenValue b w)] -> Eval (SeqMap b w)
|
||||
infiniteSeqMap xs =
|
||||
memoMap (SeqMap $ \i -> genericIndex xs i)
|
||||
-- TODO: use an int-trie?
|
||||
memoMap (IndexSeqMap $ \i -> genericIndex xs i)
|
||||
|
||||
-- | Create a finite list of length `n` of the values from [0..n-1] in
|
||||
-- the given the sequence emap.
|
||||
@ -106,7 +118,11 @@ streamSeqMap m = [ lookupSeqMap m i | i <- [0..] ]
|
||||
reverseSeqMap :: Integer -- ^ Size of the sequence map
|
||||
-> SeqMap b w
|
||||
-> SeqMap b w
|
||||
reverseSeqMap n vals = SeqMap $ \i -> lookupSeqMap vals (n - 1 - i)
|
||||
reverseSeqMap n vals = IndexSeqMap $ \i -> lookupSeqMap vals (n - 1 - i)
|
||||
|
||||
updateSeqMap :: SeqMap b w -> Integer -> Eval (GenValue b w) -> SeqMap b w
|
||||
updateSeqMap (UpdateSeqMap m sm) i x = UpdateSeqMap (Map.insert i x m) sm
|
||||
updateSeqMap (IndexSeqMap f) i x = UpdateSeqMap (Map.singleton i x) f
|
||||
|
||||
-- | Given a number `n` and a sequence map, return two new sequence maps:
|
||||
-- the first containing the values from `[0..n-1]` and the next containing
|
||||
@ -115,33 +131,25 @@ splitSeqMap :: Integer -> SeqMap b w -> (SeqMap b w, SeqMap b w)
|
||||
splitSeqMap n xs = (hd,tl)
|
||||
where
|
||||
hd = xs
|
||||
tl = SeqMap $ \i -> lookupSeqMap xs (i+n)
|
||||
tl = IndexSeqMap $ \i -> lookupSeqMap xs (i+n)
|
||||
|
||||
-- | Given a sequence map, return a new sequence map that is memoized using
|
||||
-- fixed sized memo table. The memo table is managed using a Least-Recently-Used
|
||||
-- (LRU) cache eviction policy.
|
||||
--
|
||||
-- Currently, the cache size is fixed at 64 elements.
|
||||
-- This seems to provide a good compromize between memory useage and effective
|
||||
-- memoization.
|
||||
memoMap :: SeqMap b w -> Eval (SeqMap b w)
|
||||
-- a finite map memo table.
|
||||
memoMap x = do
|
||||
-- TODO: make the size of the LRU cache a tuneable parameter...
|
||||
let lruSize = 64
|
||||
lru <- io $ LRU.newAtomicLRU (Just lruSize)
|
||||
return $ SeqMap $ memo lru
|
||||
cache <- io $ newIORef $ Map.empty
|
||||
return $ IndexSeqMap (memo cache)
|
||||
|
||||
where
|
||||
memo lru i = do
|
||||
mz <- io $ LRU.lookup i lru
|
||||
case mz of
|
||||
Just z -> return z
|
||||
Nothing -> doEval lru i
|
||||
memo cache i = do
|
||||
mz <- io (Map.lookup i <$> readIORef cache)
|
||||
case mz of
|
||||
Just z -> return z
|
||||
Nothing -> doEval cache i
|
||||
|
||||
doEval lru i = do
|
||||
v <- lookupSeqMap x i
|
||||
io $ LRU.insert i v lru
|
||||
return v
|
||||
doEval cache i = do
|
||||
v <- lookupSeqMap x i
|
||||
io $ modifyIORef' cache (Map.insert i v)
|
||||
return v
|
||||
|
||||
-- | Apply the given evaluation function pointwise to the two given
|
||||
-- sequence maps.
|
||||
@ -150,13 +158,13 @@ zipSeqMap :: (GenValue b w -> GenValue b w -> Eval (GenValue b w))
|
||||
-> SeqMap b w
|
||||
-> Eval (SeqMap b w)
|
||||
zipSeqMap f x y =
|
||||
memoMap (SeqMap $ \i -> join (f <$> lookupSeqMap x i <*> lookupSeqMap y i))
|
||||
memoMap (IndexSeqMap $ \i -> join (f <$> lookupSeqMap x i <*> lookupSeqMap y i))
|
||||
|
||||
-- | Apply the given function to each value in the given sequence map
|
||||
mapSeqMap :: (GenValue b w -> Eval (GenValue b w))
|
||||
-> SeqMap b w -> Eval (SeqMap b w)
|
||||
mapSeqMap f x =
|
||||
memoMap (SeqMap $ \i -> f =<< lookupSeqMap x i)
|
||||
memoMap (IndexSeqMap $ \i -> f =<< lookupSeqMap x i)
|
||||
|
||||
-- | For efficency reasons, we handle finite sequences of bits as special cases
|
||||
-- in the evaluator. In cases where we know it is safe to do so, we prefer to
|
||||
@ -224,6 +232,7 @@ forceValue v = case v of
|
||||
VStream _ -> return ()
|
||||
VFun _ -> return ()
|
||||
VPoly _ -> return ()
|
||||
VNumPoly _ -> return ()
|
||||
|
||||
|
||||
instance (Show b, Show w) => Show (GenValue b w) where
|
||||
@ -236,6 +245,7 @@ instance (Show b, Show w) => Show (GenValue b w) where
|
||||
VStream _ -> "stream"
|
||||
VFun _ -> "fun"
|
||||
VPoly _ -> "poly"
|
||||
VNumPoly _ -> "numpoly"
|
||||
|
||||
type Value = GenValue Bool BV
|
||||
|
||||
@ -282,6 +292,7 @@ ppValue opts = loop
|
||||
)
|
||||
VFun _ -> return $ text "<function>"
|
||||
VPoly _ -> return $ text "<polymorphic value>"
|
||||
VNumPoly _ -> return $ text "<polymorphic value>"
|
||||
|
||||
ppWordVal :: WordValue b w -> Eval Doc
|
||||
ppWordVal w = ppWord opts <$> asWordVal w
|
||||
@ -505,10 +516,10 @@ toStream vs =
|
||||
VStream <$> infiniteSeqMap (map ready vs)
|
||||
|
||||
toFinSeq :: BitWord b w
|
||||
=> Integer -> TValue -> [GenValue b w] -> Eval (GenValue b w)
|
||||
=> Integer -> TValue -> [GenValue b w] -> 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)
|
||||
| isTBit elty = VWord len $ ready $ WordVal $ packWord $ map fromVBit vs
|
||||
| otherwise = VSeq len $ finiteSeqMap (map ready vs)
|
||||
|
||||
-- | This is strict!
|
||||
boolToWord :: [Bool] -> Value
|
||||
@ -519,7 +530,7 @@ boolToWord bs = VWord (genericLength bs) $ ready $ WordVal $ packWord bs
|
||||
toSeq :: BitWord b w
|
||||
=> Nat' -> TValue -> [GenValue b w] -> Eval (GenValue b w)
|
||||
toSeq len elty vals = case len of
|
||||
Nat n -> toFinSeq n elty vals
|
||||
Nat n -> return $ toFinSeq n elty vals
|
||||
Inf -> toStream vals
|
||||
|
||||
|
||||
|
||||
@ -18,12 +18,11 @@
|
||||
{-# LANGUAGE BangPatterns #-}
|
||||
module Cryptol.Prims.Eval where
|
||||
|
||||
import Control.Monad (join, when, unless)
|
||||
import Control.Monad (join, unless)
|
||||
|
||||
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
|
||||
import Cryptol.Eval.Value
|
||||
@ -34,9 +33,7 @@ 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 Data.List (sortBy)
|
||||
import qualified Data.Sequence as Seq
|
||||
import Data.Ord (comparing)
|
||||
import Data.Bits (Bits(..))
|
||||
@ -46,8 +43,6 @@ import qualified Data.Text as T
|
||||
|
||||
import System.Random.TF.Gen (seedTFGen)
|
||||
|
||||
import Debug.Trace(trace)
|
||||
|
||||
-- Primitives ------------------------------------------------------------------
|
||||
|
||||
instance EvalPrims Bool BV where
|
||||
@ -522,10 +517,10 @@ zeroV ty = case ty of
|
||||
-- sequences
|
||||
TVSeq w ety
|
||||
| isTBit ety -> word w 0
|
||||
| otherwise -> VSeq w (SeqMap $ \_ -> ready $ zeroV ety)
|
||||
| otherwise -> VSeq w (IndexSeqMap $ \_ -> ready $ zeroV ety)
|
||||
|
||||
TVStream ety ->
|
||||
VStream (SeqMap $ \_ -> ready $ zeroV ety)
|
||||
VStream (IndexSeqMap $ \_ -> ready $ zeroV ety)
|
||||
|
||||
-- functions
|
||||
TVFun _ bty ->
|
||||
@ -578,14 +573,14 @@ joinSeq (Nat parts) each TVBit xs
|
||||
|
||||
-- infinite sequence of words
|
||||
joinSeq Inf each TVBit xs
|
||||
= return $ VStream $ SeqMap $ \i -> do
|
||||
= return $ VStream $ IndexSeqMap $ \i -> do
|
||||
let (q,r) = divMod i each
|
||||
ys <- fromWordVal "join seq" =<< lookupSeqMap xs q
|
||||
VBit <$> (asBitsVal ys `Seq.index` fromInteger r)
|
||||
|
||||
-- finite or infinite sequence of non-words
|
||||
joinSeq parts each _a xs
|
||||
= return $ mkSeq $ SeqMap $ \i -> do
|
||||
= return $ mkSeq $ IndexSeqMap $ \i -> do
|
||||
let (q,r) = divMod i each
|
||||
ys <- fromSeq "join seq" =<< lookupSeqMap xs q
|
||||
lookupSeqMap ys r
|
||||
@ -683,11 +678,11 @@ ecSplitV =
|
||||
case (parts, each) of
|
||||
(Nat p, Nat e) | isTBit a -> do
|
||||
VWord _ val' <- val
|
||||
return $ VSeq p $ SeqMap $ \i -> do
|
||||
return $ VSeq p $ IndexSeqMap $ \i -> do
|
||||
return $ VWord e (extractWordVal e ((p-i-1)*e) <$> val')
|
||||
(Inf, Nat e) | isTBit a -> do
|
||||
val' <- delay Nothing (fromSeq "ecSplitV" =<< val)
|
||||
return $ VStream $ SeqMap $ \i ->
|
||||
return $ VStream $ IndexSeqMap $ \i ->
|
||||
return $ VWord e $ return $ BitsVal $ Seq.fromFunction (fromInteger e) $ \j ->
|
||||
let idx = i*e + toInteger j
|
||||
in idx `seq` do
|
||||
@ -695,14 +690,14 @@ ecSplitV =
|
||||
fromVBit <$> lookupSeqMap xs idx
|
||||
(Nat p, Nat e) -> do
|
||||
val' <- delay Nothing (fromSeq "ecSplitV" =<< val)
|
||||
return $ VSeq p $ SeqMap $ \i ->
|
||||
return $ VSeq e $ SeqMap $ \j -> do
|
||||
return $ VSeq p $ IndexSeqMap $ \i ->
|
||||
return $ VSeq e $ IndexSeqMap $ \j -> do
|
||||
xs <- val'
|
||||
lookupSeqMap xs (e * i + j)
|
||||
(Inf , Nat e) -> do
|
||||
val' <- delay Nothing (fromSeq "ecSplitV" =<< val)
|
||||
return $ VStream $ SeqMap $ \i ->
|
||||
return $ VSeq e $ SeqMap $ \j -> do
|
||||
return $ VStream $ IndexSeqMap $ \i ->
|
||||
return $ VSeq e $ IndexSeqMap $ \j -> do
|
||||
xs <- val'
|
||||
lookupSeqMap xs (e * i + j)
|
||||
_ -> evalPanic "splitV" ["invalid type arguments to split"]
|
||||
@ -730,7 +725,7 @@ transposeV :: BitWord b w
|
||||
-> Eval (GenValue b w)
|
||||
transposeV a b c xs
|
||||
| isTBit c, Nat na <- a =
|
||||
return $ bseq $ SeqMap $ \bi ->
|
||||
return $ bseq $ IndexSeqMap $ \bi ->
|
||||
return $ VWord na $ return $ BitsVal $
|
||||
Seq.fromFunction (fromInteger na) $ \ai -> do
|
||||
ys <- flip lookupSeqMap (toInteger ai) =<< fromSeq "transposeV" xs
|
||||
@ -740,8 +735,8 @@ transposeV a b c xs
|
||||
_ -> evalPanic "transpose" ["expected sequence of bits"]
|
||||
|
||||
| otherwise = do
|
||||
return $ bseq $ SeqMap $ \bi ->
|
||||
return $ aseq $ SeqMap $ \ai -> do
|
||||
return $ bseq $ IndexSeqMap $ \bi ->
|
||||
return $ aseq $ IndexSeqMap $ \ai -> do
|
||||
ys <- flip lookupSeqMap ai =<< fromSeq "transposeV 1" xs
|
||||
z <- flip lookupSeqMap bi =<< fromSeq "transposeV 2" ys
|
||||
return z
|
||||
@ -772,7 +767,7 @@ ccatV front back elty (VWord m l) (VWord n r) =
|
||||
|
||||
ccatV front back elty (VWord m l) (VStream r) = do
|
||||
l' <- delay Nothing l
|
||||
return $ VStream $ SeqMap $ \i ->
|
||||
return $ VStream $ IndexSeqMap $ \i ->
|
||||
if i < m then
|
||||
VBit <$> (flip indexWordValue i =<< l')
|
||||
else
|
||||
@ -782,7 +777,7 @@ ccatV front back elty l r = do
|
||||
l'' <- delay Nothing (fromSeq "ccatV left" l)
|
||||
r'' <- delay Nothing (fromSeq "ccatV right" r)
|
||||
let Nat n = front
|
||||
mkSeq (evalTF TCAdd [front,back]) elty <$> return (SeqMap $ \i ->
|
||||
mkSeq (evalTF TCAdd [front,back]) elty <$> return (IndexSeqMap $ \i ->
|
||||
if i < n then do
|
||||
ls <- l''
|
||||
lookupSeqMap ls i
|
||||
@ -934,7 +929,7 @@ shiftLB w bs by =
|
||||
Seq.replicate (fromInteger (min w by)) (ready False)
|
||||
|
||||
shiftLS :: Nat' -> TValue -> SeqValMap -> Integer -> SeqValMap
|
||||
shiftLS w ety vs by = SeqMap $ \i ->
|
||||
shiftLS w ety vs by = IndexSeqMap $ \i ->
|
||||
case w of
|
||||
Nat len
|
||||
| i+by < len -> lookupSeqMap vs (i+by)
|
||||
@ -954,7 +949,7 @@ shiftRB w bs by =
|
||||
Seq.take (fromInteger (w - min w by)) bs
|
||||
|
||||
shiftRS :: Nat' -> TValue -> SeqValMap -> Integer -> SeqValMap
|
||||
shiftRS w ety vs by = SeqMap $ \i ->
|
||||
shiftRS w ety vs by = IndexSeqMap $ \i ->
|
||||
case w of
|
||||
Nat len
|
||||
| i >= by -> lookupSeqMap vs (i-by)
|
||||
@ -977,7 +972,7 @@ rotateLB w bs by =
|
||||
in tl Seq.>< hd
|
||||
|
||||
rotateLS :: Nat' -> TValue -> SeqValMap -> Integer -> SeqValMap
|
||||
rotateLS w _ vs by = SeqMap $ \i ->
|
||||
rotateLS w _ vs by = IndexSeqMap $ \i ->
|
||||
case w of
|
||||
Nat len -> lookupSeqMap vs ((by + i) `mod` len)
|
||||
_ -> panic "Cryptol.Eval.Prim.rotateLS" [ "unexpected infinite sequence" ]
|
||||
@ -994,7 +989,7 @@ rotateRB w bs by =
|
||||
in tl Seq.>< hd
|
||||
|
||||
rotateRS :: Nat' -> TValue -> SeqValMap -> Integer -> SeqValMap
|
||||
rotateRS w _ vs by = SeqMap $ \i ->
|
||||
rotateRS w _ vs by = IndexSeqMap $ \i ->
|
||||
case w of
|
||||
Nat len -> lookupSeqMap vs ((len - by + i) `mod` len)
|
||||
_ -> panic "Cryptol.Eval.Prim.rotateRS" [ "unexpected infinite sequence" ]
|
||||
@ -1014,7 +1009,7 @@ indexPrimOne bits_op word_op =
|
||||
lam $ \ l -> return $
|
||||
lam $ \ r -> do
|
||||
vs <- l >>= \case
|
||||
VWord _ w -> w >>= \w' -> return $ SeqMap (\i -> VBit <$> indexWordValue w' i)
|
||||
VWord _ w -> w >>= \w' -> return $ IndexSeqMap (\i -> VBit <$> indexWordValue w' i)
|
||||
VSeq _ vs -> return vs
|
||||
VStream vs -> return vs
|
||||
_ -> evalPanic "Expected sequence value" ["indexPrimOne"]
|
||||
@ -1057,12 +1052,12 @@ indexPrimMany bits_op word_op =
|
||||
lam $ \ l -> return $
|
||||
lam $ \ r -> do
|
||||
vs <- (l >>= \case
|
||||
VWord _ w -> w >>= \w' -> return $ SeqMap (\i -> VBit <$> indexWordValue w' i)
|
||||
VWord _ w -> w >>= \w' -> return $ IndexSeqMap (\i -> VBit <$> indexWordValue w' i)
|
||||
VSeq _ vs -> return vs
|
||||
VStream vs -> return vs
|
||||
_ -> evalPanic "Expected sequence value" ["indexPrimMany"])
|
||||
ixs <- fromSeq "indexPrimMany idx" =<< r
|
||||
mkSeq m a <$> memoMap (SeqMap $ \i -> do
|
||||
mkSeq m a <$> memoMap (IndexSeqMap $ \i -> do
|
||||
lookupSeqMap ixs i >>= \case
|
||||
VWord _ w -> w >>= \case
|
||||
WordVal w' -> word_op (fromNat n) a vs w'
|
||||
@ -1082,8 +1077,7 @@ updateFront len _eltTy vs w val = do
|
||||
case len of
|
||||
Inf -> return ()
|
||||
Nat n -> unless (idx < n) (invalidIndex idx)
|
||||
return $ SeqMap $ \i ->
|
||||
if i == idx then val else lookupSeqMap vs i
|
||||
return $ updateSeqMap vs idx val
|
||||
|
||||
updateFront_bits
|
||||
:: Nat'
|
||||
@ -1112,9 +1106,7 @@ updateBack Inf _eltTy _vs _w _val =
|
||||
updateBack (Nat n) _eltTy vs w val = do
|
||||
idx <- bvVal <$> asWordVal w
|
||||
unless (idx < n) (invalidIndex idx)
|
||||
let idx' = n - idx - 1
|
||||
return $ SeqMap $ \i ->
|
||||
if i == idx' then val else lookupSeqMap vs i
|
||||
return $ updateSeqMap vs (n - idx - 1) val
|
||||
|
||||
updateBack_bits
|
||||
:: Nat'
|
||||
@ -1168,7 +1160,7 @@ fromThenV =
|
||||
| bits' >= Arch.maxBigIntWidth -> wordTooWide bits'
|
||||
(Nat first', Nat next', Nat len', Nat bits') ->
|
||||
let diff = next' - first'
|
||||
in VSeq len' $ SeqMap $ \i ->
|
||||
in VSeq len' $ IndexSeqMap $ \i ->
|
||||
ready $ VWord bits' $ return $
|
||||
WordVal $ wordLit bits' (first' + i*diff)
|
||||
_ -> evalPanic "fromThenV" ["invalid arguments"]
|
||||
@ -1185,7 +1177,7 @@ fromToV =
|
||||
| bits' >= Arch.maxBigIntWidth -> wordTooWide bits'
|
||||
(Nat first', Nat lst', Nat bits') ->
|
||||
let len = 1 + (lst' - first')
|
||||
in VSeq len $ SeqMap $ \i ->
|
||||
in VSeq len $ IndexSeqMap $ \i ->
|
||||
ready $ VWord bits' $ return $
|
||||
WordVal $ wordLit bits' (first' + i)
|
||||
_ -> evalPanic "fromToV" ["invalid arguments"]
|
||||
@ -1204,7 +1196,7 @@ fromThenToV =
|
||||
| bits' >= Arch.maxBigIntWidth -> wordTooWide bits'
|
||||
(Nat first', Nat next', Nat lst', Nat len', Nat bits') ->
|
||||
let diff = next' - first'
|
||||
in VSeq len' $ SeqMap $ \i ->
|
||||
in VSeq len' $ IndexSeqMap $ \i ->
|
||||
ready $ VWord bits' $ return $
|
||||
WordVal $ wordLit bits' (first' + i*diff)
|
||||
_ -> evalPanic "fromThenToV" ["invalid arguments"]
|
||||
@ -1215,7 +1207,7 @@ infFromV :: BitWord b w
|
||||
infFromV =
|
||||
nlam $ \(finNat' -> bits) ->
|
||||
wlam $ \first ->
|
||||
return $ VStream $ SeqMap $ \i ->
|
||||
return $ VStream $ IndexSeqMap $ \i ->
|
||||
ready $ VWord bits $ return $
|
||||
WordVal $ wordPlus first (wordLit bits i)
|
||||
|
||||
@ -1226,7 +1218,7 @@ infFromThenV =
|
||||
wlam $ \first -> return $
|
||||
wlam $ \next -> do
|
||||
let diff = wordMinus next first
|
||||
return $ VStream $ SeqMap $ \i ->
|
||||
return $ VStream $ IndexSeqMap $ \i ->
|
||||
ready $ VWord bits $ return $
|
||||
WordVal $ wordPlus first (wordMult diff (wordLit bits i))
|
||||
|
||||
@ -1261,10 +1253,10 @@ errorV ty msg = case ty of
|
||||
TVSeq w ety
|
||||
| isTBit ety -> return $ VWord w $ return $ BitsVal $
|
||||
Seq.replicate (fromInteger w) (cryUserError msg)
|
||||
| otherwise -> return $ VSeq w (SeqMap $ \_ -> errorV ety msg)
|
||||
| otherwise -> return $ VSeq w (IndexSeqMap $ \_ -> errorV ety msg)
|
||||
|
||||
TVStream ety ->
|
||||
return $ VStream (SeqMap $ \_ -> errorV ety msg)
|
||||
return $ VStream (IndexSeqMap $ \_ -> errorV ety msg)
|
||||
|
||||
-- functions
|
||||
TVFun _ bty ->
|
||||
|
||||
@ -255,8 +255,7 @@ parseValue (FTSeq n FTBit) cws =
|
||||
Eval.packWord (map fromVBit vs), cws')
|
||||
where (vs, cws') = parseValues (replicate n FTBit) cws
|
||||
parseValue (FTSeq n t) cws =
|
||||
(Eval.VSeq (toInteger n) $ Eval.SeqMap $ \i ->
|
||||
return $ genericIndex vs i
|
||||
(Eval.VSeq (toInteger n) $ Eval.finiteSeqMap (map Eval.ready vs)
|
||||
, cws'
|
||||
)
|
||||
where (vs, cws') = parseValues (replicate n t) cws
|
||||
@ -320,8 +319,7 @@ forallFinType ty =
|
||||
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) $ Eval.SeqMap $ \i ->
|
||||
return $ genericIndex vs i
|
||||
return $ VSeq (toInteger n) $ Eval.finiteSeqMap (map Eval.ready vs)
|
||||
FTTuple ts -> VTuple <$> mapM (fmap Eval.ready . forallFinType) ts
|
||||
FTRecord fs -> VRecord <$> mapM (traverseSnd (fmap Eval.ready . forallFinType)) fs
|
||||
|
||||
@ -332,7 +330,6 @@ existsFinType ty =
|
||||
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) $ Eval.SeqMap $ \i ->
|
||||
return $ genericIndex vs i
|
||||
return $ VSeq (toInteger n) $ Eval.finiteSeqMap (map Eval.ready vs)
|
||||
FTTuple ts -> VTuple <$> mapM (fmap Eval.ready . existsFinType) ts
|
||||
FTRecord fs -> VRecord <$> mapM (traverseSnd (fmap Eval.ready . existsFinType)) fs
|
||||
|
||||
@ -24,7 +24,7 @@ module Cryptol.Symbolic.Value
|
||||
, fromVBit, fromVFun, fromVPoly, fromVTuple, fromVRecord, lookupRecord
|
||||
, fromSeq, fromVWord
|
||||
, evalPanic
|
||||
, iteSValue, mergeValue, mergeWord
|
||||
, iteSValue, mergeValue, mergeWord, mergeBit
|
||||
)
|
||||
where
|
||||
|
||||
@ -36,10 +36,10 @@ import Data.SBV.Dynamic
|
||||
--import Cryptol.Eval.Monad
|
||||
import Cryptol.Eval.Type (TValue(..), isTBit, tvSeq)
|
||||
import Cryptol.Eval.Value ( GenValue(..), BitWord(..), lam, tlam, toStream,
|
||||
toFinSeq, toSeq, WordValue(..), asWordVal, asBitsVal,
|
||||
toFinSeq, toSeq, WordValue(..), asBitsVal,
|
||||
fromSeq, fromVBit, fromVWord, fromVFun, fromVPoly,
|
||||
fromVTuple, fromVRecord, lookupRecord, SeqMap(..),
|
||||
ppBV,BV(..),integerToChar)
|
||||
ppBV,BV(..),integerToChar, lookupSeqMap )
|
||||
import Cryptol.Utils.Panic (panic)
|
||||
import Cryptol.Utils.PP
|
||||
|
||||
@ -117,7 +117,7 @@ mergeValue f c v1 v2 =
|
||||
| otherwise = panic "Cryptol.Symbolic.Value"
|
||||
[ "mergeValue.mergeField: incompatible values" ]
|
||||
mergeSeqMap x y =
|
||||
SeqMap $ \i -> mergeValue f c <$> lookupSeqMap x i <*> lookupSeqMap y i
|
||||
IndexSeqMap $ \i -> mergeValue f c <$> lookupSeqMap x i <*> lookupSeqMap y i
|
||||
|
||||
-- Symbolic Big-endian Words -------------------------------------------------------
|
||||
|
||||
|
||||
@ -21,7 +21,6 @@ import Data.List(genericReplicate)
|
||||
|
||||
import Prelude ()
|
||||
import Prelude.Compat
|
||||
import Data.List (genericIndex)
|
||||
|
||||
-- | A test result is either a pass, a failure due to evaluating to
|
||||
-- @False@, or a failure due to an exception raised during evaluation
|
||||
@ -121,7 +120,7 @@ typeValues ty =
|
||||
[ VWord n (ready (WordVal (BV n x))) | x <- [ 0 .. 2^n - 1 ] ]
|
||||
|
||||
[ TCon (TC (TCNum n)) _, t ] ->
|
||||
[ VSeq n (SeqMap $ \i -> return $ genericIndex xs i)
|
||||
[ VSeq n (finiteSeqMap (map ready xs))
|
||||
| xs <- sequence $ genericReplicate n
|
||||
$ typeValues t ]
|
||||
_ -> []
|
||||
|
||||
@ -110,7 +110,7 @@ randomWord w _sz g =
|
||||
randomStream :: RandomGen g => Gen g -> Gen g
|
||||
randomStream mkElem sz g =
|
||||
let (g1,g2) = split g
|
||||
in (VStream $ SeqMap $ genericIndex (map ready (unfoldr (Just . mkElem sz) g1)), g2)
|
||||
in (VStream $ IndexSeqMap $ genericIndex (map ready (unfoldr (Just . mkElem sz) g1)), g2)
|
||||
|
||||
{- | Generate a random sequence. This should be used for sequences
|
||||
other than bits. For sequences of bits use "randomWord". -}
|
||||
@ -120,7 +120,7 @@ randomSequence w mkElem sz g = do
|
||||
let f g = let (x,g') = mkElem sz g
|
||||
in seq x (Just (ready x, g'))
|
||||
let xs = Seq.fromList $ genericTake w $ unfoldr f g1
|
||||
seq xs (VSeq w $ SeqMap $ (Seq.index xs . fromInteger), g2)
|
||||
seq xs (VSeq w $ IndexSeqMap $ (Seq.index xs . fromInteger), g2)
|
||||
|
||||
-- | Generate a random tuple value.
|
||||
randomTuple :: RandomGen g => [Gen g] -> Gen g
|
||||
|
||||
Loading…
Reference in New Issue
Block a user