`mir_slice_value` and `mir_slice_range_value` #1948

RyanGlScott · 2023-09-22T22:21:03Z

This adds mir_slice_value and mir_slice_range_value functions to the MIR backend, which allow writing specifications involving slice arguments. Currently, only slices to array references are supported, although we may expand the scope of these commands in the future.

Some interesting parts of the implementation:

The TypeShape for slices is ever-so-slightly different from the TypeShape for tuples (TupleShape), so I added a new SliceShape TypeShape to tell them apart.
There is a MirSetupSliceRaw constructor that is only used for crucible-mir-comp purposes at the moment. In the future, we may want to expose a SAWScript command that uses this to allow users to directly construct a slice from a pointer and a length.
mir_alloc now explicitly disallows allocating slice references, so passing mir_slice or mir_str as an argument will throw an error.

This checks off one box in #1859.

RyanGlScott · 2023-09-22T22:22:28Z

src/SAWScript/Crucible/MIR/TypeShape.hs

+    --
+    -- To make it easier to recurse on the 'TypeShape's for the slice's
+    -- reference and length types, we provide the 'sliceShapeParts' function.
+    SliceShape :: M.Ty


Note the new addition of SliceShape, which is distinct from TupleShape.

RyanGlScott · 2023-09-22T22:23:05Z

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

+-- | A slice-related MIR 'SetupValue'.
+data MirSetupSlice
+  = MirSetupSliceRaw (MS.SetupValue MIR) (MS.SetupValue MIR)
+    -- ^ A \"raw\" slice constructed directly from a pointer and a length.
+    -- Currently, this is only used by @crucible-mir-comp@. SAWScript offers no
+    -- way to use this, although we may consider doing so in the future.
+  | MirSetupSlice (MS.SetupValue MIR)
+    -- ^ A slice of a reference to a contiguous sequence 'SetupValue'.
+    -- Currently, this only supports references to arrays.
+  | MirSetupSliceRange (MS.SetupValue MIR) Int Int
+    -- ^ A slice of a reference to a contiguous sequence 'SetupValue', where the
+    -- slice only covers the range specified by the given start and end values
+    -- (the first and second 'Int', respectively). Currently, this only
+    -- supports references to arrays, and it only supports concrete ranges.


An important new data type that classifies all of the different ways one can construct slice values in SAW/crucible-mir-comp.

RyanGlScott · 2023-09-22T22:23:40Z

src/SAWScript/Crucible/MIR/ResolveSetupValue.hs

+        MirSetupSliceRaw{} ->
+          panic "typeOfSetupValue" ["MirSetupSliceRaw not yet implemented"]


MirSetupSliceRaw is only used in crucible-mir-comp at the moment, so I didn't bother implemented support for it in SAW.

RyanGlScott · 2023-09-22T22:24:24Z

src/SAWScript/Crucible/MIR/ResolveSetupValue.hs

+        MirSetupSlice arrRef -> do
+          SetupSliceFromArray _elemTpr sliceShp refVal len <-
+            resolveSetupSliceFromArray bak arrRef
+          lenVal <- usizeBvLit sym len
+          pure $ MIRVal sliceShp (Ctx.Empty Ctx.:> RV refVal Ctx.:> RV lenVal)
+        MirSetupSliceRange arrRef start end -> do
+          unless (start <= end) $
+            fail $ "slice index starts at " ++ show start
+                ++ " but ends at " ++ show end
+          SetupSliceFromArray elemTpr sliceShp refVal0 len <-
+            resolveSetupSliceFromArray bak arrRef
+          unless (end < len) $
+            fail $ "range end index " ++ show end
+                ++ " out of range for slice of length " ++ show len
+          startBV <- usizeBvLit sym start
+          refVal1 <- Mir.mirRef_offsetIO bak iTypes elemTpr refVal0 startBV
+          lenVal <- usizeBvLit sym $ end - start
+          pure $ MIRVal sliceShp (Ctx.Empty Ctx.:> RV refVal1 Ctx.:> RV lenVal)


This is where the magic happens, such as interfacing with the crucible-mir memory model and checking the start/end values of slice ranges.

RyanGlScott · 2023-09-22T22:25:05Z

doc/manual/manual.md

@@ -2648,6 +2650,77 @@ construct compound values:
 * `mir_tuple_value : [MIRValue] -> MIRValue` construct a tuple with the given
  list of values as elements.

+### MIR slices


Documentation

RyanGlScott · 2023-09-25T14:13:16Z

Thinking about this some more, there are a couple of unresolved questions in this PR:

What happens if a user writes mir_alloc (mir_slice ty)? I'm not sure what the semantics of this should be. I suppose we could allocate a slice with a symbolic length, but that goes against the usual SAW philosophy of using fixed-length sequence types whenever possible. Perhaps mir_alloc (mir_slice ty) should just throw an explicit error? Or maybe we should offer an alternative mir_alloc_slice <ty> <len> command for this purpose?
This PR doesn't provide users any way to create &str slices. Indeed, I'm not sure what user interface we'd want to provide for str. I suppose we could allow users to create str references from values of type [u8; N], but this would require users to be very aware of UTF-8 particulars (e.g., a slice of the string "💖" would have to be created from the array [240, 159, 146, 150]). Not to mention that I'm not sure if we'd want to allow things like mir_elem str 1, since Rust generally forbids indexing into strings...

RyanGlScott · 2023-10-09T23:17:40Z

Thinking about this some more:

We disallow mir_alloc (mir_slice ty), since it is unclear what its semantics should be. I also don't think we need to add a special mir_alloc_slice command, as I don't think it would provide much value.
I'm going to punt on the question of string slices for now, as that is a can of worms that I don't want to open just yet. Let's make mir_alloc mir_str an error, just like with mir_alloc (mir_slice ty).

RyanGlScott · 2023-10-10T14:40:58Z

I've implemented the ideas in #1948 (comment), so this is now ready for review.

RyanGlScott · 2023-10-10T21:04:23Z

I've realized that mir_slice_value arr_ref always produces a slice with the same mutability as the underlying arr_ref. A consequence of this is that there is no way to obtain an immutable slice of a mutable array, even though such a thing is possible in Rust. I imagine that we will want to be able to do this, so I think we will need a _mut counterpart to mir_slice_value (and mir_slice_range_value), with the stipulation that you cannot call mir_slice_mut_value on an immutable array.

spernsteiner · 2023-10-10T21:08:59Z

In general, it might be nice to have a way to cast &mut T to &T in SAWscript. Then you could cast before calling mir_slice_value if needed.

RyanGlScott · 2023-10-10T21:16:44Z

Ah, I like that idea better. A casting function would also be handy if you wanted to take an immutable slice of a static mut array value. The alternative would be to add something like mir_static_immut_ref_of_mut, which would be kind of ridiculous.

RyanGlScott · 2023-10-11T14:15:58Z

I've opened #1954 to track this idea. This idea can be implemented separately and applies to more things than just slices, so I don't think we need to hold up this PR while we wait for that.

spernsteiner

Looks generally good, except for some confusion around half-open vs inclusive ranges in mir_slice_range_value. It should use half-open for consistency with Rust, where arr[start..end] is much more common than the inclusive version arr[start..=end].

I'm not entirely clear on why we need a separate SliceShape when it's a strict subset of StructShape, but it doesn't seem like it was much trouble to introduce this distinction.

doc/manual/manual.md

intTests/test_mir_verify_slices/test.saw

src/SAWScript/Crucible/MIR/ResolveSetupValue.hs

src/SAWScript/Interpreter.hs

This adds `mir_slice_value` and `mir_slice_range_value` functions to the MIR backend, which allow writing specifications involving slice arguments. Currently, only slices to array references are supported, although we may expand the scope of these commands in the future. Some interesting parts of the implementation: 1. The `TypeShape` for slices is _ever_-so-slightly different from the `TypeShape` for tuples (`TupleShape`), so I added a new `SliceShape` `TypeShape` to tell them apart. 2. There is a `MirSetupSliceRaw` constructor that is _only_ used for `crucible-mir-comp` purposes at the moment. In the future, we may want to expose a SAWScript command that uses this to allow users to directly construct a slice from a pointer and a length. 3. `mir_alloc` now explicitly disallows allocating slice references, so passing `mir_slice` or `mir_str` as an argument will throw an error. This checks off one box in #1859.

spernsteiner

If all the half-open range stuff is fixed, then I think this is good to merge.

RyanGlScott requested a review from spernsteiner September 22, 2023 22:21

RyanGlScott mentioned this pull request Sep 22, 2023

Support Rust verification in SAW via crucible-mir #1859

Closed

29 tasks

RyanGlScott commented Sep 22, 2023

View reviewed changes

RyanGlScott mentioned this pull request Sep 27, 2023

Start a SAW Rust verification tutorial #1939

Merged

RyanGlScott force-pushed the T1859-mir-slices branch from ab0b82e to 9fa9f7f Compare October 10, 2023 14:40

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

RyanGlScott marked this pull request as draft October 10, 2023 21:04

RyanGlScott mentioned this pull request Oct 11, 2023

Add mir_cast_to_immut_ref function #1954

Open

RyanGlScott marked this pull request as ready for review October 11, 2023 14:16

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

RyanGlScott force-pushed the T1859-mir-slices branch from 9fa9f7f to 091a94e Compare October 13, 2023 13:45

spernsteiner reviewed Nov 2, 2023

View reviewed changes

RyanGlScott added 2 commits November 4, 2023 15:50

Review comments

813b844

RyanGlScott force-pushed the T1859-mir-slices branch from 091a94e to 813b844 Compare November 4, 2023 20:31

RyanGlScott requested a review from spernsteiner November 4, 2023 20:32

spernsteiner approved these changes Nov 6, 2023

View reviewed changes

RyanGlScott added the PR: ready to merge Magic flag for pull requests to ask Mergify to merge given an approval and a successful CI run label Nov 6, 2023

mergify bot merged commit 67ef60c into master Nov 6, 2023
39 checks passed

mergify bot deleted the T1859-mir-slices branch November 6, 2023 17:40

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

`mir_slice_value` and `mir_slice_range_value` #1948

`mir_slice_value` and `mir_slice_range_value` #1948

RyanGlScott commented Sep 22, 2023 •

edited

Loading

RyanGlScott Sep 22, 2023

RyanGlScott Sep 22, 2023

RyanGlScott Sep 22, 2023

RyanGlScott Sep 22, 2023

RyanGlScott Sep 22, 2023

RyanGlScott commented Sep 25, 2023 •

edited

Loading

RyanGlScott commented Oct 9, 2023

RyanGlScott commented Oct 10, 2023

RyanGlScott commented Oct 10, 2023

spernsteiner commented Oct 10, 2023

RyanGlScott commented Oct 10, 2023

RyanGlScott commented Oct 11, 2023

spernsteiner left a comment

spernsteiner left a comment

		MirSetupSliceRaw{} ->
		panic "typeOfSetupValue" ["MirSetupSliceRaw not yet implemented"]

mir_slice_value and mir_slice_range_value #1948

mir_slice_value and mir_slice_range_value #1948

Conversation

RyanGlScott commented Sep 22, 2023 • edited Loading

RyanGlScott Sep 22, 2023

Choose a reason for hiding this comment

RyanGlScott Sep 22, 2023

Choose a reason for hiding this comment

RyanGlScott Sep 22, 2023

Choose a reason for hiding this comment

RyanGlScott Sep 22, 2023

Choose a reason for hiding this comment

RyanGlScott Sep 22, 2023

Choose a reason for hiding this comment

RyanGlScott commented Sep 25, 2023 • edited Loading

RyanGlScott commented Oct 9, 2023

RyanGlScott commented Oct 10, 2023

RyanGlScott commented Oct 10, 2023

spernsteiner commented Oct 10, 2023

RyanGlScott commented Oct 10, 2023

RyanGlScott commented Oct 11, 2023

spernsteiner left a comment

Choose a reason for hiding this comment

spernsteiner left a comment

Choose a reason for hiding this comment

`mir_slice_value` and `mir_slice_range_value` #1948

`mir_slice_value` and `mir_slice_range_value` #1948

RyanGlScott commented Sep 22, 2023 •

edited

Loading

RyanGlScott commented Sep 25, 2023 •

edited

Loading