From 62fba0ca8d7e31b6f6f3691dbf0089380d5a0345 Mon Sep 17 00:00:00 2001 From: coord_e Date: Tue, 15 Sep 2026 23:42:40 +0900 Subject: [PATCH 1/5] Represent slices with native SMT sequences --- src/analyze/annot.rs | 16 ++ src/analyze/annot_fn.rs | 69 +++--- src/analyze/basic_block.rs | 24 +- src/analyze/did_cache.rs | 16 ++ src/chc.rs | 134 +++++------ src/chc/format_context.rs | 39 +--- src/chc/smtlib2.rs | 34 +-- src/chc/unbox.rs | 12 +- src/refine/template.rs | 14 ++ src/rty.rs | 20 +- src/rty/subtyping.rs | 3 + std.rs | 221 ++++++++++++------ .../fail/loop_invariant_fn_param_at_entry.rs | 4 +- tests/ui/fail/seq_concat_index.rs | 2 +- tests/ui/fail/seq_specs_vec_build.rs | 8 +- tests/ui/fail/seq_subsequence.rs | 13 ++ tests/ui/fail/slice_first_mut.rs | 2 +- tests/ui/fail/slice_index.rs | 2 +- tests/ui/fail/slice_index_mut.rs | 2 +- tests/ui/fail/slice_last_mut.rs | 4 +- tests/ui/fail/slice_methods.rs | 6 +- tests/ui/fail/slice_methods_mut.rs | 2 +- tests/ui/fail/slice_split_first.rs | 22 ++ tests/ui/fail/slice_split_first_loop.rs | 20 ++ .../fail/slice_split_first_loop_invariant.rs | 23 ++ tests/ui/fail/slice_split_first_mut.rs | 25 ++ tests/ui/fail/slice_split_first_mut_loop.rs | 27 +++ .../slice_split_first_mut_loop_invariant.rs | 35 +++ .../ui/fail/slice_split_first_mut_preserve.rs | 24 ++ .../pass/loop_invariant_fn_param_at_entry.rs | 4 +- tests/ui/pass/seq_concat_index.rs | 2 +- tests/ui/pass/seq_specs_vec_build.rs | 8 +- tests/ui/pass/seq_subsequence.rs | 26 +++ tests/ui/pass/slice_first_mut.rs | 2 +- tests/ui/pass/slice_index.rs | 6 +- tests/ui/pass/slice_index_mut.rs | 2 +- tests/ui/pass/slice_last_mut.rs | 4 +- tests/ui/pass/slice_methods.rs | 10 +- tests/ui/pass/slice_methods_mut.rs | 2 +- tests/ui/pass/slice_split_first.rs | 22 ++ tests/ui/pass/slice_split_first_loop.rs | 20 ++ .../pass/slice_split_first_loop_invariant.rs | 23 ++ tests/ui/pass/slice_split_first_mut.rs | 25 ++ tests/ui/pass/slice_split_first_mut_loop.rs | 27 +++ .../slice_split_first_mut_loop_invariant.rs | 35 +++ .../ui/pass/slice_split_first_mut_preserve.rs | 24 ++ 46 files changed, 747 insertions(+), 318 deletions(-) create mode 100644 tests/ui/fail/seq_subsequence.rs create mode 100644 tests/ui/fail/slice_split_first.rs create mode 100644 tests/ui/fail/slice_split_first_loop.rs create mode 100644 tests/ui/fail/slice_split_first_loop_invariant.rs create mode 100644 tests/ui/fail/slice_split_first_mut.rs create mode 100644 tests/ui/fail/slice_split_first_mut_loop.rs create mode 100644 tests/ui/fail/slice_split_first_mut_loop_invariant.rs create mode 100644 tests/ui/fail/slice_split_first_mut_preserve.rs create mode 100644 tests/ui/pass/seq_subsequence.rs create mode 100644 tests/ui/pass/slice_split_first.rs create mode 100644 tests/ui/pass/slice_split_first_loop.rs create mode 100644 tests/ui/pass/slice_split_first_loop_invariant.rs create mode 100644 tests/ui/pass/slice_split_first_mut.rs create mode 100644 tests/ui/pass/slice_split_first_mut_loop.rs create mode 100644 tests/ui/pass/slice_split_first_mut_loop_invariant.rs create mode 100644 tests/ui/pass/slice_split_first_mut_preserve.rs diff --git a/src/analyze/annot.rs b/src/analyze/annot.rs index 390518dc..b7d7098b 100644 --- a/src/analyze/annot.rs +++ b/src/analyze/annot.rs @@ -162,6 +162,22 @@ pub fn seq_push_path() -> [Symbol; 3] { ] } +pub fn seq_store_path() -> [Symbol; 3] { + [ + Symbol::intern("thrust"), + Symbol::intern("def"), + Symbol::intern("seq_store"), + ] +} + +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..0535d668 100644 --- a/src/analyze/annot_fn.rs +++ b/src/analyze/annot_fn.rs @@ -581,17 +581,6 @@ impl<'a, 'tcx> AnnotFnTranslator<'a, 'tcx> { self.type_builder.build(elem_ty) } - fn adt_arg_type_at( - &self, - expr: &'tcx rustc_hir::Expr<'tcx>, - idx: usize, - ) -> rty::Type { - let mir_ty::TyKind::Adt(_, args) = self.expr_ty(expr).kind() else { - panic!("expected ADT"); - }; - self.type_builder.build(args.type_at(idx)) - } - fn variant_ctor_term( &self, ctor_did: rustc_span::def_id::DefId, @@ -807,18 +796,17 @@ impl<'a, 'tcx> AnnotFnTranslator<'a, 'tcx> { FormulaOrTerm::Term(term.tuple_proj(index)) } ExprKind::Index(array, index, _) => { - let array_ty = self.expr_ty(array); - let array_term = self.to_term(array); let index_term = self.to_term(index); - let is_seq = array_ty + let is_seq = self + .expr_ty(array) .ty_adt_def() .is_some_and(|adt| Some(adt.did()) == self.def_ids.seq_model()); - let array_inner = if is_seq { - array_term.tuple_proj(0) + let term = if is_seq { + self.to_term(array).seq_nth(index_term) } else { - array_term + self.to_term(array).select(index_term) }; - FormulaOrTerm::Term(array_inner.select(index_term)) + FormulaOrTerm::Term(term) } ExprKind::MethodCall(method, receiver, args, _) => { if let Some(def_id) = self.typeck.type_dependent_def_id(hir.hir_id) { @@ -840,28 +828,34 @@ impl<'a, 'tcx> AnnotFnTranslator<'a, 'tcx> { if Some(def_id) == self.def_ids.seq_len() { assert!(args.is_empty(), "Seq::len does not take any arguments"); let t = self.to_term(receiver); - return FormulaOrTerm::Term(t.tuple_proj(1)); + return FormulaOrTerm::Term(t.seq_len()); } if Some(def_id) == self.def_ids.seq_push() { assert_eq!(args.len(), 1, "Seq::push takes exactly 1 argument"); let t = self.to_term(receiver); let v = self.to_term(&args[0]); - let arr = t.clone().tuple_proj(0); - let len = t.tuple_proj(1); - let new_arr = arr.store(len.clone(), v); - let new_len = len.add(chc::Term::int(1)); - return FormulaOrTerm::Term(chc::Term::tuple(vec![new_arr, new_len])); + return FormulaOrTerm::Term(t.seq_concat(v.seq_unit())); + } + if Some(def_id) == self.def_ids.seq_store() { + assert_eq!(args.len(), 2, "Seq::store takes exactly 2 arguments"); + let seq = self.to_term(receiver); + let index = self.to_term(&args[0]); + let value = self.to_term(&args[1]); + return FormulaOrTerm::Term(seq.seq_store(index, value)); + } + if Some(def_id) == self.def_ids.seq_subsequence() { + assert_eq!(args.len(), 2, "Seq::subsequence takes exactly 2 arguments"); + let seq = self.to_term(receiver); + let start = self.to_term(&args[0]); + let end = self.to_term(&args[1]); + let length = end.sub(start.clone()); + return FormulaOrTerm::Term(seq.seq_extract(start, length)); } 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(); - let t = self.to_term(receiver); + let seq = self.to_term(receiver); let other = self.to_term(&args[0]); - let a_len = t.clone().tuple_proj(1); - let b_len = other.clone().tuple_proj(1); - let new_arr = chc::Term::seq_concat(elem_sort, t, other); - let new_len = a_len.add(b_len); - return FormulaOrTerm::Term(chc::Term::tuple(vec![new_arr, new_len])); + return FormulaOrTerm::Term(seq.seq_concat(other)); } } unimplemented!("unsupported method call in formula: {:?}", method) @@ -941,21 +935,12 @@ impl<'a, 'tcx> AnnotFnTranslator<'a, 'tcx> { if Some(def_id) == self.def_ids.seq_empty() { assert!(args.is_empty(), "Seq::empty does not take any arguments"); let elem_sort = self.node_arg_type_at(func_expr.hir_id, 0).to_sort(); - return FormulaOrTerm::Term(chc::Term::tuple(vec![ - chc::Term::array_empty(chc::Sort::int(), elem_sort), - chc::Term::int(0), - ])); + return FormulaOrTerm::Term(chc::Term::seq_empty(elem_sort)); } if Some(def_id) == self.def_ids.seq_singleton() { assert_eq!(args.len(), 1, "Seq::singleton takes exactly 1 argument"); let v = self.to_term(&args[0]); - let elem_sort = self.node_arg_type_at(func_expr.hir_id, 0).to_sort(); - let new_arr = chc::Term::array_empty(chc::Sort::int(), elem_sort) - .store(chc::Term::int(0), v); - return FormulaOrTerm::Term(chc::Term::tuple(vec![ - new_arr, - chc::Term::int(1), - ])); + return FormulaOrTerm::Term(v.seq_unit()); } if let rustc_hir::def::DefKind::Ctor(ctor_of, _) = def_kind { let terms = args.iter().map(|e| self.to_term(e)).collect(); diff --git a/src/analyze/basic_block.rs b/src/analyze/basic_block.rs index e244aa3a..8902d065 100644 --- a/src/analyze/basic_block.rs +++ b/src/analyze/basic_block.rs @@ -544,29 +544,19 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { Rvalue::Aggregate(kind, fields) => { match *kind { mir::AggregateKind::Array(mir_elem_ty) => { - // Build Seq = (Box>, Box) from array literal elements, - // pinning each element at its index via store folds. - // // TODO: Stop embedding knowledge of `<[T; N] as Model>::Ty` in the analyzer let mut builder = PlaceTypeBuilder::default(); let elem_ty = self.type_builder.build(mir_elem_ty).vacuous(); - let mut arr_term = - chc::Term::array_empty(chc::Sort::int(), elem_ty.to_sort()); - for (i, field) in fields.iter().enumerate() { + let mut seq = chc::Term::seq_empty(elem_ty.to_sort()); + for field in fields.iter() { let pty = self.operand_type(field.clone()); let (_, elem_term) = builder.subsume(pty); - arr_term = arr_term.store(chc::Term::int(i as i64), elem_term); + seq = seq.seq_concat(elem_term.seq_unit()); } - let arr_pty = builder.build( - rty::ArrayType::new(rty::Type::int(), elem_ty).into(), - arr_term, - ); - let size = fields.len(); - let size_pty = PlaceType::with_ty_and_term( - rty::Type::int(), - chc::Term::int(size as i64), - ); - PlaceType::tuple(vec![arr_pty.boxed(), size_pty.boxed()]) + builder.build( + rty::Type::Seq(Box::new(rty::RefinedType::unrefined(elem_ty))), + seq, + ) } mir::AggregateKind::Adt(did, variant_idx, args, _, _) if self.tcx.def_kind(did) == DefKind::Enum => diff --git a/src/analyze/did_cache.rs b/src/analyze/did_cache.rs index d29f8510..55aa1f40 100644 --- a/src/analyze/did_cache.rs +++ b/src/analyze/did_cache.rs @@ -29,6 +29,8 @@ struct DefIds { seq_singleton: OnceCell>, seq_len: OnceCell>, seq_push: OnceCell>, + seq_store: OnceCell>, + seq_subsequence: OnceCell>, seq_concat: OnceCell>, exists: OnceCell>, @@ -222,6 +224,20 @@ impl<'tcx> DefIdCache<'tcx> { .get_or_init(|| self.annotated_def(&crate::analyze::annot::seq_push_path())) } + pub fn seq_store(&self) -> Option { + *self + .def_ids + .seq_store + .get_or_init(|| self.annotated_def(&crate::analyze::annot::seq_store_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..110916db 100644 --- a/src/chc.rs +++ b/src/chc.rs @@ -96,6 +96,7 @@ pub enum Sort { Mut(Box), Tuple(Vec), Array(Box, Box), + Seq(Box), Datatype(DatatypeSort), } @@ -153,6 +154,9 @@ where ) } } + Sort::Seq(elem) => allocator + .text("Seq") + .append(elem.pretty(allocator).angles()), Sort::Datatype(sort) => sort.pretty(allocator), } } @@ -181,7 +185,7 @@ impl Sort { f(self); match self { Sort::Null | Sort::Int | Sort::Bool | Sort::String | Sort::Param(_) => {} - Sort::Box(s) | Sort::Mut(s) => s.walk(Box::new(&mut f)), + Sort::Box(s) | Sort::Mut(s) | Sort::Seq(s) => s.walk(Box::new(&mut f)), Sort::Tuple(ss) => { for s in ss { s.walk(Box::new(&mut f)); @@ -257,6 +261,10 @@ impl Sort { Sort::Array(Box::new(from), Box::new(to)) } + pub fn seq(elem: Sort) -> Self { + Sort::Seq(Box::new(elem)) + } + pub fn datatype(symbol: DatatypeSymbol, args: Vec) -> Self { Sort::Datatype(DatatypeSort { symbol, args }) } @@ -289,7 +297,7 @@ impl Sort { pub fn instantiate_params(&mut self, args: &[Sort]) { match self { Sort::Param(i) => *self = args[*i].clone(), - Sort::Box(s) => s.instantiate_params(args), + Sort::Box(s) | Sort::Seq(s) => s.instantiate_params(args), Sort::Mut(s) => s.instantiate_params(args), Sort::Tuple(ss) => { for s in ss { @@ -407,7 +415,15 @@ impl Function { Self::OR => Sort::bool(), Self::NOT => Sort::bool(), Self::NEG => Sort::int(), - Self::STORE => args.into_iter().next().unwrap(), + Self::STORE | Self::SEQ_CONCAT | Self::SEQ_EXTRACT => args.into_iter().next().unwrap(), + Self::SEQ_LEN => Sort::int(), + Self::SEQ_UNIT => Sort::seq(args.into_iter().next().unwrap()), + Self::SEQ_NTH => { + let Sort::Seq(elem) = args.into_iter().next().unwrap() else { + panic!("invalid SEQ_NTH sort"); + }; + *elem + } Self::SELECT => { let Sort::Array(_, elem) = args.into_iter().next().unwrap() else { panic!("invalid SELECT sort"); @@ -433,53 +449,14 @@ impl Function { pub const NEG: Function = Function::new("-"); pub const STORE: Function = Function::new("store"); pub const SELECT: Function = Function::new("select"); + pub const SEQ_CONCAT: Function = Function::new("seq.++"); + pub const SEQ_EXTRACT: Function = Function::new("seq.extract"); + pub const SEQ_LEN: Function = Function::new("seq.len"); + pub const SEQ_UNIT: Function = Function::new("seq.unit"); + pub const SEQ_NTH: Function = Function::new("seq.nth"); pub const ITE: Function = Function::new("ite"); } -#[derive(Debug, Clone)] -pub struct SeqConcatTerm { - pub seq1: Term, - pub seq2: Term, -} - -impl<'a, D, V> Pretty<'a, D, termcolor::ColorSpec> for &SeqConcatTerm -where - V: Var, - D: pretty::DocAllocator<'a, termcolor::ColorSpec>, - D::Doc: Clone, -{ - fn pretty(self, allocator: &'a D) -> pretty::DocBuilder<'a, D, termcolor::ColorSpec> { - allocator - .text("concat") - .append(allocator.line()) - .append(self.seq1.pretty_atom(allocator)) - .append(allocator.text(",")) - .append(allocator.line()) - .append(self.seq2.pretty_atom(allocator)) - .parens() - } -} - -impl SeqConcatTerm { - pub fn iter_args(&self) -> impl Iterator> { - std::iter::once(&self.seq1).chain(std::iter::once(&self.seq2)) - } - - pub fn iter_args_mut(&mut self) -> impl Iterator> { - std::iter::once(&mut self.seq1).chain(std::iter::once(&mut self.seq2)) - } - - pub fn subst_var(self, mut f: F) -> SeqConcatTerm - where - F: FnMut(V) -> Term, - { - SeqConcatTerm { - seq1: self.seq1.subst_var(&mut f), - seq2: self.seq2.subst_var(f), - } - } -} - /// A logical term. #[derive(Debug, Clone)] pub enum Term { @@ -495,7 +472,7 @@ pub enum Term { MutFinal(Box>), App(Function, Vec>), ArrayEmpty(Sort, Sort), - SeqConcat(Sort, Box>), + SeqEmpty(Sort), Tuple(Vec>), TupleProj(Box>, usize), DatatypeCtor(DatatypeSort, DatatypeSymbol, Vec>), @@ -548,7 +525,7 @@ where } } Term::ArrayEmpty(_, _) => allocator.text("[]"), - Term::SeqConcat(_, t) => t.pretty(allocator), + Term::SeqEmpty(_) => allocator.text("seq.empty"), Term::Tuple(ts) => { let separator = allocator.text(",").append(allocator.line()); if ts.len() == 1 { @@ -613,7 +590,7 @@ 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::SeqConcat(s, t) => Term::SeqConcat(s, Box::new(t.subst_var(f))), + Term::SeqEmpty(s) => Term::SeqEmpty(s), 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), Term::DatatypeCtor(sort, c_sym, args) => Term::DatatypeCtor( @@ -661,7 +638,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::SeqConcat(elem, _) => Sort::array(Sort::int(), elem.clone()), + Term::SeqEmpty(elem) => Sort::seq(elem.clone()), Term::Tuple(ts) => { // TODO: remove this let mut var_sort: Box Sort> = Box::new(var_sort); @@ -689,7 +666,7 @@ 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::SeqConcat(_, t) => Box::new(t.iter_args().flat_map(|t| t.fv_impl())), + Term::SeqEmpty(_) => Box::new(std::iter::empty()), Term::Tuple(ts) => Box::new(ts.iter().flat_map(|t| t.fv_impl())), Term::TupleProj(t, _) => t.fv_impl(), Term::DatatypeCtor(_, _, args) => Box::new(args.iter().flat_map(|t| t.fv_impl())), @@ -737,6 +714,7 @@ impl Term { ), Sort::Tuple(ts) => Term::Tuple(ts.iter().map(Self::default_for).collect()), Sort::Array(i, e) => Term::ArrayEmpty((**i).clone(), (**e).clone()), + Sort::Seq(elem) => Term::SeqEmpty((**elem).clone()), // TODO: defaults for Datatype and Param. Sort::Datatype(_) | Sort::Param(_) => { unimplemented!("no default value for sort {sort:?}") @@ -756,8 +734,39 @@ impl Term { Term::ArrayEmpty(index, elem) } - pub fn seq_concat(elem_sort: Sort, seq1: Term, seq2: Term) -> Self { - Term::SeqConcat(elem_sort, Box::new(SeqConcatTerm { seq1, seq2 })) + pub fn seq_empty(elem: Sort) -> Self { + Term::SeqEmpty(elem) + } + + pub fn seq_unit(self) -> Self { + Term::App(Function::SEQ_UNIT, vec![self]) + } + + pub fn seq_concat(self, other: Self) -> Self { + Term::App(Function::SEQ_CONCAT, vec![self, other]) + } + + pub fn seq_extract(self, start: Self, length: Self) -> Self { + Term::App(Function::SEQ_EXTRACT, vec![self, start, length]) + } + + pub fn seq_len(self) -> Self { + Term::App(Function::SEQ_LEN, vec![self]) + } + + pub fn seq_nth(self, index: Self) -> Self { + Term::App(Function::SEQ_NTH, vec![self, index]) + } + + pub fn seq_store(self, index: Self, elem: Self) -> Self + where + V: Clone, + { + let prefix = self.clone().seq_extract(Self::int(0), index.clone()); + let suffix_start = index.add(Self::int(1)); + let suffix_length = self.clone().seq_len().sub(suffix_start.clone()); + let suffix = self.seq_extract(suffix_start, suffix_length); + prefix.seq_concat(elem.seq_unit()).seq_concat(suffix) } pub fn boxed(self) -> Self { @@ -863,23 +872,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..6f60f39f 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,11 +46,7 @@ fn term_sorts(clause: &chc::Clause, t: &chc::Term, sorts: &mut BTreeSet {} - chc::Term::SeqConcat(_, t) => { - for arg in t.iter_args() { - term_sorts(clause, arg, sorts); - } - } + chc::Term::SeqEmpty(_) => {} chc::Term::Tuple(ts) => { for t in ts { term_sorts(clause, t, sorts); @@ -89,6 +84,7 @@ impl<'a> std::fmt::Display for SortSymbol<'a> { chc::Sort::Param(i) => write!(f, "T{}", i), chc::Sort::Box(s) => write!(f, "Box{}", SortSymbol::new(s).sorts()), chc::Sort::Mut(s) => write!(f, "Mut{}", SortSymbol::new(s).sorts()), + chc::Sort::Seq(elem) => write!(f, "Seq{}", SortSymbol::new(elem).sorts()), chc::Sort::Tuple(ss) => write!(f, "Tuple{}", SortSymbols::new(ss)), chc::Sort::Array(s1, s2) => { write!(f, "Array{}", SortSymbols::new(&[*s1.clone(), *s2.clone()])) @@ -302,21 +298,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 +305,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,13 +376,9 @@ 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::Seq(elem) => Box::new(format!("(Seq {})", self.fmt_sort(elem))), chc::Sort::Array(s1, s2) => { let s1 = self.fmt_sort(s1); let s2 = self.fmt_sort(s2); diff --git a/src/chc/smtlib2.rs b/src/chc/smtlib2.rs index b27982a9..9079256c 100644 --- a/src/chc/smtlib2.rs +++ b/src/chc/smtlib2.rs @@ -169,14 +169,8 @@ impl<'ctx, 'a> std::fmt::Display for Term<'ctx, 'a> { Term::new(self.ctx, self.clause, &default) ) } - chc::Term::SeqConcat(elem, t) => { - let name = self.ctx.seq_concat(elem); - write!( - f, - "({} {})", - name, - List::open(t.iter_args().map(|t| Term::new(self.ctx, self.clause, t))) - ) + chc::Term::SeqEmpty(elem) => { + write!(f, "(as seq.empty (Seq {}))", self.ctx.fmt_sort(elem)) } chc::Term::Tuple(ts) => { let ss: Vec<_> = ts.iter().map(|t| self.clause.term_sort(t)).collect(); @@ -638,30 +632,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..70a7bb77 100644 --- a/src/chc/unbox.rs +++ b/src/chc/unbox.rs @@ -2,13 +2,6 @@ use super::*; -fn unbox_seq_concat_term(t: SeqConcatTerm) -> SeqConcatTerm { - let SeqConcatTerm { seq1, seq2 } = t; - let seq1 = unbox_term(seq1); - let seq2 = unbox_term(seq2); - SeqConcatTerm { seq1, seq2 } -} - fn unbox_term(term: Term) -> Term { match term { Term::Var(_) | Term::Bool(_) | Term::Int(_) | Term::String(_) | Term::Null => term, @@ -19,9 +12,7 @@ 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::SeqConcat(s, t) => { - Term::SeqConcat(unbox_sort(s), Box::new(unbox_seq_concat_term(*t))) - } + Term::SeqEmpty(s) => Term::SeqEmpty(unbox_sort(s)), Term::Tuple(ts) => Term::Tuple(ts.into_iter().map(unbox_term).collect()), Term::TupleProj(t, i) => Term::TupleProj(Box::new(unbox_term(*t)), i), Term::DatatypeCtor(s1, s2, args) => Term::DatatypeCtor( @@ -82,6 +73,7 @@ fn unbox_sort(sort: Sort) -> Sort { Sort::Mut(inner) => Sort::Mut(Box::new(unbox_sort(*inner))), Sort::Tuple(sorts) => Sort::Tuple(sorts.into_iter().map(unbox_sort).collect()), Sort::Array(s1, s2) => Sort::Array(Box::new(unbox_sort(*s1)), Box::new(unbox_sort(*s2))), + Sort::Seq(elem) => Sort::seq(unbox_sort(*elem)), Sort::Datatype(sort) => Sort::Datatype(unbox_datatype_sort(sort)), } } diff --git a/src/refine/template.rs b/src/refine/template.rs index 246688cc..fd471a26 100644 --- a/src/refine/template.rs +++ b/src/refine/template.rs @@ -188,6 +188,13 @@ impl<'tcx> TypeBuilder<'tcx> { return Some(rty::PointerType::own(elem_ty).into()); } + if Some(adt.did()) == self.def_ids.seq_model() { + let elem_ty = self.build(args.type_at(0)); + return Some(rty::Type::Seq(Box::new(rty::RefinedType::unrefined( + elem_ty, + )))); + } + if Some(adt.did()) == self.def_ids.array_model() { let idx_ty = self.build(args.type_at(0)); let elem_ty = self.build(args.type_at(1)); @@ -375,6 +382,13 @@ where return Some(rty::PointerType::own(elem_ty).into()); } + if Some(adt.did()) == self.inner.def_ids.seq_model() { + let elem_ty = self.build(args.type_at(0)); + return Some(rty::Type::Seq(Box::new(rty::RefinedType::unrefined( + elem_ty, + )))); + } + if Some(adt.did()) == self.inner.def_ids.array_model() { let idx_ty = self.build(args.type_at(0)); let elem_ty = self.build(args.type_at(1)); diff --git a/src/rty.rs b/src/rty.rs index cea3583d..5f1a08e5 100644 --- a/src/rty.rs +++ b/src/rty.rs @@ -936,6 +936,7 @@ pub enum Type { Function(FunctionType), Tuple(TupleType), Array(ArrayType), + Seq(Box>), Enum(EnumType), } @@ -992,6 +993,9 @@ where Type::Function(ty) => ty.pretty(allocator), Type::Tuple(ty) => ty.pretty(allocator), Type::Array(ty) => ty.pretty(allocator), + Type::Seq(elem) => allocator + .text("Seq") + .append(elem.pretty(allocator).angles()), Type::Enum(ty) => ty.pretty(allocator), } } @@ -1136,6 +1140,7 @@ impl Type { let elem_sorts = ty.elems.iter().map(|ty| ty.ty.to_sort()).collect(); chc::Sort::tuple(elem_sorts) } + Type::Seq(elem) => chc::Sort::seq(elem.ty.to_sort()), Type::Array(ty) => { let index_sort = ty.index.ty.to_sort(); let elem_sort = ty.elem.ty.to_sort(); @@ -1162,6 +1167,7 @@ impl Type { Type::Function(ty) => Type::Function(ty), Type::Tuple(ty) => Type::Tuple(ty.subst_var(f)), Type::Array(ty) => Type::Array(ty.subst_var(f)), + Type::Seq(elem) => Type::Seq(Box::new(elem.subst_var(f))), Type::Enum(ty) => Type::Enum(ty.subst_var(f)), } } @@ -1180,6 +1186,7 @@ impl Type { Type::Function(ty) => Type::Function(ty), Type::Tuple(ty) => Type::Tuple(ty.map_var(f)), Type::Array(ty) => Type::Array(ty.map_var(f)), + Type::Seq(elem) => Type::Seq(Box::new(elem.map_var(f))), Type::Enum(ty) => Type::Enum(ty.map_var(f)), } } @@ -1199,6 +1206,7 @@ impl Type { Type::Function(ty) => Type::Function(ty), Type::Tuple(ty) => Type::Tuple(ty.strip_refinement()), Type::Array(ty) => Type::Array(ty.strip_refinement()), + Type::Seq(elem) => Type::Seq(Box::new(RefinedType::unrefined(elem.strip_refinement()))), Type::Enum(ty) => Type::Enum(ty.strip_refinement()), } } @@ -1211,6 +1219,7 @@ impl Type { Type::Function(ty) => ty.free_ty_params(), Type::Tuple(ty) => ty.free_ty_params(), Type::Array(ty) => ty.free_ty_params(), + Type::Seq(elem) => elem.free_ty_params(), Type::Enum(ty) => ty.free_ty_params(), } } @@ -1833,6 +1842,7 @@ impl RefinedType { } Type::Tuple(ty) => ty.subst_ty_params(subst), Type::Array(ty) => ty.subst_ty_params(subst), + Type::Seq(elem) => elem.subst_ty_params(subst), Type::Enum(ty) => ty.subst_ty_params(subst), } } @@ -1872,6 +1882,7 @@ impl RefinedType { } (Type::Tuple(ty1), Type::Tuple(ty2)) => ty1.unify_ty_params(ty2), (Type::Array(ty1), Type::Array(ty2)) => ty1.unify_ty_params(ty2), + (Type::Seq(elem1), Type::Seq(elem2)) => elem1.unify_ty_params(*elem2), (Type::Enum(ty1), Type::Enum(ty2)) => ty1.unify_ty_params(ty2), (t1, t2) => panic!("unify_ty_params: mismatched types t1={:?}, t2={:?}", t1, t2), } @@ -1894,7 +1905,7 @@ fn subst_ty_params_in_sort(sort: &mut chc::Sort, subst: &TypeParamSubst) { *sort = rty.ty.to_sort(); } } - chc::Sort::Box(s) | chc::Sort::Mut(s) => { + chc::Sort::Box(s) | chc::Sort::Mut(s) | chc::Sort::Seq(s) => { subst_ty_params_in_sort(s, subst); } chc::Sort::Tuple(sorts) => { @@ -1990,12 +2001,7 @@ 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::SeqConcat(sort, t) => { - subst_ty_params_in_sort(sort, subst); - for arg in t.iter_args_mut() { - subst_ty_params_in_term(arg, subst); - } - } + chc::Term::SeqEmpty(sort) => subst_ty_params_in_sort(sort, subst), chc::Term::DatatypeCtor(s, _, args) => { for arg in s.args_mut() { subst_ty_params_in_sort(arg, subst); diff --git a/src/rty/subtyping.rs b/src/rty/subtyping.rs index 6c713e0e..c2bd07eb 100644 --- a/src/rty/subtyping.rs +++ b/src/rty/subtyping.rs @@ -138,6 +138,9 @@ where let cs = relate_refined_type(&builder, &got.ret, &expected.ret, relation); clauses.extend(cs); } + (Type::Seq(got), Type::Seq(expected)) => { + clauses.extend(relate_refined_type(scope, got, expected, relation)); + } (Type::Array(got), Type::Array(expected)) => { let cs1 = relate_refined_type(scope, &got.index, &expected.index, relation); clauses.extend(cs1); diff --git a/std.rs b/std.rs index 96d88669..e2880d91 100644 --- a/std.rs +++ b/std.rs @@ -188,10 +188,7 @@ mod thrust_models { } #[thrust::def::seq_model] - pub struct Seq { - pub array: Array, - pub length: Int, - } + pub struct Seq(PhantomData); impl PartialEq for Seq where U: super::Model { #[thrust::ignored] @@ -238,6 +235,27 @@ mod thrust_models { unimplemented!() } + #[allow(dead_code)] + #[thrust::def::seq_store] + #[thrust::ignored] + pub fn store(self, _index: U, _value: T) -> Self + where + U: super::Model, + { + 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] @@ -745,14 +763,14 @@ fn _extern_spec_i32_is_negative(x: i32) -> bool { #[thrust::extern_spec_fn] #[thrust_macros::requires(true)] -#[thrust_macros::ensures(result.length == 0)] +#[thrust_macros::ensures(result.len() == 0)] fn _extern_spec_vec_new() -> Vec where T: thrust_models::Model, T::Ty: PartialEq { Vec::::new() } #[thrust::extern_spec_fn] #[thrust_macros::requires(true)] -#[thrust_macros::ensures(!vec == thrust_models::model::Seq { array: (*vec).array.store((*vec).length, elem), length: (*vec).length + 1 })] +#[thrust_macros::ensures(!vec == (*vec).push(elem))] fn _extern_spec_vec_push(vec: &mut Vec, elem: T) where T: thrust_models::Model, T::Ty: PartialEq { @@ -761,24 +779,24 @@ fn _extern_spec_vec_push(vec: &mut Vec, elem: T) #[thrust::extern_spec_fn] #[thrust_macros::requires(true)] -#[thrust_macros::ensures(result == (*vec).length)] +#[thrust_macros::ensures(result == (*vec).len())] fn _extern_spec_vec_len(vec: &Vec) -> usize where T: thrust_models::Model, T::Ty: PartialEq { Vec::len(vec) } #[thrust::extern_spec_fn] -#[thrust_macros::requires(index < (*vec).length)] -#[thrust_macros::ensures(*result == (*vec).array[index])] +#[thrust_macros::requires(index < (*vec).len())] +#[thrust_macros::ensures(*result == (*vec)[index])] fn _extern_spec_vec_index(vec: &Vec, index: usize) -> &T where T: thrust_models::Model, T::Ty: PartialEq { as std::ops::Index>::index(vec, index) } #[thrust::extern_spec_fn] -#[thrust_macros::requires(index < (*vec).length)] +#[thrust_macros::requires(index < (*vec).len())] #[thrust_macros::ensures( - *result == (*vec).array[index] && - !result == (!vec).array[index] && - !vec == thrust_models::model::Seq { array: (*vec).array.store(index, !result), length: (*vec).length } + *result == (*vec)[index] && + !result == (!vec)[index] && + !vec == (*vec).store(index, !result) )] fn _extern_spec_vec_index_mut(vec: &mut Vec, index: usize) -> &mut T where T: thrust_models::Model, T::Ty: PartialEq @@ -788,7 +806,7 @@ fn _extern_spec_vec_index_mut(vec: &mut Vec, index: usize) -> &mut T #[thrust::extern_spec_fn] #[thrust_macros::requires(true)] -#[thrust_macros::ensures((!vec).length == 0)] +#[thrust_macros::ensures((!vec).len() == 0)] fn _extern_spec_vec_clear(vec: &mut Vec) where T: thrust_models::Model, T::Ty: PartialEq { Vec::clear(vec) } @@ -796,14 +814,14 @@ fn _extern_spec_vec_clear(vec: &mut Vec) where T: thrust_models::Model, T: #[thrust::extern_spec_fn] #[thrust_macros::requires(true)] #[thrust_macros::ensures( - (!vec).array == (*vec).array && ( + ( ( - (*vec).length > 0 && - (!vec).length == (*vec).length - 1 && - result == Some((*vec).array[(*vec).length - 1]) + (*vec).len() > 0 && + !vec == (*vec).subsequence(0, (*vec).len() - 1) && + result == Some((*vec)[(*vec).len() - 1]) ) || ( - (*vec).length == 0 && - (!vec).length == 0 && + (*vec).len() == 0 && + (!vec).len() == 0 && result == None ) ) @@ -814,7 +832,7 @@ fn _extern_spec_vec_pop(vec: &mut Vec) -> Option where T: thrust_models #[thrust::extern_spec_fn] #[thrust_macros::requires(true)] -#[thrust_macros::ensures(result == ((*vec).length == 0))] +#[thrust_macros::ensures(result == ((*vec).len() == 0))] fn _extern_spec_vec_is_empty(vec: &Vec) -> bool where T: thrust_models::Model, T::Ty: PartialEq { Vec::is_empty(vec) } @@ -823,10 +841,10 @@ fn _extern_spec_vec_is_empty(vec: &Vec) -> bool where T: thrust_models::Mo #[thrust_macros::requires(true)] #[thrust_macros::ensures( ( - (*vec).length > len && - !vec == thrust_models::model::Seq { array: (*vec).array, length: len } + (*vec).len() > len && + !vec == (*vec).subsequence(0, len) ) || ( - (*vec).length <= len && + (*vec).len() <= len && !vec == *vec ) )] @@ -863,7 +881,7 @@ fn _extern_spec_vec_as_ref(vec: &Vec) -> &[T] #[thrust::extern_spec_fn] #[thrust_macros::requires(true)] -#[thrust_macros::ensures(result == (*slice).length)] +#[thrust_macros::ensures(result == (*slice).len())] fn _extern_spec_slice_len(slice: &[T]) -> usize where T: thrust_models::Model, T::Ty: PartialEq { @@ -872,7 +890,7 @@ fn _extern_spec_slice_len(slice: &[T]) -> usize #[thrust::extern_spec_fn] #[thrust_macros::requires(true)] -#[thrust_macros::ensures(result == ((*slice).length == 0))] +#[thrust_macros::ensures(result == ((*slice).len() == 0))] fn _extern_spec_slice_is_empty(slice: &[T]) -> bool where T: thrust_models::Model, T::Ty: PartialEq { @@ -882,8 +900,8 @@ fn _extern_spec_slice_is_empty(slice: &[T]) -> bool #[thrust::extern_spec_fn] #[thrust_macros::requires(true)] #[thrust_macros::ensures( - (index < (*slice).length && result == Some(&(*slice).array[index])) - || ((*slice).length <= index && result == None) + (index < (*slice).len() && result == Some(&(*slice)[index])) + || ((*slice).len() <= index && result == None) )] fn _extern_spec_slice_get(slice: &[T], index: usize) -> Option<&T> where T: thrust_models::Model, T::Ty: PartialEq @@ -894,17 +912,14 @@ fn _extern_spec_slice_get(slice: &[T], index: usize) -> Option<&T> #[thrust::extern_spec_fn] #[thrust_macros::requires(true)] #[thrust_macros::ensures( - (index < (*slice).length + (index < (*slice).len() && result == Some(thrust_models::model::Mut::new( - (*slice).array[index], - (!slice).array[index], + (*slice)[index], + (!slice)[index], )) - && !slice == thrust_models::model::Seq { - array: (*slice).array.store(index, (!slice).array[index]), - length: (*slice).length, - } + && !slice == (*slice).store(index, (!slice)[index]) ) - || ((*slice).length <= index && result == None && !slice == *slice) + || ((*slice).len() <= index && result == None && !slice == *slice) )] fn _extern_spec_slice_get_mut(slice: &mut [T], index: usize) -> Option<&mut T> where T: thrust_models::Model, T::Ty: PartialEq @@ -915,8 +930,8 @@ fn _extern_spec_slice_get_mut(slice: &mut [T], index: usize) -> Option<&mut T #[thrust::extern_spec_fn] #[thrust_macros::requires(true)] #[thrust_macros::ensures( - ((*slice).length > 0 && result == Some(&(*slice).array[0])) - || ((*slice).length == 0 && result == None) + ((*slice).len() > 0 && result == Some(&(*slice)[0])) + || ((*slice).len() == 0 && result == None) )] fn _extern_spec_slice_first(slice: &[T]) -> Option<&T> where T: thrust_models::Model, T::Ty: PartialEq @@ -927,17 +942,14 @@ fn _extern_spec_slice_first(slice: &[T]) -> Option<&T> #[thrust::extern_spec_fn] #[thrust_macros::requires(true)] #[thrust_macros::ensures( - ((*slice).length > 0 + ((*slice).len() > 0 && result == Some(thrust_models::model::Mut::new( - (*slice).array[0], - (!slice).array[0], + (*slice)[0], + (!slice)[0], )) - && !slice == thrust_models::model::Seq { - array: (*slice).array.store(0, (!slice).array[0]), - length: (*slice).length, - } + && !slice == (*slice).store(0, (!slice)[0]) ) - || ((*slice).length == 0 && result == None && !slice == *slice) + || ((*slice).len() == 0 && result == None && !slice == *slice) )] fn _extern_spec_slice_first_mut(slice: &mut [T]) -> Option<&mut T> where T: thrust_models::Model, T::Ty: PartialEq @@ -948,8 +960,8 @@ fn _extern_spec_slice_first_mut(slice: &mut [T]) -> Option<&mut T> #[thrust::extern_spec_fn] #[thrust_macros::requires(true)] #[thrust_macros::ensures( - ((*slice).length > 0 && result == Some(&(*slice).array[(*slice).length - 1])) - || ((*slice).length == 0 && result == None) + ((*slice).len() > 0 && result == Some(&(*slice)[(*slice).len() - 1])) + || ((*slice).len() == 0 && result == None) )] fn _extern_spec_slice_last(slice: &[T]) -> Option<&T> where T: thrust_models::Model, T::Ty: PartialEq @@ -960,20 +972,17 @@ fn _extern_spec_slice_last(slice: &[T]) -> Option<&T> #[thrust::extern_spec_fn] #[thrust_macros::requires(true)] #[thrust_macros::ensures( - ((*slice).length > 0 + ((*slice).len() > 0 && result == Some(thrust_models::model::Mut::new( - (*slice).array[(*slice).length - 1], - (!slice).array[(*slice).length - 1], + (*slice)[(*slice).len() - 1], + (!slice)[(*slice).len() - 1], )) - && !slice == thrust_models::model::Seq { - array: (*slice).array.store( - (*slice).length - 1, - (!slice).array[(*slice).length - 1], - ), - length: (*slice).length, - } + && !slice == (*slice).store( + (*slice).len() - 1, + (!slice)[(*slice).len() - 1], + ) ) - || ((*slice).length == 0 && result == None && !slice == *slice) + || ((*slice).len() == 0 && result == None && !slice == *slice) )] fn _extern_spec_slice_last_mut(slice: &mut [T]) -> Option<&mut T> where T: thrust_models::Model, T::Ty: PartialEq @@ -981,12 +990,91 @@ 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).len() > 0 + && result == Some(( + &(*slice)[0], + &(*slice).subsequence(1, (*slice).len()), + )) + ) + || ((*slice).len() == 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).len() > 0 + && result == Some(( + &(*slice)[(*slice).len() - 1], + &(*slice).subsequence(0, (*slice).len() - 1), + )) + ) + || ((*slice).len() == 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).len() > 0 + && (!slice).len() == (*slice).len() + && result == Some(( + thrust_models::model::Mut::new((*slice)[0], (!slice)[0]), + thrust_models::model::Mut::new( + (*slice).subsequence(1, (*slice).len()), + (!slice).subsequence(1, (!slice).len()), + ), + )) + ) + || ((*slice).len() == 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).len() > 0 + && (!slice).len() == (*slice).len() + && result == Some(( + thrust_models::model::Mut::new( + (*slice)[(*slice).len() - 1], + (!slice)[(!slice).len() - 1], + ), + thrust_models::model::Mut::new( + (*slice).subsequence(0, (*slice).len() - 1), + (!slice).subsequence(0, (!slice).len() - 1), + ), + )) + ) + || ((*slice).len() == 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. #[thrust::extern_spec_fn] -#[thrust_macros::requires(index < (*slice).length)] -#[thrust_macros::ensures(*result == (*slice).array[index])] +#[thrust_macros::requires(index < (*slice).len())] +#[thrust_macros::ensures(*result == (*slice)[index])] fn _extern_spec_slice_index(slice: &[T], index: usize) -> &T where T: thrust_models::Model, T::Ty: PartialEq { @@ -994,14 +1082,11 @@ fn _extern_spec_slice_index(slice: &[T], index: usize) -> &T } #[thrust::extern_spec_fn] -#[thrust_macros::requires(index < (*slice).length)] +#[thrust_macros::requires(index < (*slice).len())] #[thrust_macros::ensures( - *result == (*slice).array[index] && - !result == (!slice).array[index] && - !slice == thrust_models::model::Seq { - array: (*slice).array.store(index, !result), - length: (*slice).length, - } + *result == (*slice)[index] && + !result == (!slice)[index] && + !slice == (*slice).store(index, !result) )] fn _extern_spec_slice_index_mut(slice: &mut [T], index: usize) -> &mut T where T: thrust_models::Model, T::Ty: PartialEq diff --git a/tests/ui/fail/loop_invariant_fn_param_at_entry.rs b/tests/ui/fail/loop_invariant_fn_param_at_entry.rs index fd9f2164..b4447709 100644 --- a/tests/ui/fail/loop_invariant_fn_param_at_entry.rs +++ b/tests/ui/fail/loop_invariant_fn_param_at_entry.rs @@ -2,7 +2,7 @@ //@compile-flags: -C debug-assertions=off #[thrust_macros::requires(true)] -#[thrust_macros::ensures(result.length == v.length + 2)] +#[thrust_macros::ensures(result.len() == v.len() + 2)] #[thrust_macros::context] fn push_two(v: Vec) -> Vec { let mut w = v; @@ -10,7 +10,7 @@ fn push_two(v: Vec) -> Vec { while i < 2 { thrust_macros::invariant!( |i: i64, w: Vec, v: thrust_models::FnParam>| - w.length == v.at_entry().length + i && i <= 2 + w.len() == v.at_entry().len() + i && i <= 2 ); w.push(i); w.push(i); 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_specs_vec_build.rs b/tests/ui/fail/seq_specs_vec_build.rs index 097e9b02..22c229fc 100644 --- a/tests/ui/fail/seq_specs_vec_build.rs +++ b/tests/ui/fail/seq_specs_vec_build.rs @@ -6,11 +6,11 @@ use thrust_models::model::Seq; #[thrust_macros::requires(true)] #[thrust_macros::ensures( - result.length == Seq::empty().push(10).push(20).push(30).len() - && result.array[0] == Seq::empty().push(10).push(20).push(30)[0] - && result.array[1] == Seq::empty().push(10).push(20).push(30)[1] + result.len() == Seq::empty().push(10).push(20).push(30).len() + && result[0] == Seq::empty().push(10).push(20).push(30)[0] + && result[1] == Seq::empty().push(10).push(20).push(30)[1] // wrong: last element should be 30, not 99 - && result.array[2] == Seq::empty().push(10).push(20).push(99)[2] + && result[2] == Seq::empty().push(10).push(20).push(99)[2] )] fn build_three() -> Vec { let mut v = Vec::new(); 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_first_mut.rs b/tests/ui/fail/slice_first_mut.rs index 7800f2c8..7a66826d 100644 --- a/tests/ui/fail/slice_first_mut.rs +++ b/tests/ui/fail/slice_first_mut.rs @@ -4,7 +4,7 @@ #[thrust::trusted] #[thrust_macros::requires(true)] #[thrust_macros::ensures( - (*result).length > 0 && (*result).array[0] == 10 + (*result).len() > 0 && (*result)[0] == 10 )] fn slice() -> &'static mut [i32] { unimplemented!() diff --git a/tests/ui/fail/slice_index.rs b/tests/ui/fail/slice_index.rs index c5c937d3..98167bde 100644 --- a/tests/ui/fail/slice_index.rs +++ b/tests/ui/fail/slice_index.rs @@ -3,7 +3,7 @@ #[thrust::trusted] #[thrust_macros::requires(true)] -#[thrust_macros::ensures((*result).length == 1 && (*result).array[0] == 10)] +#[thrust_macros::ensures((*result).len() == 1 && (*result)[0] == 10)] fn slice() -> &'static [i32] { unimplemented!() } diff --git a/tests/ui/fail/slice_index_mut.rs b/tests/ui/fail/slice_index_mut.rs index 95dc7064..cdfaa838 100644 --- a/tests/ui/fail/slice_index_mut.rs +++ b/tests/ui/fail/slice_index_mut.rs @@ -4,7 +4,7 @@ #[thrust::trusted] #[thrust_macros::requires(true)] #[thrust_macros::ensures( - (*result).length > 1 && (*result).array[1] == 20 + (*result).len() > 1 && (*result)[1] == 20 )] fn slice() -> &'static mut [i32] { unimplemented!() diff --git a/tests/ui/fail/slice_last_mut.rs b/tests/ui/fail/slice_last_mut.rs index 10bcedfb..62fca762 100644 --- a/tests/ui/fail/slice_last_mut.rs +++ b/tests/ui/fail/slice_last_mut.rs @@ -4,8 +4,8 @@ #[thrust::trusted] #[thrust_macros::requires(true)] #[thrust_macros::ensures( - (*result).length > 0 - && (*result).array[(*result).length - 1] == 30 + (*result).len() > 0 + && (*result)[(*result).len() - 1] == 30 )] fn slice() -> &'static mut [i32] { unimplemented!() diff --git a/tests/ui/fail/slice_methods.rs b/tests/ui/fail/slice_methods.rs index fb57d55e..87283698 100644 --- a/tests/ui/fail/slice_methods.rs +++ b/tests/ui/fail/slice_methods.rs @@ -4,9 +4,9 @@ #[thrust::trusted] #[thrust_macros::requires(true)] #[thrust_macros::ensures( - (*result).length == 2 - && (*result).array[0] == 10 - && (*result).array[1] == 20 + (*result).len() == 2 + && (*result)[0] == 10 + && (*result)[1] == 20 )] fn slice() -> &'static [i32] { unimplemented!() diff --git a/tests/ui/fail/slice_methods_mut.rs b/tests/ui/fail/slice_methods_mut.rs index a01f3ecb..3fd60c95 100644 --- a/tests/ui/fail/slice_methods_mut.rs +++ b/tests/ui/fail/slice_methods_mut.rs @@ -4,7 +4,7 @@ #[thrust::trusted] #[thrust_macros::requires(true)] #[thrust_macros::ensures( - (*result).length > 1 && (*result).array[1] == 20 + (*result).len() > 1 && (*result)[1] == 20 )] fn slice() -> &'static mut [i32] { unimplemented!() diff --git a/tests/ui/fail/slice_split_first.rs b/tests/ui/fail/slice_split_first.rs new file mode 100644 index 00000000..20f9b410 --- /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).len() == 2 + && (*result)[0] == 10 + && (*result)[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_loop.rs b/tests/ui/fail/slice_split_first_loop.rs new file mode 100644 index 00000000..e17acdef --- /dev/null +++ b/tests/ui/fail/slice_split_first_loop.rs @@ -0,0 +1,20 @@ +//@error-in-other-file: Unsat +//@compile-flags: -C debug-assertions=off +//@rustc-env: THRUST_SOLVER=tests/thrust-pcsat-wrapper + +#[thrust::callable] +fn check(slice: &[i32]) { + let mut s = slice; + let mut i = 0; + while i < slice.len() { + if let Some((first, rest)) = s.split_first() { + assert!(*first != slice[i]); + s = rest; + i += 1; + } else { + break; + } + } +} + +fn main() {} diff --git a/tests/ui/fail/slice_split_first_loop_invariant.rs b/tests/ui/fail/slice_split_first_loop_invariant.rs new file mode 100644 index 00000000..ff13f0eb --- /dev/null +++ b/tests/ui/fail/slice_split_first_loop_invariant.rs @@ -0,0 +1,23 @@ +//@error-in-other-file: Unsat +//@compile-flags: -C debug-assertions=off +//@rustc-env: THRUST_SOLVER=tests/thrust-pcsat-wrapper + +#[thrust::callable] +fn check(slice: &[i32]) { + let mut s = slice; + let mut i = 0; + while i < slice.len() { + thrust_macros::invariant!(|slice: &[i32], s: &[i32], i: usize| 0 <= i + && i <= (*slice).len() + && *s == (*slice).subsequence(i, (*slice).len())); + if let Some((first, rest)) = s.split_first() { + assert!(*first != slice[i]); + s = rest; + i += 1; + } else { + break; + } + } +} + +fn main() {} 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..ca18fdb2 --- /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).len() == 2 + && (*result)[0] == 10 + && (*result)[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_loop.rs b/tests/ui/fail/slice_split_first_mut_loop.rs new file mode 100644 index 00000000..4a068d38 --- /dev/null +++ b/tests/ui/fail/slice_split_first_mut_loop.rs @@ -0,0 +1,27 @@ +//@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).len() == 2 + && (*result)[0] == 10 + && (*result)[1] == 20 +)] +fn slice() -> &'static mut [i32] { + unimplemented!() +} + +#[thrust::callable] +fn check() { + let sl = slice(); + let mut s = &mut *sl; + while let Some((first, rest)) = s.split_first_mut() { + *first = 0; + s = rest; + } + assert!(sl[0] != 0); +} + +fn main() {} diff --git a/tests/ui/fail/slice_split_first_mut_loop_invariant.rs b/tests/ui/fail/slice_split_first_mut_loop_invariant.rs new file mode 100644 index 00000000..82485012 --- /dev/null +++ b/tests/ui/fail/slice_split_first_mut_loop_invariant.rs @@ -0,0 +1,35 @@ +//@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).len() == 2 + && (*result)[0] == 10 + && (*result)[1] == 20 +)] +fn slice() -> &'static mut [i32] { + unimplemented!() +} + +#[thrust::callable] +fn check() { + let sl = slice(); + let mut s = &mut *sl; + while let Some((first, rest)) = s.split_first_mut() { + thrust_macros::invariant!(|sl: &mut [i32], s: &mut [i32]| + ( + (!s).len() == (*s).len() + && ((!s).len() == 0 || (!s)[0] == 0) + ) ==> ( + (*sl).len() == 2 && (*sl)[0] == 0 + ) + ); + *first = 0; + s = rest; + } + assert!(sl[0] != 0); +} + +fn main() {} 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..c8a470d2 --- /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).len() == 2 + && (*result)[0] == 10 + && (*result)[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/loop_invariant_fn_param_at_entry.rs b/tests/ui/pass/loop_invariant_fn_param_at_entry.rs index e8418369..db6de3a5 100644 --- a/tests/ui/pass/loop_invariant_fn_param_at_entry.rs +++ b/tests/ui/pass/loop_invariant_fn_param_at_entry.rs @@ -2,7 +2,7 @@ //@compile-flags: -C debug-assertions=off #[thrust_macros::requires(true)] -#[thrust_macros::ensures(result.length == v.length + 2)] +#[thrust_macros::ensures(result.len() == v.len() + 2)] #[thrust_macros::context] fn push_two(v: Vec) -> Vec { let mut w = v; @@ -10,7 +10,7 @@ fn push_two(v: Vec) -> Vec { while i < 2 { thrust_macros::invariant!( |i: i64, w: Vec, v: thrust_models::FnParam>| - w.length == v.at_entry().length + i && i <= 2 + w.len() == v.at_entry().len() + i && i <= 2 ); w.push(i); i += 1; 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_specs_vec_build.rs b/tests/ui/pass/seq_specs_vec_build.rs index 70f1d667..494ec6a8 100644 --- a/tests/ui/pass/seq_specs_vec_build.rs +++ b/tests/ui/pass/seq_specs_vec_build.rs @@ -6,10 +6,10 @@ use thrust_models::model::Seq; #[thrust_macros::requires(true)] #[thrust_macros::ensures( - result.length == Seq::empty().push(10).push(20).push(30).len() - && result.array[0] == Seq::empty().push(10).push(20).push(30)[0] - && result.array[1] == Seq::empty().push(10).push(20).push(30)[1] - && result.array[2] == Seq::empty().push(10).push(20).push(30)[2] + result.len() == Seq::empty().push(10).push(20).push(30).len() + && result[0] == Seq::empty().push(10).push(20).push(30)[0] + && result[1] == Seq::empty().push(10).push(20).push(30)[1] + && result[2] == Seq::empty().push(10).push(20).push(30)[2] )] fn build_three() -> Vec { let mut v = Vec::new(); 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_first_mut.rs b/tests/ui/pass/slice_first_mut.rs index 24ea5d93..1d592a5d 100644 --- a/tests/ui/pass/slice_first_mut.rs +++ b/tests/ui/pass/slice_first_mut.rs @@ -4,7 +4,7 @@ #[thrust::trusted] #[thrust_macros::requires(true)] #[thrust_macros::ensures( - (*result).length > 0 && (*result).array[0] == 10 + (*result).len() > 0 && (*result)[0] == 10 )] fn slice() -> &'static mut [i32] { unimplemented!() diff --git a/tests/ui/pass/slice_index.rs b/tests/ui/pass/slice_index.rs index 1e044954..1519a7dc 100644 --- a/tests/ui/pass/slice_index.rs +++ b/tests/ui/pass/slice_index.rs @@ -4,9 +4,9 @@ #[thrust::trusted] #[thrust_macros::requires(true)] #[thrust_macros::ensures( - (*result).length == 2 - && (*result).array[0] == 10 - && (*result).array[1] == 20 + (*result).len() == 2 + && (*result)[0] == 10 + && (*result)[1] == 20 )] fn slice() -> &'static [i32] { unimplemented!() diff --git a/tests/ui/pass/slice_index_mut.rs b/tests/ui/pass/slice_index_mut.rs index c84f1a5e..22f95ce3 100644 --- a/tests/ui/pass/slice_index_mut.rs +++ b/tests/ui/pass/slice_index_mut.rs @@ -4,7 +4,7 @@ #[thrust::trusted] #[thrust_macros::requires(true)] #[thrust_macros::ensures( - (*result).length > 1 && (*result).array[1] == 20 + (*result).len() > 1 && (*result)[1] == 20 )] fn slice() -> &'static mut [i32] { unimplemented!() diff --git a/tests/ui/pass/slice_last_mut.rs b/tests/ui/pass/slice_last_mut.rs index 92f94287..cc8d0e8e 100644 --- a/tests/ui/pass/slice_last_mut.rs +++ b/tests/ui/pass/slice_last_mut.rs @@ -4,8 +4,8 @@ #[thrust::trusted] #[thrust_macros::requires(true)] #[thrust_macros::ensures( - (*result).length > 0 - && (*result).array[(*result).length - 1] == 30 + (*result).len() > 0 + && (*result)[(*result).len() - 1] == 30 )] fn slice() -> &'static mut [i32] { unimplemented!() diff --git a/tests/ui/pass/slice_methods.rs b/tests/ui/pass/slice_methods.rs index 70671165..a0565820 100644 --- a/tests/ui/pass/slice_methods.rs +++ b/tests/ui/pass/slice_methods.rs @@ -4,11 +4,11 @@ #[thrust::trusted] #[thrust_macros::requires(true)] #[thrust_macros::ensures( - (*result).length == 4 - && (*result).array[0] == 10 - && (*result).array[1] == 20 - && (*result).array[2] == 30 - && (*result).array[3] == 40 + (*result).len() == 4 + && (*result)[0] == 10 + && (*result)[1] == 20 + && (*result)[2] == 30 + && (*result)[3] == 40 )] fn slice() -> &'static [i32] { unimplemented!() diff --git a/tests/ui/pass/slice_methods_mut.rs b/tests/ui/pass/slice_methods_mut.rs index b7ef7bed..9d61f5bc 100644 --- a/tests/ui/pass/slice_methods_mut.rs +++ b/tests/ui/pass/slice_methods_mut.rs @@ -4,7 +4,7 @@ #[thrust::trusted] #[thrust_macros::requires(true)] #[thrust_macros::ensures( - (*result).length > 1 && (*result).array[1] == 20 + (*result).len() > 1 && (*result)[1] == 20 )] fn slice() -> &'static mut [i32] { unimplemented!() diff --git a/tests/ui/pass/slice_split_first.rs b/tests/ui/pass/slice_split_first.rs new file mode 100644 index 00000000..744f25f0 --- /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).len() == 2 + && (*result)[0] == 10 + && (*result)[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_loop.rs b/tests/ui/pass/slice_split_first_loop.rs new file mode 100644 index 00000000..21666500 --- /dev/null +++ b/tests/ui/pass/slice_split_first_loop.rs @@ -0,0 +1,20 @@ +//@check-pass +//@compile-flags: -C debug-assertions=off +//@rustc-env: THRUST_SOLVER=tests/thrust-pcsat-wrapper + +#[thrust::callable] +fn check(slice: &[i32]) { + let mut s = slice; + let mut i = 0; + while i < slice.len() { + if let Some((first, rest)) = s.split_first() { + assert!(*first == slice[i]); + s = rest; + i += 1; + } else { + break; + } + } +} + +fn main() {} diff --git a/tests/ui/pass/slice_split_first_loop_invariant.rs b/tests/ui/pass/slice_split_first_loop_invariant.rs new file mode 100644 index 00000000..045b28da --- /dev/null +++ b/tests/ui/pass/slice_split_first_loop_invariant.rs @@ -0,0 +1,23 @@ +//@check-pass +//@compile-flags: -C debug-assertions=off +//@rustc-env: THRUST_SOLVER=tests/thrust-pcsat-wrapper + +#[thrust::callable] +fn check(slice: &[i32]) { + let mut s = slice; + let mut i = 0; + while i < slice.len() { + thrust_macros::invariant!(|slice: &[i32], s: &[i32], i: usize| 0 <= i + && i <= (*slice).len() + && *s == (*slice).subsequence(i, (*slice).len())); + if let Some((first, rest)) = s.split_first() { + assert!(*first == slice[i]); + s = rest; + i += 1; + } else { + break; + } + } +} + +fn main() {} 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..694221a8 --- /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).len() == 2 + && (*result)[0] == 10 + && (*result)[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_loop.rs b/tests/ui/pass/slice_split_first_mut_loop.rs new file mode 100644 index 00000000..ba47b2fe --- /dev/null +++ b/tests/ui/pass/slice_split_first_mut_loop.rs @@ -0,0 +1,27 @@ +//@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).len() == 2 + && (*result)[0] == 10 + && (*result)[1] == 20 +)] +fn slice() -> &'static mut [i32] { + unimplemented!() +} + +#[thrust::callable] +fn check() { + let sl = slice(); + let mut s = &mut *sl; + while let Some((first, rest)) = s.split_first_mut() { + *first = 0; + s = rest; + } + assert!(sl[0] == 0); +} + +fn main() {} diff --git a/tests/ui/pass/slice_split_first_mut_loop_invariant.rs b/tests/ui/pass/slice_split_first_mut_loop_invariant.rs new file mode 100644 index 00000000..7eef0660 --- /dev/null +++ b/tests/ui/pass/slice_split_first_mut_loop_invariant.rs @@ -0,0 +1,35 @@ +//@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).len() == 2 + && (*result)[0] == 10 + && (*result)[1] == 20 +)] +fn slice() -> &'static mut [i32] { + unimplemented!() +} + +#[thrust::callable] +fn check() { + let sl = slice(); + let mut s = &mut *sl; + while let Some((first, rest)) = s.split_first_mut() { + thrust_macros::invariant!(|sl: &mut [i32], s: &mut [i32]| + ( + (!s).len() == (*s).len() + && ((!s).len() == 0 || (!s)[0] == 0) + ) ==> ( + (*sl).len() == 2 && (*sl)[0] == 0 + ) + ); + *first = 0; + s = rest; + } + assert!(sl[0] == 0); +} + +fn main() {} 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..30068333 --- /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).len() == 2 + && (*result)[0] == 10 + && (*result)[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); +} From b5fe42e7648e03b6e174f88d88256b6855cecb72 Mon Sep 17 00:00:00 2001 From: coord_e Date: Wed, 16 Sep 2026 13:46:48 +0900 Subject: [PATCH 2/5] Emit sequence updates through a shared seq.store definition --- src/chc.rs | 16 ++++++---------- std.rs | 3 +++ 2 files changed, 9 insertions(+), 10 deletions(-) diff --git a/src/chc.rs b/src/chc.rs index 110916db..75a943a0 100644 --- a/src/chc.rs +++ b/src/chc.rs @@ -415,7 +415,9 @@ impl Function { Self::OR => Sort::bool(), Self::NOT => Sort::bool(), Self::NEG => Sort::int(), - Self::STORE | Self::SEQ_CONCAT | Self::SEQ_EXTRACT => args.into_iter().next().unwrap(), + Self::STORE | Self::SEQ_CONCAT | Self::SEQ_EXTRACT | Self::SEQ_STORE => { + args.into_iter().next().unwrap() + } Self::SEQ_LEN => Sort::int(), Self::SEQ_UNIT => Sort::seq(args.into_iter().next().unwrap()), Self::SEQ_NTH => { @@ -454,6 +456,7 @@ impl Function { pub const SEQ_LEN: Function = Function::new("seq.len"); pub const SEQ_UNIT: Function = Function::new("seq.unit"); pub const SEQ_NTH: Function = Function::new("seq.nth"); + pub const SEQ_STORE: Function = Function::new("seq.store"); pub const ITE: Function = Function::new("ite"); } @@ -758,15 +761,8 @@ impl Term { Term::App(Function::SEQ_NTH, vec![self, index]) } - pub fn seq_store(self, index: Self, elem: Self) -> Self - where - V: Clone, - { - let prefix = self.clone().seq_extract(Self::int(0), index.clone()); - let suffix_start = index.add(Self::int(1)); - let suffix_length = self.clone().seq_len().sub(suffix_start.clone()); - let suffix = self.seq_extract(suffix_start, suffix_length); - prefix.seq_concat(elem.seq_unit()).seq_concat(suffix) + pub fn seq_store(self, index: Self, elem: Self) -> Self { + Term::App(Function::SEQ_STORE, vec![self, index, elem]) } pub fn boxed(self) -> Self { diff --git a/std.rs b/std.rs index e2880d91..36730f95 100644 --- a/std.rs +++ b/std.rs @@ -235,6 +235,9 @@ mod thrust_models { unimplemented!() } + /// Returns `self` with the element at `index` replaced by `value`. + /// + /// The result is unspecified when `index` is out of range. #[allow(dead_code)] #[thrust::def::seq_store] #[thrust::ignored] From e0960cf08d3e5c1af7f3a76e341bee7b8bdca5fd Mon Sep 17 00:00:00 2001 From: coord_e Date: Thu, 17 Sep 2026 20:10:05 +0900 Subject: [PATCH 3/5] Use latest PCSat in CI --- .github/workflows/ci.yml | 25 +++++++++++++++++++++---- 1 file changed, 21 insertions(+), 4 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index b7299f32..781b3513 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -28,13 +28,30 @@ jobs: permissions: contents: read timeout-minutes: 10 - env: - # see tests/thrust-pcsat-wrapper - COAR_IMAGE: ghcr.io/hiroshi-unno/coar@sha256:73144ed27a02b163d1a71b41b58f3b5414f12e91326015600cfdca64ff19f011 steps: - uses: actions/checkout@v7 - uses: ./.github/actions/setup-z3 - - run: docker pull "$COAR_IMAGE" + - name: Install PCSat dependencies + run: | + sudo apt-get update + sudo apt-get install \ + libblas3 \ + libgcc-s1 \ + libgmp10 \ + liblapack3 \ + libmpfr6 \ + libstdc++6 \ + zlib1g + - name: Download latest PCSat + run: | + cd $(mktemp -d) + curl -fsS "$PCSAT_URL" -o thrust-pcsat-wrapper.tar.gz + echo "$PCSAT_SHA256 thrust-pcsat-wrapper.tar.gz" | sha256sum -c --strict + tar --strip-components=1 -xf thrust-pcsat-wrapper.tar.gz + mv thrust-pcsat-wrapper "$GITHUB_WORKSPACE/tests/thrust-pcsat-wrapper" + env: + PCSAT_URL: https://thrust-ci-public.s3.ap-northeast-1.amazonaws.com/pcsat/thrust-pcsat-wrapper-873d558c6a.tar.gz + PCSAT_SHA256: cae6829b40cfde196ae231f4a97eed5b873756cb59619f580934b488c1e7a11a - run: rustup show - uses: Swatinem/rust-cache@v2 - run: cargo test From 7ec0b721f49ed955e215868acd6c254e1dcc4ee5 Mon Sep 17 00:00:00 2001 From: coord_e Date: Thu, 17 Sep 2026 20:12:45 +0900 Subject: [PATCH 4/5] Require PCSat in all seq test cases --- tests/ui/fail/array_literal_1.rs | 1 + tests/ui/fail/array_literal_2.rs | 1 + tests/ui/fail/array_literal_3.rs | 1 + tests/ui/fail/ghost_const.rs | 1 + tests/ui/fail/ghost_field.rs | 1 + tests/ui/fail/ghost_local.rs | 1 + tests/ui/fail/ghost_self.rs | 1 + tests/ui/fail/loop_invariant_fn_param_at_entry.rs | 1 + tests/ui/fail/seq_basic.rs | 1 + tests/ui/fail/seq_concat.rs | 1 + tests/ui/fail/slice_first_mut.rs | 1 + tests/ui/fail/slice_index.rs | 1 + tests/ui/fail/slice_index_mut.rs | 1 + tests/ui/fail/slice_last_mut.rs | 1 + tests/ui/fail/slice_len_guard_mut.rs | 1 + tests/ui/fail/slice_methods.rs | 1 + tests/ui/fail/slice_methods_mut.rs | 1 + tests/ui/fail/vec_1.rs | 1 + tests/ui/fail/vec_2.rs | 1 + tests/ui/fail/vec_3.rs | 1 + tests/ui/fail/vec_deref.rs | 1 + tests/ui/pass/array_literal_1.rs | 1 + tests/ui/pass/array_literal_2.rs | 1 + tests/ui/pass/array_literal_3.rs | 1 + tests/ui/pass/ghost_const.rs | 1 + tests/ui/pass/ghost_field.rs | 1 + tests/ui/pass/ghost_local.rs | 1 + tests/ui/pass/ghost_self.rs | 1 + tests/ui/pass/loop_invariant_fn_param_at_entry.rs | 1 + tests/ui/pass/seq_basic.rs | 1 + tests/ui/pass/seq_concat.rs | 1 + tests/ui/pass/slice_first_mut.rs | 1 + tests/ui/pass/slice_index.rs | 1 + tests/ui/pass/slice_index_mut.rs | 1 + tests/ui/pass/slice_last_mut.rs | 1 + tests/ui/pass/slice_len_guard_mut.rs | 1 + tests/ui/pass/slice_methods.rs | 1 + tests/ui/pass/slice_methods_mut.rs | 1 + tests/ui/pass/vec_1.rs | 1 + tests/ui/pass/vec_2.rs | 1 + tests/ui/pass/vec_3.rs | 1 + tests/ui/pass/vec_deref.rs | 1 + 42 files changed, 42 insertions(+) diff --git a/tests/ui/fail/array_literal_1.rs b/tests/ui/fail/array_literal_1.rs index 1fa49d74..c0a2a902 100644 --- a/tests/ui/fail/array_literal_1.rs +++ b/tests/ui/fail/array_literal_1.rs @@ -1,5 +1,6 @@ //@error-in-other-file: Unsat //@compile-flags: -C debug-assertions=off +//@rustc-env: THRUST_SOLVER=tests/thrust-pcsat-wrapper fn main() { let arr = [1i32, 2, 3]; diff --git a/tests/ui/fail/array_literal_2.rs b/tests/ui/fail/array_literal_2.rs index 99ccdb15..69726e9d 100644 --- a/tests/ui/fail/array_literal_2.rs +++ b/tests/ui/fail/array_literal_2.rs @@ -1,5 +1,6 @@ //@error-in-other-file: Unsat //@compile-flags: -C debug-assertions=off +//@rustc-env: THRUST_SOLVER=tests/thrust-pcsat-wrapper fn main() { let arr = [0i32, 0, 0, 0]; diff --git a/tests/ui/fail/array_literal_3.rs b/tests/ui/fail/array_literal_3.rs index dc085982..0954cb5f 100644 --- a/tests/ui/fail/array_literal_3.rs +++ b/tests/ui/fail/array_literal_3.rs @@ -1,5 +1,6 @@ //@error-in-other-file: Unsat //@compile-flags: -C debug-assertions=off +//@rustc-env: THRUST_SOLVER=tests/thrust-pcsat-wrapper fn main() { let mut arr = [1i32, 2, 3]; diff --git a/tests/ui/fail/ghost_const.rs b/tests/ui/fail/ghost_const.rs index 2cc9cf57..ef60e40a 100644 --- a/tests/ui/fail/ghost_const.rs +++ b/tests/ui/fail/ghost_const.rs @@ -1,5 +1,6 @@ //@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}; use thrust_models::Ghost; diff --git a/tests/ui/fail/ghost_field.rs b/tests/ui/fail/ghost_field.rs index 70aafb7e..8f1bbd4a 100644 --- a/tests/ui/fail/ghost_field.rs +++ b/tests/ui/fail/ghost_field.rs @@ -1,5 +1,6 @@ //@error-in-other-file: Unsat //@compile-flags: -C debug-assertions=off -A unused-variables +//@rustc-env: THRUST_SOLVER=tests/thrust-pcsat-wrapper use thrust_models::model::{Int, Seq}; use thrust_models::Ghost; diff --git a/tests/ui/fail/ghost_local.rs b/tests/ui/fail/ghost_local.rs index 010e8356..55dca094 100644 --- a/tests/ui/fail/ghost_local.rs +++ b/tests/ui/fail/ghost_local.rs @@ -1,5 +1,6 @@ //@error-in-other-file: Unsat //@compile-flags: -C debug-assertions=off -A unused-variables +//@rustc-env: THRUST_SOLVER=tests/thrust-pcsat-wrapper use thrust_models::model::{Int, Seq}; use thrust_models::Ghost; diff --git a/tests/ui/fail/ghost_self.rs b/tests/ui/fail/ghost_self.rs index d0ab9794..a7dfc0ad 100644 --- a/tests/ui/fail/ghost_self.rs +++ b/tests/ui/fail/ghost_self.rs @@ -1,5 +1,6 @@ //@error-in-other-file: Unsat //@compile-flags: -C debug-assertions=off -A unused-variables +//@rustc-env: THRUST_SOLVER=tests/thrust-pcsat-wrapper use thrust_models::model::{Int, Seq}; use thrust_models::Ghost; diff --git a/tests/ui/fail/loop_invariant_fn_param_at_entry.rs b/tests/ui/fail/loop_invariant_fn_param_at_entry.rs index b4447709..e1f6886d 100644 --- a/tests/ui/fail/loop_invariant_fn_param_at_entry.rs +++ b/tests/ui/fail/loop_invariant_fn_param_at_entry.rs @@ -1,5 +1,6 @@ //@error-in-other-file: Unsat //@compile-flags: -C debug-assertions=off +//@rustc-env: THRUST_SOLVER=tests/thrust-pcsat-wrapper #[thrust_macros::requires(true)] #[thrust_macros::ensures(result.len() == v.len() + 2)] diff --git a/tests/ui/fail/seq_basic.rs b/tests/ui/fail/seq_basic.rs index ff340d90..5501dd98 100644 --- a/tests/ui/fail/seq_basic.rs +++ b/tests/ui/fail/seq_basic.rs @@ -1,5 +1,6 @@ //@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}; diff --git a/tests/ui/fail/seq_concat.rs b/tests/ui/fail/seq_concat.rs index bba0a6cd..ef606c8f 100644 --- a/tests/ui/fail/seq_concat.rs +++ b/tests/ui/fail/seq_concat.rs @@ -1,5 +1,6 @@ //@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}; diff --git a/tests/ui/fail/slice_first_mut.rs b/tests/ui/fail/slice_first_mut.rs index 7a66826d..20dcb87a 100644 --- a/tests/ui/fail/slice_first_mut.rs +++ b/tests/ui/fail/slice_first_mut.rs @@ -1,5 +1,6 @@ //@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)] diff --git a/tests/ui/fail/slice_index.rs b/tests/ui/fail/slice_index.rs index 98167bde..d4c440ab 100644 --- a/tests/ui/fail/slice_index.rs +++ b/tests/ui/fail/slice_index.rs @@ -1,5 +1,6 @@ //@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)] diff --git a/tests/ui/fail/slice_index_mut.rs b/tests/ui/fail/slice_index_mut.rs index cdfaa838..0fa20620 100644 --- a/tests/ui/fail/slice_index_mut.rs +++ b/tests/ui/fail/slice_index_mut.rs @@ -1,5 +1,6 @@ //@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)] diff --git a/tests/ui/fail/slice_last_mut.rs b/tests/ui/fail/slice_last_mut.rs index 62fca762..e8eabd56 100644 --- a/tests/ui/fail/slice_last_mut.rs +++ b/tests/ui/fail/slice_last_mut.rs @@ -1,5 +1,6 @@ //@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)] diff --git a/tests/ui/fail/slice_len_guard_mut.rs b/tests/ui/fail/slice_len_guard_mut.rs index de2c5074..d48f400d 100644 --- a/tests/ui/fail/slice_len_guard_mut.rs +++ b/tests/ui/fail/slice_len_guard_mut.rs @@ -1,5 +1,6 @@ //@error-in-other-file: Unsat //@compile-flags: -C debug-assertions=off -C opt-level=2 +//@rustc-env: THRUST_SOLVER=tests/thrust-pcsat-wrapper #[thrust::callable] fn check(v: &mut [i32], i: usize) { diff --git a/tests/ui/fail/slice_methods.rs b/tests/ui/fail/slice_methods.rs index 87283698..3e6ad3c2 100644 --- a/tests/ui/fail/slice_methods.rs +++ b/tests/ui/fail/slice_methods.rs @@ -1,5 +1,6 @@ //@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)] diff --git a/tests/ui/fail/slice_methods_mut.rs b/tests/ui/fail/slice_methods_mut.rs index 3fd60c95..613a7da1 100644 --- a/tests/ui/fail/slice_methods_mut.rs +++ b/tests/ui/fail/slice_methods_mut.rs @@ -1,5 +1,6 @@ //@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)] diff --git a/tests/ui/fail/vec_1.rs b/tests/ui/fail/vec_1.rs index 43f772bc..394c3ccd 100644 --- a/tests/ui/fail/vec_1.rs +++ b/tests/ui/fail/vec_1.rs @@ -1,5 +1,6 @@ //@error-in-other-file: Unsat //@compile-flags: -C debug-assertions=off +//@rustc-env: THRUST_SOLVER=tests/thrust-pcsat-wrapper fn main() { let mut v = Vec::new(); diff --git a/tests/ui/fail/vec_2.rs b/tests/ui/fail/vec_2.rs index 420adb77..b2df962a 100644 --- a/tests/ui/fail/vec_2.rs +++ b/tests/ui/fail/vec_2.rs @@ -1,5 +1,6 @@ //@error-in-other-file: Unsat //@compile-flags: -C debug-assertions=off +//@rustc-env: THRUST_SOLVER=tests/thrust-pcsat-wrapper fn main() { let mut v = Vec::new(); diff --git a/tests/ui/fail/vec_3.rs b/tests/ui/fail/vec_3.rs index 811ce700..ccb6e065 100644 --- a/tests/ui/fail/vec_3.rs +++ b/tests/ui/fail/vec_3.rs @@ -1,5 +1,6 @@ //@error-in-other-file: Unsat //@compile-flags: -C debug-assertions=off +//@rustc-env: THRUST_SOLVER=tests/thrust-pcsat-wrapper fn main() { let mut v = Vec::new(); diff --git a/tests/ui/fail/vec_deref.rs b/tests/ui/fail/vec_deref.rs index 57852710..761046d7 100644 --- a/tests/ui/fail/vec_deref.rs +++ b/tests/ui/fail/vec_deref.rs @@ -1,5 +1,6 @@ //@error-in-other-file: Unsat //@compile-flags: -C debug-assertions=off +//@rustc-env: THRUST_SOLVER=tests/thrust-pcsat-wrapper fn main() { let mut v: Vec = Vec::new(); diff --git a/tests/ui/pass/array_literal_1.rs b/tests/ui/pass/array_literal_1.rs index 4a563891..710dd5d6 100644 --- a/tests/ui/pass/array_literal_1.rs +++ b/tests/ui/pass/array_literal_1.rs @@ -1,5 +1,6 @@ //@check-pass //@compile-flags: -C debug-assertions=off +//@rustc-env: THRUST_SOLVER=tests/thrust-pcsat-wrapper fn main() { let arr = [1i32, 2, 3]; diff --git a/tests/ui/pass/array_literal_2.rs b/tests/ui/pass/array_literal_2.rs index abbc05e6..8be04c05 100644 --- a/tests/ui/pass/array_literal_2.rs +++ b/tests/ui/pass/array_literal_2.rs @@ -1,5 +1,6 @@ //@check-pass //@compile-flags: -C debug-assertions=off +//@rustc-env: THRUST_SOLVER=tests/thrust-pcsat-wrapper fn main() { let arr = [0i32, 0, 0, 0]; diff --git a/tests/ui/pass/array_literal_3.rs b/tests/ui/pass/array_literal_3.rs index 10f29014..34a4b179 100644 --- a/tests/ui/pass/array_literal_3.rs +++ b/tests/ui/pass/array_literal_3.rs @@ -1,5 +1,6 @@ //@check-pass //@compile-flags: -C debug-assertions=off +//@rustc-env: THRUST_SOLVER=tests/thrust-pcsat-wrapper fn main() { let mut arr = [1i32, 2, 3]; diff --git a/tests/ui/pass/ghost_const.rs b/tests/ui/pass/ghost_const.rs index 6e2158ef..99c0f800 100644 --- a/tests/ui/pass/ghost_const.rs +++ b/tests/ui/pass/ghost_const.rs @@ -1,5 +1,6 @@ //@check-pass //@compile-flags: -C debug-assertions=off +//@rustc-env: THRUST_SOLVER=tests/thrust-pcsat-wrapper use thrust_models::model::{Int, Seq}; use thrust_models::Ghost; diff --git a/tests/ui/pass/ghost_field.rs b/tests/ui/pass/ghost_field.rs index 1edee942..f6a978d4 100644 --- a/tests/ui/pass/ghost_field.rs +++ b/tests/ui/pass/ghost_field.rs @@ -1,5 +1,6 @@ //@check-pass //@compile-flags: -C debug-assertions=off -A unused-variables +//@rustc-env: THRUST_SOLVER=tests/thrust-pcsat-wrapper use thrust_models::model::{Int, Seq}; use thrust_models::Ghost; diff --git a/tests/ui/pass/ghost_local.rs b/tests/ui/pass/ghost_local.rs index 8eefbfcf..eadf0394 100644 --- a/tests/ui/pass/ghost_local.rs +++ b/tests/ui/pass/ghost_local.rs @@ -1,5 +1,6 @@ //@check-pass //@compile-flags: -C debug-assertions=off -A unused-variables +//@rustc-env: THRUST_SOLVER=tests/thrust-pcsat-wrapper use thrust_models::model::{Int, Seq}; use thrust_models::Ghost; diff --git a/tests/ui/pass/ghost_self.rs b/tests/ui/pass/ghost_self.rs index 8e7aec8c..7b8e901a 100644 --- a/tests/ui/pass/ghost_self.rs +++ b/tests/ui/pass/ghost_self.rs @@ -1,5 +1,6 @@ //@check-pass //@compile-flags: -C debug-assertions=off -A unused-variables +//@rustc-env: THRUST_SOLVER=tests/thrust-pcsat-wrapper use thrust_models::model::{Int, Seq}; use thrust_models::Ghost; diff --git a/tests/ui/pass/loop_invariant_fn_param_at_entry.rs b/tests/ui/pass/loop_invariant_fn_param_at_entry.rs index db6de3a5..72484c1a 100644 --- a/tests/ui/pass/loop_invariant_fn_param_at_entry.rs +++ b/tests/ui/pass/loop_invariant_fn_param_at_entry.rs @@ -1,5 +1,6 @@ //@check-pass //@compile-flags: -C debug-assertions=off +//@rustc-env: THRUST_SOLVER=tests/thrust-pcsat-wrapper #[thrust_macros::requires(true)] #[thrust_macros::ensures(result.len() == v.len() + 2)] diff --git a/tests/ui/pass/seq_basic.rs b/tests/ui/pass/seq_basic.rs index 99ff2286..758f41cf 100644 --- a/tests/ui/pass/seq_basic.rs +++ b/tests/ui/pass/seq_basic.rs @@ -1,5 +1,6 @@ //@check-pass //@compile-flags: -C debug-assertions=off +//@rustc-env: THRUST_SOLVER=tests/thrust-pcsat-wrapper use thrust_models::model::{Int, Seq}; diff --git a/tests/ui/pass/seq_concat.rs b/tests/ui/pass/seq_concat.rs index 1821bbe9..df08fcb6 100644 --- a/tests/ui/pass/seq_concat.rs +++ b/tests/ui/pass/seq_concat.rs @@ -1,5 +1,6 @@ //@check-pass //@compile-flags: -C debug-assertions=off +//@rustc-env: THRUST_SOLVER=tests/thrust-pcsat-wrapper use thrust_models::model::{Int, Seq}; diff --git a/tests/ui/pass/slice_first_mut.rs b/tests/ui/pass/slice_first_mut.rs index 1d592a5d..4bc80f27 100644 --- a/tests/ui/pass/slice_first_mut.rs +++ b/tests/ui/pass/slice_first_mut.rs @@ -1,5 +1,6 @@ //@check-pass //@compile-flags: -C debug-assertions=off +//@rustc-env: THRUST_SOLVER=tests/thrust-pcsat-wrapper #[thrust::trusted] #[thrust_macros::requires(true)] diff --git a/tests/ui/pass/slice_index.rs b/tests/ui/pass/slice_index.rs index 1519a7dc..1aa8e82e 100644 --- a/tests/ui/pass/slice_index.rs +++ b/tests/ui/pass/slice_index.rs @@ -1,5 +1,6 @@ //@check-pass //@compile-flags: -C debug-assertions=off +//@rustc-env: THRUST_SOLVER=tests/thrust-pcsat-wrapper #[thrust::trusted] #[thrust_macros::requires(true)] diff --git a/tests/ui/pass/slice_index_mut.rs b/tests/ui/pass/slice_index_mut.rs index 22f95ce3..6476fe5c 100644 --- a/tests/ui/pass/slice_index_mut.rs +++ b/tests/ui/pass/slice_index_mut.rs @@ -1,5 +1,6 @@ //@check-pass //@compile-flags: -C debug-assertions=off +//@rustc-env: THRUST_SOLVER=tests/thrust-pcsat-wrapper #[thrust::trusted] #[thrust_macros::requires(true)] diff --git a/tests/ui/pass/slice_last_mut.rs b/tests/ui/pass/slice_last_mut.rs index cc8d0e8e..2d3694f3 100644 --- a/tests/ui/pass/slice_last_mut.rs +++ b/tests/ui/pass/slice_last_mut.rs @@ -1,5 +1,6 @@ //@check-pass //@compile-flags: -C debug-assertions=off +//@rustc-env: THRUST_SOLVER=tests/thrust-pcsat-wrapper #[thrust::trusted] #[thrust_macros::requires(true)] diff --git a/tests/ui/pass/slice_len_guard_mut.rs b/tests/ui/pass/slice_len_guard_mut.rs index 23950648..8efe07ea 100644 --- a/tests/ui/pass/slice_len_guard_mut.rs +++ b/tests/ui/pass/slice_len_guard_mut.rs @@ -1,5 +1,6 @@ //@check-pass //@compile-flags: -C debug-assertions=off -C opt-level=2 +//@rustc-env: THRUST_SOLVER=tests/thrust-pcsat-wrapper // At `-C opt-level=1` and above rustc reads slice metadata straight off the `&mut [i32]` // local (`_len = PtrMetadata(copy _v)`) instead of through a shared reborrow, so this pins diff --git a/tests/ui/pass/slice_methods.rs b/tests/ui/pass/slice_methods.rs index a0565820..e1022b3b 100644 --- a/tests/ui/pass/slice_methods.rs +++ b/tests/ui/pass/slice_methods.rs @@ -1,5 +1,6 @@ //@check-pass //@compile-flags: -C debug-assertions=off +//@rustc-env: THRUST_SOLVER=tests/thrust-pcsat-wrapper #[thrust::trusted] #[thrust_macros::requires(true)] diff --git a/tests/ui/pass/slice_methods_mut.rs b/tests/ui/pass/slice_methods_mut.rs index 9d61f5bc..aed2d3b2 100644 --- a/tests/ui/pass/slice_methods_mut.rs +++ b/tests/ui/pass/slice_methods_mut.rs @@ -1,5 +1,6 @@ //@check-pass //@compile-flags: -C debug-assertions=off +//@rustc-env: THRUST_SOLVER=tests/thrust-pcsat-wrapper #[thrust::trusted] #[thrust_macros::requires(true)] diff --git a/tests/ui/pass/vec_1.rs b/tests/ui/pass/vec_1.rs index cdab8ce5..d1d94547 100644 --- a/tests/ui/pass/vec_1.rs +++ b/tests/ui/pass/vec_1.rs @@ -1,5 +1,6 @@ //@check-pass //@compile-flags: -C debug-assertions=off +//@rustc-env: THRUST_SOLVER=tests/thrust-pcsat-wrapper fn main() { let mut v = Vec::new(); diff --git a/tests/ui/pass/vec_2.rs b/tests/ui/pass/vec_2.rs index 419a3516..021a12a1 100644 --- a/tests/ui/pass/vec_2.rs +++ b/tests/ui/pass/vec_2.rs @@ -1,5 +1,6 @@ //@check-pass //@compile-flags: -C debug-assertions=off +//@rustc-env: THRUST_SOLVER=tests/thrust-pcsat-wrapper fn main() { let mut v = Vec::new(); diff --git a/tests/ui/pass/vec_3.rs b/tests/ui/pass/vec_3.rs index a560af35..a48c7323 100644 --- a/tests/ui/pass/vec_3.rs +++ b/tests/ui/pass/vec_3.rs @@ -1,5 +1,6 @@ //@check-pass //@compile-flags: -C debug-assertions=off +//@rustc-env: THRUST_SOLVER=tests/thrust-pcsat-wrapper fn main() { let mut v = Vec::new(); diff --git a/tests/ui/pass/vec_deref.rs b/tests/ui/pass/vec_deref.rs index 54b3e760..7fc1c758 100644 --- a/tests/ui/pass/vec_deref.rs +++ b/tests/ui/pass/vec_deref.rs @@ -1,5 +1,6 @@ //@check-pass //@compile-flags: -C debug-assertions=off +//@rustc-env: THRUST_SOLVER=tests/thrust-pcsat-wrapper fn main() { let mut v: Vec = Vec::new(); From 7d886e09d5647e3dfd22dcc9597b516bc95c7a5c Mon Sep 17 00:00:00 2001 From: coord_e Date: Mon, 21 Sep 2026 16:04:13 +0900 Subject: [PATCH 5/5] Remove unstable slice_split_first_mut_loop.rs cases for now --- tests/ui/fail/slice_split_first_mut_loop.rs | 27 --------------------- tests/ui/pass/slice_split_first_mut_loop.rs | 27 --------------------- 2 files changed, 54 deletions(-) delete mode 100644 tests/ui/fail/slice_split_first_mut_loop.rs delete mode 100644 tests/ui/pass/slice_split_first_mut_loop.rs diff --git a/tests/ui/fail/slice_split_first_mut_loop.rs b/tests/ui/fail/slice_split_first_mut_loop.rs deleted file mode 100644 index 4a068d38..00000000 --- a/tests/ui/fail/slice_split_first_mut_loop.rs +++ /dev/null @@ -1,27 +0,0 @@ -//@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).len() == 2 - && (*result)[0] == 10 - && (*result)[1] == 20 -)] -fn slice() -> &'static mut [i32] { - unimplemented!() -} - -#[thrust::callable] -fn check() { - let sl = slice(); - let mut s = &mut *sl; - while let Some((first, rest)) = s.split_first_mut() { - *first = 0; - s = rest; - } - assert!(sl[0] != 0); -} - -fn main() {} diff --git a/tests/ui/pass/slice_split_first_mut_loop.rs b/tests/ui/pass/slice_split_first_mut_loop.rs deleted file mode 100644 index ba47b2fe..00000000 --- a/tests/ui/pass/slice_split_first_mut_loop.rs +++ /dev/null @@ -1,27 +0,0 @@ -//@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).len() == 2 - && (*result)[0] == 10 - && (*result)[1] == 20 -)] -fn slice() -> &'static mut [i32] { - unimplemented!() -} - -#[thrust::callable] -fn check() { - let sl = slice(); - let mut s = &mut *sl; - while let Some((first, rest)) = s.split_first_mut() { - *first = 0; - s = rest; - } - assert!(sl[0] == 0); -} - -fn main() {}