diff options
| -rw-r--r-- | src/Interpreter.ml | 148 | ||||
| -rw-r--r-- | src/Print.ml | 5 |
2 files changed, 90 insertions, 63 deletions
diff --git a/src/Interpreter.ml b/src/Interpreter.ml index dee5daf3..05dc3f5a 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -2226,26 +2226,28 @@ let eval_box_deref_mut (config : C.config) (** Auxiliary function - see [eval_non_local_function_call]. - In practice, does nothing put aside checking the input types: the box - value has been moved to a local variable in the function frame, this value - is then dropped uppon exiting. + Note that 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 + 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) (ctx : C.eval_ctx) : C.eval_ctx eval_result = - match (region_params, type_params, ctx.env) with - | ( [], - [ boxed_ty ], - Var (input_var, input_value) :: Var (_ret_var, _) :: C.Frame :: _ ) -> - (* Check the arguments *) - assert (input_var.var_ty = input_value.V.ty); - (* Sanity check for type invariant *) - (let input_ty = ty_get_box input_value.V.ty in + (type_params : T.ety list) (args : E.operand list) (dest : E.place) + (ctx : C.eval_ctx) : C.eval_ctx eval_result = + match (region_params, type_params, args) with + | [], [ boxed_ty ], [ E.Move input_box_place ] -> + (* Required type checking *) + let input_box = read_place_unwrap config Write input_box_place ctx in + (let input_ty = ty_get_box input_box.V.ty in assert (input_ty = boxed_ty)); - (* Required type checking *) + (* Drop the value *) + let ctx = drop_value config ctx input_box_place in - (* Update the return value *) - let dest = mk_place_from_var_id V.VarId.zero in + (* Update the destination by setting it to `()` *) let ctx = assign_to_place config ctx mk_unit_value dest in (* Return *) @@ -2274,53 +2276,74 @@ let eval_non_local_function_call (config : C.config) (ctx : C.eval_ctx) ^ "\n- type_params: " ^ type_params ^ "\n- args: " ^ args ^ "\n- dest: " ^ dest)); - (* Evaluate the operands *) - let ctx, args_vl = eval_operands config ctx args in - - (* Push the stack frame: we initialize the frame with the return variable, - and one variable per input argument *) - let ctx = ctx_push_frame ctx in + (* 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 + *) + match fid with + | A.BoxFree -> + (* Degenerate case: box_free *) + eval_box_free config region_params type_params args dest ctx + | _ -> ( + (* "Normal" case: not box_free *) + (* Evaluate the operands *) + let ctx, args_vl = eval_operands config ctx args in - (* Create and push the return variable *) - let ret_vid = V.VarId.zero in - let ret_ty = - get_non_local_function_return_type fid region_params type_params - in - let ret_var = mk_var ret_vid (Some "@return") ret_ty in - let ctx = C.ctx_push_uninitialized_var ctx ret_var in - - (* Create and push the input variables *) - let input_vars = - V.VarId.vector_to_list - (V.VarId.mapi_from1 - (fun id v -> (mk_var id None v.V.ty, v)) - (V.VarId.vector_of_list args_vl)) - in - let ctx = C.ctx_push_vars ctx input_vars in + (* Push the stack frame: we initialize the frame with the return variable, + and one variable per input argument *) + let ctx = ctx_push_frame ctx in - (* "Execute" the function body. As the functions are assumed, here we call - custom functions to perform the proper manipulations: we don't have - access to a body. *) - let res = - match fid with - | A.BoxNew -> eval_box_new config region_params type_params ctx - | A.BoxDeref -> eval_box_deref config region_params type_params ctx - | A.BoxDerefMut -> eval_box_deref_mut config region_params type_params ctx - | A.BoxFree -> eval_box_free config region_params type_params ctx - in + (* Create and push the return variable *) + let ret_vid = V.VarId.zero in + let ret_ty = + get_non_local_function_return_type fid region_params type_params + in + let ret_var = mk_var ret_vid (Some "@return") ret_ty in + let ctx = C.ctx_push_uninitialized_var ctx ret_var in + + (* Create and push the input variables *) + let input_vars = + V.VarId.vector_to_list + (V.VarId.mapi_from1 + (fun id v -> (mk_var id None v.V.ty, v)) + (V.VarId.vector_of_list args_vl)) + in + let ctx = C.ctx_push_vars ctx input_vars in + + (* "Execute" the function body. As the functions are assumed, here we call + custom functions to perform the proper manipulations: we don't have + access to a body. *) + let res = + match fid with + | A.BoxNew -> eval_box_new config region_params type_params ctx + | A.BoxDeref -> eval_box_deref config region_params type_params ctx + | A.BoxDerefMut -> + eval_box_deref_mut config region_params type_params ctx + | A.BoxFree -> failwith "Unreachable" + (* should have been treated above *) + in - (* Check if the function body evaluated correctly *) - match res with - | Error err -> Error err - | Ok ctx -> - (* Pop the stack frame and retrieve the return value *) - let ctx, ret_value = ctx_pop_frame config ctx in + (* Check if the function body evaluated correctly *) + match res with + | Error err -> Error err + | Ok ctx -> + (* Pop the stack frame and retrieve the return value *) + let ctx, ret_value = ctx_pop_frame config ctx in - (* Move the return value to its destination *) - let ctx = assign_to_place config ctx ret_value dest in + (* Move the return value to its destination *) + let ctx = assign_to_place config ctx ret_value dest in - (* Return *) - Ok ctx + (* Return *) + Ok ctx) (** Evaluate a statement *) let rec eval_statement (config : C.config) (ctx : C.eval_ctx) (st : A.statement) @@ -2455,10 +2478,13 @@ and eval_function_body (config : C.config) (ctx : C.eval_ctx) and eval_expression (config : C.config) (ctx : C.eval_ctx) (e : A.expression) : (C.eval_ctx * statement_eval_res) eval_result = (* Debugging *) - L.log#ldebug - (lazy - ("\n" ^ eval_ctx_to_string ctx ^ "\nAbout to evaluate expression: \n" - ^ expression_to_string ctx e ^ "\n")); + (match e with + | A.Statement _ | A.Sequence (_, _) -> () + | A.Loop _ | A.Switch (_, _) -> + L.log#ldebug + (lazy + ("\n" ^ eval_ctx_to_string ctx ^ "\nAbout to evaluate expression: \n" + ^ expression_to_string ctx e ^ "\n"))); (* Evaluate *) match e with | A.Statement st -> eval_statement config ctx st diff --git a/src/Print.ml b/src/Print.ml index 3c5fd71c..8547d5cb 100644 --- a/src/Print.ml +++ b/src/Print.ml @@ -236,7 +236,7 @@ module Values = struct (fun (field, value) -> field ^ " = " ^ value ^ ";") field_values in - let field_values = String.concat "; " field_values in + let field_values = String.concat " " field_values in adt_ident ^ " { " ^ field_values ^ " }" else adt_ident | Tuple values -> @@ -718,7 +718,8 @@ module CfimAst = struct "core::ops::deref::DerefMut" ^ params ^ "::deref_mut" | A.BoxFree -> "alloc::alloc::box_free" ^ params) in - name_params ^ args + let dest = place_to_string fmt call.A.dest in + dest ^ " := move " ^ name_params ^ args | A.Panic -> "panic" | A.Return -> "return" | A.Break i -> "break " ^ string_of_int i |