Refactor: Make MirPointsTo accept a SetupValue, not an AllocIndex

In an upcoming commit, we will want to be able to write things such as
`mir_points_to (mir_global "X") ...`. This isn't currently possible with the
way `MirPointsTo` is currently designed, as it expects the left-hand side of a
`mir_points_to` statement to always be an `AllocIndex`, i.e., something created
via `mir_alloc`/`mir_alloc_mut`. This patch generalizes the `AllocIndex` field
in `MirPointsTo` to a `SetupValue` to allow other forms of references to be
used in `mir_points_to` statements.

In most places, this is a simple matter of wrapping the `AllocIndex` in a
`SetupVar`.  It was slightly tricky to update the code in `crucible-mir-comp`
to accommodate this, as that code relies on a subtle assumption about the
left-hand sides of `MirPointsTo` values only originating from `SetupVar`s. I
have documented this assumption in the new `setupVarAllocIndex` function.

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

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)

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"

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
 

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   ->

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

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