diff options
Diffstat (limited to 'compiler/InterpreterLoops.ml')
| -rw-r--r-- | compiler/InterpreterLoops.ml | 566 |
1 files changed, 495 insertions, 71 deletions
diff --git a/compiler/InterpreterLoops.ml b/compiler/InterpreterLoops.ml index 08607deb..002abfb5 100644 --- a/compiler/InterpreterLoops.ml +++ b/compiler/InterpreterLoops.ml @@ -49,11 +49,11 @@ let mk_match_ctx (ctx : C.eval_ctx) : match_ctx = { ctx; aids; sids; bids } type updt_env_kind = - | EndAbsInSrc of V.AbstractionId.id - | EndBorrowsInSrc of V.BorrowId.Set.t - | EndBorrowInSrc of V.BorrowId.id - | EndBorrowInTgt of V.BorrowId.id - | EndBorrowsInTgt of V.BorrowId.Set.t + | AbsInLeft of V.AbstractionId.id + | LoanInLeft of V.BorrowId.id + | LoansInLeft of V.BorrowId.Set.t + | LoanInRight of V.BorrowId.id + | LoansInRight of V.BorrowId.Set.t (** Utility exception *) exception ValueMatchFailure of updt_env_kind @@ -63,43 +63,87 @@ type joined_ctx_or_update = (match_ctx, updt_env_kind) result (** Union Find *) module UnionFind = UF.Make (UF.StoreMap) -(** A small utility *) +(** 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; - borrow_to_abs : V.AbstractionId.id V.BorrowId.Map.t; - loan_to_abs : V.AbstractionId.id V.BorrowId.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 (explore : V.abs -> bool) (env : C.env) : - 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 = - abs_to_borrows := - V.AbstractionId.Map.update abs_id - (fun bids -> Some (V.BorrowId.Set.add bid (Option.get bids))) - !abs_to_borrows; - assert (not (V.BorrowId.Map.mem bid !borrow_to_abs)); - borrow_to_abs := V.BorrowId.Map.add bid abs_id !borrow_to_abs + 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 = - abs_to_loans := - V.AbstractionId.Map.update abs_id - (fun bids -> Some (V.BorrowId.Set.add bid (Option.get bids))) - !abs_to_loans; - assert (not (V.BorrowId.Map.mem bid !loan_to_abs)); - loan_to_abs := V.BorrowId.Map.add bid abs_id !loan_to_abs + 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 = @@ -159,8 +203,10 @@ let compute_abs_borrows_loans_maps (explore : V.abs -> bool) (env : C.env) : abs_ids = List.rev !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; } (** Collapse an environment. @@ -178,11 +224,19 @@ let compute_abs_borrows_loans_maps (explore : V.abs -> bool) (env : C.env) : merge them. In effect, this allows us to merge newly introduced abstractions/borrows with their parent abstractions. + + [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) (thresh : cnt_thresholds) +let collapse_ctx (loop_id : V.LoopId.id) + (merge_funs : merge_duplicates_funcs option) (thresh : cnt_thresholds) (ctx0 : C.eval_ctx) : C.eval_ctx = let abs_kind = V.Loop loop_id in - let can_end = true in + let can_end = false in + let destructure_shared_values = true in let is_fresh_abs_id (id : V.AbstractionId.id) : bool = V.AbstractionId.Ord.compare thresh.aid id >= 0 in @@ -201,7 +255,8 @@ let collapse_ctx (loop_id : V.LoopId.id) (thresh : cnt_thresholds) | C.Var (DummyBinder id, v) -> if is_fresh_did id then let absl = - convert_value_to_abstractions abs_kind can_end ctx0 v + convert_value_to_abstractions abs_kind can_end + destructure_shared_values ctx0 v in List.map (fun abs -> C.Abs abs) absl else [ ee ]) @@ -210,18 +265,28 @@ let collapse_ctx (loop_id : V.LoopId.id) (thresh : cnt_thresholds) (* 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 explore env 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 - (* Use the maps to merge the abstractions together *) + (* 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 @@ -243,35 +308,41 @@ let collapse_ctx (loop_id : V.LoopId.id) (thresh : cnt_thresholds) (fun bid -> match V.BorrowId.Map.find_opt bid loan_to_abs with | None -> (* Nothing to do *) () - | Some 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 *) - (* Lookup the abstractions *) - let abs0 = C.ctx_lookup_abs !ctx abs_id0 in - let abs1 = C.ctx_lookup_abs !ctx abs_id1 in - (* Merge them - note that we take care to merge [abs0] into [abs1] - (the order is important). - *) - let nabs = merge_abstractions abs_kind can_end !ctx abs1 abs0 in - (* Update the environment *) - ctx := fst (C.ctx_subst_abs !ctx abs_id1 nabs); - ctx := fst (C.ctx_remove_abs !ctx abs_id0); - (* Update the union find *) - let abs_ref_merged = UF.union abs_ref0 abs_ref1 in - UF.set abs_ref_merged nabs.abs_id) + | 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 *) + (* Lookup the abstractions *) + let abs0 = C.ctx_lookup_abs !ctx abs_id0 in + let abs1 = C.ctx_lookup_abs !ctx abs_id1 in + (* Merge them - note that we take care to merge [abs0] into [abs1] + (the order is important). + *) + let nabs = + merge_abstractions abs_kind can_end merge_funs !ctx abs1 + abs0 + in + (* Update the environment *) + ctx := fst (C.ctx_subst_abs !ctx abs_id1 nabs); + ctx := fst (C.ctx_remove_abs !ctx abs_id0); + (* Update the union find *) + let abs_ref_merged = UF.union abs_ref0 abs_ref1 in + UF.set abs_ref_merged nabs.abs_id) + abs_ids1) bids) abs_ids; @@ -313,6 +384,355 @@ let match_rtypes (rid_map : T.RegionId.InjSubst.t ref) (ctx : C.eval_ctx) in match_types check_regions ctx ty0 ty1 +(** See {!Match} *) +module type Matcher = sig + (** 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 *) + val match_shared_borrows : + T.ety -> V.mvalue -> V.borrow_id -> V.borrow_id -> V.mvalue * 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 + + (** The shared value is the result of a match *) + 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 +end + +(** Generic functor to implement matching functions between values, environments, + etc. + + We use it for joins, to check if two environments are convertible, etc. + *) +module Match (M : Matcher) = struct + (** Match two values *) + 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 + assert (v0.V.ty = v1.V.ty); + match (v0.V.value, v1.V.value) with + | V.Primitive pv0, V.Primitive pv1 -> + if pv0 = pv1 then v1 + else ( + assert (v0.V.ty = v1.V.ty); + M.match_distinct_primitive_values v0.V.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 v0.V.ty av0 av1) + | Bottom, Bottom -> v1 + | Borrow bc0, Borrow bc1 -> + let bc = + match (bc0, bc1) with + | SharedBorrow (mv0, bid0), SharedBorrow (mv1, bid1) -> + (* Not completely sure what to do with the meta-value. If a shared + symbolic value gets expanded in a branch, it may be simplified + (by being folded back to a symbolic value) upon doing the join, + which as a result would lead to code where it is considered as + mutable (which is sound). On the other hand, if we access a + symbolic value in a loop, the translated loop should take it as + input anyway, so maybe this actually leads to equivalent + code. + *) + let mv = match_rec mv0 mv1 in + assert (not (value_has_borrows ctx mv.V.value)); + let mv, bid = M.match_shared_borrows v0.V.ty mv bid0 bid1 in + V.SharedBorrow (mv, 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 v0.V.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; V.ty = v1.V.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 v0.V.ty ids0 ids1 sv in + V.SharedLoan (ids, sv) + | MutLoan id0, MutLoan id1 -> + let id = M.match_mut_loans v0.V.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 -> + let sv = M.match_symbolic_values sv0 sv1 in + { v1 with V.value = V.Symbolic sv } + (* (* TODO: id check mapping *) + let id0 = lookup_sid sv0.sv_id in + let id1 = sv1.sv_id in + if id0 = id1 then ( + assert (sv0.sv_kind = sv1.sv_kind); + (* Sanity check: the types should be the same *) + match_rtypes rid_map ctx sv0.sv_ty sv1.sv_ty; + (* Return *) + v1) + else ( + (* 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)); + raise (Failure "Unimplemented") + *) + | 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 _, _ -> raise (Failure "Unimplemented") + | _, Symbolic _ -> raise (Failure "Unimplemented") + | _ -> raise (Failure "Unreachable") +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 + +module MakeJoinMatcher (S : MatchJoinState) : Matcher = struct + (** Small utility *) + let push_abs (abs : V.abs) : unit = S.nabs := abs :: !S.nabs + + 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) (mv : V.mvalue) (bid0 : V.borrow_id) + (bid1 : V.borrow_id) : V.mvalue * V.borrow_id = + if bid0 = bid1 then (mv, 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 sv = mk_fresh_symbolic_typed_value_from_ety V.LoopJoin ty in + + let _, bv_ty, kind = ty_as_ref 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; + can_end = false; + 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 *) + (sv, 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 (bid0, 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 sv = mk_fresh_symbolic_typed_value_from_ety V.LoopJoin ty in + + let _, bv_ty, kind = ty_as_ref 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 (bv, 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; + can_end = false; + 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 (ty : 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 loans to a value + to vary. However, we allow to dive inside a data-structure: in this + case, + *) + 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)); + + (* *) + raise (Failure "Unimplemented") + + let match_mut_loans (ty : T.ety) (id0 : V.loan_id) (id1 : V.loan_id) : + V.loan_id = + raise (Failure "Unimplemented") + + (** There are no constraints on the input symbolic values *) + let match_symbolic_values (sv0 : V.symbolic_value) (sv1 : V.symbolic_value) : + V.symbolic_value = + raise (Failure "Unimplemented") +end + +(* (** This function raises exceptions of kind {!ValueMatchFailue}. [convertible]: the function updates it to [false] if the result of the @@ -439,15 +859,16 @@ let rec match_typed_values (config : C.config) (thresh : cnt_thresholds) raise (Failure "Unimplemented")) | Loan lc, _ -> ( match lc with - | SharedLoan (ids, _) -> raise (ValueMatchFailure (EndBorrowsInSrc ids)) - | MutLoan id -> raise (ValueMatchFailure (EndBorrowInSrc id))) + | SharedLoan (ids, _) -> raise (ValueMatchFailure (LoansInLeft ids)) + | MutLoan id -> raise (ValueMatchFailure (LoanInLeft id))) | _, Loan lc -> ( match lc with - | SharedLoan (ids, _) -> raise (ValueMatchFailure (EndBorrowsInTgt ids)) - | MutLoan id -> raise (ValueMatchFailure (EndBorrowInTgt id))) + | SharedLoan (ids, _) -> raise (ValueMatchFailure (LoansInRight ids)) + | MutLoan id -> raise (ValueMatchFailure (LoanInRight id))) | Symbolic _, _ -> raise (Failure "Unimplemented") | _, Symbolic _ -> raise (Failure "Unimplemented") | _ -> raise (Failure "Unreachable") + *) (*(** This function raises exceptions of kind {!ValueMatchFailue} *) let rec match_typed_avalues (config : C.config) (thresh : cnt_thresholds) @@ -563,16 +984,19 @@ let rec match_typed_values (config : C.config) (thresh : cnt_thresholds) raise (Failure "Unimplemented")) | Loan lc, _ -> ( match lc with - | SharedLoan (ids, _) -> raise (ValueMatchFailure (EndBorrowsInSrc ids)) - | MutLoan id -> raise (ValueMatchFailure (EndBorrowInSrc id))) + | SharedLoan (ids, _) -> raise (ValueMatchFailure (LoansInLeft ids)) + | MutLoan id -> raise (ValueMatchFailure (LoanInLeft id))) | _, Loan lc -> ( match lc with - | SharedLoan (ids, _) -> raise (ValueMatchFailure (EndBorrowsInTgt ids)) - | MutLoan id -> raise (ValueMatchFailure (EndBorrowInTgt id))) + | SharedLoan (ids, _) -> raise (ValueMatchFailure (LoansInRight ids)) + | MutLoan id -> raise (ValueMatchFailure (LoanInRight id))) | _ -> raise (Failure "Unreachable")*) -(** Apply substitutions in the first abstraction, then merge the abstractions together. *) -let subst_merge_abstractions (loop_id : V.LoopId.id) (thresh : cnt_thresholds) +(** Apply substitutions in the first abstraction, then join the abstractions together. + + TODO: remove? + *) +let subst_join_abstractions (loop_id : V.LoopId.id) (thresh : cnt_thresholds) (rid_map : T.RegionId.InjSubst.t) (bid_map : V.BorrowId.InjSubst.t) (sid_map : V.SymbolicValueId.InjSubst.t) (ctx : C.eval_ctx) (abs0 : V.abs) (abs1 : V.abs) : V.abs = @@ -599,7 +1023,7 @@ let subst_merge_abstractions (loop_id : V.LoopId.id) (thresh : cnt_thresholds) (* Merge the two abstractions *) let abs_kind = V.Loop loop_id in let can_end = false in - merge_abstractions abs_kind can_end ctx abs0 abs1 + merge_abstractions abs_kind can_end None ctx abs0 abs1 (** Merge a borrow with the abstraction containing the associated loan, where the abstraction must be a *loop abstraction* (we don't synthesize code during @@ -750,22 +1174,22 @@ let compute_loop_entry_fixed_point (config : C.config) (* Check if the join succeeded, or if we need to end abstractions/borrows in the original environment first *) match join_ctxs mctx with - | Error (EndAbsInSrc id) -> + | Error (AbsInLeft id) -> let ctx1 = InterpreterBorrows.end_abstraction_no_synth config id mctx.ctx in eval_iteration_then_join { mctx with ctx = ctx1 } - | Error (EndBorrowInSrc id) -> + | Error (LoanInLeft id) -> let ctx1 = InterpreterBorrows.end_borrow_no_synth config id mctx.ctx in eval_iteration_then_join { mctx with ctx = ctx1 } - | Error (EndBorrowsInSrc ids) -> + | Error (LoansInLeft ids) -> let ctx1 = InterpreterBorrows.end_borrows_no_synth config ids mctx.ctx in eval_iteration_then_join { mctx with ctx = ctx1 } - | Error (EndBorrowInTgt _ | EndBorrowsInTgt _) -> + | Error (LoanInRight _ | LoansInRight _) -> (* Shouldn't happen here *) raise (Failure "Unreachable") | Ok mctx1 -> |