Merge pull request #1948 from GaloisInc/T1859-mir-slices

`mir_slice_value` and `mir_slice_range_value`

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,95 @@ 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 (`&[T; N]` or `&mut [T; N]`), not an array itself. The type of
+  `mir_slice_value base` will be `&[T]` (if `base` is an immutable reference)
+  or `&mut [T]` (if `base` is a mutable reference).
+* `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
+  (`&[T; N]` or `&mut [T; N]`), not an array itself. The type of
+  `mir_slice_value base` will be `&[T]` (if `base` is an immutable reference)
+  or `&mut [T]` (if `base` is a mutable reference).
+
+  `start` and `end` are assumed to be zero-indexed. `start` must not exceed
+  `end`, and `end` must not exceed 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
+over the range `[1..3]`, i.e., ranging from second element to the fourth.
+Because this is a half-open range, the resulting slice has length 2:
+
+~~~~
+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 not
+// exceed 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 6];
+
+  mir_return (mir_term {{ 3 : [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