Make minor modifications

6 files changed, 53 insertions, 20 deletions

diff --git a/compiler/Driver.ml b/compiler/Driver.ml
index 128ae890..aa293469 100644
--- a/compiler/Driver.ml
+++ b/compiler/Driver.ml
@@ -23,6 +23,7 @@ let _ =
   Easy_logging.Handlers.set_level main_logger_handler EL.Debug;
   main_log#set_level EL.Info;
   llbc_of_json_logger#set_level EL.Info;
+  regions_hierarchy_log#set_level EL.Info;
   pre_passes_log#set_level EL.Info;
   associated_types_log#set_level EL.Info;
   contexts_log#set_level EL.Info;
diff --git a/compiler/Interpreter.ml b/compiler/Interpreter.ml
index 69c9af62..b94825cc 100644
--- a/compiler/Interpreter.ml
+++ b/compiler/Interpreter.ml
@@ -65,7 +65,8 @@ let normalize_inst_fun_sig (ctx : C.eval_ctx) (sg : A.inst_fun_sig) :
     normalize because a trait clause was instantiated with a specific trait ref).
  *)
 let symbolic_instantiate_fun_sig (ctx : C.eval_ctx) (sg : A.fun_sig)
-    (kind : A.fun_kind) : C.eval_ctx * A.inst_fun_sig =
+    (regions_hierarchy : T.region_groups) (kind : A.fun_kind) :
+    C.eval_ctx * A.inst_fun_sig =
   let tr_self =
     match kind with
     | RegularKind | TraitMethodImpl _ -> T.UnknownTrait __FUNCTION__
@@ -147,7 +148,7 @@ let symbolic_instantiate_fun_sig (ctx : C.eval_ctx) (sg : A.fun_sig)
     in
     { T.regions; types; const_generics; trait_refs }
   in
-  let inst_sg = instantiate_fun_sig ctx generics tr_self sg in
+  let inst_sg = instantiate_fun_sig ctx generics tr_self sg regions_hierarchy in
   (* Compute the normalization maps *)
   let ctx =
     AssociatedTypes.ctx_add_norm_trait_types_from_preds ctx
@@ -200,7 +201,7 @@ let initialize_symbolic_context_for_fun (ctx : C.decls_ctx) (fdef : A.fun_decl)
      at the same time the normalization map for the associated types.
   *)
   let ctx, inst_sg =
-    symbolic_instantiate_fun_sig ctx fdef.signature fdef.kind
+    symbolic_instantiate_fun_sig ctx fdef.signature regions_hierarchy fdef.kind
   in
   (* Create fresh symbolic values for the inputs *)
   let input_svs =
@@ -275,8 +276,11 @@ let evaluate_function_symbolic_synthesize_backward_from_return
    * the return type. Note that it is important to re-generate
    * an instantiation of the signature, so that we use fresh
    * region ids for the return abstractions. *)
+  let regions_hierarchy =
+    FunIdMap.find (FRegular fdef.def_id) ctx.fun_context.regions_hierarchies
+  in
   let _, ret_inst_sg =
-    symbolic_instantiate_fun_sig ctx fdef.signature fdef.kind
+    symbolic_instantiate_fun_sig ctx fdef.signature regions_hierarchy fdef.kind
   in
   let ret_rty = ret_inst_sg.output in
   (* Move the return value out of the return variable *)
@@ -287,9 +291,6 @@ let evaluate_function_symbolic_synthesize_backward_from_return
    * will end - this will allow us to, first, mark the other return
    * regions as non-endable, and, second, end those parent regions in
    * proper order. *)
-  let regions_hierarchy =
-    FunIdMap.find (FRegular fdef.def_id) ctx.fun_context.regions_hierarchies
-  in
   let parent_rgs = list_ancestor_region_groups regions_hierarchy back_id in
   let parent_input_abs_ids =
     T.RegionGroupId.mapi
diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml
index 3627490d..b78c2691 100644
--- a/compiler/InterpreterStatements.ml
+++ b/compiler/InterpreterStatements.ml
@@ -1114,8 +1114,13 @@ and eval_transparent_function_call_symbolic (config : C.config) (call : A.call)
             ^ "\n- def.signature:\n"
             ^ fun_sig_to_string ctx def.A.signature));
         let tr_self = T.UnknownTrait __FUNCTION__ in
+        let regions_hierarchy =
+          LlbcAstUtils.FunIdMap.find (FRegular fid)
+            ctx.fun_context.regions_hierarchies
+        in
         let inst_sg =
           instantiate_fun_sig ctx call.func.generics tr_self def.A.signature
+            regions_hierarchy
         in
         (call.func.func, call.func.generics, def, inst_sg)
     | FunId (FAssumed _) ->
@@ -1154,9 +1159,14 @@ and eval_transparent_function_call_symbolic (config : C.config) (call : A.call)
                 let method_def = C.ctx_lookup_fun_decl ctx id in
                 (* Instantiate *)
                 let tr_self = T.TraitRef trait_ref in
+                let fid : A.fun_id = FRegular id in
+                let regions_hierarchy =
+                  LlbcAstUtils.FunIdMap.find fid
+                    ctx.fun_context.regions_hierarchies
+                in
                 let inst_sg =
                   instantiate_fun_sig ctx generics tr_self
-                    method_def.A.signature
+                    method_def.A.signature regions_hierarchy
                 in
                 (* Also update the function identifier: we want to forget
                    the fact that we called a trait method, and treat it as
@@ -1164,7 +1174,7 @@ and eval_transparent_function_call_symbolic (config : C.config) (call : A.call)
                    which implements the method. In order to do this properly,
                    we also need to update the generics.
                 *)
-                let func = E.FunId (FRegular id) in
+                let func = E.FunId fid in
                 (func, generics, method_def, inst_sg)
             | None ->
                 (* If not found, lookup the methods provided by the trait *declaration*
@@ -1210,10 +1220,14 @@ and eval_transparent_function_call_symbolic (config : C.config) (call : A.call)
                     ^ "\n- parent params info: "
                     ^ Print.option_to_string A.show_params_info
                         method_def.signature.parent_params_info));
+                let regions_hierarchy =
+                  LlbcAstUtils.FunIdMap.find (FRegular method_id)
+                    ctx.fun_context.regions_hierarchies
+                in
                 let tr_self = T.TraitRef trait_ref in
                 let inst_sg =
                   instantiate_fun_sig ctx all_generics tr_self
-                    method_def.A.signature
+                    method_def.A.signature regions_hierarchy
                 in
                 (call.func.func, call.func.generics, method_def, inst_sg))
         | _ ->
@@ -1236,9 +1250,14 @@ and eval_transparent_function_call_symbolic (config : C.config) (call : A.call)
             let method_def = C.ctx_lookup_fun_decl ctx method_id in
             log#ldebug (lazy ("method:\n" ^ fun_decl_to_string ctx method_def));
             (* Instantiate *)
+            let regions_hierarchy =
+              LlbcAstUtils.FunIdMap.find (FRegular method_id)
+                ctx.fun_context.regions_hierarchies
+            in
             let tr_self = T.TraitRef trait_ref in
             let inst_sg =
               instantiate_fun_sig ctx generics tr_self method_def.A.signature
+                regions_hierarchy
             in
             (call.func.func, call.func.generics, method_def, inst_sg))
   in
@@ -1437,10 +1456,15 @@ and eval_assumed_function_call_symbolic (config : C.config)
             (* Should have been treated above *)
             raise (Failure "Unreachable")
         | _ ->
+            let regions_hierarchy =
+              LlbcAstUtils.FunIdMap.find (FAssumed fid)
+                ctx.fun_context.regions_hierarchies
+            in
             (* There shouldn't be any reference to Self *)
             let tr_self = T.UnknownTrait __FUNCTION__ in
             instantiate_fun_sig ctx generics tr_self
               (Assumed.get_assumed_fun_sig fid)
+              regions_hierarchy
       in
 
       (* Evaluate the function call *)
diff --git a/compiler/InterpreterUtils.ml b/compiler/InterpreterUtils.ml
index 5e2746c5..e5a5b2ea 100644
--- a/compiler/InterpreterUtils.ml
+++ b/compiler/InterpreterUtils.ml
@@ -463,7 +463,8 @@ let initialize_eval_context (ctx : C.decls_ctx)
     evaluating in symbolic mode).
  *)
 let instantiate_fun_sig (ctx : C.eval_ctx) (generics : T.generic_args)
-    (tr_self : T.trait_instance_id) (sg : A.fun_sig) : A.inst_fun_sig =
+    (tr_self : T.trait_instance_id) (sg : A.fun_sig)
+    (regions_hierarchy : T.region_groups) : A.inst_fun_sig =
   log#ldebug
     (lazy
       ("instantiate_fun_sig:" ^ "\n- generics: "
@@ -474,11 +475,6 @@ let instantiate_fun_sig (ctx : C.eval_ctx) (generics : T.generic_args)
   (* Erase the regions in the generics we use for the instantiation *)
   let generics = Subst.generic_args_erase_regions generics in
   let tr_self = Subst.trait_instance_id_erase_regions tr_self in
-  (* Compute the regions hierarchy *)
-  let regions_hierarchy =
-    RegionsHierarchy.compute_regions_hierarchy_for_sig
-      ctx.type_context.type_decls sg
-  in
   (* Generate fresh abstraction ids and create a substitution from region
    * group ids to abstraction ids *)
   let rg_abs_ids_bindings =
diff --git a/compiler/Logging.ml b/compiler/Logging.ml
index 721655b8..f4ad87a9 100644
--- a/compiler/Logging.ml
+++ b/compiler/Logging.ml
@@ -6,6 +6,9 @@ include Charon.Logging
 (** Logger for PrePasses *)
 let pre_passes_log = L.get_logger "MainLogger.PrePasses"
 
+(** Logger for RegionsHierarchy *)
+let regions_hierarchy_log = L.get_logger "MainLogger.RegionsHierarchy"
+
 (** Logger for Translate *)
 let translate_log = L.get_logger "MainLogger.Translate"
 
diff --git a/compiler/RegionsHierarchy.ml b/compiler/RegionsHierarchy.ml
index dd566426..ce5880bf 100644
--- a/compiler/RegionsHierarchy.ml
+++ b/compiler/RegionsHierarchy.ml
@@ -25,6 +25,7 @@
     be grouped together).
  *)
 
+open Names
 open Types
 open TypesUtils
 open Expressions
@@ -34,8 +35,12 @@ open Assumed
 open SCC
 module Subst = Substitute
 
+(** The local logger *)
+let log = Logging.regions_hierarchy_log
+
 let compute_regions_hierarchy_for_sig (type_decls : type_decl TypeDeclId.Map.t)
-    (sg : fun_sig) : region_groups =
+    (fun_name : name) (sg : fun_sig) : region_groups =
+  log#ldebug (lazy (__FUNCTION__ ^ ": " ^ name_to_string fun_name));
   (* Create the dependency graph.
 
      An edge from 'short to 'long means that 'long outlives 'short (that is
@@ -229,15 +234,18 @@ let compute_regions_hierarchies (type_decls : type_decl TypeDeclId.Map.t)
     (fun_decls : fun_decl FunDeclId.Map.t) : region_groups FunIdMap.t =
   let regular =
     List.map
-      (fun (fid, d) -> (FRegular fid, d.signature))
+      (fun ((fid, d) : FunDeclId.id * fun_decl) ->
+        (FRegular fid, (d.name, d.signature)))
       (FunDeclId.Map.bindings fun_decls)
   in
   let assumed =
     List.map
-      (fun (info : assumed_fun_info) -> (FAssumed info.fun_id, info.fun_sig))
+      (fun (info : assumed_fun_info) ->
+        (FAssumed info.fun_id, (info.name, info.fun_sig)))
       assumed_fun_infos
   in
   FunIdMap.of_list
     (List.map
-       (fun (fid, sg) -> (fid, compute_regions_hierarchy_for_sig type_decls sg))
+       (fun (fid, (name, sg)) ->
+         (fid, compute_regions_hierarchy_for_sig type_decls name sg))
        (regular @ assumed))