From 26c25bf375742cf4d5a0ab160b9646e90c067f18 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Fri, 18 Aug 2023 10:27:55 +0200 Subject: Update following the introduction of ConstantExpr --- compiler/InterpreterStatements.ml | 198 ++++++++++++++++++++------------------ 1 file changed, 103 insertions(+), 95 deletions(-) (limited to 'compiler/InterpreterStatements.ml') diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml index 045c4484..6d520059 100644 --- a/compiler/InterpreterStatements.ml +++ b/compiler/InterpreterStatements.ml @@ -421,16 +421,16 @@ let pop_frame_assign (config : C.config) (dest : E.place) : cm_fun = (** Auxiliary function - see {!eval_non_local_function_call} *) let eval_replace_concrete (_config : C.config) (_region_params : T.erased_region list) (_type_params : T.ety list) - (_cg_params : T.const_generic list) : cm_fun = + (_cg_args : T.const_generic list) : cm_fun = fun _cf _ctx -> raise Unimplemented (** Auxiliary function - see {!eval_non_local_function_call} *) let eval_box_new_concrete (config : C.config) (region_params : T.erased_region list) (type_params : T.ety list) - (cg_params : T.const_generic list) : cm_fun = + (cg_args : T.const_generic list) : cm_fun = fun cf ctx -> (* Check and retrieve the arguments *) - match (region_params, type_params, cg_params, ctx.env) with + match (region_params, type_params, cg_args, ctx.env) with | ( [], [ boxed_ty ], [], @@ -470,10 +470,10 @@ let eval_box_new_concrete (config : C.config) and [std::DerefMut::deref_mut] - see {!eval_non_local_function_call} *) let eval_box_deref_mut_or_shared_concrete (config : C.config) (region_params : T.erased_region list) (type_params : T.ety list) - (cg_params : T.const_generic list) (is_mut : bool) : cm_fun = + (cg_args : T.const_generic list) (is_mut : bool) : cm_fun = fun cf ctx -> (* Check the arguments *) - match (region_params, type_params, cg_params, ctx.env) with + match (region_params, type_params, cg_args, ctx.env) with | ( [], [ boxed_ty ], [], @@ -517,18 +517,18 @@ let eval_box_deref_mut_or_shared_concrete (config : C.config) (** Auxiliary function - see {!eval_non_local_function_call} *) let eval_box_deref_concrete (config : C.config) (region_params : T.erased_region list) (type_params : T.ety list) - (cg_params : T.const_generic list) : cm_fun = + (cg_args : T.const_generic list) : cm_fun = let is_mut = false in - eval_box_deref_mut_or_shared_concrete config region_params type_params - cg_params is_mut + eval_box_deref_mut_or_shared_concrete config region_params type_params cg_args + is_mut (** Auxiliary function - see {!eval_non_local_function_call} *) let eval_box_deref_mut_concrete (config : C.config) (region_params : T.erased_region list) (type_params : T.ety list) - (cg_params : T.const_generic list) : cm_fun = + (cg_args : T.const_generic list) : cm_fun = let is_mut = true in - eval_box_deref_mut_or_shared_concrete config region_params type_params - cg_params is_mut + eval_box_deref_mut_or_shared_concrete config region_params type_params cg_args + is_mut (** Auxiliary function - see {!eval_non_local_function_call}. @@ -550,10 +550,10 @@ let eval_box_deref_mut_concrete (config : C.config) the destination (by setting it to [()]). *) let eval_box_free (config : C.config) (region_params : T.erased_region list) - (type_params : T.ety list) (cg_params : T.const_generic list) + (type_params : T.ety list) (cg_args : T.const_generic list) (args : E.operand list) (dest : E.place) : cm_fun = fun cf ctx -> - match (region_params, type_params, cg_params, args) with + match (region_params, type_params, cg_args, args) with | [], [ boxed_ty ], [], [ E.Move input_box_place ] -> (* Required type checking *) let input_box = InterpreterPaths.read_place Write input_box_place ctx in @@ -573,14 +573,17 @@ let eval_box_free (config : C.config) (region_params : T.erased_region list) (** Auxiliary function - see {!eval_non_local_function_call} *) let eval_vec_function_concrete (_config : C.config) (_fid : A.assumed_fun_id) (_region_params : T.erased_region list) (_type_params : T.ety list) - (_cg_params : T.const_generic list) : cm_fun = + (_cg_args : T.const_generic list) : cm_fun = fun _cf _ctx -> raise Unimplemented (** Evaluate a non-local function call in concrete mode *) let eval_non_local_function_call_concrete (config : C.config) (fid : A.assumed_fun_id) (region_params : T.erased_region list) - (type_params : T.ety list) (cg_params : T.const_generic list) + (type_params : T.ety list) (cg_args : T.const_generic list) (args : E.operand list) (dest : E.place) : cm_fun = + (* Sanity check: we don't fully handle the const generic vars environment + in concrete mode yet *) + assert (cg_args = []); (* There are two cases (and this is extremely annoying): - the function is not box_free - the function is box_free @@ -589,7 +592,7 @@ let eval_non_local_function_call_concrete (config : C.config) match fid with | A.BoxFree -> (* Degenerate case: box_free *) - eval_box_free config region_params type_params cg_params args dest + eval_box_free config region_params type_params cg_args args dest | _ -> (* "Normal" case: not box_free *) (* Evaluate the operands *) @@ -612,7 +615,7 @@ let eval_non_local_function_call_concrete (config : C.config) let ret_vid = E.VarId.zero in let ret_ty = get_non_local_function_return_type fid region_params type_params - cg_params + cg_args in let ret_var = mk_var ret_vid (Some "@return") ret_ty in let cc = comp cc (push_uninitialized_var ret_var) in @@ -631,19 +634,19 @@ let eval_non_local_function_call_concrete (config : C.config) let cf_eval_body : cm_fun = match fid with | A.Replace -> - eval_replace_concrete config region_params type_params cg_params + eval_replace_concrete config region_params type_params cg_args | BoxNew -> - eval_box_new_concrete config region_params type_params cg_params + eval_box_new_concrete config region_params type_params cg_args | BoxDeref -> - eval_box_deref_concrete config region_params type_params cg_params + eval_box_deref_concrete config region_params type_params cg_args | BoxDerefMut -> eval_box_deref_mut_concrete config region_params type_params - cg_params + cg_args | BoxFree -> (* Should have been treated above *) raise (Failure "Unreachable") | VecNew | VecPush | VecInsert | VecLen | VecIndex | VecIndexMut -> eval_vec_function_concrete config fid region_params type_params - cg_params + cg_args | ArrayIndexShared | ArrayIndexMut | ArrayToSliceShared | ArrayToSliceMut | ArraySubsliceShared | ArraySubsliceMut | SliceIndexShared | SliceIndexMut | SliceSubsliceShared @@ -663,7 +666,7 @@ let eval_non_local_function_call_concrete (config : C.config) comp cf_eval_ops cf_eval_call let instantiate_fun_sig (type_params : T.ety list) - (cg_params : T.const_generic list) (sg : A.fun_sig) : A.inst_fun_sig = + (cg_args : T.const_generic list) (sg : A.fun_sig) : A.inst_fun_sig = (* Generate fresh abstraction ids and create a substitution from region * group ids to abstraction ids *) let rg_abs_ids_bindings = @@ -694,7 +697,7 @@ let instantiate_fun_sig (type_params : T.ety list) let rtype_params = List.map ety_no_regions_to_rty type_params in let tsubst = Subst.make_type_subst_from_vars sg.type_params rtype_params in let cgsubst = - Subst.make_const_generic_subst_from_vars sg.const_generic_params cg_params + Subst.make_const_generic_subst_from_vars sg.const_generic_params cg_args in (* Substitute the signature *) let inst_sig = Subst.substitute_signature asubst rsubst tsubst cgsubst sg in @@ -1054,81 +1057,86 @@ and eval_local_function_call_concrete (config : C.config) (fid : A.FunDeclId.id) (_region_args : T.erased_region list) (type_args : T.ety list) (cg_args : T.const_generic list) (args : E.operand list) (dest : E.place) : st_cm_fun = - fun cf ctx -> - (* Retrieve the (correctly instantiated) body *) - let def = C.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 -> - raise - (Failure - ("Can't evaluate a call to an opaque function: " - ^ Print.name_to_string def.name)) - | Some body -> body - in - let tsubst = - Subst.make_type_subst_from_vars def.A.signature.type_params type_args - in - let cgsubst = - Subst.make_const_generic_subst_from_vars - def.A.signature.const_generic_params cg_args - in - let locals, body_st = Subst.fun_body_substitute_in_body tsubst cgsubst body in - - (* Evaluate the input operands *) - assert (List.length args = body.A.arg_count); - let cc = eval_operands config 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) - | _ -> raise (Failure "Unreachable") - in - let input_locals, locals = - Collections.List.split_at locals body.A.arg_count - in - - let cc = comp_transmit cc (push_var ret_var (mk_bottom ret_var.var_ty)) 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 inputs cf - in - let cc = comp cc cf_push_inputs in + (* Sanity check: we don't fully handle the const generic vars environment + in concrete mode yet *) + assert (cg_args = []); + fun cf ctx -> + (* Retrieve the (correctly instantiated) body *) + let def = C.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 -> + raise + (Failure + ("Can't evaluate a call to an opaque function: " + ^ Print.name_to_string def.name)) + | Some body -> body + in + let tsubst = + Subst.make_type_subst_from_vars def.A.signature.type_params type_args + in + let cgsubst = + Subst.make_const_generic_subst_from_vars + def.A.signature.const_generic_params cg_args + in + let locals, body_st = + Subst.fun_body_substitute_in_body tsubst cgsubst body + in - (* 3. Push the remaining local variables (initialized as {!Bottom}) *) - let cc = comp cc (push_uninitialized_vars locals) in + (* Evaluate the input operands *) + assert (List.length args = body.A.arg_count); + let cc = eval_operands config 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) + | _ -> raise (Failure "Unreachable") + in + let input_locals, locals = + Collections.List.split_at locals body.A.arg_count + in - (* Execute the function body *) - let cc = comp cc (eval_function_body config body_st) in + let cc = comp_transmit cc (push_var ret_var (mk_bottom ret_var.var_ty)) 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 dest (cf Unit) - | Break _ | Continue _ | Unit | LoopReturn _ | EndEnterLoop _ - | EndContinue _ -> - raise (Failure "Unreachable") - in - let cc = comp cc cf_finish 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 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 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 dest (cf Unit) + | Break _ | Continue _ | Unit | LoopReturn _ | EndEnterLoop _ + | EndContinue _ -> + raise (Failure "Unreachable") + in + let cc = comp cc cf_finish in - (* Continue *) - cc cf ctx + (* Continue *) + cc cf ctx (** Evaluate a local (i.e., non-assumed) function call in symbolic mode *) and eval_local_function_call_symbolic (config : C.config) (fid : A.FunDeclId.id) -- cgit v1.2.3 From 6f22190cba92a44b6c74bfcce8f5ed142a68e195 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Thu, 31 Aug 2023 12:47:43 +0200 Subject: Start adding support for traits --- compiler/InterpreterStatements.ml | 305 +++++++++++++++++++------------------- 1 file changed, 154 insertions(+), 151 deletions(-) (limited to 'compiler/InterpreterStatements.ml') diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml index 6d520059..d38f8b95 100644 --- a/compiler/InterpreterStatements.ml +++ b/compiler/InterpreterStatements.ml @@ -17,6 +17,7 @@ open InterpreterProjectors open InterpreterExpansion open InterpreterPaths open InterpreterExpressions +module PCtx = Print.EvalCtxLlbcAst (** The local logger *) let log = L.statements_log @@ -232,9 +233,8 @@ let set_discriminant (config : C.config) (p : E.place) let update_value cf (v : V.typed_value) : m_fun = fun ctx -> match (v.V.ty, v.V.value) with - | ( T.Adt - (((T.AdtId _ | T.Assumed T.Option) as type_id), regions, types, cgs), - V.Adt av ) -> ( + | T.Adt (((T.AdtId _ | T.Assumed T.Option) as type_id), generics), V.Adt av + -> ( (* There are two situations: - either the discriminant is already the proper one (in which case we don't do anything) @@ -251,28 +251,26 @@ let set_discriminant (config : C.config) (p : E.place) let bottom_v = match type_id with | T.AdtId def_id -> - compute_expanded_bottom_adt_value - ctx.type_context.type_decls def_id (Some variant_id) - regions types cgs + compute_expanded_bottom_adt_value ctx def_id + (Some variant_id) generics | T.Assumed T.Option -> - assert (regions = []); + assert (generics.regions = []); compute_expanded_bottom_option_value variant_id - (Collections.List.to_cons_nil types) + (Collections.List.to_cons_nil generics.types) | _ -> raise (Failure "Unreachable") in assign_to_place config bottom_v p (cf Unit) ctx) - | ( T.Adt - (((T.AdtId _ | T.Assumed T.Option) as type_id), regions, types, cgs), - V.Bottom ) -> + | T.Adt (((T.AdtId _ | T.Assumed T.Option) as type_id), generics), V.Bottom + -> let bottom_v = match type_id with | T.AdtId def_id -> - compute_expanded_bottom_adt_value ctx.type_context.type_decls - def_id (Some variant_id) regions types cgs + compute_expanded_bottom_adt_value ctx def_id (Some variant_id) + generics | T.Assumed T.Option -> - assert (regions = []); + assert (generics.regions = []); compute_expanded_bottom_option_value variant_id - (Collections.List.to_cons_nil types) + (Collections.List.to_cons_nil generics.types) | _ -> raise (Failure "Unreachable") in assign_to_place config bottom_v p (cf Unit) ctx @@ -301,24 +299,34 @@ let ctx_push_frame (ctx : C.eval_ctx) : C.eval_ctx = let push_frame : cm_fun = fun cf ctx -> cf (ctx_push_frame ctx) (** Small helper: compute the type of the return value for a specific - instantiation of a non-local function. + instantiation of an assumed function. *) -let get_non_local_function_return_type (fid : A.assumed_fun_id) - (region_params : T.erased_region list) (type_params : T.ety list) - (const_generic_params : T.const_generic list) : T.ety = +let get_assumed_function_return_type (ctx : C.eval_ctx) (fid : A.assumed_fun_id) + (generics : T.egeneric_args) : T.ety = + assert (generics.trait_refs = []); (* [Box::free] has a special treatment *) - match (fid, region_params, type_params, const_generic_params) with - | A.BoxFree, [], [ _ ], [] -> mk_unit_ty + match fid with + | A.BoxFree -> + assert (generics.regions = []); + assert (List.length generics.types = 1); + assert (generics.const_generics = []); + mk_unit_ty | _ -> (* Retrieve the function's signature *) let sg = Assumed.get_assumed_sig fid in (* Instantiate the return type *) - let tsubst = Subst.make_type_subst_from_vars sg.type_params type_params in - let cgsubst = - Subst.make_const_generic_subst_from_vars sg.const_generic_params - const_generic_params + (* There shouldn't be any reference to Self *) + let tr_self : T.erased_region T.trait_instance_id = + T.UnknownTrait __FUNCTION__ + in + let { Subst.r_subst = _; ty_subst; cg_subst; tr_subst; tr_self } = + Subst.make_esubst_from_generics sg.generics generics tr_self in - Subst.erase_regions_substitute_types tsubst cgsubst sg.output + let ty = + Subst.erase_regions_substitute_types ty_subst cg_subst tr_subst tr_self + sg.output + in + Assoc.ctx_normalize_type ctx ty let move_return_value (config : C.config) (pop_return_value : bool) (cf : V.typed_value option -> m_fun) : m_fun = @@ -418,19 +426,19 @@ let pop_frame_assign (config : C.config) (dest : E.place) : cm_fun = in comp cf_pop cf_assign -(** Auxiliary function - see {!eval_non_local_function_call} *) -let eval_replace_concrete (_config : C.config) - (_region_params : T.erased_region list) (_type_params : T.ety list) - (_cg_args : T.const_generic list) : cm_fun = +(** Auxiliary function - see {!eval_assumed_function_call} *) +let eval_replace_concrete (_config : C.config) (_generics : T.egeneric_args) : + cm_fun = fun _cf _ctx -> raise Unimplemented -(** Auxiliary function - see {!eval_non_local_function_call} *) -let eval_box_new_concrete (config : C.config) - (region_params : T.erased_region list) (type_params : T.ety list) - (cg_args : T.const_generic list) : cm_fun = +(** Auxiliary function - see {!eval_assumed_function_call} *) +let eval_box_new_concrete (config : C.config) (generics : T.egeneric_args) : + cm_fun = fun cf ctx -> (* Check and retrieve the arguments *) - match (region_params, type_params, cg_args, ctx.env) with + match + (generics.regions, generics.types, generics.const_generics, ctx.env) + with | ( [], [ boxed_ty ], [], @@ -448,7 +456,8 @@ let eval_box_new_concrete (config : C.config) (* Create the new box *) let cf_create cf (moved_input_value : V.typed_value) : m_fun = (* Create the box value *) - let box_ty = T.Adt (T.Assumed T.Box, [], [ boxed_ty ], []) in + let generics = TypesUtils.mk_generic_args_from_types [ boxed_ty ] in + let box_ty = T.Adt (T.Assumed T.Box, generics) in let box_v = V.Adt { variant_id = None; field_values = [ moved_input_value ] } in @@ -467,13 +476,14 @@ let eval_box_new_concrete (config : C.config) | _ -> raise (Failure "Inconsistent state") (** Auxiliary function which factorizes code to evaluate [std::Deref::deref] - and [std::DerefMut::deref_mut] - see {!eval_non_local_function_call} *) + and [std::DerefMut::deref_mut] - see {!eval_assumed_function_call} *) let eval_box_deref_mut_or_shared_concrete (config : C.config) - (region_params : T.erased_region list) (type_params : T.ety list) - (cg_args : T.const_generic list) (is_mut : bool) : cm_fun = + (generics : T.egeneric_args) (is_mut : bool) : cm_fun = fun cf ctx -> (* Check the arguments *) - match (region_params, type_params, cg_args, ctx.env) with + match + (generics.regions, generics.types, generics.const_generics, ctx.env) + with | ( [], [ boxed_ty ], [], @@ -495,7 +505,7 @@ let eval_box_deref_mut_or_shared_concrete (config : C.config) { E.var_id = input_var.C.index; projection = [ E.Deref; E.DerefBox ] } in let borrow_kind = if is_mut then E.Mut else E.Shared in - let rv = E.Ref (p, borrow_kind) in + let rv = E.RvRef (p, borrow_kind) in let cf_borrow = eval_rvalue_not_global config rv in (* Move the borrow to its destination *) @@ -514,23 +524,19 @@ let eval_box_deref_mut_or_shared_concrete (config : C.config) comp cf_borrow cf_move cf ctx | _ -> raise (Failure "Inconsistent state") -(** Auxiliary function - see {!eval_non_local_function_call} *) -let eval_box_deref_concrete (config : C.config) - (region_params : T.erased_region list) (type_params : T.ety list) - (cg_args : T.const_generic list) : cm_fun = +(** Auxiliary function - see {!eval_assumed_function_call} *) +let eval_box_deref_concrete (config : C.config) (generics : T.egeneric_args) : + cm_fun = let is_mut = false in - eval_box_deref_mut_or_shared_concrete config region_params type_params cg_args - is_mut + eval_box_deref_mut_or_shared_concrete config generics is_mut -(** Auxiliary function - see {!eval_non_local_function_call} *) -let eval_box_deref_mut_concrete (config : C.config) - (region_params : T.erased_region list) (type_params : T.ety list) - (cg_args : T.const_generic list) : cm_fun = +(** Auxiliary function - see {!eval_assumed_function_call} *) +let eval_box_deref_mut_concrete (config : C.config) (generics : T.egeneric_args) + : cm_fun = let is_mut = true in - eval_box_deref_mut_or_shared_concrete config region_params type_params cg_args - is_mut + eval_box_deref_mut_or_shared_concrete config generics is_mut -(** Auxiliary function - see {!eval_non_local_function_call}. +(** Auxiliary function - see {!eval_assumed_function_call}. [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, @@ -549,11 +555,10 @@ let eval_box_deref_mut_concrete (config : C.config) It thus updates the box value (by calling {!drop_value}) and updates the destination (by setting it to [()]). *) -let eval_box_free (config : C.config) (region_params : T.erased_region list) - (type_params : T.ety list) (cg_args : T.const_generic list) +let eval_box_free (config : C.config) (generics : T.egeneric_args) (args : E.operand list) (dest : E.place) : cm_fun = fun cf ctx -> - match (region_params, type_params, cg_args, args) with + match (generics.regions, generics.types, generics.const_generics, args) with | [], [ boxed_ty ], [], [ E.Move input_box_place ] -> (* Required type checking *) let input_box = InterpreterPaths.read_place Write input_box_place ctx in @@ -570,20 +575,18 @@ let eval_box_free (config : C.config) (region_params : T.erased_region list) cc cf ctx | _ -> raise (Failure "Inconsistent state") -(** Auxiliary function - see {!eval_non_local_function_call} *) +(** Auxiliary function - see {!eval_assumed_function_call} *) let eval_vec_function_concrete (_config : C.config) (_fid : A.assumed_fun_id) - (_region_params : T.erased_region list) (_type_params : T.ety list) - (_cg_args : T.const_generic list) : cm_fun = + (_generics : T.egeneric_args) : cm_fun = fun _cf _ctx -> raise Unimplemented (** Evaluate a non-local function call in concrete mode *) -let eval_non_local_function_call_concrete (config : C.config) - (fid : A.assumed_fun_id) (region_params : T.erased_region list) - (type_params : T.ety list) (cg_args : T.const_generic list) +let eval_assumed_function_call_concrete (config : C.config) + (fid : A.assumed_fun_id) (generics : T.egeneric_args) (args : E.operand list) (dest : E.place) : cm_fun = (* Sanity check: we don't fully handle the const generic vars environment in concrete mode yet *) - assert (cg_args = []); + assert (generics.const_generics = []); (* There are two cases (and this is extremely annoying): - the function is not box_free - the function is box_free @@ -592,7 +595,7 @@ let eval_non_local_function_call_concrete (config : C.config) match fid with | A.BoxFree -> (* Degenerate case: box_free *) - eval_box_free config region_params type_params cg_args args dest + eval_box_free config generics args dest | _ -> (* "Normal" case: not box_free *) (* Evaluate the operands *) @@ -607,16 +610,14 @@ let eval_non_local_function_call_concrete (config : C.config) * but it made it less clear where the computed values came from, * so we reversed the modifications. *) let cf_eval_call cf (args_vl : V.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 = E.VarId.zero in - let ret_ty = - get_non_local_function_return_type fid region_params type_params - cg_args - in + let ret_ty = get_assumed_function_return_type ctx fid generics in let ret_var = mk_var ret_vid (Some "@return") ret_ty in let cc = comp cc (push_uninitialized_var ret_var) in @@ -633,20 +634,14 @@ let eval_non_local_function_call_concrete (config : C.config) * access to a body. *) let cf_eval_body : cm_fun = match fid with - | A.Replace -> - eval_replace_concrete config region_params type_params cg_args - | BoxNew -> - eval_box_new_concrete config region_params type_params cg_args - | BoxDeref -> - eval_box_deref_concrete config region_params type_params cg_args - | BoxDerefMut -> - eval_box_deref_mut_concrete config region_params type_params - cg_args + | A.Replace -> eval_replace_concrete config generics + | BoxNew -> eval_box_new_concrete config generics + | BoxDeref -> eval_box_deref_concrete config generics + | BoxDerefMut -> eval_box_deref_mut_concrete config generics | BoxFree -> (* Should have been treated above *) raise (Failure "Unreachable") | VecNew | VecPush | VecInsert | VecLen | VecIndex | VecIndexMut -> - eval_vec_function_concrete config fid region_params type_params - cg_args + eval_vec_function_concrete config fid generics | ArrayIndexShared | ArrayIndexMut | ArrayToSliceShared | ArrayToSliceMut | ArraySubsliceShared | ArraySubsliceMut | SliceIndexShared | SliceIndexMut | SliceSubsliceShared @@ -660,13 +655,13 @@ let eval_non_local_function_call_concrete (config : C.config) let cc = comp cc (pop_frame_assign config dest) in (* Continue *) - cc cf + cc cf ctx in (* Compose and apply *) comp cf_eval_ops cf_eval_call -let instantiate_fun_sig (type_params : T.ety list) - (cg_args : T.const_generic list) (sg : A.fun_sig) : A.inst_fun_sig = +let instantiate_fun_sig (ctx : C.eval_ctx) (generics : T.egeneric_args) + (tr_self : T.rtrait_instance_id) (sg : A.fun_sig) : A.inst_fun_sig = (* Generate fresh abstraction ids and create a substitution from region * group ids to abstraction ids *) let rg_abs_ids_bindings = @@ -685,7 +680,7 @@ let instantiate_fun_sig (type_params : T.ety list) T.RegionGroupId.Map.find rg_id asubst_map in (* Generate fresh regions and their substitutions *) - let _, rsubst, _ = Subst.fresh_regions_with_substs sg.region_params in + let _, rsubst, _ = Subst.fresh_regions_with_substs sg.generics.regions in (* Generate the type substitution * Note that we need the substitution to map the type variables to * {!rty} types (not {!ety}). In order to do that, we convert the @@ -694,13 +689,28 @@ let instantiate_fun_sig (type_params : T.ety list) * This is a current limitation of the analysis: there is still some * work to do to properly handle full type parametrization. * *) - let rtype_params = List.map ety_no_regions_to_rty type_params in - let tsubst = Subst.make_type_subst_from_vars sg.type_params rtype_params in + let rtype_params = List.map ety_no_regions_to_rty generics.types in + let tsubst = Subst.make_type_subst_from_vars sg.generics.types rtype_params in let cgsubst = - Subst.make_const_generic_subst_from_vars sg.const_generic_params cg_args + Subst.make_const_generic_subst_from_vars sg.generics.const_generics + generics.const_generics + in + (* TODO: something annoying with the trait ref subst: we need to use region + types, but the arguments use erased regions. For now we use the fact + that no regions should appear inside. In the future: we should merge + ety and rty. *) + let trait_refs = + List.map TypesUtils.etrait_ref_no_regions_to_gr_trait_ref + generics.trait_refs + in + let tr_subst = + Subst.make_trait_subst_from_clauses sg.generics.trait_clauses trait_refs in (* Substitute the signature *) - let inst_sig = Subst.substitute_signature asubst rsubst tsubst cgsubst sg in + let inst_sig = + Assoc.ctx_subst_norm_signature ctx asubst rsubst tsubst cgsubst tr_subst + tr_self sg + in (* Return *) inst_sig @@ -839,7 +849,7 @@ let rec eval_statement (config : C.config) (st : A.statement) : st_cm_fun = match rvalue with | E.Global _ -> raise (Failure "Unreachable") | E.Use _ - | E.Ref (_, (E.Shared | E.Mut | E.TwoPhaseMut | E.Shallow)) + | E.RvRef (_, (E.Shared | E.Mut | E.TwoPhaseMut | E.Shallow)) | E.UnaryOp _ | E.BinaryOp _ | E.Discriminant _ | E.Aggregate _ -> let rp = rvalue_get_place rvalue in @@ -896,7 +906,9 @@ and eval_global (config : C.config) (dest : E.place) (gid : LA.GlobalDeclId.id) match config.mode with | ConcreteMode -> (* Treat the evaluation of the global as a call to the global body (without arguments) *) - (eval_local_function_call_concrete config global.body_id [] [] [] [] dest) + let generics = TypesUtils.mk_empty_generic_args in + (eval_transparent_function_call_concrete config global.body_id generics [] + dest) cf ctx | SymbolicMode -> (* Generate a fresh symbolic value. In the translation, this fresh symbolic value will be @@ -1040,26 +1052,26 @@ and eval_switch (config : C.config) (switch : A.switch) : st_cm_fun = (** Evaluate a function call (auxiliary helper for [eval_statement]) *) and eval_function_call (config : C.config) (call : A.call) : st_cm_fun = - (* There are two cases: + (* There are several cases: - this is a local function, in which case we execute its body - - this is a non-local function, in which case there is a special treatment + - this is an assumed function, in which case there is a special treatment + - this is a trait method *) match call.func with - | A.Regular fid -> - eval_local_function_call config fid call.region_args call.type_args - call.const_generic_args call.args call.dest - | A.Assumed fid -> - eval_non_local_function_call config fid call.region_args call.type_args - call.const_generic_args call.args call.dest + | A.FunId (A.Regular fid) -> + eval_transparent_function_call config fid call.generics call.args + call.dest + | A.FunId (A.Assumed fid) -> + eval_assumed_function_call config fid call.generics call.args call.dest + | A.TraitMethod _ -> raise (Failure "Unimplemented") (** Evaluate a local (i.e., non-assumed) function call in concrete mode *) -and eval_local_function_call_concrete (config : C.config) (fid : A.FunDeclId.id) - (_region_args : T.erased_region list) (type_args : T.ety list) - (cg_args : T.const_generic list) (args : E.operand list) (dest : E.place) : - st_cm_fun = +and eval_transparent_function_call_concrete (config : C.config) + (fid : A.FunDeclId.id) (generics : T.egeneric_args) (args : E.operand list) + (dest : E.place) : st_cm_fun = (* Sanity check: we don't fully handle the const generic vars environment in concrete mode yet *) - assert (cg_args = []); + assert (generics.const_generics = []); fun cf ctx -> (* Retrieve the (correctly instantiated) body *) let def = C.ctx_lookup_fun_decl ctx fid in @@ -1073,16 +1085,14 @@ and eval_local_function_call_concrete (config : C.config) (fid : A.FunDeclId.id) ^ Print.name_to_string def.name)) | Some body -> body in - let tsubst = - Subst.make_type_subst_from_vars def.A.signature.type_params type_args - in - let cgsubst = - Subst.make_const_generic_subst_from_vars - def.A.signature.const_generic_params cg_args - in - let locals, body_st = - Subst.fun_body_substitute_in_body tsubst cgsubst body + (* TODO: we need to normalize the types if we want to correctly support traits *) + assert (ctx.trait_clauses = [] && generics.trait_refs = []); + (* There shouldn't be any reference to Self *) + let tr_self = T.UnknownTrait __FUNCTION__ in + let subst = + Subst.make_esubst_from_generics def.A.signature.generics generics tr_self in + let locals, body_st = Subst.fun_body_substitute_in_body subst body in (* Evaluate the input operands *) assert (List.length args = body.A.arg_count); @@ -1139,22 +1149,23 @@ and eval_local_function_call_concrete (config : C.config) (fid : A.FunDeclId.id) cc cf ctx (** Evaluate a local (i.e., non-assumed) function call in symbolic mode *) -and eval_local_function_call_symbolic (config : C.config) (fid : A.FunDeclId.id) - (region_args : T.erased_region list) (type_args : T.ety list) - (cg_args : T.const_generic list) (args : E.operand list) (dest : E.place) : - st_cm_fun = +and eval_transparent_function_call_symbolic (config : C.config) + (fid : A.FunDeclId.id) (generics : T.egeneric_args) (args : E.operand list) + (dest : E.place) : st_cm_fun = fun cf ctx -> (* Retrieve the (correctly instantiated) signature *) let def = C.ctx_lookup_fun_decl ctx fid in let sg = def.A.signature in (* Instantiate the signature and introduce fresh abstraction and region ids * while doing so *) - let inst_sg = instantiate_fun_sig type_args cg_args sg in + (* There shouldn't be any reference to Self *) + let tr_self = T.UnknownTrait __FUNCTION__ in + let inst_sg = instantiate_fun_sig ctx generics tr_self sg in (* Sanity check *) assert (List.length args = List.length def.A.signature.inputs); (* Evaluate the function call *) eval_function_call_symbolic_from_inst_sig config (A.Regular fid) inst_sg - region_args type_args cg_args args dest cf ctx + generics args dest cf ctx (** Evaluate a function call in symbolic mode by using the function signature. @@ -1162,10 +1173,8 @@ and eval_local_function_call_symbolic (config : C.config) (fid : A.FunDeclId.id) calls in symbolic mode: only their signatures matter. *) and eval_function_call_symbolic_from_inst_sig (config : C.config) - (fid : A.fun_id) (inst_sg : A.inst_fun_sig) - (_region_args : T.erased_region list) (type_args : T.ety list) - (cg_args : T.const_generic list) (args : E.operand list) (dest : E.place) : - st_cm_fun = + (fid : A.fun_id) (inst_sg : A.inst_fun_sig) (generics : T.egeneric_args) + (args : E.operand list) (dest : E.place) : st_cm_fun = fun cf ctx -> (* Generate a fresh symbolic value for the return value *) let ret_sv_ty = inst_sg.A.output in @@ -1232,8 +1241,8 @@ and eval_function_call_symbolic_from_inst_sig (config : C.config) let expr = cf ctx in (* Synthesize the symbolic AST *) - S.synthesize_regular_function_call fid call_id ctx abs_ids type_args cg_args - args args_places ret_spc dest_place expr + S.synthesize_regular_function_call fid call_id ctx abs_ids generics args + args_places ret_spc dest_place expr in let cc = comp cc cf_call in @@ -1294,9 +1303,8 @@ and eval_function_call_symbolic_from_inst_sig (config : C.config) cc (cf Unit) ctx (** Evaluate a non-local function call in symbolic mode *) -and eval_non_local_function_call_symbolic (config : C.config) - (fid : A.assumed_fun_id) (region_args : T.erased_region list) - (type_args : T.ety list) (cg_args : T.const_generic list) +and eval_assumed_function_call_symbolic (config : C.config) + (fid : A.assumed_fun_id) (generics : T.egeneric_args) (args : E.operand list) (dest : E.place) : st_cm_fun = fun cf ctx -> (* Sanity check: make sure the type parameters don't contain regions - @@ -1304,7 +1312,7 @@ and eval_non_local_function_call_symbolic (config : C.config) assert ( List.for_all (fun ty -> not (ty_has_borrows ctx.type_context.type_infos ty)) - type_args); + generics.types); (* There are two cases (and this is extremely annoying): - the function is not box_free @@ -1315,7 +1323,7 @@ and eval_non_local_function_call_symbolic (config : C.config) | A.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 region_args type_args cg_args args dest (cf Unit) ctx + eval_box_free config generics args dest (cf Unit) ctx | _ -> (* "Normal" case: not box_free *) (* In symbolic mode, the behaviour of a function call is completely defined @@ -1327,55 +1335,50 @@ and eval_non_local_function_call_symbolic (config : C.config) (* should have been treated above *) raise (Failure "Unreachable") | _ -> - instantiate_fun_sig type_args cg_args (Assumed.get_assumed_sig fid) + (* There shouldn't be any reference to Self *) + let tr_self = T.UnknownTrait __FUNCTION__ in + instantiate_fun_sig ctx generics tr_self + (Assumed.get_assumed_sig fid) in (* Evaluate the function call *) eval_function_call_symbolic_from_inst_sig config (A.Assumed fid) inst_sig - region_args type_args cg_args args dest cf ctx + generics args dest cf ctx (** Evaluate a non-local (i.e, assumed) function call such as [Box::deref] (auxiliary helper for [eval_statement]) *) -and eval_non_local_function_call (config : C.config) (fid : A.assumed_fun_id) - (region_args : T.erased_region list) (type_args : T.ety list) - (cg_args : T.const_generic list) (args : E.operand list) (dest : E.place) : +and eval_assumed_function_call (config : C.config) (fid : A.assumed_fun_id) + (generics : T.egeneric_args) (args : E.operand list) (dest : E.place) : st_cm_fun = fun cf ctx -> (* Debug *) log#ldebug (lazy - (let type_args = - "[" ^ String.concat ", " (List.map (ety_to_string ctx) type_args) ^ "]" - in + (let generics = PCtx.egeneric_args_to_string ctx generics in let args = "[" ^ String.concat ", " (List.map (operand_to_string ctx) args) ^ "]" in let dest = place_to_string ctx dest in - "eval_non_local_function_call:\n- fid:" ^ A.show_assumed_fun_id fid - ^ "\n- type_args: " ^ type_args ^ "\n- args: " ^ args ^ "\n- dest: " - ^ dest)); + "eval_assumed_function_call:\n- fid:" ^ A.show_assumed_fun_id fid + ^ "\n- generics: " ^ generics ^ "\n- args: " ^ args ^ "\n- dest: " ^ dest)); match config.mode with | C.ConcreteMode -> - eval_non_local_function_call_concrete config fid region_args type_args - cg_args args dest (cf Unit) ctx + eval_assumed_function_call_concrete config fid generics args dest + (cf Unit) ctx | C.SymbolicMode -> - eval_non_local_function_call_symbolic config fid region_args type_args - cg_args args dest cf ctx + eval_assumed_function_call_symbolic config fid generics args dest cf ctx (** Evaluate a local (i.e, not assumed) function call (auxiliary helper for [eval_statement]) *) -and eval_local_function_call (config : C.config) (fid : A.FunDeclId.id) - (region_args : T.erased_region list) (type_args : T.ety list) - (cg_args : T.const_generic list) (args : E.operand list) (dest : E.place) : +and eval_transparent_function_call (config : C.config) (fid : A.FunDeclId.id) + (generics : T.egeneric_args) (args : E.operand list) (dest : E.place) : st_cm_fun = match config.mode with | ConcreteMode -> - eval_local_function_call_concrete config fid region_args type_args cg_args - args dest + eval_transparent_function_call_concrete config fid generics args dest | SymbolicMode -> - eval_local_function_call_symbolic config fid region_args type_args cg_args - args dest + eval_transparent_function_call_symbolic config fid generics args dest (** Evaluate a statement seen as a function body *) and eval_function_body (config : C.config) (body : A.statement) : st_cm_fun = -- cgit v1.2.3 From 06360698561019d7f480dcb4263e2099d9a03ca5 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Fri, 1 Sep 2023 12:01:03 +0200 Subject: Implement the normalization functions in AssociatedTypes --- compiler/InterpreterStatements.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'compiler/InterpreterStatements.ml') diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml index d38f8b95..3fb07956 100644 --- a/compiler/InterpreterStatements.ml +++ b/compiler/InterpreterStatements.ml @@ -326,7 +326,7 @@ let get_assumed_function_return_type (ctx : C.eval_ctx) (fid : A.assumed_fun_id) Subst.erase_regions_substitute_types ty_subst cg_subst tr_subst tr_self sg.output in - Assoc.ctx_normalize_type ctx ty + Assoc.ctx_normalize_ety ctx ty let move_return_value (config : C.config) (pop_return_value : bool) (cf : V.typed_value option -> m_fun) : m_fun = -- cgit v1.2.3 From aed317881d3083bba6a2cf154289486ef47ddf85 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Fri, 1 Sep 2023 16:57:07 +0200 Subject: Update PureMicroPasses --- compiler/InterpreterStatements.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'compiler/InterpreterStatements.ml') diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml index 3fb07956..3a483b80 100644 --- a/compiler/InterpreterStatements.ml +++ b/compiler/InterpreterStatements.ml @@ -1086,7 +1086,7 @@ and eval_transparent_function_call_concrete (config : C.config) | Some body -> body in (* TODO: we need to normalize the types if we want to correctly support traits *) - assert (ctx.trait_clauses = [] && generics.trait_refs = []); + assert (generics.trait_refs = []); (* There shouldn't be any reference to Self *) let tr_self = T.UnknownTrait __FUNCTION__ in let subst = -- cgit v1.2.3 From 8233c5a4918864166f877c9fcea19b4250185583 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Sun, 10 Sep 2023 20:29:18 +0200 Subject: Implement handling of trait method function calls --- compiler/InterpreterStatements.ml | 181 ++++++++++++++++++++++++-------------- 1 file changed, 115 insertions(+), 66 deletions(-) (limited to 'compiler/InterpreterStatements.ml') diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml index 3a483b80..5791a359 100644 --- a/compiler/InterpreterStatements.ml +++ b/compiler/InterpreterStatements.ml @@ -582,8 +582,10 @@ let eval_vec_function_concrete (_config : C.config) (_fid : A.assumed_fun_id) (** Evaluate a non-local function call in concrete mode *) let eval_assumed_function_call_concrete (config : C.config) - (fid : A.assumed_fun_id) (generics : T.egeneric_args) - (args : E.operand list) (dest : E.place) : cm_fun = + (fid : A.assumed_fun_id) (call : A.call) : cm_fun = + let generics = call.generics in + let args = call.args in + let dest = call.dest in (* Sanity check: we don't fully handle the const generic vars environment in concrete mode yet *) assert (generics.const_generics = []); @@ -906,9 +908,16 @@ and eval_global (config : C.config) (dest : E.place) (gid : LA.GlobalDeclId.id) match config.mode with | ConcreteMode -> (* Treat the evaluation of the global as a call to the global body (without arguments) *) - let generics = TypesUtils.mk_empty_generic_args in - (eval_transparent_function_call_concrete config global.body_id generics [] - dest) + let call = + { + A.func = A.FunId (A.Regular global.body_id); + generics = TypesUtils.mk_empty_generic_args; + trait_and_method_generic_args = None; + args = []; + dest; + } + in + (eval_transparent_function_call_concrete config global.body_id call) cf ctx | SymbolicMode -> (* Generate a fresh symbolic value. In the translation, this fresh symbolic value will be @@ -1057,18 +1066,38 @@ and eval_function_call (config : C.config) (call : A.call) : st_cm_fun = - this is an assumed function, in which case there is a special treatment - this is a trait method *) + match config.mode with + | C.ConcreteMode -> eval_function_call_concrete config call + | C.SymbolicMode -> eval_function_call_symbolic config call + +and eval_function_call_concrete (config : C.config) (call : A.call) : st_cm_fun + = + fun cf ctx -> match call.func with | A.FunId (A.Regular fid) -> - eval_transparent_function_call config fid call.generics call.args - call.dest + eval_transparent_function_call_concrete config fid call cf ctx | A.FunId (A.Assumed fid) -> - eval_assumed_function_call config fid call.generics call.args call.dest - | A.TraitMethod _ -> raise (Failure "Unimplemented") + (* 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 fid call (cf Unit) ctx + | A.TraitMethod (_, _) -> raise (Failure "Unimplemented") + +and eval_function_call_symbolic (config : C.config) (call : A.call) : st_cm_fun + = + match call.func with + | A.FunId (A.Regular _) | A.TraitMethod (_, _) -> + eval_transparent_function_call_symbolic config call + | A.FunId (A.Assumed fid) -> + eval_assumed_function_call_symbolic config fid call (** Evaluate a local (i.e., non-assumed) function call in concrete mode *) and eval_transparent_function_call_concrete (config : C.config) - (fid : A.FunDeclId.id) (generics : T.egeneric_args) (args : E.operand list) - (dest : E.place) : st_cm_fun = + (fid : A.FunDeclId.id) (call : A.call) : st_cm_fun = + let generics = call.A.generics in + let args = call.A.args in + let dest = call.A.dest in (* Sanity check: we don't fully handle the const generic vars environment in concrete mode yet *) assert (generics.const_generics = []); @@ -1149,23 +1178,73 @@ and eval_transparent_function_call_concrete (config : C.config) cc cf ctx (** Evaluate a local (i.e., non-assumed) function call in symbolic mode *) -and eval_transparent_function_call_symbolic (config : C.config) - (fid : A.FunDeclId.id) (generics : T.egeneric_args) (args : E.operand list) - (dest : E.place) : st_cm_fun = +and eval_transparent_function_call_symbolic (config : C.config) (call : A.call) + : st_cm_fun = fun cf ctx -> - (* Retrieve the (correctly instantiated) signature *) - let def = C.ctx_lookup_fun_decl ctx fid in - let sg = def.A.signature in - (* Instantiate the signature and introduce fresh abstraction and region ids - * while doing so *) - (* There shouldn't be any reference to Self *) - let tr_self = T.UnknownTrait __FUNCTION__ in - let inst_sg = instantiate_fun_sig ctx generics tr_self sg in + (* Instantiate the signature and introduce fresh abstractions and region ids while doing so *) + let def, inst_sg = + match call.func with + | A.FunId (A.Regular fid) -> + let def = C.ctx_lookup_fun_decl ctx fid in + let tr_self = T.UnknownTrait __FUNCTION__ in + let inst_sg = + instantiate_fun_sig ctx call.generics tr_self def.A.signature + in + (def, inst_sg) + | A.FunId (A.Assumed _) -> + (* Unreachable: must be a transparent function *) + raise (Failure "Unreachable") + | A.TraitMethod (trait_ref, method_name) -> ( + (* When instantiating, we need to group the generics for the trait ref + and the method *) + let generics = Option.get call.trait_and_method_generic_args in + (* Lookup the trait method signature - there are several possibilities + depending on whethere we call a top-level trait method impl or the + method from a local clause *) + match trait_ref.trait_id with + | TraitImpl impl_id -> + (* Lookup the trait impl *) + let trait_impl = C.ctx_lookup_trait_impl ctx impl_id in + let _, method_id = + List.find + (fun (s, _) -> s = method_name) + trait_impl.required_methods + in + let method_def = C.ctx_lookup_fun_decl ctx method_id in + (* Instantiate *) + let tr_self = T.UnknownTrait __FUNCTION__ in + let inst_sg = + instantiate_fun_sig ctx generics tr_self method_def.A.signature + in + (method_def, inst_sg) + | _ -> + (* We are using a local clause - we lookup the trait decl *) + let trait_decl = + C.ctx_lookup_trait_decl ctx trait_ref.trait_decl_ref.trait_decl_id + in + (* Lookup the method decl *) + let _, method_id = + List.find + (fun (s, _) -> s = method_name) + trait_decl.required_methods + in + let method_def = C.ctx_lookup_fun_decl ctx method_id in + (* Instantiate *) + let tr_self = T.TraitRef trait_ref in + let tr_self = + TypesUtils.etrait_instance_id_no_regions_to_gr_trait_instance_id + tr_self + in + let inst_sg = + instantiate_fun_sig ctx generics tr_self method_def.A.signature + in + (method_def, inst_sg)) + in (* Sanity check *) - assert (List.length args = List.length def.A.signature.inputs); + assert (List.length call.args = List.length def.A.signature.inputs); (* Evaluate the function call *) - eval_function_call_symbolic_from_inst_sig config (A.Regular fid) inst_sg - generics args dest cf ctx + eval_function_call_symbolic_from_inst_sig config call.func inst_sg + call.generics call.args call.dest cf ctx (** Evaluate a function call in symbolic mode by using the function signature. @@ -1173,9 +1252,12 @@ and eval_transparent_function_call_symbolic (config : C.config) calls in symbolic mode: only their signatures matter. *) and eval_function_call_symbolic_from_inst_sig (config : C.config) - (fid : A.fun_id) (inst_sg : A.inst_fun_sig) (generics : T.egeneric_args) - (args : E.operand list) (dest : E.place) : st_cm_fun = + (fid : A.fun_id_or_trait_method_ref) (inst_sg : A.inst_fun_sig) + (generics : T.egeneric_args) (args : E.operand list) (dest : E.place) : + st_cm_fun = fun cf ctx -> + (* TODO: trait methods are not supported yet *) + let fid = match fid with A.FunId fid -> fid | _ -> raise (Failure "TODO") in (* Generate a fresh symbolic value for the return value *) let ret_sv_ty = inst_sg.A.output in let ret_spc = mk_fresh_symbolic_value V.FunCallRet ret_sv_ty in @@ -1304,9 +1386,11 @@ and eval_function_call_symbolic_from_inst_sig (config : C.config) (** Evaluate a non-local function call in symbolic mode *) and eval_assumed_function_call_symbolic (config : C.config) - (fid : A.assumed_fun_id) (generics : T.egeneric_args) - (args : E.operand list) (dest : E.place) : st_cm_fun = + (fid : A.assumed_fun_id) (call : A.call) : st_cm_fun = fun cf ctx -> + let generics = call.generics in + let args = call.args in + let dest = call.dest in (* Sanity check: make sure the type parameters don't contain regions - * this is a current limitation of our synthesis *) assert ( @@ -1342,43 +1426,8 @@ and eval_assumed_function_call_symbolic (config : C.config) in (* Evaluate the function call *) - eval_function_call_symbolic_from_inst_sig config (A.Assumed fid) inst_sig - generics args dest cf ctx - -(** Evaluate a non-local (i.e, assumed) function call such as [Box::deref] - (auxiliary helper for [eval_statement]) *) -and eval_assumed_function_call (config : C.config) (fid : A.assumed_fun_id) - (generics : T.egeneric_args) (args : E.operand list) (dest : E.place) : - st_cm_fun = - fun cf ctx -> - (* Debug *) - log#ldebug - (lazy - (let generics = PCtx.egeneric_args_to_string ctx generics in - let args = - "[" ^ String.concat ", " (List.map (operand_to_string ctx) args) ^ "]" - in - let dest = place_to_string ctx dest in - "eval_assumed_function_call:\n- fid:" ^ A.show_assumed_fun_id fid - ^ "\n- generics: " ^ generics ^ "\n- args: " ^ args ^ "\n- dest: " ^ dest)); - - match config.mode with - | C.ConcreteMode -> - eval_assumed_function_call_concrete config fid generics args dest - (cf Unit) ctx - | C.SymbolicMode -> - eval_assumed_function_call_symbolic config fid generics args dest cf ctx - -(** Evaluate a local (i.e, not assumed) function call (auxiliary helper for - [eval_statement]) *) -and eval_transparent_function_call (config : C.config) (fid : A.FunDeclId.id) - (generics : T.egeneric_args) (args : E.operand list) (dest : E.place) : - st_cm_fun = - match config.mode with - | ConcreteMode -> - eval_transparent_function_call_concrete config fid generics args dest - | SymbolicMode -> - eval_transparent_function_call_symbolic config fid generics args dest + eval_function_call_symbolic_from_inst_sig config (A.FunId (A.Assumed fid)) + inst_sig generics args dest cf ctx (** Evaluate a statement seen as a function body *) and eval_function_body (config : C.config) (body : A.statement) : st_cm_fun = -- cgit v1.2.3 From 5921be8e2e8955db5101354d8bf29ae6a3693f48 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Mon, 11 Sep 2023 06:35:07 +0200 Subject: Make progress on correctly handling trait method calls in the symbolic execution --- compiler/InterpreterStatements.ml | 126 ++++++++++++++++++++++++++++++-------- 1 file changed, 102 insertions(+), 24 deletions(-) (limited to 'compiler/InterpreterStatements.ml') diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml index 5791a359..1ea16e58 100644 --- a/compiler/InterpreterStatements.ml +++ b/compiler/InterpreterStatements.ml @@ -1082,12 +1082,12 @@ and eval_function_call_concrete (config : C.config) (call : A.call) : st_cm_fun * where we haven't panicked. Of course, the translation needs to take the * panic case into account... *) eval_assumed_function_call_concrete config fid call (cf Unit) ctx - | A.TraitMethod (_, _) -> raise (Failure "Unimplemented") + | A.TraitMethod _ -> raise (Failure "Unimplemented") and eval_function_call_symbolic (config : C.config) (call : A.call) : st_cm_fun = match call.func with - | A.FunId (A.Regular _) | A.TraitMethod (_, _) -> + | A.FunId (A.Regular _) | A.TraitMethod _ -> eval_transparent_function_call_symbolic config call | A.FunId (A.Assumed fid) -> eval_assumed_function_call_symbolic config fid call @@ -1182,7 +1182,7 @@ and eval_transparent_function_call_symbolic (config : C.config) (call : A.call) : st_cm_fun = fun cf ctx -> (* Instantiate the signature and introduce fresh abstractions and region ids while doing so *) - let def, inst_sg = + let func, def, self_trait_ref, inst_sg = match call.func with | A.FunId (A.Regular fid) -> let def = C.ctx_lookup_fun_decl ctx fid in @@ -1190,11 +1190,19 @@ and eval_transparent_function_call_symbolic (config : C.config) (call : A.call) let inst_sg = instantiate_fun_sig ctx call.generics tr_self def.A.signature in - (def, inst_sg) + (call.func, def, None, inst_sg) | A.FunId (A.Assumed _) -> (* Unreachable: must be a transparent function *) raise (Failure "Unreachable") - | A.TraitMethod (trait_ref, method_name) -> ( + | A.TraitMethod (trait_ref, method_name, _) -> ( + log#ldebug + (lazy + ("trait method call:\n- call: " ^ call_to_string ctx call + ^ "\n- method name: " ^ method_name ^ "\n- generics:\n" + ^ egeneric_args_to_string ctx call.generics + ^ "\n- trait and method generics:\n" + ^ egeneric_args_to_string ctx + (Option.get call.trait_and_method_generic_args))); (* When instantiating, we need to group the generics for the trait ref and the method *) let generics = Option.get call.trait_and_method_generic_args in @@ -1202,31 +1210,97 @@ and eval_transparent_function_call_symbolic (config : C.config) (call : A.call) depending on whethere we call a top-level trait method impl or the method from a local clause *) match trait_ref.trait_id with - | TraitImpl impl_id -> + | TraitImpl impl_id -> ( (* Lookup the trait impl *) let trait_impl = C.ctx_lookup_trait_impl ctx impl_id in - let _, method_id = - List.find + log#ldebug + (lazy ("trait impl: " ^ trait_impl_to_string ctx trait_impl)); + (* First look in the required methods *) + let method_id = + List.find_opt (fun (s, _) -> s = method_name) trait_impl.required_methods in - let method_def = C.ctx_lookup_fun_decl ctx method_id in - (* Instantiate *) - let tr_self = T.UnknownTrait __FUNCTION__ in - let inst_sg = - instantiate_fun_sig ctx generics tr_self method_def.A.signature - in - (method_def, inst_sg) + match method_id with + | Some (_, id) -> + let method_def = C.ctx_lookup_fun_decl ctx id in + (* Instantiate *) + let tr_self = + T.TraitRef (etrait_ref_no_regions_to_gr_trait_ref trait_ref) + in + let inst_sg = + instantiate_fun_sig ctx generics tr_self + method_def.A.signature + in + (call.func, method_def, None, inst_sg) + | None -> + (* If not found, lookup the methods provided by the trait *declaration* + (remember: for now, we forbid overriding provided methods) *) + assert (trait_impl.provided_methods = []); + let trait_decl = + C.ctx_lookup_trait_decl ctx + trait_ref.trait_decl_ref.trait_decl_id + in + let _, method_id = + List.find + (fun (s, _) -> s = method_name) + trait_decl.provided_methods + in + let method_id = Option.get method_id in + let method_def = C.ctx_lookup_fun_decl ctx method_id in + (* For the instantiation we have to do something perculiar + because the method was defined for the trait declaration. + We have to group: + - the parameters given to the trait decl reference + - the parameters given to the method itself + For instance: + {[ + trait Foo { + fn f(...) { ... } + } + + fn g(x : G) where Clause0: Foo + { + x.f::(...) // The arguments to f are: + } + ]} + *) + let generics = + TypesUtils.merge_generic_args + trait_ref.trait_decl_ref.decl_generics call.generics + in + log#ldebug + (lazy + ("provided method call:" ^ "\n- method name: " ^ method_name + ^ "\n- generics:\n" + ^ egeneric_args_to_string ctx generics)); + let tr_self = + T.TraitRef (etrait_ref_no_regions_to_gr_trait_ref trait_ref) + in + let inst_sg = + instantiate_fun_sig ctx generics tr_self + method_def.A.signature + in + (* We directly call the function, pretending it is not a trait method call *) + (* TODO: we need to add the self trait ref *) + let func = A.FunId (A.Regular method_def.def_id) in + (func, method_def, Some trait_ref, inst_sg)) | _ -> (* We are using a local clause - we lookup the trait decl *) let trait_decl = C.ctx_lookup_trait_decl ctx trait_ref.trait_decl_ref.trait_decl_id in - (* Lookup the method decl *) + (* Lookup the method decl in the required *and* the provided methods *) let _, method_id = + let provided = + List.filter_map + (fun (id, f) -> + match f with None -> None | Some f -> Some (id, f)) + trait_decl.provided_methods + in List.find (fun (s, _) -> s = method_name) - trait_decl.required_methods + (List.append trait_decl.required_methods provided) in let method_def = C.ctx_lookup_fun_decl ctx method_id in (* Instantiate *) @@ -1238,26 +1312,30 @@ and eval_transparent_function_call_symbolic (config : C.config) (call : A.call) let inst_sg = instantiate_fun_sig ctx generics tr_self method_def.A.signature in - (method_def, inst_sg)) + (call.func, method_def, None, inst_sg)) in (* Sanity check *) assert (List.length call.args = List.length def.A.signature.inputs); (* Evaluate the function call *) - eval_function_call_symbolic_from_inst_sig config call.func inst_sg + eval_function_call_symbolic_from_inst_sig config func inst_sg self_trait_ref call.generics call.args call.dest cf ctx (** Evaluate a function call in symbolic mode by using the function signature. This allows us to factorize the evaluation of local and non-local function calls in symbolic mode: only their signatures matter. + + The [self_trait_ref] trait ref refers to [Self]. We use it when calling + a provided trait method, because those methods have a special treatment: + we dot not group them with the required trait methods, and forbid (for now) + overriding them. We treat them as regular method, which take an additional + trait ref as input. *) and eval_function_call_symbolic_from_inst_sig (config : C.config) (fid : A.fun_id_or_trait_method_ref) (inst_sg : A.inst_fun_sig) - (generics : T.egeneric_args) (args : E.operand list) (dest : E.place) : - st_cm_fun = + (self_trait_ref : T.etrait_ref option) (generics : T.egeneric_args) + (args : E.operand list) (dest : E.place) : st_cm_fun = fun cf ctx -> - (* TODO: trait methods are not supported yet *) - let fid = match fid with A.FunId fid -> fid | _ -> raise (Failure "TODO") in (* Generate a fresh symbolic value for the return value *) let ret_sv_ty = inst_sg.A.output in let ret_spc = mk_fresh_symbolic_value V.FunCallRet ret_sv_ty in @@ -1427,7 +1505,7 @@ and eval_assumed_function_call_symbolic (config : C.config) (* Evaluate the function call *) eval_function_call_symbolic_from_inst_sig config (A.FunId (A.Assumed fid)) - inst_sig generics args dest cf ctx + inst_sig None generics args dest cf ctx (** Evaluate a statement seen as a function body *) and eval_function_body (config : C.config) (body : A.statement) : st_cm_fun = -- cgit v1.2.3 From 78a2731924aa13989998c6be4a5a6865ce5098aa Mon Sep 17 00:00:00 2001 From: Son Ho Date: Wed, 13 Sep 2023 07:33:30 +0200 Subject: Make minor modifications --- compiler/InterpreterStatements.ml | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) (limited to 'compiler/InterpreterStatements.ml') diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml index 1ea16e58..97fb80f4 100644 --- a/compiler/InterpreterStatements.ml +++ b/compiler/InterpreterStatements.ml @@ -1198,7 +1198,7 @@ and eval_transparent_function_call_symbolic (config : C.config) (call : A.call) log#ldebug (lazy ("trait method call:\n- call: " ^ call_to_string ctx call - ^ "\n- method name: " ^ method_name ^ "\n- generics:\n" + ^ "\n- method name: " ^ method_name ^ "\n- call.generics:\n" ^ egeneric_args_to_string ctx call.generics ^ "\n- trait and method generics:\n" ^ egeneric_args_to_string ctx @@ -1273,7 +1273,10 @@ and eval_transparent_function_call_symbolic (config : C.config) (call : A.call) (lazy ("provided method call:" ^ "\n- method name: " ^ method_name ^ "\n- generics:\n" - ^ egeneric_args_to_string ctx generics)); + ^ egeneric_args_to_string ctx generics + ^ "\n- parent params info: " + ^ Print.option_to_string A.show_params_info + method_def.signature.parent_params_info)); let tr_self = T.TraitRef (etrait_ref_no_regions_to_gr_trait_ref trait_ref) in @@ -1303,6 +1306,7 @@ and eval_transparent_function_call_symbolic (config : C.config) (call : A.call) (List.append trait_decl.required_methods provided) in let method_def = C.ctx_lookup_fun_decl ctx method_id in + log#ldebug (lazy ("method:\n" ^ fun_decl_to_string ctx method_def)); (* Instantiate *) let tr_self = T.TraitRef trait_ref in let tr_self = -- cgit v1.2.3 From 60aa9ff5b31e47ecc2ac2dff55ee06582af62806 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Wed, 13 Sep 2023 23:39:13 +0200 Subject: Fix some issues --- compiler/InterpreterStatements.ml | 7 +++++++ 1 file changed, 7 insertions(+) (limited to 'compiler/InterpreterStatements.ml') diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml index 97fb80f4..88e20a92 100644 --- a/compiler/InterpreterStatements.ml +++ b/compiler/InterpreterStatements.ml @@ -664,6 +664,13 @@ let eval_assumed_function_call_concrete (config : C.config) let instantiate_fun_sig (ctx : C.eval_ctx) (generics : T.egeneric_args) (tr_self : T.rtrait_instance_id) (sg : A.fun_sig) : A.inst_fun_sig = + log#ldebug + (lazy + ("instantiate_fun_sig:" ^ "\n- generics: " + ^ egeneric_args_to_string ctx generics + ^ "\n- tr_self: " + ^ rtrait_instance_id_to_string ctx tr_self + ^ "\n- sg: " ^ fun_sig_to_string ctx sg)); (* Generate fresh abstraction ids and create a substitution from region * group ids to abstraction ids *) let rg_abs_ids_bindings = -- cgit v1.2.3 From 9bfbfcc5aa3a05aafa2b7b5014256b30a878f0a2 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Sun, 17 Sep 2023 01:20:17 +0200 Subject: Fix some issues with calls to trait methods --- compiler/InterpreterStatements.ml | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) (limited to 'compiler/InterpreterStatements.ml') diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml index 88e20a92..b00aca7e 100644 --- a/compiler/InterpreterStatements.ml +++ b/compiler/InterpreterStatements.ml @@ -1201,7 +1201,7 @@ and eval_transparent_function_call_symbolic (config : C.config) (call : A.call) | A.FunId (A.Assumed _) -> (* Unreachable: must be a transparent function *) raise (Failure "Unreachable") - | A.TraitMethod (trait_ref, method_name, _) -> ( + | A.TraitMethod (trait_ref, method_name, method_decl_id) -> ( log#ldebug (lazy ("trait method call:\n- call: " ^ call_to_string ctx call @@ -1230,6 +1230,7 @@ and eval_transparent_function_call_symbolic (config : C.config) (call : A.call) in match method_id with | Some (_, id) -> + (* This is a required method *) let method_def = C.ctx_lookup_fun_decl ctx id in (* Instantiate *) let tr_self = @@ -1239,7 +1240,11 @@ and eval_transparent_function_call_symbolic (config : C.config) (call : A.call) instantiate_fun_sig ctx generics tr_self method_def.A.signature in - (call.func, method_def, None, inst_sg) + (* Also update the function identifier: we want to forget + the fact that we called a trait method, and treat it as + a regular function acll. *) + let func = A.FunId (A.Regular method_decl_id) in + (func, method_def, None, inst_sg) | None -> (* If not found, lookup the methods provided by the trait *declaration* (remember: for now, we forbid overriding provided methods) *) -- cgit v1.2.3 From 245a19a962c2fbd546c90c4ff16767a03af591e9 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Sun, 17 Sep 2023 01:22:45 +0200 Subject: Fix a minor issue --- compiler/InterpreterStatements.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'compiler/InterpreterStatements.ml') diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml index b00aca7e..d67d57db 100644 --- a/compiler/InterpreterStatements.ml +++ b/compiler/InterpreterStatements.ml @@ -1201,7 +1201,7 @@ and eval_transparent_function_call_symbolic (config : C.config) (call : A.call) | A.FunId (A.Assumed _) -> (* Unreachable: must be a transparent function *) raise (Failure "Unreachable") - | A.TraitMethod (trait_ref, method_name, method_decl_id) -> ( + | A.TraitMethod (trait_ref, method_name, _) -> ( log#ldebug (lazy ("trait method call:\n- call: " ^ call_to_string ctx call @@ -1243,7 +1243,7 @@ and eval_transparent_function_call_symbolic (config : C.config) (call : A.call) (* Also update the function identifier: we want to forget the fact that we called a trait method, and treat it as a regular function acll. *) - let func = A.FunId (A.Regular method_decl_id) in + let func = A.FunId (A.Regular id) in (func, method_def, None, inst_sg) | None -> (* If not found, lookup the methods provided by the trait *declaration* -- cgit v1.2.3 From f2928eaa854688b679f7e504c036866ee7664fe5 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Sun, 17 Sep 2023 03:17:51 +0200 Subject: Update the handling of calls to trait impl methods --- compiler/InterpreterStatements.ml | 75 ++++++++++++++++++++++++++++++++++----- 1 file changed, 67 insertions(+), 8 deletions(-) (limited to 'compiler/InterpreterStatements.ml') diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml index d67d57db..2a5c8952 100644 --- a/compiler/InterpreterStatements.ml +++ b/compiler/InterpreterStatements.ml @@ -1188,8 +1188,64 @@ and eval_transparent_function_call_concrete (config : C.config) and eval_transparent_function_call_symbolic (config : C.config) (call : A.call) : st_cm_fun = fun cf ctx -> - (* Instantiate the signature and introduce fresh abstractions and region ids while doing so *) - let func, def, self_trait_ref, inst_sg = + (* Instantiate the signature and introduce fresh abstractions and region ids while doing so. + + We perform some manipulations when instantiating the signature. + In particular, we have a special treatment of trait method calls when + the trait ref is a known impl. + + For instance: + {[ + trait HasValue { + fn has_value(&self) -> bool; + } + + impl HasValue for Option { + fn has_value(&self) { + match self { + None => false, + Some(_) => true, + } + } + } + + fn option_has_value(x: &Option) -> bool { + x.has_value() + } + ]} + + The generated code looks like this: + {[ + structure HasValue (T : Type) = { + has_value : T -> result bool + } + + let OptionHasValueImpl.has_value (T : Type) (self : T) : result bool = + match self with + | None => false + | Some _ => true + + let OptionHasValueInstance (T : Type) : HasValue (Option T) = { + has_value = OptionHasValueInstance.has_value + } + ]} + + In [option_has_value], we don't want to refer to the [has_value] method + of the instance of [HasValue] for [Option]. We want to refer directly + to the function which implements [has_value] for [Option]. + That is, instead of generating this: + {[ + let option_has_value (T : Type) (x : Option T) : result bool = + (OptionHasValueInstance T).has_value x + ]} + + We want to generate this: + {[ + let option_has_value (T : Type) (x : Option T) : result bool = + OptionHasValueImpl.has_value T x + ]} + *) + let func, generics, def, self_trait_ref, inst_sg = match call.func with | A.FunId (A.Regular fid) -> let def = C.ctx_lookup_fun_decl ctx fid in @@ -1197,7 +1253,7 @@ and eval_transparent_function_call_symbolic (config : C.config) (call : A.call) let inst_sg = instantiate_fun_sig ctx call.generics tr_self def.A.signature in - (call.func, def, None, inst_sg) + (call.func, call.generics, def, None, inst_sg) | A.FunId (A.Assumed _) -> (* Unreachable: must be a transparent function *) raise (Failure "Unreachable") @@ -1242,9 +1298,12 @@ and eval_transparent_function_call_symbolic (config : C.config) (call : A.call) in (* Also update the function identifier: we want to forget the fact that we called a trait method, and treat it as - a regular function acll. *) + a regular function call to the top-level function + which implements the method. In order to do this properly, + we also need to update the generics. + *) let func = A.FunId (A.Regular id) in - (func, method_def, None, inst_sg) + (func, generics, method_def, None, inst_sg) | None -> (* If not found, lookup the methods provided by the trait *declaration* (remember: for now, we forbid overriding provided methods) *) @@ -1299,7 +1358,7 @@ and eval_transparent_function_call_symbolic (config : C.config) (call : A.call) (* We directly call the function, pretending it is not a trait method call *) (* TODO: we need to add the self trait ref *) let func = A.FunId (A.Regular method_def.def_id) in - (func, method_def, Some trait_ref, inst_sg)) + (func, generics, method_def, Some trait_ref, inst_sg)) | _ -> (* We are using a local clause - we lookup the trait decl *) let trait_decl = @@ -1328,13 +1387,13 @@ and eval_transparent_function_call_symbolic (config : C.config) (call : A.call) let inst_sg = instantiate_fun_sig ctx generics tr_self method_def.A.signature in - (call.func, method_def, None, inst_sg)) + (call.func, generics, method_def, None, inst_sg)) in (* Sanity check *) assert (List.length call.args = List.length def.A.signature.inputs); (* Evaluate the function call *) eval_function_call_symbolic_from_inst_sig config func inst_sg self_trait_ref - call.generics call.args call.dest cf ctx + generics call.args call.dest cf ctx (** Evaluate a function call in symbolic mode by using the function signature. -- cgit v1.2.3 From 296f97bb6a768ffd85f35db2762f2db4f7a357ad Mon Sep 17 00:00:00 2001 From: Son Ho Date: Sun, 17 Sep 2023 04:43:01 +0200 Subject: Make progress on correctly extracting trait method calls --- compiler/InterpreterStatements.ml | 33 ++++++++++++++++++++------------- 1 file changed, 20 insertions(+), 13 deletions(-) (limited to 'compiler/InterpreterStatements.ml') diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml index 2a5c8952..f54c5dbd 100644 --- a/compiler/InterpreterStatements.ml +++ b/compiler/InterpreterStatements.ml @@ -1191,6 +1191,9 @@ and eval_transparent_function_call_symbolic (config : C.config) (call : A.call) (* Instantiate the signature and introduce fresh abstractions and region ids while doing so. We perform some manipulations when instantiating the signature. + + # Trait impl calls + ================== In particular, we have a special treatment of trait method calls when the trait ref is a known impl. @@ -1216,11 +1219,11 @@ and eval_transparent_function_call_symbolic (config : C.config) (call : A.call) The generated code looks like this: {[ - structure HasValue (T : Type) = { - has_value : T -> result bool + structure HasValue (Self : Type) = { + has_value : Self -> result bool } - let OptionHasValueImpl.has_value (T : Type) (self : T) : result bool = + let OptionHasValueImpl.has_value (Self : Type) (self : Self) : result bool = match self with | None => false | Some _ => true @@ -1244,6 +1247,13 @@ and eval_transparent_function_call_symbolic (config : C.config) (call : A.call) let option_has_value (T : Type) (x : Option T) : result bool = OptionHasValueImpl.has_value T x ]} + + # Provided trait methods + ======================== + Calls to provided trait methods also have a special treatment because + for now we forbid overriding provided trait methods in the trait implementations, + which means that whenever we call a provided trait method, we do not refer + to a trait clause but directly to the method provided in the trait declaration. *) let func, generics, def, self_trait_ref, inst_sg = match call.func with @@ -1319,7 +1329,7 @@ and eval_transparent_function_call_symbolic (config : C.config) (call : A.call) in let method_id = Option.get method_id in let method_def = C.ctx_lookup_fun_decl ctx method_id in - (* For the instantiation we have to do something perculiar + (* For the instantiation we have to do something peculiar because the method was defined for the trait declaration. We have to group: - the parameters given to the trait decl reference @@ -1336,15 +1346,15 @@ and eval_transparent_function_call_symbolic (config : C.config) (call : A.call) } ]} *) - let generics = + let all_generics = TypesUtils.merge_generic_args trait_ref.trait_decl_ref.decl_generics call.generics in log#ldebug (lazy ("provided method call:" ^ "\n- method name: " ^ method_name - ^ "\n- generics:\n" - ^ egeneric_args_to_string ctx generics + ^ "\n- all_generics:\n" + ^ egeneric_args_to_string ctx all_generics ^ "\n- parent params info: " ^ Print.option_to_string A.show_params_info method_def.signature.parent_params_info)); @@ -1352,13 +1362,10 @@ and eval_transparent_function_call_symbolic (config : C.config) (call : A.call) T.TraitRef (etrait_ref_no_regions_to_gr_trait_ref trait_ref) in let inst_sg = - instantiate_fun_sig ctx generics tr_self + instantiate_fun_sig ctx all_generics tr_self method_def.A.signature in - (* We directly call the function, pretending it is not a trait method call *) - (* TODO: we need to add the self trait ref *) - let func = A.FunId (A.Regular method_def.def_id) in - (func, generics, method_def, Some trait_ref, inst_sg)) + (call.func, call.generics, method_def, Some trait_ref, inst_sg)) | _ -> (* We are using a local clause - we lookup the trait decl *) let trait_decl = @@ -1387,7 +1394,7 @@ and eval_transparent_function_call_symbolic (config : C.config) (call : A.call) let inst_sg = instantiate_fun_sig ctx generics tr_self method_def.A.signature in - (call.func, generics, method_def, None, inst_sg)) + (call.func, call.generics, method_def, None, inst_sg)) in (* Sanity check *) assert (List.length call.args = List.length def.A.signature.inputs); -- cgit v1.2.3 From 353a9627cf39290f2fe841a45e52726aa9fe6512 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Sun, 17 Sep 2023 06:58:17 +0200 Subject: Normalize the function signatures before translation to pure --- compiler/InterpreterStatements.ml | 61 --------------------------------------- 1 file changed, 61 deletions(-) (limited to 'compiler/InterpreterStatements.ml') diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml index f54c5dbd..dc15c6ac 100644 --- a/compiler/InterpreterStatements.ml +++ b/compiler/InterpreterStatements.ml @@ -662,67 +662,6 @@ let eval_assumed_function_call_concrete (config : C.config) (* Compose and apply *) comp cf_eval_ops cf_eval_call -let instantiate_fun_sig (ctx : C.eval_ctx) (generics : T.egeneric_args) - (tr_self : T.rtrait_instance_id) (sg : A.fun_sig) : A.inst_fun_sig = - log#ldebug - (lazy - ("instantiate_fun_sig:" ^ "\n- generics: " - ^ egeneric_args_to_string ctx generics - ^ "\n- tr_self: " - ^ rtrait_instance_id_to_string ctx tr_self - ^ "\n- sg: " ^ fun_sig_to_string ctx sg)); - (* Generate fresh abstraction ids and create a substitution from region - * group ids to abstraction ids *) - let rg_abs_ids_bindings = - List.map - (fun rg -> - let abs_id = C.fresh_abstraction_id () in - (rg.T.id, abs_id)) - sg.regions_hierarchy - in - let asubst_map : V.AbstractionId.id T.RegionGroupId.Map.t = - List.fold_left - (fun mp (rg_id, abs_id) -> T.RegionGroupId.Map.add rg_id abs_id mp) - T.RegionGroupId.Map.empty rg_abs_ids_bindings - in - let asubst (rg_id : T.RegionGroupId.id) : V.AbstractionId.id = - T.RegionGroupId.Map.find rg_id asubst_map - in - (* Generate fresh regions and their substitutions *) - let _, rsubst, _ = Subst.fresh_regions_with_substs sg.generics.regions in - (* Generate the type substitution - * Note that we need the substitution to map the type variables to - * {!rty} types (not {!ety}). In order to do that, we convert the - * type parameters to types with regions. This is possible only - * if those types don't contain any regions. - * This is a current limitation of the analysis: there is still some - * work to do to properly handle full type parametrization. - * *) - let rtype_params = List.map ety_no_regions_to_rty generics.types in - let tsubst = Subst.make_type_subst_from_vars sg.generics.types rtype_params in - let cgsubst = - Subst.make_const_generic_subst_from_vars sg.generics.const_generics - generics.const_generics - in - (* TODO: something annoying with the trait ref subst: we need to use region - types, but the arguments use erased regions. For now we use the fact - that no regions should appear inside. In the future: we should merge - ety and rty. *) - let trait_refs = - List.map TypesUtils.etrait_ref_no_regions_to_gr_trait_ref - generics.trait_refs - in - let tr_subst = - Subst.make_trait_subst_from_clauses sg.generics.trait_clauses trait_refs - in - (* Substitute the signature *) - let inst_sig = - Assoc.ctx_subst_norm_signature ctx asubst rsubst tsubst cgsubst tr_subst - tr_self sg - in - (* Return *) - inst_sig - (** Helper Create abstractions (with no avalues, which have to be inserted afterwards) -- cgit v1.2.3 From b946902f8cb8b83c2ca93eceebe99dfbc985987d Mon Sep 17 00:00:00 2001 From: Son Ho Date: Tue, 19 Sep 2023 18:07:13 +0200 Subject: Cleanup a bit --- compiler/InterpreterStatements.ml | 20 ++++++++++---------- 1 file changed, 10 insertions(+), 10 deletions(-) (limited to 'compiler/InterpreterStatements.ml') diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml index dc15c6ac..42073f0b 100644 --- a/compiler/InterpreterStatements.ml +++ b/compiler/InterpreterStatements.ml @@ -1194,7 +1194,7 @@ and eval_transparent_function_call_symbolic (config : C.config) (call : A.call) which means that whenever we call a provided trait method, we do not refer to a trait clause but directly to the method provided in the trait declaration. *) - let func, generics, def, self_trait_ref, inst_sg = + let func, generics, def, inst_sg = match call.func with | A.FunId (A.Regular fid) -> let def = C.ctx_lookup_fun_decl ctx fid in @@ -1202,7 +1202,7 @@ and eval_transparent_function_call_symbolic (config : C.config) (call : A.call) let inst_sg = instantiate_fun_sig ctx call.generics tr_self def.A.signature in - (call.func, call.generics, def, None, inst_sg) + (call.func, call.generics, def, inst_sg) | A.FunId (A.Assumed _) -> (* Unreachable: must be a transparent function *) raise (Failure "Unreachable") @@ -1252,7 +1252,7 @@ and eval_transparent_function_call_symbolic (config : C.config) (call : A.call) we also need to update the generics. *) let func = A.FunId (A.Regular id) in - (func, generics, method_def, None, inst_sg) + (func, generics, method_def, inst_sg) | None -> (* If not found, lookup the methods provided by the trait *declaration* (remember: for now, we forbid overriding provided methods) *) @@ -1304,7 +1304,7 @@ and eval_transparent_function_call_symbolic (config : C.config) (call : A.call) instantiate_fun_sig ctx all_generics tr_self method_def.A.signature in - (call.func, call.generics, method_def, Some trait_ref, inst_sg)) + (call.func, call.generics, method_def, inst_sg)) | _ -> (* We are using a local clause - we lookup the trait decl *) let trait_decl = @@ -1333,13 +1333,13 @@ and eval_transparent_function_call_symbolic (config : C.config) (call : A.call) let inst_sg = instantiate_fun_sig ctx generics tr_self method_def.A.signature in - (call.func, call.generics, method_def, None, inst_sg)) + (call.func, call.generics, method_def, inst_sg)) in (* Sanity check *) assert (List.length call.args = List.length def.A.signature.inputs); (* Evaluate the function call *) - eval_function_call_symbolic_from_inst_sig config func inst_sg self_trait_ref - generics call.args call.dest cf ctx + eval_function_call_symbolic_from_inst_sig config func inst_sg generics + call.args call.dest cf ctx (** Evaluate a function call in symbolic mode by using the function signature. @@ -1354,8 +1354,8 @@ and eval_transparent_function_call_symbolic (config : C.config) (call : A.call) *) and eval_function_call_symbolic_from_inst_sig (config : C.config) (fid : A.fun_id_or_trait_method_ref) (inst_sg : A.inst_fun_sig) - (self_trait_ref : T.etrait_ref option) (generics : T.egeneric_args) - (args : E.operand list) (dest : E.place) : st_cm_fun = + (generics : T.egeneric_args) (args : E.operand list) (dest : E.place) : + st_cm_fun = fun cf ctx -> (* Generate a fresh symbolic value for the return value *) let ret_sv_ty = inst_sg.A.output in @@ -1526,7 +1526,7 @@ and eval_assumed_function_call_symbolic (config : C.config) (* Evaluate the function call *) eval_function_call_symbolic_from_inst_sig config (A.FunId (A.Assumed fid)) - inst_sig None generics args dest cf ctx + inst_sig generics args dest cf ctx (** Evaluate a statement seen as a function body *) and eval_function_body (config : C.config) (body : A.statement) : st_cm_fun = -- cgit v1.2.3 From 0f0e4be7dc746e2676db33f850bbeddf239eaec8 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Fri, 13 Oct 2023 00:40:37 +0200 Subject: Add sup --- compiler/InterpreterStatements.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'compiler/InterpreterStatements.ml') diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml index 42073f0b..36bc3492 100644 --- a/compiler/InterpreterStatements.ml +++ b/compiler/InterpreterStatements.ml @@ -646,7 +646,7 @@ let eval_assumed_function_call_concrete (config : C.config) eval_vec_function_concrete config fid generics | ArrayIndexShared | ArrayIndexMut | ArrayToSliceShared | ArrayToSliceMut | ArraySubsliceShared | ArraySubsliceMut - | SliceIndexShared | SliceIndexMut | SliceSubsliceShared + | ArrayRepeat | SliceIndexShared | SliceIndexMut | SliceSubsliceShared | SliceSubsliceMut | SliceLen -> raise (Failure "Unimplemented") in -- cgit v1.2.3 From f11d5186b467df318f7c09eedf8b5629c165b453 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Fri, 20 Oct 2023 15:05:00 +0200 Subject: Start updating to handle function pointers --- compiler/InterpreterStatements.ml | 78 ++++++++++++++++++++++----------------- 1 file changed, 44 insertions(+), 34 deletions(-) (limited to 'compiler/InterpreterStatements.ml') diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml index 36bc3492..9f35c6f2 100644 --- a/compiler/InterpreterStatements.ml +++ b/compiler/InterpreterStatements.ml @@ -306,7 +306,7 @@ let get_assumed_function_return_type (ctx : C.eval_ctx) (fid : A.assumed_fun_id) assert (generics.trait_refs = []); (* [Box::free] has a special treatment *) match fid with - | A.BoxFree -> + | BoxFree -> assert (generics.regions = []); assert (List.length generics.types = 1); assert (generics.const_generics = []); @@ -583,7 +583,7 @@ let eval_vec_function_concrete (_config : C.config) (_fid : A.assumed_fun_id) (** Evaluate a non-local function call in concrete mode *) let eval_assumed_function_call_concrete (config : C.config) (fid : A.assumed_fun_id) (call : A.call) : cm_fun = - let generics = call.generics in + let generics = call.func.generics in let args = call.args in let dest = call.dest in (* Sanity check: we don't fully handle the const generic vars environment @@ -595,7 +595,7 @@ let eval_assumed_function_call_concrete (config : C.config) See {!eval_box_free} *) match fid with - | A.BoxFree -> + | BoxFree -> (* Degenerate case: box_free *) eval_box_free config generics args dest | _ -> @@ -636,7 +636,7 @@ let eval_assumed_function_call_concrete (config : C.config) * access to a body. *) let cf_eval_body : cm_fun = match fid with - | A.Replace -> eval_replace_concrete config generics + | Replace -> eval_replace_concrete config generics | BoxNew -> eval_box_new_concrete config generics | BoxDeref -> eval_box_deref_concrete config generics | BoxDerefMut -> eval_box_deref_mut_concrete config generics @@ -854,15 +854,14 @@ and eval_global (config : C.config) (dest : E.place) (gid : LA.GlobalDeclId.id) match config.mode with | ConcreteMode -> (* Treat the evaluation of the global as a call to the global body (without arguments) *) - let call = + let func = { - A.func = A.FunId (A.Regular global.body_id); + E.func = FunId (Regular global.body_id); generics = TypesUtils.mk_empty_generic_args; trait_and_method_generic_args = None; - args = []; - dest; } in + let call = { A.func; args = []; dest } in (eval_transparent_function_call_concrete config global.body_id call) cf ctx | SymbolicMode -> @@ -1019,29 +1018,28 @@ and eval_function_call (config : C.config) (call : A.call) : st_cm_fun = and eval_function_call_concrete (config : C.config) (call : A.call) : st_cm_fun = fun cf ctx -> - match call.func with - | A.FunId (A.Regular fid) -> + match call.func.func with + | FunId (Regular fid) -> eval_transparent_function_call_concrete config fid call cf ctx - | A.FunId (A.Assumed fid) -> + | FunId (Assumed 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 fid call (cf Unit) ctx - | A.TraitMethod _ -> raise (Failure "Unimplemented") + | TraitMethod _ -> raise (Failure "Unimplemented") and eval_function_call_symbolic (config : C.config) (call : A.call) : st_cm_fun = - match call.func with - | A.FunId (A.Regular _) | A.TraitMethod _ -> + match call.func.func with + | FunId (Regular _) | TraitMethod _ -> eval_transparent_function_call_symbolic config call - | A.FunId (A.Assumed fid) -> - eval_assumed_function_call_symbolic config fid call + | FunId (Assumed fid) -> eval_assumed_function_call_symbolic config fid call (** Evaluate a local (i.e., non-assumed) function call in concrete mode *) and eval_transparent_function_call_concrete (config : C.config) (fid : A.FunDeclId.id) (call : A.call) : st_cm_fun = - let generics = call.A.generics in + let generics = call.func.generics in let args = call.A.args in let dest = call.A.dest in (* Sanity check: we don't fully handle the const generic vars environment @@ -1195,29 +1193,29 @@ and eval_transparent_function_call_symbolic (config : C.config) (call : A.call) to a trait clause but directly to the method provided in the trait declaration. *) let func, generics, def, inst_sg = - match call.func with - | A.FunId (A.Regular fid) -> + match call.func.func with + | FunId (Regular fid) -> let def = C.ctx_lookup_fun_decl ctx fid in let tr_self = T.UnknownTrait __FUNCTION__ in let inst_sg = - instantiate_fun_sig ctx call.generics tr_self def.A.signature + instantiate_fun_sig ctx call.func.generics tr_self def.A.signature in - (call.func, call.generics, def, inst_sg) - | A.FunId (A.Assumed _) -> + (call.func.func, call.func.generics, def, inst_sg) + | FunId (Assumed _) -> (* Unreachable: must be a transparent function *) raise (Failure "Unreachable") - | A.TraitMethod (trait_ref, method_name, _) -> ( + | TraitMethod (trait_ref, method_name, _) -> ( log#ldebug (lazy ("trait method call:\n- call: " ^ call_to_string ctx call ^ "\n- method name: " ^ method_name ^ "\n- call.generics:\n" - ^ egeneric_args_to_string ctx call.generics + ^ egeneric_args_to_string ctx call.func.generics ^ "\n- trait and method generics:\n" ^ egeneric_args_to_string ctx - (Option.get call.trait_and_method_generic_args))); + (Option.get call.func.trait_and_method_generic_args))); (* When instantiating, we need to group the generics for the trait ref and the method *) - let generics = Option.get call.trait_and_method_generic_args in + let generics = Option.get call.func.trait_and_method_generic_args in (* Lookup the trait method signature - there are several possibilities depending on whethere we call a top-level trait method impl or the method from a local clause *) @@ -1251,7 +1249,7 @@ and eval_transparent_function_call_symbolic (config : C.config) (call : A.call) which implements the method. In order to do this properly, we also need to update the generics. *) - let func = A.FunId (A.Regular id) in + let func = E.FunId (Regular id) in (func, generics, method_def, inst_sg) | None -> (* If not found, lookup the methods provided by the trait *declaration* @@ -1287,7 +1285,7 @@ and eval_transparent_function_call_symbolic (config : C.config) (call : A.call) *) let all_generics = TypesUtils.merge_generic_args - trait_ref.trait_decl_ref.decl_generics call.generics + trait_ref.trait_decl_ref.decl_generics call.func.generics in log#ldebug (lazy @@ -1304,7 +1302,7 @@ and eval_transparent_function_call_symbolic (config : C.config) (call : A.call) instantiate_fun_sig ctx all_generics tr_self method_def.A.signature in - (call.func, call.generics, method_def, inst_sg)) + (call.func.func, call.func.generics, method_def, inst_sg)) | _ -> (* We are using a local clause - we lookup the trait decl *) let trait_decl = @@ -1333,7 +1331,7 @@ and eval_transparent_function_call_symbolic (config : C.config) (call : A.call) let inst_sg = instantiate_fun_sig ctx generics tr_self method_def.A.signature in - (call.func, call.generics, method_def, inst_sg)) + (call.func.func, call.func.generics, method_def, inst_sg)) in (* Sanity check *) assert (List.length call.args = List.length def.A.signature.inputs); @@ -1357,6 +1355,18 @@ and eval_function_call_symbolic_from_inst_sig (config : C.config) (generics : T.egeneric_args) (args : E.operand list) (dest : E.place) : st_cm_fun = fun cf ctx -> + log#ldebug + (lazy + ("eval_function_call_symbolic_from_inst_sig:\n- fid: " + ^ fun_id_or_trait_method_ref_to_string ctx fid + ^ "\n- inst_sg:\n" + ^ inst_fun_sig_to_string ctx inst_sg + ^ "\n- call.generics:\n" + ^ egeneric_args_to_string ctx generics + ^ "\n- args:\n" + ^ String.concat ", " (List.map (operand_to_string ctx) args) + ^ "\n- dest:\n" ^ place_to_string ctx dest)); + (* Generate a fresh symbolic value for the return value *) let ret_sv_ty = inst_sg.A.output in let ret_spc = mk_fresh_symbolic_value V.FunCallRet ret_sv_ty in @@ -1487,7 +1497,7 @@ and eval_function_call_symbolic_from_inst_sig (config : C.config) and eval_assumed_function_call_symbolic (config : C.config) (fid : A.assumed_fun_id) (call : A.call) : st_cm_fun = fun cf ctx -> - let generics = call.generics in + let generics = call.func.generics in let args = call.args in let dest = call.dest in (* Sanity check: make sure the type parameters don't contain regions - @@ -1503,7 +1513,7 @@ and eval_assumed_function_call_symbolic (config : C.config) See {!eval_box_free} *) match fid with - | A.BoxFree -> + | 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 generics args dest (cf Unit) ctx @@ -1514,7 +1524,7 @@ and eval_assumed_function_call_symbolic (config : C.config) * instantiated signatures, and delegate the work to an auxiliary function *) let inst_sig = match fid with - | A.BoxFree -> + | BoxFree -> (* should have been treated above *) raise (Failure "Unreachable") | _ -> @@ -1525,7 +1535,7 @@ and eval_assumed_function_call_symbolic (config : C.config) in (* Evaluate the function call *) - eval_function_call_symbolic_from_inst_sig config (A.FunId (A.Assumed fid)) + eval_function_call_symbolic_from_inst_sig config (FunId (Assumed fid)) inst_sig generics args dest cf ctx (** Evaluate a statement seen as a function body *) -- cgit v1.2.3 From 838cc86cb2efc8fb64a94a94b58b82d66844e7e4 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Mon, 23 Oct 2023 13:47:39 +0200 Subject: Remove some assumed types and add more support for builtin definitions --- compiler/InterpreterStatements.ml | 100 +++----------------------------------- 1 file changed, 6 insertions(+), 94 deletions(-) (limited to 'compiler/InterpreterStatements.ml') diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml index 9f35c6f2..2aced79f 100644 --- a/compiler/InterpreterStatements.ml +++ b/compiler/InterpreterStatements.ml @@ -10,7 +10,6 @@ open TypesUtils open ValuesUtils module Inv = Invariants module S = SynthesizeSymbolic -open Utils open Cps open InterpreterUtils open InterpreterProjectors @@ -233,8 +232,7 @@ let set_discriminant (config : C.config) (p : E.place) let update_value cf (v : V.typed_value) : m_fun = fun ctx -> match (v.V.ty, v.V.value) with - | T.Adt (((T.AdtId _ | T.Assumed T.Option) as type_id), generics), V.Adt av - -> ( + | T.Adt ((T.AdtId _ as type_id), generics), V.Adt av -> ( (* There are two situations: - either the discriminant is already the proper one (in which case we don't do anything) @@ -253,24 +251,15 @@ let set_discriminant (config : C.config) (p : E.place) | T.AdtId def_id -> compute_expanded_bottom_adt_value ctx def_id (Some variant_id) generics - | T.Assumed T.Option -> - assert (generics.regions = []); - compute_expanded_bottom_option_value variant_id - (Collections.List.to_cons_nil generics.types) | _ -> raise (Failure "Unreachable") in assign_to_place config bottom_v p (cf Unit) ctx) - | T.Adt (((T.AdtId _ | T.Assumed T.Option) as type_id), generics), V.Bottom - -> + | T.Adt ((T.AdtId _ as type_id), generics), V.Bottom -> let bottom_v = match type_id with | T.AdtId def_id -> compute_expanded_bottom_adt_value ctx def_id (Some variant_id) generics - | T.Assumed T.Option -> - assert (generics.regions = []); - compute_expanded_bottom_option_value variant_id - (Collections.List.to_cons_nil generics.types) | _ -> raise (Failure "Unreachable") in assign_to_place config bottom_v p (cf Unit) ctx @@ -313,7 +302,7 @@ let get_assumed_function_return_type (ctx : C.eval_ctx) (fid : A.assumed_fun_id) mk_unit_ty | _ -> (* Retrieve the function's signature *) - let sg = Assumed.get_assumed_sig fid in + let sg = Assumed.get_assumed_fun_sig fid in (* Instantiate the return type *) (* There shouldn't be any reference to Self *) let tr_self : T.erased_region T.trait_instance_id = @@ -426,11 +415,6 @@ let pop_frame_assign (config : C.config) (dest : E.place) : cm_fun = in comp cf_pop cf_assign -(** Auxiliary function - see {!eval_assumed_function_call} *) -let eval_replace_concrete (_config : C.config) (_generics : T.egeneric_args) : - cm_fun = - fun _cf _ctx -> raise Unimplemented - (** Auxiliary function - see {!eval_assumed_function_call} *) let eval_box_new_concrete (config : C.config) (generics : T.egeneric_args) : cm_fun = @@ -475,67 +459,6 @@ let eval_box_new_concrete (config : C.config) (generics : T.egeneric_args) : comp cf_move cf_create cf ctx | _ -> raise (Failure "Inconsistent state") -(** Auxiliary function which factorizes code to evaluate [std::Deref::deref] - and [std::DerefMut::deref_mut] - see {!eval_assumed_function_call} *) -let eval_box_deref_mut_or_shared_concrete (config : C.config) - (generics : T.egeneric_args) (is_mut : bool) : cm_fun = - fun cf ctx -> - (* Check the arguments *) - match - (generics.regions, generics.types, generics.const_generics, ctx.env) - with - | ( [], - [ boxed_ty ], - [], - Var (VarBinder input_var, input_value) - :: Var (_ret_var, _) - :: C.Frame :: _ ) -> - (* Required type checking. We must have: - - input_value.ty = & (mut) Box - - boxed_ty = ty - for some ty - *) - (let _, input_ty, ref_kind = ty_get_ref input_value.V.ty in - assert (match ref_kind with T.Shared -> not is_mut | T.Mut -> is_mut); - let input_ty = ty_get_box input_ty in - assert (input_ty = boxed_ty)); - - (* Borrow the boxed value *) - let p = - { E.var_id = input_var.C.index; projection = [ E.Deref; E.DerefBox ] } - in - let borrow_kind = if is_mut then E.Mut else E.Shared in - let rv = E.RvRef (p, borrow_kind) in - let cf_borrow = eval_rvalue_not_global config rv in - - (* Move the borrow to its destination *) - let cf_move cf res : m_fun = - match res with - | Error EPanic -> - (* We can't get there by borrowing a value *) - raise (Failure "Unreachable") - | Ok borrowed_value -> - (* Move and continue *) - let destp = mk_place_from_var_id E.VarId.zero in - assign_to_place config borrowed_value destp cf - in - - (* Compose and apply *) - comp cf_borrow cf_move cf ctx - | _ -> raise (Failure "Inconsistent state") - -(** Auxiliary function - see {!eval_assumed_function_call} *) -let eval_box_deref_concrete (config : C.config) (generics : T.egeneric_args) : - cm_fun = - let is_mut = false in - eval_box_deref_mut_or_shared_concrete config generics is_mut - -(** Auxiliary function - see {!eval_assumed_function_call} *) -let eval_box_deref_mut_concrete (config : C.config) (generics : T.egeneric_args) - : cm_fun = - let is_mut = true in - eval_box_deref_mut_or_shared_concrete config generics is_mut - (** Auxiliary function - see {!eval_assumed_function_call}. [Box::free] is not handled the same way as the other assumed functions: @@ -575,11 +498,6 @@ let eval_box_free (config : C.config) (generics : T.egeneric_args) cc cf ctx | _ -> raise (Failure "Inconsistent state") -(** Auxiliary function - see {!eval_assumed_function_call} *) -let eval_vec_function_concrete (_config : C.config) (_fid : A.assumed_fun_id) - (_generics : T.egeneric_args) : cm_fun = - fun _cf _ctx -> raise Unimplemented - (** Evaluate a non-local function call in concrete mode *) let eval_assumed_function_call_concrete (config : C.config) (fid : A.assumed_fun_id) (call : A.call) : cm_fun = @@ -636,18 +554,12 @@ let eval_assumed_function_call_concrete (config : C.config) * access to a body. *) let cf_eval_body : cm_fun = match fid with - | Replace -> eval_replace_concrete config generics | BoxNew -> eval_box_new_concrete config generics - | BoxDeref -> eval_box_deref_concrete config generics - | BoxDerefMut -> eval_box_deref_mut_concrete config generics | BoxFree -> (* Should have been treated above *) raise (Failure "Unreachable") - | VecNew | VecPush | VecInsert | VecLen | VecIndex | VecIndexMut -> - eval_vec_function_concrete config fid generics | ArrayIndexShared | ArrayIndexMut | ArrayToSliceShared - | ArrayToSliceMut | ArraySubsliceShared | ArraySubsliceMut - | ArrayRepeat | SliceIndexShared | SliceIndexMut | SliceSubsliceShared - | SliceSubsliceMut | SliceLen -> + | ArrayToSliceMut | ArrayRepeat | SliceIndexShared | SliceIndexMut + | SliceLen -> raise (Failure "Unimplemented") in @@ -1531,7 +1443,7 @@ and eval_assumed_function_call_symbolic (config : C.config) (* There shouldn't be any reference to Self *) let tr_self = T.UnknownTrait __FUNCTION__ in instantiate_fun_sig ctx generics tr_self - (Assumed.get_assumed_sig fid) + (Assumed.get_assumed_fun_sig fid) in (* Evaluate the function call *) -- cgit v1.2.3 From dc18bb9eed7615bd2fcfa240011f2e41eea4b874 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Tue, 24 Oct 2023 11:15:46 +0200 Subject: Add some debugging information --- compiler/InterpreterStatements.ml | 7 +++++++ 1 file changed, 7 insertions(+) (limited to 'compiler/InterpreterStatements.ml') diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml index 2aced79f..e0c4703b 100644 --- a/compiler/InterpreterStatements.ml +++ b/compiler/InterpreterStatements.ml @@ -1108,6 +1108,13 @@ and eval_transparent_function_call_symbolic (config : C.config) (call : A.call) match call.func.func with | FunId (Regular fid) -> let def = C.ctx_lookup_fun_decl ctx fid in + log#ldebug + (lazy + ("fun call:\n- call: " ^ call_to_string ctx call + ^ "\n- call.generics:\n" + ^ egeneric_args_to_string ctx call.func.generics + ^ "\n- def.signature:\n" + ^ fun_sig_to_string ctx def.A.signature)); let tr_self = T.UnknownTrait __FUNCTION__ in let inst_sg = instantiate_fun_sig ctx call.func.generics tr_self def.A.signature -- cgit v1.2.3