From 18d0ef8946a5f339b9e0e52fd0ad00970c575523 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Wed, 24 Nov 2021 12:13:12 +0100 Subject: Implement the TwoPhaseMut case in eval_rvalue --- src/Interpreter.ml | 13 ++++++++----- 1 file changed, 8 insertions(+), 5 deletions(-) (limited to 'src') 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 -- cgit v1.2.3