Start working on eval_rvalue

1 files changed, 38 insertions, 10 deletions

diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index 5db82445..60afa79a 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -1035,6 +1035,12 @@ let read_place (config : config) (access : access_kind) (p : place) (env : env)
       if config.check_invariants then assert (env1 = env);
       Ok read_value
 
+let read_place_unwrap (config : config) (access : access_kind) (p : place)
+    (env : env) : typed_value =
+  match read_place config access p env with
+  | Error _ -> failwith "Unreachable"
+  | Ok v -> v
+
 (** Update the value at a given place *)
 let write_place (_config : config) (access : access_kind) (p : place)
     (nv : typed_value) (env : env) : env path_access_result =
@@ -1047,6 +1053,12 @@ let write_place (_config : config) (access : access_kind) (p : place)
       (* We ignore the read value *)
       Ok env1
 
+let write_place_unwrap (config : config) (access : access_kind) (p : place)
+    (nv : typed_value) (env : env) : env =
+  match write_place config access p nv env with
+  | Error _ -> failwith "Unreachable"
+  | Ok env -> env
+
 (** Auxiliary helper to expand [Bottom] values.
 
     During compilation, rustc desaggregates the ADT initializations. The
@@ -1489,7 +1501,6 @@ let eval_operand (config : config) (ctx : eval_ctx) (op : operand) :
               let ctx3 = { ctx with env = env3 } in
               (ctx3, v)))
 
-(*
 let eval_rvalue (config : config) (ctx : eval_ctx) (rvalue : rvalue) :
     eval_ctx * typed_value =
   match rvalue with
@@ -1501,15 +1512,32 @@ let eval_rvalue (config : config) (ctx : eval_ctx) (rvalue : rvalue) :
           let access = Read in
           let env1 = update_env_along_read_place config access p ctx.env in
           let env2 = collect_borrows_at_place config access p env1 in
-          (* Update the value *)
-          ()
-      | Expressions.Mut -> ()
-      | Expressions.TwoPhaseMut -> ())
-  | UnaryOp (unop, op) -> ()
-  | BinaryOp (binop, op1, op2) -> ()
-  | Discriminant p -> ()
-  | Aggregate (aggregate_kind, ops) -> ()
- *)
+          let v = read_place_unwrap config access p ctx.env in
+          (* Compute the rvalue - simply a shared borrow with a fresh id *)
+          let ctx2 = { ctx with env = env2 } in
+          let ctx3, bid = fresh_borrow_id ctx2 in
+          (* Compute the value with which to replace the value at place p *)
+          let nv =
+            match v.value with
+            | Loan (SharedLoan (bids, sv)) ->
+                (* Shared loan: insert the new borrow id *)
+                let bids1 = BorrowId.Set.add bid bids in
+                { v with value = Loan (SharedLoan (bids1, sv)) }
+            | _ ->
+                (* Not a shared loan: add a wrapper *)
+                let v' = Loan (SharedLoan (BorrowId.Set.singleton bid, v)) in
+                { v with value = v' }
+          in
+          (* Update the value in the environment *)
+          let env4 = write_place_unwrap config access p nv ctx3.env in
+          (* Return *)
+          ({ ctx3 with env = env4 }, v)
+      | Expressions.Mut -> raise Unimplemented
+      | Expressions.TwoPhaseMut -> raise Unimplemented)
+  | UnaryOp (unop, op) -> raise Unimplemented
+  | BinaryOp (binop, op1, op2) -> raise Unimplemented
+  | Discriminant p -> raise Unimplemented
+  | Aggregate (aggregate_kind, ops) -> raise Unimplemented
 
 (* TODO:
    update write_value