change: store the def_id of the corresponding function in TypeBuilder

Author: coeff-aij

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(),
         )

src/analyze/basic_block.rs

@@ -1166,14 +1166,15 @@ 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();
         let body = Cow::Borrowed(tcx.optimized_mir(local_def_id.to_def_id()));
         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,

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(&param.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()
                     }

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);

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<RefCell<TypeParamMap>>,
     system: Rc<RefCell<chc::System>>,
@@ -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<RefCell<TypeParamMap>>,
         system: Rc<RefCell<chc::System>>,
     ) -> 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,16 +102,29 @@ impl<'tcx> TypeBuilder<'tcx> {
     fn translate_param_type(&self, ty: &mir_ty::ParamTy) -> rty::Type<rty::Closed> {
         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()
     }
 
     fn translate_alias_type(&self, ty: &mir_ty::AliasTy) -> rty::Type<rty::Closed> {
         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()
     }