module T = Types module V = Values module E = Expressions module C = Contexts module Subst = Substitute module A = LlbcAst module L = Logging open Utils open TypesUtils module PA = Print.EvalCtxLlbcAst open Cps (* TODO: we should probably rename the file to ContextsUtils *) (** The local logger *) let log = L.interpreter_log (** Some utilities *) (** Auxiliary function - call a function which requires a continuation, and return the let context given to the continuation *) let get_cf_ctx_no_synth (f : cm_fun) (ctx : C.eval_ctx) : C.eval_ctx = let nctx = ref None in let cf ctx = assert (!nctx = None); nctx := Some ctx; None in let _ = f cf ctx in Option.get !nctx let eval_ctx_to_string_no_filter = Print.Contexts.eval_ctx_to_string_no_filter let eval_ctx_to_string = Print.Contexts.eval_ctx_to_string let ety_to_string = PA.ety_to_string let rty_to_string = PA.rty_to_string let symbolic_value_to_string = PA.symbolic_value_to_string let borrow_content_to_string = PA.borrow_content_to_string let loan_content_to_string = PA.loan_content_to_string let aborrow_content_to_string = PA.aborrow_content_to_string let aloan_content_to_string = PA.aloan_content_to_string let aproj_to_string = PA.aproj_to_string let typed_value_to_string = PA.typed_value_to_string let typed_avalue_to_string = PA.typed_avalue_to_string let place_to_string = PA.place_to_string let operand_to_string = PA.operand_to_string let egeneric_args_to_string = PA.egeneric_args_to_string let rtrait_instance_id_to_string = PA.rtrait_instance_id_to_string let fun_sig_to_string = PA.fun_sig_to_string let fun_decl_to_string = PA.fun_decl_to_string let call_to_string = PA.call_to_string let trait_impl_to_string ctx = PA.trait_impl_to_string { ctx with type_vars = []; const_generic_vars = [] } let statement_to_string ctx = PA.statement_to_string ctx "" " " let statement_to_string_with_tab ctx = PA.statement_to_string ctx " " " " let env_elem_to_string ctx = PA.env_elem_to_string ctx "" " " let env_to_string ctx env = eval_ctx_to_string { ctx with env } let abs_to_string ctx = PA.abs_to_string ctx "" " " let same_symbolic_id (sv0 : V.symbolic_value) (sv1 : V.symbolic_value) : bool = sv0.V.sv_id = sv1.V.sv_id let mk_var (index : E.VarId.id) (name : string option) (var_ty : T.ety) : A.var = { A.index; name; var_ty } (** Small helper - TODO: move *) let mk_place_from_var_id (var_id : E.VarId.id) : E.place = { var_id; projection = [] } (** Create a fresh symbolic value *) let mk_fresh_symbolic_value (sv_kind : V.sv_kind) (ty : T.rty) : V.symbolic_value = let sv_id = C.fresh_symbolic_value_id () in let svalue = { V.sv_kind; V.sv_id; V.sv_ty = ty } in svalue (** Create a fresh symbolic value *) let mk_fresh_symbolic_typed_value (sv_kind : V.sv_kind) (rty : T.rty) : V.typed_value = let ty = Subst.erase_regions rty in (* Generate the fresh a symbolic value *) let value = mk_fresh_symbolic_value sv_kind rty in let value = V.Symbolic value in { V.value; V.ty } (** Create a fresh symbolic value *) let mk_fresh_symbolic_typed_value_from_ety (sv_kind : V.sv_kind) (ety : T.ety) : V.typed_value = let ty = TypesUtils.ety_no_regions_to_rty ety in mk_fresh_symbolic_typed_value sv_kind ty (** Create a typed value from a symbolic value. *) let mk_typed_value_from_symbolic_value (svalue : V.symbolic_value) : V.typed_value = let av = V.Symbolic svalue in let av : V.typed_value = { V.value = av; V.ty = Subst.erase_regions svalue.V.sv_ty } in av (** Create a loans projector value from a symbolic value. Checks if the projector will actually project some regions. If not, returns {!V.AIgnored} ([_]). TODO: update to handle 'static *) let mk_aproj_loans_value_from_symbolic_value (regions : T.RegionId.Set.t) (svalue : V.symbolic_value) : V.typed_avalue = if ty_has_regions_in_set regions svalue.sv_ty then let av = V.ASymbolic (V.AProjLoans (svalue, [])) in let av : V.typed_avalue = { V.value = av; V.ty = svalue.V.sv_ty } in av else { V.value = V.AIgnored; ty = svalue.V.sv_ty } (** Create a borrows projector from a symbolic value *) let mk_aproj_borrows_from_symbolic_value (proj_regions : T.RegionId.Set.t) (svalue : V.symbolic_value) (proj_ty : T.rty) : V.aproj = if ty_has_regions_in_set proj_regions proj_ty then V.AProjBorrows (svalue, proj_ty) else V.AIgnoredProjBorrows (** TODO: move *) let borrow_is_asb (bid : V.BorrowId.id) (asb : V.abstract_shared_borrow) : bool = match asb with | V.AsbBorrow bid' -> bid' = bid | V.AsbProjReborrows _ -> false (** TODO: move *) let borrow_in_asb (bid : V.BorrowId.id) (asb : V.abstract_shared_borrows) : bool = List.exists (borrow_is_asb bid) asb (** TODO: move *) let remove_borrow_from_asb (bid : V.BorrowId.id) (asb : V.abstract_shared_borrows) : V.abstract_shared_borrows = let removed = ref 0 in let asb = List.filter (fun asb -> if not (borrow_is_asb bid asb) then true else ( removed := !removed + 1; false)) asb in assert (!removed = 1); asb (** We sometimes need to return a value whose type may vary depending on whether we find it in a "concrete" value or an abstraction (ex.: loan contents when we perform environment lookups by using borrow ids) TODO: change the name "abstract" *) type ('a, 'b) concrete_or_abs = Concrete of 'a | Abstract of 'b [@@deriving show] (** Generic loan content: concrete or abstract *) type g_loan_content = (V.loan_content, V.aloan_content) concrete_or_abs [@@deriving show] (** Generic borrow content: concrete or abstract *) type g_borrow_content = (V.borrow_content, V.aborrow_content) concrete_or_abs [@@deriving show] type abs_or_var_id = | AbsId of V.AbstractionId.id | VarId of E.VarId.id | DummyVarId of C.DummyVarId.id (** Utility exception *) exception FoundBorrowContent of V.borrow_content (** Utility exception *) exception FoundLoanContent of V.loan_content (** Utility exception *) exception FoundABorrowContent of V.aborrow_content (** Utility exception *) exception FoundGBorrowContent of g_borrow_content (** Utility exception *) exception FoundGLoanContent of g_loan_content (** Utility exception *) exception FoundAProjBorrows of V.symbolic_value * T.rty let symbolic_value_id_in_ctx (sv_id : V.SymbolicValueId.id) (ctx : C.eval_ctx) : bool = let obj = object inherit [_] C.iter_eval_ctx as super method! visit_Symbolic _ sv = if sv.V.sv_id = sv_id then raise Found else () method! visit_aproj env aproj = (match aproj with | AProjLoans (sv, _) | AProjBorrows (sv, _) -> if sv.V.sv_id = sv_id then raise Found else () | AEndedProjLoans _ | AEndedProjBorrows _ | AIgnoredProjBorrows -> ()); super#visit_aproj env aproj method! visit_abstract_shared_borrows _ asb = let visit (asb : V.abstract_shared_borrow) : unit = match asb with | V.AsbBorrow _ -> () | V.AsbProjReborrows (sv, _) -> if sv.V.sv_id = sv_id then raise Found else () in List.iter visit asb end in (* We use exceptions *) try obj#visit_eval_ctx () ctx; false with Found -> true (** Check that a symbolic value doesn't contain ended regions. Note that we don't check that the set of ended regions is empty: we check that the set of ended regions doesn't intersect the set of regions used in the type (this is more general). *) let symbolic_value_has_ended_regions (ended_regions : T.RegionId.Set.t) (s : V.symbolic_value) : bool = let regions = rty_regions s.V.sv_ty in not (T.RegionId.Set.disjoint regions ended_regions) (** Check if a {!type:V.value} contains [⊥]. Note that this function is very general: it also checks wether symbolic values contain already ended regions. *) let bottom_in_value (ended_regions : T.RegionId.Set.t) (v : V.typed_value) : bool = let obj = object inherit [_] V.iter_typed_value method! visit_Bottom _ = raise Found method! visit_symbolic_value _ s = if symbolic_value_has_ended_regions ended_regions s then raise Found else () end in (* We use exceptions *) try obj#visit_typed_value () v; false with Found -> true let value_has_ret_symbolic_value_with_borrow_under_mut (ctx : C.eval_ctx) (v : V.typed_value) : bool = let obj = object inherit [_] V.iter_typed_value method! visit_symbolic_value _ s = match s.sv_kind with | V.FunCallRet | V.LoopOutput | V.LoopJoin -> if ty_has_borrow_under_mut ctx.type_context.type_infos s.sv_ty then raise Found else () | V.SynthInput | V.SynthInputGivenBack | V.FunCallGivenBack | V.SynthRetGivenBack | V.Global | V.LoopGivenBack | V.Aggregate | V.ConstGeneric | V.TraitConst -> () end in (* We use exceptions *) try obj#visit_typed_value () v; false with Found -> true (** Return the place used in an rvalue, if that makes sense. This is used to compute meta-data, to find pretty names. *) let rvalue_get_place (rv : E.rvalue) : E.place option = match rv with | Use (Copy p | Move p) -> Some p | Use (Constant _) -> None | RvRef (p, _) -> Some p | UnaryOp _ | BinaryOp _ | Global _ | Discriminant _ | Aggregate _ -> None (** See {!ValuesUtils.symbolic_value_has_borrows} *) let symbolic_value_has_borrows (ctx : C.eval_ctx) (sv : V.symbolic_value) : bool = ValuesUtils.symbolic_value_has_borrows ctx.type_context.type_infos sv (** See {!ValuesUtils.value_has_borrows}. *) let value_has_borrows (ctx : C.eval_ctx) (v : V.value) : bool = ValuesUtils.value_has_borrows ctx.type_context.type_infos v (** See {!ValuesUtils.value_has_loans_or_borrows}. *) let value_has_loans_or_borrows (ctx : C.eval_ctx) (v : V.value) : bool = ValuesUtils.value_has_loans_or_borrows ctx.type_context.type_infos v (** See {!ValuesUtils.value_has_loans}. *) let value_has_loans (v : V.value) : bool = ValuesUtils.value_has_loans v (** See {!compute_typed_value_ids}, {!compute_context_ids}, etc. *) type ids_sets = { aids : V.AbstractionId.Set.t; blids : V.BorrowId.Set.t; (** All the borrow/loan ids *) borrow_ids : V.BorrowId.Set.t; (** Only the borrow ids *) loan_ids : V.BorrowId.Set.t; (** Only the loan ids *) dids : C.DummyVarId.Set.t; rids : T.RegionId.Set.t; sids : V.SymbolicValueId.Set.t; } [@@deriving show] (** See {!compute_typed_value_ids}, {!compute_context_ids}, etc. TODO: there misses information. *) type ids_to_values = { sids_to_values : V.symbolic_value V.SymbolicValueId.Map.t; } let compute_ids () = let blids = ref V.BorrowId.Set.empty in let borrow_ids = ref V.BorrowId.Set.empty in let loan_ids = ref V.BorrowId.Set.empty in let aids = ref V.AbstractionId.Set.empty in let dids = ref C.DummyVarId.Set.empty in let rids = ref T.RegionId.Set.empty in let sids = ref V.SymbolicValueId.Set.empty in let sids_to_values = ref V.SymbolicValueId.Map.empty in let get_ids () = { aids = !aids; blids = !blids; borrow_ids = !borrow_ids; loan_ids = !loan_ids; dids = !dids; rids = !rids; sids = !sids; } in let get_ids_to_values () = { sids_to_values = !sids_to_values } in let obj = object inherit [_] C.iter_eval_ctx as super method! visit_dummy_var_id _ did = dids := C.DummyVarId.Set.add did !dids method! visit_borrow_id _ id = blids := V.BorrowId.Set.add id !blids; borrow_ids := V.BorrowId.Set.add id !borrow_ids method! visit_loan_id _ id = blids := V.BorrowId.Set.add id !blids; loan_ids := V.BorrowId.Set.add id !loan_ids method! visit_abstraction_id _ id = aids := V.AbstractionId.Set.add id !aids method! visit_region_id _ id = rids := T.RegionId.Set.add id !rids method! visit_symbolic_value env sv = sids := V.SymbolicValueId.Set.add sv.sv_id !sids; sids_to_values := V.SymbolicValueId.Map.add sv.sv_id sv !sids_to_values; super#visit_symbolic_value env sv method! visit_symbolic_value_id _ id = (* TODO: can we get there without going through [visit_symbolic_value] first? *) sids := V.SymbolicValueId.Set.add id !sids end in (obj, get_ids, get_ids_to_values) (** Compute the sets of ids found in a list of typed values. *) let compute_typed_values_ids (xl : V.typed_value list) : ids_sets * ids_to_values = let compute, get_ids, get_ids_to_values = compute_ids () in List.iter (compute#visit_typed_value ()) xl; (get_ids (), get_ids_to_values ()) (** Compute the sets of ids found in a typed value. *) let compute_typed_value_ids (x : V.typed_value) : ids_sets * ids_to_values = compute_typed_values_ids [ x ] (** Compute the sets of ids found in a list of abstractions. *) let compute_absl_ids (xl : V.abs list) : ids_sets * ids_to_values = let compute, get_ids, get_ids_to_values = compute_ids () in List.iter (compute#visit_abs ()) xl; (get_ids (), get_ids_to_values ()) (** Compute the sets of ids found in an abstraction. *) let compute_abs_ids (x : V.abs) : ids_sets * ids_to_values = compute_absl_ids [ x ] (** Compute the sets of ids found in an environment. *) let compute_env_ids (x : C.env) : ids_sets * ids_to_values = let compute, get_ids, get_ids_to_values = compute_ids () in compute#visit_env () x; (get_ids (), get_ids_to_values ()) (** Compute the sets of ids found in an environment element. *) let compute_env_elem_ids (x : C.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 : C.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 : C.eval_ctx) : ids_sets * ids_to_values = compute_contexts_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 : C.decls_ctx) (region_groups : T.RegionGroupId.id list) (type_vars : T.type_var list) (const_generic_vars : T.const_generic_var list) : C.eval_ctx = C.reset_global_counters (); let const_generic_vars_map = T.ConstGenericVarId.Map.of_list (List.map (fun (cg : T.const_generic_var) -> let ty = TypesUtils.ety_no_regions_to_rty (T.Literal cg.ty) in let cv = mk_fresh_symbolic_typed_value V.ConstGeneric ty in (cg.index, cv)) const_generic_vars) in { C.type_context = ctx.type_ctx; C.fun_context = ctx.fun_ctx; C.global_context = ctx.global_ctx; C.trait_decls_context = ctx.trait_decls_ctx; C.trait_impls_context = ctx.trait_impls_ctx; C.region_groups; C.type_vars; C.const_generic_vars; C.const_generic_vars_map; C.norm_trait_etypes = C.ETraitTypeRefMap.empty (* Empty for now *); C.norm_trait_rtypes = C.RTraitTypeRefMap.empty (* Empty for now *); C.norm_trait_stypes = C.STraitTypeRefMap.empty (* Empty for now *); C.env = [ C.Frame ]; C.ended_regions = T.RegionId.Set.empty; } (** Instantiate a function signature, introducing **fresh** abstraction ids and region ids. This is mostly used in preparation of function calls (when evaluating in symbolic mode). Note: there are no region parameters, because they should be erased. *) let instantiate_fun_sig (ctx : C.eval_ctx) (generics : T.egeneric_args) (tr_self : T.rtrait_instance_id) (sg : A.fun_sig) : A.inst_fun_sig = log#ldebug (lazy ("instantiate_fun_sig:" ^ "\n- generics: " ^ egeneric_args_to_string ctx generics ^ "\n- tr_self: " ^ rtrait_instance_id_to_string ctx tr_self ^ "\n- sg: " ^ fun_sig_to_string ctx sg)); (* Generate fresh abstraction ids and create a substitution from region * group ids to abstraction ids *) let rg_abs_ids_bindings = List.map (fun rg -> let abs_id = C.fresh_abstraction_id () in (rg.T.id, abs_id)) sg.regions_hierarchy in let asubst_map : V.AbstractionId.id T.RegionGroupId.Map.t = List.fold_left (fun mp (rg_id, abs_id) -> T.RegionGroupId.Map.add rg_id abs_id mp) T.RegionGroupId.Map.empty rg_abs_ids_bindings in let asubst (rg_id : T.RegionGroupId.id) : V.AbstractionId.id = T.RegionGroupId.Map.find rg_id asubst_map in (* Generate fresh regions and their substitutions *) let _, rsubst, _ = Subst.fresh_regions_with_substs sg.generics.regions in (* Generate the type substitution * Note that we need the substitution to map the type variables to * {!rty} types (not {!ety}). In order to do that, we convert the * type parameters to types with regions. This is possible only * if those types don't contain any regions. * This is a current limitation of the analysis: there is still some * work to do to properly handle full type parametrization. * *) let rtype_params = List.map ety_no_regions_to_rty generics.types in let tsubst = Subst.make_type_subst_from_vars sg.generics.types rtype_params in let cgsubst = Subst.make_const_generic_subst_from_vars sg.generics.const_generics generics.const_generics in (* TODO: something annoying with the trait ref subst: we need to use region types, but the arguments use erased regions. For now we use the fact that no regions should appear inside. In the future: we should merge ety and rty. *) let trait_refs = List.map TypesUtils.etrait_ref_no_regions_to_gr_trait_ref generics.trait_refs in let tr_subst = Subst.make_trait_subst_from_clauses sg.generics.trait_clauses trait_refs in (* Substitute the signature *) let inst_sig = AssociatedTypes.ctx_subst_norm_signature ctx asubst rsubst tsubst cgsubst tr_subst tr_self sg in (* Return *) inst_sig