diff options
| -rw-r--r-- | src/Interpreter.ml | 33 | ||||
| -rw-r--r-- | src/Types.ml | 1 |
2 files changed, 18 insertions, 16 deletions
diff --git a/src/Interpreter.ml b/src/Interpreter.ml index 57a4e08b..5d6af03a 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -2172,13 +2172,22 @@ let eval_box_deref_mut (config : C.config) (** Auxiliary function - see [eval_non_local_function_call]. - Note that this function doesn't behave like the others: it does not expect + `Box::free` is not handled the same way as the other assumed functions: + - in the regular case, whenever we need to evaluate an assumed function, + we evaluate the operands, push a frame, call a dedicated function + to correctly update the variables in the frame (and mimic the execution + of a body) and finally pop the frame + - in the case of `Box::free`: the value given to this function is often + of the form `Box(⊥)` because we can move the value out of the + box before freeing the box. It makes it invalid to see box_free as a + "regular" function: it is not valid to call a function with arguments + which contain `⊥`. For this reason, we execute `Box::free` as drop_value, + but this is a bit annoying with regards to the semantics... + + Followingly this function doesn't behave like the others: it does not expect a stack frame to have been pushed, but rather simply behaves like [drop_value]. - Followingly: it updates the box value (by calling [drop_value]) and updates + It thus updates the box value (by calling [drop_value]) and updates the destination (by setting it to `()`). - - See the comments in [eval_non_local_function_call] for more explanations of - why we do this this way. *) let eval_box_free (config : C.config) (region_params : T.erased_region list) (type_params : T.ety list) (args : E.operand list) (dest : E.place) @@ -2223,17 +2232,9 @@ let eval_non_local_function_call (config : C.config) (ctx : C.eval_ctx) ^ dest)); (* There are two cases (and this is extremely annoying): - - the function is not box_free: evaluate the operands, push a frame - and call a dedicated function to correctly update the variables - in the frame (and mimic the execution of a body), pop the frame - - the function is box_free: the value given to this function is often - of the form `Box(⊥)` because we generally move the value out of the - box before freeing the box. The annoying thing is that it makes it - invalid to see box_free as a "regular" function: it is not valid - to call a function with arguments which contain `⊥`. For this reason, - we translate box_free as drop_value, but this is a bit annoying with - regards to the semantics... - TODO: think about that, deeply + - the function is not box_free + - the function is box_free + See [eval_box_free] *) match fid with | A.BoxFree -> diff --git a/src/Types.ml b/src/Types.ml index fce5c827..7b4da265 100644 --- a/src/Types.ml +++ b/src/Types.ml @@ -23,6 +23,7 @@ type region_var = { (** Unique index identifying the region - TODO: may be redundant *) rv_name : string option; (** Region name *) } +(* TODO: merge with type_var? (for the name collision issues) *) [@@deriving show] (** A region. |