From 8b8ff9b613b8f1dfb77f6d95f3cc47af9d3756d7 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Thu, 24 Aug 2023 15:11:26 -0400 Subject: [PATCH] SetupValue: Use proper TTG-style extension fields This removes all of the `HasSetup* :: Bool` type families in favor of new `X* :: Type` type families. These largely serve the same purpose of distinguishing which constructors of `SetupValue` are permissible in each language backend, but they are permit bundling additional, language-specific information into a `SetupValue`. For instance, the `XSetupStruct` instance for `LLVM` evaluates to `Bool`, representing whether we are dealing with an LLVM packed struct or not, and the `XSetupCast` instance for `LLVM` evaluates to an LLVM `Type` to represent the type to cast to. One consequence of this design, aside from some `SetupValue` fields moving around, is that `ppSetupValue` now must perform case analysis on which language backend is currently in use in order to pretty-print any backend-specific data. This is accomplished with the new `SAWExt` data type and the corresponding `IsExt` class. There is a lot of code that shifts around in this patch, but everything is still functionally equivalent. In a subsequent patch, I will introduce additional data into MIR-specific extension fields. Fixes #1914. --- .../src/Mir/Compositional/Builder.hs | 10 +- .../src/Mir/Compositional/Override.hs | 12 +- src/SAWScript/Crucible/Common/MethodSpec.hs | 100 ++++++++++---- src/SAWScript/Crucible/Common/Setup/Value.hs | 122 +++++++++--------- src/SAWScript/Crucible/JVM/Override.hs | 4 +- .../Crucible/JVM/ResolveSetupValue.hs | 8 +- src/SAWScript/Crucible/JVM/Setup/Value.hs | 22 ++-- src/SAWScript/Crucible/LLVM/Builtins.hs | 4 +- src/SAWScript/Crucible/LLVM/MethodSpecIR.hs | 8 +- src/SAWScript/Crucible/LLVM/Override.hs | 12 +- .../Crucible/LLVM/ResolveSetupValue.hs | 12 +- src/SAWScript/Crucible/LLVM/Setup/Value.hs | 24 ++-- src/SAWScript/Crucible/MIR/Override.hs | 6 +- .../Crucible/MIR/ResolveSetupValue.hs | 8 +- src/SAWScript/Crucible/MIR/Setup/Value.hs | 22 ++-- 15 files changed, 213 insertions(+), 161 deletions(-) diff --git a/crucible-mir-comp/src/Mir/Compositional/Builder.hs b/crucible-mir-comp/src/Mir/Compositional/Builder.hs index b55229775e..91d5b40a21 100644 --- a/crucible-mir-comp/src/Mir/Compositional/Builder.hs +++ b/crucible-mir-comp/src/Mir/Compositional/Builder.hs @@ -635,11 +635,11 @@ substMethodSpec sc sm ms = do MS.SetupVar _ -> return sv MS.SetupTerm tt -> MS.SetupTerm <$> goTypedTerm tt MS.SetupNull _ -> return sv - MS.SetupStruct b packed svs -> MS.SetupStruct b packed <$> mapM goSetupValue svs + MS.SetupStruct b svs -> MS.SetupStruct b <$> mapM goSetupValue svs MS.SetupArray b svs -> MS.SetupArray b <$> mapM goSetupValue svs MS.SetupElem b sv idx -> MS.SetupElem b <$> goSetupValue sv <*> pure idx MS.SetupField b sv name -> MS.SetupField b <$> goSetupValue sv <*> pure name - MS.SetupCast v _ _ -> case v of {} + MS.SetupCast v _ -> case v of {} MS.SetupUnion v _ _ -> case v of {} MS.SetupGlobal _ _ -> return sv MS.SetupGlobalInitializer _ _ -> return sv @@ -677,14 +677,14 @@ regToSetup bak p eval shp rv = go shp rv go :: forall tp. TypeShape tp -> RegValue sym tp -> BuilderT sym t (OverrideSim p sym MIR rtp args ret) (MS.SetupValue MIR) - go (UnitShape _) () = return $ MS.SetupStruct () False [] + go (UnitShape _) () = return $ MS.SetupStruct () [] go (PrimShape _ btpr) expr = do -- Record all vars used in `expr` cache <- use msbVisitCache visitExprVars cache expr $ \var -> do msbPrePost p . seVars %= Set.insert (Some var) liftIO $ MS.SetupTerm <$> eval btpr expr - go (TupleShape _ _ flds) rvs = MS.SetupStruct () False <$> goFields flds rvs + go (TupleShape _ _ flds) rvs = MS.SetupStruct () <$> goFields flds rvs go (ArrayShape _ _ shp) vec = do svs <- case vec of MirVector_Vector v -> mapM (go shp) (toList v) @@ -695,7 +695,7 @@ regToSetup bak p eval shp rv = go shp rv return $ MS.SetupArray () svs go (StructShape _ _ flds) (AnyValue tpr rvs) | Just Refl <- testEquality tpr shpTpr = - MS.SetupStruct () False <$> goFields flds rvs + MS.SetupStruct () <$> goFields flds rvs | otherwise = error $ "regToSetup: type error: expected " ++ show shpTpr ++ ", but got Any wrapping " ++ show tpr where shpTpr = StructRepr $ fmapFC fieldShapeType flds diff --git a/crucible-mir-comp/src/Mir/Compositional/Override.hs b/crucible-mir-comp/src/Mir/Compositional/Override.hs index e238b9452a..22dea6d78c 100644 --- a/crucible-mir-comp/src/Mir/Compositional/Override.hs +++ b/crucible-mir-comp/src/Mir/Compositional/Override.hs @@ -356,7 +356,7 @@ matchArg sym sc eval allocSpecs md shp rv sv = go shp rv sv where go :: forall tp. TypeShape tp -> RegValue sym tp -> MS.SetupValue MIR -> MirOverrideMatcher sym () - go (UnitShape _) () (MS.SetupStruct () False []) = return () + go (UnitShape _) () (MS.SetupStruct () []) = return () go (PrimShape _ _btpr) expr (MS.SetupTerm tt) = do loc <- use MS.osLocation exprTerm <- liftIO $ eval expr @@ -390,14 +390,14 @@ matchArg sym sc eval allocSpecs md shp rv sv = go shp rv sv ("mismatch on " ++ show (W4.exprType expr) ++ ": expected " ++ show (W4.printSymExpr val)) "" - go (TupleShape _ _ flds) rvs (MS.SetupStruct () False svs) = goFields flds rvs svs + go (TupleShape _ _ flds) rvs (MS.SetupStruct () svs) = goFields flds rvs svs go (ArrayShape _ _ shp) vec (MS.SetupArray () svs) = case vec of MirVector_Vector v -> zipWithM_ (\x y -> go shp x y) (toList v) svs MirVector_PartialVector pv -> forM_ (zip (toList pv) svs) $ \(p, sv) -> do rv <- liftIO $ readMaybeType sym "vector element" (shapeType shp) p go shp rv sv MirVector_Array _ -> error $ "matchArg: MirVector_Array NYI" - go (StructShape _ _ flds) (AnyValue tpr rvs) (MS.SetupStruct () False svs) + go (StructShape _ _ flds) (AnyValue tpr rvs) (MS.SetupStruct () svs) | Just Refl <- testEquality tpr shpTpr = goFields flds rvs svs | otherwise = error $ "matchArg: type error: expected " ++ show shpTpr ++ ", but got Any wrapping " ++ show tpr @@ -510,7 +510,7 @@ setupToReg :: forall sym t st fs tp. setupToReg sym sc termSub regMap allocMap shp sv = go shp sv where go :: forall tp. TypeShape tp -> MS.SetupValue MIR -> IO (RegValue sym tp) - go (UnitShape _) (MS.SetupStruct _ False []) = return () + go (UnitShape _) (MS.SetupStruct _ []) = return () go (PrimShape _ btpr) (MS.SetupTerm tt) = do term <- liftIO $ SAW.scInstantiateExt sc termSub $ SAW.ttTerm tt Some expr <- termToExpr sym sc regMap term @@ -519,11 +519,11 @@ setupToReg sym sc termSub regMap allocMap shp sv = go shp sv Nothing -> error $ "setupToReg: expected " ++ show btpr ++ ", but got " ++ show (W4.exprType expr) return expr - go (TupleShape _ _ flds) (MS.SetupStruct _ False svs) = goFields flds svs + go (TupleShape _ _ flds) (MS.SetupStruct _ svs) = goFields flds svs go (ArrayShape _ _ shp) (MS.SetupArray _ svs) = do rvs <- mapM (go shp) svs return $ MirVector_Vector $ V.fromList rvs - go (StructShape _ _ flds) (MS.SetupStruct _ False svs) = + go (StructShape _ _ flds) (MS.SetupStruct _ svs) = AnyValue (StructRepr $ fmapFC fieldShapeType flds) <$> goFields flds svs go (TransparentShape _ shp) sv = go shp sv go (RefShape _ _ _ tpr) (MS.SetupVar alloc) = case Map.lookup alloc allocMap of diff --git a/src/SAWScript/Crucible/Common/MethodSpec.hs b/src/SAWScript/Crucible/Common/MethodSpec.hs index ec4d92a4e6..3df49ee9af 100644 --- a/src/SAWScript/Crucible/Common/MethodSpec.hs +++ b/src/SAWScript/Crucible/Common/MethodSpec.hs @@ -15,8 +15,10 @@ Grow\", and is prevalent across the Crucible codebase. {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE LambdaCase #-} +{-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeFamilyDependencies #-} {-# LANGUAGE UndecidableInstances #-} @@ -32,23 +34,19 @@ module SAWScript.Crucible.Common.MethodSpec , AllocSpec , TypeName , ExtType - , CastType , PointsTo , AllocGlobal , ResolvedState - , BoolToType - , B - - , HasSetupNull - , HasSetupStruct - , HasSetupArray - , HasSetupElem - , HasSetupField - , HasSetupGlobal - , HasSetupCast - , HasSetupUnion - , HasSetupGlobalInitializer + , XSetupNull + , XSetupStruct + , XSetupArray + , XSetupElem + , XSetupField + , XSetupGlobal + , XSetupCast + , XSetupUnion + , XSetupGlobalInitializer , SetupValue(..) , SetupValueHas @@ -62,7 +60,7 @@ module SAWScript.Crucible.Common.MethodSpec , setupToTypedTerm , setupToTerm - , HasGhostState + , XGhostState , GhostValue , GhostType , GhostGlobal @@ -111,10 +109,12 @@ module SAWScript.Crucible.Common.MethodSpec , makeCrucibleMethodSpecIR ) where +import Data.Kind (Type) import Data.Map (Map) import qualified Data.Map as Map import Data.Set (Set) import Data.Time.Clock +import Data.Void (absurd) import Control.Monad.Trans.Maybe import Control.Monad.Trans (lift) @@ -126,9 +126,11 @@ import Data.Parameterized.Nonce -- what4 import What4.ProgramLoc (ProgramLoc(plSourceLoc), Position) +import Lang.Crucible.JVM (JVM) import qualified Lang.Crucible.Types as Crucible (IntrinsicType, EmptyCtx) import qualified Lang.Crucible.CFG.Common as Crucible (GlobalVar) +import Mir.Intrinsics (MIR) import qualified Cryptol.Utils.PP as Cryptol @@ -136,6 +138,9 @@ import Verifier.SAW.TypedTerm as SAWVerifier import Verifier.SAW.SharedTerm as SAWVerifier import SAWScript.Crucible.Common.Setup.Value +import SAWScript.Crucible.LLVM.Setup.Value (LLVM) +import SAWScript.Crucible.JVM.Setup.Value () +import SAWScript.Crucible.MIR.Setup.Value () import SAWScript.Options import SAWScript.Prover.SolverStats import SAWScript.Utils (bullets) @@ -153,30 +158,75 @@ stateCond PostState = "postcondition" -------------------------------------------------------------------------------- -- ** SetupValue +-- | A singleton type that encodes the extensions used for each SAW backend. +-- Matching on a value of type @'SAWExt' ext@ allows one to learn which backend +-- is currently in use. +data SAWExt :: Type -> Type where + LLVMExt :: SAWExt (LLVM arch) + JVMExt :: SAWExt JVM + MIRExt :: SAWExt MIR + +-- | This allows checking which SAW backend we are using at runtime. +class IsExt ext where + sawExt :: SAWExt ext + +instance IsExt (LLVM arch) where + sawExt = LLVMExt +instance IsExt JVM where + sawExt = JVMExt +instance IsExt MIR where + sawExt = MIRExt + -- | Note that most 'SetupValue' concepts (like allocation indices) -- are implementation details and won't be familiar to users. --- Consider using 'resolveSetupValue' and printing an 'LLVMVal' --- with @PP.pretty@ instead. -ppSetupValue :: Show (CastType ext) => SetupValue ext -> PP.Doc ann +-- Consider using 'resolveSetupValue' and printing the language-specific value +-- (e.g., an 'LLVMVal') with @PP.pretty@ instead. +ppSetupValue :: forall ext ann. IsExt ext => SetupValue ext -> PP.Doc ann ppSetupValue setupval = case setupval of SetupTerm tm -> ppTypedTerm tm SetupVar i -> ppAllocIndex i SetupNull _ -> PP.pretty "NULL" - SetupStruct _ packed vs - | packed -> PP.angles (PP.braces (commaList (map ppSetupValue vs))) - | otherwise -> PP.braces (commaList (map ppSetupValue vs)) + SetupStruct x vs -> + case (ext, x) of + (LLVMExt, packed) -> + ppSetupStructLLVM packed vs + (JVMExt, empty) -> + absurd empty + (MIRExt, ()) -> + ppSetupStructDefault vs SetupArray _ vs -> PP.brackets (commaList (map ppSetupValue vs)) SetupElem _ v i -> PP.parens (ppSetupValue v) PP.<> PP.pretty ("." ++ show i) SetupField _ v f -> PP.parens (ppSetupValue v) PP.<> PP.pretty ("." ++ f) SetupUnion _ v u -> PP.parens (ppSetupValue v) PP.<> PP.pretty ("." ++ u) - SetupCast _ v tp -> PP.parens (ppSetupValue v) PP.<> PP.pretty (" AS " ++ show tp) + SetupCast x v -> + case (ext, x) of + (LLVMExt, tp) -> + PP.parens (ppSetupValue v) PP.<> PP.pretty (" AS " ++ show tp) + (JVMExt, empty) -> + absurd empty + (MIRExt, empty) -> + absurd empty SetupGlobal _ nm -> PP.pretty ("global(" ++ nm ++ ")") SetupGlobalInitializer _ nm -> PP.pretty ("global_initializer(" ++ nm ++ ")") where + ext :: SAWExt ext + ext = sawExt @ext + commaList :: [PP.Doc ann] -> PP.Doc ann commaList [] = PP.emptyDoc commaList (x:xs) = x PP.<> PP.hcat (map (\y -> PP.comma PP.<+> y) xs) + ppSetupStructLLVM :: + Bool + -- ^ 'True' if this is an LLVM packed struct, 'False' otherwise. + -> [SetupValue ext] -> PP.Doc ann + ppSetupStructLLVM packed vs + | packed = PP.angles (ppSetupStructDefault vs) + | otherwise = ppSetupStructDefault vs + + ppSetupStructDefault :: [SetupValue ext] -> PP.Doc ann + ppSetupStructDefault vs = PP.braces (commaList (map ppSetupValue vs)) + ppAllocIndex :: AllocIndex -> PP.Doc ann ppAllocIndex i = PP.pretty '@' <> PP.viaShow i @@ -224,7 +274,7 @@ setupToTerm opts sc = \case SetupTerm term -> return (ttTerm term) - SetupStruct _ _ fields -> + SetupStruct _ fields -> do ts <- mapM (setupToTerm opts sc) fields lift $ scTuple sc ts @@ -248,7 +298,7 @@ setupToTerm opts sc = typ <- lift $ scTypeOf sc et lift $ scAt sc lent typ art ixt - SetupStruct _ _ fs -> + SetupStruct _ fs -> do st <- setupToTerm opts sc base lift $ scTupleSelector sc st ind (length fs) @@ -270,14 +320,14 @@ type GhostGlobal = Crucible.GlobalVar GhostType data SetupCondition ext where SetupCond_Equal :: ConditionMetadata -> SetupValue ext -> SetupValue ext -> SetupCondition ext SetupCond_Pred :: ConditionMetadata -> TypedTerm -> SetupCondition ext - SetupCond_Ghost :: B (HasGhostState ext) -> + SetupCond_Ghost :: XGhostState ext -> ConditionMetadata -> GhostGlobal -> TypedTerm -> SetupCondition ext deriving instance ( SetupValueHas Show ext - , Show (B (HasGhostState ext)) + , Show (XGhostState ext) ) => Show (SetupCondition ext) -- | Verification state (either pre- or post-) specification diff --git a/src/SAWScript/Crucible/Common/Setup/Value.hs b/src/SAWScript/Crucible/Common/Setup/Value.hs index 615f728b9f..6fb0aec6c7 100644 --- a/src/SAWScript/Crucible/Common/Setup/Value.hs +++ b/src/SAWScript/Crucible/Common/Setup/Value.hs @@ -32,28 +32,24 @@ module SAWScript.Crucible.Common.Setup.Value , AllocSpec , TypeName , ExtType - , CastType , PointsTo , AllocGlobal , ResolvedState - , BoolToType - , B - - , HasSetupNull - , HasSetupStruct - , HasSetupArray - , HasSetupElem - , HasSetupField - , HasSetupGlobal - , HasSetupCast - , HasSetupUnion - , HasSetupGlobalInitializer + , XSetupNull + , XSetupStruct + , XSetupArray + , XSetupElem + , XSetupField + , XSetupGlobal + , XSetupCast + , XSetupUnion + , XSetupGlobalInitializer , SetupValue(..) , SetupValueHas - , HasGhostState + , XGhostState , ConditionMetadata(..) @@ -66,7 +62,6 @@ module SAWScript.Crucible.Common.Setup.Value import Data.Constraint (Constraint) import Data.Kind (Type) import Data.Set (Set) -import Data.Void (Void) import What4.ProgramLoc (ProgramLoc) @@ -93,9 +88,6 @@ type family TypeName ext :: Type -- | The type of types of the syntax extension we're dealing with type family ExtType ext :: Type --- | The types that can appear in casts -type family CastType ext :: Type - -- | The type of points-to assertions type family PointsTo ext :: Type @@ -108,24 +100,34 @@ type family ResolvedState ext :: Type -------------------------------------------------------------------------------- -- ** SetupValue --- | An injective type family mapping type-level booleans to types -type family BoolToType (b :: Bool) = (t :: Type) | t -> b where - BoolToType 'True = () - BoolToType 'False = Void - -type B b = BoolToType b - - -- The following type families describe what SetupValues are legal for which - -- languages. -type family HasSetupNull ext :: Bool -type family HasSetupStruct ext :: Bool -type family HasSetupArray ext :: Bool -type family HasSetupElem ext :: Bool -type family HasSetupField ext :: Bool -type family HasSetupGlobal ext :: Bool -type family HasSetupCast ext :: Bool -type family HasSetupUnion ext :: Bool -type family HasSetupGlobalInitializer ext :: Bool +-- The following type families are extension fields, which describe what +-- SetupValues are legal for which language backends. Instances for these type +-- families adhere to the following conventions: +-- +-- - If a SetupValue constructor is used in a particular backend and there is +-- some data that is /only/ used by that backend, then the corresponding +-- extension field should have a @type instance@ that evaluates to the type of +-- that data. For instance, the @XSetupCast@ instance for @LLVM@ might +-- evaluate to an LLVM @Type@ to represent the type to cast to. +-- +-- - If a SetupValue constructor is used in a particular backend but there is +-- no backend-specific information, then the corresponding extension field +-- should have a @type instance@ that evaluates to @()@. +-- +-- - If a SetupValue constructor is not used in a particular backend, its +-- corresponding extension field should have a @type instance@ that evaluates +-- to Void. Any code that pattern matches on the constructor should then +-- dispatch on the Void value using the 'absurd' function. + +type family XSetupNull ext +type family XSetupStruct ext +type family XSetupArray ext +type family XSetupElem ext +type family XSetupField ext +type family XSetupGlobal ext +type family XSetupCast ext +type family XSetupUnion ext +type family XSetupGlobalInitializer ext -- | From the manual: \"The SetupValue type corresponds to values that can occur -- during symbolic execution, which includes both 'Term' values, pointers, and @@ -133,35 +135,35 @@ type family HasSetupGlobalInitializer ext :: Bool data SetupValue ext where SetupVar :: AllocIndex -> SetupValue ext SetupTerm :: TypedTerm -> SetupValue ext - SetupNull :: B (HasSetupNull ext) -> SetupValue ext - -- | If the 'Bool' is 'True', it's a (LLVM) packed struct - SetupStruct :: B (HasSetupStruct ext) -> Bool -> [SetupValue ext] -> SetupValue ext - SetupArray :: B (HasSetupArray ext) -> [SetupValue ext] -> SetupValue ext - SetupElem :: B (HasSetupElem ext) -> SetupValue ext -> Int -> SetupValue ext - SetupField :: B (HasSetupField ext) -> SetupValue ext -> String -> SetupValue ext - SetupCast :: B (HasSetupCast ext) -> SetupValue ext -> CastType ext -> SetupValue ext - SetupUnion :: B (HasSetupUnion ext) -> SetupValue ext -> String -> SetupValue ext + SetupNull :: XSetupNull ext -> SetupValue ext + SetupStruct :: XSetupStruct ext -> [SetupValue ext] -> SetupValue ext + SetupArray :: XSetupArray ext -> [SetupValue ext] -> SetupValue ext + SetupElem :: XSetupElem ext -> SetupValue ext -> Int -> SetupValue ext + SetupField :: XSetupField ext -> SetupValue ext -> String -> SetupValue ext + SetupCast :: XSetupCast ext -> SetupValue ext -> SetupValue ext + SetupUnion :: XSetupUnion ext -> SetupValue ext -> String -> SetupValue ext -- | A pointer to a global variable - SetupGlobal :: B (HasSetupGlobal ext) -> String -> SetupValue ext + SetupGlobal :: XSetupGlobal ext -> String -> SetupValue ext -- | This represents the value of a global's initializer. SetupGlobalInitializer :: - B (HasSetupGlobalInitializer ext) -> String -> SetupValue ext + XSetupGlobalInitializer ext -> String -> SetupValue ext --- | This constraint can be solved for any ext so long as '()' and 'Void' have --- the constraint. Unfortunately, GHC can't (yet?) reason over the equations --- in our closed type family, and realize that +-- | This constraint can be solved for any ext so long as '()', 'Void', and any +-- other types used in the right-hand sides of extension field +-- @type instance@s have the constraint. Unfortunately, GHC can't (yet?) +-- reason over the equations in our closed type family and realize that, so we +-- must explicitly abstract this reasoning out into a type synonym. type SetupValueHas (c :: Type -> Constraint) ext = - ( c (B (HasSetupNull ext)) - , c (B (HasSetupStruct ext)) - , c (B (HasSetupArray ext)) - , c (B (HasSetupElem ext)) - , c (B (HasSetupField ext)) - , c (B (HasSetupCast ext)) - , c (B (HasSetupUnion ext)) - , c (B (HasSetupGlobal ext)) - , c (B (HasSetupGlobalInitializer ext)) - , c (CastType ext) + ( c (XSetupNull ext) + , c (XSetupStruct ext) + , c (XSetupArray ext) + , c (XSetupElem ext) + , c (XSetupField ext) + , c (XSetupCast ext) + , c (XSetupUnion ext) + , c (XSetupGlobal ext) + , c (XSetupGlobalInitializer ext) ) deriving instance (SetupValueHas Show ext) => Show (SetupValue ext) @@ -178,7 +180,7 @@ deriving instance (SetupValueHas Show ext) => Show (SetupValue ext) -- TODO: documentation -type family HasGhostState ext :: Bool +type family XGhostState ext -------------------------------------------------------------------------------- -- ** Pre- and post-conditions diff --git a/src/SAWScript/Crucible/JVM/Override.hs b/src/SAWScript/Crucible/JVM/Override.hs index 1b3404c4ba..41c316a317 100644 --- a/src/SAWScript/Crucible/JVM/Override.hs +++ b/src/SAWScript/Crucible/JVM/Override.hs @@ -964,11 +964,11 @@ instantiateSetupValue sc s v = MS.SetupTerm tt -> MS.SetupTerm <$> doTerm tt MS.SetupNull () -> return v MS.SetupGlobal empty _ -> absurd empty - MS.SetupStruct empty _ _ -> absurd empty + MS.SetupStruct empty _ -> absurd empty MS.SetupArray empty _ -> absurd empty MS.SetupElem empty _ _ -> absurd empty MS.SetupField empty _ _ -> absurd empty - MS.SetupCast empty _ _ -> absurd empty + MS.SetupCast empty _ -> absurd empty MS.SetupUnion empty _ _ -> absurd empty MS.SetupGlobalInitializer empty _ -> absurd empty where diff --git a/src/SAWScript/Crucible/JVM/ResolveSetupValue.hs b/src/SAWScript/Crucible/JVM/ResolveSetupValue.hs index c167fcab62..685cb42a98 100644 --- a/src/SAWScript/Crucible/JVM/ResolveSetupValue.hs +++ b/src/SAWScript/Crucible/JVM/ResolveSetupValue.hs @@ -139,11 +139,11 @@ typeOfSetupValue _cc env _nameEnv val = -- type-safe field accesses. return (J.ClassType (J.mkClassName "java/lang/Object")) MS.SetupGlobal empty _ -> absurd empty - MS.SetupStruct empty _ _ -> absurd empty + MS.SetupStruct empty _ -> absurd empty MS.SetupArray empty _ -> absurd empty MS.SetupElem empty _ _ -> absurd empty MS.SetupField empty _ _ -> absurd empty - MS.SetupCast empty _ _ -> absurd empty + MS.SetupCast empty _ -> absurd empty MS.SetupUnion empty _ _ -> absurd empty MS.SetupGlobalInitializer empty _ -> absurd empty @@ -170,11 +170,11 @@ resolveSetupVal cc env _tyenv _nameEnv val = MS.SetupNull () -> return (RVal (W4.maybePartExpr sym Nothing)) MS.SetupGlobal empty _ -> absurd empty - MS.SetupStruct empty _ _ -> absurd empty + MS.SetupStruct empty _ -> absurd empty MS.SetupArray empty _ -> absurd empty MS.SetupElem empty _ _ -> absurd empty MS.SetupField empty _ _ -> absurd empty - MS.SetupCast empty _ _ -> absurd empty + MS.SetupCast empty _ -> absurd empty MS.SetupUnion empty _ _ -> absurd empty MS.SetupGlobalInitializer empty _ -> absurd empty where diff --git a/src/SAWScript/Crucible/JVM/Setup/Value.hs b/src/SAWScript/Crucible/JVM/Setup/Value.hs index 47587d578a..04711a02e6 100644 --- a/src/SAWScript/Crucible/JVM/Setup/Value.hs +++ b/src/SAWScript/Crucible/JVM/Setup/Value.hs @@ -53,6 +53,7 @@ module SAWScript.Crucible.JVM.Setup.Value ) where import Control.Lens +import Data.Void (Void) import qualified Prettyprinter as PPL import qualified Lang.Crucible.FunctionHandle as Crucible (HandleAllocator) @@ -74,24 +75,23 @@ import qualified SAWScript.Crucible.Common.Setup.Value as MS -------------------------------------------------------------------------------- -- ** Language features -type instance MS.HasSetupNull CJ.JVM = 'True -type instance MS.HasSetupGlobal CJ.JVM = 'False -type instance MS.HasSetupStruct CJ.JVM = 'False -type instance MS.HasSetupArray CJ.JVM = 'False -type instance MS.HasSetupElem CJ.JVM = 'False -type instance MS.HasSetupField CJ.JVM = 'False -type instance MS.HasSetupCast CJ.JVM = 'False -type instance MS.HasSetupUnion CJ.JVM = 'False -type instance MS.HasSetupGlobalInitializer CJ.JVM = 'False +type instance MS.XSetupNull CJ.JVM = () +type instance MS.XSetupGlobal CJ.JVM = Void +type instance MS.XSetupStruct CJ.JVM = Void +type instance MS.XSetupArray CJ.JVM = Void +type instance MS.XSetupElem CJ.JVM = Void +type instance MS.XSetupField CJ.JVM = Void +type instance MS.XSetupCast CJ.JVM = Void +type instance MS.XSetupUnion CJ.JVM = Void +type instance MS.XSetupGlobalInitializer CJ.JVM = Void -type instance MS.HasGhostState CJ.JVM = 'False +type instance MS.XGhostState CJ.JVM = Void type JIdent = String -- FIXME(huffman): what to put here? type instance MS.TypeName CJ.JVM = JIdent type instance MS.ExtType CJ.JVM = J.Type -type instance MS.CastType CJ.JVM = () type instance MS.ResolvedState CJ.JVM = () -------------------------------------------------------------------------------- diff --git a/src/SAWScript/Crucible/LLVM/Builtins.hs b/src/SAWScript/Crucible/LLVM/Builtins.hs index fb12066c61..f70e250bc4 100644 --- a/src/SAWScript/Crucible/LLVM/Builtins.hs +++ b/src/SAWScript/Crucible/LLVM/Builtins.hs @@ -2215,7 +2215,7 @@ constructExpandedSetupValue cc sc loc t = traverse (constructExpandedSetupValue cc sc loc) (Crucible.siFieldTypes si) -- FIXME: should this always be unpacked? - pure $ mkAllLLVM $ SetupStruct () False $ map (\a -> getAllLLVM a) fields + pure $ mkAllLLVM $ SetupStruct False $ map (\a -> getAllLLVM a) fields Crucible.PtrType symTy -> case Crucible.asMemType symTy of @@ -2503,7 +2503,7 @@ llvm_fresh_pointer lty = constructFreshPointer (llvmTypeAlias lty) loc memTy llvm_cast_pointer :: AllLLVM SetupValue -> L.Type -> AllLLVM SetupValue -llvm_cast_pointer ptr lty = mkAllLLVM (SetupCast () (getAllLLVM ptr) lty) +llvm_cast_pointer ptr lty = mkAllLLVM (SetupCast lty (getAllLLVM ptr)) constructFreshPointer :: Crucible.HasPtrWidth (Crucible.ArchWidth arch) => diff --git a/src/SAWScript/Crucible/LLVM/MethodSpecIR.hs b/src/SAWScript/Crucible/LLVM/MethodSpecIR.hs index 99aec90161..2ed66092e3 100644 --- a/src/SAWScript/Crucible/LLVM/MethodSpecIR.hs +++ b/src/SAWScript/Crucible/LLVM/MethodSpecIR.hs @@ -382,13 +382,13 @@ anySetupArray :: [AllLLVM MS.SetupValue] -> AllLLVM MS.SetupValue anySetupArray vals = mkAllLLVM (MS.SetupArray () $ map (\a -> getAllLLVM a) vals) anySetupStruct :: Bool -> [AllLLVM MS.SetupValue] -> AllLLVM MS.SetupValue -anySetupStruct b vals = mkAllLLVM (MS.SetupStruct () b $ map (\a -> getAllLLVM a) vals) +anySetupStruct b vals = mkAllLLVM (MS.SetupStruct b $ map (\a -> getAllLLVM a) vals) anySetupElem :: AllLLVM MS.SetupValue -> Int -> AllLLVM MS.SetupValue anySetupElem val idx = mkAllLLVM (MS.SetupElem () (getAllLLVM val) idx) anySetupCast :: AllLLVM MS.SetupValue -> L.Type -> AllLLVM MS.SetupValue -anySetupCast val ty = mkAllLLVM (MS.SetupCast () (getAllLLVM val) ty) +anySetupCast val ty = mkAllLLVM (MS.SetupCast ty (getAllLLVM val)) anySetupField :: AllLLVM MS.SetupValue -> String -> AllLLVM MS.SetupValue anySetupField val field = mkAllLLVM (MS.SetupField () (getAllLLVM val) field) @@ -447,7 +447,7 @@ markResolved val0 path0 rs = go path0 val0 MS.SetupGlobal _ name -> rs & rsGlobals %~ Map.alter (ins path) name MS.SetupElem _ v idx -> go (ResolvedElem idx : path) v MS.SetupField _ v fld -> go (ResolvedField fld : path) v - MS.SetupCast _ v tp -> go (ResolvedCast tp : path) v + MS.SetupCast tp v -> go (ResolvedCast tp : path) v _ -> rs ins path Nothing = Just [path] @@ -468,7 +468,7 @@ testResolved val0 path0 rs = go path0 val0 MS.SetupGlobal _ c -> test path (Map.lookup c (_rsGlobals rs)) MS.SetupElem _ v idx -> go (ResolvedElem idx : path) v MS.SetupField _ v fld -> go (ResolvedField fld : path) v - MS.SetupCast _ v tp -> go (ResolvedCast tp : path) v + MS.SetupCast tp v -> go (ResolvedCast tp : path) v _ -> False test _ Nothing = False diff --git a/src/SAWScript/Crucible/LLVM/Override.hs b/src/SAWScript/Crucible/LLVM/Override.hs index 308bfcf1b9..3e4c838e6a 100644 --- a/src/SAWScript/Crucible/LLVM/Override.hs +++ b/src/SAWScript/Crucible/LLVM/Override.hs @@ -1116,11 +1116,11 @@ matchPointsTos opts sc cc spec prepost = go False [] setupVars v = case v of SetupVar i -> Set.singleton i - SetupStruct _ _ xs -> foldMap setupVars xs + SetupStruct _ xs -> foldMap setupVars xs SetupArray _ xs -> foldMap setupVars xs SetupElem _ x _ -> setupVars x SetupField _ x _ -> setupVars x - SetupCast _ x _ -> setupVars x + SetupCast _ x -> setupVars x SetupUnion _ x _ -> setupVars x SetupTerm _ -> Set.empty SetupNull _ -> Set.empty @@ -1291,7 +1291,7 @@ matchArg opts sc cc cs prepost md actual expectedTy expected = | (x, z) <- zip (V.toList xs) zs ] -- match the fields of struct point-wise - (Crucible.LLVMValStruct xs, Crucible.StructType fields, SetupStruct () _ zs) -> + (Crucible.LLVMValStruct xs, Crucible.StructType fields, SetupStruct _ zs) -> sequence_ [ matchArg opts sc cc cs prepost md x y z | ((_,x),y,z) <- zip3 (V.toList xs) @@ -2470,9 +2470,9 @@ instantiateSetupValue :: instantiateSetupValue sc s v = case v of SetupVar{} -> return v - SetupTerm tt -> SetupTerm <$> doTerm tt - SetupStruct () p vs -> SetupStruct () p <$> mapM (instantiateSetupValue sc s) vs - SetupArray () vs -> SetupArray () <$> mapM (instantiateSetupValue sc s) vs + SetupTerm tt -> SetupTerm <$> doTerm tt + SetupStruct p vs -> SetupStruct p <$> mapM (instantiateSetupValue sc s) vs + SetupArray () vs -> SetupArray () <$> mapM (instantiateSetupValue sc s) vs SetupElem{} -> return v SetupField{} -> return v SetupCast{} -> return v diff --git a/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs b/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs index cf3ca4f3ef..59877cfa87 100644 --- a/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs +++ b/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs @@ -120,7 +120,7 @@ resolveSetupValueInfo cc env nameEnv v = -- TODO? is this a panic situation? throwError $ "Type information for local allocation value not found: " ++ show i - SetupCast () _ (L.Alias alias) -> pure (L.guessAliasInfo mdMap alias) + SetupCast (L.Alias alias) _ -> pure (L.guessAliasInfo mdMap alias) SetupField () a n -> do i <- resolveSetupValueInfo cc env nameEnv a @@ -445,7 +445,7 @@ typeOfSetupValue cc env nameEnv val = , show (ppTypedTermType tp) ] - SetupStruct () packed vs -> + SetupStruct packed vs -> do memTys <- traverse (typeOfSetupValue cc env nameEnv) vs let si = Crucible.mkStructInfo dl packed memTys return (Crucible.StructType si) @@ -469,9 +469,9 @@ typeOfSetupValue cc env nameEnv val = [ "Could not determine LLVM type from computed debug type information:" , show info ] - Just ltp -> typeOfSetupValue cc env nameEnv (SetupCast () v ltp) + Just ltp -> typeOfSetupValue cc env nameEnv (SetupCast ltp v) - SetupCast () v ltp -> + SetupCast ltp v -> do memTy <- typeOfSetupValue cc env nameEnv v if Crucible.isPointerMemType memTy then @@ -614,11 +614,11 @@ resolveSetupVal cc mem env tyenv nameEnv val = SetupTerm tm -> resolveTypedTerm cc tm -- NB, SetupCast values should always be pointers. Pointer casts have no -- effect on the actual computed LLVMVal. - SetupCast () v _lty -> resolveSetupVal cc mem env tyenv nameEnv v + SetupCast _lty v -> resolveSetupVal cc mem env tyenv nameEnv v -- NB, SetupUnion values should always be pointers. Pointer casts have no -- effect on the actual computed LLVMVal. SetupUnion () v _n -> resolveSetupVal cc mem env tyenv nameEnv v - SetupStruct () packed vs -> do + SetupStruct packed vs -> do vals <- mapM (resolveSetupVal cc mem env tyenv nameEnv) vs let tps = map Crucible.llvmValStorableType vals let t = Crucible.mkStructType (V.fromList (mkFields packed dl Crucible.noAlignment 0 tps)) diff --git a/src/SAWScript/Crucible/LLVM/Setup/Value.hs b/src/SAWScript/Crucible/LLVM/Setup/Value.hs index 5895298e8c..9416b96a7b 100644 --- a/src/SAWScript/Crucible/LLVM/Setup/Value.hs +++ b/src/SAWScript/Crucible/LLVM/Setup/Value.hs @@ -116,21 +116,21 @@ import Verifier.SAW.TypedTerm data LLVM (arch :: CL.LLVMArch) -type instance Setup.HasSetupNull (LLVM _) = 'True -type instance Setup.HasSetupStruct (LLVM _) = 'True -type instance Setup.HasSetupArray (LLVM _) = 'True -type instance Setup.HasSetupElem (LLVM _) = 'True -type instance Setup.HasSetupField (LLVM _) = 'True -type instance Setup.HasSetupCast (LLVM _) = 'True -type instance Setup.HasSetupUnion (LLVM _) = 'True -type instance Setup.HasSetupGlobal (LLVM _) = 'True -type instance Setup.HasSetupGlobalInitializer (LLVM _) = 'True - -type instance Setup.HasGhostState (LLVM _) = 'True +type instance Setup.XSetupNull (LLVM _) = () +-- 'True' if this is an LLVM packed struct, 'False' otherwise. +type instance Setup.XSetupStruct (LLVM _) = Bool +type instance Setup.XSetupArray (LLVM _) = () +type instance Setup.XSetupElem (LLVM _) = () +type instance Setup.XSetupField (LLVM _) = () +type instance Setup.XSetupCast (LLVM _) = L.Type +type instance Setup.XSetupUnion (LLVM _) = () +type instance Setup.XSetupGlobal (LLVM _) = () +type instance Setup.XSetupGlobalInitializer (LLVM _) = () + +type instance Setup.XGhostState (LLVM _) = () type instance Setup.TypeName (LLVM arch) = CL.Ident type instance Setup.ExtType (LLVM arch) = CL.MemType -type instance Setup.CastType (LLVM arch) = L.Type -------------------------------------------------------------------------------- -- *** LLVMMethodId diff --git a/src/SAWScript/Crucible/MIR/Override.hs b/src/SAWScript/Crucible/MIR/Override.hs index 7a5892c44a..0b23c3de0a 100644 --- a/src/SAWScript/Crucible/MIR/Override.hs +++ b/src/SAWScript/Crucible/MIR/Override.hs @@ -181,11 +181,11 @@ instantiateSetupValue sc s v = MS.SetupTerm tt -> MS.SetupTerm <$> doTerm tt MS.SetupNull empty -> absurd empty MS.SetupGlobal empty _ -> absurd empty - MS.SetupStruct _ _ _ -> return v + MS.SetupStruct _ _ -> return v MS.SetupArray _ _ -> return v MS.SetupElem _ _ _ -> return v MS.SetupField _ _ _ -> return v - MS.SetupCast empty _ _ -> absurd empty + MS.SetupCast empty _ -> absurd empty MS.SetupUnion empty _ _ -> absurd empty MS.SetupGlobalInitializer empty _ -> absurd empty where @@ -308,7 +308,7 @@ matchArg opts sc cc cs _prepost md actual@(MIRVal (RefShape _refTy pointeeTy mut MS.SetupNull empty -> absurd empty MS.SetupGlobal empty _ -> absurd empty - MS.SetupCast empty _ _ -> absurd empty + MS.SetupCast empty _ -> absurd empty MS.SetupUnion empty _ _ -> absurd empty MS.SetupGlobalInitializer empty _ -> absurd empty diff --git a/src/SAWScript/Crucible/MIR/ResolveSetupValue.hs b/src/SAWScript/Crucible/MIR/ResolveSetupValue.hs index e1327ae6c5..5daca1d080 100644 --- a/src/SAWScript/Crucible/MIR/ResolveSetupValue.hs +++ b/src/SAWScript/Crucible/MIR/ResolveSetupValue.hs @@ -123,11 +123,11 @@ typeOfSetupValue _mcc env _nameEnv val = MS.SetupNull empty -> absurd empty MS.SetupGlobal empty _ -> absurd empty - MS.SetupStruct _ _ _ -> panic "typeOfSetupValue" ["structs not yet implemented"] + MS.SetupStruct _ _ -> panic "typeOfSetupValue" ["structs not yet implemented"] MS.SetupArray _ _ -> panic "typeOfSetupValue" ["arrays not yet implemented"] MS.SetupElem _ _ _ -> panic "typeOfSetupValue" ["elems not yet implemented"] MS.SetupField _ _ _ -> panic "typeOfSetupValue" ["fields not yet implemented"] - MS.SetupCast empty _ _ -> absurd empty + MS.SetupCast empty _ -> absurd empty MS.SetupUnion empty _ _ -> absurd empty MS.SetupGlobalInitializer empty _ -> absurd empty @@ -160,7 +160,7 @@ resolveSetupVal mcc env tyenv nameEnv val = MS.SetupTerm tm -> resolveTypedTerm mcc tm MS.SetupNull empty -> absurd empty MS.SetupGlobal empty _ -> absurd empty - MS.SetupStruct _ _ _ -> panic "resolveSetupValue" ["structs not yet implemented"] + MS.SetupStruct _ _ -> panic "resolveSetupValue" ["structs not yet implemented"] MS.SetupArray () [] -> fail "resolveSetupVal: invalid empty array" MS.SetupArray () vs -> do vals <- V.mapM (resolveSetupVal mcc env tyenv nameEnv) (V.fromList vs) @@ -186,7 +186,7 @@ resolveSetupVal mcc env tyenv nameEnv val = (Mir.MirVector_Vector vals') MS.SetupElem _ _ _ -> panic "resolveSetupValue" ["elems not yet implemented"] MS.SetupField _ _ _ -> panic "resolveSetupValue" ["fields not yet implemented"] - MS.SetupCast empty _ _ -> absurd empty + MS.SetupCast empty _ -> absurd empty MS.SetupUnion empty _ _ -> absurd empty MS.SetupGlobalInitializer empty _ -> absurd empty diff --git a/src/SAWScript/Crucible/MIR/Setup/Value.hs b/src/SAWScript/Crucible/MIR/Setup/Value.hs index 9f2bc01f02..c935340da2 100644 --- a/src/SAWScript/Crucible/MIR/Setup/Value.hs +++ b/src/SAWScript/Crucible/MIR/Setup/Value.hs @@ -46,6 +46,7 @@ import Control.Lens (makeLenses) import Data.Parameterized.Classes import Data.Parameterized.Some import Data.Text (Text) +import Data.Void (Void) import Lang.Crucible.FunctionHandle (HandleAllocator) import Lang.Crucible.Types @@ -57,17 +58,17 @@ import qualified Mir.Mir as M import SAWScript.Crucible.Common import qualified SAWScript.Crucible.Common.Setup.Value as MS -type instance MS.HasSetupNull MIR = 'False -type instance MS.HasSetupGlobal MIR = 'False -type instance MS.HasSetupStruct MIR = 'True -type instance MS.HasSetupArray MIR = 'True -type instance MS.HasSetupElem MIR = 'True -type instance MS.HasSetupField MIR = 'True -type instance MS.HasSetupCast MIR = 'False -type instance MS.HasSetupUnion MIR = 'False -type instance MS.HasSetupGlobalInitializer MIR = 'False +type instance MS.XSetupNull MIR = Void +type instance MS.XSetupGlobal MIR = Void +type instance MS.XSetupStruct MIR = () +type instance MS.XSetupArray MIR = () +type instance MS.XSetupElem MIR = () +type instance MS.XSetupField MIR = () +type instance MS.XSetupCast MIR = Void +type instance MS.XSetupUnion MIR = Void +type instance MS.XSetupGlobalInitializer MIR = Void -type instance MS.HasGhostState MIR = 'False +type instance MS.XGhostState MIR = Void type instance MS.TypeName MIR = Text type instance MS.ExtType MIR = M.Ty @@ -76,7 +77,6 @@ type instance MS.MethodId MIR = DefId type instance MS.AllocSpec MIR = Some MirAllocSpec type instance MS.PointsTo MIR = MirPointsTo type instance MS.ResolvedState MIR = () -type instance MS.CastType MIR = () type instance MS.Codebase MIR = CollectionState