Start generalizing evaluator code to be used in both the

concrete and symbolic evaluators.

src/Cryptol/Eval.hs

@@ -23,7 +23,7 @@ module Cryptol.Eval (
 import Cryptol.Eval.Env
 import Cryptol.Eval.Monad
 import Cryptol.Eval.Type
-import Cryptol.Eval.Value
+import Cryptol.Eval.Value hiding (evalPrim)
 import Cryptol.ModuleSystem.Name
 import Cryptol.TypeCheck.AST
 import Cryptol.TypeCheck.Solver.InfNat(Nat'(..))
@@ -41,6 +41,9 @@ import qualified Data.Map.Strict as Map
 import Prelude ()
 import Prelude.Compat
 
+type EvalEnv = GenEvalEnv Bool BV
+type ReadEnv = EvalEnv
+
 -- Expression Evaluation -------------------------------------------------------
 
 moduleEnv :: Module -> EvalEnv -> Eval EvalEnv

src/Cryptol/Eval/Env.hs

@@ -29,16 +29,15 @@ import Prelude.Compat
 
 -- Evaluation Environment ------------------------------------------------------
 
-type ReadEnv = EvalEnv
-
-data EvalEnv = EvalEnv
-  { envVars       :: !(Map.Map Name (Eval Value))
+data GenEvalEnv b w = EvalEnv
+  { envVars       :: !(Map.Map Name (Eval (GenValue b w)))
   , envTypes      :: !(Map.Map TVar TValue)
   } deriving (Generic)
 
-instance NFData EvalEnv where rnf = genericRnf
+instance (NFData b, NFData w) => NFData (GenEvalEnv b w)
+  where rnf = genericRnf
 
-instance Monoid EvalEnv where
+instance Monoid (GenEvalEnv b w) where
   mempty = EvalEnv
     { envVars       = Map.empty
     , envTypes      = Map.empty
@@ -49,22 +48,20 @@ instance Monoid EvalEnv where
     , envTypes    = Map.union (envTypes    l) (envTypes    r)
     }
 
-ppEnv :: PPOpts -> EvalEnv -> Eval Doc
+ppEnv :: BitWord b w => PPOpts -> GenEvalEnv b w -> Eval Doc
 ppEnv opts env = brackets . fsep <$> mapM bind (Map.toList (envVars env))
   where
    bind (k,v) = do vdoc <- ppValue opts =<< v
                    return (pp k <+> text "->" <+> vdoc)
 
---instance PP (WithBase EvalEnv) where
---  ppPrec _ (WithBase opts env) = brackets (fsep (map bind (Map.toList (envVars env))))
---    where
---    bind (k,v) = pp k <+> text "->" <+> ppValue opts v
-
-emptyEnv :: EvalEnv
+emptyEnv :: GenEvalEnv b w
 emptyEnv  = mempty
 
 -- | Bind a variable in the evaluation environment.
-bindVar :: Name -> Eval Value -> EvalEnv -> Eval EvalEnv
+bindVar :: Name
+        -> Eval (GenValue b w)
+        -> GenEvalEnv b w
+        -> Eval (GenEvalEnv b w)
 bindVar n val env = do
   let nm = show $ ppLocName n
   val' <- delay (Just nm) val
@@ -72,15 +69,15 @@ bindVar n val env = do
 
 -- | Lookup a variable in the environment.
 {-# INLINE lookupVar #-}
-lookupVar :: Name -> EvalEnv -> Maybe (Eval Value)
+lookupVar :: Name -> GenEvalEnv b w -> Maybe (Eval (GenValue b w))
 lookupVar n env = Map.lookup n (envVars env)
 
 -- | Bind a type variable of kind *.
 {-# INLINE bindType #-}
-bindType :: TVar -> TValue -> EvalEnv -> EvalEnv
+bindType :: TVar -> TValue -> GenEvalEnv b w -> GenEvalEnv b w
 bindType p ty env = env { envTypes = Map.insert p ty (envTypes env) }
 
 -- | Lookup a type variable.
 {-# INLINE lookupType #-}
-lookupType :: TVar -> EvalEnv -> Maybe TValue
+lookupType :: TVar -> GenEvalEnv b w -> Maybe TValue
 lookupType p env = Map.lookup p (envTypes env)

src/Cryptol/Eval/Type.hs

@@ -22,7 +22,7 @@ import Data.Maybe(fromMaybe)
 -- Type Evaluation -------------------------------------------------------------
 
 -- | Evaluation for types.
-evalType :: EvalEnv -> Type -> TValue
+evalType :: GenEvalEnv b w -> Type -> TValue
 evalType env = TValue . go
   where
   go ty =

src/Cryptol/Eval/Value.hs

@@ -9,6 +9,7 @@
 {-# LANGUAGE PatternGuards #-}
 {-# LANGUAGE DeriveFunctor #-}
 {-# LANGUAGE DeriveGeneric #-}
+{-# LANGUAGE FunctionalDependencies #-}
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE Safe #-}
@@ -99,6 +100,17 @@ data BV = BV !Integer !Integer deriving (Generic)
 instance Show BV where
   show = show . bvVal
 
+-- | Apply an integer function to the values of bitvectors.
+--   This function assumes both bitvectors are the same width,
+--   and the result of the function will not require masking.
+binBV :: (Integer -> Integer -> Integer) -> BV -> BV -> BV
+binBV f (BV w x) (BV _ y) = BV w (f x y)
+
+-- | Apply an integer function to the values of a bitvector.
+--   This function assumes the function will not require masking.
+unaryBV :: (Integer -> Integer) -> BV -> BV
+unaryBV f (BV w x) = BV w $ f x
+
 bvVal :: BV -> Integer
 bvVal (BV _w x) = x
 
@@ -149,7 +161,7 @@ memoMap x = do
     m <- io $ readIORef r
     case Map.lookup i m of
       Just (Just z) -> return z
-      Just Nothing -> 
+      Just Nothing ->
         cryLoopError $ unwords ["memoMap location:", show i]
       Nothing -> do
         --io $ putStrLn $ unwords ["Forcing memo map location", show i]
@@ -165,7 +177,7 @@ zipSeqMap :: (GenValue b w -> GenValue b w -> Eval (GenValue b w))
           -> Eval (SeqMap b w)
 zipSeqMap f x y =
   memoMap (SeqMap $ \i -> join (f <$> lookupSeqMap x i <*> lookupSeqMap y i))
-  
+
 mapSeqMap :: (GenValue b w -> Eval (GenValue b w))
           -> SeqMap b w -> Eval (SeqMap b w)
 mapSeqMap f x =
@@ -227,10 +239,14 @@ atFst f (x,y) = fmap (,y) $ f x
 atSnd :: Functor f => (a -> f b) -> (c, a) -> f (c, b)
 atSnd f (x,y) = fmap (x,) $ f y
 
-ppValue :: PPOpts -> Value -> Eval Doc
+ppValue :: forall b w
+         . BitWord b w
+        => PPOpts
+        -> GenValue b w
+        -> Eval Doc
 ppValue opts = loop
   where
-  loop :: Value -> Eval Doc
+  loop :: GenValue b w -> Eval Doc
   loop val = case val of
     VRecord fs         -> do fs' <- traverse (atSnd (>>=loop)) $ fs
                              return $ braces (sep (punctuate comma (map ppField fs')))
@@ -238,8 +254,7 @@ ppValue opts = loop
       ppField (f,r) = pp f <+> char '=' <+> r
     VTuple vals        -> do vals' <- traverse (>>=loop) vals
                              return $ parens (sep (punctuate comma vals'))
-    VBit b | b         -> return $ text "True"
-           | otherwise -> return $ text "False"
+    VBit b             -> return $ ppBit b
     VSeq sz isWord vals
        | isWord        -> ppWord opts <$> fromVWord "ppValue" val
        | otherwise     -> ppWordSeq sz vals
@@ -252,13 +267,17 @@ ppValue opts = loop
     VFun _             -> return $ text "<function>"
     VPoly _            -> return $ text "<polymorphic value>"
 
-  ppWordSeq :: Integer -> SeqValMap -> Eval Doc
+  ppWordSeq :: Integer -> SeqMap b w -> Eval Doc
   ppWordSeq sz vals = do
     ws <- sequence (enumerateSeqMap sz vals)
     case ws of
       w : _
-        | Just l <- vWordLen w, asciiMode opts l ->
-              text . show . map (integerToChar . bvVal) <$> traverse (fromVWord "ppWordSeq") ws
+        | Just l <- vWordLen w
+        , asciiMode opts l
+        -> do vs <- traverse (fromVWord "ppWordSeq") ws
+              case traverse wordAsChar vs of
+                Just str -> return $ text str
+                _ -> return $ brackets (fsep (punctuate comma $ map (ppWord opts) vs))
       _ -> do ws' <- traverse loop ws
               return $ brackets (fsep (punctuate comma ws'))
 
@@ -268,14 +287,9 @@ asciiMode opts width = useAscii opts && (width == 7 || width == 8)
 integerToChar :: Integer -> Char
 integerToChar = toEnum . fromInteger
 
---data WithBase a = WithBase PPOpts a
---    deriving (Functor)
 
---instance PP (WithBase Value) where
---  ppPrec _ (WithBase opts v) = ppValue opts v
-
-ppWord :: PPOpts -> BV -> Doc
-ppWord opts (BV width i)
+ppBV :: PPOpts -> BV -> Doc
+ppBV opts (BV width i)
   | base > 36 = integer i -- not sure how to rule this out
   | asciiMode opts width = text (show (toEnum (fromInteger i) :: Char))
   | otherwise = prefix <> text value
@@ -303,7 +317,17 @@ ppWord opts (BV width i)
 
 -- Big-endian Words ------------------------------------------------------------
 
-class BitWord b w where
+class BitWord b w | b -> w, w -> b where
+  ppBit :: b -> Doc
+
+  ppWord :: PPOpts -> w -> Doc
+
+  wordAsChar :: w -> Maybe Char
+
+  wordLen :: w -> Integer
+
+  bitLit :: Bool -> b
+  wordLit :: Integer -> Integer -> w
 
   -- | NOTE this assumes that the sequence of bits is big-endian and finite, so the
   -- first element of the list will be the most significant bit.
@@ -313,6 +337,12 @@ class BitWord b w where
   -- most significant bit is the first element of the list.
   unpackWord :: w -> [b]
 
+class BitWord b w => EvalPrims b w where
+  evalPrim :: Decl -> GenValue b w
+  iteValue :: b
+           -> Eval (GenValue b w)
+           -> Eval (GenValue b w)
+           -> Eval (GenValue b w)
 
 mask :: Integer  -- ^ Bit-width
      -> Integer  -- ^ Value
@@ -322,6 +352,16 @@ mask w i | w >= Arch.maxBigIntWidth = wordTooWide w
 
 
 instance BitWord Bool BV where
+  wordLen (BV w _) = w
+  wordAsChar (BV _ x) = Just $ integerToChar x
+
+  ppBit b | b         = text "True"
+          | otherwise = text "False"
+
+  ppWord = ppBV
+
+  bitLit b = b
+  wordLit = mkBv
 
   packWord bits = BV (toInteger w) a
     where
@@ -420,7 +460,7 @@ fromStr :: Value -> Eval String
 fromStr (VSeq n _ vals) =
   traverse (\x -> toEnum . fromInteger <$> (fromWord "fromStr" =<< x)) (enumerateSeqMap n vals)
 fromStr _ = evalPanic "fromStr" ["Not a finite sequence"]
-  
+
 
 -- | Extract a packed word.
 fromVWord :: BitWord b w => String -> GenValue b w -> Eval w
@@ -429,9 +469,9 @@ fromVWord msg val = case val of
   VSeq n isWord bs | isWord -> packWord <$> traverse (fromVBit<$>) (enumerateSeqMap n bs)
   _                         -> evalPanic "fromVWord" ["not a word", msg]
 
-vWordLen :: Value -> Maybe Integer
+vWordLen :: BitWord b w => GenValue b w -> Maybe Integer
 vWordLen val = case val of
-  VWord (BV n _)           -> Just n
+  VWord w                  -> Just (wordLen w)
   VSeq n isWord _ | isWord -> Just n
   _                        -> Nothing
 

src/Cryptol/ModuleSystem/Env.hs

@@ -18,6 +18,7 @@ import Paths_cryptol (getDataDir)
 #endif
 
 import Cryptol.Eval (EvalEnv)
+import Cryptol.Eval.Value (BV)
 import Cryptol.ModuleSystem.Interface
 import Cryptol.ModuleSystem.Name (Supply,emptySupply)
 import qualified Cryptol.ModuleSystem.NamingEnv as R

src/Cryptol/ModuleSystem/Monad.hs

@@ -10,7 +10,9 @@
 {-# LANGUAGE DeriveGeneric #-}
 module Cryptol.ModuleSystem.Monad where
 
-import           Cryptol.Eval.Env (EvalEnv)
+import           Cryptol.Eval (EvalEnv)
+import           Cryptol.Eval.Value (BV)
+
 import qualified Cryptol.Eval.Monad           as E
 import           Cryptol.ModuleSystem.Env
 import           Cryptol.ModuleSystem.Interface
@@ -29,6 +31,7 @@ import           Cryptol.Parser.Position (Range)
 import           Cryptol.Utils.Ident (interactiveName)
 import           Cryptol.Utils.PP
 
+import Control.Monad.IO.Class
 import Control.Exception (IOException)
 import Data.Function (on)
 import Data.Maybe (isJust)
@@ -278,6 +281,9 @@ instance Monad m => FreshM (ModuleT m) where
        set $! me { meSupply = s' }
        return a
 
+instance MonadIO m => MonadIO (ModuleT m) where
+  liftIO m = lift $ liftIO m
+
 runModuleT :: Monad m
            => ModuleEnv
            -> ModuleT m a

src/Cryptol/Symbolic.hs

@@ -32,7 +32,7 @@ import Cryptol.Symbolic.Value
 
 import qualified Cryptol.Eval.Value as Eval
 import qualified Cryptol.Eval.Type (evalType)
-import qualified Cryptol.Eval.Env (EvalEnv(..))
+import qualified Cryptol.Eval.Env (GenEvalEnv(..))
 import Cryptol.TypeCheck.AST
 import Cryptol.TypeCheck.Solver.InfNat (Nat'(..))
 import Cryptol.Utils.Ident (Ident)
@@ -496,4 +496,4 @@ evalMatch :: Env -> Match -> [Env]
 evalMatch env m = case m of
   From n _ty expr -> [ bindVar (n, v) env | v <- fromSeq (evalExpr env expr) ]
   Let d           -> [ bindVar (evalDecl env d) env ]
--}
+-}