Add SMT Array primitives. (#54)

* Add SMT Array primitives.

* Address comments.

* Add comment.

prelude/Prelude.sawcore

@@ -1507,6 +1507,15 @@ test_fun6 x =
                  #((bitvector 64 -> CompM (bitvector 64)), #()))) ->
       funs.1 x);
 
+--------------------------------------------------------------------------------
+-- SMT Array
+
+primitive Array : sort 0 -> sort 0 -> sort 0;
+
+primitive arrayConstant : (a b : sort 0) -> b -> (Array a b);
+primitive arrayLookup : (a b : sort 0) -> (Array a b) -> a -> b;
+primitive arrayUpdate : (a b : sort 0) -> (Array a b) -> a -> b -> (Array a b);
+
 
 --------------------------------------------------------------------------------
 -- General axioms

src/Verifier/SAW/FiniteValue.hs

@@ -49,6 +49,7 @@ data FirstOrderType
   = FOTBit
   | FOTInt
   | FOTVec Natural FirstOrderType
+  | FOTArray FirstOrderType FirstOrderType
   | FOTTuple [FirstOrderType]
   | FOTRec (Map FieldName FirstOrderType)
   deriving (Eq, Show)
@@ -59,6 +60,7 @@ data FirstOrderValue
   | FOVInt Integer
   | FOVWord Natural Integer -- ^ a more efficient special case for 'FOVVec FOTBit _'.
   | FOVVec FirstOrderType [FirstOrderValue]
+  | FOVArray FirstOrderType FirstOrderType
   | FOVTuple [FirstOrderValue]
   | FOVRec (Map FieldName FirstOrderValue)
   deriving Eq
@@ -90,6 +92,7 @@ instance Show FirstOrderValue where
       FOVInt i    -> shows i
       FOVWord _ x -> shows x
       FOVVec _ vs -> showString "[" . commaSep (map shows vs) . showString "]"
+      FOVArray{}  -> shows $ firstOrderTypeOf fv
       FOVTuple vs -> showString "(" . commaSep (map shows vs) . showString ")"
       FOVRec vm   -> showString "{" . commaSep (map showField (Map.assocs vm)) . showString "}"
     where
@@ -109,6 +112,7 @@ ppFirstOrderValue opts = loop
    FOVInt i      -> integer i
    FOVWord _w i  -> ppNat opts i
    FOVVec _ xs   -> brackets (sep (punctuate comma (map loop xs)))
+   FOVArray{}    -> text $ show $ firstOrderTypeOf fv
    FOVTuple xs   -> parens (sep (punctuate comma (map loop xs)))
    FOVRec xs     -> braces (sep (punctuate comma (map ppField (Map.toList xs))))
       where ppField (f,x) = pretty f <+> char '=' <+> loop x
@@ -158,6 +162,11 @@ firstOrderTypeOf fv =
     FOVInt _    -> FOTInt
     FOVWord n _ -> FOTVec n FOTBit
     FOVVec t vs -> FOTVec (fromIntegral (length vs)) t
+    -- Note: FOVArray contains type information, but not an actual Array value,
+    -- because it is not possible to obtain Array values from SMT solvers. This
+    -- is needed to display a counterexample that includes variables of Array
+    -- type.
+    FOVArray t1 t2 -> FOTArray t1 t2
     FOVTuple vs -> FOTTuple (map firstOrderTypeOf vs)
     FOVRec vm   -> FOTRec (fmap firstOrderTypeOf vm)
 
@@ -194,6 +203,10 @@ asFirstOrderType sc t = do
       -> return FOTInt
     (R.isVecType return -> Just (n R.:*: tp))
       -> FOTVec n <$> asFirstOrderType sc tp
+    (R.asArrayType -> Just (tp1 R.:*: tp2)) -> do
+      tp1' <- asFirstOrderType sc tp1
+      tp2' <- asFirstOrderType sc tp2
+      return $ FOTArray tp1' tp2'
     (R.asTupleType -> Just ts)
       -> FOTTuple <$> traverse (asFirstOrderType sc) ts
     (R.asRecordType -> Just tm)
@@ -227,6 +240,9 @@ scFirstOrderType sc ft =
     FOTVec n t  -> do n' <- scNat sc n
                       t' <- scFirstOrderType sc t
                       scVecType sc n' t'
+    FOTArray t1 t2 -> do t1' <- scFirstOrderType sc t1
+                         t2' <- scFirstOrderType sc t2
+                         scArrayType sc t1' t2'
     FOTTuple ts -> scTupleType sc =<< traverse (scFirstOrderType sc) ts
     FOTRec tm   ->
       scRecordType sc =<< (Map.assocs <$> traverse (scFirstOrderType sc) tm)
@@ -247,6 +263,9 @@ scFirstOrderValue sc fv =
     FOVVec t vs -> do t' <- scFirstOrderType sc t
                       vs' <- traverse (scFirstOrderValue sc) vs
                       scVector sc t' vs'
+    FOVArray t1 t2 -> do t1' <- scFirstOrderType sc t1
+                         t2' <- scFirstOrderType sc t2
+                         scArrayType sc t1' t2'
     FOVTuple vs -> scTuple sc =<< traverse (scFirstOrderValue sc) vs
     FOVRec vm   -> scRecord sc =<< traverse (scFirstOrderValue sc) vm
 

src/Verifier/SAW/Prelude/Constants.hs

@@ -55,3 +55,9 @@ preludeStringIdent =  mkIdent preludeModuleName "String"
 
 preludeStringType :: FlatTermF e
 preludeStringType = GlobalDef preludeStringIdent
+
+preludeArrayIdent :: Ident
+preludeArrayIdent =  mkIdent preludeModuleName "Array"
+
+preludeArrayTypeFun :: FlatTermF e
+preludeArrayTypeFun = GlobalDef preludeArrayIdent

src/Verifier/SAW/Recognizer.hs

@@ -66,6 +66,7 @@ module Verifier.SAW.Recognizer
   , asMux
   , asEq
   , asEqTrue
+  , asArrayType
   ) where
 
 import Control.Applicative
@@ -371,3 +372,6 @@ asEq t =
 
 asEqTrue :: Recognizer Term Term
 asEqTrue = isGlobalDef "Prelude.EqTrue" @> return
+
+asArrayType :: Recognizer Term (Term :*: Term)
+asArrayType = (isGlobalDef "Prelude.Array" @> return) <@> return

src/Verifier/SAW/SharedTerm.hs

@@ -161,6 +161,10 @@ module Verifier.SAW.SharedTerm
   , scIte
   , scSingle
   , scSlice
+  , scArrayType
+  , scArrayConstant
+  , scArrayLookup
+  , scArrayUpdate
   -- *** Integer primitives
   , scIntegerType
   , scIntegerConst
@@ -1560,6 +1564,22 @@ scUpdBvFun :: SharedContext -> Term -> Term
            -> Term -> Term -> Term -> IO Term
 scUpdBvFun sc n a f i v = scGlobalApply sc "Prelude.updBvFun" [n, a, f, i, v]
 
+-- | Array :: sort 0 -> sort 0 -> sort 0
+scArrayType :: SharedContext -> Term -> Term -> IO Term
+scArrayType sc a b = scGlobalApply sc "Prelude.Array" [a, b]
+
+-- arrayConstant :: (a b :: sort 0) -> b -> (Array a b);
+scArrayConstant :: SharedContext -> Term -> Term -> Term -> IO Term
+scArrayConstant sc a b e = scGlobalApply sc "Prelude.arrayConstant" [a, b, e]
+
+-- | arrayLookup :: (a b :: sort 0) -> (Array a b) -> a -> b;
+scArrayLookup :: SharedContext -> Term -> Term -> Term -> Term -> IO Term
+scArrayLookup sc a b f i = scGlobalApply sc "Prelude.arrayLookup" [a, b, f, i]
+
+-- | arrayUpdate :: (a b :: sort 0) -> (Array a b) -> a -> b -> (Array a b);
+scArrayUpdate :: SharedContext -> Term -> Term -> Term -> Term -> Term -> IO Term
+scArrayUpdate sc a b f i e = scGlobalApply sc "Prelude.arrayUpdate" [a, b, f, i, e]
+
 ------------------------------------------------------------
 -- | The default instance of the SharedContext operations.
 mkSharedContext :: IO SharedContext

src/Verifier/SAW/Simulator/Concrete.hs

@@ -64,6 +64,7 @@ type instance EvalM Concrete = Identity
 type instance VBool Concrete = Bool
 type instance VWord Concrete = BitVector
 type instance VInt  Concrete = Integer
+type instance VArray Concrete = ()
 type instance Extra Concrete = CExtra
 
 type CValue = Value Concrete -- (WithM Identity Concrete)
@@ -224,6 +225,11 @@ prims =
   , Prims.bpIntLt  = pure2 (<)
   , Prims.bpIntMin = pure2 min
   , Prims.bpIntMax = pure2 max
+
+    -- Array operations
+  , Prims.bpArrayConstant = unsupportedConcretePrimitive "bpArrayConstant"
+  , Prims.bpArrayLookup = unsupportedConcretePrimitive "bpArrayLookup"
+  , Prims.bpArrayUpdate = unsupportedConcretePrimitive "bpArrayUpdate"
   }
 
 unsupportedConcretePrimitive :: String -> a

src/Verifier/SAW/Simulator/Prims.hs

@@ -118,6 +118,10 @@ data BasePrims l =
   , bpIntLt :: VInt l -> VInt l -> MBool l
   , bpIntMin :: VInt l -> VInt l -> MInt l
   , bpIntMax :: VInt l -> VInt l -> MInt l
+    -- Array operations
+  , bpArrayConstant :: Value l -> Value l -> MArray l
+  , bpArrayLookup :: VArray l -> Value l -> MValue l
+  , bpArrayUpdate :: VArray l -> Value l -> Value l -> MArray l
   }
 
 bpBool :: VMonad l => BasePrims l -> Bool -> MBool l
@@ -247,6 +251,11 @@ constMap bp = Map.fromList
   , ("Prelude.eq", eqOp bp)
   , ("Prelude.ite", iteOp bp)
   , ("Prelude.iteDep", iteOp bp)
+  -- SMT Arrays
+  , ("Prelude.Array", arrayTypeOp)
+  , ("Prelude.arrayConstant", arrayConstantOp bp)
+  , ("Prelude.arrayLookup", arrayLookupOp bp)
+  , ("Prelude.arrayUpdate", arrayUpdateOp bp)
   ]
 
 -- | Call this function to indicate that a programming error has
@@ -329,6 +338,10 @@ vecIdx err v n =
     Just a -> a
     Nothing -> err
 
+toArray :: (VMonad l, Show (Extra l)) => Value l -> MArray l
+toArray (VArray f) = return f
+toArray x = panic $ unwords ["Verifier.SAW.Simulator.toArray", show x]
+
 ------------------------------------------------------------
 -- Standard operator types
 
@@ -1208,3 +1221,39 @@ fixOp =
   constFun $
   strictFun $ \f ->
   force =<< mfix (\x -> delay (apply f x))
+
+------------------------------------------------------------
+-- SMT Array
+
+-- Array :: sort 0 -> sort 0 -> sort 0
+arrayTypeOp :: VMonad l => Value l
+arrayTypeOp = pureFun $ \a -> pureFun $ \b -> VArrayType a b
+
+-- arrayConstant :: (a b :: sort 0) -> b -> (Array a b);
+arrayConstantOp :: VMonad l => BasePrims l -> Value l
+arrayConstantOp bp =
+  pureFun $ \a ->
+  constFun $
+  strictFun $ \e ->
+    VArray <$> (bpArrayConstant bp) a e
+
+-- arrayLookup :: (a b :: sort 0) -> (Array a b) -> a -> b;
+arrayLookupOp :: (VMonad l, Show (Extra l)) => BasePrims l -> Value l
+arrayLookupOp bp =
+  constFun $
+  constFun $
+  pureFun $ \f ->
+  strictFun $ \i -> do
+    f' <- toArray f
+    (bpArrayLookup bp) f' i
+
+-- arrayUpdate :: (a b :: sort 0) -> (Array a b) -> a -> b -> (Array a b);
+arrayUpdateOp :: (VMonad l, Show (Extra l)) => BasePrims l -> Value l
+arrayUpdateOp bp =
+  constFun $
+  constFun $
+  pureFun $ \f ->
+  pureFun $ \i ->
+  strictFun $ \e -> do
+    f' <- toArray f
+    VArray <$> (bpArrayUpdate bp) f' i e

src/Verifier/SAW/Simulator/RME.hs

@@ -73,6 +73,7 @@ type instance EvalM ReedMuller = Identity
 type instance VBool ReedMuller = RME
 type instance VWord ReedMuller = Vector RME
 type instance VInt  ReedMuller = Integer
+type instance VArray ReedMuller = ()
 type instance Extra ReedMuller = RExtra
 
 type RValue = Value ReedMuller
@@ -212,6 +213,10 @@ prims =
   , Prims.bpIntLt  = pure2 (\x y -> RME.constant (x < y))
   , Prims.bpIntMin = unsupportedRMEPrimitive "bpIntMin"
   , Prims.bpIntMax = unsupportedRMEPrimitive "bpIntMax"
+    -- Array operations
+  , Prims.bpArrayConstant = unsupportedRMEPrimitive "bpArrayConstant"
+  , Prims.bpArrayLookup = unsupportedRMEPrimitive "bpArrayLookup"
+  , Prims.bpArrayUpdate = unsupportedRMEPrimitive "bpArrayUpdate"
   }
 
 unsupportedRMEPrimitive :: String -> a

src/Verifier/SAW/Simulator/Value.hs

@@ -58,6 +58,8 @@ data Value l
   | VNat !Integer
   | VInt (VInt l)
   | VIntType
+  | VArray (VArray l)
+  | VArrayType (Value l) (Value l)
   | VString !String
   | VFloat !Float
   | VDouble !Double
@@ -80,6 +82,8 @@ type family VBool l :: Type
 type family VWord l :: Type
 -- | Integers for value instantiation 'l'
 type family VInt  l :: Type
+-- | SMT arrays for value instantiation 'l'
+type family VArray l :: Type
 -- | Additional constructors for instantiation 'l'
 type family Extra l :: Type
 
@@ -95,6 +99,9 @@ type MWord l      = EvalM l (VWord l)
 -- | Short-hand for a monadic integer.
 type MInt l       = EvalM l (VInt  l)
 
+-- | Short-hand for a monadic array.
+type MArray l     = EvalM l (VArray l)
+
 -- | Short hand to specify that the evaluation monad is a monad (very common)
 type VMonad l     = Monad (EvalM l)
 
@@ -110,6 +117,7 @@ type instance EvalM (WithM m l) = m
 type instance VBool (WithM m l) = VBool l
 type instance VWord (WithM m l) = VWord l
 type instance VInt  (WithM m l) = VInt l
+type instance VArray (WithM m l) = VArray l
 type instance Extra (WithM m l) = Extra l
 
 --------------------------------------------------------------------------------
@@ -140,6 +148,8 @@ instance Show (Extra l) => Show (Value l) where
       VNat n         -> shows n
       VInt _         -> showString "<<integer>>"
       VIntType       -> showString "Integer"
+      VArray{}       -> showString "<<array>>"
+      VArrayType{}   -> showString "Array"
       VFloat float   -> shows float
       VDouble double -> shows double
       VString s      -> shows s