From 858afd644edfd60680aa122e7b3bf255cd5dd043 Mon Sep 17 00:00:00 2001 From: Andrei Stefanescu Date: Wed, 7 Jul 2021 16:01:39 +0000 Subject: [PATCH] Add support for arrayCopy, arraySet, and arrayRangeEqual primitives. --- cryptol-saw-core/saw/Cryptol.sawcore | 9 ++ cryptol-saw-core/src/Verifier/SAW/Cryptol.hs | 3 + .../src/Verifier/SAW/Simulator/BitBlast.hs | 4 + .../src/Verifier/SAW/Simulator/SBV.hs | 4 + .../src/Verifier/SAW/Simulator/What4.hs | 92 +++++++++++++++++++ .../SAW/Simulator/What4/ReturnTrip.hs | 38 ++++++++ saw-core/prelude/Prelude.sawcore | 3 + saw-core/src/Verifier/SAW/Rewriter.hs | 5 + saw-core/src/Verifier/SAW/SharedTerm.hs | 17 +++- .../src/Verifier/SAW/Simulator/Concrete.hs | 4 + saw-core/src/Verifier/SAW/Simulator/Prims.hs | 57 ++++++++++++ saw-core/src/Verifier/SAW/Simulator/RME.hs | 4 + .../src/Verifier/SAW/Simulator/TermModel.hs | 34 +++++++ 13 files changed, 273 insertions(+), 1 deletion(-) diff --git a/cryptol-saw-core/saw/Cryptol.sawcore b/cryptol-saw-core/saw/Cryptol.sawcore index 8b5401f6f8..883ac8ad51 100644 --- a/cryptol-saw-core/saw/Cryptol.sawcore +++ b/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 diff --git a/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs b/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs index 64e8fc8f4f..d8624b1fc6 100644 --- a/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs +++ b/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) diff --git a/saw-core-aig/src/Verifier/SAW/Simulator/BitBlast.hs b/saw-core-aig/src/Verifier/SAW/Simulator/BitBlast.hs index 4052b21c2d..7850d9d1ae 100644 --- a/saw-core-aig/src/Verifier/SAW/Simulator/BitBlast.hs +++ b/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 diff --git a/saw-core-sbv/src/Verifier/SAW/Simulator/SBV.hs b/saw-core-sbv/src/Verifier/SAW/Simulator/SBV.hs index 2ac7ace229..db209362ca 100644 --- a/saw-core-sbv/src/Verifier/SAW/Simulator/SBV.hs +++ b/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 diff --git a/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs b/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs index a73abb5867..cd58c24f62 100644 --- a/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs +++ b/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) diff --git a/saw-core-what4/src/Verifier/SAW/Simulator/What4/ReturnTrip.hs b/saw-core-what4/src/Verifier/SAW/Simulator/What4/ReturnTrip.hs index fa3d74e2ba..dab564682b 100644 --- a/saw-core-what4/src/Verifier/SAW/Simulator/What4/ReturnTrip.hs +++ b/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 diff --git a/saw-core/prelude/Prelude.sawcore b/saw-core/prelude/Prelude.sawcore index 82ddf83936..73127d79e2 100644 --- a/saw-core/prelude/Prelude.sawcore +++ b/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; -------------------------------------------------------------------------------- diff --git a/saw-core/src/Verifier/SAW/Rewriter.hs b/saw-core/src/Verifier/SAW/Rewriter.hs index 563ac409a5..f8d4a5ab32 100644 --- a/saw-core/src/Verifier/SAW/Rewriter.hs +++ b/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 diff --git a/saw-core/src/Verifier/SAW/SharedTerm.hs b/saw-core/src/Verifier/SAW/SharedTerm.hs index ca32959f5d..f39ef02f12 100644 --- a/saw-core/src/Verifier/SAW/SharedTerm.hs +++ b/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 diff --git a/saw-core/src/Verifier/SAW/Simulator/Concrete.hs b/saw-core/src/Verifier/SAW/Simulator/Concrete.hs index 8d7cc572f0..0aa577dc56 100644 --- a/saw-core/src/Verifier/SAW/Simulator/Concrete.hs +++ b/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 diff --git a/saw-core/src/Verifier/SAW/Simulator/Prims.hs b/saw-core/src/Verifier/SAW/Simulator/Prims.hs index dfad8e5da1..87d8ea915b 100644 --- a/saw-core/src/Verifier/SAW/Simulator/Prims.hs +++ b/saw-core/src/Verifier/SAW/Simulator/Prims.hs @@ -184,6 +184,7 @@ data BasePrims l = , bpMuxBool :: VBool l -> VBool l -> VBool l -> MBool l , bpMuxWord :: VBool l -> VWord l -> VWord l -> MWord l , bpMuxInt :: VBool l -> VInt l -> VInt l -> MInt l + , bpMuxArray :: VBool l -> VArray l -> VArray l -> MArray l , bpMuxExtra :: TValue l -> VBool l -> Extra l -> Extra l -> EvalM l (Extra l) -- Booleans , bpTrue :: VBool l @@ -250,6 +251,9 @@ data BasePrims l = , bpArrayLookup :: VArray l -> Value l -> MValue l , bpArrayUpdate :: VArray l -> Value l -> Value l -> MArray l , bpArrayEq :: VArray l -> VArray l -> MBool l + , bpArrayCopy :: VArray l -> VWord l -> VArray l -> VWord l -> VWord l -> MArray l + , bpArraySet :: VArray l -> VWord l -> Value l -> VWord l -> MArray l + , bpArrayRangeEq :: VArray l -> VWord l -> VArray l -> VWord l -> VWord l -> MBool l } bpBool :: VMonad l => BasePrims l -> Bool -> MBool l @@ -374,6 +378,9 @@ constMap bp = Map.fromList , ("Prelude.arrayLookup", arrayLookupOp bp) , ("Prelude.arrayUpdate", arrayUpdateOp bp) , ("Prelude.arrayEq", arrayEqOp bp) + , ("Prelude.arrayCopy", arrayCopyOp bp) + , ("Prelude.arraySet", arraySetOp bp) + , ("Prelude.arrayRangeEq", arrayRangeEqOp bp) ] -- | Call this function to indicate that a programming error has @@ -1180,6 +1187,7 @@ muxValue bp tp0 b = value tp0 value _ (VBool x) (VBool y) = VBool <$> bpMuxBool bp b x y value _ (VWord x) (VWord y) = VWord <$> bpMuxWord bp b x y value _ (VInt x) (VInt y) = VInt <$> bpMuxInt bp b x y + value _ (VArray x) (VArray y) = VArray <$> bpMuxArray bp b x y value _ (VIntMod n x) (VIntMod _ y) = VIntMod n <$> bpMuxInt bp b x y value tp x@(VWord _) y = do xv <- toVector' x @@ -1305,3 +1313,52 @@ arrayEqOp bp = do x' <- toArray x y' <- toArray y VBool <$> bpArrayEq bp 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; +arrayCopyOp :: (VMonad l, Show (Extra l)) => BasePrims l -> Prim l +arrayCopyOp bp = + constFun $ + constFun $ + strictFun $ \f -> + strictFun $ \i -> + strictFun $ \g -> + strictFun $ \j -> + strictFun $ \l -> Prim $ + do f' <- toArray f + i' <- toWord (bpPack bp) i + g' <- toArray g + j' <- toWord (bpPack bp) j + l' <- toWord (bpPack bp) l + VArray <$> (bpArrayCopy bp) 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; +arraySetOp :: (VMonad l, Show (Extra l)) => BasePrims l -> Prim l +arraySetOp bp = + constFun $ + constFun $ + strictFun $ \f -> + strictFun $ \i -> + strictFun $ \e -> + strictFun $ \l -> Prim $ + do f' <- toArray f + i' <- toWord (bpPack bp) i + l' <- toWord (bpPack bp) l + VArray <$> (bpArraySet bp) 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; +arrayRangeEqOp :: (VMonad l, Show (Extra l)) => BasePrims l -> Prim l +arrayRangeEqOp bp = + constFun $ + constFun $ + strictFun $ \f -> + strictFun $ \i -> + strictFun $ \g -> + strictFun $ \j -> + strictFun $ \l -> Prim $ + do f' <- toArray f + i' <- toWord (bpPack bp) i + g' <- toArray g + j' <- toWord (bpPack bp) j + l' <- toWord (bpPack bp) l + VBool <$> (bpArrayRangeEq bp) f' i' g' j' l' + diff --git a/saw-core/src/Verifier/SAW/Simulator/RME.hs b/saw-core/src/Verifier/SAW/Simulator/RME.hs index f026be38a0..77ba4e2d88 100644 --- a/saw-core/src/Verifier/SAW/Simulator/RME.hs +++ b/saw-core/src/Verifier/SAW/Simulator/RME.hs @@ -166,6 +166,7 @@ prims = , Prims.bpMuxBool = pure3 RME.mux , Prims.bpMuxWord = pure3 muxRMEV , Prims.bpMuxInt = pure3 muxInt + , Prims.bpMuxArray = unsupportedRMEPrimitive "bpMuxArray" , Prims.bpMuxExtra = \tp -> pure3 (muxExtra tp) -- Booleans , Prims.bpTrue = RME.true @@ -232,6 +233,9 @@ prims = , Prims.bpArrayLookup = unsupportedRMEPrimitive "bpArrayLookup" , Prims.bpArrayUpdate = unsupportedRMEPrimitive "bpArrayUpdate" , Prims.bpArrayEq = unsupportedRMEPrimitive "bpArrayEq" + , Prims.bpArrayCopy = unsupportedRMEPrimitive "bpArrayCopy" + , Prims.bpArraySet = unsupportedRMEPrimitive "bpArraySet" + , Prims.bpArrayRangeEq = unsupportedRMEPrimitive "bpArrayRangeEq" } unsupportedRMEPrimitive :: String -> a diff --git a/saw-core/src/Verifier/SAW/Simulator/TermModel.hs b/saw-core/src/Verifier/SAW/Simulator/TermModel.hs index d6bbc03fb9..c92fe468fe 100644 --- a/saw-core/src/Verifier/SAW/Simulator/TermModel.hs +++ b/saw-core/src/Verifier/SAW/Simulator/TermModel.hs @@ -668,6 +668,14 @@ prims sc cfg = a <- scIntegerType sc Left <$> scIte sc a tm x' y' + , Prims.bpMuxArray = \c x@(TMArray a a' b b' arr1) y@(TMArray _ _ _ _ arr2) -> + case c of + Right bb -> if bb then pure x else pure y + Left tm -> + do t <- scArrayType sc a' b' + arr' <- scIte sc t tm arr1 arr2 + return $ TMArray a a' b b' arr' + , Prims.bpMuxExtra = \tp c x y -> case c of Right b -> if b then pure x else pure y @@ -868,6 +876,32 @@ prims sc cfg = pure (Right True) else Left <$> scArrayEq sc a' b' arr1 arr2 + + , Prims.bpArrayCopy = \(TMArray a a' b b' arr1) idx1 (TMArray _ _ _ _ arr2) idx2 len -> + do let n = wordWidth idx1 + n' <- scNat sc n + idx1' <- wordTerm sc idx1 + idx2' <- wordTerm sc idx2 + len' <- wordTerm sc len + arr' <- scArrayCopy sc n' b' arr1 idx1' arr2 idx2' len' + pure (TMArray a a' b b' arr') + + , Prims.bpArraySet = \(TMArray a a' b b' arr) idx val len -> + do let n = wordWidth idx + n' <- scNat sc n + idx' <- wordTerm sc idx + val' <- readBackValue sc cfg b val + len' <- wordTerm sc len + arr' <- scArraySet sc n' b' arr idx' val' len' + pure (TMArray a a' b b' arr') + + , Prims.bpArrayRangeEq = \(TMArray _ _ _ b' arr1) idx1 (TMArray _ _ _ _ arr2) idx2 len -> + do let n = wordWidth idx1 + n' <- scNat sc n + idx1' <- wordTerm sc idx1 + idx2' <- wordTerm sc idx2 + len' <- wordTerm sc len + Left <$> scArrayRangeEq sc n' b' arr1 idx1' arr2 idx2' len' }