diff --git a/cryptol.cabal b/cryptol.cabal index 2605a11c1..a737c0d32 100644 --- a/cryptol.cabal +++ b/cryptol.cabal @@ -160,7 +160,6 @@ library Cryptol.Backend, Cryptol.Backend.Arch, - Cryptol.Backend.SeqMap, Cryptol.Backend.Concrete, Cryptol.Backend.FloatHelpers, Cryptol.Backend.Monad, diff --git a/src/Cryptol/Backend.hs b/src/Cryptol/Backend.hs index 052d1feed..586932b1f 100644 --- a/src/Cryptol/Backend.hs +++ b/src/Cryptol/Backend.hs @@ -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(..) @@ -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)) @@ -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. @@ -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) @@ -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) diff --git a/src/Cryptol/Backend/Concrete.hs b/src/Cryptol/Backend/Concrete.hs index af1d60596..03ae7718e 100644 --- a/src/Cryptol/Backend/Concrete.hs +++ b/src/Cryptol/Backend/Concrete.hs @@ -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 diff --git a/src/Cryptol/Backend/SeqMap.hs b/src/Cryptol/Backend/SeqMap.hs deleted file mode 100644 index 69e356a9b..000000000 --- a/src/Cryptol/Backend/SeqMap.hs +++ /dev/null @@ -1,140 +0,0 @@ --- | --- Module : Cryptol.Eval.SeqMap --- Copyright : (c) 2020 Galois, Inc. --- License : BSD3 --- Maintainer : cryptol@galois.com --- Stability : provisional --- Portability : portable --- - -module Cryptol.Backend.SeqMap - ( SeqMap (..) - , lookupSeqMap - , finiteSeqMap - , infiniteSeqMap - , enumerateSeqMap - , streamSeqMap - , reverseSeqMap - , updateSeqMap - , dropSeqMap - , concatSeqMap - , splitSeqMap - , memoMap - , zipSeqMap - , mapSeqMap - ) where - -import Control.Monad.IO.Class -import Data.IORef -import Data.List (genericIndex) -import qualified Data.Map.Strict as Map - -import Cryptol.Backend -import Cryptol.Utils.Panic(panic) - - -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) diff --git a/src/Cryptol/Eval.hs b/src/Cryptol/Eval.hs index 343fd5879..e9ad2a223 100644 --- a/src/Cryptol/Eval.hs +++ b/src/Cryptol/Eval.hs @@ -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 diff --git a/src/Cryptol/Eval/Concrete.hs b/src/Cryptol/Eval/Concrete.hs index 4dadd2f13..20093f72c 100644 --- a/src/Cryptol/Eval/Concrete.hs +++ b/src/Cryptol/Eval/Concrete.hs @@ -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 diff --git a/src/Cryptol/Eval/Generic.hs b/src/Cryptol/Eval/Generic.hs index 5d51b92fd..849a58095 100644 --- a/src/Cryptol/Eval/Generic.hs +++ b/src/Cryptol/Eval/Generic.hs @@ -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 diff --git a/src/Cryptol/Eval/SBV.hs b/src/Cryptol/Eval/SBV.hs index 819ce41ba..1fd6afa71 100644 --- a/src/Cryptol/Eval/SBV.hs +++ b/src/Cryptol/Eval/SBV.hs @@ -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 diff --git a/src/Cryptol/Eval/Value.hs b/src/Cryptol/Eval/Value.hs index e3c5f4521..828a30fce 100644 --- a/src/Cryptol/Eval/Value.hs +++ b/src/Cryptol/Eval/Value.hs @@ -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 ) diff --git a/src/Cryptol/Eval/What4.hs b/src/Cryptol/Eval/What4.hs index 3323700e5..797102798 100644 --- a/src/Cryptol/Eval/What4.hs +++ b/src/Cryptol/Eval/What4.hs @@ -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 diff --git a/src/Cryptol/REPL/Command.hs b/src/Cryptol/REPL/Command.hs index 0a7f2372a..445827802 100644 --- a/src/Cryptol/REPL/Command.hs +++ b/src/Cryptol/REPL/Command.hs @@ -63,8 +63,8 @@ import qualified Cryptol.ModuleSystem.Renamer as M (RenamerWarning(SymbolShadowe import qualified Cryptol.Utils.Ident as M import qualified Cryptol.ModuleSystem.Env as M +import qualified Cryptol.Backend as E import qualified Cryptol.Backend.Monad as E -import qualified Cryptol.Backend.SeqMap as E import Cryptol.Eval.Concrete( Concrete(..) ) import qualified Cryptol.Eval.Concrete as Concrete import qualified Cryptol.Eval.Env as E diff --git a/src/Cryptol/Symbolic.hs b/src/Cryptol/Symbolic.hs index 1c2687940..0b7973724 100644 --- a/src/Cryptol/Symbolic.hs +++ b/src/Cryptol/Symbolic.hs @@ -50,7 +50,6 @@ import qualified LibBF as FP import Cryptol.Backend import Cryptol.Backend.FloatHelpers(bfValue) -import Cryptol.Backend.SeqMap import qualified Cryptol.Eval.Concrete as Concrete import Cryptol.Eval.Value diff --git a/src/Cryptol/Testing/Random.hs b/src/Cryptol/Testing/Random.hs index 59b1ee3f9..3e063bdd3 100644 --- a/src/Cryptol/Testing/Random.hs +++ b/src/Cryptol/Testing/Random.hs @@ -39,10 +39,9 @@ import qualified Data.Sequence as Seq import System.Random (split, random, randomR) import System.Random.TF.Gen (TFGen) -import Cryptol.Backend (Backend(..), SRational(..)) +import Cryptol.Backend (Backend(..), SRational(..), SeqMap(..), finiteSeqMap) import Cryptol.Backend.Monad (runEval,Eval,EvalErrorEx(..)) import Cryptol.Backend.Concrete -import Cryptol.Backend.SeqMap import Cryptol.Eval.Type (TValue(..)) import Cryptol.Eval.Value (GenValue(..), WordValue(..),