From 239435fc667fa0d18979e603ce3fd4caa128cd54 Mon Sep 17 00:00:00 2001 From: Escherichia Date: Thu, 23 May 2024 23:21:12 +0200 Subject: Update the interpreter so that it is not written in CPS style (#120) * Start turning the compiler in a style which is less CPS * Update a function in InterpreterExpressions.ml * WIP work on cps * WIP * WIP, currently on InterpreterStatements.ml * WIP * Finished CPS-related modification * Fixed some warning related to documentation comments * Finished loop support, fixed a loop * fixed a typed value * Fixed check_disappeared related error * cleaned check_disappeared related error * Start cleaning up * Do more cleanup * Make some cleanup and fix an issue * Do more cleanup * Do more cleanup * Do more cleanup * Do more cleanup * Do more cleanup * Do more cleanup * Do more cleanup * Do more cleanup * Rename a function * Do more cleanup * Cleanup the loops code and fix some bugs * Cleanup assign_to_place * Make a minor cleanup --------- Co-authored-by: Son Ho --- compiler/InterpreterStatements.ml | 1280 +++++++++++++++++++------------------ 1 file changed, 645 insertions(+), 635 deletions(-) (limited to 'compiler/InterpreterStatements.ml') diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml index 9ad6487b..66677eff 100644 --- a/compiler/InterpreterStatements.ml +++ b/compiler/InterpreterStatements.ml @@ -20,7 +20,7 @@ let log = L.statements_log (** Drop a value at a given place - TODO: factorize this with [assign_to_place] *) let drop_value (config : config) (meta : Meta.meta) (p : place) : cm_fun = - fun cf ctx -> + fun ctx -> log#ldebug (lazy ("drop_value: place: " ^ place_to_string ctx p ^ "\n- Initial context:\n" @@ -29,11 +29,11 @@ let drop_value (config : config) (meta : Meta.meta) (p : place) : cm_fun = let access = Write in (* First make sure we can access the place, by ending loans or expanding * symbolic values along the path, for instance *) - let cc = update_ctx_along_read_place config meta access p in + let ctx, cc = update_ctx_along_read_place config meta access p ctx in (* Prepare the place (by ending the outer loans *at* the place). *) - let cc = comp cc (prepare_lplace config meta p) in + let v, ctx, cc = comp2 cc (prepare_lplace config meta p ctx) in (* Replace the value with {!Bottom} *) - let replace cf (v : typed_value) ctx = + let ctx = (* Move the value at destination (that we will overwrite) to a dummy variable * to preserve the borrows it may contain *) let mv = InterpreterPaths.read_place meta access p ctx in @@ -46,47 +46,41 @@ let drop_value (config : config) (meta : Meta.meta) (p : place) : cm_fun = (lazy ("drop_value: place: " ^ place_to_string ctx p ^ "\n- Final context:\n" ^ eval_ctx_to_string ~meta:(Some meta) ctx)); - cf ctx + ctx in (* Compose and apply *) - comp cc replace cf ctx + (ctx, cc) (** Push a dummy variable to the environment *) -let push_dummy_var (vid : DummyVarId.id) (v : typed_value) : cm_fun = - fun cf ctx -> - let ctx = ctx_push_dummy_var ctx vid v in - cf ctx +let push_dummy_var (vid : DummyVarId.id) (v : typed_value) (ctx : eval_ctx) : + eval_ctx = + ctx_push_dummy_var ctx vid v (** Remove a dummy variable from the environment *) -let remove_dummy_var (meta : Meta.meta) (vid : DummyVarId.id) - (cf : typed_value -> m_fun) : m_fun = - fun ctx -> +let remove_dummy_var (meta : Meta.meta) (vid : DummyVarId.id) (ctx : eval_ctx) : + typed_value * eval_ctx = let ctx, v = ctx_remove_dummy_var meta ctx vid in - cf v ctx + (v, ctx) (** Push an uninitialized variable to the environment *) -let push_uninitialized_var (meta : Meta.meta) (var : var) : cm_fun = - fun cf ctx -> - let ctx = ctx_push_uninitialized_var meta ctx var in - cf ctx +let push_uninitialized_var (meta : Meta.meta) (var : var) (ctx : eval_ctx) : + eval_ctx = + ctx_push_uninitialized_var meta ctx var (** Push a list of uninitialized variables to the environment *) -let push_uninitialized_vars (meta : Meta.meta) (vars : var list) : cm_fun = - fun cf ctx -> - let ctx = ctx_push_uninitialized_vars meta ctx vars in - cf ctx +let push_uninitialized_vars (meta : Meta.meta) (vars : var list) + (ctx : eval_ctx) : eval_ctx = + ctx_push_uninitialized_vars meta ctx vars (** Push a variable to the environment *) -let push_var (meta : Meta.meta) (var : var) (v : typed_value) : cm_fun = - fun cf ctx -> - let ctx = ctx_push_var meta ctx var v in - cf ctx +let push_var (meta : Meta.meta) (var : var) (v : typed_value) (ctx : eval_ctx) : + eval_ctx = + ctx_push_var meta ctx var v (** Push a list of variables to the environment *) -let push_vars (meta : Meta.meta) (vars : (var * typed_value) list) : cm_fun = - fun cf ctx -> - let ctx = ctx_push_vars meta ctx vars in - cf ctx +let push_vars (meta : Meta.meta) (vars : (var * typed_value) list) + (ctx : eval_ctx) : eval_ctx = + ctx_push_vars meta ctx vars (** Assign a value to a given place. @@ -97,7 +91,7 @@ let push_vars (meta : Meta.meta) (vars : (var * typed_value) list) : cm_fun = *) let assign_to_place (config : config) (meta : Meta.meta) (rv : typed_value) (p : place) : cm_fun = - fun cf ctx -> + fun ctx -> log#ldebug (lazy ("assign_to_place:" ^ "\n- rv: " @@ -106,58 +100,51 @@ let assign_to_place (config : config) (meta : Meta.meta) (rv : typed_value) ^ eval_ctx_to_string ~meta:(Some meta) ctx)); (* Push the rvalue to a dummy variable, for bookkeeping *) let rvalue_vid = fresh_dummy_var_id () in - let cc = push_dummy_var rvalue_vid rv in + let ctx = push_dummy_var rvalue_vid rv ctx in (* Prepare the destination *) - let cc = comp cc (prepare_lplace config meta p) in + let _, ctx, cc = prepare_lplace config meta p ctx in (* Retrieve the rvalue from the dummy variable *) - let cc = comp cc (fun cf _lv -> remove_dummy_var meta rvalue_vid cf) in + let rv, ctx = remove_dummy_var meta rvalue_vid ctx in + (* Move the value at destination (that we will overwrite) to a dummy variable + to preserve the borrows *) + let mv = InterpreterPaths.read_place meta Write p ctx in + let dest_vid = fresh_dummy_var_id () in + let ctx = ctx_push_dummy_var ctx dest_vid mv in + (* Write to the destination *) + (* Checks - maybe the bookkeeping updated the rvalue and introduced bottoms *) + exec_assert __FILE__ __LINE__ + (not (bottom_in_value ctx.ended_regions rv)) + meta "The value to move contains bottom"; (* Update the destination *) - let move_dest cf (rv : typed_value) : m_fun = - fun ctx -> - (* Move the value at destination (that we will overwrite) to a dummy variable - * to preserve the borrows *) - let mv = InterpreterPaths.read_place meta Write p ctx in - let dest_vid = fresh_dummy_var_id () in - let ctx = ctx_push_dummy_var ctx dest_vid mv in - (* Write to the destination *) - (* Checks - maybe the bookkeeping updated the rvalue and introduced bottoms *) - exec_assert __FILE__ __LINE__ - (not (bottom_in_value ctx.ended_regions rv)) - meta "The value to move contains bottom"; - (* Update the destination *) - let ctx = write_place meta Write p rv ctx in - (* Debug *) - log#ldebug - (lazy - ("assign_to_place:" ^ "\n- rv: " - ^ typed_value_to_string ~meta:(Some meta) ctx rv - ^ "\n- p: " ^ place_to_string ctx p ^ "\n- Final context:\n" - ^ eval_ctx_to_string ~meta:(Some meta) ctx)); - (* Continue *) - cf ctx - in - (* Compose and apply *) - comp cc move_dest cf ctx + let ctx = write_place meta Write p rv ctx in + (* Debug *) + log#ldebug + (lazy + ("assign_to_place:" ^ "\n- rv: " + ^ typed_value_to_string ~meta:(Some meta) ctx rv + ^ "\n- p: " ^ place_to_string ctx p ^ "\n- Final context:\n" + ^ eval_ctx_to_string ~meta:(Some meta) ctx)); + (* Return *) + (ctx, cc) (** Evaluate an assertion, when the scrutinee is not symbolic *) let eval_assertion_concrete (config : config) (meta : Meta.meta) (assertion : assertion) : st_cm_fun = - fun cf ctx -> + fun ctx -> (* There won't be any symbolic expansions: fully evaluate the operand *) - let eval_op = eval_operand config meta assertion.cond in - let eval_assert cf (v : typed_value) : m_fun = - fun ctx -> + let v, ctx, eval_op = eval_operand config meta assertion.cond ctx in + let st = match v.value with | VLiteral (VBool b) -> (* Branch *) - if b = assertion.expected then cf Unit ctx else cf Panic ctx + if b = assertion.expected then Unit else Panic | _ -> craise __FILE__ __LINE__ meta ("Expected a boolean, got: " ^ typed_value_to_string ~meta:(Some meta) ctx v) in (* Compose and apply *) - comp eval_op eval_assert cf ctx + ((ctx, st), eval_op) (** Evaluates an assertion. @@ -167,13 +154,12 @@ let eval_assertion_concrete (config : config) (meta : Meta.meta) *) let eval_assertion (config : config) (meta : Meta.meta) (assertion : assertion) : st_cm_fun = - fun cf ctx -> + fun ctx -> (* Evaluate the operand *) - let eval_op = eval_operand config meta assertion.cond in + let v, ctx, cf_eval_op = eval_operand config meta assertion.cond ctx in (* Evaluate the assertion *) - let eval_assert cf (v : typed_value) : m_fun = - fun ctx -> - sanity_check __FILE__ __LINE__ (v.ty = TLiteral TBool) meta; + sanity_check __FILE__ __LINE__ (v.ty = TLiteral TBool) meta; + let st, cf_eval_assert = (* We make a choice here: we could completely decouple the concrete and * symbolic executions here but choose not to. In the case where we * know the concrete value of the boolean we test, we use this value @@ -182,7 +168,7 @@ let eval_assertion (config : config) (meta : Meta.meta) (assertion : assertion) match v.value with | VLiteral (VBool _) -> (* Delegate to the concrete evaluation function *) - eval_assertion_concrete config meta assertion cf ctx + eval_assertion_concrete config meta assertion ctx | VSymbolic sv -> sanity_check __FILE__ __LINE__ (config.mode = SymbolicMode) meta; sanity_check __FILE__ __LINE__ (sv.sv_ty = TLiteral TBool) meta; @@ -191,20 +177,18 @@ let eval_assertion (config : config) (meta : Meta.meta) (assertion : assertion) * We will of course synthesize an assertion in the generated code * (see below). *) let ctx = - apply_symbolic_expansion_non_borrow config meta sv - (SeLiteral (VBool true)) ctx + apply_symbolic_expansion_non_borrow config meta sv ctx + (SeLiteral (VBool true)) in - (* Continue *) - let expr = cf Unit ctx in (* Add the synthesized assertion *) - S.synthesize_assertion ctx v expr + ((ctx, Unit), S.synthesize_assertion ctx v) | _ -> craise __FILE__ __LINE__ meta ("Expected a boolean, got: " ^ typed_value_to_string ~meta:(Some meta) ctx v) in (* Compose and apply *) - comp eval_op eval_assert cf ctx + (st, cc_comp cf_eval_op cf_eval_assert) (** Updates the discriminant of a value at a given place. @@ -219,7 +203,7 @@ let eval_assertion (config : config) (meta : Meta.meta) (assertion : assertion) *) let set_discriminant (config : config) (meta : Meta.meta) (p : place) (variant_id : VariantId.id) : st_cm_fun = - fun cf ctx -> + fun ctx -> log#ldebug (lazy ("set_discriminant:" ^ "\n- p: " ^ place_to_string ctx p @@ -229,69 +213,67 @@ let set_discriminant (config : config) (meta : Meta.meta) (p : place) ^ eval_ctx_to_string ~meta:(Some meta) ctx)); (* Access the value *) let access = Write in - let cc = update_ctx_along_read_place config meta access p in - let cc = comp cc (prepare_lplace config meta p) in + let ctx, cc = update_ctx_along_read_place config meta access p ctx in + let v, ctx, cc = comp2 cc (prepare_lplace config meta p ctx) in (* Update the value *) - let update_value cf (v : typed_value) : m_fun = - fun ctx -> - match (v.ty, v.value) with - | TAdt ((TAdtId _ as type_id), generics), VAdt av -> ( - (* There are two situations: - - either the discriminant is already the proper one (in which case we - don't do anything) - - or it is not the proper one, in which case we replace the value with - a variant with all its fields set to {!Bottom} - *) - match av.variant_id with - | None -> - craise __FILE__ __LINE__ meta - "Found a struct value while expected an enum" - | Some variant_id' -> - if variant_id' = variant_id then (* Nothing to do *) - cf Unit ctx - else - (* Replace the value *) - let bottom_v = - match type_id with - | TAdtId def_id -> - compute_expanded_bottom_adt_value meta ctx def_id - (Some variant_id) generics - | _ -> craise __FILE__ __LINE__ meta "Unreachable" - in - assign_to_place config meta bottom_v p (cf Unit) ctx) - | TAdt ((TAdtId _ as type_id), generics), VBottom -> - let bottom_v = - match type_id with - | TAdtId def_id -> - compute_expanded_bottom_adt_value meta ctx def_id - (Some variant_id) generics - | _ -> craise __FILE__ __LINE__ meta "Unreachable" - in - assign_to_place config meta bottom_v p (cf Unit) ctx - | _, VSymbolic _ -> - sanity_check __FILE__ __LINE__ (config.mode = SymbolicMode) meta; - (* This is a bit annoying: in theory we should expand the symbolic value - * then set the discriminant, because in the case the discriminant is - * exactly the one we set, the fields are left untouched, and in the - * other cases they are set to Bottom. - * For now, we forbid setting the discriminant of a symbolic value: - * setting a discriminant should only be used to initialize a value, - * or reset an already initialized value, really. *) - craise __FILE__ __LINE__ meta "Unexpected value" - | _, (VAdt _ | VBottom) -> - craise __FILE__ __LINE__ meta "Inconsistent state" - | _, (VLiteral _ | VBorrow _ | VLoan _) -> - craise __FILE__ __LINE__ meta "Unexpected value" - in - (* Compose and apply *) - comp cc update_value cf ctx + match (v.ty, v.value) with + | TAdt ((TAdtId _ as type_id), generics), VAdt av -> ( + (* There are two situations: + - either the discriminant is already the proper one (in which case we + don't do anything) + - or it is not the proper one, in which case we replace the value with + a variant with all its fields set to {!Bottom} + *) + match av.variant_id with + | None -> + craise __FILE__ __LINE__ meta + "Found a struct value while expecting an enum" + | Some variant_id' -> + if variant_id' = variant_id then (* Nothing to do *) + ((ctx, Unit), cc) + else + (* Replace the value *) + let bottom_v = + match type_id with + | TAdtId def_id -> + compute_expanded_bottom_adt_value meta ctx def_id + (Some variant_id) generics + | _ -> craise __FILE__ __LINE__ meta "Unreachable" + in + let ctx, cc = + comp cc (assign_to_place config meta bottom_v p ctx) + in + ((ctx, Unit), cc)) + | TAdt ((TAdtId _ as type_id), generics), VBottom -> + let bottom_v = + match type_id with + | TAdtId def_id -> + compute_expanded_bottom_adt_value meta ctx def_id (Some variant_id) + generics + | _ -> craise __FILE__ __LINE__ meta "Unreachable" + in + let ctx, cc = comp cc (assign_to_place config meta bottom_v p ctx) in + ((ctx, Unit), cc) + | _, VSymbolic _ -> + sanity_check __FILE__ __LINE__ (config.mode = SymbolicMode) meta; + (* This is a bit annoying: in theory we should expand the symbolic value + * then set the discriminant, because in the case the discriminant is + * exactly the one we set, the fields are left untouched, and in the + * other cases they are set to Bottom. + * For now, we forbid setting the discriminant of a symbolic value: + * setting a discriminant should only be used to initialize a value, + * or reset an already initialized value, really. *) + craise __FILE__ __LINE__ meta "Unexpected value" + | _, (VAdt _ | VBottom) -> craise __FILE__ __LINE__ meta "Inconsistent state" + | _, (VLiteral _ | VBorrow _ | VLoan _) -> + craise __FILE__ __LINE__ meta "Unexpected value" (** Push a frame delimiter in the context's environment *) let ctx_push_frame (ctx : eval_ctx) : eval_ctx = { ctx with env = EFrame :: ctx.env } (** Push a frame delimiter in the context's environment *) -let push_frame : cm_fun = fun cf ctx -> cf (ctx_push_frame ctx) +let push_frame (ctx : eval_ctx) : eval_ctx = ctx_push_frame ctx (** Small helper: compute the type of the return value for a specific instantiation of an assumed function. @@ -323,17 +305,19 @@ let get_assumed_function_return_type (meta : Meta.meta) (ctx : eval_ctx) AssociatedTypes.ctx_normalize_erase_ty meta ctx ty let move_return_value (config : config) (meta : Meta.meta) - (pop_return_value : bool) (cf : typed_value option -> m_fun) : m_fun = - fun ctx -> + (pop_return_value : bool) (ctx : eval_ctx) : + typed_value option * eval_ctx * (eval_result -> eval_result) = if pop_return_value then let ret_vid = VarId.zero in - let cc = eval_operand config meta (Move (mk_place_from_var_id ret_vid)) in - cc (fun v ctx -> cf (Some v) ctx) ctx - else cf None ctx + let v, ctx, cc = + eval_operand config meta (Move (mk_place_from_var_id ret_vid)) ctx + in + (Some v, ctx, cc) + else (None, ctx, fun e -> e) let pop_frame (config : config) (meta : Meta.meta) (pop_return_value : bool) - (cf : typed_value option -> m_fun) : m_fun = - fun ctx -> + (ctx : eval_ctx) : + typed_value option * eval_ctx * (eval_result -> eval_result) = (* Debug *) log#ldebug (lazy ("pop_frame:\n" ^ eval_ctx_to_string ~meta:(Some meta) ctx)); @@ -358,40 +342,31 @@ let pop_frame (config : config) (meta : Meta.meta) (pop_return_value : bool) ^ "]")); (* Move the return value out of the return variable *) - let cc = move_return_value config meta pop_return_value in - (* Sanity check *) - let cc = - comp_check_value cc (fun ret_value ctx -> - match ret_value with - | None -> () - | Some ret_value -> - sanity_check __FILE__ __LINE__ - (not (bottom_in_value ctx.ended_regions ret_value)) - meta) + let v, ctx, cc = move_return_value config meta pop_return_value ctx in + let _ = + match v with + | None -> () + | Some ret_value -> + sanity_check __FILE__ __LINE__ + (not (bottom_in_value ctx.ended_regions ret_value)) + meta in (* Drop the outer *loans* we find in the local variables *) - let cf_drop_loans_in_locals cf (ret_value : typed_value option) : m_fun = - (* Drop the loans *) - let locals = List.rev locals in - let cf_drop = - List.fold_left - (fun cf lid -> - drop_outer_loans_at_lplace config meta (mk_place_from_var_id lid) cf) - (cf ret_value) locals - in - (* Apply *) - cf_drop + let ctx, cc = + comp cc + ((* Drop the loans *) + let locals = List.rev locals in + fold_left_apply_continuation + (fun lid ctx -> + drop_outer_loans_at_lplace config meta (mk_place_from_var_id lid) ctx) + locals ctx) in - let cc = comp cc cf_drop_loans_in_locals in (* Debug *) - let cc = - comp_check_value cc (fun _ ctx -> - log#ldebug - (lazy - ("pop_frame: after dropping outer loans in local variables:\n" - ^ eval_ctx_to_string ~meta:(Some meta) ctx))) - in + log#ldebug + (lazy + ("pop_frame: after dropping outer loans in local variables:\n" + ^ eval_ctx_to_string ~meta:(Some meta) ctx)); (* Pop the frame - we remove the [Frame] delimiter, and reintroduce all * the local variables (which may still contain borrow permissions - but @@ -405,28 +380,22 @@ let pop_frame (config : config) (meta : Meta.meta) (pop_return_value : bool) EBinding (BDummy vid, v) :: pop env | EFrame :: env -> (* Stop here *) env in - let cf_pop cf (ret_value : typed_value option) : m_fun = - fun ctx -> - let env = pop ctx.env in - let ctx = { ctx with env } in - cf ret_value ctx - in - (* Compose and apply *) - comp cc cf_pop cf ctx + let env = pop ctx.env in + let ctx = { ctx with env } in + (* Return *) + (v, ctx, cc) (** Pop the current frame and assign the returned value to its destination. *) let pop_frame_assign (config : config) (meta : Meta.meta) (dest : place) : cm_fun = - let cf_pop = pop_frame config meta true in - let cf_assign cf ret_value : m_fun = - assign_to_place config meta (Option.get ret_value) dest cf - in - comp cf_pop cf_assign + fun ctx -> + let v, ctx, cc = pop_frame config meta true ctx in + comp cc (assign_to_place config meta (Option.get v) dest ctx) (** Auxiliary function - see {!eval_assumed_function_call} *) let eval_box_new_concrete (config : config) (meta : Meta.meta) (generics : generic_args) : cm_fun = - fun cf ctx -> + fun ctx -> (* Check and retrieve the arguments *) match (generics.regions, generics.types, generics.const_generics, ctx.env) @@ -443,30 +412,22 @@ let eval_box_new_concrete (config : config) (meta : Meta.meta) meta "The input given to Box::new doesn't have the proper type"; (* Move the input value *) - let cf_move = - eval_operand config meta (Move (mk_place_from_var_id input_var.index)) + let v, ctx, cc = + eval_operand config meta + (Move (mk_place_from_var_id input_var.index)) + ctx in (* Create the new box *) - let cf_create cf (moved_input_value : typed_value) : m_fun = - (* Create the box value *) - let generics = TypesUtils.mk_generic_args_from_types [ boxed_ty ] in - let box_ty = TAdt (TAssumed TBox, generics) in - let box_v = - VAdt { variant_id = None; field_values = [ moved_input_value ] } - in - let box_v = mk_typed_value meta box_ty box_v in - - (* Move this value to the return variable *) - let dest = mk_place_from_var_id VarId.zero in - let cf_assign = assign_to_place config meta box_v dest in - - (* Continue *) - cf_assign cf - in - - (* Compose and apply *) - comp cf_move cf_create cf ctx + (* Create the box value *) + let generics = TypesUtils.mk_generic_args_from_types [ boxed_ty ] in + let box_ty = TAdt (TAssumed TBox, generics) in + let box_v = VAdt { variant_id = None; field_values = [ v ] } in + let box_v = mk_typed_value meta box_ty box_v in + + (* Move this value to the return variable *) + let dest = mk_place_from_var_id VarId.zero in + comp cc (assign_to_place config meta box_v dest ctx) | _ -> craise __FILE__ __LINE__ meta "Inconsistent state" (** Auxiliary function - see {!eval_assumed_function_call}. @@ -490,7 +451,7 @@ let eval_box_new_concrete (config : config) (meta : Meta.meta) *) let eval_box_free (config : config) (meta : Meta.meta) (generics : generic_args) (args : operand list) (dest : place) : cm_fun = - fun cf ctx -> + fun ctx -> match (generics.regions, generics.types, generics.const_generics, args) with | [], [ boxed_ty ], [], [ Move input_box_place ] -> (* Required type checking *) @@ -502,18 +463,16 @@ let eval_box_free (config : config) (meta : Meta.meta) (generics : generic_args) meta; (* Drop the value *) - let cc = drop_value config meta input_box_place in + let ctx, cc = drop_value config meta input_box_place ctx in (* Update the destination by setting it to [()] *) - let cc = comp cc (assign_to_place config meta mk_unit_value dest) in - - (* Continue *) - cc cf ctx + comp cc (assign_to_place config meta mk_unit_value dest ctx) | _ -> craise __FILE__ __LINE__ meta "Inconsistent state" (** Evaluate a non-local function call in concrete mode *) let eval_assumed_function_call_concrete (config : config) (meta : Meta.meta) (fid : assumed_fun_id) (call : call) : cm_fun = + fun ctx -> let args = call.args in let dest = call.dest in match call.func with @@ -533,12 +492,12 @@ let eval_assumed_function_call_concrete (config : config) (meta : Meta.meta) match fid with | BoxFree -> (* Degenerate case: box_free *) - eval_box_free config meta generics args dest + eval_box_free config meta generics args dest ctx | _ -> (* "Normal" case: not box_free *) (* Evaluate the operands *) (* let ctx, args_vl = eval_operands config ctx args in *) - let cf_eval_ops = eval_operands config meta args in + let args_vl, ctx, cc = eval_operands config meta args ctx in (* Evaluate the call * @@ -547,53 +506,42 @@ let eval_assumed_function_call_concrete (config : config) (meta : Meta.meta) * below, without having to introduce an intermediary function call, * but it made it less clear where the computed values came from, * so we reversed the modifications. *) - let cf_eval_call cf (args_vl : typed_value list) : m_fun = - fun ctx -> - (* Push the stack frame: we initialize the frame with the return variable, - and one variable per input argument *) - let cc = push_frame in - - (* Create and push the return variable *) - let ret_vid = VarId.zero in - let ret_ty = - get_assumed_function_return_type meta ctx fid generics - in - let ret_var = mk_var ret_vid (Some "@return") ret_ty in - let cc = comp cc (push_uninitialized_var meta ret_var) in - - (* Create and push the input variables *) - let input_vars = - VarId.mapi_from1 - (fun id (v : typed_value) -> (mk_var id None v.ty, v)) - args_vl - in - let cc = comp cc (push_vars meta 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 cf_eval_body : cm_fun = - match fid with - | BoxNew -> eval_box_new_concrete config meta generics - | BoxFree -> - (* Should have been treated above *) - craise __FILE__ __LINE__ meta "Unreachable" - | ArrayIndexShared | ArrayIndexMut | ArrayToSliceShared - | ArrayToSliceMut | ArrayRepeat | SliceIndexShared | SliceIndexMut - -> - craise __FILE__ __LINE__ meta "Unimplemented" - in - - let cc = comp cc cf_eval_body in - - (* Pop the frame *) - let cc = comp cc (pop_frame_assign config meta dest) in - - (* Continue *) - cc cf ctx + (* Push the stack frame: we initialize the frame with the return variable, + and one variable per input argument *) + let ctx = push_frame ctx in + + (* Create and push the return variable *) + let ret_vid = VarId.zero in + let ret_ty = get_assumed_function_return_type meta ctx fid generics in + let ret_var = mk_var ret_vid (Some "@return") ret_ty in + let ctx = push_uninitialized_var meta ret_var ctx in + + (* Create and push the input variables *) + let input_vars = + VarId.mapi_from1 + (fun id (v : typed_value) -> (mk_var id None v.ty, v)) + args_vl in - (* Compose and apply *) - comp cf_eval_ops cf_eval_call) + let ctx = push_vars meta input_vars 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 ctx, cf_eval_body = + match fid with + | BoxNew -> eval_box_new_concrete config meta generics ctx + | BoxFree -> + (* Should have been treated above *) + craise __FILE__ __LINE__ meta "Unreachable" + | ArrayIndexShared | ArrayIndexMut | ArrayToSliceShared + | ArrayToSliceMut | ArrayRepeat | SliceIndexShared | SliceIndexMut + -> + craise __FILE__ __LINE__ meta "Unimplemented" + in + let cc = cc_comp cc cf_eval_body in + + (* Pop the frame *) + comp cc (pop_frame_assign config meta dest ctx)) (** Helper @@ -947,8 +895,8 @@ let eval_transparent_function_call_symbolic_inst (meta : Meta.meta) inst_sg ))) (** Evaluate a statement *) -let rec eval_statement (config : config) (st : statement) : st_cm_fun = - fun cf ctx -> +let rec eval_statement (config : config) (st : statement) : stl_cm_fun = + fun ctx -> (* Debugging *) log#ldebug (lazy @@ -959,16 +907,15 @@ let rec eval_statement (config : config) (st : statement) : st_cm_fun = ^ "\n\n")); (* Take a snapshot of the current context for the purpose of generating pretty names *) - let cc = S.cf_save_snapshot in + let cc = S.save_snapshot ctx in (* Expand the symbolic values if necessary - we need to do that before - * checking the invariants *) - let cc = comp cc (greedy_expand_symbolic_values config st.meta) in + checking the invariants *) + let ctx, cc = comp cc (greedy_expand_symbolic_values config st.meta ctx) in (* Sanity check *) - let cc = comp cc (Invariants.cf_check_invariants st.meta) in + Invariants.check_invariants st.meta ctx; (* Evaluate *) - let cf_eval_st cf : m_fun = - fun ctx -> + let stl, cf_eval_st = log#ldebug (lazy ("\neval_statement: cf_eval_st: statement:\n" @@ -980,96 +927,118 @@ let rec eval_statement (config : config) (st : statement) : st_cm_fun = match rvalue with | Global (gid, generics) -> (* Evaluate the global *) - eval_global config p gid generics cf ctx + eval_global config st.meta p gid generics ctx | _ -> (* Evaluate the rvalue *) - let cf_eval_rvalue = eval_rvalue_not_global config st.meta rvalue in + let res, ctx, cc = + eval_rvalue_not_global config st.meta rvalue ctx + in (* Assign *) - let cf_assign cf (res : (typed_value, eval_error) result) ctx = - log#ldebug - (lazy - ("about to assign to place: " ^ place_to_string ctx p - ^ "\n- Context:\n" - ^ eval_ctx_to_string ~meta:(Some st.meta) ctx)); + log#ldebug + (lazy + ("about to assign to place: " ^ place_to_string ctx p + ^ "\n- Context:\n" + ^ eval_ctx_to_string ~meta:(Some st.meta) ctx)); + let (ctx, res), cf_assign = match res with - | Error EPanic -> cf Panic ctx - | Ok rv -> ( - let expr = - assign_to_place config st.meta rv p (cf Unit) ctx - in - (* Update the synthesized AST - here we store meta-information. + | Error EPanic -> ((ctx, Panic), fun e -> e) + | Ok rv -> + (* Update the synthesized AST - here we store additional meta-information. * We do it only in specific cases (it is not always useful, and * also it can lead to issues - for instance, if we borrow a * reserved borrow, we later can't translate it to pure values...) *) - match rvalue with - | Global _ -> craise __FILE__ __LINE__ st.meta "Unreachable" - | Use _ - | RvRef (_, (BShared | BMut | BTwoPhaseMut | BShallow)) - | UnaryOp _ | BinaryOp _ | Discriminant _ | Aggregate _ -> - let rp = rvalue_get_place rvalue in - let rp = - match rp with - | Some rp -> Some (S.mk_mplace st.meta rp ctx) - | None -> None - in - S.synthesize_assignment ctx - (S.mk_mplace st.meta p ctx) - rv rp expr) + let cc = + match rvalue with + | Global _ -> craise __FILE__ __LINE__ st.meta "Unreachable" + | Use _ + | RvRef (_, (BShared | BMut | BTwoPhaseMut | BShallow)) + | UnaryOp _ | BinaryOp _ | Discriminant _ | Aggregate _ -> + let rp = rvalue_get_place rvalue in + let rp = + match rp with + | Some rp -> Some (S.mk_mplace st.meta rp ctx) + | None -> None + in + S.synthesize_assignment ctx + (S.mk_mplace st.meta p ctx) + rv rp + in + let ctx, cc = + comp cc (assign_to_place config st.meta rv p ctx) + in + ((ctx, Unit), cc) in - + let cc = cc_comp cc cf_assign in (* Compose and apply *) - comp cf_eval_rvalue cf_assign cf ctx) - | FakeRead p -> eval_fake_read config st.meta p (cf Unit) ctx + ([ (ctx, res) ], cc_singleton __FILE__ __LINE__ st.meta cc)) + | FakeRead p -> + let ctx, cc = eval_fake_read config st.meta p ctx in + ([ (ctx, Unit) ], cc_singleton __FILE__ __LINE__ st.meta cc) | SetDiscriminant (p, variant_id) -> - set_discriminant config st.meta p variant_id cf ctx - | Drop p -> drop_value config st.meta p (cf Unit) ctx - | Assert assertion -> eval_assertion config st.meta assertion cf ctx - | Call call -> eval_function_call config st.meta call cf ctx - | Panic -> cf Panic ctx - | Return -> cf Return ctx - | Break i -> cf (Break i) ctx - | Continue i -> cf (Continue i) ctx - | Nop -> cf Unit ctx + let (ctx, res), cc = set_discriminant config st.meta p variant_id ctx in + ([ (ctx, res) ], cc_singleton __FILE__ __LINE__ st.meta cc) + | Drop p -> + let ctx, cc = drop_value config st.meta p ctx in + ([ (ctx, Unit) ], cc_singleton __FILE__ __LINE__ st.meta cc) + | Assert assertion -> + let (ctx, res), cc = eval_assertion config st.meta assertion ctx in + ([ (ctx, res) ], cc_singleton __FILE__ __LINE__ st.meta cc) + | Call call -> eval_function_call config st.meta call ctx + | Panic -> ([ (ctx, Panic) ], cc_singleton __FILE__ __LINE__ st.meta cc) + | Return -> ([ (ctx, Return) ], cc_singleton __FILE__ __LINE__ st.meta cc) + | Break i -> ([ (ctx, Break i) ], cc_singleton __FILE__ __LINE__ st.meta cc) + | Continue i -> + ([ (ctx, Continue i) ], cc_singleton __FILE__ __LINE__ st.meta cc) + | Nop -> ([ (ctx, Unit) ], cc_singleton __FILE__ __LINE__ st.meta cc) | Sequence (st1, st2) -> (* Evaluate the first statement *) - let cf_st1 = eval_statement config st1 in - (* Evaluate the sequence *) - let cf_st2 cf res = - match res with - (* Evaluation successful: evaluate the second statement *) - | Unit -> eval_statement config st2 cf - (* Control-flow break: transmit. We enumerate the cases on purpose *) - | Panic | Break _ | Continue _ | Return | LoopReturn _ - | EndEnterLoop _ | EndContinue _ -> - cf res + let ctx_resl, cf_st1 = eval_statement config st1 ctx in + (* Evaluate the sequence (evaluate the second statement if the first + statement successfully evaluated, otherwise transfmit the control-flow + break) *) + let ctx_res_cfl = + List.map + (fun (ctx, res) -> + match res with + (* Evaluation successful: evaluate the second statement *) + | Unit -> eval_statement config st2 ctx + (* Control-flow break: transmit. We enumerate the cases on purpose *) + | Panic | Break _ | Continue _ | Return | LoopReturn _ + | EndEnterLoop _ | EndContinue _ -> + ([ (ctx, res) ], cc_singleton __FILE__ __LINE__ st.meta cc)) + ctx_resl + in + (* Put everything together: + - we return the flattened list of contexts and results + - we need to build the continuation which will build the whole + expression from the continuations for the individual branches + *) + let ctx_resl, cf_st2 = + comp_seqs __FILE__ __LINE__ st.meta ctx_res_cfl in - (* Compose and apply *) - comp cf_st1 cf_st2 cf ctx + (ctx_resl, cc_comp cf_st1 cf_st2) | Loop loop_body -> - InterpreterLoops.eval_loop config st.meta - (eval_statement config loop_body) - cf ctx - | Switch switch -> eval_switch config st.meta switch cf ctx + let eval_loop_body = eval_statement config loop_body in + InterpreterLoops.eval_loop config st.meta eval_loop_body ctx + | Switch switch -> eval_switch config st.meta switch ctx in (* Compose and apply *) - comp cc cf_eval_st cf ctx + (stl, cc_comp cc cf_eval_st) -and eval_global (config : config) (dest : place) (gid : GlobalDeclId.id) - (generics : generic_args) : st_cm_fun = - fun cf ctx -> +and eval_global (config : config) (meta : Meta.meta) (dest : place) + (gid : GlobalDeclId.id) (generics : generic_args) : stl_cm_fun = + fun ctx -> let global = ctx_lookup_global_decl ctx gid in match config.mode with | ConcreteMode -> (* Treat the evaluation of the global as a call to the global body *) let func = { func = FunId (FRegular global.body); generics } in let call = { func = FnOpRegular func; args = []; dest } in - (eval_transparent_function_call_concrete config global.item_meta.meta - global.body call) - cf ctx - | SymbolicMode -> + eval_transparent_function_call_concrete config meta global.body call ctx + | SymbolicMode -> ( (* Generate a fresh symbolic value. In the translation, this fresh symbolic value will be * defined as equal to the value of the global (see {!S.synthesize_global_eval}). *) - cassert __FILE__ __LINE__ (ty_no_regions global.ty) global.item_meta.meta + cassert __FILE__ __LINE__ (ty_no_regions global.ty) meta "Const globals should not contain regions"; (* Instantiate the type *) (* There shouldn't be any reference to Self *) @@ -1082,19 +1051,24 @@ and eval_global (config : config) (dest : place) (gid : GlobalDeclId.id) Subst.erase_regions_substitute_types ty_subst cg_subst tr_subst tr_self global.ty in - let sval = mk_fresh_symbolic_value global.item_meta.meta ty in - let cc = - assign_to_place config global.item_meta.meta + let sval = mk_fresh_symbolic_value meta ty in + let ctx, cc = + assign_to_place config meta (mk_typed_value_from_symbolic_value sval) - dest + dest ctx in - let e = cc (cf Unit) ctx in - S.synthesize_global_eval gid generics sval e + ( [ (ctx, Unit) ], + fun el -> + match el with + | Some [ e ] -> + (cc_comp (S.synthesize_global_eval gid generics sval) cc) (Some e) + | Some _ -> internal_error __FILE__ __LINE__ meta + | _ -> None )) (** Evaluate a switch *) and eval_switch (config : config) (meta : Meta.meta) (switch : switch) : - st_cm_fun = - fun cf ctx -> + stl_cm_fun = + fun ctx -> (* We evaluate the operand in two steps: * first we prepare it, then we check if its value is concrete or * symbolic. If it is concrete, we can then evaluate the operand @@ -1104,130 +1078,147 @@ and eval_switch (config : config) (meta : Meta.meta) (switch : switch) : * (and would thus floating in thin air...)! * *) (* Match on the targets *) - let cf_match : st_cm_fun = - fun cf ctx -> - match switch with - | If (op, st1, st2) -> - (* Evaluate the operand *) - let cf_eval_op = eval_operand config meta op in - (* Switch on the value *) - let cf_if (cf : st_m_fun) (op_v : typed_value) : m_fun = - fun ctx -> - match op_v.value with - | VLiteral (VBool b) -> - (* Evaluate the if and the branch body *) - let cf_branch cf : m_fun = - (* Branch *) - if b then eval_statement config st1 cf - else eval_statement config st2 cf - in - (* Compose the continuations *) - cf_branch cf ctx - | VSymbolic sv -> - (* Expand the symbolic boolean, and continue by evaluating - * the branches *) - let cf_true : st_cm_fun = eval_statement config st1 in - let cf_false : st_cm_fun = eval_statement config st2 in + match switch with + | If (op, st1, st2) -> + (* Evaluate the operand *) + let op_v, ctx, cf_eval_op = eval_operand config meta op ctx in + (* Switch on the value *) + let ctx_resl, cf_if = + match op_v.value with + | VLiteral (VBool b) -> + (* Branch *) + if b then eval_statement config st1 ctx + else eval_statement config st2 ctx + | VSymbolic sv -> + (* Expand the symbolic boolean, and continue by evaluating + the branches *) + let (ctx_true, ctx_false), cf_bool = expand_symbolic_bool config meta sv (S.mk_opt_place_from_op meta op ctx) - cf_true cf_false cf ctx - | _ -> craise __FILE__ __LINE__ meta "Inconsistent state" - in - (* Compose *) - comp cf_eval_op cf_if cf ctx - | SwitchInt (op, int_ty, stgts, otherwise) -> - (* Evaluate the operand *) - let cf_eval_op = eval_operand config meta op in - (* Switch on the value *) - let cf_switch (cf : st_m_fun) (op_v : typed_value) : m_fun = - fun ctx -> - match op_v.value with - | VLiteral (VScalar sv) -> - (* Evaluate the branch *) - let cf_eval_branch cf = - (* Sanity check *) - sanity_check __FILE__ __LINE__ (sv.int_ty = int_ty) meta; - (* Find the branch *) - match List.find_opt (fun (svl, _) -> List.mem sv svl) stgts with - | None -> eval_statement config otherwise cf - | Some (_, tgt) -> eval_statement config tgt cf - in - (* Compose *) - cf_eval_branch cf ctx - | VSymbolic sv -> - (* Expand the symbolic value and continue by evaluating the - * proper branches *) - let stgts = - List.map - (fun (cv, tgt_st) -> (cv, eval_statement config tgt_st)) - stgts - in - (* Several branches may be grouped together: every branch is described - * by a pair (list of values, branch expression). - * In order to do a symbolic evaluation, we make this "flat" by - * de-grouping the branches. *) - let stgts = - List.concat - (List.map - (fun (vl, st) -> List.map (fun v -> (v, st)) vl) - stgts) - in - (* Translate the otherwise branch *) - let otherwise = eval_statement config otherwise in - (* Expand and continue *) + ctx + in + let resl_true = eval_statement config st1 ctx_true in + let resl_false = eval_statement config st2 ctx_false in + let ctx_resl, cf_branches = + comp_seqs __FILE__ __LINE__ meta [ resl_true; resl_false ] + in + let cc el = + match cf_branches el with + | None -> None + | Some [ e_true; e_false ] -> cf_bool (Some (e_true, e_false)) + | _ -> internal_error __FILE__ __LINE__ meta + in + (ctx_resl, cc) + | _ -> craise __FILE__ __LINE__ meta "Inconsistent state" + in + (* Compose *) + (ctx_resl, cc_comp cf_eval_op cf_if) + | SwitchInt (op, int_ty, stgts, otherwise) -> + (* Evaluate the operand *) + let op_v, ctx, cf_eval_op = eval_operand config meta op ctx in + (* Switch on the value *) + let ctx_resl, cf_switch = + match op_v.value with + | VLiteral (VScalar sv) -> ( + (* Sanity check *) + sanity_check __FILE__ __LINE__ (sv.int_ty = int_ty) meta; + (* Find the branch *) + match List.find_opt (fun (svl, _) -> List.mem sv svl) stgts with + | None -> eval_statement config otherwise ctx + | Some (_, tgt) -> eval_statement config tgt ctx) + | VSymbolic sv -> + (* Several branches may be grouped together: every branch is described + by a pair (list of values, branch expression). + In order to do a symbolic evaluation, we make this "flat" by + de-grouping the branches. *) + let values, branches = + List.split + (List.concat + (List.map + (fun (vl, st) -> List.map (fun v -> (v, st)) vl) + stgts)) + in + (* Expand the symbolic value *) + let (ctx_branches, ctx_otherwise), cf_int = expand_symbolic_int config meta sv (S.mk_opt_place_from_op meta op ctx) - int_ty stgts otherwise cf ctx - | _ -> craise __FILE__ __LINE__ meta "Inconsistent state" - in - (* Compose *) - comp cf_eval_op cf_switch cf ctx - | Match (p, stgts, otherwise) -> - (* Access the place *) - let access = Read in - let expand_prim_copy = false in - let cf_read_p cf : m_fun = - access_rplace_reorganize_and_read config meta expand_prim_copy access - p cf - in - (* Match on the value *) - let cf_match (cf : st_m_fun) (p_v : typed_value) : m_fun = - fun ctx -> - (* The value may be shared: we need to ignore the shared loans - to read the value itself *) - let p_v = value_strip_shared_loans p_v in - (* Match *) - match p_v.value with - | VAdt adt -> ( - (* Evaluate the discriminant *) - let dv = Option.get adt.variant_id in - (* Find the branch, evaluate and continue *) - match List.find_opt (fun (svl, _) -> List.mem dv svl) stgts with - | None -> ( - match otherwise with - | None -> craise __FILE__ __LINE__ meta "No otherwise branch" - | Some otherwise -> eval_statement config otherwise cf ctx) - | Some (_, tgt) -> eval_statement config tgt cf ctx) - | VSymbolic sv -> - (* Expand the symbolic value - may lead to branching *) - let cf_expand = - expand_symbolic_adt config meta sv - (Some (S.mk_mplace meta p ctx)) - in - (* Re-evaluate the switch - the value is not symbolic anymore, - which means we will go to the other branch *) - cf_expand (eval_switch config meta switch) cf ctx - | _ -> craise __FILE__ __LINE__ meta "Inconsistent state" - in - (* Compose *) - comp cf_read_p cf_match cf ctx - in - (* Compose the continuations *) - cf_match cf ctx + int_ty values ctx + in + (* Evaluate the branches: first the "regular" branches *) + let resl_branches = + List.map + (fun (ctx, branch) -> eval_statement config branch ctx) + (List.combine ctx_branches branches) + in + (* Then evaluate the "otherwise" branch *) + let resl_otherwise = + eval_statement config otherwise ctx_otherwise + in + (* Compose the continuations *) + let resl, cf = + comp_seqs __FILE__ __LINE__ meta + (resl_branches @ [ resl_otherwise ]) + in + let cc el = + match el with + | None -> None + | Some el -> + let el, e_otherwise = Collections.List.pop_last el in + cf_int (Some (el, e_otherwise)) + in + (resl, cc_comp cc cf) + | _ -> craise __FILE__ __LINE__ meta "Inconsistent state" + in + (* Compose *) + (ctx_resl, cc_comp cf_eval_op cf_switch) + | Match (p, stgts, otherwise) -> + (* Access the place *) + let access = Read in + let expand_prim_copy = false in + let p_v, ctx, cf_read_p = + access_rplace_reorganize_and_read config meta expand_prim_copy access p + ctx + in + (* Match on the value *) + let ctx_resl, cf_match = + (* The value may be shared: we need to ignore the shared loans + to read the value itself *) + let p_v = value_strip_shared_loans p_v in + (* Match *) + match p_v.value with + | VAdt adt -> ( + (* Evaluate the discriminant *) + let dv = Option.get adt.variant_id in + (* Find the branch, evaluate and continue *) + match List.find_opt (fun (svl, _) -> List.mem dv svl) stgts with + | None -> ( + match otherwise with + | None -> craise __FILE__ __LINE__ meta "No otherwise branch" + | Some otherwise -> eval_statement config otherwise ctx) + | Some (_, tgt) -> eval_statement config tgt ctx) + | VSymbolic sv -> + (* Expand the symbolic value - may lead to branching *) + let ctxl, cf_expand = + expand_symbolic_adt config meta sv + (Some (S.mk_mplace meta p ctx)) + ctx + in + (* Re-evaluate the switch - the value is not symbolic anymore, + which means we will go to the other branch *) + let resl = + List.map (fun ctx -> (eval_switch config meta switch) ctx) ctxl + in + (* Compose the continuations *) + let ctx_resl, cf = comp_seqs __FILE__ __LINE__ meta resl in + (ctx_resl, cc_comp cf_expand cf) + | _ -> craise __FILE__ __LINE__ meta "Inconsistent state" + in + (* Compose *) + (ctx_resl, cc_comp cf_read_p cf_match) (** Evaluate a function call (auxiliary helper for [eval_statement]) *) and eval_function_call (config : config) (meta : Meta.meta) (call : call) : - st_cm_fun = + stl_cm_fun = (* There are several cases: - this is a local function, in which case we execute its body - this is an assumed function, in which case there is a special treatment @@ -1238,24 +1229,32 @@ and eval_function_call (config : config) (meta : Meta.meta) (call : call) : | SymbolicMode -> eval_function_call_symbolic config meta call and eval_function_call_concrete (config : config) (meta : Meta.meta) - (call : call) : st_cm_fun = - fun cf ctx -> + (call : call) : stl_cm_fun = + fun ctx -> match call.func with | FnOpMove _ -> craise __FILE__ __LINE__ meta "Closures are not supported yet" | FnOpRegular func -> ( match func.func with | FunId (FRegular fid) -> - eval_transparent_function_call_concrete config meta fid call cf ctx - | FunId (FAssumed fid) -> + eval_transparent_function_call_concrete config meta fid call ctx + | FunId (FAssumed fid) -> ( (* Continue - note that we do as if the function call has been successful, * by giving {!Unit} to the continuation, because we place us in the case * where we haven't panicked. Of course, the translation needs to take the * panic case into account... *) - eval_assumed_function_call_concrete config meta fid call (cf Unit) ctx + let ctx, cc = + eval_assumed_function_call_concrete config meta fid call ctx + in + ( [ (ctx, Unit) ], + fun el -> + match el with + | Some [ e ] -> cc (Some e) + | Some _ -> internal_error __FILE__ __LINE__ meta + | _ -> None )) | TraitMethod _ -> craise __FILE__ __LINE__ meta "Unimplemented") and eval_function_call_symbolic (config : config) (meta : Meta.meta) - (call : call) : st_cm_fun = + (call : call) : stl_cm_fun = match call.func with | FnOpMove _ -> craise __FILE__ __LINE__ meta "Closures are not supported yet" | FnOpRegular func -> ( @@ -1267,7 +1266,8 @@ and eval_function_call_symbolic (config : config) (meta : Meta.meta) (** Evaluate a local (i.e., non-assumed) function call in concrete mode *) and eval_transparent_function_call_concrete (config : config) (meta : Meta.meta) - (fid : FunDeclId.id) (call : call) : st_cm_fun = + (fid : FunDeclId.id) (call : call) : stl_cm_fun = + fun ctx -> let args = call.args in let dest = call.dest in match call.func with @@ -1277,91 +1277,96 @@ and eval_transparent_function_call_concrete (config : config) (meta : Meta.meta) (* Sanity check: we don't fully handle the const generic vars environment in concrete mode yet *) sanity_check __FILE__ __LINE__ (generics.const_generics = []) meta; - fun cf ctx -> - (* Retrieve the (correctly instantiated) body *) - let def = ctx_lookup_fun_decl ctx fid in - (* We can evaluate the function call only if it is not opaque *) - let body = - match def.body with - | None -> - craise __FILE__ __LINE__ meta - ("Can't evaluate a call to an opaque function: " - ^ name_to_string ctx def.name) - | Some body -> body - in - (* TODO: we need to normalize the types if we want to correctly support traits *) - cassert __FILE__ __LINE__ (generics.trait_refs = []) body.meta - "Traits are not supported yet in concrete mode"; - (* There shouldn't be any reference to Self *) - let tr_self = UnknownTrait __FUNCTION__ in - let subst = - Subst.make_subst_from_generics def.signature.generics generics tr_self - in - let locals, body_st = Subst.fun_body_substitute_in_body subst body in - - (* Evaluate the input operands *) - sanity_check __FILE__ __LINE__ - (List.length args = body.arg_count) - body.meta; - let cc = eval_operands config body.meta args in - - (* Push a frame delimiter - we use {!comp_transmit} to transmit the result - * of the operands evaluation from above to the functions afterwards, while - * ignoring it in this function *) - let cc = comp_transmit cc push_frame in - - (* Compute the initial values for the local variables *) - (* 1. Push the return value *) - let ret_var, locals = - match locals with - | ret_ty :: locals -> (ret_ty, locals) - | _ -> craise __FILE__ __LINE__ meta "Unreachable" - in - let input_locals, locals = - Collections.List.split_at locals body.arg_count - in + (* Retrieve the (correctly instantiated) body *) + let def = ctx_lookup_fun_decl ctx fid in + (* We can evaluate the function call only if it is not opaque *) + let body = + match def.body with + | None -> + craise __FILE__ __LINE__ meta + ("Can't evaluate a call to an opaque function: " + ^ name_to_string ctx def.name) + | Some body -> body + in + (* TODO: we need to normalize the types if we want to correctly support traits *) + cassert __FILE__ __LINE__ (generics.trait_refs = []) body.meta + "Traits are not supported yet in concrete mode"; + (* There shouldn't be any reference to Self *) + let tr_self = UnknownTrait __FUNCTION__ in + let subst = + Subst.make_subst_from_generics def.signature.generics generics tr_self + in + let locals, body_st = Subst.fun_body_substitute_in_body subst body in + + (* Evaluate the input operands *) + sanity_check __FILE__ __LINE__ + (List.length args = body.arg_count) + body.meta; + let vl, ctx, cc = eval_operands config body.meta args ctx in + + (* Push a frame delimiter - we use {!comp_transmit} to transmit the result + * of the operands evaluation from above to the functions afterwards, while + * ignoring it in this function *) + let ctx = push_frame ctx in + + (* Compute the initial values for the local variables *) + (* 1. Push the return value *) + let ret_var, locals = + match locals with + | ret_ty :: locals -> (ret_ty, locals) + | _ -> craise __FILE__ __LINE__ meta "Unreachable" + in + let input_locals, locals = + Collections.List.split_at locals body.arg_count + in - let cc = - comp_transmit cc - (push_var meta ret_var (mk_bottom meta ret_var.var_ty)) - in + let ctx = push_var meta ret_var (mk_bottom meta ret_var.var_ty) ctx in - (* 2. Push the input values *) - let cf_push_inputs cf args = - let inputs = List.combine input_locals args in - (* Note that this function checks that the variables and their values - * have the same type (this is important) *) - push_vars meta inputs cf - in - let cc = comp cc cf_push_inputs in - - (* 3. Push the remaining local variables (initialized as {!Bottom}) *) - let cc = comp cc (push_uninitialized_vars meta locals) in - - (* Execute the function body *) - let cc = comp cc (eval_function_body config body_st) in - - (* Pop the stack frame and move the return value to its destination *) - let cf_finish cf res = - match res with - | Panic -> cf Panic - | Return -> - (* Pop the stack frame, retrieve the return value, move it to - * its destination and continue *) - pop_frame_assign config meta dest (cf Unit) - | Break _ | Continue _ | Unit | LoopReturn _ | EndEnterLoop _ - | EndContinue _ -> - craise __FILE__ __LINE__ meta "Unreachable" - in - let cc = comp cc cf_finish in + (* 2. Push the input values *) + let ctx = + let inputs = List.combine input_locals vl in + (* Note that this function checks that the variables and their values + * have the same type (this is important) *) + push_vars meta inputs ctx + in - (* Continue *) - cc cf ctx + (* 3. Push the remaining local variables (initialized as {!Bottom}) *) + let ctx = push_uninitialized_vars meta locals ctx in + + (* Execute the function body *) + let ctx_resl, cc = comp cc (eval_function_body config body_st ctx) in + + (* Pop the stack frame and move the return value to its destination *) + let ctx_resl_cfl = + List.map + (fun (ctx, res) -> + match res with + | Panic -> ((ctx, Panic), fun e -> e) + | Return -> + (* Pop the stack frame, retrieve the return value, move it to + its destination and continue *) + let ctx, cf = pop_frame_assign config meta dest ctx in + ((ctx, Unit), cf) + | Break _ | Continue _ | Unit | LoopReturn _ | EndEnterLoop _ + | EndContinue _ -> + craise __FILE__ __LINE__ meta "Unreachable") + ctx_resl + in + let ctx_resl, cfl = List.split ctx_resl_cfl in + let cf_pop el = + match el with + | None -> None + | Some el -> + Some + (List.map Option.get (List.map2 (fun cf e -> cf (Some e)) cfl el)) + in + (* Continue *) + (ctx_resl, cc_comp cc cf_pop) (** Evaluate a local (i.e., non-assumed) function call in symbolic mode *) and eval_transparent_function_call_symbolic (config : config) (meta : Meta.meta) - (call : call) : st_cm_fun = - fun cf ctx -> + (call : call) : stl_cm_fun = + fun ctx -> let func, generics, trait_method_generics, def, regions_hierarchy, inst_sg = eval_transparent_function_call_symbolic_inst meta call ctx in @@ -1383,7 +1388,7 @@ and eval_transparent_function_call_symbolic (config : config) (meta : Meta.meta) (* Evaluate the function call *) eval_function_call_symbolic_from_inst_sig config def.item_meta.meta func def.signature regions_hierarchy inst_sg generics trait_method_generics - call.args call.dest cf ctx + call.args call.dest ctx (** Evaluate a function call in symbolic mode by using the function signature. @@ -1401,8 +1406,8 @@ and eval_function_call_symbolic_from_inst_sig (config : config) (regions_hierarchy : region_var_groups) (inst_sg : inst_fun_sig) (generics : generic_args) (trait_method_generics : (generic_args * trait_instance_id) option) - (args : operand list) (dest : place) : st_cm_fun = - fun cf ctx -> + (args : operand list) (dest : place) : stl_cm_fun = + fun ctx -> log#ldebug (lazy ("eval_function_call_symbolic_from_inst_sig:\n- fid: " @@ -1428,70 +1433,65 @@ and eval_function_call_symbolic_from_inst_sig (config : config) let dest_place = Some (S.mk_mplace meta dest ctx) in (* Evaluate the input operands *) - let cc = eval_operands config meta args in + let args, ctx, cc = eval_operands config meta args ctx in (* Generate the abstractions and insert them in the context *) let abs_ids = List.map (fun rg -> rg.id) inst_sg.regions_hierarchy in - let cf_call cf (args : typed_value list) : m_fun = - fun ctx -> - let args_with_rtypes = List.combine args inst_sg.inputs in - - (* Check the type of the input arguments *) - cassert __FILE__ __LINE__ - (List.for_all - (fun ((arg, rty) : typed_value * rty) -> - arg.ty = Subst.erase_regions rty) - args_with_rtypes) - meta "The input arguments don't have the proper type"; - (* Check that the input arguments don't contain symbolic values that can't - * be fed to functions (i.e., symbolic values output from function return - * values and which contain borrows of borrows can't be used as function - * inputs *) - sanity_check __FILE__ __LINE__ - (List.for_all - (fun arg -> - not (value_has_ret_symbolic_value_with_borrow_under_mut ctx arg)) - args) - meta; - - (* Initialize the abstractions and push them in the context. - * First, we define the function which, given an initialized, empty - * abstraction, computes the avalues which should be inserted inside. - *) - let compute_abs_avalues (abs : abs) (ctx : eval_ctx) : - eval_ctx * typed_avalue list = - (* Project over the input values *) - let ctx, args_projs = - List.fold_left_map - (fun ctx (arg, arg_rty) -> - apply_proj_borrows_on_input_value config meta ctx abs.regions - abs.ancestors_regions arg arg_rty) - ctx args_with_rtypes - in - (* Group the input and output values *) - (ctx, List.append args_projs [ ret_av abs.regions ]) - in - (* Actually initialize and insert the abstractions *) - let call_id = fresh_fun_call_id () in - let region_can_end _ = true in - let ctx = - create_push_abstractions_from_abs_region_groups - (fun rg_id -> FunCall (call_id, rg_id)) - inst_sg.regions_hierarchy region_can_end compute_abs_avalues ctx - in + let args_with_rtypes = List.combine args inst_sg.inputs in - (* Apply the continuation *) - let expr = cf ctx in + (* Check the type of the input arguments *) + cassert __FILE__ __LINE__ + (List.for_all + (fun ((arg, rty) : typed_value * rty) -> + arg.ty = Subst.erase_regions rty) + args_with_rtypes) + meta "The input arguments don't have the proper type"; + (* Check that the input arguments don't contain symbolic values that can't + * be fed to functions (i.e., symbolic values output from function return + * values and which contain borrows of borrows can't be used as function + * inputs *) + sanity_check __FILE__ __LINE__ + (List.for_all + (fun arg -> + not (value_has_ret_symbolic_value_with_borrow_under_mut ctx arg)) + args) + meta; - (* Synthesize the symbolic AST *) - S.synthesize_regular_function_call fid call_id ctx sg regions_hierarchy - abs_ids generics trait_method_generics args args_places ret_spc dest_place - expr + (* Initialize the abstractions and push them in the context. + * First, we define the function which, given an initialized, empty + * abstraction, computes the avalues which should be inserted inside. + *) + let compute_abs_avalues (abs : abs) (ctx : eval_ctx) : + eval_ctx * typed_avalue list = + (* Project over the input values *) + let ctx, args_projs = + List.fold_left_map + (fun ctx (arg, arg_rty) -> + apply_proj_borrows_on_input_value config meta ctx abs.regions + abs.ancestors_regions arg arg_rty) + ctx args_with_rtypes + in + (* Group the input and output values *) + (ctx, List.append args_projs [ ret_av abs.regions ]) + in + (* Actually initialize and insert the abstractions *) + let call_id = fresh_fun_call_id () in + let region_can_end _ = true in + let ctx = + create_push_abstractions_from_abs_region_groups + (fun rg_id -> FunCall (call_id, rg_id)) + inst_sg.regions_hierarchy region_can_end compute_abs_avalues ctx + in + (* Synthesize the symbolic AST *) + let cc = + cc_comp cc + (S.synthesize_regular_function_call fid call_id ctx sg regions_hierarchy + abs_ids generics trait_method_generics args args_places ret_spc + dest_place) in - let cc = comp cc cf_call in (* Move the return value to its destination *) - let cc = comp cc (assign_to_place config meta ret_value dest) in + let ctx, cc = comp cc (assign_to_place config meta ret_value dest ctx) in (* End the abstractions which don't contain loans and don't have parent * abstractions. @@ -1499,8 +1499,7 @@ and eval_function_call_symbolic_from_inst_sig (config : config) * retry (because then we might end their children abstractions) *) let abs_ids = ref abs_ids in - let rec end_abs_with_no_loans cf : m_fun = - fun ctx -> + let rec end_abs_with_no_loans ctx = (* Find the abstractions which don't contain loans *) let no_loans_abs, with_loans_abs = List.partition @@ -1521,35 +1520,36 @@ and eval_function_call_symbolic_from_inst_sig (config : config) abs_ids := with_loans_abs; (* End the abstractions which can be ended *) let no_loans_abs = AbstractionId.Set.of_list no_loans_abs in - let cc = InterpreterBorrows.end_abstractions config meta no_loans_abs in + let ctx, cc = + InterpreterBorrows.end_abstractions config meta no_loans_abs ctx + in (* Recursive call *) - let cc = comp cc end_abs_with_no_loans in - (* Continue *) - cc cf ctx) + comp cc (end_abs_with_no_loans ctx)) else (* No abstractions to end: continue *) - cf ctx + (ctx, fun e -> e) in (* Try to end the abstractions with no loans if: * - the option is enabled * - the function returns unit * (see the documentation of {!config} for more information) *) - let cc = - if Config.return_unit_end_abs_with_no_loans && ty_is_unit inst_sg.output - then comp cc end_abs_with_no_loans - else cc + let ctx, cc = + comp cc + (if Config.return_unit_end_abs_with_no_loans && ty_is_unit inst_sg.output + then end_abs_with_no_loans ctx + else (ctx, fun e -> e)) in (* Continue - note that we do as if the function call has been successful, * by giving {!Unit} to the continuation, because we place us in the case * where we haven't panicked. Of course, the translation needs to take the * panic case into account... *) - cc (cf Unit) ctx + ([ (ctx, Unit) ], cc_singleton __FILE__ __LINE__ meta cc) (** Evaluate a non-local function call in symbolic mode *) and eval_assumed_function_call_symbolic (config : config) (meta : Meta.meta) - (fid : assumed_fun_id) (call : call) (func : fn_ptr) : st_cm_fun = - fun cf ctx -> + (fid : assumed_fun_id) (call : call) (func : fn_ptr) : stl_cm_fun = + fun ctx -> let generics = func.generics in let args = call.args in let dest = call.dest in @@ -1570,7 +1570,8 @@ and eval_assumed_function_call_symbolic (config : config) (meta : Meta.meta) | BoxFree -> (* Degenerate case: box_free - note that this is not really a function * call: no need to call a "synthesize_..." function *) - eval_box_free config meta generics args dest (cf Unit) ctx + let ctx, cc = eval_box_free config meta generics args dest ctx in + ([ (ctx, Unit) ], cc_singleton __FILE__ __LINE__ meta cc) | _ -> (* "Normal" case: not box_free *) (* In symbolic mode, the behaviour of a function call is completely defined @@ -1598,25 +1599,34 @@ and eval_assumed_function_call_symbolic (config : config) (meta : Meta.meta) (* Evaluate the function call *) eval_function_call_symbolic_from_inst_sig config meta (FunId (FAssumed fid)) sg regions_hierarchy inst_sig generics None args - dest cf ctx + dest ctx (** Evaluate a statement seen as a function body *) -and eval_function_body (config : config) (body : statement) : st_cm_fun = - fun cf ctx -> +and eval_function_body (config : config) (body : statement) : stl_cm_fun = + fun ctx -> log#ldebug (lazy "eval_function_body:"); - let cc = eval_statement config body in - let cf_finish cf res = - log#ldebug (lazy "eval_function_body: cf_finish"); - (* Note that we *don't* check the result ({!Panic}, {!Return}, etc.): we - * delegate the check to the caller. *) - (* Expand the symbolic values if necessary - we need to do that before - * checking the invariants *) - let cc = greedy_expand_symbolic_values config body.meta in - (* Sanity check *) - let cc = comp_check_ctx cc (Invariants.check_invariants body.meta) in - (* Check if right meta *) - (* Continue *) - cc (cf res) + let ctx_resl, cf_body = eval_statement config body ctx in + let ctx_res_cfl = + List.map + (fun (ctx, res) -> + log#ldebug (lazy "eval_function_body: cf_finish"); + (* Note that we *don't* check the result ({!Panic}, {!Return}, etc.): we + * delegate the check to the caller. *) + (* Expand the symbolic values if necessary - we need to do that before + * checking the invariants *) + let ctx, cf = greedy_expand_symbolic_values config body.meta ctx in + (* Sanity check *) + Invariants.check_invariants body.meta ctx; + (* Continue *) + ((ctx, res), cf)) + ctx_resl + in + let ctx_resl, cfl = List.split ctx_res_cfl in + let cf_end el = + match el with + | None -> None + | Some el -> + Some (List.map Option.get (List.map2 (fun cf e -> cf (Some e)) cfl el)) in (* Compose and continue *) - comp cc cf_finish cf ctx + (ctx_resl, cc_comp cf_body cf_end) -- cgit v1.2.3