diff options
Diffstat (limited to '')
| -rw-r--r-- | compiler/InterpreterBorrows.ml | 14 | ||||
| -rw-r--r-- | compiler/InterpreterBorrows.mli | 19 |
2 files changed, 22 insertions, 11 deletions
diff --git a/compiler/InterpreterBorrows.ml b/compiler/InterpreterBorrows.ml index ab3fb7ea..208918af 100644 --- a/compiler/InterpreterBorrows.ml +++ b/compiler/InterpreterBorrows.ml @@ -163,6 +163,8 @@ let end_borrow_get_borrow (allowed_abs : V.AbstractionId.id option) | V.AMutBorrow (bid, _) -> (* Check if this is the borrow we are looking for *) if bid = l then ( + (* TODO: treat this case differently. We should not introduce + a bottom value. *) (* When ending a mut borrow, there are two cases: * - in the general case, we have to end the whole abstraction * (and thus raise an exception to signal that to the caller) @@ -181,7 +183,8 @@ let end_borrow_get_borrow (allowed_abs : V.AbstractionId.id option) * Also note that, as we are moving the borrowed value inside the * abstraction (and not really giving the value back to the context) * we do not insert {!AEndedMutBorrow} but rather {!ABottom} *) - V.ABottom) + raise (Failure "Unimplemented") + (* V.ABottom *)) else (* Update the outer borrows before diving into the child avalue *) let outer = update_outer_borrows outer (Borrow bid) in @@ -201,7 +204,7 @@ let end_borrow_get_borrow (allowed_abs : V.AbstractionId.id option) | V.AIgnoredMutBorrow (_, _) | V.AEndedMutBorrow _ | V.AEndedIgnoredMutBorrow - { given_back_loans_proj = _; child = _; given_back_meta = _ } + { given_back = _; child = _; given_back_meta = _ } | V.AEndedSharedBorrow -> (* Nothing special to do *) super#visit_ABorrow outer bc @@ -337,7 +340,7 @@ let give_back_value (config : C.config) (bid : V.BorrowId.id) * the value... Think about a more elegant way. *) let given_back_meta = as_symbolic nv.value in (* The loan projector *) - let given_back_loans_proj = + let given_back = mk_aproj_loans_value_from_symbolic_value abs.regions sv in (* Continue giving back in the child value *) @@ -345,7 +348,7 @@ let give_back_value (config : C.config) (bid : V.BorrowId.id) (* Return *) V.ABorrow (V.AEndedIgnoredMutBorrow - { given_back_loans_proj; child; given_back_meta }) + { given_back; child; given_back_meta }) | _ -> raise (Failure "Unreachable") else (* Continue exploring *) @@ -1708,8 +1711,7 @@ let destructure_abs (abs_kind : V.abs_kind) (can_end : bool) (* Just explore the child *) list_avalues false push_fail child_av | V.AEndedIgnoredMutBorrow - { child = child_av; given_back_loans_proj = _; given_back_meta = _ } - -> + { child = child_av; given_back = _; given_back_meta = _ } -> (* We don't support nested borrows for now *) assert (not (ty_has_borrows ctx.type_context.type_infos child_av.ty)); (* Just explore the child *) diff --git a/compiler/InterpreterBorrows.mli b/compiler/InterpreterBorrows.mli index 6a8fb87c..a2a1cfde 100644 --- a/compiler/InterpreterBorrows.mli +++ b/compiler/InterpreterBorrows.mli @@ -215,14 +215,23 @@ type merge_duplicates_funcs = { abs'01 { mut_borrow l0, mut_borrow l2 } ]} + Also, we merge all their regions together. For instance, if [abs'0] projects + region [r0] and [abs'1] projects region [r1], we pick one of the two, say [r0] + (the one with the smallest index in practice) and substitute [r1] with [r0] + in the whole context. + Parameters: - [kind] - [can_end] - - [merge_funs]: in the case it can happen that a loan or a borrow appears in - both abstractions, we use those functions to merge the different occurrences - (such things can happen when joining environments: we might temporarily - duplicate borrows during the join, before merging those borrows together). - For instance, this happens for the following abstractions is forbidden: + - [merge_funs]: Those functions are used to merge borrows/loans with the + *same ids*. For instance, when performing environment joins we may introduce + abstractions which both contain loans/borrows with the same ids. When we + later merge those abstractions together, we need to call a merge function + to reconcile the borrows/loans. For instance, if both abstractions contain + the same shared loan [l0], we will call {!merge_ashared_borrows} to derive + a shared value for the merged shared loans. + + For instance, this happens for the following abstractions: {[ abs'0 { mut_borrow l0, mut_loan l1 } // mut_borrow l0 ! abs'1 { mut_borrow l0, mut_loan l2 } // mut_borrow l0 ! |