diff options
-rw-r--r-- | compiler/AssociatedTypes.ml | 10 | ||||
-rw-r--r-- | compiler/Contexts.ml | 42 | ||||
-rw-r--r-- | compiler/Interpreter.ml | 8 | ||||
-rw-r--r-- | compiler/InterpreterBorrows.ml | 12 | ||||
-rw-r--r-- | compiler/InterpreterExpansion.ml | 2 | ||||
-rw-r--r-- | compiler/InterpreterExpressions.ml | 5 | ||||
-rw-r--r-- | compiler/InterpreterLoopsFixedPoint.ml | 18 | ||||
-rw-r--r-- | compiler/InterpreterLoopsJoinCtxs.ml | 36 | ||||
-rw-r--r-- | compiler/InterpreterLoopsMatchCtxs.ml | 4 | ||||
-rw-r--r-- | compiler/InterpreterStatements.ml | 12 | ||||
-rw-r--r-- | compiler/InterpreterUtils.ml | 26 | ||||
-rw-r--r-- | compiler/Invariants.ml | 2 | ||||
-rw-r--r-- | compiler/Print.ml | 10 | ||||
-rw-r--r-- | compiler/SymbolicToPure.ml | 78 | ||||
-rw-r--r-- | compiler/Translate.ml | 14 |
15 files changed, 139 insertions, 140 deletions
diff --git a/compiler/AssociatedTypes.ml b/compiler/AssociatedTypes.ml index e2f687e8..054c8169 100644 --- a/compiler/AssociatedTypes.ml +++ b/compiler/AssociatedTypes.ml @@ -493,11 +493,11 @@ let norm_ctx_normalize_trait_type_constraint (ctx : norm_ctx) let mk_norm_ctx (ctx : eval_ctx) : norm_ctx = { norm_trait_types = ctx.norm_trait_types; - type_decls = ctx.type_context.type_decls; - fun_decls = ctx.fun_context.fun_decls; - global_decls = ctx.global_context.global_decls; - trait_decls = ctx.trait_decls_context.trait_decls; - trait_impls = ctx.trait_impls_context.trait_impls; + type_decls = ctx.type_ctx.type_decls; + fun_decls = ctx.fun_ctx.fun_decls; + global_decls = ctx.global_ctx.global_decls; + trait_decls = ctx.trait_decls_ctx.trait_decls; + trait_impls = ctx.trait_impls_ctx.trait_impls; type_vars = ctx.type_vars; const_generic_vars = ctx.const_generic_vars; } diff --git a/compiler/Contexts.ml b/compiler/Contexts.ml index a30ed0f1..5d646a61 100644 --- a/compiler/Contexts.ml +++ b/compiler/Contexts.ml @@ -180,35 +180,35 @@ type config = { let mk_config (mode : interpreter_mode) : config = { mode } -type type_context = { +type type_ctx = { type_decls_groups : type_declaration_group TypeDeclId.Map.t; type_decls : type_decl TypeDeclId.Map.t; type_infos : TypesAnalysis.type_infos; } [@@deriving show] -type fun_context = { +type fun_ctx = { fun_decls : fun_decl FunDeclId.Map.t; fun_infos : FunsAnalysis.fun_info FunDeclId.Map.t; regions_hierarchies : region_var_groups FunIdMap.t; } [@@deriving show] -type global_context = { global_decls : global_decl GlobalDeclId.Map.t } +type global_ctx = { global_decls : global_decl GlobalDeclId.Map.t } [@@deriving show] -type trait_decls_context = { trait_decls : trait_decl TraitDeclId.Map.t } +type trait_decls_ctx = { trait_decls : trait_decl TraitDeclId.Map.t } [@@deriving show] -type trait_impls_context = { trait_impls : trait_impl TraitImplId.Map.t } +type trait_impls_ctx = { trait_impls : trait_impl TraitImplId.Map.t } [@@deriving show] type decls_ctx = { - type_ctx : type_context; - fun_ctx : fun_context; - global_ctx : global_context; - trait_decls_ctx : trait_decls_context; - trait_impls_ctx : trait_impls_context; + type_ctx : type_ctx; + fun_ctx : fun_ctx; + global_ctx : global_ctx; + trait_decls_ctx : trait_decls_ctx; + trait_impls_ctx : trait_impls_ctx; } [@@deriving show] @@ -230,11 +230,11 @@ module TraitTypeRefMap = Collections.MakeMap (TraitTypeRefOrd) (** Evaluation context *) type eval_ctx = { - type_context : type_context; - fun_context : fun_context; - global_context : global_context; - trait_decls_context : trait_decls_context; - trait_impls_context : trait_impls_context; + type_ctx : type_ctx; + fun_ctx : fun_ctx; + global_ctx : global_ctx; + trait_decls_ctx : trait_decls_ctx; + trait_impls_ctx : trait_impls_ctx; region_groups : RegionGroupId.id list; type_vars : type_var list; const_generic_vars : const_generic_var list; @@ -290,20 +290,20 @@ let ctx_lookup_var_binder (ctx : eval_ctx) (vid : VarId.id) : var_binder = fst (env_lookup_var ctx.env vid) let ctx_lookup_type_decl (ctx : eval_ctx) (tid : TypeDeclId.id) : type_decl = - TypeDeclId.Map.find tid ctx.type_context.type_decls + TypeDeclId.Map.find tid ctx.type_ctx.type_decls let ctx_lookup_fun_decl (ctx : eval_ctx) (fid : FunDeclId.id) : fun_decl = - FunDeclId.Map.find fid ctx.fun_context.fun_decls + FunDeclId.Map.find fid ctx.fun_ctx.fun_decls let ctx_lookup_global_decl (ctx : eval_ctx) (gid : GlobalDeclId.id) : global_decl = - GlobalDeclId.Map.find gid ctx.global_context.global_decls + GlobalDeclId.Map.find gid ctx.global_ctx.global_decls let ctx_lookup_trait_decl (ctx : eval_ctx) (id : TraitDeclId.id) : trait_decl = - TraitDeclId.Map.find id ctx.trait_decls_context.trait_decls + TraitDeclId.Map.find id ctx.trait_decls_ctx.trait_decls let ctx_lookup_trait_impl (ctx : eval_ctx) (id : TraitImplId.id) : trait_impl = - TraitImplId.Map.find id ctx.trait_impls_context.trait_impls + TraitImplId.Map.find id ctx.trait_impls_ctx.trait_impls (** Retrieve a variable's value in the current frame *) let env_lookup_var_value (env : env) (vid : VarId.id) : typed_value = @@ -528,7 +528,7 @@ let ctx_set_abs_can_end (ctx : eval_ctx) (abs_id : AbstractionId.id) fst (ctx_subst_abs ctx abs_id abs) let ctx_type_decl_is_rec (ctx : eval_ctx) (id : TypeDeclId.id) : bool = - let decl_group = TypeDeclId.Map.find id ctx.type_context.type_decls_groups in + let decl_group = TypeDeclId.Map.find id ctx.type_ctx.type_decls_groups in match decl_group with RecGroup _ -> true | NonRecGroup _ -> false (** Visitor to iterate over the values in the *current* frame *) diff --git a/compiler/Interpreter.ml b/compiler/Interpreter.ml index 76432faa..22d176c9 100644 --- a/compiler/Interpreter.ml +++ b/compiler/Interpreter.ml @@ -195,7 +195,7 @@ let initialize_symbolic_context_for_fun (ctx : decls_ctx) (fdef : fun_decl) : List.map (fun (g : region_var_group) -> g.id) regions_hierarchy in let ctx = - initialize_eval_context ctx region_groups sg.generics.types + initialize_eval_ctx ctx region_groups sg.generics.types sg.generics.const_generics in (* Instantiate the signature. This updates the context because we compute @@ -277,7 +277,7 @@ let evaluate_function_symbolic_synthesize_backward_from_return (config : config) * 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 + FunIdMap.find (FRegular fdef.def_id) ctx.fun_ctx.regions_hierarchies in let _, ret_inst_sg = symbolic_instantiate_fun_sig ctx fdef.signature regions_hierarchy fdef.kind @@ -466,7 +466,7 @@ let evaluate_function_symbolic (synthesize : bool) (ctx : decls_ctx) let ctx, input_svs, inst_sg = initialize_symbolic_context_for_fun ctx fdef in let regions_hierarchy = - FunIdMap.find (FRegular fdef.def_id) ctx.fun_context.regions_hierarchies + FunIdMap.find (FRegular fdef.def_id) ctx.fun_ctx.regions_hierarchies in (* Create the continuation to finish the evaluation *) @@ -615,7 +615,7 @@ module Test = struct assert (body.arg_count = 0); (* Create the evaluation context *) - let ctx = initialize_eval_context decls_ctx [] [] [] in + let ctx = initialize_eval_ctx decls_ctx [] [] [] in (* Insert the (uninitialized) local variables *) let ctx = ctx_push_uninitialized_vars ctx body.locals in diff --git a/compiler/InterpreterBorrows.ml b/compiler/InterpreterBorrows.ml index e56919fa..a2eb2545 100644 --- a/compiler/InterpreterBorrows.ml +++ b/compiler/InterpreterBorrows.ml @@ -1628,7 +1628,7 @@ let destructure_abs (abs_kind : abs_kind) (can_end : bool) push { value; ty } | AIgnoredMutLoan (opt_bid, child_av) -> (* We don't support nested borrows for now *) - assert (not (ty_has_borrows ctx.type_context.type_infos child_av.ty)); + assert (not (ty_has_borrows ctx.type_ctx.type_infos child_av.ty)); assert (opt_bid = None); (* Simply explore the child *) list_avalues false push_fail child_av @@ -1639,7 +1639,7 @@ let destructure_abs (abs_kind : abs_kind) (can_end : bool) { child = child_av; given_back = _; given_back_meta = _ } | AIgnoredSharedLoan child_av -> (* We don't support nested borrows for now *) - assert (not (ty_has_borrows ctx.type_context.type_infos child_av.ty)); + assert (not (ty_has_borrows ctx.type_ctx.type_infos child_av.ty)); (* Simply explore the child *) list_avalues false push_fail child_av) | ABorrow bc -> ( @@ -1659,14 +1659,14 @@ let destructure_abs (abs_kind : abs_kind) (can_end : bool) push av | AIgnoredMutBorrow (opt_bid, child_av) -> (* We don't support nested borrows for now *) - assert (not (ty_has_borrows ctx.type_context.type_infos child_av.ty)); + assert (not (ty_has_borrows ctx.type_ctx.type_infos child_av.ty)); assert (opt_bid = None); (* Just explore the child *) list_avalues false push_fail child_av | AEndedIgnoredMutBorrow { child = child_av; given_back = _; given_back_meta = _ } -> (* We don't support nested borrows for now *) - assert (not (ty_has_borrows ctx.type_context.type_infos child_av.ty)); + assert (not (ty_has_borrows ctx.type_ctx.type_infos child_av.ty)); (* Just explore the child *) list_avalues false push_fail child_av | AProjSharedBorrow asb -> @@ -1683,7 +1683,7 @@ let destructure_abs (abs_kind : abs_kind) (can_end : bool) | ASymbolic _ -> (* For now, we fore all symbolic values containing borrows to be eagerly expanded *) - assert (not (ty_has_borrows ctx.type_context.type_infos ty)) + assert (not (ty_has_borrows ctx.type_ctx.type_infos ty)) and list_values (v : typed_value) : typed_avalue list * typed_value = let ty = v.ty in match v.value with @@ -1732,7 +1732,7 @@ let destructure_abs (abs_kind : abs_kind) (can_end : bool) | VSymbolic _ -> (* For now, we fore all symbolic values containing borrows to be eagerly expanded *) - assert (not (ty_has_borrows ctx.type_context.type_infos ty)); + assert (not (ty_has_borrows ctx.type_ctx.type_infos ty)); ([], v) in diff --git a/compiler/InterpreterExpansion.ml b/compiler/InterpreterExpansion.ml index bbf4d9d5..e489ddc3 100644 --- a/compiler/InterpreterExpansion.ml +++ b/compiler/InterpreterExpansion.ml @@ -627,7 +627,7 @@ let greedy_expand_symbolics_with_borrows (config : config) : cm_fun = inherit [_] iter_eval_ctx method! visit_VSymbolic _ sv = - if ty_has_borrows ctx.type_context.type_infos sv.sv_ty then + if ty_has_borrows ctx.type_ctx.type_infos sv.sv_ty then raise (FoundSymbolicValue sv) else () diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml index 1b5b79dd..8536b4ab 100644 --- a/compiler/InterpreterExpressions.ml +++ b/compiler/InterpreterExpressions.ml @@ -32,8 +32,7 @@ let expand_primitively_copyable_at_place (config : config) fun cf ctx -> let v = read_place access p ctx in match - find_first_primitively_copyable_sv_with_borrows - ctx.type_context.type_infos v + find_first_primitively_copyable_sv_with_borrows ctx.type_ctx.type_infos v with | None -> cf ctx | Some sv -> @@ -351,7 +350,7 @@ let eval_operand_no_reorganize (config : config) (op : operand) assert ( Option.is_none (find_first_primitively_copyable_sv_with_borrows - ctx.type_context.type_infos v)); + ctx.type_ctx.type_infos v)); (* Actually perform the copy *) let allow_adt_copy = false in let ctx, v = copy_value allow_adt_copy config ctx v in diff --git a/compiler/InterpreterLoopsFixedPoint.ml b/compiler/InterpreterLoopsFixedPoint.ml index c4e180fa..4dabe974 100644 --- a/compiler/InterpreterLoopsFixedPoint.ml +++ b/compiler/InterpreterLoopsFixedPoint.ml @@ -300,7 +300,7 @@ let prepare_ashared_loans (loop_id : LoopId.id option) : cm_fun = let env = List.append fresh_absl env in let ctx = { ctx with env } in - let _, new_ctx_ids_map = compute_context_ids ctx in + let _, new_ctx_ids_map = compute_ctx_ids ctx in (* Synthesize *) match cf ctx with @@ -385,8 +385,8 @@ let compute_loop_entry_fixed_point (config : config) (loop_id : LoopId.id) match !fixed_ids with | Some _ -> ctx1 | None -> - let old_ids, _ = compute_context_ids ctx1 in - let new_ids, _ = compute_contexts_ids !ctxs in + let old_ids, _ = compute_ctx_ids ctx1 in + let new_ids, _ = compute_ctxs_ids !ctxs in let blids = BorrowId.Set.diff old_ids.blids new_ids.blids in let aids = AbstractionId.Set.diff old_ids.aids new_ids.aids in (* End those borrows and abstractions *) @@ -409,7 +409,7 @@ let compute_loop_entry_fixed_point (config : config) (loop_id : LoopId.id) ctxs := List.map (end_borrows_abs blids aids) !ctxs; (* Note that the fixed ids are given by the original context, from *before* we introduce fresh abstractions/reborrows for the shared values *) - fixed_ids := Some (fst (compute_context_ids ctx0)); + fixed_ids := Some (fst (compute_ctx_ids ctx0)); ctx1 in @@ -424,12 +424,12 @@ let compute_loop_entry_fixed_point (config : config) (loop_id : LoopId.id) intersection of ids between the original environment and the list of new environments *) let compute_fixed_ids (ctxl : eval_ctx list) : ids_sets = - let fixed_ids, _ = compute_context_ids ctx0 in + let fixed_ids, _ = compute_ctx_ids ctx0 in let { aids; blids; borrow_ids; loan_ids; dids; rids; sids } = fixed_ids in let sids = ref sids in List.iter (fun ctx -> - let fixed_ids, _ = compute_context_ids ctx in + let fixed_ids, _ = compute_ctx_ids ctx in sids := SymbolicValueId.Set.inter !sids fixed_ids.sids) ctxl; let sids = !sids in @@ -568,7 +568,7 @@ let compute_loop_entry_fixed_point (config : config) (loop_id : LoopId.id) InterpreterBorrows.end_abstraction_no_synth config abs_id ctx in (* Explore the context, and check which abstractions are not there anymore *) - let ids, _ = compute_context_ids ctx in + let ids, _ = compute_ctx_ids ctx in let ended_ids = AbstractionId.Set.diff !fp_aids ids.aids in add_ended_aids rg_id ended_ids) ctx.region_groups @@ -840,8 +840,8 @@ let compute_fixed_point_id_correspondance (fixed_ids : ids_sets) let compute_fp_ctx_symbolic_values (ctx : eval_ctx) (fp_ctx : eval_ctx) : SymbolicValueId.Set.t * symbolic_value list = - let old_ids, _ = compute_context_ids ctx in - let fp_ids, fp_ids_maps = compute_context_ids fp_ctx in + let old_ids, _ = compute_ctx_ids ctx in + let fp_ids, fp_ids_maps = compute_ctx_ids fp_ctx in let fresh_sids = SymbolicValueId.Set.diff fp_ids.sids old_ids.sids in (* Compute the set of symbolic values which appear in shared values inside diff --git a/compiler/InterpreterLoopsJoinCtxs.ml b/compiler/InterpreterLoopsJoinCtxs.ml index 8d485483..445e5abf 100644 --- a/compiler/InterpreterLoopsJoinCtxs.ml +++ b/compiler/InterpreterLoopsJoinCtxs.ml @@ -326,8 +326,8 @@ let mk_collapse_ctx_merge_duplicate_funs (loop_id : LoopId.id) (ctx : eval_ctx) let _ = let _, ty0, _ = ty_as_ref ty0 in let _, ty1, _ = ty_as_ref ty1 in - assert (not (ty_has_borrows ctx.type_context.type_infos ty0)); - assert (not (ty_has_borrows ctx.type_context.type_infos ty1)) + assert (not (ty_has_borrows ctx.type_ctx.type_infos ty0)); + assert (not (ty_has_borrows ctx.type_ctx.type_infos ty1)) in (* Same remarks as for [merge_amut_borrows] *) @@ -543,11 +543,11 @@ let join_ctxs (loop_id : LoopId.id) (fixed_ids : ids_sets) (ctx0 : eval_ctx) (* Construct the joined context - of course, the type, fun, etc. contexts * should be the same in the two contexts *) let { - type_context; - fun_context; - global_context; - trait_decls_context; - trait_impls_context; + type_ctx; + fun_ctx; + global_ctx; + trait_decls_ctx; + trait_impls_ctx; region_groups; type_vars; const_generic_vars; @@ -559,11 +559,11 @@ let join_ctxs (loop_id : LoopId.id) (fixed_ids : ids_sets) (ctx0 : eval_ctx) ctx0 in let { - type_context = _; - fun_context = _; - global_context = _; - trait_decls_context = _; - trait_impls_context = _; + type_ctx = _; + fun_ctx = _; + global_ctx = _; + trait_decls_ctx = _; + trait_impls_ctx = _; region_groups = _; type_vars = _; const_generic_vars = _; @@ -577,11 +577,11 @@ let join_ctxs (loop_id : LoopId.id) (fixed_ids : ids_sets) (ctx0 : eval_ctx) let ended_regions = RegionId.Set.union ended_regions0 ended_regions1 in Ok { - type_context; - fun_context; - global_context; - trait_decls_context; - trait_impls_context; + type_ctx; + fun_ctx; + global_ctx; + trait_decls_ctx; + trait_impls_ctx; region_groups; type_vars; const_generic_vars; @@ -621,7 +621,7 @@ let destructure_new_abs (loop_id : LoopId.id) contexts we join don't have non-fixed abstractions with the same ids. *) let refresh_abs (old_abs : AbstractionId.Set.t) (ctx : eval_ctx) : eval_ctx = - let ids, _ = compute_context_ids ctx in + let ids, _ = compute_ctx_ids ctx in let abs_to_refresh = AbstractionId.Set.diff ids.aids old_abs in let aids_subst = List.map diff --git a/compiler/InterpreterLoopsMatchCtxs.ml b/compiler/InterpreterLoopsMatchCtxs.ml index 90559c29..2a688fa7 100644 --- a/compiler/InterpreterLoopsMatchCtxs.ml +++ b/compiler/InterpreterLoopsMatchCtxs.ml @@ -658,7 +658,7 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct else ( (* The caller should have checked that the symbolic values don't contain borrows *) - assert (not (ty_has_borrows S.ctx.type_context.type_infos sv0.sv_ty)); + assert (not (ty_has_borrows S.ctx.type_ctx.type_infos sv0.sv_ty)); (* We simply introduce a fresh symbolic value *) mk_fresh_symbolic_value sv0.sv_ty) @@ -669,7 +669,7 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct - there are no borrows in the "regular" value If there are loans in the regular value, raise an exception. *) - assert (not (ty_has_borrows S.ctx.type_context.type_infos sv.sv_ty)); + assert (not (ty_has_borrows S.ctx.type_ctx.type_infos sv.sv_ty)); assert (not (value_has_borrows S.ctx v.value)); let value_is_left = not left in (match InterpreterBorrowsCore.get_first_loan_in_value v with diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml index 30b7b333..da617c64 100644 --- a/compiler/InterpreterStatements.ml +++ b/compiler/InterpreterStatements.ml @@ -747,7 +747,7 @@ let eval_transparent_function_call_symbolic_inst (call : call) (ctx : eval_ctx) let tr_self = UnknownTrait __FUNCTION__ in let regions_hierarchy = LlbcAstUtils.FunIdMap.find (FRegular fid) - ctx.fun_context.regions_hierarchies + ctx.fun_ctx.regions_hierarchies in let inst_sg = instantiate_fun_sig ctx func.generics tr_self def.signature @@ -793,7 +793,7 @@ let eval_transparent_function_call_symbolic_inst (call : call) (ctx : eval_ctx) let fid : fun_id = FRegular id in let regions_hierarchy = LlbcAstUtils.FunIdMap.find fid - ctx.fun_context.regions_hierarchies + ctx.fun_ctx.regions_hierarchies in let inst_sg = instantiate_fun_sig ctx generics tr_self @@ -853,7 +853,7 @@ let eval_transparent_function_call_symbolic_inst (call : call) (ctx : eval_ctx) method_def.signature.parent_params_info)); let regions_hierarchy = LlbcAstUtils.FunIdMap.find (FRegular method_id) - ctx.fun_context.regions_hierarchies + ctx.fun_ctx.regions_hierarchies in let tr_self = TraitRef trait_ref in let inst_sg = @@ -884,7 +884,7 @@ let eval_transparent_function_call_symbolic_inst (call : call) (ctx : eval_ctx) (* Instantiate *) let regions_hierarchy = LlbcAstUtils.FunIdMap.find (FRegular method_id) - ctx.fun_context.regions_hierarchies + ctx.fun_ctx.regions_hierarchies in let tr_self = TraitRef trait_ref in let inst_sg = @@ -1450,7 +1450,7 @@ and eval_assumed_function_call_symbolic (config : config) (fid : assumed_fun_id) * this is a current limitation of our synthesis *) assert ( List.for_all - (fun ty -> not (ty_has_borrows ctx.type_context.type_infos ty)) + (fun ty -> not (ty_has_borrows ctx.type_ctx.type_infos ty)) generics.types); (* There are two cases (and this is extremely annoying): @@ -1476,7 +1476,7 @@ and eval_assumed_function_call_symbolic (config : config) (fid : assumed_fun_id) | _ -> let regions_hierarchy = LlbcAstUtils.FunIdMap.find (FAssumed fid) - ctx.fun_context.regions_hierarchies + ctx.fun_ctx.regions_hierarchies in (* There shouldn't be any reference to Self *) let tr_self = UnknownTrait __FUNCTION__ in diff --git a/compiler/InterpreterUtils.ml b/compiler/InterpreterUtils.ml index e04a6b90..a1a06ee5 100644 --- a/compiler/InterpreterUtils.ml +++ b/compiler/InterpreterUtils.ml @@ -265,7 +265,7 @@ let value_has_ret_symbolic_value_with_borrow_under_mut (ctx : eval_ctx) inherit [_] iter_typed_value method! visit_symbolic_value _ s = - if ty_has_borrow_under_mut ctx.type_context.type_infos s.sv_ty then + if ty_has_borrow_under_mut ctx.type_ctx.type_infos s.sv_ty then raise Found else () end @@ -288,15 +288,15 @@ let rvalue_get_place (rv : rvalue) : place option = (** See {!ValuesUtils.symbolic_value_has_borrows} *) let symbolic_value_has_borrows (ctx : eval_ctx) (sv : symbolic_value) : bool = - ValuesUtils.symbolic_value_has_borrows ctx.type_context.type_infos sv + ValuesUtils.symbolic_value_has_borrows ctx.type_ctx.type_infos sv (** See {!ValuesUtils.value_has_borrows}. *) let value_has_borrows (ctx : eval_ctx) (v : value) : bool = - ValuesUtils.value_has_borrows ctx.type_context.type_infos v + ValuesUtils.value_has_borrows ctx.type_ctx.type_infos v (** See {!ValuesUtils.value_has_loans_or_borrows}. *) let value_has_loans_or_borrows (ctx : eval_ctx) (v : value) : bool = - ValuesUtils.value_has_loans_or_borrows ctx.type_context.type_infos v + ValuesUtils.value_has_loans_or_borrows ctx.type_ctx.type_infos v (** See {!ValuesUtils.value_has_loans}. *) let value_has_loans (v : value) : bool = ValuesUtils.value_has_loans v @@ -401,19 +401,19 @@ let compute_env_elem_ids (x : env_elem) : ids_sets * ids_to_values = compute_env_ids [ x ] (** Compute the sets of ids found in a list of contexts. *) -let compute_contexts_ids (ctxl : eval_ctx list) : ids_sets * ids_to_values = +let compute_ctxs_ids (ctxl : eval_ctx list) : ids_sets * ids_to_values = let compute, get_ids, get_ids_to_values = compute_ids () in List.iter (compute#visit_eval_ctx ()) ctxl; (get_ids (), get_ids_to_values ()) (** Compute the sets of ids found in a context. *) -let compute_context_ids (ctx : eval_ctx) : ids_sets * ids_to_values = - compute_contexts_ids [ ctx ] +let compute_ctx_ids (ctx : eval_ctx) : ids_sets * ids_to_values = + compute_ctxs_ids [ ctx ] (** **WARNING**: this function doesn't compute the normalized types (for the trait type aliases). This should be computed afterwards. *) -let initialize_eval_context (ctx : decls_ctx) +let initialize_eval_ctx (ctx : decls_ctx) (region_groups : RegionGroupId.id list) (type_vars : type_var list) (const_generic_vars : const_generic_var list) : eval_ctx = reset_global_counters (); @@ -427,11 +427,11 @@ let initialize_eval_context (ctx : decls_ctx) const_generic_vars) in { - type_context = ctx.type_ctx; - fun_context = ctx.fun_ctx; - global_context = ctx.global_ctx; - trait_decls_context = ctx.trait_decls_ctx; - trait_impls_context = ctx.trait_impls_ctx; + type_ctx = ctx.type_ctx; + fun_ctx = ctx.fun_ctx; + global_ctx = ctx.global_ctx; + trait_decls_ctx = ctx.trait_decls_ctx; + trait_impls_ctx = ctx.trait_impls_ctx; region_groups; type_vars; const_generic_vars; diff --git a/compiler/Invariants.ml b/compiler/Invariants.ml index fa0d7436..b87cdff7 100644 --- a/compiler/Invariants.ml +++ b/compiler/Invariants.ml @@ -768,7 +768,7 @@ let check_symbolic_values (ctx : eval_ctx) : unit = assert (info.env_count = 0 || info.aproj_borrows = []); (* A symbolic value containing borrows can't be duplicated (i.e., copied): * it must be expanded first *) - if ty_has_borrows ctx.type_context.type_infos info.ty then + if ty_has_borrows ctx.type_ctx.type_infos info.ty then assert (info.env_count <= 1); (* A duplicated symbolic value is necessarily primitively copyable *) assert (info.env_count <= 1 || ty_is_primitively_copyable info.ty); diff --git a/compiler/Print.ml b/compiler/Print.ml index 0e2ec1fc..8999c77d 100644 --- a/compiler/Print.ml +++ b/compiler/Print.ml @@ -409,11 +409,11 @@ module Contexts = struct } let eval_ctx_to_fmt_env (ctx : eval_ctx) : fmt_env = - let type_decls = ctx.type_context.type_decls in - let fun_decls = ctx.fun_context.fun_decls in - let global_decls = ctx.global_context.global_decls in - let trait_decls = ctx.trait_decls_context.trait_decls in - let trait_impls = ctx.trait_impls_context.trait_impls in + let type_decls = ctx.type_ctx.type_decls in + let fun_decls = ctx.fun_ctx.fun_decls in + let global_decls = ctx.global_ctx.global_decls in + let trait_decls = ctx.trait_decls_ctx.trait_decls in + let trait_impls = ctx.trait_impls_ctx.trait_impls in (* Below: it is always safe to omit fields - if an id can't be found at printing time, we print the id (in raw form) instead of the name it designates. *) diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml index 204fc399..d8213317 100644 --- a/compiler/SymbolicToPure.ml +++ b/compiler/SymbolicToPure.ml @@ -15,7 +15,7 @@ module PP = PrintPure (** The local logger *) let log = Logging.symbolic_to_pure_log -type type_context = { +type type_ctx = { llbc_type_decls : T.type_decl TypeDeclId.Map.t; type_decls : type_decl TypeDeclId.Map.t; (** We use this for type-checking (for sanity checks) when translating @@ -43,18 +43,18 @@ type fun_sig_named_outputs = { } [@@deriving show] -type fun_context = { +type fun_ctx = { llbc_fun_decls : A.fun_decl A.FunDeclId.Map.t; fun_infos : fun_info A.FunDeclId.Map.t; regions_hierarchies : T.region_var_groups FunIdMap.t; } [@@deriving show] -type global_context = { llbc_global_decls : A.global_decl A.GlobalDeclId.Map.t } +type global_ctx = { llbc_global_decls : A.global_decl A.GlobalDeclId.Map.t } [@@deriving show] -type trait_decls_context = A.trait_decl A.TraitDeclId.Map.t [@@deriving show] -type trait_impls_context = A.trait_impl A.TraitImplId.Map.t [@@deriving show] +type trait_decls_ctx = A.trait_decl A.TraitDeclId.Map.t [@@deriving show] +type trait_impls_ctx = A.trait_impl A.TraitImplId.Map.t [@@deriving show] (** Whenever we translate a function call or an ended abstraction, we store the related information (this is useful when translating ended @@ -120,11 +120,11 @@ type loop_info = { (** Body synthesis context *) type bs_ctx = { - type_context : type_context; (* TODO: rename *) - fun_context : fun_context; (* TODO: rename *) - global_context : global_context; (* TODO: rename *) - trait_decls_ctx : trait_decls_context; - trait_impls_ctx : trait_impls_context; + type_ctx : type_ctx; + fun_ctx : fun_ctx; + global_ctx : global_ctx; + trait_decls_ctx : trait_decls_ctx; + trait_impls_ctx : trait_impls_ctx; fun_decl : A.fun_decl; bid : RegionGroupId.id option; (** TODO: rename @@ -234,9 +234,9 @@ type bs_ctx = { (* TODO: move *) let bs_ctx_to_fmt_env (ctx : bs_ctx) : Print.fmt_env = - let type_decls = ctx.type_context.llbc_type_decls in - let fun_decls = ctx.fun_context.llbc_fun_decls in - let global_decls = ctx.global_context.llbc_global_decls in + let type_decls = ctx.type_ctx.llbc_type_decls in + let fun_decls = ctx.fun_ctx.llbc_fun_decls in + let global_decls = ctx.global_ctx.llbc_global_decls in let trait_decls = ctx.trait_decls_ctx in let trait_impls = ctx.trait_impls_ctx in let { regions; types; const_generics; trait_clauses } : T.generic_params = @@ -258,9 +258,9 @@ let bs_ctx_to_fmt_env (ctx : bs_ctx) : Print.fmt_env = } let bs_ctx_to_pure_fmt_env (ctx : bs_ctx) : PrintPure.fmt_env = - let type_decls = ctx.type_context.llbc_type_decls in - let fun_decls = ctx.fun_context.llbc_fun_decls in - let global_decls = ctx.global_context.llbc_global_decls in + let type_decls = ctx.type_ctx.llbc_type_decls in + let fun_decls = ctx.fun_ctx.llbc_fun_decls in + let global_decls = ctx.global_ctx.llbc_global_decls in let trait_decls = ctx.trait_decls_ctx in let trait_impls = ctx.trait_impls_ctx in let generics = ctx.sg.generics in @@ -346,11 +346,11 @@ let abs_to_string (ctx : bs_ctx) (abs : V.abs) : string = let bs_ctx_lookup_llbc_type_decl (id : TypeDeclId.id) (ctx : bs_ctx) : T.type_decl = - TypeDeclId.Map.find id ctx.type_context.llbc_type_decls + TypeDeclId.Map.find id ctx.type_ctx.llbc_type_decls let bs_ctx_lookup_llbc_fun_decl (id : A.FunDeclId.id) (ctx : bs_ctx) : A.fun_decl = - A.FunDeclId.Map.find id ctx.fun_context.llbc_fun_decls + A.FunDeclId.Map.find id ctx.fun_ctx.llbc_fun_decls (* Some generic translation functions (we need to translate different "flavours" of types: forward types, backward types, etc.) *) @@ -617,13 +617,13 @@ and translate_fwd_trait_instance_id (type_infos : type_infos) (** Simply calls [translate_fwd_ty] *) let ctx_translate_fwd_ty (ctx : bs_ctx) (ty : T.ty) : ty = - let type_infos = ctx.type_context.type_infos in + let type_infos = ctx.type_ctx.type_infos in translate_fwd_ty type_infos ty (** Simply calls [translate_fwd_generic_args] *) let ctx_translate_fwd_generic_args (ctx : bs_ctx) (generics : T.generic_args) : generic_args = - let type_infos = ctx.type_context.type_infos in + let type_infos = ctx.type_ctx.type_infos in translate_fwd_generic_args type_infos generics (** Translate a type, when some regions may have ended. @@ -708,7 +708,7 @@ let rec translate_back_ty (type_infos : type_infos) (** Simply calls [translate_back_ty] *) let ctx_translate_back_ty (ctx : bs_ctx) (keep_region : 'r -> bool) (inside_mut : bool) (ty : T.ty) : ty option = - let type_infos = ctx.type_context.type_infos in + let type_infos = ctx.type_ctx.type_infos in translate_back_ty type_infos keep_region inside_mut ty let mk_type_check_ctx (ctx : bs_ctx) : PureTypeCheck.tc_ctx = @@ -721,8 +721,8 @@ let mk_type_check_ctx (ctx : bs_ctx) : PureTypeCheck.tc_ctx = in let env = VarId.Map.empty in { - PureTypeCheck.type_decls = ctx.type_context.type_decls; - global_decls = ctx.global_context.llbc_global_decls; + PureTypeCheck.type_decls = ctx.type_ctx.type_decls; + global_decls = ctx.global_ctx.llbc_global_decls; env; const_generics; } @@ -742,7 +742,7 @@ let translate_fun_id_or_trait_method_ref (ctx : bs_ctx) match id with | FunId fun_id -> FunId fun_id | TraitMethod (trait_ref, method_name, fun_decl_id) -> - let type_infos = ctx.type_context.type_infos in + let type_infos = ctx.type_ctx.type_infos in let trait_ref = translate_fwd_trait_ref type_infos trait_ref in TraitMethod (trait_ref, method_name, fun_decl_id) @@ -894,7 +894,7 @@ let translate_fun_sig_to_decomposed (decls_ctx : C.decls_ctx) List.map (fun (g : T.region_var_group) -> g.id) regions_hierarchy in let ctx = - InterpreterUtils.initialize_eval_context decls_ctx region_groups + InterpreterUtils.initialize_eval_ctx decls_ctx region_groups sg.generics.types sg.generics.const_generics in (* Compute the normalization map for the *sty* types and add it to the context *) @@ -1786,7 +1786,7 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) : (* Retrieve the effect information about this function (can fail, * takes a state as input, etc.) *) let effect_info = - get_fun_effect_info ctx.fun_context.fun_infos fid None None + get_fun_effect_info ctx.fun_ctx.fun_infos fid None None in (* Depending on the function effects: * - add the fuel @@ -2006,7 +2006,7 @@ and translate_end_abstraction_fun_call (ectx : C.eval_ctx) (abs : V.abs) raise (Failure "Unreachable") in let effect_info = - get_fun_effect_info ctx.fun_context.fun_infos fun_id None (Some rg_id) + get_fun_effect_info ctx.fun_ctx.fun_infos fun_id None (Some rg_id) in let generics = ctx_translate_fwd_generic_args ctx call.generics in (* Retrieve the original call and the parent abstractions *) @@ -2194,8 +2194,8 @@ and translate_end_abstraction_loop (ectx : C.eval_ctx) (abs : V.abs) | V.LoopCall -> let fun_id = E.FRegular ctx.fun_decl.def_id in let effect_info = - get_fun_effect_info ctx.fun_context.fun_infos (FunId fun_id) - (Some vloop_id) (Some rg_id) + get_fun_effect_info ctx.fun_ctx.fun_infos (FunId fun_id) (Some vloop_id) + (Some rg_id) in let loop_info = LoopId.Map.find loop_id ctx.loops in let generics = loop_info.generics in @@ -2306,7 +2306,7 @@ and translate_end_abstraction_loop (ectx : C.eval_ctx) (abs : V.abs) and translate_global_eval (gid : A.GlobalDeclId.id) (sval : V.symbolic_value) (e : S.expression) (ctx : bs_ctx) : texpression = let ctx, var = fresh_var_for_symbolic_value sval ctx in - let decl = A.GlobalDeclId.Map.find gid ctx.global_context.llbc_global_decls in + let decl = A.GlobalDeclId.Map.find gid ctx.global_ctx.llbc_global_decls in let global_expr = { id = Global gid; generics = empty_generic_args } in (* We use translate_fwd_ty to translate the global type *) let ty = ctx_translate_fwd_ty ctx decl.ty in @@ -2482,7 +2482,7 @@ and translate_ExpandAdt_one_branch (sv : V.symbolic_value) - if we forbid using field projectors. *) let is_rec_def = - T.TypeDeclId.Set.mem adt_id ctx.type_context.recursive_decls + T.TypeDeclId.Set.mem adt_id ctx.type_ctx.recursive_decls in let use_let_with_cons = is_enum @@ -2495,7 +2495,7 @@ and translate_ExpandAdt_one_branch (sv : V.symbolic_value) like Coq don't, in which case we have to deconstruct the whole ADT at once (`let (a, b, c) = x in`) *) || TypesUtils.type_decl_from_type_id_is_tuple_struct - ctx.type_context.type_infos type_id + ctx.type_ctx.type_infos type_id && not (Config.backend_has_tuple_projectors ()) in if use_let_with_cons then @@ -2588,7 +2588,7 @@ and translate_intro_symbolic (ectx : C.eval_ctx) (p : S.mplace option) { e = StructUpdate su; ty = var.ty } | VaCgValue cg_id -> { e = CVar cg_id; ty = var.ty } | VaTraitConstValue (trait_ref, generics, const_name) -> - let type_infos = ctx.type_context.type_infos in + let type_infos = ctx.type_ctx.type_infos in let trait_ref = translate_fwd_trait_ref type_infos trait_ref in let generics = translate_fwd_generic_args type_infos generics in let qualif_id = TraitConst (trait_ref, generics, const_name) in @@ -2722,7 +2722,7 @@ and translate_forward_end (ectx : C.eval_ctx) let sg = ctx.fun_decl.signature in let regions_hierarchy = LlbcAstUtils.FunIdMap.find (FRegular def_id) - ctx.fun_context.regions_hierarchies + ctx.fun_ctx.regions_hierarchies in List.map (fun (gid, _) -> @@ -2816,7 +2816,7 @@ and translate_forward_end (ectx : C.eval_ctx) (* Lookup the effect info for the loop function *) let fid = E.FRegular ctx.fun_decl.def_id in let effect_info = - get_fun_effect_info ctx.fun_context.fun_infos (FunId fid) None ctx.bid + get_fun_effect_info ctx.fun_ctx.fun_infos (FunId fid) None ctx.bid in (* Introduce a fresh output value for the forward function *) @@ -2949,7 +2949,7 @@ and translate_loop (loop : S.loop) (ctx : bs_ctx) : texpression = List.map (fun ty -> assert ( - not (TypesUtils.ty_has_borrows !ctx.type_context.type_infos ty)); + not (TypesUtils.ty_has_borrows !ctx.type_ctx.type_infos ty)); (None, ctx_translate_fwd_ty !ctx ty)) tys in @@ -3173,7 +3173,7 @@ let translate_fun_decl (ctx : bs_ctx) (body : S.expression option) : fun_decl = (* Translate the signature *) let signature = translate_fun_sig_from_decomposed ctx.sg ctx.bid in let regions_hierarchy = - FunIdMap.find (FRegular def_id) ctx.fun_context.regions_hierarchies + FunIdMap.find (FRegular def_id) ctx.fun_ctx.regions_hierarchies in (* Translate the body, if there is *) let body = @@ -3181,8 +3181,8 @@ let translate_fun_decl (ctx : bs_ctx) (body : S.expression option) : fun_decl = | None -> None | Some body -> let effect_info = - get_fun_effect_info ctx.fun_context.fun_infos - (FunId (FRegular def_id)) None bid + get_fun_effect_info ctx.fun_ctx.fun_infos (FunId (FRegular def_id)) + None bid in let body = translate_expression body ctx in (* Add a match over the fuel, if necessary *) diff --git a/compiler/Translate.ml b/compiler/Translate.ml index 8b221c93..e153f4f4 100644 --- a/compiler/Translate.ml +++ b/compiler/Translate.ml @@ -72,7 +72,7 @@ let translate_function_to_pure (trans_ctx : trans_ctx) | RecGroup _ -> Some tid) (TypeDeclId.Map.bindings trans_ctx.type_ctx.type_decls_groups)) in - let type_context = + let type_ctx = { SymbolicToPure.type_infos = trans_ctx.type_ctx.type_infos; llbc_type_decls = trans_ctx.type_ctx.type_decls; @@ -80,14 +80,14 @@ let translate_function_to_pure (trans_ctx : trans_ctx) recursive_decls = recursive_type_decls; } in - let fun_context = + let fun_ctx = { SymbolicToPure.llbc_fun_decls = trans_ctx.fun_ctx.fun_decls; fun_infos = trans_ctx.fun_ctx.fun_infos; regions_hierarchies = trans_ctx.fun_ctx.regions_hierarchies; } in - let global_context = + let global_ctx = { SymbolicToPure.llbc_global_decls = trans_ctx.global_ctx.global_decls } in @@ -134,7 +134,7 @@ let translate_function_to_pure (trans_ctx : trans_ctx) in let regions_hierarchy = - LlbcAstUtils.FunIdMap.find (FRegular def_id) fun_context.regions_hierarchies + LlbcAstUtils.FunIdMap.find (FRegular def_id) fun_ctx.regions_hierarchies in let var_counter, back_state_vars = @@ -160,9 +160,9 @@ let translate_function_to_pure (trans_ctx : trans_ctx) back_state_vars; fuel0; fuel; - type_context; - fun_context; - global_context; + type_ctx; + fun_ctx; + global_ctx; trait_decls_ctx = trans_ctx.trait_decls_ctx.trait_decls; trait_impls_ctx = trans_ctx.trait_impls_ctx.trait_impls; fun_decl = fdef; |