Add support for arrayCopy, arraySet, and arrayRangeEqual primitives.

cryptol-saw-core/saw/Cryptol.sawcore

@@ -1741,6 +1741,15 @@ ecArrayLookup = arrayLookup;
 ecArrayUpdate : (a b : sort 0) -> (Array a b) -> a -> b -> (Array a b);
 ecArrayUpdate = arrayUpdate;
 
+ecArrayCopy : (n : Num) -> (a : sort 0) -> Array (seq n Bool) a -> seq n Bool -> Array (seq n Bool) a -> seq n Bool -> seq n Bool -> Array (seq n Bool) a;
+ecArrayCopy = finNumRec (\(n : Num) -> (a : sort 0) -> Array (seq n Bool) a -> seq n Bool -> Array (seq n Bool) a -> seq n Bool -> seq n Bool -> Array (seq n Bool) a) arrayCopy;
+
+ecArraySet : (n : Num) -> (a : sort 0) -> Array (seq n Bool) a -> seq n Bool -> a -> seq n Bool -> Array (seq n Bool) a;
+ecArraySet = finNumRec (\(n : Num) -> (a : sort 0) -> Array (seq n Bool) a -> seq n Bool -> a -> seq n Bool -> Array (seq n Bool) a) arraySet;
+
+ecArrayRangeEq : (n : Num) -> (a : sort 0) -> Array (seq n Bool) a -> seq n Bool -> Array (seq n Bool) a -> seq n Bool -> seq n Bool -> Bool;
+ecArrayRangeEq = finNumRec (\(n : Num) -> (a : sort 0) -> Array (seq n Bool) a -> seq n Bool -> Array (seq n Bool) a -> seq n Bool -> seq n Bool -> Bool) arrayRangeEq;
+
 --------------------------------------------------------------------------------
 -- Suite-B Primitives
 

cryptol-saw-core/src/Verifier/SAW/Cryptol.hs

@@ -809,6 +809,9 @@ arrayPrims =
   [ ("arrayConstant", flip scGlobalDef "Cryptol.ecArrayConstant") -- {a,b} b -> Array a b
   , ("arrayLookup",   flip scGlobalDef "Cryptol.ecArrayLookup") -- {a,b} Array a b -> a -> b
   , ("arrayUpdate",   flip scGlobalDef "Cryptol.ecArrayUpdate") -- {a,b} Array a b -> a -> b -> Array a b
+  , ("arrayCopy", flip scGlobalDef "Cryptol.ecArrayCopy") -- {n,a} Array [n] a -> [n] -> Array [n] a -> [n] -> [n] -> Array [n] a
+  , ("arraySet", flip scGlobalDef "Cryptol.ecArraySet") -- {n,a} Array [n] a -> [n] -> a -> [n] -> Array [n] a
+  , ("arrayRangeEqual", flip scGlobalDef "Cryptol.ecArrayRangeEq") -- {n,a} Array [n] a -> [n] -> Array [n] a -> [n] -> [n] -> Bit
   ]
 
 floatPrims :: Map C.PrimIdent (SharedContext -> IO Term)

saw-core-aig/src/Verifier/SAW/Simulator/BitBlast.hs

@@ -184,6 +184,7 @@ prims be =
   , Prims.bpMuxBool  = \b x y -> AIG.lazyMux be b (pure x) (pure y)
   , Prims.bpMuxWord  = \b x y -> AIG.iteM be b (pure x) (pure y)
   , Prims.bpMuxInt   = muxInt
+  , Prims.bpMuxArray = unsupportedAIGPrimitive "bpMuxArray"
   , Prims.bpMuxExtra = muxBExtra be
     -- Booleans
   , Prims.bpTrue   = AIG.trueLit be
@@ -252,6 +253,9 @@ prims be =
   , Prims.bpArrayLookup = unsupportedAIGPrimitive "bpArrayLookup"
   , Prims.bpArrayUpdate = unsupportedAIGPrimitive "bpArrayUpdate"
   , Prims.bpArrayEq = unsupportedAIGPrimitive "bpArrayEq"
+  , Prims.bpArrayCopy = unsupportedAIGPrimitive "bpArrayCopy"
+  , Prims.bpArraySet = unsupportedAIGPrimitive "bpArraySet"
+  , Prims.bpArrayRangeEq = unsupportedAIGPrimitive "bpArrayRangeEq"
   }
 
 unsupportedAIGPrimitive :: String -> a

saw-core-sbv/src/Verifier/SAW/Simulator/SBV.hs

@@ -118,6 +118,7 @@ prims =
   , Prims.bpMuxBool  = pure3 svIte
   , Prims.bpMuxWord  = pure3 svIte
   , Prims.bpMuxInt   = pure3 svIte
+  , Prims.bpMuxArray = unsupportedSBVPrimitive "bpMuxArray"
   , Prims.bpMuxExtra = muxSbvExtra
     -- Booleans
   , Prims.bpTrue   = svTrue
@@ -184,6 +185,9 @@ prims =
   , Prims.bpArrayLookup = unsupportedSBVPrimitive "bpArrayLookup"
   , Prims.bpArrayUpdate = unsupportedSBVPrimitive "bpArrayUpdate"
   , Prims.bpArrayEq = unsupportedSBVPrimitive "bpArrayEq"
+  , Prims.bpArrayCopy = unsupportedSBVPrimitive "bpArrayCopy"
+  , Prims.bpArraySet = unsupportedSBVPrimitive "bpArraySet"
+  , Prims.bpArrayRangeEq = unsupportedSBVPrimitive "bpArrayRangeEq"
   }
 
 unsupportedSBVPrimitive :: String -> a

saw-core-what4/src/Verifier/SAW/Simulator/What4.hs

@@ -175,6 +175,7 @@ prims sym =
   , Prims.bpMuxBool  = W.itePred sym
   , Prims.bpMuxWord  = SW.bvIte  sym
   , Prims.bpMuxInt   = W.intIte  sym
+  , Prims.bpMuxArray = arrayIte sym
   , Prims.bpMuxExtra = muxWhat4Extra sym
     -- Booleans
   , Prims.bpTrue   = W.truePred  sym
@@ -241,6 +242,9 @@ prims sym =
   , Prims.bpArrayLookup = arrayLookup sym
   , Prims.bpArrayUpdate = arrayUpdate sym
   , Prims.bpArrayEq = arrayEq sym
+  , Prims.bpArrayCopy = arrayCopy sym
+  , Prims.bpArraySet = arraySet sym
+  , Prims.bpArrayRangeEq = arrayRangeEq sym
   }
 
 
@@ -647,6 +651,75 @@ arrayUpdate sym arr idx elm
   | otherwise =
     panic "Verifier.SAW.Simulator.What4.Panic.arrayUpdate" ["argument type mismatch"]
 
+arrayCopy ::
+  W.IsSymExprBuilder sym =>
+  sym ->
+  SArray sym ->
+  SWord sym ->
+  SArray sym ->
+  SWord sym ->
+  SWord sym ->
+  IO (SArray sym)
+arrayCopy sym dest_arr dest_idx src_arr src_idx len
+  | SArray dest_arr_expr <- dest_arr
+  , DBV dest_idx_expr <- dest_idx
+  , SArray src_arr_expr <- src_arr
+  , DBV src_idx_expr <- src_idx
+  , DBV len_expr <- len
+  , W.BaseArrayRepr (Ctx.Empty Ctx.:> idx_repr) _ <- W.exprType dest_arr_expr
+  , Just Refl <- testEquality (W.exprType dest_arr_expr) (W.exprType src_arr_expr)
+  , Just Refl <- testEquality idx_repr (W.exprType dest_idx_expr)
+  , Just Refl <- testEquality idx_repr (W.exprType src_idx_expr)
+  , Just Refl <- testEquality idx_repr (W.exprType len_expr) =
+    SArray <$> W.arrayCopy sym dest_arr_expr dest_idx_expr src_arr_expr src_idx_expr len_expr
+  | otherwise =
+    panic "Verifier.SAW.Simulator.What4.Panic.arrayCopy" ["argument type mismatch"]
+
+arraySet ::
+  W.IsSymExprBuilder sym =>
+  sym ->
+  SArray sym ->
+  SWord sym ->
+  SValue sym ->
+  SWord sym ->
+  IO (SArray sym)
+arraySet sym arr idx elm len
+  | SArray arr_expr <- arr
+  , DBV idx_expr <- idx
+  , Just (Some elm_expr) <- valueToSymExpr elm
+  , DBV len_expr <- len
+  , W.BaseArrayRepr (Ctx.Empty Ctx.:> idx_repr) elm_repr <- W.exprType arr_expr
+  , Just Refl <- testEquality idx_repr (W.exprType idx_expr)
+  , Just Refl <- testEquality idx_repr (W.exprType len_expr)
+  , Just Refl <- testEquality elm_repr (W.exprType elm_expr) =
+    SArray <$> W.arraySet sym arr_expr idx_expr elm_expr len_expr
+  | otherwise =
+    panic "Verifier.SAW.Simulator.What4.Panic.arraySet" ["argument type mismatch"]
+
+arrayRangeEq ::
+  W.IsSymExprBuilder sym =>
+  sym ->
+  SArray sym ->
+  SWord sym ->
+  SArray sym ->
+  SWord sym ->
+  SWord sym ->
+  IO (SBool sym)
+arrayRangeEq sym x_arr x_idx y_arr y_idx len
+  | SArray x_arr_expr <- x_arr
+  , DBV x_idx_expr <- x_idx
+  , SArray y_arr_expr <- y_arr
+  , DBV y_idx_expr <- y_idx
+  , DBV len_expr <- len
+  , W.BaseArrayRepr (Ctx.Empty Ctx.:> idx_repr) _ <- W.exprType x_arr_expr
+  , Just Refl <- testEquality (W.exprType x_arr_expr) (W.exprType y_arr_expr)
+  , Just Refl <- testEquality idx_repr (W.exprType x_idx_expr)
+  , Just Refl <- testEquality idx_repr (W.exprType y_idx_expr)
+  , Just Refl <- testEquality idx_repr (W.exprType len_expr) =
+    W.arrayRangeEq sym x_arr_expr x_idx_expr y_arr_expr y_idx_expr len_expr
+  | otherwise =
+    panic "Verifier.SAW.Simulator.What4.Panic.arrayRangeEq" ["argument type mismatch"]
+
 arrayEq ::
   W.IsSymExprBuilder sym =>
   sym ->
@@ -664,6 +737,24 @@ arrayEq sym lhs_arr rhs_arr
   | otherwise =
     panic "Verifier.SAW.Simulator.What4.Panic.arrayEq" ["argument type mismatch"]
 
+arrayIte ::
+  W.IsSymExprBuilder sym =>
+  sym ->
+  W.Pred sym ->
+  SArray sym ->
+  SArray sym ->
+  IO (SArray sym)
+arrayIte sym cond lhs_arr rhs_arr
+  | SArray lhs_arr_expr <- lhs_arr
+  , SArray rhs_arr_expr <- rhs_arr
+  , W.BaseArrayRepr (Ctx.Empty Ctx.:> lhs_idx_repr) lhs_elm_repr <- W.exprType lhs_arr_expr
+  , W.BaseArrayRepr (Ctx.Empty Ctx.:> rhs_idx_repr) rhs_elm_repr <- W.exprType rhs_arr_expr
+  , Just Refl <- testEquality lhs_idx_repr rhs_idx_repr
+  , Just Refl <- testEquality lhs_elm_repr rhs_elm_repr =
+    SArray <$> W.arrayIte sym cond lhs_arr_expr rhs_arr_expr
+  | otherwise =
+    panic "Verifier.SAW.Simulator.What4.Panic.arrayIte" ["argument type mismatch"]
+
 ----------------------------------------------------------------------
 -- | A basic symbolic simulator/evaluator: interprets a saw-core Term as
 -- a symbolic value
@@ -1391,6 +1482,7 @@ mkArgTerm sc ty val =
     (VIntType, VInt _)   -> return ArgTermVar
     (_, VWord ZBV)       -> return ArgTermBVZero     -- 0-width bitvector is a constant
     (_, VWord (DBV _))   -> return ArgTermVar
+    (_, VArray{})        -> return ArgTermVar
     (VUnitType, VUnit)   -> return ArgTermUnit
     (VIntModType n, VIntMod _ _) -> pure (ArgTermToIntMod n ArgTermVar)
 

saw-core-what4/src/Verifier/SAW/Simulator/What4/ReturnTrip.hs

@@ -367,6 +367,15 @@ scEq sym sc tp x y =
     BaseBoolRepr    -> scBoolEq sc x y
     BaseRealRepr    -> scRealEq sym sc x y
     BaseIntegerRepr -> scIntEq sc x y
+    BaseArrayRepr idxTypes range
+      | Ctx.Empty Ctx.:> idx_type <- idxTypes ->
+        do let SAWExpr x' = x
+           let SAWExpr y' = y
+           sc_idx_type <- baseSCType sym sc idx_type
+           sc_elm_type <- baseSCType sym sc range
+           SAWExpr <$> SC.scArrayEq sc sc_idx_type sc_elm_type x' y'
+      | otherwise ->
+        unsupported sym ("SAW backend: equality comparison on unsupported multidimensional array type:" ++ show tp)
     BaseBVRepr w    ->
       do let SAWExpr x' = x
          let SAWExpr y' = y
@@ -797,6 +806,35 @@ evaluateExpr sym st sc cache = f []
                SAWExpr <$> SC.scArrayUpdate sc sc_idx_type sc_elm_type sc_arr sc_idx sc_elm
           | otherwise -> unimplemented "multidimensional UpdateArray"
 
+        B.CopyArray w a_repr dest_arr dest_idx src_arr src_idx len _dest_end_idx _src_end_idx ->
+          do sc_w <- SC.scNat sc (natValue w)
+             sc_a <- baseSCType sym sc a_repr
+             sc_dest_arr <- f env dest_arr
+             sc_dest_idx <- f env dest_idx
+             sc_src_arr <- f env src_arr
+             sc_src_idx <- f env src_idx
+             sc_len <- f env len
+             SAWExpr <$> SC.scArrayCopy sc sc_w sc_a sc_dest_arr sc_dest_idx sc_src_arr sc_src_idx sc_len
+
+        B.SetArray w a_repr arr idx val len _end_idx ->
+          do sc_w <- SC.scNat sc (natValue w)
+             sc_a <- baseSCType sym sc a_repr
+             sc_arr <- f env arr
+             sc_idx <- f env idx
+             sc_val <- f env val
+             sc_len <- f env len
+             SAWExpr <$> SC.scArraySet sc sc_w sc_a sc_arr sc_idx sc_val sc_len
+
+        B.EqualArrayRange w a_repr x_arr x_idx y_arr y_idx len _x_end_idx _y_end_idx ->
+          do sc_w <- SC.scNat sc (natValue w)
+             sc_a <- baseSCType sym sc a_repr
+             sc_x_arr <- f env x_arr
+             sc_x_idx <- f env x_idx
+             sc_y_arr <- f env y_arr
+             sc_y_idx <- f env y_idx
+             sc_len <- f env len
+             SAWExpr <$> SC.scArrayRangeEq sc sc_w sc_a sc_x_arr sc_x_idx sc_y_arr sc_y_idx sc_len
+
         B.IntDiv x y ->
           do x' <- f env x
              y' <- f env y

saw-core/prelude/Prelude.sawcore

@@ -2241,6 +2241,9 @@ 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);
+primitive arrayCopy : (n : Nat) -> (a : sort 0) -> Array (Vec n Bool) a -> Vec n Bool -> Array (Vec n Bool) a -> Vec n Bool -> Vec n Bool -> Array (Vec n Bool) a;
+primitive arraySet : (n : Nat) -> (a : sort 0) -> Array (Vec n Bool) a -> Vec n Bool -> a -> Vec n Bool -> Array (Vec n Bool) a;
+primitive arrayRangeEq : (n : Nat) -> (a : sort 0) -> Array (Vec n Bool) a -> Vec n Bool -> Array (Vec n Bool) a -> Vec n Bool -> Vec n Bool -> Bool;
 primitive arrayEq     : (a b : sort 0) -> (Array a b) -> (Array a b) -> Bool;
 
 --------------------------------------------------------------------------------

saw-core/src/Verifier/SAW/Rewriter.hs

@@ -290,6 +290,9 @@ boolEqIdent = mkIdent (mkModuleName ["Prelude"]) "boolEq"
 vecEqIdent :: Ident
 vecEqIdent = mkIdent (mkModuleName ["Prelude"]) "vecEq"
 
+arrayEqIdent :: Ident
+arrayEqIdent = mkIdent (mkModuleName ["Prelude"]) "arrayEq"
+
 equalNatIdent :: Ident
 equalNatIdent = mkIdent (mkModuleName ["Prelude"]) "equalNat"
 
@@ -345,6 +348,8 @@ ruleOfProp (R.asApplyAll -> (R.isGlobalDef boolEqIdent -> Just (), [x, y])) ann
   Just $ mkRewriteRule [] x y ann
 ruleOfProp (R.asApplyAll -> (R.isGlobalDef vecEqIdent -> Just (), [_, _, _, x, y])) ann =
   Just $ mkRewriteRule [] x y ann
+ruleOfProp (R.asApplyAll -> (R.isGlobalDef arrayEqIdent -> Just (), [_, _, x, y])) ann =
+  Just $ mkRewriteRule [] x y ann
 ruleOfProp (unwrapTermF -> Constant _ body) ann = ruleOfProp body ann
 ruleOfProp (R.asEq -> Just (_, x, y)) ann =
   Just $ mkRewriteRule [] x y ann

saw-core/src/Verifier/SAW/SharedTerm.hs

@@ -231,6 +231,9 @@ module Verifier.SAW.SharedTerm
   , scArrayLookup
   , scArrayUpdate
   , scArrayEq
+  , scArrayCopy
+  , scArraySet
+  , scArrayRangeEq
     -- ** Utilities
 --  , scTrue
 --  , scFalse
@@ -2230,7 +2233,7 @@ scArrayConstant sc a b e = scGlobalApply sc "Prelude.arrayConstant" [a, b, e]
 scArrayLookup :: SharedContext -> Term -> Term -> Term -> Term -> IO Term
 scArrayLookup sc a b f i = scGlobalApply sc "Prelude.arrayLookup" [a, b, f, i]
 
--- Create a term computing an array updated at a particular index.
+-- | Create a term computing an array updated at a particular index.
 --
 -- > arrayUpdate : (a b : sort 0) -> (Array a b) -> a -> b -> (Array a b);
 scArrayUpdate :: SharedContext -> Term -> Term -> Term -> Term -> Term -> IO Term
@@ -2242,6 +2245,18 @@ scArrayUpdate sc a b f i e = scGlobalApply sc "Prelude.arrayUpdate" [a, b, f, i,
 scArrayEq :: SharedContext -> Term -> Term -> Term -> Term -> IO Term
 scArrayEq sc a b x y = scGlobalApply sc "Prelude.arrayEq" [a, b, x, y]
 
+-- > arrayCopy : (n : Nat) -> (a : sort 0) -> Array (Vec n Bool) a -> Vec n Bool -> Array (Vec n Bool) a -> Vec n Bool -> Vec n Bool -> Array (Vec n Bool) a;
+scArrayCopy :: SharedContext -> Term -> Term -> Term -> Term -> Term -> Term -> Term -> IO Term
+scArrayCopy sc n a f i g j l = scGlobalApply sc "Prelude.arrayCopy" [n, a, f, i, g, j, l]
+
+-- > arraySet : (n : Nat) -> (a : sort 0) -> Array (Vec n Bool) a -> Vec n Bool -> a -> Vec n Bool -> Array (Vec n Bool) a;
+scArraySet :: SharedContext -> Term -> Term -> Term -> Term -> Term -> Term -> IO Term
+scArraySet sc n a f i e l = scGlobalApply sc "Prelude.arraySet" [n, a, f, i, e, l]
+
+-- > arrayRangeEq : (n : Nat) -> (a : sort 0) -> Array (Vec n Bool) a -> Vec n Bool -> Array (Vec n Bool) a -> Vec n Bool -> Vec n Bool -> Bool;
+scArrayRangeEq :: SharedContext -> Term -> Term -> Term -> Term -> Term -> Term -> Term -> IO Term
+scArrayRangeEq sc n a f i g j l = scGlobalApply sc "Prelude.arrayRangeEq" [n, a, f, i, g, j, l]
+
 ------------------------------------------------------------
 -- | The default instance of the SharedContext operations.
 mkSharedContext :: IO SharedContext

saw-core/src/Verifier/SAW/Simulator/Concrete.hs

@@ -145,6 +145,7 @@ prims =
   , Prims.bpMuxBool  = pure3 ite
   , Prims.bpMuxWord  = pure3 ite
   , Prims.bpMuxInt   = pure3 ite
+  , Prims.bpMuxArray = unsupportedConcretePrimitive "bpMuxArray"
   , Prims.bpMuxExtra = \_tp -> pure3 ite
     -- Booleans
   , Prims.bpTrue   = True
@@ -213,6 +214,9 @@ prims =
   , Prims.bpArrayLookup = unsupportedConcretePrimitive "bpArrayLookup"
   , Prims.bpArrayUpdate = unsupportedConcretePrimitive "bpArrayUpdate"
   , Prims.bpArrayEq = unsupportedConcretePrimitive "bpArrayEq"
+  , Prims.bpArrayCopy = unsupportedConcretePrimitive "bpArrayCopy"
+  , Prims.bpArraySet = unsupportedConcretePrimitive "bpArraySet"
+  , Prims.bpArrayRangeEq = unsupportedConcretePrimitive "bpArrayRangeEq"
   }
 
 unsupportedConcretePrimitive :: String -> a