diff options
Diffstat (limited to '')
| -rw-r--r-- | compiler/Driver.ml | 3 | ||||
| -rw-r--r-- | compiler/InterpreterLoops.ml | 4101 | ||||
| -rw-r--r-- | compiler/InterpreterLoops.mli | 62 | ||||
| -rw-r--r-- | compiler/InterpreterLoopsCore.ml | 386 | ||||
| -rw-r--r-- | compiler/InterpreterLoopsFixedPoint.ml | 965 | ||||
| -rw-r--r-- | compiler/InterpreterLoopsFixedPoint.mli | 166 | ||||
| -rw-r--r-- | compiler/InterpreterLoopsJoinCtxs.ml | 719 | ||||
| -rw-r--r-- | compiler/InterpreterLoopsJoinCtxs.mli | 120 | ||||
| -rw-r--r-- | compiler/InterpreterLoopsMatchCtxs.ml | 1591 | ||||
| -rw-r--r-- | compiler/InterpreterLoopsMatchCtxs.mli | 301 | ||||
| -rw-r--r-- | compiler/Logging.ml | 9 | ||||
| -rw-r--r-- | compiler/dune | 4 |
12 files changed, 4329 insertions, 4098 deletions
diff --git a/compiler/Driver.ml b/compiler/Driver.ml index 3d2e84ad..dfe4e908 100644 --- a/compiler/Driver.ml +++ b/compiler/Driver.ml @@ -24,6 +24,9 @@ let _ = pre_passes_log#set_level EL.Info; interpreter_log#set_level EL.Info; statements_log#set_level EL.Info; + loops_match_ctxs_log#set_level EL.Info; + loops_join_ctxs_log#set_level EL.Info; + loops_fixed_point_log#set_level EL.Info; loops_log#set_level EL.Info; paths_log#set_level EL.Info; expressions_log#set_level EL.Info; diff --git a/compiler/InterpreterLoops.ml b/compiler/InterpreterLoops.ml index dd0cfc3f..5b170ac5 100644 --- a/compiler/InterpreterLoops.ml +++ b/compiler/InterpreterLoops.ml @@ -1,61 +1,3 @@ -(** This module implements support for loops. - - Throughout the module, we will use the following code as example to - illustrate what the functions do (this function simply returns a mutable - borrow to the nth element of a list): - {[ - pub fn list_nth_mut<'a, T>(mut ls: &'a mut List<T>, mut i: u32) -> &'a mut T { - loop { - match ls { - List::Nil => { - panic!() - } - List::Cons(x, tl) => { - if i == 0 { - return x; - } else { - ls = tl; - i -= 1; - } - } - } - } - } - ]} - - Upon reaching the loop entry, the environment is as follows (ignoring the - dummy variables): - {[ - abs@0 { ML l0 } - ls -> MB l0 (s2 : loops::List<T>) - i -> s1 : u32 - ]} - - Upon reaching the [continue] at the end of the first iteration, the environment - is as follows: - {[ - abs@0 { ML l0 } - ls -> MB l4 (s@6 : loops::List<T>) - i -> s@7 : u32 - _@1 -> MB l0 (loops::List::Cons (ML l1, ML l2)) - _@2 -> MB l2 (@Box (ML l4)) // tail - _@3 -> MB l1 (s@3 : T) // hd - ]} - - The fixed point we compute is: - {[ - abs@0 { ML l0 } - ls -> MB l1 (s@3 : loops::List<T>) - i -> s@4 : u32 - abs@fp { // fp: fixed-point - MB l0 - ML l1 - } - ]} - - From here, we deduce that [abs@fp { MB l0, ML l1}] is the loop abstraction. - *) - module T = Types module PV = PrimitiveValues module V = Values @@ -64,3931 +6,18 @@ module C = Contexts module Subst = Substitute module A = LlbcAst module L = Logging -open TypesUtils open ValuesUtils module Inv = Invariants module S = SynthesizeSymbolic -module UF = UnionFind open Cps open InterpreterUtils -open InterpreterBorrows -open InterpreterExpressions +open InterpreterLoopsCore +open InterpreterLoopsMatchCtxs +open InterpreterLoopsFixedPoint (** The local logger *) let log = L.loops_log -type updt_env_kind = - | AbsInLeft of V.AbstractionId.id - | LoanInLeft of V.BorrowId.id - | LoansInLeft of V.BorrowId.Set.t - | AbsInRight of V.AbstractionId.id - | LoanInRight of V.BorrowId.id - | LoansInRight of V.BorrowId.Set.t - -(** Utility exception *) -exception ValueMatchFailure of updt_env_kind - -(** Utility exception *) -exception Distinct of string - -type ctx_or_update = (C.eval_ctx, updt_env_kind) result - -(** Union Find *) -module UnionFind = UF.Make (UF.StoreMap) - -(** A small utility - - - Rem.: some environments may be ill-formed (they may contain several times - the same loan or borrow - this happens for instance when merging - environments). This is the reason why we use sets in some places (for - instance, [borrow_to_abs] maps to a *set* of ids). -*) -type abs_borrows_loans_maps = { - abs_ids : V.AbstractionId.id list; - abs_to_borrows : V.BorrowId.Set.t V.AbstractionId.Map.t; - abs_to_loans : V.BorrowId.Set.t V.AbstractionId.Map.t; - abs_to_borrows_loans : V.BorrowId.Set.t V.AbstractionId.Map.t; - borrow_to_abs : V.AbstractionId.Set.t V.BorrowId.Map.t; - loan_to_abs : V.AbstractionId.Set.t V.BorrowId.Map.t; - borrow_loan_to_abs : V.AbstractionId.Set.t V.BorrowId.Map.t; -} - -(** Compute various maps linking the abstractions and the borrows/loans they contain. - - The [explore] function is used to filter abstractions. - - [no_duplicates] checks that borrows/loans are not referenced more than once - (see the documentation for {!abs_borrows_loans_maps}). - *) -let compute_abs_borrows_loans_maps (no_duplicates : bool) - (explore : V.abs -> bool) (env : C.env) : abs_borrows_loans_maps = - let abs_ids = ref [] in - let abs_to_borrows = ref V.AbstractionId.Map.empty in - let abs_to_loans = ref V.AbstractionId.Map.empty in - let abs_to_borrows_loans = ref V.AbstractionId.Map.empty in - let borrow_to_abs = ref V.BorrowId.Map.empty in - let loan_to_abs = ref V.BorrowId.Map.empty in - let borrow_loan_to_abs = ref V.BorrowId.Map.empty in - - let module R (Id0 : Identifiers.Id) (Id1 : Identifiers.Id) = struct - (* - [check_singleton_sets]: check that the mapping maps to a singletong. - [check_not_already_registered]: check if the mapping was not already registered. - *) - let register_mapping (check_singleton_sets : bool) - (check_not_already_registered : bool) (map : Id1.Set.t Id0.Map.t ref) - (id0 : Id0.id) (id1 : Id1.id) : unit = - (* Sanity check *) - (if check_singleton_sets || check_not_already_registered then - match Id0.Map.find_opt id0 !map with - | None -> () - | Some set -> - assert ( - (not check_not_already_registered) || not (Id1.Set.mem id1 set))); - (* Update the mapping *) - map := - Id0.Map.update id0 - (fun ids -> - match ids with - | None -> Some (Id1.Set.singleton id1) - | Some ids -> - (* Sanity check *) - assert (not check_singleton_sets); - assert ( - (not check_not_already_registered) - || not (Id1.Set.mem id1 ids)); - (* Update *) - Some (Id1.Set.add id1 ids)) - !map - end in - let module RAbsBorrow = R (V.AbstractionId) (V.BorrowId) in - let module RBorrowAbs = R (V.BorrowId) (V.AbstractionId) in - let register_borrow_id abs_id bid = - RAbsBorrow.register_mapping false no_duplicates abs_to_borrows abs_id bid; - RAbsBorrow.register_mapping false false abs_to_borrows_loans abs_id bid; - RBorrowAbs.register_mapping no_duplicates no_duplicates borrow_to_abs bid - abs_id; - RBorrowAbs.register_mapping false false borrow_loan_to_abs bid abs_id - in - - let register_loan_id abs_id bid = - RAbsBorrow.register_mapping false no_duplicates abs_to_loans abs_id bid; - RAbsBorrow.register_mapping false false abs_to_borrows_loans abs_id bid; - RBorrowAbs.register_mapping no_duplicates no_duplicates loan_to_abs bid - abs_id; - RBorrowAbs.register_mapping false false borrow_loan_to_abs bid abs_id - in - - let explore_abs = - object (self : 'self) - inherit [_] V.iter_typed_avalue as super - - (** Make sure we don't register the ignored ids *) - method! visit_aloan_content abs_id lc = - match lc with - | AMutLoan _ | ASharedLoan _ -> - (* Process those normally *) - super#visit_aloan_content abs_id lc - | AIgnoredMutLoan (_, child) - | AEndedIgnoredMutLoan { child; given_back = _; given_back_meta = _ } - | AIgnoredSharedLoan child -> - (* Ignore the id of the loan, if there is *) - self#visit_typed_avalue abs_id child - | AEndedMutLoan _ | AEndedSharedLoan _ -> raise (Failure "Unreachable") - - (** Make sure we don't register the ignored ids *) - method! visit_aborrow_content abs_id bc = - match bc with - | AMutBorrow _ | ASharedBorrow _ | AProjSharedBorrow _ -> - (* Process those normally *) - super#visit_aborrow_content abs_id bc - | AIgnoredMutBorrow (_, child) - | AEndedIgnoredMutBorrow { child; given_back = _; given_back_meta = _ } - -> - (* Ignore the id of the borrow, if there is *) - self#visit_typed_avalue abs_id child - | AEndedMutBorrow _ | AEndedSharedBorrow -> - raise (Failure "Unreachable") - - method! visit_borrow_id abs_id bid = register_borrow_id abs_id bid - method! visit_loan_id abs_id lid = register_loan_id abs_id lid - end - in - - C.env_iter_abs - (fun abs -> - let abs_id = abs.abs_id in - if explore abs then ( - abs_to_borrows := - V.AbstractionId.Map.add abs_id V.BorrowId.Set.empty !abs_to_borrows; - abs_to_loans := - V.AbstractionId.Map.add abs_id V.BorrowId.Set.empty !abs_to_loans; - abs_ids := abs.abs_id :: !abs_ids; - List.iter (explore_abs#visit_typed_avalue abs.abs_id) abs.avalues) - else ()) - env; - - (* Rem.: there is no need to reverse the abs ids, because we explored the environment - starting with the freshest values and abstractions *) - { - abs_ids = !abs_ids; - abs_to_borrows = !abs_to_borrows; - abs_to_loans = !abs_to_loans; - abs_to_borrows_loans = !abs_to_borrows_loans; - borrow_to_abs = !borrow_to_abs; - loan_to_abs = !loan_to_abs; - borrow_loan_to_abs = !borrow_loan_to_abs; - } - -(** Refresh the ids of the fresh abstractions. - - We do this because {!prepare_ashared_loans} introduces some non-fixed - abstractions in contexts which are later joined: we have to make sure two - contexts we join don't have non-fixed abstractions with the same ids. - *) -let refresh_abs (old_abs : V.AbstractionId.Set.t) (ctx : C.eval_ctx) : - C.eval_ctx = - let ids, _ = compute_context_ids ctx in - let abs_to_refresh = V.AbstractionId.Set.diff ids.aids old_abs in - let aids_subst = - List.map - (fun id -> (id, C.fresh_abstraction_id ())) - (V.AbstractionId.Set.elements abs_to_refresh) - in - let aids_subst = V.AbstractionId.Map.of_list aids_subst in - let subst id = - match V.AbstractionId.Map.find_opt id aids_subst with - | None -> id - | Some id -> id - in - let env = - Subst.env_subst_ids - (fun x -> x) - (fun x -> x) - (fun x -> x) - (fun x -> x) - (fun x -> x) - subst ctx.env - in - { ctx with C.env } - -(** Reorder the loans and borrows in the fresh abstractions. - - We do this in order to enforce some structure in the environments: this - allows us to find fixed-points. Note that this function needs to be - called typically after we merge abstractions together (see {!collapse_ctx} - for instance). - *) -let reorder_loans_borrows_in_fresh_abs (old_abs_ids : V.AbstractionId.Set.t) - (ctx : C.eval_ctx) : C.eval_ctx = - let reorder_in_fresh_abs (abs : V.abs) : V.abs = - (* Split between the loans and borrows *) - let is_borrow (av : V.typed_avalue) : bool = - match av.V.value with - | ABorrow _ -> true - | ALoan _ -> false - | _ -> raise (Failure "Unexpected") - in - let aborrows, aloans = List.partition is_borrow abs.V.avalues in - - (* Reoder the borrows, and the loans. - - After experimenting, it seems that a good way of reordering the loans - and the borrows to find fixed points is simply to sort them by increasing - order of id (taking the smallest id of a set of ids, in case of sets). - *) - let get_borrow_id (av : V.typed_avalue) : V.BorrowId.id = - match av.V.value with - | V.ABorrow (V.AMutBorrow (bid, _) | V.ASharedBorrow bid) -> bid - | _ -> raise (Failure "Unexpected") - in - let get_loan_id (av : V.typed_avalue) : V.BorrowId.id = - match av.V.value with - | V.ALoan (V.AMutLoan (lid, _)) -> lid - | V.ALoan (V.ASharedLoan (lids, _, _)) -> V.BorrowId.Set.min_elt lids - | _ -> raise (Failure "Unexpected") - in - (* We use ordered maps to reorder the borrows and loans *) - let reorder (get_bid : V.typed_avalue -> V.BorrowId.id) - (values : V.typed_avalue list) : V.typed_avalue list = - List.map snd - (V.BorrowId.Map.bindings - (V.BorrowId.Map.of_list (List.map (fun v -> (get_bid v, v)) values))) - in - let aborrows = reorder get_borrow_id aborrows in - let aloans = reorder get_loan_id aloans in - let avalues = List.append aborrows aloans in - { abs with V.avalues } - in - - let reorder_in_abs (abs : V.abs) = - if V.AbstractionId.Set.mem abs.abs_id old_abs_ids then abs - else reorder_in_fresh_abs abs - in - - let env = C.env_map_abs reorder_in_abs ctx.env in - - { ctx with C.env } - -(** Destructure all the new abstractions *) -let destructure_new_abs (loop_id : V.LoopId.id) - (old_abs_ids : V.AbstractionId.Set.t) (ctx : C.eval_ctx) : C.eval_ctx = - let abs_kind = V.Loop (loop_id, None, V.LoopSynthInput) in - let can_end = true in - let destructure_shared_values = true in - let is_fresh_abs_id (id : V.AbstractionId.id) : bool = - not (V.AbstractionId.Set.mem id old_abs_ids) - in - let env = - C.env_map_abs - (fun abs -> - if is_fresh_abs_id abs.abs_id then - let abs = - destructure_abs abs_kind can_end destructure_shared_values ctx abs - in - abs - else abs) - ctx.env - in - { ctx with env } - -(** Decompose the shared avalues, so as not to have nested shared loans - inside of abstractions. - - For instance: - {[ - abs'0 { shared_aloan ls0 (true, shared_loan ls1 s0) _ } - - ~~> - - abs'0 { - shared_aloan ls0 (true, s0) _ - shared_aloan ls1 s1 _ - } - ]} - - Note that we decompose only in the "fresh" abstractions (this is controled - by the [old_aids] parameter). - - TODO: how to factorize with {!InterpreterBorrows.destructure_abs}? - *) -let decompose_shared_avalues (loop_id : V.LoopId.id) - (old_aids : V.AbstractionId.Set.t) (ctx : C.eval_ctx) : C.eval_ctx = - (* Decompose the shared avalues in a fresh abstraction. We only decompose - in fresh (i.e., non-fixed) abstractions: {!decompose_in_abs} below - ignores the fixed abstractions and delegates to this function *) - let decompose_in_fresh_abs (abs : V.abs) : V.abs = - let new_loans = ref [] in - (* When decomposing, we need to duplicate the symbolic values (we - simply introduce fresh ids) *) - let mk_value_with_fresh_sids (v : V.typed_value) : V.typed_value = - let visitor = - object - inherit [_] V.map_typed_avalue - method! visit_symbolic_value_id _ _ = C.fresh_symbolic_value_id () - end - in - visitor#visit_typed_value () v - in - (* Visit the values: whenever we enter a shared loan (which is necessarily - a strict subvalue of a shared aloan, because we only explore abstractions) - we move it outside (we remove the shared loan, register a shared value - to insert in the abstraction, and use fresh symbolic values in this new - shared value). - *) - let loan_visitor = - object (self : 'self) - inherit [_] V.map_typed_avalue as super - - method! visit_typed_value env v = - match v.V.value with - | V.Loan (V.SharedLoan (lids, sv)) -> - let sv = self#visit_typed_value env sv in - - (* Introduce fresh symbolic values for the new loan *) - let nsv = mk_value_with_fresh_sids sv in - new_loans := List.append !new_loans [ (lids, nsv) ]; - - (* Return *) - sv - | _ -> super#visit_typed_value env v - end - in - let rid = T.RegionId.Set.min_elt abs.regions in - - (* We registered new loans to add in the abstraction: actually create those - loans, and insert them in the abstraction *) - let mk_ashared_loan (lids : V.BorrowId.Set.t) (sv : V.typed_value) : - V.typed_avalue = - (* There shouldn't be nested borrows *) - let sv_ty = ety_no_regions_to_rty sv.V.ty in - let ty = T.Ref (T.Var rid, sv_ty, T.Shared) in - let child_av = mk_aignored sv_ty in - let value = V.ALoan (V.ASharedLoan (lids, sv, child_av)) in - { V.value; ty } - in - let avalues = - List.map - (fun av -> - new_loans := []; - let av = loan_visitor#visit_typed_avalue () av in - let new_loans = - List.map (fun (lids, sv) -> mk_ashared_loan lids sv) !new_loans - in - av :: List.rev new_loans) - abs.V.avalues - in - let avalues = List.concat avalues in - let abs_id = C.fresh_abstraction_id () in - let kind = V.Loop (loop_id, None, V.LoopSynthInput) in - let can_end = true in - let abs = { abs with V.abs_id; kind; can_end; avalues } in - abs - in - - (* Decompose only in the fresh abstractions *) - let decompose_in_abs abs = - if V.AbstractionId.Set.mem abs.V.abs_id old_aids then abs - else decompose_in_fresh_abs abs - in - - (* Apply in the environment *) - let env = C.env_map_abs decompose_in_abs ctx.env in - { ctx with C.env } - -(** Collapse an environment. - - We do this to simplify an environment, for the purpose of finding a loop - fixed point. - - We do the following: - - we look for all the *new* dummy values (we use sets of old ids to decide - wether a value is new or not) and convert them into abstractions - - whenever there is a new abstraction in the context, and some of its - its borrows are associated to loans in another new abstraction, we - merge them. - In effect, this allows us to merge newly introduced abstractions/borrows - with their parent abstractions. - - For instance, when evaluating the first loop iteration, we start in the - following environment: - {[ - abs@0 { ML l0 } - ls -> MB l0 (s2 : loops::List<T>) - i -> s1 : u32 - ]} - - and get the following environment upon reaching the [Continue] statement: - {[ - abs@0 { ML l0 } - ls -> MB l4 (s@6 : loops::List<T>) - i -> s@7 : u32 - _@1 -> MB l0 (loops::List::Cons (ML l1, ML l2)) - _@2 -> MB l2 (@Box (ML l4)) // tail - _@3 -> MB l1 (s@3 : T) // hd - ]} - - In this new environment, the dummy variables [_@1], [_@2] and [_@3] are - considered as new. - - We first convert the new dummy values to abstractions. It gives: - {[ - abs@0 { ML l0 } - ls -> MB l4 (s@6 : loops::List<T>) - i -> s@7 : u32 - abs@1 { MB l0, ML l1, ML l2 } - abs@2 { MB l2, ML l4 } - abs@3 { MB l1 } - ]} - - We finally merge the new abstractions together. It gives: - {[ - abs@0 { ML l0 } - ls -> MB l4 (s@6 : loops::List<T>) - i -> s@7 : u32 - abs@4 { MB l0, ML l4 } - ]} - - [merge_funs]: those are used to merge loans or borrows which appear in both - abstractions (rem.: here we mean that, for instance, both abstractions - contain a shared loan with id l0). - This can happen when merging environments (note that such environments are not well-formed - - they become well formed again after collapsing). - *) -let collapse_ctx (loop_id : V.LoopId.id) - (merge_funs : merge_duplicates_funcs option) (old_ids : ids_sets) - (ctx0 : C.eval_ctx) : C.eval_ctx = - (* Debug *) - log#ldebug - (lazy - ("collapse_ctx:\n\n- fixed_ids:\n" ^ show_ids_sets old_ids - ^ "\n\n- ctx0:\n" ^ eval_ctx_to_string ctx0 ^ "\n\n")); - - let abs_kind = V.Loop (loop_id, None, LoopSynthInput) in - let can_end = true in - let destructure_shared_values = true in - let is_fresh_abs_id (id : V.AbstractionId.id) : bool = - not (V.AbstractionId.Set.mem id old_ids.aids) - in - let is_fresh_did (id : C.DummyVarId.id) : bool = - not (C.DummyVarId.Set.mem id old_ids.dids) - in - (* Convert the dummy values to abstractions (note that when we convert - values to abstractions, the resulting abstraction should be destructured) *) - (* Note that we preserve the order of the dummy values: we replace them with - abstractions in place - this makes matching easier *) - let env = - List.concat - (List.map - (fun ee -> - match ee with - | C.Abs _ | C.Frame | C.Var (VarBinder _, _) -> [ ee ] - | C.Var (DummyBinder id, v) -> - if is_fresh_did id then - let absl = - convert_value_to_abstractions abs_kind can_end - destructure_shared_values ctx0 v - in - List.map (fun abs -> C.Abs abs) absl - else [ ee ]) - ctx0.env) - in - let ctx = { ctx0 with C.env } in - log#ldebug - (lazy - ("collapse_ctx: after converting values to abstractions:\n" - ^ show_ids_sets old_ids ^ "\n\n- ctx:\n" ^ eval_ctx_to_string ctx ^ "\n\n" - )); - - log#ldebug - (lazy - ("collapse_ctx: after decomposing the shared values in the abstractions:\n" - ^ show_ids_sets old_ids ^ "\n\n- ctx:\n" ^ eval_ctx_to_string ctx ^ "\n\n" - )); - - (* Explore all the *new* abstractions, and compute various maps *) - let explore (abs : V.abs) = is_fresh_abs_id abs.abs_id in - let ids_maps = - compute_abs_borrows_loans_maps (merge_funs = None) explore env - in - let { - abs_ids; - abs_to_borrows; - abs_to_loans = _; - abs_to_borrows_loans; - borrow_to_abs = _; - loan_to_abs; - borrow_loan_to_abs; - } = - ids_maps - in - - (* Change the merging behaviour depending on the input parameters *) - let abs_to_borrows, loan_to_abs = - if merge_funs <> None then (abs_to_borrows_loans, borrow_loan_to_abs) - else (abs_to_borrows, loan_to_abs) - in - - (* Merge the abstractions together *) - let merged_abs : V.AbstractionId.id UF.elem V.AbstractionId.Map.t = - V.AbstractionId.Map.of_list (List.map (fun id -> (id, UF.make id)) abs_ids) - in - - let ctx = ref ctx in - - (* Merge all the mergeable abs. - - We iterate over the abstractions, then over the borrows in the abstractions. - We do this because we want to control the order in which abstractions - are merged (the ids are iterated in increasing order). Otherwise, we - could simply iterate over all the borrows in [borrow_to_abs]... - *) - List.iter - (fun abs_id0 -> - let bids = V.AbstractionId.Map.find abs_id0 abs_to_borrows in - let bids = V.BorrowId.Set.elements bids in - List.iter - (fun bid -> - match V.BorrowId.Map.find_opt bid loan_to_abs with - | None -> (* Nothing to do *) () - | Some abs_ids1 -> - V.AbstractionId.Set.iter - (fun abs_id1 -> - (* We need to merge - unless we have already merged *) - (* First, find the representatives for the two abstractions (the - representative is the abstraction into which we merged) *) - let abs_ref0 = - UF.find (V.AbstractionId.Map.find abs_id0 merged_abs) - in - let abs_id0 = UF.get abs_ref0 in - let abs_ref1 = - UF.find (V.AbstractionId.Map.find abs_id1 merged_abs) - in - let abs_id1 = UF.get abs_ref1 in - (* If the two ids are the same, it means the abstractions were already merged *) - if abs_id0 = abs_id1 then () - else ( - (* We actually need to merge the abstractions *) - - (* Debug *) - log#ldebug - (lazy - ("collapse_ctx: merging abstraction " - ^ V.AbstractionId.to_string abs_id1 - ^ " into " - ^ V.AbstractionId.to_string abs_id0 - ^ ":\n\n" ^ eval_ctx_to_string !ctx)); - - (* Update the environment - pay attention to the order: we - we merge [abs_id1] *into* [abs_id0] *) - let nctx, abs_id = - merge_into_abstraction abs_kind can_end merge_funs !ctx - abs_id1 abs_id0 - in - ctx := nctx; - - (* Update the union find *) - let abs_ref_merged = UF.union abs_ref0 abs_ref1 in - UF.set abs_ref_merged abs_id)) - abs_ids1) - bids) - abs_ids; - - log#ldebug - (lazy - ("collapse_ctx:\n\n- fixed_ids:\n" ^ show_ids_sets old_ids - ^ "\n\n- after collapse:\n" ^ eval_ctx_to_string !ctx ^ "\n\n")); - - (* Reorder the loans and borrows in the fresh abstractions *) - let ctx = reorder_loans_borrows_in_fresh_abs old_ids.aids !ctx in - - log#ldebug - (lazy - ("collapse_ctx:\n\n- fixed_ids:\n" ^ show_ids_sets old_ids - ^ "\n\n- after collapse and reorder borrows/loans:\n" - ^ eval_ctx_to_string ctx ^ "\n\n")); - - (* Return the new context *) - ctx - -(** Match two types during a join. *) -let rec match_types (match_distinct_types : 'r T.ty -> 'r T.ty -> 'r T.ty) - (match_regions : 'r -> 'r -> 'r) (ty0 : 'r T.ty) (ty1 : 'r T.ty) : 'r T.ty = - let match_rec = match_types match_distinct_types match_regions in - match (ty0, ty1) with - | Adt (id0, regions0, tys0), Adt (id1, regions1, tys1) -> - assert (id0 = id1); - let id = id0 in - let regions = - List.map - (fun (id0, id1) -> match_regions id0 id1) - (List.combine regions0 regions1) - in - let tys = - List.map (fun (ty0, ty1) -> match_rec ty0 ty1) (List.combine tys0 tys1) - in - Adt (id, regions, tys) - | TypeVar vid0, TypeVar vid1 -> - assert (vid0 = vid1); - let vid = vid0 in - TypeVar vid - | Bool, Bool | Char, Char | Never, Never | Str, Str -> ty0 - | Integer int_ty0, Integer int_ty1 -> - assert (int_ty0 = int_ty1); - ty0 - | Array ty0, Array ty1 | Slice ty0, Slice ty1 -> match_rec ty0 ty1 - | Ref (r0, ty0, k0), Ref (r1, ty1, k1) -> - let r = match_regions r0 r1 in - let ty = match_rec ty0 ty1 in - assert (k0 = k1); - let k = k0 in - Ref (r, ty, k) - | _ -> match_distinct_types ty0 ty1 - -(** See {!Match}. - - This module contains specialized match functions to instantiate the generic - {!Match} functor. - *) -module type Matcher = sig - val match_etys : T.ety -> T.ety -> T.ety - val match_rtys : T.rty -> T.rty -> T.rty - - (** The input primitive values are not equal *) - val match_distinct_primitive_values : - T.ety -> V.primitive_value -> V.primitive_value -> V.typed_value - - (** The input ADTs don't have the same variant *) - val match_distinct_adts : T.ety -> V.adt_value -> V.adt_value -> V.typed_value - - (** The meta-value is the result of a match. - - We take an additional function as input, which acts as a matcher over - typed values, to be able to lookup the shared values and match them. - We do this for shared borrows (and not, e.g., mutable borrows) because - shared borrows introduce indirections, while mutable borrows carry the - borrowed values with them: we might want to explore and match those - borrowed values, in which case we have to manually look them up before - calling the match function. - *) - val match_shared_borrows : - (V.typed_value -> V.typed_value -> V.typed_value) -> - T.ety -> - V.borrow_id -> - V.borrow_id -> - V.borrow_id - - (** The input parameters are: - - [ty] - - [bid0]: first borrow id - - [bv0]: first borrowed value - - [bid1] - - [bv1] - - [bv]: the result of matching [bv0] with [bv1] - *) - val match_mut_borrows : - T.ety -> - V.borrow_id -> - V.typed_value -> - V.borrow_id -> - V.typed_value -> - V.typed_value -> - V.borrow_id * V.typed_value - - (** Parameters: - [ty] - [ids0] - [ids1] - [v]: the result of matching the shared values coming from the two loans - *) - val match_shared_loans : - T.ety -> - V.loan_id_set -> - V.loan_id_set -> - V.typed_value -> - V.loan_id_set * V.typed_value - - val match_mut_loans : T.ety -> V.loan_id -> V.loan_id -> V.loan_id - - (** There are no constraints on the input symbolic values *) - val match_symbolic_values : - V.symbolic_value -> V.symbolic_value -> V.symbolic_value - - (** Match a symbolic value with a value which is not symbolic. - - If the boolean is [true], it means the symbolic value comes from the - *left* environment. Otherwise it comes from the right environment (it - is important when throwing exceptions, for instance when we need to - end loans in one of the two environments). - *) - val match_symbolic_with_other : - bool -> V.symbolic_value -> V.typed_value -> V.typed_value - - (** Match a bottom value with a value which is not bottom. - - If the boolean is [true], it means the bottom value comes from the - *left* environment. Otherwise it comes from the right environment (it - is important when throwing exceptions, for instance when we need to - end loans in one of the two environments). - *) - val match_bottom_with_other : bool -> V.typed_value -> V.typed_value - - (** The input ADTs don't have the same variant *) - val match_distinct_aadts : - T.rty -> V.adt_avalue -> T.rty -> V.adt_avalue -> T.rty -> V.typed_avalue - - (** Parameters: - [ty0] - [bid0] - [ty1] - [bid1] - [ty]: result of matching ty0 and ty1 - *) - val match_ashared_borrows : - T.rty -> V.borrow_id -> T.rty -> V.borrow_id -> T.rty -> V.typed_avalue - - (** Parameters: - [ty0] - [bid0] - [av0] - [ty1] - [bid1] - [av1] - [ty]: result of matching ty0 and ty1 - [av]: result of matching av0 and av1 - *) - val match_amut_borrows : - T.rty -> - V.borrow_id -> - V.typed_avalue -> - T.rty -> - V.borrow_id -> - V.typed_avalue -> - T.rty -> - V.typed_avalue -> - V.typed_avalue - - (** Parameters: - [ty0] - [ids0] - [v0] - [av0] - [ty1] - [ids1] - [v1] - [av1] - [ty]: result of matching ty0 and ty1 - [v]: result of matching v0 and v1 - [av]: result of matching av0 and av1 - *) - val match_ashared_loans : - T.rty -> - V.loan_id_set -> - V.typed_value -> - V.typed_avalue -> - T.rty -> - V.loan_id_set -> - V.typed_value -> - V.typed_avalue -> - T.rty -> - V.typed_value -> - V.typed_avalue -> - V.typed_avalue - - (** Parameters: - [ty0] - [id0] - [av0] - [ty1] - [id1] - [av1] - [ty]: result of matching ty0 and ty1 - [av]: result of matching av0 and av1 - *) - val match_amut_loans : - T.rty -> - V.borrow_id -> - V.typed_avalue -> - T.rty -> - V.borrow_id -> - V.typed_avalue -> - T.rty -> - V.typed_avalue -> - V.typed_avalue - - (** Match two arbitrary avalues whose constructors don't match (this function - is typically used to raise the proper exception). - *) - val match_avalues : V.typed_avalue -> V.typed_avalue -> V.typed_avalue -end - -(** Generic functor to implement matching functions between values, environments, - etc. - - We use it for joins, to check if two environments are convertible, etc. - See for instance {!MakeJoinMatcher} and {!MakeCheckEquivMatcher}. - - The functor is parameterized by a {!Matcher}, which implements the - non-generic part of the match. More precisely, the role of {!Match} is two - provide generic functions which recursively match two values (by recursively - matching the fields of ADT values for instance). When it does need to match - values in a non-trivial manner (if two ADT values don't have the same - variant for instance) it calls the corresponding specialized function from - {!Matcher}. - *) -module Match (M : Matcher) = struct - (** Match two values. - - Rem.: this function raises exceptions of type {!ValueMatchFailure}. - *) - let rec match_typed_values (ctx : C.eval_ctx) (v0 : V.typed_value) - (v1 : V.typed_value) : V.typed_value = - let match_rec = match_typed_values ctx in - let ty = M.match_etys v0.V.ty v1.V.ty in - match (v0.V.value, v1.V.value) with - | V.Primitive pv0, V.Primitive pv1 -> - if pv0 = pv1 then v1 else M.match_distinct_primitive_values ty pv0 pv1 - | V.Adt av0, V.Adt av1 -> - if av0.variant_id = av1.variant_id then - let fields = List.combine av0.field_values av1.field_values in - let field_values = - List.map (fun (f0, f1) -> match_rec f0 f1) fields - in - let value : V.value = - V.Adt { variant_id = av0.variant_id; field_values } - in - { V.value; ty = v1.V.ty } - else ( - (* For now, we don't merge ADTs which contain borrows *) - assert (not (value_has_borrows ctx v0.V.value)); - assert (not (value_has_borrows ctx v1.V.value)); - (* Merge *) - M.match_distinct_adts ty av0 av1) - | Bottom, Bottom -> v0 - | Borrow bc0, Borrow bc1 -> - let bc = - match (bc0, bc1) with - | SharedBorrow bid0, SharedBorrow bid1 -> - let bid = M.match_shared_borrows match_rec ty bid0 bid1 in - V.SharedBorrow bid - | MutBorrow (bid0, bv0), MutBorrow (bid1, bv1) -> - let bv = match_rec bv0 bv1 in - assert (not (value_has_borrows ctx bv.V.value)); - let bid, bv = M.match_mut_borrows ty bid0 bv0 bid1 bv1 bv in - V.MutBorrow (bid, bv) - | ReservedMutBorrow _, _ - | _, ReservedMutBorrow _ - | SharedBorrow _, MutBorrow _ - | MutBorrow _, SharedBorrow _ -> - (* If we get here, either there is a typing inconsistency, or we are - trying to match a reserved borrow, which shouldn't happen because - reserved borrow should be eliminated very quickly - they are introduced - just before function calls which activate them *) - raise (Failure "Unexpected") - in - { V.value = V.Borrow bc; ty } - | Loan lc0, Loan lc1 -> - (* TODO: maybe we should enforce that the ids are always exactly the same - - without matching *) - let lc = - match (lc0, lc1) with - | SharedLoan (ids0, sv0), SharedLoan (ids1, sv1) -> - let sv = match_rec sv0 sv1 in - assert (not (value_has_borrows ctx sv.V.value)); - let ids, sv = M.match_shared_loans ty ids0 ids1 sv in - V.SharedLoan (ids, sv) - | MutLoan id0, MutLoan id1 -> - let id = M.match_mut_loans ty id0 id1 in - V.MutLoan id - | SharedLoan _, MutLoan _ | MutLoan _, SharedLoan _ -> - raise (Failure "Unreachable") - in - { V.value = Loan lc; ty = v1.V.ty } - | Symbolic sv0, Symbolic sv1 -> - (* For now, we force all the symbolic values containing borrows to - be eagerly expanded, and we don't support nested borrows *) - assert (not (value_has_borrows ctx v0.V.value)); - assert (not (value_has_borrows ctx v1.V.value)); - (* Match *) - let sv = M.match_symbolic_values sv0 sv1 in - { v1 with V.value = V.Symbolic sv } - | Loan lc, _ -> ( - match lc with - | SharedLoan (ids, _) -> raise (ValueMatchFailure (LoansInLeft ids)) - | MutLoan id -> raise (ValueMatchFailure (LoanInLeft id))) - | _, Loan lc -> ( - match lc with - | SharedLoan (ids, _) -> raise (ValueMatchFailure (LoansInRight ids)) - | MutLoan id -> raise (ValueMatchFailure (LoanInRight id))) - | Symbolic sv, _ -> M.match_symbolic_with_other true sv v1 - | _, Symbolic sv -> M.match_symbolic_with_other false sv v0 - | Bottom, _ -> M.match_bottom_with_other true v1 - | _, Bottom -> M.match_bottom_with_other false v0 - | _ -> - log#ldebug - (lazy - ("Unexpected match case:\n- value0: " - ^ typed_value_to_string ctx v0 - ^ "\n- value1: " - ^ typed_value_to_string ctx v1)); - raise (Failure "Unexpected match case") - - (** Match two avalues. - - Rem.: this function raises exceptions of type {!ValueMatchFailure}. - *) - and match_typed_avalues (ctx : C.eval_ctx) (v0 : V.typed_avalue) - (v1 : V.typed_avalue) : V.typed_avalue = - log#ldebug - (lazy - ("match_typed_avalues:\n- value0: " - ^ typed_avalue_to_string ctx v0 - ^ "\n- value1: " - ^ typed_avalue_to_string ctx v1)); - - let match_rec = match_typed_values ctx in - let match_arec = match_typed_avalues ctx in - let ty = M.match_rtys v0.V.ty v1.V.ty in - match (v0.V.value, v1.V.value) with - | V.AAdt av0, V.AAdt av1 -> - if av0.variant_id = av1.variant_id then - let fields = List.combine av0.field_values av1.field_values in - let field_values = - List.map (fun (f0, f1) -> match_arec f0 f1) fields - in - let value : V.avalue = - V.AAdt { variant_id = av0.variant_id; field_values } - in - { V.value; ty } - else (* Merge *) - M.match_distinct_aadts v0.V.ty av0 v1.V.ty av1 ty - | ABottom, ABottom -> mk_abottom ty - | AIgnored, AIgnored -> mk_aignored ty - | ABorrow bc0, ABorrow bc1 -> ( - log#ldebug (lazy "match_typed_avalues: borrows"); - match (bc0, bc1) with - | ASharedBorrow bid0, ASharedBorrow bid1 -> - log#ldebug (lazy "match_typed_avalues: shared borrows"); - M.match_ashared_borrows v0.V.ty bid0 v1.V.ty bid1 ty - | AMutBorrow (bid0, av0), AMutBorrow (bid1, av1) -> - log#ldebug (lazy "match_typed_avalues: mut borrows"); - log#ldebug - (lazy - "match_typed_avalues: mut borrows: matching children values"); - let av = match_arec av0 av1 in - log#ldebug - (lazy "match_typed_avalues: mut borrows: matched children values"); - M.match_amut_borrows v0.V.ty bid0 av0 v1.V.ty bid1 av1 ty av - | AIgnoredMutBorrow _, AIgnoredMutBorrow _ -> - (* The abstractions are destructured: we shouldn't get there *) - raise (Failure "Unexpected") - | AProjSharedBorrow asb0, AProjSharedBorrow asb1 -> ( - match (asb0, asb1) with - | [], [] -> - (* This case actually stands for ignored shared borrows, when - there are no nested borrows *) - v0 - | _ -> - (* We should get there only if there are nested borrows *) - raise (Failure "Unexpected")) - | _ -> - (* TODO: getting there is not necessarily inconsistent (it may - just be because the environments don't match) so we may want - to call a specific function (which could raise the proper - exception). - Rem.: we shouldn't get to the ended borrow cases, because - an abstraction should never contain ended borrows unless - we are *currently* ending it, in which case we need - to completely end it before continuing. - *) - raise (Failure "Unexpected")) - | ALoan lc0, ALoan lc1 -> ( - log#ldebug (lazy "match_typed_avalues: loans"); - (* TODO: maybe we should enforce that the ids are always exactly the same - - without matching *) - match (lc0, lc1) with - | ASharedLoan (ids0, sv0, av0), ASharedLoan (ids1, sv1, av1) -> - log#ldebug (lazy "match_typed_avalues: shared loans"); - let sv = match_rec sv0 sv1 in - let av = match_arec av0 av1 in - assert (not (value_has_borrows ctx sv.V.value)); - M.match_ashared_loans v0.V.ty ids0 sv0 av0 v1.V.ty ids1 sv1 av1 ty - sv av - | AMutLoan (id0, av0), AMutLoan (id1, av1) -> - log#ldebug (lazy "match_typed_avalues: mut loans"); - log#ldebug - (lazy "match_typed_avalues: mut loans: matching children values"); - let av = match_arec av0 av1 in - log#ldebug - (lazy "match_typed_avalues: mut loans: matched children values"); - M.match_amut_loans v0.V.ty id0 av0 v1.V.ty id1 av1 ty av - | AIgnoredMutLoan _, AIgnoredMutLoan _ - | AIgnoredSharedLoan _, AIgnoredSharedLoan _ -> - (* Those should have been filtered when destructuring the abstractions - - they are necessary only when there are nested borrows *) - raise (Failure "Unreachable") - | _ -> raise (Failure "Unreachable")) - | ASymbolic _, ASymbolic _ -> - (* For now, we force all the symbolic values containing borrows to - be eagerly expanded, and we don't support nested borrows *) - raise (Failure "Unreachable") - | _ -> M.match_avalues v0 v1 -end - -(* Very annoying: functors only take modules as inputs... *) -module type MatchJoinState = sig - (** The current context *) - val ctx : C.eval_ctx - - (** The current loop *) - val loop_id : V.LoopId.id - - (** The abstractions introduced when performing the matches *) - val nabs : V.abs list ref -end - -(** A matcher for joins (we use joins to compute loop fixed points). - - See the explanations for {!Match}. - - In case of loop joins: - - we match *concrete* values - - we check that the "fixed" abstractions (the abstractions to be framed - - i.e., the abstractions which are the same in the two environments to - join) are equal - - we keep the abstractions which are not in the frame, then merge those - together (if they have borrows/loans in common) later - The join matcher is used to match the *concrete* values only. For this - reason, we fail on the functions which match avalues. - *) -module MakeJoinMatcher (S : MatchJoinState) : Matcher = struct - (** Small utility *) - let push_abs (abs : V.abs) : unit = S.nabs := abs :: !S.nabs - - let push_absl (absl : V.abs list) : unit = List.iter push_abs absl - - let match_etys ty0 ty1 = - assert (ty0 = ty1); - ty0 - - let match_rtys ty0 ty1 = - (* The types must be equal - in effect, this forbids to match symbolic - values containing borrows *) - assert (ty0 = ty1); - ty0 - - let match_distinct_primitive_values (ty : T.ety) (_ : V.primitive_value) - (_ : V.primitive_value) : V.typed_value = - mk_fresh_symbolic_typed_value_from_ety V.LoopJoin ty - - let match_distinct_adts (ty : T.ety) (adt0 : V.adt_value) (adt1 : V.adt_value) - : V.typed_value = - (* Check that the ADTs don't contain borrows - this is redundant with checks - performed by the caller, but we prefer to be safe with regards to future - updates - *) - let check_no_borrows (v : V.typed_value) = - assert (not (value_has_borrows S.ctx v.V.value)) - in - List.iter check_no_borrows adt0.field_values; - List.iter check_no_borrows adt1.field_values; - - (* Check if there are loans: we request to end them *) - let check_loans (left : bool) (fields : V.typed_value list) : unit = - match InterpreterBorrowsCore.get_first_loan_in_values fields with - | Some (V.SharedLoan (ids, _)) -> - if left then raise (ValueMatchFailure (LoansInLeft ids)) - else raise (ValueMatchFailure (LoansInRight ids)) - | Some (V.MutLoan id) -> - if left then raise (ValueMatchFailure (LoanInLeft id)) - else raise (ValueMatchFailure (LoanInRight id)) - | None -> () - in - check_loans true adt0.field_values; - check_loans false adt1.field_values; - - (* No borrows, no loans: we can introduce a symbolic value *) - mk_fresh_symbolic_typed_value_from_ety V.LoopJoin ty - - let match_shared_borrows _ (ty : T.ety) (bid0 : V.borrow_id) - (bid1 : V.borrow_id) : V.borrow_id = - if bid0 = bid1 then bid0 - else - (* We replace bid0 and bid1 with a fresh borrow id, and introduce - an abstraction which links all of them: - {[ - { SB bid0, SB bid1, SL {bid2} } - ]} - *) - let rid = C.fresh_region_id () in - let bid2 = C.fresh_borrow_id () in - - (* Generate a fresh symbolic value for the shared value *) - let _, bv_ty, kind = ty_as_ref ty in - let sv = mk_fresh_symbolic_typed_value_from_ety V.LoopJoin bv_ty in - - let borrow_ty = - mk_ref_ty (T.Var rid) (ety_no_regions_to_rty bv_ty) kind - in - - (* Generate the avalues for the abstraction *) - let mk_aborrow (bid : V.borrow_id) : V.typed_avalue = - let value = V.ABorrow (V.ASharedBorrow bid) in - { V.value; ty = borrow_ty } - in - let borrows = [ mk_aborrow bid0; mk_aborrow bid1 ] in - - let loan = - V.ASharedLoan - ( V.BorrowId.Set.singleton bid2, - sv, - mk_aignored (ety_no_regions_to_rty bv_ty) ) - in - (* Note that an aloan has a borrow type *) - let loan = { V.value = V.ALoan loan; ty = borrow_ty } in - - let avalues = List.append borrows [ loan ] in - - (* Generate the abstraction *) - let abs = - { - V.abs_id = C.fresh_abstraction_id (); - kind = V.Loop (S.loop_id, None, LoopSynthInput); - can_end = true; - parents = V.AbstractionId.Set.empty; - original_parents = []; - regions = T.RegionId.Set.singleton rid; - ancestors_regions = T.RegionId.Set.empty; - avalues; - } - in - push_abs abs; - - (* Return the new borrow *) - bid2 - - let match_mut_borrows (ty : T.ety) (bid0 : V.borrow_id) (bv0 : V.typed_value) - (bid1 : V.borrow_id) (bv1 : V.typed_value) (bv : V.typed_value) : - V.borrow_id * V.typed_value = - if bid0 = bid1 then ( - (* If the merged value is not the same as the original value, we introduce - an abstraction: - - {[ - { MB bid0, ML nbid } // where nbid fresh - ]} - - and we use bid' for the borrow id that we return. - - We do this because we want to make sure that, whenever a mutably - borrowed value is modified in a loop iteration, then there is - a fresh abstraction between this borrowed value and the fixed - abstractions. - *) - assert (not (value_has_borrows S.ctx bv.V.value)); - - if bv0 = bv1 then ( - assert (bv0 = bv); - (bid0, bv)) - else - let rid = C.fresh_region_id () in - let nbid = C.fresh_borrow_id () in - - let kind = T.Mut in - let bv_ty = ety_no_regions_to_rty bv.V.ty in - let borrow_ty = mk_ref_ty (T.Var rid) bv_ty kind in - - let borrow_av = - let ty = borrow_ty in - let value = V.ABorrow (V.AMutBorrow (bid0, mk_aignored bv_ty)) in - mk_typed_avalue ty value - in - - let loan_av = - let ty = borrow_ty in - let value = V.ALoan (V.AMutLoan (nbid, mk_aignored bv_ty)) in - mk_typed_avalue ty value - in - - let avalues = [ borrow_av; loan_av ] in - - (* Generate the abstraction *) - let abs = - { - V.abs_id = C.fresh_abstraction_id (); - kind = V.Loop (S.loop_id, None, LoopSynthInput); - can_end = true; - parents = V.AbstractionId.Set.empty; - original_parents = []; - regions = T.RegionId.Set.singleton rid; - ancestors_regions = T.RegionId.Set.empty; - avalues; - } - in - push_abs abs; - - (* Return the new borrow *) - (nbid, bv)) - else - (* We replace bid0 and bid1 with a fresh borrow id, and introduce - an abstraction which links all of them: - {[ - { MB bid0, MB bid1, ML bid2 } - ]} - *) - let rid = C.fresh_region_id () in - let bid2 = C.fresh_borrow_id () in - - (* Generate a fresh symbolic value for the borrowed value *) - let _, bv_ty, kind = ty_as_ref ty in - let sv = mk_fresh_symbolic_typed_value_from_ety V.LoopJoin bv_ty in - - let borrow_ty = - mk_ref_ty (T.Var rid) (ety_no_regions_to_rty bv_ty) kind - in - - (* Generate the avalues for the abstraction *) - let mk_aborrow (bid : V.borrow_id) (bv : V.typed_value) : V.typed_avalue = - let bv_ty = ety_no_regions_to_rty bv.V.ty in - let value = V.ABorrow (V.AMutBorrow (bid, mk_aignored bv_ty)) in - { V.value; ty = borrow_ty } - in - let borrows = [ mk_aborrow bid0 bv0; mk_aborrow bid1 bv1 ] in - - let loan = V.AMutLoan (bid2, mk_aignored (ety_no_regions_to_rty bv_ty)) in - (* Note that an aloan has a borrow type *) - let loan = { V.value = V.ALoan loan; ty = borrow_ty } in - - let avalues = List.append borrows [ loan ] in - - (* Generate the abstraction *) - let abs = - { - V.abs_id = C.fresh_abstraction_id (); - kind = V.Loop (S.loop_id, None, LoopSynthInput); - can_end = true; - parents = V.AbstractionId.Set.empty; - original_parents = []; - regions = T.RegionId.Set.singleton rid; - ancestors_regions = T.RegionId.Set.empty; - avalues; - } - in - push_abs abs; - - (* Return the new borrow *) - (bid2, sv) - - let match_shared_loans (_ : T.ety) (ids0 : V.loan_id_set) - (ids1 : V.loan_id_set) (sv : V.typed_value) : - V.loan_id_set * V.typed_value = - (* Check if the ids are the same - Rem.: we forbid the sets of loans - to be different. However, if we dive inside data-structures (by - using a shared borrow) the shared values might themselves contain - shared loans, which need to be matched. For this reason, we destructure - the shared values (see {!destructure_abs}). - *) - let extra_ids_left = V.BorrowId.Set.diff ids0 ids1 in - let extra_ids_right = V.BorrowId.Set.diff ids1 ids0 in - if not (V.BorrowId.Set.is_empty extra_ids_left) then - raise (ValueMatchFailure (LoansInLeft extra_ids_left)); - if not (V.BorrowId.Set.is_empty extra_ids_right) then - raise (ValueMatchFailure (LoansInRight extra_ids_right)); - - (* This should always be true if we get here *) - assert (ids0 = ids1); - let ids = ids0 in - - (* Return *) - (ids, sv) - - let match_mut_loans (_ : T.ety) (id0 : V.loan_id) (id1 : V.loan_id) : - V.loan_id = - if id0 = id1 then id0 - else - (* We forbid this case for now: if we get there, we force to end - both borrows *) - raise (ValueMatchFailure (LoanInLeft id0)) - - let match_symbolic_values (sv0 : V.symbolic_value) (sv1 : V.symbolic_value) : - V.symbolic_value = - let id0 = sv0.sv_id in - let id1 = sv1.sv_id in - if id0 = id1 then ( - (* Sanity check *) - assert (sv0 = sv1); - (* Return *) - sv0) - 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)); - (* We simply introduce a fresh symbolic value *) - mk_fresh_symbolic_value V.LoopJoin sv0.sv_ty) - - let match_symbolic_with_other (left : bool) (sv : V.symbolic_value) - (v : V.typed_value) : V.typed_value = - (* Check that: - - there are no borrows in the symbolic value - - 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 (value_has_borrows S.ctx v.V.value)); - let value_is_left = not left in - (match InterpreterBorrowsCore.get_first_loan_in_value v with - | None -> () - | Some (SharedLoan (ids, _)) -> - if value_is_left then raise (ValueMatchFailure (LoansInLeft ids)) - else raise (ValueMatchFailure (LoansInRight ids)) - | Some (MutLoan id) -> - if value_is_left then raise (ValueMatchFailure (LoanInLeft id)) - else raise (ValueMatchFailure (LoanInRight id))); - (* Return a fresh symbolic value *) - mk_fresh_symbolic_typed_value V.LoopJoin sv.sv_ty - - let match_bottom_with_other (left : bool) (v : V.typed_value) : V.typed_value - = - (* If there are outer loans in the non-bottom value, raise an exception. - Otherwise, convert it to an abstraction and return [Bottom]. - *) - let with_borrows = false in - let value_is_left = not left in - match - InterpreterBorrowsCore.get_first_outer_loan_or_borrow_in_value - with_borrows v - with - | Some (BorrowContent _) -> raise (Failure "Unreachable") - | Some (LoanContent lc) -> ( - match lc with - | V.SharedLoan (ids, _) -> - if value_is_left then raise (ValueMatchFailure (LoansInLeft ids)) - else raise (ValueMatchFailure (LoansInRight ids)) - | V.MutLoan id -> - if value_is_left then raise (ValueMatchFailure (LoanInLeft id)) - else raise (ValueMatchFailure (LoanInRight id))) - | None -> - (* Convert the value to an abstraction *) - let abs_kind = V.Loop (S.loop_id, None, LoopSynthInput) in - let can_end = true in - let destructure_shared_values = true in - let absl = - convert_value_to_abstractions abs_kind can_end - destructure_shared_values S.ctx v - in - push_absl absl; - (* Return [Bottom] *) - mk_bottom v.V.ty - - (* As explained in comments: we don't use the join matcher to join avalues, - only concrete values *) - - let match_distinct_aadts _ _ _ _ _ = raise (Failure "Unreachable") - let match_ashared_borrows _ _ _ _ = raise (Failure "Unreachable") - let match_amut_borrows _ _ _ _ _ _ _ _ = raise (Failure "Unreachable") - let match_ashared_loans _ _ _ _ _ _ _ _ _ _ _ = raise (Failure "Unreachable") - let match_amut_loans _ _ _ _ _ _ _ _ = raise (Failure "Unreachable") - let match_avalues _ _ = raise (Failure "Unreachable") -end - -let mk_collapse_ctx_merge_duplicate_funs (loop_id : V.LoopId.id) - (ctx : C.eval_ctx) : merge_duplicates_funcs = - (* Rem.: the merge functions raise exceptions (that we catch). *) - let module S : MatchJoinState = struct - let ctx = ctx - let loop_id = loop_id - let nabs = ref [] - end in - let module JM = MakeJoinMatcher (S) in - let module M = Match (JM) in - (* Functions to match avalues (see {!merge_duplicates_funcs}). - - Those functions are used to merge borrows/loans with the *same ids*. - - They will always be called on destructured avalues (whose children are - [AIgnored] - we enforce that through sanity checks). We rely on the join - matcher [JM] to match the concrete values (for shared loans for instance). - Note that the join matcher doesn't implement match functions for avalues - (see the comments in {!MakeJoinMatcher}. - *) - let merge_amut_borrows id ty0 child0 _ty1 child1 = - (* Sanity checks *) - assert (is_aignored child0.V.value); - assert (is_aignored child1.V.value); - - (* We need to pick a type for the avalue. The types on the left and on the - right may use different regions: it doesn't really matter (here, we pick - the one from the left), because we will merge those regions together - anyway (see the comments for {!merge_into_abstraction}). - *) - let ty = ty0 in - let child = child0 in - let value = V.ABorrow (V.AMutBorrow (id, child)) in - { V.value; ty } - in - - let merge_ashared_borrows id ty0 ty1 = - (* Sanity checks *) - 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)) - in - - (* Same remarks as for [merge_amut_borrows] *) - let ty = ty0 in - let value = V.ABorrow (V.ASharedBorrow id) in - { V.value; ty } - in - - let merge_amut_loans id ty0 child0 _ty1 child1 = - (* Sanity checks *) - assert (is_aignored child0.V.value); - assert (is_aignored child1.V.value); - (* Same remarks as for [merge_amut_borrows] *) - let ty = ty0 in - let child = child0 in - let value = V.ALoan (V.AMutLoan (id, child)) in - { V.value; ty } - in - let merge_ashared_loans ids ty0 (sv0 : V.typed_value) child0 _ty1 - (sv1 : V.typed_value) child1 = - (* Sanity checks *) - assert (is_aignored child0.V.value); - assert (is_aignored child1.V.value); - (* Same remarks as for [merge_amut_borrows]. - - This time we need to also merge the shared values. We rely on the - join matcher [JM] to do so. - *) - assert (not (value_has_loans_or_borrows ctx sv0.V.value)); - assert (not (value_has_loans_or_borrows ctx sv1.V.value)); - let ty = ty0 in - let child = child0 in - let sv = M.match_typed_values ctx sv0 sv1 in - let value = V.ALoan (V.ASharedLoan (ids, sv, child)) in - { V.value; ty } - in - { - merge_amut_borrows; - merge_ashared_borrows; - merge_amut_loans; - merge_ashared_loans; - } - -let merge_into_abstraction (loop_id : V.LoopId.id) (abs_kind : V.abs_kind) - (can_end : bool) (ctx : C.eval_ctx) (aid0 : V.AbstractionId.id) - (aid1 : V.AbstractionId.id) : C.eval_ctx * V.AbstractionId.id = - let merge_funs = mk_collapse_ctx_merge_duplicate_funs loop_id ctx in - merge_into_abstraction abs_kind can_end (Some merge_funs) ctx aid0 aid1 - -(** Collapse an environment, merging the duplicated borrows/loans. - - This function simply calls {!collapse_ctx} with the proper merging functions. - - We do this because when we join environments, we may introduce duplicated - loans and borrows. See the explanations for {!join_ctxs}. - *) -let collapse_ctx_with_merge (loop_id : V.LoopId.id) (old_ids : ids_sets) - (ctx : C.eval_ctx) : C.eval_ctx = - let merge_funs = mk_collapse_ctx_merge_duplicate_funs loop_id ctx in - try collapse_ctx loop_id (Some merge_funs) old_ids ctx - with ValueMatchFailure _ -> raise (Failure "Unexpected") - -(** Join two contexts. - - We use this to join the environments at loop (re-)entry to progressively - compute a fixed point. - - We make the hypothesis (and check it) that the environments have the same - prefixes (same variable ids, same abstractions, etc.). The prefix of - variable and abstraction ids is given by the [fixed_ids] identifier sets. We - check that those prefixes are the same (the dummy variables are the same, - the abstractions are the same), match the values mapped to by the variables - which are not dummy, then group the additional dummy variables/abstractions - together. In a sense, the [fixed_ids] define a frame (in a separation logic - sense). - - Note that when joining the values mapped to by the non-dummy variables, we - may introduce duplicated borrows. Also, we don't match the abstractions - which are not in the prefix, and this can also lead to borrow - duplications. For this reason, the environment needs to be collapsed - afterwards to get rid of those duplicated loans/borrows. - - For instance, if we have: - {[ - fixed = { abs0 } - - env0 = { - abs0 { ML l0 } - l -> MB l0 s0 - } - - env1 = { - abs0 { ML l0 } - l -> MB l1 s1 - abs1 { MB l0, ML l1 } - } - ]} - - We get: - {[ - join env0 env1 = { - abs0 { ML l0 } (* abs0 is fixed: we simply check it is equal in env0 and env1 *) - l -> MB l2 s2 - abs1 { MB l0, ML l1 } (* abs1 is new: we keep it unchanged *) - abs2 { MB l0, MB l1, ML l2 } (* Introduced when joining on the "l" variable *) - } - ]} - - Rem.: in practice, this join works because we take care of pushing new values - and abstractions *at the end* of the environments, meaning the environment - prefixes keep the same structure. - - Rem.: assuming that the environment has some structure poses *no soundness - issue*. It can only make the join fail if the environments actually don't have - this structure: this is a *completeness issue*. - *) -let join_ctxs (loop_id : V.LoopId.id) (fixed_ids : ids_sets) (ctx0 : C.eval_ctx) - (ctx1 : C.eval_ctx) : ctx_or_update = - (* Debug *) - log#ldebug - (lazy - ("join_ctxs:\n\n- fixed_ids:\n" ^ show_ids_sets fixed_ids - ^ "\n\n- ctx0:\n" - ^ eval_ctx_to_string_no_filter ctx0 - ^ "\n\n- ctx1:\n" - ^ eval_ctx_to_string_no_filter ctx1 - ^ "\n\n")); - - let env0 = List.rev ctx0.env in - let env1 = List.rev ctx1.env in - - (* We need to pick a context for some functions like [match_typed_values]: - the context is only used to lookup module data, so we can pick whichever - we want. - TODO: this is not very clean. Maybe we should just carry this data around. - *) - let ctx = ctx0 in - - let nabs = ref [] in - - (* Explore the environments. *) - let join_suffixes (env0 : C.env) (env1 : C.env) : C.env = - (* Debug *) - log#ldebug - (lazy - ("join_suffixes:\n\n- fixed_ids:\n" ^ show_ids_sets fixed_ids - ^ "\n\n- ctx0:\n" - ^ eval_ctx_to_string_no_filter { ctx0 with env = List.rev env0 } - ^ "\n\n- ctx1:\n" - ^ eval_ctx_to_string_no_filter { ctx1 with env = List.rev env1 } - ^ "\n\n")); - - (* Sanity check: there are no values/abstractions which should be in the prefix *) - let check_valid (ee : C.env_elem) : unit = - match ee with - | C.Var (C.VarBinder _, _) -> - (* Variables are necessarily in the prefix *) - raise (Failure "Unreachable") - | Var (C.DummyBinder did, _) -> - assert (not (C.DummyVarId.Set.mem did fixed_ids.dids)) - | Abs abs -> - assert (not (V.AbstractionId.Set.mem abs.abs_id fixed_ids.aids)) - | Frame -> - (* This should have been eliminated *) - raise (Failure "Unreachable") - in - List.iter check_valid env0; - List.iter check_valid env1; - (* Concatenate the suffixes and append the abstractions introduced while - joining the prefixes *) - let absl = List.map (fun abs -> C.Abs abs) (List.rev !nabs) in - List.concat [ env0; env1; absl ] - in - - let module S : MatchJoinState = struct - (* The context is only used to lookup module data: we can pick whichever we want *) - let ctx = ctx - let loop_id = loop_id - let nabs = nabs - end in - let module JM = MakeJoinMatcher (S) in - let module M = Match (JM) in - (* Rem.: this function raises exceptions *) - let rec join_prefixes (env0 : C.env) (env1 : C.env) : C.env = - match (env0, env1) with - | ( (C.Var (C.DummyBinder b0, v0) as var0) :: env0', - (C.Var (C.DummyBinder b1, v1) as var1) :: env1' ) -> - (* Debug *) - log#ldebug - (lazy - ("join_prefixes: DummyBinders:\n\n- fixed_ids:\n" ^ "\n" - ^ show_ids_sets fixed_ids ^ "\n\n- value0:\n" - ^ env_elem_to_string ctx var0 - ^ "\n\n- value1:\n" - ^ env_elem_to_string ctx var1 - ^ "\n\n")); - - (* Two cases: the dummy value is an old value, in which case the bindings - must be the same and we must join their values. Otherwise, it means we - are not in the prefix anymore *) - if C.DummyVarId.Set.mem b0 fixed_ids.dids then ( - (* Still in the prefix: match the values *) - assert (b0 = b1); - let b = b0 in - let v = M.match_typed_values ctx v0 v1 in - let var = C.Var (C.DummyBinder b, v) in - (* Continue *) - var :: join_prefixes env0' env1') - else (* Not in the prefix anymore *) - join_suffixes env0 env1 - | ( (C.Var (C.VarBinder b0, v0) as var0) :: env0', - (C.Var (C.VarBinder b1, v1) as var1) :: env1' ) -> - (* Debug *) - log#ldebug - (lazy - ("join_prefixes: VarBinders:\n\n- fixed_ids:\n" ^ "\n" - ^ show_ids_sets fixed_ids ^ "\n\n- value0:\n" - ^ env_elem_to_string ctx var0 - ^ "\n\n- value1:\n" - ^ env_elem_to_string ctx var1 - ^ "\n\n")); - - (* Variable bindings *must* be in the prefix and consequently their - ids must be the same *) - assert (b0 = b1); - (* Match the values *) - let b = b0 in - let v = M.match_typed_values ctx v0 v1 in - let var = C.Var (C.VarBinder b, v) in - (* Continue *) - var :: join_prefixes env0' env1' - | (C.Abs abs0 as abs) :: env0', C.Abs abs1 :: env1' -> - (* Debug *) - log#ldebug - (lazy - ("join_prefixes: Abs:\n\n- fixed_ids:\n" ^ "\n" - ^ show_ids_sets fixed_ids ^ "\n\n- abs0:\n" ^ abs_to_string ctx abs0 - ^ "\n\n- abs1:\n" ^ abs_to_string ctx abs1 ^ "\n\n")); - - (* Same as for the dummy values: there are two cases *) - if V.AbstractionId.Set.mem abs0.abs_id fixed_ids.aids then ( - (* Still in the prefix: the abstractions must be the same *) - assert (abs0 = abs1); - (* Continue *) - abs :: join_prefixes env0' env1') - else (* Not in the prefix anymore *) - join_suffixes env0 env1 - | _ -> - (* The elements don't match: we are not in the prefix anymore *) - join_suffixes env0 env1 - in - - try - (* Remove the frame delimiter (the first element of an environment is a frame delimiter) *) - let env0, env1 = - match (env0, env1) with - | C.Frame :: env0, C.Frame :: env1 -> (env0, env1) - | _ -> raise (Failure "Unreachable") - in - - log#ldebug - (lazy - ("- env0:\n" ^ C.show_env env0 ^ "\n\n- env1:\n" ^ C.show_env env1 - ^ "\n\n")); - - let env = List.rev (C.Frame :: join_prefixes env0 env1) in - - (* Construct the joined context - of course, the type, fun, etc. contexts - * should be the same in the two contexts *) - let { - C.type_context; - fun_context; - global_context; - region_groups; - type_vars; - env = _; - ended_regions = ended_regions0; - } = - ctx0 - in - let { - C.type_context = _; - fun_context = _; - global_context = _; - region_groups = _; - type_vars = _; - env = _; - ended_regions = ended_regions1; - } = - ctx1 - in - let ended_regions = T.RegionId.Set.union ended_regions0 ended_regions1 in - Ok - { - C.type_context; - fun_context; - global_context; - region_groups; - type_vars; - env; - ended_regions; - } - with ValueMatchFailure e -> Error e - -(** See {!MakeCheckEquivMatcher}. - - Very annoying: functors only take modules as inputs... - *) -module type MatchCheckEquivState = sig - (** [true] if we check equivalence between contexts, [false] if we match - a source context with a target context. *) - val check_equiv : bool - - val ctx : C.eval_ctx - val rid_map : T.RegionId.InjSubst.t ref - - (** Substitution for the loan and borrow ids - used only if [check_equiv] is true *) - val blid_map : V.BorrowId.InjSubst.t ref - - (** Substitution for the borrow ids - used only if [check_equiv] is false *) - val borrow_id_map : V.BorrowId.InjSubst.t ref - - (** Substitution for the loans ids - used only if [check_equiv] is false *) - val loan_id_map : V.BorrowId.InjSubst.t ref - - val sid_map : V.SymbolicValueId.InjSubst.t ref - val sid_to_value_map : V.typed_value V.SymbolicValueId.Map.t ref - val aid_map : V.AbstractionId.InjSubst.t ref - val lookup_shared_value_in_ctx0 : V.BorrowId.id -> V.typed_value - val lookup_shared_value_in_ctx1 : V.BorrowId.id -> V.typed_value -end - -(** An auxiliary matcher that we use for two purposes: - - to check if two contexts are equivalent modulo id substitution (i.e., - alpha equivalent) (see {!ctxs_are_equivalent}). - - to compute a mapping between the borrows and the symbolic values in a - target context to the values and borrows in a source context (see - {!match_ctx_with_target}). - - TODO: rename - *) -module MakeCheckEquivMatcher (S : MatchCheckEquivState) = struct - module MkGetSetM (Id : Identifiers.Id) = struct - module Inj = Id.InjSubst - - let add (msg : string) (m : Inj.t ref) (k0 : Id.id) (k1 : Id.id) = - (* Check if k0 is already registered as a key *) - match Inj.find_opt k0 !m with - | None -> - (* Not registered: check if k1 is in the set of values, - otherwise add the binding *) - if Inj.Set.mem k1 (Inj.elements !m) then - raise - (Distinct - (msg ^ "adding [k0=" ^ Id.to_string k0 ^ " -> k1=" - ^ Id.to_string k1 ^ " ]: k1 already in the set of elements")) - else ( - m := Inj.add k0 k1 !m; - k1) - | Some k1' -> - (* It is: check that the bindings are consistent *) - if k1 <> k1' then raise (Distinct (msg ^ "already a binding for k0")) - else k1 - - let match_e (msg : string) (m : Inj.t ref) (k0 : Id.id) (k1 : Id.id) : Id.id - = - (* TODO: merge the add and merge functions *) - add msg m k0 k1 - - let match_el (msg : string) (m : Inj.t ref) (kl0 : Id.id list) - (kl1 : Id.id list) : Id.id list = - List.map (fun (k0, k1) -> match_e msg m k0 k1) (List.combine kl0 kl1) - - (** Figuring out mappings between sets of ids is hard in all generality... - We use the fact that the fresh ids should have been generated - the same way (i.e., in the same order) and match the ids two by - two in increasing order. - *) - let match_es (msg : string) (m : Inj.t ref) (ks0 : Id.Set.t) - (ks1 : Id.Set.t) : Id.Set.t = - Id.Set.of_list - (match_el msg m (Id.Set.elements ks0) (Id.Set.elements ks1)) - end - - module GetSetRid = MkGetSetM (T.RegionId) - - let match_rid = GetSetRid.match_e "match_rid: " S.rid_map - - (* let match_ridl = GetSetRid.match_el S.rid_map *) - let match_rids = GetSetRid.match_es "match_rids: " S.rid_map - - module GetSetBid = MkGetSetM (V.BorrowId) - - let match_blid msg = GetSetBid.match_e msg S.blid_map - let match_blidl msg = GetSetBid.match_el msg S.blid_map - let match_blids msg = GetSetBid.match_es msg S.blid_map - - let match_borrow_id = - if S.check_equiv then match_blid "match_borrow_id: " - else GetSetBid.match_e "match_borrow_id: " S.borrow_id_map - - let match_borrow_idl = - if S.check_equiv then match_blidl "match_borrow_idl: " - else GetSetBid.match_el "match_borrow_idl: " S.borrow_id_map - - let match_borrow_ids = - if S.check_equiv then match_blids "match_borrow_ids: " - else GetSetBid.match_es "match_borrow_ids: " S.borrow_id_map - - let match_loan_id = - if S.check_equiv then match_blid "match_loan_id: " - else GetSetBid.match_e "match_loan_id: " S.loan_id_map - - let match_loan_idl = - if S.check_equiv then match_blidl "match_loan_idl: " - else GetSetBid.match_el "match_loan_idl: " S.loan_id_map - - let match_loan_ids = - if S.check_equiv then match_blids "match_loan_ids: " - else GetSetBid.match_es "match_loan_ids: " S.loan_id_map - - module GetSetSid = MkGetSetM (V.SymbolicValueId) - module GetSetAid = MkGetSetM (V.AbstractionId) - - let match_aid = GetSetAid.match_e "match_aid: " S.aid_map - let match_aidl = GetSetAid.match_el "match_aidl: " S.aid_map - let match_aids = GetSetAid.match_es "match_aids: " S.aid_map - - (** *) - let match_etys ty0 ty1 = - if ty0 <> ty1 then raise (Distinct "match_etys") else ty0 - - let match_rtys ty0 ty1 = - let match_distinct_types _ _ = raise (Distinct "match_rtys") in - let match_regions r0 r1 = - match (r0, r1) with - | T.Static, T.Static -> r1 - | Var rid0, Var rid1 -> - let rid = match_rid rid0 rid1 in - Var rid - | _ -> raise (Distinct "match_rtys") - in - match_types match_distinct_types match_regions ty0 ty1 - - let match_distinct_primitive_values (ty : T.ety) (_ : V.primitive_value) - (_ : V.primitive_value) : V.typed_value = - mk_fresh_symbolic_typed_value_from_ety V.LoopJoin ty - - let match_distinct_adts (_ty : T.ety) (_adt0 : V.adt_value) - (_adt1 : V.adt_value) : V.typed_value = - raise (Distinct "match_distinct_adts") - - let match_shared_borrows - (match_typed_values : V.typed_value -> V.typed_value -> V.typed_value) - (_ty : T.ety) (bid0 : V.borrow_id) (bid1 : V.borrow_id) : V.borrow_id = - log#ldebug - (lazy - ("MakeCheckEquivMatcher: match_shared_borrows: " ^ "bid0: " - ^ V.BorrowId.to_string bid0 ^ ", bid1: " ^ V.BorrowId.to_string bid1)); - - let bid = match_borrow_id bid0 bid1 in - (* If we don't check for equivalence (i.e., we apply a fixed-point), - we lookup the shared values and match them. - *) - let _ = - if S.check_equiv then () - else - let v0 = S.lookup_shared_value_in_ctx0 bid0 in - let v1 = S.lookup_shared_value_in_ctx1 bid1 in - log#ldebug - (lazy - ("MakeCheckEquivMatcher: match_shared_borrows: looked up values:" - ^ "sv0: " - ^ typed_value_to_string S.ctx v0 - ^ ", sv1: " - ^ typed_value_to_string S.ctx v1)); - - let _ = match_typed_values v0 v1 in - () - in - bid - - let match_mut_borrows (_ty : T.ety) (bid0 : V.borrow_id) - (_bv0 : V.typed_value) (bid1 : V.borrow_id) (_bv1 : V.typed_value) - (bv : V.typed_value) : V.borrow_id * V.typed_value = - let bid = match_borrow_id bid0 bid1 in - (bid, bv) - - let match_shared_loans (_ : T.ety) (ids0 : V.loan_id_set) - (ids1 : V.loan_id_set) (sv : V.typed_value) : - V.loan_id_set * V.typed_value = - let ids = match_loan_ids ids0 ids1 in - (ids, sv) - - let match_mut_loans (_ : T.ety) (bid0 : V.loan_id) (bid1 : V.loan_id) : - V.loan_id = - match_loan_id bid0 bid1 - - let match_symbolic_values (sv0 : V.symbolic_value) (sv1 : V.symbolic_value) : - V.symbolic_value = - let id0 = sv0.sv_id in - let id1 = sv1.sv_id in - - log#ldebug - (lazy - ("MakeCheckEquivMatcher: match_symbolic_values: " ^ "sv0: " - ^ V.SymbolicValueId.to_string id0 - ^ ", sv1: " - ^ V.SymbolicValueId.to_string id1)); - - (* If we don't check for equivalence, we also update the map from sids - to values *) - if S.check_equiv then - (* Create the joined symbolic value *) - let sv_id = - GetSetSid.match_e "match_symbolic_values: ids: " S.sid_map id0 id1 - in - let sv_ty = match_rtys sv0.V.sv_ty sv1.V.sv_ty in - let sv_kind = - if sv0.V.sv_kind = sv1.V.sv_kind then sv0.V.sv_kind - else raise (Distinct "match_symbolic_values: sv_kind") - in - let sv = { V.sv_id; sv_ty; sv_kind } in - sv - else ( - (* Check: fixed values are fixed *) - assert (id0 = id1 || not (V.SymbolicValueId.InjSubst.mem id0 !S.sid_map)); - - (* Update the symbolic value mapping *) - let sv1 = mk_typed_value_from_symbolic_value sv1 in - - (* Update the symbolic value mapping *) - S.sid_to_value_map := - V.SymbolicValueId.Map.add_strict id0 sv1 !S.sid_to_value_map; - - (* Return - the returned value is not used: we can return whatever - we want *) - sv0) - - let match_symbolic_with_other (left : bool) (sv : V.symbolic_value) - (v : V.typed_value) : V.typed_value = - if S.check_equiv then raise (Distinct "match_symbolic_with_other") - else ( - assert left; - let id = sv.sv_id in - (* Check: fixed values are fixed *) - assert (not (V.SymbolicValueId.InjSubst.mem id !S.sid_map)); - (* Update the binding for the target symbolic value *) - S.sid_to_value_map := - V.SymbolicValueId.Map.add_strict id v !S.sid_to_value_map; - (* Return - the returned value is not used, so we can return whatever we want *) - v) - - let match_bottom_with_other (left : bool) (v : V.typed_value) : V.typed_value - = - (* It can happen that some variables get initialized in some branches - and not in some others, which causes problems when matching. *) - (* TODO: the returned value is not used, while it should: in generality it - should be ok to match a fixed-point with the environment we get at - a continue, where the fixed point contains some bottom values. *) - if left && not (value_has_loans_or_borrows S.ctx v.V.value) then - mk_bottom v.V.ty - else raise (Distinct "match_bottom_with_other") - - let match_distinct_aadts _ _ _ _ _ = raise (Distinct "match_distinct_adts") - - let match_ashared_borrows _ty0 bid0 _ty1 bid1 ty = - let bid = match_borrow_id bid0 bid1 in - let value = V.ABorrow (V.ASharedBorrow bid) in - { V.value; ty } - - let match_amut_borrows _ty0 bid0 _av0 _ty1 bid1 _av1 ty av = - let bid = match_borrow_id bid0 bid1 in - let value = V.ABorrow (V.AMutBorrow (bid, av)) in - { V.value; ty } - - let match_ashared_loans _ty0 ids0 _v0 _av0 _ty1 ids1 _v1 _av1 ty v av = - let bids = match_loan_ids ids0 ids1 in - let value = V.ALoan (V.ASharedLoan (bids, v, av)) in - { V.value; ty } - - let match_amut_loans _ty0 id0 _av0 _ty1 id1 _av1 ty av = - log#ldebug - (lazy - ("MakeCheckEquivMatcher:match_amut_loans:" ^ "\n- id0: " - ^ V.BorrowId.to_string id0 ^ "\n- id1: " ^ V.BorrowId.to_string id1 - ^ "\n- ty: " ^ rty_to_string S.ctx ty ^ "\n- av: " - ^ typed_avalue_to_string S.ctx av)); - - let id = match_loan_id id0 id1 in - let value = V.ALoan (V.AMutLoan (id, av)) in - { V.value; ty } - - let match_avalues v0 v1 = - log#ldebug - (lazy - ("avalues don't match:\n- v0: " - ^ typed_avalue_to_string S.ctx v0 - ^ "\n- v1: " - ^ typed_avalue_to_string S.ctx v1)); - raise (Distinct "match_avalues") -end - -(** See {!match_ctxs} *) -type ids_maps = { - aid_map : V.AbstractionId.InjSubst.t; - blid_map : V.BorrowId.InjSubst.t; - (** Substitution for the loan and borrow ids *) - borrow_id_map : V.BorrowId.InjSubst.t; (** Substitution for the borrow ids *) - loan_id_map : V.BorrowId.InjSubst.t; (** Substitution for the loan ids *) - rid_map : T.RegionId.InjSubst.t; - sid_map : V.SymbolicValueId.InjSubst.t; - sid_to_value_map : V.typed_value V.SymbolicValueId.Map.t; -} -[@@deriving show] - -(** Compute whether two contexts are equivalent modulo an identifier substitution. - - [fixed_ids]: ids for which we force the mapping to be the identity. - - We also take advantage of the structure of the environments, which should - have the same prefixes (we check it). See the explanations for {!join_ctxs}. - - TODO: explanations. - - [check_equiv]: if [true], check if the two contexts are equivalent. - If [false], compute a mapping from the first context to the second context, - in the sense of [match_ctx_with_target]. - - The lookup functions are used to match the shared values when [check_equiv] - is [false] (we sometimes use [match_ctxs] on partial environments, meaning - we have to lookup the shared values in the complete environment, otherwise - we miss some mappings). - - We return an optional ids map: [Some] if the match succeeded, [None] otherwise. - *) -let match_ctxs (check_equiv : bool) (fixed_ids : ids_sets) - (lookup_shared_value_in_ctx0 : V.BorrowId.id -> V.typed_value) - (lookup_shared_value_in_ctx1 : V.BorrowId.id -> V.typed_value) - (ctx0 : C.eval_ctx) (ctx1 : C.eval_ctx) : ids_maps option = - log#ldebug - (lazy - ("match_ctxs:\n\n- fixed_ids:\n" ^ show_ids_sets fixed_ids - ^ "\n\n- ctx0:\n" - ^ eval_ctx_to_string_no_filter ctx0 - ^ "\n\n- ctx1:\n" - ^ eval_ctx_to_string_no_filter ctx1 - ^ "\n\n")); - - (* Initialize the maps and instantiate the matcher *) - let module IdMap (Id : Identifiers.Id) = struct - let mk_map_ref (ids : Id.Set.t) : Id.InjSubst.t ref = - ref - (Id.InjSubst.of_list (List.map (fun x -> (x, x)) (Id.Set.elements ids))) - end in - let rid_map = - let module IdMap = IdMap (T.RegionId) in - IdMap.mk_map_ref fixed_ids.rids - in - let blid_map = - let module IdMap = IdMap (V.BorrowId) in - IdMap.mk_map_ref fixed_ids.blids - in - let borrow_id_map = - let module IdMap = IdMap (V.BorrowId) in - IdMap.mk_map_ref fixed_ids.borrow_ids - in - let loan_id_map = - let module IdMap = IdMap (V.BorrowId) in - IdMap.mk_map_ref fixed_ids.loan_ids - in - let aid_map = - let module IdMap = IdMap (V.AbstractionId) in - IdMap.mk_map_ref fixed_ids.aids - in - let sid_map = - let module IdMap = IdMap (V.SymbolicValueId) in - IdMap.mk_map_ref fixed_ids.sids - in - (* In case we don't try to check equivalence but want to compute a mapping - from a source context to a target context, we use a map from symbolic - value ids to values (rather than to ids). - *) - let sid_to_value_map : V.typed_value V.SymbolicValueId.Map.t ref = - ref V.SymbolicValueId.Map.empty - in - - let module S : MatchCheckEquivState = struct - let check_equiv = check_equiv - let ctx = ctx0 - let rid_map = rid_map - let blid_map = blid_map - let borrow_id_map = borrow_id_map - let loan_id_map = loan_id_map - let sid_map = sid_map - let sid_to_value_map = sid_to_value_map - let aid_map = aid_map - let lookup_shared_value_in_ctx0 = lookup_shared_value_in_ctx0 - let lookup_shared_value_in_ctx1 = lookup_shared_value_in_ctx1 - end in - let module CEM = MakeCheckEquivMatcher (S) in - let module M = Match (CEM) in - (* Match the environments - we assume that they have the same structure - (and fail if they don't) *) - - (* Small utility: check that ids are fixed/mapped to themselves *) - let ids_are_fixed (ids : ids_sets) : bool = - let { aids; blids = _; borrow_ids; loan_ids; dids; rids; sids } = ids in - V.AbstractionId.Set.subset aids fixed_ids.aids - && V.BorrowId.Set.subset borrow_ids fixed_ids.borrow_ids - && V.BorrowId.Set.subset loan_ids fixed_ids.loan_ids - && C.DummyVarId.Set.subset dids fixed_ids.dids - && T.RegionId.Set.subset rids fixed_ids.rids - && V.SymbolicValueId.Set.subset sids fixed_ids.sids - in - - (* We need to pick a context for some functions like [match_typed_values]: - the context is only used to lookup module data, so we can pick whichever - we want. - TODO: this is not very clean. Maybe we should just carry the relevant data - (i.e.e, not the whole context) around. - *) - let ctx = ctx0 in - - (* Rem.: this function raises exceptions of type [Distinct] *) - let match_abstractions (abs0 : V.abs) (abs1 : V.abs) : unit = - let { - V.abs_id = abs_id0; - kind = kind0; - can_end = can_end0; - parents = parents0; - original_parents = original_parents0; - regions = regions0; - ancestors_regions = ancestors_regions0; - avalues = avalues0; - } = - abs0 - in - - let { - V.abs_id = abs_id1; - kind = kind1; - can_end = can_end1; - parents = parents1; - original_parents = original_parents1; - regions = regions1; - ancestors_regions = ancestors_regions1; - avalues = avalues1; - } = - abs1 - in - - let _ = CEM.match_aid abs_id0 abs_id1 in - if kind0 <> kind1 || can_end0 <> can_end1 then - raise (Distinct "match_abstractions: kind or can_end"); - let _ = CEM.match_aids parents0 parents1 in - let _ = CEM.match_aidl original_parents0 original_parents1 in - let _ = CEM.match_rids regions0 regions1 in - let _ = CEM.match_rids ancestors_regions0 ancestors_regions1 in - - log#ldebug (lazy "match_abstractions: matching values"); - let _ = - List.map - (fun (v0, v1) -> M.match_typed_avalues ctx v0 v1) - (List.combine avalues0 avalues1) - in - log#ldebug (lazy "match_abstractions: values matched OK"); - () - in - - (* Rem.: this function raises exceptions of type [Distinct] *) - let rec match_envs (env0 : C.env) (env1 : C.env) : unit = - log#ldebug - (lazy - ("match_ctxs: match_envs:\n\n- fixed_ids:\n" ^ show_ids_sets fixed_ids - ^ "\n\n- rid_map: " - ^ T.RegionId.InjSubst.show_t !rid_map - ^ "\n- blid_map: " - ^ V.BorrowId.InjSubst.show_t !blid_map - ^ "\n- sid_map: " - ^ V.SymbolicValueId.InjSubst.show_t !sid_map - ^ "\n- aid_map: " - ^ V.AbstractionId.InjSubst.show_t !aid_map - ^ "\n\n- ctx0:\n" - ^ eval_ctx_to_string_no_filter { ctx0 with env = List.rev env0 } - ^ "\n\n- ctx1:\n" - ^ eval_ctx_to_string_no_filter { ctx1 with env = List.rev env1 } - ^ "\n\n")); - - match (env0, env1) with - | ( C.Var (C.DummyBinder b0, v0) :: env0', - C.Var (C.DummyBinder b1, v1) :: env1' ) -> - (* Sanity check: if the dummy value is an old value, the bindings must - be the same and their values equal (and the borrows/loans/symbolic *) - if C.DummyVarId.Set.mem b0 fixed_ids.dids then ( - (* Fixed values: the values must be equal *) - assert (b0 = b1); - assert (v0 = v1); - (* The ids present in the left value must be fixed *) - let ids, _ = compute_typed_value_ids v0 in - assert ((not S.check_equiv) || ids_are_fixed ids)); - (* We still match the values - allows to compute mappings (which - are the identity actually) *) - let _ = M.match_typed_values ctx v0 v1 in - match_envs env0' env1' - | C.Var (C.VarBinder b0, v0) :: env0', C.Var (C.VarBinder b1, v1) :: env1' - -> - assert (b0 = b1); - (* Match the values *) - let _ = M.match_typed_values ctx v0 v1 in - (* Continue *) - match_envs env0' env1' - | C.Abs abs0 :: env0', C.Abs abs1 :: env1' -> - log#ldebug (lazy "match_ctxs: match_envs: matching abs"); - (* Same as for the dummy values: there are two cases *) - if V.AbstractionId.Set.mem abs0.abs_id fixed_ids.aids then ( - log#ldebug (lazy "match_ctxs: match_envs: matching abs: fixed abs"); - (* Still in the prefix: the abstractions must be the same *) - assert (abs0 = abs1); - (* Their ids must be fixed *) - let ids, _ = compute_abs_ids abs0 in - assert ((not S.check_equiv) || ids_are_fixed ids); - (* Continue *) - match_envs env0' env1') - else ( - log#ldebug - (lazy "match_ctxs: match_envs: matching abs: not fixed abs"); - (* Match the values *) - match_abstractions abs0 abs1; - (* Continue *) - match_envs env0' env1') - | [], [] -> - (* Done *) - () - | _ -> - (* The elements don't match *) - raise (Distinct "match_ctxs: match_envs: env elements don't match") - in - - (* Match the environments. - - Rem.: we don't match the ended regions (would it make any sense actually?) *) - try - (* Remove the frame delimiter (the first element of an environment is a frame delimiter) *) - let env0 = List.rev ctx0.env in - let env1 = List.rev ctx1.env in - let env0, env1 = - match (env0, env1) with - | C.Frame :: env0, C.Frame :: env1 -> (env0, env1) - | _ -> raise (Failure "Unreachable") - in - - match_envs env0 env1; - let maps = - { - aid_map = !aid_map; - blid_map = !blid_map; - borrow_id_map = !borrow_id_map; - loan_id_map = !loan_id_map; - rid_map = !rid_map; - sid_map = !sid_map; - sid_to_value_map = !sid_to_value_map; - } - in - Some maps - with Distinct msg -> - log#ldebug (lazy ("match_ctxs: distinct: " ^ msg)); - None - -(** Compute whether two contexts are equivalent modulo an identifier substitution. - - [fixed_ids]: ids for which we force the mapping to be the identity. - - We also take advantage of the structure of the environments, which should - have the same prefixes (we check it). See the explanations for {!join_ctxs}. - - For instance, the following environments are equivalent: - {[ - env0 = { - abs@0 { ML l0 } - ls -> MB l1 (s2 : loops::List<T>) - i -> s1 : u32 - abs@1 { MB l0, ML l1 } - } - - env1 = { - abs@0 { ML l0 } - ls -> MB l2 (s4 : loops::List<T>) - i -> s3 : u32 - abs@2 { MB l0, ML l2 } - } - ]} - - We can go from [env0] to [env1] with the substitution: - {[ - abs_id_subst: { abs@1 -> abs@2 } - borrow_id_subst: { l1 -> l2 } - symbolic_id_subst: { s1 -> s3, s2 -> s4 } - ]} - *) -let ctxs_are_equivalent (fixed_ids : ids_sets) (ctx0 : C.eval_ctx) - (ctx1 : C.eval_ctx) : bool = - let check_equivalent = true in - let lookup_shared_value _ = raise (Failure "Unreachable") in - Option.is_some - (match_ctxs check_equivalent fixed_ids lookup_shared_value - lookup_shared_value ctx0 ctx1) - -(** Join the context at the entry of the loop with the contexts upon reentry - (upon reaching the [Continue] statement - the goal is to compute a fixed - point for the loop entry). - - As we may have to end loans in the environments before doing the join, - we return those updated environments, and the joined environment. - *) -let loop_join_origin_with_continue_ctxs (config : C.config) - (loop_id : V.LoopId.id) (fixed_ids : ids_sets) (old_ctx : C.eval_ctx) - (ctxl : C.eval_ctx list) : (C.eval_ctx * C.eval_ctx list) * C.eval_ctx = - (* # Join with the new contexts, one by one - - For every context, we repeteadly attempt to join it with the current - result of the join: if we fail (because we need to end loans for instance), - we update the context and retry. - Rem.: we should never have to end loans in the aggregated context, only - in the one we are trying to add to the join. - *) - let joined_ctx = ref old_ctx in - let rec join_one_aux (ctx : C.eval_ctx) : C.eval_ctx = - match join_ctxs loop_id fixed_ids !joined_ctx ctx with - | Ok nctx -> - joined_ctx := nctx; - ctx - | Error err -> - let ctx = - match err with - | LoanInRight bid -> - InterpreterBorrows.end_borrow_no_synth config bid ctx - | LoansInRight bids -> - InterpreterBorrows.end_borrows_no_synth config bids ctx - | AbsInRight _ | AbsInLeft _ | LoanInLeft _ | LoansInLeft _ -> - raise (Failure "Unexpected") - in - join_one_aux ctx - in - let join_one (ctx : C.eval_ctx) : C.eval_ctx = - log#ldebug - (lazy - ("loop_join_origin_with_continue_ctxs:join_one: initial ctx:\n" - ^ eval_ctx_to_string ctx)); - - (* Destructure the abstractions introduced in the new context *) - let ctx = destructure_new_abs loop_id fixed_ids.aids ctx in - log#ldebug - (lazy - ("loop_join_origin_with_continue_ctxs:join_one: after destructure:\n" - ^ eval_ctx_to_string ctx)); - - (* Collapse the context we want to add to the join *) - let ctx = collapse_ctx loop_id None fixed_ids ctx in - log#ldebug - (lazy - ("loop_join_origin_with_continue_ctxs:join_one: after collapse:\n" - ^ eval_ctx_to_string ctx)); - - (* Refresh the fresh abstractions *) - let ctx = refresh_abs fixed_ids.aids ctx in - - (* Join the two contexts *) - let ctx1 = join_one_aux ctx in - log#ldebug - (lazy - ("loop_join_origin_with_continue_ctxs:join_one: after join:\n" - ^ eval_ctx_to_string ctx1)); - - (* Collapse again - the join might have introduce abstractions we want - to merge with the others (note that those abstractions may actually - lead to borrows/loans duplications) *) - joined_ctx := collapse_ctx_with_merge loop_id fixed_ids !joined_ctx; - log#ldebug - (lazy - ("loop_join_origin_with_continue_ctxs:join_one: after join-collapse:\n" - ^ eval_ctx_to_string !joined_ctx)); - - (* Sanity check *) - if !Config.check_invariants then Invariants.check_invariants !joined_ctx; - (* Return *) - ctx1 - in - - let ctxl = List.map join_one ctxl in - - (* # Return *) - ((old_ctx, ctxl), !joined_ctx) - -(** Prepare the shared loans in the abstractions by moving them to fresh - abstractions. - - We use this to prepare an evaluation context before computing a fixed point. - - Because a loop iteration might lead to symbolic value expansions and create - shared loans in shared values inside the *fixed* abstractions, which we want - to leave unchanged, we introduce some reborrows in the following way: - - {[ - abs'0 { SL {l0, l1} s0 } - l0 -> SB l0 - l1 -> SB l1 - - ~~> - - abs'0 { SL {l0, l1} s0 } - l0 -> SB l2 - l1 -> SB l3 - abs'2 { SB l0, SL {l2} s2 } - abs'3 { SB l1, SL {l3} s3 } - ]} - - This is sound but leads to information loss. This way, the fixed abstraction - [abs'0] is never modified because [s0] is never accessed (and thus never - expanded). - - We do this because it makes it easier to compute joins and fixed points. - - **REMARK**: - As a side note, we only reborrow the loan ids whose corresponding borrows - appear in values (i.e., not in abstractions). - - For instance, if we have: - {[ - abs'0 { - SL {l0} s0 - SL {l1} s1 - } - abs'1 { SB l0 } - x -> SB l1 - ]} - - we only introduce a fresh abstraction for [l1]. - *) -let prepare_ashared_loans (loop_id : V.LoopId.id option) : cm_fun = - fun cf ctx0 -> - let ctx = ctx0 in - (* Compute the set of borrows which appear in the abstractions, so that - we can filter the borrows that we reborrow. - *) - let absl = - List.filter_map - (function C.Var _ | C.Frame -> None | C.Abs abs -> Some abs) - ctx.env - in - let absl_ids, absl_id_maps = compute_absl_ids absl in - let abs_borrow_ids = absl_ids.borrow_ids in - - (* Map from the fresh sids to the original symbolic values *) - let sid_subst = ref [] in - - (* Return the same value but where: - - the shared loans have been removed - - the symbolic values have been replaced with fresh symbolic values - - the region ids found in the value and belonging to the set [rids] have - been substituted with [nrid] - *) - let mk_value_with_fresh_sids_no_shared_loans (rids : T.RegionId.Set.t) - (nrid : T.RegionId.id) (v : V.typed_value) : V.typed_value = - (* Remove the shared loans *) - let v = value_remove_shared_loans v in - (* Substitute the symbolic values and the region *) - Subst.typed_value_subst_ids - (fun r -> if T.RegionId.Set.mem r rids then nrid else r) - (fun x -> x) - (fun x -> x) - (fun id -> - let nid = C.fresh_symbolic_value_id () in - let sv = V.SymbolicValueId.Map.find id absl_id_maps.sids_to_values in - sid_subst := (nid, sv) :: !sid_subst; - nid) - (fun x -> x) - v - in - - let borrow_substs = ref [] in - let fresh_absl = ref [] in - - (* Auxiliary function to create a new abstraction for a shared value found in - an abstraction. - - Example: - ======== - When exploring: - {[ - abs'0 { SL {l0, l1} s0 } - ]} - - we find the shared value: - - {[ - SL {l0, l1} s0 - ]} - - and introduce the corresponding abstraction: - {[ - abs'2 { SB l0, SL {l2} s2 } - ]} - *) - let push_abs_for_shared_value (abs : V.abs) (sv : V.typed_value) - (lid : V.BorrowId.id) : unit = - (* Create a fresh borrow (for the reborrow) *) - let nlid = C.fresh_borrow_id () in - - (* We need a fresh region for the new abstraction *) - let nrid = C.fresh_region_id () in - - (* Prepare the shared value *) - let nsv = mk_value_with_fresh_sids_no_shared_loans abs.regions nrid sv in - - (* Save the borrow substitution, to apply it to the context later *) - borrow_substs := (lid, nlid) :: !borrow_substs; - - (* Rem.: the below sanity checks are not really necessary *) - assert (V.AbstractionId.Set.is_empty abs.parents); - assert (abs.original_parents = []); - assert (T.RegionId.Set.is_empty abs.ancestors_regions); - - (* Introduce the new abstraction for the shared values *) - let rty = ety_no_regions_to_rty sv.V.ty in - - (* Create the shared loan child *) - let child_rty = rty in - let child_av = mk_aignored child_rty in - - (* Create the shared loan *) - let loan_rty = T.Ref (T.Var nrid, rty, T.Shared) in - let loan_value = - V.ALoan (V.ASharedLoan (V.BorrowId.Set.singleton nlid, nsv, child_av)) - in - let loan_value = mk_typed_avalue loan_rty loan_value in - - (* Create the shared borrow *) - let borrow_rty = loan_rty in - let borrow_value = V.ABorrow (V.ASharedBorrow lid) in - let borrow_value = mk_typed_avalue borrow_rty borrow_value in - - (* Create the abstraction *) - let avalues = [ borrow_value; loan_value ] in - let kind = - match loop_id with - | Some loop_id -> V.Loop (loop_id, None, V.LoopSynthInput) - | None -> V.Identity - in - let can_end = true in - let fresh_abs = - { - V.abs_id = C.fresh_abstraction_id (); - kind; - can_end; - parents = V.AbstractionId.Set.empty; - original_parents = []; - regions = T.RegionId.Set.singleton nrid; - ancestors_regions = T.RegionId.Set.empty; - avalues; - } - in - fresh_absl := fresh_abs :: !fresh_absl - in - - (* Explore the shared values in the context abstractions, and introduce - fresh abstractions with reborrows for those shared values. - - We simply explore the context and call {!push_abs_for_shared_value} - when necessary. - *) - let collect_shared_values_in_abs (abs : V.abs) : unit = - let collect_shared_value lids (sv : V.typed_value) = - (* Sanity check: we don't support nested borrows for now *) - assert (not (value_has_borrows ctx sv.V.value)); - - (* Filter the loan ids whose corresponding borrows appear in abstractions - (see the documentation of the function) *) - let lids = V.BorrowId.Set.diff lids abs_borrow_ids in - - (* Generate fresh borrows and values *) - V.BorrowId.Set.iter (push_abs_for_shared_value abs sv) lids - in - - let visit_avalue = - object - inherit [_] V.iter_typed_avalue as super - - method! visit_SharedLoan env lids sv = - collect_shared_value lids sv; - - (* Continue the exploration *) - super#visit_SharedLoan env lids sv - - method! visit_ASharedLoan env lids sv _ = - collect_shared_value lids sv; - - (* Continue the exploration *) - super#visit_SharedLoan env lids sv - - (** Check that there are no symbolic values with *borrows* inside the - abstraction - shouldn't happen if the symbolic values are greedily - expanded. - We do this because those values could contain shared borrows: - if it is the case, we need to duplicate them too. - TODO: implement this more general behavior. - *) - method! visit_symbolic_value env sv = - assert (not (symbolic_value_has_borrows ctx sv)); - super#visit_symbolic_value env sv - end - in - List.iter (visit_avalue#visit_typed_avalue None) abs.avalues - in - C.env_iter_abs collect_shared_values_in_abs ctx.env; - - (* Update the borrow ids in the environment. - - Example: - ======== - If we start with environment: - {[ - abs'0 { SL {l0, l1} s0 } - l0 -> SB l0 - l1 -> SB l1 - ]} - - We introduce the following abstractions: - {[ - abs'2 { SB l0, SL {l2} s2 } - abs'3 { SB l1, SL {l3} s3 } - ]} - - While doing so, we registered the fact that we introduced [l2] for [l0] - and [l3] for [l1]: we now need to perform the proper substitutions in - the values [l0] and [l1]. This gives: - - {[ - l0 -> SB l0 - l1 -> SB l1 - - ~~> - - l0 -> SB l2 - l1 -> SB l3 - ]} - *) - let env = - let bmap = V.BorrowId.Map.of_list !borrow_substs in - let bsusbt bid = - match V.BorrowId.Map.find_opt bid bmap with - | None -> bid - | Some bid -> bid - in - - let visitor = - object - inherit [_] C.map_env - method! visit_borrow_id _ bid = bsusbt bid - end - in - visitor#visit_env () ctx.env - in - - (* Add the abstractions *) - let fresh_absl = List.map (fun abs -> C.Abs abs) !fresh_absl in - let env = List.append fresh_absl env in - let ctx = { ctx with env } in - - let _, new_ctx_ids_map = compute_context_ids ctx in - - (* Synthesize *) - match cf ctx with - | None -> None - | Some e -> - (* Add the let-bindings which introduce the fresh symbolic values *) - Some - (List.fold_left - (fun e (sid, v) -> - let v = mk_typed_value_from_symbolic_value v in - let sv = - V.SymbolicValueId.Map.find sid new_ctx_ids_map.sids_to_values - in - SymbolicAst.IntroSymbolic (ctx, None, sv, v, e)) - e !sid_subst) - -let prepare_ashared_loans_no_synth (loop_id : V.LoopId.id) (ctx : C.eval_ctx) : - C.eval_ctx = - get_cf_ctx_no_synth (prepare_ashared_loans (Some loop_id)) ctx - -(** Compute a fixed-point for the context at the entry of the loop. - We also return: - - the sets of fixed ids - - the map from region group id to the corresponding abstraction appearing - in the fixed point (this is useful to compute the return type of the loop - backward functions for instance). - - Rem.: the list of symbolic values should be computable by simply exploring - the fixed point environment and listing all the symbolic values we find. - In the future, we might want to do something more precise, by listing only - the values which are read or modified (some symbolic values may be ignored). - *) -let compute_loop_entry_fixed_point (config : C.config) (loop_id : V.LoopId.id) - (eval_loop_body : st_cm_fun) (ctx0 : C.eval_ctx) : - C.eval_ctx * ids_sets * V.abs T.RegionGroupId.Map.t = - (* The continuation for when we exit the loop - we register the - environments upon loop *reentry*, and synthesize nothing by - returning [None] - *) - let ctxs = ref [] in - let register_ctx ctx = ctxs := ctx :: !ctxs in - - (* Introduce "reborrows" for the shared values in the abstractions, so that - the shared values in the fixed abstractions never get modified (technically, - they are immutable, but in practice we can introduce more shared loans, or - expand symbolic values). - - For more details, see the comments for {!prepare_ashared_loans} - *) - let ctx = prepare_ashared_loans_no_synth loop_id ctx0 in - - (* Debug *) - log#ldebug - (lazy - ("compute_loop_entry_fixed_point: after prepare_ashared_loans:" - ^ "\n\n- ctx0:\n" - ^ eval_ctx_to_string_no_filter ctx0 - ^ "\n\n- ctx1:\n" - ^ eval_ctx_to_string_no_filter ctx - ^ "\n\n")); - - let cf_exit_loop_body (res : statement_eval_res) : m_fun = - fun ctx -> - match res with - | Return | Panic | Break _ -> None - | Unit -> - (* See the comment in {!eval_loop} *) - raise (Failure "Unreachable") - | Continue i -> - (* For now we don't support continues to outer loops *) - assert (i = 0); - register_ctx ctx; - None - | LoopReturn _ | EndEnterLoop _ | EndContinue _ -> - (* We don't support nested loops for now *) - raise (Failure "Nested loops are not supported for now") - in - - (* The fixed ids. They are the ids of the original ctx, after we ended - the borrows/loans which end during the first loop iteration (we do - one loop iteration, then set it to [Some]. - *) - let fixed_ids : ids_sets option ref = ref None in - - (* Join the contexts at the loop entry - ctx1 is the current joined - context (the context at the loop entry, after we called - {!prepare_ashared_loans}, if this is the first iteration) *) - let join_ctxs (ctx1 : C.eval_ctx) : C.eval_ctx = - (* If this is the first iteration, end the borrows/loans/abs which - appear in ctx1 and not in the other contexts, then compute the - set of fixed ids. This means those borrows/loans have to end - in the loop, and we rather end them *before* the loop. *) - let ctx1 = - match !fixed_ids with - | Some _ -> ctx1 - | None -> - let old_ids, _ = compute_context_ids ctx1 in - let new_ids, _ = compute_contexts_ids !ctxs in - let blids = V.BorrowId.Set.diff old_ids.blids new_ids.blids in - let aids = V.AbstractionId.Set.diff old_ids.aids new_ids.aids in - (* End those borrows and abstractions *) - let end_borrows_abs blids aids ctx = - let ctx = - InterpreterBorrows.end_borrows_no_synth config blids ctx - in - let ctx = - InterpreterBorrows.end_abstractions_no_synth config aids ctx - in - ctx - in - (* End the borrows/abs in [ctx1] *) - let ctx1 = end_borrows_abs blids aids ctx1 in - (* We can also do the same in the contexts [ctxs]: if there are - several contexts, maybe one of them ended some borrows and some - others didn't. As we need to end those borrows anyway (the join - will detect them and ask to end them) we do it preemptively. - *) - 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)); - ctx1 - in - - let fixed_ids = Option.get !fixed_ids in - let (_, _), ctx2 = - loop_join_origin_with_continue_ctxs config loop_id fixed_ids ctx1 !ctxs - in - ctxs := []; - ctx2 - in - (* Compute the set of fixed ids - for the symbolic ids, we compute the - intersection of ids between the original environment and the list - of new environments *) - let compute_fixed_ids (ctxl : C.eval_ctx list) : ids_sets = - let fixed_ids, _ = compute_context_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 - sids := V.SymbolicValueId.Set.inter !sids fixed_ids.sids) - ctxl; - let sids = !sids in - let fixed_ids = { aids; blids; borrow_ids; loan_ids; dids; rids; sids } in - fixed_ids - in - (* Check if two contexts are equivalent - modulo alpha conversion on the - existentially quantified borrows/abstractions/symbolic values. - *) - let equiv_ctxs (ctx1 : C.eval_ctx) (ctx2 : C.eval_ctx) : bool = - let fixed_ids = compute_fixed_ids [ ctx1; ctx2 ] in - let check_equivalent = true in - let lookup_shared_value _ = raise (Failure "Unreachable") in - Option.is_some - (match_ctxs check_equivalent fixed_ids lookup_shared_value - lookup_shared_value ctx1 ctx2) - in - let max_num_iter = Config.loop_fixed_point_max_num_iters in - let rec compute_fixed_point (ctx : C.eval_ctx) (i0 : int) (i : int) : - C.eval_ctx = - if i = 0 then - raise - (Failure - ("Could not compute a loop fixed point in " ^ string_of_int i0 - ^ " iterations")) - else - (* Evaluate the loop body to register the different contexts upon reentry *) - let _ = eval_loop_body cf_exit_loop_body ctx in - (* Compute the join between the original contexts and the contexts computed - upon reentry *) - let ctx1 = join_ctxs ctx in - - (* Debug *) - log#ldebug - (lazy - ("compute_fixed_point:" ^ "\n\n- ctx0:\n" - ^ eval_ctx_to_string_no_filter ctx - ^ "\n\n- ctx1:\n" - ^ eval_ctx_to_string_no_filter ctx1 - ^ "\n\n")); - - (* Check if we reached a fixed point: if not, iterate *) - if equiv_ctxs ctx ctx1 then ctx1 else compute_fixed_point ctx1 i0 (i - 1) - in - let fp = compute_fixed_point ctx max_num_iter max_num_iter in - - (* Debug *) - log#ldebug - (lazy - ("compute_fixed_point: fixed point computed before matching with input \ - region groups:" ^ "\n\n- fp:\n" - ^ eval_ctx_to_string_no_filter fp - ^ "\n\n")); - - (* Make sure we have exactly one loop abstraction per function region (merge - abstractions accordingly). - - Rem.: this shouldn't impact the set of symbolic value ids (because we - already merged abstractions "vertically" and are now merging them - "horizontally": the symbolic values contained in the abstractions (typically - the shared values) will be preserved. - *) - let fp, rg_to_abs = - (* List the loop abstractions in the fixed-point *) - let fp_aids, add_aid, _mem_aid = V.AbstractionId.Set.mk_stateful_set () in - - let list_loop_abstractions = - object - inherit [_] C.map_eval_ctx - - method! visit_abs _ abs = - match abs.kind with - | Loop (loop_id', _, kind) -> - assert (loop_id' = loop_id); - assert (kind = V.LoopSynthInput); - (* The abstractions introduced so far should be endable *) - assert (abs.can_end = true); - add_aid abs.abs_id; - abs - | _ -> abs - end - in - let fp = list_loop_abstractions#visit_eval_ctx () fp in - - (* For every input region group: - * - evaluate until we get to a [return] - * - end the input abstraction corresponding to the input region group - * - find which loop abstractions end at that moment - * - * [fp_ended_aids] links region groups to sets of ended abstractions. - *) - let fp_ended_aids = ref T.RegionGroupId.Map.empty in - let add_ended_aids (rg_id : T.RegionGroupId.id) - (aids : V.AbstractionId.Set.t) : unit = - match T.RegionGroupId.Map.find_opt rg_id !fp_ended_aids with - | None -> - fp_ended_aids := T.RegionGroupId.Map.add rg_id aids !fp_ended_aids - | Some aids' -> - let aids = V.AbstractionId.Set.union aids aids' in - fp_ended_aids := T.RegionGroupId.Map.add rg_id aids !fp_ended_aids - in - let cf_loop : st_m_fun = - fun res ctx -> - match res with - | Continue _ | Panic -> - (* We don't want to generate anything *) - None - | Break _ -> - (* We enforce that we can't get there: see {!PrePasses.remove_loop_breaks} *) - raise (Failure "Unreachable") - | Unit | LoopReturn _ | EndEnterLoop _ | EndContinue _ -> - (* For why we can't get [Unit], see the comments inside {!eval_loop_concrete}. - For [EndEnterLoop] and [EndContinue]: we don't support nested loops for now. - *) - raise (Failure "Unreachable") - | Return -> - (* Should we consume the return value and pop the frame? - * If we check in [Interpreter] that the loop abstraction we end is - * indeed the correct one, I think it is sound to under-approximate here - * (and it shouldn't make any difference). - *) - let _ = - List.iter - (fun rg_id -> - (* Lookup the input abstraction - we use the fact that the - abstractions should have been introduced in a specific - order (and we check that it is indeed the case) *) - let abs_id = - V.AbstractionId.of_int (T.RegionGroupId.to_int rg_id) - in - (* By default, the [SynthInput] abs can't end *) - let ctx = C.ctx_set_abs_can_end ctx abs_id true in - assert ( - let abs = C.ctx_lookup_abs ctx abs_id in - abs.kind = V.SynthInput rg_id); - (* End this abstraction *) - let ctx = - 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 ended_ids = V.AbstractionId.Set.diff !fp_aids ids.aids in - add_ended_aids rg_id ended_ids) - ctx.region_groups - in - (* We don't want to generate anything *) - None - in - let _ = eval_loop_body cf_loop fp in - - (* Check that the sets of abstractions we need to end per region group are pairwise - * disjoint *) - let aids_union = ref V.AbstractionId.Set.empty in - let _ = - T.RegionGroupId.Map.iter - (fun _ ids -> - assert (V.AbstractionId.Set.disjoint !aids_union ids); - aids_union := V.AbstractionId.Set.union ids !aids_union) - !fp_ended_aids - in - - (* We also check that all the regions need to end - this is not necessary per - se, but if it doesn't happen it is bizarre and worth investigating... *) - assert (V.AbstractionId.Set.equal !aids_union !fp_aids); - - (* Merge the abstractions which need to be merged, and compute the map from - region id to abstraction id *) - let fp = ref fp in - let rg_to_abs = ref T.RegionGroupId.Map.empty in - let _ = - T.RegionGroupId.Map.iter - (fun rg_id ids -> - let ids = V.AbstractionId.Set.elements ids in - (* Retrieve the first id of the group *) - match ids with - | [] -> - (* We shouldn't get there: we actually introduce reborrows with - {!prepare_ashared_loans} and in the [match_mut_borrows] function - of {!MakeJoinMatcher} to introduce some fresh abstractions for - this purpose. - *) - raise (Failure "Unexpected") - | id0 :: ids -> - let id0 = ref id0 in - (* Add the proper region group into the abstraction *) - let abs_kind = V.Loop (loop_id, Some rg_id, V.LoopSynthInput) in - let abs = C.ctx_lookup_abs !fp !id0 in - let abs = { abs with V.kind = abs_kind } in - let fp', _ = C.ctx_subst_abs !fp !id0 abs in - fp := fp'; - (* Merge all the abstractions into this one *) - List.iter - (fun id -> - try - log#ldebug - (lazy - ("compute_loop_entry_fixed_point: merge FP \ - abstraction: " - ^ V.AbstractionId.to_string id - ^ " into " - ^ V.AbstractionId.to_string !id0)); - (* Note that we merge *into* [id0] *) - let fp', id0' = - merge_into_abstraction loop_id abs_kind false !fp id !id0 - in - fp := fp'; - id0 := id0'; - () - with ValueMatchFailure _ -> raise (Failure "Unexpected")) - ids; - (* Register the mapping *) - let abs = C.ctx_lookup_abs !fp !id0 in - rg_to_abs := T.RegionGroupId.Map.add_strict rg_id abs !rg_to_abs) - !fp_ended_aids - in - let rg_to_abs = !rg_to_abs in - - (* Reorder the loans and borrows in the fresh abstractions in the fixed-point *) - let fp = - reorder_loans_borrows_in_fresh_abs (Option.get !fixed_ids).aids !fp - in - - (* Update the abstraction's [can_end] field and their kinds. - - Note that if [remove_rg_id] is [true], we set the region id to [None] - and set the abstractions as endable: this is so that we can check that - we have a fixed point (so far in the fixed point the loop abstractions had - no region group, and we set them as endable just above). - - If [remove_rg_id] is [false], we simply set the abstractions as non-endable - to freeze them (we will use the fixed point as starting point for the - symbolic execution of the loop body, and we have to make sure the input - abstractions are frozen). - *) - let update_loop_abstractions (remove_rg_id : bool) = - object - inherit [_] C.map_eval_ctx - - method! visit_abs _ abs = - match abs.kind with - | Loop (loop_id', _, kind) -> - assert (loop_id' = loop_id); - assert (kind = V.LoopSynthInput); - let kind = - if remove_rg_id then V.Loop (loop_id, None, V.LoopSynthInput) - else abs.kind - in - { abs with can_end = remove_rg_id; kind } - | _ -> abs - end - in - let update_kinds_can_end (remove_rg_id : bool) ctx = - (update_loop_abstractions remove_rg_id)#visit_eval_ctx () ctx - in - let fp = update_kinds_can_end false fp in - - (* Sanity check: we still have a fixed point - we simply call [compute_fixed_point] - while allowing exactly one iteration to see if it fails *) - let _ = - let fp_test = update_kinds_can_end true fp in - log#ldebug - (lazy - ("compute_fixed_point: fixed point after matching with the function \ - region groups:\n" - ^ eval_ctx_to_string_no_filter fp_test)); - compute_fixed_point fp_test 1 1 - in - - (* Return *) - (fp, rg_to_abs) - in - let fixed_ids = compute_fixed_ids [ fp ] in - - (* Return *) - (fp, fixed_ids, rg_to_abs) - -(** Split an environment between the fixed abstractions, values, etc. and - the new abstractions, values, etc. - - Returns: (fixed, new abs, new dummies) - *) -let ctx_split_fixed_new (fixed_ids : ids_sets) (ctx : C.eval_ctx) : - C.env * V.abs list * V.typed_value list = - let is_fresh_did (id : C.DummyVarId.id) : bool = - not (C.DummyVarId.Set.mem id fixed_ids.dids) - in - let is_fresh_abs_id (id : V.AbstractionId.id) : bool = - not (V.AbstractionId.Set.mem id fixed_ids.aids) - in - (* Filter the new abstractions and dummy variables (there shouldn't be any new dummy variable - though) in the target context *) - let is_fresh (ee : C.env_elem) : bool = - match ee with - | C.Var (VarBinder _, _) | C.Frame -> false - | C.Var (DummyBinder bv, _) -> is_fresh_did bv - | C.Abs abs -> is_fresh_abs_id abs.abs_id - in - let new_eel, filt_env = List.partition is_fresh ctx.env in - let is_abs ee = match ee with C.Abs _ -> true | _ -> false in - let new_absl, new_dummyl = List.partition is_abs new_eel in - let new_absl = - List.map - (fun ee -> - match ee with C.Abs abs -> abs | _ -> raise (Failure "Unreachable")) - new_absl - in - let new_dummyl = - List.map - (fun ee -> - match ee with - | C.Var (DummyBinder _, v) -> v - | _ -> raise (Failure "Unreachable")) - new_dummyl - in - (filt_env, new_absl, new_dummyl) - -type borrow_loan_corresp = { - borrow_to_loan_id_map : V.BorrowId.InjSubst.t; - loan_to_borrow_id_map : V.BorrowId.InjSubst.t; -} -[@@deriving show] - -let ids_sets_empty_borrows_loans (ids : ids_sets) : ids_sets = - let { aids; blids = _; borrow_ids = _; loan_ids = _; dids; rids; sids } = - ids - in - let empty = V.BorrowId.Set.empty in - let ids = - { - aids; - blids = empty; - borrow_ids = empty; - loan_ids = empty; - dids; - rids; - sids; - } - in - ids - -(** Utility *) -type loans_borrows_pair = { - loans : V.BorrowId.Set.t; - borrows : V.BorrowId.Set.t; -} -[@@deriving show, ord] - -(** For the abstractions in the fixed point, compute the correspondance between - the borrows ids and the loans ids, if we want to introduce equivalent - identity abstractions (i.e., abstractions which do nothing - the input - borrows are exactly the output loans). - - **Context:** - ============ - When we (re-enter) the loop, we want to introduce identity abstractions - (i.e., abstractions which actually only introduce fresh identifiers for - some borrows, to abstract away a bit the borrow graph) which have the same - shape as the abstractions introduced for the fixed point (see the explanations - for [match_ctx_with_target]). This allows us to transform the environment - into a fixed point (again, see the explanations for [match_ctx_with_target]). - - In order to introduce those identity abstractions, we need to figure out, - for those abstractions, which loans should be linked to which borrows. - We do this in the following way. - - We match the fixed point environment with the environment upon first entry - in the loop, and exploit the fact that the fixed point was derived by also - joining this first entry environment: because of that, the borrows in the - abstractions introduced for the fixed-point actually exist in this first - environment (they are not fresh). For [list_nth_mut] (see the explanations - at the top of the file) we have the following: - - {[ - // Environment upon first entry in the loop - env0 = { - abs@0 { ML l0 } - ls -> MB l0 (s2 : loops::List<T>) - i -> s1 : u32 - } - - // Fixed-point environment - env_fp = { - abs@0 { ML l0 } - ls -> MB l1 (s3 : loops::List<T>) - i -> s4 : u32 - abs@fp { - MB l0 // this borrow appears in [env0] - ML l1 - } - } - ]} - - We filter those environments to remove the non-fixed dummy variables, - abstractions, etc. in a manner similar to [match_ctx_with_target]. We - get: - - {[ - filtered_env0 = { - abs@0 { ML l0 } - ls -> MB l0 (s2 : loops::List<T>) - i -> s1 : u32 - } - - filtered_env_fp = { - abs@0 { ML l0 } - ls -> MB l1 (s3 : loops::List<T>) - i -> s@ : u32 - // removed abs@fp - } - ]} - - We then match [filtered_env_fp] with [filtered_env0], taking care to not - consider loans and borrows in a disjoint manner, and ignoring the fixed - values, abstractions, loans, etc. We get: - {[ - borrows_map: { l1 -> l0 } // because we matched [MB l1 ...] with [MB l0 ...] in [ls] - loans_map: {} // we ignore abs@0, which is "fixed" - ]} - - From there we deduce that, if we want to introduce an identity abstraction with the - shape of [abs@fp], we should link [l1] to [l0]. In other words, the value retrieved - through the loan [l1] is actually the value which has to be given back to [l0]. - *) -let compute_fixed_point_id_correspondance (fixed_ids : ids_sets) - (src_ctx : C.eval_ctx) (tgt_ctx : C.eval_ctx) : borrow_loan_corresp = - log#ldebug - (lazy - ("compute_fixed_point_id_correspondance:\n\n- fixed_ids:\n" - ^ show_ids_sets fixed_ids ^ "\n\n- src_ctx:\n" ^ eval_ctx_to_string src_ctx - ^ "\n\n- tgt_ctx:\n" ^ eval_ctx_to_string tgt_ctx ^ "\n\n")); - - let filt_src_env, _, _ = ctx_split_fixed_new fixed_ids src_ctx in - let filt_src_ctx = { src_ctx with env = filt_src_env } in - let filt_tgt_env, new_absl, _ = ctx_split_fixed_new fixed_ids tgt_ctx in - let filt_tgt_ctx = { tgt_ctx with env = filt_tgt_env } in - - log#ldebug - (lazy - ("compute_fixed_point_id_correspondance:\n\n- fixed_ids:\n" - ^ show_ids_sets fixed_ids ^ "\n\n- filt_src_ctx:\n" - ^ eval_ctx_to_string filt_src_ctx - ^ "\n\n- filt_tgt_ctx:\n" - ^ eval_ctx_to_string filt_tgt_ctx - ^ "\n\n")); - - (* Match the source context and the filtered target context *) - let maps = - let check_equiv = false in - let fixed_ids = ids_sets_empty_borrows_loans fixed_ids in - let open InterpreterBorrowsCore in - let lookup_shared_loan lid ctx : V.typed_value = - match snd (lookup_loan ek_all lid ctx) with - | Concrete (V.SharedLoan (_, v)) -> v - | Abstract (V.ASharedLoan (_, v, _)) -> v - | _ -> raise (Failure "Unreachable") - in - let lookup_in_tgt id = lookup_shared_loan id tgt_ctx in - let lookup_in_src id = lookup_shared_loan id src_ctx in - Option.get - (match_ctxs check_equiv fixed_ids lookup_in_tgt lookup_in_src filt_tgt_ctx - filt_src_ctx) - in - - log#ldebug - (lazy - ("compute_fixed_point_id_correspondance:\n\n- tgt_to_src_maps:\n" - ^ show_ids_maps maps ^ "\n\n")); - - let src_to_tgt_borrow_map = - V.BorrowId.Map.of_list - (List.map - (fun (x, y) -> (y, x)) - (V.BorrowId.InjSubst.bindings maps.borrow_id_map)) - in - - (* Sanity check: for every abstraction, the target loans and borrows are mapped - to the same set of source loans and borrows. - - For instance, if we map the [env_fp] to [env0] (only looking at the bindings, - ignoring the abstractions) below: - {[ - env0 = { - abs@0 { ML l0 } - ls -> MB l0 (s2 : loops::List<T>) - i -> s1 : u32 - } - - env_fp = { - abs@0 { ML l0 } - ls -> MB l1 (s3 : loops::List<T>) - i -> s4 : u32 - abs@fp { - MB l0 - ML l1 - } - } - ]} - - We get that l1 is mapped to l0. From there, we see that abs@fp consumes - the same borrows that it gives: it is indeed an identity function. - - TODO: we should also check the mappings for the shared values (to - make sure the abstractions are indeed the identity)... - *) - List.iter - (fun abs -> - let ids, _ = compute_abs_ids abs in - (* Map the *loan* ids (we just match the corresponding *loans* ) *) - let loan_ids = - V.BorrowId.Set.map - (fun x -> V.BorrowId.InjSubst.find x maps.borrow_id_map) - ids.loan_ids - in - (* Check that the loan and borrows are related *) - assert (V.BorrowId.Set.equal ids.borrow_ids loan_ids)) - new_absl; - - (* For every target abstraction (going back to the [list_nth_mut] example, - we have to visit [abs@fp { ML l0, MB l1 }]): - - go through the tgt borrows ([l1]) - - for every tgt borrow, find the corresponding src borrow ([l0], because - we have: [borrows_map: { l1 -> l0 }]) - - from there, find the corresponding tgt loan ([l0]) - - Note that this borrow does not necessarily appear in the src_to_tgt_borrow_map, - if it actually corresponds to a borrows introduced when decomposing the - abstractions to move the shared values out of the source context abstractions. - *) - let tgt_borrow_to_loan = ref V.BorrowId.InjSubst.empty in - let visit_tgt = - object - inherit [_] V.iter_abs - - method! visit_borrow_id _ id = - (* Find the target borrow *) - let tgt_borrow_id = V.BorrowId.Map.find id src_to_tgt_borrow_map in - (* Update the map *) - tgt_borrow_to_loan := - V.BorrowId.InjSubst.add id tgt_borrow_id !tgt_borrow_to_loan - end - in - List.iter (visit_tgt#visit_abs ()) new_absl; - - (* Compute the map from loan to borrows *) - let tgt_loan_to_borrow = - V.BorrowId.InjSubst.of_list - (List.map - (fun (x, y) -> (y, x)) - (V.BorrowId.InjSubst.bindings !tgt_borrow_to_loan)) - in - - (* Return *) - { - borrow_to_loan_id_map = !tgt_borrow_to_loan; - loan_to_borrow_id_map = tgt_loan_to_borrow; - } - -(** Match a context with a target context. - - This is used to compute application of loop translations: we use this - to introduce "identity" abstractions upon (re-)entering the loop. - - For instance, the fixed point for [list_nth_mut] (see the top of the file) - is: - {[ - env_fp = { - abs@0 { ML l0 } - ls -> MB l1 (s@3 : loops::List<T>) - i -> s@4 : u32 - abs@fp { - MB l0 - ML l1 - } - } - ]} - - Upon re-entering the loop, starting from the fixed point, we get the - following environment: - {[ - env = { - abs@0 { ML l0 } - ls -> MB l5 (s@6 : loops::List<T>) - i -> s@7 : u32 - abs@1 { MB l0, ML l1 } - _@1 -> MB l1 (loops::List::Cons (ML l2, ML l3)) - _@2 -> MB l3 (@Box (ML l5)) // tail - _@3 -> MB l2 (s@3 : T) // hd - } - ]} - - We want to introduce an abstraction [abs@2], which has the same shape as [abs@fp] - above (the fixed-point abstraction), and which is actually the identity. If we do so, - we get an environment which is actually also a fixed point (we can collapse - the dummy variables and [abs@1] to actually retrieve the fixed point we - computed, and we use the fact that those values and abstractions can't be - *directly* manipulated unless we end this newly introduced [abs@2], which we - forbid). - - We match the *fixed point context* with the context upon entering the loop - by doing the following. - - 1. We filter [env_fp] and [env] to remove the newly introduced dummy variables - and abstractions. We get: - - {[ - filtered_env_fp = { - abs@0 { ML l0 } - ls -> MB l1 (s@3 : loops::List<T>) - i -> s@4 : u32 - // removed abs@fp - } - - filtered_env = { - abs@0 { ML l0 } - ls -> MB l5 (s@6 : loops::List<T>) - i -> s@7 : u32 - // removed abs@1, _@1, etc. - } - ]} - - 2. We match [filtered_env_fp] with [filtered_env] to compute a map from - the FP borrows/loans to the current borrows/loans (and also from symbolic values to - values). Note that we take care to *consider loans and borrows separately*, - and we ignore the "fixed" abstractions (which are unchanged - we checked that - when computing the fixed point). - We get: - {[ - borrows_map: { l1 -> l5 } // because we matched [MB l1 ...] with [MB l5 ...] - loans_map: {} // we ignore abs@0, which is "fixed" - ]} - - 3. We want to introduce an instance of [abs@fp] which is actually the - identity. From [compute_fixed_point_id_correspondance] and looking at - [abs@fp], we know we should link the instantiation of loan [l1] with the - instantiation of loan [l0]. We substitute [l0] with [l5] (following step 2.) - and introduce a fresh borrow [l6] for [l5] that we use to instantiate [l1]. - We get the following environment: - - {[ - env = { - abs@0 { ML l0 } - ls -> MB l6 (s@6 : loops::List<T>) - i -> s@7 : u32 - abs@1 { MB l0, ML l1 } - _@1 -> MB l1 (loops::List::Cons (ML l2, ML l3)) - _@2 -> MB l3 (@Box (ML l5)) // tail - _@3 -> MB l2 (s@3 : T) // hd - abs@2 { MB l5, ML l6 } // this is actually the identity: l6 = l5 - } - ]} - - 4. As we now have a fixed point (see above comments), we can consider than - [abs@2] links the current iteration to the last one before we exit. What we - are interested in is that: - - upon inserting [abs@2] we re-entered the loop, meaning in the translation - we need to insert a recursive call to the loop forward function - - upon ending [abs@2] we need to insert a call to the loop backward function - - Because we want to ignore them, we end the loans in the newly introduced - [abs@2] abstraction (i.e., [l6]). We get: - {[ - env = { - abs@0 { ML l0 } - ls -> ⊥ - i -> s@7 : u32 - abs@1 { MB l0, ML l1 } - _@1 -> MB l1 (loops::List::Cons (ML l2, ML l3)) - _@2 -> MB l3 (@Box (ML l5)) // tail - _@3 -> MB l2 (s@3 : T) // hd - abs@2 { MB l5 } - } - ]} - - TODO: we shouldn't need to end the loans, we should actually remove them - before inserting the new abstractions (we may have issues with the symbolic - values, if they contain borrows - above i points to [s@7], but it should - be a different symbolic value...). - - Finally, we use the map from symbolic values to values to compute the list of - input values of the loop: we simply list the values, by order of increasing - symbolic value id. We *do* use the fixed values (though they are in the frame) - because they may be *read* inside the loop. - - We can then proceed to finishing the symbolic execution and doing the - synthesis. - - Rem.: we might reorganize the [tgt_ctx] by ending loans for instance. - - **Parameters**: - [is_loop_entry]: [true] if first entry into the loop, [false] if re-entry - (i.e., continue). - [fp_input_svalues]: the list of symbolic values appearing in the fixed - point and which must be instantiated during the match (this is the list - of input parameters of the loop). - *) -let match_ctx_with_target (config : C.config) (loop_id : V.LoopId.id) - (is_loop_entry : bool) (fp_bl_maps : borrow_loan_corresp) - (fp_input_svalues : V.SymbolicValueId.id list) (fixed_ids : ids_sets) - (src_ctx : C.eval_ctx) : st_cm_fun = - fun cf tgt_ctx -> - (* Debug *) - log#ldebug - (lazy - ("match_ctx_with_target:\n" ^ "\n- fixed_ids: " ^ show_ids_sets fixed_ids - ^ "\n" ^ "\n- src_ctx: " ^ eval_ctx_to_string src_ctx ^ "\n- tgt_ctx: " - ^ eval_ctx_to_string tgt_ctx)); - - (* We first reorganize [tgt_ctx] so that we can match [src_ctx] with it (by - ending loans for instance - remember that the [src_ctx] is the fixed point - context, which results from joins during which we ended the loans which - were introduced during the loop iterations) - *) - (* End the loans which lead to mismatches when joining *) - let rec cf_reorganize_join_tgt : cm_fun = - fun cf tgt_ctx -> - (* Collect fixed values in the source and target contexts: end the loans in the - source context which don't appear in the target context *) - let filt_src_env, _, _ = ctx_split_fixed_new fixed_ids src_ctx in - let filt_tgt_env, _, _ = ctx_split_fixed_new fixed_ids tgt_ctx in - - log#ldebug - (lazy - ("match_ctx_with_target:\n" ^ "\n- fixed_ids: " - ^ show_ids_sets fixed_ids ^ "\n" ^ "\n- filt_src_ctx: " - ^ env_to_string src_ctx filt_src_env - ^ "\n- filt_tgt_ctx: " - ^ env_to_string tgt_ctx filt_tgt_env)); - - (* Remove the abstractions *) - let filter (ee : C.env_elem) : bool = - match ee with Var _ -> true | Abs _ | Frame -> false - in - let filt_src_env = List.filter filter filt_src_env in - let filt_tgt_env = List.filter filter filt_tgt_env in - - (* Match the values to check if there are loans to eliminate *) - - (* We need to pick a context for some functions like [match_typed_values]: - the context is only used to lookup module data, so we can pick whichever - we want. - TODO: this is not very clean. Maybe we should just carry this data around. - *) - let ctx = tgt_ctx in - - let nabs = ref [] in - - let module S : MatchJoinState = struct - (* The context is only used to lookup module data: we can pick whichever we want *) - let ctx = ctx - let loop_id = loop_id - let nabs = nabs - end in - let module JM = MakeJoinMatcher (S) in - let module M = Match (JM) in - try - let _ = - List.iter - (fun (var0, var1) -> - match (var0, var1) with - | C.Var (C.DummyBinder b0, v0), C.Var (C.DummyBinder b1, v1) -> - assert (b0 = b1); - let _ = M.match_typed_values ctx v0 v1 in - () - | C.Var (C.VarBinder b0, v0), C.Var (C.VarBinder b1, v1) -> - assert (b0 = b1); - let _ = M.match_typed_values ctx v0 v1 in - () - | _ -> raise (Failure "Unexpected")) - (List.combine filt_src_env filt_tgt_env) - in - (* No exception was thrown: continue *) - cf tgt_ctx - with ValueMatchFailure e -> - (* Exception: end the corresponding borrows, and continue *) - let cc = - match e with - | LoanInRight bid -> InterpreterBorrows.end_borrow config bid - | LoansInRight bids -> InterpreterBorrows.end_borrows config bids - | AbsInRight _ | AbsInLeft _ | LoanInLeft _ | LoansInLeft _ -> - raise (Failure "Unexpected") - in - comp cc cf_reorganize_join_tgt cf tgt_ctx - in - - (* Introduce the "identity" abstractions for the loop reentry. - - Match the target context with the source context so as to compute how to - map the borrows from the target context (i.e., the fixed point context) - to the borrows in the source context. - - Substitute the *loans* in the abstractions introduced by the target context - (the abstractions of the fixed point) to properly link those abstraction: - we introduce *identity* abstractions (the loans are equal to the borrows): - we substitute the loans and introduce fresh ids for the borrows, symbolic - values, etc. About the *identity abstractions*, see the comments for - [compute_fixed_point_id_correspondance]. - - TODO: this whole thing is very technical and error-prone. - We should rely on a more primitive and safer function - [add_identity_abs] to add the identity abstractions one by one. - *) - let cf_introduce_loop_fp_abs : m_fun = - fun tgt_ctx -> - (* Match the source and target contexts *) - let filt_tgt_env, _, _ = ctx_split_fixed_new fixed_ids tgt_ctx in - let filt_src_env, new_absl, new_dummyl = - ctx_split_fixed_new fixed_ids src_ctx - in - assert (new_dummyl = []); - let filt_tgt_ctx = { tgt_ctx with env = filt_tgt_env } in - let filt_src_ctx = { src_ctx with env = filt_src_env } in - - let src_to_tgt_maps = - let check_equiv = false in - let fixed_ids = ids_sets_empty_borrows_loans fixed_ids in - let open InterpreterBorrowsCore in - let lookup_shared_loan lid ctx : V.typed_value = - match snd (lookup_loan ek_all lid ctx) with - | Concrete (V.SharedLoan (_, v)) -> v - | Abstract (V.ASharedLoan (_, v, _)) -> v - | _ -> raise (Failure "Unreachable") - in - let lookup_in_src id = lookup_shared_loan id src_ctx in - let lookup_in_tgt id = lookup_shared_loan id tgt_ctx in - (* Match *) - Option.get - (match_ctxs check_equiv fixed_ids lookup_in_src lookup_in_tgt - filt_src_ctx filt_tgt_ctx) - in - let tgt_to_src_borrow_map = - V.BorrowId.Map.of_list - (List.map - (fun (x, y) -> (y, x)) - (V.BorrowId.InjSubst.bindings src_to_tgt_maps.borrow_id_map)) - in - - (* Debug *) - log#ldebug - (lazy - ("match_ctx_with_target: cf_introduce_loop_fp_abs:" ^ "\n\n- tgt_ctx: " - ^ eval_ctx_to_string tgt_ctx ^ "\n\n- src_ctx: " - ^ eval_ctx_to_string src_ctx ^ "\n\n- filt_tgt_ctx: " - ^ eval_ctx_to_string_no_filter filt_tgt_ctx - ^ "\n\n- filt_src_ctx: " - ^ eval_ctx_to_string_no_filter filt_src_ctx - ^ "\n\n- new_absl:\n" - ^ eval_ctx_to_string - { src_ctx with C.env = List.map (fun abs -> C.Abs abs) new_absl } - ^ "\n\n- fixed_ids:\n" ^ show_ids_sets fixed_ids ^ "\n\n- fp_bl_maps:\n" - ^ show_borrow_loan_corresp fp_bl_maps - ^ "\n\n- src_to_tgt_maps: " - ^ show_ids_maps src_to_tgt_maps)); - - (* Update the borrows and symbolic ids in the source context. - - Going back to the [list_nth_mut_example], the original environment upon - re-entering the loop is: - - {[ - abs@0 { ML l0 } - ls -> MB l5 (s@6 : loops::List<T>) - i -> s@7 : u32 - _@1 -> MB l0 (loops::List::Cons (ML l1, ML l2)) - _@2 -> MB l2 (@Box (ML l4)) // tail - _@3 -> MB l1 (s@3 : T) // hd - abs@1 { MB l4, ML l5 } - ]} - - The fixed-point environment is: - {[ - env_fp = { - abs@0 { ML l0 } - ls -> MB l1 (s3 : loops::List<T>) - i -> s4 : u32 - abs@fp { - MB l0 // this borrow appears in [env0] - ML l1 - } - } - ]} - - Through matching, we detect that in [env_fp], [l1] is matched - to [l5]. We introduce a fresh borrow [l6] for [l1], and remember - in the map [src_fresh_borrows_map] that: [{ l1 -> l6}]. - - We get: - {[ - abs@0 { ML l0 } - ls -> MB l6 (s@6 : loops::List<T>) // l6 is fresh and doesn't have a corresponding loan - i -> s@7 : u32 - _@1 -> MB l0 (loops::List::Cons (ML l1, ML l2)) - _@2 -> MB l2 (@Box (ML l4)) // tail - _@3 -> MB l1 (s@3 : T) // hd - abs@1 { MB l4, ML l5 } - ]} - - Later, we will introduce the identity abstraction: - {[ - abs@2 { MB l5, ML l6 } - ]} - *) - (* First, compute the set of borrows which appear in the fresh abstractions - of the fixed-point: we want to introduce fresh ids only for those. *) - let new_absl_ids, _ = compute_absl_ids new_absl in - let src_fresh_borrows_map = ref V.BorrowId.Map.empty in - let visit_tgt = - object - inherit [_] C.map_eval_ctx - - method! visit_borrow_id _ id = - (* Map the borrow, if it needs to be mapped *) - if - (* We map the borrows for which we computed a mapping *) - V.BorrowId.InjSubst.Set.mem id - (V.BorrowId.InjSubst.elements src_to_tgt_maps.borrow_id_map) - (* And which have corresponding loans in the fresh fixed-point abstractions *) - && V.BorrowId.Set.mem - (V.BorrowId.Map.find id tgt_to_src_borrow_map) - new_absl_ids.loan_ids - then ( - let src_id = V.BorrowId.Map.find id tgt_to_src_borrow_map in - let nid = C.fresh_borrow_id () in - src_fresh_borrows_map := - V.BorrowId.Map.add src_id nid !src_fresh_borrows_map; - nid) - else id - end - in - let tgt_ctx = visit_tgt#visit_eval_ctx () tgt_ctx in - - log#ldebug - (lazy - ("match_ctx_with_target: cf_introduce_loop_fp_abs: \ - src_fresh_borrows_map:\n" - ^ V.BorrowId.Map.show V.BorrowId.to_string !src_fresh_borrows_map - ^ "\n")); - - (* Rem.: we don't update the symbolic values. It is not necessary - because there shouldn't be any symbolic value containing borrows. - - Rem.: we will need to do something about the symbolic values in the - abstractions and in the *variable bindings* once we allow symbolic - values containing borrows to not be eagerly expanded. - *) - assert Config.greedy_expand_symbolics_with_borrows; - - (* Update the borrows and loans in the abstractions of the target context. - - Going back to the [list_nth_mut] example and by using [src_fresh_borrows_map], - we instantiate the fixed-point abstractions that we will insert into the - context. - The abstraction is [abs { MB l0, ML l1 }]. - Because of [src_fresh_borrows_map], we substitute [l1] with [l6]. - Because of the match between the contexts, we substitute [l0] with [l5]. - We get: - {[ - abs@2 { MB l5, ML l6 } - ]} - *) - let region_id_map = ref T.RegionId.Map.empty in - let get_rid rid = - match T.RegionId.Map.find_opt rid !region_id_map with - | Some rid -> rid - | None -> - let nid = C.fresh_region_id () in - region_id_map := T.RegionId.Map.add rid nid !region_id_map; - nid - in - let visit_src = - object - inherit [_] C.map_eval_ctx as super - - method! visit_borrow_id _ bid = - log#ldebug - (lazy - ("match_ctx_with_target: cf_introduce_loop_fp_abs: \ - visit_borrow_id: " ^ V.BorrowId.to_string bid ^ "\n")); - - (* Lookup the id of the loan corresponding to this borrow *) - let src_lid = - V.BorrowId.InjSubst.find bid fp_bl_maps.borrow_to_loan_id_map - in - - log#ldebug - (lazy - ("match_ctx_with_target: cf_introduce_loop_fp_abs: looked up \ - src_lid: " - ^ V.BorrowId.to_string src_lid - ^ "\n")); - - (* Lookup the tgt borrow id to which this borrow was mapped *) - let tgt_bid = - V.BorrowId.InjSubst.find src_lid src_to_tgt_maps.borrow_id_map - in - - log#ldebug - (lazy - ("match_ctx_with_target: cf_introduce_loop_fp_abs: looked up \ - tgt_bid: " - ^ V.BorrowId.to_string tgt_bid - ^ "\n")); - - tgt_bid - - method! visit_loan_id _ id = - log#ldebug - (lazy - ("match_ctx_with_target: cf_introduce_loop_fp_abs: \ - visit_loan_id: " ^ V.BorrowId.to_string id ^ "\n")); - (* Map the borrow - rem.: we mapped the borrows *in the values*, - meaning we know how to map the *corresponding loans in the - abstractions* *) - match V.BorrowId.Map.find_opt id !src_fresh_borrows_map with - | None -> - (* No mapping: this means that the borrow was mapped when - we matched values (it doesn't come from a fresh abstraction) - and because of this, it should actually be mapped to itself *) - assert ( - V.BorrowId.InjSubst.find id src_to_tgt_maps.borrow_id_map = id); - id - | Some id -> id - - method! visit_symbolic_value_id _ _ = C.fresh_symbolic_value_id () - method! visit_abstraction_id _ _ = C.fresh_abstraction_id () - method! visit_region_id _ id = get_rid id - - (** We also need to change the abstraction kind *) - method! visit_abs env abs = - match abs.kind with - | V.Loop (loop_id', rg_id, kind) -> - assert (loop_id' = loop_id); - assert (kind = V.LoopSynthInput); - let can_end = false in - let kind = V.Loop (loop_id, rg_id, V.LoopCall) in - let abs = { abs with kind; can_end } in - super#visit_abs env abs - | _ -> super#visit_abs env abs - end - in - let new_absl = List.map (visit_src#visit_abs ()) new_absl in - let new_absl = List.map (fun abs -> C.Abs abs) new_absl in - - (* Add the abstractions from the target context to the source context *) - let nenv = List.append new_absl tgt_ctx.env in - let tgt_ctx = { tgt_ctx with env = nenv } in - - log#ldebug - (lazy - ("match_ctx_with_target:cf_introduce_loop_fp_abs:\n- result ctx:\n" - ^ eval_ctx_to_string tgt_ctx)); - - (* Sanity check *) - if !Config.check_invariants then - Invariants.check_borrowed_values_invariant tgt_ctx; - - (* End all the borrows which appear in the *new* abstractions *) - let new_borrows = - V.BorrowId.Set.of_list - (List.map snd (V.BorrowId.Map.bindings !src_fresh_borrows_map)) - in - let cc = InterpreterBorrows.end_borrows config new_borrows in - - (* Compute the loop input values *) - let input_values = - V.SymbolicValueId.Map.of_list - (List.map - (fun sid -> - ( sid, - V.SymbolicValueId.Map.find sid src_to_tgt_maps.sid_to_value_map - )) - fp_input_svalues) - in - - (* Continue *) - cc - (cf - (if is_loop_entry then EndEnterLoop (loop_id, input_values) - else EndContinue (loop_id, input_values))) - tgt_ctx - in - - (* Compose and continue *) - cf_reorganize_join_tgt cf_introduce_loop_fp_abs tgt_ctx - (** Evaluate a loop in concrete mode *) let eval_loop_concrete (eval_loop_body : st_cm_fun) : st_cm_fun = fun cf ctx -> @@ -4036,129 +65,6 @@ let eval_loop_concrete (eval_loop_body : st_cm_fun) : st_cm_fun = (* Apply *) eval_loop_body reeval_loop_body ctx -(** Compute the set of "quantified" symbolic value ids in a fixed-point context. - - We compute: - - the set of symbolic value ids that are freshly introduced - - the list of input symbolic values - *) -let compute_fp_ctx_symbolic_values (ctx : C.eval_ctx) (fp_ctx : C.eval_ctx) : - V.SymbolicValueId.Set.t * V.symbolic_value list = - let old_ids, _ = compute_context_ids ctx in - let fp_ids, fp_ids_maps = compute_context_ids fp_ctx in - let fresh_sids = V.SymbolicValueId.Set.diff fp_ids.sids old_ids.sids in - - (* Compute the set of symbolic values which appear in shared values inside - *fixed* abstractions: because we introduce fresh abstractions and reborrows - with {!prepare_ashared_loans}, those values are never accessed directly - inside the loop iterations: we can ignore them (and should, because - otherwise it leads to a very ugly translation with duplicated, unused - values) *) - let shared_sids_in_fixed_abs = - let fixed_absl = - List.filter - (fun (ee : C.env_elem) -> - match ee with - | C.Var _ | C.Frame -> false - | Abs abs -> V.AbstractionId.Set.mem abs.abs_id old_ids.aids) - ctx.env - in - - (* Rem.: as we greedily expand the symbolic values containing borrows, and - in particular the (mutable/shared) borrows, we could simply list the - symbolic values appearing in the abstractions: those are necessarily - shared values. We prefer to be more general, in prevision of later - changes. - *) - let sids = ref V.SymbolicValueId.Set.empty in - let visitor = - object (self) - inherit [_] C.iter_env - - method! visit_ASharedLoan inside_shared _ sv child_av = - self#visit_typed_value true sv; - self#visit_typed_avalue inside_shared child_av - - method! visit_symbolic_value_id inside_shared sid = - if inside_shared then sids := V.SymbolicValueId.Set.add sid !sids - end - in - visitor#visit_env false fixed_absl; - !sids - in - - (* Remove the shared symbolic values present in the fixed abstractions - - see comments for [shared_sids_in_fixed_abs]. *) - let sids_to_values = fp_ids_maps.sids_to_values in - - log#ldebug - (lazy - ("compute_fp_ctx_symbolic_values:" ^ "\n- shared_sids_in_fixed_abs:" - ^ V.SymbolicValueId.Set.show shared_sids_in_fixed_abs - ^ "\n- all_sids_to_values: " - ^ V.SymbolicValueId.Map.show (symbolic_value_to_string ctx) sids_to_values - ^ "\n")); - - let sids_to_values = - V.SymbolicValueId.Map.filter - (fun sid _ -> - not (V.SymbolicValueId.Set.mem sid shared_sids_in_fixed_abs)) - sids_to_values - in - - (* List the input symbolic values in proper order. - - We explore the environment, and order the symbolic values in the order - in which they are found - this way, the symbolic values found in a - variable [x] which appears before [y] are listed first, for instance. - *) - let input_svalues = - let found_sids = ref V.SymbolicValueId.Set.empty in - let ordered_sids = ref [] in - - let visitor = - object (self) - inherit [_] C.iter_env - - (** We lookup the shared values *) - method! visit_SharedBorrow env bid = - let open InterpreterBorrowsCore in - let v = - match snd (lookup_loan ek_all bid fp_ctx) with - | Concrete (V.SharedLoan (_, v)) -> v - | Abstract (V.ASharedLoan (_, v, _)) -> v - | _ -> raise (Failure "Unreachable") - in - self#visit_typed_value env v - - method! visit_symbolic_value_id _ id = - if not (V.SymbolicValueId.Set.mem id !found_sids) then ( - found_sids := V.SymbolicValueId.Set.add id !found_sids; - ordered_sids := id :: !ordered_sids) - end - in - - List.iter (visitor#visit_env_elem ()) (List.rev fp_ctx.env); - - List.filter_map - (fun id -> V.SymbolicValueId.Map.find_opt id sids_to_values) - (List.rev !ordered_sids) - in - - log#ldebug - (lazy - ("compute_fp_ctx_symbolic_values:" ^ "\n- src context:\n" - ^ eval_ctx_to_string_no_filter ctx - ^ "\n- fixed point:\n" - ^ eval_ctx_to_string_no_filter fp_ctx - ^ "\n- fresh_sids: " - ^ V.SymbolicValueId.Set.show fresh_sids - ^ "\n- input_svalues: " - ^ Print.list_to_string (symbolic_value_to_string ctx) input_svalues - ^ "\n\n")); - - (fresh_sids, input_svalues) - (** Evaluate a loop in symbolic mode *) let eval_loop_symbolic (config : C.config) (eval_loop_body : st_cm_fun) : st_cm_fun = @@ -4307,7 +213,6 @@ let eval_loop_symbolic (config : C.config) (eval_loop_body : st_cm_fun) : S.synthesize_loop loop_id input_svalues fresh_sids rg_to_given_back end_expr loop_expr -(** Evaluate a loop *) let eval_loop (config : C.config) (eval_loop_body : st_cm_fun) : st_cm_fun = fun cf ctx -> match config.C.mode with diff --git a/compiler/InterpreterLoops.mli b/compiler/InterpreterLoops.mli new file mode 100644 index 00000000..7395739b --- /dev/null +++ b/compiler/InterpreterLoops.mli @@ -0,0 +1,62 @@ +(** This module implements support for loops. + + Throughout the module, we will use the following code as example to + illustrate what the functions do (this function simply returns a mutable + borrow to the nth element of a list): + {[ + pub fn list_nth_mut<'a, T>(mut ls: &'a mut List<T>, mut i: u32) -> &'a mut T { + loop { + match ls { + List::Nil => { + panic!() + } + List::Cons(x, tl) => { + if i == 0 { + return x; + } else { + ls = tl; + i -= 1; + } + } + } + } + } + ]} + + Upon reaching the loop entry, the environment is as follows (ignoring the + dummy variables): + {[ + abs@0 { ML l0 } + ls -> MB l0 (s2 : loops::List<T>) + i -> s1 : u32 + ]} + + Upon reaching the [continue] at the end of the first iteration, the environment + is as follows: + {[ + abs@0 { ML l0 } + ls -> MB l4 (s@6 : loops::List<T>) + i -> s@7 : u32 + _@1 -> MB l0 (loops::List::Cons (ML l1, ML l2)) + _@2 -> MB l2 (@Box (ML l4)) // tail + _@3 -> MB l1 (s@3 : T) // hd + ]} + + The fixed point we compute is: + {[ + abs@0 { ML l0 } + ls -> MB l1 (s@3 : loops::List<T>) + i -> s@4 : u32 + abs@fp { // fp: fixed-point + MB l0 + ML l1 + } + ]} + + From here, we deduce that [abs@fp { MB l0, ML l1}] is the loop abstraction. + *) + +module C = Contexts + +(** Evaluate a loop *) +val eval_loop : C.config -> Cps.st_cm_fun -> Cps.st_cm_fun diff --git a/compiler/InterpreterLoopsCore.ml b/compiler/InterpreterLoopsCore.ml new file mode 100644 index 00000000..209fce1c --- /dev/null +++ b/compiler/InterpreterLoopsCore.ml @@ -0,0 +1,386 @@ +(** Core definitions for the [IntepreterLoops*] *) + +module T = Types +module PV = PrimitiveValues +module V = Values +module E = Expressions +module C = Contexts +module Subst = Substitute +module A = LlbcAst +module L = Logging +module Inv = Invariants +module S = SynthesizeSymbolic +module UF = UnionFind +open InterpreterUtils +open InterpreterExpressions + +type updt_env_kind = + | AbsInLeft of V.AbstractionId.id + | LoanInLeft of V.BorrowId.id + | LoansInLeft of V.BorrowId.Set.t + | AbsInRight of V.AbstractionId.id + | LoanInRight of V.BorrowId.id + | LoansInRight of V.BorrowId.Set.t + +(** Utility exception *) +exception ValueMatchFailure of updt_env_kind + +(** Utility exception *) +exception Distinct of string + +type ctx_or_update = (C.eval_ctx, updt_env_kind) result + +(** Union Find *) +module UnionFind = UF.Make (UF.StoreMap) + +(** A small utility - + + Rem.: some environments may be ill-formed (they may contain several times + the same loan or borrow - this happens for instance when merging + environments). This is the reason why we use sets in some places (for + instance, [borrow_to_abs] maps to a *set* of ids). +*) +type abs_borrows_loans_maps = { + abs_ids : V.AbstractionId.id list; + abs_to_borrows : V.BorrowId.Set.t V.AbstractionId.Map.t; + abs_to_loans : V.BorrowId.Set.t V.AbstractionId.Map.t; + abs_to_borrows_loans : V.BorrowId.Set.t V.AbstractionId.Map.t; + borrow_to_abs : V.AbstractionId.Set.t V.BorrowId.Map.t; + loan_to_abs : V.AbstractionId.Set.t V.BorrowId.Map.t; + borrow_loan_to_abs : V.AbstractionId.Set.t V.BorrowId.Map.t; +} + +(** See {!InterpreterLoopsMatchCtxs.MakeMatcher} and {!InterpreterLoopsCore.Matcher}. + + This module contains primitive match functions to instantiate the generic + {!InterpreterLoopsMatchCtxs.MakeMatcher} functor. + *) +module type PrimMatcher = sig + val match_etys : T.ety -> T.ety -> T.ety + val match_rtys : T.rty -> T.rty -> T.rty + + (** The input primitive values are not equal *) + val match_distinct_primitive_values : + T.ety -> V.primitive_value -> V.primitive_value -> V.typed_value + + (** The input ADTs don't have the same variant *) + val match_distinct_adts : T.ety -> V.adt_value -> V.adt_value -> V.typed_value + + (** The meta-value is the result of a match. + + We take an additional function as input, which acts as a matcher over + typed values, to be able to lookup the shared values and match them. + We do this for shared borrows (and not, e.g., mutable borrows) because + shared borrows introduce indirections, while mutable borrows carry the + borrowed values with them: we might want to explore and match those + borrowed values, in which case we have to manually look them up before + calling the match function. + *) + val match_shared_borrows : + (V.typed_value -> V.typed_value -> V.typed_value) -> + T.ety -> + V.borrow_id -> + V.borrow_id -> + V.borrow_id + + (** The input parameters are: + - [ty] + - [bid0]: first borrow id + - [bv0]: first borrowed value + - [bid1] + - [bv1] + - [bv]: the result of matching [bv0] with [bv1] + *) + val match_mut_borrows : + T.ety -> + V.borrow_id -> + V.typed_value -> + V.borrow_id -> + V.typed_value -> + V.typed_value -> + V.borrow_id * V.typed_value + + (** Parameters: + [ty] + [ids0] + [ids1] + [v]: the result of matching the shared values coming from the two loans + *) + val match_shared_loans : + T.ety -> + V.loan_id_set -> + V.loan_id_set -> + V.typed_value -> + V.loan_id_set * V.typed_value + + val match_mut_loans : T.ety -> V.loan_id -> V.loan_id -> V.loan_id + + (** There are no constraints on the input symbolic values *) + val match_symbolic_values : + V.symbolic_value -> V.symbolic_value -> V.symbolic_value + + (** Match a symbolic value with a value which is not symbolic. + + If the boolean is [true], it means the symbolic value comes from the + *left* environment. Otherwise it comes from the right environment (it + is important when throwing exceptions, for instance when we need to + end loans in one of the two environments). + *) + val match_symbolic_with_other : + bool -> V.symbolic_value -> V.typed_value -> V.typed_value + + (** Match a bottom value with a value which is not bottom. + + If the boolean is [true], it means the bottom value comes from the + *left* environment. Otherwise it comes from the right environment (it + is important when throwing exceptions, for instance when we need to + end loans in one of the two environments). + *) + val match_bottom_with_other : bool -> V.typed_value -> V.typed_value + + (** The input ADTs don't have the same variant *) + val match_distinct_aadts : + T.rty -> V.adt_avalue -> T.rty -> V.adt_avalue -> T.rty -> V.typed_avalue + + (** Parameters: + [ty0] + [bid0] + [ty1] + [bid1] + [ty]: result of matching ty0 and ty1 + *) + val match_ashared_borrows : + T.rty -> V.borrow_id -> T.rty -> V.borrow_id -> T.rty -> V.typed_avalue + + (** Parameters: + [ty0] + [bid0] + [av0] + [ty1] + [bid1] + [av1] + [ty]: result of matching ty0 and ty1 + [av]: result of matching av0 and av1 + *) + val match_amut_borrows : + T.rty -> + V.borrow_id -> + V.typed_avalue -> + T.rty -> + V.borrow_id -> + V.typed_avalue -> + T.rty -> + V.typed_avalue -> + V.typed_avalue + + (** Parameters: + [ty0] + [ids0] + [v0] + [av0] + [ty1] + [ids1] + [v1] + [av1] + [ty]: result of matching ty0 and ty1 + [v]: result of matching v0 and v1 + [av]: result of matching av0 and av1 + *) + val match_ashared_loans : + T.rty -> + V.loan_id_set -> + V.typed_value -> + V.typed_avalue -> + T.rty -> + V.loan_id_set -> + V.typed_value -> + V.typed_avalue -> + T.rty -> + V.typed_value -> + V.typed_avalue -> + V.typed_avalue + + (** Parameters: + [ty0] + [id0] + [av0] + [ty1] + [id1] + [av1] + [ty]: result of matching ty0 and ty1 + [av]: result of matching av0 and av1 + *) + val match_amut_loans : + T.rty -> + V.borrow_id -> + V.typed_avalue -> + T.rty -> + V.borrow_id -> + V.typed_avalue -> + T.rty -> + V.typed_avalue -> + V.typed_avalue + + (** Match two arbitrary avalues whose constructors don't match (this function + is typically used to raise the proper exception). + *) + val match_avalues : V.typed_avalue -> V.typed_avalue -> V.typed_avalue +end + +module type Matcher = sig + (** Match two values. + + Rem.: this function raises exceptions of type {!Aeneas.InterpreterLoopsCore.ValueMatchFailure}. + *) + val match_typed_values : + C.eval_ctx -> V.typed_value -> V.typed_value -> V.typed_value + + (** Match two avalues. + + Rem.: this function raises exceptions of type {!Aeneas.InterpreterLoopsCore.ValueMatchFailure}. + *) + val match_typed_avalues : + C.eval_ctx -> V.typed_avalue -> V.typed_avalue -> V.typed_avalue +end + +(** See {!InterpreterLoopsMatchCtxs.MakeCheckEquivMatcher} and + {!InterpreterLoopsCore.CheckEquivMatcher}. + + Very annoying: functors only take modules as inputs... + *) +module type MatchCheckEquivState = sig + (** [true] if we check equivalence between contexts, [false] if we match + a source context with a target context. *) + val check_equiv : bool + + val ctx : C.eval_ctx + val rid_map : T.RegionId.InjSubst.t ref + + (** Substitution for the loan and borrow ids - used only if [check_equiv] is true *) + val blid_map : V.BorrowId.InjSubst.t ref + + (** Substitution for the borrow ids - used only if [check_equiv] is false *) + val borrow_id_map : V.BorrowId.InjSubst.t ref + + (** Substitution for the loans ids - used only if [check_equiv] is false *) + val loan_id_map : V.BorrowId.InjSubst.t ref + + val sid_map : V.SymbolicValueId.InjSubst.t ref + val sid_to_value_map : V.typed_value V.SymbolicValueId.Map.t ref + val aid_map : V.AbstractionId.InjSubst.t ref + val lookup_shared_value_in_ctx0 : V.BorrowId.id -> V.typed_value + val lookup_shared_value_in_ctx1 : V.BorrowId.id -> V.typed_value +end + +module type CheckEquivMatcher = sig + include PrimMatcher + + val match_aid : V.abstraction_id -> V.abstraction_id -> V.abstraction_id + + val match_aidl : + V.abstraction_id list -> V.abstraction_id list -> V.abstraction_id list + + val match_aids : + V.abstraction_id_set -> V.abstraction_id_set -> V.abstraction_id_set + + val match_rid : V.region_id -> V.region_id -> V.region_id + val match_rids : V.region_id_set -> V.region_id_set -> V.region_id_set + val match_borrow_id : V.borrow_id -> V.borrow_id -> V.borrow_id + + val match_borrow_idl : + V.borrow_id list -> V.borrow_id list -> V.borrow_id list + + val match_borrow_ids : V.borrow_id_set -> V.borrow_id_set -> V.borrow_id_set + val match_loan_id : V.loan_id -> V.loan_id -> V.loan_id + val match_loan_idl : V.loan_id list -> V.loan_id list -> V.loan_id list + val match_loan_ids : V.loan_id_set -> V.loan_id_set -> V.loan_id_set +end + +(** See {!InterpreterLoopsMatchCtxs.match_ctxs} *) +type ids_maps = { + aid_map : V.AbstractionId.InjSubst.t; + blid_map : V.BorrowId.InjSubst.t; + (** Substitution for the loan and borrow ids *) + borrow_id_map : V.BorrowId.InjSubst.t; (** Substitution for the borrow ids *) + loan_id_map : V.BorrowId.InjSubst.t; (** Substitution for the loan ids *) + rid_map : T.RegionId.InjSubst.t; + sid_map : V.SymbolicValueId.InjSubst.t; + sid_to_value_map : V.typed_value V.SymbolicValueId.Map.t; +} +[@@deriving show] + +type borrow_loan_corresp = { + borrow_to_loan_id_map : V.BorrowId.InjSubst.t; + loan_to_borrow_id_map : V.BorrowId.InjSubst.t; +} +[@@deriving show] + +(* Very annoying: functors only take modules as inputs... *) +module type MatchJoinState = sig + (** The current context *) + val ctx : C.eval_ctx + + (** The current loop *) + val loop_id : V.LoopId.id + + (** The abstractions introduced when performing the matches *) + val nabs : V.abs list ref +end + +(** Split an environment between the fixed abstractions, values, etc. and + the new abstractions, values, etc. + + Returns: (fixed, new abs, new dummies) + *) +let ctx_split_fixed_new (fixed_ids : ids_sets) (ctx : C.eval_ctx) : + C.env * V.abs list * V.typed_value list = + let is_fresh_did (id : C.DummyVarId.id) : bool = + not (C.DummyVarId.Set.mem id fixed_ids.dids) + in + let is_fresh_abs_id (id : V.AbstractionId.id) : bool = + not (V.AbstractionId.Set.mem id fixed_ids.aids) + in + (* Filter the new abstractions and dummy variables (there shouldn't be any new dummy variable + though) in the target context *) + let is_fresh (ee : C.env_elem) : bool = + match ee with + | C.Var (VarBinder _, _) | C.Frame -> false + | C.Var (DummyBinder bv, _) -> is_fresh_did bv + | C.Abs abs -> is_fresh_abs_id abs.abs_id + in + let new_eel, filt_env = List.partition is_fresh ctx.env in + let is_abs ee = match ee with C.Abs _ -> true | _ -> false in + let new_absl, new_dummyl = List.partition is_abs new_eel in + let new_absl = + List.map + (fun ee -> + match ee with C.Abs abs -> abs | _ -> raise (Failure "Unreachable")) + new_absl + in + let new_dummyl = + List.map + (fun ee -> + match ee with + | C.Var (DummyBinder _, v) -> v + | _ -> raise (Failure "Unreachable")) + new_dummyl + in + (filt_env, new_absl, new_dummyl) + +let ids_sets_empty_borrows_loans (ids : ids_sets) : ids_sets = + let { aids; blids = _; borrow_ids = _; loan_ids = _; dids; rids; sids } = + ids + in + let empty = V.BorrowId.Set.empty in + let ids = + { + aids; + blids = empty; + borrow_ids = empty; + loan_ids = empty; + dids; + rids; + sids; + } + in + ids diff --git a/compiler/InterpreterLoopsFixedPoint.ml b/compiler/InterpreterLoopsFixedPoint.ml new file mode 100644 index 00000000..aff8f3fe --- /dev/null +++ b/compiler/InterpreterLoopsFixedPoint.ml @@ -0,0 +1,965 @@ +module T = Types +module PV = PrimitiveValues +module V = Values +module E = Expressions +module C = Contexts +module Subst = Substitute +module A = LlbcAst +module L = Logging +open TypesUtils +open ValuesUtils +module Inv = Invariants +module S = SynthesizeSymbolic +open Cps +open InterpreterUtils +open InterpreterLoopsCore +open InterpreterLoopsMatchCtxs +open InterpreterLoopsJoinCtxs + +(** The local logger *) +let log = L.loops_fixed_point_log + +(** Reorder the loans and borrows in the fresh abstractions. + + We do this in order to enforce some structure in the environments: this + allows us to find fixed-points. Note that this function needs to be + called typically after we merge abstractions together (see {!collapse_ctx} + for instance). + *) +let reorder_loans_borrows_in_fresh_abs (old_abs_ids : V.AbstractionId.Set.t) + (ctx : C.eval_ctx) : C.eval_ctx = + let reorder_in_fresh_abs (abs : V.abs) : V.abs = + (* Split between the loans and borrows *) + let is_borrow (av : V.typed_avalue) : bool = + match av.V.value with + | ABorrow _ -> true + | ALoan _ -> false + | _ -> raise (Failure "Unexpected") + in + let aborrows, aloans = List.partition is_borrow abs.V.avalues in + + (* Reoder the borrows, and the loans. + + After experimenting, it seems that a good way of reordering the loans + and the borrows to find fixed points is simply to sort them by increasing + order of id (taking the smallest id of a set of ids, in case of sets). + *) + let get_borrow_id (av : V.typed_avalue) : V.BorrowId.id = + match av.V.value with + | V.ABorrow (V.AMutBorrow (bid, _) | V.ASharedBorrow bid) -> bid + | _ -> raise (Failure "Unexpected") + in + let get_loan_id (av : V.typed_avalue) : V.BorrowId.id = + match av.V.value with + | V.ALoan (V.AMutLoan (lid, _)) -> lid + | V.ALoan (V.ASharedLoan (lids, _, _)) -> V.BorrowId.Set.min_elt lids + | _ -> raise (Failure "Unexpected") + in + (* We use ordered maps to reorder the borrows and loans *) + let reorder (get_bid : V.typed_avalue -> V.BorrowId.id) + (values : V.typed_avalue list) : V.typed_avalue list = + List.map snd + (V.BorrowId.Map.bindings + (V.BorrowId.Map.of_list (List.map (fun v -> (get_bid v, v)) values))) + in + let aborrows = reorder get_borrow_id aborrows in + let aloans = reorder get_loan_id aloans in + let avalues = List.append aborrows aloans in + { abs with V.avalues } + in + + let reorder_in_abs (abs : V.abs) = + if V.AbstractionId.Set.mem abs.abs_id old_abs_ids then abs + else reorder_in_fresh_abs abs + in + + let env = C.env_map_abs reorder_in_abs ctx.env in + + { ctx with C.env } + +let prepare_ashared_loans (loop_id : V.LoopId.id option) : cm_fun = + fun cf ctx0 -> + let ctx = ctx0 in + (* Compute the set of borrows which appear in the abstractions, so that + we can filter the borrows that we reborrow. + *) + let absl = + List.filter_map + (function C.Var _ | C.Frame -> None | C.Abs abs -> Some abs) + ctx.env + in + let absl_ids, absl_id_maps = compute_absl_ids absl in + let abs_borrow_ids = absl_ids.borrow_ids in + + (* Map from the fresh sids to the original symbolic values *) + let sid_subst = ref [] in + + (* Return the same value but where: + - the shared loans have been removed + - the symbolic values have been replaced with fresh symbolic values + - the region ids found in the value and belonging to the set [rids] have + been substituted with [nrid] + *) + let mk_value_with_fresh_sids_no_shared_loans (rids : T.RegionId.Set.t) + (nrid : T.RegionId.id) (v : V.typed_value) : V.typed_value = + (* Remove the shared loans *) + let v = value_remove_shared_loans v in + (* Substitute the symbolic values and the region *) + Subst.typed_value_subst_ids + (fun r -> if T.RegionId.Set.mem r rids then nrid else r) + (fun x -> x) + (fun x -> x) + (fun id -> + let nid = C.fresh_symbolic_value_id () in + let sv = V.SymbolicValueId.Map.find id absl_id_maps.sids_to_values in + sid_subst := (nid, sv) :: !sid_subst; + nid) + (fun x -> x) + v + in + + let borrow_substs = ref [] in + let fresh_absl = ref [] in + + (* Auxiliary function to create a new abstraction for a shared value found in + an abstraction. + + Example: + ======== + When exploring: + {[ + abs'0 { SL {l0, l1} s0 } + ]} + + we find the shared value: + + {[ + SL {l0, l1} s0 + ]} + + and introduce the corresponding abstraction: + {[ + abs'2 { SB l0, SL {l2} s2 } + ]} + *) + let push_abs_for_shared_value (abs : V.abs) (sv : V.typed_value) + (lid : V.BorrowId.id) : unit = + (* Create a fresh borrow (for the reborrow) *) + let nlid = C.fresh_borrow_id () in + + (* We need a fresh region for the new abstraction *) + let nrid = C.fresh_region_id () in + + (* Prepare the shared value *) + let nsv = mk_value_with_fresh_sids_no_shared_loans abs.regions nrid sv in + + (* Save the borrow substitution, to apply it to the context later *) + borrow_substs := (lid, nlid) :: !borrow_substs; + + (* Rem.: the below sanity checks are not really necessary *) + assert (V.AbstractionId.Set.is_empty abs.parents); + assert (abs.original_parents = []); + assert (T.RegionId.Set.is_empty abs.ancestors_regions); + + (* Introduce the new abstraction for the shared values *) + let rty = ety_no_regions_to_rty sv.V.ty in + + (* Create the shared loan child *) + let child_rty = rty in + let child_av = mk_aignored child_rty in + + (* Create the shared loan *) + let loan_rty = T.Ref (T.Var nrid, rty, T.Shared) in + let loan_value = + V.ALoan (V.ASharedLoan (V.BorrowId.Set.singleton nlid, nsv, child_av)) + in + let loan_value = mk_typed_avalue loan_rty loan_value in + + (* Create the shared borrow *) + let borrow_rty = loan_rty in + let borrow_value = V.ABorrow (V.ASharedBorrow lid) in + let borrow_value = mk_typed_avalue borrow_rty borrow_value in + + (* Create the abstraction *) + let avalues = [ borrow_value; loan_value ] in + let kind = + match loop_id with + | Some loop_id -> V.Loop (loop_id, None, V.LoopSynthInput) + | None -> V.Identity + in + let can_end = true in + let fresh_abs = + { + V.abs_id = C.fresh_abstraction_id (); + kind; + can_end; + parents = V.AbstractionId.Set.empty; + original_parents = []; + regions = T.RegionId.Set.singleton nrid; + ancestors_regions = T.RegionId.Set.empty; + avalues; + } + in + fresh_absl := fresh_abs :: !fresh_absl + in + + (* Explore the shared values in the context abstractions, and introduce + fresh abstractions with reborrows for those shared values. + + We simply explore the context and call {!push_abs_for_shared_value} + when necessary. + *) + let collect_shared_values_in_abs (abs : V.abs) : unit = + let collect_shared_value lids (sv : V.typed_value) = + (* Sanity check: we don't support nested borrows for now *) + assert (not (value_has_borrows ctx sv.V.value)); + + (* Filter the loan ids whose corresponding borrows appear in abstractions + (see the documentation of the function) *) + let lids = V.BorrowId.Set.diff lids abs_borrow_ids in + + (* Generate fresh borrows and values *) + V.BorrowId.Set.iter (push_abs_for_shared_value abs sv) lids + in + + let visit_avalue = + object + inherit [_] V.iter_typed_avalue as super + + method! visit_SharedLoan env lids sv = + collect_shared_value lids sv; + + (* Continue the exploration *) + super#visit_SharedLoan env lids sv + + method! visit_ASharedLoan env lids sv _ = + collect_shared_value lids sv; + + (* Continue the exploration *) + super#visit_SharedLoan env lids sv + + (** Check that there are no symbolic values with *borrows* inside the + abstraction - shouldn't happen if the symbolic values are greedily + expanded. + We do this because those values could contain shared borrows: + if it is the case, we need to duplicate them too. + TODO: implement this more general behavior. + *) + method! visit_symbolic_value env sv = + assert (not (symbolic_value_has_borrows ctx sv)); + super#visit_symbolic_value env sv + end + in + List.iter (visit_avalue#visit_typed_avalue None) abs.avalues + in + C.env_iter_abs collect_shared_values_in_abs ctx.env; + + (* Update the borrow ids in the environment. + + Example: + ======== + If we start with environment: + {[ + abs'0 { SL {l0, l1} s0 } + l0 -> SB l0 + l1 -> SB l1 + ]} + + We introduce the following abstractions: + {[ + abs'2 { SB l0, SL {l2} s2 } + abs'3 { SB l1, SL {l3} s3 } + ]} + + While doing so, we registered the fact that we introduced [l2] for [l0] + and [l3] for [l1]: we now need to perform the proper substitutions in + the values [l0] and [l1]. This gives: + + {[ + l0 -> SB l0 + l1 -> SB l1 + + ~~> + + l0 -> SB l2 + l1 -> SB l3 + ]} + *) + let env = + let bmap = V.BorrowId.Map.of_list !borrow_substs in + let bsusbt bid = + match V.BorrowId.Map.find_opt bid bmap with + | None -> bid + | Some bid -> bid + in + + let visitor = + object + inherit [_] C.map_env + method! visit_borrow_id _ bid = bsusbt bid + end + in + visitor#visit_env () ctx.env + in + + (* Add the abstractions *) + let fresh_absl = List.map (fun abs -> C.Abs abs) !fresh_absl in + let env = List.append fresh_absl env in + let ctx = { ctx with env } in + + let _, new_ctx_ids_map = compute_context_ids ctx in + + (* Synthesize *) + match cf ctx with + | None -> None + | Some e -> + (* Add the let-bindings which introduce the fresh symbolic values *) + Some + (List.fold_left + (fun e (sid, v) -> + let v = mk_typed_value_from_symbolic_value v in + let sv = + V.SymbolicValueId.Map.find sid new_ctx_ids_map.sids_to_values + in + SymbolicAst.IntroSymbolic (ctx, None, sv, v, e)) + e !sid_subst) + +let prepare_ashared_loans_no_synth (loop_id : V.LoopId.id) (ctx : C.eval_ctx) : + C.eval_ctx = + get_cf_ctx_no_synth (prepare_ashared_loans (Some loop_id)) ctx + +let compute_loop_entry_fixed_point (config : C.config) (loop_id : V.LoopId.id) + (eval_loop_body : st_cm_fun) (ctx0 : C.eval_ctx) : + C.eval_ctx * ids_sets * V.abs T.RegionGroupId.Map.t = + (* The continuation for when we exit the loop - we register the + environments upon loop *reentry*, and synthesize nothing by + returning [None] + *) + let ctxs = ref [] in + let register_ctx ctx = ctxs := ctx :: !ctxs in + + (* Introduce "reborrows" for the shared values in the abstractions, so that + the shared values in the fixed abstractions never get modified (technically, + they are immutable, but in practice we can introduce more shared loans, or + expand symbolic values). + + For more details, see the comments for {!prepare_ashared_loans} + *) + let ctx = prepare_ashared_loans_no_synth loop_id ctx0 in + + (* Debug *) + log#ldebug + (lazy + ("compute_loop_entry_fixed_point: after prepare_ashared_loans:" + ^ "\n\n- ctx0:\n" + ^ eval_ctx_to_string_no_filter ctx0 + ^ "\n\n- ctx1:\n" + ^ eval_ctx_to_string_no_filter ctx + ^ "\n\n")); + + let cf_exit_loop_body (res : statement_eval_res) : m_fun = + fun ctx -> + match res with + | Return | Panic | Break _ -> None + | Unit -> + (* See the comment in {!eval_loop} *) + raise (Failure "Unreachable") + | Continue i -> + (* For now we don't support continues to outer loops *) + assert (i = 0); + register_ctx ctx; + None + | LoopReturn _ | EndEnterLoop _ | EndContinue _ -> + (* We don't support nested loops for now *) + raise (Failure "Nested loops are not supported for now") + in + + (* The fixed ids. They are the ids of the original ctx, after we ended + the borrows/loans which end during the first loop iteration (we do + one loop iteration, then set it to [Some]. + *) + let fixed_ids : ids_sets option ref = ref None in + + (* Join the contexts at the loop entry - ctx1 is the current joined + context (the context at the loop entry, after we called + {!prepare_ashared_loans}, if this is the first iteration) *) + let join_ctxs (ctx1 : C.eval_ctx) : C.eval_ctx = + (* If this is the first iteration, end the borrows/loans/abs which + appear in ctx1 and not in the other contexts, then compute the + set of fixed ids. This means those borrows/loans have to end + in the loop, and we rather end them *before* the loop. *) + let ctx1 = + match !fixed_ids with + | Some _ -> ctx1 + | None -> + let old_ids, _ = compute_context_ids ctx1 in + let new_ids, _ = compute_contexts_ids !ctxs in + let blids = V.BorrowId.Set.diff old_ids.blids new_ids.blids in + let aids = V.AbstractionId.Set.diff old_ids.aids new_ids.aids in + (* End those borrows and abstractions *) + let end_borrows_abs blids aids ctx = + let ctx = + InterpreterBorrows.end_borrows_no_synth config blids ctx + in + let ctx = + InterpreterBorrows.end_abstractions_no_synth config aids ctx + in + ctx + in + (* End the borrows/abs in [ctx1] *) + let ctx1 = end_borrows_abs blids aids ctx1 in + (* We can also do the same in the contexts [ctxs]: if there are + several contexts, maybe one of them ended some borrows and some + others didn't. As we need to end those borrows anyway (the join + will detect them and ask to end them) we do it preemptively. + *) + 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)); + ctx1 + in + + let fixed_ids = Option.get !fixed_ids in + let (_, _), ctx2 = + loop_join_origin_with_continue_ctxs config loop_id fixed_ids ctx1 !ctxs + in + ctxs := []; + ctx2 + in + (* Compute the set of fixed ids - for the symbolic ids, we compute the + intersection of ids between the original environment and the list + of new environments *) + let compute_fixed_ids (ctxl : C.eval_ctx list) : ids_sets = + let fixed_ids, _ = compute_context_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 + sids := V.SymbolicValueId.Set.inter !sids fixed_ids.sids) + ctxl; + let sids = !sids in + let fixed_ids = { aids; blids; borrow_ids; loan_ids; dids; rids; sids } in + fixed_ids + in + (* Check if two contexts are equivalent - modulo alpha conversion on the + existentially quantified borrows/abstractions/symbolic values. + *) + let equiv_ctxs (ctx1 : C.eval_ctx) (ctx2 : C.eval_ctx) : bool = + let fixed_ids = compute_fixed_ids [ ctx1; ctx2 ] in + let check_equivalent = true in + let lookup_shared_value _ = raise (Failure "Unreachable") in + Option.is_some + (match_ctxs check_equivalent fixed_ids lookup_shared_value + lookup_shared_value ctx1 ctx2) + in + let max_num_iter = Config.loop_fixed_point_max_num_iters in + let rec compute_fixed_point (ctx : C.eval_ctx) (i0 : int) (i : int) : + C.eval_ctx = + if i = 0 then + raise + (Failure + ("Could not compute a loop fixed point in " ^ string_of_int i0 + ^ " iterations")) + else + (* Evaluate the loop body to register the different contexts upon reentry *) + let _ = eval_loop_body cf_exit_loop_body ctx in + (* Compute the join between the original contexts and the contexts computed + upon reentry *) + let ctx1 = join_ctxs ctx in + + (* Debug *) + log#ldebug + (lazy + ("compute_fixed_point:" ^ "\n\n- ctx0:\n" + ^ eval_ctx_to_string_no_filter ctx + ^ "\n\n- ctx1:\n" + ^ eval_ctx_to_string_no_filter ctx1 + ^ "\n\n")); + + (* Check if we reached a fixed point: if not, iterate *) + if equiv_ctxs ctx ctx1 then ctx1 else compute_fixed_point ctx1 i0 (i - 1) + in + let fp = compute_fixed_point ctx max_num_iter max_num_iter in + + (* Debug *) + log#ldebug + (lazy + ("compute_fixed_point: fixed point computed before matching with input \ + region groups:" ^ "\n\n- fp:\n" + ^ eval_ctx_to_string_no_filter fp + ^ "\n\n")); + + (* Make sure we have exactly one loop abstraction per function region (merge + abstractions accordingly). + + Rem.: this shouldn't impact the set of symbolic value ids (because we + already merged abstractions "vertically" and are now merging them + "horizontally": the symbolic values contained in the abstractions (typically + the shared values) will be preserved. + *) + let fp, rg_to_abs = + (* List the loop abstractions in the fixed-point *) + let fp_aids, add_aid, _mem_aid = V.AbstractionId.Set.mk_stateful_set () in + + let list_loop_abstractions = + object + inherit [_] C.map_eval_ctx + + method! visit_abs _ abs = + match abs.kind with + | Loop (loop_id', _, kind) -> + assert (loop_id' = loop_id); + assert (kind = V.LoopSynthInput); + (* The abstractions introduced so far should be endable *) + assert (abs.can_end = true); + add_aid abs.abs_id; + abs + | _ -> abs + end + in + let fp = list_loop_abstractions#visit_eval_ctx () fp in + + (* For every input region group: + * - evaluate until we get to a [return] + * - end the input abstraction corresponding to the input region group + * - find which loop abstractions end at that moment + * + * [fp_ended_aids] links region groups to sets of ended abstractions. + *) + let fp_ended_aids = ref T.RegionGroupId.Map.empty in + let add_ended_aids (rg_id : T.RegionGroupId.id) + (aids : V.AbstractionId.Set.t) : unit = + match T.RegionGroupId.Map.find_opt rg_id !fp_ended_aids with + | None -> + fp_ended_aids := T.RegionGroupId.Map.add rg_id aids !fp_ended_aids + | Some aids' -> + let aids = V.AbstractionId.Set.union aids aids' in + fp_ended_aids := T.RegionGroupId.Map.add rg_id aids !fp_ended_aids + in + let cf_loop : st_m_fun = + fun res ctx -> + match res with + | Continue _ | Panic -> + (* We don't want to generate anything *) + None + | Break _ -> + (* We enforce that we can't get there: see {!PrePasses.remove_loop_breaks} *) + raise (Failure "Unreachable") + | Unit | LoopReturn _ | EndEnterLoop _ | EndContinue _ -> + (* For why we can't get [Unit], see the comments inside {!eval_loop_concrete}. + For [EndEnterLoop] and [EndContinue]: we don't support nested loops for now. + *) + raise (Failure "Unreachable") + | Return -> + (* Should we consume the return value and pop the frame? + * If we check in [Interpreter] that the loop abstraction we end is + * indeed the correct one, I think it is sound to under-approximate here + * (and it shouldn't make any difference). + *) + let _ = + List.iter + (fun rg_id -> + (* Lookup the input abstraction - we use the fact that the + abstractions should have been introduced in a specific + order (and we check that it is indeed the case) *) + let abs_id = + V.AbstractionId.of_int (T.RegionGroupId.to_int rg_id) + in + (* By default, the [SynthInput] abs can't end *) + let ctx = C.ctx_set_abs_can_end ctx abs_id true in + assert ( + let abs = C.ctx_lookup_abs ctx abs_id in + abs.kind = V.SynthInput rg_id); + (* End this abstraction *) + let ctx = + 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 ended_ids = V.AbstractionId.Set.diff !fp_aids ids.aids in + add_ended_aids rg_id ended_ids) + ctx.region_groups + in + (* We don't want to generate anything *) + None + in + let _ = eval_loop_body cf_loop fp in + + (* Check that the sets of abstractions we need to end per region group are pairwise + * disjoint *) + let aids_union = ref V.AbstractionId.Set.empty in + let _ = + T.RegionGroupId.Map.iter + (fun _ ids -> + assert (V.AbstractionId.Set.disjoint !aids_union ids); + aids_union := V.AbstractionId.Set.union ids !aids_union) + !fp_ended_aids + in + + (* We also check that all the regions need to end - this is not necessary per + se, but if it doesn't happen it is bizarre and worth investigating... *) + assert (V.AbstractionId.Set.equal !aids_union !fp_aids); + + (* Merge the abstractions which need to be merged, and compute the map from + region id to abstraction id *) + let fp = ref fp in + let rg_to_abs = ref T.RegionGroupId.Map.empty in + let _ = + T.RegionGroupId.Map.iter + (fun rg_id ids -> + let ids = V.AbstractionId.Set.elements ids in + (* Retrieve the first id of the group *) + match ids with + | [] -> + (* We shouldn't get there: we actually introduce reborrows with + {!prepare_ashared_loans} and in the [match_mut_borrows] function + of {!MakeJoinMatcher} to introduce some fresh abstractions for + this purpose. + *) + raise (Failure "Unexpected") + | id0 :: ids -> + let id0 = ref id0 in + (* Add the proper region group into the abstraction *) + let abs_kind = V.Loop (loop_id, Some rg_id, V.LoopSynthInput) in + let abs = C.ctx_lookup_abs !fp !id0 in + let abs = { abs with V.kind = abs_kind } in + let fp', _ = C.ctx_subst_abs !fp !id0 abs in + fp := fp'; + (* Merge all the abstractions into this one *) + List.iter + (fun id -> + try + log#ldebug + (lazy + ("compute_loop_entry_fixed_point: merge FP \ + abstraction: " + ^ V.AbstractionId.to_string id + ^ " into " + ^ V.AbstractionId.to_string !id0)); + (* Note that we merge *into* [id0] *) + let fp', id0' = + merge_into_abstraction loop_id abs_kind false !fp id !id0 + in + fp := fp'; + id0 := id0'; + () + with ValueMatchFailure _ -> raise (Failure "Unexpected")) + ids; + (* Register the mapping *) + let abs = C.ctx_lookup_abs !fp !id0 in + rg_to_abs := T.RegionGroupId.Map.add_strict rg_id abs !rg_to_abs) + !fp_ended_aids + in + let rg_to_abs = !rg_to_abs in + + (* Reorder the loans and borrows in the fresh abstractions in the fixed-point *) + let fp = + reorder_loans_borrows_in_fresh_abs (Option.get !fixed_ids).aids !fp + in + + (* Update the abstraction's [can_end] field and their kinds. + + Note that if [remove_rg_id] is [true], we set the region id to [None] + and set the abstractions as endable: this is so that we can check that + we have a fixed point (so far in the fixed point the loop abstractions had + no region group, and we set them as endable just above). + + If [remove_rg_id] is [false], we simply set the abstractions as non-endable + to freeze them (we will use the fixed point as starting point for the + symbolic execution of the loop body, and we have to make sure the input + abstractions are frozen). + *) + let update_loop_abstractions (remove_rg_id : bool) = + object + inherit [_] C.map_eval_ctx + + method! visit_abs _ abs = + match abs.kind with + | Loop (loop_id', _, kind) -> + assert (loop_id' = loop_id); + assert (kind = V.LoopSynthInput); + let kind = + if remove_rg_id then V.Loop (loop_id, None, V.LoopSynthInput) + else abs.kind + in + { abs with can_end = remove_rg_id; kind } + | _ -> abs + end + in + let update_kinds_can_end (remove_rg_id : bool) ctx = + (update_loop_abstractions remove_rg_id)#visit_eval_ctx () ctx + in + let fp = update_kinds_can_end false fp in + + (* Sanity check: we still have a fixed point - we simply call [compute_fixed_point] + while allowing exactly one iteration to see if it fails *) + let _ = + let fp_test = update_kinds_can_end true fp in + log#ldebug + (lazy + ("compute_fixed_point: fixed point after matching with the function \ + region groups:\n" + ^ eval_ctx_to_string_no_filter fp_test)); + compute_fixed_point fp_test 1 1 + in + + (* Return *) + (fp, rg_to_abs) + in + let fixed_ids = compute_fixed_ids [ fp ] in + + (* Return *) + (fp, fixed_ids, rg_to_abs) + +let compute_fixed_point_id_correspondance (fixed_ids : ids_sets) + (src_ctx : C.eval_ctx) (tgt_ctx : C.eval_ctx) : borrow_loan_corresp = + log#ldebug + (lazy + ("compute_fixed_point_id_correspondance:\n\n- fixed_ids:\n" + ^ show_ids_sets fixed_ids ^ "\n\n- src_ctx:\n" ^ eval_ctx_to_string src_ctx + ^ "\n\n- tgt_ctx:\n" ^ eval_ctx_to_string tgt_ctx ^ "\n\n")); + + let filt_src_env, _, _ = ctx_split_fixed_new fixed_ids src_ctx in + let filt_src_ctx = { src_ctx with env = filt_src_env } in + let filt_tgt_env, new_absl, _ = ctx_split_fixed_new fixed_ids tgt_ctx in + let filt_tgt_ctx = { tgt_ctx with env = filt_tgt_env } in + + log#ldebug + (lazy + ("compute_fixed_point_id_correspondance:\n\n- fixed_ids:\n" + ^ show_ids_sets fixed_ids ^ "\n\n- filt_src_ctx:\n" + ^ eval_ctx_to_string filt_src_ctx + ^ "\n\n- filt_tgt_ctx:\n" + ^ eval_ctx_to_string filt_tgt_ctx + ^ "\n\n")); + + (* Match the source context and the filtered target context *) + let maps = + let check_equiv = false in + let fixed_ids = ids_sets_empty_borrows_loans fixed_ids in + let open InterpreterBorrowsCore in + let lookup_shared_loan lid ctx : V.typed_value = + match snd (lookup_loan ek_all lid ctx) with + | Concrete (V.SharedLoan (_, v)) -> v + | Abstract (V.ASharedLoan (_, v, _)) -> v + | _ -> raise (Failure "Unreachable") + in + let lookup_in_tgt id = lookup_shared_loan id tgt_ctx in + let lookup_in_src id = lookup_shared_loan id src_ctx in + Option.get + (match_ctxs check_equiv fixed_ids lookup_in_tgt lookup_in_src filt_tgt_ctx + filt_src_ctx) + in + + log#ldebug + (lazy + ("compute_fixed_point_id_correspondance:\n\n- tgt_to_src_maps:\n" + ^ show_ids_maps maps ^ "\n\n")); + + let src_to_tgt_borrow_map = + V.BorrowId.Map.of_list + (List.map + (fun (x, y) -> (y, x)) + (V.BorrowId.InjSubst.bindings maps.borrow_id_map)) + in + + (* Sanity check: for every abstraction, the target loans and borrows are mapped + to the same set of source loans and borrows. + + For instance, if we map the [env_fp] to [env0] (only looking at the bindings, + ignoring the abstractions) below: + {[ + env0 = { + abs@0 { ML l0 } + ls -> MB l0 (s2 : loops::List<T>) + i -> s1 : u32 + } + + env_fp = { + abs@0 { ML l0 } + ls -> MB l1 (s3 : loops::List<T>) + i -> s4 : u32 + abs@fp { + MB l0 + ML l1 + } + } + ]} + + We get that l1 is mapped to l0. From there, we see that abs@fp consumes + the same borrows that it gives: it is indeed an identity function. + + TODO: we should also check the mappings for the shared values (to + make sure the abstractions are indeed the identity)... + *) + List.iter + (fun abs -> + let ids, _ = compute_abs_ids abs in + (* Map the *loan* ids (we just match the corresponding *loans* ) *) + let loan_ids = + V.BorrowId.Set.map + (fun x -> V.BorrowId.InjSubst.find x maps.borrow_id_map) + ids.loan_ids + in + (* Check that the loan and borrows are related *) + assert (V.BorrowId.Set.equal ids.borrow_ids loan_ids)) + new_absl; + + (* For every target abstraction (going back to the [list_nth_mut] example, + we have to visit [abs@fp { ML l0, MB l1 }]): + - go through the tgt borrows ([l1]) + - for every tgt borrow, find the corresponding src borrow ([l0], because + we have: [borrows_map: { l1 -> l0 }]) + - from there, find the corresponding tgt loan ([l0]) + + Note that this borrow does not necessarily appear in the src_to_tgt_borrow_map, + if it actually corresponds to a borrows introduced when decomposing the + abstractions to move the shared values out of the source context abstractions. + *) + let tgt_borrow_to_loan = ref V.BorrowId.InjSubst.empty in + let visit_tgt = + object + inherit [_] V.iter_abs + + method! visit_borrow_id _ id = + (* Find the target borrow *) + let tgt_borrow_id = V.BorrowId.Map.find id src_to_tgt_borrow_map in + (* Update the map *) + tgt_borrow_to_loan := + V.BorrowId.InjSubst.add id tgt_borrow_id !tgt_borrow_to_loan + end + in + List.iter (visit_tgt#visit_abs ()) new_absl; + + (* Compute the map from loan to borrows *) + let tgt_loan_to_borrow = + V.BorrowId.InjSubst.of_list + (List.map + (fun (x, y) -> (y, x)) + (V.BorrowId.InjSubst.bindings !tgt_borrow_to_loan)) + in + + (* Return *) + { + borrow_to_loan_id_map = !tgt_borrow_to_loan; + loan_to_borrow_id_map = tgt_loan_to_borrow; + } + +let compute_fp_ctx_symbolic_values (ctx : C.eval_ctx) (fp_ctx : C.eval_ctx) : + V.SymbolicValueId.Set.t * V.symbolic_value list = + let old_ids, _ = compute_context_ids ctx in + let fp_ids, fp_ids_maps = compute_context_ids fp_ctx in + let fresh_sids = V.SymbolicValueId.Set.diff fp_ids.sids old_ids.sids in + + (* Compute the set of symbolic values which appear in shared values inside + *fixed* abstractions: because we introduce fresh abstractions and reborrows + with {!prepare_ashared_loans}, those values are never accessed directly + inside the loop iterations: we can ignore them (and should, because + otherwise it leads to a very ugly translation with duplicated, unused + values) *) + let shared_sids_in_fixed_abs = + let fixed_absl = + List.filter + (fun (ee : C.env_elem) -> + match ee with + | C.Var _ | C.Frame -> false + | Abs abs -> V.AbstractionId.Set.mem abs.abs_id old_ids.aids) + ctx.env + in + + (* Rem.: as we greedily expand the symbolic values containing borrows, and + in particular the (mutable/shared) borrows, we could simply list the + symbolic values appearing in the abstractions: those are necessarily + shared values. We prefer to be more general, in prevision of later + changes. + *) + let sids = ref V.SymbolicValueId.Set.empty in + let visitor = + object (self) + inherit [_] C.iter_env + + method! visit_ASharedLoan inside_shared _ sv child_av = + self#visit_typed_value true sv; + self#visit_typed_avalue inside_shared child_av + + method! visit_symbolic_value_id inside_shared sid = + if inside_shared then sids := V.SymbolicValueId.Set.add sid !sids + end + in + visitor#visit_env false fixed_absl; + !sids + in + + (* Remove the shared symbolic values present in the fixed abstractions - + see comments for [shared_sids_in_fixed_abs]. *) + let sids_to_values = fp_ids_maps.sids_to_values in + + log#ldebug + (lazy + ("compute_fp_ctx_symbolic_values:" ^ "\n- shared_sids_in_fixed_abs:" + ^ V.SymbolicValueId.Set.show shared_sids_in_fixed_abs + ^ "\n- all_sids_to_values: " + ^ V.SymbolicValueId.Map.show (symbolic_value_to_string ctx) sids_to_values + ^ "\n")); + + let sids_to_values = + V.SymbolicValueId.Map.filter + (fun sid _ -> + not (V.SymbolicValueId.Set.mem sid shared_sids_in_fixed_abs)) + sids_to_values + in + + (* List the input symbolic values in proper order. + + We explore the environment, and order the symbolic values in the order + in which they are found - this way, the symbolic values found in a + variable [x] which appears before [y] are listed first, for instance. + *) + let input_svalues = + let found_sids = ref V.SymbolicValueId.Set.empty in + let ordered_sids = ref [] in + + let visitor = + object (self) + inherit [_] C.iter_env + + (** We lookup the shared values *) + method! visit_SharedBorrow env bid = + let open InterpreterBorrowsCore in + let v = + match snd (lookup_loan ek_all bid fp_ctx) with + | Concrete (V.SharedLoan (_, v)) -> v + | Abstract (V.ASharedLoan (_, v, _)) -> v + | _ -> raise (Failure "Unreachable") + in + self#visit_typed_value env v + + method! visit_symbolic_value_id _ id = + if not (V.SymbolicValueId.Set.mem id !found_sids) then ( + found_sids := V.SymbolicValueId.Set.add id !found_sids; + ordered_sids := id :: !ordered_sids) + end + in + + List.iter (visitor#visit_env_elem ()) (List.rev fp_ctx.env); + + List.filter_map + (fun id -> V.SymbolicValueId.Map.find_opt id sids_to_values) + (List.rev !ordered_sids) + in + + log#ldebug + (lazy + ("compute_fp_ctx_symbolic_values:" ^ "\n- src context:\n" + ^ eval_ctx_to_string_no_filter ctx + ^ "\n- fixed point:\n" + ^ eval_ctx_to_string_no_filter fp_ctx + ^ "\n- fresh_sids: " + ^ V.SymbolicValueId.Set.show fresh_sids + ^ "\n- input_svalues: " + ^ Print.list_to_string (symbolic_value_to_string ctx) input_svalues + ^ "\n\n")); + + (fresh_sids, input_svalues) diff --git a/compiler/InterpreterLoopsFixedPoint.mli b/compiler/InterpreterLoopsFixedPoint.mli new file mode 100644 index 00000000..cb03bc9e --- /dev/null +++ b/compiler/InterpreterLoopsFixedPoint.mli @@ -0,0 +1,166 @@ +module T = Types +module PV = PrimitiveValues +module V = Values +module E = Expressions +module C = Contexts +module Subst = Substitute +module A = LlbcAst +module L = Logging +module Inv = Invariants +module S = SynthesizeSymbolic +open InterpreterUtils +open InterpreterLoopsCore + +(** Prepare the shared loans in the abstractions by moving them to fresh + abstractions. + + We use this to prepare an evaluation context before computing a fixed point. + + Because a loop iteration might lead to symbolic value expansions and create + shared loans in shared values inside the *fixed* abstractions, which we want + to leave unchanged, we introduce some reborrows in the following way: + + {[ + abs'0 { SL {l0, l1} s0 } + l0 -> SB l0 + l1 -> SB l1 + + ~~> + + abs'0 { SL {l0, l1} s0 } + l0 -> SB l2 + l1 -> SB l3 + abs'2 { SB l0, SL {l2} s2 } + abs'3 { SB l1, SL {l3} s3 } + ]} + + This is sound but leads to information loss. This way, the fixed abstraction + [abs'0] is never modified because [s0] is never accessed (and thus never + expanded). + + We do this because it makes it easier to compute joins and fixed points. + + **REMARK**: + As a side note, we only reborrow the loan ids whose corresponding borrows + appear in values (i.e., not in abstractions). + + For instance, if we have: + {[ + abs'0 { + SL {l0} s0 + SL {l1} s1 + } + abs'1 { SB l0 } + x -> SB l1 + ]} + + we only introduce a fresh abstraction for [l1]. + *) +val prepare_ashared_loans : V.loop_id option -> Cps.cm_fun + +(** Compute a fixed-point for the context at the entry of the loop. + We also return: + - the sets of fixed ids + - the map from region group id to the corresponding abstraction appearing + in the fixed point (this is useful to compute the return type of the loop + backward functions for instance). + + Rem.: the list of symbolic values should be computable by simply exploring + the fixed point environment and listing all the symbolic values we find. + In the future, we might want to do something more precise, by listing only + the values which are read or modified (some symbolic values may be ignored). + *) +val compute_loop_entry_fixed_point : + C.config -> + V.loop_id -> + Cps.st_cm_fun -> + C.eval_ctx -> + C.eval_ctx * ids_sets * V.abs SymbolicAst.region_group_id_map + +(** For the abstractions in the fixed point, compute the correspondance between + the borrows ids and the loans ids, if we want to introduce equivalent + identity abstractions (i.e., abstractions which do nothing - the input + borrows are exactly the output loans). + + **Context:** + ============ + When we (re-enter) the loop, we want to introduce identity abstractions + (i.e., abstractions which actually only introduce fresh identifiers for + some borrows, to abstract away a bit the borrow graph) which have the same + shape as the abstractions introduced for the fixed point (see the explanations + for [match_ctx_with_target]). This allows us to transform the environment + into a fixed point (again, see the explanations for [match_ctx_with_target]). + + In order to introduce those identity abstractions, we need to figure out, + for those abstractions, which loans should be linked to which borrows. + We do this in the following way. + + We match the fixed point environment with the environment upon first entry + in the loop, and exploit the fact that the fixed point was derived by also + joining this first entry environment: because of that, the borrows in the + abstractions introduced for the fixed-point actually exist in this first + environment (they are not fresh). For [list_nth_mut] (see the explanations + at the top of the file) we have the following: + + {[ + // Environment upon first entry in the loop + env0 = { + abs@0 { ML l0 } + ls -> MB l0 (s2 : loops::List<T>) + i -> s1 : u32 + } + + // Fixed-point environment + env_fp = { + abs@0 { ML l0 } + ls -> MB l1 (s3 : loops::List<T>) + i -> s4 : u32 + abs@fp { + MB l0 // this borrow appears in [env0] + ML l1 + } + } + ]} + + We filter those environments to remove the non-fixed dummy variables, + abstractions, etc. in a manner similar to [match_ctx_with_target]. We + get: + + {[ + filtered_env0 = { + abs@0 { ML l0 } + ls -> MB l0 (s2 : loops::List<T>) + i -> s1 : u32 + } + + filtered_env_fp = { + abs@0 { ML l0 } + ls -> MB l1 (s3 : loops::List<T>) + i -> s@ : u32 + // removed abs@fp + } + ]} + + We then match [filtered_env_fp] with [filtered_env0], taking care to not + consider loans and borrows in a disjoint manner, and ignoring the fixed + values, abstractions, loans, etc. We get: + {[ + borrows_map: { l1 -> l0 } // because we matched [MB l1 ...] with [MB l0 ...] in [ls] + loans_map: {} // we ignore abs@0, which is "fixed" + ]} + + From there we deduce that, if we want to introduce an identity abstraction with the + shape of [abs@fp], we should link [l1] to [l0]. In other words, the value retrieved + through the loan [l1] is actually the value which has to be given back to [l0]. + *) +val compute_fixed_point_id_correspondance : + ids_sets -> C.eval_ctx -> C.eval_ctx -> borrow_loan_corresp + +(** Compute the set of "quantified" symbolic value ids in a fixed-point context. + + We compute: + - the set of symbolic value ids that are freshly introduced + - the list of input symbolic values + *) +val compute_fp_ctx_symbolic_values : + C.eval_ctx -> C.eval_ctx -> V.symbolic_value_id_set * V.symbolic_value list diff --git a/compiler/InterpreterLoopsJoinCtxs.ml b/compiler/InterpreterLoopsJoinCtxs.ml new file mode 100644 index 00000000..6fb0449d --- /dev/null +++ b/compiler/InterpreterLoopsJoinCtxs.ml @@ -0,0 +1,719 @@ +module T = Types +module PV = PrimitiveValues +module V = Values +module E = Expressions +module C = Contexts +module Subst = Substitute +module A = LlbcAst +module L = Logging +open TypesUtils +open ValuesUtils +module Inv = Invariants +module S = SynthesizeSymbolic +module UF = UnionFind +open InterpreterUtils +open InterpreterBorrows +open InterpreterLoopsCore +open InterpreterLoopsMatchCtxs + +(** The local logger *) +let log = L.loops_join_ctxs_log + +(** Reorder the loans and borrows in the fresh abstractions. + + We do this in order to enforce some structure in the environments: this + allows us to find fixed-points. Note that this function needs to be + called typically after we merge abstractions together (see {!collapse_ctx} + for instance). + *) +let reorder_loans_borrows_in_fresh_abs (old_abs_ids : V.AbstractionId.Set.t) + (ctx : C.eval_ctx) : C.eval_ctx = + let reorder_in_fresh_abs (abs : V.abs) : V.abs = + (* Split between the loans and borrows *) + let is_borrow (av : V.typed_avalue) : bool = + match av.V.value with + | ABorrow _ -> true + | ALoan _ -> false + | _ -> raise (Failure "Unexpected") + in + let aborrows, aloans = List.partition is_borrow abs.V.avalues in + + (* Reoder the borrows, and the loans. + + After experimenting, it seems that a good way of reordering the loans + and the borrows to find fixed points is simply to sort them by increasing + order of id (taking the smallest id of a set of ids, in case of sets). + *) + let get_borrow_id (av : V.typed_avalue) : V.BorrowId.id = + match av.V.value with + | V.ABorrow (V.AMutBorrow (bid, _) | V.ASharedBorrow bid) -> bid + | _ -> raise (Failure "Unexpected") + in + let get_loan_id (av : V.typed_avalue) : V.BorrowId.id = + match av.V.value with + | V.ALoan (V.AMutLoan (lid, _)) -> lid + | V.ALoan (V.ASharedLoan (lids, _, _)) -> V.BorrowId.Set.min_elt lids + | _ -> raise (Failure "Unexpected") + in + (* We use ordered maps to reorder the borrows and loans *) + let reorder (get_bid : V.typed_avalue -> V.BorrowId.id) + (values : V.typed_avalue list) : V.typed_avalue list = + List.map snd + (V.BorrowId.Map.bindings + (V.BorrowId.Map.of_list (List.map (fun v -> (get_bid v, v)) values))) + in + let aborrows = reorder get_borrow_id aborrows in + let aloans = reorder get_loan_id aloans in + let avalues = List.append aborrows aloans in + { abs with V.avalues } + in + + let reorder_in_abs (abs : V.abs) = + if V.AbstractionId.Set.mem abs.abs_id old_abs_ids then abs + else reorder_in_fresh_abs abs + in + + let env = C.env_map_abs reorder_in_abs ctx.env in + + { ctx with C.env } + +(** Collapse an environment. + + We do this to simplify an environment, for the purpose of finding a loop + fixed point. + + We do the following: + - we look for all the *new* dummy values (we use sets of old ids to decide + wether a value is new or not) and convert them into abstractions + - whenever there is a new abstraction in the context, and some of its + its borrows are associated to loans in another new abstraction, we + merge them. + In effect, this allows us to merge newly introduced abstractions/borrows + with their parent abstractions. + + For instance, when evaluating the first loop iteration, we start in the + following environment: + {[ + abs@0 { ML l0 } + ls -> MB l0 (s2 : loops::List<T>) + i -> s1 : u32 + ]} + + and get the following environment upon reaching the [Continue] statement: + {[ + abs@0 { ML l0 } + ls -> MB l4 (s@6 : loops::List<T>) + i -> s@7 : u32 + _@1 -> MB l0 (loops::List::Cons (ML l1, ML l2)) + _@2 -> MB l2 (@Box (ML l4)) // tail + _@3 -> MB l1 (s@3 : T) // hd + ]} + + In this new environment, the dummy variables [_@1], [_@2] and [_@3] are + considered as new. + + We first convert the new dummy values to abstractions. It gives: + {[ + abs@0 { ML l0 } + ls -> MB l4 (s@6 : loops::List<T>) + i -> s@7 : u32 + abs@1 { MB l0, ML l1, ML l2 } + abs@2 { MB l2, ML l4 } + abs@3 { MB l1 } + ]} + + We finally merge the new abstractions together. It gives: + {[ + abs@0 { ML l0 } + ls -> MB l4 (s@6 : loops::List<T>) + i -> s@7 : u32 + abs@4 { MB l0, ML l4 } + ]} + + [merge_funs]: those are used to merge loans or borrows which appear in both + abstractions (rem.: here we mean that, for instance, both abstractions + contain a shared loan with id l0). + This can happen when merging environments (note that such environments are not well-formed - + they become well formed again after collapsing). + *) +let collapse_ctx (loop_id : V.LoopId.id) + (merge_funs : merge_duplicates_funcs option) (old_ids : ids_sets) + (ctx0 : C.eval_ctx) : C.eval_ctx = + (* Debug *) + log#ldebug + (lazy + ("collapse_ctx:\n\n- fixed_ids:\n" ^ show_ids_sets old_ids + ^ "\n\n- ctx0:\n" ^ eval_ctx_to_string ctx0 ^ "\n\n")); + + let abs_kind = V.Loop (loop_id, None, LoopSynthInput) in + let can_end = true in + let destructure_shared_values = true in + let is_fresh_abs_id (id : V.AbstractionId.id) : bool = + not (V.AbstractionId.Set.mem id old_ids.aids) + in + let is_fresh_did (id : C.DummyVarId.id) : bool = + not (C.DummyVarId.Set.mem id old_ids.dids) + in + (* Convert the dummy values to abstractions (note that when we convert + values to abstractions, the resulting abstraction should be destructured) *) + (* Note that we preserve the order of the dummy values: we replace them with + abstractions in place - this makes matching easier *) + let env = + List.concat + (List.map + (fun ee -> + match ee with + | C.Abs _ | C.Frame | C.Var (VarBinder _, _) -> [ ee ] + | C.Var (DummyBinder id, v) -> + if is_fresh_did id then + let absl = + convert_value_to_abstractions abs_kind can_end + destructure_shared_values ctx0 v + in + List.map (fun abs -> C.Abs abs) absl + else [ ee ]) + ctx0.env) + in + let ctx = { ctx0 with C.env } in + log#ldebug + (lazy + ("collapse_ctx: after converting values to abstractions:\n" + ^ show_ids_sets old_ids ^ "\n\n- ctx:\n" ^ eval_ctx_to_string ctx ^ "\n\n" + )); + + log#ldebug + (lazy + ("collapse_ctx: after decomposing the shared values in the abstractions:\n" + ^ show_ids_sets old_ids ^ "\n\n- ctx:\n" ^ eval_ctx_to_string ctx ^ "\n\n" + )); + + (* Explore all the *new* abstractions, and compute various maps *) + let explore (abs : V.abs) = is_fresh_abs_id abs.abs_id in + let ids_maps = + compute_abs_borrows_loans_maps (merge_funs = None) explore env + in + let { + abs_ids; + abs_to_borrows; + abs_to_loans = _; + abs_to_borrows_loans; + borrow_to_abs = _; + loan_to_abs; + borrow_loan_to_abs; + } = + ids_maps + in + + (* Change the merging behaviour depending on the input parameters *) + let abs_to_borrows, loan_to_abs = + if merge_funs <> None then (abs_to_borrows_loans, borrow_loan_to_abs) + else (abs_to_borrows, loan_to_abs) + in + + (* Merge the abstractions together *) + let merged_abs : V.AbstractionId.id UF.elem V.AbstractionId.Map.t = + V.AbstractionId.Map.of_list (List.map (fun id -> (id, UF.make id)) abs_ids) + in + + let ctx = ref ctx in + + (* Merge all the mergeable abs. + + We iterate over the abstractions, then over the borrows in the abstractions. + We do this because we want to control the order in which abstractions + are merged (the ids are iterated in increasing order). Otherwise, we + could simply iterate over all the borrows in [borrow_to_abs]... + *) + List.iter + (fun abs_id0 -> + let bids = V.AbstractionId.Map.find abs_id0 abs_to_borrows in + let bids = V.BorrowId.Set.elements bids in + List.iter + (fun bid -> + match V.BorrowId.Map.find_opt bid loan_to_abs with + | None -> (* Nothing to do *) () + | Some abs_ids1 -> + V.AbstractionId.Set.iter + (fun abs_id1 -> + (* We need to merge - unless we have already merged *) + (* First, find the representatives for the two abstractions (the + representative is the abstraction into which we merged) *) + let abs_ref0 = + UF.find (V.AbstractionId.Map.find abs_id0 merged_abs) + in + let abs_id0 = UF.get abs_ref0 in + let abs_ref1 = + UF.find (V.AbstractionId.Map.find abs_id1 merged_abs) + in + let abs_id1 = UF.get abs_ref1 in + (* If the two ids are the same, it means the abstractions were already merged *) + if abs_id0 = abs_id1 then () + else ( + (* We actually need to merge the abstractions *) + + (* Debug *) + log#ldebug + (lazy + ("collapse_ctx: merging abstraction " + ^ V.AbstractionId.to_string abs_id1 + ^ " into " + ^ V.AbstractionId.to_string abs_id0 + ^ ":\n\n" ^ eval_ctx_to_string !ctx)); + + (* Update the environment - pay attention to the order: we + we merge [abs_id1] *into* [abs_id0] *) + let nctx, abs_id = + merge_into_abstraction abs_kind can_end merge_funs !ctx + abs_id1 abs_id0 + in + ctx := nctx; + + (* Update the union find *) + let abs_ref_merged = UF.union abs_ref0 abs_ref1 in + UF.set abs_ref_merged abs_id)) + abs_ids1) + bids) + abs_ids; + + log#ldebug + (lazy + ("collapse_ctx:\n\n- fixed_ids:\n" ^ show_ids_sets old_ids + ^ "\n\n- after collapse:\n" ^ eval_ctx_to_string !ctx ^ "\n\n")); + + (* Reorder the loans and borrows in the fresh abstractions *) + let ctx = reorder_loans_borrows_in_fresh_abs old_ids.aids !ctx in + + log#ldebug + (lazy + ("collapse_ctx:\n\n- fixed_ids:\n" ^ show_ids_sets old_ids + ^ "\n\n- after collapse and reorder borrows/loans:\n" + ^ eval_ctx_to_string ctx ^ "\n\n")); + + (* Return the new context *) + ctx + +let mk_collapse_ctx_merge_duplicate_funs (loop_id : V.LoopId.id) + (ctx : C.eval_ctx) : merge_duplicates_funcs = + (* Rem.: the merge functions raise exceptions (that we catch). *) + let module S : MatchJoinState = struct + let ctx = ctx + let loop_id = loop_id + let nabs = ref [] + end in + let module JM = MakeJoinMatcher (S) in + let module M = MakeMatcher (JM) in + (* Functions to match avalues (see {!merge_duplicates_funcs}). + + Those functions are used to merge borrows/loans with the *same ids*. + + They will always be called on destructured avalues (whose children are + [AIgnored] - we enforce that through sanity checks). We rely on the join + matcher [JM] to match the concrete values (for shared loans for instance). + Note that the join matcher doesn't implement match functions for avalues + (see the comments in {!MakeJoinMatcher}. + *) + let merge_amut_borrows id ty0 child0 _ty1 child1 = + (* Sanity checks *) + assert (is_aignored child0.V.value); + assert (is_aignored child1.V.value); + + (* We need to pick a type for the avalue. The types on the left and on the + right may use different regions: it doesn't really matter (here, we pick + the one from the left), because we will merge those regions together + anyway (see the comments for {!merge_into_abstraction}). + *) + let ty = ty0 in + let child = child0 in + let value = V.ABorrow (V.AMutBorrow (id, child)) in + { V.value; ty } + in + + let merge_ashared_borrows id ty0 ty1 = + (* Sanity checks *) + 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)) + in + + (* Same remarks as for [merge_amut_borrows] *) + let ty = ty0 in + let value = V.ABorrow (V.ASharedBorrow id) in + { V.value; ty } + in + + let merge_amut_loans id ty0 child0 _ty1 child1 = + (* Sanity checks *) + assert (is_aignored child0.V.value); + assert (is_aignored child1.V.value); + (* Same remarks as for [merge_amut_borrows] *) + let ty = ty0 in + let child = child0 in + let value = V.ALoan (V.AMutLoan (id, child)) in + { V.value; ty } + in + let merge_ashared_loans ids ty0 (sv0 : V.typed_value) child0 _ty1 + (sv1 : V.typed_value) child1 = + (* Sanity checks *) + assert (is_aignored child0.V.value); + assert (is_aignored child1.V.value); + (* Same remarks as for [merge_amut_borrows]. + + This time we need to also merge the shared values. We rely on the + join matcher [JM] to do so. + *) + assert (not (value_has_loans_or_borrows ctx sv0.V.value)); + assert (not (value_has_loans_or_borrows ctx sv1.V.value)); + let ty = ty0 in + let child = child0 in + let sv = M.match_typed_values ctx sv0 sv1 in + let value = V.ALoan (V.ASharedLoan (ids, sv, child)) in + { V.value; ty } + in + { + merge_amut_borrows; + merge_ashared_borrows; + merge_amut_loans; + merge_ashared_loans; + } + +let merge_into_abstraction (loop_id : V.LoopId.id) (abs_kind : V.abs_kind) + (can_end : bool) (ctx : C.eval_ctx) (aid0 : V.AbstractionId.id) + (aid1 : V.AbstractionId.id) : C.eval_ctx * V.AbstractionId.id = + let merge_funs = mk_collapse_ctx_merge_duplicate_funs loop_id ctx in + merge_into_abstraction abs_kind can_end (Some merge_funs) ctx aid0 aid1 + +(** Collapse an environment, merging the duplicated borrows/loans. + + This function simply calls {!collapse_ctx} with the proper merging functions. + + We do this because when we join environments, we may introduce duplicated + loans and borrows. See the explanations for {!join_ctxs}. + *) +let collapse_ctx_with_merge (loop_id : V.LoopId.id) (old_ids : ids_sets) + (ctx : C.eval_ctx) : C.eval_ctx = + let merge_funs = mk_collapse_ctx_merge_duplicate_funs loop_id ctx in + try collapse_ctx loop_id (Some merge_funs) old_ids ctx + with ValueMatchFailure _ -> raise (Failure "Unexpected") + +let join_ctxs (loop_id : V.LoopId.id) (fixed_ids : ids_sets) (ctx0 : C.eval_ctx) + (ctx1 : C.eval_ctx) : ctx_or_update = + (* Debug *) + log#ldebug + (lazy + ("join_ctxs:\n\n- fixed_ids:\n" ^ show_ids_sets fixed_ids + ^ "\n\n- ctx0:\n" + ^ eval_ctx_to_string_no_filter ctx0 + ^ "\n\n- ctx1:\n" + ^ eval_ctx_to_string_no_filter ctx1 + ^ "\n\n")); + + let env0 = List.rev ctx0.env in + let env1 = List.rev ctx1.env in + + (* We need to pick a context for some functions like [match_typed_values]: + the context is only used to lookup module data, so we can pick whichever + we want. + TODO: this is not very clean. Maybe we should just carry this data around. + *) + let ctx = ctx0 in + + let nabs = ref [] in + + (* Explore the environments. *) + let join_suffixes (env0 : C.env) (env1 : C.env) : C.env = + (* Debug *) + log#ldebug + (lazy + ("join_suffixes:\n\n- fixed_ids:\n" ^ show_ids_sets fixed_ids + ^ "\n\n- ctx0:\n" + ^ eval_ctx_to_string_no_filter { ctx0 with env = List.rev env0 } + ^ "\n\n- ctx1:\n" + ^ eval_ctx_to_string_no_filter { ctx1 with env = List.rev env1 } + ^ "\n\n")); + + (* Sanity check: there are no values/abstractions which should be in the prefix *) + let check_valid (ee : C.env_elem) : unit = + match ee with + | C.Var (C.VarBinder _, _) -> + (* Variables are necessarily in the prefix *) + raise (Failure "Unreachable") + | Var (C.DummyBinder did, _) -> + assert (not (C.DummyVarId.Set.mem did fixed_ids.dids)) + | Abs abs -> + assert (not (V.AbstractionId.Set.mem abs.abs_id fixed_ids.aids)) + | Frame -> + (* This should have been eliminated *) + raise (Failure "Unreachable") + in + List.iter check_valid env0; + List.iter check_valid env1; + (* Concatenate the suffixes and append the abstractions introduced while + joining the prefixes *) + let absl = List.map (fun abs -> C.Abs abs) (List.rev !nabs) in + List.concat [ env0; env1; absl ] + in + + let module S : MatchJoinState = struct + (* The context is only used to lookup module data: we can pick whichever we want *) + let ctx = ctx + let loop_id = loop_id + let nabs = nabs + end in + let module JM = MakeJoinMatcher (S) in + let module M = MakeMatcher (JM) in + (* Rem.: this function raises exceptions *) + let rec join_prefixes (env0 : C.env) (env1 : C.env) : C.env = + match (env0, env1) with + | ( (C.Var (C.DummyBinder b0, v0) as var0) :: env0', + (C.Var (C.DummyBinder b1, v1) as var1) :: env1' ) -> + (* Debug *) + log#ldebug + (lazy + ("join_prefixes: DummyBinders:\n\n- fixed_ids:\n" ^ "\n" + ^ show_ids_sets fixed_ids ^ "\n\n- value0:\n" + ^ env_elem_to_string ctx var0 + ^ "\n\n- value1:\n" + ^ env_elem_to_string ctx var1 + ^ "\n\n")); + + (* Two cases: the dummy value is an old value, in which case the bindings + must be the same and we must join their values. Otherwise, it means we + are not in the prefix anymore *) + if C.DummyVarId.Set.mem b0 fixed_ids.dids then ( + (* Still in the prefix: match the values *) + assert (b0 = b1); + let b = b0 in + let v = M.match_typed_values ctx v0 v1 in + let var = C.Var (C.DummyBinder b, v) in + (* Continue *) + var :: join_prefixes env0' env1') + else (* Not in the prefix anymore *) + join_suffixes env0 env1 + | ( (C.Var (C.VarBinder b0, v0) as var0) :: env0', + (C.Var (C.VarBinder b1, v1) as var1) :: env1' ) -> + (* Debug *) + log#ldebug + (lazy + ("join_prefixes: VarBinders:\n\n- fixed_ids:\n" ^ "\n" + ^ show_ids_sets fixed_ids ^ "\n\n- value0:\n" + ^ env_elem_to_string ctx var0 + ^ "\n\n- value1:\n" + ^ env_elem_to_string ctx var1 + ^ "\n\n")); + + (* Variable bindings *must* be in the prefix and consequently their + ids must be the same *) + assert (b0 = b1); + (* Match the values *) + let b = b0 in + let v = M.match_typed_values ctx v0 v1 in + let var = C.Var (C.VarBinder b, v) in + (* Continue *) + var :: join_prefixes env0' env1' + | (C.Abs abs0 as abs) :: env0', C.Abs abs1 :: env1' -> + (* Debug *) + log#ldebug + (lazy + ("join_prefixes: Abs:\n\n- fixed_ids:\n" ^ "\n" + ^ show_ids_sets fixed_ids ^ "\n\n- abs0:\n" ^ abs_to_string ctx abs0 + ^ "\n\n- abs1:\n" ^ abs_to_string ctx abs1 ^ "\n\n")); + + (* Same as for the dummy values: there are two cases *) + if V.AbstractionId.Set.mem abs0.abs_id fixed_ids.aids then ( + (* Still in the prefix: the abstractions must be the same *) + assert (abs0 = abs1); + (* Continue *) + abs :: join_prefixes env0' env1') + else (* Not in the prefix anymore *) + join_suffixes env0 env1 + | _ -> + (* The elements don't match: we are not in the prefix anymore *) + join_suffixes env0 env1 + in + + try + (* Remove the frame delimiter (the first element of an environment is a frame delimiter) *) + let env0, env1 = + match (env0, env1) with + | C.Frame :: env0, C.Frame :: env1 -> (env0, env1) + | _ -> raise (Failure "Unreachable") + in + + log#ldebug + (lazy + ("- env0:\n" ^ C.show_env env0 ^ "\n\n- env1:\n" ^ C.show_env env1 + ^ "\n\n")); + + let env = List.rev (C.Frame :: join_prefixes env0 env1) in + + (* Construct the joined context - of course, the type, fun, etc. contexts + * should be the same in the two contexts *) + let { + C.type_context; + fun_context; + global_context; + region_groups; + type_vars; + env = _; + ended_regions = ended_regions0; + } = + ctx0 + in + let { + C.type_context = _; + fun_context = _; + global_context = _; + region_groups = _; + type_vars = _; + env = _; + ended_regions = ended_regions1; + } = + ctx1 + in + let ended_regions = T.RegionId.Set.union ended_regions0 ended_regions1 in + Ok + { + C.type_context; + fun_context; + global_context; + region_groups; + type_vars; + env; + ended_regions; + } + with ValueMatchFailure e -> Error e + +(** Destructure all the new abstractions *) +let destructure_new_abs (loop_id : V.LoopId.id) + (old_abs_ids : V.AbstractionId.Set.t) (ctx : C.eval_ctx) : C.eval_ctx = + let abs_kind = V.Loop (loop_id, None, V.LoopSynthInput) in + let can_end = true in + let destructure_shared_values = true in + let is_fresh_abs_id (id : V.AbstractionId.id) : bool = + not (V.AbstractionId.Set.mem id old_abs_ids) + in + let env = + C.env_map_abs + (fun abs -> + if is_fresh_abs_id abs.abs_id then + let abs = + destructure_abs abs_kind can_end destructure_shared_values ctx abs + in + abs + else abs) + ctx.env + in + { ctx with env } + +(** Refresh the ids of the fresh abstractions. + + We do this because {!prepare_ashared_loans} introduces some non-fixed + abstractions in contexts which are later joined: we have to make sure two + contexts we join don't have non-fixed abstractions with the same ids. + *) +let refresh_abs (old_abs : V.AbstractionId.Set.t) (ctx : C.eval_ctx) : + C.eval_ctx = + let ids, _ = compute_context_ids ctx in + let abs_to_refresh = V.AbstractionId.Set.diff ids.aids old_abs in + let aids_subst = + List.map + (fun id -> (id, C.fresh_abstraction_id ())) + (V.AbstractionId.Set.elements abs_to_refresh) + in + let aids_subst = V.AbstractionId.Map.of_list aids_subst in + let subst id = + match V.AbstractionId.Map.find_opt id aids_subst with + | None -> id + | Some id -> id + in + let env = + Subst.env_subst_ids + (fun x -> x) + (fun x -> x) + (fun x -> x) + (fun x -> x) + (fun x -> x) + subst ctx.env + in + { ctx with C.env } + +let loop_join_origin_with_continue_ctxs (config : C.config) + (loop_id : V.LoopId.id) (fixed_ids : ids_sets) (old_ctx : C.eval_ctx) + (ctxl : C.eval_ctx list) : (C.eval_ctx * C.eval_ctx list) * C.eval_ctx = + (* # Join with the new contexts, one by one + + For every context, we repeteadly attempt to join it with the current + result of the join: if we fail (because we need to end loans for instance), + we update the context and retry. + Rem.: we should never have to end loans in the aggregated context, only + in the one we are trying to add to the join. + *) + let joined_ctx = ref old_ctx in + let rec join_one_aux (ctx : C.eval_ctx) : C.eval_ctx = + match join_ctxs loop_id fixed_ids !joined_ctx ctx with + | Ok nctx -> + joined_ctx := nctx; + ctx + | Error err -> + let ctx = + match err with + | LoanInRight bid -> + InterpreterBorrows.end_borrow_no_synth config bid ctx + | LoansInRight bids -> + InterpreterBorrows.end_borrows_no_synth config bids ctx + | AbsInRight _ | AbsInLeft _ | LoanInLeft _ | LoansInLeft _ -> + raise (Failure "Unexpected") + in + join_one_aux ctx + in + let join_one (ctx : C.eval_ctx) : C.eval_ctx = + log#ldebug + (lazy + ("loop_join_origin_with_continue_ctxs:join_one: initial ctx:\n" + ^ eval_ctx_to_string ctx)); + + (* Destructure the abstractions introduced in the new context *) + let ctx = destructure_new_abs loop_id fixed_ids.aids ctx in + log#ldebug + (lazy + ("loop_join_origin_with_continue_ctxs:join_one: after destructure:\n" + ^ eval_ctx_to_string ctx)); + + (* Collapse the context we want to add to the join *) + let ctx = collapse_ctx loop_id None fixed_ids ctx in + log#ldebug + (lazy + ("loop_join_origin_with_continue_ctxs:join_one: after collapse:\n" + ^ eval_ctx_to_string ctx)); + + (* Refresh the fresh abstractions *) + let ctx = refresh_abs fixed_ids.aids ctx in + + (* Join the two contexts *) + let ctx1 = join_one_aux ctx in + log#ldebug + (lazy + ("loop_join_origin_with_continue_ctxs:join_one: after join:\n" + ^ eval_ctx_to_string ctx1)); + + (* Collapse again - the join might have introduce abstractions we want + to merge with the others (note that those abstractions may actually + lead to borrows/loans duplications) *) + joined_ctx := collapse_ctx_with_merge loop_id fixed_ids !joined_ctx; + log#ldebug + (lazy + ("loop_join_origin_with_continue_ctxs:join_one: after join-collapse:\n" + ^ eval_ctx_to_string !joined_ctx)); + + (* Sanity check *) + if !Config.check_invariants then Invariants.check_invariants !joined_ctx; + (* Return *) + ctx1 + in + + let ctxl = List.map join_one ctxl in + + (* # Return *) + ((old_ctx, ctxl), !joined_ctx) diff --git a/compiler/InterpreterLoopsJoinCtxs.mli b/compiler/InterpreterLoopsJoinCtxs.mli new file mode 100644 index 00000000..ae655fb8 --- /dev/null +++ b/compiler/InterpreterLoopsJoinCtxs.mli @@ -0,0 +1,120 @@ +module T = Types +module PV = PrimitiveValues +module V = Values +module E = Expressions +module C = Contexts +module Subst = Substitute +module A = LlbcAst +module L = Logging +module Inv = Invariants +module S = SynthesizeSymbolic +open InterpreterUtils +open InterpreterLoopsCore + +(** Merge an abstraction into another abstraction in a context. + + This function is similar to {!InterpreterBorrows.merge_into_abstraction}. + + Parameters: + - [loop_id] + - [abs_kind] + - [can_end] + - [ctx] + - [aid0] + - [aid1] + *) +val merge_into_abstraction : + V.loop_id -> + V.abs_kind -> + bool -> + C.eval_ctx -> + V.abstraction_id -> + V.abstraction_id -> + C.eval_ctx * V.abstraction_id + +(** Join two contexts. + + We use this to join the environments at loop (re-)entry to progressively + compute a fixed point. + + We make the hypothesis (and check it) that the environments have the same + prefixes (same variable ids, same abstractions, etc.). The prefix of + variable and abstraction ids is given by the [fixed_ids] identifier sets. We + check that those prefixes are the same (the dummy variables are the same, + the abstractions are the same), match the values mapped to by the variables + which are not dummy, then group the additional dummy variables/abstractions + together. In a sense, the [fixed_ids] define a frame (in a separation logic + sense). + + Note that when joining the values mapped to by the non-dummy variables, we + may introduce duplicated borrows. Also, we don't match the abstractions + which are not in the prefix, and this can also lead to borrow + duplications. For this reason, the environment needs to be collapsed + afterwards to get rid of those duplicated loans/borrows. + + For instance, if we have: + {[ + fixed = { abs0 } + + env0 = { + abs0 { ML l0 } + l -> MB l0 s0 + } + + env1 = { + abs0 { ML l0 } + l -> MB l1 s1 + abs1 { MB l0, ML l1 } + } + ]} + + We get: + {[ + join env0 env1 = { + abs0 { ML l0 } (* abs0 is fixed: we simply check it is equal in env0 and env1 *) + l -> MB l2 s2 + abs1 { MB l0, ML l1 } (* abs1 is new: we keep it unchanged *) + abs2 { MB l0, MB l1, ML l2 } (* Introduced when joining on the "l" variable *) + } + ]} + + Rem.: in practice, this join works because we take care of pushing new values + and abstractions *at the end* of the environments, meaning the environment + prefixes keep the same structure. + + Rem.: assuming that the environment has some structure poses *no soundness + issue*. It can only make the join fail if the environments actually don't have + this structure: this is a *completeness issue*. + + Parameters: + - [loop_id] + - [fixed_ids] + - [ctx0] + - [ctx1] + *) +val join_ctxs : + V.loop_id -> ids_sets -> C.eval_ctx -> C.eval_ctx -> ctx_or_update + +(** Join the context at the entry of the loop with the contexts upon reentry + (upon reaching the [Continue] statement - the goal is to compute a fixed + point for the loop entry). + + As we may have to end loans in the environments before doing the join, + we return those updated environments, and the joined environment. + + This function is mostly built on top of {!join_ctxs}. + + Parameters: + - [config] + - [loop_id] + - [fixed_ids] + - [old_ctx] + - [ctxl] + *) +val loop_join_origin_with_continue_ctxs : + C.config -> + V.loop_id -> + ids_sets -> + C.eval_ctx -> + C.eval_ctx list -> + (C.eval_ctx * C.eval_ctx list) * C.eval_ctx diff --git a/compiler/InterpreterLoopsMatchCtxs.ml b/compiler/InterpreterLoopsMatchCtxs.ml new file mode 100644 index 00000000..f9d45f20 --- /dev/null +++ b/compiler/InterpreterLoopsMatchCtxs.ml @@ -0,0 +1,1591 @@ +(** This module implements support to match contexts for loops. + + The matching functions are used for instance to compute joins, or + to check if two contexts are equivalent (modulo conversion). + *) + +module T = Types +module PV = PrimitiveValues +module V = Values +module E = Expressions +module C = Contexts +module Subst = Substitute +module A = LlbcAst +module L = Logging +open TypesUtils +open ValuesUtils +module Inv = Invariants +module S = SynthesizeSymbolic +open Cps +open InterpreterUtils +open InterpreterBorrows +open InterpreterLoopsCore + +(** The local logger *) +let log = L.loops_match_ctxs_log + +let compute_abs_borrows_loans_maps (no_duplicates : bool) + (explore : V.abs -> bool) (env : C.env) : abs_borrows_loans_maps = + let abs_ids = ref [] in + let abs_to_borrows = ref V.AbstractionId.Map.empty in + let abs_to_loans = ref V.AbstractionId.Map.empty in + let abs_to_borrows_loans = ref V.AbstractionId.Map.empty in + let borrow_to_abs = ref V.BorrowId.Map.empty in + let loan_to_abs = ref V.BorrowId.Map.empty in + let borrow_loan_to_abs = ref V.BorrowId.Map.empty in + + let module R (Id0 : Identifiers.Id) (Id1 : Identifiers.Id) = struct + (* + [check_singleton_sets]: check that the mapping maps to a singletong. + [check_not_already_registered]: check if the mapping was not already registered. + *) + let register_mapping (check_singleton_sets : bool) + (check_not_already_registered : bool) (map : Id1.Set.t Id0.Map.t ref) + (id0 : Id0.id) (id1 : Id1.id) : unit = + (* Sanity check *) + (if check_singleton_sets || check_not_already_registered then + match Id0.Map.find_opt id0 !map with + | None -> () + | Some set -> + assert ( + (not check_not_already_registered) || not (Id1.Set.mem id1 set))); + (* Update the mapping *) + map := + Id0.Map.update id0 + (fun ids -> + match ids with + | None -> Some (Id1.Set.singleton id1) + | Some ids -> + (* Sanity check *) + assert (not check_singleton_sets); + assert ( + (not check_not_already_registered) + || not (Id1.Set.mem id1 ids)); + (* Update *) + Some (Id1.Set.add id1 ids)) + !map + end in + let module RAbsBorrow = R (V.AbstractionId) (V.BorrowId) in + let module RBorrowAbs = R (V.BorrowId) (V.AbstractionId) in + let register_borrow_id abs_id bid = + RAbsBorrow.register_mapping false no_duplicates abs_to_borrows abs_id bid; + RAbsBorrow.register_mapping false false abs_to_borrows_loans abs_id bid; + RBorrowAbs.register_mapping no_duplicates no_duplicates borrow_to_abs bid + abs_id; + RBorrowAbs.register_mapping false false borrow_loan_to_abs bid abs_id + in + + let register_loan_id abs_id bid = + RAbsBorrow.register_mapping false no_duplicates abs_to_loans abs_id bid; + RAbsBorrow.register_mapping false false abs_to_borrows_loans abs_id bid; + RBorrowAbs.register_mapping no_duplicates no_duplicates loan_to_abs bid + abs_id; + RBorrowAbs.register_mapping false false borrow_loan_to_abs bid abs_id + in + + let explore_abs = + object (self : 'self) + inherit [_] V.iter_typed_avalue as super + + (** Make sure we don't register the ignored ids *) + method! visit_aloan_content abs_id lc = + match lc with + | AMutLoan _ | ASharedLoan _ -> + (* Process those normally *) + super#visit_aloan_content abs_id lc + | AIgnoredMutLoan (_, child) + | AEndedIgnoredMutLoan { child; given_back = _; given_back_meta = _ } + | AIgnoredSharedLoan child -> + (* Ignore the id of the loan, if there is *) + self#visit_typed_avalue abs_id child + | AEndedMutLoan _ | AEndedSharedLoan _ -> raise (Failure "Unreachable") + + (** Make sure we don't register the ignored ids *) + method! visit_aborrow_content abs_id bc = + match bc with + | AMutBorrow _ | ASharedBorrow _ | AProjSharedBorrow _ -> + (* Process those normally *) + super#visit_aborrow_content abs_id bc + | AIgnoredMutBorrow (_, child) + | AEndedIgnoredMutBorrow { child; given_back = _; given_back_meta = _ } + -> + (* Ignore the id of the borrow, if there is *) + self#visit_typed_avalue abs_id child + | AEndedMutBorrow _ | AEndedSharedBorrow -> + raise (Failure "Unreachable") + + method! visit_borrow_id abs_id bid = register_borrow_id abs_id bid + method! visit_loan_id abs_id lid = register_loan_id abs_id lid + end + in + + C.env_iter_abs + (fun abs -> + let abs_id = abs.abs_id in + if explore abs then ( + abs_to_borrows := + V.AbstractionId.Map.add abs_id V.BorrowId.Set.empty !abs_to_borrows; + abs_to_loans := + V.AbstractionId.Map.add abs_id V.BorrowId.Set.empty !abs_to_loans; + abs_ids := abs.abs_id :: !abs_ids; + List.iter (explore_abs#visit_typed_avalue abs.abs_id) abs.avalues) + else ()) + env; + + (* Rem.: there is no need to reverse the abs ids, because we explored the environment + starting with the freshest values and abstractions *) + { + abs_ids = !abs_ids; + abs_to_borrows = !abs_to_borrows; + abs_to_loans = !abs_to_loans; + abs_to_borrows_loans = !abs_to_borrows_loans; + borrow_to_abs = !borrow_to_abs; + loan_to_abs = !loan_to_abs; + borrow_loan_to_abs = !borrow_loan_to_abs; + } + +(** Match two types during a join. *) +let rec match_types (match_distinct_types : 'r T.ty -> 'r T.ty -> 'r T.ty) + (match_regions : 'r -> 'r -> 'r) (ty0 : 'r T.ty) (ty1 : 'r T.ty) : 'r T.ty = + let match_rec = match_types match_distinct_types match_regions in + match (ty0, ty1) with + | Adt (id0, regions0, tys0), Adt (id1, regions1, tys1) -> + assert (id0 = id1); + let id = id0 in + let regions = + List.map + (fun (id0, id1) -> match_regions id0 id1) + (List.combine regions0 regions1) + in + let tys = + List.map (fun (ty0, ty1) -> match_rec ty0 ty1) (List.combine tys0 tys1) + in + Adt (id, regions, tys) + | TypeVar vid0, TypeVar vid1 -> + assert (vid0 = vid1); + let vid = vid0 in + TypeVar vid + | Bool, Bool | Char, Char | Never, Never | Str, Str -> ty0 + | Integer int_ty0, Integer int_ty1 -> + assert (int_ty0 = int_ty1); + ty0 + | Array ty0, Array ty1 | Slice ty0, Slice ty1 -> match_rec ty0 ty1 + | Ref (r0, ty0, k0), Ref (r1, ty1, k1) -> + let r = match_regions r0 r1 in + let ty = match_rec ty0 ty1 in + assert (k0 = k1); + let k = k0 in + Ref (r, ty, k) + | _ -> match_distinct_types ty0 ty1 + +module MakeMatcher (M : PrimMatcher) : Matcher = struct + let rec match_typed_values (ctx : C.eval_ctx) (v0 : V.typed_value) + (v1 : V.typed_value) : V.typed_value = + let match_rec = match_typed_values ctx in + let ty = M.match_etys v0.V.ty v1.V.ty in + match (v0.V.value, v1.V.value) with + | V.Primitive pv0, V.Primitive pv1 -> + if pv0 = pv1 then v1 else M.match_distinct_primitive_values ty pv0 pv1 + | V.Adt av0, V.Adt av1 -> + if av0.variant_id = av1.variant_id then + let fields = List.combine av0.field_values av1.field_values in + let field_values = + List.map (fun (f0, f1) -> match_rec f0 f1) fields + in + let value : V.value = + V.Adt { variant_id = av0.variant_id; field_values } + in + { V.value; ty = v1.V.ty } + else ( + (* For now, we don't merge ADTs which contain borrows *) + assert (not (value_has_borrows ctx v0.V.value)); + assert (not (value_has_borrows ctx v1.V.value)); + (* Merge *) + M.match_distinct_adts ty av0 av1) + | Bottom, Bottom -> v0 + | Borrow bc0, Borrow bc1 -> + let bc = + match (bc0, bc1) with + | SharedBorrow bid0, SharedBorrow bid1 -> + let bid = M.match_shared_borrows match_rec ty bid0 bid1 in + V.SharedBorrow bid + | MutBorrow (bid0, bv0), MutBorrow (bid1, bv1) -> + let bv = match_rec bv0 bv1 in + assert (not (value_has_borrows ctx bv.V.value)); + let bid, bv = M.match_mut_borrows ty bid0 bv0 bid1 bv1 bv in + V.MutBorrow (bid, bv) + | ReservedMutBorrow _, _ + | _, ReservedMutBorrow _ + | SharedBorrow _, MutBorrow _ + | MutBorrow _, SharedBorrow _ -> + (* If we get here, either there is a typing inconsistency, or we are + trying to match a reserved borrow, which shouldn't happen because + reserved borrow should be eliminated very quickly - they are introduced + just before function calls which activate them *) + raise (Failure "Unexpected") + in + { V.value = V.Borrow bc; ty } + | Loan lc0, Loan lc1 -> + (* TODO: maybe we should enforce that the ids are always exactly the same - + without matching *) + let lc = + match (lc0, lc1) with + | SharedLoan (ids0, sv0), SharedLoan (ids1, sv1) -> + let sv = match_rec sv0 sv1 in + assert (not (value_has_borrows ctx sv.V.value)); + let ids, sv = M.match_shared_loans ty ids0 ids1 sv in + V.SharedLoan (ids, sv) + | MutLoan id0, MutLoan id1 -> + let id = M.match_mut_loans ty id0 id1 in + V.MutLoan id + | SharedLoan _, MutLoan _ | MutLoan _, SharedLoan _ -> + raise (Failure "Unreachable") + in + { V.value = Loan lc; ty = v1.V.ty } + | Symbolic sv0, Symbolic sv1 -> + (* For now, we force all the symbolic values containing borrows to + be eagerly expanded, and we don't support nested borrows *) + assert (not (value_has_borrows ctx v0.V.value)); + assert (not (value_has_borrows ctx v1.V.value)); + (* Match *) + let sv = M.match_symbolic_values sv0 sv1 in + { v1 with V.value = V.Symbolic sv } + | Loan lc, _ -> ( + match lc with + | SharedLoan (ids, _) -> raise (ValueMatchFailure (LoansInLeft ids)) + | MutLoan id -> raise (ValueMatchFailure (LoanInLeft id))) + | _, Loan lc -> ( + match lc with + | SharedLoan (ids, _) -> raise (ValueMatchFailure (LoansInRight ids)) + | MutLoan id -> raise (ValueMatchFailure (LoanInRight id))) + | Symbolic sv, _ -> M.match_symbolic_with_other true sv v1 + | _, Symbolic sv -> M.match_symbolic_with_other false sv v0 + | Bottom, _ -> M.match_bottom_with_other true v1 + | _, Bottom -> M.match_bottom_with_other false v0 + | _ -> + log#ldebug + (lazy + ("Unexpected match case:\n- value0: " + ^ typed_value_to_string ctx v0 + ^ "\n- value1: " + ^ typed_value_to_string ctx v1)); + raise (Failure "Unexpected match case") + + and match_typed_avalues (ctx : C.eval_ctx) (v0 : V.typed_avalue) + (v1 : V.typed_avalue) : V.typed_avalue = + log#ldebug + (lazy + ("match_typed_avalues:\n- value0: " + ^ typed_avalue_to_string ctx v0 + ^ "\n- value1: " + ^ typed_avalue_to_string ctx v1)); + + let match_rec = match_typed_values ctx in + let match_arec = match_typed_avalues ctx in + let ty = M.match_rtys v0.V.ty v1.V.ty in + match (v0.V.value, v1.V.value) with + | V.AAdt av0, V.AAdt av1 -> + if av0.variant_id = av1.variant_id then + let fields = List.combine av0.field_values av1.field_values in + let field_values = + List.map (fun (f0, f1) -> match_arec f0 f1) fields + in + let value : V.avalue = + V.AAdt { variant_id = av0.variant_id; field_values } + in + { V.value; ty } + else (* Merge *) + M.match_distinct_aadts v0.V.ty av0 v1.V.ty av1 ty + | ABottom, ABottom -> mk_abottom ty + | AIgnored, AIgnored -> mk_aignored ty + | ABorrow bc0, ABorrow bc1 -> ( + log#ldebug (lazy "match_typed_avalues: borrows"); + match (bc0, bc1) with + | ASharedBorrow bid0, ASharedBorrow bid1 -> + log#ldebug (lazy "match_typed_avalues: shared borrows"); + M.match_ashared_borrows v0.V.ty bid0 v1.V.ty bid1 ty + | AMutBorrow (bid0, av0), AMutBorrow (bid1, av1) -> + log#ldebug (lazy "match_typed_avalues: mut borrows"); + log#ldebug + (lazy + "match_typed_avalues: mut borrows: matching children values"); + let av = match_arec av0 av1 in + log#ldebug + (lazy "match_typed_avalues: mut borrows: matched children values"); + M.match_amut_borrows v0.V.ty bid0 av0 v1.V.ty bid1 av1 ty av + | AIgnoredMutBorrow _, AIgnoredMutBorrow _ -> + (* The abstractions are destructured: we shouldn't get there *) + raise (Failure "Unexpected") + | AProjSharedBorrow asb0, AProjSharedBorrow asb1 -> ( + match (asb0, asb1) with + | [], [] -> + (* This case actually stands for ignored shared borrows, when + there are no nested borrows *) + v0 + | _ -> + (* We should get there only if there are nested borrows *) + raise (Failure "Unexpected")) + | _ -> + (* TODO: getting there is not necessarily inconsistent (it may + just be because the environments don't match) so we may want + to call a specific function (which could raise the proper + exception). + Rem.: we shouldn't get to the ended borrow cases, because + an abstraction should never contain ended borrows unless + we are *currently* ending it, in which case we need + to completely end it before continuing. + *) + raise (Failure "Unexpected")) + | ALoan lc0, ALoan lc1 -> ( + log#ldebug (lazy "match_typed_avalues: loans"); + (* TODO: maybe we should enforce that the ids are always exactly the same - + without matching *) + match (lc0, lc1) with + | ASharedLoan (ids0, sv0, av0), ASharedLoan (ids1, sv1, av1) -> + log#ldebug (lazy "match_typed_avalues: shared loans"); + let sv = match_rec sv0 sv1 in + let av = match_arec av0 av1 in + assert (not (value_has_borrows ctx sv.V.value)); + M.match_ashared_loans v0.V.ty ids0 sv0 av0 v1.V.ty ids1 sv1 av1 ty + sv av + | AMutLoan (id0, av0), AMutLoan (id1, av1) -> + log#ldebug (lazy "match_typed_avalues: mut loans"); + log#ldebug + (lazy "match_typed_avalues: mut loans: matching children values"); + let av = match_arec av0 av1 in + log#ldebug + (lazy "match_typed_avalues: mut loans: matched children values"); + M.match_amut_loans v0.V.ty id0 av0 v1.V.ty id1 av1 ty av + | AIgnoredMutLoan _, AIgnoredMutLoan _ + | AIgnoredSharedLoan _, AIgnoredSharedLoan _ -> + (* Those should have been filtered when destructuring the abstractions - + they are necessary only when there are nested borrows *) + raise (Failure "Unreachable") + | _ -> raise (Failure "Unreachable")) + | ASymbolic _, ASymbolic _ -> + (* For now, we force all the symbolic values containing borrows to + be eagerly expanded, and we don't support nested borrows *) + raise (Failure "Unreachable") + | _ -> M.match_avalues v0 v1 +end + +module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct + (** Small utility *) + let push_abs (abs : V.abs) : unit = S.nabs := abs :: !S.nabs + + let push_absl (absl : V.abs list) : unit = List.iter push_abs absl + + let match_etys ty0 ty1 = + assert (ty0 = ty1); + ty0 + + let match_rtys ty0 ty1 = + (* The types must be equal - in effect, this forbids to match symbolic + values containing borrows *) + assert (ty0 = ty1); + ty0 + + let match_distinct_primitive_values (ty : T.ety) (_ : V.primitive_value) + (_ : V.primitive_value) : V.typed_value = + mk_fresh_symbolic_typed_value_from_ety V.LoopJoin ty + + let match_distinct_adts (ty : T.ety) (adt0 : V.adt_value) (adt1 : V.adt_value) + : V.typed_value = + (* Check that the ADTs don't contain borrows - this is redundant with checks + performed by the caller, but we prefer to be safe with regards to future + updates + *) + let check_no_borrows (v : V.typed_value) = + assert (not (value_has_borrows S.ctx v.V.value)) + in + List.iter check_no_borrows adt0.field_values; + List.iter check_no_borrows adt1.field_values; + + (* Check if there are loans: we request to end them *) + let check_loans (left : bool) (fields : V.typed_value list) : unit = + match InterpreterBorrowsCore.get_first_loan_in_values fields with + | Some (V.SharedLoan (ids, _)) -> + if left then raise (ValueMatchFailure (LoansInLeft ids)) + else raise (ValueMatchFailure (LoansInRight ids)) + | Some (V.MutLoan id) -> + if left then raise (ValueMatchFailure (LoanInLeft id)) + else raise (ValueMatchFailure (LoanInRight id)) + | None -> () + in + check_loans true adt0.field_values; + check_loans false adt1.field_values; + + (* No borrows, no loans: we can introduce a symbolic value *) + mk_fresh_symbolic_typed_value_from_ety V.LoopJoin ty + + let match_shared_borrows _ (ty : T.ety) (bid0 : V.borrow_id) + (bid1 : V.borrow_id) : V.borrow_id = + if bid0 = bid1 then bid0 + else + (* We replace bid0 and bid1 with a fresh borrow id, and introduce + an abstraction which links all of them: + {[ + { SB bid0, SB bid1, SL {bid2} } + ]} + *) + let rid = C.fresh_region_id () in + let bid2 = C.fresh_borrow_id () in + + (* Generate a fresh symbolic value for the shared value *) + let _, bv_ty, kind = ty_as_ref ty in + let sv = mk_fresh_symbolic_typed_value_from_ety V.LoopJoin bv_ty in + + let borrow_ty = + mk_ref_ty (T.Var rid) (ety_no_regions_to_rty bv_ty) kind + in + + (* Generate the avalues for the abstraction *) + let mk_aborrow (bid : V.borrow_id) : V.typed_avalue = + let value = V.ABorrow (V.ASharedBorrow bid) in + { V.value; ty = borrow_ty } + in + let borrows = [ mk_aborrow bid0; mk_aborrow bid1 ] in + + let loan = + V.ASharedLoan + ( V.BorrowId.Set.singleton bid2, + sv, + mk_aignored (ety_no_regions_to_rty bv_ty) ) + in + (* Note that an aloan has a borrow type *) + let loan = { V.value = V.ALoan loan; ty = borrow_ty } in + + let avalues = List.append borrows [ loan ] in + + (* Generate the abstraction *) + let abs = + { + V.abs_id = C.fresh_abstraction_id (); + kind = V.Loop (S.loop_id, None, LoopSynthInput); + can_end = true; + parents = V.AbstractionId.Set.empty; + original_parents = []; + regions = T.RegionId.Set.singleton rid; + ancestors_regions = T.RegionId.Set.empty; + avalues; + } + in + push_abs abs; + + (* Return the new borrow *) + bid2 + + let match_mut_borrows (ty : T.ety) (bid0 : V.borrow_id) (bv0 : V.typed_value) + (bid1 : V.borrow_id) (bv1 : V.typed_value) (bv : V.typed_value) : + V.borrow_id * V.typed_value = + if bid0 = bid1 then ( + (* If the merged value is not the same as the original value, we introduce + an abstraction: + + {[ + { MB bid0, ML nbid } // where nbid fresh + ]} + + and we use bid' for the borrow id that we return. + + We do this because we want to make sure that, whenever a mutably + borrowed value is modified in a loop iteration, then there is + a fresh abstraction between this borrowed value and the fixed + abstractions. + *) + assert (not (value_has_borrows S.ctx bv.V.value)); + + if bv0 = bv1 then ( + assert (bv0 = bv); + (bid0, bv)) + else + let rid = C.fresh_region_id () in + let nbid = C.fresh_borrow_id () in + + let kind = T.Mut in + let bv_ty = ety_no_regions_to_rty bv.V.ty in + let borrow_ty = mk_ref_ty (T.Var rid) bv_ty kind in + + let borrow_av = + let ty = borrow_ty in + let value = V.ABorrow (V.AMutBorrow (bid0, mk_aignored bv_ty)) in + mk_typed_avalue ty value + in + + let loan_av = + let ty = borrow_ty in + let value = V.ALoan (V.AMutLoan (nbid, mk_aignored bv_ty)) in + mk_typed_avalue ty value + in + + let avalues = [ borrow_av; loan_av ] in + + (* Generate the abstraction *) + let abs = + { + V.abs_id = C.fresh_abstraction_id (); + kind = V.Loop (S.loop_id, None, LoopSynthInput); + can_end = true; + parents = V.AbstractionId.Set.empty; + original_parents = []; + regions = T.RegionId.Set.singleton rid; + ancestors_regions = T.RegionId.Set.empty; + avalues; + } + in + push_abs abs; + + (* Return the new borrow *) + (nbid, bv)) + else + (* We replace bid0 and bid1 with a fresh borrow id, and introduce + an abstraction which links all of them: + {[ + { MB bid0, MB bid1, ML bid2 } + ]} + *) + let rid = C.fresh_region_id () in + let bid2 = C.fresh_borrow_id () in + + (* Generate a fresh symbolic value for the borrowed value *) + let _, bv_ty, kind = ty_as_ref ty in + let sv = mk_fresh_symbolic_typed_value_from_ety V.LoopJoin bv_ty in + + let borrow_ty = + mk_ref_ty (T.Var rid) (ety_no_regions_to_rty bv_ty) kind + in + + (* Generate the avalues for the abstraction *) + let mk_aborrow (bid : V.borrow_id) (bv : V.typed_value) : V.typed_avalue = + let bv_ty = ety_no_regions_to_rty bv.V.ty in + let value = V.ABorrow (V.AMutBorrow (bid, mk_aignored bv_ty)) in + { V.value; ty = borrow_ty } + in + let borrows = [ mk_aborrow bid0 bv0; mk_aborrow bid1 bv1 ] in + + let loan = V.AMutLoan (bid2, mk_aignored (ety_no_regions_to_rty bv_ty)) in + (* Note that an aloan has a borrow type *) + let loan = { V.value = V.ALoan loan; ty = borrow_ty } in + + let avalues = List.append borrows [ loan ] in + + (* Generate the abstraction *) + let abs = + { + V.abs_id = C.fresh_abstraction_id (); + kind = V.Loop (S.loop_id, None, LoopSynthInput); + can_end = true; + parents = V.AbstractionId.Set.empty; + original_parents = []; + regions = T.RegionId.Set.singleton rid; + ancestors_regions = T.RegionId.Set.empty; + avalues; + } + in + push_abs abs; + + (* Return the new borrow *) + (bid2, sv) + + let match_shared_loans (_ : T.ety) (ids0 : V.loan_id_set) + (ids1 : V.loan_id_set) (sv : V.typed_value) : + V.loan_id_set * V.typed_value = + (* Check if the ids are the same - Rem.: we forbid the sets of loans + to be different. However, if we dive inside data-structures (by + using a shared borrow) the shared values might themselves contain + shared loans, which need to be matched. For this reason, we destructure + the shared values (see {!destructure_abs}). + *) + let extra_ids_left = V.BorrowId.Set.diff ids0 ids1 in + let extra_ids_right = V.BorrowId.Set.diff ids1 ids0 in + if not (V.BorrowId.Set.is_empty extra_ids_left) then + raise (ValueMatchFailure (LoansInLeft extra_ids_left)); + if not (V.BorrowId.Set.is_empty extra_ids_right) then + raise (ValueMatchFailure (LoansInRight extra_ids_right)); + + (* This should always be true if we get here *) + assert (ids0 = ids1); + let ids = ids0 in + + (* Return *) + (ids, sv) + + let match_mut_loans (_ : T.ety) (id0 : V.loan_id) (id1 : V.loan_id) : + V.loan_id = + if id0 = id1 then id0 + else + (* We forbid this case for now: if we get there, we force to end + both borrows *) + raise (ValueMatchFailure (LoanInLeft id0)) + + let match_symbolic_values (sv0 : V.symbolic_value) (sv1 : V.symbolic_value) : + V.symbolic_value = + let id0 = sv0.sv_id in + let id1 = sv1.sv_id in + if id0 = id1 then ( + (* Sanity check *) + assert (sv0 = sv1); + (* Return *) + sv0) + 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)); + (* We simply introduce a fresh symbolic value *) + mk_fresh_symbolic_value V.LoopJoin sv0.sv_ty) + + let match_symbolic_with_other (left : bool) (sv : V.symbolic_value) + (v : V.typed_value) : V.typed_value = + (* Check that: + - there are no borrows in the symbolic value + - 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 (value_has_borrows S.ctx v.V.value)); + let value_is_left = not left in + (match InterpreterBorrowsCore.get_first_loan_in_value v with + | None -> () + | Some (SharedLoan (ids, _)) -> + if value_is_left then raise (ValueMatchFailure (LoansInLeft ids)) + else raise (ValueMatchFailure (LoansInRight ids)) + | Some (MutLoan id) -> + if value_is_left then raise (ValueMatchFailure (LoanInLeft id)) + else raise (ValueMatchFailure (LoanInRight id))); + (* Return a fresh symbolic value *) + mk_fresh_symbolic_typed_value V.LoopJoin sv.sv_ty + + let match_bottom_with_other (left : bool) (v : V.typed_value) : V.typed_value + = + (* If there are outer loans in the non-bottom value, raise an exception. + Otherwise, convert it to an abstraction and return [Bottom]. + *) + let with_borrows = false in + let value_is_left = not left in + match + InterpreterBorrowsCore.get_first_outer_loan_or_borrow_in_value + with_borrows v + with + | Some (BorrowContent _) -> raise (Failure "Unreachable") + | Some (LoanContent lc) -> ( + match lc with + | V.SharedLoan (ids, _) -> + if value_is_left then raise (ValueMatchFailure (LoansInLeft ids)) + else raise (ValueMatchFailure (LoansInRight ids)) + | V.MutLoan id -> + if value_is_left then raise (ValueMatchFailure (LoanInLeft id)) + else raise (ValueMatchFailure (LoanInRight id))) + | None -> + (* Convert the value to an abstraction *) + let abs_kind = V.Loop (S.loop_id, None, LoopSynthInput) in + let can_end = true in + let destructure_shared_values = true in + let absl = + convert_value_to_abstractions abs_kind can_end + destructure_shared_values S.ctx v + in + push_absl absl; + (* Return [Bottom] *) + mk_bottom v.V.ty + + (* As explained in comments: we don't use the join matcher to join avalues, + only concrete values *) + + let match_distinct_aadts _ _ _ _ _ = raise (Failure "Unreachable") + let match_ashared_borrows _ _ _ _ = raise (Failure "Unreachable") + let match_amut_borrows _ _ _ _ _ _ _ _ = raise (Failure "Unreachable") + let match_ashared_loans _ _ _ _ _ _ _ _ _ _ _ = raise (Failure "Unreachable") + let match_amut_loans _ _ _ _ _ _ _ _ = raise (Failure "Unreachable") + let match_avalues _ _ = raise (Failure "Unreachable") +end + +module MakeCheckEquivMatcher (S : MatchCheckEquivState) : CheckEquivMatcher = +struct + module MkGetSetM (Id : Identifiers.Id) = struct + module Inj = Id.InjSubst + + let add (msg : string) (m : Inj.t ref) (k0 : Id.id) (k1 : Id.id) = + (* Check if k0 is already registered as a key *) + match Inj.find_opt k0 !m with + | None -> + (* Not registered: check if k1 is in the set of values, + otherwise add the binding *) + if Inj.Set.mem k1 (Inj.elements !m) then + raise + (Distinct + (msg ^ "adding [k0=" ^ Id.to_string k0 ^ " -> k1=" + ^ Id.to_string k1 ^ " ]: k1 already in the set of elements")) + else ( + m := Inj.add k0 k1 !m; + k1) + | Some k1' -> + (* It is: check that the bindings are consistent *) + if k1 <> k1' then raise (Distinct (msg ^ "already a binding for k0")) + else k1 + + let match_e (msg : string) (m : Inj.t ref) (k0 : Id.id) (k1 : Id.id) : Id.id + = + (* TODO: merge the add and merge functions *) + add msg m k0 k1 + + let match_el (msg : string) (m : Inj.t ref) (kl0 : Id.id list) + (kl1 : Id.id list) : Id.id list = + List.map (fun (k0, k1) -> match_e msg m k0 k1) (List.combine kl0 kl1) + + (** Figuring out mappings between sets of ids is hard in all generality... + We use the fact that the fresh ids should have been generated + the same way (i.e., in the same order) and match the ids two by + two in increasing order. + *) + let match_es (msg : string) (m : Inj.t ref) (ks0 : Id.Set.t) + (ks1 : Id.Set.t) : Id.Set.t = + Id.Set.of_list + (match_el msg m (Id.Set.elements ks0) (Id.Set.elements ks1)) + end + + module GetSetRid = MkGetSetM (T.RegionId) + + let match_rid = GetSetRid.match_e "match_rid: " S.rid_map + let match_rids = GetSetRid.match_es "match_rids: " S.rid_map + + module GetSetBid = MkGetSetM (V.BorrowId) + + let match_blid msg = GetSetBid.match_e msg S.blid_map + let match_blidl msg = GetSetBid.match_el msg S.blid_map + let match_blids msg = GetSetBid.match_es msg S.blid_map + + let match_borrow_id = + if S.check_equiv then match_blid "match_borrow_id: " + else GetSetBid.match_e "match_borrow_id: " S.borrow_id_map + + let match_borrow_idl = + if S.check_equiv then match_blidl "match_borrow_idl: " + else GetSetBid.match_el "match_borrow_idl: " S.borrow_id_map + + let match_borrow_ids = + if S.check_equiv then match_blids "match_borrow_ids: " + else GetSetBid.match_es "match_borrow_ids: " S.borrow_id_map + + let match_loan_id = + if S.check_equiv then match_blid "match_loan_id: " + else GetSetBid.match_e "match_loan_id: " S.loan_id_map + + let match_loan_idl = + if S.check_equiv then match_blidl "match_loan_idl: " + else GetSetBid.match_el "match_loan_idl: " S.loan_id_map + + let match_loan_ids = + if S.check_equiv then match_blids "match_loan_ids: " + else GetSetBid.match_es "match_loan_ids: " S.loan_id_map + + module GetSetSid = MkGetSetM (V.SymbolicValueId) + module GetSetAid = MkGetSetM (V.AbstractionId) + + let match_aid = GetSetAid.match_e "match_aid: " S.aid_map + let match_aidl = GetSetAid.match_el "match_aidl: " S.aid_map + let match_aids = GetSetAid.match_es "match_aids: " S.aid_map + + (** *) + let match_etys ty0 ty1 = + if ty0 <> ty1 then raise (Distinct "match_etys") else ty0 + + let match_rtys ty0 ty1 = + let match_distinct_types _ _ = raise (Distinct "match_rtys") in + let match_regions r0 r1 = + match (r0, r1) with + | T.Static, T.Static -> r1 + | Var rid0, Var rid1 -> + let rid = match_rid rid0 rid1 in + Var rid + | _ -> raise (Distinct "match_rtys") + in + match_types match_distinct_types match_regions ty0 ty1 + + let match_distinct_primitive_values (ty : T.ety) (_ : V.primitive_value) + (_ : V.primitive_value) : V.typed_value = + mk_fresh_symbolic_typed_value_from_ety V.LoopJoin ty + + let match_distinct_adts (_ty : T.ety) (_adt0 : V.adt_value) + (_adt1 : V.adt_value) : V.typed_value = + raise (Distinct "match_distinct_adts") + + let match_shared_borrows + (match_typed_values : V.typed_value -> V.typed_value -> V.typed_value) + (_ty : T.ety) (bid0 : V.borrow_id) (bid1 : V.borrow_id) : V.borrow_id = + log#ldebug + (lazy + ("MakeCheckEquivMatcher: match_shared_borrows: " ^ "bid0: " + ^ V.BorrowId.to_string bid0 ^ ", bid1: " ^ V.BorrowId.to_string bid1)); + + let bid = match_borrow_id bid0 bid1 in + (* If we don't check for equivalence (i.e., we apply a fixed-point), + we lookup the shared values and match them. + *) + let _ = + if S.check_equiv then () + else + let v0 = S.lookup_shared_value_in_ctx0 bid0 in + let v1 = S.lookup_shared_value_in_ctx1 bid1 in + log#ldebug + (lazy + ("MakeCheckEquivMatcher: match_shared_borrows: looked up values:" + ^ "sv0: " + ^ typed_value_to_string S.ctx v0 + ^ ", sv1: " + ^ typed_value_to_string S.ctx v1)); + + let _ = match_typed_values v0 v1 in + () + in + bid + + let match_mut_borrows (_ty : T.ety) (bid0 : V.borrow_id) + (_bv0 : V.typed_value) (bid1 : V.borrow_id) (_bv1 : V.typed_value) + (bv : V.typed_value) : V.borrow_id * V.typed_value = + let bid = match_borrow_id bid0 bid1 in + (bid, bv) + + let match_shared_loans (_ : T.ety) (ids0 : V.loan_id_set) + (ids1 : V.loan_id_set) (sv : V.typed_value) : + V.loan_id_set * V.typed_value = + let ids = match_loan_ids ids0 ids1 in + (ids, sv) + + let match_mut_loans (_ : T.ety) (bid0 : V.loan_id) (bid1 : V.loan_id) : + V.loan_id = + match_loan_id bid0 bid1 + + let match_symbolic_values (sv0 : V.symbolic_value) (sv1 : V.symbolic_value) : + V.symbolic_value = + let id0 = sv0.sv_id in + let id1 = sv1.sv_id in + + log#ldebug + (lazy + ("MakeCheckEquivMatcher: match_symbolic_values: " ^ "sv0: " + ^ V.SymbolicValueId.to_string id0 + ^ ", sv1: " + ^ V.SymbolicValueId.to_string id1)); + + (* If we don't check for equivalence, we also update the map from sids + to values *) + if S.check_equiv then + (* Create the joined symbolic value *) + let sv_id = + GetSetSid.match_e "match_symbolic_values: ids: " S.sid_map id0 id1 + in + let sv_ty = match_rtys sv0.V.sv_ty sv1.V.sv_ty in + let sv_kind = + if sv0.V.sv_kind = sv1.V.sv_kind then sv0.V.sv_kind + else raise (Distinct "match_symbolic_values: sv_kind") + in + let sv = { V.sv_id; sv_ty; sv_kind } in + sv + else ( + (* Check: fixed values are fixed *) + assert (id0 = id1 || not (V.SymbolicValueId.InjSubst.mem id0 !S.sid_map)); + + (* Update the symbolic value mapping *) + let sv1 = mk_typed_value_from_symbolic_value sv1 in + + (* Update the symbolic value mapping *) + S.sid_to_value_map := + V.SymbolicValueId.Map.add_strict id0 sv1 !S.sid_to_value_map; + + (* Return - the returned value is not used: we can return whatever + we want *) + sv0) + + let match_symbolic_with_other (left : bool) (sv : V.symbolic_value) + (v : V.typed_value) : V.typed_value = + if S.check_equiv then raise (Distinct "match_symbolic_with_other") + else ( + assert left; + let id = sv.sv_id in + (* Check: fixed values are fixed *) + assert (not (V.SymbolicValueId.InjSubst.mem id !S.sid_map)); + (* Update the binding for the target symbolic value *) + S.sid_to_value_map := + V.SymbolicValueId.Map.add_strict id v !S.sid_to_value_map; + (* Return - the returned value is not used, so we can return whatever we want *) + v) + + let match_bottom_with_other (left : bool) (v : V.typed_value) : V.typed_value + = + (* It can happen that some variables get initialized in some branches + and not in some others, which causes problems when matching. *) + (* TODO: the returned value is not used, while it should: in generality it + should be ok to match a fixed-point with the environment we get at + a continue, where the fixed point contains some bottom values. *) + if left && not (value_has_loans_or_borrows S.ctx v.V.value) then + mk_bottom v.V.ty + else raise (Distinct "match_bottom_with_other") + + let match_distinct_aadts _ _ _ _ _ = raise (Distinct "match_distinct_adts") + + let match_ashared_borrows _ty0 bid0 _ty1 bid1 ty = + let bid = match_borrow_id bid0 bid1 in + let value = V.ABorrow (V.ASharedBorrow bid) in + { V.value; ty } + + let match_amut_borrows _ty0 bid0 _av0 _ty1 bid1 _av1 ty av = + let bid = match_borrow_id bid0 bid1 in + let value = V.ABorrow (V.AMutBorrow (bid, av)) in + { V.value; ty } + + let match_ashared_loans _ty0 ids0 _v0 _av0 _ty1 ids1 _v1 _av1 ty v av = + let bids = match_loan_ids ids0 ids1 in + let value = V.ALoan (V.ASharedLoan (bids, v, av)) in + { V.value; ty } + + let match_amut_loans _ty0 id0 _av0 _ty1 id1 _av1 ty av = + log#ldebug + (lazy + ("MakeCheckEquivMatcher:match_amut_loans:" ^ "\n- id0: " + ^ V.BorrowId.to_string id0 ^ "\n- id1: " ^ V.BorrowId.to_string id1 + ^ "\n- ty: " ^ rty_to_string S.ctx ty ^ "\n- av: " + ^ typed_avalue_to_string S.ctx av)); + + let id = match_loan_id id0 id1 in + let value = V.ALoan (V.AMutLoan (id, av)) in + { V.value; ty } + + let match_avalues v0 v1 = + log#ldebug + (lazy + ("avalues don't match:\n- v0: " + ^ typed_avalue_to_string S.ctx v0 + ^ "\n- v1: " + ^ typed_avalue_to_string S.ctx v1)); + raise (Distinct "match_avalues") +end + +let match_ctxs (check_equiv : bool) (fixed_ids : ids_sets) + (lookup_shared_value_in_ctx0 : V.BorrowId.id -> V.typed_value) + (lookup_shared_value_in_ctx1 : V.BorrowId.id -> V.typed_value) + (ctx0 : C.eval_ctx) (ctx1 : C.eval_ctx) : ids_maps option = + log#ldebug + (lazy + ("match_ctxs:\n\n- fixed_ids:\n" ^ show_ids_sets fixed_ids + ^ "\n\n- ctx0:\n" + ^ eval_ctx_to_string_no_filter ctx0 + ^ "\n\n- ctx1:\n" + ^ eval_ctx_to_string_no_filter ctx1 + ^ "\n\n")); + + (* Initialize the maps and instantiate the matcher *) + let module IdMap (Id : Identifiers.Id) = struct + let mk_map_ref (ids : Id.Set.t) : Id.InjSubst.t ref = + ref + (Id.InjSubst.of_list (List.map (fun x -> (x, x)) (Id.Set.elements ids))) + end in + let rid_map = + let module IdMap = IdMap (T.RegionId) in + IdMap.mk_map_ref fixed_ids.rids + in + let blid_map = + let module IdMap = IdMap (V.BorrowId) in + IdMap.mk_map_ref fixed_ids.blids + in + let borrow_id_map = + let module IdMap = IdMap (V.BorrowId) in + IdMap.mk_map_ref fixed_ids.borrow_ids + in + let loan_id_map = + let module IdMap = IdMap (V.BorrowId) in + IdMap.mk_map_ref fixed_ids.loan_ids + in + let aid_map = + let module IdMap = IdMap (V.AbstractionId) in + IdMap.mk_map_ref fixed_ids.aids + in + let sid_map = + let module IdMap = IdMap (V.SymbolicValueId) in + IdMap.mk_map_ref fixed_ids.sids + in + (* In case we don't try to check equivalence but want to compute a mapping + from a source context to a target context, we use a map from symbolic + value ids to values (rather than to ids). + *) + let sid_to_value_map : V.typed_value V.SymbolicValueId.Map.t ref = + ref V.SymbolicValueId.Map.empty + in + + let module S : MatchCheckEquivState = struct + let check_equiv = check_equiv + let ctx = ctx0 + let rid_map = rid_map + let blid_map = blid_map + let borrow_id_map = borrow_id_map + let loan_id_map = loan_id_map + let sid_map = sid_map + let sid_to_value_map = sid_to_value_map + let aid_map = aid_map + let lookup_shared_value_in_ctx0 = lookup_shared_value_in_ctx0 + let lookup_shared_value_in_ctx1 = lookup_shared_value_in_ctx1 + end in + let module CEM = MakeCheckEquivMatcher (S) in + let module M = MakeMatcher (CEM) in + (* Match the environments - we assume that they have the same structure + (and fail if they don't) *) + + (* Small utility: check that ids are fixed/mapped to themselves *) + let ids_are_fixed (ids : ids_sets) : bool = + let { aids; blids = _; borrow_ids; loan_ids; dids; rids; sids } = ids in + V.AbstractionId.Set.subset aids fixed_ids.aids + && V.BorrowId.Set.subset borrow_ids fixed_ids.borrow_ids + && V.BorrowId.Set.subset loan_ids fixed_ids.loan_ids + && C.DummyVarId.Set.subset dids fixed_ids.dids + && T.RegionId.Set.subset rids fixed_ids.rids + && V.SymbolicValueId.Set.subset sids fixed_ids.sids + in + + (* We need to pick a context for some functions like [match_typed_values]: + the context is only used to lookup module data, so we can pick whichever + we want. + TODO: this is not very clean. Maybe we should just carry the relevant data + (i.e.e, not the whole context) around. + *) + let ctx = ctx0 in + + (* Rem.: this function raises exceptions of type [Distinct] *) + let match_abstractions (abs0 : V.abs) (abs1 : V.abs) : unit = + let { + V.abs_id = abs_id0; + kind = kind0; + can_end = can_end0; + parents = parents0; + original_parents = original_parents0; + regions = regions0; + ancestors_regions = ancestors_regions0; + avalues = avalues0; + } = + abs0 + in + + let { + V.abs_id = abs_id1; + kind = kind1; + can_end = can_end1; + parents = parents1; + original_parents = original_parents1; + regions = regions1; + ancestors_regions = ancestors_regions1; + avalues = avalues1; + } = + abs1 + in + + let _ = CEM.match_aid abs_id0 abs_id1 in + if kind0 <> kind1 || can_end0 <> can_end1 then + raise (Distinct "match_abstractions: kind or can_end"); + let _ = CEM.match_aids parents0 parents1 in + let _ = CEM.match_aidl original_parents0 original_parents1 in + let _ = CEM.match_rids regions0 regions1 in + let _ = CEM.match_rids ancestors_regions0 ancestors_regions1 in + + log#ldebug (lazy "match_abstractions: matching values"); + let _ = + List.map + (fun (v0, v1) -> M.match_typed_avalues ctx v0 v1) + (List.combine avalues0 avalues1) + in + log#ldebug (lazy "match_abstractions: values matched OK"); + () + in + + (* Rem.: this function raises exceptions of type [Distinct] *) + let rec match_envs (env0 : C.env) (env1 : C.env) : unit = + log#ldebug + (lazy + ("match_ctxs: match_envs:\n\n- fixed_ids:\n" ^ show_ids_sets fixed_ids + ^ "\n\n- rid_map: " + ^ T.RegionId.InjSubst.show_t !rid_map + ^ "\n- blid_map: " + ^ V.BorrowId.InjSubst.show_t !blid_map + ^ "\n- sid_map: " + ^ V.SymbolicValueId.InjSubst.show_t !sid_map + ^ "\n- aid_map: " + ^ V.AbstractionId.InjSubst.show_t !aid_map + ^ "\n\n- ctx0:\n" + ^ eval_ctx_to_string_no_filter { ctx0 with env = List.rev env0 } + ^ "\n\n- ctx1:\n" + ^ eval_ctx_to_string_no_filter { ctx1 with env = List.rev env1 } + ^ "\n\n")); + + match (env0, env1) with + | ( C.Var (C.DummyBinder b0, v0) :: env0', + C.Var (C.DummyBinder b1, v1) :: env1' ) -> + (* Sanity check: if the dummy value is an old value, the bindings must + be the same and their values equal (and the borrows/loans/symbolic *) + if C.DummyVarId.Set.mem b0 fixed_ids.dids then ( + (* Fixed values: the values must be equal *) + assert (b0 = b1); + assert (v0 = v1); + (* The ids present in the left value must be fixed *) + let ids, _ = compute_typed_value_ids v0 in + assert ((not S.check_equiv) || ids_are_fixed ids)); + (* We still match the values - allows to compute mappings (which + are the identity actually) *) + let _ = M.match_typed_values ctx v0 v1 in + match_envs env0' env1' + | C.Var (C.VarBinder b0, v0) :: env0', C.Var (C.VarBinder b1, v1) :: env1' + -> + assert (b0 = b1); + (* Match the values *) + let _ = M.match_typed_values ctx v0 v1 in + (* Continue *) + match_envs env0' env1' + | C.Abs abs0 :: env0', C.Abs abs1 :: env1' -> + log#ldebug (lazy "match_ctxs: match_envs: matching abs"); + (* Same as for the dummy values: there are two cases *) + if V.AbstractionId.Set.mem abs0.abs_id fixed_ids.aids then ( + log#ldebug (lazy "match_ctxs: match_envs: matching abs: fixed abs"); + (* Still in the prefix: the abstractions must be the same *) + assert (abs0 = abs1); + (* Their ids must be fixed *) + let ids, _ = compute_abs_ids abs0 in + assert ((not S.check_equiv) || ids_are_fixed ids); + (* Continue *) + match_envs env0' env1') + else ( + log#ldebug + (lazy "match_ctxs: match_envs: matching abs: not fixed abs"); + (* Match the values *) + match_abstractions abs0 abs1; + (* Continue *) + match_envs env0' env1') + | [], [] -> + (* Done *) + () + | _ -> + (* The elements don't match *) + raise (Distinct "match_ctxs: match_envs: env elements don't match") + in + + (* Match the environments. + + Rem.: we don't match the ended regions (would it make any sense actually?) *) + try + (* Remove the frame delimiter (the first element of an environment is a frame delimiter) *) + let env0 = List.rev ctx0.env in + let env1 = List.rev ctx1.env in + let env0, env1 = + match (env0, env1) with + | C.Frame :: env0, C.Frame :: env1 -> (env0, env1) + | _ -> raise (Failure "Unreachable") + in + + match_envs env0 env1; + let maps = + { + aid_map = !aid_map; + blid_map = !blid_map; + borrow_id_map = !borrow_id_map; + loan_id_map = !loan_id_map; + rid_map = !rid_map; + sid_map = !sid_map; + sid_to_value_map = !sid_to_value_map; + } + in + Some maps + with Distinct msg -> + log#ldebug (lazy ("match_ctxs: distinct: " ^ msg)); + None + +let ctxs_are_equivalent (fixed_ids : ids_sets) (ctx0 : C.eval_ctx) + (ctx1 : C.eval_ctx) : bool = + let check_equivalent = true in + let lookup_shared_value _ = raise (Failure "Unreachable") in + Option.is_some + (match_ctxs check_equivalent fixed_ids lookup_shared_value + lookup_shared_value ctx0 ctx1) + +let match_ctx_with_target (config : C.config) (loop_id : V.LoopId.id) + (is_loop_entry : bool) (fp_bl_maps : borrow_loan_corresp) + (fp_input_svalues : V.SymbolicValueId.id list) (fixed_ids : ids_sets) + (src_ctx : C.eval_ctx) : st_cm_fun = + fun cf tgt_ctx -> + (* Debug *) + log#ldebug + (lazy + ("match_ctx_with_target:\n" ^ "\n- fixed_ids: " ^ show_ids_sets fixed_ids + ^ "\n" ^ "\n- src_ctx: " ^ eval_ctx_to_string src_ctx ^ "\n- tgt_ctx: " + ^ eval_ctx_to_string tgt_ctx)); + + (* We first reorganize [tgt_ctx] so that we can match [src_ctx] with it (by + ending loans for instance - remember that the [src_ctx] is the fixed point + context, which results from joins during which we ended the loans which + were introduced during the loop iterations) + *) + (* End the loans which lead to mismatches when joining *) + let rec cf_reorganize_join_tgt : cm_fun = + fun cf tgt_ctx -> + (* Collect fixed values in the source and target contexts: end the loans in the + source context which don't appear in the target context *) + let filt_src_env, _, _ = ctx_split_fixed_new fixed_ids src_ctx in + let filt_tgt_env, _, _ = ctx_split_fixed_new fixed_ids tgt_ctx in + + log#ldebug + (lazy + ("match_ctx_with_target:\n" ^ "\n- fixed_ids: " + ^ show_ids_sets fixed_ids ^ "\n" ^ "\n- filt_src_ctx: " + ^ env_to_string src_ctx filt_src_env + ^ "\n- filt_tgt_ctx: " + ^ env_to_string tgt_ctx filt_tgt_env)); + + (* Remove the abstractions *) + let filter (ee : C.env_elem) : bool = + match ee with Var _ -> true | Abs _ | Frame -> false + in + let filt_src_env = List.filter filter filt_src_env in + let filt_tgt_env = List.filter filter filt_tgt_env in + + (* Match the values to check if there are loans to eliminate *) + + (* We need to pick a context for some functions like [match_typed_values]: + the context is only used to lookup module data, so we can pick whichever + we want. + TODO: this is not very clean. Maybe we should just carry this data around. + *) + let ctx = tgt_ctx in + + let nabs = ref [] in + + let module S : MatchJoinState = struct + (* The context is only used to lookup module data: we can pick whichever we want *) + let ctx = ctx + let loop_id = loop_id + let nabs = nabs + end in + let module JM = MakeJoinMatcher (S) in + let module M = MakeMatcher (JM) in + try + let _ = + List.iter + (fun (var0, var1) -> + match (var0, var1) with + | C.Var (C.DummyBinder b0, v0), C.Var (C.DummyBinder b1, v1) -> + assert (b0 = b1); + let _ = M.match_typed_values ctx v0 v1 in + () + | C.Var (C.VarBinder b0, v0), C.Var (C.VarBinder b1, v1) -> + assert (b0 = b1); + let _ = M.match_typed_values ctx v0 v1 in + () + | _ -> raise (Failure "Unexpected")) + (List.combine filt_src_env filt_tgt_env) + in + (* No exception was thrown: continue *) + cf tgt_ctx + with ValueMatchFailure e -> + (* Exception: end the corresponding borrows, and continue *) + let cc = + match e with + | LoanInRight bid -> InterpreterBorrows.end_borrow config bid + | LoansInRight bids -> InterpreterBorrows.end_borrows config bids + | AbsInRight _ | AbsInLeft _ | LoanInLeft _ | LoansInLeft _ -> + raise (Failure "Unexpected") + in + comp cc cf_reorganize_join_tgt cf tgt_ctx + in + + (* Introduce the "identity" abstractions for the loop reentry. + + Match the target context with the source context so as to compute how to + map the borrows from the target context (i.e., the fixed point context) + to the borrows in the source context. + + Substitute the *loans* in the abstractions introduced by the target context + (the abstractions of the fixed point) to properly link those abstraction: + we introduce *identity* abstractions (the loans are equal to the borrows): + we substitute the loans and introduce fresh ids for the borrows, symbolic + values, etc. About the *identity abstractions*, see the comments for + [compute_fixed_point_id_correspondance]. + + TODO: this whole thing is very technical and error-prone. + We should rely on a more primitive and safer function + [add_identity_abs] to add the identity abstractions one by one. + *) + let cf_introduce_loop_fp_abs : m_fun = + fun tgt_ctx -> + (* Match the source and target contexts *) + let filt_tgt_env, _, _ = ctx_split_fixed_new fixed_ids tgt_ctx in + let filt_src_env, new_absl, new_dummyl = + ctx_split_fixed_new fixed_ids src_ctx + in + assert (new_dummyl = []); + let filt_tgt_ctx = { tgt_ctx with env = filt_tgt_env } in + let filt_src_ctx = { src_ctx with env = filt_src_env } in + + let src_to_tgt_maps = + let check_equiv = false in + let fixed_ids = ids_sets_empty_borrows_loans fixed_ids in + let open InterpreterBorrowsCore in + let lookup_shared_loan lid ctx : V.typed_value = + match snd (lookup_loan ek_all lid ctx) with + | Concrete (V.SharedLoan (_, v)) -> v + | Abstract (V.ASharedLoan (_, v, _)) -> v + | _ -> raise (Failure "Unreachable") + in + let lookup_in_src id = lookup_shared_loan id src_ctx in + let lookup_in_tgt id = lookup_shared_loan id tgt_ctx in + (* Match *) + Option.get + (match_ctxs check_equiv fixed_ids lookup_in_src lookup_in_tgt + filt_src_ctx filt_tgt_ctx) + in + let tgt_to_src_borrow_map = + V.BorrowId.Map.of_list + (List.map + (fun (x, y) -> (y, x)) + (V.BorrowId.InjSubst.bindings src_to_tgt_maps.borrow_id_map)) + in + + (* Debug *) + log#ldebug + (lazy + ("match_ctx_with_target: cf_introduce_loop_fp_abs:" ^ "\n\n- tgt_ctx: " + ^ eval_ctx_to_string tgt_ctx ^ "\n\n- src_ctx: " + ^ eval_ctx_to_string src_ctx ^ "\n\n- filt_tgt_ctx: " + ^ eval_ctx_to_string_no_filter filt_tgt_ctx + ^ "\n\n- filt_src_ctx: " + ^ eval_ctx_to_string_no_filter filt_src_ctx + ^ "\n\n- new_absl:\n" + ^ eval_ctx_to_string + { src_ctx with C.env = List.map (fun abs -> C.Abs abs) new_absl } + ^ "\n\n- fixed_ids:\n" ^ show_ids_sets fixed_ids ^ "\n\n- fp_bl_maps:\n" + ^ show_borrow_loan_corresp fp_bl_maps + ^ "\n\n- src_to_tgt_maps: " + ^ show_ids_maps src_to_tgt_maps)); + + (* Update the borrows and symbolic ids in the source context. + + Going back to the [list_nth_mut_example], the original environment upon + re-entering the loop is: + + {[ + abs@0 { ML l0 } + ls -> MB l5 (s@6 : loops::List<T>) + i -> s@7 : u32 + _@1 -> MB l0 (loops::List::Cons (ML l1, ML l2)) + _@2 -> MB l2 (@Box (ML l4)) // tail + _@3 -> MB l1 (s@3 : T) // hd + abs@1 { MB l4, ML l5 } + ]} + + The fixed-point environment is: + {[ + env_fp = { + abs@0 { ML l0 } + ls -> MB l1 (s3 : loops::List<T>) + i -> s4 : u32 + abs@fp { + MB l0 // this borrow appears in [env0] + ML l1 + } + } + ]} + + Through matching, we detect that in [env_fp], [l1] is matched + to [l5]. We introduce a fresh borrow [l6] for [l1], and remember + in the map [src_fresh_borrows_map] that: [{ l1 -> l6}]. + + We get: + {[ + abs@0 { ML l0 } + ls -> MB l6 (s@6 : loops::List<T>) // l6 is fresh and doesn't have a corresponding loan + i -> s@7 : u32 + _@1 -> MB l0 (loops::List::Cons (ML l1, ML l2)) + _@2 -> MB l2 (@Box (ML l4)) // tail + _@3 -> MB l1 (s@3 : T) // hd + abs@1 { MB l4, ML l5 } + ]} + + Later, we will introduce the identity abstraction: + {[ + abs@2 { MB l5, ML l6 } + ]} + *) + (* First, compute the set of borrows which appear in the fresh abstractions + of the fixed-point: we want to introduce fresh ids only for those. *) + let new_absl_ids, _ = compute_absl_ids new_absl in + let src_fresh_borrows_map = ref V.BorrowId.Map.empty in + let visit_tgt = + object + inherit [_] C.map_eval_ctx + + method! visit_borrow_id _ id = + (* Map the borrow, if it needs to be mapped *) + if + (* We map the borrows for which we computed a mapping *) + V.BorrowId.InjSubst.Set.mem id + (V.BorrowId.InjSubst.elements src_to_tgt_maps.borrow_id_map) + (* And which have corresponding loans in the fresh fixed-point abstractions *) + && V.BorrowId.Set.mem + (V.BorrowId.Map.find id tgt_to_src_borrow_map) + new_absl_ids.loan_ids + then ( + let src_id = V.BorrowId.Map.find id tgt_to_src_borrow_map in + let nid = C.fresh_borrow_id () in + src_fresh_borrows_map := + V.BorrowId.Map.add src_id nid !src_fresh_borrows_map; + nid) + else id + end + in + let tgt_ctx = visit_tgt#visit_eval_ctx () tgt_ctx in + + log#ldebug + (lazy + ("match_ctx_with_target: cf_introduce_loop_fp_abs: \ + src_fresh_borrows_map:\n" + ^ V.BorrowId.Map.show V.BorrowId.to_string !src_fresh_borrows_map + ^ "\n")); + + (* Rem.: we don't update the symbolic values. It is not necessary + because there shouldn't be any symbolic value containing borrows. + + Rem.: we will need to do something about the symbolic values in the + abstractions and in the *variable bindings* once we allow symbolic + values containing borrows to not be eagerly expanded. + *) + assert Config.greedy_expand_symbolics_with_borrows; + + (* Update the borrows and loans in the abstractions of the target context. + + Going back to the [list_nth_mut] example and by using [src_fresh_borrows_map], + we instantiate the fixed-point abstractions that we will insert into the + context. + The abstraction is [abs { MB l0, ML l1 }]. + Because of [src_fresh_borrows_map], we substitute [l1] with [l6]. + Because of the match between the contexts, we substitute [l0] with [l5]. + We get: + {[ + abs@2 { MB l5, ML l6 } + ]} + *) + let region_id_map = ref T.RegionId.Map.empty in + let get_rid rid = + match T.RegionId.Map.find_opt rid !region_id_map with + | Some rid -> rid + | None -> + let nid = C.fresh_region_id () in + region_id_map := T.RegionId.Map.add rid nid !region_id_map; + nid + in + let visit_src = + object + inherit [_] C.map_eval_ctx as super + + method! visit_borrow_id _ bid = + log#ldebug + (lazy + ("match_ctx_with_target: cf_introduce_loop_fp_abs: \ + visit_borrow_id: " ^ V.BorrowId.to_string bid ^ "\n")); + + (* Lookup the id of the loan corresponding to this borrow *) + let src_lid = + V.BorrowId.InjSubst.find bid fp_bl_maps.borrow_to_loan_id_map + in + + log#ldebug + (lazy + ("match_ctx_with_target: cf_introduce_loop_fp_abs: looked up \ + src_lid: " + ^ V.BorrowId.to_string src_lid + ^ "\n")); + + (* Lookup the tgt borrow id to which this borrow was mapped *) + let tgt_bid = + V.BorrowId.InjSubst.find src_lid src_to_tgt_maps.borrow_id_map + in + + log#ldebug + (lazy + ("match_ctx_with_target: cf_introduce_loop_fp_abs: looked up \ + tgt_bid: " + ^ V.BorrowId.to_string tgt_bid + ^ "\n")); + + tgt_bid + + method! visit_loan_id _ id = + log#ldebug + (lazy + ("match_ctx_with_target: cf_introduce_loop_fp_abs: \ + visit_loan_id: " ^ V.BorrowId.to_string id ^ "\n")); + (* Map the borrow - rem.: we mapped the borrows *in the values*, + meaning we know how to map the *corresponding loans in the + abstractions* *) + match V.BorrowId.Map.find_opt id !src_fresh_borrows_map with + | None -> + (* No mapping: this means that the borrow was mapped when + we matched values (it doesn't come from a fresh abstraction) + and because of this, it should actually be mapped to itself *) + assert ( + V.BorrowId.InjSubst.find id src_to_tgt_maps.borrow_id_map = id); + id + | Some id -> id + + method! visit_symbolic_value_id _ _ = C.fresh_symbolic_value_id () + method! visit_abstraction_id _ _ = C.fresh_abstraction_id () + method! visit_region_id _ id = get_rid id + + (** We also need to change the abstraction kind *) + method! visit_abs env abs = + match abs.kind with + | V.Loop (loop_id', rg_id, kind) -> + assert (loop_id' = loop_id); + assert (kind = V.LoopSynthInput); + let can_end = false in + let kind = V.Loop (loop_id, rg_id, V.LoopCall) in + let abs = { abs with kind; can_end } in + super#visit_abs env abs + | _ -> super#visit_abs env abs + end + in + let new_absl = List.map (visit_src#visit_abs ()) new_absl in + let new_absl = List.map (fun abs -> C.Abs abs) new_absl in + + (* Add the abstractions from the target context to the source context *) + let nenv = List.append new_absl tgt_ctx.env in + let tgt_ctx = { tgt_ctx with env = nenv } in + + log#ldebug + (lazy + ("match_ctx_with_target:cf_introduce_loop_fp_abs:\n- result ctx:\n" + ^ eval_ctx_to_string tgt_ctx)); + + (* Sanity check *) + if !Config.check_invariants then + Invariants.check_borrowed_values_invariant tgt_ctx; + + (* End all the borrows which appear in the *new* abstractions *) + let new_borrows = + V.BorrowId.Set.of_list + (List.map snd (V.BorrowId.Map.bindings !src_fresh_borrows_map)) + in + let cc = InterpreterBorrows.end_borrows config new_borrows in + + (* Compute the loop input values *) + let input_values = + V.SymbolicValueId.Map.of_list + (List.map + (fun sid -> + ( sid, + V.SymbolicValueId.Map.find sid src_to_tgt_maps.sid_to_value_map + )) + fp_input_svalues) + in + + (* Continue *) + cc + (cf + (if is_loop_entry then EndEnterLoop (loop_id, input_values) + else EndContinue (loop_id, input_values))) + tgt_ctx + in + + (* Compose and continue *) + cf_reorganize_join_tgt cf_introduce_loop_fp_abs tgt_ctx diff --git a/compiler/InterpreterLoopsMatchCtxs.mli b/compiler/InterpreterLoopsMatchCtxs.mli new file mode 100644 index 00000000..7e585dd6 --- /dev/null +++ b/compiler/InterpreterLoopsMatchCtxs.mli @@ -0,0 +1,301 @@ +(** This module implements support to match contexts for loops. + + The matching functions are used for instance to compute joins, or + to check if two contexts are equivalent (modulo conversion). + *) + +module T = Types +module PV = PrimitiveValues +module V = Values +module E = Expressions +module C = Contexts +module Subst = Substitute +module A = LlbcAst +module Inv = Invariants +module S = SynthesizeSymbolic +open Cps +open InterpreterUtils +open InterpreterLoopsCore + +(** Compute various maps linking the abstractions and the borrows/loans they contain. + + Parameters: + - [no_duplicates]: checks that borrows/loans are not referenced more than once + (see the documentation for {!type:InterpreterLoopsCore.abs_borrows_loans_maps}). + - [explore]: this function is used to filter abstractions. + - [env] + *) +val compute_abs_borrows_loans_maps : + bool -> (V.abs -> bool) -> C.env -> abs_borrows_loans_maps + +(** Generic functor to implement matching functions between values, environments, + etc. + + We use it for joins, to check if two environments are convertible, etc. + See for instance {!MakeJoinMatcher} and {!MakeCheckEquivMatcher}. + + The functor is parameterized by a {!InterpreterLoopsCore.PrimMatcher}, which implements the + non-generic part of the match. More precisely, the role of {!InterpreterLoopsCore.PrimMatcher} is two + provide generic functions which recursively match two values (by recursively + matching the fields of ADT values for instance). When it does need to match + values in a non-trivial manner (if two ADT values don't have the same + variant for instance) it calls the corresponding specialized function from + {!InterpreterLoopsCore.PrimMatcher}. + *) +module MakeMatcher : functor (PM : PrimMatcher) -> Matcher + +(** A matcher for joins (we use joins to compute loop fixed points). + + See the explanations for {!MakeMatcher}. + + In case of loop joins: + - we match *concrete* values + - we check that the "fixed" abstractions (the abstractions to be framed + - i.e., the abstractions which are the same in the two environments to + join) are equal + - we keep the abstractions which are not in the frame, then merge those + together (if they have borrows/loans in common) later + The join matcher is used to match the *concrete* values only. For this + reason, we fail on the functions which match avalues. + *) +module MakeJoinMatcher : functor (S : MatchJoinState) -> PrimMatcher + +(** An auxiliary matcher that we use for two purposes: + - to check if two contexts are equivalent modulo id substitution (i.e., + alpha equivalent) (see {!ctxs_are_equivalent}). + - to compute a mapping between the borrows and the symbolic values in a + target context to the values and borrows in a source context (see + {!match_ctx_with_target}). + *) +module MakeCheckEquivMatcher : functor (S : MatchCheckEquivState) -> + CheckEquivMatcher + +(** Compute whether two contexts are equivalent modulo an identifier substitution. + + [fixed_ids]: ids for which we force the mapping to be the identity. + + We also take advantage of the structure of the environments, which should + have the same prefixes (we check it). See the explanations for {!InterpreterLoopsJoinCtxs.join_ctxs}. + + TODO: explanations. + + The input parameters are: + - [check_equiv]: if [true], check if the two contexts are equivalent. + If [false], compute a mapping from the first context to the second context, + in the sense of [match_ctx_with_target]. + + - [fixed_ids] + + - [lookup_shared_value_in_ctx0], [lookup_shared_value_in_ctx1]: + The lookup functions are used to match the shared values when [check_equiv] + is [false] (we sometimes use [match_ctxs] on partial environments, meaning + we have to lookup the shared values in the complete environment, otherwise + we miss some mappings). + + - [ctx0] + - [ctx1] + + We return an optional ids map: [Some] if the match succeeded, [None] otherwise. + *) +val match_ctxs : + bool -> + ids_sets -> + (V.loan_id -> V.typed_value) -> + (V.loan_id -> V.typed_value) -> + C.eval_ctx -> + C.eval_ctx -> + ids_maps option + +(** Compute whether two contexts are equivalent modulo an identifier substitution. + + We also take advantage of the structure of the environments, which should + have the same prefixes (we check it). See the explanations for + {!InterpreterLoopsJoinCtxs.join_ctxs}. + + For instance, the following environments are equivalent: + {[ + env0 = { + abs@0 { ML l0 } + ls -> MB l1 (s2 : loops::List<T>) + i -> s1 : u32 + abs@1 { MB l0, ML l1 } + } + + env1 = { + abs@0 { ML l0 } + ls -> MB l2 (s4 : loops::List<T>) + i -> s3 : u32 + abs@2 { MB l0, ML l2 } + } + ]} + + We can go from [env0] to [env1] with the substitution: + {[ + abs_id_subst: { abs@1 -> abs@2 } + borrow_id_subst: { l1 -> l2 } + symbolic_id_subst: { s1 -> s3, s2 -> s4 } + ]} + + + Parameters: + - [fixed_ids]: ids for which we force the mapping to be the identity. + - [ctx0] + - [ctx1] + *) +val ctxs_are_equivalent : ids_sets -> C.eval_ctx -> C.eval_ctx -> bool + +(** Match a context with a target context. + + This is used to compute application of loop translations: we use this + to introduce "identity" abstractions upon (re-)entering the loop. + + For instance, the fixed point for [list_nth_mut] (see the top of the file) + is: + {[ + env_fp = { + abs@0 { ML l0 } + ls -> MB l1 (s@3 : loops::List<T>) + i -> s@4 : u32 + abs@fp { + MB l0 + ML l1 + } + } + ]} + + Upon re-entering the loop, starting from the fixed point, we get the + following environment: + {[ + env = { + abs@0 { ML l0 } + ls -> MB l5 (s@6 : loops::List<T>) + i -> s@7 : u32 + abs@1 { MB l0, ML l1 } + _@1 -> MB l1 (loops::List::Cons (ML l2, ML l3)) + _@2 -> MB l3 (@Box (ML l5)) // tail + _@3 -> MB l2 (s@3 : T) // hd + } + ]} + + We want to introduce an abstraction [abs@2], which has the same shape as [abs@fp] + above (the fixed-point abstraction), and which is actually the identity. If we do so, + we get an environment which is actually also a fixed point (we can collapse + the dummy variables and [abs@1] to actually retrieve the fixed point we + computed, and we use the fact that those values and abstractions can't be + *directly* manipulated unless we end this newly introduced [abs@2], which we + forbid). + + We match the *fixed point context* with the context upon entering the loop + by doing the following. + + 1. We filter [env_fp] and [env] to remove the newly introduced dummy variables + and abstractions. We get: + + {[ + filtered_env_fp = { + abs@0 { ML l0 } + ls -> MB l1 (s@3 : loops::List<T>) + i -> s@4 : u32 + // removed abs@fp + } + + filtered_env = { + abs@0 { ML l0 } + ls -> MB l5 (s@6 : loops::List<T>) + i -> s@7 : u32 + // removed abs@1, _@1, etc. + } + ]} + + 2. We match [filtered_env_fp] with [filtered_env] to compute a map from + the FP borrows/loans to the current borrows/loans (and also from symbolic values to + values). Note that we take care to *consider loans and borrows separately*, + and we ignore the "fixed" abstractions (which are unchanged - we checked that + when computing the fixed point). + We get: + {[ + borrows_map: { l1 -> l5 } // because we matched [MB l1 ...] with [MB l5 ...] + loans_map: {} // we ignore abs@0, which is "fixed" + ]} + + 3. We want to introduce an instance of [abs@fp] which is actually the + identity. From [compute_fixed_point_id_correspondance] and looking at + [abs@fp], we know we should link the instantiation of loan [l1] with the + instantiation of loan [l0]. We substitute [l0] with [l5] (following step 2.) + and introduce a fresh borrow [l6] for [l5] that we use to instantiate [l1]. + We get the following environment: + + {[ + env = { + abs@0 { ML l0 } + ls -> MB l6 (s@6 : loops::List<T>) + i -> s@7 : u32 + abs@1 { MB l0, ML l1 } + _@1 -> MB l1 (loops::List::Cons (ML l2, ML l3)) + _@2 -> MB l3 (@Box (ML l5)) // tail + _@3 -> MB l2 (s@3 : T) // hd + abs@2 { MB l5, ML l6 } // this is actually the identity: l6 = l5 + } + ]} + + 4. As we now have a fixed point (see above comments), we can consider than + [abs@2] links the current iteration to the last one before we exit. What we + are interested in is that: + - upon inserting [abs@2] we re-entered the loop, meaning in the translation + we need to insert a recursive call to the loop forward function + - upon ending [abs@2] we need to insert a call to the loop backward function + + Because we want to ignore them, we end the loans in the newly introduced + [abs@2] abstraction (i.e., [l6]). We get: + {[ + env = { + abs@0 { ML l0 } + ls -> ⊥ + i -> s@7 : u32 + abs@1 { MB l0, ML l1 } + _@1 -> MB l1 (loops::List::Cons (ML l2, ML l3)) + _@2 -> MB l3 (@Box (ML l5)) // tail + _@3 -> MB l2 (s@3 : T) // hd + abs@2 { MB l5 } + } + ]} + + TODO: we shouldn't need to end the loans, we should actually remove them + before inserting the new abstractions (we may have issues with the symbolic + values, if they contain borrows - above i points to [s@7], but it should + be a different symbolic value...). + + Finally, we use the map from symbolic values to values to compute the list of + input values of the loop: we simply list the values, by order of increasing + symbolic value id. We *do* use the fixed values (though they are in the frame) + because they may be *read* inside the loop. + + We can then proceed to finishing the symbolic execution and doing the + synthesis. + + Rem.: we might reorganize the [tgt_ctx] by ending loans for instance. + + **Parameters**: + - [config] + - [loop_id] + - [is_loop_entry]: [true] if first entry into the loop, [false] if re-entry + (i.e., continue). + - [fp_bl_maps]: for the abstractions in the fixed-point (the source context), + the maps from loans to borrows and borrows to loans, if those abstractions + are seen as identity abstractions (for every of those abstractions, there + must be a bijection between the borrows and the loans) + - [fp_input_svalues]: the list of symbolic values appearing in the fixed + point (the source context) and which must be instantiated during the match + (this is the list of input parameters of the loop). + - [fixed_ids] + - [src_ctx] + *) +val match_ctx_with_target : + C.config -> + V.loop_id -> + bool -> + borrow_loan_corresp -> + V.symbolic_value_id list -> + ids_sets -> + C.eval_ctx -> + st_cm_fun diff --git a/compiler/Logging.ml b/compiler/Logging.ml index 706ea5cb..9dc1f5e3 100644 --- a/compiler/Logging.ml +++ b/compiler/Logging.ml @@ -24,6 +24,15 @@ let pure_to_extract_log = L.get_logger "MainLogger.ExtractBase" (** Logger for Interpreter *) let interpreter_log = L.get_logger "MainLogger.Interpreter" +(** Logger for InterpreterLoopsMatchCtxs *) +let loops_match_ctxs_log = L.get_logger "MainLogger.Interpreter.LoopsMatchCtxs" + +(** Logger for InterpreterLoopsJoinCtxs *) +let loops_join_ctxs_log = L.get_logger "MainLogger.Interpreter.LoopsJoinCtxs" + +(** Logger for InterpreterLoopsFixedPoint *) +let loops_fixed_point_log = L.get_logger "MainLogger.Interpreter.FixedPoint" + (** Logger for InterpreterLoops *) let loops_log = L.get_logger "MainLogger.Interpreter.Loops" diff --git a/compiler/dune b/compiler/dune index 0d899ecf..ae9cef04 100644 --- a/compiler/dune +++ b/compiler/dune @@ -29,6 +29,10 @@ InterpreterExpansion InterpreterExpressions Interpreter + InterpreterLoopsCore + InterpreterLoopsMatchCtxs + InterpreterLoopsJoinCtxs + InterpreterLoopsFixedPoint InterpreterLoops InterpreterPaths InterpreterProjectors |