diff options
Diffstat (limited to 'compiler')
| -rw-r--r-- | compiler/Driver.ml | 1 | ||||
| -rw-r--r-- | compiler/Interpreter.ml | 15 | ||||
| -rw-r--r-- | compiler/InterpreterStatements.ml | 30 | ||||
| -rw-r--r-- | compiler/InterpreterUtils.ml | 8 | ||||
| -rw-r--r-- | compiler/Logging.ml | 3 | ||||
| -rw-r--r-- | compiler/RegionsHierarchy.ml | 16 |
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)) |