From e97d6539a682fc738ac8f86195f2cca3588cd278 Mon Sep 17 00:00:00 2001 From: Andrei Stefanescu Date: Tue, 9 Jun 2020 21:34:44 -0700 Subject: [PATCH] Add SMT Array primitives. (#11) * Add SMT Array primitives. * Use panic instead of fail. --- saw-core-what4.cabal | 2 + src/Verifier/SAW/Simulator/What4.hs | 112 +++++++++++++++++- .../SAW/Simulator/What4/FirstOrder.hs | 16 ++- src/Verifier/SAW/Simulator/What4/Panic.hs | 22 ++++ 4 files changed, 145 insertions(+), 7 deletions(-) create mode 100644 src/Verifier/SAW/Simulator/What4/Panic.hs diff --git a/saw-core-what4.cabal b/saw-core-what4.cabal index b9d30bbe..740a8b0d 100644 --- a/saw-core-what4.cabal +++ b/saw-core-what4.cabal @@ -23,6 +23,7 @@ library saw-core, what4, crucible-saw, + panic, transformers, vector, parameterized-utils >= 1.0.8 && < 2.2, @@ -33,4 +34,5 @@ library Verifier.SAW.Simulator.What4.SWord Verifier.SAW.Simulator.What4.FirstOrder Verifier.SAW.Simulator.What4.PosNat + Verifier.SAW.Simulator.What4.Panic GHC-options: -Wall -Werror diff --git a/src/Verifier/SAW/Simulator/What4.hs b/src/Verifier/SAW/Simulator/What4.hs index 84aa92f3..f0e7ac95 100644 --- a/src/Verifier/SAW/Simulator/What4.hs +++ b/src/Verifier/SAW/Simulator/What4.hs @@ -19,6 +19,7 @@ {-# LANGUAGE DeriveTraversable #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-} +{-# LANGUAGE LambdaCase #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE PatternGuards #-} @@ -100,12 +101,21 @@ import qualified Lang.Crucible.Backend.SAWCore as CS import Verifier.SAW.Simulator.What4.SWord import Verifier.SAW.Simulator.What4.PosNat import Verifier.SAW.Simulator.What4.FirstOrder +import Verifier.SAW.Simulator.What4.Panic --------------------------------------------------------------------- -- empty datatype to index (open) type families -- for this backend data What4 (sym :: *) +-- | A What4 symbolic array where the domain and co-domain types do not appear +-- in the type +data SArray sym where + SArray :: + W.IsExpr (W.SymExpr sym) => + W.SymArray sym (Ctx.EmptyCtx Ctx.::> itp) etp -> + SArray sym + -- type abbreviations for uniform naming type SBool sym = Pred sym type SInt sym = SymInteger sym @@ -114,6 +124,7 @@ type instance EvalM (What4 sym) = IO type instance VBool (What4 sym) = SBool sym type instance VWord (What4 sym) = SWord sym type instance VInt (What4 sym) = SInt sym +type instance VArray (What4 sym) = SArray sym type instance Extra (What4 sym) = What4Extra sym type SValue sym = Value (What4 sym) @@ -213,6 +224,10 @@ prims = , Prims.bpIntLt = W.intLt sym , Prims.bpIntMin = intMin sym , Prims.bpIntMax = intMax sym + -- Array operations + , Prims.bpArrayConstant = arrayConstant sym + , Prims.bpArrayLookup = arrayLookup sym + , Prims.bpArrayUpdate = arrayUpdate sym } @@ -268,6 +283,26 @@ wordFun :: (Sym sym) => (SWord sym -> IO (SValue sym)) -> SValue sym wordFun f = strictFun (\x -> f =<< toWord x) +valueToSymExpr :: SValue sym -> Maybe (Some (W.SymExpr sym)) +valueToSymExpr = \case + VBool b -> Just $ Some b + VInt i -> Just $ Some i + VWord (DBV w) -> Just $ Some w + VArray (SArray a) -> Just $ Some a + _ -> Nothing + +symExprToValue :: + IsExpr (SymExpr sym) => + W.BaseTypeRepr tp -> + W.SymExpr sym tp -> + Maybe (SValue sym) +symExprToValue tp expr = case tp of + BaseBoolRepr -> Just $ VBool expr + BaseIntegerRepr -> Just $ VInt expr + (BaseBVRepr w) -> Just $ withKnownNat w $ VWord $ DBV expr + (BaseArrayRepr (Ctx.Empty Ctx.:> _) _) -> Just $ VArray $ SArray expr + _ -> Nothing + -- -- Integer bit/vector conversions -- @@ -472,6 +507,59 @@ selectV merger maxValue valueFn vx = p <- bvAt (given :: sym) vx j merger p (impl j (y `setBit` j)) (impl j y) where j = i - 1 +instance Show (SArray sym) where + show (SArray arr) = show $ W.printSymExpr arr + +arrayConstant :: + W.IsSymExprBuilder sym => + sym -> + SValue sym -> + SValue sym -> + IO (SArray sym) +arrayConstant sym ity elm + | Just (Some idx_repr) <- valueAsBaseType ity + , Just (Some elm_expr) <- valueToSymExpr elm = + SArray <$> W.constantArray sym (Ctx.Empty Ctx.:> idx_repr) elm_expr + | otherwise = + panic "Verifier.SAW.Simulator.What4.Panic.arrayConstant" ["argument type mismatch"] + +arrayLookup :: + W.IsSymExprBuilder sym => + sym -> + SArray sym -> + SValue sym -> + IO (SValue sym) +arrayLookup sym arr idx + | SArray arr_expr <- arr + , Just (Some idx_expr) <- valueToSymExpr idx + , W.BaseArrayRepr (Ctx.Empty Ctx.:> idx_repr) elm_repr <- W.exprType arr_expr + , Just Refl <- testEquality idx_repr (W.exprType idx_expr) = do + elm_expr <- W.arrayLookup sym arr_expr (Ctx.Empty Ctx.:> idx_expr) + maybe + (panic "Verifier.SAW.Simulator.What4.Panic.arrayLookup" ["argument type mismatch"]) + return + (symExprToValue elm_repr elm_expr) + | otherwise = + panic "Verifier.SAW.Simulator.What4.Panic.arrayLookup" ["argument type mismatch"] + +arrayUpdate :: + W.IsSymExprBuilder sym => + sym -> + SArray sym -> + SValue sym -> + SValue sym -> + IO (SArray sym) +arrayUpdate sym arr idx elm + | SArray arr_expr <- arr + , Just (Some idx_expr) <- valueToSymExpr idx + , Just (Some elm_expr) <- valueToSymExpr elm + , 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 elm_repr (W.exprType elm_expr) = + SArray <$> W.arrayUpdate sym arr_expr (Ctx.Empty Ctx.:> idx_expr) elm_expr + | otherwise = + panic "Verifier.SAW.Simulator.What4.Panic.arrayUpdate" ["argument type mismatch"] + ---------------------------------------------------------------------- -- | A basic symbolic simulator/evaluator: interprets a saw-core Term as -- a symbolic value @@ -577,6 +665,12 @@ parseUninterpreted sym ref app ty = | i <- [0 .. n-1] ] return (VVector (V.fromList (map ready xs))) + VArrayType ity ety + | Just (Some idx_repr) <- valueAsBaseType ity + , Just (Some elm_repr) <- valueAsBaseType ety + -> (VArray . SArray) <$> + mkUninterpreted sym ref app (BaseArrayRepr (Ctx.Empty Ctx.:> idx_repr) elm_repr) + VUnitType -> return VUnit @@ -645,6 +739,7 @@ applyUnintApp app0 v = VBool sb -> return (extendUnintApp app0 sb BaseBoolRepr) VInt si -> return (extendUnintApp app0 si BaseIntegerRepr) VWord (DBV sw) -> return (extendUnintApp app0 sw (W.exprType sw)) + VArray (SArray sa) -> return (extendUnintApp app0 sa (W.exprType sa)) VWord ZBV -> return app0 VCtorApp i xv -> foldM applyUnintApp app' =<< traverse force xv where app' = suffixUnintApp ("_" ++ identName i) app0 @@ -720,6 +815,8 @@ vAsFirstOrderType v = -> return FOTInt VVecType (VNat n) v2 -> FOTVec (fromInteger n) <$> vAsFirstOrderType v2 + VArrayType iv ev + -> FOTArray <$> vAsFirstOrderType iv <*> vAsFirstOrderType ev VUnitType -> return (FOTTuple []) VPairType v1 v2 @@ -733,6 +830,9 @@ vAsFirstOrderType v = mapM (\(f,tp) -> (f,) <$> vAsFirstOrderType tp) tps) _ -> Nothing +valueAsBaseType :: IsSymExprBuilder sym => SValue sym -> Maybe (Some W.BaseTypeRepr) +valueAsBaseType v = fmap fotToBaseType $ vAsFirstOrderType v + ------------------------------------------------------------------------------ -- | Generate a new symbolic value (a variable) from a given first-order-type @@ -812,11 +912,7 @@ newVarFOT fot typedToSValue :: (IsExpr (SymExpr sym)) => TypedExpr sym -> IO (SValue sym) typedToSValue (TypedExpr ty expr) = - case ty of - BaseBoolRepr -> return $ VBool expr - BaseIntegerRepr -> return $ VInt expr - (BaseBVRepr w) -> return $ withKnownNat w $ VWord (DBV expr) - _ -> fail "Cannot handle" + maybe (fail "Cannot handle") return $ symExprToValue ty expr ---------------------------------------------------------------------- -- Evaluation through crucible-saw backend @@ -940,6 +1036,12 @@ parseUninterpretedSAW sym sc ref trm app ty = xs <- traverse mkElem [0 .. n-1] return (VVector (V.fromList (map ready xs))) + VArrayType ity ety + | Just (Some idx_repr) <- valueAsBaseType ity + , Just (Some elm_repr) <- valueAsBaseType ety + -> (VArray . SArray) <$> + mkUninterpretedSAW sym ref trm app (BaseArrayRepr (Ctx.Empty Ctx.:> idx_repr) elm_repr) + VUnitType -> return VUnit diff --git a/src/Verifier/SAW/Simulator/What4/FirstOrder.hs b/src/Verifier/SAW/Simulator/What4/FirstOrder.hs index e7c1aa2d..caea4670 100644 --- a/src/Verifier/SAW/Simulator/What4/FirstOrder.hs +++ b/src/Verifier/SAW/Simulator/What4/FirstOrder.hs @@ -55,6 +55,10 @@ fotToBaseType (FOTVec nat FOTBit) fotToBaseType (FOTVec nat fot) | Some assn <- listToAssn (replicate (fromIntegral nat) fot) = Some (BaseStructRepr assn) +fotToBaseType (FOTArray fot1 fot2) + | Some ty1 <- fotToBaseType fot1 + , Some ty2 <- fotToBaseType fot2 + = Some $ BaseArrayRepr (Empty :> ty1) ty2 fotToBaseType (FOTTuple fots) | Some assn <- listToAssn fots = Some (BaseStructRepr assn) @@ -78,7 +82,11 @@ typeReprToFOT (BaseBVRepr w) = pure $ FOTVec (natValue w) FOTBit typeReprToFOT BaseRealRepr = Left "No FO Real" typeReprToFOT BaseComplexRepr = Left "No FO Complex" typeReprToFOT (BaseStringRepr _) = Left "No FO String" -typeReprToFOT (BaseArrayRepr _ctx _b) = Left "TODO: FO Arrays" +typeReprToFOT (BaseArrayRepr (Empty :> ty) b) + | Right fot1 <- typeReprToFOT ty + , Right fot2 <- typeReprToFOT b + = pure $ FOTArray fot1 fot2 +typeReprToFOT ty@(BaseArrayRepr _ctx _b) = Left $ "Unsupported FO Array: " ++ show ty typeReprToFOT (BaseFloatRepr _) = Left "No FO Floating point" typeReprToFOT (BaseStructRepr ctx) = FOTTuple <$> assnToList ctx @@ -100,7 +108,11 @@ groundToFOV BaseRealRepr _ = Left "Real is not FOV" groundToFOV BaseComplexRepr _ = Left "Complex is not FOV" groundToFOV (BaseStringRepr _) _ = Left "String is not FOV" groundToFOV (BaseFloatRepr _) _ = Left "Floating point is not FOV" -groundToFOV (BaseArrayRepr _idx _b) _ = Left "TODO: FOV Array" +groundToFOV (BaseArrayRepr (Empty :> ty) b) _ + | Right fot1 <- typeReprToFOT ty + , Right fot2 <- typeReprToFOT b + = pure $ FOVArray fot1 fot2 +groundToFOV (BaseArrayRepr _idx _b) _ = Left "Unsupported FOV Array" groundToFOV (BaseStructRepr ctx) tup = FOVTuple <$> tupleToList ctx tup diff --git a/src/Verifier/SAW/Simulator/What4/Panic.hs b/src/Verifier/SAW/Simulator/What4/Panic.hs new file mode 100644 index 00000000..635f1f50 --- /dev/null +++ b/src/Verifier/SAW/Simulator/What4/Panic.hs @@ -0,0 +1,22 @@ +{-# LANGUAGE Trustworthy #-} +{-# LANGUAGE TemplateHaskell #-} + +module Verifier.SAW.Simulator.What4.Panic + ( panic + ) where + +import Panic hiding (panic) +import qualified Panic + +data SAWCoreWhat4 = SAWCoreWhat4 + +panic :: HasCallStack => String -> [String] -> a +panic = Panic.panic SAWCoreWhat4 + +instance PanicComponent SAWCoreWhat4 where + panicComponentName _ = "SAWCoreWhat4" + panicComponentIssues _ = "https://github.com/GaloisInc/saw-core-what4/issues" + + {-# Noinline panicComponentRevision #-} + panicComponentRevision = $useGitRevision +