Add subsequence and slice split operations

src/analyze/annot.rs

@@ -177,6 +177,14 @@ pub fn seq_push_path() -> [Symbol; 3] {
     ]
 }
 
+pub fn seq_subsequence_path() -> [Symbol; 3] {
+    [
+        Symbol::intern("thrust"),
+        Symbol::intern("def"),
+        Symbol::intern("seq_subsequence"),
+    ]
+}
+
 pub fn seq_concat_path() -> [Symbol; 3] {
     [
         Symbol::intern("thrust"),

src/analyze/annot_fn.rs

@@ -717,6 +717,21 @@ impl<'a, 'tcx> AnnotFnTranslator<'a, 'tcx> {
                             new_arr, offset, new_len,
                         ]));
                     }
+                    if Some(def_id) == self.def_ids.seq_subsequence() {
+                        assert_eq!(args.len(), 2, "Seq::subsequence takes exactly 2 arguments");
+                        let t = self.to_term(receiver);
+                        let start = self.to_term(&args[0]);
+                        let end = self.to_term(&args[1]);
+                        let arr = t.clone().tuple_proj(0);
+                        let offset = t.tuple_proj(1);
+                        // A subsequence shares the underlying array, advances the offset by
+                        // `start`, and sets the length to `end - start`.
+                        return FormulaOrTerm::Term(chc::Term::tuple(vec![
+                            arr,
+                            offset.add(start.clone()),
+                            end.sub(start),
+                        ]));
+                    }
                     if Some(def_id) == self.def_ids.seq_concat() {
                         assert_eq!(args.len(), 1, "Seq::concat takes exactly 1 argument");
                         let elem_sort = self.adt_arg_type_at(receiver, 0).to_sort();

src/analyze/did_cache.rs

@@ -29,6 +29,7 @@ struct DefIds {
     seq_singleton: OnceCell<Option<DefId>>,
     seq_len: OnceCell<Option<DefId>>,
     seq_push: OnceCell<Option<DefId>>,
+    seq_subsequence: OnceCell<Option<DefId>>,
     seq_concat: OnceCell<Option<DefId>>,
 
     exists: OnceCell<Option<DefId>>,
@@ -221,6 +222,13 @@ impl<'tcx> DefIdCache<'tcx> {
             .get_or_init(|| self.annotated_def(&crate::analyze::annot::seq_push_path()))
     }
 
+    pub fn seq_subsequence(&self) -> Option<DefId> {
+        *self
+            .def_ids
+            .seq_subsequence
+            .get_or_init(|| self.annotated_def(&crate::analyze::annot::seq_subsequence_path()))
+    }
+
     pub fn seq_concat(&self) -> Option<DefId> {
         *self
             .def_ids

std.rs

@@ -239,6 +239,17 @@ mod thrust_models {
                 unimplemented!()
             }
 
+            #[allow(dead_code)]
+            #[thrust::def::seq_subsequence]
+            #[thrust::ignored]
+            pub fn subsequence<U, V>(self, _start: U, _end: V) -> Self
+            where
+                U: super::Model<Ty = Int>,
+                V: super::Model<Ty = Int>,
+            {
+                unimplemented!()
+            }
+
             #[allow(dead_code)]
             #[thrust::def::seq_concat]
             #[thrust::ignored]
@@ -961,6 +972,87 @@ fn _extern_spec_slice_last_mut<T>(slice: &mut [T]) -> Option<&mut T>
     <[T]>::last_mut(slice)
 }
 
+#[thrust::extern_spec_fn]
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures(
+    ((*slice).length > 0
+        && result == Some((
+            &(*slice).array[(*slice).offset],
+            &(*slice).subsequence(1, (*slice).length),
+        ))
+    )
+    || ((*slice).length == 0 && result == None)
+)]
+fn _extern_spec_slice_split_first<T>(slice: &[T]) -> Option<(&T, &[T])>
+    where T: thrust_models::Model, T::Ty: PartialEq
+{
+    <[T]>::split_first(slice)
+}
+
+#[thrust::extern_spec_fn]
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures(
+    ((*slice).length > 0
+        && result == Some((
+            &(*slice).array[(*slice).offset + (*slice).length - 1],
+            &(*slice).subsequence(0, (*slice).length - 1),
+        ))
+    )
+    || ((*slice).length == 0 && result == None)
+)]
+fn _extern_spec_slice_split_last<T>(slice: &[T]) -> Option<(&T, &[T])>
+    where T: thrust_models::Model, T::Ty: PartialEq
+{
+    <[T]>::split_last(slice)
+}
+
+#[thrust::extern_spec_fn]
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures(
+    ((*slice).length > 0
+        && (!slice).offset == (*slice).offset
+        && (!slice).length == (*slice).length
+        && result == Some((
+            thrust_models::model::Mut::new((*slice)[0], (!slice)[0]),
+            thrust_models::model::Mut::new(
+                (*slice).subsequence(1, (*slice).length),
+                (!slice).subsequence(1, (!slice).length),
+            ),
+        ))
+    )
+    || ((*slice).length == 0 && result == None && !slice == *slice)
+)]
+fn _extern_spec_slice_split_first_mut<T>(slice: &mut [T]) -> Option<(&mut T, &mut [T])>
+    where T: thrust_models::Model, T::Ty: PartialEq
+{
+    <[T]>::split_first_mut(slice)
+}
+
+#[thrust::extern_spec_fn]
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures(
+    ((*slice).length > 0
+        && (!slice).offset == (*slice).offset
+        && (!slice).length == (*slice).length
+        && result == Some((
+            thrust_models::model::Mut::new(
+                (*slice)[(*slice).length - 1],
+                (!slice)[(!slice).length - 1],
+            ),
+            thrust_models::model::Mut::new(
+                (*slice).subsequence(0, (*slice).length - 1),
+                (!slice).subsequence(0, (!slice).length - 1),
+            ),
+        ))
+    )
+    || ((*slice).length == 0 && result == None && !slice == *slice)
+)]
+fn _extern_spec_slice_split_last_mut<T>(slice: &mut [T]) -> Option<(&mut T, &mut [T])>
+    where T: thrust_models::Model, T::Ty: PartialEq
+{
+    <[T]>::split_last_mut(slice)
+}
+
 // TODO: The following specs for Index/IndexMut methods are too specific; we should write specs for
 //       a generic index (I: SliceIndex) that isn't specific to usize, maybe once #83 is implemented.
 

tests/ui/fail/slice_split_first.rs

@@ -0,0 +1,19 @@
+//@error-in-other-file: Unsat
+//@compile-flags: -C debug-assertions=off
+#[thrust::trusted]
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures(
+    (*result).length == 2
+        && (*result).array[(*result).offset] == 10
+        && (*result).array[(*result).offset + 1] == 20
+)]
+fn slice() -> &'static [i32] {
+    unimplemented!()
+}
+
+fn main() {
+    let slice = slice();
+    let (first, _tail) = slice.split_first().unwrap();
+    // wrong: the first element is 10, not 11
+    assert!(*first == 11);
+}

tests/ui/fail/slice_split_first_mut.rs

@@ -0,0 +1,19 @@
+//@error-in-other-file: Unsat
+//@compile-flags: -C debug-assertions=off
+#[thrust::trusted]
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures(
+    (*result).length == 2
+        && (*result).array[(*result).offset] == 10
+        && (*result).array[(*result).offset + 1] == 20
+)]
+fn slice() -> &'static mut [i32] {
+    unimplemented!()
+}
+
+fn main() {
+    let slice = slice();
+    let (first, _tail) = slice.split_first_mut().unwrap();
+    // wrong: the first element is 10, not 11
+    assert!(*first == 11);
+}

tests/ui/fail/slice_split_first_mut_mutation_unsound.rs

@@ -0,0 +1,28 @@
+//@error-in-other-file: Unsat
+//@compile-flags: -C debug-assertions=off
+
+// KNOWN LIMITATION: mutation through a `&mut` returned inside a tuple (as
+// `split_first_mut` does) does not currently propagate back to the original
+// slice, which is unsound. This test is expected to be rejected (`Unsat`) once
+// that is fixed; it is kept here as a reproduction until the fix lands.
+#[thrust::trusted]
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures(
+    (*result).length == 2
+        && (*result).array[(*result).offset] == 10
+        && (*result).array[(*result).offset + 1] == 20
+)]
+fn slice() -> &'static mut [i32] {
+    unimplemented!()
+}
+
+fn main() {
+    let slice = slice();
+    {
+        // Destructure the returned tuple, then mutate through its first reference.
+        let (first, _tail) = slice.split_first_mut().unwrap();
+        *first = 11;
+    }
+    // The mutation makes slice[0] equal to 11, so this must be rejected.
+    assert!(slice[0] == 12);
+}

tests/ui/fail/slice_split_last.rs

@@ -0,0 +1,19 @@
+//@error-in-other-file: Unsat
+//@compile-flags: -C debug-assertions=off
+#[thrust::trusted]
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures(
+    (*result).length == 2
+        && (*result).array[(*result).offset] == 10
+        && (*result).array[(*result).offset + 1] == 20
+)]
+fn slice() -> &'static [i32] {
+    unimplemented!()
+}
+
+fn main() {
+    let slice = slice();
+    let (last, _init) = slice.split_last().unwrap();
+    // wrong: the last element is 20, not 21
+    assert!(*last == 21);
+}

tests/ui/fail/slice_split_last_mut.rs

@@ -0,0 +1,19 @@
+//@error-in-other-file: Unsat
+//@compile-flags: -C debug-assertions=off
+#[thrust::trusted]
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures(
+    (*result).length == 2
+        && (*result).array[(*result).offset] == 10
+        && (*result).array[(*result).offset + 1] == 20
+)]
+fn slice() -> &'static mut [i32] {
+    unimplemented!()
+}
+
+fn main() {
+    let slice = slice();
+    let (last, _init) = slice.split_last_mut().unwrap();
+    // wrong: the last element is 20, not 21
+    assert!(*last == 21);
+}

tests/ui/pass/slice_split_first.rs

@@ -0,0 +1,20 @@
+//@check-pass
+//@compile-flags: -C debug-assertions=off
+#[thrust::trusted]
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures(
+    (*result).length == 2
+        && (*result).array[(*result).offset] == 10
+        && (*result).array[(*result).offset + 1] == 20
+)]
+fn slice() -> &'static [i32] {
+    unimplemented!()
+}
+
+fn main() {
+    let slice = slice();
+    let (first, tail) = slice.split_first().unwrap();
+    assert!(*first == 10);
+    assert!(tail.len() == 1);
+    assert!(*tail.first().unwrap() == 20);
+}

tests/ui/pass/slice_split_first_mut.rs

@@ -0,0 +1,20 @@
+//@check-pass
+//@compile-flags: -C debug-assertions=off
+#[thrust::trusted]
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures(
+    (*result).length == 2
+        && (*result).array[(*result).offset] == 10
+        && (*result).array[(*result).offset + 1] == 20
+)]
+fn slice() -> &'static mut [i32] {
+    unimplemented!()
+}
+
+fn main() {
+    let slice = slice();
+    let (first, tail) = slice.split_first_mut().unwrap();
+    assert!(*first == 10);
+    assert!(tail.len() == 1);
+    assert!(*tail.first().unwrap() == 20);
+}

tests/ui/pass/slice_split_last.rs

@@ -0,0 +1,20 @@
+//@check-pass
+//@compile-flags: -C debug-assertions=off
+#[thrust::trusted]
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures(
+    (*result).length == 2
+        && (*result).array[(*result).offset] == 10
+        && (*result).array[(*result).offset + 1] == 20
+)]
+fn slice() -> &'static [i32] {
+    unimplemented!()
+}
+
+fn main() {
+    let slice = slice();
+    let (last, init) = slice.split_last().unwrap();
+    assert!(*last == 20);
+    assert!(init.len() == 1);
+    assert!(*init.first().unwrap() == 10);
+}

tests/ui/pass/slice_split_last_mut.rs

@@ -0,0 +1,20 @@
+//@check-pass
+//@compile-flags: -C debug-assertions=off
+#[thrust::trusted]
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures(
+    (*result).length == 2
+        && (*result).array[(*result).offset] == 10
+        && (*result).array[(*result).offset + 1] == 20
+)]
+fn slice() -> &'static mut [i32] {
+    unimplemented!()
+}
+
+fn main() {
+    let slice = slice();
+    let (last, init) = slice.split_last_mut().unwrap();
+    assert!(*last == 20);
+    assert!(init.len() == 1);
+    assert!(*init.first().unwrap() == 10);
+}