diff --git a/src/analyze.rs b/src/analyze.rs index a4ffa5f4..6ba7faea 100644 --- a/src/analyze.rs +++ b/src/analyze.rs @@ -271,6 +271,14 @@ impl<'tcx> Analyzer<'tcx> { self.def_ids.clone() } + pub fn mark_uses_seq_concat(&self) { + self.system.borrow_mut().uses_seq_concat = true; + } + + pub fn mark_uses_seq_subseq(&self) { + self.system.borrow_mut().uses_seq_subseq = true; + } + pub fn add_clause(&mut self, clause: chc::Clause) { self.system.borrow_mut().push_clause(clause); } diff --git a/src/analyze/annot.rs b/src/analyze/annot.rs index 76e76e22..ae74ca94 100644 --- a/src/analyze/annot.rs +++ b/src/analyze/annot.rs @@ -137,6 +137,62 @@ pub fn array_model_store_path() -> [Symbol; 3] { ] } +pub fn seq_model_path() -> [Symbol; 3] { + [ + Symbol::intern("thrust"), + Symbol::intern("def"), + Symbol::intern("seq_model"), + ] +} + +pub fn seq_empty_path() -> [Symbol; 3] { + [ + Symbol::intern("thrust"), + Symbol::intern("def"), + Symbol::intern("seq_empty"), + ] +} + +pub fn seq_singleton_path() -> [Symbol; 3] { + [ + Symbol::intern("thrust"), + Symbol::intern("def"), + Symbol::intern("seq_singleton"), + ] +} + +pub fn seq_len_path() -> [Symbol; 3] { + [ + Symbol::intern("thrust"), + Symbol::intern("def"), + Symbol::intern("seq_len"), + ] +} + +pub fn seq_push_path() -> [Symbol; 3] { + [ + Symbol::intern("thrust"), + Symbol::intern("def"), + Symbol::intern("seq_push"), + ] +} + +pub fn seq_concat_path() -> [Symbol; 3] { + [ + Symbol::intern("thrust"), + Symbol::intern("def"), + Symbol::intern("seq_concat"), + ] +} + +pub fn seq_subsequence_path() -> [Symbol; 3] { + [ + Symbol::intern("thrust"), + Symbol::intern("def"), + Symbol::intern("seq_subsequence"), + ] +} + pub fn exists_path() -> [Symbol; 3] { [ Symbol::intern("thrust"), diff --git a/src/analyze/annot_fn.rs b/src/analyze/annot_fn.rs index 0249e4aa..7edd1c55 100644 --- a/src/analyze/annot_fn.rs +++ b/src/analyze/annot_fn.rs @@ -623,9 +623,18 @@ 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); - FormulaOrTerm::Term(array_term.select(index_term)) + let is_seq = array_ty + .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) + } else { + array_term + }; + FormulaOrTerm::Term(array_inner.select(index_term)) } ExprKind::MethodCall(method, receiver, args, _) => { if let Some(def_id) = self.typeck.type_dependent_def_id(hir.hir_id) { @@ -644,6 +653,56 @@ impl<'a, 'tcx> AnnotFnTranslator<'a, 'tcx> { let t = self.to_term(receiver); return FormulaOrTerm::Term(t); } + 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)); + } + 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])); + } + if Some(def_id) == self.def_ids.seq_concat() { + assert_eq!(args.len(), 1, "Seq::concat takes exactly 1 argument"); + self.analyzer.mark_uses_seq_concat(); + let t = self.to_term(receiver); + let other = self.to_term(&args[0]); + let a_arr = t.clone().tuple_proj(0); + let a_len = t.tuple_proj(1); + let b_arr = other.clone().tuple_proj(0); + let b_len = other.tuple_proj(1); + // The array half is the recursive SMT-defined + // function `seq_concat_arr_int(sa, sn, ta, tn)`; + // the length half is computed inline so length + // properties remain provable on any solver (the + // SMT obligation never has to mention the array). + let new_arr = chc::Term::App( + chc::Function::SEQ_CONCAT_ARR_INT, + vec![a_arr, a_len.clone(), b_arr, b_len.clone()], + ); + let new_len = a_len.add(b_len); + 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"); + self.analyzer.mark_uses_seq_subseq(); + let t = self.to_term(receiver); + let l = self.to_term(&args[0]); + let r = self.to_term(&args[1]); + let arr = t.tuple_proj(0); + let new_arr = chc::Term::App( + chc::Function::SEQ_SUBSEQ_ARR_INT, + vec![arr, l.clone(), r.clone()], + ); + let new_len = r.sub(l); + return FormulaOrTerm::Term(chc::Term::tuple(vec![new_arr, new_len])); + } } unimplemented!("unsupported method call in formula: {:?}", method) } @@ -719,6 +778,24 @@ impl<'a, 'tcx> AnnotFnTranslator<'a, 'tcx> { let t = self.to_term(&args[0]); return FormulaOrTerm::Term(chc::Term::box_(t)); } + if Some(def_id) == self.def_ids.seq_empty() { + assert!(args.is_empty(), "Seq::empty does not take any arguments"); + let arr = chc::Term::App(chc::Function::SEQ_DEFAULT_ARR_INT, vec![]); + return FormulaOrTerm::Term(chc::Term::tuple(vec![ + arr, + chc::Term::int(0), + ])); + } + 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 arr = chc::Term::App(chc::Function::SEQ_DEFAULT_ARR_INT, vec![]); + let new_arr = arr.store(chc::Term::int(0), v); + return FormulaOrTerm::Term(chc::Term::tuple(vec![ + new_arr, + chc::Term::int(1), + ])); + } if let rustc_hir::def::DefKind::Ctor(ctor_of, _) = def_kind { let terms = args.iter().map(|e| self.to_term(e)).collect(); match ctor_of { diff --git a/src/analyze/did_cache.rs b/src/analyze/did_cache.rs index 15149120..650d3756 100644 --- a/src/analyze/did_cache.rs +++ b/src/analyze/did_cache.rs @@ -24,6 +24,14 @@ struct DefIds { box_model_new: OnceCell>, array_model_store: OnceCell>, + seq_model: OnceCell>, + seq_empty: OnceCell>, + seq_singleton: OnceCell>, + seq_len: OnceCell>, + seq_push: OnceCell>, + seq_concat: OnceCell>, + seq_subsequence: OnceCell>, + exists: OnceCell>, forall: OnceCell>, implies: OnceCell>, @@ -179,6 +187,55 @@ impl<'tcx> DefIdCache<'tcx> { .get_or_init(|| self.annotated_def(&crate::analyze::annot::array_model_store_path())) } + pub fn seq_model(&self) -> Option { + *self + .def_ids + .seq_model + .get_or_init(|| self.annotated_def(&crate::analyze::annot::seq_model_path())) + } + + pub fn seq_empty(&self) -> Option { + *self + .def_ids + .seq_empty + .get_or_init(|| self.annotated_def(&crate::analyze::annot::seq_empty_path())) + } + + pub fn seq_singleton(&self) -> Option { + *self + .def_ids + .seq_singleton + .get_or_init(|| self.annotated_def(&crate::analyze::annot::seq_singleton_path())) + } + + pub fn seq_len(&self) -> Option { + *self + .def_ids + .seq_len + .get_or_init(|| self.annotated_def(&crate::analyze::annot::seq_len_path())) + } + + pub fn seq_push(&self) -> Option { + *self + .def_ids + .seq_push + .get_or_init(|| self.annotated_def(&crate::analyze::annot::seq_push_path())) + } + + pub fn seq_concat(&self) -> Option { + *self + .def_ids + .seq_concat + .get_or_init(|| self.annotated_def(&crate::analyze::annot::seq_concat_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 exists(&self) -> Option { *self .def_ids diff --git a/src/annot.rs b/src/annot.rs index e51836e9..8457f60b 100644 --- a/src/annot.rs +++ b/src/annot.rs @@ -91,7 +91,7 @@ pub struct AnnotPathSegment { /// A trait for resolving variables in annotations to their logical representation and their sorts. pub trait Resolver { - type Output; + type Output: Clone; fn resolve(&self, ident: Ident) -> Option<(Self::Output, chc::Sort)>; } @@ -1222,7 +1222,7 @@ struct RefinementResolver<'a, T> { self_: Option<(Ident, chc::Sort)>, } -impl<'a, T> Resolver for RefinementResolver<'a, T> { +impl<'a, T: Clone> Resolver for RefinementResolver<'a, T> { type Output = rty::RefinedTypeVar; fn resolve(&self, ident: Ident) -> Option<(Self::Output, chc::Sort)> { if let Some((self_ident, sort)) = &self.self_ { @@ -1256,7 +1256,7 @@ pub struct MappedResolver<'a, T, F> { map: F, } -impl<'a, T, F, U> Resolver for MappedResolver<'a, T, F> +impl<'a, T: Clone, F, U: Clone> Resolver for MappedResolver<'a, T, F> where F: Fn(T) -> U, { @@ -1290,7 +1290,7 @@ impl<'a, T> Default for StackedResolver<'a, T> { } } -impl<'a, T> Resolver for StackedResolver<'a, T> { +impl<'a, T: Clone> Resolver for StackedResolver<'a, T> { type Output = T; fn resolve(&self, ident: Ident) -> Option<(Self::Output, chc::Sort)> { for resolver in &self.resolvers { diff --git a/src/chc.rs b/src/chc.rs index 2a61f375..13c31fae 100644 --- a/src/chc.rs +++ b/src/chc.rs @@ -414,6 +414,13 @@ impl Function { }; *elem } + Self::ITE => { + // (ite cond then_ else_) : sort_of(then_) + args.into_iter().nth(1).expect("ITE takes 3 args") + } + Self::SEQ_DEFAULT_ARR_INT | Self::SEQ_CONCAT_ARR_INT | Self::SEQ_SUBSEQ_ARR_INT => { + Sort::array(Sort::int(), Sort::int()) + } _ => unimplemented!(), } } @@ -432,6 +439,47 @@ impl Function { pub const NEG: Function = Function::new("-"); pub const STORE: Function = Function::new("store"); pub const SELECT: Function = Function::new("select"); + pub const ITE: Function = Function::new("ite"); + + /// Designated empty/default array of element sort `Int`. Used by + /// `Seq::empty()` and `Seq::singleton(_)` to fill the array slot of + /// an otherwise length-determined sequence. Defined as + /// `((as const (Array Int Int)) 0)` in the SMT preamble; the + /// concrete contents are irrelevant because the length (0 or 1) is + /// the only thing reasoned about. + pub const SEQ_DEFAULT_ARR_INT: Function = Function::new("seq_default_arr_int"); + /// The array of `Seq::concat(_, _)` for element sort `Int`. Defined + /// in the SMT preamble via `define-fun-rec` as the structural + /// recursion over the second sequence's length: + /// ```smt2 + /// (define-fun-rec seq_concat_arr_int + /// ((sa (Array Int Int)) (sn Int) (ta (Array Int Int)) (tn Int)) + /// (Array Int Int) + /// (ite (<= tn 0) sa + /// (store (seq_concat_arr_int sa sn ta (- tn 1)) + /// (+ sn (- tn 1)) + /// (select ta (- tn 1))))) + /// ``` + /// pcsat unfolds this for any concrete `tn`. Universally quantified + /// `tn` is currently out of reach (no inductive invariant found in a + /// reasonable budget); the follow-up peephole commit sidesteps this + /// for indexed access. z3-Spacer in HORN logic treats every + /// `define-fun-rec` as uninterpreted and returns `unknown` — by user + /// direction, we don't aim to support indexed reasoning on Z3. + pub const SEQ_CONCAT_ARR_INT: Function = Function::new("seq_concat_arr_int"); + /// The array of `Seq::subsequence(_, l, r)` for element sort `Int`. + /// Defined via `define-fun-rec` as the structural recursion over + /// `r - l`: + /// ```smt2 + /// (define-fun-rec seq_subseq_arr_int + /// ((a (Array Int Int)) (l Int) (r Int)) + /// (Array Int Int) + /// (ite (<= r l) seq_default_arr_int + /// (store (seq_subseq_arr_int a l (- r 1)) + /// (- (- r 1) l) + /// (select a (- r 1))))) + /// ``` + pub const SEQ_SUBSEQ_ARR_INT: Function = Function::new("seq_subseq_arr_int"); } /// A logical term. @@ -744,10 +792,91 @@ impl Term { Term::App(Function::NEG, vec![self]) } - pub fn select(self, index: Self) -> Self { + pub fn select(self, index: Self) -> Self + where + V: Clone, + { + // Peephole 1: when both indices are concrete integer literals, reduce + // `select(store(a, i, v), j)` to `v` (`i == j`) or `select(a, j)` + // (`i != j`). Same motivation as the `tuple_proj` simplifier: keep + // datatype/array constructors from leaking into Spacer clauses where + // it can't reduce them. Non-literal indices are deferred to the + // solver via the general select-of-store axiom. + if let (Term::App(Function::STORE, _), Term::Int(j)) = (&self, &index) { + let Term::App(_, mut args) = self else { + unreachable!() + }; + assert_eq!(args.len(), 3, "STORE takes 3 args"); + let stored_value = args.pop().unwrap(); + let stored_index = args.pop().unwrap(); + let base = args.pop().unwrap(); + if let Term::Int(i) = &stored_index { + return if i == j { + stored_value + } else { + base.select(index) + }; + } + // Re-build the original term if we couldn't simplify. + return Term::App( + Function::SELECT, + vec![ + Term::App(Function::STORE, vec![base, stored_index, stored_value]), + index, + ], + ); + } + // Peephole 2: inline one step of the `seq_concat_arr_int` / + // `seq_subseq_arr_int` 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_arr_int(sa, sn, ta, tn), i) + // ↦ ite(i < sn, select(sa, i), select(ta, i - sn))` + if let Term::App(Function::SEQ_CONCAT_ARR_INT, _) = &self { + let Term::App(_, mut args) = self else { + unreachable!() + }; + assert_eq!(args.len(), 4, "SEQ_CONCAT_ARR_INT takes 4 args"); + let _tn = args.pop().unwrap(); + let ta = args.pop().unwrap(); + let sn = args.pop().unwrap(); + let sa = args.pop().unwrap(); + let cond = index.clone().lt(sn.clone()); + let then_ = sa.select(index.clone()); + let else_ = ta.select(index.sub(sn)); + return Term::ite(cond, then_, else_); + } + // `select(seq_subseq_arr_int(a, l, r), i) + // ↦ ite(0 <= i < r - l, select(a, l + i), select(seq_default_arr_int, 0))` + // The `r - l` bound matches the recursive definition's base + // case. Out-of-range indices fall through to the designated + // default array, mirroring the base case `r <= l → default`. + if let Term::App(Function::SEQ_SUBSEQ_ARR_INT, _) = &self { + let Term::App(_, mut args) = self else { + unreachable!() + }; + assert_eq!(args.len(), 3, "SEQ_SUBSEQ_ARR_INT takes 3 args"); + let r = args.pop().unwrap(); + let l = args.pop().unwrap(); + let a = args.pop().unwrap(); + let len = r.sub(l.clone()); + let in_range = index.clone().ge(Term::int(0)).and(index.clone().lt(len)); + let then_ = a.select(l.add(index)); + let else_ = Term::App(Function::SEQ_DEFAULT_ARR_INT, vec![]).select(Term::int(0)); + return Term::ite(in_range, then_, else_); + } Term::App(Function::SELECT, vec![self, index]) } + pub fn ite(cond: Self, then_: Self, else_: Self) -> Self { + Term::App(Function::ITE, vec![cond, then_, else_]) + } + pub fn store(self, index: Self, elem: Self) -> Self { Term::App(Function::STORE, vec![self, index, elem]) } @@ -757,6 +886,13 @@ impl Term { } pub fn tuple_proj(self, i: usize) -> Self { + // Peephole: `tuple_proj(tuple(t0,...,tn), i)` ↦ `ti`. Without this, + // HORN solvers like Spacer struggle to reduce datatype constructors + // appearing inside clauses, which makes downstream reasoning brittle. + if let Term::Tuple(mut ts) = self { + assert!(i < ts.len(), "tuple_proj index out of bounds"); + return ts.swap_remove(i); + } Term::TupleProj(Box::new(self), i) } @@ -1851,6 +1987,13 @@ pub struct System { pub user_defined_pred_defs: Vec, pub clauses: IndexVec, pub pred_vars: IndexVec, + /// Set by the analyzer when `Seq::concat` is lowered, gating the + /// `seq_concat_arr_int` declaration in the SMT preamble. pcsat would + /// otherwise treat the unused function as a synthesis target and + /// fail to parse. + pub uses_seq_concat: bool, + /// Same as [`Self::uses_seq_concat`] but for `Seq::subsequence`. + pub uses_seq_subseq: bool, } impl System { diff --git a/src/chc/smtlib2.rs b/src/chc/smtlib2.rs index 7904d58d..81245ba9 100644 --- a/src/chc/smtlib2.rs +++ b/src/chc/smtlib2.rs @@ -152,12 +152,16 @@ impl<'ctx, 'a> std::fmt::Display for Term<'ctx, 'a> { ) } chc::Term::App(fn_, args) => { - write!( - f, - "({} {})", - fn_, - List::open(args.iter().map(|t| Term::new(self.ctx, self.clause, t))) - ) + if args.is_empty() { + write!(f, "{}", fn_) + } else { + write!( + f, + "({} {})", + fn_, + List::open(args.iter().map(|t| Term::new(self.ctx, self.clause, t))) + ) + } } chc::Term::Tuple(ts) => { let ss: Vec<_> = ts.iter().map(|t| self.clause.term_sort(t)).collect(); @@ -624,6 +628,53 @@ impl<'a> std::fmt::Display for System<'a> { writeln!(f, "{}\n", RawCommand::new(raw_command))?; } + // Designated default array used as the array slot of `Seq::empty()` / + // `Seq::singleton(_)`. Always emitted even when unused — harmless, + // and lets the analyzer emit references unconditionally. Defined + // (not declared) so pcsat does not treat it as a synthesis target; + // the concrete value is irrelevant because indices ≥ length are + // never accessed. + writeln!( + f, + "(define-fun seq_default_arr_int () (Array Int Int) \ + ((as const (Array Int Int)) 0))\n" + )?; + // Recursive definitions of `seq_concat_arr_int(sa, sn, ta, tn)` and + // `seq_subseq_arr_int(a, l, r)`: the array half of the + // `Seq::concat` / `Seq::subsequence` result. Emitted via + // `define-fun-rec` so pcsat can unfold them for any concrete + // recursion bound (`tn` for concat, `r - l` for subsequence). + // Universally quantified bounds are out of reach without further + // optimisation; see the follow-up peephole commit and + // `chc::Function::SEQ_CONCAT_ARR_INT`. + // + // The length half of both operations is computed inline by the + // analyzer (`a.len + b.len` for concat, `r - l` for subsequence), + // so the length-only reasoning that worked under z3 before still + // works — the SMT obligation simply never references the array + // half. + if self.inner.uses_seq_concat { + writeln!( + f, + "(define-fun-rec seq_concat_arr_int \ + ((sa (Array Int Int)) (sn Int) (ta (Array Int Int)) (tn Int)) (Array Int Int) \ + (ite (<= tn 0) sa \ + (store (seq_concat_arr_int sa sn ta (- tn 1)) \ + (+ sn (- tn 1)) \ + (select ta (- tn 1)))))\n" + )?; + } + if self.inner.uses_seq_subseq { + writeln!( + f, + "(define-fun-rec seq_subseq_arr_int \ + ((a (Array Int Int)) (l Int) (r Int)) (Array Int Int) \ + (ite (<= r l) seq_default_arr_int \ + (store (seq_subseq_arr_int a l (- r 1)) \ + (- (- r 1) l) \ + (select a (- r 1)))))\n" + )?; + } for user_defined_pred_def in &self.inner.user_defined_pred_defs { writeln!( f, diff --git a/src/chc/unbox.rs b/src/chc/unbox.rs index bfb782eb..eaf8ba88 100644 --- a/src/chc/unbox.rs +++ b/src/chc/unbox.rs @@ -181,6 +181,8 @@ pub fn unbox(system: System) -> System { user_defined_pred_defs, clauses, pred_vars, + uses_seq_concat, + uses_seq_subseq, } = system; let datatypes = datatypes.into_iter().map(unbox_datatype).collect(); let clauses = clauses.into_iter().map(unbox_clause).collect(); @@ -195,5 +197,7 @@ pub fn unbox(system: System) -> System { user_defined_pred_defs, clauses, pred_vars, + uses_seq_concat, + uses_seq_subseq, } } diff --git a/std.rs b/std.rs index 87e5bde2..62a88015 100644 --- a/std.rs +++ b/std.rs @@ -195,6 +195,77 @@ mod thrust_models { unimplemented!() } } + + #[thrust::def::seq_model] + pub struct Seq(pub Array, pub Int); + + impl PartialEq for Seq where U: super::Model { + #[thrust::ignored] + fn eq(&self, _other: &U) -> bool { + unimplemented!() + } + } + + impl std::ops::Index for Seq where U: super::Model { + type Output = T; + + #[thrust::ignored] + fn index(&self, _index: U) -> &Self::Output { + unimplemented!() + } + } + + impl Seq { + #[allow(dead_code)] + #[thrust::def::seq_empty] + #[thrust::ignored] + pub fn empty() -> Self { + unimplemented!() + } + + #[allow(dead_code)] + #[thrust::def::seq_singleton] + #[thrust::ignored] + pub fn singleton(_x: T) -> Self { + unimplemented!() + } + + #[allow(dead_code)] + #[thrust::def::seq_len] + #[thrust::ignored] + pub fn len(&self) -> Int { + unimplemented!() + } + + #[allow(dead_code)] + #[thrust::def::seq_push] + #[thrust::ignored] + pub fn push(self, _x: T) -> Self { + unimplemented!() + } + + #[allow(dead_code)] + #[thrust::def::seq_concat] + #[thrust::ignored] + pub fn concat(self, _other: Self) -> Self { + unimplemented!() + } + + #[allow(dead_code)] + #[thrust::def::seq_subsequence] + #[thrust::ignored] + pub fn subsequence(&self, _l: L, _r: R) -> Self + where + L: super::Model, + R: super::Model, + { + unimplemented!() + } + } + } + + impl Model for model::Seq where T: Model { + type Ty = model::Seq<::Ty>; } impl Model for model::Int { diff --git a/tests/ui/fail/seq_concat.rs b/tests/ui/fail/seq_concat.rs new file mode 100644 index 00000000..bba0a6cd --- /dev/null +++ b/tests/ui/fail/seq_concat.rs @@ -0,0 +1,13 @@ +//@error-in-other-file: Unsat +//@compile-flags: -C debug-assertions=off + +use thrust_models::model::{Int, Seq}; + +#[thrust_macros::requires(true)] +#[thrust_macros::ensures(s.concat(t).len() == s.len() + t.len() + 1)] +fn concat_lengths_add(s: Seq, t: Seq) -> () { + let _ = s; + let _ = t; +} + +fn main() {} diff --git a/tests/ui/fail/seq_concat_index.rs b/tests/ui/fail/seq_concat_index.rs new file mode 100644 index 00000000..15587a70 --- /dev/null +++ b/tests/ui/fail/seq_concat_index.rs @@ -0,0 +1,15 @@ +//@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(0 <= i && i < s.len())] +#[thrust_macros::ensures(s.concat(t)[i] == t[i])] +fn concat_index_left(s: Seq, t: Seq, i: Int) -> () { + let _ = s; + let _ = t; + let _ = i; +} + +fn main() {} diff --git a/tests/ui/fail/seq_concat_index_right.rs b/tests/ui/fail/seq_concat_index_right.rs new file mode 100644 index 00000000..03f7cb78 --- /dev/null +++ b/tests/ui/fail/seq_concat_index_right.rs @@ -0,0 +1,15 @@ +//@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(s.len() <= i && i < s.len() + t.len())] +#[thrust_macros::ensures(s.concat(t)[i] == s[i - s.len()])] +fn concat_index_right(s: Seq, t: Seq, i: Int) -> () { + let _ = s; + let _ = t; + let _ = i; +} + +fn main() {} diff --git a/tests/ui/fail/seq_empty.rs b/tests/ui/fail/seq_empty.rs new file mode 100644 index 00000000..dde487cd --- /dev/null +++ b/tests/ui/fail/seq_empty.rs @@ -0,0 +1,10 @@ +//@error-in-other-file: Unsat +//@compile-flags: -C debug-assertions=off + +use thrust_models::model::{Int, Seq}; + +#[thrust_macros::requires(true)] +#[thrust_macros::ensures(Seq::::empty().len() == 1)] +fn empty_has_zero_len() -> () {} + +fn main() {} diff --git a/tests/ui/fail/seq_index.rs b/tests/ui/fail/seq_index.rs new file mode 100644 index 00000000..cc147cae --- /dev/null +++ b/tests/ui/fail/seq_index.rs @@ -0,0 +1,13 @@ +//@error-in-other-file: Unsat +//@compile-flags: -C debug-assertions=off + +use thrust_models::model::{Int, Seq}; + +#[thrust_macros::requires(true)] +#[thrust_macros::ensures(s.push(x)[s.len()] == x + 1)] +fn push_index(s: Seq, x: Int) -> () { + let _ = s; + let _ = x; +} + +fn main() {} diff --git a/tests/ui/fail/seq_len_push.rs b/tests/ui/fail/seq_len_push.rs new file mode 100644 index 00000000..d485752c --- /dev/null +++ b/tests/ui/fail/seq_len_push.rs @@ -0,0 +1,13 @@ +//@error-in-other-file: Unsat +//@compile-flags: -C debug-assertions=off + +use thrust_models::model::{Int, Seq}; + +#[thrust_macros::requires(true)] +#[thrust_macros::ensures(s.push(x).len() == s.len() + 2)] +fn push_increments(s: Seq, x: Int) -> () { + let _ = s; + let _ = x; +} + +fn main() {} diff --git a/tests/ui/fail/seq_singleton.rs b/tests/ui/fail/seq_singleton.rs new file mode 100644 index 00000000..5bbe41e5 --- /dev/null +++ b/tests/ui/fail/seq_singleton.rs @@ -0,0 +1,12 @@ +//@error-in-other-file: Unsat +//@compile-flags: -C debug-assertions=off + +use thrust_models::model::{Int, Seq}; + +#[thrust_macros::requires(true)] +#[thrust_macros::ensures(Seq::singleton(x).len() == 2)] +fn singleton_holds_one(x: Int) -> () { + let _ = x; +} + +fn main() {} diff --git a/tests/ui/fail/seq_specs_concat_run.rs b/tests/ui/fail/seq_specs_concat_run.rs new file mode 100644 index 00000000..772bc92f --- /dev/null +++ b/tests/ui/fail/seq_specs_concat_run.rs @@ -0,0 +1,21 @@ +//@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(true)] +#[thrust_macros::ensures( + // wrong: swap order + result.1 == Seq::::singleton(x).concat(Seq::::singleton(y)).len() + && result.0[0] == Seq::::singleton(y).concat(Seq::::singleton(x))[0] + && result.0[1] == Seq::::singleton(y).concat(Seq::::singleton(x))[1] +)] +fn pair(x: i64, y: i64) -> Vec { + let mut v = Vec::new(); + v.push(x); + v.push(y); + v +} + +fn main() {} diff --git a/tests/ui/fail/seq_specs_loop_invariant.rs b/tests/ui/fail/seq_specs_loop_invariant.rs new file mode 100644 index 00000000..eb7b3412 --- /dev/null +++ b/tests/ui/fail/seq_specs_loop_invariant.rs @@ -0,0 +1,26 @@ +//@error-in-other-file: Unsat +//@compile-flags: -C debug-assertions=off +//@rustc-env: THRUST_SOLVER=tests/thrust-pcsat-wrapper + +use thrust_models::model::Seq; + +#[thrust_macros::requires(true)] +// wrong: should be `.push(0).push(1).push(2).len()` (== 3), not 4 pushes +#[thrust_macros::ensures( + result.1 == Seq::::empty().push(0).push(1).push(2).push(3).len() +)] +#[thrust_macros::invariant_context] +fn push_three() -> Vec { + let mut w: Vec = Vec::new(); + let mut i: i64 = 0; + while i < 3 { + thrust_macros::invariant!( + |i: i64, w: Vec| 0 <= i && i <= 3 && w.1 == i + ); + w.push(i); + i += 1; + } + w +} + +fn main() {} diff --git a/tests/ui/fail/seq_specs_vec_build.rs b/tests/ui/fail/seq_specs_vec_build.rs new file mode 100644 index 00000000..9849df49 --- /dev/null +++ b/tests/ui/fail/seq_specs_vec_build.rs @@ -0,0 +1,23 @@ +//@error-in-other-file: Unsat +//@compile-flags: -C debug-assertions=off +//@rustc-env: THRUST_SOLVER=tests/thrust-pcsat-wrapper + +use thrust_models::model::Seq; + +#[thrust_macros::requires(true)] +#[thrust_macros::ensures( + result.1 == Seq::::empty().push(10).push(20).push(30).len() + && result.0[0] == Seq::::empty().push(10).push(20).push(30)[0] + && result.0[1] == Seq::::empty().push(10).push(20).push(30)[1] + // wrong: last element should be 30, not 99 + && result.0[2] == Seq::::empty().push(10).push(20).push(99)[2] +)] +fn build_three() -> Vec { + let mut v = Vec::new(); + v.push(10); + v.push(20); + v.push(30); + v +} + +fn main() {} diff --git a/tests/ui/fail/seq_subseq_index.rs b/tests/ui/fail/seq_subseq_index.rs new file mode 100644 index 00000000..c41d589c --- /dev/null +++ b/tests/ui/fail/seq_subseq_index.rs @@ -0,0 +1,16 @@ +//@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(0 <= l && l <= r && r <= s.len() && 0 <= i && i < r - l)] +#[thrust_macros::ensures(s.subsequence(l, r)[i] == s[i])] +fn subseq_index(s: Seq, l: Int, r: Int, i: Int) -> () { + let _ = s; + let _ = l; + let _ = r; + let _ = i; +} + +fn main() {} diff --git a/tests/ui/fail/seq_subsequence.rs b/tests/ui/fail/seq_subsequence.rs new file mode 100644 index 00000000..dccae619 --- /dev/null +++ b/tests/ui/fail/seq_subsequence.rs @@ -0,0 +1,14 @@ +//@error-in-other-file: Unsat +//@compile-flags: -C debug-assertions=off + +use thrust_models::model::{Int, Seq}; + +#[thrust_macros::requires(true)] +#[thrust_macros::ensures(s.subsequence(l, r).len() == r - l + 1)] +fn subsequence_length(s: Seq, l: Int, r: Int) -> () { + let _ = s; + let _ = l; + let _ = r; +} + +fn main() {} diff --git a/tests/ui/pass/seq_concat.rs b/tests/ui/pass/seq_concat.rs new file mode 100644 index 00000000..1821bbe9 --- /dev/null +++ b/tests/ui/pass/seq_concat.rs @@ -0,0 +1,13 @@ +//@check-pass +//@compile-flags: -C debug-assertions=off + +use thrust_models::model::{Int, Seq}; + +#[thrust_macros::requires(true)] +#[thrust_macros::ensures(s.concat(t).len() == s.len() + t.len())] +fn concat_lengths_add(s: Seq, t: Seq) -> () { + let _ = s; + let _ = t; +} + +fn main() {} diff --git a/tests/ui/pass/seq_concat_index.rs b/tests/ui/pass/seq_concat_index.rs new file mode 100644 index 00000000..f28e5d92 --- /dev/null +++ b/tests/ui/pass/seq_concat_index.rs @@ -0,0 +1,15 @@ +//@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 <= i && i < s.len())] +#[thrust_macros::ensures(s.concat(t)[i] == s[i])] +fn concat_index_left(s: Seq, t: Seq, i: Int) -> () { + let _ = s; + let _ = t; + let _ = i; +} + +fn main() {} diff --git a/tests/ui/pass/seq_concat_index_right.rs b/tests/ui/pass/seq_concat_index_right.rs new file mode 100644 index 00000000..f7db4eb2 --- /dev/null +++ b/tests/ui/pass/seq_concat_index_right.rs @@ -0,0 +1,15 @@ +//@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(s.len() <= i && i < s.len() + t.len())] +#[thrust_macros::ensures(s.concat(t)[i] == t[i - s.len()])] +fn concat_index_right(s: Seq, t: Seq, i: Int) -> () { + let _ = s; + let _ = t; + let _ = i; +} + +fn main() {} diff --git a/tests/ui/pass/seq_empty.rs b/tests/ui/pass/seq_empty.rs new file mode 100644 index 00000000..a412f12b --- /dev/null +++ b/tests/ui/pass/seq_empty.rs @@ -0,0 +1,10 @@ +//@check-pass +//@compile-flags: -C debug-assertions=off + +use thrust_models::model::{Int, Seq}; + +#[thrust_macros::requires(true)] +#[thrust_macros::ensures(Seq::::empty().len() == 0)] +fn empty_has_zero_len() -> () {} + +fn main() {} diff --git a/tests/ui/pass/seq_index.rs b/tests/ui/pass/seq_index.rs new file mode 100644 index 00000000..6a5b6f81 --- /dev/null +++ b/tests/ui/pass/seq_index.rs @@ -0,0 +1,13 @@ +//@check-pass +//@compile-flags: -C debug-assertions=off + +use thrust_models::model::{Int, Seq}; + +#[thrust_macros::requires(true)] +#[thrust_macros::ensures(s.push(x)[s.len()] == x)] +fn push_index(s: Seq, x: Int) -> () { + let _ = s; + let _ = x; +} + +fn main() {} diff --git a/tests/ui/pass/seq_len_push.rs b/tests/ui/pass/seq_len_push.rs new file mode 100644 index 00000000..bb62ae92 --- /dev/null +++ b/tests/ui/pass/seq_len_push.rs @@ -0,0 +1,13 @@ +//@check-pass +//@compile-flags: -C debug-assertions=off + +use thrust_models::model::{Int, Seq}; + +#[thrust_macros::requires(true)] +#[thrust_macros::ensures(s.push(x).len() == s.len() + 1)] +fn push_increments(s: Seq, x: Int) -> () { + let _ = s; + let _ = x; +} + +fn main() {} diff --git a/tests/ui/pass/seq_singleton.rs b/tests/ui/pass/seq_singleton.rs new file mode 100644 index 00000000..697398c2 --- /dev/null +++ b/tests/ui/pass/seq_singleton.rs @@ -0,0 +1,12 @@ +//@check-pass +//@compile-flags: -C debug-assertions=off + +use thrust_models::model::{Int, Seq}; + +#[thrust_macros::requires(true)] +#[thrust_macros::ensures(Seq::singleton(x).len() == 1 && Seq::singleton(x)[0] == x)] +fn singleton_holds_one(x: Int) -> () { + let _ = x; +} + +fn main() {} diff --git a/tests/ui/pass/seq_specs_concat_run.rs b/tests/ui/pass/seq_specs_concat_run.rs new file mode 100644 index 00000000..b6719059 --- /dev/null +++ b/tests/ui/pass/seq_specs_concat_run.rs @@ -0,0 +1,29 @@ +//@check-pass +//@compile-flags: -C debug-assertions=off +//@rustc-env: THRUST_SOLVER=tests/thrust-pcsat-wrapper + +// A real runtime function returns the concatenation of two singletons. +// The post relates the result Vec to `Seq::singleton(x).concat(Seq::singleton(y))`, +// and the analyzer must reduce `concat[0]` / `concat[1]` syntactically. + +use thrust_models::model::{Int, Seq}; + +#[thrust_macros::requires(true)] +#[thrust_macros::ensures( + result.1 == Seq::::singleton(x).concat(Seq::::singleton(y)).len() + && result.0[0] == Seq::::singleton(x).concat(Seq::::singleton(y))[0] + && result.0[1] == Seq::::singleton(x).concat(Seq::::singleton(y))[1] +)] +fn pair(x: i64, y: i64) -> Vec { + let mut v = Vec::new(); + v.push(x); + v.push(y); + v +} + +fn main() { + let v = pair(7, 8); + assert!(v.len() == 2); + assert!(v[0] == 7); + assert!(v[1] == 8); +} diff --git a/tests/ui/pass/seq_specs_loop_invariant.rs b/tests/ui/pass/seq_specs_loop_invariant.rs new file mode 100644 index 00000000..f5abba9a --- /dev/null +++ b/tests/ui/pass/seq_specs_loop_invariant.rs @@ -0,0 +1,31 @@ +//@check-pass +//@compile-flags: -C debug-assertions=off +//@rustc-env: THRUST_SOLVER=tests/thrust-pcsat-wrapper + +// A loop builds a Vec by repeatedly pushing values; the loop invariant +// links the Vec's runtime length with a Seq value built by the same +// pushes in spec position. The Seq-side reasoning (`Seq::empty().len() +// == 0`, `s.push(x).len() == s.len() + 1`) drives the loop bound check. + +use thrust_models::model::Seq; + +#[thrust_macros::requires(true)] +#[thrust_macros::ensures(result.1 == Seq::::empty().push(0).push(1).push(2).len())] +#[thrust_macros::invariant_context] +fn push_three() -> Vec { + let mut w: Vec = Vec::new(); + let mut i: i64 = 0; + while i < 3 { + thrust_macros::invariant!( + |i: i64, w: Vec| 0 <= i && i <= 3 && w.1 == i + ); + w.push(i); + i += 1; + } + w +} + +fn main() { + let v = push_three(); + assert!(v.len() == 3); +} diff --git a/tests/ui/pass/seq_specs_vec_build.rs b/tests/ui/pass/seq_specs_vec_build.rs new file mode 100644 index 00000000..bf290c15 --- /dev/null +++ b/tests/ui/pass/seq_specs_vec_build.rs @@ -0,0 +1,33 @@ +//@check-pass +//@compile-flags: -C debug-assertions=off +//@rustc-env: THRUST_SOLVER=tests/thrust-pcsat-wrapper + +// A runtime function (builds a Vec) specified via Seq operations. +// The spec uses `Seq::empty().push(x).push(y)` to describe the contents, +// and the analyzer must reduce both sides syntactically (length and +// indexed access) to discharge each conjunct. + +use thrust_models::model::Seq; + +#[thrust_macros::requires(true)] +#[thrust_macros::ensures( + result.1 == Seq::::empty().push(10).push(20).push(30).len() + && result.0[0] == Seq::::empty().push(10).push(20).push(30)[0] + && result.0[1] == Seq::::empty().push(10).push(20).push(30)[1] + && result.0[2] == Seq::::empty().push(10).push(20).push(30)[2] +)] +fn build_three() -> Vec { + let mut v = Vec::new(); + v.push(10); + v.push(20); + v.push(30); + v +} + +fn main() { + let v = build_three(); + assert!(v.len() == 3); + assert!(v[0] == 10); + assert!(v[1] == 20); + assert!(v[2] == 30); +} diff --git a/tests/ui/pass/seq_subseq_index.rs b/tests/ui/pass/seq_subseq_index.rs new file mode 100644 index 00000000..3531cd17 --- /dev/null +++ b/tests/ui/pass/seq_subseq_index.rs @@ -0,0 +1,16 @@ +//@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 <= l && l <= r && r <= s.len() && 0 <= i && i < r - l)] +#[thrust_macros::ensures(s.subsequence(l, r)[i] == s[l + i])] +fn subseq_index(s: Seq, l: Int, r: Int, i: Int) -> () { + let _ = s; + let _ = l; + let _ = r; + let _ = i; +} + +fn main() {} diff --git a/tests/ui/pass/seq_subsequence.rs b/tests/ui/pass/seq_subsequence.rs new file mode 100644 index 00000000..aef50700 --- /dev/null +++ b/tests/ui/pass/seq_subsequence.rs @@ -0,0 +1,14 @@ +//@check-pass +//@compile-flags: -C debug-assertions=off + +use thrust_models::model::{Int, Seq}; + +#[thrust_macros::requires(true)] +#[thrust_macros::ensures(s.subsequence(l, r).len() == r - l)] +fn subsequence_length(s: Seq, l: Int, r: Int) -> () { + let _ = s; + let _ = l; + let _ = r; +} + +fn main() {}