diff options
Diffstat (limited to '')
| -rw-r--r-- | src/Interpreter.ml | 39 |
1 files changed, 31 insertions, 8 deletions
diff --git a/src/Interpreter.ml b/src/Interpreter.ml index 971bced8..9787af65 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -182,8 +182,16 @@ let lookup_loan (ek : exploration_kind) (l : V.BorrowId.id) (env : C.env) : This is a helper function: it might break invariants. *) -let update_loan_in_value (ek : exploration_kind) (l : V.BorrowId.id) - (nlc : V.loan_content) (v : V.typed_value) : V.typed_value = +let update_loan_in_value (r : bool ref) (ek : exploration_kind) + (l : V.BorrowId.id) (nlc : V.loan_content) (v : V.typed_value) : + V.typed_value = + (* We use a reference to check that we update exactly one loan: when updating + * inside values, we check we don't update more than one loan. *) + let set_ref r = + assert (not !r); + r := true + in + let obj = object inherit [_] V.map_typed_value as super @@ -194,7 +202,9 @@ let update_loan_in_value (ek : exploration_kind) (l : V.BorrowId.id) (** Control the diving into mutable borrows *) method! visit_SharedLoan env bids sv = - if V.BorrowId.Set.mem l bids then nlc + if V.BorrowId.Set.mem l bids then ( + set_ref env; + nlc) else if ek.enter_shared_loans then super#visit_SharedLoan env bids sv else V.SharedLoan (bids, sv) (** Shared loan: checks if this is the loan we are looking for, and @@ -202,28 +212,41 @@ let update_loan_in_value (ek : exploration_kind) (l : V.BorrowId.id) *) method! visit_MutLoan env bid = - if bid = l then nlc else super#visit_MutLoan env bid + if bid = l then ( + set_ref env; + nlc) + else super#visit_MutLoan env bid (** Mut loan: checks if this is the loan we are looking for *) end in - obj#visit_typed_value () v + let v = obj#visit_typed_value r v in + v (** Update a loan content. The loan is referred to by a borrow id. - This is a helper function: it might break invariants. + This is a helper function: it might break invariants. + + TODO: use visitors for environments. *) let update_loan (ek : exploration_kind) (l : V.BorrowId.id) (nlc : V.loan_content) (env : C.env) : C.env = + (* We use a reference to check that we update exactly one loan. + * [update_loan_in_value] checks that we update at most once. + * We then check that we updated at least once before returning. *) + let r = ref false in let update_loan_in_env_value (ev : C.env_value) : C.env_value = match ev with - | C.Var (vid, v) -> Var (vid, update_loan_in_value ek l nlc v) + | C.Var (vid, v) -> Var (vid, update_loan_in_value r ek l nlc v) | C.Abs _ -> raise Unimplemented (* TODO *) | C.Frame -> C.Frame in - List.map update_loan_in_env_value env + let env = List.map update_loan_in_env_value env in + (* Check that we updated at least one loan *) + assert !r; + env (** Lookup a borrow content in a value *) let rec lookup_borrow_in_value (ek : exploration_kind) (l : V.BorrowId.id) |