Make progress on write_projection

2 files changed, 92 insertions, 1 deletions

diff --git a/src/Identifiers.ml b/src/Identifiers.ml
index 04c5427b..dbe2ae83 100644
--- a/src/Identifiers.ml
+++ b/src/Identifiers.ml
@@ -1,3 +1,5 @@
+open Errors
+
 (** Signature for a module describing an identifier.
     
     We often need identifiers (for definitions, variables, etc.) and in
@@ -23,6 +25,8 @@ module type Id = sig
 
   val nth_opt : 'a vector -> id -> 'a option
 
+  val update_nth : 'a vector -> id -> 'a -> 'a vector
+
   module Set : Set.S with type elt = id
 
   val set_to_string : Set.t -> string
@@ -63,6 +67,12 @@ module IdGen () : Id = struct
 
   let nth_opt v id = List.nth_opt v id
 
+  let rec update_nth vec id v =
+    match (vec, id) with
+    | [], _ -> unreachable __LOC__
+    | _ :: vec', 0 -> v :: vec'
+    | x :: vec', _ -> x :: update_nth vec' (id - 1) v
+
   module Set = Set.Make (struct
     type t = id
 
diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index c5a1dad1..3dbb5020 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -536,7 +536,7 @@ let rec read_projection (config : config) (access : path_access) (env : env)
             (* We can enter shared loans only if we are in "read" mode *)
             | Read, SharedLoan (_, sv) -> enter_loans sv
             | Write, SharedLoan (bids, _) -> Error (FailSharedLoan bids)
-            (* We can always enter mutable loans *)
+            (* We always have to end mutable loans *)
             | _, MutLoan bid -> Error (FailMutLoan bid))
         | _ -> Ok v
       in
@@ -581,6 +581,7 @@ let rec read_projection (config : config) (access : path_access) (env : env)
                   read_projection config access env p' sv
               | Write, SharedBorrow _ -> unreachable __LOC__
               | _, MutBorrow (_, bv) -> read_projection config access env p' bv
+              (* We need to activate inactivated mutable borrows *)
               | _, InactivatedMutBorrow bid ->
                   Error (FailInactivatedMutBorrow bid))
           (* Remaining cases: error. We enumerate all the value variants
@@ -606,6 +607,86 @@ let read_place (config : config) (access : path_access) (p : place) (env0 : env)
   in
   read_in_env env0
 
+(** Update the value at the end of a projection *)
+let rec write_projection (config : config) (new_value : typed_value)
+    (p : projection) (v : typed_value) : typed_value path_access_result =
+  match p with
+  | [] -> Ok v
+  | pe :: p' -> (
+      (* Match on the projection element and the value *)
+      match (pe, v.value) with
+      (* Field projection *)
+      | Field (ProjAdt (_def_id, opt_variant_id), field_id), Adt adt -> (
+          (* Check that the projection is consistent with the current value *)
+          (match (opt_variant_id, adt.variant_id) with
+          | None, None -> ()
+          | Some vid, Some vid' -> if vid <> vid' then unreachable __LOC__
+          | _ -> unreachable __LOC__);
+          (* Actually project *)
+          match FieldId.nth_opt adt.field_values field_id with
+          | None -> unreachable __LOC__
+          | Some fv -> (
+              (* Update the field value *)
+              match write_projection config new_value p fv with
+              | Error err -> Error err
+              | Ok nfv ->
+                  (* Reinsert the field value *)
+                  let nvalues =
+                    FieldId.update_nth adt.field_values field_id nfv
+                  in
+                  let nadt = Adt { adt with field_values = nvalues } in
+                  Ok { v with value = nadt }))
+      (* Tuples *)
+      | Field (ProjTuple _, field_id), Tuple values -> (
+          (* Project *)
+          match FieldId.nth_opt values field_id with
+          | None -> unreachable __LOC__
+          | Some fv -> (
+              (* Update the field value *)
+              match write_projection config new_value p fv with
+              | Error err -> Error err
+              | Ok nfv ->
+                  (* Reinsert the field value *)
+                  let nvalues = FieldId.update_nth values field_id nfv in
+                  let ntuple = Tuple nvalues in
+                  Ok { v with value = ntuple }))
+      (* If we reach Bottom, it may mean we need to expand an uninitialized
+       * enumeration value *)
+      | Field (ProjAdt (_, Some _variant_id), _), Bottom ->
+          Error (FailBottom (1 + List.length p', pe, v.ty))
+      (* Symbolic value: needs to be expanded *)
+      | _, Symbolic sp ->
+          assert (config.mode = SymbolicMode);
+          (* Expand the symbolic value *)
+          Error (FailSymbolic (pe, sp))
+      (* Box dereferencement *)
+      | DerefBox, Assumed (Box bv) -> (
+          (* Update the boxed value *)
+          match write_projection config new_value p' bv with
+          | Error err -> Error err
+          | Ok nbv -> Ok { v with value = Assumed (Box nbv) })
+      (* Borrow dereferencement *)
+      | Deref, Borrow bc -> (
+          match bc with
+          | SharedBorrow _ ->
+              (* We can't update inside shared borrows *)
+              unreachable __LOC__
+          | MutBorrow (bid, bv) -> (
+              match write_projection config new_value p' bv with
+              | Error err -> Error err
+              | Ok nbv -> Ok { v with value = Borrow (MutBorrow (bid, nbv)) })
+          (* We need to activate inactivated mutable borrows *)
+          | InactivatedMutBorrow bid -> Error (FailInactivatedMutBorrow bid))
+      (* We can never enter loans *)
+      | _, Loan (SharedLoan (bids, _)) -> Error (FailSharedLoan bids)
+      (* We also always have to end mutable loans *)
+      | _, Loan (MutLoan bid) -> Error (FailMutLoan bid)
+      (* Remaining cases: error. We enumerate all the value variants
+       * on purpose, to make sure we statically catch errors if we
+       * modify the [value] definition. *)
+      | _, (Concrete _ | Adt _ | Tuple _ | Bottom | Assumed _ | Borrow _) ->
+          unreachable __LOC__)
+
 (*
 (** Update the value at the end of a projection *)
 let rec write_projection (config : config) (nv : typed_value) (p : projection)