Key basic block types by generic args as well as def id

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<RefCell<chc::System>>,
 
-    basic_blocks: HashMap<LocalDefId, HashMap<BasicBlock, BasicBlockDef>>,
+    basic_blocks: HashMap<LocalDefInstantiation<'tcx>, HashMap<BasicBlock, BasicBlockDef>>,
     def_ids: did_cache::DefIdCache<'tcx>,
 
     enum_defs: Rc<RefCell<EnumDefs>>,
@@ -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<rty::FunctionParamIdx>,
     ) {
         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) {

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<Var>) {
@@ -927,7 +927,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
         bb: BasicBlock,
         outer_fn_param_vars: &HashMap<rty::FunctionParamIdx, Var>,
     ) {
-        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<F, T>(&mut self, assumptions: Vec<impl Into<Assumption>>, 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,

src/analyze/local_def.rs

@@ -967,23 +967,26 @@ 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
                 // analysis. Record only unrefined type here.
                 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 =

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: K + Copy>(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);
+}

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: K + Copy>(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);
+}