From fbed2dc368eebccf08c2a30f870bdb19cb047257 Mon Sep 17 00:00:00 2001 From: coeff-aij <175928954+coeff-aij@users.noreply.github.com> Date: Fri, 9 Jan 2026 13:08:23 +0000 Subject: [PATCH 01/11] add: test for raw_define attribute --- tests/ui/pass/annot_raw_define.rs | 24 ++++++++++++++++++++++++ 1 file changed, 24 insertions(+) create mode 100644 tests/ui/pass/annot_raw_define.rs diff --git a/tests/ui/pass/annot_raw_define.rs b/tests/ui/pass/annot_raw_define.rs new file mode 100644 index 0000000..ed8ee54 --- /dev/null +++ b/tests/ui/pass/annot_raw_define.rs @@ -0,0 +1,24 @@ +//@check-pass +//@compile-flags: -Adead_code -C debug-assertions=off + +// Insert definitions written in SMT-LIB2 format into .smt file directly. +// This feature is intended for debug or experiment purpose. +#![thrust::raw_define("(define-fun is_double ((x Int) (doubled_x Int)) Bool + (=( + (* (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 a0863f108ccbb9a2dffa9bd85a4428540fade296 Mon Sep 17 00:00:00 2001 From: coeff-aij <175928954+coeff-aij@users.noreply.github.com> Date: Sat, 10 Jan 2026 07:42:25 +0000 Subject: [PATCH 02/11] add: RawDefinition for System --- src/chc.rs | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/src/chc.rs b/src/chc.rs index 5543de4..eefdc4f 100644 --- a/src/chc.rs +++ b/src/chc.rs @@ -1606,6 +1606,14 @@ impl Clause { } } +/// A definition specified using #![thrust::define_raw()] +/// +/// Those will be directly inserted into the generated SMT-LIB2 file. +#[derive(Debug, Clone)] +pub struct RawDefinition { + pub definition: String, +} + /// A selector for a datatype constructor. /// /// A selector is a function that extracts a field from a datatype value. @@ -1655,6 +1663,7 @@ pub struct PredVarDef { /// A CHC system. #[derive(Debug, Clone, Default)] pub struct System { + pub raw_definitions: Vec, pub datatypes: Vec, pub clauses: IndexVec, pub pred_vars: IndexVec, @@ -1665,6 +1674,10 @@ impl System { self.pred_vars.push(PredVarDef { sig, debug_info }) } + pub fn push_raw_definition(&mut self, raw_definition: RawDefinition) { + self.raw_definitions.push(raw_definition) + } + pub fn push_clause(&mut self, clause: Clause) -> Option { if clause.is_nop() { return None; From 3f3740d8ba240673081cc705b96bd3eeea034528 Mon Sep 17 00:00:00 2001 From: coeff-aij <175928954+coeff-aij@users.noreply.github.com> Date: Sat, 10 Jan 2026 07:43:18 +0000 Subject: [PATCH 03/11] add: formatting for RawDefinition --- src/chc/format_context.rs | 8 +++++++- src/chc/smtlib2.rs | 29 +++++++++++++++++++++++++++++ 2 files changed, 36 insertions(+), 1 deletion(-) diff --git a/src/chc/format_context.rs b/src/chc/format_context.rs index 2123315..1c75215 100644 --- a/src/chc/format_context.rs +++ b/src/chc/format_context.rs @@ -21,6 +21,7 @@ use crate::chc::{self, hoice::HoiceDatatypeRenamer}; pub struct FormatContext { renamer: HoiceDatatypeRenamer, datatypes: Vec, + raw_definitions: Vec, } // FIXME: this is obviously ineffective and should be replaced @@ -273,13 +274,18 @@ impl FormatContext { .filter(|d| d.params == 0) .collect(); let renamer = HoiceDatatypeRenamer::new(&datatypes); - FormatContext { renamer, datatypes } + let raw_definitions = system.raw_definitions.clone(); + FormatContext { renamer, datatypes, raw_definitions } } pub fn datatypes(&self) -> &[chc::Datatype] { &self.datatypes } + pub fn raw_definitions(&self) -> &[chc::RawDefinition] { + &self.raw_definitions + } + pub fn box_ctor(&self, sort: &chc::Sort) -> impl std::fmt::Display { let ss = Sort::new(sort).sorts(); format!("box{ss}") diff --git a/src/chc/smtlib2.rs b/src/chc/smtlib2.rs index 167d108..0e0f2e9 100644 --- a/src/chc/smtlib2.rs +++ b/src/chc/smtlib2.rs @@ -370,6 +370,30 @@ impl<'ctx, 'a> Clause<'ctx, 'a> { } } +/// A wrapper around a [`chc::RawDefinition`] that provides a [`std::fmt::Display`] implementation in SMT-LIB2 format. +#[derive(Debug, Clone)] +pub struct RawDefinition<'a> { + inner: &'a chc::RawDefinition, +} + +impl<'a> std::fmt::Display for RawDefinition<'a> { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + write!( + f, + "{}", + self.inner.definition, + ) + } +} + +impl<'a> RawDefinition<'a> { + pub fn new(inner: &'a chc::RawDefinition) -> Self { + Self { + inner + } + } +} + /// A wrapper around a [`chc::DatatypeSelector`] that provides a [`std::fmt::Display`] implementation in SMT-LIB2 format. #[derive(Debug, Clone)] pub struct DatatypeSelector<'ctx, 'a> { @@ -555,6 +579,11 @@ 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")?; + // insert definition from #![thrust::define_chc()] here + for raw_def in self.ctx.raw_definitions() { + writeln!(f, "{}\n", RawDefinition::new(raw_def))?; + } + writeln!(f, "{}\n", Datatypes::new(&self.ctx, self.ctx.datatypes()))?; for datatype in self.ctx.datatypes() { writeln!(f, "{}", DatatypeDiscrFun::new(&self.ctx, datatype))?; From 155dc278470a9c19c12eedc6569782c3919a3732 Mon Sep 17 00:00:00 2001 From: coeff-aij <175928954+coeff-aij@users.noreply.github.com> Date: Sun, 11 Jan 2026 16:07:25 +0000 Subject: [PATCH 04/11] add: raw_define path --- src/analyze/annot.rs | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/analyze/annot.rs b/src/analyze/annot.rs index 2dbb9ea..30e70d3 100644 --- a/src/analyze/annot.rs +++ b/src/analyze/annot.rs @@ -37,6 +37,10 @@ pub fn extern_spec_fn_path() -> [Symbol; 2] { [Symbol::intern("thrust"), Symbol::intern("extern_spec_fn")] } +pub fn raw_define_path() -> [Symbol; 2] { + [Symbol::intern("thrust"), Symbol::intern("raw_define")] +} + /// A [`annot::Resolver`] implementation for resolving function parameters. /// /// The parameter names and their sorts needs to be configured via From be16c1fdec72957aa9632e2bc29482a062e06c23 Mon Sep 17 00:00:00 2001 From: coeff-aij <175928954+coeff-aij@users.noreply.github.com> Date: Sun, 11 Jan 2026 16:07:50 +0000 Subject: [PATCH 05/11] add: parse raw definitions --- src/annot.rs | 39 ++++++++++++++++++++++++++++++++++++++- 1 file changed, 38 insertions(+), 1 deletion(-) diff --git a/src/annot.rs b/src/annot.rs index 128c289..6541fee 100644 --- a/src/annot.rs +++ b/src/annot.rs @@ -8,7 +8,7 @@ //! The main entry point is [`AnnotParser`], which parses a [`TokenStream`] into a //! [`rty::RefinedType`] or a [`chc::Formula`]. -use rustc_ast::token::{BinOpToken, Delimiter, LitKind, Token, TokenKind}; +use rustc_ast::token::{BinOpToken, Delimiter, LitKind, Lit, Token, TokenKind}; use rustc_ast::tokenstream::{RefTokenTreeCursor, Spacing, TokenStream, TokenTree}; use rustc_index::IndexVec; use rustc_span::symbol::Ident; @@ -1076,6 +1076,32 @@ where .ok_or_else(|| ParseAttrError::unexpected_term("in annotation"))?; Ok(AnnotFormula::Formula(formula)) } + + pub fn parse_annot_raw_definition(&mut self) -> Result { + let t = self.next_token("raw CHC definition")?; + + match t { + Token { + kind: TokenKind::Literal( + Lit { kind, symbol, .. } + ), + .. + } => { + match kind { + LitKind::Str => { + let definition = symbol.to_string(); + Ok(chc::RawDefinition{ definition }) + }, + _ => Err(ParseAttrError::unexpected_token( + "string literal", t.clone() + )) + } + }, + _ => Err(ParseAttrError::unexpected_token( + "string literal", t.clone() + )) + } + } } /// A [`Resolver`] implementation for resolving specific variable as [`rty::RefinedTypeVar::Value`]. @@ -1208,4 +1234,15 @@ where parser.end_of_input()?; Ok(formula) } + + pub fn parse_raw_definition(&self, ts: TokenStream) -> Result { + let mut parser = Parser { + resolver: &self.resolver, + cursor: ts.trees(), + formula_existentials: Default::default(), + }; + let raw_definition = parser.parse_annot_raw_definition()?; + parser.end_of_input()?; + Ok(raw_definition) + } } From e050fc3b4d17dc703d3fedae8607f3d0d9e49964 Mon Sep 17 00:00:00 2001 From: coeff-aij <175928954+coeff-aij@users.noreply.github.com> Date: Sun, 11 Jan 2026 16:45:20 +0000 Subject: [PATCH 06/11] fix: invalid SMT-LIB2 format --- tests/ui/pass/annot_raw_define.rs | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/tests/ui/pass/annot_raw_define.rs b/tests/ui/pass/annot_raw_define.rs index ed8ee54..c1c47a7 100644 --- a/tests/ui/pass/annot_raw_define.rs +++ b/tests/ui/pass/annot_raw_define.rs @@ -3,11 +3,12 @@ // Insert definitions written in SMT-LIB2 format into .smt file directly. // This feature is intended for debug or experiment purpose. +#![feature(custom_inner_attributes)] #![thrust::raw_define("(define-fun is_double ((x Int) (doubled_x Int)) Bool - (=( - (* (x 2)) + (= + (* x 2) doubled_x - )) + ) )")] #[thrust::requires(true)] @@ -20,5 +21,5 @@ fn double(x: i64) -> i64 { fn main() { let a = 3; assert!(double(a) == 6); - assert!(is_double(a, double(a))); + // assert!(is_double(a, double(a))); } From 547dd7865dffd8b6d44f5c670cf10e46b9b77821 Mon Sep 17 00:00:00 2001 From: coeff-aij <175928954+coeff-aij@users.noreply.github.com> Date: Sun, 11 Jan 2026 16:46:15 +0000 Subject: [PATCH 07/11] add: analyze inner-attribute #[raw_define()] for the given crate --- src/analyze/crate_.rs | 28 ++++++++++++++++++++++++++++ 1 file changed, 28 insertions(+) diff --git a/src/analyze/crate_.rs b/src/analyze/crate_.rs index 9dd85f9..c71021e 100644 --- a/src/analyze/crate_.rs +++ b/src/analyze/crate_.rs @@ -2,12 +2,14 @@ use std::collections::HashSet; +use rustc_hir::def_id::CRATE_DEF_ID; use rustc_middle::ty::{self as mir_ty, TyCtxt}; use rustc_span::def_id::{DefId, LocalDefId}; use crate::analyze; use crate::chc; use crate::rty::{self, ClauseBuilderExt as _}; +use crate::annot; /// An implementation of local crate analysis. /// @@ -26,6 +28,31 @@ pub struct Analyzer<'tcx, 'ctx> { } impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { + // fn is_annotated_as_raw_define(&self) -> bool { + // self.tcx + // .get_attrs_by_path( + // CRATE_DEF_ID.to_def_id(), + // &analyze::annot::raw_define_path(), + // ) + // .next() + // .is_some() + // } + + fn analyze_raw_define_annot(&mut self) { + for attrs in self.tcx.get_attrs_by_path( + CRATE_DEF_ID.to_def_id(), + &analyze::annot::raw_define_path(), + ) { + let ts = analyze::annot::extract_annot_tokens(attrs.clone()); + let parser = annot::AnnotParser::new( + // TODO: this resolver is not actually used. + analyze::annot::ParamResolver::default() + ); + let raw_definition = parser.parse_raw_definition(ts).unwrap(); + self.ctx.system.borrow_mut().push_raw_definition(raw_definition); + } + } + fn refine_local_defs(&mut self) { for local_def_id in self.tcx.mir_keys(()) { if self.tcx.def_kind(*local_def_id).is_fn_like() { @@ -187,6 +214,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { let span = tracing::debug_span!("crate", krate = %self.tcx.crate_name(rustc_span::def_id::LOCAL_CRATE)); let _guard = span.enter(); + self.analyze_raw_define_annot(); self.refine_local_defs(); self.analyze_local_defs(); self.assert_callable_entry(); From 2529cdb70b4300e03087fd9e78697d45ecb95e40 Mon Sep 17 00:00:00 2001 From: coeff-aij <175928954+coeff-aij@users.noreply.github.com> Date: Sun, 11 Jan 2026 16:48:01 +0000 Subject: [PATCH 08/11] fix: error relate to new raw_definitions field of System --- src/chc/unbox.rs | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/chc/unbox.rs b/src/chc/unbox.rs index 5be1240..40c2e6a 100644 --- a/src/chc/unbox.rs +++ b/src/chc/unbox.rs @@ -161,6 +161,7 @@ pub fn unbox(system: System) -> System { clauses, pred_vars, datatypes, + raw_definitions, } = system; let datatypes = datatypes.into_iter().map(unbox_datatype).collect(); let clauses = clauses.into_iter().map(unbox_clause).collect(); @@ -169,5 +170,6 @@ pub fn unbox(system: System) -> System { clauses, pred_vars, datatypes, + raw_definitions, } } From afcd68c4121f82812bd320562736ed6041c665dd Mon Sep 17 00:00:00 2001 From: coeff-aij <175928954+coeff-aij@users.noreply.github.com> Date: Mon, 12 Jan 2026 02:16:41 +0900 Subject: [PATCH 09/11] remove: unused code --- src/analyze/crate_.rs | 10 ---------- 1 file changed, 10 deletions(-) diff --git a/src/analyze/crate_.rs b/src/analyze/crate_.rs index c71021e..4172f94 100644 --- a/src/analyze/crate_.rs +++ b/src/analyze/crate_.rs @@ -28,16 +28,6 @@ pub struct Analyzer<'tcx, 'ctx> { } impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { - // fn is_annotated_as_raw_define(&self) -> bool { - // self.tcx - // .get_attrs_by_path( - // CRATE_DEF_ID.to_def_id(), - // &analyze::annot::raw_define_path(), - // ) - // .next() - // .is_some() - // } - fn analyze_raw_define_annot(&mut self) { for attrs in self.tcx.get_attrs_by_path( CRATE_DEF_ID.to_def_id(), From b222ede1f5bfb153c15e636a93538a7a879a811e Mon Sep 17 00:00:00 2001 From: coeff-aij <175928954+coeff-aij@users.noreply.github.com> Date: Mon, 12 Jan 2026 05:43:54 +0000 Subject: [PATCH 10/11] add: positiive test for multiple raw_define annotations --- tests/ui/pass/annot_raw_define_multi.rs | 33 +++++++++++++++++++++++++ 1 file changed, 33 insertions(+) create mode 100644 tests/ui/pass/annot_raw_define_multi.rs diff --git a/tests/ui/pass/annot_raw_define_multi.rs b/tests/ui/pass/annot_raw_define_multi.rs new file mode 100644 index 0000000..ae9e0eb --- /dev/null +++ b/tests/ui/pass/annot_raw_define_multi.rs @@ -0,0 +1,33 @@ +//@check-pass +//@compile-flags: -Adead_code -C debug-assertions=off + +// Insert definitions written in SMT-LIB2 format into .smt file directly. +// This feature is intended for debug or experiment purpose. +#![feature(custom_inner_attributes)] +#![thrust::raw_define("(define-fun is_double ((x Int) (doubled_x Int)) Bool + (= + (* x 2) + doubled_x + ) +)")] + +// multiple raw definitions can be inserted. +#![thrust::raw_define("(define-fun is_triple ((x Int) (tripled_x Int)) Bool + (= + (* x 3) + tripled_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 44a97dabc25670d45361e44ab41fae6391496b42 Mon Sep 17 00:00:00 2001 From: coeff-aij <175928954+coeff-aij@users.noreply.github.com> Date: Mon, 12 Jan 2026 05:48:47 +0000 Subject: [PATCH 11/11] add: negative tests for raw_define --- tests/ui/fail/annot_raw_define.rs | 20 +++++++++++++++++++ .../fail/annot_raw_define_without_params.rs | 20 +++++++++++++++++++ 2 files changed, 40 insertions(+) create mode 100644 tests/ui/fail/annot_raw_define.rs create mode 100644 tests/ui/fail/annot_raw_define_without_params.rs diff --git a/tests/ui/fail/annot_raw_define.rs b/tests/ui/fail/annot_raw_define.rs new file mode 100644 index 0000000..346a158 --- /dev/null +++ b/tests/ui/fail/annot_raw_define.rs @@ -0,0 +1,20 @@ +//@error-in-other-file: UnexpectedToken +//@compile-flags: -Adead_code -C debug-assertions=off + +// Insert definitions written in SMT-LIB2 format into .smt file directly. +// This feature is intended for debug or experiment purpose. +#![feature(custom_inner_attributes)] +#![thrust::raw_define(true)] // argument must be single string literal + +#[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))); +} diff --git a/tests/ui/fail/annot_raw_define_without_params.rs b/tests/ui/fail/annot_raw_define_without_params.rs new file mode 100644 index 0000000..d6683a8 --- /dev/null +++ b/tests/ui/fail/annot_raw_define_without_params.rs @@ -0,0 +1,20 @@ +//@error-in-other-file: invalid attribute +//@compile-flags: -Adead_code -C debug-assertions=off + +// Insert definitions written in SMT-LIB2 format into .smt file directly. +// This feature is intended for debug or experiment purpose. +#![feature(custom_inner_attributes)] +#![thrust::raw_define] // argument must be single string literal + +#[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))); +}