diff --git a/src/analyze/annot.rs b/src/analyze/annot.rs index b246df43..7a0342dd 100644 --- a/src/analyze/annot.rs +++ b/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"), diff --git a/src/analyze/annot_fn.rs b/src/analyze/annot_fn.rs index f817712c..4769a91f 100644 --- a/src/analyze/annot_fn.rs +++ b/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(); diff --git a/src/analyze/did_cache.rs b/src/analyze/did_cache.rs index 4dbcf110..78b35fb5 100644 --- a/src/analyze/did_cache.rs +++ b/src/analyze/did_cache.rs @@ -29,6 +29,7 @@ struct DefIds { seq_singleton: OnceCell>, seq_len: OnceCell>, seq_push: OnceCell>, + seq_subsequence: OnceCell>, seq_concat: OnceCell>, exists: OnceCell>, @@ -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 { + *self + .def_ids + .seq_subsequence + .get_or_init(|| self.annotated_def(&crate::analyze::annot::seq_subsequence_path())) + } + pub fn seq_concat(&self) -> Option { *self .def_ids diff --git a/std.rs b/std.rs index 62d29442..3428336d 100644 --- a/std.rs +++ b/std.rs @@ -239,6 +239,17 @@ mod thrust_models { unimplemented!() } + #[allow(dead_code)] + #[thrust::def::seq_subsequence] + #[thrust::ignored] + pub fn subsequence(self, _start: U, _end: V) -> Self + where + U: super::Model, + V: super::Model, + { + unimplemented!() + } + #[allow(dead_code)] #[thrust::def::seq_concat] #[thrust::ignored] @@ -961,6 +972,87 @@ fn _extern_spec_slice_last_mut(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(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(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(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(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. diff --git a/tests/ui/fail/slice_split_first.rs b/tests/ui/fail/slice_split_first.rs new file mode 100644 index 00000000..6857e4e9 --- /dev/null +++ b/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); +} diff --git a/tests/ui/fail/slice_split_first_mut.rs b/tests/ui/fail/slice_split_first_mut.rs new file mode 100644 index 00000000..504a026d --- /dev/null +++ b/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); +} diff --git a/tests/ui/fail/slice_split_first_mut_mutation_unsound.rs b/tests/ui/fail/slice_split_first_mut_mutation_unsound.rs new file mode 100644 index 00000000..abc11ff5 --- /dev/null +++ b/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); +} diff --git a/tests/ui/fail/slice_split_last.rs b/tests/ui/fail/slice_split_last.rs new file mode 100644 index 00000000..776d903f --- /dev/null +++ b/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); +} diff --git a/tests/ui/fail/slice_split_last_mut.rs b/tests/ui/fail/slice_split_last_mut.rs new file mode 100644 index 00000000..98c0f202 --- /dev/null +++ b/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); +} diff --git a/tests/ui/pass/slice_split_first.rs b/tests/ui/pass/slice_split_first.rs new file mode 100644 index 00000000..0ecd79d1 --- /dev/null +++ b/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); +} diff --git a/tests/ui/pass/slice_split_first_mut.rs b/tests/ui/pass/slice_split_first_mut.rs new file mode 100644 index 00000000..6370b970 --- /dev/null +++ b/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); +} diff --git a/tests/ui/pass/slice_split_last.rs b/tests/ui/pass/slice_split_last.rs new file mode 100644 index 00000000..5a180dde --- /dev/null +++ b/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); +} diff --git a/tests/ui/pass/slice_split_last_mut.rs b/tests/ui/pass/slice_split_last_mut.rs new file mode 100644 index 00000000..1a2b8ab7 --- /dev/null +++ b/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); +}