diff --git a/src/analyze.rs b/src/analyze.rs index 9b3967cf..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,7 +270,7 @@ pub struct Analyzer<'tcx> { /// Resulting CHC system. system: Rc>, - basic_blocks: HashMap>, + basic_blocks: HashMap, HashMap>, def_ids: did_cache::DefIdCache<'tcx>, enum_defs: Rc>, @@ -613,12 +622,12 @@ impl<'tcx> Analyzer<'tcx> { pub fn register_basic_block_ty_with_precondition( &mut self, - def_id: LocalDefId, + instantiation: LocalDefInstantiation<'tcx>, bb: BasicBlock, rty: BasicBlockType, ) { self.register_basic_block_def( - def_id, + instantiation, bb, BasicBlockDef { ty: rty, @@ -629,12 +638,12 @@ impl<'tcx> Analyzer<'tcx> { pub fn register_basic_block_ty_without_precondition( &mut self, - def_id: LocalDefId, + instantiation: LocalDefInstantiation<'tcx>, bb: BasicBlock, rty: BasicBlockType, ) { self.register_basic_block_def( - def_id, + instantiation, bb, BasicBlockDef { ty: rty, @@ -643,26 +652,34 @@ 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, + instantiation: LocalDefInstantiation<'tcx>, + bb: BasicBlock, + def: BasicBlockDef, + ) { tracing::debug!( - def_id = ?def_id, + ?instantiation, ?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(instantiation) + .or_default() + .insert(bb, def); } pub fn register_basic_block_precondition( &mut self, - def_id: LocalDefId, + instantiation: LocalDefInstantiation<'tcx>, bb: BasicBlock, precondition: rty::Refinement, ) { let bb_def = &mut self .basic_blocks - .get_mut(&def_id) + .get_mut(&instantiation) .unwrap() .get_mut(&bb) .unwrap(); @@ -674,16 +691,20 @@ 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, + instantiation: LocalDefInstantiation<'tcx>, + bb: BasicBlock, + ) -> &BasicBlockType { + &self.basic_blocks[&instantiation][&bb].ty } pub fn basic_block_ty_with_precondition( &self, - def_id: LocalDefId, + instantiation: LocalDefInstantiation<'tcx>, bb: BasicBlock, ) -> &BasicBlockType { - let def = &self.basic_blocks[&def_id][&bb]; + let def = &self.basic_blocks[&instantiation][&bb]; assert!( def.has_precondition, "basic block does not have precondition" @@ -723,10 +744,10 @@ impl<'tcx> Analyzer<'tcx> { pub fn basic_block_analyzer( &mut self, - local_def_id: LocalDefId, + instantiation: LocalDefInstantiation<'tcx>, bb: BasicBlock, ) -> basic_block::Analyzer<'tcx, '_> { - basic_block::Analyzer::new(self, local_def_id, 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 97cc7f89..2c9751fc 100644 --- a/src/analyze/basic_block.rs +++ b/src/analyze/basic_block.rs @@ -188,7 +188,7 @@ pub struct Analyzer<'tcx, 'ctx> { ctx: &'ctx mut analyze::Analyzer<'tcx>, tcx: TyCtxt<'tcx>, - local_def_id: LocalDefId, + instantiation: analyze::LocalDefInstantiation<'tcx>, drop_points: DropPoints, basic_block: BasicBlock, body: Cow<'tcx, Body<'tcx>>, @@ -223,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, bb) + .basic_block_ty_with_precondition(self.instantiation, bb) } fn bind_local(&mut self, local: Local, rty: rty::RefinedType) { @@ -927,7 +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, 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() { @@ -951,7 +951,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { let precondition = capture.finish(&self.env); self.ctx - .register_basic_block_precondition(self.local_def_id, bb, precondition); + .register_basic_block_precondition(self.instantiation, bb, precondition); } fn with_assumptions(&mut self, assumptions: Vec>, callback: F) -> T @@ -1712,9 +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, + 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())); @@ -1725,7 +1726,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { Self { ctx, tcx, - local_def_id, + instantiation, drop_points, basic_block, body, diff --git a/src/analyze/local_def.rs b/src/analyze/local_def.rs index 6a9cdf1b..1b322278 100644 --- a/src/analyze/local_def.rs +++ b/src/analyze/local_def.rs @@ -967,14 +967,14 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { } bty.set_precondition(inv); self.ctx - .register_basic_block_ty_with_precondition(self.local_def_id, bb, bty); + .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, bb, bty); + .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 @@ -982,8 +982,11 @@ 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.instantiation(), + bb, + bty, + ); }; } } @@ -998,11 +1001,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.instantiation(), bb) .clone(); let drop_points = self.drop_points[&bb].clone(); self.ctx - .basic_block_analyzer(self.local_def_id, bb) + .basic_block_analyzer(self.instantiation(), bb) .body(self.body.clone()) .drop_points(drop_points) .run(&rty, expected_fn_ty); @@ -1109,7 +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, 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(); @@ -1147,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 = 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); +}