mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-12-26 17:32:30 +03:00
Break SeqMap out into a separate module
This commit is contained in:
Rob Dockins
parent
5a84ea5b58
commit
3f710468e8
@ -164,6 +164,7 @@ library
|
||||
Cryptol.Backend.Concrete,
|
||||
Cryptol.Backend.FloatHelpers,
|
||||
Cryptol.Backend.Monad,
|
||||
Cryptol.Backend.SeqMap,
|
||||
Cryptol.Backend.SBV,
|
||||
Cryptol.Backend.What4,
|
||||
|
||||
|
||||
163
src/Cryptol/Backend/SeqMap.hs
Normal file
163
src/Cryptol/Backend/SeqMap.hs
Normal file
@ -0,0 +1,163 @@
|
||||
-- |
|
||||
-- Module : Cryptol.Backend.SeqMap
|
||||
-- Copyright : (c) 2013-2021 Galois, Inc.
|
||||
-- License : BSD3
|
||||
-- Maintainer : cryptol@galois.com
|
||||
-- Stability : provisional
|
||||
-- Portability : portable
|
||||
|
||||
{-# LANGUAGE DeriveAnyClass #-}
|
||||
{-# LANGUAGE DeriveFunctor #-}
|
||||
{-# LANGUAGE DeriveGeneric #-}
|
||||
{-# LANGUAGE DoAndIfThenElse #-}
|
||||
{-# LANGUAGE FlexibleInstances #-}
|
||||
{-# LANGUAGE FlexibleContexts #-}
|
||||
{-# LANGUAGE ImplicitParams #-}
|
||||
{-# LANGUAGE LambdaCase #-}
|
||||
{-# LANGUAGE MultiParamTypeClasses #-}
|
||||
{-# LANGUAGE PatternGuards #-}
|
||||
{-# LANGUAGE Safe #-}
|
||||
{-# LANGUAGE ScopedTypeVariables #-}
|
||||
{-# LANGUAGE StandaloneDeriving #-}
|
||||
{-# LANGUAGE TupleSections #-}
|
||||
{-# LANGUAGE TypeFamilies #-}
|
||||
{-# LANGUAGE ViewPatterns #-}
|
||||
|
||||
module Cryptol.Backend.SeqMap
|
||||
( -- * Sequence Maps
|
||||
SeqMap (..)
|
||||
, lookupSeqMap
|
||||
, finiteSeqMap
|
||||
, infiniteSeqMap
|
||||
, enumerateSeqMap
|
||||
, streamSeqMap
|
||||
, reverseSeqMap
|
||||
, updateSeqMap
|
||||
, dropSeqMap
|
||||
, concatSeqMap
|
||||
, splitSeqMap
|
||||
, memoMap
|
||||
, zipSeqMap
|
||||
, mapSeqMap
|
||||
) where
|
||||
|
||||
import Control.Monad
|
||||
import Control.Monad.IO.Class
|
||||
import Data.List
|
||||
import Data.IORef
|
||||
import Data.Map.Strict (Map)
|
||||
import qualified Data.Map.Strict as Map
|
||||
|
||||
import Cryptol.Backend
|
||||
import Cryptol.Utils.Panic(panic)
|
||||
|
||||
-- | A sequence map represents a mapping from nonnegative integer indices
|
||||
-- to values. These are used to represent both finite and infinite sequences.
|
||||
data SeqMap sym a
|
||||
= IndexSeqMap !(Integer -> SEval sym a)
|
||||
| UpdateSeqMap !(Map Integer (SEval sym a))
|
||||
!(Integer -> SEval sym a)
|
||||
|
||||
lookupSeqMap :: SeqMap sym a -> Integer -> SEval sym a
|
||||
lookupSeqMap (IndexSeqMap f) i = f i
|
||||
lookupSeqMap (UpdateSeqMap m f) i =
|
||||
case Map.lookup i m of
|
||||
Just x -> x
|
||||
Nothing -> f i
|
||||
|
||||
|
||||
-- | Generate a finite sequence map from a list of values
|
||||
finiteSeqMap :: [SEval sym a] -> SeqMap sym a
|
||||
finiteSeqMap xs =
|
||||
UpdateSeqMap
|
||||
(Map.fromList (zip [0..] xs))
|
||||
(\i -> panic "finiteSeqMap" ["Out of bounds access of finite seq map", "length: " ++ show (length xs), show i])
|
||||
|
||||
-- | Generate an infinite sequence map from a stream of values
|
||||
infiniteSeqMap :: Backend sym => sym -> [SEval sym a] -> SEval sym (SeqMap sym a)
|
||||
infiniteSeqMap sym xs =
|
||||
-- TODO: use an int-trie?
|
||||
memoMap sym (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.
|
||||
enumerateSeqMap :: (Integral n) => n -> SeqMap sym a -> [SEval sym a]
|
||||
enumerateSeqMap n m = [ lookupSeqMap m i | i <- [0 .. (toInteger n)-1] ]
|
||||
|
||||
-- | Create an infinite stream of all the values in a sequence map
|
||||
streamSeqMap :: SeqMap sym a -> [SEval sym a]
|
||||
streamSeqMap m = [ lookupSeqMap m i | i <- [0..] ]
|
||||
|
||||
-- | Reverse the order of a finite sequence map
|
||||
reverseSeqMap :: Integer -- ^ Size of the sequence map
|
||||
-> SeqMap sym a
|
||||
-> SeqMap sym a
|
||||
reverseSeqMap n vals = IndexSeqMap $ \i -> lookupSeqMap vals (n - 1 - i)
|
||||
|
||||
updateSeqMap :: SeqMap sym a -> Integer -> SEval sym a -> SeqMap sym a
|
||||
updateSeqMap (UpdateSeqMap m sm) i x = UpdateSeqMap (Map.insert i x m) sm
|
||||
updateSeqMap (IndexSeqMap f) i x = UpdateSeqMap (Map.singleton i x) f
|
||||
|
||||
-- | Concatenate the first @n@ values of the first sequence map onto the
|
||||
-- beginning of the second sequence map.
|
||||
concatSeqMap :: Integer -> SeqMap sym a -> SeqMap sym a -> SeqMap sym a
|
||||
concatSeqMap n x y =
|
||||
IndexSeqMap $ \i ->
|
||||
if i < n
|
||||
then lookupSeqMap x i
|
||||
else lookupSeqMap y (i-n)
|
||||
|
||||
-- | 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
|
||||
-- the values from @n@ onward.
|
||||
splitSeqMap :: Integer -> SeqMap sym a -> (SeqMap sym a, SeqMap sym a)
|
||||
splitSeqMap n xs = (hd,tl)
|
||||
where
|
||||
hd = xs
|
||||
tl = IndexSeqMap $ \i -> lookupSeqMap xs (i+n)
|
||||
|
||||
-- | Drop the first @n@ elements of the given 'SeqMap'.
|
||||
dropSeqMap :: Integer -> SeqMap sym a -> SeqMap sym a
|
||||
dropSeqMap 0 xs = xs
|
||||
dropSeqMap n xs = IndexSeqMap $ \i -> lookupSeqMap xs (i+n)
|
||||
|
||||
-- | Given a sequence map, return a new sequence map that is memoized using
|
||||
-- a finite map memo table.
|
||||
memoMap :: Backend sym => sym -> SeqMap sym a -> SEval sym (SeqMap sym a)
|
||||
memoMap sym x = do
|
||||
stk <- sGetCallStack sym
|
||||
cache <- liftIO $ newIORef $ Map.empty
|
||||
return $ IndexSeqMap (memo cache stk)
|
||||
|
||||
where
|
||||
memo cache stk i = do
|
||||
mz <- liftIO (Map.lookup i <$> readIORef cache)
|
||||
case mz of
|
||||
Just z -> return z
|
||||
Nothing -> sWithCallStack sym stk (doEval cache i)
|
||||
|
||||
doEval cache i = do
|
||||
v <- lookupSeqMap x i
|
||||
liftIO $ atomicModifyIORef' cache (\m -> (Map.insert i v m, ()))
|
||||
return v
|
||||
|
||||
-- | Apply the given evaluation function pointwise to the two given
|
||||
-- sequence maps.
|
||||
zipSeqMap ::
|
||||
Backend sym =>
|
||||
sym ->
|
||||
(a -> a -> SEval sym a) ->
|
||||
SeqMap sym a ->
|
||||
SeqMap sym a ->
|
||||
SEval sym (SeqMap sym a)
|
||||
zipSeqMap sym f x y =
|
||||
memoMap sym (IndexSeqMap $ \i -> join (f <$> lookupSeqMap x i <*> lookupSeqMap y i))
|
||||
|
||||
-- | Apply the given function to each value in the given sequence map
|
||||
mapSeqMap ::
|
||||
Backend sym =>
|
||||
sym ->
|
||||
(a -> SEval sym a) ->
|
||||
SeqMap sym a -> SEval sym (SeqMap sym a)
|
||||
mapSeqMap sym f x =
|
||||
memoMap sym (IndexSeqMap $ \i -> f =<< lookupSeqMap x i)
|
||||
@ -466,7 +466,7 @@ sshrV =
|
||||
logicShift :: (Integer -> Integer -> Integer -> Integer)
|
||||
-- ^ The function may assume its arguments are masked.
|
||||
-- It is responsible for masking its result if needed.
|
||||
-> (Nat' -> TValue -> SeqMap Concrete -> Integer -> SeqMap Concrete)
|
||||
-> (Nat' -> TValue -> SeqMap Concrete (GenValue Concrete) -> Integer -> SeqMap Concrete (GenValue Concrete))
|
||||
-> Prim Concrete
|
||||
logicShift opW opS =
|
||||
PNumPoly \a ->
|
||||
@ -513,7 +513,7 @@ signedShiftRW w ival by
|
||||
else
|
||||
shiftR (signedValue w ival) (fromInteger by')
|
||||
|
||||
shiftLS :: Nat' -> TValue -> SeqMap Concrete -> Integer -> SeqMap Concrete
|
||||
shiftLS :: Nat' -> TValue -> SeqMap Concrete (GenValue Concrete) -> Integer -> SeqMap Concrete (GenValue Concrete)
|
||||
shiftLS w ety vs by
|
||||
| by < 0 = shiftRS w ety vs (negate by)
|
||||
|
||||
@ -525,7 +525,7 @@ shiftLS w ety vs by = IndexSeqMap $ \i ->
|
||||
| otherwise -> evalPanic "shiftLS" ["Index out of bounds"]
|
||||
Inf -> lookupSeqMap vs (i+by)
|
||||
|
||||
shiftRS :: Nat' -> TValue -> SeqMap Concrete -> Integer -> SeqMap Concrete
|
||||
shiftRS :: Nat' -> TValue -> SeqMap Concrete (GenValue Concrete) -> Integer -> SeqMap Concrete (GenValue Concrete)
|
||||
shiftRS w ety vs by
|
||||
| by < 0 = shiftLS w ety vs (negate by)
|
||||
|
||||
@ -546,7 +546,7 @@ rotateLW 0 i _ = i
|
||||
rotateLW w i by = mask w $ (i `shiftL` b) .|. (i `shiftR` (fromInteger w - b))
|
||||
where b = fromInteger (by `mod` w)
|
||||
|
||||
rotateLS :: Nat' -> TValue -> SeqMap Concrete -> Integer -> SeqMap Concrete
|
||||
rotateLS :: Nat' -> TValue -> SeqMap Concrete (GenValue Concrete) -> Integer -> SeqMap Concrete (GenValue Concrete)
|
||||
rotateLS w _ vs by = IndexSeqMap $ \i ->
|
||||
case w of
|
||||
Nat len -> lookupSeqMap vs ((by + i) `mod` len)
|
||||
@ -558,7 +558,7 @@ rotateRW 0 i _ = i
|
||||
rotateRW w i by = mask w $ (i `shiftR` b) .|. (i `shiftL` (fromInteger w - b))
|
||||
where b = fromInteger (by `mod` w)
|
||||
|
||||
rotateRS :: Nat' -> TValue -> SeqMap Concrete -> Integer -> SeqMap Concrete
|
||||
rotateRS :: Nat' -> TValue -> SeqMap Concrete (GenValue Concrete) -> Integer -> SeqMap Concrete (GenValue Concrete)
|
||||
rotateRS w _ vs by = IndexSeqMap $ \i ->
|
||||
case w of
|
||||
Nat len -> lookupSeqMap vs ((len - by + i) `mod` len)
|
||||
@ -567,22 +567,22 @@ rotateRS w _ vs by = IndexSeqMap $ \i ->
|
||||
|
||||
-- Sequence Primitives ---------------------------------------------------------
|
||||
|
||||
indexFront :: Nat' -> TValue -> SeqMap Concrete -> TValue -> BV -> Eval Value
|
||||
indexFront :: Nat' -> TValue -> SeqMap Concrete (GenValue Concrete) -> TValue -> BV -> Eval Value
|
||||
indexFront _mblen _a vs _ix (bvVal -> ix) = lookupSeqMap vs ix
|
||||
|
||||
indexFront_bits :: Nat' -> TValue -> SeqMap Concrete -> TValue -> [Bool] -> Eval Value
|
||||
indexFront_bits :: Nat' -> TValue -> SeqMap Concrete (GenValue Concrete) -> TValue -> [Bool] -> Eval Value
|
||||
indexFront_bits mblen a vs ix bs = indexFront mblen a vs ix =<< packWord Concrete bs
|
||||
|
||||
indexFront_int :: Nat' -> TValue -> SeqMap Concrete -> TValue -> Integer -> Eval Value
|
||||
indexFront_int :: Nat' -> TValue -> SeqMap Concrete (GenValue Concrete) -> TValue -> Integer -> Eval Value
|
||||
indexFront_int _mblen _a vs _ix idx = lookupSeqMap vs idx
|
||||
|
||||
indexBack :: Nat' -> TValue -> SeqMap Concrete -> TValue -> BV -> Eval Value
|
||||
indexBack :: Nat' -> TValue -> SeqMap Concrete (GenValue Concrete) -> TValue -> BV -> Eval Value
|
||||
indexBack mblen a vs ix (bvVal -> idx) = indexBack_int mblen a vs ix idx
|
||||
|
||||
indexBack_bits :: Nat' -> TValue -> SeqMap Concrete -> TValue -> [Bool] -> Eval Value
|
||||
indexBack_bits :: Nat' -> TValue -> SeqMap Concrete (GenValue Concrete) -> TValue -> [Bool] -> Eval Value
|
||||
indexBack_bits mblen a vs ix bs = indexBack mblen a vs ix =<< packWord Concrete bs
|
||||
|
||||
indexBack_int :: Nat' -> TValue -> SeqMap Concrete -> TValue -> Integer -> Eval Value
|
||||
indexBack_int :: Nat' -> TValue -> SeqMap Concrete (GenValue Concrete) -> TValue -> Integer -> Eval Value
|
||||
indexBack_int mblen _a vs _ix idx =
|
||||
case mblen of
|
||||
Nat len -> lookupSeqMap vs (len - idx - 1)
|
||||
@ -591,10 +591,10 @@ indexBack_int mblen _a vs _ix idx =
|
||||
updateFront ::
|
||||
Nat' {- ^ length of the sequence -} ->
|
||||
TValue {- ^ type of values in the sequence -} ->
|
||||
SeqMap Concrete {- ^ sequence to update -} ->
|
||||
SeqMap Concrete (GenValue Concrete) {- ^ sequence to update -} ->
|
||||
Either Integer (WordValue Concrete) {- ^ index -} ->
|
||||
Eval Value {- ^ new value at index -} ->
|
||||
Eval (SeqMap Concrete)
|
||||
Eval (SeqMap Concrete (GenValue Concrete))
|
||||
updateFront _len _eltTy vs (Left idx) val = do
|
||||
return $ updateSeqMap vs idx val
|
||||
|
||||
@ -619,10 +619,10 @@ updateFront_word _len _eltTy bs (Right w) val = do
|
||||
updateBack ::
|
||||
Nat' {- ^ length of the sequence -} ->
|
||||
TValue {- ^ type of values in the sequence -} ->
|
||||
SeqMap Concrete {- ^ sequence to update -} ->
|
||||
SeqMap Concrete (GenValue Concrete) {- ^ sequence to update -} ->
|
||||
Either Integer (WordValue Concrete) {- ^ index -} ->
|
||||
Eval Value {- ^ new value at index -} ->
|
||||
Eval (SeqMap Concrete)
|
||||
Eval (SeqMap Concrete (GenValue Concrete))
|
||||
updateBack Inf _eltTy _vs _w _val =
|
||||
evalPanic "Unexpected infinite sequence in updateEnd" []
|
||||
updateBack (Nat n) _eltTy vs (Left idx) val = do
|
||||
|
||||
@ -969,7 +969,7 @@ joinWordVal sym w1 w2
|
||||
Concrete ->
|
||||
Integer ->
|
||||
Integer ->
|
||||
SeqMap Concrete ->
|
||||
SeqMap Concrete (GenValue Concrete)->
|
||||
SEval Concrete (GenValue Concrete)
|
||||
#-}
|
||||
joinWords :: forall sym.
|
||||
@ -977,7 +977,7 @@ joinWords :: forall sym.
|
||||
sym ->
|
||||
Integer ->
|
||||
Integer ->
|
||||
SeqMap sym ->
|
||||
SeqMap sym (GenValue sym) ->
|
||||
SEval sym (GenValue sym)
|
||||
joinWords sym nParts nEach xs =
|
||||
loop (WordVal <$> wordLit sym 0 0) (enumerateSeqMap nParts xs)
|
||||
@ -999,7 +999,7 @@ joinWords sym nParts nEach xs =
|
||||
Nat' ->
|
||||
Integer ->
|
||||
TValue ->
|
||||
SeqMap Concrete ->
|
||||
SeqMap Concrete (GenValue Concrete) ->
|
||||
SEval Concrete (GenValue Concrete)
|
||||
#-}
|
||||
joinSeq ::
|
||||
@ -1008,7 +1008,7 @@ joinSeq ::
|
||||
Nat' ->
|
||||
Integer ->
|
||||
TValue ->
|
||||
SeqMap sym ->
|
||||
SeqMap sym (GenValue sym) ->
|
||||
SEval sym (GenValue sym)
|
||||
|
||||
-- Special case for 0 length inner sequences.
|
||||
@ -1568,9 +1568,9 @@ assertIndexInBounds sym (Nat n) (Right (LargeBitsVal w bits)) =
|
||||
indexPrim ::
|
||||
Backend sym =>
|
||||
sym ->
|
||||
(Nat' -> TValue -> SeqMap sym -> TValue -> SInteger sym -> SEval sym (GenValue sym)) ->
|
||||
(Nat' -> TValue -> SeqMap sym -> TValue -> [SBit sym] -> SEval sym (GenValue sym)) ->
|
||||
(Nat' -> TValue -> SeqMap sym -> TValue -> SWord sym -> SEval sym (GenValue sym)) ->
|
||||
(Nat' -> TValue -> SeqMap sym (GenValue sym) -> TValue -> SInteger sym -> SEval sym (GenValue sym)) ->
|
||||
(Nat' -> TValue -> SeqMap sym (GenValue sym) -> TValue -> [SBit sym] -> SEval sym (GenValue sym)) ->
|
||||
(Nat' -> TValue -> SeqMap sym (GenValue sym) -> TValue -> SWord sym -> SEval sym (GenValue sym)) ->
|
||||
Prim sym
|
||||
indexPrim sym int_op bits_op word_op =
|
||||
PNumPoly \len ->
|
||||
@ -1599,7 +1599,7 @@ updatePrim ::
|
||||
Backend sym =>
|
||||
sym ->
|
||||
(Nat' -> TValue -> WordValue sym -> Either (SInteger sym) (WordValue sym) -> SEval sym (GenValue sym) -> SEval sym (WordValue sym)) ->
|
||||
(Nat' -> TValue -> SeqMap sym -> Either (SInteger sym) (WordValue sym) -> SEval sym (GenValue sym) -> SEval sym (SeqMap sym)) ->
|
||||
(Nat' -> TValue -> SeqMap sym (GenValue sym) -> Either (SInteger sym) (WordValue sym) -> SEval sym (GenValue sym) -> SEval sym (SeqMap sym (GenValue sym))) ->
|
||||
Prim sym
|
||||
updatePrim sym updateWord updateSeq =
|
||||
PNumPoly \len ->
|
||||
@ -1700,11 +1700,11 @@ infFromThenV sym =
|
||||
|
||||
barrelShifter :: Backend sym =>
|
||||
sym ->
|
||||
(SeqMap sym -> Integer -> SEval sym (SeqMap sym))
|
||||
(SeqMap sym (GenValue sym) -> Integer -> SEval sym (SeqMap sym (GenValue sym)))
|
||||
{- ^ concrete shifting operation -} ->
|
||||
SeqMap sym {- ^ initial value -} ->
|
||||
SeqMap sym (GenValue sym) {- ^ initial value -} ->
|
||||
[SBit sym] {- ^ bits of shift amount, in big-endian order -} ->
|
||||
SEval sym (SeqMap sym)
|
||||
SEval sym (SeqMap sym (GenValue sym))
|
||||
barrelShifter sym shift_op = go
|
||||
where
|
||||
go x [] = return x
|
||||
@ -2059,9 +2059,9 @@ mergeValue sym c v1 v2 =
|
||||
mergeSeqMap :: Backend sym =>
|
||||
sym ->
|
||||
SBit sym ->
|
||||
SeqMap sym ->
|
||||
SeqMap sym ->
|
||||
SeqMap sym
|
||||
SeqMap sym (GenValue sym)->
|
||||
SeqMap sym (GenValue sym)->
|
||||
SeqMap sym (GenValue sym)
|
||||
mergeSeqMap sym c x y =
|
||||
IndexSeqMap $ \i ->
|
||||
iteValue sym c (lookupSeqMap x i) (lookupSeqMap y i)
|
||||
@ -2169,8 +2169,8 @@ sparkParMap ::
|
||||
sym ->
|
||||
(SEval sym (GenValue sym) -> SEval sym (GenValue sym)) ->
|
||||
Integer ->
|
||||
SeqMap sym ->
|
||||
SEval sym (SeqMap sym)
|
||||
SeqMap sym (GenValue sym) ->
|
||||
SEval sym (SeqMap sym (GenValue sym))
|
||||
sparkParMap sym f n m =
|
||||
finiteSeqMap <$> mapM (sSpark sym . g) (enumerateSeqMap n m)
|
||||
where
|
||||
|
||||
@ -92,7 +92,7 @@ indexFront ::
|
||||
SBV ->
|
||||
Nat' ->
|
||||
TValue ->
|
||||
SeqMap SBV ->
|
||||
SeqMap SBV (GenValue SBV) ->
|
||||
TValue ->
|
||||
SVal ->
|
||||
SEval SBV Value
|
||||
@ -131,7 +131,7 @@ indexBack ::
|
||||
SBV ->
|
||||
Nat' ->
|
||||
TValue ->
|
||||
SeqMap SBV ->
|
||||
SeqMap SBV (GenValue SBV) ->
|
||||
TValue ->
|
||||
SWord SBV ->
|
||||
SEval SBV Value
|
||||
@ -142,7 +142,7 @@ indexFront_bits ::
|
||||
SBV ->
|
||||
Nat' ->
|
||||
TValue ->
|
||||
SeqMap SBV ->
|
||||
SeqMap SBV (GenValue SBV) ->
|
||||
TValue ->
|
||||
[SBit SBV] ->
|
||||
SEval SBV Value
|
||||
@ -175,7 +175,7 @@ indexBack_bits ::
|
||||
SBV ->
|
||||
Nat' ->
|
||||
TValue ->
|
||||
SeqMap SBV ->
|
||||
SeqMap SBV (GenValue SBV) ->
|
||||
TValue ->
|
||||
[SBit SBV] ->
|
||||
SEval SBV Value
|
||||
@ -204,10 +204,10 @@ updateFrontSym ::
|
||||
SBV ->
|
||||
Nat' ->
|
||||
TValue ->
|
||||
SeqMap SBV ->
|
||||
SeqMap SBV (GenValue SBV) ->
|
||||
Either (SInteger SBV) (WordValue SBV) ->
|
||||
SEval SBV (GenValue SBV) ->
|
||||
SEval SBV (SeqMap SBV)
|
||||
SEval SBV (SeqMap SBV (GenValue SBV))
|
||||
updateFrontSym sym _len _eltTy vs (Left idx) val =
|
||||
case SBV.svAsInteger idx of
|
||||
Just i -> return $ updateSeqMap vs i val
|
||||
@ -275,10 +275,10 @@ updateBackSym ::
|
||||
SBV ->
|
||||
Nat' ->
|
||||
TValue ->
|
||||
SeqMap SBV ->
|
||||
SeqMap SBV (GenValue SBV) ->
|
||||
Either (SInteger SBV) (WordValue SBV) ->
|
||||
SEval SBV (GenValue SBV) ->
|
||||
SEval SBV (SeqMap SBV)
|
||||
SEval SBV (SeqMap SBV (GenValue SBV))
|
||||
updateBackSym _ Inf _ _ _ _ = evalPanic "Expected finite sequence" ["updateBackSym"]
|
||||
|
||||
updateBackSym sym (Nat n) _eltTy vs (Left idx) val =
|
||||
|
||||
@ -89,16 +89,12 @@ module Cryptol.Eval.Value
|
||||
, updateWordValue
|
||||
) where
|
||||
|
||||
import Control.Monad.IO.Class
|
||||
import Data.Bits
|
||||
import Data.IORef
|
||||
import Data.Map.Strict (Map)
|
||||
import Data.Ratio
|
||||
import qualified Data.Map.Strict as Map
|
||||
import MonadLib
|
||||
import Numeric (showIntAtBase)
|
||||
|
||||
import Cryptol.Backend
|
||||
import Cryptol.Backend.SeqMap
|
||||
import qualified Cryptol.Backend.Arch as Arch
|
||||
import Cryptol.Backend.Monad
|
||||
( evalPanic, wordTooWide, CallStack, combineCallStacks )
|
||||
@ -112,8 +108,6 @@ import Cryptol.Utils.Panic(panic)
|
||||
import Cryptol.Utils.PP
|
||||
import Cryptol.Utils.RecordMap
|
||||
|
||||
import Data.List(genericIndex)
|
||||
|
||||
import GHC.Generics (Generic)
|
||||
|
||||
-- | Some options for evalutaion
|
||||
@ -124,121 +118,11 @@ data EvalOpts = EvalOpts
|
||||
|
||||
-- Values ----------------------------------------------------------------------
|
||||
|
||||
-- | A sequence map represents a mapping from nonnegative integer indices
|
||||
-- to values. These are used to represent both finite and infinite sequences.
|
||||
data SeqMap sym
|
||||
= IndexSeqMap !(Integer -> SEval sym (GenValue sym))
|
||||
| UpdateSeqMap !(Map Integer (SEval sym (GenValue sym)))
|
||||
!(Integer -> SEval sym (GenValue sym))
|
||||
|
||||
lookupSeqMap :: SeqMap sym -> Integer -> SEval sym (GenValue sym)
|
||||
lookupSeqMap (IndexSeqMap f) i = f i
|
||||
lookupSeqMap (UpdateSeqMap m f) i =
|
||||
case Map.lookup i m of
|
||||
Just x -> x
|
||||
Nothing -> f i
|
||||
|
||||
-- | An arbitrarily-chosen number of elements where we switch from a dense
|
||||
-- sequence representation of bit-level words to 'SeqMap' representation.
|
||||
largeBitSize :: Integer
|
||||
largeBitSize = 1 `shiftL` 48
|
||||
|
||||
-- | Generate a finite sequence map from a list of values
|
||||
finiteSeqMap :: [SEval sym (GenValue sym)] -> SeqMap sym
|
||||
finiteSeqMap xs =
|
||||
UpdateSeqMap
|
||||
(Map.fromList (zip [0..] xs))
|
||||
(\i -> panic "finiteSeqMap" ["Out of bounds access of finite seq map", "length: " ++ show (length xs), show i])
|
||||
|
||||
-- | Generate an infinite sequence map from a stream of values
|
||||
infiniteSeqMap :: Backend sym => sym -> [SEval sym (GenValue sym)] -> SEval sym (SeqMap sym)
|
||||
infiniteSeqMap sym xs =
|
||||
-- TODO: use an int-trie?
|
||||
memoMap sym (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.
|
||||
enumerateSeqMap :: (Integral n) => n -> SeqMap sym -> [SEval sym (GenValue sym)]
|
||||
enumerateSeqMap n m = [ lookupSeqMap m i | i <- [0 .. (toInteger n)-1] ]
|
||||
|
||||
-- | Create an infinite stream of all the values in a sequence map
|
||||
streamSeqMap :: SeqMap sym -> [SEval sym (GenValue sym)]
|
||||
streamSeqMap m = [ lookupSeqMap m i | i <- [0..] ]
|
||||
|
||||
-- | Reverse the order of a finite sequence map
|
||||
reverseSeqMap :: Integer -- ^ Size of the sequence map
|
||||
-> SeqMap sym
|
||||
-> SeqMap sym
|
||||
reverseSeqMap n vals = IndexSeqMap $ \i -> lookupSeqMap vals (n - 1 - i)
|
||||
|
||||
updateSeqMap :: SeqMap sym -> Integer -> SEval sym (GenValue sym) -> SeqMap sym
|
||||
updateSeqMap (UpdateSeqMap m sm) i x = UpdateSeqMap (Map.insert i x m) sm
|
||||
updateSeqMap (IndexSeqMap f) i x = UpdateSeqMap (Map.singleton i x) f
|
||||
|
||||
-- | Concatenate the first @n@ values of the first sequence map onto the
|
||||
-- beginning of the second sequence map.
|
||||
concatSeqMap :: Integer -> SeqMap sym -> SeqMap sym -> SeqMap sym
|
||||
concatSeqMap n x y =
|
||||
IndexSeqMap $ \i ->
|
||||
if i < n
|
||||
then lookupSeqMap x i
|
||||
else lookupSeqMap y (i-n)
|
||||
|
||||
-- | 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
|
||||
-- the values from @n@ onward.
|
||||
splitSeqMap :: Integer -> SeqMap sym -> (SeqMap sym, SeqMap sym)
|
||||
splitSeqMap n xs = (hd,tl)
|
||||
where
|
||||
hd = xs
|
||||
tl = IndexSeqMap $ \i -> lookupSeqMap xs (i+n)
|
||||
|
||||
-- | Drop the first @n@ elements of the given 'SeqMap'.
|
||||
dropSeqMap :: Integer -> SeqMap sym -> SeqMap sym
|
||||
dropSeqMap 0 xs = xs
|
||||
dropSeqMap n xs = IndexSeqMap $ \i -> lookupSeqMap xs (i+n)
|
||||
|
||||
-- | Given a sequence map, return a new sequence map that is memoized using
|
||||
-- a finite map memo table.
|
||||
memoMap :: Backend sym => sym -> SeqMap sym -> SEval sym (SeqMap sym)
|
||||
memoMap sym x = do
|
||||
stk <- sGetCallStack sym
|
||||
cache <- liftIO $ newIORef $ Map.empty
|
||||
return $ IndexSeqMap (memo cache stk)
|
||||
|
||||
where
|
||||
memo cache stk i = do
|
||||
mz <- liftIO (Map.lookup i <$> readIORef cache)
|
||||
case mz of
|
||||
Just z -> return z
|
||||
Nothing -> sWithCallStack sym stk (doEval cache i)
|
||||
|
||||
doEval cache i = do
|
||||
v <- lookupSeqMap x i
|
||||
liftIO $ atomicModifyIORef' cache (\m -> (Map.insert i v m, ()))
|
||||
return v
|
||||
|
||||
-- | Apply the given evaluation function pointwise to the two given
|
||||
-- sequence maps.
|
||||
zipSeqMap ::
|
||||
Backend sym =>
|
||||
sym ->
|
||||
(GenValue sym -> GenValue sym -> SEval sym (GenValue sym)) ->
|
||||
SeqMap sym ->
|
||||
SeqMap sym ->
|
||||
SEval sym (SeqMap sym)
|
||||
zipSeqMap sym f x y =
|
||||
memoMap sym (IndexSeqMap $ \i -> join (f <$> lookupSeqMap x i <*> lookupSeqMap y i))
|
||||
|
||||
-- | Apply the given function to each value in the given sequence map
|
||||
mapSeqMap ::
|
||||
Backend sym =>
|
||||
sym ->
|
||||
(GenValue sym -> SEval sym (GenValue sym)) ->
|
||||
SeqMap sym -> SEval sym (SeqMap sym)
|
||||
mapSeqMap sym f x =
|
||||
memoMap sym (IndexSeqMap $ \i -> f =<< lookupSeqMap x i)
|
||||
|
||||
-- | For efficiency 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
|
||||
-- used a "packed word" representation of bit sequences. This allows us to rely
|
||||
@ -251,7 +135,8 @@ mapSeqMap sym f x =
|
||||
data WordValue sym
|
||||
= ThunkWordVal Integer !(SEval sym (WordValue sym))
|
||||
| WordVal !(SWord sym) -- ^ Packed word representation for bit sequences.
|
||||
| LargeBitsVal !Integer !(SeqMap sym) -- ^ A large bitvector sequence, represented as a
|
||||
| LargeBitsVal !Integer !(SeqMap sym (GenValue sym))
|
||||
-- ^ A large bitvector sequence, represented as a
|
||||
-- 'SeqMap' of bits.
|
||||
deriving (Generic)
|
||||
|
||||
@ -262,8 +147,8 @@ asWordVal sym (ThunkWordVal _ m) = asWordVal sym =<< m
|
||||
asWordVal sym (LargeBitsVal n xs) = packWord sym =<< traverse (fromVBit <$>) (enumerateSeqMap n xs)
|
||||
|
||||
-- | Force a word value into a sequence of bits
|
||||
asBitsMap :: Backend sym => sym -> WordValue sym -> SeqMap sym
|
||||
asBitsMap sym (WordVal w) = IndexSeqMap $ \i -> VBit <$> (wordBit sym w i)
|
||||
asBitsMap :: Backend sym => sym -> WordValue sym -> SeqMap sym (GenValue sym)
|
||||
asBitsMap sym (WordVal w) = IndexSeqMap $ \i -> VBit <$> wordBit sym w i
|
||||
asBitsMap sym (ThunkWordVal _ m) = IndexSeqMap $ \i -> do mp <- asBitsMap sym <$> m; lookupSeqMap mp i
|
||||
asBitsMap _ (LargeBitsVal _ xs) = xs
|
||||
|
||||
@ -272,7 +157,7 @@ asBitsMap _ (LargeBitsVal _ xs) = xs
|
||||
enumerateWordValue :: Backend sym => sym -> WordValue sym -> SEval sym [SBit sym]
|
||||
enumerateWordValue sym (WordVal w) = unpackWord sym w
|
||||
enumerateWordValue sym (ThunkWordVal _ m) = enumerateWordValue sym =<< m
|
||||
enumerateWordValue _ (LargeBitsVal n xs) = traverse (fromVBit <$>) (enumerateSeqMap n xs)
|
||||
enumerateWordValue _ (LargeBitsVal n xs) = traverse (fromVBit <$>) (enumerateSeqMap n xs)
|
||||
|
||||
-- | Turn a word value into a sequence of bits, forcing each bit.
|
||||
-- The sequence is returned in reverse of the usual order, which is little-endian order.
|
||||
@ -326,10 +211,10 @@ data GenValue sym
|
||||
| VInteger !(SInteger sym) -- ^ @ Integer @ or @ Z n @
|
||||
| VRational !(SRational sym) -- ^ @ Rational @
|
||||
| VFloat !(SFloat sym)
|
||||
| VSeq !Integer !(SeqMap sym) -- ^ @ [n]a @
|
||||
| VSeq !Integer !(SeqMap sym (GenValue sym)) -- ^ @ [n]a @
|
||||
-- Invariant: VSeq is never a sequence of bits
|
||||
| VWord !Integer !(WordValue sym) -- ^ @ [n]Bit @
|
||||
| VStream !(SeqMap sym) -- ^ @ [inf]a @
|
||||
| VStream !(SeqMap sym (GenValue sym)) -- ^ @ [inf]a @
|
||||
| VFun CallStack (SEval sym (GenValue sym) -> SEval sym (GenValue sym)) -- ^ functions
|
||||
| VPoly CallStack (TValue -> SEval sym (GenValue sym)) -- ^ polymorphic values (kind *)
|
||||
| VNumPoly CallStack (Nat' -> SEval sym (GenValue sym)) -- ^ polymorphic values (kind #)
|
||||
@ -412,7 +297,7 @@ ppValue x opts = loop
|
||||
ppWordVal :: WordValue sym -> SEval sym Doc
|
||||
ppWordVal w = ppSWord x opts =<< asWordVal x w
|
||||
|
||||
ppWordSeq :: Integer -> SeqMap sym -> SEval sym Doc
|
||||
ppWordSeq :: Integer -> SeqMap sym (GenValue sym) -> SEval sym Doc
|
||||
ppWordSeq sz vals = do
|
||||
ws <- sequence (enumerateSeqMap sz vals)
|
||||
case ws of
|
||||
@ -553,7 +438,7 @@ ilam sym f =
|
||||
|
||||
-- | Construct either a finite sequence, or a stream. In the finite case,
|
||||
-- record whether or not the elements were bits, to aid pretty-printing.
|
||||
mkSeq :: Backend sym => Nat' -> TValue -> SeqMap sym -> GenValue sym
|
||||
mkSeq :: Backend sym => Nat' -> TValue -> SeqMap sym (GenValue sym) -> GenValue sym
|
||||
mkSeq len elty vals = case len of
|
||||
Nat n
|
||||
| isTBit elty -> VWord n $ LargeBitsVal n vals
|
||||
@ -582,13 +467,13 @@ fromVRational val = case val of
|
||||
_ -> evalPanic "fromVRational" ["not a Rational"]
|
||||
|
||||
-- | Extract a finite sequence value.
|
||||
fromVSeq :: GenValue sym -> SeqMap sym
|
||||
fromVSeq :: GenValue sym -> SeqMap sym (GenValue sym)
|
||||
fromVSeq val = case val of
|
||||
VSeq _ vs -> vs
|
||||
_ -> evalPanic "fromVSeq" ["not a sequence"]
|
||||
|
||||
-- | Extract a sequence.
|
||||
fromSeq :: Backend sym => String -> GenValue sym -> SEval sym (SeqMap sym)
|
||||
fromSeq :: Backend sym => String -> GenValue sym -> SEval sym (SeqMap sym (GenValue sym))
|
||||
fromSeq msg val = case val of
|
||||
VSeq _ vs -> return vs
|
||||
VStream vs -> return vs
|
||||
|
||||
@ -459,7 +459,7 @@ getUninterpFn sym funNm args ret =
|
||||
]
|
||||
|
||||
toWord32 :: W4.IsSymExprBuilder sym =>
|
||||
What4 sym -> String -> SeqMap (What4 sym) -> Integer -> SEval (What4 sym) (W4.SymBV sym 32)
|
||||
What4 sym -> String -> SeqMap (What4 sym) (GenValue (What4 sym)) -> Integer -> SEval (What4 sym) (W4.SymBV sym 32)
|
||||
toWord32 sym nm ss i =
|
||||
do x <- fromVWord sym nm =<< lookupSeqMap ss i
|
||||
case x of
|
||||
@ -470,7 +470,7 @@ fromWord32 :: W4.IsSymExprBuilder sym => W4.SymBV sym 32 -> SEval (What4 sym) (V
|
||||
fromWord32 = pure . VWord 32 . WordVal . SW.DBV
|
||||
|
||||
toWord64 :: W4.IsSymExprBuilder sym =>
|
||||
What4 sym -> String -> SeqMap (What4 sym) -> Integer -> SEval (What4 sym) (W4.SymBV sym 64)
|
||||
What4 sym -> String -> SeqMap (What4 sym) (GenValue (What4 sym)) -> Integer -> SEval (What4 sym) (W4.SymBV sym 64)
|
||||
toWord64 sym nm ss i =
|
||||
do x <- fromVWord sym nm =<< lookupSeqMap ss i
|
||||
case x of
|
||||
@ -537,7 +537,7 @@ indexFront_int ::
|
||||
What4 sym ->
|
||||
Nat' ->
|
||||
TValue ->
|
||||
SeqMap (What4 sym) ->
|
||||
SeqMap (What4 sym) (GenValue (What4 sym)) ->
|
||||
TValue ->
|
||||
SInteger (What4 sym) ->
|
||||
SEval (What4 sym) (Value sym)
|
||||
@ -586,7 +586,7 @@ indexBack_int ::
|
||||
What4 sym ->
|
||||
Nat' ->
|
||||
TValue ->
|
||||
SeqMap (What4 sym) ->
|
||||
SeqMap (What4 sym) (GenValue (What4 sym)) ->
|
||||
TValue ->
|
||||
SInteger (What4 sym) ->
|
||||
SEval (What4 sym) (Value sym)
|
||||
@ -598,7 +598,7 @@ indexFront_word ::
|
||||
What4 sym ->
|
||||
Nat' ->
|
||||
TValue ->
|
||||
SeqMap (What4 sym) ->
|
||||
SeqMap (What4 sym) (GenValue (What4 sym)) ->
|
||||
TValue ->
|
||||
SWord (What4 sym) ->
|
||||
SEval (What4 sym) (Value sym)
|
||||
@ -639,7 +639,7 @@ indexBack_word ::
|
||||
What4 sym ->
|
||||
Nat' ->
|
||||
TValue ->
|
||||
SeqMap (What4 sym) ->
|
||||
SeqMap (What4 sym) (GenValue (What4 sym)) ->
|
||||
TValue ->
|
||||
SWord (What4 sym) ->
|
||||
SEval (What4 sym) (Value sym)
|
||||
@ -651,7 +651,7 @@ indexFront_bits :: forall sym.
|
||||
What4 sym ->
|
||||
Nat' ->
|
||||
TValue ->
|
||||
SeqMap (What4 sym) ->
|
||||
SeqMap (What4 sym) (GenValue (What4 sym)) ->
|
||||
TValue ->
|
||||
[SBit (What4 sym)] ->
|
||||
SEval (What4 sym) (Value sym)
|
||||
@ -684,7 +684,7 @@ indexBack_bits ::
|
||||
What4 sym ->
|
||||
Nat' ->
|
||||
TValue ->
|
||||
SeqMap (What4 sym) ->
|
||||
SeqMap (What4 sym) (GenValue (What4 sym)) ->
|
||||
TValue ->
|
||||
[SBit (What4 sym)] ->
|
||||
SEval (What4 sym) (Value sym)
|
||||
@ -723,10 +723,10 @@ updateFrontSym ::
|
||||
What4 sym ->
|
||||
Nat' ->
|
||||
TValue ->
|
||||
SeqMap (What4 sym) ->
|
||||
SeqMap (What4 sym) (GenValue (What4 sym)) ->
|
||||
Either (SInteger (What4 sym)) (WordValue (What4 sym)) ->
|
||||
SEval (What4 sym) (Value sym) ->
|
||||
SEval (What4 sym) (SeqMap (What4 sym))
|
||||
SEval (What4 sym) (SeqMap (What4 sym) (GenValue (What4 sym)))
|
||||
updateFrontSym sym _len _eltTy vs (Left idx) val =
|
||||
case W4.asInteger idx of
|
||||
Just i -> return $ updateSeqMap vs i val
|
||||
@ -748,10 +748,10 @@ updateBackSym ::
|
||||
What4 sym ->
|
||||
Nat' ->
|
||||
TValue ->
|
||||
SeqMap (What4 sym) ->
|
||||
SeqMap (What4 sym) (GenValue (What4 sym)) ->
|
||||
Either (SInteger (What4 sym)) (WordValue (What4 sym)) ->
|
||||
SEval (What4 sym) (Value sym) ->
|
||||
SEval (What4 sym) (SeqMap (What4 sym))
|
||||
SEval (What4 sym) (SeqMap (What4 sym) (GenValue (What4 sym)))
|
||||
updateBackSym _ Inf _ _ _ _ = evalPanic "Expected finite sequence" ["updateBackSym"]
|
||||
|
||||
updateBackSym sym (Nat n) _eltTy vs (Left idx) val =
|
||||
|
||||
Loading…
Reference in New Issue
Block a user