MIR string slices

This adds rudimentary support for constructing MIR `str` slice references via
the new `mir_str_slice_value` and `mir_str_slice_range_value` SAWScript
functions. These behave much like their cousins `mir_slice_value` and
`mir_slice_range_value` (which work for array slices), except that they return
something of type `&str` instead of, say, `&[u8]`. See the manual for the full
details and current limitations of the approach.

The `mir_str_slice_value`/`mir_str_slice_range_value` functions mostly share
the same implementation as `mir_slice_value`/`mir_slice_range_value`, except
for some minor differences regarding how the underlying types are handled.
There is now a new `MirSliceInfo` data type that signals whether we are dealing
with a `str` slice or an array slice.

Fixes #1997.

CHANGES.md

@@ -1,3 +1,11 @@
+# next -- TBA
+
+## New Features
+
+* Add `mir_str_slice_value` and `mir_str_slice_range_value` functions, which
+  allow taking `&str` slices. For more information, see the documentation in the
+  [SAW manual](https://github.com/GaloisInc/saw-script/blob/master/doc/manual/manual.md#string-slices).
+
 # Version 1.1 -- 2024-02-05
 
 ## New Features

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

@@ -655,11 +655,11 @@ substMethodSpec sc sm ms = do
 
     goSetupSlice (MirSetupSliceRaw ref len) =
       MirSetupSliceRaw <$> goSetupValue ref <*> goSetupValue len
-    goSetupSlice (MirSetupSlice arr) =
-      MirSetupSlice <$> goSetupValue arr
-    goSetupSlice (MirSetupSliceRange arr start end) = do
+    goSetupSlice (MirSetupSlice sliceInfo arr) =
+      MirSetupSlice sliceInfo <$> goSetupValue arr
+    goSetupSlice (MirSetupSliceRange sliceInfo arr start end) = do
       arr' <- goSetupValue arr
-      pure $ MirSetupSliceRange arr' start end
+      pure $ MirSetupSliceRange sliceInfo arr' start end
 
     goTypedTerm tt = do
         term' <- goTerm $ SAW.ttTerm tt

doc/manual/head.tex

@@ -1,5 +1,4 @@
 \usepackage{listings}
-\usepackage{float}
 \usepackage{xspace}
 \usepackage{color}
 \usepackage{tikz}
@@ -32,7 +31,8 @@
          framexleftmargin=5pt,
          framexrightmargin=-1pt,
          framexbottommargin=4pt,
-         showstringspaces=false
+         showstringspaces=false,
+         literate={ș}{{\textcommabelow{s}}}1,
 }
 
 \author{The Galois SAW Team\\\texttt{saw@galois.com}}

doc/manual/manual.md

@@ -3024,6 +3024,10 @@ construct compound values:
 * `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_str_slice_value : MIRValue -> MIRValue`: see the "MIR slices" section
+  below.
+* `mir_str_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.
@@ -3051,8 +3055,13 @@ fields), which are not currently supported.
 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:
+an existing reference value that points to the thing being sliced.
+
+SAW currently supports taking slices of arrays and strings.
+
+#### Array slices
+
+The following commands are used to construct slices of arrays:
 
 * `mir_slice_value : MIRValue -> MIRValue`: the SAWScript expression
   `mir_slice_value base` is equivalent to the Rust expression `&base[..]`,
@@ -3124,16 +3133,110 @@ let f_fail_spec_ = do {
 };
 ~~~~
 
-SAW's support for slices is currently limited:
+Note that 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
+this limitation prevents you from using SAW, please file an issue [on
+GitHub](https://github.com/GaloisInc/saw-script/issues).
+
+#### String slices
+
+In addition to slices of arrays (i.e., of type `&[T]`), SAW also supports
+slices of strings (i.e., of type `&str`) through the following commands:
+
+* `mir_str_slice_value : MIRValue -> MIRValue`: the SAWScript expression
+  `mir_str_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 of bytes (`&[u8; N]` or `&mut [u8; N]`), not an array itself. The type
+  of `mir_str_slice_value base` will be `&str` (if `base` is an immutable
+  reference) or `&mut str` (if `base` is a mutable reference).
+* `mir_str_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 of
+  bytes (`&[u8; N]` or `&mut [u8; N]`), not an array itself. The type of
+  `mir_slice_value base` will be `&str` (if `base` is an immutable reference)
+  or `&mut str` (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.
+
+One unusual requirement about `mir_str_slice_value` and
+`mir_str_slice_range_value` is that they require the argument to be of type
+`&[u8; N]`, i.e., a reference to an array of bytes. This is an artifact of the
+way that strings are encoded in Cryptol. The following Cryptol expressions:
+
+* `"A"`
+* `"123"`
+* `"Hello World"`
+
+Have the following types:
+
+* `[1][8]`
+* `[3][8]`
+* `[11][8]`
+
+This is because Cryptol strings are syntactic shorthand for sequences of bytes.
+The following Cryptol expressions are wholly equivalent:
+
+* `[0x41]`
+* `[0x31, 0x32, 0x33]`
+* `[0x48, 0x65, 0x6c, 0x6c, 0x6f, 0x20, 0x57, 0x6f, 0x72, 0x6c, 0x64]`
+
+These represent the strings in the extended ASCII character encoding. The
+Cryptol sequence type `[N][8]` is equivalent to the Rust type `[u8; N]`, so the
+requirement to have something of type `&[u8; N]` as an argument reflects this
+design choice.
 
-* 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.
+As an example of how to write specifications involving string slices,
+consider this Rust function:
+
+~~~ .rs
+pub fn my_len(s: &str) -> usize {
+    s.len()
+}
+~~~
+
+We can use `mir_str_slice_value` to write a specification for `my_len` when it
+is given the string `"hello"` as an argument:
+
+~~~
+let my_len_spec = do {
+  s <- mir_alloc (mir_array 5 mir_u8);
+  mir_points_to s (mir_term {{ "hello" }});
+
+  mir_execute_func [mir_str_slice_value s];
+
+  mir_return (mir_term {{ 5 : [32] }});
+};
+~~~
+
+Currently, Cryptol only supports characters that can be encoded in a single
+byte. As a result, it is not currently possible to take slices of strings with
+certain characters. For example, the string `"roșu"` cannot be used as a
+Cryptol expression, as the character `'ș'` would require 10 bits to represent
+instead of 8. The alternative is to use UTF-8 to encode such characters. For
+instance, the UTF-8 encoding of the string `"roșu"` is `"ro\200\153u"`, where
+`"\200\153"` is a sequence of two bytes that represents the `'ș'` character.
+
+SAW makes no attempt to ensure that string slices over a particular range
+aligns with UTF-8 character boundaries. For example, the following Rust code
+would panic:
+
+~~~ .rs
+    let rosu: &str = "roșu";
+    let s: &str = &rosu[0..3];
+    println!("{:?}", s);
+~~~
+~~~
+thread 'main' panicked at 'byte index 3 is not a char boundary; it is inside 'ș' (bytes 2..4) of `roșu`'
+~~~
 
-If either of these limitations prevent you from using SAW, please file an issue
-[on GitHub](https://github.com/GaloisInc/saw-script/issues).
+On the other hand, SAW will allow you define a slice of the form
+`mir_str_slice_range r 0 3`, where `r` is a reference to `"ro\200\153u"`. It is
+the responsibility of the SAW user to ensure that `mir_str_slice_range` indices
+align with character boundaries.
 
 ### Finding MIR algebraic data types
 

intTests/test_mir_verify_str_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_str_slices/test.linked-mir.json

@@ -0,0 +1 @@
+{"fns":[{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Ref::fb1cfdc5725cd03b"}],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::Ref::fb1cfdc5725cd03b"}},"pos":"test.rs:2:24: 2:36","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Ref::fb1cfdc5725cd03b"}},"kind":"Copy"}}}],"terminator":{"args":[{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::Ref::fb1cfdc5725cd03b"}},"kind":"Move"}],"cleanup":null,"destination":[{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_3","ty":"ty::Ref::78e545a0deb2a880"}},"bb1"],"from_hir_call":true,"func":{"data":{"rendered":{"kind":"zst"},"ty":"ty::FnDef::1965db56546f3d3b"},"kind":"Constant"},"kind":"Call","pos":"test.rs:2:24: 2:36"}},"blockid":"bb0"},{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_2","ty":"ty::Ref::78e545a0deb2a880"}},"pos":"test.rs:2:24: 2:36","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_3","ty":"ty::Ref::78e545a0deb2a880"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_6","ty":"ty::usize"}},"pos":"test.rs:3:11: 3:12","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":"_7","ty":"ty::usize"}},"pos":"test.rs:3:5: 3:13","rhs":{"kind":"Len","lv":{"data":[{"kind":"Deref"}],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_2","ty":"ty::Ref::78e545a0deb2a880"}}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_8","ty":"ty::bool"}},"pos":"test.rs:3:5: 3:13","rhs":{"L":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_6","ty":"ty::usize"}},"kind":"Copy"},"R":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_7","ty":"ty::usize"}},"kind":"Copy"},"kind":"BinaryOp","op":{"kind":"Lt"}}}],"terminator":{"cleanup":null,"cond":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_8","ty":"ty::bool"}},"kind":"Move"},"expected":true,"kind":"Assert","msg":"index out of bounds: the length is move _7 but the index is _6","pos":"test.rs:3:5: 3:13","target":"bb2"}},"blockid":"bb1"},{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_5","ty":"ty::u8"}},"pos":"test.rs:3:5: 3:13","rhs":{"kind":"Use","usevar":{"data":{"data":[{"kind":"Deref"},{"kind":"Index","op":{"is_zst":false,"mut":{"kind":"Not"},"name":"_6","ty":"ty::usize"}}],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_2","ty":"ty::Ref::78e545a0deb2a880"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_10","ty":"ty::usize"}},"pos":"test.rs:3:22: 3:23","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":"_11","ty":"ty::usize"}},"pos":"test.rs:3:16: 3:24","rhs":{"kind":"Len","lv":{"data":[{"kind":"Deref"}],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_2","ty":"ty::Ref::78e545a0deb2a880"}}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_12","ty":"ty::bool"}},"pos":"test.rs:3:16: 3:24","rhs":{"L":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_10","ty":"ty::usize"}},"kind":"Copy"},"R":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_11","ty":"ty::usize"}},"kind":"Copy"},"kind":"BinaryOp","op":{"kind":"Lt"}}}],"terminator":{"cleanup":null,"cond":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_12","ty":"ty::bool"}},"kind":"Move"},"expected":true,"kind":"Assert","msg":"index out of bounds: the length is move _11 but the index is _10","pos":"test.rs:3:16: 3:24","target":"bb3"}},"blockid":"bb2"},{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_9","ty":"ty::u8"}},"pos":"test.rs:3:16: 3:24","rhs":{"kind":"Use","usevar":{"data":{"data":[{"kind":"Deref"},{"kind":"Index","op":{"is_zst":false,"mut":{"kind":"Not"},"name":"_10","ty":"ty::usize"}}],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_2","ty":"ty::Ref::78e545a0deb2a880"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_13","ty":"ty::Tuple::cb405746ec5fdf41"}},"pos":"test.rs:3:5: 3:24","rhs":{"L":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_5","ty":"ty::u8"}},"kind":"Copy"},"R":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_9","ty":"ty::u8"}},"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":"_13","ty":"ty::Tuple::cb405746ec5fdf41"}},"kind":"Move"},"expected":false,"kind":"Assert","msg":"attempt to compute `move _5 + move _9`, which would overflow","pos":"test.rs:3:5: 3:24","target":"bb4"}},"blockid":"bb3"},{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u8"}},"pos":"test.rs:3:5: 3:24","rhs":{"kind":"Use","usevar":{"data":{"data":[{"field":0,"kind":"Field","ty":"ty::u8"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_13","ty":"ty::Tuple::cb405746ec5fdf41"}},"kind":"Move"}}}],"terminator":{"kind":"Return","pos":"test.rs:4:2: 4:2"}},"blockid":"bb4"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u8"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_2","ty":"ty::Ref::78e545a0deb2a880"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_3","ty":"ty::Ref::78e545a0deb2a880"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::Ref::fb1cfdc5725cd03b"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_5","ty":"ty::u8"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_6","ty":"ty::usize"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_7","ty":"ty::usize"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_8","ty":"ty::bool"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_9","ty":"ty::u8"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_10","ty":"ty::usize"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_11","ty":"ty::usize"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_12","ty":"ty::bool"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_13","ty":"ty::Tuple::cb405746ec5fdf41"}]},"name":"test/6856685a::f","return_ty":"ty::u8","spread_arg":null},{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Ref::fb1cfdc5725cd03b"}],"body":{"blocks":[{"block":{"data":[{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/str/mod.rs:327:33: 327:37","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::Ref::fb1cfdc5725cd03b"}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::Ref::fb1cfdc5725cd03b"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/str/mod.rs:327:33: 327:37","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Ref::fb1cfdc5725cd03b"}},"kind":"Copy"}}}],"terminator":{"args":[{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::Ref::fb1cfdc5725cd03b"}},"kind":"Move"}],"cleanup":null,"destination":[{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Ref::78e545a0deb2a880"}},"bb1"],"from_hir_call":true,"func":{"data":{"rendered":{"kind":"zst"},"ty":"ty::FnDef::ff682f6e5e018699"},"kind":"Constant"},"kind":"Call","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/str/mod.rs:327:18: 327:38"}},"blockid":"bb0"},{"block":{"data":[{"kind":"StorageDead","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/str/mod.rs:327:37: 327:38","sdvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::Ref::fb1cfdc5725cd03b"}}],"terminator":{"kind":"Return","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/str/mod.rs:328:6: 328:6"}},"blockid":"bb1"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Ref::78e545a0deb2a880"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::Ref::fb1cfdc5725cd03b"}]},"name":"core/73237d41::str::{impl#0}::as_bytes","return_ty":"ty::Ref::78e545a0deb2a880","spread_arg":null}],"adts":[],"statics":[],"vtables":[],"traits":[],"intrinsics":[{"inst":{"def_id":"test/6856685a::f","kind":"Item","substs":[]},"name":"test/6856685a::f"},{"inst":{"def_id":"core/73237d41::str::{impl#0}::as_bytes","kind":"Item","substs":[]},"name":"core/73237d41::str::{impl#0}::as_bytes"},{"inst":{"def_id":"core/73237d41::intrinsics::{extern#0}::transmute","kind":"Intrinsic","substs":["ty::Ref::fb1cfdc5725cd03b","ty::Ref::78e545a0deb2a880"]},"name":"core/73237d41::intrinsics::{extern#0}::transmute::_instf78f029a53f4941f[0]"}],"tys":[{"name":"ty::str","ty":{"kind":"Str"}},{"name":"ty::Ref::fb1cfdc5725cd03b","ty":{"kind":"Ref","mutability":{"kind":"Not"},"ty":"ty::str"}},{"name":"ty::u8","ty":{"kind":"Uint","uintkind":{"kind":"U8"}}},{"name":"ty::Slice::8c8d8339a6a54cae","ty":{"kind":"Slice","ty":"ty::u8"}},{"name":"ty::Ref::78e545a0deb2a880","ty":{"kind":"Ref","mutability":{"kind":"Not"},"ty":"ty::Slice::8c8d8339a6a54cae"}},{"name":"ty::usize","ty":{"kind":"Uint","uintkind":{"kind":"Usize"}}},{"name":"ty::bool","ty":{"kind":"Bool"}},{"name":"ty::Tuple::cb405746ec5fdf41","ty":{"kind":"Tuple","tys":["ty::u8","ty::bool"]}},{"name":"ty::FnDef::1965db56546f3d3b","ty":{"defid":"core/73237d41::str::{impl#0}::as_bytes","kind":"FnDef"}},{"name":"ty::FnDef::ff682f6e5e018699","ty":{"defid":"core/73237d41::intrinsics::{extern#0}::transmute::_instf78f029a53f4941f[0]","kind":"FnDef"}}],"roots":["test/6856685a::f"]}

intTests/test_mir_verify_str_slices/test.rs

@@ -0,0 +1,4 @@
+pub fn f(s: &str) -> u8 {
+    let bytes: &[u8] = s.as_bytes();
+    bytes[0] + bytes[1]
+}