diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 7740817..a3c8103 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -24,9 +24,33 @@ jobs: runs-on: ubuntu-latest permissions: contents: read + env: + COAR_IMAGE: ghcr.io/hiroshi-unno/coar@sha256:73144ed27a02b163d1a71b41b58f3b5414f12e91326015600cfdca64ff19f011 steps: - uses: actions/checkout@v4 - uses: ./.github/actions/setup-z3 + - name: Setup thrust-pcsat-wrapper + run: | + docker pull "$COAR_IMAGE" + + cat <<"EOF" > thrust-pcsat-wrapper + #!/bin/bash + + smt2=$(mktemp -p . --suffix .smt2) + trap "rm -f $smt2" EXIT + cp "$1" "$smt2" + out=$( + docker run --rm -v "$PWD:/mnt" -w /root/coar "$COAR_IMAGE" \ + main.exe -c ./config/solver/pcsat_tbq_ar.json -p pcsp "/mnt/$smt2" + ) + exit_code=$? + echo "${out%,*}" + exit "$exit_code" + EOF + chmod +x thrust-pcsat-wrapper + + mkdir -p ~/.local/bin + mv thrust-pcsat-wrapper ~/.local/bin/thrust-pcsat-wrapper - run: rustup show - uses: Swatinem/rust-cache@v2 - run: cargo test diff --git a/src/annot.rs b/src/annot.rs index f559bb8..730b75e 100644 --- a/src/annot.rs +++ b/src/annot.rs @@ -12,6 +12,7 @@ use rustc_ast::token::{BinOpToken, Delimiter, LitKind, Token, TokenKind}; use rustc_ast::tokenstream::{RefTokenTreeCursor, Spacing, TokenStream, TokenTree}; use rustc_index::IndexVec; use rustc_span::symbol::Ident; +use std::collections::HashMap; use crate::chc; use crate::pretty::PrettyDisplayExt as _; @@ -185,6 +186,7 @@ impl FormulaOrTerm { struct Parser<'a, T> { resolver: T, cursor: RefTokenTreeCursor<'a>, + formula_existentials: HashMap, } impl<'a, T> Parser<'a, T> @@ -232,6 +234,15 @@ where } } + fn expect_next_ident(&mut self) -> Result { + let t = self.next_token("ident")?; + if let Some((ident, _)) = t.ident() { + Ok(ident) + } else { + Err(ParseAttrError::unexpected_token("ident", t.clone())) + } + } + fn consume(&mut self) { self.cursor.next().unwrap(); } @@ -296,6 +307,7 @@ where let mut parser = Parser { resolver: self.boxed_resolver(), cursor: s.trees(), + formula_existentials: self.formula_existentials.clone(), }; let formula_or_term = parser.parse_formula_or_term_or_tuple()?; parser.end_of_input()?; @@ -305,9 +317,17 @@ where }; let formula_or_term = if let Some((ident, _)) = t.ident() { - match ident.as_str() { - "true" => FormulaOrTerm::Formula(chc::Formula::top()), - "false" => FormulaOrTerm::Formula(chc::Formula::bottom()), + match ( + ident.as_str(), + self.formula_existentials.get(ident.name.as_str()), + ) { + ("true", _) => FormulaOrTerm::Formula(chc::Formula::top()), + ("false", _) => FormulaOrTerm::Formula(chc::Formula::bottom()), + (_, Some(sort)) => { + let var = + chc::Term::FormulaExistentialVar(sort.clone(), ident.name.to_string()); + FormulaOrTerm::Term(var, sort.clone()) + } _ => { let (v, sort) = self.resolve(ident)?; FormulaOrTerm::Term(chc::Term::var(v), sort) @@ -575,8 +595,94 @@ where Ok(formula_or_term) } + fn parse_exists(&mut self) -> Result> { + match self.look_ahead_token(0) { + Some(Token { + kind: TokenKind::Ident(sym, _), + .. + }) if sym.as_str() == "exists" => { + self.consume(); + let mut vars = Vec::new(); + loop { + let ident = self.expect_next_ident()?; + self.expect_next_token(TokenKind::Colon, ":")?; + let sort = self.parse_sort()?; + vars.push((ident.name.to_string(), sort)); + match self.next_token(". or ,")? { + Token { + kind: TokenKind::Comma, + .. + } => {} + Token { + kind: TokenKind::Dot, + .. + } => break, + t => return Err(ParseAttrError::unexpected_token(". or ,", t.clone())), + } + } + self.formula_existentials.extend(vars.iter().cloned()); + let formula = self + .parse_formula_or_term()? + .into_formula() + .ok_or_else(|| ParseAttrError::unexpected_term("in exists formula"))?; + for (name, _) in &vars { + self.formula_existentials.remove(name); + } + Ok(FormulaOrTerm::Formula(chc::Formula::exists(vars, formula))) + } + _ => self.parse_binop_5(), + } + } + fn parse_formula_or_term(&mut self) -> Result> { - self.parse_binop_5() + self.parse_exists() + } + + fn parse_sort(&mut self) -> Result { + let tt = self.next_token_tree("sort")?.clone(); + match tt { + TokenTree::Token( + Token { + kind: TokenKind::Ident(sym, _), + .. + }, + _, + ) => { + let sort = match sym.as_str() { + "bool" => chc::Sort::bool(), + "int" => chc::Sort::int(), + "string" => unimplemented!(), + "null" => chc::Sort::null(), + "fn" => unimplemented!(), + _ => unimplemented!(), + }; + Ok(sort) + } + TokenTree::Delimited(_, _, Delimiter::Parenthesis, ts) => { + let mut parser = Parser { + resolver: self.boxed_resolver(), + cursor: ts.trees(), + formula_existentials: self.formula_existentials.clone(), + }; + let mut sorts = Vec::new(); + loop { + sorts.push(parser.parse_sort()?); + match parser.look_ahead_token(0) { + Some(Token { + kind: TokenKind::Comma, + .. + }) => { + parser.consume(); + } + None => break, + Some(t) => return Err(ParseAttrError::unexpected_token(",", t.clone())), + } + } + parser.end_of_input()?; + Ok(chc::Sort::tuple(sorts)) + } + t => Err(ParseAttrError::unexpected_token_tree("sort", t.clone())), + } } fn parse_ty(&mut self) -> Result> { @@ -662,6 +768,7 @@ where let mut parser = Parser { resolver: self.boxed_resolver(), cursor: ts.trees(), + formula_existentials: self.formula_existentials.clone(), }; let mut rtys = Vec::new(); loop { @@ -697,6 +804,7 @@ where let mut parser = Parser { resolver: self.boxed_resolver(), cursor: ts.trees(), + formula_existentials: self.formula_existentials.clone(), }; let self_ident = if matches!( parser.look_ahead_token(1), @@ -720,6 +828,7 @@ where let mut parser = Parser { resolver: RefinementResolver::new(self.boxed_resolver()), cursor: parser.cursor, + formula_existentials: self.formula_existentials.clone(), }; if let Some(self_ident) = self_ident { parser.resolver.set_self(self_ident, ty.to_sort()); @@ -859,6 +968,7 @@ where let mut parser = Parser { resolver: &self.resolver, cursor: ts.trees(), + formula_existentials: Default::default(), }; let rty = parser.parse_rty()?; parser.end_of_input()?; @@ -869,6 +979,7 @@ where let mut parser = Parser { resolver: &self.resolver, cursor: ts.trees(), + formula_existentials: Default::default(), }; let formula = parser.parse_annot_formula()?; parser.end_of_input()?; diff --git a/src/chc.rs b/src/chc.rs index 6f5db32..fbd301b 100644 --- a/src/chc.rs +++ b/src/chc.rs @@ -406,6 +406,8 @@ pub enum Term { TupleProj(Box>, usize), DatatypeCtor(DatatypeSort, DatatypeSymbol, Vec>), DatatypeDiscr(DatatypeSymbol, Box>), + /// Used in [`Formula`] to represent existentially quantified variables appearing in annotations. + FormulaExistentialVar(Sort, String), } impl<'a, 'b, D, V> Pretty<'a, D, termcolor::ColorSpec> for &'b Term @@ -475,6 +477,7 @@ where Term::DatatypeDiscr(_, t) => allocator .text("discriminant") .append(t.pretty(allocator).parens()), + Term::FormulaExistentialVar(_, name) => allocator.text(name.clone()), } } } @@ -521,6 +524,7 @@ impl Term { args.into_iter().map(|t| t.subst_var(&mut f)).collect(), ), Term::DatatypeDiscr(d_sym, t) => Term::DatatypeDiscr(d_sym, Box::new(t.subst_var(f))), + Term::FormulaExistentialVar(sort, name) => Term::FormulaExistentialVar(sort, name), } } @@ -562,15 +566,18 @@ impl Term { Term::TupleProj(t, i) => t.sort(var_sort).tuple_elem(*i), Term::DatatypeCtor(sort, _, _) => sort.clone().into(), Term::DatatypeDiscr(_, _) => Sort::int(), + Term::FormulaExistentialVar(sort, _) => sort.clone(), } } fn fv_impl(&self) -> Box + '_> { match self { Term::Var(v) => Box::new(std::iter::once(v)), - Term::Null | Term::Bool(_) | Term::Int(_) | Term::String(_) => { - Box::new(std::iter::empty()) - } + Term::Null + | Term::Bool(_) + | Term::Int(_) + | Term::String(_) + | Term::FormulaExistentialVar { .. } => Box::new(std::iter::empty()), Term::Box(t) => t.fv_impl(), Term::Mut(t1, t2) => Box::new(t1.fv_impl().chain(t2.fv_impl())), Term::BoxCurrent(t) => t.fv_impl(), @@ -1083,6 +1090,7 @@ pub enum Formula { Not(Box>), And(Vec>), Or(Vec>), + Exists(Vec<(String, Sort)>, Box>), } impl Default for Formula { @@ -1124,6 +1132,25 @@ where ); inner.group() } + Formula::Exists(vars, fo) => { + let vars = allocator.intersperse( + vars.iter().map(|(name, sort)| { + allocator + .text(name.clone()) + .append(allocator.text(":")) + .append(allocator.text(" ")) + .append(sort.pretty(allocator)) + }), + allocator.text(", ").append(allocator.line()), + ); + allocator + .text("∃") + .append(vars) + .append(allocator.text(".")) + .append(allocator.line()) + .append(fo.pretty(allocator).nest(2)) + .group() + } } } } @@ -1139,7 +1166,9 @@ impl Formula { D::Doc: Clone, { match self { - Formula::And(_) | Formula::Or(_) => self.pretty(allocator).parens(), + Formula::And(_) | Formula::Or(_) | Formula::Exists { .. } => { + self.pretty(allocator).parens() + } _ => self.pretty(allocator), } } @@ -1158,6 +1187,7 @@ impl Formula { Formula::Not(fo) => fo.is_bottom(), Formula::And(fs) => fs.iter().all(Formula::is_top), Formula::Or(fs) => fs.iter().any(Formula::is_top), + Formula::Exists(_, fo) => fo.is_top(), } } @@ -1167,6 +1197,7 @@ impl Formula { Formula::Not(fo) => fo.is_top(), Formula::And(fs) => fs.iter().any(Formula::is_bottom), Formula::Or(fs) => fs.iter().all(Formula::is_bottom), + Formula::Exists(_, fo) => fo.is_bottom(), } } @@ -1197,6 +1228,10 @@ impl Formula { } } + pub fn exists(vars: Vec<(String, Sort)>, body: Self) -> Self { + Formula::Exists(vars, Box::new(body)) + } + pub fn subst_var(self, f: F) -> Formula where F: FnMut(V) -> Term, @@ -1210,6 +1245,7 @@ impl Formula { Formula::And(fs.into_iter().map(|fo| fo.subst_var(&mut f)).collect()) } Formula::Or(fs) => Formula::Or(fs.into_iter().map(|fo| fo.subst_var(&mut f)).collect()), + Formula::Exists(vars, fo) => Formula::Exists(vars, Box::new(fo.subst_var(f))), } } @@ -1224,6 +1260,7 @@ impl Formula { Formula::Not(fo) => Formula::Not(Box::new(fo.map_var(&mut f))), Formula::And(fs) => Formula::And(fs.into_iter().map(|fo| fo.map_var(&mut f)).collect()), Formula::Or(fs) => Formula::Or(fs.into_iter().map(|fo| fo.map_var(&mut f)).collect()), + Formula::Exists(vars, fo) => Formula::Exists(vars, Box::new(fo.map_var(f))), } } @@ -1237,6 +1274,7 @@ impl Formula { Formula::Not(fo) => Box::new(fo.fv()), Formula::And(fs) => Box::new(fs.iter().flat_map(Formula::fv)), Formula::Or(fs) => Box::new(fs.iter().flat_map(Formula::fv)), + Formula::Exists(_, fo) => Box::new(fo.fv()), } } @@ -1250,6 +1288,7 @@ impl Formula { Formula::Not(fo) => Box::new(fo.iter_atoms()), Formula::And(fs) => Box::new(fs.iter().flat_map(Formula::iter_atoms)), Formula::Or(fs) => Box::new(fs.iter().flat_map(Formula::iter_atoms)), + Formula::Exists(_, fo) => Box::new(fo.iter_atoms()), } } @@ -1291,6 +1330,9 @@ impl Formula { *self = fs.pop().unwrap(); } } + Formula::Exists(_, fo) => { + fo.simplify(); + } } } } diff --git a/src/chc/format_context.rs b/src/chc/format_context.rs index ed82811..2123315 100644 --- a/src/chc/format_context.rs +++ b/src/chc/format_context.rs @@ -57,6 +57,7 @@ fn term_sorts(clause: &chc::Clause, t: &chc::Term, sorts: &mut BTreeSet term_sorts(clause, t, sorts), + chc::Term::FormulaExistentialVar(_, _) => {} } } diff --git a/src/chc/smtlib2.rs b/src/chc/smtlib2.rs index c708770..3cef75e 100644 --- a/src/chc/smtlib2.rs +++ b/src/chc/smtlib2.rs @@ -202,6 +202,7 @@ impl<'ctx, 'a> std::fmt::Display for Term<'ctx, 'a> { Term::new(self.ctx, self.clause, t) ) } + chc::Term::FormulaExistentialVar(_, name) => write!(f, "{}", name), } } } @@ -280,6 +281,14 @@ impl<'ctx, 'a> std::fmt::Display for Formula<'ctx, 'a> { let fs = List::open(fs.iter().map(|fo| Formula::new(self.ctx, self.clause, fo))); write!(f, "(or {})", fs) } + chc::Formula::Exists(vars, fo) => { + let vars = + List::closed(vars.iter().map(|(v, s)| { + List::closed([v.to_string(), self.ctx.fmt_sort(s).to_string()]) + })); + let fo = Formula::new(self.ctx, self.clause, fo); + write!(f, "(exists {vars} {fo})") + } } } } diff --git a/src/chc/unbox.rs b/src/chc/unbox.rs index 532f623..ffc4600 100644 --- a/src/chc/unbox.rs +++ b/src/chc/unbox.rs @@ -17,6 +17,9 @@ fn unbox_term(term: Term) -> Term { Term::DatatypeCtor(s1, s2, args.into_iter().map(unbox_term).collect()) } Term::DatatypeDiscr(sym, arg) => Term::DatatypeDiscr(sym, Box::new(unbox_term(*arg))), + Term::FormulaExistentialVar(sort, name) => { + Term::FormulaExistentialVar(unbox_sort(sort), name) + } } } @@ -52,6 +55,10 @@ fn unbox_formula(formula: Formula) -> Formula { Formula::Not(fo) => Formula::Not(Box::new(unbox_formula(*fo))), Formula::And(fs) => Formula::And(fs.into_iter().map(unbox_formula).collect()), Formula::Or(fs) => Formula::Or(fs.into_iter().map(unbox_formula).collect()), + Formula::Exists(vars, fo) => { + let vars = vars.into_iter().map(|(v, s)| (v, unbox_sort(s))).collect(); + Formula::Exists(vars, Box::new(unbox_formula(*fo))) + } } } diff --git a/tests/ui/fail/annot_exists.rs b/tests/ui/fail/annot_exists.rs new file mode 100644 index 0000000..888b2ec --- /dev/null +++ b/tests/ui/fail/annot_exists.rs @@ -0,0 +1,16 @@ +//@error-in-other-file: Unsat +//@compile-flags: -C debug-assertions=off +//@rustc-env: THRUST_SOLVER=thrust-pcsat-wrapper + +#[thrust::trusted] +#[thrust::callable] +fn rand() -> i32 { unimplemented!() } + +#[thrust::requires(true)] +#[thrust::ensures(exists x:int. result == 2 * x)] +fn f() -> i32 { + let x = rand(); + x + x + x +} + +fn main() {} diff --git a/tests/ui/pass/annot_exists.rs b/tests/ui/pass/annot_exists.rs new file mode 100644 index 0000000..95151e9 --- /dev/null +++ b/tests/ui/pass/annot_exists.rs @@ -0,0 +1,16 @@ +//@check-pass +//@compile-flags: -C debug-assertions=off +//@rustc-env: THRUST_SOLVER=thrust-pcsat-wrapper + +#[thrust::trusted] +#[thrust::callable] +fn rand() -> i32 { unimplemented!() } + +#[thrust::requires(true)] +#[thrust::ensures(exists x:int. result == 2 * x)] +fn f() -> i32 { + let x = rand(); + x + x +} + +fn main() {}