From 4eae8924b014f4f5fa518b8915ea122e79e4ff9e Mon Sep 17 00:00:00 2001 From: coeff-aij <175928954+coeff-aij@users.noreply.github.com> Date: Sat, 23 May 2026 17:46:56 +0900 Subject: [PATCH 01/55] add: ForallSort --- src/chc.rs | 61 ++++++++++++++++++++++++++++++++++++++- src/chc/format_context.rs | 1 + src/chc/unbox.rs | 5 ++++ src/rty.rs | 6 +++- 4 files changed, 71 insertions(+), 2 deletions(-) diff --git a/src/chc.rs b/src/chc.rs index 58166391..3d32d7c4 100644 --- a/src/chc.rs +++ b/src/chc.rs @@ -84,6 +84,45 @@ impl DatatypeSort { } } +rustc_index::newtype_index! { + /// An index representing sort-level variable. + /// + /// We manage sort-level variables using indices that are unique in the whole CHC system. + /// [`System`] contains `Vec` that manages the indices of the variables. + #[orderable] + #[debug_format = "a{}"] + pub struct ForallSortIdx { } +} + +impl Default for ForallSortIdx { + fn default() -> Self { + 0_usize.into() + } +} + +impl std::fmt::Display for ForallSortIdx { + fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result { + write!(f, "a{}", self.index()) + } +} + +impl<'a, D> Pretty<'a, D, termcolor::ColorSpec> for &ForallSortIdx +where + D: pretty::DocAllocator<'a, termcolor::ColorSpec>, +{ + fn pretty(self, allocator: &'a D) -> pretty::DocBuilder<'a, D, termcolor::ColorSpec> { + allocator + .as_string(self) + .annotate(ForallSortIdx::color_spec()) + } +} + +impl ForallSortIdx { + fn color_spec() -> termcolor::ColorSpec { + termcolor::ColorSpec::new() + } +} + /// A sort is the type of a logical term. #[derive(Debug, Clone, PartialEq, Eq, Hash, PartialOrd, Ord)] pub enum Sort { @@ -97,6 +136,7 @@ pub enum Sort { Tuple(Vec), Array(Box, Box), Datatype(DatatypeSort), + Forall(ForallSortIdx), } impl From for Sort { @@ -154,6 +194,7 @@ where } } Sort::Datatype(sort) => sort.pretty(allocator), + Sort::Forall(idx) => idx.pretty(allocator), } } } @@ -180,7 +221,12 @@ impl Sort { fn walk_impl<'a, 'b>(&'a self, mut f: Box) { f(self); match self { - Sort::Null | Sort::Int | Sort::Bool | Sort::String | Sort::Param(_) => {} + Sort::Null + | Sort::Int + | Sort::Bool + | Sort::String + | Sort::Param(_) + | Sort::Forall(_) => {} Sort::Box(s) | Sort::Mut(s) => s.walk(Box::new(&mut f)), Sort::Tuple(ss) => { for s in ss { @@ -261,6 +307,10 @@ impl Sort { Sort::Datatype(DatatypeSort { symbol, args }) } + pub fn forall(index: ForallSortIdx) -> Self { + Sort::Forall(index) + } + pub fn into_datatype(self) -> Option { match self { Sort::Datatype(sort) => Some(sort), @@ -1783,6 +1833,8 @@ pub struct System { pub user_defined_pred_defs: Vec, pub clauses: IndexVec, pub pred_vars: IndexVec, + pub forall_sorts: Vec, + pub num_forall_sort_idx: ForallSortIdx, } impl System { @@ -1790,6 +1842,13 @@ impl System { self.pred_vars.push(PredVarDef { sig, debug_info }) } + pub fn new_forall_sort(&mut self) -> ForallSortIdx { + let new_idx = self.num_forall_sort_idx; + self.num_forall_sort_idx += 1; + self.forall_sorts.push(new_idx); + new_idx + } + pub fn push_raw_command(&mut self, raw_command: RawCommand) { self.raw_commands.push(raw_command) } diff --git a/src/chc/format_context.rs b/src/chc/format_context.rs index 94548274..86895e02 100644 --- a/src/chc/format_context.rs +++ b/src/chc/format_context.rs @@ -87,6 +87,7 @@ impl<'a> std::fmt::Display for SortSymbol<'a> { write!(f, "Array{}", SortSymbols::new(&[*s1.clone(), *s2.clone()])) } chc::Sort::Datatype(s) => write!(f, "{}{}", s.symbol, SortSymbols::new(&s.args)), + chc::Sort::Forall(i) => write!(f, "{}", i), } } } diff --git a/src/chc/unbox.rs b/src/chc/unbox.rs index b3b24d52..08d36c4e 100644 --- a/src/chc/unbox.rs +++ b/src/chc/unbox.rs @@ -72,6 +72,7 @@ fn unbox_sort(sort: Sort) -> Sort { Sort::Tuple(sorts) => Sort::Tuple(sorts.into_iter().map(unbox_sort).collect()), Sort::Array(s1, s2) => Sort::Array(Box::new(unbox_sort(*s1)), Box::new(unbox_sort(*s2))), Sort::Datatype(sort) => Sort::Datatype(unbox_datatype_sort(sort)), + Sort::Forall(i) => Sort::Forall(i), } } @@ -174,6 +175,8 @@ pub fn unbox(system: System) -> System { user_defined_pred_defs, clauses, pred_vars, + forall_sorts, + num_forall_sort_idx, } = system; let datatypes = datatypes.into_iter().map(unbox_datatype).collect(); let clauses = clauses.into_iter().map(unbox_clause).collect(); @@ -188,5 +191,7 @@ pub fn unbox(system: System) -> System { user_defined_pred_defs, clauses, pred_vars, + forall_sorts, + num_forall_sort_idx, } } diff --git a/src/rty.rs b/src/rty.rs index f1254fc6..876dc02d 100644 --- a/src/rty.rs +++ b/src/rty.rs @@ -1757,7 +1757,11 @@ impl RefinedType { /// Substitutes type parameters in a sort. fn subst_ty_params_in_sort(sort: &mut chc::Sort, subst: &TypeParamSubst) { match sort { - chc::Sort::Null | chc::Sort::Int | chc::Sort::Bool | chc::Sort::String => {} + chc::Sort::Null + | chc::Sort::Int + | chc::Sort::Bool + | chc::Sort::String + | chc::Sort::Forall(_) => {} chc::Sort::Param(idx) => { let type_param_idx = TypeParamIdx::from_usize(*idx); if let Some(rty) = subst.get(type_param_idx) { From 2e330a33808828905fd51aa2586f0a4c617454a4 Mon Sep 17 00:00:00 2001 From: coeff-aij <175928954+coeff-aij@users.noreply.github.com> Date: Sun, 24 May 2026 17:54:43 +0900 Subject: [PATCH 02/55] change: translate param type using ForallSortIdx --- src/refine/template.rs | 46 +++++++++++++++++++----------------------- 1 file changed, 21 insertions(+), 25 deletions(-) diff --git a/src/refine/template.rs b/src/refine/template.rs index ed0762ed..56fca463 100644 --- a/src/refine/template.rs +++ b/src/refine/template.rs @@ -1,4 +1,6 @@ +use std::cell::RefCell; use std::collections::HashMap; +use std::rc::Rc; use rustc_index::IndexVec; use rustc_middle::mir::{Local, Mutability}; @@ -6,7 +8,7 @@ use rustc_middle::ty as mir_ty; use rustc_span::def_id::DefId; use super::basic_block::BasicBlockType; -use crate::analyze::DefIdCache; +use crate::analyze::{DefIdCache, TypeParams}; use crate::chc; use crate::refine; use crate::rty; @@ -71,43 +73,37 @@ where pub struct TypeBuilder<'tcx> { tcx: mir_ty::TyCtxt<'tcx>, def_ids: DefIdCache<'tcx>, + def_id: DefId, typing_env: mir_ty::TypingEnv<'tcx>, - /// Maps index in [`mir_ty::ParamTy`] to [`rty::TypeParamIdx`]. - /// These indices may differ because we skip lifetime parameters and they always need to be - /// mapped when we translate a [`mir_ty::ParamTy`] to [`rty::ParamType`]. - /// See [`rty::TypeParamIdx`] for more details. - param_idx_mapping: HashMap, + type_params: Rc>, + system: Rc>, } impl<'tcx> TypeBuilder<'tcx> { - pub fn new(tcx: mir_ty::TyCtxt<'tcx>, def_ids: DefIdCache<'tcx>, def_id: DefId) -> Self { - let generics = tcx.generics_of(def_id); - let mut param_idx_mapping: HashMap = Default::default(); - for i in 0..generics.count() { - let generic_param = generics.param_at(i, tcx); - match generic_param.kind { - mir_ty::GenericParamDefKind::Lifetime => {} - mir_ty::GenericParamDefKind::Type { .. } => { - param_idx_mapping.insert(i as u32, param_idx_mapping.len().into()); - } - mir_ty::GenericParamDefKind::Const { .. } => {} - } - } + pub fn new( + tcx: mir_ty::TyCtxt<'tcx>, + def_ids: DefIdCache<'tcx>, + def_id: DefId, + type_params: Rc>, + system: Rc>, + ) -> Self { let typing_env = mir_ty::TypingEnv::post_analysis(tcx, def_id); Self { tcx, def_ids, + def_id, typing_env, - param_idx_mapping, + type_params, + system, } } fn translate_param_type(&self, ty: &mir_ty::ParamTy) -> rty::Type { - let index = *self - .param_idx_mapping - .get(&ty.index) - .expect("unknown type param idx"); - rty::ParamType::new(index).into() + let mut type_params = self.type_params.borrow_mut(); + let index = type_params + .entry((self.def_id, ty.index)) + .or_insert(self.system.borrow_mut().new_forall_sort()); + rty::ParamType::new(*index).into() } /// Replaces {closure} types with thrust_models::Closure<{closure}>. From f95cfdee2c69f4c25feb082ea5d8273daca2c2fa Mon Sep 17 00:00:00 2001 From: coeff-aij <175928954+coeff-aij@users.noreply.github.com> Date: Mon, 8 Jun 2026 11:58:38 +0900 Subject: [PATCH 03/55] change: translate Type::Param into chc::Sort::Forall --- src/analyze.rs | 27 ++++++++++-- src/analyze/annot_fn.rs | 12 ++++- src/analyze/basic_block.rs | 2 +- src/analyze/local_def.rs | 2 +- src/rty.rs | 4 +- src/rty/params.rs | 89 +++++++++++++++++++------------------- 6 files changed, 83 insertions(+), 53 deletions(-) diff --git a/src/analyze.rs b/src/analyze.rs index 2f0dbe5d..5148279c 100644 --- a/src/analyze.rs +++ b/src/analyze.rs @@ -197,6 +197,7 @@ impl refine::EnumDefProvider for Rc> { } pub type Env = refine::Env>>; +pub type TypeParams = HashMap<(DefId, u32), chc::ForallSortIdx>; #[derive(Debug, Clone)] struct DeferredFormulaFnDef<'tcx> { @@ -224,6 +225,8 @@ pub struct Analyzer<'tcx> { def_ids: did_cache::DefIdCache<'tcx>, enum_defs: Rc>, + + type_params: Rc>, } impl<'tcx> crate::refine::TemplateRegistry for Analyzer<'tcx> { @@ -251,6 +254,7 @@ impl<'tcx> Analyzer<'tcx> { let system = Default::default(); let basic_blocks = Default::default(); let enum_defs = Default::default(); + let type_params = Default::default(); Self { tcx, defs, @@ -259,6 +263,7 @@ impl<'tcx> Analyzer<'tcx> { basic_blocks, def_ids: did_cache::DefIdCache::new(tcx), enum_defs, + type_params, } } @@ -292,7 +297,7 @@ impl<'tcx> Analyzer<'tcx> { .iter() .map(|field| { let field_ty = self.tcx.type_of(field.did).instantiate_identity(); - TypeBuilder::new(self.tcx, self.def_ids(), def_id).build(field_ty) + self.type_builder(self.def_ids(), def_id).build(field_ty) }) .collect(); rty::EnumVariantDef { @@ -412,7 +417,13 @@ impl<'tcx> Analyzer<'tcx> { def_id: DefId, generic_args: mir_ty::GenericArgsRef<'tcx>, ) -> Option { - let type_builder = TypeBuilder::new(self.tcx, self.def_ids(), def_id); + let type_builder = TypeBuilder::new( + self.tcx, + self.def_ids(), + def_id, + self.type_params.clone(), + self.system.clone(), + ); let mut def_ty = match self.defs.get(&def_id)? { DefTy::Concrete(rty) => rty.clone(), DefTy::Deferred(deferred) => deferred.cache.borrow().get(&generic_args)?.clone(), @@ -456,7 +467,7 @@ impl<'tcx> Analyzer<'tcx> { def_id: DefId, generic_args: mir_ty::GenericArgsRef<'tcx>, ) -> Option { - let type_builder = TypeBuilder::new(self.tcx, self.def_ids(), def_id); + let type_builder = self.type_builder(self.def_ids(), def_id); let deferred_ty = match self.defs.get(&def_id)? { DefTy::Concrete(rty) => { @@ -641,6 +652,16 @@ impl<'tcx> Analyzer<'tcx> { basic_block::Analyzer::new(self, local_def_id, bb) } + pub fn type_builder(&self, def_ids: DefIdCache<'tcx>, def_id: DefId) -> TypeBuilder<'tcx> { + TypeBuilder::new( + self.tcx, + def_ids, + def_id, + self.type_params.clone(), + self.system.clone(), + ) + } + pub fn solve(&mut self) { if let Err(err) = self.system.borrow().solve() { self.tcx.dcx().err(format!("verification error: {:?}", err)); diff --git a/src/analyze/annot_fn.rs b/src/analyze/annot_fn.rs index 2711cd81..2bbbe673 100644 --- a/src/analyze/annot_fn.rs +++ b/src/analyze/annot_fn.rs @@ -7,7 +7,7 @@ use rustc_middle::ty::{self as mir_ty, TyCtxt}; use crate::analyze::{self, did_cache::DefIdCache}; use crate::annot::AnnotFormula; -use crate::chc; +use crate::chc::{self}; use crate::refine::{self, TypeBuilder}; use crate::rty; @@ -151,7 +151,13 @@ impl<'a, 'tcx> AnnotFnTranslator<'a, 'tcx> { let generic_args = tcx.mk_args(&[]); let typeck = tcx.typeck(local_def_id); let def_ids = analyzer.def_ids(); - let type_builder = TypeBuilder::new(tcx, def_ids.clone(), local_def_id.to_def_id()); + let type_builder = TypeBuilder::new( + tcx, + def_ids.clone(), + local_def_id.to_def_id(), + analyzer.type_params.clone(), + analyzer.system.clone(), + ); let mut translator = Self { tcx, local_def_id, @@ -178,6 +184,8 @@ impl<'a, 'tcx> AnnotFnTranslator<'a, 'tcx> { self.tcx, self.def_ids.clone(), self.local_def_id.to_def_id(), + self.analyzer.type_params.clone(), + self.analyzer.system.clone(), ); self } diff --git a/src/analyze/basic_block.rs b/src/analyze/basic_block.rs index b76fb1a3..b7746f31 100644 --- a/src/analyze/basic_block.rs +++ b/src/analyze/basic_block.rs @@ -1334,7 +1334,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { let env = ctx.new_env(); let local_decls = body.local_decls.clone(); let prophecy_vars = Default::default(); - let type_builder = TypeBuilder::new(tcx, ctx.def_ids(), local_def_id.to_def_id()); + let type_builder = ctx.type_builder(ctx.def_ids(), local_def_id.to_def_id()); Self { ctx, tcx, diff --git a/src/analyze/local_def.rs b/src/analyze/local_def.rs index 393c80d8..3169ac03 100644 --- a/src/analyze/local_def.rs +++ b/src/analyze/local_def.rs @@ -1185,7 +1185,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { let tcx = ctx.tcx; let body = tcx.optimized_mir(local_def_id.to_def_id()).clone(); let drop_points = Default::default(); - let type_builder = TypeBuilder::new(tcx, ctx.def_ids(), local_def_id.to_def_id()); + let type_builder = ctx.type_builder(ctx.def_ids(), local_def_id.to_def_id()); let generic_args = tcx.mk_args(&[]); Self { ctx, diff --git a/src/rty.rs b/src/rty.rs index 876dc02d..8f6f930e 100644 --- a/src/rty.rs +++ b/src/rty.rs @@ -729,7 +729,7 @@ impl EnumType { /// A type parameter. #[derive(Debug, Clone)] pub struct ParamType { - pub idx: TypeParamIdx, + idx: TypeParamIdx, } impl<'a, D> Pretty<'a, D, termcolor::ColorSpec> for &ParamType @@ -1034,7 +1034,7 @@ impl Type { // currently String sort seems not available in HORN logic of Z3 Type::String => chc::Sort::null(), Type::Never => chc::Sort::null(), - Type::Param(ty) => chc::Sort::param(ty.index().into()), + Type::Param(ty) => chc::Sort::forall(ty.index()), Type::Pointer(ty) => { let elem_sort = ty.elem.ty.to_sort(); diff --git a/src/rty/params.rs b/src/rty/params.rs index ef05138e..88e0bf4e 100644 --- a/src/rty/params.rs +++ b/src/rty/params.rs @@ -2,56 +2,57 @@ use std::collections::BTreeMap; -use pretty::{termcolor, Pretty}; +// use pretty::{termcolor, Pretty}; use rustc_index::IndexVec; use crate::chc; use super::{Closed, RefinedType, Type}; -rustc_index::newtype_index! { - /// An index representing a type parameter. - /// - /// ## Note on indexing of type parameters - /// - /// The index of [`rustc_middle::ty::ParamTy`] is based on all generic parameters in - /// the definition, including lifetimes. Given the following definition: - /// - /// ```rust - /// struct X<'a, T> { f: &'a T } - /// ``` - /// - /// The type of field `f` is `&T1` (not `&T0`) in MIR. However, in Thrust, we ignore lifetime - /// parameters and the index of [`rty::ParamType`](super::ParamType) is based on type parameters only, giving `f` - /// the type `&T0`. [`TypeBuilder`](crate::refine::TypeBuilder) takes care of this difference when translating MIR - /// types to Thrust types. - #[orderable] - #[debug_format = "T{}"] - pub struct TypeParamIdx { } -} - -impl std::fmt::Display for TypeParamIdx { - fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result { - write!(f, "T{}", self.index()) - } -} - -impl<'a, D> Pretty<'a, D, termcolor::ColorSpec> for &TypeParamIdx -where - D: pretty::DocAllocator<'a, termcolor::ColorSpec>, -{ - fn pretty(self, allocator: &'a D) -> pretty::DocBuilder<'a, D, termcolor::ColorSpec> { - allocator - .as_string(self) - .annotate(TypeParamIdx::color_spec()) - } -} - -impl TypeParamIdx { - fn color_spec() -> termcolor::ColorSpec { - termcolor::ColorSpec::new() - } -} +pub type TypeParamIdx = chc::ForallSortIdx; +// rustc_index::newtype_index! { +// /// An index representing a type parameter. +// /// +// /// ## Note on indexing of type parameters +// /// +// /// The index of [`rustc_middle::ty::ParamTy`] is based on all generic parameters in +// /// the definition, including lifetimes. Given the following definition: +// /// +// /// ```rust +// /// struct X<'a, T> { f: &'a T } +// /// ``` +// /// +// /// The type of field `f` is `&T1` (not `&T0`) in MIR. However, in Thrust, we ignore lifetime +// /// parameters and the index of [`rty::ParamType`](super::ParamType) is based on type parameters only, giving `f` +// /// the type `&T0`. [`TypeBuilder`](crate::refine::TypeBuilder) takes care of this difference when translating MIR +// /// types to Thrust types. +// #[orderable] +// #[debug_format = "T{}"] +// pub struct TypeParamIdx { } +// } + +// impl std::fmt::Display for TypeParamIdx { +// fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result { +// write!(f, "T{}", self.index()) +// } +// } + +// impl<'a, D> Pretty<'a, D, termcolor::ColorSpec> for &TypeParamIdx +// where +// D: pretty::DocAllocator<'a, termcolor::ColorSpec>, +// { +// fn pretty(self, allocator: &'a D) -> pretty::DocBuilder<'a, D, termcolor::ColorSpec> { +// allocator +// .as_string(self) +// .annotate(TypeParamIdx::color_spec()) +// } +// } + +// impl TypeParamIdx { +// fn color_spec() -> termcolor::ColorSpec { +// termcolor::ColorSpec::new() +// } +// } pub type RefinedTypeArgs = IndexVec>; pub type TypeArgs = IndexVec>; From debaa614289ab1185f025dc448599728620ac022 Mon Sep 17 00:00:00 2001 From: coeff-aij <175928954+coeff-aij@users.noreply.github.com> Date: Mon, 8 Jun 2026 12:00:48 +0900 Subject: [PATCH 04/55] change: use forall sort instead of deferred type --- src/analyze/crate_.rs | 13 +++---------- 1 file changed, 3 insertions(+), 10 deletions(-) diff --git a/src/analyze/crate_.rs b/src/analyze/crate_.rs index 74198f18..d5ed1f95 100644 --- a/src/analyze/crate_.rs +++ b/src/analyze/crate_.rs @@ -120,16 +120,9 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { }; use mir_ty::TypeVisitableExt as _; - if sig.has_param() { - // TODO: needs clear criteria on whether extern_spec'ed target fn is analyzed or not - if target_def_id.as_local().is_none_or(|def_id| { - self.skip_analysis.contains(&def_id) || !self.tcx.is_mir_available(def_id) - }) { - self.ctx - .register_deferred_def_without_analysis(target_def_id, local_def_id); - } else { - self.ctx.register_deferred_def(target_def_id, local_def_id); - } + if sig.has_param() && self.skip_analysis.contains(&local_def_id) { + self.ctx + .register_deferred_def_without_analysis(target_def_id, local_def_id); } else { let expected = analyzer.expected_ty(); self.ctx.register_def(target_def_id, expected); From 03d79322e23315923055ea664ef09a3dad0d0350 Mon Sep 17 00:00:00 2001 From: coeff-aij <175928954+coeff-aij@users.noreply.github.com> Date: Sun, 24 May 2026 21:49:11 +0900 Subject: [PATCH 05/55] add: output (define-forall-sort) --- src/chc/smtlib2.rs | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/chc/smtlib2.rs b/src/chc/smtlib2.rs index e8886ed6..617c1ac7 100644 --- a/src/chc/smtlib2.rs +++ b/src/chc/smtlib2.rs @@ -600,6 +600,10 @@ 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")?; + for forall_sort_idx in &self.inner.forall_sorts { + writeln!(f, "(declare-forall-sort {})\n", forall_sort_idx)?; + } + writeln!(f, "{}\n", Datatypes::new(&self.ctx, self.ctx.datatypes()))?; for datatype in self.ctx.datatypes() { writeln!(f, "{}", DatatypeDiscrFun::new(&self.ctx, datatype))?; From 0d47cc8377c266fe79ef8ea39cb2c2556827d386 Mon Sep 17 00:00:00 2001 From: coeff-aij <175928954+coeff-aij@users.noreply.github.com> Date: Sun, 24 May 2026 21:49:33 +0900 Subject: [PATCH 06/55] fix: duplication of ForallSortIdx for the same parameter --- src/refine/template.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/refine/template.rs b/src/refine/template.rs index 56fca463..37aa9a67 100644 --- a/src/refine/template.rs +++ b/src/refine/template.rs @@ -102,7 +102,7 @@ impl<'tcx> TypeBuilder<'tcx> { let mut type_params = self.type_params.borrow_mut(); let index = type_params .entry((self.def_id, ty.index)) - .or_insert(self.system.borrow_mut().new_forall_sort()); + .or_insert_with(|| self.system.borrow_mut().new_forall_sort()); rty::ParamType::new(*index).into() } From 4e35b61e73be3fcd125f11e4f1e73afae9513524 Mon Sep 17 00:00:00 2001 From: coeff-aij <175928954+coeff-aij@users.noreply.github.com> Date: Sun, 24 May 2026 22:53:26 +0900 Subject: [PATCH 07/55] add test cases using unknown type parameters with trait bounds --- tests/ui/pass/traits/simple_loop.rs | 28 ++++++++++++++++++++++++++++ 1 file changed, 28 insertions(+) create mode 100644 tests/ui/pass/traits/simple_loop.rs diff --git a/tests/ui/pass/traits/simple_loop.rs b/tests/ui/pass/traits/simple_loop.rs new file mode 100644 index 00000000..857ecdb3 --- /dev/null +++ b/tests/ui/pass/traits/simple_loop.rs @@ -0,0 +1,28 @@ +//@check-pass +//@compile-flags: -C debug-assertions=off +//@rustc-env: THRUST_SOLVER=tests/thrust-pcsat-wrapper THRUST_SOLVER_TIMEOUT_SECS=60 + +#[thrust_macros::context] +trait A { + #[thrust_macros::requires(Self::p(x))] + #[thrust_macros::ensures(Self::p(result))] + fn f(&self, x: i64) -> i64; + + #[thrust_macros::predicate] + fn p(x: i64) -> bool; +} + +#[thrust_macros::requires(T::p(x))] +#[thrust_macros::ensures(T::p(result))] +fn target(a: &T, x: i64) -> i64 { + let mut v = x; + let mut i = 0; + while i < 3 { + v = a.f(v); + i += 1; + } + + v +} + +fn main() {} From 2ef31cbcbb38c2c635adff3e73cdb71cdb5ca690 Mon Sep 17 00:00:00 2001 From: coeff-aij <175928954+coeff-aij@users.noreply.github.com> Date: Mon, 25 May 2026 22:19:14 +0900 Subject: [PATCH 08/55] change: use DeferredType for generic functions without requires/ensures conditions --- src/analyze/crate_.rs | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/analyze/crate_.rs b/src/analyze/crate_.rs index d5ed1f95..78114384 100644 --- a/src/analyze/crate_.rs +++ b/src/analyze/crate_.rs @@ -123,6 +123,9 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { if sig.has_param() && self.skip_analysis.contains(&local_def_id) { self.ctx .register_deferred_def_without_analysis(target_def_id, local_def_id); + } else if sig.has_param() && !analyzer.is_fully_annotated() { + self.ctx + .register_deferred_def(local_def_id); } else { let expected = analyzer.expected_ty(); self.ctx.register_def(target_def_id, expected); From f42debfbfbfc7d86f8045fe4c2f8c84eb6dc3e1f Mon Sep 17 00:00:00 2001 From: coeff-aij <175928954+coeff-aij@users.noreply.github.com> Date: Mon, 25 May 2026 22:53:52 +0900 Subject: [PATCH 09/55] change: prevent overwriting concrete types with deferred types --- src/analyze.rs | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/src/analyze.rs b/src/analyze.rs index 5148279c..a770c605 100644 --- a/src/analyze.rs +++ b/src/analyze.rs @@ -392,9 +392,8 @@ impl<'tcx> Analyzer<'tcx> { ?mode, "register_deferred_def" ); - self.defs.insert( - target_def_id, - DefTy::Deferred(DeferredDefTy { + self.defs.entry( target_def_id).or_insert_with( + || DefTy::Deferred(DeferredDefTy { local_def_id, cache: Rc::new(RefCell::new(HashMap::new())), mode, From 0a2cc1772c22e2a9f775b681c97fbab6d5be6698 Mon Sep 17 00:00:00 2001 From: coeff-aij <175928954+coeff-aij@users.noreply.github.com> Date: Tue, 26 May 2026 00:35:02 +0900 Subject: [PATCH 10/55] change: disable DeferredType completely --- src/analyze/crate_.rs | 16 +++++----------- 1 file changed, 5 insertions(+), 11 deletions(-) diff --git a/src/analyze/crate_.rs b/src/analyze/crate_.rs index 78114384..155e0bec 100644 --- a/src/analyze/crate_.rs +++ b/src/analyze/crate_.rs @@ -119,17 +119,8 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { local_def_id.to_def_id() }; - use mir_ty::TypeVisitableExt as _; - if sig.has_param() && self.skip_analysis.contains(&local_def_id) { - self.ctx - .register_deferred_def_without_analysis(target_def_id, local_def_id); - } else if sig.has_param() && !analyzer.is_fully_annotated() { - self.ctx - .register_deferred_def(local_def_id); - } else { - let expected = analyzer.expected_ty(); - self.ctx.register_def(target_def_id, expected); - } + let expected = analyzer.expected_ty(); + self.ctx.register_def(target_def_id, expected); } fn analyze_local_defs(&mut self) { @@ -138,11 +129,13 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { continue; }; if self.skip_analysis.contains(local_def_id) { + tracing::debug!("this is marked as skip analysis: {:?}", local_def_id); 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 + tracing::debug!("this is marked as deferred type: {:?}", local_def_id); continue; }; @@ -156,6 +149,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { .map(|ty_param| (ty_param, rty::RefinedType::unrefined(rty::Type::int()))) .collect(), ); + tracing::debug!("expected type of {:?} is {:#?}", local_def_id, expected); expected.subst_ty_params(&subst); let generic_args = self.placeholder_generic_args(*local_def_id); self.ctx From dc9b0e91334b4b7622bfbef8045d0838970ef8cd Mon Sep 17 00:00:00 2001 From: coeff-aij <175928954+coeff-aij@users.noreply.github.com> Date: Mon, 8 Jun 2026 12:04:25 +0900 Subject: [PATCH 11/55] remove all extern_spec in std.rs temporarily --- src/analyze.rs | 8 +- src/analyze/crate_.rs | 2 - std.rs | 814 +++++++++++++++++++++--------------------- 3 files changed, 411 insertions(+), 413 deletions(-) diff --git a/src/analyze.rs b/src/analyze.rs index a770c605..2545baff 100644 --- a/src/analyze.rs +++ b/src/analyze.rs @@ -392,13 +392,13 @@ impl<'tcx> Analyzer<'tcx> { ?mode, "register_deferred_def" ); - self.defs.entry( target_def_id).or_insert_with( - || DefTy::Deferred(DeferredDefTy { + self.defs.entry(target_def_id).or_insert_with(|| { + DefTy::Deferred(DeferredDefTy { local_def_id, cache: Rc::new(RefCell::new(HashMap::new())), mode, - }), - ); + }) + }); } pub fn concrete_def_ty(&self, def_id: DefId) -> Option<&rty::RefinedType> { diff --git a/src/analyze/crate_.rs b/src/analyze/crate_.rs index 155e0bec..fb7a01b3 100644 --- a/src/analyze/crate_.rs +++ b/src/analyze/crate_.rs @@ -69,8 +69,6 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { #[tracing::instrument(skip(self), fields(def_id = %self.tcx.def_path_str(local_def_id)))] fn refine_fn_def(&mut self, local_def_id: LocalDefId) { - let sig = self.ctx.fn_sig(local_def_id.to_def_id()); - let mut analyzer = self.ctx.local_def_analyzer(local_def_id); if analyzer.is_annotated_as_trusted() { diff --git a/std.rs b/std.rs index 132e3859..56aa2d06 100644 --- a/std.rs +++ b/std.rs @@ -333,410 +333,410 @@ mod thrust_models { } } -#[thrust::extern_spec_fn] -#[thrust_macros::requires(true)] -#[thrust_macros::ensures(result == thrust_models::model::Box::new(x))] -fn _extern_spec_box_new(x: T) -> Box where T: thrust_models::Model, T::Ty: PartialEq { - Box::new(x) -} - -#[thrust::extern_spec_fn] -#[thrust_macros::requires(true)] -#[thrust_macros::ensures(result == (x == y))] -fn _extern_spec_box_partialeq_eq(x: &Box, y: &Box) -> bool - where T: thrust_models::Model + PartialEq, T::Ty: PartialEq -{ - as PartialEq>::eq(x, y) -} - -#[thrust::extern_spec_fn] -#[thrust_macros::requires(true)] -#[thrust_macros::ensures(*x == !y && *y == !x)] -fn _extern_spec_std_mem_swap(x: &mut T, y: &mut T) where T: thrust_models::Model, T::Ty: PartialEq { - std::mem::swap(x, y) -} - -#[thrust::extern_spec_fn] -#[thrust_macros::requires(true)] -#[thrust_macros::ensures(!dest == src && result == *dest)] -fn _extern_spec_std_mem_replace(dest: &mut T, src: T) -> T where T: thrust_models::Model, T::Ty: PartialEq { - std::mem::replace(dest, src) -} - -#[thrust::extern_spec_fn] -#[thrust_macros::requires(true)] -#[thrust_macros::ensures(result == (x == y))] -fn _extern_spec_option_partialeq_eq(x: &Option, y: &Option) -> bool - where T: thrust_models::Model + PartialEq, T::Ty: PartialEq -{ - as PartialEq>::eq(x, y) -} - -#[thrust::extern_spec_fn] -#[thrust_macros::requires(opt != None)] -#[thrust_macros::ensures(Some(result) == opt)] -fn _extern_spec_option_unwrap(opt: Option) -> T where T: thrust_models::Model, T::Ty: PartialEq { - Option::unwrap(opt) -} - -#[thrust::extern_spec_fn] -#[thrust_macros::requires(true)] -#[thrust_macros::ensures( - (*opt == None && result == true) - || (*opt != None && result == false) -)] -fn _extern_spec_option_is_none(opt: &Option) -> bool where T: thrust_models::Model, T::Ty: PartialEq { - Option::is_none(opt) -} - -#[thrust::extern_spec_fn] -#[thrust_macros::requires(true)] -#[thrust_macros::ensures( - (*opt == None && result == false) - || (*opt != None && result == true) -)] -fn _extern_spec_option_is_some(opt: &Option) -> bool where T: thrust_models::Model, T::Ty: PartialEq { - Option::is_some(opt) -} - -#[thrust::extern_spec_fn] -#[thrust_macros::requires(true)] -#[thrust_macros::ensures( - (opt != None && Some(result) == opt) - || (opt == None && result == default) -)] -fn _extern_spec_option_unwrap_or(opt: Option, default: T) -> T where T: thrust_models::Model, T::Ty: PartialEq { - Option::unwrap_or(opt, default) -} - -#[thrust::extern_spec_fn] -#[thrust_macros::requires( - opt == None || thrust_models::exists(|i| opt == Some(i) && thrust_macros::pre!(f(i))) -)] -#[thrust_macros::ensures( - (opt == None && result == None) - || thrust_models::exists(|i| thrust_models::exists(|j| - opt == Some(i) && thrust_macros::post!(f(i), j) && result == Some(j))) -)] -fn _extern_spec_option_map(opt: Option, f: F) -> Option -where - T: thrust_models::Model, T::Ty: PartialEq, - U: thrust_models::Model, U::Ty: PartialEq, - F: FnOnce(T) -> U, -{ - Option::map(opt, f) -} - -#[thrust::extern_spec_fn] -#[thrust_macros::requires(opt != None || thrust_macros::pre!(f()))] -#[thrust_macros::ensures( - (opt != None && Some(result) == opt) - || (opt == None && thrust_macros::post!(f(), result)) -)] -fn _extern_spec_option_unwrap_or_else(opt: Option, f: F) -> T -where - T: thrust_models::Model, T::Ty: PartialEq, - F: FnOnce() -> T, -{ - Option::unwrap_or_else(opt, f) -} - -#[thrust::extern_spec_fn] -#[thrust_macros::requires(true)] -#[thrust_macros::ensures( - (thrust_models::exists(|x| opt == Some(x) && result == Ok(x))) - || (opt == None && result == Err(err)) -)] -fn _extern_spec_option_ok_or(opt: Option, err: E) -> Result - where T: thrust_models::Model, T::Ty: PartialEq, - E: thrust_models::Model, E::Ty: PartialEq, -{ - Option::ok_or(opt, err) -} - -#[thrust::extern_spec_fn] -#[thrust_macros::requires(true)] -#[thrust_macros::ensures(!opt == None && result == *opt)] -fn _extern_spec_option_take(opt: &mut Option) -> Option where T: thrust_models::Model, T::Ty: PartialEq { - Option::take(opt) -} - -#[thrust::extern_spec_fn] -#[thrust_macros::requires(true)] -#[thrust_macros::ensures(!opt == Some(src) && result == *opt)] -fn _extern_spec_option_replace(opt: &mut Option, src: T) -> Option - where T: thrust_models::Model, T::Ty: PartialEq -{ - Option::replace(opt, src) -} - -#[thrust::extern_spec_fn] -#[thrust_macros::requires(true)] -#[thrust_macros::ensures( - thrust_models::exists(|x| opt == &Some(x) && result == Some(&x)) - || (opt == &None && result == None) -)] -fn _extern_spec_option_as_ref(opt: &Option) -> Option<&T> where T: thrust_models::Model, T::Ty: PartialEq { - Option::as_ref(opt) -} - -#[thrust::extern_spec_fn] -#[thrust_macros::requires(true)] -#[thrust_macros::ensures( - thrust_models::exists(|x1, x2| - *opt == Some(x1) && - !opt == Some(x2) && - result == Some(thrust_models::model::Mut::new(x1, x2)) - ) - || ( - *opt == None && - !opt == None && - result == None - ) -)] -fn _extern_spec_option_as_mut(opt: &mut Option) -> Option<&mut T> - where T: thrust_models::Model, T::Ty: PartialEq -{ - Option::as_mut(opt) -} - -#[thrust::extern_spec_fn] -#[thrust_macros::requires(true)] -#[thrust_macros::ensures(result == (x == y))] -fn _extern_spec_result_partialeq_eq(x: &Result, y: &Result) -> bool - where T: thrust_models::Model + PartialEq, T::Ty: PartialEq, - E: thrust_models::Model + PartialEq, E::Ty: PartialEq, -{ - as PartialEq>::eq(x, y) -} - -#[thrust::extern_spec_fn] -#[thrust_macros::requires(thrust_models::exists(|x| res == Ok(x)))] -#[thrust_macros::ensures(Ok(result) == res)] -fn _extern_spec_result_unwrap(res: Result) -> T - where T: thrust_models::Model, T::Ty: PartialEq, - E: thrust_models::Model, E::Ty: PartialEq, -{ - Result::unwrap(res) -} - -#[thrust::extern_spec_fn] -#[thrust_macros::requires(thrust_models::exists(|x| res == Err(x)))] -#[thrust_macros::ensures(Err(result) == res)] -fn _extern_spec_result_unwrap_err(res: Result) -> E - where T: thrust_models::Model, T::Ty: PartialEq, - E: thrust_models::Model, E::Ty: PartialEq, -{ - Result::unwrap_err(res) -} - -#[thrust::extern_spec_fn] -#[thrust_macros::requires(true)] -#[thrust_macros::ensures( - thrust_models::exists(|x| res == Ok(x) && result == Some(x)) - || thrust_models::exists(|x| res == Err(x) && result == None) -)] -fn _extern_spec_result_ok(res: Result) -> Option - where T: thrust_models::Model, T::Ty: PartialEq, - E: thrust_models::Model, E::Ty: PartialEq, -{ - Result::ok(res) -} - -#[thrust::extern_spec_fn] -#[thrust_macros::requires(true)] -#[thrust_macros::ensures( - thrust_models::exists(|x| res == Ok(x) && result == None) - || thrust_models::exists(|x| res == Err(x) && result == Some(x)) -)] -fn _extern_spec_result_err(res: Result) -> Option - where T: thrust_models::Model, T::Ty: PartialEq, - E: thrust_models::Model, E::Ty: PartialEq, -{ - Result::err(res) -} - -#[thrust::extern_spec_fn] -#[thrust_macros::requires(true)] -#[thrust_macros::ensures( - thrust_models::exists(|x| *res == Ok(x) && result == true) - || thrust_models::exists(|x| *res == Err(x) && result == false) -)] -fn _extern_spec_result_is_ok(res: &Result) -> bool - where T: thrust_models::Model, T::Ty: PartialEq, - E: thrust_models::Model, E::Ty: PartialEq, -{ - Result::is_ok(res) -} - -#[thrust::extern_spec_fn] -#[thrust_macros::requires(true)] -#[thrust_macros::ensures( - thrust_models::exists(|x| *res == Ok(x) && result == false) - || thrust_models::exists(|x| *res == Err(x) && result == true) -)] -fn _extern_spec_result_is_err(res: &Result) -> bool - where T: thrust_models::Model, T::Ty: PartialEq, - E: thrust_models::Model, E::Ty: PartialEq, -{ - Result::is_err(res) -} - -#[thrust::extern_spec_fn] -#[thrust_macros::requires(true)] // TODO: require x != i32::MIN -#[thrust_macros::ensures(result >= 0 && (result == x || result == -x))] -fn _extern_spec_i32_abs(x: i32) -> i32 { - i32::abs(x) -} - -#[thrust::extern_spec_fn] -#[thrust_macros::requires(true)] -#[thrust_macros::ensures( - (x >= y && result == (x - y)) - || (x < y && result == (y - x)) -)] -fn _extern_spec_i32_abs_diff(x: i32, y: i32) -> u32 { - i32::abs_diff(x, y) -} - -#[thrust::extern_spec_fn] -#[thrust_macros::requires(true)] -#[thrust_macros::ensures((x == 0 && result == 0) || (x > 0 && result == 1) || (x < 0 && result == -1))] -fn _extern_spec_i32_signum(x: i32) -> i32 { - i32::signum(x) -} - -#[thrust::extern_spec_fn] -#[thrust_macros::requires(true)] -#[thrust_macros::ensures((x < 0 && result == false) || (x >= 0 && result == true))] -fn _extern_spec_i32_is_positive(x: i32) -> bool { - i32::is_positive(x) -} - -#[thrust::extern_spec_fn] -#[thrust_macros::requires(true)] -#[thrust_macros::ensures((x <= 0 && result == true) || (x > 0 && result == false))] -fn _extern_spec_i32_is_negative(x: i32) -> bool { - i32::is_negative(x) -} - -#[thrust::extern_spec_fn] -#[thrust_macros::requires(true)] -#[thrust_macros::ensures(result.1 == 0)] -fn _extern_spec_vec_new() -> Vec where T: thrust_models::Model, T::Ty: PartialEq { - Vec::::new() -} - -#[thrust::extern_spec_fn] -#[thrust_macros::requires(true)] -#[thrust_macros::ensures(!vec == thrust_models::model::Vec((*vec).0.store((*vec).1, elem), (*vec).1 + 1))] -fn _extern_spec_vec_push(vec: &mut Vec, elem: T) - where T: thrust_models::Model, T::Ty: PartialEq -{ - Vec::push(vec, elem) -} - -#[thrust::extern_spec_fn] -#[thrust_macros::requires(true)] -#[thrust_macros::ensures(result == vec.1)] -fn _extern_spec_vec_len(vec: &Vec) -> usize where T: thrust_models::Model, T::Ty: PartialEq { - Vec::len(vec) -} - -#[thrust::extern_spec_fn] -#[thrust_macros::requires(index < vec.1)] -#[thrust_macros::ensures(*result == vec.0[index])] -fn _extern_spec_vec_index(vec: &Vec, index: usize) -> &T where T: thrust_models::Model, T::Ty: PartialEq { - as std::ops::Index>::index(vec, index) -} - -#[thrust::extern_spec_fn] -#[thrust_macros::requires(index < (*vec).1)] -#[thrust_macros::ensures( - *result == (*vec).0[index] && - !result == (!vec).0[index] && - !vec == thrust_models::model::Vec((*vec).0.store(index, !result), (*vec).1) -)] -fn _extern_spec_vec_index_mut(vec: &mut Vec, index: usize) -> &mut T - where T: thrust_models::Model, T::Ty: PartialEq -{ - as std::ops::IndexMut>::index_mut(vec, index) -} - -#[thrust::extern_spec_fn] -#[thrust_macros::requires(true)] -#[thrust_macros::ensures((!vec).1 == 0)] -fn _extern_spec_vec_clear(vec: &mut Vec) where T: thrust_models::Model, T::Ty: PartialEq { - Vec::clear(vec) -} - -#[thrust::extern_spec_fn] -#[thrust_macros::requires(true)] -#[thrust_macros::ensures( - (!vec).0 == (*vec).0 && ( - ( - (*vec).1 > 0 && - (!vec).1 == (*vec).1 - 1 && - result == Some((*vec).0[(*vec).1 - 1]) - ) || ( - (*vec).1 == 0 && - (!vec).1 == 0 && - result == None - ) - ) -)] -fn _extern_spec_vec_pop(vec: &mut Vec) -> Option where T: thrust_models::Model, T::Ty: PartialEq { - Vec::pop(vec) -} - -#[thrust::extern_spec_fn] -#[thrust_macros::requires(true)] -#[thrust_macros::ensures(result == ((*vec).1 == 0))] -fn _extern_spec_vec_is_empty(vec: &Vec) -> bool where T: thrust_models::Model, T::Ty: PartialEq { - Vec::is_empty(vec) -} - -#[thrust::extern_spec_fn] -#[thrust_macros::requires(true)] -#[thrust_macros::ensures( - ( - (*vec).1 > len && - !vec == thrust_models::model::Vec((*vec).0, len) - ) || ( - (*vec).1 <= len && - !vec == *vec - ) -)] -fn _extern_spec_vec_truncate(vec: &mut Vec, len: usize) where T: thrust_models::Model, T::Ty: PartialEq { - Vec::truncate(vec, len) -} - -// TODO: The following specs of some trait methods are too restrictive; we should allow for a -// per-impl spec once we can describe the spec of blanket impls. - -#[thrust::extern_spec_fn] -#[thrust_macros::requires(true)] -#[thrust_macros::ensures(result == (*x == *y))] -fn _extern_spec_partialeq_eq(x: &T, y: &T) -> bool - where T: thrust_models::Model + PartialEq, T::Ty: PartialEq -{ - PartialEq::eq(x, y) -} - -#[thrust::extern_spec_fn] -#[thrust_macros::requires(true)] -#[thrust_macros::ensures(result == (*x < *y))] -fn _extern_spec_partialord_lt(x: &T, y: &T) -> bool - where T: thrust_models::Model + PartialOrd, T::Ty: PartialOrd -{ - PartialOrd::lt(x, y) -} - -#[thrust::extern_spec_fn] -#[thrust_macros::requires(true)] -#[thrust_macros::ensures(result == (*x > *y))] -fn _extern_spec_partialord_gt(x: &T, y: &T) -> bool - where T: thrust_models::Model + PartialOrd, T::Ty: PartialOrd -{ - PartialOrd::gt(x, y) -} +// #[thrust::extern_spec_fn] +// #[thrust_macros::requires(true)] +// #[thrust_macros::ensures(result == thrust_models::model::Box::new(x))] +// fn _extern_spec_box_new(x: T) -> Box where T: thrust_models::Model, T::Ty: PartialEq { +// Box::new(x) +// } + +// #[thrust::extern_spec_fn] +// #[thrust_macros::requires(true)] +// #[thrust_macros::ensures(result == (x == y))] +// fn _extern_spec_box_partialeq_eq(x: &Box, y: &Box) -> bool +// where T: thrust_models::Model + PartialEq, T::Ty: PartialEq +// { +// as PartialEq>::eq(x, y) +// } + +// #[thrust::extern_spec_fn] +// #[thrust_macros::requires(true)] +// #[thrust_macros::ensures(*x == !y && *y == !x)] +// fn _extern_spec_std_mem_swap(x: &mut T, y: &mut T) where T: thrust_models::Model, T::Ty: PartialEq { +// std::mem::swap(x, y) +// } + +// #[thrust::extern_spec_fn] +// #[thrust_macros::requires(true)] +// #[thrust_macros::ensures(!dest == src && result == *dest)] +// fn _extern_spec_std_mem_replace(dest: &mut T, src: T) -> T where T: thrust_models::Model, T::Ty: PartialEq { +// std::mem::replace(dest, src) +// } + +// #[thrust::extern_spec_fn] +// #[thrust_macros::requires(true)] +// #[thrust_macros::ensures(result == (x == y))] +// fn _extern_spec_option_partialeq_eq(x: &Option, y: &Option) -> bool +// where T: thrust_models::Model + PartialEq, T::Ty: PartialEq +// { +// as PartialEq>::eq(x, y) +// } + +// #[thrust::extern_spec_fn] +// #[thrust_macros::requires(opt != None)] +// #[thrust_macros::ensures(Some(result) == opt)] +// fn _extern_spec_option_unwrap(opt: Option) -> T where T: thrust_models::Model, T::Ty: PartialEq { +// Option::unwrap(opt) +// } + +// #[thrust::extern_spec_fn] +// #[thrust_macros::requires(true)] +// #[thrust_macros::ensures( +// (*opt == None && result == true) +// || (*opt != None && result == false) +// )] +// fn _extern_spec_option_is_none(opt: &Option) -> bool where T: thrust_models::Model, T::Ty: PartialEq { +// Option::is_none(opt) +// } + +// #[thrust::extern_spec_fn] +// #[thrust_macros::requires(true)] +// #[thrust_macros::ensures( +// (*opt == None && result == false) +// || (*opt != None && result == true) +// )] +// fn _extern_spec_option_is_some(opt: &Option) -> bool where T: thrust_models::Model, T::Ty: PartialEq { +// Option::is_some(opt) +// } + +// #[thrust::extern_spec_fn] +// #[thrust_macros::requires(true)] +// #[thrust_macros::ensures( +// (opt != None && Some(result) == opt) +// || (opt == None && result == default) +// )] +// fn _extern_spec_option_unwrap_or(opt: Option, default: T) -> T where T: thrust_models::Model, T::Ty: PartialEq { +// Option::unwrap_or(opt, default) +// } + +// #[thrust::extern_spec_fn] +// #[thrust_macros::requires( +// opt == None || thrust_models::exists(|i| opt == Some(i) && thrust_macros::pre!(f(i))) +// )] +// #[thrust_macros::ensures( +// (opt == None && result == None) +// || thrust_models::exists(|i| thrust_models::exists(|j| +// opt == Some(i) && thrust_macros::post!(f(i), j) && result == Some(j))) +// )] +// fn _extern_spec_option_map(opt: Option, f: F) -> Option +// where +// T: thrust_models::Model, T::Ty: PartialEq, +// U: thrust_models::Model, U::Ty: PartialEq, +// F: FnOnce(T) -> U, +// { +// Option::map(opt, f) +// } + +// #[thrust::extern_spec_fn] +// #[thrust_macros::requires(opt != None || thrust_macros::pre!(f()))] +// #[thrust_macros::ensures( +// (opt != None && Some(result) == opt) +// || (opt == None && thrust_macros::post!(f(), result)) +// )] +// fn _extern_spec_option_unwrap_or_else(opt: Option, f: F) -> T +// where +// T: thrust_models::Model, T::Ty: PartialEq, +// F: FnOnce() -> T, +// { +// Option::unwrap_or_else(opt, f) +// } + +// #[thrust::extern_spec_fn] +// #[thrust_macros::requires(true)] +// #[thrust_macros::ensures( +// (thrust_models::exists(|x| opt == Some(x) && result == Ok(x))) +// || (opt == None && result == Err(err)) +// )] +// fn _extern_spec_option_ok_or(opt: Option, err: E) -> Result +// where T: thrust_models::Model, T::Ty: PartialEq, +// E: thrust_models::Model, E::Ty: PartialEq, +// { +// Option::ok_or(opt, err) +// } + +// #[thrust::extern_spec_fn] +// #[thrust_macros::requires(true)] +// #[thrust_macros::ensures(!opt == None && result == *opt)] +// fn _extern_spec_option_take(opt: &mut Option) -> Option where T: thrust_models::Model, T::Ty: PartialEq { +// Option::take(opt) +// } + +// #[thrust::extern_spec_fn] +// #[thrust_macros::requires(true)] +// #[thrust_macros::ensures(!opt == Some(src) && result == *opt)] +// fn _extern_spec_option_replace(opt: &mut Option, src: T) -> Option +// where T: thrust_models::Model, T::Ty: PartialEq +// { +// Option::replace(opt, src) +// } + +// #[thrust::extern_spec_fn] +// #[thrust_macros::requires(true)] +// #[thrust_macros::ensures( +// thrust_models::exists(|x| opt == &Some(x) && result == Some(&x)) +// || (opt == &None && result == None) +// )] +// fn _extern_spec_option_as_ref(opt: &Option) -> Option<&T> where T: thrust_models::Model, T::Ty: PartialEq { +// Option::as_ref(opt) +// } + +// #[thrust::extern_spec_fn] +// #[thrust_macros::requires(true)] +// #[thrust_macros::ensures( +// thrust_models::exists(|x1, x2| +// *opt == Some(x1) && +// !opt == Some(x2) && +// result == Some(thrust_models::model::Mut::new(x1, x2)) +// ) +// || ( +// *opt == None && +// !opt == None && +// result == None +// ) +// )] +// fn _extern_spec_option_as_mut(opt: &mut Option) -> Option<&mut T> +// where T: thrust_models::Model, T::Ty: PartialEq +// { +// Option::as_mut(opt) +// } + +// #[thrust::extern_spec_fn] +// #[thrust_macros::requires(true)] +// #[thrust_macros::ensures(result == (x == y))] +// fn _extern_spec_result_partialeq_eq(x: &Result, y: &Result) -> bool +// where T: thrust_models::Model + PartialEq, T::Ty: PartialEq, +// E: thrust_models::Model + PartialEq, E::Ty: PartialEq, +// { +// as PartialEq>::eq(x, y) +// } + +// #[thrust::extern_spec_fn] +// #[thrust_macros::requires(thrust_models::exists(|x| res == Ok(x)))] +// #[thrust_macros::ensures(Ok(result) == res)] +// fn _extern_spec_result_unwrap(res: Result) -> T +// where T: thrust_models::Model, T::Ty: PartialEq, +// E: thrust_models::Model, E::Ty: PartialEq, +// { +// Result::unwrap(res) +// } + +// #[thrust::extern_spec_fn] +// #[thrust_macros::requires(thrust_models::exists(|x| res == Err(x)))] +// #[thrust_macros::ensures(Err(result) == res)] +// fn _extern_spec_result_unwrap_err(res: Result) -> E +// where T: thrust_models::Model, T::Ty: PartialEq, +// E: thrust_models::Model, E::Ty: PartialEq, +// { +// Result::unwrap_err(res) +// } + +// #[thrust::extern_spec_fn] +// #[thrust_macros::requires(true)] +// #[thrust_macros::ensures( +// thrust_models::exists(|x| res == Ok(x) && result == Some(x)) +// || thrust_models::exists(|x| res == Err(x) && result == None) +// )] +// fn _extern_spec_result_ok(res: Result) -> Option +// where T: thrust_models::Model, T::Ty: PartialEq, +// E: thrust_models::Model, E::Ty: PartialEq, +// { +// Result::ok(res) +// } + +// #[thrust::extern_spec_fn] +// #[thrust_macros::requires(true)] +// #[thrust_macros::ensures( +// thrust_models::exists(|x| res == Ok(x) && result == None) +// || thrust_models::exists(|x| res == Err(x) && result == Some(x)) +// )] +// fn _extern_spec_result_err(res: Result) -> Option +// where T: thrust_models::Model, T::Ty: PartialEq, +// E: thrust_models::Model, E::Ty: PartialEq, +// { +// Result::err(res) +// } + +// #[thrust::extern_spec_fn] +// #[thrust_macros::requires(true)] +// #[thrust_macros::ensures( +// thrust_models::exists(|x| *res == Ok(x) && result == true) +// || thrust_models::exists(|x| *res == Err(x) && result == false) +// )] +// fn _extern_spec_result_is_ok(res: &Result) -> bool +// where T: thrust_models::Model, T::Ty: PartialEq, +// E: thrust_models::Model, E::Ty: PartialEq, +// { +// Result::is_ok(res) +// } + +// #[thrust::extern_spec_fn] +// #[thrust_macros::requires(true)] +// #[thrust_macros::ensures( +// thrust_models::exists(|x| *res == Ok(x) && result == false) +// || thrust_models::exists(|x| *res == Err(x) && result == true) +// )] +// fn _extern_spec_result_is_err(res: &Result) -> bool +// where T: thrust_models::Model, T::Ty: PartialEq, +// E: thrust_models::Model, E::Ty: PartialEq, +// { +// Result::is_err(res) +// } + +// #[thrust::extern_spec_fn] +// #[thrust_macros::requires(true)] // TODO: require x != i32::MIN +// #[thrust_macros::ensures(result >= 0 && (result == x || result == -x))] +// fn _extern_spec_i32_abs(x: i32) -> i32 { +// i32::abs(x) +// } + +// #[thrust::extern_spec_fn] +// #[thrust_macros::requires(true)] +// #[thrust_macros::ensures( +// (x >= y && result == (x - y)) +// || (x < y && result == (y - x)) +// )] +// fn _extern_spec_i32_abs_diff(x: i32, y: i32) -> u32 { +// i32::abs_diff(x, y) +// } + +// #[thrust::extern_spec_fn] +// #[thrust_macros::requires(true)] +// #[thrust_macros::ensures((x == 0 && result == 0) || (x > 0 && result == 1) || (x < 0 && result == -1))] +// fn _extern_spec_i32_signum(x: i32) -> i32 { +// i32::signum(x) +// } + +// #[thrust::extern_spec_fn] +// #[thrust_macros::requires(true)] +// #[thrust_macros::ensures((x < 0 && result == false) || (x >= 0 && result == true))] +// fn _extern_spec_i32_is_positive(x: i32) -> bool { +// i32::is_positive(x) +// } + +// #[thrust::extern_spec_fn] +// #[thrust_macros::requires(true)] +// #[thrust_macros::ensures((x <= 0 && result == true) || (x > 0 && result == false))] +// fn _extern_spec_i32_is_negative(x: i32) -> bool { +// i32::is_negative(x) +// } + +// #[thrust::extern_spec_fn] +// #[thrust_macros::requires(true)] +// #[thrust_macros::ensures(result.1 == 0)] +// fn _extern_spec_vec_new() -> Vec where T: thrust_models::Model, T::Ty: PartialEq { +// Vec::::new() +// } + +// #[thrust::extern_spec_fn] +// #[thrust_macros::requires(true)] +// #[thrust_macros::ensures(!vec == thrust_models::model::Vec((*vec).0.store((*vec).1, elem), (*vec).1 + 1))] +// fn _extern_spec_vec_push(vec: &mut Vec, elem: T) +// where T: thrust_models::Model, T::Ty: PartialEq +// { +// Vec::push(vec, elem) +// } + +// #[thrust::extern_spec_fn] +// #[thrust_macros::requires(true)] +// #[thrust_macros::ensures(result == vec.1)] +// fn _extern_spec_vec_len(vec: &Vec) -> usize where T: thrust_models::Model, T::Ty: PartialEq { +// Vec::len(vec) +// } + +// #[thrust::extern_spec_fn] +// #[thrust_macros::requires(index < vec.1)] +// #[thrust_macros::ensures(*result == vec.0[index])] +// fn _extern_spec_vec_index(vec: &Vec, index: usize) -> &T where T: thrust_models::Model, T::Ty: PartialEq { +// as std::ops::Index>::index(vec, index) +// } + +// #[thrust::extern_spec_fn] +// #[thrust_macros::requires(index < (*vec).1)] +// #[thrust_macros::ensures( +// *result == (*vec).0[index] && +// !result == (!vec).0[index] && +// !vec == thrust_models::model::Vec((*vec).0.store(index, !result), (*vec).1) +// )] +// fn _extern_spec_vec_index_mut(vec: &mut Vec, index: usize) -> &mut T +// where T: thrust_models::Model, T::Ty: PartialEq +// { +// as std::ops::IndexMut>::index_mut(vec, index) +// } + +// #[thrust::extern_spec_fn] +// #[thrust_macros::requires(true)] +// #[thrust_macros::ensures((!vec).1 == 0)] +// fn _extern_spec_vec_clear(vec: &mut Vec) where T: thrust_models::Model, T::Ty: PartialEq { +// Vec::clear(vec) +// } + +// #[thrust::extern_spec_fn] +// #[thrust_macros::requires(true)] +// #[thrust_macros::ensures( +// (!vec).0 == (*vec).0 && ( +// ( +// (*vec).1 > 0 && +// (!vec).1 == (*vec).1 - 1 && +// result == Some((*vec).0[(*vec).1 - 1]) +// ) || ( +// (*vec).1 == 0 && +// (!vec).1 == 0 && +// result == None +// ) +// ) +// )] +// fn _extern_spec_vec_pop(vec: &mut Vec) -> Option where T: thrust_models::Model, T::Ty: PartialEq { +// Vec::pop(vec) +// } + +// #[thrust::extern_spec_fn] +// #[thrust_macros::requires(true)] +// #[thrust_macros::ensures(result == ((*vec).1 == 0))] +// fn _extern_spec_vec_is_empty(vec: &Vec) -> bool where T: thrust_models::Model, T::Ty: PartialEq { +// Vec::is_empty(vec) +// } + +// #[thrust::extern_spec_fn] +// #[thrust_macros::requires(true)] +// #[thrust_macros::ensures( +// ( +// (*vec).1 > len && +// !vec == thrust_models::model::Vec((*vec).0, len) +// ) || ( +// (*vec).1 <= len && +// !vec == *vec +// ) +// )] +// fn _extern_spec_vec_truncate(vec: &mut Vec, len: usize) where T: thrust_models::Model, T::Ty: PartialEq { +// Vec::truncate(vec, len) +// } + +// // TODO: The following specs of some trait methods are too restrictive; we should allow for a +// // per-impl spec once we can describe the spec of blanket impls. + +// #[thrust::extern_spec_fn] +// #[thrust_macros::requires(true)] +// #[thrust_macros::ensures(result == (*x == *y))] +// fn _extern_spec_partialeq_eq(x: &T, y: &T) -> bool +// where T: thrust_models::Model + PartialEq, T::Ty: PartialEq +// { +// PartialEq::eq(x, y) +// } + +// #[thrust::extern_spec_fn] +// #[thrust_macros::requires(true)] +// #[thrust_macros::ensures(result == (*x < *y))] +// fn _extern_spec_partialord_lt(x: &T, y: &T) -> bool +// where T: thrust_models::Model + PartialOrd, T::Ty: PartialOrd +// { +// PartialOrd::lt(x, y) +// } + +// #[thrust::extern_spec_fn] +// #[thrust_macros::requires(true)] +// #[thrust_macros::ensures(result == (*x > *y))] +// fn _extern_spec_partialord_gt(x: &T, y: &T) -> bool +// where T: thrust_models::Model + PartialOrd, T::Ty: PartialOrd +// { +// PartialOrd::gt(x, y) +// } From 6d82bfbded4dc45d8d18466af7a35fd9c88f61e6 Mon Sep 17 00:00:00 2001 From: coeff-aij <175928954+coeff-aij@users.noreply.github.com> Date: Mon, 8 Jun 2026 12:09:21 +0900 Subject: [PATCH 12/55] add: imcomplete support for alias types --- src/analyze.rs | 13 ++++++++++--- src/refine/template.rs | 17 +++++++++++++---- 2 files changed, 23 insertions(+), 7 deletions(-) diff --git a/src/analyze.rs b/src/analyze.rs index 2545baff..2ba4a983 100644 --- a/src/analyze.rs +++ b/src/analyze.rs @@ -8,6 +8,7 @@ use std::cell::RefCell; use std::collections::HashMap; +use std::hash::Hash; use std::rc::Rc; use rustc_hir::lang_items::LangItem; @@ -19,7 +20,7 @@ use rustc_span::Symbol; use crate::analyze; use crate::annot::{AnnotFormula, AnnotParser, Resolver}; -use crate::chc; +use crate::chc::{self, ForallSortIdx}; use crate::pretty::PrettyDisplayExt as _; use crate::refine::{self, BasicBlockType, TypeBuilder}; use crate::rty; @@ -197,7 +198,13 @@ impl refine::EnumDefProvider for Rc> { } pub type Env = refine::Env>>; -pub type TypeParams = HashMap<(DefId, u32), chc::ForallSortIdx>; +pub type TypeParamMap = HashMap; + +#[derive(Eq, PartialEq, Hash)] +pub enum TypeParam { + GenericType(DefId, u32), + AssocType(DefId), +} #[derive(Debug, Clone)] struct DeferredFormulaFnDef<'tcx> { @@ -226,7 +233,7 @@ pub struct Analyzer<'tcx> { enum_defs: Rc>, - type_params: Rc>, + type_params: Rc>, } impl<'tcx> crate::refine::TemplateRegistry for Analyzer<'tcx> { diff --git a/src/refine/template.rs b/src/refine/template.rs index 37aa9a67..ccbf8761 100644 --- a/src/refine/template.rs +++ b/src/refine/template.rs @@ -8,7 +8,7 @@ use rustc_middle::ty as mir_ty; use rustc_span::def_id::DefId; use super::basic_block::BasicBlockType; -use crate::analyze::{DefIdCache, TypeParams}; +use crate::analyze::{DefIdCache, TypeParam, TypeParamMap}; use crate::chc; use crate::refine; use crate::rty; @@ -75,7 +75,7 @@ pub struct TypeBuilder<'tcx> { def_ids: DefIdCache<'tcx>, def_id: DefId, typing_env: mir_ty::TypingEnv<'tcx>, - type_params: Rc>, + type_params: Rc>, system: Rc>, } @@ -84,7 +84,7 @@ impl<'tcx> TypeBuilder<'tcx> { tcx: mir_ty::TyCtxt<'tcx>, def_ids: DefIdCache<'tcx>, def_id: DefId, - type_params: Rc>, + type_params: Rc>, system: Rc>, ) -> Self { let typing_env = mir_ty::TypingEnv::post_analysis(tcx, def_id); @@ -101,7 +101,15 @@ impl<'tcx> TypeBuilder<'tcx> { fn translate_param_type(&self, ty: &mir_ty::ParamTy) -> rty::Type { let mut type_params = self.type_params.borrow_mut(); let index = type_params - .entry((self.def_id, ty.index)) + .entry(TypeParam::GenericType(self.def_id, ty.index)) + .or_insert_with(|| self.system.borrow_mut().new_forall_sort()); + rty::ParamType::new(*index).into() + } + + fn translate_alias_type(&self, ty: &mir_ty::AliasTy) -> rty::Type { + let mut type_params = self.type_params.borrow_mut(); + let index = type_params + .entry(TypeParam::AssocType(ty.def_id)) .or_insert_with(|| self.system.borrow_mut().new_forall_sort()); rty::ParamType::new(*index).into() } @@ -254,6 +262,7 @@ impl<'tcx> TypeBuilder<'tcx> { unimplemented!("unsupported ADT: {:?}", ty); } } + mir_ty::TyKind::Alias(_, ty) => self.translate_alias_type(ty), kind => unimplemented!("unrefined_ty: {:?}", kind), } } From a0df8dc4cf8c6bd26162e8b33ddfbf9cb0ea44d4 Mon Sep 17 00:00:00 2001 From: coeff-aij <175928954+coeff-aij@users.noreply.github.com> Date: Wed, 27 May 2026 14:15:33 +0900 Subject: [PATCH 13/55] change: use Type::Param and chc::Sort::Forall for type prameters constrained with trait bounds --- src/analyze/crate_.rs | 20 +++++--------------- src/rty/subtyping.rs | 3 ++- 2 files changed, 7 insertions(+), 16 deletions(-) diff --git a/src/analyze/crate_.rs b/src/analyze/crate_.rs index fb7a01b3..5fe2769f 100644 --- a/src/analyze/crate_.rs +++ b/src/analyze/crate_.rs @@ -8,7 +8,7 @@ use rustc_span::def_id::LocalDefId; use crate::analyze; use crate::chc; -use crate::rty::{self, ClauseBuilderExt as _}; +use crate::rty::ClauseBuilderExt as _; /// An implementation of local crate analysis. /// @@ -139,16 +139,8 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { // check polymorphic function def by replacing type params with some opaque type // (and this is no-op if the function is mono) - let mut expected = expected.clone(); - let subst = rty::TypeParamSubst::new( - expected - .free_ty_params() - .into_iter() - .map(|ty_param| (ty_param, rty::RefinedType::unrefined(rty::Type::int()))) - .collect(), - ); + let expected = expected.clone(); tracing::debug!("expected type of {:?} is {:#?}", local_def_id, expected); - expected.subst_ty_params(&subst); let generic_args = self.placeholder_generic_args(*local_def_id); self.ctx .local_def_analyzer(*local_def_id) @@ -187,12 +179,10 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { let arg = match param.kind { mir_ty::GenericParamDefKind::Type { .. } => { if constrained_params.contains(¶m.index) { - panic!( - "unable to check generic function with constrained type parameter: {}", - self.tcx.def_path_str(local_def_id) - ); + mir_ty::Ty::new_param(self.tcx, param.index, param.name).into() + } else { + self.tcx.types.i32.into() } - self.tcx.types.i32.into() } mir_ty::GenericParamDefKind::Const { .. } => { unimplemented!() diff --git a/src/rty/subtyping.rs b/src/rty/subtyping.rs index 03477f02..1f015342 100644 --- a/src/rty/subtyping.rs +++ b/src/rty/subtyping.rs @@ -73,7 +73,8 @@ where (Type::Int, Type::Int) | (Type::Bool, Type::Bool) | (Type::String, Type::String) - | (Type::Never, Type::Never) => {} + | (Type::Never, Type::Never) + | (Type::Param(_), Type::Param(_)) => {} (Type::Enum(got), Type::Enum(expected)) if got.symbol() == expected.symbol() => { for (got_ty, expected_ty) in got.args.iter().zip(expected.args.iter()) { let cs = self.relate_sub_refined_type(got_ty, expected_ty); From 85d9e0192dbcfe6d97d09fb20012660bee42e554 Mon Sep 17 00:00:00 2001 From: coeff-aij <175928954+coeff-aij@users.noreply.github.com> Date: Wed, 27 May 2026 14:21:21 +0900 Subject: [PATCH 14/55] add: ForallPred represents unresolved user-defined predicates --- src/chc.rs | 40 ++++++++++++++++++++++++++++++++++++++++ src/chc/unbox.rs | 1 + 2 files changed, 41 insertions(+) diff --git a/src/chc.rs b/src/chc.rs index 3d32d7c4..88e354da 100644 --- a/src/chc.rs +++ b/src/chc.rs @@ -1044,6 +1044,32 @@ impl UserDefinedPred { } } +#[derive(Debug, Clone, PartialEq, Eq, Hash)] +pub struct ForallPred { + inner: String, +} + +impl std::fmt::Display for ForallPred { + fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result { + self.inner.fmt(f) + } +} + +impl<'a, D> Pretty<'a, D, termcolor::ColorSpec> for &ForallPred +where + D: pretty::DocAllocator<'a, termcolor::ColorSpec>, +{ + fn pretty(self, allocator: &'a D) -> pretty::DocBuilder<'a, D, termcolor::ColorSpec> { + allocator.text(self.inner.clone()) + } +} + +impl ForallPred { + pub fn new(inner: String) -> Self { + Self { inner } + } +} + /// A predicate. #[derive(Debug, Clone, PartialEq, Eq, Hash)] pub enum Pred { @@ -1051,6 +1077,7 @@ pub enum Pred { Var(PredVarId), Matcher(MatcherPred), UserDefined(UserDefinedPred), + ForallPred(ForallPred), } impl std::fmt::Display for Pred { @@ -1060,6 +1087,7 @@ impl std::fmt::Display for Pred { Pred::Var(p) => p.fmt(f), Pred::Matcher(p) => p.fmt(f), Pred::UserDefined(p) => p.fmt(f), + Pred::ForallPred(p) => p.fmt(f), } } } @@ -1075,6 +1103,7 @@ where Pred::Var(p) => p.pretty(allocator), Pred::Matcher(p) => p.pretty(allocator), Pred::UserDefined(p) => p.pretty(allocator), + Pred::ForallPred(p) => p.pretty(allocator), } } } @@ -1103,6 +1132,12 @@ impl From for Pred { } } +impl From for Pred { + fn from(p: ForallPred) -> Self { + Pred::ForallPred(p) + } +} + impl Pred { pub fn name(&self) -> std::borrow::Cow<'static, str> { match self { @@ -1110,6 +1145,7 @@ impl Pred { Pred::Var(p) => p.to_string().into(), Pred::Matcher(p) => p.name().into(), Pred::UserDefined(p) => p.to_string().into(), + Pred::ForallPred(p) => p.to_string().into(), } } @@ -1119,6 +1155,7 @@ impl Pred { Pred::Var(_) => false, Pred::Matcher(_) => false, Pred::UserDefined(_) => false, + Pred::ForallPred(_) => false, } } @@ -1128,6 +1165,7 @@ impl Pred { Pred::Var(_) => false, Pred::Matcher(_) => false, Pred::UserDefined(_) => false, + Pred::ForallPred(_) => false, } } @@ -1137,6 +1175,7 @@ impl Pred { Pred::Var(_) => false, Pred::Matcher(_) => false, Pred::UserDefined(_) => false, + Pred::ForallPred(_) => false, } } @@ -1146,6 +1185,7 @@ impl Pred { Pred::Var(_) => false, Pred::Matcher(_) => false, Pred::UserDefined(_) => false, + Pred::ForallPred(_) => false, } } } diff --git a/src/chc/unbox.rs b/src/chc/unbox.rs index 08d36c4e..edf3f854 100644 --- a/src/chc/unbox.rs +++ b/src/chc/unbox.rs @@ -43,6 +43,7 @@ fn unbox_pred(pred: Pred) -> Pred { Pred::Var(pred) => Pred::Var(pred), Pred::Matcher(pred) => unbox_matcher_pred(pred), Pred::UserDefined(pred) => Pred::UserDefined(pred), + Pred::ForallPred(pred) => Pred::ForallPred(pred), } } From 4d381fc7933bfcae1061ba38e08b219b202d3a2c Mon Sep 17 00:00:00 2001 From: coeff-aij <175928954+coeff-aij@users.noreply.github.com> Date: Wed, 27 May 2026 14:22:22 +0900 Subject: [PATCH 15/55] change: replace unresolved user-defined predicates with ForallPred --- src/analyze/annot_fn.rs | 58 +++++++++++++++++++++++++++++------------ src/refine.rs | 13 ++++++--- 2 files changed, 50 insertions(+), 21 deletions(-) diff --git a/src/analyze/annot_fn.rs b/src/analyze/annot_fn.rs index 2bbbe673..ca78a99e 100644 --- a/src/analyze/annot_fn.rs +++ b/src/analyze/annot_fn.rs @@ -3,7 +3,7 @@ use std::collections::HashMap; use pretty::{termcolor, Pretty}; use rustc_hir::{def_id::LocalDefId, HirId}; use rustc_index::IndexVec; -use rustc_middle::ty::{self as mir_ty, TyCtxt}; +use rustc_middle::ty::{self as mir_ty, TyCtxt, TypeFoldable}; use crate::analyze::{self, did_cache::DefIdCache}; use crate::annot::AnnotFormula; @@ -219,29 +219,48 @@ impl<'a, 'tcx> AnnotFnTranslator<'a, 'tcx> { } } + fn instantiate_generics( + &self, + ty: T, + generic_args: mir_ty::GenericArgsRef<'tcx>, + ) -> Option + where + T: TypeFoldable>, + { + if !self.generic_args.is_empty() { + Some(mir_ty::EarlyBinder::bind(ty).instantiate(self.tcx, generic_args)) + } else { + None + } + } + fn expr_ty(&self, expr: &'tcx rustc_hir::Expr<'tcx>) -> mir_ty::Ty<'tcx> { let ty = self.typeck.expr_ty(expr); - let instantiated = mir_ty::EarlyBinder::bind(ty).instantiate(self.tcx, self.generic_args); + let instantiated = self + .instantiate_generics(ty, self.generic_args) + .unwrap_or(ty); let typing_env = mir_ty::TypingEnv::fully_monomorphized(); self.tcx.normalize_erasing_regions(typing_env, instantiated) } fn pat_ty(&self, pat: &'tcx rustc_hir::Pat<'tcx>) -> mir_ty::Ty<'tcx> { let ty = self.typeck.pat_ty(pat); - let instantiated = mir_ty::EarlyBinder::bind(ty).instantiate(self.tcx, self.generic_args); + let instantiated = self + .instantiate_generics(ty, self.generic_args) + .unwrap_or(ty); let typing_env = mir_ty::TypingEnv::fully_monomorphized(); self.tcx.normalize_erasing_regions(typing_env, instantiated) } pub fn to_formula_fn(&self) -> FormulaFn<'tcx> { let formula = self.to_formula(self.body.value); - let params = self - .tcx - .fn_sig(self.local_def_id.to_def_id()) - .instantiate(self.tcx, self.generic_args) - .skip_binder() - .inputs() - .to_vec(); + let fn_sig = self.tcx.fn_sig(self.local_def_id.to_def_id()); + let binder = if self.generic_args.is_empty() { + fn_sig.skip_binder() + } else { + fn_sig.instantiate(self.tcx, self.generic_args) + }; + let params = binder.skip_binder().inputs().to_vec(); FormulaFn { params: IndexVec::from_raw(params), formula, @@ -630,8 +649,12 @@ impl<'a, 'tcx> AnnotFnTranslator<'a, 'tcx> { outer_generic_args = ?self.generic_args, "resolving predicate call in formula" ); - let generic_args = mir_ty::EarlyBinder::bind(generic_args) - .instantiate(self.tcx, self.generic_args); + let (is_unresolved_args, generic_args) = + match self.instantiate_generics(generic_args, self.generic_args) { + Some(args) => (false, args), + None => (true, generic_args), + }; + let instance = mir_ty::Instance::try_resolve( self.tcx, typing_env, @@ -639,14 +662,15 @@ impl<'a, 'tcx> AnnotFnTranslator<'a, 'tcx> { generic_args, ) .unwrap(); - let pred_def_id = if let Some(instance) = instance { - instance.def_id() + let pred_def_id = instance.map_or(def_id, |instance| instance.def_id()); + + let pred = if is_unresolved_args { + refine::user_defined_pred(self.tcx, pred_def_id).into() } else { - def_id + refine::forall_pred(self.tcx, pred_def_id).into() }; - let pred = refine::user_defined_pred(self.tcx, pred_def_id); let arg_terms = args.iter().map(|e| self.to_term(e)).collect(); - let atom = chc::Atom::new(pred.into(), arg_terms); + let atom = chc::Atom::new(pred, arg_terms); return FormulaOrTerm::Formula(chc::Formula::Atom(atom)); } } diff --git a/src/refine.rs b/src/refine.rs index 5a1fd8d3..cbbd37c4 100644 --- a/src/refine.rs +++ b/src/refine.rs @@ -18,15 +18,16 @@ pub use env::{ Assumption, EnumDefProvider, Env, PlaceType, PlaceTypeBuilder, PlaceTypeVar, TempVarIdx, Var, }; -use crate::chc::{DatatypeSymbol, UserDefinedPred}; +use crate::chc::{DatatypeSymbol, ForallPred, UserDefinedPred}; use rustc_middle::ty as mir_ty; use rustc_span::def_id::DefId; -fn stable_def_id_symbol(tcx: mir_ty::TyCtxt<'_>, did: DefId) -> String { +fn stable_def_id_symbol(tcx: mir_ty::TyCtxt<'_>, did: DefId, prefix: &str) -> String { let hash = tcx.def_path_hash(did); let path = tcx.def_path(did); if let Some(name) = path.data.last().and_then(|d| d.data.get_opt_name()) { - format!("{}_{}", name, hash.0.to_hex()) + tracing::debug!("stable_def_id_symbol: name={}", name); + format!("{}_{}_{}", prefix, name, hash.0.to_hex()) } else { hash.0.to_hex() } @@ -37,5 +38,9 @@ pub fn datatype_symbol(tcx: mir_ty::TyCtxt<'_>, did: DefId) -> DatatypeSymbol { } pub fn user_defined_pred(tcx: mir_ty::TyCtxt<'_>, did: DefId) -> UserDefinedPred { - UserDefinedPred::new(stable_def_id_symbol(tcx, did)) + UserDefinedPred::new(stable_def_id_symbol(tcx, did, "p")) +} + +pub fn forall_pred(tcx: mir_ty::TyCtxt<'_>, did: DefId) -> ForallPred { + ForallPred::new(stable_def_id_symbol(tcx, did, "q")) } From 14170e7bc8518786fd7196b41f3936d91b89ef25 Mon Sep 17 00:00:00 2001 From: coeff-aij <175928954+coeff-aij@users.noreply.github.com> Date: Wed, 27 May 2026 14:40:55 +0900 Subject: [PATCH 16/55] fix: distinguish different type parameters in subtyping --- src/rty/subtyping.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/rty/subtyping.rs b/src/rty/subtyping.rs index 1f015342..3b9cae09 100644 --- a/src/rty/subtyping.rs +++ b/src/rty/subtyping.rs @@ -73,8 +73,7 @@ where (Type::Int, Type::Int) | (Type::Bool, Type::Bool) | (Type::String, Type::String) - | (Type::Never, Type::Never) - | (Type::Param(_), Type::Param(_)) => {} + | (Type::Never, Type::Never) => {} (Type::Enum(got), Type::Enum(expected)) if got.symbol() == expected.symbol() => { for (got_ty, expected_ty) in got.args.iter().zip(expected.args.iter()) { let cs = self.relate_sub_refined_type(got_ty, expected_ty); @@ -124,6 +123,7 @@ where let cs2 = self.relate_sub_refined_type(&got.elem, &expected.elem); clauses.extend(cs2); } + (Type::Param(got), Type::Param(expected)) if got.idx == expected.idx => {} _ => panic!( "inconsistent types: got={}, expected={}", got.display(), From 6ee71de16dfb8944703bef3da41d264d4fa93ad4 Mon Sep 17 00:00:00 2001 From: coeff-aij <175928954+coeff-aij@users.noreply.github.com> Date: Wed, 27 May 2026 17:33:52 +0900 Subject: [PATCH 17/55] change: store the def_id of the corresponding function in TypeBuilder --- src/analyze.rs | 7 ++++--- src/analyze/basic_block.rs | 3 ++- src/analyze/crate_.rs | 9 ++++++++- src/analyze/local_def.rs | 2 +- src/refine/template.rs | 28 +++++++++++++++++++++------- 5 files changed, 36 insertions(+), 13 deletions(-) diff --git a/src/analyze.rs b/src/analyze.rs index 2ba4a983..1d9a77eb 100644 --- a/src/analyze.rs +++ b/src/analyze.rs @@ -654,15 +654,16 @@ impl<'tcx> Analyzer<'tcx> { &mut self, local_def_id: LocalDefId, bb: BasicBlock, + owner_fn_id: DefId ) -> basic_block::Analyzer<'tcx, '_> { - basic_block::Analyzer::new(self, local_def_id, bb) + basic_block::Analyzer::new(self, local_def_id, bb, owner_fn_id) } - pub fn type_builder(&self, def_ids: DefIdCache<'tcx>, def_id: DefId) -> TypeBuilder<'tcx> { + pub fn type_builder(&self, def_ids: DefIdCache<'tcx>, owner_fn_id: DefId) -> TypeBuilder<'tcx> { TypeBuilder::new( self.tcx, def_ids, - def_id, + owner_fn_id, self.type_params.clone(), self.system.clone(), ) diff --git a/src/analyze/basic_block.rs b/src/analyze/basic_block.rs index b7746f31..c00cec30 100644 --- a/src/analyze/basic_block.rs +++ b/src/analyze/basic_block.rs @@ -1327,6 +1327,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { ctx: &'ctx mut analyze::Analyzer<'tcx>, local_def_id: LocalDefId, basic_block: BasicBlock, + owner_fn_id: DefId, ) -> Self { let tcx = ctx.tcx; let drop_points = DropPoints::default(); @@ -1334,7 +1335,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { let env = ctx.new_env(); let local_decls = body.local_decls.clone(); let prophecy_vars = Default::default(); - let type_builder = ctx.type_builder(ctx.def_ids(), local_def_id.to_def_id()); + let type_builder = ctx.type_builder(ctx.def_ids(), owner_fn_id); Self { ctx, tcx, diff --git a/src/analyze/crate_.rs b/src/analyze/crate_.rs index 5fe2769f..c7c55b2c 100644 --- a/src/analyze/crate_.rs +++ b/src/analyze/crate_.rs @@ -179,7 +179,14 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { let arg = match param.kind { mir_ty::GenericParamDefKind::Type { .. } => { if constrained_params.contains(¶m.index) { - mir_ty::Ty::new_param(self.tcx, param.index, param.name).into() + let new_param = + mir_ty::Ty::new_param(self.tcx, param.index, param.name).into(); + tracing::debug!( + "replace the cosnstrained param {:#?} with the new param {:#?}.", + param, + new_param + ); + new_param } else { self.tcx.types.i32.into() } diff --git a/src/analyze/local_def.rs b/src/analyze/local_def.rs index 3169ac03..ab10dde1 100644 --- a/src/analyze/local_def.rs +++ b/src/analyze/local_def.rs @@ -1057,7 +1057,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { .clone(); let drop_points = self.drop_points[&bb].clone(); self.ctx - .basic_block_analyzer(self.local_def_id, bb) + .basic_block_analyzer(self.local_def_id, bb, self.body.source.def_id()) .body(self.body.clone()) .drop_points(drop_points) .run(&rty, expected_fn_ty); diff --git a/src/refine/template.rs b/src/refine/template.rs index ccbf8761..61e2acc4 100644 --- a/src/refine/template.rs +++ b/src/refine/template.rs @@ -73,7 +73,7 @@ where pub struct TypeBuilder<'tcx> { tcx: mir_ty::TyCtxt<'tcx>, def_ids: DefIdCache<'tcx>, - def_id: DefId, + owner_fn_id: DefId, typing_env: mir_ty::TypingEnv<'tcx>, type_params: Rc>, system: Rc>, @@ -83,15 +83,16 @@ impl<'tcx> TypeBuilder<'tcx> { pub fn new( tcx: mir_ty::TyCtxt<'tcx>, def_ids: DefIdCache<'tcx>, - def_id: DefId, + owner_fn_id: DefId, type_params: Rc>, system: Rc>, ) -> Self { - let typing_env = mir_ty::TypingEnv::post_analysis(tcx, def_id); + tracing::debug!("TypeBuilder is created for {owner_fn_id:?}."); + let typing_env = mir_ty::TypingEnv::post_analysis(tcx, owner_fn_id); Self { tcx, def_ids, - def_id, + owner_fn_id, typing_env, type_params, system, @@ -101,8 +102,17 @@ impl<'tcx> TypeBuilder<'tcx> { fn translate_param_type(&self, ty: &mir_ty::ParamTy) -> rty::Type { let mut type_params = self.type_params.borrow_mut(); let index = type_params - .entry(TypeParam::GenericType(self.def_id, ty.index)) - .or_insert_with(|| self.system.borrow_mut().new_forall_sort()); + .entry(TypeParam::GenericType(self.owner_fn_id, ty.index)) + .or_insert_with(|| { + let idx = self.system.borrow_mut().new_forall_sort(); + tracing::debug!( + "issue the new ForallSortIdx {} for ParamTy {:?} at {:?}.", + idx, + ty, + self.owner_fn_id + ); + idx + }); rty::ParamType::new(*index).into() } @@ -110,7 +120,11 @@ impl<'tcx> TypeBuilder<'tcx> { let mut type_params = self.type_params.borrow_mut(); let index = type_params .entry(TypeParam::AssocType(ty.def_id)) - .or_insert_with(|| self.system.borrow_mut().new_forall_sort()); + .or_insert_with(|| { + let idx = self.system.borrow_mut().new_forall_sort(); + tracing::debug!("issue the new ForallSortIdx {} for AliasTy {:#?}.", idx, ty); + idx + }); rty::ParamType::new(*index).into() } From 6c8add1237f8d968e20a5996dde13fa8a67574a8 Mon Sep 17 00:00:00 2001 From: coeff-aij <175928954+coeff-aij@users.noreply.github.com> Date: Thu, 28 May 2026 14:15:56 +0900 Subject: [PATCH 18/55] fix: identify type parameters using the DefId of the owner(e.g. `fn f` for `T` in the body) --- src/analyze.rs | 3 ++- src/analyze/basic_block.rs | 5 +++-- src/analyze/local_def.rs | 2 +- src/refine/template.rs | 2 +- 4 files changed, 7 insertions(+), 5 deletions(-) diff --git a/src/analyze.rs b/src/analyze.rs index 1d9a77eb..e25df5cd 100644 --- a/src/analyze.rs +++ b/src/analyze.rs @@ -472,8 +472,9 @@ impl<'tcx> Analyzer<'tcx> { &mut self, def_id: DefId, generic_args: mir_ty::GenericArgsRef<'tcx>, + caller_def_id: DefId, ) -> Option { - let type_builder = self.type_builder(self.def_ids(), def_id); + let type_builder = self.type_builder(self.def_ids(), caller_def_id); let deferred_ty = match self.defs.get(&def_id)? { DefTy::Concrete(rty) => { diff --git a/src/analyze/basic_block.rs b/src/analyze/basic_block.rs index c00cec30..65b5a528 100644 --- a/src/analyze/basic_block.rs +++ b/src/analyze/basic_block.rs @@ -868,7 +868,8 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { def_id: DefId, args: mir_ty::GenericArgsRef<'tcx>, ) -> rty::Type { - if let Some(def_ty) = self.ctx.def_ty_with_args(def_id, args) { + let caller_def_id = self.type_builder.owner_fn_id; + if let Some(def_ty) = self.ctx.def_ty_with_args(def_id, args, caller_def_id) { return def_ty.ty; } @@ -880,7 +881,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { ); } tracing::info!(?def_id, ?resolved_def_id, ?resolved_args, "resolved"); - let Some(def_ty) = self.ctx.def_ty_with_args(resolved_def_id, resolved_args) else { + let Some(def_ty) = self.ctx.def_ty_with_args(resolved_def_id, resolved_args, caller_def_id) else { panic!( "unknown def (resolved): {:?}, args: {:?}", resolved_def_id, resolved_args diff --git a/src/analyze/local_def.rs b/src/analyze/local_def.rs index ab10dde1..0fcfb5a9 100644 --- a/src/analyze/local_def.rs +++ b/src/analyze/local_def.rs @@ -317,7 +317,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { .associated_item(self.local_def_id.to_def_id()) .trait_item_def_id .unwrap(); - self.ctx.def_ty_with_args(trait_item_did, trait_ref.args) + self.ctx.def_ty_with_args(trait_item_did, trait_ref.args, trait_ref.def_id) } // TODO: Remove this eager precompute together with diff --git a/src/refine/template.rs b/src/refine/template.rs index 61e2acc4..34f2a38b 100644 --- a/src/refine/template.rs +++ b/src/refine/template.rs @@ -73,7 +73,7 @@ where pub struct TypeBuilder<'tcx> { tcx: mir_ty::TyCtxt<'tcx>, def_ids: DefIdCache<'tcx>, - owner_fn_id: DefId, + pub owner_fn_id: DefId, typing_env: mir_ty::TypingEnv<'tcx>, type_params: Rc>, system: Rc>, From af226a4367ae1dbb6f6dcd4caa079f0c3d4ac322 Mon Sep 17 00:00:00 2001 From: coeff-aij <175928954+coeff-aij@users.noreply.github.com> Date: Thu, 28 May 2026 20:51:51 +0900 Subject: [PATCH 19/55] fix: wrong conditionals to insert forall predicates --- src/analyze/annot_fn.rs | 14 ++++++++++---- 1 file changed, 10 insertions(+), 4 deletions(-) diff --git a/src/analyze/annot_fn.rs b/src/analyze/annot_fn.rs index ca78a99e..0cba0bca 100644 --- a/src/analyze/annot_fn.rs +++ b/src/analyze/annot_fn.rs @@ -649,7 +649,7 @@ impl<'a, 'tcx> AnnotFnTranslator<'a, 'tcx> { outer_generic_args = ?self.generic_args, "resolving predicate call in formula" ); - let (is_unresolved_args, generic_args) = + let (mut is_unresolved_args, generic_args) = match self.instantiate_generics(generic_args, self.generic_args) { Some(args) => (false, args), None => (true, generic_args), @@ -662,13 +662,19 @@ impl<'a, 'tcx> AnnotFnTranslator<'a, 'tcx> { generic_args, ) .unwrap(); - let pred_def_id = instance.map_or(def_id, |instance| instance.def_id()); + let pred_def_id = if let Some(instance) = instance { + instance.def_id() + } else { + is_unresolved_args = true; + def_id + }; let pred = if is_unresolved_args { - refine::user_defined_pred(self.tcx, pred_def_id).into() - } else { refine::forall_pred(self.tcx, pred_def_id).into() + } else { + refine::user_defined_pred(self.tcx, pred_def_id).into() }; + tracing::debug!("resolved predicate call in formula: {:?}", pred); let arg_terms = args.iter().map(|e| self.to_term(e)).collect(); let atom = chc::Atom::new(pred, arg_terms); return FormulaOrTerm::Formula(chc::Formula::Atom(atom)); From 3888011a0b53e55b658ef6638ad0a56e96d69772 Mon Sep 17 00:00:00 2001 From: coeff-aij <175928954+coeff-aij@users.noreply.github.com> Date: Thu, 28 May 2026 23:57:33 +0900 Subject: [PATCH 20/55] fix: normalize thrust::Model::Ty --- src/refine/template.rs | 15 ++++++++++++++- 1 file changed, 14 insertions(+), 1 deletion(-) diff --git a/src/refine/template.rs b/src/refine/template.rs index 34f2a38b..c20f4ba8 100644 --- a/src/refine/template.rs +++ b/src/refine/template.rs @@ -170,19 +170,32 @@ impl<'tcx> TypeBuilder<'tcx> { } fn resolve_model_ty(&self, orig_ty: mir_ty::Ty<'tcx>) -> mir_ty::Ty<'tcx> { + tracing::debug!("attempting to resolve the type {:#?}.", orig_ty); let ty = self.replace_closure_model(orig_ty); let Some(model_ty_def_id) = self.def_ids.model_ty() else { return ty; }; let args = self.tcx.mk_args(&[ty.into()]); + tracing::debug!("generic args are {:#?}.", args); let projection_ty = mir_ty::Ty::new_projection(self.tcx, model_ty_def_id, args); if let Ok(normalized_ty) = self .tcx .try_normalize_erasing_regions(self.typing_env, projection_ty) { - return normalized_ty; + tracing::debug!("the type {:#?} is resolved as the type {:#?}.", orig_ty, ty); + let contains_model_ty_alias = normalized_ty.walk().any(|arg| { + if let mir_ty::GenericArgKind::Type(t) = arg.kind() { + matches!(t.kind(), mir_ty::TyKind::Alias(_, alias_ty) if alias_ty.def_id == model_ty_def_id) + } else { + false + } + }); + if !contains_model_ty_alias { + return normalized_ty; + } } + tracing::debug!("the type {:#?} is replaced as the {:#?}.", orig_ty, ty); ty } From 968a4a7576c99352336b3975eb9127c9aa60183c Mon Sep 17 00:00:00 2001 From: coeff-aij <175928954+coeff-aij@users.noreply.github.com> Date: Mon, 8 Jun 2026 12:17:20 +0900 Subject: [PATCH 21/55] fix: propagate the DefId for the owner function of formula_fn and extern_spec_fn --- src/analyze.rs | 15 +++- src/analyze/annot_fn.rs | 9 +- src/analyze/basic_block.rs | 5 +- src/analyze/crate_.rs | 10 +-- src/analyze/local_def.rs | 163 ++++++++++++++++++++++--------------- 5 files changed, 119 insertions(+), 83 deletions(-) diff --git a/src/analyze.rs b/src/analyze.rs index e25df5cd..439b1456 100644 --- a/src/analyze.rs +++ b/src/analyze.rs @@ -448,6 +448,7 @@ impl<'tcx> Analyzer<'tcx> { &self, local_def_id: LocalDefId, generic_args: mir_ty::GenericArgsRef<'tcx>, + owner_fn_id: DefId, ) -> Option> { let deferred_formula_fn = self.formula_fns.get(&local_def_id)?; @@ -458,7 +459,7 @@ impl<'tcx> Analyzer<'tcx> { let translator = annot_fn::AnnotFnTranslator::new(self, local_def_id) .with_generic_args(generic_args) - .with_def_id_cache(self.def_ids()); + .with_def_id_cache(self.def_ids(), owner_fn_id); let formula_fn = translator.to_formula_fn(); deferred_formula_fn_cache .borrow_mut() @@ -655,7 +656,7 @@ impl<'tcx> Analyzer<'tcx> { &mut self, local_def_id: LocalDefId, bb: BasicBlock, - owner_fn_id: DefId + owner_fn_id: DefId, ) -> basic_block::Analyzer<'tcx, '_> { basic_block::Analyzer::new(self, local_def_id, bb, owner_fn_id) } @@ -761,6 +762,7 @@ impl<'tcx> Analyzer<'tcx> { resolver: T, self_type_name: Option, generic_args: mir_ty::GenericArgsRef<'tcx>, + owner_fn_id: DefId, ) -> Option> where T: Resolver, @@ -791,7 +793,9 @@ impl<'tcx> Analyzer<'tcx> { if require_annot.is_some() { unimplemented!(); } - let Some(formula_fn) = self.formula_fn_with_args(formula_def_id, generic_args) else { + let Some(formula_fn) = + self.formula_fn_with_args(formula_def_id, generic_args, owner_fn_id) + else { panic!( "require annotation {:?} is not a formula function", formula_def_id @@ -810,6 +814,7 @@ impl<'tcx> Analyzer<'tcx> { resolver: T, self_type_name: Option, generic_args: mir_ty::GenericArgsRef<'tcx>, + owner_fn_id: DefId, ) -> Option> where T: Resolver>, @@ -841,7 +846,9 @@ impl<'tcx> Analyzer<'tcx> { if ensure_annot.is_some() { unimplemented!(); } - let Some(formula_fn) = self.formula_fn_with_args(formula_def_id, generic_args) else { + let Some(formula_fn) = + self.formula_fn_with_args(formula_def_id, generic_args, owner_fn_id) + else { panic!( "ensure annotation {:?} is not a formula function", formula_def_id diff --git a/src/analyze/annot_fn.rs b/src/analyze/annot_fn.rs index 0cba0bca..a9c6f234 100644 --- a/src/analyze/annot_fn.rs +++ b/src/analyze/annot_fn.rs @@ -1,7 +1,10 @@ use std::collections::HashMap; use pretty::{termcolor, Pretty}; -use rustc_hir::{def_id::LocalDefId, HirId}; +use rustc_hir::{ + def_id::{DefId, LocalDefId}, + HirId, +}; use rustc_index::IndexVec; use rustc_middle::ty::{self as mir_ty, TyCtxt, TypeFoldable}; @@ -178,12 +181,12 @@ impl<'a, 'tcx> AnnotFnTranslator<'a, 'tcx> { self } - pub fn with_def_id_cache(mut self, def_ids: DefIdCache<'tcx>) -> Self { + pub fn with_def_id_cache(mut self, def_ids: DefIdCache<'tcx>, owner_fn_id: DefId) -> Self { self.def_ids = def_ids; self.type_builder = TypeBuilder::new( self.tcx, self.def_ids.clone(), - self.local_def_id.to_def_id(), + owner_fn_id, self.analyzer.type_params.clone(), self.analyzer.system.clone(), ); diff --git a/src/analyze/basic_block.rs b/src/analyze/basic_block.rs index 65b5a528..d7447024 100644 --- a/src/analyze/basic_block.rs +++ b/src/analyze/basic_block.rs @@ -881,7 +881,10 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { ); } tracing::info!(?def_id, ?resolved_def_id, ?resolved_args, "resolved"); - let Some(def_ty) = self.ctx.def_ty_with_args(resolved_def_id, resolved_args, caller_def_id) else { + let Some(def_ty) = self + .ctx + .def_ty_with_args(resolved_def_id, resolved_args, caller_def_id) + else { panic!( "unknown def (resolved): {:?}, args: {:?}", resolved_def_id, resolved_args diff --git a/src/analyze/crate_.rs b/src/analyze/crate_.rs index c7c55b2c..58bd309e 100644 --- a/src/analyze/crate_.rs +++ b/src/analyze/crate_.rs @@ -111,14 +111,9 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { } } - let target_def_id = if analyzer.is_annotated_as_extern_spec_fn() { - analyzer.extern_spec_fn_target_def_id() - } else { - local_def_id.to_def_id() - }; - + let owner_fn_id = analyzer.owner_fn_id; let expected = analyzer.expected_ty(); - self.ctx.register_def(target_def_id, expected); + self.ctx.register_def(owner_fn_id, expected); } fn analyze_local_defs(&mut self) { @@ -140,7 +135,6 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { // check polymorphic function def by replacing type params with some opaque type // (and this is no-op if the function is mono) let expected = expected.clone(); - tracing::debug!("expected type of {:?} is {:#?}", local_def_id, expected); let generic_args = self.placeholder_generic_args(*local_def_id); self.ctx .local_def_analyzer(*local_def_id) diff --git a/src/analyze/local_def.rs b/src/analyze/local_def.rs index 0fcfb5a9..6f717ef8 100644 --- a/src/analyze/local_def.rs +++ b/src/analyze/local_def.rs @@ -36,6 +36,82 @@ fn stmt_str_literal(stmt: &rustc_hir::Stmt) -> Option { } } +fn is_annotated_as_extern_spec_fn_impl(tcx: &TyCtxt, local_def_id: &LocalDefId) -> bool { + tcx.get_attrs_by_path( + local_def_id.to_def_id(), + &analyze::annot::extern_spec_fn_path(), + ) + .next() + .is_some() +} + +/// Extract the target DefId from `#[thrust::extern_spec_fn]` function. +/// +/// The target is identified as the tail call expression (last expression without +/// semicolon) in the function body block. +fn extern_spec_fn_target_def_id_impl<'tcx>( + tcx: &TyCtxt<'tcx>, + local_def_id: &LocalDefId, + mir_body: &Body<'tcx>, +) -> DefId { + let hir_node = tcx.hir_node_by_def_id(*local_def_id); + let hir_body_id = match hir_node { + rustc_hir::Node::Item(item) => { + let rustc_hir::ItemKind::Fn { body: body_id, .. } = item.kind else { + panic!("extern_spec_fn must be a function"); + }; + body_id + } + rustc_hir::Node::ImplItem(impl_item) => { + let rustc_hir::ImplItemKind::Fn(_, body_id) = impl_item.kind else { + panic!("extern_spec_fn must be a function"); + }; + body_id + } + rustc_hir::Node::TraitItem(trait_item) => { + let rustc_hir::TraitItemKind::Fn(_, rustc_hir::TraitFn::Provided(body_id)) = + trait_item.kind + else { + panic!("extern_spec_fn must be a function with a body"); + }; + body_id + } + _ => panic!("extern_spec_fn must be a function item or impl item"), + }; + + let hir_body = tcx.hir_body(hir_body_id); + + // The body is a block; the tail expression is the function call to the target. + let rustc_hir::ExprKind::Block(block, _) = &hir_body.value.kind else { + panic!("extern_spec_fn body must be a block"); + }; + let tail_expr = block + .expr + .expect("extern_spec_fn block must end with a tail call expression"); + + let rustc_hir::ExprKind::Call(func_expr, _) = &tail_expr.kind else { + panic!("extern_spec_fn tail expression must be a function call"); + }; + let rustc_hir::ExprKind::Path(qpath) = &func_expr.kind else { + panic!("extern_spec_fn call must be a path expression"); + }; + + let typeck_result = tcx.typeck(local_def_id); + let hir_id = func_expr.hir_id; + let rustc_hir::def::Res::Def(_, def_id) = typeck_result.qpath_res(qpath, hir_id) else { + panic!("extern_spec_fn call must resolve to a definition"); + }; + + let args = typeck_result.node_args(hir_id); + let typing_env = mir_body.typing_env(*tcx); + let instance = mir_ty::Instance::try_resolve(*tcx, typing_env, def_id, args).unwrap(); + if let Some(instance) = instance { + instance.def_id() + } else { + def_id + } +} + /// An implementation of the typing of local definitions. /// /// The current implementation only applies to function definitions. The entry point is @@ -45,6 +121,7 @@ pub struct Analyzer<'tcx, 'ctx> { tcx: TyCtxt<'tcx>, local_def_id: LocalDefId, + pub owner_fn_id: DefId, body: Body<'tcx>, /// to substitute HIR types during translation in [`crate::analyze::annot_fn`] @@ -200,13 +277,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { } pub fn is_annotated_as_extern_spec_fn(&self) -> bool { - self.tcx - .get_attrs_by_path( - self.local_def_id.to_def_id(), - &analyze::annot::extern_spec_fn_path(), - ) - .next() - .is_some() + is_annotated_as_extern_spec_fn_impl(&self.tcx, &self.local_def_id) } pub fn is_annotated_as_predicate(&self) -> bool { @@ -317,7 +388,8 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { .associated_item(self.local_def_id.to_def_id()) .trait_item_def_id .unwrap(); - self.ctx.def_ty_with_args(trait_item_did, trait_ref.args, trait_ref.def_id) + self.ctx + .def_ty_with_args(trait_item_did, trait_ref.args, trait_ref.def_id) } // TODO: Remove this eager precompute together with @@ -340,7 +412,9 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { if fn_def_id == self.local_def_id.to_def_id() { continue; } - let _ = self.ctx.def_ty_with_args(fn_def_id, fn_args); + let _ = self + .ctx + .def_ty_with_args(fn_def_id, fn_args, self.owner_fn_id); } } @@ -386,6 +460,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { ¶m_resolver, self_type_name.clone(), self.generic_args, + self.owner_fn_id, ); let mut ensure_annot = self.ctx.extract_ensure_annot( @@ -393,6 +468,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { &result_param_resolver, self_type_name.clone(), self.generic_args, + self.owner_fn_id, ); if let Some(trait_item_id) = self.local_trait_item_id() { @@ -402,12 +478,14 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { ¶m_resolver, self_type_name.clone(), self.generic_args, + self.owner_fn_id, ); let trait_ensure_annot = self.ctx.extract_ensure_annot( trait_item_id, &result_param_resolver, self_type_name.clone(), self.generic_args, + self.owner_fn_id, ); assert!(require_annot.is_none() || trait_require_annot.is_none()); @@ -475,62 +553,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { /// The target is identified as the tail call expression (last expression without /// semicolon) in the function body block. pub fn extern_spec_fn_target_def_id(&self) -> DefId { - let node = self.tcx.hir_node_by_def_id(self.local_def_id); - let body_id = match node { - rustc_hir::Node::Item(item) => { - let rustc_hir::ItemKind::Fn { body: body_id, .. } = item.kind else { - panic!("extern_spec_fn must be a function"); - }; - body_id - } - rustc_hir::Node::ImplItem(impl_item) => { - let rustc_hir::ImplItemKind::Fn(_, body_id) = impl_item.kind else { - panic!("extern_spec_fn must be a function"); - }; - body_id - } - rustc_hir::Node::TraitItem(trait_item) => { - let rustc_hir::TraitItemKind::Fn(_, rustc_hir::TraitFn::Provided(body_id)) = - trait_item.kind - else { - panic!("extern_spec_fn must be a function with a body"); - }; - body_id - } - _ => panic!("extern_spec_fn must be a function item or impl item"), - }; - - let body = self.tcx.hir_body(body_id); - - // The body is a block; the tail expression is the function call to the target. - let rustc_hir::ExprKind::Block(block, _) = &body.value.kind else { - panic!("extern_spec_fn body must be a block"); - }; - let tail_expr = block - .expr - .expect("extern_spec_fn block must end with a tail call expression"); - - let rustc_hir::ExprKind::Call(func_expr, _) = &tail_expr.kind else { - panic!("extern_spec_fn tail expression must be a function call"); - }; - let rustc_hir::ExprKind::Path(qpath) = &func_expr.kind else { - panic!("extern_spec_fn call must be a path expression"); - }; - - let typeck_result = self.tcx.typeck(self.local_def_id); - let hir_id = func_expr.hir_id; - let rustc_hir::def::Res::Def(_, def_id) = typeck_result.qpath_res(qpath, hir_id) else { - panic!("extern_spec_fn call must resolve to a definition"); - }; - - let args = typeck_result.node_args(hir_id); - let typing_env = self.body.typing_env(self.tcx); - let instance = mir_ty::Instance::try_resolve(self.tcx, typing_env, def_id, args).unwrap(); - if let Some(instance) = instance { - instance.def_id() - } else { - def_id - } + extern_spec_fn_target_def_id_impl(&self.tcx, &self.local_def_id, &self.body) } fn is_mut_param(&self, param_idx: rty::FunctionParamIdx) -> bool { @@ -938,7 +961,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { ) -> rty::Refinement { let formula_fn = self .ctx - .formula_fn_with_args(formula_def_id, generic_args) + .formula_fn_with_args(formula_def_id, generic_args, self.owner_fn_id) .expect("invariant formula function is not registered"); let idents = self.tcx.fn_arg_idents(formula_def_id.to_def_id()); @@ -1185,12 +1208,18 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { let tcx = ctx.tcx; let body = tcx.optimized_mir(local_def_id.to_def_id()).clone(); let drop_points = Default::default(); - let type_builder = ctx.type_builder(ctx.def_ids(), local_def_id.to_def_id()); + let owner_fn_id = if is_annotated_as_extern_spec_fn_impl(&tcx, &local_def_id) { + extern_spec_fn_target_def_id_impl(&tcx, &local_def_id, &body) + } else { + local_def_id.to_def_id() + }; + let type_builder = ctx.type_builder(ctx.def_ids(), owner_fn_id); let generic_args = tcx.mk_args(&[]); Self { ctx, tcx, local_def_id, + owner_fn_id, body, generic_args, drop_points, From 87969f20e3969742b1a3d003ccf830ba63b31f2b Mon Sep 17 00:00:00 2001 From: coeff-aij <175928954+coeff-aij@users.noreply.github.com> Date: Fri, 29 May 2026 17:06:43 +0900 Subject: [PATCH 22/55] fix: use both TypeParamIdx and ForallSortIdx for type parameters --- src/refine/template.rs | 42 +++++++++++++------- src/rty.rs | 36 ++++++++++------- src/rty/params.rs | 89 +++++++++++++++++++++--------------------- src/rty/subtyping.rs | 3 +- 4 files changed, 95 insertions(+), 75 deletions(-) diff --git a/src/refine/template.rs b/src/refine/template.rs index c20f4ba8..e283b06d 100644 --- a/src/refine/template.rs +++ b/src/refine/template.rs @@ -75,6 +75,11 @@ pub struct TypeBuilder<'tcx> { def_ids: DefIdCache<'tcx>, pub owner_fn_id: DefId, typing_env: mir_ty::TypingEnv<'tcx>, + /// Maps index in [`mir_ty::ParamTy`] to [`rty::TypeParamIdx`]. + /// These indices may differ because we skip lifetime parameters and they always need to be + /// mapped when we translate a [`mir_ty::ParamTy`] to [`rty::ParamType`]. + /// See [`rty::TypeParamIdx`] for more details. + param_idx_mapping: HashMap, type_params: Rc>, system: Rc>, } @@ -87,6 +92,19 @@ impl<'tcx> TypeBuilder<'tcx> { type_params: Rc>, system: Rc>, ) -> Self { + let generics = tcx.generics_of(owner_fn_id); + let mut param_idx_mapping: HashMap = Default::default(); + for i in 0..generics.count() { + let generic_param = generics.param_at(i, tcx); + match generic_param.kind { + mir_ty::GenericParamDefKind::Lifetime => {} + mir_ty::GenericParamDefKind::Type { .. } => { + param_idx_mapping.insert(i as u32, param_idx_mapping.len().into()); + } + mir_ty::GenericParamDefKind::Const { .. } => {} + } + } + tracing::debug!("TypeBuilder is created for {owner_fn_id:?}."); let typing_env = mir_ty::TypingEnv::post_analysis(tcx, owner_fn_id); Self { @@ -94,14 +112,20 @@ impl<'tcx> TypeBuilder<'tcx> { def_ids, owner_fn_id, typing_env, + param_idx_mapping, type_params, system, } } fn translate_param_type(&self, ty: &mir_ty::ParamTy) -> rty::Type { + let param_local_idx = *self + .param_idx_mapping + .get(&ty.index) + .expect("unknown type param idx"); + let mut type_params = self.type_params.borrow_mut(); - let index = type_params + let forall_sort_idx = type_params .entry(TypeParam::GenericType(self.owner_fn_id, ty.index)) .or_insert_with(|| { let idx = self.system.borrow_mut().new_forall_sort(); @@ -113,19 +137,7 @@ impl<'tcx> TypeBuilder<'tcx> { ); idx }); - rty::ParamType::new(*index).into() - } - - fn translate_alias_type(&self, ty: &mir_ty::AliasTy) -> rty::Type { - let mut type_params = self.type_params.borrow_mut(); - let index = type_params - .entry(TypeParam::AssocType(ty.def_id)) - .or_insert_with(|| { - let idx = self.system.borrow_mut().new_forall_sort(); - tracing::debug!("issue the new ForallSortIdx {} for AliasTy {:#?}.", idx, ty); - idx - }); - rty::ParamType::new(*index).into() + rty::ParamType::new(param_local_idx, *forall_sort_idx).into() } /// Replaces {closure} types with thrust_models::Closure<{closure}>. @@ -289,7 +301,7 @@ impl<'tcx> TypeBuilder<'tcx> { unimplemented!("unsupported ADT: {:?}", ty); } } - mir_ty::TyKind::Alias(_, ty) => self.translate_alias_type(ty), + // mir_ty::TyKind::Alias(_, ty) => self.translate_alias_type(ty), kind => unimplemented!("unrefined_ty: {:?}", kind), } } diff --git a/src/rty.rs b/src/rty.rs index 8f6f930e..dcf9576f 100644 --- a/src/rty.rs +++ b/src/rty.rs @@ -43,7 +43,7 @@ use pretty::{termcolor, Pretty}; use rustc_abi::VariantIdx; use rustc_index::IndexVec; -use crate::chc; +use crate::chc::{self, ForallSortIdx}; mod template; pub use template::{Template, TemplateBuilder}; @@ -729,7 +729,8 @@ impl EnumType { /// A type parameter. #[derive(Debug, Clone)] pub struct ParamType { - idx: TypeParamIdx, + type_param_idx: TypeParamIdx, + forall_sort_idx: ForallSortIdx, } impl<'a, D> Pretty<'a, D, termcolor::ColorSpec> for &ParamType @@ -737,17 +738,24 @@ where D: pretty::DocAllocator<'a, termcolor::ColorSpec>, { fn pretty(self, allocator: &'a D) -> pretty::DocBuilder<'a, D, termcolor::ColorSpec> { - self.idx.pretty(allocator) + self.type_param_idx.pretty(allocator) } } impl ParamType { - pub fn new(idx: TypeParamIdx) -> Self { - ParamType { idx } + pub fn new(type_param_idx: TypeParamIdx, forall_sort_idx: ForallSortIdx) -> Self { + ParamType { + type_param_idx, + forall_sort_idx, + } + } + + pub fn type_param_index(&self) -> TypeParamIdx { + self.type_param_idx } - pub fn index(&self) -> TypeParamIdx { - self.idx + pub fn forall_sort_index(&self) -> ForallSortIdx { + self.forall_sort_idx } pub fn into_closed_ty(self) -> Type { @@ -1034,7 +1042,7 @@ impl Type { // currently String sort seems not available in HORN logic of Z3 Type::String => chc::Sort::null(), Type::Never => chc::Sort::null(), - Type::Param(ty) => chc::Sort::forall(ty.index()), + Type::Param(ty) => chc::Sort::forall(ty.forall_sort_index()), Type::Pointer(ty) => { let elem_sort = ty.elem.ty.to_sort(); @@ -1120,7 +1128,7 @@ impl Type { pub fn free_ty_params(&self) -> HashSet { match self { Type::Int | Type::Bool | Type::String | Type::Never => Default::default(), - Type::Param(ty) => std::iter::once(ty.index()).collect(), + Type::Param(ty) => std::iter::once(ty.type_param_index()).collect(), Type::Pointer(ty) => ty.free_ty_params(), Type::Function(ty) => ty.free_ty_params(), Type::Tuple(ty) => ty.free_ty_params(), @@ -1687,7 +1695,7 @@ impl RefinedType { match &mut self.ty { Type::Int | Type::Bool | Type::String | Type::Never => {} Type::Param(ty) => { - if let Some(rty) = subst.get(ty.index()) { + if let Some(rty) = subst.get(ty.type_param_index()) { let RefinedType { ty: replacement_ty, refinement, @@ -1723,15 +1731,15 @@ impl RefinedType { | (Type::Bool, Type::Bool) | (Type::String, Type::String) | (Type::Never, Type::Never) => Default::default(), - (Type::Param(pty), ty) if !ty.free_ty_params().contains(&pty.index()) => { + (Type::Param(pty), ty) if !ty.free_ty_params().contains(&pty.type_param_index()) => { TypeParamSubst::singleton( - pty.index(), + pty.type_param_index(), RefinedType::new(ty.clone(), other.refinement.clone()), ) } - (ty, Type::Param(pty)) if !ty.free_ty_params().contains(&pty.index()) => { + (ty, Type::Param(pty)) if !ty.free_ty_params().contains(&pty.type_param_index()) => { TypeParamSubst::singleton( - pty.index(), + pty.type_param_index(), RefinedType::new(ty.clone(), self.refinement.clone()), ) } diff --git a/src/rty/params.rs b/src/rty/params.rs index 88e0bf4e..ef05138e 100644 --- a/src/rty/params.rs +++ b/src/rty/params.rs @@ -2,57 +2,56 @@ use std::collections::BTreeMap; -// use pretty::{termcolor, Pretty}; +use pretty::{termcolor, Pretty}; use rustc_index::IndexVec; use crate::chc; use super::{Closed, RefinedType, Type}; -pub type TypeParamIdx = chc::ForallSortIdx; -// rustc_index::newtype_index! { -// /// An index representing a type parameter. -// /// -// /// ## Note on indexing of type parameters -// /// -// /// The index of [`rustc_middle::ty::ParamTy`] is based on all generic parameters in -// /// the definition, including lifetimes. Given the following definition: -// /// -// /// ```rust -// /// struct X<'a, T> { f: &'a T } -// /// ``` -// /// -// /// The type of field `f` is `&T1` (not `&T0`) in MIR. However, in Thrust, we ignore lifetime -// /// parameters and the index of [`rty::ParamType`](super::ParamType) is based on type parameters only, giving `f` -// /// the type `&T0`. [`TypeBuilder`](crate::refine::TypeBuilder) takes care of this difference when translating MIR -// /// types to Thrust types. -// #[orderable] -// #[debug_format = "T{}"] -// pub struct TypeParamIdx { } -// } - -// impl std::fmt::Display for TypeParamIdx { -// fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result { -// write!(f, "T{}", self.index()) -// } -// } - -// impl<'a, D> Pretty<'a, D, termcolor::ColorSpec> for &TypeParamIdx -// where -// D: pretty::DocAllocator<'a, termcolor::ColorSpec>, -// { -// fn pretty(self, allocator: &'a D) -> pretty::DocBuilder<'a, D, termcolor::ColorSpec> { -// allocator -// .as_string(self) -// .annotate(TypeParamIdx::color_spec()) -// } -// } - -// impl TypeParamIdx { -// fn color_spec() -> termcolor::ColorSpec { -// termcolor::ColorSpec::new() -// } -// } +rustc_index::newtype_index! { + /// An index representing a type parameter. + /// + /// ## Note on indexing of type parameters + /// + /// The index of [`rustc_middle::ty::ParamTy`] is based on all generic parameters in + /// the definition, including lifetimes. Given the following definition: + /// + /// ```rust + /// struct X<'a, T> { f: &'a T } + /// ``` + /// + /// The type of field `f` is `&T1` (not `&T0`) in MIR. However, in Thrust, we ignore lifetime + /// parameters and the index of [`rty::ParamType`](super::ParamType) is based on type parameters only, giving `f` + /// the type `&T0`. [`TypeBuilder`](crate::refine::TypeBuilder) takes care of this difference when translating MIR + /// types to Thrust types. + #[orderable] + #[debug_format = "T{}"] + pub struct TypeParamIdx { } +} + +impl std::fmt::Display for TypeParamIdx { + fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result { + write!(f, "T{}", self.index()) + } +} + +impl<'a, D> Pretty<'a, D, termcolor::ColorSpec> for &TypeParamIdx +where + D: pretty::DocAllocator<'a, termcolor::ColorSpec>, +{ + fn pretty(self, allocator: &'a D) -> pretty::DocBuilder<'a, D, termcolor::ColorSpec> { + allocator + .as_string(self) + .annotate(TypeParamIdx::color_spec()) + } +} + +impl TypeParamIdx { + fn color_spec() -> termcolor::ColorSpec { + termcolor::ColorSpec::new() + } +} pub type RefinedTypeArgs = IndexVec>; pub type TypeArgs = IndexVec>; diff --git a/src/rty/subtyping.rs b/src/rty/subtyping.rs index 3b9cae09..72ec7df6 100644 --- a/src/rty/subtyping.rs +++ b/src/rty/subtyping.rs @@ -123,7 +123,8 @@ where let cs2 = self.relate_sub_refined_type(&got.elem, &expected.elem); clauses.extend(cs2); } - (Type::Param(got), Type::Param(expected)) if got.idx == expected.idx => {} + (Type::Param(got), Type::Param(expected)) + if got.forall_sort_idx == expected.forall_sort_idx => {} _ => panic!( "inconsistent types: got={}, expected={}", got.display(), From 2855cc57643307b68c2c344c062f6b05265e7a0d Mon Sep 17 00:00:00 2001 From: coeff-aij <175928954+coeff-aij@users.noreply.github.com> Date: Sat, 30 May 2026 18:04:51 +0900 Subject: [PATCH 23/55] add: insert declarations of universally quantified predicate variables using (declare-forall-fun) --- src/analyze/annot_fn.rs | 14 +++++++++++++- src/chc.rs | 7 +++++++ src/chc/smtlib2.rs | 32 ++++++++++++++++++++++++++++++++ src/chc/unbox.rs | 11 +++++++++++ 4 files changed, 63 insertions(+), 1 deletion(-) diff --git a/src/analyze/annot_fn.rs b/src/analyze/annot_fn.rs index a9c6f234..3b3e44e8 100644 --- a/src/analyze/annot_fn.rs +++ b/src/analyze/annot_fn.rs @@ -672,8 +672,20 @@ impl<'a, 'tcx> AnnotFnTranslator<'a, 'tcx> { def_id }; + let typeck_results = self.tcx.typeck(self.local_def_id); let pred = if is_unresolved_args { - refine::forall_pred(self.tcx, pred_def_id).into() + let pred = refine::forall_pred(self.tcx, pred_def_id); + let sig = args + .iter() + .map(|e| { + let ty = typeck_results.expr_ty(e); + self.type_builder.build(ty).to_sort() + }) + .collect(); + self.system + .borrow_mut() + .register_forall_pred(pred.clone(), sig); + pred.into() } else { refine::user_defined_pred(self.tcx, pred_def_id).into() }; diff --git a/src/chc.rs b/src/chc.rs index 88e354da..a07c62c8 100644 --- a/src/chc.rs +++ b/src/chc.rs @@ -1,5 +1,7 @@ //! A multi-sorted CHC system with tuples. +use std::collections::HashMap; + use pretty::{termcolor, Pretty}; use rustc_index::IndexVec; @@ -1875,6 +1877,7 @@ pub struct System { pub pred_vars: IndexVec, pub forall_sorts: Vec, pub num_forall_sort_idx: ForallSortIdx, + forall_pred_vars: HashMap, } impl System { @@ -1882,6 +1885,10 @@ impl System { self.pred_vars.push(PredVarDef { sig, debug_info }) } + pub fn register_forall_pred(&mut self, pred: ForallPred, sig: PredSig) { + self.forall_pred_vars.entry(pred).or_insert(sig); + } + pub fn new_forall_sort(&mut self) -> ForallSortIdx { let new_idx = self.num_forall_sort_idx; self.num_forall_sort_idx += 1; diff --git a/src/chc/smtlib2.rs b/src/chc/smtlib2.rs index 617c1ac7..aab762bf 100644 --- a/src/chc/smtlib2.rs +++ b/src/chc/smtlib2.rs @@ -589,6 +589,34 @@ impl<'ctx, 'a> UserDefinedPredDef<'ctx, 'a> { Self { ctx, inner } } } + +pub struct ForallPredDef<'ctx, 'a> { + ctx: &'ctx FormatContext, + symbol: &'a chc::ForallPred, + sig: &'a chc::PredSig, +} + +impl<'ctx, 'a> std::fmt::Display for ForallPredDef<'ctx, 'a> { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + let params = List::closed(self.sig.iter().map(|sort| self.ctx.fmt_sort(sort))); + write!( + f, + "(declare-forall-fun {name} {params} Bool)", + name = self.symbol, + ) + } +} + +impl<'ctx, 'a> ForallPredDef<'ctx, 'a> { + pub fn new( + ctx: &'ctx FormatContext, + symbol: &'a chc::ForallPred, + sig: &'a chc::PredSig, + ) -> Self { + Self { ctx, symbol, sig } + } +} + /// A wrapper around a [`chc::System`] that provides a [`std::fmt::Display`] implementation in SMT-LIB2 format. #[derive(Debug, Clone)] pub struct System<'a> { @@ -604,6 +632,10 @@ impl<'a> std::fmt::Display for System<'a> { writeln!(f, "(declare-forall-sort {})\n", forall_sort_idx)?; } + for (symbol, sig) in &self.inner.forall_pred_vars { + writeln!(f, "{}\n", ForallPredDef::new(&self.ctx, symbol, sig))?; + } + 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 edf3f854..3f856e48 100644 --- a/src/chc/unbox.rs +++ b/src/chc/unbox.rs @@ -164,6 +164,11 @@ fn unbox_user_defined_pred_def(user_defined_pred_def: UserDefinedPredDef) -> Use UserDefinedPredDef { symbol, sig, body } } +fn unbox_forall_pred_var_def((pred, sig): (ForallPred, PredSig)) -> (ForallPred, PredSig) { + let sig = sig.into_iter().map(unbox_sort).collect(); + (pred, sig) +} + /// 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. @@ -178,6 +183,7 @@ pub fn unbox(system: System) -> System { pred_vars, forall_sorts, num_forall_sort_idx, + forall_pred_vars, } = system; let datatypes = datatypes.into_iter().map(unbox_datatype).collect(); let clauses = clauses.into_iter().map(unbox_clause).collect(); @@ -186,6 +192,10 @@ pub fn unbox(system: System) -> System { .into_iter() .map(unbox_user_defined_pred_def) .collect(); + let forall_pred_vars = forall_pred_vars + .into_iter() + .map(unbox_forall_pred_var_def) + .collect(); System { raw_commands, datatypes, @@ -194,5 +204,6 @@ pub fn unbox(system: System) -> System { pred_vars, forall_sorts, num_forall_sort_idx, + forall_pred_vars, } } From 81274967dce0f40b93bd5854b656a6f613435fc0 Mon Sep 17 00:00:00 2001 From: coeff-aij <175928954+coeff-aij@users.noreply.github.com> Date: Sun, 31 May 2026 03:11:11 +0900 Subject: [PATCH 24/55] add: analyze and output dependencies between predicates --- src/chc.rs | 107 ++++++++++++++++++++++++++++++++++++++++++++- src/chc/smtlib2.rs | 65 +++++++++++++++++++++++---- 2 files changed, 163 insertions(+), 9 deletions(-) diff --git a/src/chc.rs b/src/chc.rs index a07c62c8..f31a553e 100644 --- a/src/chc.rs +++ b/src/chc.rs @@ -1,6 +1,7 @@ //! A multi-sorted CHC system with tuples. -use std::collections::HashMap; +use std::collections::{HashMap, HashSet}; +use std::hash::Hash; use pretty::{termcolor, Pretty}; use rustc_index::IndexVec; @@ -1192,6 +1193,19 @@ impl Pred { } } +impl TryFrom for ForallPred { + type Error = String; + fn try_from(value: Pred) -> Result { + if let Pred::ForallPred(forall_pred) = value { + Ok(forall_pred) + } else { + Err(format!( + "expected the variant `Pred::ForallPred`, got {value:#?}." + )) + } + } +} + /// An atom is a predicate applied to a list of terms. #[derive(Debug, Clone)] pub struct Atom { @@ -1867,6 +1881,33 @@ pub struct UserDefinedPredDef { body: String, } +pub fn compute_transitive_closure(direct_deps: &HashMap>) -> HashMap> +where + T: Clone + Eq + Hash, +{ + let mut closure = HashMap::new(); + + for start_id in direct_deps.keys() { + let mut visited = HashSet::new(); + let mut stack = vec![start_id.clone()]; + + // Search by DFS + while let Some(current_id) = stack.pop() { + if let Some(deps) = direct_deps.get(¤t_id) { + for next_id in deps { + if visited.insert(next_id.clone()) { + stack.push(next_id.clone()); + } + } + } + } + + closure.insert(start_id.clone(), visited); + } + + closure +} + /// A CHC system. #[derive(Debug, Clone, Default)] pub struct System { @@ -1918,6 +1959,70 @@ impl System { Some(self.clauses.push(clause)) } + fn compute_forall_dependency(clause: &Clause) -> HashSet { + clause + .body + .iter_atoms() + .filter_map(|atom| atom.pred.clone().try_into().ok()) + .collect() + } + + fn compute_exists_dependency(clause: &Clause) -> HashSet { + clause + .body + .iter_atoms() + .filter_map(|atom| match atom.pred { + Pred::Var(id) => Some(id), + _ => None, + }) + .collect() + } + + fn compute_dependency(&self) -> HashMap> { + let mut exists_deps: HashMap> = HashMap::new(); + let mut forall_deps: HashMap> = HashMap::new(); + + for (clause_idx, clause) in self.clauses.iter_enumerated() { + let Pred::Var(head_id) = clause.head.pred else { + continue; + }; + + let exists = Self::compute_exists_dependency(clause); + let forall = Self::compute_forall_dependency(clause); + + tracing::debug!( + "exists deps for {:?} at {:?}: {:?}", + head_id, + clause_idx, + exists + ); + + exists_deps.entry(head_id).or_default().extend(exists); + forall_deps.entry(head_id).or_default().extend(forall); + } + tracing::debug!("direct forall dependencies: {:#?}", forall_deps); + tracing::debug!("direct exists dependencies: {:#?}", exists_deps); + + let transitive_exists_deps = compute_transitive_closure(&exists_deps); + tracing::debug!("transitive exists dependencies: {:#?}", exists_deps); + + let mut propagated_forall_deps = HashMap::new(); + + for (pred, reachable_preds) in transitive_exists_deps { + let mut deps = forall_deps.get(&pred).cloned().unwrap_or_default(); + + for reachable in reachable_preds { + if let Some(foralls) = forall_deps.get(&reachable) { + deps.extend(foralls.iter().cloned()); + } + } + + propagated_forall_deps.insert(pred, deps); + } + + propagated_forall_deps + } + pub fn smtlib2(&self) -> smtlib2::System<'_> { smtlib2::System::new(self) } diff --git a/src/chc/smtlib2.rs b/src/chc/smtlib2.rs index aab762bf..6546ffac 100644 --- a/src/chc/smtlib2.rs +++ b/src/chc/smtlib2.rs @@ -6,6 +6,8 @@ //! such as naming convention and solver-specific workarounds. //! The output of this module is what gets passed to the external CHC solver. +use std::collections::HashSet; + use crate::chc::{self, format_context::FormatContext}; /// A helper struct to display a list of items. @@ -617,6 +619,44 @@ impl<'ctx, 'a> ForallPredDef<'ctx, 'a> { } } +pub struct DepExistsPredVarDef<'ctx, 'a> { + ctx: &'ctx FormatContext, + id: &'a chc::PredVarId, + def: &'a chc::PredVarDef, + dependencies: &'a HashSet, +} + +impl<'ctx, 'a> std::fmt::Display for DepExistsPredVarDef<'ctx, 'a> { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + if !self.def.debug_info.is_empty() { + writeln!(f, "{}", self.def.debug_info.display("; "))?; + } + writeln!( + f, + "(declare-dep-exists-fun {} {} {} Bool)", + self.id, + List::closed(self.dependencies), + List::closed(self.def.sig.iter().map(|s| self.ctx.fmt_sort(s))), + ) + } +} + +impl<'ctx, 'a> DepExistsPredVarDef<'ctx, 'a> { + pub fn new( + ctx: &'ctx FormatContext, + id: &'a chc::PredVarId, + def: &'a chc::PredVarDef, + dependencies: &'a HashSet, + ) -> Self { + Self { + ctx, + id, + def, + dependencies, + } + } +} + /// A wrapper around a [`chc::System`] that provides a [`std::fmt::Display`] implementation in SMT-LIB2 format. #[derive(Debug, Clone)] pub struct System<'a> { @@ -656,16 +696,25 @@ impl<'a> std::fmt::Display for System<'a> { } writeln!(f)?; + let dependencies = self.inner.compute_dependency(); for (p, def) in self.inner.pred_vars.iter_enumerated() { - if !def.debug_info.is_empty() { - writeln!(f, "{}", def.debug_info.display("; "))?; + if dependencies.contains_key(&p) && !dependencies[&p].is_empty() { + writeln!( + f, + "{}\n", + DepExistsPredVarDef::new(&self.ctx, &p, def, &dependencies[&p]) + )?; + } else { + if !def.debug_info.is_empty() { + writeln!(f, "{}", def.debug_info.display("; "))?; + } + writeln!( + f, + "(declare-fun {} {} Bool)\n", + p, + List::closed(def.sig.iter().map(|s| self.ctx.fmt_sort(s))) + )?; } - writeln!( - f, - "(declare-fun {} {} Bool)\n", - p, - List::closed(def.sig.iter().map(|s| self.ctx.fmt_sort(s))) - )?; } for (id, clause) in self.inner.clauses.iter_enumerated() { writeln!( From 23187ce4217f52a0d6d3278062536c5d59522116 Mon Sep 17 00:00:00 2001 From: coeff-aij <175928954+coeff-aij@users.noreply.github.com> Date: Wed, 3 Jun 2026 21:14:37 +0900 Subject: [PATCH 25/55] add: translate alias type into forall sort --- src/refine/template.rs | 10 +++++++++- src/rty.rs | 42 ++++++++++++++++++++++++++++++++++++++++-- 2 files changed, 49 insertions(+), 3 deletions(-) diff --git a/src/refine/template.rs b/src/refine/template.rs index e283b06d..5382353a 100644 --- a/src/refine/template.rs +++ b/src/refine/template.rs @@ -140,6 +140,14 @@ impl<'tcx> TypeBuilder<'tcx> { rty::ParamType::new(param_local_idx, *forall_sort_idx).into() } + fn translate_alias_type(&self, ty: &mir_ty::AliasTy) -> rty::Type { + let mut type_params = self.type_params.borrow_mut(); + let index = type_params + .entry(TypeParam::AssocType(ty.def_id)) + .or_insert_with(|| self.system.borrow_mut().new_forall_sort()); + rty::AliasType::new(*index).into() + } + /// Replaces {closure} types with thrust_models::Closure<{closure}>. /// /// Ideally, we want to have `impl Model for F where F: Fn` instead of this and let @@ -301,7 +309,7 @@ impl<'tcx> TypeBuilder<'tcx> { unimplemented!("unsupported ADT: {:?}", ty); } } - // mir_ty::TyKind::Alias(_, ty) => self.translate_alias_type(ty), + mir_ty::TyKind::Alias(_, ty) => self.translate_alias_type(ty), kind => unimplemented!("unrefined_ty: {:?}", kind), } } diff --git a/src/rty.rs b/src/rty.rs index dcf9576f..da781836 100644 --- a/src/rty.rs +++ b/src/rty.rs @@ -763,6 +763,30 @@ impl ParamType { } } +#[derive(Debug, Clone)] +pub struct AliasType { + forall_sort_idx: ForallSortIdx, +} + +impl<'a, D> Pretty<'a, D, termcolor::ColorSpec> for &AliasType +where + D: pretty::DocAllocator<'a, termcolor::ColorSpec>, +{ + fn pretty(self, allocator: &'a D) -> pretty::DocBuilder<'a, D, termcolor::ColorSpec> { + self.forall_sort_idx.pretty(allocator) + } +} + +impl AliasType { + pub fn new(forall_sort_idx: ForallSortIdx) -> Self { + AliasType { forall_sort_idx } + } + + pub fn forall_sort_index(&self) -> ForallSortIdx { + self.forall_sort_idx + } +} + /// An array type. #[derive(Debug, Clone)] pub struct ArrayType { @@ -854,6 +878,7 @@ pub enum Type { String, Never, Param(ParamType), + Alias(AliasType), Pointer(PointerType), Function(FunctionType), Tuple(TupleType), @@ -867,6 +892,12 @@ impl From for Type { } } +impl From for Type { + fn from(t: AliasType) -> Type { + Type::Alias(t) + } +} + impl From for Type { fn from(t: FunctionType) -> Type { Type::Function(t) @@ -910,6 +941,7 @@ where Type::String => allocator.text("string"), Type::Never => allocator.text("!"), Type::Param(ty) => ty.pretty(allocator), + Type::Alias(ty) => ty.pretty(allocator), Type::Pointer(ty) => ty.pretty(allocator), Type::Function(ty) => ty.pretty(allocator), Type::Tuple(ty) => ty.pretty(allocator), @@ -1043,6 +1075,7 @@ impl Type { Type::String => chc::Sort::null(), Type::Never => chc::Sort::null(), Type::Param(ty) => chc::Sort::forall(ty.forall_sort_index()), + Type::Alias(ty) => chc::Sort::Forall(ty.forall_sort_index()), Type::Pointer(ty) => { let elem_sort = ty.elem.ty.to_sort(); @@ -1080,6 +1113,7 @@ impl Type { Type::String => Type::String, Type::Never => Type::Never, Type::Param(ty) => Type::Param(ty), + Type::Alias(ty) => Type::Alias(ty), Type::Pointer(ty) => Type::Pointer(ty.subst_var(f)), Type::Function(ty) => Type::Function(ty), Type::Tuple(ty) => Type::Tuple(ty.subst_var(f)), @@ -1098,6 +1132,7 @@ impl Type { Type::String => Type::String, Type::Never => Type::Never, Type::Param(ty) => Type::Param(ty), + Type::Alias(ty) => Type::Alias(ty), Type::Pointer(ty) => Type::Pointer(ty.map_var(f)), Type::Function(ty) => Type::Function(ty), Type::Tuple(ty) => Type::Tuple(ty.map_var(f)), @@ -1117,6 +1152,7 @@ impl Type { Type::String => Type::String, Type::Never => Type::Never, Type::Param(ty) => Type::Param(ty), + Type::Alias(ty) => Type::Alias(ty), Type::Pointer(ty) => Type::Pointer(ty.strip_refinement()), Type::Function(ty) => Type::Function(ty), Type::Tuple(ty) => Type::Tuple(ty.strip_refinement()), @@ -1127,7 +1163,9 @@ impl Type { pub fn free_ty_params(&self) -> HashSet { match self { - Type::Int | Type::Bool | Type::String | Type::Never => Default::default(), + Type::Int | Type::Bool | Type::String | Type::Never | Type::Alias(_) => { + Default::default() + } Type::Param(ty) => std::iter::once(ty.type_param_index()).collect(), Type::Pointer(ty) => ty.free_ty_params(), Type::Function(ty) => ty.free_ty_params(), @@ -1693,7 +1731,7 @@ impl RefinedType { { self.refinement.subst_ty_params_in_sorts(subst); match &mut self.ty { - Type::Int | Type::Bool | Type::String | Type::Never => {} + Type::Int | Type::Bool | Type::String | Type::Never | Type::Alias(_) => {} Type::Param(ty) => { if let Some(rty) = subst.get(ty.type_param_index()) { let RefinedType { From 01f9f6cf026c16b3c311f58a1b4c12af79740b26 Mon Sep 17 00:00:00 2001 From: coeff-aij <175928954+coeff-aij@users.noreply.github.com> Date: Wed, 3 Jun 2026 21:16:16 +0900 Subject: [PATCH 26/55] add: tests for unknown type parameters --- tests/ui/pass/traits/simple_loop_call.rs | 45 ++++++++++++++++++++++++ tests/ui/pass/traits/simple_loop_self.rs | 28 +++++++++++++++ 2 files changed, 73 insertions(+) create mode 100644 tests/ui/pass/traits/simple_loop_call.rs create mode 100644 tests/ui/pass/traits/simple_loop_self.rs diff --git a/tests/ui/pass/traits/simple_loop_call.rs b/tests/ui/pass/traits/simple_loop_call.rs new file mode 100644 index 00000000..de2f0e82 --- /dev/null +++ b/tests/ui/pass/traits/simple_loop_call.rs @@ -0,0 +1,45 @@ +//@check-pass +//@compile-flags: -C debug-assertions=off +//@rustc-env: THRUST_SOLVER=tests/thrust-pcsat-wrapper THRUST_SOLVER_TIMEOUT_SECS=60 + +#[thrust_macros::context] +trait A { + #[thrust_macros::requires(Self::p(x))] + #[thrust_macros::ensures(Self::p(result))] + fn f(&self, x: i64) -> i64; + + #[thrust_macros::predicate] + fn p(x: i64) -> bool; +} + +#[thrust_macros::requires(T::p(x))] +#[thrust_macros::ensures(T::p(result))] +fn target(a: &T, x: i64) -> i64 { + let mut v = x; + let mut i = 0; + while i < 3 { + v = a.f(v); + i += 1; + } + + v +} + +struct B(i64); + +impl A for B { + #[thrust_macros::requires(Self::p(x))] + #[thrust_macros::ensures(Self::p(result))] + fn f(&self, x: i64) -> i64{ + x + } + + #[thrust_macros::predicate] + fn p(x: i64) -> bool { + "(> x 0)"; true + } +} + +fn main() { + +} diff --git a/tests/ui/pass/traits/simple_loop_self.rs b/tests/ui/pass/traits/simple_loop_self.rs new file mode 100644 index 00000000..0c026e06 --- /dev/null +++ b/tests/ui/pass/traits/simple_loop_self.rs @@ -0,0 +1,28 @@ +//@check-pass +//@compile-flags: -C debug-assertions=off +//@rustc-env: THRUST_SOLVER=tests/thrust-pcsat-wrapper THRUST_SOLVER_TIMEOUT_SECS=60 + +#[thrust_macros::context] +trait A { + #[thrust_macros::requires(Self::p(*self, x))] + #[thrust_macros::ensures(Self::p(*self, result))] + fn f(&self, x: i64) -> i64; + + #[thrust_macros::predicate] + fn p(self, x: i64) -> bool; +} + +#[thrust_macros::requires(T::p(*a, x))] +#[thrust_macros::ensures(T::p(*a, result))] +fn target(a: &T, x: i64) -> i64 { + let mut v = x; + let mut i = 0; + while i < 3 { + v = a.f(v); + i += 1; + } + + v +} + +fn main() {} From 743bcdaa7c59d201dcef2ced448ca746ad469dea Mon Sep 17 00:00:00 2001 From: coeff-aij <175928954+coeff-aij@users.noreply.github.com> Date: Mon, 8 Jun 2026 15:39:43 +0900 Subject: [PATCH 27/55] fix: propagate owner_fn_id of type parameters --- src/analyze/annot_fn.rs | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/analyze/annot_fn.rs b/src/analyze/annot_fn.rs index 3b3e44e8..97dacd98 100644 --- a/src/analyze/annot_fn.rs +++ b/src/analyze/annot_fn.rs @@ -682,7 +682,8 @@ impl<'a, 'tcx> AnnotFnTranslator<'a, 'tcx> { self.type_builder.build(ty).to_sort() }) .collect(); - self.system + self.analyzer + .system .borrow_mut() .register_forall_pred(pred.clone(), sig); pred.into() From d5cdefb0e874bbb7eaab72a860a18e5aca3ce5c9 Mon Sep 17 00:00:00 2001 From: coeff-aij <175928954+coeff-aij@users.noreply.github.com> Date: Thu, 4 Jun 2026 00:24:40 +0900 Subject: [PATCH 28/55] add: debug print for AliasTy --- src/refine/template.rs | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) diff --git a/src/refine/template.rs b/src/refine/template.rs index 5382353a..5b5cf58f 100644 --- a/src/refine/template.rs +++ b/src/refine/template.rs @@ -144,7 +144,16 @@ impl<'tcx> TypeBuilder<'tcx> { let mut type_params = self.type_params.borrow_mut(); let index = type_params .entry(TypeParam::AssocType(ty.def_id)) - .or_insert_with(|| self.system.borrow_mut().new_forall_sort()); + .or_insert_with(|| { + let idx = self.system.borrow_mut().new_forall_sort(); + tracing::debug!( + "issue the new ForallSortIdx {} for AliasTy {:?}.", + idx, + ty, + ); + idx + }); + rty::AliasType::new(*index).into() } From 0dc245d2d299fe5600741d9e343f3e18fbae542f Mon Sep 17 00:00:00 2001 From: coeff-aij <175928954+coeff-aij@users.noreply.github.com> Date: Mon, 8 Jun 2026 15:41:12 +0900 Subject: [PATCH 29/55] fix: propagate owner_fn_id of type parameters --- src/analyze/annot_fn.rs | 9 ++++++++- src/refine/template.rs | 8 ++------ 2 files changed, 10 insertions(+), 7 deletions(-) diff --git a/src/analyze/annot_fn.rs b/src/analyze/annot_fn.rs index 97dacd98..9705528b 100644 --- a/src/analyze/annot_fn.rs +++ b/src/analyze/annot_fn.rs @@ -243,7 +243,9 @@ impl<'a, 'tcx> AnnotFnTranslator<'a, 'tcx> { .instantiate_generics(ty, self.generic_args) .unwrap_or(ty); let typing_env = mir_ty::TypingEnv::fully_monomorphized(); - self.tcx.normalize_erasing_regions(typing_env, instantiated) + self.tcx + .try_normalize_erasing_regions(typing_env, instantiated) + .unwrap_or(instantiated) } fn pat_ty(&self, pat: &'tcx rustc_hir::Pat<'tcx>) -> mir_ty::Ty<'tcx> { @@ -682,6 +684,11 @@ impl<'a, 'tcx> AnnotFnTranslator<'a, 'tcx> { self.type_builder.build(ty).to_sort() }) .collect(); + tracing::debug!( + "register ForallPred {:?} with signature {:?}", + pred, + sig + ); self.analyzer .system .borrow_mut() diff --git a/src/refine/template.rs b/src/refine/template.rs index 5b5cf58f..adf5baff 100644 --- a/src/refine/template.rs +++ b/src/refine/template.rs @@ -146,14 +146,10 @@ impl<'tcx> TypeBuilder<'tcx> { .entry(TypeParam::AssocType(ty.def_id)) .or_insert_with(|| { let idx = self.system.borrow_mut().new_forall_sort(); - tracing::debug!( - "issue the new ForallSortIdx {} for AliasTy {:?}.", - idx, - ty, - ); + tracing::debug!("issue the new ForallSortIdx {} for AliasTy {:?}.", idx, ty,); idx }); - + rty::AliasType::new(*index).into() } From 5d5026458460ecbd5cb835ef7ef41a662fd6f71c Mon Sep 17 00:00:00 2001 From: coeff-aij <175928954+coeff-aij@users.noreply.github.com> Date: Thu, 4 Jun 2026 20:09:31 +0900 Subject: [PATCH 30/55] add: translate ::Ty into ParamTy --- src/refine/template.rs | 20 ++++++++++++++++++-- 1 file changed, 18 insertions(+), 2 deletions(-) diff --git a/src/refine/template.rs b/src/refine/template.rs index adf5baff..369ff4c5 100644 --- a/src/refine/template.rs +++ b/src/refine/template.rs @@ -208,7 +208,11 @@ impl<'tcx> TypeBuilder<'tcx> { .tcx .try_normalize_erasing_regions(self.typing_env, projection_ty) { - tracing::debug!("the type {:#?} is resolved as the type {:#?}.", orig_ty, ty); + tracing::debug!( + "the type {:#?} is normalized as the type {:#?}.", + orig_ty, + normalized_ty + ); let contains_model_ty_alias = normalized_ty.walk().any(|arg| { if let mir_ty::GenericArgKind::Type(t) = arg.kind() { matches!(t.kind(), mir_ty::TyKind::Alias(_, alias_ty) if alias_ty.def_id == model_ty_def_id) @@ -314,7 +318,19 @@ impl<'tcx> TypeBuilder<'tcx> { unimplemented!("unsupported ADT: {:?}", ty); } } - mir_ty::TyKind::Alias(_, ty) => self.translate_alias_type(ty), + mir_ty::TyKind::Alias(mir_ty::AliasTyKind::Projection, ty) => { + if let Some(model_ty_def_id) = self.def_ids.model_ty() { + let arg_ty = ty.args.type_at(0); + + if ty.def_id == model_ty_def_id + && matches!(arg_ty.kind(), mir_ty::TyKind::Param(_)) + { + return self.build(arg_ty); + } + } + + self.translate_alias_type(ty) + } kind => unimplemented!("unrefined_ty: {:?}", kind), } } From 516cbd522f4926ba5b53f8b4a868b555027c16b7 Mon Sep 17 00:00:00 2001 From: coeff-aij <175928954+coeff-aij@users.noreply.github.com> Date: Mon, 8 Jun 2026 12:34:30 +0900 Subject: [PATCH 31/55] add: register_generic_def() for substitution of generic args from call site --- src/analyze.rs | 76 +++++++++++++++++++++++++++++----------- src/analyze/crate_.rs | 9 ++++- src/analyze/local_def.rs | 5 +++ 3 files changed, 68 insertions(+), 22 deletions(-) diff --git a/src/analyze.rs b/src/analyze.rs index 439b1456..3bd42386 100644 --- a/src/analyze.rs +++ b/src/analyze.rs @@ -160,9 +160,18 @@ struct DeferredDefTy<'tcx> { mode: DeferredDefMode, } +#[derive(Debug, Clone)] +struct GenericDefTy<'tcx> { + // this is different from a key in defs when the def is extern_spec_fn + local_def_id: LocalDefId, + cache: Rc, rty::RefinedType>>>, + rty: rty::RefinedType, +} + #[derive(Debug, Clone)] enum DefTy<'tcx> { Concrete(rty::RefinedType), + Generic(GenericDefTy<'tcx>), Deferred(DeferredDefTy<'tcx>), } @@ -408,9 +417,27 @@ impl<'tcx> Analyzer<'tcx> { }); } + pub fn register_generic_def( + &mut self, + target_def_id: DefId, + local_def_id: LocalDefId, + rty: rty::RefinedType, + ) { + tracing::info!(?target_def_id, ?local_def_id, rty = %rty.display(), "register_generic_def"); + self.defs.insert( + target_def_id, + DefTy::Generic(GenericDefTy { + rty, + local_def_id, + cache: Rc::new(RefCell::new(HashMap::new())), + }), + ); + } + pub fn concrete_def_ty(&self, def_id: DefId) -> Option<&rty::RefinedType> { self.defs.get(&def_id).and_then(|def_ty| match def_ty { DefTy::Concrete(rty) => Some(rty), + DefTy::Generic(GenericDefTy { rty, .. }) => Some(rty), DefTy::Deferred(_) => None, }) } @@ -432,6 +459,7 @@ impl<'tcx> Analyzer<'tcx> { ); let mut def_ty = match self.defs.get(&def_id)? { DefTy::Concrete(rty) => rty.clone(), + DefTy::Generic(generic) => generic.cache.borrow().get(&generic_args)?.clone(), DefTy::Deferred(deferred) => deferred.cache.borrow().get(&generic_args)?.clone(), }; def_ty.instantiate_ty_params( @@ -477,29 +505,35 @@ impl<'tcx> Analyzer<'tcx> { ) -> Option { let type_builder = self.type_builder(self.def_ids(), caller_def_id); - let deferred_ty = match self.defs.get(&def_id)? { - DefTy::Concrete(rty) => { - let mut def_ty = rty.clone(); - def_ty.instantiate_ty_params( - generic_args - .types() - .map(|ty| type_builder.build(ty)) - .map(rty::RefinedType::unrefined) - .collect(), - ); - return Some(def_ty); - } - DefTy::Deferred(deferred) => deferred, - }; + let (local_def_id, instantiated_ty_cache, deferred_ty_mode) = + match self.defs.get(&def_id)? { + DefTy::Concrete(rty) => { + let mut def_ty = rty.clone(); + def_ty.instantiate_ty_params( + generic_args + .types() + .map(|ty| type_builder.build(ty)) + .map(rty::RefinedType::unrefined) + .collect(), + ); + return Some(def_ty); + } + DefTy::Generic(generic) => (generic.local_def_id, Rc::clone(&generic.cache), None), + DefTy::Deferred(deferred) => ( + deferred.local_def_id, + Rc::clone(&deferred.cache), + Some(deferred.mode), + ), + }; - let deferred_ty_cache = Rc::clone(&deferred_ty.cache); // to cut reference to allow &mut self - if let Some(rty) = deferred_ty_cache.borrow().get(&generic_args) { + if let Some(rty) = instantiated_ty_cache.borrow().get(&generic_args) { return Some(rty.clone()); } - let deferred_ty_mode = deferred_ty.mode; - let mut analyzer = self.local_def_analyzer(deferred_ty.local_def_id); - analyzer.generic_args(generic_args); + let mut analyzer = self.local_def_analyzer(local_def_id); + analyzer + .owner_fn_id(caller_def_id) + .generic_args(generic_args); let mut expected = analyzer.expected_ty(); // parameters in annotations are left as params @@ -511,12 +545,12 @@ impl<'tcx> Analyzer<'tcx> { .map(rty::RefinedType::unrefined) .collect(), ); - deferred_ty_cache + instantiated_ty_cache .borrow_mut() .insert(generic_args, expected.clone()); tracing::info!(?def_id, rty = %expected.display(), ?generic_args, "deferred def"); - if deferred_ty_mode.should_analyze() { + if deferred_ty_mode.is_some_and(|mode| mode.should_analyze()) { let mut body_analyzer = if analyzer.local_def_id().to_def_id() == def_id { analyzer } else { diff --git a/src/analyze/crate_.rs b/src/analyze/crate_.rs index 58bd309e..bec659e3 100644 --- a/src/analyze/crate_.rs +++ b/src/analyze/crate_.rs @@ -69,6 +69,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { #[tracing::instrument(skip(self), fields(def_id = %self.tcx.def_path_str(local_def_id)))] fn refine_fn_def(&mut self, local_def_id: LocalDefId) { + let sig = self.ctx.fn_sig(local_def_id.to_def_id()); let mut analyzer = self.ctx.local_def_analyzer(local_def_id); if analyzer.is_annotated_as_trusted() { @@ -113,7 +114,13 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { let owner_fn_id = analyzer.owner_fn_id; let expected = analyzer.expected_ty(); - self.ctx.register_def(owner_fn_id, expected); + use mir_ty::TypeVisitableExt as _; + if sig.has_param() { + self.ctx + .register_generic_def(owner_fn_id, local_def_id, expected); + } else { + self.ctx.register_def(owner_fn_id, expected); + } } fn analyze_local_defs(&mut self) { diff --git a/src/analyze/local_def.rs b/src/analyze/local_def.rs index 6f717ef8..7e912627 100644 --- a/src/analyze/local_def.rs +++ b/src/analyze/local_def.rs @@ -1231,6 +1231,11 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { self.local_def_id } + pub fn owner_fn_id(&mut self, owner_fn_id: DefId) -> &mut Self { + self.owner_fn_id = owner_fn_id; + self + } + pub fn generic_args(&mut self, generic_args: mir_ty::GenericArgsRef<'tcx>) -> &mut Self { self.generic_args = generic_args; self.body = From 6de74be128e656c91739f7aeb1a6a12e2fb449ce Mon Sep 17 00:00:00 2001 From: coeff-aij <175928954+coeff-aij@users.noreply.github.com> Date: Sun, 7 Jun 2026 23:36:32 +0900 Subject: [PATCH 32/55] fix: instantiate generic type parameters contained in args of predicate calls --- src/analyze/annot_fn.rs | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/analyze/annot_fn.rs b/src/analyze/annot_fn.rs index 9705528b..c1872560 100644 --- a/src/analyze/annot_fn.rs +++ b/src/analyze/annot_fn.rs @@ -681,6 +681,9 @@ impl<'a, 'tcx> AnnotFnTranslator<'a, 'tcx> { .iter() .map(|e| { let ty = typeck_results.expr_ty(e); + let ty = self + .instantiate_generics(ty, generic_args) + .unwrap_or(ty); self.type_builder.build(ty).to_sort() }) .collect(); From b921e2cad5116f66ab2c958039d0694a35b4b7dd Mon Sep 17 00:00:00 2001 From: coeff-aij <175928954+coeff-aij@users.noreply.github.com> Date: Mon, 8 Jun 2026 12:48:13 +0900 Subject: [PATCH 33/55] add: distinguish calls of forall-predicates with different type parameters --- src/analyze/annot_fn.rs | 11 +++-------- src/chc.rs | 26 ++++++++++++++++++++------ src/chc/format_context.rs | 5 +++++ src/chc/smtlib2.rs | 23 ++++++++++------------- src/chc/unbox.rs | 6 +++--- src/refine.rs | 6 +++--- 6 files changed, 44 insertions(+), 33 deletions(-) diff --git a/src/analyze/annot_fn.rs b/src/analyze/annot_fn.rs index c1872560..fe88537f 100644 --- a/src/analyze/annot_fn.rs +++ b/src/analyze/annot_fn.rs @@ -676,8 +676,7 @@ impl<'a, 'tcx> AnnotFnTranslator<'a, 'tcx> { let typeck_results = self.tcx.typeck(self.local_def_id); let pred = if is_unresolved_args { - let pred = refine::forall_pred(self.tcx, pred_def_id); - let sig = args + let sig: Vec = args .iter() .map(|e| { let ty = typeck_results.expr_ty(e); @@ -687,15 +686,11 @@ impl<'a, 'tcx> AnnotFnTranslator<'a, 'tcx> { self.type_builder.build(ty).to_sort() }) .collect(); - tracing::debug!( - "register ForallPred {:?} with signature {:?}", - pred, - sig - ); + let pred = refine::forall_pred(self.tcx, pred_def_id, sig); self.analyzer .system .borrow_mut() - .register_forall_pred(pred.clone(), sig); + .register_forall_pred(pred.clone()); pred.into() } else { refine::user_defined_pred(self.tcx, pred_def_id).into() diff --git a/src/chc.rs b/src/chc.rs index f31a553e..53662747 100644 --- a/src/chc.rs +++ b/src/chc.rs @@ -1050,6 +1050,7 @@ impl UserDefinedPred { #[derive(Debug, Clone, PartialEq, Eq, Hash)] pub struct ForallPred { inner: String, + args: Vec, } impl std::fmt::Display for ForallPred { @@ -1061,15 +1062,28 @@ impl std::fmt::Display for ForallPred { impl<'a, D> Pretty<'a, D, termcolor::ColorSpec> for &ForallPred where D: pretty::DocAllocator<'a, termcolor::ColorSpec>, + D::Doc: Clone, { fn pretty(self, allocator: &'a D) -> pretty::DocBuilder<'a, D, termcolor::ColorSpec> { - allocator.text(self.inner.clone()) + let args = allocator.intersperse( + self.args.iter().map(|a| a.pretty(allocator)), + allocator.text(", "), + ); + allocator + .text("forall_pred") + .append( + allocator + .as_string(&self.inner) + .append(args.angles()) + .angles(), + ) + .group() } } impl ForallPred { - pub fn new(inner: String) -> Self { - Self { inner } + pub fn new(inner: String, args: Vec) -> Self { + Self { inner, args } } } @@ -1918,7 +1932,7 @@ pub struct System { pub pred_vars: IndexVec, pub forall_sorts: Vec, pub num_forall_sort_idx: ForallSortIdx, - forall_pred_vars: HashMap, + forall_pred_vars: HashSet, } impl System { @@ -1926,8 +1940,8 @@ impl System { self.pred_vars.push(PredVarDef { sig, debug_info }) } - pub fn register_forall_pred(&mut self, pred: ForallPred, sig: PredSig) { - self.forall_pred_vars.entry(pred).or_insert(sig); + pub fn register_forall_pred(&mut self, pred: ForallPred) { + self.forall_pred_vars.insert(pred); } pub fn new_forall_sort(&mut self) -> ForallSortIdx { diff --git a/src/chc/format_context.rs b/src/chc/format_context.rs index 86895e02..ad54df74 100644 --- a/src/chc/format_context.rs +++ b/src/chc/format_context.rs @@ -348,6 +348,11 @@ impl FormatContext { format!("matcher_pred<{}>", self.fmt_datatype_symbol(sym)) } + pub fn forall_pred(&self, p: &chc::ForallPred) -> impl std::fmt::Display { + let ss = SortSymbols::new(&p.args); + format!("{}{}", p.inner, ss) + } + fn fmt_sort_impl(&self, sort: &chc::Sort) -> Box { match sort { chc::Sort::Array(s1, s2) => { diff --git a/src/chc/smtlib2.rs b/src/chc/smtlib2.rs index 6546ffac..929ff547 100644 --- a/src/chc/smtlib2.rs +++ b/src/chc/smtlib2.rs @@ -234,6 +234,7 @@ impl<'ctx, 'a> std::fmt::Display for Atom<'ctx, 'a> { } let pred = match &self.inner.pred { chc::Pred::Matcher(p) => self.ctx.matcher_pred(p).to_string(), + chc::Pred::ForallPred(p) => self.ctx.forall_pred(p).to_string(), p => p.name().into_owned(), }; if self.inner.args.is_empty() { @@ -594,28 +595,24 @@ impl<'ctx, 'a> UserDefinedPredDef<'ctx, 'a> { pub struct ForallPredDef<'ctx, 'a> { ctx: &'ctx FormatContext, - symbol: &'a chc::ForallPred, - sig: &'a chc::PredSig, + pred: &'a chc::ForallPred, } impl<'ctx, 'a> std::fmt::Display for ForallPredDef<'ctx, 'a> { fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { - let params = List::closed(self.sig.iter().map(|sort| self.ctx.fmt_sort(sort))); + let params = self.pred.args.iter().map(|sort| self.ctx.fmt_sort(sort)); + let params = List::closed(params); write!( f, "(declare-forall-fun {name} {params} Bool)", - name = self.symbol, + name = self.ctx.forall_pred(self.pred), ) } } impl<'ctx, 'a> ForallPredDef<'ctx, 'a> { - pub fn new( - ctx: &'ctx FormatContext, - symbol: &'a chc::ForallPred, - sig: &'a chc::PredSig, - ) -> Self { - Self { ctx, symbol, sig } + pub fn new(ctx: &'ctx FormatContext, pred: &'a chc::ForallPred) -> Self { + Self { ctx, pred } } } @@ -635,7 +632,7 @@ impl<'ctx, 'a> std::fmt::Display for DepExistsPredVarDef<'ctx, 'a> { f, "(declare-dep-exists-fun {} {} {} Bool)", self.id, - List::closed(self.dependencies), + List::closed(self.dependencies.iter().map(|p| self.ctx.forall_pred(p))), List::closed(self.def.sig.iter().map(|s| self.ctx.fmt_sort(s))), ) } @@ -672,8 +669,8 @@ impl<'a> std::fmt::Display for System<'a> { writeln!(f, "(declare-forall-sort {})\n", forall_sort_idx)?; } - for (symbol, sig) in &self.inner.forall_pred_vars { - writeln!(f, "{}\n", ForallPredDef::new(&self.ctx, symbol, sig))?; + for pred in &self.inner.forall_pred_vars { + writeln!(f, "{}\n", ForallPredDef::new(&self.ctx, pred))?; } writeln!(f, "{}\n", Datatypes::new(&self.ctx, self.ctx.datatypes()))?; diff --git a/src/chc/unbox.rs b/src/chc/unbox.rs index 3f856e48..3b8bd6a8 100644 --- a/src/chc/unbox.rs +++ b/src/chc/unbox.rs @@ -164,9 +164,9 @@ fn unbox_user_defined_pred_def(user_defined_pred_def: UserDefinedPredDef) -> Use UserDefinedPredDef { symbol, sig, body } } -fn unbox_forall_pred_var_def((pred, sig): (ForallPred, PredSig)) -> (ForallPred, PredSig) { - let sig = sig.into_iter().map(unbox_sort).collect(); - (pred, sig) +fn unbox_forall_pred_var_def(pred: ForallPred) -> ForallPred { + let args = pred.args.into_iter().map(unbox_sort).collect(); + ForallPred { args, ..pred } } /// Remove all `Box` sorts and `Box`/`BoxCurrent` terms from the system. diff --git a/src/refine.rs b/src/refine.rs index cbbd37c4..5ecd82c9 100644 --- a/src/refine.rs +++ b/src/refine.rs @@ -18,7 +18,7 @@ pub use env::{ Assumption, EnumDefProvider, Env, PlaceType, PlaceTypeBuilder, PlaceTypeVar, TempVarIdx, Var, }; -use crate::chc::{DatatypeSymbol, ForallPred, UserDefinedPred}; +use crate::chc::{DatatypeSymbol, ForallPred, Sort, UserDefinedPred}; use rustc_middle::ty as mir_ty; use rustc_span::def_id::DefId; @@ -41,6 +41,6 @@ pub fn user_defined_pred(tcx: mir_ty::TyCtxt<'_>, did: DefId) -> UserDefinedPred UserDefinedPred::new(stable_def_id_symbol(tcx, did, "p")) } -pub fn forall_pred(tcx: mir_ty::TyCtxt<'_>, did: DefId) -> ForallPred { - ForallPred::new(stable_def_id_symbol(tcx, did, "q")) +pub fn forall_pred(tcx: mir_ty::TyCtxt<'_>, did: DefId, args: Vec) -> ForallPred { + ForallPred::new(stable_def_id_symbol(tcx, did, "q"), args) } From 59f401c5f5918dd5bb3d776a8d955d55d6f810d2 Mon Sep 17 00:00:00 2001 From: coeff-aij <175928954+coeff-aij@users.noreply.github.com> Date: Mon, 8 Jun 2026 01:44:07 +0900 Subject: [PATCH 34/55] fix: skip expected_ty() for trait methods without MIR body --- src/analyze.rs | 38 ++++++++++++++++++++------------------ src/analyze/crate_.rs | 6 +++++- 2 files changed, 25 insertions(+), 19 deletions(-) diff --git a/src/analyze.rs b/src/analyze.rs index 3bd42386..5dbc0d19 100644 --- a/src/analyze.rs +++ b/src/analyze.rs @@ -165,7 +165,7 @@ struct GenericDefTy<'tcx> { // this is different from a key in defs when the def is extern_spec_fn local_def_id: LocalDefId, cache: Rc, rty::RefinedType>>>, - rty: rty::RefinedType, + rty: Option, } #[derive(Debug, Clone)] @@ -421,9 +421,9 @@ impl<'tcx> Analyzer<'tcx> { &mut self, target_def_id: DefId, local_def_id: LocalDefId, - rty: rty::RefinedType, + rty: Option, ) { - tracing::info!(?target_def_id, ?local_def_id, rty = %rty.display(), "register_generic_def"); + tracing::info!(?target_def_id, ?local_def_id, ?rty, "register_generic_def"); self.defs.insert( target_def_id, DefTy::Generic(GenericDefTy { @@ -437,7 +437,7 @@ impl<'tcx> Analyzer<'tcx> { pub fn concrete_def_ty(&self, def_id: DefId) -> Option<&rty::RefinedType> { self.defs.get(&def_id).and_then(|def_ty| match def_ty { DefTy::Concrete(rty) => Some(rty), - DefTy::Generic(GenericDefTy { rty, .. }) => Some(rty), + DefTy::Generic(GenericDefTy { rty, .. }) => rty.as_ref(), DefTy::Deferred(_) => None, }) } @@ -497,6 +497,20 @@ impl<'tcx> Analyzer<'tcx> { Some(formula_fn) } + fn instantiate_generic_args( + ty: &mut rty::RefinedType, + generic_args: mir_ty::GenericArgsRef<'tcx>, + type_builder: &TypeBuilder<'tcx>, + ) { + ty.instantiate_ty_params( + generic_args + .types() + .map(|ty| type_builder.build(ty)) + .map(rty::RefinedType::unrefined) + .collect(), + ); + } + pub fn def_ty_with_args( &mut self, def_id: DefId, @@ -509,13 +523,7 @@ impl<'tcx> Analyzer<'tcx> { match self.defs.get(&def_id)? { DefTy::Concrete(rty) => { let mut def_ty = rty.clone(); - def_ty.instantiate_ty_params( - generic_args - .types() - .map(|ty| type_builder.build(ty)) - .map(rty::RefinedType::unrefined) - .collect(), - ); + Self::instantiate_generic_args(&mut def_ty, generic_args, &type_builder); return Some(def_ty); } DefTy::Generic(generic) => (generic.local_def_id, Rc::clone(&generic.cache), None), @@ -538,13 +546,7 @@ impl<'tcx> Analyzer<'tcx> { let mut expected = analyzer.expected_ty(); // parameters in annotations are left as params // TODO: remove this after annotation V2 - expected.instantiate_ty_params( - generic_args - .types() - .map(|ty| type_builder.build(ty)) - .map(rty::RefinedType::unrefined) - .collect(), - ); + Self::instantiate_generic_args(&mut expected, generic_args, &type_builder); instantiated_ty_cache .borrow_mut() .insert(generic_args, expected.clone()); diff --git a/src/analyze/crate_.rs b/src/analyze/crate_.rs index bec659e3..7918d89a 100644 --- a/src/analyze/crate_.rs +++ b/src/analyze/crate_.rs @@ -113,12 +113,16 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { } let owner_fn_id = analyzer.owner_fn_id; - let expected = analyzer.expected_ty(); use mir_ty::TypeVisitableExt as _; if sig.has_param() { + let expected = self + .tcx + .is_mir_available(owner_fn_id) + .then(|| analyzer.expected_ty()); self.ctx .register_generic_def(owner_fn_id, local_def_id, expected); } else { + let expected = analyzer.expected_ty(); self.ctx.register_def(owner_fn_id, expected); } } From e4ed770ed19658fdd243b025541306fe2720a0f2 Mon Sep 17 00:00:00 2001 From: coeff-aij <175928954+coeff-aij@users.noreply.github.com> Date: Tue, 9 Jun 2026 22:52:39 +0900 Subject: [PATCH 35/55] change: try to bypass the instantiation of unknown generic args on precompute_callable_param_contracts() --- src/analyze/local_def.rs | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/src/analyze/local_def.rs b/src/analyze/local_def.rs index 7e912627..314f88fd 100644 --- a/src/analyze/local_def.rs +++ b/src/analyze/local_def.rs @@ -397,8 +397,12 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { // `def_ty_with_args` directly. fn precompute_callable_param_contracts(&mut self, sig: &mir_ty::FnSig<'tcx>) { for input_ty in sig.inputs() { - let inst = - mir_ty::EarlyBinder::bind(*input_ty).instantiate(self.tcx, self.generic_args); + use crate::rustc_middle::ty::TypeVisitableExt; + let inst = if input_ty.has_param() && self.generic_args.is_empty() { + *input_ty + } else { + mir_ty::EarlyBinder::bind(*input_ty).instantiate(self.tcx, self.generic_args) + }; let inst = self .tcx .normalize_erasing_regions(mir_ty::TypingEnv::fully_monomorphized(), inst); From 686793628db9f87ae02421eea25bb3f17873a8c2 Mon Sep 17 00:00:00 2001 From: coeff-aij <175928954+coeff-aij@users.noreply.github.com> Date: Thu, 11 Jun 2026 12:51:04 +0900 Subject: [PATCH 36/55] add: register FunctionType for type parameters with Fn/FnMut/FnOnce trait --- src/analyze.rs | 11 ++++- src/analyze/annot_fn.rs | 94 +++++++++++++++++++++++++++++++++++++++++ src/refine/template.rs | 10 +++++ 3 files changed, 114 insertions(+), 1 deletion(-) diff --git a/src/analyze.rs b/src/analyze.rs index 5dbc0d19..74b870b4 100644 --- a/src/analyze.rs +++ b/src/analyze.rs @@ -209,7 +209,7 @@ impl refine::EnumDefProvider for Rc> { pub type Env = refine::Env>>; pub type TypeParamMap = HashMap; -#[derive(Eq, PartialEq, Hash)] +#[derive(Eq, PartialEq, Hash, Debug, Clone)] pub enum TypeParam { GenericType(DefId, u32), AssocType(DefId), @@ -243,6 +243,7 @@ pub struct Analyzer<'tcx> { enum_defs: Rc>, type_params: Rc>, + closure_type_params: Rc>>, } impl<'tcx> crate::refine::TemplateRegistry for Analyzer<'tcx> { @@ -271,6 +272,7 @@ impl<'tcx> Analyzer<'tcx> { let basic_blocks = Default::default(); let enum_defs = Default::default(); let type_params = Default::default(); + let closure_type_params = Default::default(); Self { tcx, defs, @@ -280,6 +282,7 @@ impl<'tcx> Analyzer<'tcx> { def_ids: did_cache::DefIdCache::new(tcx), enum_defs, type_params, + closure_type_params, } } @@ -434,6 +437,10 @@ impl<'tcx> Analyzer<'tcx> { ); } + pub fn get_closure_type(&self, type_param: TypeParam) -> Option { + self.closure_type_params.borrow().get(&type_param).cloned() + } + pub fn concrete_def_ty(&self, def_id: DefId) -> Option<&rty::RefinedType> { self.defs.get(&def_id).and_then(|def_ty| match def_ty { DefTy::Concrete(rty) => Some(rty), @@ -455,6 +462,7 @@ impl<'tcx> Analyzer<'tcx> { self.def_ids(), def_id, self.type_params.clone(), + self.closure_type_params.clone(), self.system.clone(), ); let mut def_ty = match self.defs.get(&def_id)? { @@ -703,6 +711,7 @@ impl<'tcx> Analyzer<'tcx> { def_ids, owner_fn_id, self.type_params.clone(), + self.closure_type_params.clone(), self.system.clone(), ) } diff --git a/src/analyze/annot_fn.rs b/src/analyze/annot_fn.rs index fe88537f..e23161e5 100644 --- a/src/analyze/annot_fn.rs +++ b/src/analyze/annot_fn.rs @@ -159,6 +159,7 @@ impl<'a, 'tcx> AnnotFnTranslator<'a, 'tcx> { def_ids.clone(), local_def_id.to_def_id(), analyzer.type_params.clone(), + analyzer.closure_type_params.clone(), analyzer.system.clone(), ); let mut translator = Self { @@ -188,6 +189,7 @@ impl<'a, 'tcx> AnnotFnTranslator<'a, 'tcx> { self.def_ids.clone(), owner_fn_id, self.analyzer.type_params.clone(), + self.analyzer.closure_type_params.clone(), self.analyzer.system.clone(), ); self @@ -298,12 +300,104 @@ impl<'a, 'tcx> AnnotFnTranslator<'a, 'tcx> { recv_ty = *inner; } let mir_ty::TyKind::Closure(def_id, args) = recv_ty.kind() else { + if let mir_ty::TyKind::Param(ty) = recv_ty.kind() { + tracing::debug!("ParamTy is found: {ty:?}"); + let closure_fun_ty = self.type_param_as_callable_sig(*ty); + tracing::debug!( + "the obtained FunctionType for the closure {ty:?}: {closure_fun_ty:#?}" + ); + if let Some(closure_fun_ty) = closure_fun_ty.clone() { + self.type_builder.register_closure_type_param( + analyze::TypeParam::GenericType(self.local_def_id.to_def_id(), ty.index), + closure_fun_ty, + ); + }; + return closure_fun_ty; + } return None; }; self.analyzer .known_function_ty_with_args(*def_id, self.tcx.mk_args(args.as_closure().parent_args())) } + #[tracing::instrument(skip(self))] + fn closure_trait_args( + &self, + param_ty: mir_ty::ParamTy, + pred: mir_ty::TraitPredicate<'tcx>, + ) -> Option>> { + let trait_ref = pred.trait_ref; + if trait_ref.self_ty() != param_ty.to_ty(self.tcx) { + return None; + } + + let receiver_type = self.type_builder.build(trait_ref.args.type_at(0)); + use mir_ty::ClosureKind::*; + let receiver_type = match self.tcx.fn_trait_kind_from_def_id(trait_ref.def_id)? { + Fn => rty::PointerType::immut_to(receiver_type).into(), + FnMut => rty::PointerType::mut_to(receiver_type).into(), + FnOnce => receiver_type, + }; + + let mir_ty::Tuple(other_params) = trait_ref.args.type_at(1).kind() else { + return None; + }; + + let other_params = other_params.iter().map(|ty| { + let ty = self + .instantiate_generics(ty, self.generic_args) + .unwrap_or(ty); + self.type_builder.build(ty) + }); + let params = std::iter::once(receiver_type) + .chain(other_params) + .map(|ty| rty::RefinedType::unrefined(ty.vacuous())) + .collect(); + tracing::debug!("found the signature for closure trait: {params:#?}"); + Some(params) + } + + #[tracing::instrument(skip(self))] + fn closure_trait_ret( + &self, + param_ty: mir_ty::ParamTy, + pred: mir_ty::ProjectionPredicate<'tcx>, + ) -> Option> { + let projection = pred.projection_term; + if projection.def_id != self.tcx.lang_items().fn_once_output()? + || projection.args.type_at(0) != param_ty.to_ty(self.tcx) + { + return None; + } + + let ret_ty = self.type_builder.build(pred.term.expect_type()).vacuous(); + tracing::debug!(?ret_ty); + Some(rty::RefinedType::unrefined(ret_ty)) + } + + fn type_param_as_callable_sig(&self, param_ty: mir_ty::ParamTy) -> Option { + let param_ty = self + .instantiate_generics(param_ty, self.generic_args) + .unwrap_or(param_ty); + let mut predicates = self + .tcx + .predicates_of(self.local_def_id) + .predicates + .iter() + .map(|(clause, _)| { + self.instantiate_generics(*clause, self.generic_args) + .unwrap_or(*clause) + }); + let params = predicates.clone().find_map(|clause| { + self.closure_trait_args(param_ty, clause.as_trait_clause()?.skip_binder()) + }); + let ret = predicates.find_map(|clause| { + self.closure_trait_ret(param_ty, clause.as_projection_clause()?.skip_binder()) + }); + + Some(rty::FunctionType::new(params?, ret?)) + } + /// Extracts the logical argument terms passed to `closure_precondition`/ /// `closure_postcondition`. The arguments are supplied as a single tuple (e.g. `(x,)` or /// `()`), whose elements are the logical arguments of the closure. diff --git a/src/refine/template.rs b/src/refine/template.rs index 369ff4c5..6297b415 100644 --- a/src/refine/template.rs +++ b/src/refine/template.rs @@ -81,6 +81,7 @@ pub struct TypeBuilder<'tcx> { /// See [`rty::TypeParamIdx`] for more details. param_idx_mapping: HashMap, type_params: Rc>, + closure_type_params: Rc>>, system: Rc>, } @@ -90,6 +91,7 @@ impl<'tcx> TypeBuilder<'tcx> { def_ids: DefIdCache<'tcx>, owner_fn_id: DefId, type_params: Rc>, + closure_type_params: Rc>>, system: Rc>, ) -> Self { let generics = tcx.generics_of(owner_fn_id); @@ -114,6 +116,7 @@ impl<'tcx> TypeBuilder<'tcx> { typing_env, param_idx_mapping, type_params, + closure_type_params, system, } } @@ -153,6 +156,13 @@ impl<'tcx> TypeBuilder<'tcx> { rty::AliasType::new(*index).into() } + pub fn register_closure_type_param(&self, type_param: TypeParam, fun_type: rty::FunctionType) { + tracing::info!(?type_param, ?fun_type, "register_closure_type_param"); + self.closure_type_params + .borrow_mut() + .insert(type_param, fun_type); + } + /// Replaces {closure} types with thrust_models::Closure<{closure}>. /// /// Ideally, we want to have `impl Model for F where F: Fn` instead of this and let From 1c53d16d3be83bec0daaa10902671832bf167786 Mon Sep 17 00:00:00 2001 From: coeff-aij <175928954+coeff-aij@users.noreply.github.com> Date: Thu, 11 Jun 2026 14:27:35 +0900 Subject: [PATCH 37/55] fix: wrong annotations in a test --- tests/ui/pass/traits/simple_loop_call.rs | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/tests/ui/pass/traits/simple_loop_call.rs b/tests/ui/pass/traits/simple_loop_call.rs index de2f0e82..39115fd8 100644 --- a/tests/ui/pass/traits/simple_loop_call.rs +++ b/tests/ui/pass/traits/simple_loop_call.rs @@ -25,11 +25,15 @@ fn target(a: &T, x: i64) -> i64 { v } +#[derive(PartialEq)] struct B(i64); +impl thrust_models::Model for B { + type Ty = B; +} + +#[thrust_macros::context] impl A for B { - #[thrust_macros::requires(Self::p(x))] - #[thrust_macros::ensures(Self::p(result))] fn f(&self, x: i64) -> i64{ x } From 1eb229bf7299d7dc056ddac423162b742cd82f4d Mon Sep 17 00:00:00 2001 From: coeff-aij <175928954+coeff-aij@users.noreply.github.com> Date: Thu, 11 Jun 2026 14:29:17 +0900 Subject: [PATCH 38/55] add: more tests for traits --- tests/ui/pass/traits/simple_loop_2int.rs | 28 +++++++++++++++++ tests/ui/pass/traits/two_loops.rs | 40 ++++++++++++++++++++++++ 2 files changed, 68 insertions(+) create mode 100644 tests/ui/pass/traits/simple_loop_2int.rs create mode 100644 tests/ui/pass/traits/two_loops.rs diff --git a/tests/ui/pass/traits/simple_loop_2int.rs b/tests/ui/pass/traits/simple_loop_2int.rs new file mode 100644 index 00000000..6edb3530 --- /dev/null +++ b/tests/ui/pass/traits/simple_loop_2int.rs @@ -0,0 +1,28 @@ +//@check-pass +//@compile-flags: -C debug-assertions=off +//@rustc-env: THRUST_SOLVER=tests/thrust-pcsat-wrapper THRUST_SOLVER_TIMEOUT_SECS=60 + +#[thrust_macros::context] +trait A { + #[thrust_macros::requires(Self::p(x, x))] + #[thrust_macros::ensures(Self::p(result, result))] + fn f(&self, x: i64) -> i64; + + #[thrust_macros::predicate] + fn p(x: i64, y: i64) -> bool; +} + +#[thrust_macros::requires(T::p(x, x))] +#[thrust_macros::ensures(T::p(result, result))] +fn target(a: &T, x: i64) -> i64 { + let mut v = x; + let mut i = 0; + while i < 3 { + v = a.f(v); + i += 1; + } + + v +} + +fn main() {} diff --git a/tests/ui/pass/traits/two_loops.rs b/tests/ui/pass/traits/two_loops.rs new file mode 100644 index 00000000..198354b1 --- /dev/null +++ b/tests/ui/pass/traits/two_loops.rs @@ -0,0 +1,40 @@ +//@check-pass +//@compile-flags: -C debug-assertions=off +//@rustc-env: THRUST_SOLVER=tests/thrust-pcsat-wrapper THRUST_SOLVER_TIMEOUT_SECS=60 + +#[thrust_macros::context] +trait A { + #[thrust_macros::requires(true)] + #[thrust_macros::ensures(Self::p(*result))] + fn f(&self) -> &Self; + #[thrust_macros::requires(Self::q(*self))] + #[thrust_macros::ensures(Self::q(*result))] + fn g(&self) -> &Self; + + #[thrust_macros::predicate] + fn p(self) -> bool; + #[thrust_macros::predicate] + fn q(self) -> bool; +} + +#[thrust_macros::requires(T::q(*y))] +#[thrust_macros::ensures(T::p(*result.0) && T::q(*result.1))] +fn target<'a, T: A>(x: &'a T, y: &'a T) -> (&'a T, &'a T) { + let mut v = x; + let mut w = y; + let mut i = 0; + while i < 3 { // The loop depends on P + v = v.f(); + i += 1; + } + + let mut j = 0; + while j < 3 { // The loop depends on Q + w = w.g(); + j += 1; + } + + (v, w) +} + +fn main() {} From 52ad0ae0feb92b2de814f2194e4b3f5d331ab41a Mon Sep 17 00:00:00 2001 From: coeff-aij <175928954+coeff-aij@users.noreply.github.com> Date: Thu, 11 Jun 2026 14:29:48 +0900 Subject: [PATCH 39/55] add: test for &mut T (not supported for now) --- tests/ui/pass/traits/simple_loop_self_mut.rs | 32 ++++++++++++++++++++ 1 file changed, 32 insertions(+) create mode 100644 tests/ui/pass/traits/simple_loop_self_mut.rs diff --git a/tests/ui/pass/traits/simple_loop_self_mut.rs b/tests/ui/pass/traits/simple_loop_self_mut.rs new file mode 100644 index 00000000..53a69e22 --- /dev/null +++ b/tests/ui/pass/traits/simple_loop_self_mut.rs @@ -0,0 +1,32 @@ +//@check-pass +//@compile-flags: -C debug-assertions=off +//@rustc-env: THRUST_SOLVER=tests/thrust-pcsat-wrapper THRUST_SOLVER_TIMEOUT_SECS=60 + +#[thrust_macros::context] +trait A { + #[thrust_macros::requires(Self::p(*self, !self, x))] + #[thrust_macros::ensures(Self::p(*self, !self, result))] + fn f(&mut self, x: i64) -> i64; + + #[thrust_macros::predicate] + fn p(self, after: Self, x: i64) -> bool; +} + +// impl thrust_models::Model for A { +// type Ty = A; +// } + +#[thrust_macros::requires(T::p(*a, !a, x))] +#[thrust_macros::ensures(T::p(*a, !a, result))] +fn target(a: &mut T, x: i64) -> i64 { + let mut v = x; + let mut i = 0; + while i < 3 { + v = a.f(v); + i += 1; + } + + v +} + +fn main() {} From eaddc786ae25a56fe952f9bca3e616517bdb2df9 Mon Sep 17 00:00:00 2001 From: coeff-aij <175928954+coeff-aij@users.noreply.github.com> Date: Thu, 11 Jun 2026 15:03:49 +0900 Subject: [PATCH 40/55] fix: error on mutable references with unknown type parameters `&mut T` (ad-hoc) --- src/refine/template.rs | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/src/refine/template.rs b/src/refine/template.rs index 6297b415..d9196384 100644 --- a/src/refine/template.rs +++ b/src/refine/template.rs @@ -282,6 +282,13 @@ impl<'tcx> TypeBuilder<'tcx> { let elem_ty = self.build(*elem_ty); rty::PointerType::immut_to(elem_ty).into() } + mir_ty::TyKind::Ref(_, elem_ty, mir_ty::Mutability::Mut) => { + let elem_ty = self.build(*elem_ty); + if !matches!(elem_ty, rty::Type::Param(_)) { + panic!("unsupported mutable reference type: {elem_ty:?}"); + } + rty::PointerType::mut_to(elem_ty).into() + } mir_ty::TyKind::Tuple(ts) => { // elaboration: all fields are boxed let elems = ts @@ -481,6 +488,13 @@ where let elem_ty = self.build(*elem_ty); rty::PointerType::immut_to(elem_ty).into() } + mir_ty::TyKind::Ref(_, elem_ty, mir_ty::Mutability::Mut) => { + let elem_ty = self.build(*elem_ty); + if !matches!(elem_ty, rty::Type::Param(_)) { + panic!("unsupported mutable reference type: {elem_ty:?}"); + } + rty::PointerType::mut_to(elem_ty).into() + } mir_ty::TyKind::Tuple(ts) => { // elaboration: all fields are boxed let elems = ts From 3fb04522ab45480867ee545630a508e1f304ac49 Mon Sep 17 00:00:00 2001 From: coeff-aij <175928954+coeff-aij@users.noreply.github.com> Date: Fri, 12 Jun 2026 18:04:40 +0900 Subject: [PATCH 41/55] fix: wrong DefId and argument types for type parameter with fn trait --- src/analyze/annot_fn.rs | 19 ++++++------------- 1 file changed, 6 insertions(+), 13 deletions(-) diff --git a/src/analyze/annot_fn.rs b/src/analyze/annot_fn.rs index e23161e5..464022d7 100644 --- a/src/analyze/annot_fn.rs +++ b/src/analyze/annot_fn.rs @@ -308,7 +308,7 @@ impl<'a, 'tcx> AnnotFnTranslator<'a, 'tcx> { ); if let Some(closure_fun_ty) = closure_fun_ty.clone() { self.type_builder.register_closure_type_param( - analyze::TypeParam::GenericType(self.local_def_id.to_def_id(), ty.index), + analyze::TypeParam::GenericType(self.type_builder.owner_fn_id, ty.index), closure_fun_ty, ); }; @@ -330,8 +330,10 @@ impl<'a, 'tcx> AnnotFnTranslator<'a, 'tcx> { if trait_ref.self_ty() != param_ty.to_ty(self.tcx) { return None; } + tracing::debug!(?trait_ref.args); let receiver_type = self.type_builder.build(trait_ref.args.type_at(0)); + use mir_ty::ClosureKind::*; let receiver_type = match self.tcx.fn_trait_kind_from_def_id(trait_ref.def_id)? { Fn => rty::PointerType::immut_to(receiver_type).into(), @@ -339,18 +341,9 @@ impl<'a, 'tcx> AnnotFnTranslator<'a, 'tcx> { FnOnce => receiver_type, }; - let mir_ty::Tuple(other_params) = trait_ref.args.type_at(1).kind() else { - return None; - }; - - let other_params = other_params.iter().map(|ty| { - let ty = self - .instantiate_generics(ty, self.generic_args) - .unwrap_or(ty); - self.type_builder.build(ty) - }); - let params = std::iter::once(receiver_type) - .chain(other_params) + let other_params = self.type_builder.build(trait_ref.args.type_at(1)); + let params = [receiver_type, other_params] + .into_iter() .map(|ty| rty::RefinedType::unrefined(ty.vacuous())) .collect(); tracing::debug!("found the signature for closure trait: {params:#?}"); From 11b2ffd9a134f3bb8fcb9ce79d5760d3be12b1c7 Mon Sep 17 00:00:00 2001 From: coeff-aij <175928954+coeff-aij@users.noreply.github.com> Date: Fri, 12 Jun 2026 18:06:45 +0900 Subject: [PATCH 42/55] add: resolve type parameter with fn trait as FunctionType --- src/analyze/basic_block.rs | 62 +++++++++++++------- src/analyze/basic_block/visitor/rust_call.rs | 2 +- 2 files changed, 43 insertions(+), 21 deletions(-) diff --git a/src/analyze/basic_block.rs b/src/analyze/basic_block.rs index d7447024..0a0835f9 100644 --- a/src/analyze/basic_block.rs +++ b/src/analyze/basic_block.rs @@ -9,7 +9,7 @@ use rustc_middle::mir::{ use rustc_middle::ty::{self as mir_ty, TyCtxt}; use rustc_span::def_id::{DefId, LocalDefId}; -use crate::analyze; +use crate::analyze::{self, TypeParam}; use crate::chc; use crate::pretty::PrettyDisplayExt as _; use crate::refine::{ @@ -131,6 +131,11 @@ impl PrecondCapture { } } +enum ResolvedCallable<'tcx> { + Closure(DefId, mir_ty::GenericArgsRef<'tcx>), + Generic(TypeParam), +} + pub struct Analyzer<'tcx, 'ctx> { ctx: &'ctx mut analyze::Analyzer<'tcx>, tcx: TyCtxt<'tcx>, @@ -603,7 +608,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { _ty, ) => { let func_ty = match operand.const_fn_def() { - Some((def_id, args)) => self.fn_def_ty(def_id, args), + Some((def_id, args)) => self.callable_ty(def_id, args), _ => unimplemented!(), }; PlaceType::with_ty_and_term(func_ty.vacuous(), chc::Term::null()) @@ -830,40 +835,47 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { }); } - fn resolve_fn_def( + fn resolve_callable( &self, def_id: DefId, args: mir_ty::GenericArgsRef<'tcx>, - ) -> (DefId, mir_ty::GenericArgsRef<'tcx>) { + ) -> ResolvedCallable<'tcx> { if self.ctx.is_fn_trait_method(def_id) { // When calling a closure via `Fn`/`FnMut`/`FnOnce` trait, // we simply replace the def_id with the closure's function def_id. // This skips shims, and makes self arguments mismatch. visitor::RustCallVisitor // adjusts the arguments accordingly. - let mir_ty::TyKind::Closure(closure_def_id, closure_args) = args.type_at(0).kind() - else { - panic!("expected closure arg for fn trait"); - }; - tracing::debug!(?closure_def_id, "closure instance"); - // closure_args contains [parent_generics..., upvars, return_ty, fn_sig_binder, ...]. - // Only the parent generics are meaningful to def_ty_with_args; the rest are internal - // closure encoding that type_builder.build() cannot handle. - let parent_count = self.tcx.generics_of(*closure_def_id).parent_count; - let parent_args = self.tcx.mk_args(&closure_args[..parent_count]); - (*closure_def_id, parent_args) + match args.type_at(0).kind() { + mir_ty::TyKind::Closure(closure_def_id, closure_args) => { + tracing::debug!(?closure_def_id, "closure instance"); + // closure_args contains [parent_generics..., upvars, return_ty, fn_sig_binder, ...]. + // Only the parent generics are meaningful to def_ty_with_args; the rest are internal + // closure encoding that type_builder.build() cannot handle. + let parent_count = self.tcx.generics_of(*closure_def_id).parent_count; + let parent_args = self.tcx.mk_args(&closure_args[..parent_count]); + ResolvedCallable::Closure(*closure_def_id, parent_args) + } + mir_ty::TyKind::Param(ty) => ResolvedCallable::Generic(TypeParam::GenericType( + self.type_builder.owner_fn_id, + ty.index, + )), + kind => { + panic!("expected closure arg for fn trait, got: {kind:?}"); + } + } } else { let typing_env = self.body.typing_env(self.tcx); let instance = mir_ty::Instance::try_resolve(self.tcx, typing_env, def_id, args).unwrap(); if let Some(instance) = instance { - (instance.def_id(), instance.args) + ResolvedCallable::Closure(instance.def_id(), instance.args) } else { - (def_id, args) + ResolvedCallable::Closure(def_id, args) } } } - fn fn_def_ty( + fn callable_ty( &mut self, def_id: DefId, args: mir_ty::GenericArgsRef<'tcx>, @@ -873,7 +885,17 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { return def_ty.ty; } - let (resolved_def_id, resolved_args) = self.resolve_fn_def(def_id, args); + let (resolved_def_id, resolved_args) = match self.resolve_callable(def_id, args) { + ResolvedCallable::Closure(def_id, args) => (def_id, args), + ResolvedCallable::Generic(type_param) => { + tracing::debug!(?type_param, ?self.ctx.closure_type_params); + return self + .ctx + .get_closure_type(type_param) + .expect("unknown closure type") + .into(); + } + }; if resolved_def_id == def_id { panic!( "unknown def (and not resolved): {:?}, args: {:?}", @@ -899,7 +921,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { { // TODO: handle const_fn_def on Env side let func_ty = if let Some((def_id, args)) = func.const_fn_def() { - self.fn_def_ty(def_id, args).vacuous() + self.callable_ty(def_id, args).vacuous() } else { self.operand_type(func.clone()).ty }; diff --git a/src/analyze/basic_block/visitor/rust_call.rs b/src/analyze/basic_block/visitor/rust_call.rs index 53100100..53191be7 100644 --- a/src/analyze/basic_block/visitor/rust_call.rs +++ b/src/analyze/basic_block/visitor/rust_call.rs @@ -59,7 +59,7 @@ impl<'a, 'tcx, 'ctx> mir::visit::MutVisitor<'tcx> for RustCallVisitor<'a, 'tcx, // RustCallVisitor expects all generic args to be already instantiated let mir_ty::TyKind::Closure(resolved_def_id, _) = generic_args.type_at(0).kind() else { - panic!("expected closure arg for fn trait"); + return; }; let fn_sig = self.analyzer.ctx().fn_sig(*resolved_def_id); if !matches!(fn_sig.abi, rustc_abi::ExternAbi::RustCall) { From d40d441ea0e4132def9d54ca04aac6fbd3ec79e1 Mon Sep 17 00:00:00 2001 From: coeff-aij <175928954+coeff-aij@users.noreply.github.com> Date: Sat, 13 Jun 2026 19:03:05 +0900 Subject: [PATCH 43/55] fix: double instantiation of argument types in precompute_callable_param_contracts() --- src/analyze/local_def.rs | 9 ++------- 1 file changed, 2 insertions(+), 7 deletions(-) diff --git a/src/analyze/local_def.rs b/src/analyze/local_def.rs index 314f88fd..a5d02123 100644 --- a/src/analyze/local_def.rs +++ b/src/analyze/local_def.rs @@ -397,15 +397,9 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { // `def_ty_with_args` directly. fn precompute_callable_param_contracts(&mut self, sig: &mir_ty::FnSig<'tcx>) { for input_ty in sig.inputs() { - use crate::rustc_middle::ty::TypeVisitableExt; - let inst = if input_ty.has_param() && self.generic_args.is_empty() { - *input_ty - } else { - mir_ty::EarlyBinder::bind(*input_ty).instantiate(self.tcx, self.generic_args) - }; let inst = self .tcx - .normalize_erasing_regions(mir_ty::TypingEnv::fully_monomorphized(), inst); + .normalize_erasing_regions(mir_ty::TypingEnv::fully_monomorphized(), *input_ty); let (fn_def_id, fn_args) = match inst.kind() { mir_ty::TyKind::Closure(def_id, args) => { (*def_id, self.tcx.mk_args(args.as_closure().parent_args())) @@ -1237,6 +1231,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { pub fn owner_fn_id(&mut self, owner_fn_id: DefId) -> &mut Self { self.owner_fn_id = owner_fn_id; + self.type_builder = self.ctx.type_builder(self.ctx.def_ids(), owner_fn_id); self } From 55d02cabda7e35fd48710a7363c6ea1533ff4906 Mon Sep 17 00:00:00 2001 From: coeff-aij <175928954+coeff-aij@users.noreply.github.com> Date: Sat, 13 Jun 2026 19:04:28 +0900 Subject: [PATCH 44/55] change: distinguish ForallPred with type parameters instead of argument types --- src/analyze/annot_fn.rs | 16 +++++----------- src/chc.rs | 9 ++++++--- src/chc/format_context.rs | 2 +- src/chc/smtlib2.rs | 6 +++++- src/chc/unbox.rs | 7 +++++-- 5 files changed, 22 insertions(+), 18 deletions(-) diff --git a/src/analyze/annot_fn.rs b/src/analyze/annot_fn.rs index 464022d7..1aeb1d9c 100644 --- a/src/analyze/annot_fn.rs +++ b/src/analyze/annot_fn.rs @@ -761,19 +761,13 @@ impl<'a, 'tcx> AnnotFnTranslator<'a, 'tcx> { def_id }; - let typeck_results = self.tcx.typeck(self.local_def_id); let pred = if is_unresolved_args { - let sig: Vec = args - .iter() - .map(|e| { - let ty = typeck_results.expr_ty(e); - let ty = self - .instantiate_generics(ty, generic_args) - .unwrap_or(ty); - self.type_builder.build(ty).to_sort() - }) + tracing::debug!(?self.local_def_id, ?generic_args, ?self.type_builder.owner_fn_id); + let type_params = generic_args + .types() + .map(|ty| self.type_builder.build(ty).to_sort()) .collect(); - let pred = refine::forall_pred(self.tcx, pred_def_id, sig); + let pred = refine::forall_pred(self.tcx, pred_def_id, type_params); self.analyzer .system .borrow_mut() diff --git a/src/chc.rs b/src/chc.rs index 53662747..9861319a 100644 --- a/src/chc.rs +++ b/src/chc.rs @@ -1050,7 +1050,7 @@ impl UserDefinedPred { #[derive(Debug, Clone, PartialEq, Eq, Hash)] pub struct ForallPred { inner: String, - args: Vec, + type_parameters: Vec, } impl std::fmt::Display for ForallPred { @@ -1066,7 +1066,7 @@ where { fn pretty(self, allocator: &'a D) -> pretty::DocBuilder<'a, D, termcolor::ColorSpec> { let args = allocator.intersperse( - self.args.iter().map(|a| a.pretty(allocator)), + self.type_parameters.iter().map(|a| a.pretty(allocator)), allocator.text(", "), ); allocator @@ -1083,7 +1083,10 @@ where impl ForallPred { pub fn new(inner: String, args: Vec) -> Self { - Self { inner, args } + Self { + inner, + type_parameters: args, + } } } diff --git a/src/chc/format_context.rs b/src/chc/format_context.rs index ad54df74..ce583c2b 100644 --- a/src/chc/format_context.rs +++ b/src/chc/format_context.rs @@ -349,7 +349,7 @@ impl FormatContext { } pub fn forall_pred(&self, p: &chc::ForallPred) -> impl std::fmt::Display { - let ss = SortSymbols::new(&p.args); + let ss = SortSymbols::new(&p.type_parameters); format!("{}{}", p.inner, ss) } diff --git a/src/chc/smtlib2.rs b/src/chc/smtlib2.rs index 929ff547..fdc2abe6 100644 --- a/src/chc/smtlib2.rs +++ b/src/chc/smtlib2.rs @@ -600,7 +600,11 @@ pub struct ForallPredDef<'ctx, 'a> { impl<'ctx, 'a> std::fmt::Display for ForallPredDef<'ctx, 'a> { fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { - let params = self.pred.args.iter().map(|sort| self.ctx.fmt_sort(sort)); + let params = self + .pred + .type_parameters + .iter() + .map(|sort| self.ctx.fmt_sort(sort)); let params = List::closed(params); write!( f, diff --git a/src/chc/unbox.rs b/src/chc/unbox.rs index 3b8bd6a8..8817e0a9 100644 --- a/src/chc/unbox.rs +++ b/src/chc/unbox.rs @@ -165,8 +165,11 @@ fn unbox_user_defined_pred_def(user_defined_pred_def: UserDefinedPredDef) -> Use } fn unbox_forall_pred_var_def(pred: ForallPred) -> ForallPred { - let args = pred.args.into_iter().map(unbox_sort).collect(); - ForallPred { args, ..pred } + let args = pred.type_parameters.into_iter().map(unbox_sort).collect(); + ForallPred { + type_parameters: args, + ..pred + } } /// Remove all `Box` sorts and `Box`/`BoxCurrent` terms from the system. From 482b186c73b522fd095cada70590c67bc0539907 Mon Sep 17 00:00:00 2001 From: coeff-aij <175928954+coeff-aij@users.noreply.github.com> Date: Sat, 13 Jun 2026 19:40:39 +0900 Subject: [PATCH 45/55] add: introduce ForallPreds corresponding to pre-/post-condition of type parameters with fn traits --- src/analyze/annot_fn.rs | 40 +++++++++++++++++++++++++++++++++++----- 1 file changed, 35 insertions(+), 5 deletions(-) diff --git a/src/analyze/annot_fn.rs b/src/analyze/annot_fn.rs index 1aeb1d9c..07966a40 100644 --- a/src/analyze/annot_fn.rs +++ b/src/analyze/annot_fn.rs @@ -368,6 +368,16 @@ impl<'a, 'tcx> AnnotFnTranslator<'a, 'tcx> { Some(rty::RefinedType::unrefined(ret_ty)) } + fn register_forall_pred(&self, type_params: Vec) -> chc::ForallPred { + let predicate = + refine::forall_pred(self.tcx, self.local_def_id.to_def_id(), type_params.clone()); + self.analyzer + .system + .borrow_mut() + .register_forall_pred(predicate.clone()); + predicate + } + fn type_param_as_callable_sig(&self, param_ty: mir_ty::ParamTy) -> Option { let param_ty = self .instantiate_generics(param_ty, self.generic_args) @@ -381,14 +391,34 @@ impl<'a, 'tcx> AnnotFnTranslator<'a, 'tcx> { self.instantiate_generics(*clause, self.generic_args) .unwrap_or(*clause) }); - let params = predicates.clone().find_map(|clause| { + + let mut params = predicates.clone().find_map(|clause| { self.closure_trait_args(param_ty, clause.as_trait_clause()?.skip_binder()) - }); - let ret = predicates.find_map(|clause| { + })?; + let mut ret = predicates.find_map(|clause| { self.closure_trait_ret(param_ty, clause.as_projection_clause()?.skip_binder()) - }); + })?; + + let receiver = rty::FunctionParamIdx::from_usize(0); + let arg = rty::FunctionParamIdx::from_usize(1); + + let free = |idx| chc::Term::var(rty::RefinedTypeVar::Free(idx)); + let value = chc::Term::var(rty::RefinedTypeVar::Value); + + let type_params = vec![self.type_builder.build(param_ty.to_ty(self.tcx)).to_sort()]; + + let pre_pred = self.register_forall_pred(type_params.clone()); + let post_pred = self.register_forall_pred(type_params); + + params[receiver].extend_refinement( + chc::Atom::new(pre_pred.into(), vec![value.clone(), free(arg)]).into(), + ); + + ret.extend_refinement( + chc::Atom::new(post_pred.into(), vec![free(receiver), free(arg), value]).into(), + ); - Some(rty::FunctionType::new(params?, ret?)) + Some(rty::FunctionType::new(params, ret)) } /// Extracts the logical argument terms passed to `closure_precondition`/ From acb05790fded47c5146f9447d80640bbe15d5985 Mon Sep 17 00:00:00 2001 From: coeff-aij <175928954+coeff-aij@users.noreply.github.com> Date: Sat, 13 Jun 2026 20:03:48 +0900 Subject: [PATCH 46/55] change: use forall sort instead of i32 type to represent unknown type parameters without trait bounds --- src/analyze/crate_.rs | 18 +++++++----------- 1 file changed, 7 insertions(+), 11 deletions(-) diff --git a/src/analyze/crate_.rs b/src/analyze/crate_.rs index 7918d89a..f2b19802 100644 --- a/src/analyze/crate_.rs +++ b/src/analyze/crate_.rs @@ -183,18 +183,14 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { let param = generics.param_at(idx, self.tcx); let arg = match param.kind { mir_ty::GenericParamDefKind::Type { .. } => { - if constrained_params.contains(¶m.index) { - let new_param = - mir_ty::Ty::new_param(self.tcx, param.index, param.name).into(); - tracing::debug!( - "replace the cosnstrained param {:#?} with the new param {:#?}.", - param, - new_param - ); + let new_param = + mir_ty::Ty::new_param(self.tcx, param.index, param.name).into(); + tracing::debug!( + "replace the cosnstrained param {:#?} with the new param {:#?}.", + param, new_param - } else { - self.tcx.types.i32.into() - } + ); + new_param } mir_ty::GenericParamDefKind::Const { .. } => { unimplemented!() From 8121a82245a0c866d20396686351e149842a1389 Mon Sep 17 00:00:00 2001 From: coeff-aij <175928954+coeff-aij@users.noreply.github.com> Date: Sat, 13 Jun 2026 20:23:39 +0900 Subject: [PATCH 47/55] revert: comment out for some extern_spec in std.rs --- std.rs | 218 ++++++++++++++++++++++++++++----------------------------- 1 file changed, 109 insertions(+), 109 deletions(-) diff --git a/std.rs b/std.rs index 56aa2d06..35d1a4c2 100644 --- a/std.rs +++ b/std.rs @@ -363,51 +363,51 @@ mod thrust_models { // std::mem::replace(dest, src) // } -// #[thrust::extern_spec_fn] -// #[thrust_macros::requires(true)] -// #[thrust_macros::ensures(result == (x == y))] -// fn _extern_spec_option_partialeq_eq(x: &Option, y: &Option) -> bool -// where T: thrust_models::Model + PartialEq, T::Ty: PartialEq -// { -// as PartialEq>::eq(x, y) -// } +#[thrust::extern_spec_fn] +#[thrust_macros::requires(true)] +#[thrust_macros::ensures(result == (x == y))] +fn _extern_spec_option_partialeq_eq(x: &Option, y: &Option) -> bool + where T: thrust_models::Model + PartialEq, T::Ty: PartialEq +{ + as PartialEq>::eq(x, y) +} -// #[thrust::extern_spec_fn] -// #[thrust_macros::requires(opt != None)] -// #[thrust_macros::ensures(Some(result) == opt)] -// fn _extern_spec_option_unwrap(opt: Option) -> T where T: thrust_models::Model, T::Ty: PartialEq { -// Option::unwrap(opt) -// } +#[thrust::extern_spec_fn] +#[thrust_macros::requires(opt != None)] +#[thrust_macros::ensures(Some(result) == opt)] +fn _extern_spec_option_unwrap(opt: Option) -> T where T: thrust_models::Model, T::Ty: PartialEq { + Option::unwrap(opt) +} -// #[thrust::extern_spec_fn] -// #[thrust_macros::requires(true)] -// #[thrust_macros::ensures( -// (*opt == None && result == true) -// || (*opt != None && result == false) -// )] -// fn _extern_spec_option_is_none(opt: &Option) -> bool where T: thrust_models::Model, T::Ty: PartialEq { -// Option::is_none(opt) -// } +#[thrust::extern_spec_fn] +#[thrust_macros::requires(true)] +#[thrust_macros::ensures( + (*opt == None && result == true) + || (*opt != None && result == false) +)] +fn _extern_spec_option_is_none(opt: &Option) -> bool where T: thrust_models::Model, T::Ty: PartialEq { + Option::is_none(opt) +} -// #[thrust::extern_spec_fn] -// #[thrust_macros::requires(true)] -// #[thrust_macros::ensures( -// (*opt == None && result == false) -// || (*opt != None && result == true) -// )] -// fn _extern_spec_option_is_some(opt: &Option) -> bool where T: thrust_models::Model, T::Ty: PartialEq { -// Option::is_some(opt) -// } +#[thrust::extern_spec_fn] +#[thrust_macros::requires(true)] +#[thrust_macros::ensures( + (*opt == None && result == false) + || (*opt != None && result == true) +)] +fn _extern_spec_option_is_some(opt: &Option) -> bool where T: thrust_models::Model, T::Ty: PartialEq { + Option::is_some(opt) +} -// #[thrust::extern_spec_fn] -// #[thrust_macros::requires(true)] -// #[thrust_macros::ensures( -// (opt != None && Some(result) == opt) -// || (opt == None && result == default) -// )] -// fn _extern_spec_option_unwrap_or(opt: Option, default: T) -> T where T: thrust_models::Model, T::Ty: PartialEq { -// Option::unwrap_or(opt, default) -// } +#[thrust::extern_spec_fn] +#[thrust_macros::requires(true)] +#[thrust_macros::ensures( + (opt != None && Some(result) == opt) + || (opt == None && result == default) +)] +fn _extern_spec_option_unwrap_or(opt: Option, default: T) -> T where T: thrust_models::Model, T::Ty: PartialEq { + Option::unwrap_or(opt, default) +} // #[thrust::extern_spec_fn] // #[thrust_macros::requires( @@ -500,15 +500,15 @@ mod thrust_models { // Option::as_mut(opt) // } -// #[thrust::extern_spec_fn] -// #[thrust_macros::requires(true)] -// #[thrust_macros::ensures(result == (x == y))] -// fn _extern_spec_result_partialeq_eq(x: &Result, y: &Result) -> bool -// where T: thrust_models::Model + PartialEq, T::Ty: PartialEq, -// E: thrust_models::Model + PartialEq, E::Ty: PartialEq, -// { -// as PartialEq>::eq(x, y) -// } +#[thrust::extern_spec_fn] +#[thrust_macros::requires(true)] +#[thrust_macros::ensures(result == (x == y))] +fn _extern_spec_result_partialeq_eq(x: &Result, y: &Result) -> bool + where T: thrust_models::Model + PartialEq, T::Ty: PartialEq, + E: thrust_models::Model + PartialEq, E::Ty: PartialEq, +{ + as PartialEq>::eq(x, y) +} // #[thrust::extern_spec_fn] // #[thrust_macros::requires(thrust_models::exists(|x| res == Ok(x)))] @@ -582,43 +582,43 @@ mod thrust_models { // Result::is_err(res) // } -// #[thrust::extern_spec_fn] -// #[thrust_macros::requires(true)] // TODO: require x != i32::MIN -// #[thrust_macros::ensures(result >= 0 && (result == x || result == -x))] -// fn _extern_spec_i32_abs(x: i32) -> i32 { -// i32::abs(x) -// } +#[thrust::extern_spec_fn] +#[thrust_macros::requires(true)] // TODO: require x != i32::MIN +#[thrust_macros::ensures(result >= 0 && (result == x || result == -x))] +fn _extern_spec_i32_abs(x: i32) -> i32 { + i32::abs(x) +} -// #[thrust::extern_spec_fn] -// #[thrust_macros::requires(true)] -// #[thrust_macros::ensures( -// (x >= y && result == (x - y)) -// || (x < y && result == (y - x)) -// )] -// fn _extern_spec_i32_abs_diff(x: i32, y: i32) -> u32 { -// i32::abs_diff(x, y) -// } +#[thrust::extern_spec_fn] +#[thrust_macros::requires(true)] +#[thrust_macros::ensures( + (x >= y && result == (x - y)) + || (x < y && result == (y - x)) +)] +fn _extern_spec_i32_abs_diff(x: i32, y: i32) -> u32 { + i32::abs_diff(x, y) +} -// #[thrust::extern_spec_fn] -// #[thrust_macros::requires(true)] -// #[thrust_macros::ensures((x == 0 && result == 0) || (x > 0 && result == 1) || (x < 0 && result == -1))] -// fn _extern_spec_i32_signum(x: i32) -> i32 { -// i32::signum(x) -// } +#[thrust::extern_spec_fn] +#[thrust_macros::requires(true)] +#[thrust_macros::ensures((x == 0 && result == 0) || (x > 0 && result == 1) || (x < 0 && result == -1))] +fn _extern_spec_i32_signum(x: i32) -> i32 { + i32::signum(x) +} -// #[thrust::extern_spec_fn] -// #[thrust_macros::requires(true)] -// #[thrust_macros::ensures((x < 0 && result == false) || (x >= 0 && result == true))] -// fn _extern_spec_i32_is_positive(x: i32) -> bool { -// i32::is_positive(x) -// } +#[thrust::extern_spec_fn] +#[thrust_macros::requires(true)] +#[thrust_macros::ensures((x < 0 && result == false) || (x >= 0 && result == true))] +fn _extern_spec_i32_is_positive(x: i32) -> bool { + i32::is_positive(x) +} -// #[thrust::extern_spec_fn] -// #[thrust_macros::requires(true)] -// #[thrust_macros::ensures((x <= 0 && result == true) || (x > 0 && result == false))] -// fn _extern_spec_i32_is_negative(x: i32) -> bool { -// i32::is_negative(x) -// } +#[thrust::extern_spec_fn] +#[thrust_macros::requires(true)] +#[thrust_macros::ensures((x <= 0 && result == true) || (x > 0 && result == false))] +fn _extern_spec_i32_is_negative(x: i32) -> bool { + i32::is_negative(x) +} // #[thrust::extern_spec_fn] // #[thrust_macros::requires(true)] @@ -711,32 +711,32 @@ mod thrust_models { // Vec::truncate(vec, len) // } -// // TODO: The following specs of some trait methods are too restrictive; we should allow for a -// // per-impl spec once we can describe the spec of blanket impls. +// TODO: The following specs of some trait methods are too restrictive; we should allow for a +// per-impl spec once we can describe the spec of blanket impls. -// #[thrust::extern_spec_fn] -// #[thrust_macros::requires(true)] -// #[thrust_macros::ensures(result == (*x == *y))] -// fn _extern_spec_partialeq_eq(x: &T, y: &T) -> bool -// where T: thrust_models::Model + PartialEq, T::Ty: PartialEq -// { -// PartialEq::eq(x, y) -// } +#[thrust::extern_spec_fn] +#[thrust_macros::requires(true)] +#[thrust_macros::ensures(result == (*x == *y))] +fn _extern_spec_partialeq_eq(x: &T, y: &T) -> bool + where T: thrust_models::Model + PartialEq, T::Ty: PartialEq +{ + PartialEq::eq(x, y) +} -// #[thrust::extern_spec_fn] -// #[thrust_macros::requires(true)] -// #[thrust_macros::ensures(result == (*x < *y))] -// fn _extern_spec_partialord_lt(x: &T, y: &T) -> bool -// where T: thrust_models::Model + PartialOrd, T::Ty: PartialOrd -// { -// PartialOrd::lt(x, y) -// } +#[thrust::extern_spec_fn] +#[thrust_macros::requires(true)] +#[thrust_macros::ensures(result == (*x < *y))] +fn _extern_spec_partialord_lt(x: &T, y: &T) -> bool + where T: thrust_models::Model + PartialOrd, T::Ty: PartialOrd +{ + PartialOrd::lt(x, y) +} -// #[thrust::extern_spec_fn] -// #[thrust_macros::requires(true)] -// #[thrust_macros::ensures(result == (*x > *y))] -// fn _extern_spec_partialord_gt(x: &T, y: &T) -> bool -// where T: thrust_models::Model + PartialOrd, T::Ty: PartialOrd -// { -// PartialOrd::gt(x, y) -// } +#[thrust::extern_spec_fn] +#[thrust_macros::requires(true)] +#[thrust_macros::ensures(result == (*x > *y))] +fn _extern_spec_partialord_gt(x: &T, y: &T) -> bool + where T: thrust_models::Model + PartialOrd, T::Ty: PartialOrd +{ + PartialOrd::gt(x, y) +} From f55687e553c992954055c8dceef554f69ebe1669 Mon Sep 17 00:00:00 2001 From: coeff-aij <175928954+coeff-aij@users.noreply.github.com> Date: Sun, 14 Jun 2026 03:03:19 +0900 Subject: [PATCH 48/55] add: distinguish args of projection(e.g. ::Item and ::Item) --- src/analyze.rs | 12 +++--- src/analyze/basic_block.rs | 2 +- src/refine/template.rs | 22 +++++++---- src/rty.rs | 76 ++++++++++++++++++++++++++++++++++---- src/rty/subtyping.rs | 2 + 5 files changed, 92 insertions(+), 22 deletions(-) diff --git a/src/analyze.rs b/src/analyze.rs index 74b870b4..94b43a60 100644 --- a/src/analyze.rs +++ b/src/analyze.rs @@ -207,12 +207,12 @@ impl refine::EnumDefProvider for Rc> { } pub type Env = refine::Env>>; -pub type TypeParamMap = HashMap; +pub type TypeParamMap<'tcx> = HashMap, ForallSortIdx>; #[derive(Eq, PartialEq, Hash, Debug, Clone)] -pub enum TypeParam { +pub enum TypeParam<'tcx> { GenericType(DefId, u32), - AssocType(DefId), + AssocType(DefId, mir_ty::GenericArgsRef<'tcx>), } #[derive(Debug, Clone)] @@ -242,8 +242,8 @@ pub struct Analyzer<'tcx> { enum_defs: Rc>, - type_params: Rc>, - closure_type_params: Rc>>, + type_params: Rc>>, + closure_type_params: Rc, rty::FunctionType>>>, } impl<'tcx> crate::refine::TemplateRegistry for Analyzer<'tcx> { @@ -437,7 +437,7 @@ impl<'tcx> Analyzer<'tcx> { ); } - pub fn get_closure_type(&self, type_param: TypeParam) -> Option { + pub fn get_closure_type(&self, type_param: TypeParam<'tcx>) -> Option { self.closure_type_params.borrow().get(&type_param).cloned() } diff --git a/src/analyze/basic_block.rs b/src/analyze/basic_block.rs index 0a0835f9..28b56fa4 100644 --- a/src/analyze/basic_block.rs +++ b/src/analyze/basic_block.rs @@ -133,7 +133,7 @@ impl PrecondCapture { enum ResolvedCallable<'tcx> { Closure(DefId, mir_ty::GenericArgsRef<'tcx>), - Generic(TypeParam), + Generic(TypeParam<'tcx>), } pub struct Analyzer<'tcx, 'ctx> { diff --git a/src/refine/template.rs b/src/refine/template.rs index d9196384..9deff0b4 100644 --- a/src/refine/template.rs +++ b/src/refine/template.rs @@ -80,8 +80,8 @@ pub struct TypeBuilder<'tcx> { /// mapped when we translate a [`mir_ty::ParamTy`] to [`rty::ParamType`]. /// See [`rty::TypeParamIdx`] for more details. param_idx_mapping: HashMap, - type_params: Rc>, - closure_type_params: Rc>>, + type_params: Rc>>, + closure_type_params: Rc, rty::FunctionType>>>, system: Rc>, } @@ -90,8 +90,8 @@ impl<'tcx> TypeBuilder<'tcx> { tcx: mir_ty::TyCtxt<'tcx>, def_ids: DefIdCache<'tcx>, owner_fn_id: DefId, - type_params: Rc>, - closure_type_params: Rc>>, + type_params: Rc>>, + closure_type_params: Rc, rty::FunctionType>>>, system: Rc>, ) -> Self { let generics = tcx.generics_of(owner_fn_id); @@ -143,20 +143,26 @@ impl<'tcx> TypeBuilder<'tcx> { rty::ParamType::new(param_local_idx, *forall_sort_idx).into() } - fn translate_alias_type(&self, ty: &mir_ty::AliasTy) -> rty::Type { + fn translate_alias_type(&self, ty: &mir_ty::AliasTy<'tcx>) -> rty::Type { let mut type_params = self.type_params.borrow_mut(); let index = type_params - .entry(TypeParam::AssocType(ty.def_id)) + .entry(TypeParam::AssocType(ty.def_id, ty.args)) .or_insert_with(|| { let idx = self.system.borrow_mut().new_forall_sort(); tracing::debug!("issue the new ForallSortIdx {} for AliasTy {:?}.", idx, ty,); idx }); - rty::AliasType::new(*index).into() + let args: Vec> = ty.args.types().map(|t| self.build(t)).collect(); + + rty::AliasType::new(*index, args).into() } - pub fn register_closure_type_param(&self, type_param: TypeParam, fun_type: rty::FunctionType) { + pub fn register_closure_type_param( + &self, + type_param: TypeParam<'tcx>, + fun_type: rty::FunctionType, + ) { tracing::info!(?type_param, ?fun_type, "register_closure_type_param"); self.closure_type_params .borrow_mut() diff --git a/src/rty.rs b/src/rty.rs index da781836..13e1e060 100644 --- a/src/rty.rs +++ b/src/rty.rs @@ -763,28 +763,56 @@ impl ParamType { } } +/// A projection type representing an unresolved associated type. +/// +/// This preserves the structural identity of projections like `::Item` +/// or ` as Iterator>::Item`, keeping them distinct even before normalization. +/// +/// The `args` field stores the generic arguments (Self type + other args), which can +/// recursively contain other types including params, ADTs, and other projections. +/// For example, ` as Iterator>::Item` would have `args = [Map]`. #[derive(Debug, Clone)] pub struct AliasType { forall_sort_idx: ForallSortIdx, + args: Vec>, } impl<'a, D> Pretty<'a, D, termcolor::ColorSpec> for &AliasType where D: pretty::DocAllocator<'a, termcolor::ColorSpec>, + D::Doc: Clone, { fn pretty(self, allocator: &'a D) -> pretty::DocBuilder<'a, D, termcolor::ColorSpec> { - self.forall_sort_idx.pretty(allocator) + let sort = self.forall_sort_idx.pretty(allocator); + if self.args.is_empty() { + sort + } else { + let args = allocator.intersperse( + self.args.iter().map(|ty| ty.pretty(allocator)), + allocator.text(",").append(allocator.line()), + ); + sort.append(allocator.line()) + .append(args.nest(2).angles()) + .group() + } } } impl AliasType { - pub fn new(forall_sort_idx: ForallSortIdx) -> Self { - AliasType { forall_sort_idx } + pub fn new(forall_sort_idx: ForallSortIdx, args: Vec>) -> Self { + AliasType { + forall_sort_idx, + args, + } } pub fn forall_sort_index(&self) -> ForallSortIdx { self.forall_sort_idx } + + pub fn args(&self) -> &[Type] { + &self.args + } } /// An array type. @@ -1163,10 +1191,13 @@ impl Type { pub fn free_ty_params(&self) -> HashSet { match self { - Type::Int | Type::Bool | Type::String | Type::Never | Type::Alias(_) => { - Default::default() - } + Type::Int | Type::Bool | Type::String | Type::Never => Default::default(), Type::Param(ty) => std::iter::once(ty.type_param_index()).collect(), + Type::Alias(ty) => ty + .args() + .iter() + .flat_map(|ty| ty.free_ty_params()) + .collect(), Type::Pointer(ty) => ty.free_ty_params(), Type::Function(ty) => ty.free_ty_params(), Type::Tuple(ty) => ty.free_ty_params(), @@ -1731,7 +1762,7 @@ impl RefinedType { { self.refinement.subst_ty_params_in_sorts(subst); match &mut self.ty { - Type::Int | Type::Bool | Type::String | Type::Never | Type::Alias(_) => {} + Type::Int | Type::Bool | Type::String | Type::Never => {} Type::Param(ty) => { if let Some(rty) = subst.get(ty.type_param_index()) { let RefinedType { @@ -1742,6 +1773,19 @@ impl RefinedType { self.ty = replacement_ty; } } + Type::Alias(alias) => { + let subst_closed = subst.clone().strip_refinement(); + let new_args: Vec> = alias + .args() + .iter() + .map(|arg| { + let mut arg_rty = RefinedType::unrefined(arg.clone()); + arg_rty.subst_ty_params(&subst_closed); + arg_rty.ty + }) + .collect(); + self.ty = Type::Alias(AliasType::new(alias.forall_sort_index(), new_args)); + } Type::Pointer(ty) => ty.subst_ty_params(subst), Type::Function(ty) => { let subst = subst.clone().strip_refinement(); @@ -1789,6 +1833,24 @@ impl RefinedType { (Type::Tuple(ty1), Type::Tuple(ty2)) => ty1.unify_ty_params(ty2), (Type::Array(ty1), Type::Array(ty2)) => ty1.unify_ty_params(ty2), (Type::Enum(ty1), Type::Enum(ty2)) => ty1.unify_ty_params(ty2), + (Type::Alias(a1), Type::Alias(a2)) + if a1.forall_sort_index() == a2.forall_sort_index() => + { + assert_eq!(a1.args().len(), a2.args().len()); + let args1: Vec> = a1 + .args() + .iter() + .cloned() + .map(|ty| RefinedType::unrefined(ty).vacuous()) + .collect(); + let args2: Vec> = a2 + .args() + .iter() + .cloned() + .map(|ty| RefinedType::unrefined(ty).vacuous()) + .collect(); + unify_tys_params(args1, args2) + } (t1, t2) => panic!("unify_ty_params: mismatched types t1={:?}, t2={:?}", t1, t2), } } diff --git a/src/rty/subtyping.rs b/src/rty/subtyping.rs index 72ec7df6..71196fde 100644 --- a/src/rty/subtyping.rs +++ b/src/rty/subtyping.rs @@ -125,6 +125,8 @@ where } (Type::Param(got), Type::Param(expected)) if got.forall_sort_idx == expected.forall_sort_idx => {} + (Type::Alias(got), Type::Alias(expected)) + if got.forall_sort_index() == expected.forall_sort_index() => {} _ => panic!( "inconsistent types: got={}, expected={}", got.display(), From c4cb3bcd3566e6b4aecdef70629034276aafed1b Mon Sep 17 00:00:00 2001 From: coeff-aij <175928954+coeff-aij@users.noreply.github.com> Date: Sun, 14 Jun 2026 04:35:29 +0900 Subject: [PATCH 49/55] add: opaque type handling for Box and Vec --- src/analyze/did_cache.rs | 4 ++++ src/refine/template.rs | 34 ++++++++++++++++++++++++++++++++++ 2 files changed, 38 insertions(+) diff --git a/src/analyze/did_cache.rs b/src/analyze/did_cache.rs index ee08a576..045b2ba1 100644 --- a/src/analyze/did_cache.rs +++ b/src/analyze/did_cache.rs @@ -53,6 +53,10 @@ impl<'tcx> DefIdCache<'tcx> { self.tcx.lang_items().owned_box() } + pub fn vec(&self) -> Option { + self.tcx.get_diagnostic_item(Symbol::intern("Vec")) + } + pub fn unique(&self) -> Option { *self.def_ids.unique.get_or_init(|| { let box_did = self.box_()?; diff --git a/src/refine/template.rs b/src/refine/template.rs index 9deff0b4..6ed54d3c 100644 --- a/src/refine/template.rs +++ b/src/refine/template.rs @@ -320,6 +320,23 @@ impl<'tcx> TypeBuilder<'tcx> { if let Some(model_ty) = self.model_adt(def, params) { return model_ty; } + // Treat Box and Vec as opaque types to avoid traversing internal structure + if Some(def.did()) == self.def_ids.box_() { + let elem_ty = self.build(params.type_at(0)); + return rty::PointerType::own(elem_ty).into(); + } + if Some(def.did()) == self.def_ids.vec() { + let elem_ty = self.build(params.type_at(0)); + // Vec is represented as a tuple of (Array, Int) in the model + let idx_ty = rty::Type::int(); + let array_ty = rty::ArrayType::new(idx_ty, elem_ty.clone()); + let len_ty = rty::Type::int(); + return rty::TupleType::new(vec![ + rty::PointerType::own(rty::Type::Array(array_ty)).into(), + rty::PointerType::own(len_ty).into(), + ]) + .into(); + } if def.is_enum() { let sym = refine::datatype_symbol(self.tcx, def.did()); let args: IndexVec<_, _> = params @@ -521,6 +538,23 @@ where if let Some(model_ty) = self.model_adt(def, params) { return model_ty; } + // Treat Box and Vec as opaque types to avoid traversing internal structure + if Some(def.did()) == self.inner.def_ids.box_() { + let elem_ty = self.build(params.type_at(0)); + return rty::PointerType::own(elem_ty).into(); + } + if Some(def.did()) == self.inner.def_ids.vec() { + let elem_ty = self.build(params.type_at(0)); + // Vec is represented as a tuple of (Array, Int) in the model + let idx_ty = rty::Type::int(); + let array_ty = rty::ArrayType::new(idx_ty, elem_ty.clone()); + let len_ty = rty::Type::int(); + return rty::TupleType::new(vec![ + rty::PointerType::own(rty::Type::Array(array_ty)).into(), + rty::PointerType::own(len_ty).into(), + ]) + .into(); + } if def.is_enum() { let sym = refine::datatype_symbol(self.inner.tcx, def.did()); let args: IndexVec<_, _> = From b6db7540e8aaa712d20ed38aae8cc6e6ddc22c8a Mon Sep 17 00:00:00 2001 From: coeff-aij <175928954+coeff-aij@users.noreply.github.com> Date: Sun, 14 Jun 2026 04:36:05 +0900 Subject: [PATCH 50/55] fix: use try_normalize_erasing_regions to avoid panic --- src/analyze/annot_fn.rs | 4 +++- src/analyze/local_def.rs | 3 ++- 2 files changed, 5 insertions(+), 2 deletions(-) diff --git a/src/analyze/annot_fn.rs b/src/analyze/annot_fn.rs index 07966a40..46a9aa23 100644 --- a/src/analyze/annot_fn.rs +++ b/src/analyze/annot_fn.rs @@ -256,7 +256,9 @@ impl<'a, 'tcx> AnnotFnTranslator<'a, 'tcx> { .instantiate_generics(ty, self.generic_args) .unwrap_or(ty); let typing_env = mir_ty::TypingEnv::fully_monomorphized(); - self.tcx.normalize_erasing_regions(typing_env, instantiated) + self.tcx + .try_normalize_erasing_regions(typing_env, instantiated) + .unwrap_or(instantiated) } pub fn to_formula_fn(&self) -> FormulaFn<'tcx> { diff --git a/src/analyze/local_def.rs b/src/analyze/local_def.rs index a5d02123..264240c8 100644 --- a/src/analyze/local_def.rs +++ b/src/analyze/local_def.rs @@ -399,7 +399,8 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { for input_ty in sig.inputs() { let inst = self .tcx - .normalize_erasing_regions(mir_ty::TypingEnv::fully_monomorphized(), *input_ty); + .try_normalize_erasing_regions(mir_ty::TypingEnv::fully_monomorphized(), *input_ty) + .unwrap_or(*input_ty); let (fn_def_id, fn_args) = match inst.kind() { mir_ty::TyKind::Closure(def_id, args) => { (*def_id, self.tcx.mk_args(args.as_closure().parent_args())) From b1ad064f626b107a9038b522fef1cf876c0c7c13 Mon Sep 17 00:00:00 2001 From: coeff-aij <175928954+coeff-aij@users.noreply.github.com> Date: Sun, 14 Jun 2026 04:34:25 +0900 Subject: [PATCH 51/55] fix: relax &mut restriction to allow any element type --- src/refine/template.rs | 6 ------ 1 file changed, 6 deletions(-) diff --git a/src/refine/template.rs b/src/refine/template.rs index 6ed54d3c..377bcb28 100644 --- a/src/refine/template.rs +++ b/src/refine/template.rs @@ -290,9 +290,6 @@ impl<'tcx> TypeBuilder<'tcx> { } mir_ty::TyKind::Ref(_, elem_ty, mir_ty::Mutability::Mut) => { let elem_ty = self.build(*elem_ty); - if !matches!(elem_ty, rty::Type::Param(_)) { - panic!("unsupported mutable reference type: {elem_ty:?}"); - } rty::PointerType::mut_to(elem_ty).into() } mir_ty::TyKind::Tuple(ts) => { @@ -513,9 +510,6 @@ where } mir_ty::TyKind::Ref(_, elem_ty, mir_ty::Mutability::Mut) => { let elem_ty = self.build(*elem_ty); - if !matches!(elem_ty, rty::Type::Param(_)) { - panic!("unsupported mutable reference type: {elem_ty:?}"); - } rty::PointerType::mut_to(elem_ty).into() } mir_ty::TyKind::Tuple(ts) => { From 2077ab732140961aad301b792b4e856f4edaf6ac Mon Sep 17 00:00:00 2001 From: coeff-aij <175928954+coeff-aij@users.noreply.github.com> Date: Sun, 14 Jun 2026 21:33:36 +0900 Subject: [PATCH 52/55] revert: commenting out most of extern_spec in std.rs --- src/analyze/crate_.rs | 3 +- std.rs | 490 +++++++++++++++++++++--------------------- 2 files changed, 246 insertions(+), 247 deletions(-) diff --git a/src/analyze/crate_.rs b/src/analyze/crate_.rs index f2b19802..2188b099 100644 --- a/src/analyze/crate_.rs +++ b/src/analyze/crate_.rs @@ -183,8 +183,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { let param = generics.param_at(idx, self.tcx); let arg = match param.kind { mir_ty::GenericParamDefKind::Type { .. } => { - let new_param = - mir_ty::Ty::new_param(self.tcx, param.index, param.name).into(); + let new_param = mir_ty::Ty::new_param(self.tcx, param.index, param.name).into(); tracing::debug!( "replace the cosnstrained param {:#?} with the new param {:#?}.", param, diff --git a/std.rs b/std.rs index 35d1a4c2..ef846777 100644 --- a/std.rs +++ b/std.rs @@ -333,35 +333,35 @@ mod thrust_models { } } -// #[thrust::extern_spec_fn] -// #[thrust_macros::requires(true)] -// #[thrust_macros::ensures(result == thrust_models::model::Box::new(x))] -// fn _extern_spec_box_new(x: T) -> Box where T: thrust_models::Model, T::Ty: PartialEq { -// Box::new(x) -// } +#[thrust::extern_spec_fn] +#[thrust_macros::requires(true)] +#[thrust_macros::ensures(result == thrust_models::model::Box::new(x))] +fn _extern_spec_box_new(x: T) -> Box where T: thrust_models::Model, T::Ty: PartialEq { + Box::new(x) +} -// #[thrust::extern_spec_fn] -// #[thrust_macros::requires(true)] -// #[thrust_macros::ensures(result == (x == y))] -// fn _extern_spec_box_partialeq_eq(x: &Box, y: &Box) -> bool -// where T: thrust_models::Model + PartialEq, T::Ty: PartialEq -// { -// as PartialEq>::eq(x, y) -// } +#[thrust::extern_spec_fn] +#[thrust_macros::requires(true)] +#[thrust_macros::ensures(result == (x == y))] +fn _extern_spec_box_partialeq_eq(x: &Box, y: &Box) -> bool + where T: thrust_models::Model + PartialEq, T::Ty: PartialEq +{ + as PartialEq>::eq(x, y) +} -// #[thrust::extern_spec_fn] -// #[thrust_macros::requires(true)] -// #[thrust_macros::ensures(*x == !y && *y == !x)] -// fn _extern_spec_std_mem_swap(x: &mut T, y: &mut T) where T: thrust_models::Model, T::Ty: PartialEq { -// std::mem::swap(x, y) -// } +#[thrust::extern_spec_fn] +#[thrust_macros::requires(true)] +#[thrust_macros::ensures(*x == !y && *y == !x)] +fn _extern_spec_std_mem_swap(x: &mut T, y: &mut T) where T: thrust_models::Model, T::Ty: PartialEq { + std::mem::swap(x, y) +} -// #[thrust::extern_spec_fn] -// #[thrust_macros::requires(true)] -// #[thrust_macros::ensures(!dest == src && result == *dest)] -// fn _extern_spec_std_mem_replace(dest: &mut T, src: T) -> T where T: thrust_models::Model, T::Ty: PartialEq { -// std::mem::replace(dest, src) -// } +#[thrust::extern_spec_fn] +#[thrust_macros::requires(true)] +#[thrust_macros::ensures(!dest == src && result == *dest)] +fn _extern_spec_std_mem_replace(dest: &mut T, src: T) -> T where T: thrust_models::Model, T::Ty: PartialEq { + std::mem::replace(dest, src) +} #[thrust::extern_spec_fn] #[thrust_macros::requires(true)] @@ -409,23 +409,23 @@ fn _extern_spec_option_unwrap_or(opt: Option, default: T) -> T where T: th Option::unwrap_or(opt, default) } -// #[thrust::extern_spec_fn] -// #[thrust_macros::requires( -// opt == None || thrust_models::exists(|i| opt == Some(i) && thrust_macros::pre!(f(i))) -// )] -// #[thrust_macros::ensures( -// (opt == None && result == None) -// || thrust_models::exists(|i| thrust_models::exists(|j| -// opt == Some(i) && thrust_macros::post!(f(i), j) && result == Some(j))) -// )] -// fn _extern_spec_option_map(opt: Option, f: F) -> Option -// where -// T: thrust_models::Model, T::Ty: PartialEq, -// U: thrust_models::Model, U::Ty: PartialEq, -// F: FnOnce(T) -> U, -// { -// Option::map(opt, f) -// } +#[thrust::extern_spec_fn] +#[thrust_macros::requires( + opt == None || thrust_models::exists(|i| opt == Some(i) && thrust_macros::pre!(f(i))) +)] +#[thrust_macros::ensures( + (opt == None && result == None) + || thrust_models::exists(|i| thrust_models::exists(|j| + opt == Some(i) && thrust_macros::post!(f(i), j) && result == Some(j))) +)] +fn _extern_spec_option_map(opt: Option, f: F) -> Option +where + T: thrust_models::Model, T::Ty: PartialEq, + U: thrust_models::Model, U::Ty: PartialEq, + F: FnOnce(T) -> U, +{ + Option::map(opt, f) +} // #[thrust::extern_spec_fn] // #[thrust_macros::requires(opt != None || thrust_macros::pre!(f()))] @@ -441,64 +441,64 @@ fn _extern_spec_option_unwrap_or(opt: Option, default: T) -> T where T: th // Option::unwrap_or_else(opt, f) // } -// #[thrust::extern_spec_fn] -// #[thrust_macros::requires(true)] -// #[thrust_macros::ensures( -// (thrust_models::exists(|x| opt == Some(x) && result == Ok(x))) -// || (opt == None && result == Err(err)) -// )] -// fn _extern_spec_option_ok_or(opt: Option, err: E) -> Result -// where T: thrust_models::Model, T::Ty: PartialEq, -// E: thrust_models::Model, E::Ty: PartialEq, -// { -// Option::ok_or(opt, err) -// } +#[thrust::extern_spec_fn] +#[thrust_macros::requires(true)] +#[thrust_macros::ensures( + (thrust_models::exists(|x| opt == Some(x) && result == Ok(x))) + || (opt == None && result == Err(err)) +)] +fn _extern_spec_option_ok_or(opt: Option, err: E) -> Result + where T: thrust_models::Model, T::Ty: PartialEq, + E: thrust_models::Model, E::Ty: PartialEq, +{ + Option::ok_or(opt, err) +} -// #[thrust::extern_spec_fn] -// #[thrust_macros::requires(true)] -// #[thrust_macros::ensures(!opt == None && result == *opt)] -// fn _extern_spec_option_take(opt: &mut Option) -> Option where T: thrust_models::Model, T::Ty: PartialEq { -// Option::take(opt) -// } +#[thrust::extern_spec_fn] +#[thrust_macros::requires(true)] +#[thrust_macros::ensures(!opt == None && result == *opt)] +fn _extern_spec_option_take(opt: &mut Option) -> Option where T: thrust_models::Model, T::Ty: PartialEq { + Option::take(opt) +} -// #[thrust::extern_spec_fn] -// #[thrust_macros::requires(true)] -// #[thrust_macros::ensures(!opt == Some(src) && result == *opt)] -// fn _extern_spec_option_replace(opt: &mut Option, src: T) -> Option -// where T: thrust_models::Model, T::Ty: PartialEq -// { -// Option::replace(opt, src) -// } +#[thrust::extern_spec_fn] +#[thrust_macros::requires(true)] +#[thrust_macros::ensures(!opt == Some(src) && result == *opt)] +fn _extern_spec_option_replace(opt: &mut Option, src: T) -> Option + where T: thrust_models::Model, T::Ty: PartialEq +{ + Option::replace(opt, src) +} -// #[thrust::extern_spec_fn] -// #[thrust_macros::requires(true)] -// #[thrust_macros::ensures( -// thrust_models::exists(|x| opt == &Some(x) && result == Some(&x)) -// || (opt == &None && result == None) -// )] -// fn _extern_spec_option_as_ref(opt: &Option) -> Option<&T> where T: thrust_models::Model, T::Ty: PartialEq { -// Option::as_ref(opt) -// } +#[thrust::extern_spec_fn] +#[thrust_macros::requires(true)] +#[thrust_macros::ensures( + thrust_models::exists(|x| opt == &Some(x) && result == Some(&x)) + || (opt == &None && result == None) +)] +fn _extern_spec_option_as_ref(opt: &Option) -> Option<&T> where T: thrust_models::Model, T::Ty: PartialEq { + Option::as_ref(opt) +} -// #[thrust::extern_spec_fn] -// #[thrust_macros::requires(true)] -// #[thrust_macros::ensures( -// thrust_models::exists(|x1, x2| -// *opt == Some(x1) && -// !opt == Some(x2) && -// result == Some(thrust_models::model::Mut::new(x1, x2)) -// ) -// || ( -// *opt == None && -// !opt == None && -// result == None -// ) -// )] -// fn _extern_spec_option_as_mut(opt: &mut Option) -> Option<&mut T> -// where T: thrust_models::Model, T::Ty: PartialEq -// { -// Option::as_mut(opt) -// } +#[thrust::extern_spec_fn] +#[thrust_macros::requires(true)] +#[thrust_macros::ensures( + thrust_models::exists(|x1, x2| + *opt == Some(x1) && + !opt == Some(x2) && + result == Some(thrust_models::model::Mut::new(x1, x2)) + ) + || ( + *opt == None && + !opt == None && + result == None + ) +)] +fn _extern_spec_option_as_mut(opt: &mut Option) -> Option<&mut T> + where T: thrust_models::Model, T::Ty: PartialEq +{ + Option::as_mut(opt) +} #[thrust::extern_spec_fn] #[thrust_macros::requires(true)] @@ -510,77 +510,77 @@ fn _extern_spec_result_partialeq_eq(x: &Result, y: &Result) -> as PartialEq>::eq(x, y) } -// #[thrust::extern_spec_fn] -// #[thrust_macros::requires(thrust_models::exists(|x| res == Ok(x)))] -// #[thrust_macros::ensures(Ok(result) == res)] -// fn _extern_spec_result_unwrap(res: Result) -> T -// where T: thrust_models::Model, T::Ty: PartialEq, -// E: thrust_models::Model, E::Ty: PartialEq, -// { -// Result::unwrap(res) -// } +#[thrust::extern_spec_fn] +#[thrust_macros::requires(thrust_models::exists(|x| res == Ok(x)))] +#[thrust_macros::ensures(Ok(result) == res)] +fn _extern_spec_result_unwrap(res: Result) -> T + where T: thrust_models::Model, T::Ty: PartialEq, + E: thrust_models::Model, E::Ty: PartialEq, +{ + Result::unwrap(res) +} -// #[thrust::extern_spec_fn] -// #[thrust_macros::requires(thrust_models::exists(|x| res == Err(x)))] -// #[thrust_macros::ensures(Err(result) == res)] -// fn _extern_spec_result_unwrap_err(res: Result) -> E -// where T: thrust_models::Model, T::Ty: PartialEq, -// E: thrust_models::Model, E::Ty: PartialEq, -// { -// Result::unwrap_err(res) -// } +#[thrust::extern_spec_fn] +#[thrust_macros::requires(thrust_models::exists(|x| res == Err(x)))] +#[thrust_macros::ensures(Err(result) == res)] +fn _extern_spec_result_unwrap_err(res: Result) -> E + where T: thrust_models::Model, T::Ty: PartialEq, + E: thrust_models::Model, E::Ty: PartialEq, +{ + Result::unwrap_err(res) +} -// #[thrust::extern_spec_fn] -// #[thrust_macros::requires(true)] -// #[thrust_macros::ensures( -// thrust_models::exists(|x| res == Ok(x) && result == Some(x)) -// || thrust_models::exists(|x| res == Err(x) && result == None) -// )] -// fn _extern_spec_result_ok(res: Result) -> Option -// where T: thrust_models::Model, T::Ty: PartialEq, -// E: thrust_models::Model, E::Ty: PartialEq, -// { -// Result::ok(res) -// } +#[thrust::extern_spec_fn] +#[thrust_macros::requires(true)] +#[thrust_macros::ensures( + thrust_models::exists(|x| res == Ok(x) && result == Some(x)) + || thrust_models::exists(|x| res == Err(x) && result == None) +)] +fn _extern_spec_result_ok(res: Result) -> Option + where T: thrust_models::Model, T::Ty: PartialEq, + E: thrust_models::Model, E::Ty: PartialEq, +{ + Result::ok(res) +} -// #[thrust::extern_spec_fn] -// #[thrust_macros::requires(true)] -// #[thrust_macros::ensures( -// thrust_models::exists(|x| res == Ok(x) && result == None) -// || thrust_models::exists(|x| res == Err(x) && result == Some(x)) -// )] -// fn _extern_spec_result_err(res: Result) -> Option -// where T: thrust_models::Model, T::Ty: PartialEq, -// E: thrust_models::Model, E::Ty: PartialEq, -// { -// Result::err(res) -// } +#[thrust::extern_spec_fn] +#[thrust_macros::requires(true)] +#[thrust_macros::ensures( + thrust_models::exists(|x| res == Ok(x) && result == None) + || thrust_models::exists(|x| res == Err(x) && result == Some(x)) +)] +fn _extern_spec_result_err(res: Result) -> Option + where T: thrust_models::Model, T::Ty: PartialEq, + E: thrust_models::Model, E::Ty: PartialEq, +{ + Result::err(res) +} -// #[thrust::extern_spec_fn] -// #[thrust_macros::requires(true)] -// #[thrust_macros::ensures( -// thrust_models::exists(|x| *res == Ok(x) && result == true) -// || thrust_models::exists(|x| *res == Err(x) && result == false) -// )] -// fn _extern_spec_result_is_ok(res: &Result) -> bool -// where T: thrust_models::Model, T::Ty: PartialEq, -// E: thrust_models::Model, E::Ty: PartialEq, -// { -// Result::is_ok(res) -// } +#[thrust::extern_spec_fn] +#[thrust_macros::requires(true)] +#[thrust_macros::ensures( + thrust_models::exists(|x| *res == Ok(x) && result == true) + || thrust_models::exists(|x| *res == Err(x) && result == false) +)] +fn _extern_spec_result_is_ok(res: &Result) -> bool + where T: thrust_models::Model, T::Ty: PartialEq, + E: thrust_models::Model, E::Ty: PartialEq, +{ + Result::is_ok(res) +} -// #[thrust::extern_spec_fn] -// #[thrust_macros::requires(true)] -// #[thrust_macros::ensures( -// thrust_models::exists(|x| *res == Ok(x) && result == false) -// || thrust_models::exists(|x| *res == Err(x) && result == true) -// )] -// fn _extern_spec_result_is_err(res: &Result) -> bool -// where T: thrust_models::Model, T::Ty: PartialEq, -// E: thrust_models::Model, E::Ty: PartialEq, -// { -// Result::is_err(res) -// } +#[thrust::extern_spec_fn] +#[thrust_macros::requires(true)] +#[thrust_macros::ensures( + thrust_models::exists(|x| *res == Ok(x) && result == false) + || thrust_models::exists(|x| *res == Err(x) && result == true) +)] +fn _extern_spec_result_is_err(res: &Result) -> bool + where T: thrust_models::Model, T::Ty: PartialEq, + E: thrust_models::Model, E::Ty: PartialEq, +{ + Result::is_err(res) +} #[thrust::extern_spec_fn] #[thrust_macros::requires(true)] // TODO: require x != i32::MIN @@ -620,96 +620,96 @@ fn _extern_spec_i32_is_negative(x: i32) -> bool { i32::is_negative(x) } -// #[thrust::extern_spec_fn] -// #[thrust_macros::requires(true)] -// #[thrust_macros::ensures(result.1 == 0)] -// fn _extern_spec_vec_new() -> Vec where T: thrust_models::Model, T::Ty: PartialEq { -// Vec::::new() -// } +#[thrust::extern_spec_fn] +#[thrust_macros::requires(true)] +#[thrust_macros::ensures(result.1 == 0)] +fn _extern_spec_vec_new() -> Vec where T: thrust_models::Model, T::Ty: PartialEq { + Vec::::new() +} -// #[thrust::extern_spec_fn] -// #[thrust_macros::requires(true)] -// #[thrust_macros::ensures(!vec == thrust_models::model::Vec((*vec).0.store((*vec).1, elem), (*vec).1 + 1))] -// fn _extern_spec_vec_push(vec: &mut Vec, elem: T) -// where T: thrust_models::Model, T::Ty: PartialEq -// { -// Vec::push(vec, elem) -// } +#[thrust::extern_spec_fn] +#[thrust_macros::requires(true)] +#[thrust_macros::ensures(!vec == thrust_models::model::Vec((*vec).0.store((*vec).1, elem), (*vec).1 + 1))] +fn _extern_spec_vec_push(vec: &mut Vec, elem: T) + where T: thrust_models::Model, T::Ty: PartialEq +{ + Vec::push(vec, elem) +} -// #[thrust::extern_spec_fn] -// #[thrust_macros::requires(true)] -// #[thrust_macros::ensures(result == vec.1)] -// fn _extern_spec_vec_len(vec: &Vec) -> usize where T: thrust_models::Model, T::Ty: PartialEq { -// Vec::len(vec) -// } +#[thrust::extern_spec_fn] +#[thrust_macros::requires(true)] +#[thrust_macros::ensures(result == vec.1)] +fn _extern_spec_vec_len(vec: &Vec) -> usize where T: thrust_models::Model, T::Ty: PartialEq { + Vec::len(vec) +} -// #[thrust::extern_spec_fn] -// #[thrust_macros::requires(index < vec.1)] -// #[thrust_macros::ensures(*result == vec.0[index])] -// fn _extern_spec_vec_index(vec: &Vec, index: usize) -> &T where T: thrust_models::Model, T::Ty: PartialEq { -// as std::ops::Index>::index(vec, index) -// } +#[thrust::extern_spec_fn] +#[thrust_macros::requires(index < vec.1)] +#[thrust_macros::ensures(*result == vec.0[index])] +fn _extern_spec_vec_index(vec: &Vec, index: usize) -> &T where T: thrust_models::Model, T::Ty: PartialEq { + as std::ops::Index>::index(vec, index) +} -// #[thrust::extern_spec_fn] -// #[thrust_macros::requires(index < (*vec).1)] -// #[thrust_macros::ensures( -// *result == (*vec).0[index] && -// !result == (!vec).0[index] && -// !vec == thrust_models::model::Vec((*vec).0.store(index, !result), (*vec).1) -// )] -// fn _extern_spec_vec_index_mut(vec: &mut Vec, index: usize) -> &mut T -// where T: thrust_models::Model, T::Ty: PartialEq -// { -// as std::ops::IndexMut>::index_mut(vec, index) -// } +#[thrust::extern_spec_fn] +#[thrust_macros::requires(index < (*vec).1)] +#[thrust_macros::ensures( + *result == (*vec).0[index] && + !result == (!vec).0[index] && + !vec == thrust_models::model::Vec((*vec).0.store(index, !result), (*vec).1) +)] +fn _extern_spec_vec_index_mut(vec: &mut Vec, index: usize) -> &mut T + where T: thrust_models::Model, T::Ty: PartialEq +{ + as std::ops::IndexMut>::index_mut(vec, index) +} -// #[thrust::extern_spec_fn] -// #[thrust_macros::requires(true)] -// #[thrust_macros::ensures((!vec).1 == 0)] -// fn _extern_spec_vec_clear(vec: &mut Vec) where T: thrust_models::Model, T::Ty: PartialEq { -// Vec::clear(vec) -// } +#[thrust::extern_spec_fn] +#[thrust_macros::requires(true)] +#[thrust_macros::ensures((!vec).1 == 0)] +fn _extern_spec_vec_clear(vec: &mut Vec) where T: thrust_models::Model, T::Ty: PartialEq { + Vec::clear(vec) +} -// #[thrust::extern_spec_fn] -// #[thrust_macros::requires(true)] -// #[thrust_macros::ensures( -// (!vec).0 == (*vec).0 && ( -// ( -// (*vec).1 > 0 && -// (!vec).1 == (*vec).1 - 1 && -// result == Some((*vec).0[(*vec).1 - 1]) -// ) || ( -// (*vec).1 == 0 && -// (!vec).1 == 0 && -// result == None -// ) -// ) -// )] -// fn _extern_spec_vec_pop(vec: &mut Vec) -> Option where T: thrust_models::Model, T::Ty: PartialEq { -// Vec::pop(vec) -// } +#[thrust::extern_spec_fn] +#[thrust_macros::requires(true)] +#[thrust_macros::ensures( + (!vec).0 == (*vec).0 && ( + ( + (*vec).1 > 0 && + (!vec).1 == (*vec).1 - 1 && + result == Some((*vec).0[(*vec).1 - 1]) + ) || ( + (*vec).1 == 0 && + (!vec).1 == 0 && + result == None + ) + ) +)] +fn _extern_spec_vec_pop(vec: &mut Vec) -> Option where T: thrust_models::Model, T::Ty: PartialEq { + Vec::pop(vec) +} -// #[thrust::extern_spec_fn] -// #[thrust_macros::requires(true)] -// #[thrust_macros::ensures(result == ((*vec).1 == 0))] -// fn _extern_spec_vec_is_empty(vec: &Vec) -> bool where T: thrust_models::Model, T::Ty: PartialEq { -// Vec::is_empty(vec) -// } +#[thrust::extern_spec_fn] +#[thrust_macros::requires(true)] +#[thrust_macros::ensures(result == ((*vec).1 == 0))] +fn _extern_spec_vec_is_empty(vec: &Vec) -> bool where T: thrust_models::Model, T::Ty: PartialEq { + Vec::is_empty(vec) +} -// #[thrust::extern_spec_fn] -// #[thrust_macros::requires(true)] -// #[thrust_macros::ensures( -// ( -// (*vec).1 > len && -// !vec == thrust_models::model::Vec((*vec).0, len) -// ) || ( -// (*vec).1 <= len && -// !vec == *vec -// ) -// )] -// fn _extern_spec_vec_truncate(vec: &mut Vec, len: usize) where T: thrust_models::Model, T::Ty: PartialEq { -// Vec::truncate(vec, len) -// } +#[thrust::extern_spec_fn] +#[thrust_macros::requires(true)] +#[thrust_macros::ensures( + ( + (*vec).1 > len && + !vec == thrust_models::model::Vec((*vec).0, len) + ) || ( + (*vec).1 <= len && + !vec == *vec + ) +)] +fn _extern_spec_vec_truncate(vec: &mut Vec, len: usize) where T: thrust_models::Model, T::Ty: PartialEq { + Vec::truncate(vec, len) +} // TODO: The following specs of some trait methods are too restrictive; we should allow for a // per-impl spec once we can describe the spec of blanket impls. From 92764b7d093df34da3a1120f80ff733a5c8f8d97 Mon Sep 17 00:00:00 2001 From: coeff-aij <175928954+coeff-aij@users.noreply.github.com> Date: Sun, 14 Jun 2026 21:41:30 +0900 Subject: [PATCH 53/55] add: annotations for fold() (WIP) --- tests/ui/pass/traits/fold.rs | 116 +++++++++++++++++++++++++++++++++++ 1 file changed, 116 insertions(+) create mode 100644 tests/ui/pass/traits/fold.rs diff --git a/tests/ui/pass/traits/fold.rs b/tests/ui/pass/traits/fold.rs new file mode 100644 index 00000000..a30491a7 --- /dev/null +++ b/tests/ui/pass/traits/fold.rs @@ -0,0 +1,116 @@ +//@check-pass +//@compile-flags: -C debug-assertions=off +//@rustc-env: THRUST_SOLVER=tests/thrust-pcsat-wrapper THRUST_SOLVER_TIMEOUT_SECS=60 + +#[thrust_macros::context] +trait Iterator { + type Item; + + #[thrust_macros::ensures( + Self::completed(*self) + || thrust_models::exists(|i| (result == Some(i)) && Self::step(*self, i, !self)) + )] + #[thrust_macros::ensures(!Self::completed(*self) || (result == None && *self == !self))] + fn next(&mut self) -> Option; + + #[thrust_macros::predicate] + fn completed(self) -> bool; + #[thrust_macros::predicate] + fn step(self, item: Self::Item, dist: Self) -> bool; + + #[thrust_macros::requires(true)] + #[thrust_macros::ensures( + // ∃ it: Vec. (it.0 : Array, it.1 : Int) + thrust_models::exists(|it: thrust_models::model::Vec| + // ∃ acc: Vec. (acc.0 : Array, acc.1 : Int) + thrust_models::exists(|acc| + it.0[0] == *self && + acc.0[0] == init && + Self::completed(it.0[it.1 - 1]) && + result == acc.0[it.1 - 1] && + // ∀ i. (0 ≤ i ∧ i < it.1 - 1) ⟹ + // ∃ item. Self::step(it[i], item, it[i+1]) + // ∧ post!(f(acc[i], item), acc[i+1]) + // !(∃ i. (0 ≤ i ∧ i < it.1 - 1) ∧ !(∃ item. step ∧ post)) + !( + thrust_models::exists(|i| + (0 <= i && i < it.1 - 1) && + !( + thrust_models::exists(|item| + Self::step(it.0[i], item, it.0[i + 1]) && + thrust_macros::post!( + f(acc.0[i], item), + acc.0[i + 1] + ) + ) + ) + ) + ) + )) + )] + fn fold(mut self, init: B, mut f: F) -> B + where + Self: Sized, + F: FnMut(B, Self::Item) -> B, + { + let mut accum = init; + while let Some(x) = self.next() { + accum = f(accum, x); + } + accum + } +} + +struct Range { + start: i64, + end: i64, +} + +impl thrust_models::Model for Range { + type Ty = Range; +} + +#[thrust_macros::context] +impl Iterator for Range { + type Item = i64; + + fn next(&mut self) -> Option { + if self.start < self.end { + let item = self.start; + self.start += 1; + Some(item) + } else { + None + } + } + + #[thrust_macros::predicate] + fn completed(self) -> bool { + // (tuple_proj.0 self) is equivalent to self.start + // !(self.start < self.end) is written as following: + "(not (< + (tuple_proj.0 self_) + (tuple_proj.1 self_) + ))"; + true + } + + #[thrust_macros::predicate] + fn step(self, item: Self::Item, dist: Self) -> bool { + // self.end == dist.end && self.start == item && self.start + 1 == dist.start + // is written as following: + "(and + (= (tuple_proj.1 self_) (tuple_proj.1 dist)) + (= (tuple_proj.0 self_) item) + (= (+ (tuple_proj.0 self_) 1) (tuple_proj.0 dist)) + )"; + true + } +} + +fn main() { + let mut range = Range { start: 0, end: 5 }; + let sum = range.fold(0, |x, y| x + y); + + assert!(sum == 10); +} \ No newline at end of file From 312f3623a223af4c91a7baeda8733085d52eec33 Mon Sep 17 00:00:00 2001 From: coeff-aij <175928954+coeff-aij@users.noreply.github.com> Date: Sun, 14 Jun 2026 23:03:47 +0900 Subject: [PATCH 54/55] fix annotations on fold() (WIP) --- tests/ui/pass/traits/fold.rs | 61 ++++++++++++++++++++++++++---------- 1 file changed, 45 insertions(+), 16 deletions(-) diff --git a/tests/ui/pass/traits/fold.rs b/tests/ui/pass/traits/fold.rs index a30491a7..2265ec43 100644 --- a/tests/ui/pass/traits/fold.rs +++ b/tests/ui/pass/traits/fold.rs @@ -2,13 +2,15 @@ //@compile-flags: -C debug-assertions=off //@rustc-env: THRUST_SOLVER=tests/thrust-pcsat-wrapper THRUST_SOLVER_TIMEOUT_SECS=60 +use thrust_models::exists; + #[thrust_macros::context] trait Iterator { type Item; #[thrust_macros::ensures( Self::completed(*self) - || thrust_models::exists(|i| (result == Some(i)) && Self::step(*self, i, !self)) + || exists(|i| (result == Some(i)) && Self::step(*self, i, !self)) )] #[thrust_macros::ensures(!Self::completed(*self) || (result == None && *self == !self))] fn next(&mut self) -> Option; @@ -18,26 +20,25 @@ trait Iterator { #[thrust_macros::predicate] fn step(self, item: Self::Item, dist: Self) -> bool; + #[thrust_macros::invariant_context] #[thrust_macros::requires(true)] #[thrust_macros::ensures( - // ∃ it: Vec. (it.0 : Array, it.1 : Int) - thrust_models::exists(|it: thrust_models::model::Vec| - // ∃ acc: Vec. (acc.0 : Array, acc.1 : Int) - thrust_models::exists(|acc| - it.0[0] == *self && + exists(|it: thrust_models::model::Vec| + exists(|fn_: thrust_models::model::Vec| + exists(|acc| + exists(|l: thrust_models::model::Int| + it.0[0] == self && acc.0[0] == init && - Self::completed(it.0[it.1 - 1]) && - result == acc.0[it.1 - 1] && - // ∀ i. (0 ≤ i ∧ i < it.1 - 1) ⟹ - // ∃ item. Self::step(it[i], item, it[i+1]) - // ∧ post!(f(acc[i], item), acc[i+1]) - // !(∃ i. (0 ≤ i ∧ i < it.1 - 1) ∧ !(∃ item. step ∧ post)) + Self::completed(it.0[l - 1]) && + result == acc.0[l - 1] && !( - thrust_models::exists(|i| - (0 <= i && i < it.1 - 1) && + exists(|i| + (0 <= i && i < l - 1) && !( - thrust_models::exists(|item| + exists(|item| + !Self::completed(it.0[i]) && Self::step(it.0[i], item, it.0[i + 1]) && + thrust_macros::pre!(f(acc.0[i], item)) && thrust_macros::post!( f(acc.0[i], item), acc.0[i + 1] @@ -46,7 +47,7 @@ trait Iterator { ) ) ) - )) + )))) )] fn fold(mut self, init: B, mut f: F) -> B where @@ -55,6 +56,34 @@ trait Iterator { { let mut accum = init; while let Some(x) = self.next() { + thrust_macros::invariant!( + |accum: B| + exists(|it: thrust_models::model::Vec| + exists(|fn_: thrust_models::model::Vec| + exists(|acc| + exists(|l: thrust_models::model::Int| + it.0[0] == self && + fn_.0[0] == f && + acc.0[0] == init && + accum == acc.0[l - 1] && + !( + exists(|i: thrust_models::model::Int| + (0 <= i && i < l - 1) && + !( + exists(|item: Self::Item| + !Self::completed(it.0[i]) && + Self::step(it.0[i], item, it.0[i + 1]) && + thrust_macros::pre!(f(acc.0[i], item)) && + thrust_macros::post!( + f(acc.0[i], item), + acc.0[i + 1] + ) + ) + ) + ) + ) + )))) + ); accum = f(accum, x); } accum From 848f511c3846f89b1a848e8bf8c120a8d5cbc24c Mon Sep 17 00:00:00 2001 From: coeff-aij <175928954+coeff-aij@users.noreply.github.com> Date: Sun, 14 Jun 2026 23:46:42 +0900 Subject: [PATCH 55/55] add test codes for reproducing/avoiding annotation errors --- .../ui/annot-error/array_index_literal_int.rs | 24 ++++++++ .../array_index_literal_int_workaround.rs | 27 +++++++++ .../annot-error/formula_fn_capture_local.rs | 47 +++++++++++++++ .../invariant_context_self_trait_bound.rs | 50 ++++++++++++++++ ...ant_context_self_trait_bound_workaround.rs | 60 +++++++++++++++++++ .../invariant_context_trait_method.rs | 27 +++++++++ ...variant_context_trait_method_workaround.rs | 49 +++++++++++++++ 7 files changed, 284 insertions(+) create mode 100644 tests/ui/annot-error/array_index_literal_int.rs create mode 100644 tests/ui/annot-error/array_index_literal_int_workaround.rs create mode 100644 tests/ui/annot-error/formula_fn_capture_local.rs create mode 100644 tests/ui/annot-error/invariant_context_self_trait_bound.rs create mode 100644 tests/ui/annot-error/invariant_context_self_trait_bound_workaround.rs create mode 100644 tests/ui/annot-error/invariant_context_trait_method.rs create mode 100644 tests/ui/annot-error/invariant_context_trait_method_workaround.rs diff --git a/tests/ui/annot-error/array_index_literal_int.rs b/tests/ui/annot-error/array_index_literal_int.rs new file mode 100644 index 00000000..bb64b171 --- /dev/null +++ b/tests/ui/annot-error/array_index_literal_int.rs @@ -0,0 +1,24 @@ +// Reproduces: an integer literal used as an `Array` index in a spec +// expression fails to type-check (E0308 "expected `Int`, found integer"). +// +// `thrust_models::model::Array` has an `Index` impl whose index +// type is the `I` parameter; for `Array` that is the `model::Int` +// ZST, which is not the same as Rust's `{integer}` literal type. The spec +// attribute path lowers `it[0]` as a Rust expression, so the `0` must be +// a `model::Int`-typed term. No such literal is constructible in Rust +// source today. +// +// See `array_index_literal_int_workaround.rs` for the bound-variable +// form that sidesteps the literal. + +#[thrust_macros::requires(true)] +#[thrust_macros::ensures( + thrust_models::exists(|it: thrust_models::model::Array| + it[0] == 0 + ) +)] +fn head(arr: Vec) -> i64 { + arr[0] +} + +fn main() {} diff --git a/tests/ui/annot-error/array_index_literal_int_workaround.rs b/tests/ui/annot-error/array_index_literal_int_workaround.rs new file mode 100644 index 00000000..74d74953 --- /dev/null +++ b/tests/ui/annot-error/array_index_literal_int_workaround.rs @@ -0,0 +1,27 @@ +// Annotation-side workaround for `array_index_literal_int.rs`. +// +// Rather than writing the literal `0` as the index (which fails because +// the `Index` impl on `Array` requires `I`-typed indices, and +// `model::Int` has no Rust literal form), bind the index with an +// existential and let typeck infer its sort: +// +// exists(|idx| it[idx] == 0) +// +// `idx` gets the `model::Int` sort from the `Index` site's expected +// `I = model::Int`. The expression type-checks; the trade-off is that +// the spec no longer pins a specific index like "0" or "1" — it just +// asserts "there exists some index such that the value at that index is 0". + +#[thrust_macros::requires(true)] +#[thrust_macros::ensures( + thrust_models::exists(|it: thrust_models::model::Array| + thrust_models::exists(|idx| + it[idx] == 0 + ) + ) +)] +fn head(arr: Vec) -> i64 { + arr[0] +} + +fn main() {} diff --git a/tests/ui/annot-error/formula_fn_capture_local.rs b/tests/ui/annot-error/formula_fn_capture_local.rs new file mode 100644 index 00000000..ba7ec28c --- /dev/null +++ b/tests/ui/annot-error/formula_fn_capture_local.rs @@ -0,0 +1,47 @@ +// Reproduces: a `formula_fn` produced by `requires`/`ensures`/`invariant!` +// cannot capture the surrounding function's local bindings (E0434 "can't +// capture dynamic environment in a fn item"). +// +// The macro lowers the spec into a free `fn _thrust_ensures_X(...)` whose +// only inputs are the host parameters (lowered to their `Model::Ty`) and +// the closure's bound variables. Any reference to a `let`-bound name in +// the host function is rejected. +// +// Same shape, applied to `_invariant_with_context!`: the host signature +// re-declared in the macro head (e.g. `fn run(self, f: B, g: F)`) +// is *not* threaded into the `formula_fn` parameters either; the macro +// currently only lowers the closure params plus the synthetic +// `__ThrustSelf` (for `Self` rewrite). +// +// No annotation-side workaround: this is a macro bug in +// `thrust-macros/src/invariant.rs::expand_invariant` (the host-signature +// re-declaration is parsed but its parameters are dropped on the floor). +// Either fix the macro to lower the re-declared signature's params via +// `type_lowering.lower_params(...)` and add them to the formula_fn, or +// restructure the invariant to not mention the host parameters (which +// often defeats the point of the invariant). + +#[thrust_macros::context] +trait Foo { + fn run(self, f: B, g: F) -> B + where + Self: Sized, + F: FnOnce(B) -> B, + { + let mut x: i64 = 0; + while x < 1 { + thrust_macros::_invariant_with_context!( + #[thrust::_outer_context(trait Foo {})] + fn run(self: Self, f: B, g: F) -> B + where + Self: Sized, + F: FnOnce(B) -> B; + |x: i64| x == f && g == f + ); + x += 1; + } + f + } +} + +fn main() {} diff --git a/tests/ui/annot-error/invariant_context_self_trait_bound.rs b/tests/ui/annot-error/invariant_context_self_trait_bound.rs new file mode 100644 index 00000000..25f9ca12 --- /dev/null +++ b/tests/ui/annot-error/invariant_context_self_trait_bound.rs @@ -0,0 +1,50 @@ +// Reproduces: when an `_invariant_with_context!` rewrites `Self` to a +// synthetic `__ThrustSelf` generic in the injected `formula_fn`, it does +// NOT automatically propagate the host trait bound (here `Self: Foo`). +// Calling trait items (the user-defined predicates `completed` / `step` +// and the associated `Item` type) on the synthetic `Self` therefore +// fails with E0599 / E0220 "no function / associated type named X found +// for `__ThrustSelf`". +// +// See `invariant_context_self_trait_bound_workaround.rs` for a partial +// workaround (`Self: Sized + Foo` in the re-declared where clause) that +// silences E0599 (the trait method calls) but leaves E0220 (the +// associated type) untouched — fully fixing the latter requires the +// `expand_invariant` macro to also rewrite `Self` to `__ThrustSelf` in +// the propagated where-clause predicates. + +#[thrust_macros::context] +trait Foo { + type Item; + + #[thrust_macros::predicate] + fn completed(self) -> bool; + #[thrust_macros::predicate] + fn step(self, item: Self::Item, dist: Self) -> bool; + + fn run(mut self, init: B, mut f: F) -> B + where + Self: Sized, + F: FnMut(B, Self::Item) -> B, + { + let mut accum = init; + while true { + thrust_macros::_invariant_with_context!( + #[thrust::_outer_context(trait Foo { type Item; })] + fn run(mut self: Self, init: B, mut f: F) -> B + where + Self: Sized, + F: FnMut(B, Self::Item) -> B; + |accum: B| thrust_models::exists( + |item: Self::Item| + Self::step(*self, item, *self) + && accum == init + ) + ); + break; + } + accum + } +} + +fn main() {} diff --git a/tests/ui/annot-error/invariant_context_self_trait_bound_workaround.rs b/tests/ui/annot-error/invariant_context_self_trait_bound_workaround.rs new file mode 100644 index 00000000..3fc07657 --- /dev/null +++ b/tests/ui/annot-error/invariant_context_self_trait_bound_workaround.rs @@ -0,0 +1,60 @@ +// Annotation-side partial workaround for +// `invariant_context_self_trait_bound.rs`. +// +// Adding the host trait bound to the re-declared signature's where +// clause (`Self: Sized + Foo` instead of just `Self: Sized`) makes the +// `expand_invariant` macro copy it into the `formula_fn`'s where +// clause, so `__ThrustSelf: Foo` is in scope. That silences the trait +// method-call errors (E0599 for `__ThrustSelf::step` / +// `__ThrustSelf::completed`). +// +// What it does NOT fix: E0220 for `__ThrustSelf::Item`. The macro's +// `where_predicates()` walk copies the re-declared where-clause +// predicates verbatim — `Self` is *not* rewritten to `__ThrustSelf` in +// the copied predicates, so the copy still talks about `Self` (host +// type) rather than `__ThrustSelf` (synthetic). The associated type +// `Item` lookup goes through `Self` instead of `__ThrustSelf`, and Rust +// complains. Fully fixing this needs the macro to rewrite `Self` to +// `__ThrustSelf` in the propagated where-clause predicates, then add +// `<__ThrustSelf as Foo>::Item` (or an analogous `Item` projection) to +// the `__ThrustSelf` parameter scope. + +#[thrust_macros::context] +trait Foo { + type Item; + + #[thrust_macros::predicate] + fn completed(self) -> bool; + #[thrust_macros::predicate] + fn step(self, item: Self::Item, dist: Self) -> bool; + + fn run(mut self, init: B, mut f: F) -> B + where + Self: Sized, + F: FnMut(B, Self::Item) -> B, + { + let mut accum = init; + while true { + thrust_macros::_invariant_with_context!( + #[thrust::_outer_context(trait Foo { type Item; })] + fn run(mut self: Self, init: B, mut f: F) -> B + where + // ← the partial-fix: add the host trait bound to + // the re-declared where clause. The macro copies + // it to the formula_fn where, so __ThrustSelf: Foo + // resolves the trait method calls. + Self: Sized + Foo, + F: FnMut(B, Self::Item) -> B; + |accum: B| thrust_models::exists( + |item: Self::Item| + Self::step(*self, item, *self) + && accum == init + ) + ); + break; + } + accum + } +} + +fn main() {} diff --git a/tests/ui/annot-error/invariant_context_trait_method.rs b/tests/ui/annot-error/invariant_context_trait_method.rs new file mode 100644 index 00000000..d4bea507 --- /dev/null +++ b/tests/ui/annot-error/invariant_context_trait_method.rs @@ -0,0 +1,27 @@ +// Reproduces: `#[thrust_macros::invariant_context]` attached to a *trait* +// method fails with E0401 ("can't use `Self` from outer item"). +// +// `invariant_context` is `ItemFn`-only (`thrust-macros/src/invariant_context.rs`). +// On a trait method it parses, but it never threads the trait-level `Self` +// through to the generated `formula_fn`, so the injected +// `_invariant_with_context!` macro ends up rewriting the closure body against +// the outer trait's `Self` (which is out of scope) and Rust rejects the use. + +#[thrust_macros::context] +trait Foo { + type Item; + + #[thrust_macros::invariant_context] + fn run(&mut self) + where + Self: Sized, + { + let mut x: i64 = 0; + while x < 1 { + thrust_macros::invariant!(|x: i64| x >= 0); + x += 1; + } + } +} + +fn main() {} diff --git a/tests/ui/annot-error/invariant_context_trait_method_workaround.rs b/tests/ui/annot-error/invariant_context_trait_method_workaround.rs new file mode 100644 index 00000000..5630319d --- /dev/null +++ b/tests/ui/annot-error/invariant_context_trait_method_workaround.rs @@ -0,0 +1,49 @@ +// Annotation-side workaround for `invariant_context_trait_method.rs`. +// +// The `#[thrust_macros::invariant_context]` attribute is `ItemFn`-only +// (its `expand` parses as `syn::ItemFn`), so attaching it to a trait +// method triggers E0401 because the trait's `Self` is out of scope for +// the generated `formula_fn`. The other annotation-side attempt — +// hand-rolling `thrust_macros::_invariant_with_context!` inside the +// loop body — runs into the same problem (the macro's `SelfRewriter` +// only kicks in when the closure body actually mentions `Self`; +// otherwise `Self: Model` constraints are produced against the outer +// `Self` and Rust rejects them). +// +// Workaround: drop the invariant on the trait method, and instead +// provide it on the concrete impl method, where `invariant_context` +// works (`ItemFn` parse target). The impl is the only place the +// invariant is meaningful anyway: the trait method's spec is +// independent of any concrete iterator type. + +#[thrust_macros::context] +trait Foo { + type Item; + + fn run(&mut self); +} + +struct Bar; + +impl thrust_models::Model for Bar { + type Ty = Bar; +} + +#[thrust_macros::context] +impl Foo for Bar { + type Item = i64; + + // `invariant_context` on an impl method is fine: the host is an + // `ItemFn` (`impl` method) and `Self` is the impl's self-type, + // not the trait's. + #[thrust_macros::invariant_context] + fn run(&mut self) { + let mut x: i64 = 0; + while x < 1 { + thrust_macros::invariant!(|x: i64| x >= 0); + x += 1; + } + } +} + +fn main() {}