diff options
Diffstat (limited to '')
| -rw-r--r-- | src/Interpreter.ml | 22 |
1 files changed, 20 insertions, 2 deletions
diff --git a/src/Interpreter.ml b/src/Interpreter.ml index 60afa79a..5e12cd74 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -1516,6 +1516,8 @@ let eval_rvalue (config : config) (ctx : eval_ctx) (rvalue : rvalue) : (* 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 + let rv_ty = Types.Ref (Erased, v.ty, Shared) in + let rv = { value = Borrow (SharedBorrow bid); ty = rv_ty } in (* Compute the value with which to replace the value at place p *) let nv = match v.value with @@ -1531,8 +1533,24 @@ 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 }, v) - | Expressions.Mut -> raise Unimplemented + ({ ctx3 with env = env4 }, rv) + | Expressions.Mut -> + (* Access the value *) + let access = 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 + (* Compute the rvalue - write the value in a mutable borrow *) + let ctx2 = { ctx with env = env2 } in + let ctx3, bid = fresh_borrow_id ctx2 in + let rv_ty = Types.Ref (Erased, v.ty, Mut) in + let rv = { value = Borrow (MutBorrow (bid, v)); ty = rv_ty } in + (* Compute the value with which to replace the value at place p *) + let nv = { v with value = Loan (MutLoan bid) } in + (* 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) | UnaryOp (unop, op) -> raise Unimplemented | BinaryOp (binop, op1, op2) -> raise Unimplemented |