`mir_static` and `mir_static_initializer` #1941

RyanGlScott · 2023-09-18T14:18:52Z

This adds support for the mir_static and mir_static_initializer functions in the MIR backend, which are used to write specifications involving top-level static values. These behave like the llvm_global and llvm_global_initializer functions in the LLVM backend, but with the following differences:

There is nor MIR counterpart to the llvm_alloc_global command, as MIR static values are not "allocated" in the same way that LLVM globals are. (We still require users to initialize mutable MIR statics, however.)
By design, static references created with mir_static cannot alias allocations created with mir_alloc, as the two forms of allocations are handled through different mechanisms in the crucible-mir memory model.

This checks off one box in #1859.

RyanGlScott

Here are the highlights of the patch:

RyanGlScott · 2023-09-18T14:20:46Z

src/SAWScript/Crucible/MIR/Setup/Value.hs

 -- | 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").
-data MirPointsTo = MirPointsTo MS.ConditionMetadata MS.AllocIndex [MS.SetupValue MIR]
+data MirPointsTo = MirPointsTo MS.ConditionMetadata (MS.SetupValue MIR) [MS.SetupValue MIR]


The first commit in this PR is all about this change, where we represent the reference value in a MirPointsTo statement with a SetupValue instead of an AllocIndex. This is required to support things like mir_points_to (mir_static ...) ..., as mir_static references do not have an AllocIndex. There is a bit of code churn that results from this change, but it's mostly straightforward. (I'll note one exception in another inline comment.)

RyanGlScott · 2023-09-18T14:21:54Z

crucible-mir-comp/src/Mir/Compositional/Override.hs

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


This is the one part of crucible-mir-comp that was somewhat tricky to adapt to the AllocIndex -> SetupValue change. I believe it should be safe here to assume that this particular class of SetupValues should always be SetupVars (which have an AllocIndex), but please double-check my understanding here.

That sounds right to me, and matches the changes I see elsewhere in the diff.

RyanGlScott · 2023-09-18T14:22:35Z

doc/manual/manual.md

@@ -2892,6 +2896,68 @@ point of a call to `f`. This specification also constrains `y` to prevent
 signed integer overflow resulting from the `x + y` expression in `f`,
 which is undefined behavior in C.

+### MIR static items


The documentation for mir_static and mir_static_initializer. There is more that could be said here about how mutable static items interact with overrides, but I need to implement overrides first before I can meaningfully talk about this :)

RyanGlScott · 2023-09-18T14:24:22Z

src/SAWScript/Crucible/MIR/Builtins.hs

                               }

+{-
+Note [Translating MIR statics in SAW]


Translating static items is a somewhat involved process, so I wrote up a high-level description of this works in this Note.

RyanGlScott · 2023-09-18T14:24:47Z

src/SAWScript/Crucible/MIR/Builtins.hs

+     -- There is quite a bit of faff below, all for the sake of translating
+     -- top-level static values. See Note [Translating MIR statics in SAW] for
+     -- a high-level description of what this code is doing.


The code below here is the implementation of Note [Translating MIR statics in SAW].

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.

spernsteiner

Looks generally reasonable to me.

spernsteiner · 2023-10-12T16:50:22Z

doc/manual/manual.md

+command, just like with other forms of references. Immutable static items
+(e.g., `static X: u8 = 42`) are initialized implicitly in every SAW
+specification, so there is no need for users to do so manually. Mutable static
+items (e.g., `static mut Y: u8 = 27`), on the other hand, are *not* initialized
+implicitly, and users must explicitly pick a value to initialize them with.


Eventually, this logic should be updated to treat statics that are non-mut but also non-Freeze statics, such as static Z: AtomicU8 = ...;, the same way we treat mut statics. These statics get compiled to mutable LLVM globals, and the values stored there can be modified at run time.

I've opened #1957 for this.

intTests/test_mir_statics/test.rs

saw-remote-api/python/tests/saw/test-files/mir_statics.rs

spernsteiner · 2023-10-12T18:16:29Z

crucible-mir-comp/src/Mir/Compositional/Override.hs

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


That sounds right to me, and matches the changes I see elsewhere in the diff.

This adds support for the `mir_static` and `mir_static_initializer` functions in the MIR backend, which are used to write specifications involving top-level `static` values. These behave like the `llvm_global` and `llvm_global_initializer` functions in the LLVM backend, but with the following differences: 1. There is nor MIR counterpart to the `llvm_alloc_global` command, as MIR static values are not "allocated" in the same way that LLVM globals are. (We still require users to initialize mutable MIR statics, however.) 2. By design, static references created with `mir_static` cannot alias allocations created with `mir_alloc`, as the two forms of allocations are handled through different mechanisms in the `crucible-mir` memory model. This checks off one box in #1859.

RyanGlScott requested a review from spernsteiner September 18, 2023 14:18

RyanGlScott commented Sep 18, 2023

View reviewed changes

This was referenced Sep 22, 2023

Support Rust verification in SAW via crucible-mir #1859

Closed

Start a SAW Rust verification tutorial #1939

Merged

RyanGlScott force-pushed the T1859-mir-globals branch from 2c38dd4 to c6af1c3 Compare October 10, 2023 14:43

RyanGlScott requested a review from bboston7 October 10, 2023 14:43

RyanGlScott mentioned this pull request Oct 11, 2023

Add mir_cast_to_immut_ref function #1954

Open

RyanGlScott requested a review from andreistefanescu October 11, 2023 16:48

spernsteiner approved these changes Oct 12, 2023

View reviewed changes

RyanGlScott mentioned this pull request Oct 12, 2023

MIR: Require users to initialize Freeze statics in specifications #1957

Open

RyanGlScott force-pushed the T1859-mir-globals branch from c6af1c3 to b0e7c25 Compare October 12, 2023 18:55

RyanGlScott added the ready-to-merge If at least one person approves this PR, automatically merge it when CI finishes successfully. label Oct 12, 2023

mergify bot merged commit 46341c2 into master Oct 12, 2023
40 checks passed

mergify bot deleted the T1859-mir-globals branch October 12, 2023 20:27

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

`mir_static` and `mir_static_initializer` #1941

`mir_static` and `mir_static_initializer` #1941

RyanGlScott commented Sep 18, 2023

RyanGlScott left a comment

RyanGlScott Sep 18, 2023

RyanGlScott Sep 18, 2023

spernsteiner Oct 12, 2023

RyanGlScott Sep 18, 2023

RyanGlScott Sep 18, 2023

RyanGlScott Sep 18, 2023

spernsteiner left a comment

spernsteiner Oct 12, 2023

RyanGlScott Oct 12, 2023

spernsteiner Oct 12, 2023

mir_static and mir_static_initializer #1941

mir_static and mir_static_initializer #1941

Conversation

RyanGlScott commented Sep 18, 2023

RyanGlScott left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

spernsteiner left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

`mir_static` and `mir_static_initializer` #1941

`mir_static` and `mir_static_initializer` #1941