diff options
| -rw-r--r-- | src/Interpreter.ml | 43 | ||||
| -rw-r--r-- | src/Values.ml | 16 |
2 files changed, 56 insertions, 3 deletions
diff --git a/src/Interpreter.ml b/src/Interpreter.ml index 4b2a303c..baf433c2 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -663,9 +663,48 @@ let end_borrow_get_borrow_in_env (io : inner_outer) let outer_borrows = update_outer_borrows io outer (Borrow l') in V.Borrow (super#visit_MutBorrow outer l' bv) - method! visit_ALoan outer bc = raise Unimplemented + method! visit_ALoan outer lc = + (* Note that the children avalues are just other, independent loans, + * so we don't need to update the outer borrows when diving in. + * We keep track of the parents/children relationship only because we + * need it to properly instantiate the backward functions when generating + * the pure translation. *) + match lc with + | V.AMutLoan (bid, av) -> + (* Nothing special to do *) + V.ALoan (super#visit_AMutLoan outer bid av) + | V.ASharedLoan (bids, v, av) -> + (* Explore the shared value - we need to update the outer borrows *) + let souter = update_outer_borrows io outer (Borrows bids) in + let v = super#visit_typed_value souter v in + (* Explore the child avalue - we keep the same outer borrows *) + let av = super#visit_typed_avalue outer av in + (* Reconstruct *) + V.ALoan (V.ASharedLoan (bids, v, av)) + | V.AEndedMutLoan { given_back; child } -> + (* The loan has ended, so no need to update the outer borrows *) + V.ALoan (super#visit_AEndedMutLoan outer given_back child) + | V.AEndedSharedLoan (v, av) -> + (* The loan has ended, so no need to update the outer borrows *) + V.ALoan (super#visit_AEndedSharedLoan outer v av) + | V.AIgnoredMutLoan (bid, av) -> + (* Nothing special to do *) + V.ALoan (super#visit_AIgnoredMutLoan outer bid av) + | V.AEndedIgnoredMutLoan { given_back; child } -> + (* Nothing special to do *) + V.ALoan (super#visit_AEndedIgnoredMutLoan outer given_back child) + | V.AIgnoredSharedLoan asb -> + (* Nothing special to do *) + V.ALoan (super#visit_AIgnoredSharedLoan outer asb) + (** We reimplement [visit_ALoan] because we may have to update the + outer borrows *) - method! visit_ABorrow outer bc = raise Unimplemented + method! visit_ABorrow outer bc = + match bc with + | V.AMutBorrow (bid, av) -> raise Unimplemented + | V.ASharedBorrow bid -> raise Unimplemented + | V.AIgnoredMutBorrow av -> raise Unimplemented + | V.AIgnoredSharedBorrow asb -> raise Unimplemented method! visit_abs outer abs = (* Update the outer abs *) diff --git a/src/Values.ml b/src/Values.ml index f2f2274d..44c80578 100644 --- a/src/Values.ml +++ b/src/Values.ml @@ -216,6 +216,14 @@ and adt_avalue = { field_values : typed_avalue list; } +(** A loan content as stored in an abstraction. + + Note that the children avalues are independent of the parent avalues. + For instance, the child avalue contained in an [AMutLoan] will likely + contain other, independent loans. We keep track of the hierarchy because + we need it to properly instantiate the backward functions when generating + the pure translation. +*) and aloan_content = | AMutLoan of (BorrowId.id[@opaque]) * typed_avalue | ASharedLoan of (BorrowId.set_t[@opaque]) * typed_value * typed_avalue @@ -227,7 +235,13 @@ and aloan_content = (** Note that when a borrow content is ended, it is replaced by Bottom (while we need to track ended loans more precisely, especially because of their - children values) *) + children values). + + Note that contrary to [aloan_content], here the children avalues are + note independent of the parent avalues. For instance, a value + `AMutBorrow (_, AMutBorrow (_, ...)` (ignoring the types) really is + to be seen like a `mut_borrow ... (mut_borrow ...)`. +*) and aborrow_content = | AMutBorrow of (BorrowId.id[@opaque]) * typed_avalue | ASharedBorrow of (BorrowId.id[@opaque]) |