From b09e4fe17da7409a879ce3c14a8159aecdb29c15 Mon Sep 17 00:00:00 2001 From: coeff-aij <175928954+coeff-aij@users.noreply.github.com> Date: Thu, 25 Dec 2025 08:24:37 +0000 Subject: [PATCH 01/10] add: test for annotations of predicates --- tests/ui/pass/annot_preds.rs | 24 ++++++++++++++++++++++++ 1 file changed, 24 insertions(+) create mode 100644 tests/ui/pass/annot_preds.rs diff --git a/tests/ui/pass/annot_preds.rs b/tests/ui/pass/annot_preds.rs new file mode 100644 index 0000000..79bf978 --- /dev/null +++ b/tests/ui/pass/annot_preds.rs @@ -0,0 +1,24 @@ +//@check-pass +//@compile-flags: -Adead_code -C debug-assertions=off + +#[thrust::predicate] +fn is_double(x: i64, doubled_x: i64) -> bool { + x * 2 == doubled_x + // "(=( + // (* (x 2)) + // doubled_x + // ))" +} + +#[thrust::requires(true)] +#[thrust::ensures(result == 2 * x)] +// #[thrust::ensures(is_double(x, result))] +fn double(x: i64) -> i64 { + x + x +} + +fn main() { + let a = 3; + assert!(double(a) == 6); + assert!(is_double(a, double(a))); +} From e149696b55ad0e1c92aa4c1488a1b05d81ef5135 Mon Sep 17 00:00:00 2001 From: coeff-aij <175928954+coeff-aij@users.noreply.github.com> Date: Fri, 23 Jan 2026 10:51:35 +0000 Subject: [PATCH 02/10] add: definitions to check if functions are marked as predicates --- src/analyze/annot.rs | 4 ++++ src/analyze/local_def.rs | 10 ++++++++++ 2 files changed, 14 insertions(+) diff --git a/src/analyze/annot.rs b/src/analyze/annot.rs index 1d7658e..b884b31 100644 --- a/src/analyze/annot.rs +++ b/src/analyze/annot.rs @@ -41,6 +41,10 @@ pub fn raw_command_path() -> [Symbol; 2] { [Symbol::intern("thrust"), Symbol::intern("raw_command")] } +pub fn predicate_path() -> [Symbol; 2] { + [Symbol::intern("thrust"), Symbol::intern("predicate")] +} + /// A [`annot::Resolver`] implementation for resolving function parameters. /// /// The parameter names and their sorts needs to be configured via diff --git a/src/analyze/local_def.rs b/src/analyze/local_def.rs index d556ef0..7ac4b0d 100644 --- a/src/analyze/local_def.rs +++ b/src/analyze/local_def.rs @@ -135,6 +135,16 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { .next() .is_some() } + + pub fn is_annotated_as_predicate(&self) -> bool { + self.tcx + .get_attrs_by_path( + self.local_def_id.to_def_id(), + &analyze::annot::predicate_path(), + ) + .next() + .is_some() + } // TODO: unify this logic with extraction functions above pub fn is_fully_annotated(&self) -> bool { From 07154d8b376a1a6dc936459e8b4f1dc770c2e5aa Mon Sep 17 00:00:00 2001 From: coeff-aij <175928954+coeff-aij@users.noreply.github.com> Date: Mon, 12 Jan 2026 16:16:11 +0900 Subject: [PATCH 03/10] add: gather functions marked as predicates into Analyzer::predicates --- src/analyze/crate_.rs | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/src/analyze/crate_.rs b/src/analyze/crate_.rs index bd1d87b..2255c21 100644 --- a/src/analyze/crate_.rs +++ b/src/analyze/crate_.rs @@ -24,6 +24,7 @@ pub struct Analyzer<'tcx, 'ctx> { tcx: TyCtxt<'tcx>, ctx: &'ctx mut analyze::Analyzer<'tcx>, trusted: HashSet, + predicates: HashSet, } impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { @@ -82,6 +83,10 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { self.trusted.insert(local_def_id.to_def_id()); } + if analyzer.is_annotated_as_predicate() { + self.predicates.insert(local_def_id.to_def_id()); + } + use mir_ty::TypeVisitableExt as _; if sig.has_param() && !analyzer.is_fully_annotated() { self.ctx.register_deferred_def(local_def_id.to_def_id()); @@ -212,7 +217,8 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { pub fn new(ctx: &'ctx mut analyze::Analyzer<'tcx>) -> Self { let tcx = ctx.tcx; let trusted = HashSet::default(); - Self { ctx, tcx, trusted } + let predicates = HashSet::default(); + Self { ctx, tcx, trusted, predicates } } pub fn run(&mut self) { From 9dee274741a59bb228a121cb45d6eef0e2d83780 Mon Sep 17 00:00:00 2001 From: coeff-aij <175928954+coeff-aij@users.noreply.github.com> Date: Sun, 4 Jan 2026 20:41:42 +0900 Subject: [PATCH 04/10] add: logging for found predicates --- src/analyze/crate_.rs | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/analyze/crate_.rs b/src/analyze/crate_.rs index 2255c21..4c149b1 100644 --- a/src/analyze/crate_.rs +++ b/src/analyze/crate_.rs @@ -110,6 +110,11 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { tracing::info!(?local_def_id, "trusted"); continue; } + if self.predicates.contains_key(&local_def_id.to_def_id()) { + let sig = self.predicates.get(&local_def_id.to_def_id()).unwrap(); + tracing::info!(?local_def_id, ?sig, "predicate"); + continue; + } let Some(expected) = self.ctx.concrete_def_ty(local_def_id.to_def_id()) else { // when the local_def_id is deferred it would be skipped continue; From 52046b21b384de296dc43d871cae3309248906ed Mon Sep 17 00:00:00 2001 From: coeff-aij <175928954+coeff-aij@users.noreply.github.com> Date: Fri, 23 Jan 2026 09:45:52 +0000 Subject: [PATCH 05/10] add: UserDefinedPredDefs in chc::System --- src/chc.rs | 20 ++++++++++++++++++++ 1 file changed, 20 insertions(+) diff --git a/src/chc.rs b/src/chc.rs index e9741bb..60b5a28 100644 --- a/src/chc.rs +++ b/src/chc.rs @@ -1700,11 +1700,21 @@ pub struct PredVarDef { pub debug_info: DebugInfo, } +pub type UserDefinedPredSig = Vec<(String, Sort)>; + +#[derive(Debug, Clone)] +pub struct UserDefinedPredDef { + symbol: UserDefinedPred, + sig: UserDefinedPredSig, + body: RawCommand, +} + /// A CHC system. #[derive(Debug, Clone, Default)] pub struct System { pub raw_commands: Vec, pub datatypes: Vec, + pub user_defined_pred_defs: Vec, pub clauses: IndexVec, pub pred_vars: IndexVec, } @@ -1718,6 +1728,16 @@ impl System { self.raw_commands.push(raw_command) } + pub fn push_pred_define( + &mut self, + symbol: UserDefinedPred, + sig: UserDefinedPredSig, + body: RawCommand, + ) { + self.user_defined_pred_defs + .push(UserDefinedPredDef { symbol, sig, body }) + } + pub fn push_clause(&mut self, clause: Clause) -> Option { if clause.is_nop() { return None; From 5e06c95977a8f6c601748985aa6beefb8be1dcc5 Mon Sep 17 00:00:00 2001 From: coeff-aij <175928954+coeff-aij@users.noreply.github.com> Date: Fri, 23 Jan 2026 10:55:22 +0000 Subject: [PATCH 06/10] add: parse `#[thrust::predicate]` and register user-defined predicate definitions --- src/analyze/crate_.rs | 13 +++++--- src/analyze/local_def.rs | 66 +++++++++++++++++++++++++++++++++++++++- 2 files changed, 74 insertions(+), 5 deletions(-) diff --git a/src/analyze/crate_.rs b/src/analyze/crate_.rs index 4c149b1..cdbc721 100644 --- a/src/analyze/crate_.rs +++ b/src/analyze/crate_.rs @@ -85,6 +85,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { if analyzer.is_annotated_as_predicate() { self.predicates.insert(local_def_id.to_def_id()); + analyzer.analyze_predicate_definition(local_def_id); } use mir_ty::TypeVisitableExt as _; @@ -110,9 +111,8 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { tracing::info!(?local_def_id, "trusted"); continue; } - if self.predicates.contains_key(&local_def_id.to_def_id()) { - let sig = self.predicates.get(&local_def_id.to_def_id()).unwrap(); - tracing::info!(?local_def_id, ?sig, "predicate"); + if self.predicates.contains(&local_def_id.to_def_id()) { + tracing::info!(?local_def_id, "predicate"); continue; } let Some(expected) = self.ctx.concrete_def_ty(local_def_id.to_def_id()) else { @@ -223,7 +223,12 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { let tcx = ctx.tcx; let trusted = HashSet::default(); let predicates = HashSet::default(); - Self { ctx, tcx, trusted, predicates } + Self { + ctx, + tcx, + trusted, + predicates, + } } pub fn run(&mut self) { diff --git a/src/analyze/local_def.rs b/src/analyze/local_def.rs index 7ac4b0d..45c89bc 100644 --- a/src/analyze/local_def.rs +++ b/src/analyze/local_def.rs @@ -16,6 +16,27 @@ use crate::pretty::PrettyDisplayExt as _; use crate::refine::{BasicBlockType, TypeBuilder}; use crate::rty; +fn stmt_str_literal(stmt: &rustc_hir::Stmt) -> Option { + use rustc_ast::LitKind; + use rustc_hir::{Expr, ExprKind, Stmt, StmtKind}; + + match stmt { + Stmt { + kind: + StmtKind::Semi(Expr { + kind: + ExprKind::Lit(rustc_hir::Lit { + node: LitKind::Str(symbol, _), + .. + }), + .. + }), + .. + } => Some(symbol.to_string()), + _ => None, + } +} + /// An implementation of the typing of local definitions. /// /// The current implementation only applies to function definitions. The entry point is @@ -106,6 +127,49 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { ret_annot } + pub fn analyze_predicate_definition(&self, local_def_id: LocalDefId) { + let pred_name = self.tcx.item_name(local_def_id.to_def_id()).to_string(); + + // function's body + use rustc_hir::{Block, Expr, ExprKind}; + + let hir_map = self.tcx.hir(); + let body_id = hir_map.maybe_body_owned_by(local_def_id).unwrap(); + let hir_body = hir_map.body(body_id); + + let command = match hir_body.value { + Expr { + kind: ExprKind::Block(Block { stmts, .. }, _), + .. + } => stmts + .iter() + .find_map(stmt_str_literal) + .expect("invalid predicate definition: no string literal was found."), + _ => panic!("expected function body, got: {hir_body:?}"), + }; + + // names and sorts of arguments + let arg_names = self + .tcx + .fn_arg_names(local_def_id.to_def_id()) + .iter() + .map(|ident| ident.to_string()); + + let sig = self.ctx.local_fn_sig(local_def_id); + let arg_sorts = sig + .inputs() + .iter() + .map(|input_ty| self.type_builder.build(*input_ty).to_sort()); + + let arg_name_and_sorts = arg_names.into_iter().zip(arg_sorts).collect::>(); + + self.ctx.system.borrow_mut().push_pred_define( + chc::UserDefinedPred::new(pred_name), + chc::UserDefinedPredSig::from(arg_name_and_sorts), + chc::RawCommand { command }, + ); + } + pub fn is_annotated_as_trusted(&self) -> bool { self.tcx .get_attrs_by_path( @@ -135,7 +199,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { .next() .is_some() } - + pub fn is_annotated_as_predicate(&self) -> bool { self.tcx .get_attrs_by_path( From 125b56e37d6ac07e012ea2a427895d9b4c2658e2 Mon Sep 17 00:00:00 2001 From: coeff-aij <175928954+coeff-aij@users.noreply.github.com> Date: Fri, 23 Jan 2026 09:48:25 +0000 Subject: [PATCH 07/10] add: format `UserDefinedPredDef` in SMT-LIB2 --- src/chc/smtlib2.rs | 35 +++++++++++++++++++++++++++++++++++ src/chc/unbox.rs | 23 +++++++++++++++++++---- 2 files changed, 54 insertions(+), 4 deletions(-) diff --git a/src/chc/smtlib2.rs b/src/chc/smtlib2.rs index 1fb7319..193b013 100644 --- a/src/chc/smtlib2.rs +++ b/src/chc/smtlib2.rs @@ -562,6 +562,33 @@ impl<'ctx, 'a> MatcherPredFun<'ctx, 'a> { } } +pub struct UserDefinedPredDef<'ctx, 'a> { + ctx: &'ctx FormatContext, + inner: &'a chc::UserDefinedPredDef, +} + +impl<'ctx, 'a> std::fmt::Display for UserDefinedPredDef<'ctx, 'a> { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + let params = List::closed( + self.inner + .sig + .iter() + .map(|(name, sort)| format!("({} {})", name, self.ctx.fmt_sort(sort))), + ); + write!( + f, + "(define-fun {name} {params} Bool {body})", + name = self.inner.symbol, + body = RawCommand::new(&self.inner.body), + ) + } +} + +impl<'ctx, 'a> UserDefinedPredDef<'ctx, 'a> { + pub fn new(ctx: &'ctx FormatContext, inner: &'a chc::UserDefinedPredDef) -> Self { + Self { ctx, inner } + } +} /// A wrapper around a [`chc::System`] that provides a [`std::fmt::Display`] implementation in SMT-LIB2 format. #[derive(Debug, Clone)] pub struct System<'a> { @@ -578,6 +605,14 @@ impl<'a> std::fmt::Display for System<'a> { writeln!(f, "{}\n", RawCommand::new(raw_command))?; } + for user_defined_pred_def in &self.inner.user_defined_pred_defs { + writeln!( + f, + "{}\n", + UserDefinedPredDef::new(&self.ctx, user_defined_pred_def) + )?; + } + writeln!(f, "{}\n", Datatypes::new(&self.ctx, self.ctx.datatypes()))?; for datatype in self.ctx.datatypes() { writeln!(f, "{}", DatatypeDiscrFun::new(&self.ctx, datatype))?; diff --git a/src/chc/unbox.rs b/src/chc/unbox.rs index 30ea31c..cb5ce8f 100644 --- a/src/chc/unbox.rs +++ b/src/chc/unbox.rs @@ -152,6 +152,15 @@ fn unbox_datatype(datatype: Datatype) -> Datatype { } } +fn unbox_user_defined_pred_def(user_defined_pred_def: UserDefinedPredDef) -> UserDefinedPredDef { + let UserDefinedPredDef { symbol, sig, body } = user_defined_pred_def; + let sig = sig + .into_iter() + .map(|(name, sort)| (name, unbox_sort(sort))) + .collect(); + UserDefinedPredDef { symbol, sig, body } +} + /// Remove all `Box` sorts and `Box`/`BoxCurrent` terms from the system. /// /// The box values in Thrust represent an owned pointer, but are logically equivalent to the inner type. @@ -159,18 +168,24 @@ fn unbox_datatype(datatype: Datatype) -> Datatype { /// This function traverses a [`System`] and removes all `Box` related constructs. pub fn unbox(system: System) -> System { let System { + raw_commands, + datatypes, + user_defined_pred_defs, clauses, pred_vars, - datatypes, - raw_commands, } = system; let datatypes = datatypes.into_iter().map(unbox_datatype).collect(); let clauses = clauses.into_iter().map(unbox_clause).collect(); let pred_vars = pred_vars.into_iter().map(unbox_pred_var_def).collect(); + let user_defined_pred_defs = user_defined_pred_defs + .into_iter() + .map(unbox_user_defined_pred_def) + .collect(); System { + raw_commands, + datatypes, + user_defined_pred_defs, clauses, pred_vars, - datatypes, - raw_commands, } } From 3a2e20b77e48f81a60fcfc5c37146d1bdba26080 Mon Sep 17 00:00:00 2001 From: coeff-aij <175928954+coeff-aij@users.noreply.github.com> Date: Fri, 23 Jan 2026 09:49:42 +0000 Subject: [PATCH 08/10] fix: test for `#[thrust::predicate]` --- tests/ui/pass/annot_preds.rs | 13 +++++-------- 1 file changed, 5 insertions(+), 8 deletions(-) diff --git a/tests/ui/pass/annot_preds.rs b/tests/ui/pass/annot_preds.rs index 79bf978..9fa5bec 100644 --- a/tests/ui/pass/annot_preds.rs +++ b/tests/ui/pass/annot_preds.rs @@ -3,16 +3,14 @@ #[thrust::predicate] fn is_double(x: i64, doubled_x: i64) -> bool { - x * 2 == doubled_x - // "(=( - // (* (x 2)) - // doubled_x - // ))" + "(= + (* x 2) + doubled_x + )"; true } #[thrust::requires(true)] -#[thrust::ensures(result == 2 * x)] -// #[thrust::ensures(is_double(x, result))] +#[thrust::ensures(is_double(x, result))] fn double(x: i64) -> i64 { x + x } @@ -20,5 +18,4 @@ fn double(x: i64) -> i64 { fn main() { let a = 3; assert!(double(a) == 6); - assert!(is_double(a, double(a))); } From 0735236247ba2dce0a36b84513426d4dceb388df Mon Sep 17 00:00:00 2001 From: coeff-aij <175928954+coeff-aij@users.noreply.github.com> Date: Sat, 24 Jan 2026 00:47:35 +0900 Subject: [PATCH 09/10] fix: use String for predicate body --- src/analyze/local_def.rs | 4 ++-- src/chc.rs | 4 ++-- src/chc/smtlib2.rs | 2 +- 3 files changed, 5 insertions(+), 5 deletions(-) diff --git a/src/analyze/local_def.rs b/src/analyze/local_def.rs index 45c89bc..a4bfd64 100644 --- a/src/analyze/local_def.rs +++ b/src/analyze/local_def.rs @@ -137,7 +137,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { let body_id = hir_map.maybe_body_owned_by(local_def_id).unwrap(); let hir_body = hir_map.body(body_id); - let command = match hir_body.value { + let predicate_body = match hir_body.value { Expr { kind: ExprKind::Block(Block { stmts, .. }, _), .. @@ -166,7 +166,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { self.ctx.system.borrow_mut().push_pred_define( chc::UserDefinedPred::new(pred_name), chc::UserDefinedPredSig::from(arg_name_and_sorts), - chc::RawCommand { command }, + predicate_body, ); } diff --git a/src/chc.rs b/src/chc.rs index 60b5a28..3c72b5c 100644 --- a/src/chc.rs +++ b/src/chc.rs @@ -1706,7 +1706,7 @@ pub type UserDefinedPredSig = Vec<(String, Sort)>; pub struct UserDefinedPredDef { symbol: UserDefinedPred, sig: UserDefinedPredSig, - body: RawCommand, + body: String, } /// A CHC system. @@ -1732,7 +1732,7 @@ impl System { &mut self, symbol: UserDefinedPred, sig: UserDefinedPredSig, - body: RawCommand, + body: String, ) { self.user_defined_pred_defs .push(UserDefinedPredDef { symbol, sig, body }) diff --git a/src/chc/smtlib2.rs b/src/chc/smtlib2.rs index 193b013..e6585ac 100644 --- a/src/chc/smtlib2.rs +++ b/src/chc/smtlib2.rs @@ -579,7 +579,7 @@ impl<'ctx, 'a> std::fmt::Display for UserDefinedPredDef<'ctx, 'a> { f, "(define-fun {name} {params} Bool {body})", name = self.inner.symbol, - body = RawCommand::new(&self.inner.body), + body = &self.inner.body, ) } } From 1e495d0da548394b9edfdd6744f4eec03950cc4f Mon Sep 17 00:00:00 2001 From: coeff-aij <175928954+coeff-aij@users.noreply.github.com> Date: Mon, 26 Jan 2026 11:57:44 +0000 Subject: [PATCH 10/10] fix: insert raw commands and user-defined predicates before datatype defintions in .smt2 file --- src/chc/smtlib2.rs | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) diff --git a/src/chc/smtlib2.rs b/src/chc/smtlib2.rs index e6585ac..e8886ed 100644 --- a/src/chc/smtlib2.rs +++ b/src/chc/smtlib2.rs @@ -600,6 +600,12 @@ impl<'a> std::fmt::Display for System<'a> { fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { writeln!(f, "(set-logic HORN)\n")?; + writeln!(f, "{}\n", Datatypes::new(&self.ctx, self.ctx.datatypes()))?; + for datatype in self.ctx.datatypes() { + writeln!(f, "{}", DatatypeDiscrFun::new(&self.ctx, datatype))?; + writeln!(f, "{}", MatcherPredFun::new(&self.ctx, datatype))?; + } + // insert command from #![thrust::raw_command()] here for raw_command in &self.inner.raw_commands { writeln!(f, "{}\n", RawCommand::new(raw_command))?; @@ -613,11 +619,6 @@ impl<'a> std::fmt::Display for System<'a> { )?; } - writeln!(f, "{}\n", Datatypes::new(&self.ctx, self.ctx.datatypes()))?; - for datatype in self.ctx.datatypes() { - writeln!(f, "{}", DatatypeDiscrFun::new(&self.ctx, datatype))?; - writeln!(f, "{}", MatcherPredFun::new(&self.ctx, datatype))?; - } writeln!(f)?; for (p, def) in self.inner.pred_vars.iter_enumerated() { if !def.debug_info.is_empty() {