summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorSon Ho2021-12-08 12:05:35 +0100
committerSon Ho2021-12-08 12:05:35 +0100
commit2a9f50f0894a371358cc09dfa5d705e91c855764 (patch)
tree5c116f301fab07e7031618aa826ed7190ceea8bb /src
parentb8bd4db2aed58c6e8dc7578156e753edbc9c9cb3 (diff)
Insert commented code in Interpreter.ml
Diffstat (limited to 'src')
-rw-r--r--src/Interpreter.ml48
1 files changed, 48 insertions, 0 deletions
diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index 97763abe..d6367702 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -134,6 +134,26 @@ let lookup_loan_opt (ek : exploration_kind) (l : V.BorrowId.id) (env : C.env) :
if ek.enter_mut_borrows then super#visit_MutBorrow env bid mv else ()
(** Control the diving into mutable borrows *)
+ (* TODO
+ method! visit_Loan env lc =
+ match lc with
+ | V.SharedLoan (bids, sv) ->
+ (* Check if this is the loan we are looking for, and control the dive *)
+ if V.BorrowId.Set.mem l bids then
+ raise (FoundLoanContent (V.SharedLoan (bids, sv)))
+ else if ek.enter_shared_loans then
+ super#visit_SharedLoan env bids sv
+ else ()
+ | V.MutLoan bid ->
+ (* Check if this is the loan we are looking for *)
+ if bid = l then raise (FoundLoanContent (V.MutLoan bid))
+ else super#visit_MutLoan env bid
+ (** We reimplement [visit_Loan] (rather than the more precise functions
+ [visit_SharedLoan], etc.) on purpose: as we have an exhaustive match
+ below, we are more resilient to definition updates (the compiler
+ is our friend).
+ *)
+ *)
method! visit_SharedLoan env bids sv =
if V.BorrowId.Set.mem l bids then
raise (FoundLoanContent (V.SharedLoan (bids, sv)))
@@ -385,6 +405,34 @@ let rec bottom_in_value (v : V.typed_value) : bool =
let rec end_borrow_get_borrow_in_value (config : C.config) (io : inner_outer)
(l : V.BorrowId.id) (outer_borrows : borrow_ids option) (v0 : V.typed_value)
: V.typed_value * borrow_lres =
+ (* (* We use a reference to check if we update a borrow, and that we don't
+ * update more than one borrow. *)
+ let r = ref false in
+ let set_ref () =
+ assert (not !r);
+ r := true
+ in
+
+ (* The environment is used to keep track of the outer loans *)
+ let obj =
+ object
+ inherit [_] C.map_env_concrete as super
+
+ method! visit_MutLoan outer_borrows bid =
+ super#visit_MutLoan outer_borrows bid
+ (** Nothing particular to do *)
+
+ method! visit_SharedLoan outer_borrows bids v =
+ let outer_borrows = update_outer_borrows io outer_borrows (Borrows bids) in
+ super#visit_SharedLoan outer_borrows bids v
+ (** Update the outer borrows *)
+
+ method! visit_borrow_content outer_borrows bc =
+ match bc with
+ | V.SharedBorrow l' ->
+ if l = l' then (set_ref (); Bottom
+
+ method! visit_MutBorrow outer_borrows bid mv = *)
match v0.V.value with
| V.Concrete _ | V.Bottom | V.Symbolic _ -> (v0, NotFound)
| V.Adt adt ->