Skip to content

Commit

Permalink
Actually, I think it makes more sense to just put SeqMap
Browse files Browse the repository at this point in the history
directly into the `Cryptol.Backend` module.
  • Loading branch information
robdockins committed Jan 4, 2021
1 parent bf25423 commit dfe522a
Show file tree
Hide file tree
Showing 13 changed files with 141 additions and 161 deletions.
1 change: 0 additions & 1 deletion cryptol.cabal
Original file line number Diff line number Diff line change
Expand Up @@ -160,7 +160,6 @@ library

Cryptol.Backend,
Cryptol.Backend.Arch,
Cryptol.Backend.SeqMap,
Cryptol.Backend.Concrete,
Cryptol.Backend.FloatHelpers,
Cryptol.Backend.Monad,
Expand Down
148 changes: 139 additions & 9 deletions src/Cryptol/Backend.hs
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,22 @@ module Cryptol.Backend
, cryUserError
, cryNoPrimError
, FPArith2
, SeqMap(..)

-- * Sequence Maps
, SeqMap (..)
, lookupSeqMap
, finiteSeqMap
, infiniteSeqMap
, enumerateSeqMap
, streamSeqMap
, reverseSeqMap
, updateSeqMap
, dropSeqMap
, concatSeqMap
, splitSeqMap
, memoMap
, zipSeqMap
, mapSeqMap

-- * Rationals
, SRational(..)
Expand All @@ -31,14 +46,19 @@ module Cryptol.Backend
) where

import Control.Monad.IO.Class
import Data.IORef
import Data.Kind (Type)
import Data.List (genericIndex)
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map

import Cryptol.Backend.FloatHelpers (BF)
import Cryptol.Backend.Monad
( EvalError(..), CallStack, pushCallFrame )
import Cryptol.ModuleSystem.Name(Name)
import Cryptol.Parser.Position
import Cryptol.Utils.Panic(panic)


invalidIndex :: Backend sym => sym -> Integer -> SEval sym a
invalidIndex sym i = raiseError sym (InvalidIndex (Just i))
Expand Down Expand Up @@ -193,13 +213,6 @@ iteRational :: Backend sym => sym -> SBit sym -> SRational sym -> SRational sym
iteRational sym p (SRational a b) (SRational c d) =
SRational <$> iteInteger sym p a c <*> iteInteger sym p b d

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

-- | This type class defines a collection of operations on bits, words and integers that
-- are necessary to define generic evaluator primitives that operate on both concrete
-- and symbolic values uniformly.
Expand Down Expand Up @@ -277,7 +290,7 @@ class (MonadIO (SEval sym), Monad (SGen sym)) => Backend sym where

sGenerateBit :: sym -> SGen sym (SBit sym)

sUnboundedWord :: sym -> Integer -> SGen sym (SWord sym)
sUnboundedWord :: sym -> Integer -> SGen sym (SWord sym)
sBoundedWord :: sym -> (SWord sym, SWord sym) -> SGen sym (SWord sym)
sBoundedSignedWord :: sym -> (SWord sym, SWord sym) -> SGen sym (SWord sym)

Expand Down Expand Up @@ -733,3 +746,120 @@ type FPArith2 sym =
SFloat sym ->
SFloat sym ->
SEval sym (SFloat sym)




-- | 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 ->
do xi <- lookupSeqMap x i
yi <- lookupSeqMap y i
f xi yi)

-- | 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)
1 change: 0 additions & 1 deletion src/Cryptol/Backend/Concrete.hs
Original file line number Diff line number Diff line change
Expand Up @@ -51,7 +51,6 @@ import qualified Cryptol.Backend.Arch as Arch
import qualified Cryptol.Backend.FloatHelpers as FP
import Cryptol.Backend
import Cryptol.Backend.Monad
import Cryptol.Backend.SeqMap
import Cryptol.TypeCheck.Solver.InfNat (genLog)
import Cryptol.Utils.Panic (panic)
import Cryptol.Utils.PP
Expand Down
140 changes: 0 additions & 140 deletions src/Cryptol/Backend/SeqMap.hs

This file was deleted.

1 change: 0 additions & 1 deletion src/Cryptol/Eval.hs
Original file line number Diff line number Diff line change
Expand Up @@ -40,7 +40,6 @@ module Cryptol.Eval (
import Cryptol.Backend
import Cryptol.Backend.Concrete( Concrete(..) )
import Cryptol.Backend.Monad
import Cryptol.Backend.SeqMap
import Cryptol.Eval.Generic ( iteValue )
import Cryptol.Eval.Env
import Cryptol.Eval.Prims
Expand Down
1 change: 0 additions & 1 deletion src/Cryptol/Eval/Concrete.hs
Original file line number Diff line number Diff line change
Expand Up @@ -42,7 +42,6 @@ import Cryptol.Backend
import Cryptol.Backend.Concrete
import Cryptol.Backend.FloatHelpers
import Cryptol.Backend.Monad
import Cryptol.Backend.SeqMap

import Cryptol.Eval.Generic hiding (logicShift)
import Cryptol.Eval.Prims
Expand Down
1 change: 0 additions & 1 deletion src/Cryptol/Eval/Generic.hs
Original file line number Diff line number Diff line change
Expand Up @@ -39,7 +39,6 @@ import Cryptol.Backend
import Cryptol.Backend.Concrete (Concrete(..))
import Cryptol.Backend.Monad( Eval, evalPanic, EvalError(..), Unsupported(..) )
import Cryptol.Testing.Random( randomValue )
import Cryptol.Backend.SeqMap

import Cryptol.Eval.Prims
import Cryptol.Eval.Type
Expand Down
1 change: 0 additions & 1 deletion src/Cryptol/Eval/SBV.hs
Original file line number Diff line number Diff line change
Expand Up @@ -32,7 +32,6 @@ import Data.SBV.Dynamic as SBV
import Cryptol.Backend
import Cryptol.Backend.Monad ( EvalError(..), Unsupported(..) )
import Cryptol.Backend.SBV
import Cryptol.Backend.SeqMap

import Cryptol.Eval.Type (TValue(..))
import Cryptol.Eval.Generic
Expand Down
1 change: 0 additions & 1 deletion src/Cryptol/Eval/Value.hs
Original file line number Diff line number Diff line change
Expand Up @@ -82,7 +82,6 @@ import Data.Ratio
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 )
Expand Down
1 change: 0 additions & 1 deletion src/Cryptol/Eval/What4.hs
Original file line number Diff line number Diff line change
Expand Up @@ -42,7 +42,6 @@ import qualified What4.Utils.AbstractDomains as W4

import Cryptol.Backend
import Cryptol.Backend.Monad ( EvalError(..), Unsupported(..) )
import Cryptol.Backend.SeqMap
import Cryptol.Backend.What4
import qualified Cryptol.Backend.What4.SFloat as W4

Expand Down
Loading

0 comments on commit dfe522a

Please sign in to comment.