diff --git a/crucible-mir-comp/src/Mir/Compositional/Builder.hs b/crucible-mir-comp/src/Mir/Compositional/Builder.hs index ba2f1ccc8b..c8effab421 100644 --- a/crucible-mir-comp/src/Mir/Compositional/Builder.hs +++ b/crucible-mir-comp/src/Mir/Compositional/Builder.hs @@ -273,8 +273,8 @@ addArg tpr argRef msb = , MS.conditionType = "add argument value" , MS.conditionContext = "" } - msbSpec . MS.csPreState . MS.csPointsTos %= (MirPointsTo md (fr ^. frAlloc) svs :) - msbSpec . MS.csPostState . MS.csPointsTos %= (MirPointsTo md (fr ^. frAlloc) svs' :) + msbSpec . MS.csPreState . MS.csPointsTos %= (MirPointsTo md (MS.SetupVar (fr ^. frAlloc)) svs :) + msbSpec . MS.csPostState . MS.csPointsTos %= (MirPointsTo md (MS.SetupVar (fr ^. frAlloc)) svs' :) msbSpec . MS.csArgBindings . at (fromIntegral idx) .= Just (ty, sv) where @@ -318,7 +318,7 @@ setReturn tpr argRef msb = , MS.conditionType = "set return value" , MS.conditionContext = "" } - msbSpec . MS.csPostState . MS.csPointsTos %= (MirPointsTo md (fr ^. frAlloc) svs :) + msbSpec . MS.csPostState . MS.csPointsTos %= (MirPointsTo md (MS.SetupVar (fr ^. frAlloc)) svs :) msbSpec . MS.csRetValue .= Just sv where diff --git a/crucible-mir-comp/src/Mir/Compositional/Override.hs b/crucible-mir-comp/src/Mir/Compositional/Override.hs index 831700f8b8..0b966eed67 100644 --- a/crucible-mir-comp/src/Mir/Compositional/Override.hs +++ b/crucible-mir-comp/src/Mir/Compositional/Override.hs @@ -208,7 +208,8 @@ runSpec cs mh ms = ovrWithBackend $ \bak -> -- to allocation `alloc` before we see the PointsTo for `alloc` itself. -- This ensures we can obtain a MirReference for each PointsTo that we -- see. - forM_ (reverse $ ms ^. MS.csPreState . MS.csPointsTos) $ \(MirPointsTo md alloc svs) -> do + forM_ (reverse $ ms ^. MS.csPreState . MS.csPointsTos) $ \(MirPointsTo md ref svs) -> do + alloc <- setupVarAllocIndex ref allocSub <- use MS.setupValueSub Some ptr <- case Map.lookup alloc allocSub of Just x -> return x @@ -311,7 +312,8 @@ runSpec cs mh ms = ovrWithBackend $ \bak -> -- figuring out which memory is accessible and mutable and thus needs to be -- clobbered, and for adding appropriate fresh variables and `PointsTo`s to -- the post state. - forM_ (ms ^. MS.csPostState . MS.csPointsTos) $ \(MirPointsTo _md alloc svs) -> do + forM_ (ms ^. MS.csPostState . MS.csPointsTos) $ \(MirPointsTo _md ref svs) -> do + alloc <- setupVarAllocIndex ref Some ptr <- case Map.lookup alloc allocMap of Just x -> return x Nothing -> error $ "post PointsTos are out of order: no ref for " ++ show alloc @@ -589,3 +591,20 @@ checkDisjoint bak refs = go refs assert bak disjoint $ GenericSimError $ "references " ++ show alloc ++ " and " ++ show alloc' ++ " must not overlap" go rest + +-- | Take a 'MS.SetupValue' that is assumed to be a bare 'MS.SetupVar' and +-- extract the underlying 'MS.AllocIndex'. If this assumption does not hold, +-- this function will raise an error. +-- +-- This is used in conjunction with 'MirPointsTo' values. With the way that +-- @crucible-mir-comp@ is currently set up, the only sort of 'MS.SetupValue' +-- that will be put into a 'MirPointsTo' value's left-hand side is a +-- 'MS.SetupVar', so we can safely use this function on such 'MS.SetupValue's. +-- Other parts of SAW can break this assumption (e.g., if you wrote something +-- like @mir_points_to (mir_global "X") ...@ in a SAW specification), but these +-- parts of SAW are not used in @crucible-mir-comp@. +setupVarAllocIndex :: Applicative m => MS.SetupValue MIR -> m MS.AllocIndex +setupVarAllocIndex (MS.SetupVar idx) = pure idx +setupVarAllocIndex val = + error $ "setupVarAllocIndex: Expected SetupVar, received: " + ++ show (MS.ppSetupValue val) diff --git a/src/SAWScript/Crucible/MIR/Builtins.hs b/src/SAWScript/Crucible/MIR/Builtins.hs index 25c6e1d9e8..ec87539e42 100644 --- a/src/SAWScript/Crucible/MIR/Builtins.hs +++ b/src/SAWScript/Crucible/MIR/Builtins.hs @@ -279,11 +279,6 @@ mir_points_to ref val = let env = MS.csAllocations (st ^. Setup.csMethodSpec) nameEnv = MS.csTypeNames (st ^. Setup.csMethodSpec) - allocIdx <- - case ref of - MS.SetupVar idx -> pure idx - _ -> X.throwM $ MIRPointsToNonReference ref - referentTy <- mir_points_to_check_lhs_validity ref loc valTy <- typeOfSetupValue cc env nameEnv val unless (checkCompatibleTys referentTy valTy) $ @@ -300,7 +295,7 @@ mir_points_to ref val = , MS.conditionType = "MIR points-to" , MS.conditionContext = "" } - Setup.addPointsTo (MirPointsTo md allocIdx [val]) + Setup.addPointsTo (MirPointsTo md ref [val]) -- | Perform a set of validity checks on the LHS reference value in a -- 'mir_points_to' command. In particular: @@ -320,7 +315,8 @@ mir_points_to_check_lhs_validity ref loc = refTy <- typeOfSetupValue cc env nameEnv ref case refTy of Mir.TyRef referentTy _ -> pure referentTy - _ -> throwCrucibleSetup loc $ "lhs not a reference type: " ++ show refTy + _ -> throwCrucibleSetup loc $ "lhs not a reference type: " + ++ show (PP.pretty refTy) mir_verify :: Mir.RustModule -> @@ -558,25 +554,37 @@ setupPrePointsTos mspec cc env pts mem0 = foldM doPointsTo mem0 pts Crucible.SymGlobalState Sym -> MirPointsTo -> IO (Crucible.SymGlobalState Sym) - doPointsTo globals (MirPointsTo _ allocIdx referents) = + doPointsTo globals (MirPointsTo _ reference referents) = mccWithBackend cc $ \bak -> do + MIRVal referenceShp referenceVal <- + resolveSetupVal cc env tyenv nameEnv reference + -- By the time we reach here, we have already checked (in mir_points_to) + -- that we are in fact dealing with a reference value, so the call to + -- `testRefShape` below should always succeed. + IsRefShape _ _ _ referenceInnerTy <- + case testRefShape referenceShp of + Just irs -> pure irs + Nothing -> + panic "setupPrePointsTos" + [ "Unexpected non-reference type:" + , show $ PP.pretty $ shapeMirTy referenceShp + ] referent <- firstPointsToReferent referents - MIRVal referentTy referentVal <- + MIRVal referentShp referentVal <- resolveSetupVal cc env tyenv nameEnv referent - Some mp <- pure $ lookupAllocIndex env allocIdx -- By the time we reach here, we have already checked (in mir_points_to) -- that the type of the reference is compatible with the right-hand side -- value, so the equality check below should never fail. Refl <- - case W4.testEquality (mp^.mpType) (shapeType referentTy) of + case W4.testEquality referenceInnerTy (shapeType referentShp) of Just r -> pure r Nothing -> panic "setupPrePointsTos" [ "Unexpected type mismatch between reference and referent" - , "Reference type: " ++ show (mp^.mpType) - , "Referent type: " ++ show (shapeType referentTy) + , "Reference type: " ++ show referenceInnerTy + , "Referent type: " ++ show (shapeType referentShp) ] - Mir.writeMirRefIO bak globals Mir.mirIntrinsicTypes (mp^.mpRef) referentVal + Mir.writeMirRefIO bak globals Mir.mirIntrinsicTypes referenceVal referentVal -- | Collects boolean terms that should be assumed to be true. setupPrestateConditions :: @@ -1100,7 +1108,6 @@ setupCrucibleContext rm = data MIRSetupError = MIRFreshVarInvalidType Mir.Ty - | MIRPointsToNonReference SetupValue | MIRArgTypeMismatch Int Mir.Ty Mir.Ty -- argument position, expected, found | MIRArgNumberWrong Int Int -- number expected, number found | MIRReturnUnexpected Mir.Ty -- found @@ -1115,11 +1122,6 @@ instance Show MIRSetupError where case err of MIRFreshVarInvalidType jty -> "mir_fresh_var: Invalid type: " ++ show jty - MIRPointsToNonReference ptr -> - unlines - [ "mir_points_to: Left-hand side is not a valid reference" - , show (MS.ppSetupValue ptr) - ] MIRArgTypeMismatch i expected found -> unlines [ "mir_execute_func: Argument type mismatch" diff --git a/src/SAWScript/Crucible/MIR/MethodSpecIR.hs b/src/SAWScript/Crucible/MIR/MethodSpecIR.hs index 87e4cc430a..1233e548bc 100644 --- a/src/SAWScript/Crucible/MIR/MethodSpecIR.hs +++ b/src/SAWScript/Crucible/MIR/MethodSpecIR.hs @@ -65,8 +65,8 @@ mccSym :: Getter MIRCrucibleContext Sym mccSym = to (\mcc -> mccWithBackend mcc backendGetSym) instance PP.Pretty MirPointsTo where - pretty (MirPointsTo _md alloc sv) = PP.parens $ - PP.pretty (show alloc) PP.<+> "->" PP.<+> PP.list (map MS.ppSetupValue sv) + pretty (MirPointsTo _md ref sv) = PP.parens $ + MS.ppSetupValue ref PP.<+> "->" PP.<+> PP.list (map MS.ppSetupValue sv) type MIRMethodSpec = MS.CrucibleMethodSpecIR MIR diff --git a/src/SAWScript/Crucible/MIR/Override.hs b/src/SAWScript/Crucible/MIR/Override.hs index e488ecd1a5..7192bfa7db 100644 --- a/src/SAWScript/Crucible/MIR/Override.hs +++ b/src/SAWScript/Crucible/MIR/Override.hs @@ -30,6 +30,7 @@ import qualified Data.Parameterized.Context as Ctx import Data.Parameterized.Some (Some(..)) import qualified Data.Parameterized.TraversableFC as FC import qualified Data.Set as Set +import Data.Set (Set) import qualified Data.Vector as V import Data.Void (absurd) import qualified Prettyprinter as PP @@ -242,16 +243,29 @@ learnPointsTo :: MS.PrePost -> MirPointsTo -> OverrideMatcher MIR w () -learnPointsTo opts sc cc spec prepost (MirPointsTo md allocIdx referents) = +learnPointsTo opts sc cc spec prepost (MirPointsTo md reference referents) = mccWithBackend cc $ \bak -> do let col = cc ^. mccRustModule . Mir.rmCS ^. Mir.collection globals <- OM (use overrideGlobals) - Some mp <- resolveAllocIndexMIR allocIdx - let mpMirTy = mp^.mpMirType - let mpTpr = tyToShapeEq col mpMirTy (mp^.mpType) - val <- firstPointsToReferent referents - v <- liftIO $ Mir.readMirRefIO bak globals Mir.mirIntrinsicTypes (mp^.mpType) (mp^.mpRef) - matchArg opts sc cc spec prepost md (MIRVal mpTpr v) mpMirTy val + MIRVal referenceShp referenceVal <- + resolveSetupValueMIR opts cc sc spec reference + -- By the time we reach here, we have already checked (in mir_points_to) + -- that we are in fact dealing with a reference value, so the call to + -- `testRefShape` below should always succeed. + IsRefShape _ referenceInnerMirTy _ referenceInnerTpr <- + case testRefShape referenceShp of + Just irs -> pure irs + Nothing -> + panic "learnPointsTo" + [ "Unexpected non-reference type:" + , show $ PP.pretty $ shapeMirTy referenceShp + ] + let innerShp = tyToShapeEq col referenceInnerMirTy referenceInnerTpr + referentVal <- firstPointsToReferent referents + v <- liftIO $ Mir.readMirRefIO bak globals Mir.mirIntrinsicTypes + referenceInnerTpr referenceVal + matchArg opts sc cc spec prepost md (MIRVal innerShp v) + referenceInnerMirTy referentVal -- | Process a "crucible_precond" statement from the precondition -- section of the CrucibleSetup block. @@ -423,12 +437,29 @@ matchPointsTos opts sc cc spec prepost = go False [] -- determine if a precondition is ready to be checked checkPointsTo :: MirPointsTo -> OverrideMatcher MIR w Bool - checkPointsTo (MirPointsTo _ allocIdx _) = checkAllocIndex allocIdx + checkPointsTo (MirPointsTo _ ref _) = checkSetupValue ref - checkAllocIndex :: AllocIndex -> OverrideMatcher MIR w Bool - checkAllocIndex i = + checkSetupValue :: SetupValue -> OverrideMatcher MIR w Bool + checkSetupValue v = do m <- OM (use setupValueSub) - return (Map.member i m) + return (all (`Map.member` m) (setupVars v)) + + -- Compute the set of variable identifiers in a 'SetupValue' + setupVars :: SetupValue -> Set AllocIndex + setupVars v = + case v of + MS.SetupVar i -> Set.singleton i + MS.SetupStruct _ xs -> foldMap setupVars xs + MS.SetupTuple _ xs -> foldMap setupVars xs + MS.SetupArray _ xs -> foldMap setupVars xs + MS.SetupElem _ x _ -> setupVars x + MS.SetupField _ x _ -> setupVars x + MS.SetupTerm _ -> Set.empty + MS.SetupCast empty _ -> absurd empty + MS.SetupUnion empty _ _ -> absurd empty + MS.SetupNull empty -> absurd empty + MS.SetupGlobal empty _ -> absurd empty + MS.SetupGlobalInitializer empty _ -> absurd empty matchTerm :: SharedContext {- ^ context for constructing SAW terms -} -> @@ -499,11 +530,6 @@ readPartExprMaybe _sym (W4.PE p v) | Just True <- W4.asConstantPred p = Just v | otherwise = Nothing -resolveAllocIndexMIR :: AllocIndex -> OverrideMatcher MIR w (Some (MirPointer Sym)) -resolveAllocIndexMIR i = - do m <- OM (use setupValueSub) - pure $ lookupAllocIndex m i - resolveSetupValueMIR :: Options -> MIRCrucibleContext -> diff --git a/src/SAWScript/Crucible/MIR/Setup/Value.hs b/src/SAWScript/Crucible/MIR/Setup/Value.hs index 9aca21d93f..5e34c624e3 100644 --- a/src/SAWScript/Crucible/MIR/Setup/Value.hs +++ b/src/SAWScript/Crucible/MIR/Setup/Value.hs @@ -99,7 +99,7 @@ type instance MS.Pointer' MIR sym = Some (MirPointer sym) -- referenced by the slice. The @mir_points_to@ command, on the other hand, -- always creates 'MirPointsTo' values with exactly one value in the list (see -- the @firstPointsToReferent@ function in "SAWScript.Crucible.MIR.Override"). -data MirPointsTo = MirPointsTo MS.ConditionMetadata MS.AllocIndex [MS.SetupValue MIR] +data MirPointsTo = MirPointsTo MS.ConditionMetadata (MS.SetupValue MIR) [MS.SetupValue MIR] deriving (Show) data MirAllocSpec tp = MirAllocSpec diff --git a/src/SAWScript/Crucible/MIR/TypeShape.hs b/src/SAWScript/Crucible/MIR/TypeShape.hs index 5fed734473..47e845e01d 100644 --- a/src/SAWScript/Crucible/MIR/TypeShape.hs +++ b/src/SAWScript/Crucible/MIR/TypeShape.hs @@ -18,6 +18,8 @@ module SAWScript.Crucible.MIR.TypeShape , shapeMirTy , fieldShapeMirTy , shapeToTerm + , IsRefShape(..) + , testRefShape ) where import Control.Lens ((^.), (^..), each) @@ -251,6 +253,27 @@ shapeToTerm sc = go goField (OptField shp) = go shp goField (ReqField shp) = go shp +-- | A witness that a 'TypeShape' is equal to a 'RefShape'. +data IsRefShape (tp :: CrucibleType) where + IsRefShape :: M.Ty + -- ^ The reference type + -> M.Ty + -- ^ The pointee type + -> M.Mutability + -- ^ Is the reference mutable or immutable? + -> TypeRepr tp + -- ^ The Crucible representation of the pointee type + -> IsRefShape (MirReferenceType tp) + +-- | Check that a 'TypeShape' is equal to a 'RefShape'. If so, return 'Just' a +-- witness of that equality. Otherwise, return 'Nothing'. +testRefShape :: TypeShape tp -> Maybe (IsRefShape tp) +testRefShape shp = + case shp of + RefShape ty ty' mut shp' + -> Just $ IsRefShape ty ty' mut shp' + _ -> Nothing + $(pure []) instance TestEquality TypeShape where