Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Mir.Intrinsics functions use SimState when SymGlobalState/IntrinsicTypes would suffice #1105

Closed
RyanGlScott opened this issue Aug 21, 2023 · 1 comment · Fixed by #1106
Closed
Assignees
Labels
crucible MIR Issues relating to Rust/MIR support technical debt

Comments

@RyanGlScott
Copy link
Contributor

While working on the Rust SAW backend (see GaloisInc/saw-script#1859), I discovered that the cruible-mir memory model–related functions in Mir.Intrinsics have types that are too specific for SAW's needs. Here is one example of such a type:

writeRefRoot :: forall p sym bak ext rtp f a tp.
(IsSymBackend sym bak) =>
SimState p sym ext rtp f a ->
bak ->
MirReferenceRoot sym tp ->
RegValue sym tp ->
MuxLeafT sym IO (SimState p sym ext rtp f a)

SAW needs to write to references as part of the implementation of some of its MIR-related commands, and it ends up calling this function at some point. Or, at the very least, it should call this function, but there is a catch: it requires a SimState as an argument. This is inconvenient for SAW's needs, as the setup-related code that it uses to install MIR specifications doesn't have easy access to a SimState. (It does have access to a SimState when actually simulating the code, but that happens much later in the pipeline.)

What's more, I don't think functions like writeRefRoot even need to use SimState. If you look at the function's implementation:

writeRefRoot s bak (RefCell_RefRoot rc) v = do
let sym = backendGetSym bak
let iTypes = ctxIntrinsicTypes $ s^.stateContext
let gs = s ^. stateTree . actFrame . gpGlobals
let tpr = refType rc
let f p a b = liftIO $ muxRegForType sym iTypes tpr p a b
let oldv = lookupRef rc gs
newv <- leafUpdatePartExpr bak f v oldv
return $ s & stateTree . actFrame . gpGlobals %~ updateRef rc newv

The only parts of the SimState that the function ever uses are the SymGlobalState and IntrinsicTypes. Indeed, this is a pattern that holds for nearly every function in Mir.Intrinsics that currently uses SimState. We could just as well refactor writeRefRoot to have this type signature:

writeRefRoot :: forall sym bak tp.
    (IsSymBackend sym bak) =>
    bak ->
    SymGlobalState sym -> -- new
    IntrinsicTypes sym -> -- new
    MirReferenceRoot sym tp ->
    RegValue sym tp ->
    MuxLeafT sym IO (SymGlobalState sym) -- new

If we did this, then it would be much easier for SAW to call into the crucible-mir memory model.

@RyanGlScott RyanGlScott added crucible technical debt MIR Issues relating to Rust/MIR support labels Aug 21, 2023
@RyanGlScott RyanGlScott self-assigned this Aug 21, 2023
RyanGlScott added a commit to GaloisInc/saw-script that referenced this issue Aug 21, 2023
This is primarily motivated by a need to bring in a fix for
GaloisInc/crucible#1105 into SAW soon. In order to do
this, I will need to bump the `crucible` submodule to a more recent commit, so
this patch lays the groundwork for doing so.
RyanGlScott added a commit to GaloisInc/saw-script that referenced this issue Aug 21, 2023
This is primarily motivated by a need to bring in a fix for
GaloisInc/crucible#1105 into SAW soon. In order to do
this, I will need to bump the `crucible` submodule to a more recent commit, so
this patch lays the groundwork for doing so.

Most of the changes can be brought in directly without any further changes to
SAW.  One exception in `cryptol`, where I had to explicitly initialize
`mInScope` to accommodate the changes from
GaloisInc/cryptol#1559.  Just like how `cryptol`
initializes `mInScope` to `mempty` after parsing a Cryptol `NormalModule`, so
too does SAW.
RyanGlScott added a commit that referenced this issue Aug 22, 2023
…s will suffice

This makes it possible to call into the `crucible-mir` memory model without
needing access to a full-blown `SimState`, which is sometimes not available in
SAW contexts.

Fixes #1105.
RyanGlScott added a commit to GaloisInc/saw-script that referenced this issue Aug 23, 2023
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.
@RyanGlScott
Copy link
Contributor Author

I added a small number of *IO functions in #1106 for a particular SAW patch, but now I need more for another patch. Perhaps this is a sign that I should bite the bullet and add *IO entrypoints for everything in Mir.Intrinsics (or at least everything used in execMirStmt).

RyanGlScott added a commit that referenced this issue Aug 31, 2023
A follow-up to #1105/#1106. I found myself needing `subanyMirRefIO`,
`subfieldMirRefIO`, and `subjustMirRefIO` in an upcoming SAW patch, but to
avoid having to make a bunch of little patches each time I need more things
from the `crucible-mir` memory model, I opted to define `*IO` functions for
each memory model operation that performs side effects. After this patch, it
should be straightforward to call anything in the `crucible-mir` memory model
without too much trouble.
RyanGlScott added a commit that referenced this issue Aug 31, 2023
…1107)

A follow-up to #1105/#1106. I found myself needing `subanyMirRefIO`,
`subfieldMirRefIO`, and `subjustMirRefIO` in an upcoming SAW patch, but to
avoid having to make a bunch of little patches each time I need more things
from the `crucible-mir` memory model, I opted to define `*IO` functions for
each memory model operation that performs side effects. After this patch, it
should be straightforward to call anything in the `crucible-mir` memory model
without too much trouble.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
crucible MIR Issues relating to Rust/MIR support technical debt
Projects
None yet
1 participant