summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorSon Ho2021-11-24 12:13:12 +0100
committerSon Ho2021-11-24 12:13:12 +0100
commit18d0ef8946a5f339b9e0e52fd0ad00970c575523 (patch)
tree67d2386138dfd5baf9811e1037e0ac7906d1701d /src
parent95494c3efe9d49c55398dff2d755748808d7e7b4 (diff)
Implement the TwoPhaseMut case in eval_rvalue
Diffstat (limited to 'src')
-rw-r--r--src/Interpreter.ml13
1 files changed, 8 insertions, 5 deletions
diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index 5e12cd74..29f06e87 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -1507,9 +1507,9 @@ let eval_rvalue (config : config) (ctx : eval_ctx) (rvalue : rvalue) :
| Use op -> eval_operand config ctx op
| Ref (p, bkind) -> (
match bkind with
- | Expressions.Shared ->
+ | Expressions.Shared | Expressions.TwoPhaseMut ->
(* Access the value *)
- let access = Read in
+ let access = if bkind = Expressions.Shared then Read else Write 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
let v = read_place_unwrap config access p ctx.env in
@@ -1517,7 +1517,11 @@ let eval_rvalue (config : config) (ctx : eval_ctx) (rvalue : rvalue) :
let ctx2 = { ctx with env = env2 } in
let ctx3, bid = fresh_borrow_id ctx2 in
let rv_ty = Types.Ref (Erased, v.ty, Shared) in
- let rv = { value = Borrow (SharedBorrow bid); ty = rv_ty } in
+ let bc =
+ if bkind = Expressions.Shared then SharedBorrow bid
+ else InactivatedMutBorrow bid
+ in
+ let rv = { value = Borrow bc; ty = rv_ty } in
(* Compute the value with which to replace the value at place p *)
let nv =
match v.value with
@@ -1550,8 +1554,7 @@ let eval_rvalue (config : config) (ctx : eval_ctx) (rvalue : rvalue) :
(* Update the value in the environment *)
let env4 = write_place_unwrap config access p nv ctx3.env in
(* Return *)
- ({ ctx3 with env = env4 }, rv)
- | Expressions.TwoPhaseMut -> raise Unimplemented)
+ ({ ctx3 with env = env4 }, rv))
| UnaryOp (unop, op) -> raise Unimplemented
| BinaryOp (binop, op1, op2) -> raise Unimplemented
| Discriminant p -> raise Unimplemented