Update expand_bottom_value

1 files changed, 15 insertions, 241 deletions

diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index 17253fb8..0dd73cb2 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -865,7 +865,10 @@ let rec access_projection (access : projection_access) (env : env)
     { enter_shared_loans = true; enter_mut_borrows = true; enter_abs = true }
   in
   match p with
-  | [] -> Ok (env, { read = v; updated = update v })
+  | [] ->
+      let nv = update v in
+      assert (nv.ty = v.ty);
+      Ok (env, { read = v; updated = nv })
   | pe :: p' -> (
       (* Match on the projection element and the value *)
       match (pe, v.value) with
@@ -1032,7 +1035,7 @@ let read_place (config : config) (access : access_kind) (p : place) (env : env)
       Ok read_value
 
 (** Update the value at a given place *)
-let write_place (config : config) (access : access_kind) (p : place)
+let write_place (_config : config) (access : access_kind) (p : place)
     (nv : typed_value) (env : env) : env path_access_result =
   let access = access_kind_to_projection_access access in
   (* The update function substitutes the value with the new value *)
@@ -1043,238 +1046,7 @@ let write_place (config : config) (access : access_kind) (p : place)
       (* We ignore the read value *)
       Ok env1
 
-(*
-(*
-TODO: loans
-    (* Borrow dereferencement *)
-    | Deref, Borrow bc -> (
-      match (access, bc) with
-      | Read, SharedBorrow bid ->
-         let sv = lookup_shared_value_from_borrow_id bid env in
-         (match access_projection config access env p' sv with
-          | Error err -> Error err
-          | Ok res ->
-             let nv = { v with value = Borrow (SharedBorrow
-                                         ) 
-                             | Write, SharedBorrow _ ->
-                                failwith "Can't write to a shared borrow"
-                             | (Read | Write), MutBorrow (_, bv) ->
-                                access_projection config access env p' bv
-                             | Move, _ -> failwith "Can't move out of a borrow"
-                             (* We need to activate inactivated mutable borrows *)
-                             | _, InactivatedMutBorrow bid ->
-                                Error (FailInactivatedMutBorrow 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 _ | Assumed _ | Borrow _) ->
-                       failwith "Unreachable"
-                       *)
-
-(*
-(** Read the value at the end of a projection. *)
-let rec read_projection (config : config) (access : access_kind) (env : env)
-    (p : projection) (v : typed_value) :
-    (typed_value * typed_value) path_access_result =
-  match p with
-  | [] -> Ok v
-  | pe :: p' -> (
-      (* The projection is non-empty: we need to enter all the loans we find,
-       * if we are allowed to do so *)
-      let rec enter_loans (v : typed_value) : typed_value path_access_result =
-        match v.value with
-        | Loan lc -> (
-            match (access, lc) with
-            (* We can enter shared loans only if we are in "read" mode *)
-            | Read, SharedLoan (_, sv) -> enter_loans sv
-            | (Write | Move), SharedLoan (bids, _) ->
-                Error (FailSharedLoan bids)
-            (* We always have to end mutable loans *)
-            | _, MutLoan bid -> Error (FailMutLoan bid))
-        | _ -> Ok v
-      in
-      (* Enter inside the loans and match on the resulting value *)
-      match enter_loans v with
-      | Ok v -> (
-          (* 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 failwith "Unreachable"
-              | _ -> failwith "Unreachable");
-              (* Actually project *)
-              let fv = FieldId.nth adt.field_values field_id in
-              read_projection config access env p fv
-          (* Tuples *)
-          | Field (ProjTuple _, field_id), Tuple values ->
-              let fv = FieldId.nth values field_id in
-              read_projection config access env p fv
-          (* We can expand [Bottom] values only while *writing* to places *)
-          | _, Bottom -> failwith "Unreachable"
-          (* 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) ->
-              read_projection config access env p' bv
-          (* Borrow dereferencement *)
-          | Deref, Borrow bc -> (
-              match (access, bc) with
-              | Read, SharedBorrow bid ->
-                  let sv = lookup_shared_value_from_borrow_id bid env in
-                  read_projection config access env p' sv
-              | Write, SharedBorrow _ ->
-                  failwith "Can't write to a shared borrow"
-              | (Read | Write), MutBorrow (_, bv) ->
-                  read_projection config access env p' bv
-              | Move, _ -> failwith "Can't move out of a borrow"
-              (* We need to activate inactivated mutable borrows *)
-              | _, InactivatedMutBorrow bid ->
-                  Error (FailInactivatedMutBorrow 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 _ | Assumed _ | Borrow _ | Loan _) ->
-              failwith "Unreachable")
-      (* Entering loans failed *)
-      | res -> res)*)
-
-(** Read the value at the end of a place *)
-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
-    | [] -> failwith "Unreachable"
-    | Var (vid, v) :: env' ->
-        if vid = p.var_id then read_projection config access env0 p.projection v
-        else read_in_env env'
-    | Abs _ :: env' -> read_in_env env'
-  in
-  read_in_env env0
-
-(** Update the value at the end of a projection. *)
-let rec write_projection (config : config) (access : access_kind)
-    (new_value : typed_value) (p : projection) (v : typed_value) :
-    typed_value path_access_result =
-  match p with
-  | [] -> Ok v
-  | pe :: p' -> (
-      (* The projection is non-empty: we need to enter all the loans we find,
-       * if we are allowed to do so *)
-      let rec enter_loans (v : typed_value) : typed_value path_access_result =
-        match v.value with
-        | Loan lc -> (
-            match (access, lc) with
-            (* We can enter shared loans only if we are in "read" mode *)
-            | Read, SharedLoan (_, sv) -> enter_loans sv
-            | (Write | Move), SharedLoan (bids, _) ->
-                Error (FailSharedLoan bids)
-            (* We always have to end mutable loans *)
-            | _, MutLoan bid -> Error (FailMutLoan bid))
-        | _ -> Ok v
-      in
-      (* 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 failwith "Unreachable"
-          | _ -> failwith "Unreachable");
-          (* Actually project *)
-          let fv = FieldId.nth adt.field_values field_id in
-          (* 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 *)
-          let fv = FieldId.nth values field_id in
-          (* 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 *)
-              failwith "Unreachable"
-          | 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 _) ->
-          failwith "Unreachable")
-
-(** Update the value at the end of a place.
-
-    Note that the usage of this function is very general: it can be used to
-    update a place when evaluating an assignment, or to update the set of
-    borrows pointing to the same shared value, etc.
- *)
-let write_place (config : config) (access : access_kind) (nv : typed_value)
-    (p : place) (env0 : env) : env path_access_result =
-  let rec write_in_env env : env path_access_result =
-    match env with
-    | [] -> failwith "Unreachable"
-    | Var (vid, v) :: env' -> (
-        if vid = p.var_id then
-          match write_projection config nv p.projection v with
-          | Ok nv -> Ok (Var (vid, nv) :: env')
-          | Error res -> Error res
-        else
-          match write_in_env env' with
-          | Ok env'' -> Ok (Var (vid, v) :: env'')
-          | res -> res)
-    | Abs abs :: env' -> (
-        match write_in_env env' with
-        | Ok env'' -> Ok (Abs abs :: env'')
-        | res -> res)
-  in
-  write_in_env env0
-
-(** Auxiliary function to expand [Bottom] values
+(** Auxiliary helper to expand [Bottom] values.
 
     During compilation, rustc desaggregates the ADT initializations. The
     consequence is that the following rust code:
@@ -1296,8 +1068,8 @@ let write_place (config : config) (access : access_kind) (nv : typed_value)
     variant index when writing one of its fields).
 *)
 let expand_bottom_value (config : config) (tyctx : type_def TypeDefId.vector)
-    (p : place) (env : env) (remaining_pes : int) (pe : projection_elem)
-    (ty : ety) : env =
+    (access : access_kind) (p : place) (remaining_pes : int)
+    (pe : projection_elem) (ty : ety) (env : env) : env =
   (* Prepare the update: we need to take the proper prefix of the place
      during whose evaluation we got stuck *)
   let projection' =
@@ -1306,10 +1078,11 @@ let expand_bottom_value (config : config) (tyctx : type_def TypeDefId.vector)
          (List.length p.projection - remaining_pes))
   in
   let p' = { p with projection = projection' } in
-  (* The type of the [Bottom] value should be a tuple or an ADT: use it
-     to generate the expanded value. Note that the projection element we
-     got stuck at should be a field projection, and gives the variant id
-     if the [Bottom] value is an enumeration value.
+  (* Compute the expanded value.
+     The type of the [Bottom] value should be a tuple or an ADT.
+     Note that the projection element we got stuck at should be a
+     field projection, and gives the variant id if the [Bottom] value
+     is an enumeration value.
      Also, the expanded value should be the proper ADT variant or a tuple
      with the proper arity, with all the fields initialized to [Bottom]
   *)
@@ -1357,10 +1130,11 @@ let expand_bottom_value (config : config) (tyctx : type_def TypeDefId.vector)
   in
   let nv = { value = nv; ty } in
   (* Update the environment by inserting the expanded value at the proper place *)
-  match write_place config nv p' env with
+  match write_place config access p' nv env with
   | Ok env -> env
   | Error _ -> failwith "Unreachable"
 
+(*
 (** Update the environment to be able to read a place.
 
     When reading a place, we may be stuck along the way because some value