From 9bb87284dd185b93d1069d44198b686bb85edced 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/23] 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 32456b45..80dcf3f0 100644 --- a/src/rty.rs +++ b/src/rty.rs @@ -1637,7 +1637,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 092debd9ff9dcf819b451ba0c05f4f297abbb24d 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/23] 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 a29d76d8..f3f3782e 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 e2142b87621a783e035eb7ab35c5f254e1fde7d1 Mon Sep 17 00:00:00 2001 From: coeff-aij <175928954+coeff-aij@users.noreply.github.com> Date: Sun, 24 May 2026 18:11:13 +0900 Subject: [PATCH 03/23] change: translate Type::Param into chc::Sort::Forall --- src/analyze.rs | 30 ++++++++++--- src/analyze/annot_fn.rs | 28 ++++++++++-- src/analyze/basic_block.rs | 2 +- src/analyze/local_def.rs | 2 +- src/rty.rs | 4 +- src/rty/params.rs | 89 +++++++++++++++++++------------------- 6 files changed, 98 insertions(+), 57 deletions(-) diff --git a/src/analyze.rs b/src/analyze.rs index 9339b1da..13a0316e 100644 --- a/src/analyze.rs +++ b/src/analyze.rs @@ -190,6 +190,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> { @@ -217,6 +218,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> { @@ -240,6 +243,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, @@ -248,6 +252,7 @@ impl<'tcx> Analyzer<'tcx> { basic_blocks, def_ids: did_cache::DefIdCache::new(tcx), enum_defs, + type_params, } } @@ -281,7 +286,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 { @@ -409,9 +414,14 @@ impl<'tcx> Analyzer<'tcx> { return Some(formula_fn.clone()); } - let translator = annot_fn::AnnotFnTranslator::new(self.tcx, local_def_id) - .with_generic_args(generic_args) - .with_def_id_cache(self.def_ids()); + let translator = annot_fn::AnnotFnTranslator::new( + self.tcx, + local_def_id, + self.type_params.clone(), + self.system.clone(), + ) + .with_generic_args(generic_args) + .with_def_id_cache(self.def_ids()); let formula_fn = translator.to_formula_fn(); deferred_formula_fn_cache .borrow_mut() @@ -426,7 +436,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) => { @@ -535,6 +545,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 aae82be4..2905bf46 100644 --- a/src/analyze/annot_fn.rs +++ b/src/analyze/annot_fn.rs @@ -1,13 +1,15 @@ +use std::cell::RefCell; use std::collections::HashMap; +use std::rc::Rc; 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 crate::analyze::{self, did_cache::DefIdCache}; +use crate::analyze::{self, did_cache::DefIdCache, TypeParams}; use crate::annot::AnnotFormula; -use crate::chc; +use crate::chc::{self, System}; use crate::refine::{self, TypeBuilder}; use crate::rty; @@ -137,15 +139,29 @@ pub struct AnnotFnTranslator<'tcx> { def_ids: DefIdCache<'tcx>, type_builder: TypeBuilder<'tcx>, env: HashMap>, + + type_params: Rc>, + system: Rc>, } impl<'tcx> AnnotFnTranslator<'tcx> { - pub fn new(tcx: TyCtxt<'tcx>, local_def_id: LocalDefId) -> Self { + pub fn new( + tcx: TyCtxt<'tcx>, + local_def_id: LocalDefId, + type_params: Rc>, + system: Rc>, + ) -> Self { let body = tcx.hir_body_owned_by(local_def_id); let generic_args = tcx.mk_args(&[]); let typeck = tcx.typeck(local_def_id); let def_ids = DefIdCache::new(tcx); - 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(), + type_params.clone(), + system.clone(), + ); let mut translator = Self { tcx, local_def_id, @@ -155,6 +171,8 @@ impl<'tcx> AnnotFnTranslator<'tcx> { def_ids, type_builder, env: HashMap::default(), + type_params, + system, }; translator.build_env_from_params(); translator @@ -171,6 +189,8 @@ impl<'tcx> AnnotFnTranslator<'tcx> { self.tcx, self.def_ids.clone(), self.local_def_id.to_def_id(), + self.type_params.clone(), + self.system.clone(), ); self } diff --git a/src/analyze/basic_block.rs b/src/analyze/basic_block.rs index 15d70033..e59bffe9 100644 --- a/src/analyze/basic_block.rs +++ b/src/analyze/basic_block.rs @@ -1173,7 +1173,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 be309448..8e735e85 100644 --- a/src/analyze/local_def.rs +++ b/src/analyze/local_def.rs @@ -973,7 +973,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 80dcf3f0..801948ee 100644 --- a/src/rty.rs +++ b/src/rty.rs @@ -609,7 +609,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 @@ -914,7 +914,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 2a9af20cc3334ced431148168d457aab2a6fd1fe Mon Sep 17 00:00:00 2001 From: coeff-aij <175928954+coeff-aij@users.noreply.github.com> Date: Sun, 24 May 2026 18:11:58 +0900 Subject: [PATCH 04/23] change: use forall sort instead of deferred type --- src/analyze/crate_.rs | 10 +++------- 1 file changed, 3 insertions(+), 7 deletions(-) diff --git a/src/analyze/crate_.rs b/src/analyze/crate_.rs index c85038fa..d5ed1f95 100644 --- a/src/analyze/crate_.rs +++ b/src/analyze/crate_.rs @@ -120,13 +120,9 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { }; use mir_ty::TypeVisitableExt as _; - if sig.has_param() { - if self.skip_analysis.contains(&local_def_id) { - self.ctx - .register_deferred_def_without_analysis(target_def_id, local_def_id); - } else { - self.ctx.register_deferred_def(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 c913ca407bbb2296537792f08ea41b835470efd6 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/23] 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 dfd6617a97c00c5a0acedabbbbaf21720b2effcb 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/23] 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 f3f3782e..24a8c9c8 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 0241ef98dda1a3e758a273a766d6be7bbee9e1ac 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/23] 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 6fcc8305f7742e37f660cff6a6f5a03de548e16b 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/23] 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 d77c0f2d8bf842a7b46efeba8ae03ae8587e39f5 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/23] 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 13a0316e..86f116a6 100644 --- a/src/analyze.rs +++ b/src/analyze.rs @@ -385,9 +385,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 fae056fc25ef54f372042db903f05a70c9ed16ca 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/23] 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 dc3a35e13685bca67a46fed650c66d79d7f3d394 Mon Sep 17 00:00:00 2001 From: coeff-aij <175928954+coeff-aij@users.noreply.github.com> Date: Tue, 26 May 2026 00:35:42 +0900 Subject: [PATCH 11/23] remove all extern_spec in std.rs temporarily --- std.rs | 750 ++++++++++++++++++++++++++++----------------------------- 1 file changed, 375 insertions(+), 375 deletions(-) diff --git a/std.rs b/std.rs index dc30924e..fdaa4cf8 100644 --- a/std.rs +++ b/std.rs @@ -304,378 +304,378 @@ 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(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(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 4c0040ac6f3b1ec90edb0f2752f1c856d171df72 Mon Sep 17 00:00:00 2001 From: coeff-aij <175928954+coeff-aij@users.noreply.github.com> Date: Tue, 26 May 2026 00:45:27 +0900 Subject: [PATCH 12/23] add: imcomplete support for alias types --- src/analyze.rs | 21 ++++++++++++++------- src/analyze/annot_fn.rs | 6 +++--- src/analyze/crate_.rs | 2 -- src/refine/template.rs | 17 +++++++++++++---- 4 files changed, 30 insertions(+), 16 deletions(-) diff --git a/src/analyze.rs b/src/analyze.rs index 86f116a6..eb56ed02 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; @@ -190,7 +191,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> { @@ -219,7 +226,7 @@ pub struct Analyzer<'tcx> { enum_defs: Rc>, - type_params: Rc>, + type_params: Rc>, } impl<'tcx> crate::refine::TemplateRegistry for Analyzer<'tcx> { @@ -385,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/annot_fn.rs b/src/analyze/annot_fn.rs index 2905bf46..815647e5 100644 --- a/src/analyze/annot_fn.rs +++ b/src/analyze/annot_fn.rs @@ -7,7 +7,7 @@ use rustc_hir::{def_id::LocalDefId, HirId}; use rustc_index::IndexVec; use rustc_middle::ty::{self as mir_ty, TyCtxt}; -use crate::analyze::{self, did_cache::DefIdCache, TypeParams}; +use crate::analyze::{self, did_cache::DefIdCache, TypeParamMap}; use crate::annot::AnnotFormula; use crate::chc::{self, System}; use crate::refine::{self, TypeBuilder}; @@ -140,7 +140,7 @@ pub struct AnnotFnTranslator<'tcx> { type_builder: TypeBuilder<'tcx>, env: HashMap>, - type_params: Rc>, + type_params: Rc>, system: Rc>, } @@ -148,7 +148,7 @@ impl<'tcx> AnnotFnTranslator<'tcx> { pub fn new( tcx: TyCtxt<'tcx>, local_def_id: LocalDefId, - type_params: Rc>, + type_params: Rc>, system: Rc>, ) -> Self { let body = tcx.hir_body_owned_by(local_def_id); 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/src/refine/template.rs b/src/refine/template.rs index 24a8c9c8..6be2fced 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 673d42ced17b3e7daa70a34c39311bca7821d9dc 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/23] 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 20d6f341..b22ce7ee 100644 --- a/src/rty/subtyping.rs +++ b/src/rty/subtyping.rs @@ -71,7 +71,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 a7f23e88c72b9cd990be7b3c73ef4b8834dad7e3 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/23] 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 c16077490acf0d6808f46ccf626e44f7ce5d9e43 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/23] 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 815647e5..4a9c420e 100644 --- a/src/analyze/annot_fn.rs +++ b/src/analyze/annot_fn.rs @@ -5,7 +5,7 @@ use std::rc::Rc; 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, TypeParamMap}; use crate::annot::AnnotFormula; @@ -224,29 +224,48 @@ impl<'tcx> AnnotFnTranslator<'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, @@ -515,8 +534,12 @@ impl<'tcx> AnnotFnTranslator<'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, @@ -524,14 +547,15 @@ impl<'tcx> AnnotFnTranslator<'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 60e5ad6d..1ff1291b 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 e8554404680acbeb3733ad4fcd80ddbeae8e7cad 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/23] 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 b22ce7ee..57a884d3 100644 --- a/src/rty/subtyping.rs +++ b/src/rty/subtyping.rs @@ -71,8 +71,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); @@ -121,6 +120,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 fdf13b8e8999249bbd02ca280f1831ef490e48e4 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/23] 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 eb56ed02..8d60fa4f 100644 --- a/src/analyze.rs +++ b/src/analyze.rs @@ -547,15 +547,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 e59bffe9..cbb18eea 100644 --- a/src/analyze/basic_block.rs +++ b/src/analyze/basic_block.rs @@ -1166,6 +1166,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(); @@ -1173,7 +1174,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 8e735e85..029ca9e2 100644 --- a/src/analyze/local_def.rs +++ b/src/analyze/local_def.rs @@ -865,7 +865,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { let rty = self.ctx.basic_block_ty(self.local_def_id, bb).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); diff --git a/src/refine/template.rs b/src/refine/template.rs index 6be2fced..45a70458 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 3d963695391d3bb2f5a99c7926f68feeb167f96e 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/23] 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 8d60fa4f..3befd73d 100644 --- a/src/analyze.rs +++ b/src/analyze.rs @@ -441,8 +441,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 cbb18eea..193e0896 100644 --- a/src/analyze/basic_block.rs +++ b/src/analyze/basic_block.rs @@ -636,7 +636,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; } @@ -648,7 +649,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 029ca9e2..617646ed 100644 --- a/src/analyze/local_def.rs +++ b/src/analyze/local_def.rs @@ -318,7 +318,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) } // Note that we do not expect predicate variables to be generated here diff --git a/src/refine/template.rs b/src/refine/template.rs index 45a70458..c430ca03 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 a6fe81e2e2932a0db255ce8d69a3fbad28aa5ea1 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/23] 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 4a9c420e..4596574a 100644 --- a/src/analyze/annot_fn.rs +++ b/src/analyze/annot_fn.rs @@ -534,7 +534,7 @@ impl<'tcx> AnnotFnTranslator<'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), @@ -547,13 +547,19 @@ impl<'tcx> AnnotFnTranslator<'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 7deba43263495fa67f419872a3fbf44f7a0f02b1 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/23] 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 c430ca03..11684f33 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 9824e3af744000aacbab607460027fc5b06b3610 Mon Sep 17 00:00:00 2001 From: coeff-aij <175928954+coeff-aij@users.noreply.github.com> Date: Fri, 29 May 2026 15:16:56 +0900 Subject: [PATCH 21/23] fix: propagate the DefId for the owner function of formula_fn and extern_spec_fn --- src/analyze.rs | 14 +++- src/analyze/annot_fn.rs | 8 +- src/analyze/basic_block.rs | 5 +- src/analyze/crate_.rs | 10 +-- src/analyze/local_def.rs | 157 ++++++++++++++++++++++--------------- 5 files changed, 115 insertions(+), 79 deletions(-) diff --git a/src/analyze.rs b/src/analyze.rs index 3befd73d..19e91360 100644 --- a/src/analyze.rs +++ b/src/analyze.rs @@ -412,6 +412,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)?; @@ -425,6 +426,7 @@ impl<'tcx> Analyzer<'tcx> { local_def_id, self.type_params.clone(), self.system.clone(), + owner_fn_id, ) .with_generic_args(generic_args) .with_def_id_cache(self.def_ids()); @@ -548,7 +550,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) } @@ -654,6 +656,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, @@ -684,7 +687,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 @@ -703,6 +708,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>, @@ -734,7 +740,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 4596574a..977adab4 100644 --- a/src/analyze/annot_fn.rs +++ b/src/analyze/annot_fn.rs @@ -3,7 +3,10 @@ use std::collections::HashMap; use std::rc::Rc; 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}; @@ -150,6 +153,7 @@ impl<'tcx> AnnotFnTranslator<'tcx> { local_def_id: LocalDefId, type_params: Rc>, system: Rc>, + owner_fn_id: DefId, ) -> Self { let body = tcx.hir_body_owned_by(local_def_id); let generic_args = tcx.mk_args(&[]); @@ -158,7 +162,7 @@ impl<'tcx> AnnotFnTranslator<'tcx> { let type_builder = TypeBuilder::new( tcx, def_ids.clone(), - local_def_id.to_def_id(), + owner_fn_id, type_params.clone(), system.clone(), ); diff --git a/src/analyze/basic_block.rs b/src/analyze/basic_block.rs index 193e0896..1b0949dd 100644 --- a/src/analyze/basic_block.rs +++ b/src/analyze/basic_block.rs @@ -649,7 +649,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 617646ed..de10fe8c 100644 --- a/src/analyze/local_def.rs +++ b/src/analyze/local_def.rs @@ -37,6 +37,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 @@ -46,6 +122,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`] @@ -201,13 +278,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 { @@ -318,7 +389,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) } // Note that we do not expect predicate variables to be generated here @@ -358,6 +430,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( @@ -365,6 +438,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() { @@ -374,12 +448,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()); @@ -447,62 +523,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 { @@ -973,12 +994,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 6f552d5c09d6715c224ab3797db8575d7dc75370 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/23] 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 11684f33..68cd4b58 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 801948ee..9eb3381e 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}; @@ -609,7 +609,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 @@ -617,17 +618,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 { @@ -914,7 +922,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(); @@ -1000,7 +1008,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(), @@ -1567,7 +1575,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, @@ -1603,15 +1611,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 57a884d3..092116d5 100644 --- a/src/rty/subtyping.rs +++ b/src/rty/subtyping.rs @@ -120,7 +120,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 d1a09ddd5b1aaa1bd72b88809d0a2b9572e0bae4 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/23] 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 977adab4..561abb06 100644 --- a/src/analyze/annot_fn.rs +++ b/src/analyze/annot_fn.rs @@ -558,8 +558,20 @@ impl<'tcx> AnnotFnTranslator<'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, } }