Support mir_alloc, mir_alloc_mut, and mir_points_to
#1916
Conversation
This patch adds support for specifying the memory layouts of allocations in MIR specifications through the following commands: * `mir_alloc`, which allocates an immutable reference, and `mir_alloc_mut`, which allocates a mutable reference. * `mir_points_to`, which declares that a reference points to a given value in a pre- or post-condition. These commands behave much like `llvm_alloc` and `llvm_points_to`, and the code for the MIR commands looks quite similar to the LLVM code as a result. The largest difference implementation-wise is that I need to call into the `crucible-mir` memory model in order to read values from and write values to references. This patch therefore bumps the `crucible` submodule to bring in the changes from GaloisInc/crucible#1105, which make it much more straightforward to use the `crucible-mir` memory model in a SAW setting. Along the way, this patch also performs some mild refactoring: * This adds a `ConditionMetadata` field to `MirPointsTo` for the benefit of using it in `learnPointsTo`. This required moving around some `ConditionMetadata` values in `crucible-mir-comp` as a result. * This moves the `CheckPointsToType` data type from `SAWScript.Crucible.LLVM.Builtins` to `SAWScript.Crucible.Common.Setup.Builtins`. This is because `CheckPointsToType` is now used in the `saw-remote-api` code that powers `mir_points_to` (see `SAWServer.MIRCrucibleSetup`), and it doesn't make much sense for this code to import LLVM-specific code. This checks off one box in #1859.
There was a problem hiding this comment.
Like with #1904, much of this code is mechanically adapted from the LLVM/JVM backends. I've made an effort to highlight the interesting bits that are MIR-specific.
| case refTy of | ||
| Mir.TyRef referentTy _ -> pure referentTy | ||
| _ -> throwCrucibleSetup loc $ "lhs not a reference type: " ++ show refTy |
There was a problem hiding this comment.
This code checks if the reference passed to mir_points_to is actually a reference type.
| , "Reference type: " ++ show (mp^.mpType) | ||
| , "Referent type: " ++ show (shapeType referentTy) | ||
| ] | ||
| Mir.writeMirRefIO bak globals Mir.mirIntrinsicTypes (mp^.mpRef) referentVal |
There was a problem hiding this comment.
This is one of the places in the patch that involves the crucible-mir memory model. Here, we write the right-hand side values for each mir_points_to statement in a specification's preconditions.
| -- | Allocate memory for each 'mir_alloc' or 'mir_alloc_mut'. | ||
| doAlloc :: | ||
| MIRCrucibleContext | ||
| -> Some MirAllocSpec | ||
| -> StateT (Crucible.SymGlobalState Sym) IO (Some (MirPointer Sym)) | ||
| doAlloc cc (Some ma) = | ||
| mccWithBackend cc $ \bak -> | ||
| do let col = cc ^. mccRustModule ^. Mir.rmCS ^. Mir.collection | ||
| let halloc = cc^.mccHandleAllocator | ||
| let sym = backendGetSym bak | ||
| let iTypes = Mir.mirIntrinsicTypes | ||
| Some tpr <- pure $ Mir.tyToRepr col (ma^.maMirType) | ||
|
|
||
| -- Create an uninitialized `MirVector_PartialVector` of length 1 and | ||
| -- return a pointer to its element. | ||
| ref <- liftIO $ | ||
| Mir.newMirRefIO sym halloc (Mir.MirVectorRepr tpr) | ||
|
|
||
| globals <- get | ||
| globals' <- liftIO $ do | ||
| one <- W4.bvLit sym W4.knownRepr $ BV.mkBV W4.knownRepr 1 | ||
| vec <- Mir.mirVector_uninitIO bak one | ||
| Mir.writeMirRefIO bak globals iTypes ref vec | ||
| put globals' | ||
|
|
||
| ptr <- liftIO $ do | ||
| zero <- W4.bvLit sym W4.knownRepr $ BV.mkBV W4.knownRepr 0 | ||
| Mir.subindexMirRefIO bak iTypes tpr ref zero | ||
| pure $ Some MirPointer | ||
| { _mpType = tpr | ||
| , _mpMutbl = ma^.maMutbl | ||
| , _mpMirType = ma^.maMirType | ||
| , _mpRef = ptr | ||
| } |
There was a problem hiding this comment.
This is where most of the magic powering mir_alloc{,_mut} happens. Using the crucible-mir memory model, this allocates a fresh reference, writes uninitialized memory to it, and returns the resulting pointer. This code was largely inspired by similar code in crucible-mir.
| -- | Unlike @LLVMPointsTo@ and @JVMPointsTo@, 'MirPointsTo' contains a /list/ of | ||
| -- 'MS.SetupValue's on the right-hand side. This is due to how slices are | ||
| -- represented in @crucible-mir-comp@, which stores the list of values | ||
| -- 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"). |
There was a problem hiding this comment.
I added this comment here...
| -- | @mir_points_to@ always creates a 'MirPointsTo' value with exactly one | ||
| -- referent on the right-hand side. As a result, this function should never | ||
| -- fail. | ||
| firstPointsToReferent :: | ||
| MonadFail m => [MS.SetupValue MIR] -> m (MS.SetupValue MIR) | ||
| firstPointsToReferent referents = | ||
| case referents of | ||
| [referent] -> pure referent | ||
| _ -> fail $ | ||
| "Unexpected mir_points_to statement with " ++ show (length referents) ++ | ||
| " referent(s)" |
There was a problem hiding this comment.
...to justify what this code is doing.
| 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) |
There was a problem hiding this comment.
The final place in the patch that makes use of the crucible-mir memory model, this time to read from a reference.
| -------------------------------------------------------------------------------- | ||
| -- ** Shared data types | ||
|
|
||
| -- | When invoking a points-to command, against what should SAW check the type | ||
| -- of the RHS value? | ||
| data CheckPointsToType ty | ||
| = CheckAgainstPointerType | ||
| -- ^ Check the type of the RHS value against the type that the LHS points to. | ||
| -- Used by commands such as @llvm_{conditional_}points_to@ and | ||
| -- @mir_points_to@. | ||
| | CheckAgainstCastedType ty | ||
| -- ^ Check the type of the RHS value against the provided @ty@, which | ||
| -- the LHS pointer is casted to. | ||
| -- This is currently used by @llvm_{conditional_}points_to_at_type@ only. | ||
| deriving (Functor, Foldable, Traversable) |
There was a problem hiding this comment.
Reviewers' note: this isn't new code, but rather code that was moved from SAWScript.Crucible.LLVM.Builtins. This data type is now used in the MIR-related code in saw-remote-api, so it no longer made sense for it to live in an LLVM-specific module.
There was a problem hiding this comment.
This looks reasonable to me, including all the MIR memory model integration.
I was worried that the current approach of extracting MIR types from SetupValues wouldn't be sufficient for handling slices, but that will be addressed by #1914.
RyanGlScott
added
the
PR: ready to merge
This patch adds support for specifying the memory layouts of allocations in MIR specifications through the following commands:
mir_alloc, which allocates an immutable reference, andmir_alloc_mut, which allocates a mutable reference.mir_points_to, which declares that a reference points to a given value in a pre- or post-condition.These commands behave much like
llvm_allocandllvm_points_to, and the code for the MIR commands looks quite similar to the LLVM code as a result. The largest difference implementation-wise is that I need to call into thecrucible-mirmemory model in order to read values from and write values to references. This patch therefore bumps thecruciblesubmodule to bring in the changes from GaloisInc/crucible#1105, which make it much more straightforward to use thecrucible-mirmemory model in a SAW setting.Along the way, this patch also performs some mild refactoring:
ConditionMetadatafield toMirPointsTofor the benefit of using it inlearnPointsTo. This required moving around someConditionMetadatavalues incrucible-mir-compas a result.CheckPointsToTypedata type fromSAWScript.Crucible.LLVM.BuiltinstoSAWScript.Crucible.Common.Setup.Builtins. This is becauseCheckPointsToTypeis now used in thesaw-remote-apicode that powersmir_points_to(seeSAWServer.MIRCrucibleSetup), and it doesn't make much sense for this code to import LLVM-specific code.This checks off one box in #1859.