summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/Interpreter.ml39
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)