mir_slice_value and mir_slice_range_value

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.

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

@@ -637,6 +637,7 @@ substMethodSpec sc sm ms = do
         MS.SetupNull _ -> return sv
         MS.SetupStruct b svs -> MS.SetupStruct b <$> mapM goSetupValue svs
         MS.SetupTuple b svs -> MS.SetupTuple b <$> mapM goSetupValue svs
+        MS.SetupSlice slice -> MS.SetupSlice <$> goSetupSlice slice
         MS.SetupArray b svs -> MS.SetupArray b <$> mapM goSetupValue svs
         MS.SetupElem b sv idx -> MS.SetupElem b <$> goSetupValue sv <*> pure idx
         MS.SetupField b sv name -> MS.SetupField b <$> goSetupValue sv <*> pure name
@@ -652,6 +653,14 @@ substMethodSpec sc sm ms = do
     goSetupCondition (MS.SetupCond_Ghost b loc gg tt) =
         MS.SetupCond_Ghost b loc gg <$> goTypedTerm tt
 
+    goSetupSlice (MirSetupSliceRaw ref len) =
+      MirSetupSliceRaw <$> goSetupValue ref <*> goSetupValue len
+    goSetupSlice (MirSetupSlice arr) =
+      MirSetupSlice <$> goSetupValue arr
+    goSetupSlice (MirSetupSliceRange arr start end) = do
+      arr' <- goSetupValue arr
+      pure $ MirSetupSliceRange arr' start end
+
     goTypedTerm tt = do
         term' <- goTerm $ SAW.ttTerm tt
         return $ tt { SAW.ttTerm = term' }
@@ -737,6 +746,11 @@ regToSetup bak p eval shp rv = go shp rv
         alloc <- refToAlloc bak p mutbl ty' tpr startRef len
         let offsetSv idx sv = if idx == 0 then sv else MS.SetupElem () sv idx
         return $ offsetSv idx $ MS.SetupVar alloc
+    go (SliceShape _ ty mutbl tpr) (Empty :> RV refRV :> RV lenRV) = do
+        let (refShp, lenShp) = sliceShapeParts ty mutbl tpr
+        refSV <- go refShp refRV
+        lenSV <- go lenShp lenRV
+        pure $ MS.SetupSlice $ MirSetupSliceRaw refSV lenSV
     go (FnPtrShape _ _ _) _ =
         error "Function pointers not currently supported in overrides"
 

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

@@ -63,7 +63,12 @@ clobberSymbolic sym loc nameStr shp rv = go shp rv
     go (TransparentShape _ shp) rv = go shp rv
     go (FnPtrShape _ _ _) _rv =
         error "Function pointers not currently supported in overrides"
-    go shp _rv = error $ "clobberSymbolic: " ++ show (shapeType shp) ++ " NYI"
+    go (RefShape _ _ _ _) _rv = error "clobberSymbolic: RefShape NYI"
+    go (SliceShape _ ty mutbl tpr) (Ctx.Empty Ctx.:> RV ref Ctx.:> RV len) = do
+        let (refShp, lenShp) = sliceShapeParts ty mutbl tpr
+        ref' <- go refShp ref
+        len' <- go lenShp len
+        pure $ Ctx.Empty Ctx.:> RV ref' Ctx.:> RV len'
 
     goField :: forall tp. FieldShape tp -> RegValue' sym tp ->
         OverrideSim (p sym) sym MIR rtp args ret (RegValue' sym tp)
@@ -109,6 +114,11 @@ clobberImmutSymbolic sym loc nameStr shp rv = go shp rv
     -- Since this ref is in immutable memory, whatever behavior we're
     -- approximating with this clobber can't possibly modify it.
     go (RefShape _ _ _ _tpr) rv = return rv
+    go (SliceShape _ ty mutbl tpr) (Ctx.Empty Ctx.:> RV ref Ctx.:> RV len) = do
+        let (refShp, lenShp) = sliceShapeParts ty mutbl tpr
+        ref' <- go refShp ref
+        len' <- go lenShp len
+        pure $ Ctx.Empty Ctx.:> RV ref' Ctx.:> RV len'
     go (FnPtrShape _ _ _) _rv =
         error "Function pointers not currently supported in overrides"
 

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

@@ -409,6 +409,11 @@ matchArg sym sc eval allocSpecs md shp rv sv = go shp rv sv
         goRef refTy pointeeTy mutbl tpr ref alloc 0
     go (RefShape refTy pointeeTy mutbl tpr) ref (MS.SetupElem () (MS.SetupVar alloc) idx) =
         goRef refTy pointeeTy mutbl tpr ref alloc idx
+    go (SliceShape _ ty mutbl tpr) (Ctx.Empty Ctx.:> RV ref Ctx.:> RV len)
+                                   (MS.SetupSlice (MirSetupSliceRaw refSV lenSV)) = do
+        let (refShp, lenShp) = sliceShapeParts ty mutbl tpr
+        go refShp ref refSV
+        go lenShp len lenSV
     go (FnPtrShape _ _ _) _ _ =
         error "Function pointers not currently supported in overrides"
     go shp _ sv = error $ "matchArg: type error: bad SetupValue " ++
@@ -534,6 +539,11 @@ setupToReg sym sc termSub regMap allocMap shp sv = go shp sv
             Nothing -> error $ "setupToReg: type error: bad reference type for " ++ show alloc ++
                 ": got " ++ show (ptr ^. mpType) ++ " but expected " ++ show tpr
         Nothing -> error $ "setupToReg: no definition for " ++ show alloc
+    go (SliceShape _ ty mutbl tpr) (MS.SetupSlice (MirSetupSliceRaw refSV lenSV)) = do
+        let (refShp, lenShp) = sliceShapeParts ty mutbl tpr
+        refRV <- go refShp refSV
+        lenRV <- go lenShp lenSV
+        pure $ Ctx.Empty Ctx.:> RV refRV Ctx.:> RV lenRV
     go (FnPtrShape _ _ _) _ =
         error "Function pointers not currently supported in overrides"
     go shp sv = error $ "setupToReg: type error: bad SetupValue for " ++ show (shapeType shp) ++

crux-mir-comp/src/Mir/Cryptol.hs

@@ -340,6 +340,11 @@ munge sym shp rv = do
         go (FnPtrShape _ _ _) _ =
             error "Function pointers not currently supported in overrides"
         -- TODO: RefShape
+        go (SliceShape _ ty mutbl tpr) (Ctx.Empty Ctx.:> RV ref Ctx.:> RV len) = do
+            let (refShp, lenShp) = sliceShapeParts ty mutbl tpr
+            ref' <- go refShp ref
+            len' <- go lenShp len
+            pure $ Ctx.Empty Ctx.:> RV ref' Ctx.:> RV len'
         go shp _ = error $ "munge: " ++ show (shapeType shp) ++ " NYI"
 
         goFields :: forall ctx.

doc/manual/manual.md

@@ -2125,7 +2125,6 @@ implemented include the following:
 * MIR specifications that use overrides (i.e., the `[MIRSpec]` argument to
   `mir_verify` must always be the empty list at present)
 * The ability to construct MIR `enum` values in specifications
-* The ability to specify the layout of slice values
 
 The `String` supplied as an argument to `mir_verify` is expected to be a
 function _identifier_. An identifier is expected adhere to one of the following
@@ -2639,6 +2638,9 @@ construct compound values:
 * `mir_array_value : MIRType -> [MIRValue] -> MIRValue` constructs an array
   of the given type whose elements consist of the given values. Supplying the
   element type is necessary to support length-0 arrays.
+* `mir_slice_value : MIRValue -> MIRValue`: see the "MIR slices" section below.
+* `mir_slice_range_value : MIRValue -> Int -> Int -> MIRValue`: see the
+  "MIR slices" section below.
 * `mir_struct_value : MIRAdt -> [MIRValue] -> MIRValue` construct a struct
   with the given list of values as elements. The `MIRAdt` argument determines
   what struct type to create.
@@ -2648,6 +2650,88 @@ construct compound values:
 * `mir_tuple_value : [MIRValue] -> MIRValue` construct a tuple with the given
   list of values as elements.
 
+### MIR slices
+
+Slices are a unique form of compound type that is currently only used during
+MIR verification. Unlike other forms of compound values, such as arrays, it is
+not possible to directly construct a slice. Instead, one must take a slice of
+an existing reference value that points to the thing being sliced. The
+following commands are used to construct slices:
+
+* `mir_slice_value : MIRValue -> MIRValue`: the SAWScript expression
+  `mir_slice_value base` is equivalent to the Rust expression `base[..]`,
+  i.e., a slice of the entirety of `base`. `base` must be a reference to
+  an array value.
+* `mir_slice_range_value : MIRValue -> Int -> Int -> MIRValue`: the SAWScript
+  expression `mir_slice_range_value base start end` is equivalent to the Rust
+  expression `base[start..end]`, i.e., a slice over a part of `base` which
+  ranges from `start` to `end`. `base` must be a reference to an array value,
+  and `start` and `end` are assumed to be zero-indexed. `start` must not exceed
+  `end`, and `end` must be strictly less than the length of the array that
+  `base` points to.
+
+As an example of how to use these functions, consider this Rust function, which
+accepts an arbitrary slice as an argument:
+
+~~~~ .rs
+pub fn f(s: &[u32]) -> u32 {
+    s[0] + s[1]
+}
+~~~~
+
+We can write a specification that passes a slice to the array `[1, 2, 3, 4, 5]`
+as an argument to `f`:
+
+~~~~
+let f_spec_1 = do {
+  a <- mir_alloc (mir_array 5 mir_u32);
+  mir_points_to a (mir_term {{ [1, 2, 3, 4, 5] : [5][32] }});
+
+  mir_execute_func [mir_slice_value a];
+
+  mir_return (mir_term {{ 3 : [32] }});
+};
+~~~~
+
+Alternatively, we can write a specification that passes a part of this array
+which ranges from second element to the fourth.
+
+~~~~
+let f_spec_2 = do {
+  a <- mir_alloc (mir_array 5 mir_u32);
+  mir_points_to a (mir_term {{ [1, 2, 3, 4, 5] : [5][32] }});
+
+  mir_execute_func [mir_slice_range_value a 1 3];
+
+  mir_return (mir_term {{ 5 : [32] }});
+};
+~~~~
+
+Note that we are passing _references_ of arrays to `mir_slice_value` and
+`mir_slice_range_value`. It would be an error to pass a bare array to these
+functions, so the following specification would be invalid:
+
+~~~~
+let f_fail_spec_ = do {
+  let arr = mir_term {{ [1, 2, 3, 4, 5] : [5][32] }};
+
+  mir_execute_func [mir_slice_value arr]; // BAD: `arr` is not a reference
+
+  mir_return (mir_term {{ 3 : [32] }});
+};
+~~~~
+
+SAW's support for slices is currently limited:
+
+* SAW specifications cannot say anything about `&str` slice arguments or return
+  values at present.
+* The `mir_slice_range_value` function must accept bare `Int` arguments to
+  specify the lower and upper bounds of the range. A consequence of this design
+  is that it is not possible to create a slice with a symbolic length.
+
+If either of these limitations prevent you from using SAW, please file an issue
+[on GitHub](https://github.com/GaloisInc/saw-script/issues).
+
 ### Finding MIR alegraic data types
 
 We collectively refer to MIR `struct`s and `enum`s together as _algebraic data

intTests/test_mir_verify_slices/Makefile

@@ -0,0 +1,13 @@
+all: test.linked-mir.json
+
+test.linked-mir.json: test.rs
+	saw-rustc $<
+	$(MAKE) remove-unused-build-artifacts
+
+.PHONY: remove-unused-build-artifacts
+remove-unused-build-artifacts:
+	rm -f test libtest.mir libtest.rlib
+
+.PHONY: clean
+clean: remove-unused-build-artifacts
+	rm -f test.linked-mir.json

intTests/test_mir_verify_slices/test.linked-mir.json

@@ -0,0 +1 @@
+{"fns":[{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Ref::2829f685526f8473"}],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_3","ty":"ty::usize"}},"pos":"test.rs:2:7: 2:8","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"kind":"usize","size":8,"val":"0"},"ty":"ty::usize"},"kind":"Constant"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::usize"}},"pos":"test.rs:2:5: 2:9","rhs":{"kind":"Len","lv":{"data":[{"kind":"Deref"}],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Ref::2829f685526f8473"}}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_5","ty":"ty::bool"}},"pos":"test.rs:2:5: 2:9","rhs":{"L":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_3","ty":"ty::usize"}},"kind":"Copy"},"R":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::usize"}},"kind":"Copy"},"kind":"BinaryOp","op":{"kind":"Lt"}}}],"terminator":{"cleanup":null,"cond":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_5","ty":"ty::bool"}},"kind":"Move"},"expected":true,"kind":"Assert","msg":"index out of bounds: the length is move _4 but the index is _3","pos":"test.rs:2:5: 2:9","target":"bb1"}},"blockid":"bb0"},{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::u32"}},"pos":"test.rs:2:5: 2:9","rhs":{"kind":"Use","usevar":{"data":{"data":[{"kind":"Deref"},{"kind":"Index","op":{"is_zst":false,"mut":{"kind":"Not"},"name":"_3","ty":"ty::usize"}}],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Ref::2829f685526f8473"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_7","ty":"ty::usize"}},"pos":"test.rs:2:14: 2:15","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"kind":"usize","size":8,"val":"1"},"ty":"ty::usize"},"kind":"Constant"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_8","ty":"ty::usize"}},"pos":"test.rs:2:12: 2:16","rhs":{"kind":"Len","lv":{"data":[{"kind":"Deref"}],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Ref::2829f685526f8473"}}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_9","ty":"ty::bool"}},"pos":"test.rs:2:12: 2:16","rhs":{"L":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_7","ty":"ty::usize"}},"kind":"Copy"},"R":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_8","ty":"ty::usize"}},"kind":"Copy"},"kind":"BinaryOp","op":{"kind":"Lt"}}}],"terminator":{"cleanup":null,"cond":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_9","ty":"ty::bool"}},"kind":"Move"},"expected":true,"kind":"Assert","msg":"index out of bounds: the length is move _8 but the index is _7","pos":"test.rs:2:12: 2:16","target":"bb2"}},"blockid":"bb1"},{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_6","ty":"ty::u32"}},"pos":"test.rs:2:12: 2:16","rhs":{"kind":"Use","usevar":{"data":{"data":[{"kind":"Deref"},{"kind":"Index","op":{"is_zst":false,"mut":{"kind":"Not"},"name":"_7","ty":"ty::usize"}}],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Ref::2829f685526f8473"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_10","ty":"ty::Tuple::7063e33f0dbc8a58"}},"pos":"test.rs:2:5: 2:16","rhs":{"L":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::u32"}},"kind":"Copy"},"R":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_6","ty":"ty::u32"}},"kind":"Copy"},"kind":"CheckedBinaryOp","op":{"kind":"Add"}}}],"terminator":{"cleanup":null,"cond":{"data":{"data":[{"field":1,"kind":"Field","ty":"ty::bool"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_10","ty":"ty::Tuple::7063e33f0dbc8a58"}},"kind":"Move"},"expected":false,"kind":"Assert","msg":"attempt to compute `move _2 + move _6`, which would overflow","pos":"test.rs:2:5: 2:16","target":"bb3"}},"blockid":"bb2"},{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"}},"pos":"test.rs:2:5: 2:16","rhs":{"kind":"Use","usevar":{"data":{"data":[{"field":0,"kind":"Field","ty":"ty::u32"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_10","ty":"ty::Tuple::7063e33f0dbc8a58"}},"kind":"Move"}}}],"terminator":{"kind":"Return","pos":"test.rs:3:2: 3:2"}},"blockid":"bb3"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_3","ty":"ty::usize"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::usize"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_5","ty":"ty::bool"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_6","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_7","ty":"ty::usize"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_8","ty":"ty::usize"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_9","ty":"ty::bool"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_10","ty":"ty::Tuple::7063e33f0dbc8a58"}]},"name":"test/91ae4be1::f","return_ty":"ty::u32","spread_arg":null},{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_1","ty":"ty::Ref::fb1cfdc5725cd03b"}],"body":{"blocks":[{"block":{"data":[],"terminator":{"kind":"Return","pos":"test.rs:5:21: 5:21"}},"blockid":"bb0"}],"vars":[{"is_zst":true,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Tuple::e93222e871854c41"}]},"name":"test/91ae4be1::g","return_ty":"ty::Tuple::e93222e871854c41","spread_arg":null}],"adts":[],"statics":[],"vtables":[],"traits":[],"intrinsics":[{"inst":{"def_id":"test/91ae4be1::f","kind":"Item","substs":[]},"name":"test/91ae4be1::f"},{"inst":{"def_id":"test/91ae4be1::g","kind":"Item","substs":[]},"name":"test/91ae4be1::g"}],"tys":[{"name":"ty::u32","ty":{"kind":"Uint","uintkind":{"kind":"U32"}}},{"name":"ty::Slice::f7eb0deb10702a2f","ty":{"kind":"Slice","ty":"ty::u32"}},{"name":"ty::Ref::2829f685526f8473","ty":{"kind":"Ref","mutability":{"kind":"Not"},"ty":"ty::Slice::f7eb0deb10702a2f"}},{"name":"ty::usize","ty":{"kind":"Uint","uintkind":{"kind":"Usize"}}},{"name":"ty::bool","ty":{"kind":"Bool"}},{"name":"ty::Tuple::7063e33f0dbc8a58","ty":{"kind":"Tuple","tys":["ty::u32","ty::bool"]}},{"name":"ty::str","ty":{"kind":"Str"}},{"name":"ty::Ref::fb1cfdc5725cd03b","ty":{"kind":"Ref","mutability":{"kind":"Not"},"ty":"ty::str"}},{"name":"ty::Tuple::e93222e871854c41","ty":{"kind":"Tuple","tys":[]}}],"roots":["test/91ae4be1::f","test/91ae4be1::g"]}

intTests/test_mir_verify_slices/test.rs

@@ -0,0 +1,5 @@
+pub fn f(s: &[u32]) -> u32 {
+    s[0] + s[1]
+}
+
+pub fn g(_: &str) {}

intTests/test_mir_verify_slices/test.saw

@@ -0,0 +1,115 @@
+enable_experimental;
+
+let oneThroughFive = mir_term {{ [1, 2, 3, 4, 5] : [5][32] }};
+
+let f_spec_1 = do {
+  a <- mir_alloc (mir_array 5 mir_u32);
+  mir_points_to a oneThroughFive;
+
+  mir_execute_func [mir_slice_value a];
+
+  mir_return (mir_term {{ 3 : [32] }});
+};
+
+let f_spec_2 = do {
+  a <- mir_alloc (mir_array 5 mir_u32);
+  mir_points_to a oneThroughFive;
+
+  mir_execute_func [mir_slice_range_value a 1 3];
+
+  mir_return (mir_term {{ 5 : [32] }});
+};
+
+// mir_slice_value must take an array reference as an argument.
+// Passing a bare array constitutes a type error.
+let f_fail_spec_1 = do {
+  let arr = mir_array_value mir_u32 [mir_term {{ 1 : [32] }}];
+  mir_execute_func [mir_slice_value arr];
+
+  mir_return (mir_term {{ 0 : [32] }});
+};
+
+// The end value of the range given to mir_slice_range_value must be less
+// than the length of the slice.
+let f_fail_spec_2 = do {
+  a <- mir_alloc (mir_array 5 mir_u32);
+  mir_points_to a oneThroughFive;
+
+  mir_execute_func [mir_slice_range_value a 0 5];
+
+  mir_return (mir_term {{ 0 : [32] }});
+};
+
+// The start value of the range given to mir_slice_range_value must not
+// exceed the end value.
+let f_fail_spec_3 = do {
+  a <- mir_alloc (mir_array 5 mir_u32);
+  mir_points_to a oneThroughFive;
+
+  mir_execute_func [mir_slice_range_value a 6 5];
+
+  mir_return (mir_term {{ 0 : [32] }});
+};
+
+// Indexing into a length-0 slice is disallowed.
+let f_fail_spec_4 = do {
+  a <- mir_alloc (mir_array 5 mir_u32);
+  mir_points_to a oneThroughFive;
+
+  mir_execute_func [mir_slice_range_value a 0 0];
+
+  mir_return (mir_term {{ 0 : [32] }});
+};
+
+// f requires a slice of length at least two.
+let f_fail_spec_5 = do {
+  a <- mir_alloc (mir_array 5 mir_u32);
+  mir_points_to a oneThroughFive;
+
+  mir_execute_func [mir_slice_range_value a 0 1];
+
+  mir_return (mir_term {{ 0 : [32] }});
+};
+
+// mir_alloc cannot be used to allocate slice references.
+let f_fail_spec_6 = do {
+  s <- mir_alloc (mir_slice mir_u32);
+
+  mir_execute_func [s];
+
+  mir_return (mir_term {{ 0 : [32] }});
+};
+
+// mir_alloc cannot be used to allocate str references.
+let g_fail_spec = do {
+  s <- mir_alloc mir_str;
+
+  mir_execute_func [s];
+};
+
+m <- mir_load_module "test.linked-mir.json";
+
+mir_verify m "test::f" [] false f_spec_1 z3;
+mir_verify m "test::f" [] false f_spec_2 z3;
+
+fails (
+  mir_verify m "test::f" [] false f_fail_spec_1 z3
+);
+fails (
+  mir_verify m "test::f" [] false f_fail_spec_2 z3
+);
+fails (
+  mir_verify m "test::f" [] false f_fail_spec_3 z3
+);
+fails (
+  mir_verify m "test::f" [] false f_fail_spec_4 z3
+);
+fails (
+  mir_verify m "test::f" [] false f_fail_spec_5 z3
+);
+fails (
+  mir_verify m "test::f" [] false f_fail_spec_6 z3
+);
+fails (
+  mir_verify m "test::g" [] false g_fail_spec z3
+);

intTests/test_mir_verify_slices/test.sh

@@ -0,0 +1,3 @@
+set -e
+
+$SAW test.saw

saw-remote-api/CHANGELOG.md

@@ -25,6 +25,9 @@
 * The API for `"struct"` `setup value`s now has a `"MIR ADT"` field. For
   MIR verification, this field is required. For LLVM and JVM verification,
   this field must be `null`, or else an error will be raised.
+* Add `"slice"` and `"slice range"` `setup value`s representing slices in MIR
+  verification. Attempting to use these in LLVM or JVM verification will raise
+  an error.
 
 ## 1.0.0 -- 2023-06-26