From cdb8b2266c9f761c42a3f69a7838a0f4725ea053 Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 8 Oct 2026 21:30:30 +0000 Subject: [PATCH 1/2] Key basic block types by generic args as well as def id A generic function is analyzed once per instantiation, but its basic block types were stored under its LocalDefId alone. Analyzing one instantiation from inside another (e.g. g:: calling g::) overwrote the outer instantiation's blocks, so the outer analysis continued with the inner one's block types and predicate variables. This either panicked with "precondition is already registered for basic block" or silently verified the outer instantiation against the inner one's behaviour. Fixes #328 Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Q3Dt425cRNNW8aSShzGyDA --- src/analyze.rs | 39 +++++++++++++++---- src/analyze/basic_block.rs | 17 ++++++-- src/analyze/local_def.rs | 34 +++++++++++----- tests/ui/fail/fn_poly_nested_instantiation.rs | 28 +++++++++++++ tests/ui/pass/fn_poly_nested_instantiation.rs | 28 +++++++++++++ 5 files changed, 125 insertions(+), 21 deletions(-) create mode 100644 tests/ui/fail/fn_poly_nested_instantiation.rs create mode 100644 tests/ui/pass/fn_poly_nested_instantiation.rs diff --git a/src/analyze.rs b/src/analyze.rs index 9b3967cf..c2bfb0f5 100644 --- a/src/analyze.rs +++ b/src/analyze.rs @@ -261,7 +261,8 @@ pub struct Analyzer<'tcx> { /// Resulting CHC system. system: Rc>, - basic_blocks: HashMap>, + basic_blocks: + HashMap<(LocalDefId, mir_ty::GenericArgsRef<'tcx>), HashMap>, def_ids: did_cache::DefIdCache<'tcx>, enum_defs: Rc>, @@ -614,11 +615,13 @@ impl<'tcx> Analyzer<'tcx> { pub fn register_basic_block_ty_with_precondition( &mut self, def_id: LocalDefId, + generic_args: mir_ty::GenericArgsRef<'tcx>, bb: BasicBlock, rty: BasicBlockType, ) { self.register_basic_block_def( def_id, + generic_args, bb, BasicBlockDef { ty: rty, @@ -630,11 +633,13 @@ impl<'tcx> Analyzer<'tcx> { pub fn register_basic_block_ty_without_precondition( &mut self, def_id: LocalDefId, + generic_args: mir_ty::GenericArgsRef<'tcx>, bb: BasicBlock, rty: BasicBlockType, ) { self.register_basic_block_def( def_id, + generic_args, bb, BasicBlockDef { ty: rty, @@ -643,26 +648,37 @@ impl<'tcx> Analyzer<'tcx> { ); } - fn register_basic_block_def(&mut self, def_id: LocalDefId, bb: BasicBlock, def: BasicBlockDef) { + fn register_basic_block_def( + &mut self, + def_id: LocalDefId, + generic_args: mir_ty::GenericArgsRef<'tcx>, + bb: BasicBlock, + def: BasicBlockDef, + ) { tracing::debug!( def_id = ?def_id, + ?generic_args, ?bb, rty = %def.ty.display(), has_precondition = def.has_precondition, "register_basic_block_def", ); - self.basic_blocks.entry(def_id).or_default().insert(bb, def); + self.basic_blocks + .entry((def_id, generic_args)) + .or_default() + .insert(bb, def); } pub fn register_basic_block_precondition( &mut self, def_id: LocalDefId, + generic_args: mir_ty::GenericArgsRef<'tcx>, bb: BasicBlock, precondition: rty::Refinement, ) { let bb_def = &mut self .basic_blocks - .get_mut(&def_id) + .get_mut(&(def_id, generic_args)) .unwrap() .get_mut(&bb) .unwrap(); @@ -674,16 +690,22 @@ impl<'tcx> Analyzer<'tcx> { bb_def.ty.set_precondition(precondition); } - pub fn basic_block_ty(&self, def_id: LocalDefId, bb: BasicBlock) -> &BasicBlockType { - &self.basic_blocks[&def_id][&bb].ty + pub fn basic_block_ty( + &self, + def_id: LocalDefId, + generic_args: mir_ty::GenericArgsRef<'tcx>, + bb: BasicBlock, + ) -> &BasicBlockType { + &self.basic_blocks[&(def_id, generic_args)][&bb].ty } pub fn basic_block_ty_with_precondition( &self, def_id: LocalDefId, + generic_args: mir_ty::GenericArgsRef<'tcx>, bb: BasicBlock, ) -> &BasicBlockType { - let def = &self.basic_blocks[&def_id][&bb]; + let def = &self.basic_blocks[&(def_id, generic_args)][&bb]; assert!( def.has_precondition, "basic block does not have precondition" @@ -724,9 +746,10 @@ impl<'tcx> Analyzer<'tcx> { pub fn basic_block_analyzer( &mut self, local_def_id: LocalDefId, + generic_args: mir_ty::GenericArgsRef<'tcx>, bb: BasicBlock, ) -> basic_block::Analyzer<'tcx, '_> { - basic_block::Analyzer::new(self, local_def_id, bb) + basic_block::Analyzer::new(self, local_def_id, generic_args, bb) } pub fn solve(&mut self) { diff --git a/src/analyze/basic_block.rs b/src/analyze/basic_block.rs index 97cc7f89..958ab449 100644 --- a/src/analyze/basic_block.rs +++ b/src/analyze/basic_block.rs @@ -189,6 +189,7 @@ pub struct Analyzer<'tcx, 'ctx> { tcx: TyCtxt<'tcx>, local_def_id: LocalDefId, + generic_args: mir_ty::GenericArgsRef<'tcx>, drop_points: DropPoints, basic_block: BasicBlock, body: Cow<'tcx, Body<'tcx>>, @@ -223,7 +224,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { fn basic_block_ty_with_precondition(&self, bb: BasicBlock) -> &BasicBlockType { self.ctx - .basic_block_ty_with_precondition(self.local_def_id, bb) + .basic_block_ty_with_precondition(self.local_def_id, self.generic_args, bb) } fn bind_local(&mut self, local: Local, rty: rty::RefinedType) { @@ -927,7 +928,9 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { bb: BasicBlock, outer_fn_param_vars: &HashMap, ) { - let bty = self.ctx.basic_block_ty(self.local_def_id, bb); + let bty = self + .ctx + .basic_block_ty(self.local_def_id, self.generic_args, bb); let mut capture = PrecondCapture::default(); for (param_idx, param_rty) in bty.as_ref().params.iter_enumerated() { @@ -950,8 +953,12 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { capture.push_env_state(&self.env); let precondition = capture.finish(&self.env); - self.ctx - .register_basic_block_precondition(self.local_def_id, bb, precondition); + self.ctx.register_basic_block_precondition( + self.local_def_id, + self.generic_args, + bb, + precondition, + ); } fn with_assumptions(&mut self, assumptions: Vec>, callback: F) -> T @@ -1713,6 +1720,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { pub fn new( ctx: &'ctx mut analyze::Analyzer<'tcx>, local_def_id: LocalDefId, + generic_args: mir_ty::GenericArgsRef<'tcx>, basic_block: BasicBlock, ) -> Self { let tcx = ctx.tcx; @@ -1726,6 +1734,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { ctx, tcx, local_def_id, + generic_args, drop_points, basic_block, body, diff --git a/src/analyze/local_def.rs b/src/analyze/local_def.rs index 6a9cdf1b..e5fd428d 100644 --- a/src/analyze/local_def.rs +++ b/src/analyze/local_def.rs @@ -966,15 +966,23 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { inv.push_conj(one); } bty.set_precondition(inv); - self.ctx - .register_basic_block_ty_with_precondition(self.local_def_id, bb, bty); + self.ctx.register_basic_block_ty_with_precondition( + self.local_def_id, + self.generic_args, + bb, + bty, + ); } else if analyze::basic_block::needs_own_precondition(&self.body, bb) { let bty = self .type_builder .for_template(&mut self.ctx) .build_basic_block(&self.body, live_locals, ret_ty); - self.ctx - .register_basic_block_ty_with_precondition(self.local_def_id, bb, bty); + self.ctx.register_basic_block_ty_with_precondition( + self.local_def_id, + self.generic_args, + bb, + bty, + ); } else { // The block inherits its predecessor's outgoing env state as its // precondition, materialized lazily during the predecessor's @@ -982,8 +990,12 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { let bty = self .type_builder .build_basic_block(&self.body, live_locals, ret_ty); - self.ctx - .register_basic_block_ty_without_precondition(self.local_def_id, bb, bty); + self.ctx.register_basic_block_ty_without_precondition( + self.local_def_id, + self.generic_args, + bb, + bty, + ); }; } } @@ -998,11 +1010,11 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { } let rty = self .ctx - .basic_block_ty_with_precondition(self.local_def_id, bb) + .basic_block_ty_with_precondition(self.local_def_id, self.generic_args, 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, self.generic_args, bb) .body(self.body.clone()) .drop_points(drop_points) .run(&rty, expected_fn_ty); @@ -1109,7 +1121,11 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { fn assert_entry(&mut self, expected: &rty::RefinedType) { let mut entry_ty = self .ctx - .basic_block_ty_with_precondition(self.local_def_id, mir::START_BLOCK) + .basic_block_ty_with_precondition( + self.local_def_id, + self.generic_args, + mir::START_BLOCK, + ) .clone(); tracing::debug!(expected = %expected.display(), entry = %entry_ty.display(), "assert_entry before"); let mut expected = expected.ty.as_function().cloned().unwrap(); diff --git a/tests/ui/fail/fn_poly_nested_instantiation.rs b/tests/ui/fail/fn_poly_nested_instantiation.rs new file mode 100644 index 00000000..8a9e6df1 --- /dev/null +++ b/tests/ui/fail/fn_poly_nested_instantiation.rs @@ -0,0 +1,28 @@ +//@error-in-other-file: Unsat +//@compile-flags: -C debug-assertions=off + +trait K { + fn k(&self) -> i32; +} + +impl K for i32 { + fn k(&self) -> i32 { + 1 + } +} + +impl K for i64 { + fn k(&self) -> i32 { + 2 + } +} + +fn g(t: T, n: i32) -> i32 { + let a = t.k(); + let r = if n > 0 { g(0_i64, 0) } else { 0 }; + r + a +} + +fn main() { + assert!(g(0_i32, 1) == 4); +} diff --git a/tests/ui/pass/fn_poly_nested_instantiation.rs b/tests/ui/pass/fn_poly_nested_instantiation.rs new file mode 100644 index 00000000..fa9b88d4 --- /dev/null +++ b/tests/ui/pass/fn_poly_nested_instantiation.rs @@ -0,0 +1,28 @@ +//@check-pass +//@compile-flags: -C debug-assertions=off + +trait K { + fn k(&self) -> i32; +} + +impl K for i32 { + fn k(&self) -> i32 { + 1 + } +} + +impl K for i64 { + fn k(&self) -> i32 { + 2 + } +} + +fn g(t: T, n: i32) -> i32 { + let a = t.k(); + let r = if n > 0 { g(0_i64, 0) } else { 0 }; + r + a +} + +fn main() { + assert!(g(0_i32, 1) == 3); +} From 604ae4e23d6a61df575ff38d89c73c2cb1b5b6de Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 13 Oct 2026 02:13:38 +0000 Subject: [PATCH 2/2] Name the instantiation a basic block table is keyed by Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Q3Dt425cRNNW8aSShzGyDA --- src/analyze.rs | 52 ++++++++++++++++++-------------------- src/analyze/basic_block.rs | 24 ++++++------------ src/analyze/local_def.rs | 36 +++++++++++--------------- 3 files changed, 48 insertions(+), 64 deletions(-) diff --git a/src/analyze.rs b/src/analyze.rs index c2bfb0f5..5a9ca0f6 100644 --- a/src/analyze.rs +++ b/src/analyze.rs @@ -204,6 +204,15 @@ enum DefTy<'tcx> { Deferred(DeferredDefTy<'tcx>), } +/// A local definition with its generic parameters instantiated by `generic_args`. +/// +/// A generic function body is analyzed separately for each instantiation. +#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)] +pub struct LocalDefInstantiation<'tcx> { + pub def_id: LocalDefId, + pub generic_args: mir_ty::GenericArgsRef<'tcx>, +} + #[derive(Debug, Clone)] struct BasicBlockDef { ty: BasicBlockType, @@ -261,8 +270,7 @@ pub struct Analyzer<'tcx> { /// Resulting CHC system. system: Rc>, - basic_blocks: - HashMap<(LocalDefId, mir_ty::GenericArgsRef<'tcx>), HashMap>, + basic_blocks: HashMap, HashMap>, def_ids: did_cache::DefIdCache<'tcx>, enum_defs: Rc>, @@ -614,14 +622,12 @@ impl<'tcx> Analyzer<'tcx> { pub fn register_basic_block_ty_with_precondition( &mut self, - def_id: LocalDefId, - generic_args: mir_ty::GenericArgsRef<'tcx>, + instantiation: LocalDefInstantiation<'tcx>, bb: BasicBlock, rty: BasicBlockType, ) { self.register_basic_block_def( - def_id, - generic_args, + instantiation, bb, BasicBlockDef { ty: rty, @@ -632,14 +638,12 @@ impl<'tcx> Analyzer<'tcx> { pub fn register_basic_block_ty_without_precondition( &mut self, - def_id: LocalDefId, - generic_args: mir_ty::GenericArgsRef<'tcx>, + instantiation: LocalDefInstantiation<'tcx>, bb: BasicBlock, rty: BasicBlockType, ) { self.register_basic_block_def( - def_id, - generic_args, + instantiation, bb, BasicBlockDef { ty: rty, @@ -650,35 +654,32 @@ impl<'tcx> Analyzer<'tcx> { fn register_basic_block_def( &mut self, - def_id: LocalDefId, - generic_args: mir_ty::GenericArgsRef<'tcx>, + instantiation: LocalDefInstantiation<'tcx>, bb: BasicBlock, def: BasicBlockDef, ) { tracing::debug!( - def_id = ?def_id, - ?generic_args, + ?instantiation, ?bb, rty = %def.ty.display(), has_precondition = def.has_precondition, "register_basic_block_def", ); self.basic_blocks - .entry((def_id, generic_args)) + .entry(instantiation) .or_default() .insert(bb, def); } pub fn register_basic_block_precondition( &mut self, - def_id: LocalDefId, - generic_args: mir_ty::GenericArgsRef<'tcx>, + instantiation: LocalDefInstantiation<'tcx>, bb: BasicBlock, precondition: rty::Refinement, ) { let bb_def = &mut self .basic_blocks - .get_mut(&(def_id, generic_args)) + .get_mut(&instantiation) .unwrap() .get_mut(&bb) .unwrap(); @@ -692,20 +693,18 @@ impl<'tcx> Analyzer<'tcx> { pub fn basic_block_ty( &self, - def_id: LocalDefId, - generic_args: mir_ty::GenericArgsRef<'tcx>, + instantiation: LocalDefInstantiation<'tcx>, bb: BasicBlock, ) -> &BasicBlockType { - &self.basic_blocks[&(def_id, generic_args)][&bb].ty + &self.basic_blocks[&instantiation][&bb].ty } pub fn basic_block_ty_with_precondition( &self, - def_id: LocalDefId, - generic_args: mir_ty::GenericArgsRef<'tcx>, + instantiation: LocalDefInstantiation<'tcx>, bb: BasicBlock, ) -> &BasicBlockType { - let def = &self.basic_blocks[&(def_id, generic_args)][&bb]; + let def = &self.basic_blocks[&instantiation][&bb]; assert!( def.has_precondition, "basic block does not have precondition" @@ -745,11 +744,10 @@ impl<'tcx> Analyzer<'tcx> { pub fn basic_block_analyzer( &mut self, - local_def_id: LocalDefId, - generic_args: mir_ty::GenericArgsRef<'tcx>, + instantiation: LocalDefInstantiation<'tcx>, bb: BasicBlock, ) -> basic_block::Analyzer<'tcx, '_> { - basic_block::Analyzer::new(self, local_def_id, generic_args, bb) + basic_block::Analyzer::new(self, instantiation, bb) } pub fn solve(&mut self) { diff --git a/src/analyze/basic_block.rs b/src/analyze/basic_block.rs index 958ab449..2c9751fc 100644 --- a/src/analyze/basic_block.rs +++ b/src/analyze/basic_block.rs @@ -188,8 +188,7 @@ pub struct Analyzer<'tcx, 'ctx> { ctx: &'ctx mut analyze::Analyzer<'tcx>, tcx: TyCtxt<'tcx>, - local_def_id: LocalDefId, - generic_args: mir_ty::GenericArgsRef<'tcx>, + instantiation: analyze::LocalDefInstantiation<'tcx>, drop_points: DropPoints, basic_block: BasicBlock, body: Cow<'tcx, Body<'tcx>>, @@ -224,7 +223,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { fn basic_block_ty_with_precondition(&self, bb: BasicBlock) -> &BasicBlockType { self.ctx - .basic_block_ty_with_precondition(self.local_def_id, self.generic_args, bb) + .basic_block_ty_with_precondition(self.instantiation, bb) } fn bind_local(&mut self, local: Local, rty: rty::RefinedType) { @@ -928,9 +927,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { bb: BasicBlock, outer_fn_param_vars: &HashMap, ) { - let bty = self - .ctx - .basic_block_ty(self.local_def_id, self.generic_args, bb); + let bty = self.ctx.basic_block_ty(self.instantiation, bb); let mut capture = PrecondCapture::default(); for (param_idx, param_rty) in bty.as_ref().params.iter_enumerated() { @@ -953,12 +950,8 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { capture.push_env_state(&self.env); let precondition = capture.finish(&self.env); - self.ctx.register_basic_block_precondition( - self.local_def_id, - self.generic_args, - bb, - precondition, - ); + self.ctx + .register_basic_block_precondition(self.instantiation, bb, precondition); } fn with_assumptions(&mut self, assumptions: Vec>, callback: F) -> T @@ -1719,10 +1712,10 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { pub fn new( ctx: &'ctx mut analyze::Analyzer<'tcx>, - local_def_id: LocalDefId, - generic_args: mir_ty::GenericArgsRef<'tcx>, + instantiation: analyze::LocalDefInstantiation<'tcx>, basic_block: BasicBlock, ) -> Self { + let local_def_id = instantiation.def_id; let tcx = ctx.tcx; let drop_points = DropPoints::default(); let body = Cow::Borrowed(tcx.optimized_mir(local_def_id.to_def_id())); @@ -1733,8 +1726,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { Self { ctx, tcx, - local_def_id, - generic_args, + instantiation, drop_points, basic_block, body, diff --git a/src/analyze/local_def.rs b/src/analyze/local_def.rs index e5fd428d..1b322278 100644 --- a/src/analyze/local_def.rs +++ b/src/analyze/local_def.rs @@ -966,23 +966,15 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { inv.push_conj(one); } bty.set_precondition(inv); - self.ctx.register_basic_block_ty_with_precondition( - self.local_def_id, - self.generic_args, - bb, - bty, - ); + self.ctx + .register_basic_block_ty_with_precondition(self.instantiation(), bb, bty); } else if analyze::basic_block::needs_own_precondition(&self.body, bb) { let bty = self .type_builder .for_template(&mut self.ctx) .build_basic_block(&self.body, live_locals, ret_ty); - self.ctx.register_basic_block_ty_with_precondition( - self.local_def_id, - self.generic_args, - bb, - bty, - ); + self.ctx + .register_basic_block_ty_with_precondition(self.instantiation(), bb, bty); } else { // The block inherits its predecessor's outgoing env state as its // precondition, materialized lazily during the predecessor's @@ -991,8 +983,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { .type_builder .build_basic_block(&self.body, live_locals, ret_ty); self.ctx.register_basic_block_ty_without_precondition( - self.local_def_id, - self.generic_args, + self.instantiation(), bb, bty, ); @@ -1010,11 +1001,11 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { } let rty = self .ctx - .basic_block_ty_with_precondition(self.local_def_id, self.generic_args, bb) + .basic_block_ty_with_precondition(self.instantiation(), bb) .clone(); let drop_points = self.drop_points[&bb].clone(); self.ctx - .basic_block_analyzer(self.local_def_id, self.generic_args, bb) + .basic_block_analyzer(self.instantiation(), bb) .body(self.body.clone()) .drop_points(drop_points) .run(&rty, expected_fn_ty); @@ -1121,11 +1112,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { fn assert_entry(&mut self, expected: &rty::RefinedType) { let mut entry_ty = self .ctx - .basic_block_ty_with_precondition( - self.local_def_id, - self.generic_args, - mir::START_BLOCK, - ) + .basic_block_ty_with_precondition(self.instantiation(), mir::START_BLOCK) .clone(); tracing::debug!(expected = %expected.display(), entry = %entry_ty.display(), "assert_entry before"); let mut expected = expected.ty.as_function().cloned().unwrap(); @@ -1163,6 +1150,13 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { self.local_def_id } + fn instantiation(&self) -> analyze::LocalDefInstantiation<'tcx> { + analyze::LocalDefInstantiation { + def_id: self.local_def_id, + generic_args: self.generic_args, + } + } + pub fn generic_args(&mut self, generic_args: mir_ty::GenericArgsRef<'tcx>) -> &mut Self { self.generic_args = generic_args; self.body =