Implement update_env_at_place

2 files changed, 79 insertions, 4 deletions

diff --git a/src/Identifiers.ml b/src/Identifiers.ml
index adcb9124..21898498 100644
--- a/src/Identifiers.ml
+++ b/src/Identifiers.ml
@@ -29,6 +29,8 @@ module type Id = sig
 
   val update_nth : 'a vector -> id -> 'a -> 'a vector
 
+  val iter : ('a -> unit) -> 'a vector -> unit
+
   val map : ('a -> 'b) -> 'a vector -> 'b vector
 
   module Set : Set.S with type elt = id
@@ -79,6 +81,8 @@ module IdGen () : Id = struct
     | _ :: vec', 0 -> v :: vec'
     | x :: vec', _ -> x :: update_nth vec' (id - 1) v
 
+  let iter = List.iter
+
   let map = List.map
 
   module Set = Set.Make (struct
diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index f8f991c6..70fcf2b0 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -449,7 +449,7 @@ let activate_inactivated_mut_borrow (config : config) (l : BorrowId.id)
 
 (** Paths *)
 
-type path_access = Read | Write
+type access_kind = Read | Write
 
 (** When we fail reading from or writing to a path, it might be because we
  ** need to update the environment by ending borrows, expanding symbolic
@@ -513,7 +513,7 @@ let lookup_shared_value_from_borrow_id (bid : BorrowId.id) (env : env) :
   | Some v -> v
 
 (** Read the value at the end of a projection *)
-let rec read_projection (config : config) (access : path_access) (env : env)
+let rec read_projection (config : config) (access : access_kind) (env : env)
     (p : projection) (v : typed_value) : typed_value path_access_result =
   match p with
   | [] -> Ok v
@@ -581,7 +581,7 @@ let rec read_projection (config : config) (access : path_access) (env : env)
       | res -> res)
 
 (** Read the value at the end of a place *)
-let read_place (config : config) (access : path_access) (p : place) (env0 : env)
+let read_place (config : config) (access : access_kind) (p : place) (env0 : env)
     : typed_value path_access_result =
   let rec read_in_env env : typed_value path_access_result =
     match env with
@@ -784,7 +784,7 @@ let expand_bottom_value (config : config) (tyctx : type_def TypeDefId.vector)
     uses this information to update the environment (by ending borrows,
     expanding symbolic values) until we manage to fully read the place.
  *)
-let rec update_env_along_read_place (config : config) (access : path_access)
+let rec update_env_along_read_place (config : config) (access : access_kind)
     (p : place) (env : env) : typed_value * env =
   (* Attempt to read the place: if it fails, update the environment and retry *)
   match read_place config access p env with
@@ -830,3 +830,74 @@ let rec update_env_along_write_place (config : config)
             expand_bottom_value config tyctx p env remaining_pes pe ty
       in
       update_env_along_write_place config tyctx nv p env'
+
+exception UpdateEnv of env
+(** Small utility used to break control-flow *)
+
+(** Update the value at a given place to be able to perform a manipulation.
+
+    This is used when reading, borrowing, writing to a value. We typically
+    first call [update_env_along_read_place] or [update_env_along_write_place]
+    to get access to the value, then call this function to "prepare" the value.
+
+    The [access_kind] controls the type of operation we will perform:
+    - [Read]: copy the value, perform an immutable borrow
+    - [Write]: update the value, move, mutably borrow
+ *)
+let rec update_env_at_place (config : config) (access : access_kind) (p : place)
+    (env : env) : env =
+  (* First, retrieve the value *)
+  match read_place config access p env with
+  | Error _ -> failwith "Unreachable"
+  | Ok v -> (
+      (* Explore the value to check if we need to update the environment.
+         In particular, we need to end the proper loans in the value.
+         Also, we fail if the value contains any [Bottom].
+
+         We use exceptions to make it handy.
+      *)
+      let rec inspect_update v : unit =
+        match v.value with
+        | Concrete _ -> ()
+        | Bottom -> failwith "Unreachable"
+        | Symbolic _ ->
+            (* Nothing to do for symbolic values - note that if the value needs
+               to be copied, etc. we perform additional checks later *)
+            ()
+        | Adt adt -> FieldId.iter inspect_update adt.field_values
+        | Tuple values -> FieldId.iter inspect_update values
+        | Assumed (Box v) -> inspect_update v
+        | Borrow bc -> (
+            match bc with
+            | SharedBorrow _ -> ()
+            | MutBorrow (_, tv) -> inspect_update tv
+            | InactivatedMutBorrow bid ->
+                (* We need to activate inactivated borrows *)
+                let env' = activate_inactivated_mut_borrow config bid env in
+                raise (UpdateEnv env'))
+        | Loan lc -> (
+            match lc with
+            | SharedLoan (bids, ty) -> (
+                (* End the borrows if we need a [Write] access, otherwise dive into
+                   the shared value *)
+                match access with
+                | Read -> inspect_update ty
+                | Write ->
+                    let env' = end_borrows config bids env in
+                    raise (UpdateEnv env'))
+            | MutLoan bid ->
+                (* We always need to end mutable borrows *)
+                let env' = end_borrow config bid env in
+                raise (UpdateEnv env'))
+      in
+      (* Inspect the value and update the environment while doing so.
+         If the environment gets updated: perform a recursive call (many things
+         may have been updated in the environment: first we need to retrieve the
+         proper updated value - and this value may actually not be accessible
+         anymore
+      *)
+      try
+        inspect_update v;
+        (* No environment update required: return the current environment *)
+        env
+      with UpdateEnv env' -> update_env_at_place config access p env')