summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2021-11-24 12:06:36 +0100
committerSon Ho2021-11-24 12:06:36 +0100
commit94eab3dec29c67b6ed4281932385d7a6337c96f4 (patch)
tree8f395650e3741fda90aef6de9409ee0c5b90046e
parent782499394daad2152b173218f98f53a453f1fca8 (diff)
Start working on eval_rvalue
-rw-r--r--src/Interpreter.ml48
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