diff options
| -rw-r--r-- | compiler/InterpreterBorrows.ml | 30 | ||||
| -rw-r--r-- | compiler/InterpreterExpansion.ml | 4 | ||||
| -rw-r--r-- | compiler/InterpreterLoops.ml | 193 | ||||
| -rw-r--r-- | compiler/InterpreterProjectors.ml | 31 | ||||
| -rw-r--r-- | compiler/InterpreterProjectors.mli | 12 | ||||
| -rw-r--r-- | compiler/Invariants.ml | 8 | ||||
| -rw-r--r-- | compiler/Print.ml | 6 | ||||
| -rw-r--r-- | compiler/Values.ml | 29 |
8 files changed, 279 insertions, 34 deletions
diff --git a/compiler/InterpreterBorrows.ml b/compiler/InterpreterBorrows.ml index d20a02a2..1b05911b 100644 --- a/compiler/InterpreterBorrows.ml +++ b/compiler/InterpreterBorrows.ml @@ -393,10 +393,10 @@ let give_back_value (config : C.config) (bid : V.BorrowId.id) | V.AEndedSharedLoan (_, _) -> (* Nothing special to do *) super#visit_ALoan opt_abs lc - | V.AIgnoredMutLoan (bid', child) -> + | V.AIgnoredMutLoan (opt_bid, child) -> (* This loan is ignored, but we may have to project on a subvalue * of the value which is given back *) - if bid' = bid then + if opt_bid = Some bid then (* Remember the given back value as a meta-value *) let given_back_meta = nv in (* Note that we replace the ignored mut loan by an *ended* ignored @@ -557,10 +557,10 @@ let give_back_avalue_to_same_abstraction (_config : C.config) | V.AEndedSharedLoan (_, _) -> (* Nothing special to do *) super#visit_ALoan opt_abs lc - | V.AIgnoredMutLoan (bid', child) -> + | V.AIgnoredMutLoan (bid_opt, child) -> (* This loan is ignored, but we may have to project on a subvalue * of the value which is given back *) - if bid' = bid then ( + if bid_opt = Some bid then ( (* Note that we replace the ignored mut loan by an *ended* ignored * mut loan. Also, this is not the loan we are looking for *per se*: * we don't register the fact that we inserted the value somewhere @@ -1626,10 +1626,15 @@ let destructure_abs (abs_kind : V.abs_kind) (can_end : bool) push { V.value; ty }; (* Explore the child *) list_avalues false push_fail child_av + | V.AIgnoredMutLoan (opt_bid, child_av) -> + (* We don't support nested borrows for now *) + assert (not (ty_has_borrows ctx.type_context.type_infos child_av.ty)); + assert (opt_bid = None); + (* Simply explore the child *) + list_avalues false push_fail child_av | V.AEndedMutLoan { child = child_av; given_back = _; given_back_meta = _ } | V.AEndedSharedLoan (_, child_av) - | V.AIgnoredMutLoan (_, child_av) | V.AEndedIgnoredMutLoan { child = child_av; given_back = _; given_back_meta = _ } | V.AIgnoredSharedLoan child_av -> @@ -1651,7 +1656,12 @@ let destructure_abs (abs_kind : V.abs_kind) (can_end : bool) | V.ASharedBorrow _ -> (* Nothing specific to do: keep the value as it is *) push av - | V.AIgnoredMutBorrow (_, child_av) + | V.AIgnoredMutBorrow (opt_bid, child_av) -> + (* We don't support nested borrows for now *) + assert (not (ty_has_borrows ctx.type_context.type_infos child_av.ty)); + assert (opt_bid = None); + (* Just explore the child *) + list_avalues false push_fail child_av | V.AEndedIgnoredMutBorrow { child = child_av; given_back_loans_proj = _; given_back_meta = _ } -> @@ -1659,9 +1669,11 @@ let destructure_abs (abs_kind : V.abs_kind) (can_end : bool) assert (not (ty_has_borrows ctx.type_context.type_infos child_av.ty)); (* Just explore the child *) list_avalues false push_fail child_av - | V.AProjSharedBorrow _ -> - (* Nothing specific to do: keep the value as it is *) - push_avalue av + | V.AProjSharedBorrow asb -> + (* We don't support nested borrows *) + assert (asb = []); + (* Nothing specific to do *) + () | V.AEndedMutBorrow _ | V.AEndedSharedBorrow -> (* If we get there it means the abstraction ended: it should not be in the context anymore (if we end *one* borrow in an abstraction, diff --git a/compiler/InterpreterExpansion.ml b/compiler/InterpreterExpansion.ml index 40c32ccc..8a563351 100644 --- a/compiler/InterpreterExpansion.ml +++ b/compiler/InterpreterExpansion.ml @@ -105,8 +105,8 @@ let apply_symbolic_expansion_to_target_avalues (config : C.config) assert (given_back = []); (* Apply the projector *) let projected_value = - apply_proj_loans_on_symbolic_expansion proj_regions expansion - original_sv.V.sv_ty + apply_proj_loans_on_symbolic_expansion proj_regions + ancestors_regions expansion original_sv.V.sv_ty in (* Replace *) projected_value.V.value) diff --git a/compiler/InterpreterLoops.ml b/compiler/InterpreterLoops.ml index b159ab58..00e6eb01 100644 --- a/compiler/InterpreterLoops.ml +++ b/compiler/InterpreterLoops.ml @@ -415,7 +415,12 @@ module type Matcher = sig V.typed_value -> V.borrow_id * V.typed_value - (** The shared value is the result of a match *) + (** 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 -> @@ -438,6 +443,93 @@ module type Matcher = sig *) val match_symbolic_with_other : bool -> V.symbolic_value -> 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 -> V.typed_avalue + + (** Parameters: + [ty0] + [bid0] + [ty1] + [bid1] + *) + val match_ashared_borrows : + T.rty -> V.borrow_id -> T.rty -> V.borrow_id -> V.typed_avalue + + (** Parameters: + [ty0] + [mv0] + [bid0] + [av0] + [ty1] + [mv1] + [bid1] + [av1] + [mv]: result of matching mv0 and mv1 + [av]: result of matching av0 and av1 + *) + val match_amut_borrows : + T.rty -> + V.mvalue -> + V.borrow_id -> + V.typed_avalue -> + T.rty -> + V.mvalue -> + V.borrow_id -> + V.typed_avalue -> + V.mvalue -> + V.typed_avalue -> + V.typed_avalue + + (** Parameters: + [ty0] + [ids0] + [v0] + [av0] + [ty1] + [ids1] + [v1] + [av1] + [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 -> + V.typed_value -> + V.typed_avalue -> + V.typed_avalue + + (** Parameters: + [ty0] + [id0] + [av0] + [ty1] + [id1] + [av1] + [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 -> + 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, @@ -473,7 +565,7 @@ module Match (M : Matcher) = struct assert (not (value_has_borrows ctx v1.V.value)); (* Merge *) M.match_distinct_adts v0.V.ty av0 av1) - | Bottom, Bottom -> v1 + | Bottom, Bottom -> v0 | Borrow bc0, Borrow bc1 -> let bc = match (bc0, bc1) with @@ -546,7 +638,83 @@ module Match (M : Matcher) = struct and match_typed_avalues (ctx : C.eval_ctx) (v0 : V.typed_avalue) (v1 : V.typed_avalue) : V.typed_avalue = - raise (Failure "Unreachable") + let match_rec = match_typed_values ctx in + let match_arec = match_typed_avalues ctx in + assert (v0.V.ty = v1.V.ty); + match (v0.V.value, v1.V.value) with + | V.APrimitive _, V.APrimitive _ -> + (* We simply ignore - those are actually not used *) + assert (v0.V.ty = v1.V.ty); + mk_aignored v0.V.ty + | 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 = v1.V.ty } + else (* Merge *) + M.match_distinct_aadts v0.V.ty av0 v1.V.ty av1 + | ABottom, ABottom -> v0 + | ABorrow bc0, ABorrow bc1 -> ( + match (bc0, bc1) with + | ASharedBorrow bid0, ASharedBorrow bid1 -> + M.match_ashared_borrows v0.V.ty bid0 v1.V.ty bid1 + | AMutBorrow (mv0, bid0, av0), AMutBorrow (mv1, bid1, av1) -> + (* Not sure what to do with the meta-value *) + let mv = match_rec mv0 mv1 in + let av = match_arec av0 av1 in + M.match_amut_borrows v0.V.ty mv0 bid0 av0 v1.V.ty mv1 bid1 av1 mv 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 -> ( + (* 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) -> + 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 sv + av + | AMutLoan (id0, av0), AMutLoan (id1, av1) -> + let av = match_arec av0 av1 in + M.match_amut_loans v0.V.ty id0 av0 v1.V.ty id1 av1 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... *) @@ -709,7 +877,7 @@ module MakeJoinMatcher (S : MatchJoinState) : Matcher = struct (* Return the new borrow *) (bid2, sv) - let match_shared_loans (ty : T.ety) (ids0 : V.loan_id_set) + 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 @@ -732,9 +900,13 @@ module MakeJoinMatcher (S : MatchJoinState) : Matcher = struct (* Return *) (ids, sv) - let match_mut_loans (_ : T.ety) (id0 : V.loan_id) (_ : V.loan_id) : V.loan_id - = - id0 + 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 = @@ -771,6 +943,13 @@ module MakeJoinMatcher (S : MatchJoinState) : Matcher = struct else raise (ValueMatchFailure (LoanInRight id))); (* Return a fresh symbolic value *) mk_fresh_symbolic_typed_value V.LoopJoin sv.sv_ty + + 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 (* diff --git a/compiler/InterpreterProjectors.ml b/compiler/InterpreterProjectors.ml index d656e158..87522d73 100644 --- a/compiler/InterpreterProjectors.ml +++ b/compiler/InterpreterProjectors.ml @@ -69,8 +69,7 @@ let rec apply_proj_borrows_on_shared_borrow (ctx : C.eval_ctx) | V.ReservedMutBorrow _, _ -> raise (Failure - "Can't apply a proj_borrow over a reserved mutable \ - borrow") + "Can't apply a proj_borrow over a reserved mutable borrow") | _ -> raise (Failure "Unreachable") in let asb = @@ -140,7 +139,19 @@ let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : C.eval_ctx) fresh_reborrow regions ancestors_regions bv ref_ty in V.AMutBorrow (mv, bid, bv) - | V.SharedBorrow (_, bid), T.Shared -> V.ASharedBorrow bid + | V.SharedBorrow (_, bid), T.Shared -> + (* Rem.: we don't need to also apply the projection on the + borrowed value, because for as long as the abstraction + lives then the shared borrow lives, which means that the + whole value is borrowed (and thus immutable). + This is not the case if the current borrow is not to be + projected to the current abstraction: if this happens, + then maybe there are borrows *inside* the shared value + which belong to the current abstraction, meaning we + need to lookup the shared value and project it (see the + other branch of the [if then else]). + *) + V.ASharedBorrow bid | V.ReservedMutBorrow _, _ -> raise (Failure @@ -150,7 +161,9 @@ let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : C.eval_ctx) in V.ABorrow bc else - (* Not in the set: ignore *) + (* Not in the set: ignore the borrow, but project the borrowed + value (maybe some borrows *inside* the borrowed value are in + the region set) *) let bc = match (bc, kind) with | V.MutBorrow (bid, bv), T.Mut -> @@ -249,7 +262,8 @@ let symbolic_expansion_non_shared_borrow_to_value (sv : V.symbolic_value) TODO: detailed comments. See [apply_proj_borrows] *) let apply_proj_loans_on_symbolic_expansion (regions : T.RegionId.Set.t) - (see : V.symbolic_expansion) (original_sv_ty : T.rty) : V.typed_avalue = + (ancestors_regions : T.RegionId.Set.t) (see : V.symbolic_expansion) + (original_sv_ty : T.rty) : V.typed_avalue = (* Sanity check: if we have a proj_loans over a symbolic value, it should * contain regions which we will project *) assert (ty_has_regions_in_set regions original_sv_ty); @@ -278,7 +292,12 @@ let apply_proj_loans_on_symbolic_expansion (regions : T.RegionId.Set.t) (V.ALoan (V.AMutLoan (bid, child_av)), ref_ty) else (* Not in the set: ignore *) - (V.ALoan (V.AIgnoredMutLoan (bid, child_av)), ref_ty) + (* If the borrow id is in the ancestor's regions, we still need + * to remember it *) + let opt_bid = + if region_in_set r ancestors_regions then Some bid else None + in + (V.ALoan (V.AIgnoredMutLoan (opt_bid, child_av)), ref_ty) | SeSharedRef (bids, spc), T.Ref (r, ref_ty, T.Shared) -> (* Sanity check *) assert (spc.V.sv_ty = ref_ty); diff --git a/compiler/InterpreterProjectors.mli b/compiler/InterpreterProjectors.mli index a6d8bd5c..602125c6 100644 --- a/compiler/InterpreterProjectors.mli +++ b/compiler/InterpreterProjectors.mli @@ -11,9 +11,19 @@ open InterpreterBorrowsCore Apply a proj_borrows on a shared borrow. Note that when projecting over shared values, we generate {!V.abstract_shared_borrows}, not {!V.avalue}s. + + Parameters: + [regions] + [ancestor_regions] + [see] + [original_sv_ty] *) val apply_proj_loans_on_symbolic_expansion : - T.RegionId.Set.t -> V.symbolic_expansion -> T.rty -> V.typed_avalue + T.RegionId.Set.t -> + T.RegionId.Set.t -> + V.symbolic_expansion -> + T.rty -> + V.typed_avalue (** Convert a symbolic expansion *which is not a borrow* to a value *) val symbolic_expansion_non_borrow_to_value : diff --git a/compiler/Invariants.ml b/compiler/Invariants.ml index d9ed9cea..2904289f 100644 --- a/compiler/Invariants.ml +++ b/compiler/Invariants.ml @@ -160,7 +160,8 @@ let check_loans_borrows_relation_invariant (ctx : C.eval_ctx) : unit = match lc with | V.AMutLoan (bid, _) -> register_mut_loan inside_abs bid | V.ASharedLoan (bids, _, _) -> register_shared_loan inside_abs bids - | V.AIgnoredMutLoan (bid, _) -> register_ignored_loan T.Mut bid + | V.AIgnoredMutLoan (Some bid, _) -> register_ignored_loan T.Mut bid + | V.AIgnoredMutLoan (None, _) | V.AIgnoredSharedLoan _ | V.AEndedMutLoan { given_back = _; child = _; given_back_meta = _ } | V.AEndedSharedLoan (_, _) @@ -571,7 +572,7 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit = | _ -> raise (Failure "Inconsistent context")) | V.ALoan lc, aty -> ( match lc with - | V.AMutLoan (bid, child_av) | V.AIgnoredMutLoan (bid, child_av) + | V.AMutLoan (bid, child_av) | V.AIgnoredMutLoan (Some bid, child_av) -> ( let borrowed_aty = aloan_get_expected_child_type aty in assert (child_av.V.ty = borrowed_aty); @@ -585,6 +586,9 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit = Subst.erase_regions sv.V.ty = Subst.erase_regions borrowed_aty) | _ -> raise (Failure "Inconsistent context")) + | V.AIgnoredMutLoan (None, child_av) -> + let borrowed_aty = aloan_get_expected_child_type aty in + assert (child_av.V.ty = borrowed_aty) | V.ASharedLoan (_, sv, child_av) | V.AEndedSharedLoan (sv, child_av) -> let borrowed_aty = aloan_get_expected_child_type aty in diff --git a/compiler/Print.ml b/compiler/Print.ml index 2b2f98f0..6c0c95ad 100644 --- a/compiler/Print.ml +++ b/compiler/Print.ml @@ -248,8 +248,10 @@ module Values = struct ^ ", " ^ typed_avalue_to_string fmt av ^ ")" - | AIgnoredMutLoan (bid, av) -> - "@ignored_mut_loan(" ^ V.BorrowId.to_string bid ^ ", " + | AIgnoredMutLoan (opt_bid, av) -> + "@ignored_mut_loan(" + ^ option_to_string V.BorrowId.to_string opt_bid + ^ ", " ^ typed_avalue_to_string fmt av ^ ")" | AEndedIgnoredMutLoan ml -> diff --git a/compiler/Values.ml b/compiler/Values.ml index efb0bb67..9c68ad4f 100644 --- a/compiler/Values.ml +++ b/compiler/Values.ml @@ -524,7 +524,7 @@ and aloan_content = We get (after some symbolic exansion): {[ abs0 { - a_mut_loan l0 (a_mut_loan l1) + a_mut_loan l0 (a_mut_loan l1 _) } px -> mut_borrow l0 (mut_borrow @s1) ]} @@ -542,7 +542,7 @@ and aloan_content = We get: {[ - abs0 { a_shared_loan {l0} @s0 ⊥ } + abs0 { a_shared_loan {l0} @s0 _ } px -> shared_loan l0 ]} *) @@ -579,7 +579,7 @@ and aloan_content = give back. We keep the shared value because it now behaves as a "regular" value (which contains borrows we might want to end...). *) - | AIgnoredMutLoan of loan_id * typed_avalue + | AIgnoredMutLoan of loan_id option * typed_avalue (** An ignored mutable loan. We need to keep track of ignored mutable loans, because we may have @@ -588,6 +588,9 @@ and aloan_content = the outer loan is ignored, however you need to keep track of it so that when ending the borrow corresponding to 'a you can correctly project on the inner value). + + Note that we need to do so only for borrows consumed by parent + abstractions, hence the optional loan id. Example: ======== @@ -692,7 +695,11 @@ and aborrow_content = Note that we need to do so only for borrows consumed by parent abstractions (hence the optional borrow id). - TODO: the below explanations are obsolete + Rem.: we don't have an equivalent for shared borrows because if + we ignore a shared borrow we don't need keep track it (we directly + use {!AProjSharedBorrow} to project the shared value). + + TODO: the explanations below are obsolete Example: ======== @@ -806,10 +813,22 @@ and aborrow_content = > px -> shared_loan {l1, l3, l4} (mut_borrow l0 (U32 0)) > ppx -> shared_loan {l2} (shared_borrow l1) > pppx -> ⊥ - > abs'a { a_proj_shared_borrow {l2} } + > abs'a { a_shared_borrow {l2} } > abs'b { a_proj_shared_borrow {l3} } // l3 reborrows l1 > abs'c { a_proj_shared_borrow {l4} } // l4 reborrows l0 ]} + + Rem.: we introduce {!AProjSharedBorrow} only when we project a shared + borrow *which is ignored* (i.e., the shared borrow doesn't belong to + the current abstraction). The reason is that if the shared borrow + belongs to the abstraction, then by introducing a shared borrow inside + the abstraction we make sure the whole value is shared (and thus immutable) + for as long as the abstraction lives, meaning reborrowing subvalues + is redundant. However, if the borrow doesn't belong to the abstraction, + we need to project the shared values because it may contain some + borrows which *do* belong to the current abstraction. + + TODO: maybe we should factorized [ASharedBorrow] and [AProjSharedBorrow]. *) (* TODO: the type of avalues doesn't make sense for loan avalues: they currently |