diff options
author | Son Ho | 2022-10-20 21:11:57 +0200 |
---|---|---|
committer | Son Ho | 2022-10-20 21:11:57 +0200 |
commit | aa0b10a24b8e6b8323b0741e8573ba4fc6283409 (patch) | |
tree | a6d37eea3cf1d9f10711f6119ebc54f6832890f9 /src/InterpreterStatements.ml | |
parent | 5e1e4f11dc2f75f20728ea1022b29a67c87bc07c (diff) |
Fix the semantics of drop
Diffstat (limited to 'src/InterpreterStatements.ml')
-rw-r--r-- | src/InterpreterStatements.ml | 20 |
1 files changed, 16 insertions, 4 deletions
diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml index 34310ea1..ae9e59fe 100644 --- a/src/InterpreterStatements.ml +++ b/src/InterpreterStatements.ml @@ -20,20 +20,32 @@ open InterpreterExpressions (** The local logger *) let log = L.statements_log -(** Drop a value at a given place *) +(** Drop a value at a given place - TODO: factorize this with [assign_to_place] *) let drop_value (config : C.config) (p : E.place) : cm_fun = fun cf ctx -> - log#ldebug (lazy ("drop_value: place: " ^ place_to_string ctx p)); - (* Prepare the place (by ending the outer loans and the borrows). + log#ldebug + (lazy + ("drop_value: place: " ^ place_to_string ctx p ^ "\n- Initial context:\n" + ^ eval_ctx_to_string ctx)); + (* Prepare the place (by ending the outer loans). * Note that [prepare_lplace] will use the `Write` access kind: * it is ok, because when updating the value with [Bottom] below, * we will use the `Move` access *) - let end_borrows = true in + let end_borrows = false in let prepare = prepare_lplace config end_borrows p in (* Replace the value with [Bottom] *) let replace cf (v : V.typed_value) ctx = + (* Move the value at destination (that we will overwrite) to a dummy variable + * to preserve the borrows *) + let mv = read_place_unwrap config Write p ctx in + let ctx = C.ctx_push_dummy_var ctx mv in + (* Update the destination to ⊥ *) let nv = { v with value = V.Bottom } in let ctx = write_place_unwrap config Move p nv ctx in + log#ldebug + (lazy + ("drop_value: place: " ^ place_to_string ctx p ^ "\n- Final context:\n" + ^ eval_ctx_to_string ctx)); cf ctx in (* Compose and apply *) |