diff --git a/src/analyze/annot.rs b/src/analyze/annot.rs index 390518dc..440783f3 100644 --- a/src/analyze/annot.rs +++ b/src/analyze/annot.rs @@ -162,6 +162,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 92a8b2c7..8ba6ef81 100644 --- a/src/analyze/annot_fn.rs +++ b/src/analyze/annot_fn.rs @@ -852,6 +852,16 @@ impl<'a, 'tcx> AnnotFnTranslator<'a, 'tcx> { let new_len = len.add(chc::Term::int(1)); return FormulaOrTerm::Term(chc::Term::tuple(vec![new_arr, 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.tuple_proj(0); + let new_len = end.sub(start.clone()); + let new_arr = chc::Term::subarray(arr, start, new_len.clone()); + return FormulaOrTerm::Term(chc::Term::tuple(vec![new_arr, new_len])); + } 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 d29f8510..967c4ad4 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>, @@ -222,6 +223,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/src/chc.rs b/src/chc.rs index ac8e3b99..c6a01ca2 100644 --- a/src/chc.rs +++ b/src/chc.rs @@ -221,6 +221,13 @@ impl Sort { } } + pub fn as_array_elem(&self) -> Option<&Sort> { + match self { + Sort::Array(_, elem) => Some(elem), + _ => None, + } + } + pub fn null() -> Self { Sort::Null } @@ -495,6 +502,9 @@ pub enum Term { MutFinal(Box>), App(Function, Vec>), ArrayEmpty(Sort, Sort), + /// A view whose index `i` reads `array[start + i]` within `[0, length)`. + /// Outside the view, a shared default prevents equality from constraining the backing array. + Subarray(Box>, Box>, Box>), SeqConcat(Sort, Box>), Tuple(Vec>), TupleProj(Box>, usize), @@ -548,6 +558,17 @@ where } } Term::ArrayEmpty(_, _) => allocator.text("[]"), + Term::Subarray(arr, start, length) => allocator + .text("subarray") + .append(allocator.line()) + .append(arr.pretty_atom(allocator)) + .append(allocator.text(",")) + .append(allocator.line()) + .append(start.pretty_atom(allocator)) + .append(allocator.text(",")) + .append(allocator.line()) + .append(length.pretty_atom(allocator)) + .parens(), Term::SeqConcat(_, t) => t.pretty(allocator), Term::Tuple(ts) => { let separator = allocator.text(",").append(allocator.line()); @@ -613,6 +634,11 @@ impl Term { Term::App(fun, args.into_iter().map(|t| t.subst_var(&mut f)).collect()) } Term::ArrayEmpty(s1, s2) => Term::ArrayEmpty(s1, s2), + Term::Subarray(arr, start, length) => Term::Subarray( + Box::new(arr.subst_var(&mut f)), + Box::new(start.subst_var(&mut f)), + Box::new(length.subst_var(f)), + ), Term::SeqConcat(s, t) => Term::SeqConcat(s, Box::new(t.subst_var(f))), Term::Tuple(ts) => Term::Tuple(ts.into_iter().map(|t| t.subst_var(&mut f)).collect()), Term::TupleProj(t, i) => Term::TupleProj(Box::new(t.subst_var(f)), i), @@ -661,6 +687,7 @@ impl Term { fun.sort(args.iter().map(|t| t.sort(&mut var_sort))) } Term::ArrayEmpty(index, elem) => Sort::array(index.clone(), elem.clone()), + Term::Subarray(arr, _, _) => arr.sort(var_sort), Term::SeqConcat(elem, _) => Sort::array(Sort::int(), elem.clone()), Term::Tuple(ts) => { // TODO: remove this @@ -689,6 +716,9 @@ impl Term { Term::MutCurrent(t) => t.fv_impl(), Term::MutFinal(t) => t.fv_impl(), Term::App(_, args) => Box::new(args.iter().flat_map(|t| t.fv_impl())), + Term::Subarray(arr, start, length) => { + Box::new(arr.fv_impl().chain(start.fv_impl()).chain(length.fv_impl())) + } Term::SeqConcat(_, t) => Box::new(t.iter_args().flat_map(|t| t.fv_impl())), Term::Tuple(ts) => Box::new(ts.iter().flat_map(|t| t.fv_impl())), Term::TupleProj(t, _) => t.fv_impl(), @@ -760,6 +790,10 @@ impl Term { Term::SeqConcat(elem_sort, Box::new(SeqConcatTerm { seq1, seq2 })) } + pub fn subarray(array: Term, start: Term, length: Term) -> Self { + Term::Subarray(Box::new(array), Box::new(start), Box::new(length)) + } + pub fn boxed(self) -> Self { Term::Box(Box::new(self)) } @@ -863,23 +897,6 @@ impl Term { ], ); } - // Peephole 2: inline one step of the `seq_concat` recursive definitions to reduce - // indexed access to terms over the underlying sequences. The SMT-defined functions are - // still emitted (so the rewrites use exactly their unfolded form), but pcsat can prove - // indexed properties against the inlined ITE for *any* recursion bound, where unfolding - // through `define-fun-rec` would require an inductive invariant pcsat can't find. - // - // `select(seq_concat(s, t), i) - // ↦ ite(i < len(s), select(array(s), i), select(array(t), i - len(s)))` - // where `s`/`t` are `(array, length)` tuples. - if let Term::SeqConcat(_, t) = self { - let SeqConcatTerm { seq1, seq2 } = *t; - let len1 = seq1.clone().tuple_proj(1); - let cond = index.clone().lt(len1.clone()); - let then_ = seq1.tuple_proj(0).select(index.clone()); - let else_ = seq2.tuple_proj(0).select(index.sub(len1)); - return Term::ite(cond, then_, else_); - } Term::App(Function::SELECT, vec![self, index]) } diff --git a/src/chc/format_context.rs b/src/chc/format_context.rs index 984a788a..9759ca6f 100644 --- a/src/chc/format_context.rs +++ b/src/chc/format_context.rs @@ -21,7 +21,6 @@ use crate::chc::{self, hoice::HoiceDatatypeRenamer}; pub struct FormatContext { renamer: HoiceDatatypeRenamer, datatypes: Vec, - int_array_elem_sorts: BTreeSet, } // FIXME: this is obviously ineffective and should be replaced @@ -47,6 +46,11 @@ fn term_sorts(clause: &chc::Clause, t: &chc::Term, sorts: &mut BTreeSet {} + chc::Term::Subarray(arr, start, length) => { + term_sorts(clause, arr, sorts); + term_sorts(clause, start, sorts); + term_sorts(clause, length, sorts); + } chc::Term::SeqConcat(_, t) => { for arg in t.iter_args() { term_sorts(clause, arg, sorts); @@ -302,21 +306,6 @@ impl FormatContext { } } - let int_array_elem_sorts: BTreeSet<_> = sorts - .iter() - .filter_map(|s| match s { - chc::Sort::Array(index, elem) if **index == chc::Sort::int() => Some(*elem.clone()), - _ => None, - }) - .collect(); - // The `seq_concat` definitions operate on `(array, length)` sequence tuples, so - // make sure that tuple datatype is declared for every element sort we emit one for - for elem in &int_array_elem_sorts { - sorts.insert(chc::Sort::tuple(vec![ - chc::Sort::array(chc::Sort::int(), elem.clone()), - chc::Sort::int(), - ])); - } let datatypes: Vec<_> = sorts .into_iter() .flat_map(builtin_sort_datatype) @@ -324,21 +313,13 @@ impl FormatContext { .filter(|d| d.params == 0) .collect(); let renamer = HoiceDatatypeRenamer::new(&datatypes); - FormatContext { - renamer, - datatypes, - int_array_elem_sorts, - } + FormatContext { renamer, datatypes } } pub fn datatypes(&self) -> &[chc::Datatype] { &self.datatypes } - pub fn int_array_elem_sorts(&self) -> &BTreeSet { - &self.int_array_elem_sorts - } - pub fn box_ctor(&self, sort: &chc::Sort) -> impl std::fmt::Display { let ss = SortSymbol::new(sort).sorts(); format!("box{ss}") @@ -403,11 +384,6 @@ impl FormatContext { format!("matcher_pred<{}>", self.fmt_datatype_symbol(sym)) } - pub fn seq_concat(&self, elem: &chc::Sort) -> impl std::fmt::Display { - let elem = SortSymbol::new(elem); - format!("seq_concat<{}>", elem) - } - fn fmt_sort_impl(&self, sort: &chc::Sort) -> Box { match sort { chc::Sort::Array(s1, s2) => { diff --git a/src/chc/smtlib2.rs b/src/chc/smtlib2.rs index b27982a9..3f7c1d8d 100644 --- a/src/chc/smtlib2.rs +++ b/src/chc/smtlib2.rs @@ -169,13 +169,45 @@ impl<'ctx, 'a> std::fmt::Display for Term<'ctx, 'a> { Term::new(self.ctx, self.clause, &default) ) } + chc::Term::Subarray(arr, start, length) => { + let elem = self + .clause + .term_sort(arr) + .as_array_elem() + .expect("Subarray applied to a non-array term") + .clone(); + let default = chc::Term::default_for(&elem); + write!( + f, + "(lambda ((sub!idx Int)) \ + (ite (and (<= 0 sub!idx) (< sub!idx {len})) \ + (select {arr} (+ {start} sub!idx)) \ + {default}))", + len = Term::new(self.ctx, self.clause, length), + arr = Term::new(self.ctx, self.clause, arr), + start = Term::new(self.ctx, self.clause, start), + default = Term::new(self.ctx, self.clause, &default), + ) + } chc::Term::SeqConcat(elem, t) => { - let name = self.ctx.seq_concat(elem); + let arr1 = t.seq1.clone().tuple_proj(0); + let arr2 = t.seq2.clone().tuple_proj(0); + let len1 = t.seq1.clone().tuple_proj(1); + let len2 = t.seq2.clone().tuple_proj(1); + let default = chc::Term::default_for(elem); write!( f, - "({} {})", - name, - List::open(t.iter_args().map(|t| Term::new(self.ctx, self.clause, t))) + "(lambda ((concat!idx Int)) \ + (ite (and (<= 0 concat!idx) (< concat!idx (+ {len1} {len2}))) \ + (ite (< concat!idx {len1}) \ + (select {arr1} concat!idx) \ + (select {arr2} (- concat!idx {len1}))) \ + {default}))", + arr1 = Term::new(self.ctx, self.clause, &arr1), + arr2 = Term::new(self.ctx, self.clause, &arr2), + len1 = Term::new(self.ctx, self.clause, &len1), + len2 = Term::new(self.ctx, self.clause, &len2), + default = Term::new(self.ctx, self.clause, &default), ) } chc::Term::Tuple(ts) => { @@ -638,30 +670,6 @@ impl<'a> std::fmt::Display for System<'a> { writeln!(f, "{}", MatcherPredFun::new(&self.ctx, datatype))?; } - for elem in self.ctx.int_array_elem_sorts() { - let name = self.ctx.seq_concat(elem); - let elem_ty = self.ctx.fmt_sort(elem); - // The sequences are passed as `(array, length)` tuples - let seq_fields = [ - chc::Sort::array(chc::Sort::int(), elem.clone()), - chc::Sort::int(), - ]; - let seq_ty = self.ctx.fmt_sort(&chc::Sort::tuple(seq_fields.to_vec())); - let ctor = self.ctx.tuple_ctor(&seq_fields); - let array = self.ctx.tuple_proj(&seq_fields, 0); - let len = self.ctx.tuple_proj(&seq_fields, 1); - writeln!( - f, - "(define-fun-rec {name} \ - ((s {seq_ty}) (t {seq_ty})) \ - (Array Int {elem_ty}) \ - (ite (<= ({len} t) 0) ({array} s) \ - (store ({name} s ({ctor} ({array} t) (- ({len} t) 1))) \ - (+ ({len} s) (- ({len} t) 1)) \ - (select ({array} t) (- ({len} t) 1)))))\n", - )?; - } - // insert command from #![thrust::raw_command()] here for raw_command in &self.inner.raw_commands { writeln!(f, "{}\n", RawCommand::new(raw_command))?; diff --git a/src/chc/unbox.rs b/src/chc/unbox.rs index 3fa22595..5e68a84d 100644 --- a/src/chc/unbox.rs +++ b/src/chc/unbox.rs @@ -19,6 +19,11 @@ fn unbox_term(term: Term) -> Term { Term::MutFinal(t) => Term::MutFinal(Box::new(unbox_term(*t))), Term::App(fun, args) => Term::App(fun, args.into_iter().map(unbox_term).collect()), Term::ArrayEmpty(s1, s2) => Term::ArrayEmpty(unbox_sort(s1), unbox_sort(s2)), + Term::Subarray(arr, start, length) => Term::Subarray( + Box::new(unbox_term(*arr)), + Box::new(unbox_term(*start)), + Box::new(unbox_term(*length)), + ), Term::SeqConcat(s, t) => { Term::SeqConcat(unbox_sort(s), Box::new(unbox_seq_concat_term(*t))) } diff --git a/src/rty.rs b/src/rty.rs index cea3583d..64d357ec 100644 --- a/src/rty.rs +++ b/src/rty.rs @@ -1990,6 +1990,11 @@ fn subst_ty_params_in_term(term: &mut chc::Term, subst: &TypeParamSubst subst_ty_params_in_sort(s1, subst); subst_ty_params_in_sort(s2, subst); } + chc::Term::Subarray(arr, start, length) => { + subst_ty_params_in_term(arr, subst); + subst_ty_params_in_term(start, subst); + subst_ty_params_in_term(length, subst); + } chc::Term::SeqConcat(sort, t) => { subst_ty_params_in_sort(sort, subst); for arg in t.iter_args_mut() { diff --git a/std.rs b/std.rs index 96d88669..e5264311 100644 --- a/std.rs +++ b/std.rs @@ -238,6 +238,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] @@ -981,6 +992,85 @@ 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[0], + &(*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).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).length == (*slice).length + && result == Some(( + thrust_models::model::Mut::new((*slice).array[0], (!slice).array[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).length == (*slice).length + && result == Some(( + thrust_models::model::Mut::new( + (*slice).array[(*slice).length - 1], + (!slice).array[(!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/seq_concat_index.rs b/tests/ui/fail/seq_concat_index.rs index 15587a70..fed8909e 100644 --- a/tests/ui/fail/seq_concat_index.rs +++ b/tests/ui/fail/seq_concat_index.rs @@ -4,7 +4,7 @@ use thrust_models::model::{Int, Seq}; -#[thrust_macros::requires(0 <= i && i < s.len())] +#[thrust_macros::requires(0 <= i && i < s.len() && 0 <= t.len())] #[thrust_macros::ensures(s.concat(t)[i] == t[i])] fn concat_index_left(s: Seq, t: Seq, i: Int) -> () { let _ = s; diff --git a/tests/ui/fail/seq_subsequence.rs b/tests/ui/fail/seq_subsequence.rs new file mode 100644 index 00000000..e13a5f80 --- /dev/null +++ b/tests/ui/fail/seq_subsequence.rs @@ -0,0 +1,13 @@ +//@error-in-other-file: Unsat +//@compile-flags: -C debug-assertions=off +//@rustc-env: THRUST_SOLVER=tests/thrust-pcsat-wrapper + +use thrust_models::model::{Int, Seq}; + +#[thrust_macros::requires(x != y)] +#[thrust_macros::ensures(Seq::singleton(x).push(y).subsequence(1, 2)[0] == x)] +fn subsequence_index(x: Int, y: Int) { + let _ = (x, y); +} + +fn main() {} diff --git a/tests/ui/fail/slice_split_first.rs b/tests/ui/fail/slice_split_first.rs new file mode 100644 index 00000000..5fe53816 --- /dev/null +++ b/tests/ui/fail/slice_split_first.rs @@ -0,0 +1,22 @@ +//@error-in-other-file: Unsat +//@compile-flags: -C debug-assertions=off +//@rustc-env: THRUST_SOLVER=tests/thrust-pcsat-wrapper + +#[thrust::trusted] +#[thrust_macros::requires(true)] +#[thrust_macros::ensures( + (*result).length == 2 + && (*result).array[0] == 10 + && (*result).array[1] == 20 +)] +fn slice() -> &'static [i32] { + unimplemented!() +} + +fn main() { + let slice = slice(); + let (boundary, rest) = slice.split_first().unwrap(); + assert!(*boundary == 99); + assert!(rest.len() == 1); + assert!(*rest.first().unwrap() == 20); +} 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..edcec677 --- /dev/null +++ b/tests/ui/fail/slice_split_first_mut.rs @@ -0,0 +1,25 @@ +//@error-in-other-file: Unsat +//@compile-flags: -C debug-assertions=off +//@rustc-env: THRUST_SOLVER=tests/thrust-pcsat-wrapper + +#[thrust::trusted] +#[thrust_macros::requires(true)] +#[thrust_macros::ensures( + (*result).length == 2 + && (*result).array[0] == 10 + && (*result).array[1] == 20 +)] +fn slice() -> &'static mut [i32] { + unimplemented!() +} + +fn main() { + let slice = slice(); + { + let (boundary, rest) = slice.split_first_mut().unwrap(); + *boundary = 11; + *rest.first_mut().unwrap() = 21; + } + assert!(slice[0] == 12); + assert!(slice[1] == 21); +} diff --git a/tests/ui/fail/slice_split_first_mut_preserve.rs b/tests/ui/fail/slice_split_first_mut_preserve.rs new file mode 100644 index 00000000..8b1e207f --- /dev/null +++ b/tests/ui/fail/slice_split_first_mut_preserve.rs @@ -0,0 +1,24 @@ +//@error-in-other-file: Unsat +//@compile-flags: -C debug-assertions=off +//@rustc-env: THRUST_SOLVER=tests/thrust-pcsat-wrapper + +#[thrust::trusted] +#[thrust_macros::requires(true)] +#[thrust_macros::ensures( + (*result).length == 2 + && (*result).array[0] == 10 + && (*result).array[1] == 20 +)] +fn slice() -> &'static mut [i32] { + unimplemented!() +} + +fn main() { + let slice = slice(); + { + let (first, _tail) = slice.split_first_mut().unwrap(); + *first = 11; + } + assert!(slice[0] == 12); + assert!(slice[1] == 20); +} diff --git a/tests/ui/pass/seq_concat_index.rs b/tests/ui/pass/seq_concat_index.rs index f28e5d92..eb790536 100644 --- a/tests/ui/pass/seq_concat_index.rs +++ b/tests/ui/pass/seq_concat_index.rs @@ -4,7 +4,7 @@ use thrust_models::model::{Int, Seq}; -#[thrust_macros::requires(0 <= i && i < s.len())] +#[thrust_macros::requires(0 <= i && i < s.len() && 0 <= t.len())] #[thrust_macros::ensures(s.concat(t)[i] == s[i])] fn concat_index_left(s: Seq, t: Seq, i: Int) -> () { let _ = s; diff --git a/tests/ui/pass/seq_subsequence.rs b/tests/ui/pass/seq_subsequence.rs new file mode 100644 index 00000000..fc1564db --- /dev/null +++ b/tests/ui/pass/seq_subsequence.rs @@ -0,0 +1,26 @@ +//@check-pass +//@compile-flags: -C debug-assertions=off +//@rustc-env: THRUST_SOLVER=tests/thrust-pcsat-wrapper + +use thrust_models::model::{Int, Seq}; + +#[thrust_macros::requires(0 <= start && start <= end && end <= s.len() && 0 <= i && i < end - start)] +#[thrust_macros::ensures( + s.subsequence(start, end).len() == end - start + && s.subsequence(start, end)[i] == s[start + i] +)] +fn subsequence_index(s: Seq, start: Int, end: Int, i: Int) { + let _ = (s, start, end, i); +} + +#[thrust_macros::requires(true)] +#[thrust_macros::ensures( + Seq::singleton(x).push(y).subsequence(1, 2) == Seq::singleton(y) + && Seq::singleton(x).subsequence(0, 0) == Seq::::empty() + && Seq::singleton(x).push(y).subsequence(0, 2).subsequence(1, 2)[0] == y +)] +fn subsequence_normalized(x: Int, y: Int) { + let _ = (x, y); +} + +fn main() {} diff --git a/tests/ui/pass/slice_split_first.rs b/tests/ui/pass/slice_split_first.rs new file mode 100644 index 00000000..be5047b7 --- /dev/null +++ b/tests/ui/pass/slice_split_first.rs @@ -0,0 +1,22 @@ +//@check-pass +//@compile-flags: -C debug-assertions=off +//@rustc-env: THRUST_SOLVER=tests/thrust-pcsat-wrapper + +#[thrust::trusted] +#[thrust_macros::requires(true)] +#[thrust_macros::ensures( + (*result).length == 2 + && (*result).array[0] == 10 + && (*result).array[1] == 20 +)] +fn slice() -> &'static [i32] { + unimplemented!() +} + +fn main() { + let slice = slice(); + let (boundary, rest) = slice.split_first().unwrap(); + assert!(*boundary == 10); + assert!(rest.len() == 1); + assert!(*rest.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..36c2083b --- /dev/null +++ b/tests/ui/pass/slice_split_first_mut.rs @@ -0,0 +1,25 @@ +//@check-pass +//@compile-flags: -C debug-assertions=off +//@rustc-env: THRUST_SOLVER=tests/thrust-pcsat-wrapper + +#[thrust::trusted] +#[thrust_macros::requires(true)] +#[thrust_macros::ensures( + (*result).length == 2 + && (*result).array[0] == 10 + && (*result).array[1] == 20 +)] +fn slice() -> &'static mut [i32] { + unimplemented!() +} + +fn main() { + let slice = slice(); + { + let (boundary, rest) = slice.split_first_mut().unwrap(); + *boundary = 11; + *rest.first_mut().unwrap() = 21; + } + assert!(slice[0] == 11); + assert!(slice[1] == 21); +} diff --git a/tests/ui/pass/slice_split_first_mut_preserve.rs b/tests/ui/pass/slice_split_first_mut_preserve.rs new file mode 100644 index 00000000..6d65f84d --- /dev/null +++ b/tests/ui/pass/slice_split_first_mut_preserve.rs @@ -0,0 +1,24 @@ +//@check-pass +//@compile-flags: -C debug-assertions=off +//@rustc-env: THRUST_SOLVER=tests/thrust-pcsat-wrapper + +#[thrust::trusted] +#[thrust_macros::requires(true)] +#[thrust_macros::ensures( + (*result).length == 2 + && (*result).array[0] == 10 + && (*result).array[1] == 20 +)] +fn slice() -> &'static mut [i32] { + unimplemented!() +} + +fn main() { + let slice = slice(); + { + let (first, _tail) = slice.split_first_mut().unwrap(); + *first = 11; + } + assert!(slice[0] == 11); + assert!(slice[1] == 20); +}