From 7f68acf57b166848ba38cd20a45be1205a0a4215 Mon Sep 17 00:00:00 2001 From: coord_e Date: Thu, 15 Jan 2026 02:00:21 +0900 Subject: [PATCH 01/23] Run CI workflow on pull_request From 9a0ee9b8f61a29dee7a4acc8dc40a0bbfdca8911 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 02/23] 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 984c159f514bae9f6d14159ab2204461176feb1e 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 03/23] 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 209dfed77ff1f21a25a502e59cca72ade0decb8d 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 04/23] 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 8c2716f631f2dab73a9c4c58dc31d520ce4e4642 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 05/23] 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 e19c5bcbca168fbc9b36ea1ec0ad19bd2e5b9da2 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 06/23] 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 aab6bdcd4d90551beaeb3028895f5303ee3b67db 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 07/23] 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 79813f2192c3e123155d0c80f84c3facd0904c58 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 08/23] 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 f18c14d2214a1b423761830c8e88bded9f046e58 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 09/23] 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 1b6658aba5180a28834d932933b515b04c116f8f 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 10/23] 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 bdf5b4dda0d2ce3ccc27ffd71501d95c787916f2 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 11/23] 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 393e7e6e758771377964c27cbbc065cb2c3a5213 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 12/23] 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))); +} From 55bc8586c1c5ddad6bbe8ba674c7f904fdfebf95 Mon Sep 17 00:00:00 2001 From: coeff-aij <175928954+coeff-aij@users.noreply.github.com> Date: Wed, 14 Jan 2026 08:06:47 +0000 Subject: [PATCH 13/23] fix: tests for raw_define(removing unused code, add more description) --- tests/ui/fail/annot_raw_define.rs | 7 +++---- tests/ui/fail/annot_raw_define_without_params.rs | 5 ++--- tests/ui/pass/annot_raw_define.rs | 6 ++---- tests/ui/pass/annot_raw_define_multi.rs | 4 +--- 4 files changed, 8 insertions(+), 14 deletions(-) diff --git a/tests/ui/fail/annot_raw_define.rs b/tests/ui/fail/annot_raw_define.rs index 346a158..0f04622 100644 --- a/tests/ui/fail/annot_raw_define.rs +++ b/tests/ui/fail/annot_raw_define.rs @@ -1,14 +1,14 @@ -//@error-in-other-file: UnexpectedToken //@compile-flags: -Adead_code -C debug-assertions=off +// This test panics with "invalid attribute" for now. +// TODO: reporting rustc diagnostics for parse errors -// Insert definitions written in SMT-LIB2 format into .smt file directly. +// Insert definitions written in SMT-LIB2 format into .smt2 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 } @@ -16,5 +16,4 @@ fn double(x: i64) -> i64 { 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 index d6683a8..90541d0 100644 --- a/tests/ui/fail/annot_raw_define_without_params.rs +++ b/tests/ui/fail/annot_raw_define_without_params.rs @@ -1,5 +1,6 @@ -//@error-in-other-file: invalid attribute //@compile-flags: -Adead_code -C debug-assertions=off +// This test panics with "invalid attribute" for now. +// TODO: reporting rustc diagnostics for parse errors // Insert definitions written in SMT-LIB2 format into .smt file directly. // This feature is intended for debug or experiment purpose. @@ -8,7 +9,6 @@ #[thrust::requires(true)] #[thrust::ensures(result == 2 * x)] -// #[thrust::ensures(is_double(x, result))] fn double(x: i64) -> i64 { x + x } @@ -16,5 +16,4 @@ fn double(x: i64) -> i64 { fn main() { let a = 3; assert!(double(a) == 6); - // assert!(is_double(a, double(a))); } diff --git a/tests/ui/pass/annot_raw_define.rs b/tests/ui/pass/annot_raw_define.rs index c1c47a7..ab30bd3 100644 --- a/tests/ui/pass/annot_raw_define.rs +++ b/tests/ui/pass/annot_raw_define.rs @@ -1,7 +1,7 @@ //@check-pass //@compile-flags: -Adead_code -C debug-assertions=off -// Insert definitions written in SMT-LIB2 format into .smt file directly. +// Insert definitions written in SMT-LIB2 format into .smt2 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 @@ -12,8 +12,7 @@ )")] #[thrust::requires(true)] -#[thrust::ensures(result == 2 * x)] -// #[thrust::ensures(is_double(x, result))] +#[thrust::ensures(result == 2 * x)] fn double(x: i64) -> i64 { x + x } @@ -21,5 +20,4 @@ fn double(x: i64) -> i64 { fn main() { let a = 3; assert!(double(a) == 6); - // assert!(is_double(a, double(a))); } diff --git a/tests/ui/pass/annot_raw_define_multi.rs b/tests/ui/pass/annot_raw_define_multi.rs index ae9e0eb..3b2d9d9 100644 --- a/tests/ui/pass/annot_raw_define_multi.rs +++ b/tests/ui/pass/annot_raw_define_multi.rs @@ -1,7 +1,7 @@ //@check-pass //@compile-flags: -Adead_code -C debug-assertions=off -// Insert definitions written in SMT-LIB2 format into .smt file directly. +// Insert definitions written in SMT-LIB2 format into .smt2 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 @@ -21,7 +21,6 @@ #[thrust::requires(true)] #[thrust::ensures(result == 2 * x)] -// #[thrust::ensures(is_double(x, result))] fn double(x: i64) -> i64 { x + x } @@ -29,5 +28,4 @@ fn double(x: i64) -> i64 { fn main() { let a = 3; assert!(double(a) == 6); - // assert!(is_double(a, double(a))); } From 5f8e80ea620af8db4f84fd9bf1c308c829d6f3fa Mon Sep 17 00:00:00 2001 From: coeff-aij <175928954+coeff-aij@users.noreply.github.com> Date: Wed, 14 Jan 2026 08:23:31 +0000 Subject: [PATCH 14/23] change: rename raw_define -> raw_command, RawDefine -> RawCommand, etc. --- src/analyze/annot.rs | 4 ++-- src/analyze/crate_.rs | 10 +++++----- src/annot.rs | 14 ++++++------- src/chc.rs | 12 +++++------ src/chc/format_context.rs | 10 +++++----- src/chc/smtlib2.rs | 20 +++++++++---------- src/chc/unbox.rs | 4 ++-- ...not_raw_define.rs => annot_raw_command.rs} | 4 ++-- ...rs => annot_raw_command_without_params.rs} | 4 ++-- ...not_raw_define.rs => annot_raw_command.rs} | 4 ++-- ...ne_multi.rs => annot_raw_command_multi.rs} | 8 ++++---- 11 files changed, 47 insertions(+), 47 deletions(-) rename tests/ui/fail/{annot_raw_define.rs => annot_raw_command.rs} (74%) rename tests/ui/fail/{annot_raw_define_without_params.rs => annot_raw_command_without_params.rs} (75%) rename tests/ui/pass/{annot_raw_define.rs => annot_raw_command.rs} (71%) rename tests/ui/pass/{annot_raw_define_multi.rs => annot_raw_command_multi.rs} (61%) diff --git a/src/analyze/annot.rs b/src/analyze/annot.rs index 30e70d3..1d7658e 100644 --- a/src/analyze/annot.rs +++ b/src/analyze/annot.rs @@ -37,8 +37,8 @@ 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")] +pub fn raw_command_path() -> [Symbol; 2] { + [Symbol::intern("thrust"), Symbol::intern("raw_command")] } /// A [`annot::Resolver`] implementation for resolving function parameters. diff --git a/src/analyze/crate_.rs b/src/analyze/crate_.rs index 4172f94..d5d6dde 100644 --- a/src/analyze/crate_.rs +++ b/src/analyze/crate_.rs @@ -28,18 +28,18 @@ pub struct Analyzer<'tcx, 'ctx> { } impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { - fn analyze_raw_define_annot(&mut self) { + fn analyze_raw_command_annot(&mut self) { for attrs in self.tcx.get_attrs_by_path( CRATE_DEF_ID.to_def_id(), - &analyze::annot::raw_define_path(), + &analyze::annot::raw_command_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); + let raw_command = parser.parse_raw_command(ts).unwrap(); + self.ctx.system.borrow_mut().push_raw_command(raw_command); } } @@ -204,7 +204,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.analyze_raw_command_annot(); self.refine_local_defs(); self.analyze_local_defs(); self.assert_callable_entry(); diff --git a/src/annot.rs b/src/annot.rs index 6541fee..5a9e63d 100644 --- a/src/annot.rs +++ b/src/annot.rs @@ -1077,8 +1077,8 @@ where Ok(AnnotFormula::Formula(formula)) } - pub fn parse_annot_raw_definition(&mut self) -> Result { - let t = self.next_token("raw CHC definition")?; + pub fn parse_annot_raw_command(&mut self) -> Result { + let t = self.next_token("raw CHC command")?; match t { Token { @@ -1089,8 +1089,8 @@ where } => { match kind { LitKind::Str => { - let definition = symbol.to_string(); - Ok(chc::RawDefinition{ definition }) + let command = symbol.to_string(); + Ok(chc::RawCommand{ command }) }, _ => Err(ParseAttrError::unexpected_token( "string literal", t.clone() @@ -1235,14 +1235,14 @@ where Ok(formula) } - pub fn parse_raw_definition(&self, ts: TokenStream) -> Result { + pub fn parse_raw_command(&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()?; + let raw_command = parser.parse_annot_raw_command()?; parser.end_of_input()?; - Ok(raw_definition) + Ok(raw_command) } } diff --git a/src/chc.rs b/src/chc.rs index eefdc4f..74550a3 100644 --- a/src/chc.rs +++ b/src/chc.rs @@ -1606,12 +1606,12 @@ impl Clause { } } -/// A definition specified using #![thrust::define_raw()] +/// A command 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, +pub struct RawCommand { + pub command: String, } /// A selector for a datatype constructor. @@ -1663,7 +1663,7 @@ pub struct PredVarDef { /// A CHC system. #[derive(Debug, Clone, Default)] pub struct System { - pub raw_definitions: Vec, + pub raw_commands: Vec, pub datatypes: Vec, pub clauses: IndexVec, pub pred_vars: IndexVec, @@ -1674,8 +1674,8 @@ 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_raw_command(&mut self, raw_command: RawCommand) { + self.raw_commands.push(raw_command) } pub fn push_clause(&mut self, clause: Clause) -> Option { diff --git a/src/chc/format_context.rs b/src/chc/format_context.rs index 1c75215..3240468 100644 --- a/src/chc/format_context.rs +++ b/src/chc/format_context.rs @@ -21,7 +21,7 @@ use crate::chc::{self, hoice::HoiceDatatypeRenamer}; pub struct FormatContext { renamer: HoiceDatatypeRenamer, datatypes: Vec, - raw_definitions: Vec, + raw_commands: Vec, } // FIXME: this is obviously ineffective and should be replaced @@ -274,16 +274,16 @@ impl FormatContext { .filter(|d| d.params == 0) .collect(); let renamer = HoiceDatatypeRenamer::new(&datatypes); - let raw_definitions = system.raw_definitions.clone(); - FormatContext { renamer, datatypes, raw_definitions } + let raw_commands = system.raw_commands.clone(); + FormatContext { renamer, datatypes, raw_commands } } pub fn datatypes(&self) -> &[chc::Datatype] { &self.datatypes } - pub fn raw_definitions(&self) -> &[chc::RawDefinition] { - &self.raw_definitions + pub fn raw_commands(&self) -> &[chc::RawCommand] { + &self.raw_commands } pub fn box_ctor(&self, sort: &chc::Sort) -> impl std::fmt::Display { diff --git a/src/chc/smtlib2.rs b/src/chc/smtlib2.rs index 0e0f2e9..fd2798c 100644 --- a/src/chc/smtlib2.rs +++ b/src/chc/smtlib2.rs @@ -370,24 +370,24 @@ impl<'ctx, 'a> Clause<'ctx, 'a> { } } -/// A wrapper around a [`chc::RawDefinition`] that provides a [`std::fmt::Display`] implementation in SMT-LIB2 format. +/// A wrapper around a [`chc::RawCommand`] that provides a [`std::fmt::Display`] implementation in SMT-LIB2 format. #[derive(Debug, Clone)] -pub struct RawDefinition<'a> { - inner: &'a chc::RawDefinition, +pub struct RawCommand<'a> { + inner: &'a chc::RawCommand, } -impl<'a> std::fmt::Display for RawDefinition<'a> { +impl<'a> std::fmt::Display for RawCommand<'a> { fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { write!( f, "{}", - self.inner.definition, + self.inner.command, ) } } -impl<'a> RawDefinition<'a> { - pub fn new(inner: &'a chc::RawDefinition) -> Self { +impl<'a> RawCommand<'a> { + pub fn new(inner: &'a chc::RawCommand) -> Self { Self { inner } @@ -579,9 +579,9 @@ 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))?; + // insert command from #![thrust::define_chc()] here + for raw_def in self.ctx.raw_commands() { + writeln!(f, "{}\n", RawCommand::new(raw_def))?; } writeln!(f, "{}\n", Datatypes::new(&self.ctx, self.ctx.datatypes()))?; diff --git a/src/chc/unbox.rs b/src/chc/unbox.rs index 40c2e6a..8ed320f 100644 --- a/src/chc/unbox.rs +++ b/src/chc/unbox.rs @@ -161,7 +161,7 @@ pub fn unbox(system: System) -> System { clauses, pred_vars, datatypes, - raw_definitions, + raw_commands, } = system; let datatypes = datatypes.into_iter().map(unbox_datatype).collect(); let clauses = clauses.into_iter().map(unbox_clause).collect(); @@ -170,6 +170,6 @@ pub fn unbox(system: System) -> System { clauses, pred_vars, datatypes, - raw_definitions, + raw_commands, } } diff --git a/tests/ui/fail/annot_raw_define.rs b/tests/ui/fail/annot_raw_command.rs similarity index 74% rename from tests/ui/fail/annot_raw_define.rs rename to tests/ui/fail/annot_raw_command.rs index 0f04622..c3073c0 100644 --- a/tests/ui/fail/annot_raw_define.rs +++ b/tests/ui/fail/annot_raw_command.rs @@ -2,10 +2,10 @@ // This test panics with "invalid attribute" for now. // TODO: reporting rustc diagnostics for parse errors -// Insert definitions written in SMT-LIB2 format into .smt2 file directly. +// Insert commands written in SMT-LIB2 format into .smt2 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::raw_command(true)] // argument must be single string literal #[thrust::requires(true)] #[thrust::ensures(result == 2 * x)] diff --git a/tests/ui/fail/annot_raw_define_without_params.rs b/tests/ui/fail/annot_raw_command_without_params.rs similarity index 75% rename from tests/ui/fail/annot_raw_define_without_params.rs rename to tests/ui/fail/annot_raw_command_without_params.rs index 90541d0..810e1b0 100644 --- a/tests/ui/fail/annot_raw_define_without_params.rs +++ b/tests/ui/fail/annot_raw_command_without_params.rs @@ -2,10 +2,10 @@ // This test panics with "invalid attribute" for now. // TODO: reporting rustc diagnostics for parse errors -// Insert definitions written in SMT-LIB2 format into .smt file directly. +// Insert commands 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::raw_command] // argument must be single string literal #[thrust::requires(true)] #[thrust::ensures(result == 2 * x)] diff --git a/tests/ui/pass/annot_raw_define.rs b/tests/ui/pass/annot_raw_command.rs similarity index 71% rename from tests/ui/pass/annot_raw_define.rs rename to tests/ui/pass/annot_raw_command.rs index ab30bd3..7999376 100644 --- a/tests/ui/pass/annot_raw_define.rs +++ b/tests/ui/pass/annot_raw_command.rs @@ -1,10 +1,10 @@ //@check-pass //@compile-flags: -Adead_code -C debug-assertions=off -// Insert definitions written in SMT-LIB2 format into .smt2 file directly. +// Insert commands written in SMT-LIB2 format into .smt2 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 +#![thrust::raw_command("(define-fun is_double ((x Int) (doubled_x Int)) Bool (= (* x 2) doubled_x diff --git a/tests/ui/pass/annot_raw_define_multi.rs b/tests/ui/pass/annot_raw_command_multi.rs similarity index 61% rename from tests/ui/pass/annot_raw_define_multi.rs rename to tests/ui/pass/annot_raw_command_multi.rs index 3b2d9d9..e6c2164 100644 --- a/tests/ui/pass/annot_raw_define_multi.rs +++ b/tests/ui/pass/annot_raw_command_multi.rs @@ -1,18 +1,18 @@ //@check-pass //@compile-flags: -Adead_code -C debug-assertions=off -// Insert definitions written in SMT-LIB2 format into .smt2 file directly. +// Insert commands written in SMT-LIB2 format into .smt2 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 +#![thrust::raw_command("(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 +// multiple raw commands can be inserted. +#![thrust::raw_command("(define-fun is_triple ((x Int) (tripled_x Int)) Bool (= (* x 3) tripled_x From d9e4a93bf0ed5cee9646cea488b657a6fced98f2 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 15/23] 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))); +} From 51f1afd05e3b1d436e44e1bb67576912c4aeab8f Mon Sep 17 00:00:00 2001 From: coeff-aij <175928954+coeff-aij@users.noreply.github.com> Date: Wed, 14 Jan 2026 19:48:56 +0900 Subject: [PATCH 16/23] remove: FormatContext::raw_commands --- src/chc/format_context.rs | 8 +------- src/chc/smtlib2.rs | 14 +++++++------- 2 files changed, 8 insertions(+), 14 deletions(-) diff --git a/src/chc/format_context.rs b/src/chc/format_context.rs index 3240468..2123315 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, - raw_commands: Vec, } // FIXME: this is obviously ineffective and should be replaced @@ -274,18 +273,13 @@ impl FormatContext { .filter(|d| d.params == 0) .collect(); let renamer = HoiceDatatypeRenamer::new(&datatypes); - let raw_commands = system.raw_commands.clone(); - FormatContext { renamer, datatypes, raw_commands } + FormatContext { renamer, datatypes } } pub fn datatypes(&self) -> &[chc::Datatype] { &self.datatypes } - pub fn raw_commands(&self) -> &[chc::RawCommand] { - &self.raw_commands - } - 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 fd2798c..0bd7311 100644 --- a/src/chc/smtlib2.rs +++ b/src/chc/smtlib2.rs @@ -579,9 +579,9 @@ 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 command from #![thrust::define_chc()] here - for raw_def in self.ctx.raw_commands() { - writeln!(f, "{}\n", RawCommand::new(raw_def))?; + // insert command from #![thrust::raw_command()] here + for raw_command in &self.inner.raw_commands { + writeln!(f, "{}\n", RawCommand::new(raw_command))?; } writeln!(f, "{}\n", Datatypes::new(&self.ctx, self.ctx.datatypes()))?; @@ -590,15 +590,15 @@ impl<'a> std::fmt::Display for System<'a> { 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() { - writeln!(f, "{}", def.debug_info.display("; "))?; + for (p, cmd) in self.inner.pred_vars.iter_enumerated() { + if !cmd.debug_info.is_empty() { + writeln!(f, "{}", cmd.debug_info.display("; "))?; } writeln!( f, "(declare-fun {} {} Bool)\n", p, - List::closed(def.sig.iter().map(|s| self.ctx.fmt_sort(s))) + List::closed(cmd.sig.iter().map(|s| self.ctx.fmt_sort(s))) )?; } for (id, clause) in self.inner.clauses.iter_enumerated() { From c1458e67abf72f2efe803f64ca265216198fc172 Mon Sep 17 00:00:00 2001 From: coeff-aij <175928954+coeff-aij@users.noreply.github.com> Date: Wed, 14 Jan 2026 19:59:10 +0900 Subject: [PATCH 17/23] fix: wrong description about the error on negative test --- tests/ui/fail/annot_raw_command.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/ui/fail/annot_raw_command.rs b/tests/ui/fail/annot_raw_command.rs index c3073c0..7ca52a7 100644 --- a/tests/ui/fail/annot_raw_command.rs +++ b/tests/ui/fail/annot_raw_command.rs @@ -1,5 +1,5 @@ //@compile-flags: -Adead_code -C debug-assertions=off -// This test panics with "invalid attribute" for now. +// This test panics with "UnexpectedToken" for now. // TODO: reporting rustc diagnostics for parse errors // Insert commands written in SMT-LIB2 format into .smt2 file directly. From ace4d2aa7e40cecae0bae3b8a7283207a157f920 Mon Sep 17 00:00:00 2001 From: coeff-aij <175928954+coeff-aij@users.noreply.github.com> Date: Thu, 15 Jan 2026 06:55:13 +0000 Subject: [PATCH 18/23] fix: undo accidental renames --- src/chc/smtlib2.rs | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/chc/smtlib2.rs b/src/chc/smtlib2.rs index 0bd7311..5d53fad 100644 --- a/src/chc/smtlib2.rs +++ b/src/chc/smtlib2.rs @@ -590,15 +590,15 @@ impl<'a> std::fmt::Display for System<'a> { writeln!(f, "{}", MatcherPredFun::new(&self.ctx, datatype))?; } writeln!(f)?; - for (p, cmd) in self.inner.pred_vars.iter_enumerated() { - if !cmd.debug_info.is_empty() { - writeln!(f, "{}", cmd.debug_info.display("; "))?; + for (p, def) in self.inner.pred_vars.iter_enumerated() { + if !def.debug_info.is_empty() { + writeln!(f, "{}", def.debug_info.display("; "))?; } writeln!( f, "(declare-fun {} {} Bool)\n", p, - List::closed(cmd.sig.iter().map(|s| self.ctx.fmt_sort(s))) + List::closed(def.sig.iter().map(|s| self.ctx.fmt_sort(s))) )?; } for (id, clause) in self.inner.clauses.iter_enumerated() { From bc798667551aa30c3996c2b06003946c47961e11 Mon Sep 17 00:00:00 2001 From: coeff-aij <175928954+coeff-aij@users.noreply.github.com> Date: Thu, 15 Jan 2026 08:05:49 +0000 Subject: [PATCH 19/23] change: delete annot::AnnotParser::parse_raw_definition() and proccess TokenTrees directly --- src/analyze/crate_.rs | 19 +++++++++++++------ src/annot.rs | 39 +-------------------------------------- 2 files changed, 14 insertions(+), 44 deletions(-) diff --git a/src/analyze/crate_.rs b/src/analyze/crate_.rs index d5d6dde..23e91c2 100644 --- a/src/analyze/crate_.rs +++ b/src/analyze/crate_.rs @@ -9,7 +9,6 @@ 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. /// @@ -33,13 +32,21 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { CRATE_DEF_ID.to_def_id(), &analyze::annot::raw_command_path(), ) { + use rustc_ast::token::{LitKind, Token, TokenKind}; + use rustc_ast::tokenstream::TokenTree; + 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 tt = ts.trees().next().expect("string literal"); + + let raw_command = match tt { + TokenTree::Token(Token{ kind: TokenKind::Literal(lit), .. }, _) + if lit.kind == LitKind::Str => Some(lit.symbol.to_string()), + _ => None, + }.expect("invalid raw_command annotation"); + + self.ctx.system.borrow_mut().push_raw_command( + chc::RawCommand {command: raw_command} ); - let raw_command = parser.parse_raw_command(ts).unwrap(); - self.ctx.system.borrow_mut().push_raw_command(raw_command); } } diff --git a/src/annot.rs b/src/annot.rs index 5a9e63d..128c289 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, Lit, Token, TokenKind}; +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; @@ -1076,32 +1076,6 @@ where .ok_or_else(|| ParseAttrError::unexpected_term("in annotation"))?; Ok(AnnotFormula::Formula(formula)) } - - pub fn parse_annot_raw_command(&mut self) -> Result { - let t = self.next_token("raw CHC command")?; - - match t { - Token { - kind: TokenKind::Literal( - Lit { kind, symbol, .. } - ), - .. - } => { - match kind { - LitKind::Str => { - let command = symbol.to_string(); - Ok(chc::RawCommand{ command }) - }, - _ => 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`]. @@ -1234,15 +1208,4 @@ where parser.end_of_input()?; Ok(formula) } - - pub fn parse_raw_command(&self, ts: TokenStream) -> Result { - let mut parser = Parser { - resolver: &self.resolver, - cursor: ts.trees(), - formula_existentials: Default::default(), - }; - let raw_command = parser.parse_annot_raw_command()?; - parser.end_of_input()?; - Ok(raw_command) - } } From 49370717e4713ed4d86ef58e9033b221aa155a2b Mon Sep 17 00:00:00 2001 From: coeff-aij <175928954+coeff-aij@users.noreply.github.com> Date: Fri, 16 Jan 2026 15:12:57 +0000 Subject: [PATCH 20/23] fix: run `cargo fmt` --- src/analyze/crate_.rs | 21 +++++++++++++++------ src/chc/smtlib2.rs | 10 ++-------- 2 files changed, 17 insertions(+), 14 deletions(-) diff --git a/src/analyze/crate_.rs b/src/analyze/crate_.rs index 23e91c2..fabe4b4 100644 --- a/src/analyze/crate_.rs +++ b/src/analyze/crate_.rs @@ -39,14 +39,23 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { let tt = ts.trees().next().expect("string literal"); let raw_command = match tt { - TokenTree::Token(Token{ kind: TokenKind::Literal(lit), .. }, _) - if lit.kind == LitKind::Str => Some(lit.symbol.to_string()), + TokenTree::Token( + Token { + kind: TokenKind::Literal(lit), + .. + }, + _, + ) if lit.kind == LitKind::Str => Some(lit.symbol.to_string()), _ => None, - }.expect("invalid raw_command annotation"); + } + .expect("invalid raw_command annotation"); - self.ctx.system.borrow_mut().push_raw_command( - chc::RawCommand {command: raw_command} - ); + self.ctx + .system + .borrow_mut() + .push_raw_command(chc::RawCommand { + command: raw_command, + }); } } diff --git a/src/chc/smtlib2.rs b/src/chc/smtlib2.rs index 5d53fad..1fb7319 100644 --- a/src/chc/smtlib2.rs +++ b/src/chc/smtlib2.rs @@ -378,19 +378,13 @@ pub struct RawCommand<'a> { impl<'a> std::fmt::Display for RawCommand<'a> { fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { - write!( - f, - "{}", - self.inner.command, - ) + write!(f, "{}", self.inner.command,) } } impl<'a> RawCommand<'a> { pub fn new(inner: &'a chc::RawCommand) -> Self { - Self { - inner - } + Self { inner } } } From 49f5691c57906e64ad7cd8496a1e56e4f4560416 Mon Sep 17 00:00:00 2001 From: coeff-aij <175928954+coeff-aij@users.noreply.github.com> Date: Fri, 16 Jan 2026 15:15:06 +0000 Subject: [PATCH 21/23] remove: accidentally duplicated negative tests --- tests/ui/fail/annot_raw_command.rs | 19 ------------------ .../fail/annot_raw_command_without_params.rs | 19 ------------------ tests/ui/fail/annot_raw_define.rs | 20 ------------------- .../fail/annot_raw_define_without_params.rs | 20 ------------------- 4 files changed, 78 deletions(-) delete mode 100644 tests/ui/fail/annot_raw_command.rs delete mode 100644 tests/ui/fail/annot_raw_command_without_params.rs delete mode 100644 tests/ui/fail/annot_raw_define.rs delete mode 100644 tests/ui/fail/annot_raw_define_without_params.rs diff --git a/tests/ui/fail/annot_raw_command.rs b/tests/ui/fail/annot_raw_command.rs deleted file mode 100644 index 7ca52a7..0000000 --- a/tests/ui/fail/annot_raw_command.rs +++ /dev/null @@ -1,19 +0,0 @@ -//@compile-flags: -Adead_code -C debug-assertions=off -// This test panics with "UnexpectedToken" for now. -// TODO: reporting rustc diagnostics for parse errors - -// Insert commands written in SMT-LIB2 format into .smt2 file directly. -// This feature is intended for debug or experiment purpose. -#![feature(custom_inner_attributes)] -#![thrust::raw_command(true)] // argument must be single string literal - -#[thrust::requires(true)] -#[thrust::ensures(result == 2 * x)] -fn double(x: i64) -> i64 { - x + x -} - -fn main() { - let a = 3; - assert!(double(a) == 6); -} diff --git a/tests/ui/fail/annot_raw_command_without_params.rs b/tests/ui/fail/annot_raw_command_without_params.rs deleted file mode 100644 index 810e1b0..0000000 --- a/tests/ui/fail/annot_raw_command_without_params.rs +++ /dev/null @@ -1,19 +0,0 @@ -//@compile-flags: -Adead_code -C debug-assertions=off -// This test panics with "invalid attribute" for now. -// TODO: reporting rustc diagnostics for parse errors - -// Insert commands written in SMT-LIB2 format into .smt file directly. -// This feature is intended for debug or experiment purpose. -#![feature(custom_inner_attributes)] -#![thrust::raw_command] // argument must be single string literal - -#[thrust::requires(true)] -#[thrust::ensures(result == 2 * x)] -fn double(x: i64) -> i64 { - x + x -} - -fn main() { - let a = 3; - assert!(double(a) == 6); -} diff --git a/tests/ui/fail/annot_raw_define.rs b/tests/ui/fail/annot_raw_define.rs deleted file mode 100644 index 346a158..0000000 --- a/tests/ui/fail/annot_raw_define.rs +++ /dev/null @@ -1,20 +0,0 @@ -//@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 deleted file mode 100644 index d6683a8..0000000 --- a/tests/ui/fail/annot_raw_define_without_params.rs +++ /dev/null @@ -1,20 +0,0 @@ -//@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))); -} From cac76db27c9007299ae12647d16f2783c278a9ed Mon Sep 17 00:00:00 2001 From: coeff-aij <175928954+coeff-aij@users.noreply.github.com> Date: Tue, 20 Jan 2026 20:24:37 +0900 Subject: [PATCH 22/23] Update src/analyze/crate_.rs Co-authored-by: Hiromi Ogawa --- src/analyze/crate_.rs | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/src/analyze/crate_.rs b/src/analyze/crate_.rs index fabe4b4..bd1d87b 100644 --- a/src/analyze/crate_.rs +++ b/src/analyze/crate_.rs @@ -45,10 +45,9 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { .. }, _, - ) if lit.kind == LitKind::Str => Some(lit.symbol.to_string()), - _ => None, - } - .expect("invalid raw_command annotation"); + ) if lit.kind == LitKind::Str => lit.symbol.to_string(), + _ => panic!("invalid raw_command annotation"), + }; self.ctx .system From f354b5d671353b5211235631cdc2d55ddfb3cb6e Mon Sep 17 00:00:00 2001 From: coeff-aij <175928954+coeff-aij@users.noreply.github.com> Date: Tue, 20 Jan 2026 20:24:51 +0900 Subject: [PATCH 23/23] Update src/chc.rs Co-authored-by: Hiromi Ogawa --- src/chc.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/chc.rs b/src/chc.rs index 74550a3..67ef92b 100644 --- a/src/chc.rs +++ b/src/chc.rs @@ -1606,7 +1606,7 @@ impl Clause { } } -/// A command specified using #![thrust::define_raw()] +/// A command specified using `thrust::raw_command` attribute /// /// Those will be directly inserted into the generated SMT-LIB2 file. #[derive(Debug, Clone)]