diff options
45 files changed, 366 insertions, 497 deletions
@@ -13,6 +13,7 @@ - A "default" case can now appear anywhere in a "switch", not just as the last case. - Revised parsing of command-line options, more GCC-like. +- Simpler and more robust handling of calls to variadic functions. Release 2.1, 2013-10-28 ======================= diff --git a/arm/PrintAsm.ml b/arm/PrintAsm.ml index c0e2687..7007467 100644 --- a/arm/PrintAsm.ml +++ b/arm/PrintAsm.ml @@ -39,12 +39,8 @@ let label_for_label lbl = (* Basic printing functions *) -let strip_variadic_suffix name = - try String.sub name 0 (String.index name '$') - with Not_found -> name - let print_symb oc symb = - fprintf oc "%s" (strip_variadic_suffix (extern_atom symb)) + fprintf oc "%s" (extern_atom symb) let print_label oc lbl = fprintf oc ".L%d" (label_for_label lbl) diff --git a/backend/CMparser.mly b/backend/CMparser.mly index b28578e..5d93b84 100644 --- a/backend/CMparser.mly +++ b/backend/CMparser.mly @@ -490,9 +490,9 @@ proc: signature: type_ - { {sig_args = []; sig_res = Some $1} } + { {sig_args = []; sig_res = Some $1; sig_cc = cc_default} } | VOID - { {sig_args = []; sig_res = None} } + { {sig_args = []; sig_res = None; sig_cc = cc_default} } | type_ MINUSGREATER signature { let s = $3 in {s with sig_args = $1 :: s.sig_args} } ; diff --git a/backend/Cminor.v b/backend/Cminor.v index 9f7244b..c12c6fc 100644 --- a/backend/Cminor.v +++ b/backend/Cminor.v @@ -532,7 +532,7 @@ Inductive initial_state (p: program): state -> Prop := Genv.init_mem p = Some m0 -> Genv.find_symbol ge p.(prog_main) = Some b -> Genv.find_funct_ptr ge b = Some f -> - funsig f = mksignature nil (Some Tint) -> + funsig f = signature_main -> initial_state p (Callstate f nil Kstop m0). (** A final state is a [Returnstate] with an empty continuation. *) @@ -811,7 +811,7 @@ Inductive bigstep_program_terminates (p: program): trace -> int -> Prop := Genv.init_mem p = Some m0 -> Genv.find_symbol ge p.(prog_main) = Some b -> Genv.find_funct_ptr ge b = Some f -> - funsig f = mksignature nil (Some Tint) -> + funsig f = signature_main -> eval_funcall ge m0 f nil t m (Vint r) -> bigstep_program_terminates p t r. @@ -822,7 +822,7 @@ Inductive bigstep_program_diverges (p: program): traceinf -> Prop := Genv.init_mem p = Some m0 -> Genv.find_symbol ge p.(prog_main) = Some b -> Genv.find_funct_ptr ge b = Some f -> - funsig f = mksignature nil (Some Tint) -> + funsig f = signature_main -> evalinf_funcall ge m0 f nil t -> bigstep_program_diverges p t. diff --git a/backend/CminorSel.v b/backend/CminorSel.v index c80f424..db414a2 100644 --- a/backend/CminorSel.v +++ b/backend/CminorSel.v @@ -390,7 +390,7 @@ Inductive initial_state (p: program): state -> Prop := Genv.init_mem p = Some m0 -> Genv.find_symbol ge p.(prog_main) = Some b -> Genv.find_funct_ptr ge b = Some f -> - funsig f = mksignature nil (Some Tint) -> + funsig f = signature_main -> initial_state p (Callstate f nil Kstop m0). Inductive final_state: state -> int -> Prop := diff --git a/backend/LTL.v b/backend/LTL.v index e60600a..dd79c8e 100644 --- a/backend/LTL.v +++ b/backend/LTL.v @@ -295,12 +295,12 @@ Inductive initial_state (p: program): state -> Prop := Genv.init_mem p = Some m0 -> Genv.find_symbol ge p.(prog_main) = Some b -> Genv.find_funct_ptr ge b = Some f -> - funsig f = mksignature nil (Some Tint) -> + funsig f = signature_main -> initial_state p (Callstate nil f (Locmap.init Vundef) m0). Inductive final_state: state -> int -> Prop := | final_state_intro: forall rs m r retcode, - loc_result (mksignature nil (Some Tint)) = r :: nil -> + loc_result signature_main = r :: nil -> rs (R r) = Vint retcode -> final_state (Returnstate nil rs m) retcode. diff --git a/backend/Linear.v b/backend/Linear.v index 3c52436..56d1eb9 100644 --- a/backend/Linear.v +++ b/backend/Linear.v @@ -269,12 +269,12 @@ Inductive initial_state (p: program): state -> Prop := Genv.init_mem p = Some m0 -> Genv.find_symbol ge p.(prog_main) = Some b -> Genv.find_funct_ptr ge b = Some f -> - funsig f = mksignature nil (Some Tint) -> + funsig f = signature_main -> initial_state p (Callstate nil f (Locmap.init Vundef) m0). Inductive final_state: state -> int -> Prop := | final_state_intro: forall rs m r retcode, - loc_result (mksignature nil (Some Tint)) = r :: nil -> + loc_result signature_main = r :: nil -> rs (R r) = Vint retcode -> final_state (Returnstate nil rs m) retcode. diff --git a/backend/Mach.v b/backend/Mach.v index f0fb56a..ff72a82 100644 --- a/backend/Mach.v +++ b/backend/Mach.v @@ -427,7 +427,7 @@ Inductive initial_state (p: program): state -> Prop := Inductive final_state: state -> int -> Prop := | final_state_intro: forall rs m r retcode, - loc_result (mksignature nil (Some Tint)) = r :: nil -> + loc_result signature_main = r :: nil -> rs r = Vint retcode -> final_state (Returnstate nil rs m) retcode. diff --git a/backend/PrintCminor.ml b/backend/PrintCminor.ml index 33c38f5..4c53c5e 100644 --- a/backend/PrintCminor.ml +++ b/backend/PrintCminor.ml @@ -172,12 +172,13 @@ let name_of_type = function | Tlong -> "long" | Tsingle -> "single" -let rec print_sig p = function - | {sig_args = []; sig_res = None} -> fprintf p "void" - | {sig_args = []; sig_res = Some ty} -> fprintf p "%s" (name_of_type ty) - | {sig_args = t1 :: tl; sig_res = tres} -> - fprintf p "%s ->@ " (name_of_type t1); - print_sig p {sig_args = tl; sig_res = tres} +let print_sig p sg = + List.iter + (fun t -> fprintf p "%s ->@ " (name_of_type t)) + sg.sig_args; + match sg.sig_res with + | None -> fprintf p "void" + | Some ty -> fprintf p "%s" (name_of_type ty) let rec just_skips s = match s with diff --git a/backend/RTL.v b/backend/RTL.v index b2e1e89..045250d 100644 --- a/backend/RTL.v +++ b/backend/RTL.v @@ -331,7 +331,7 @@ Inductive initial_state (p: program): state -> Prop := Genv.init_mem p = Some m0 -> Genv.find_symbol ge p.(prog_main) = Some b -> Genv.find_funct_ptr ge b = Some f -> - funsig f = mksignature nil (Some Tint) -> + funsig f = signature_main -> initial_state p (Callstate nil f nil m0). (** A final state is a [Returnstate] with an empty call stack. *) diff --git a/backend/SelectLong.vp b/backend/SelectLong.vp index 76cc79d..09f29af 100644 --- a/backend/SelectLong.vp +++ b/backend/SelectLong.vp @@ -46,13 +46,13 @@ Record helper_functions : Type := mk_helper_functions { i64_sar: ident (**r shift right signed *) }. -Definition sig_l_l := mksignature (Tlong :: nil) (Some Tlong). -Definition sig_l_f := mksignature (Tlong :: nil) (Some Tfloat). -Definition sig_l_s := mksignature (Tlong :: nil) (Some Tsingle). -Definition sig_f_l := mksignature (Tfloat :: nil) (Some Tlong). -Definition sig_ll_l := mksignature (Tlong :: Tlong :: nil) (Some Tlong). -Definition sig_li_l := mksignature (Tlong :: Tint :: nil) (Some Tlong). -Definition sig_ii_l := mksignature (Tint :: Tint :: nil) (Some Tlong). +Definition sig_l_l := mksignature (Tlong :: nil) (Some Tlong) cc_default. +Definition sig_l_f := mksignature (Tlong :: nil) (Some Tfloat) cc_default. +Definition sig_l_s := mksignature (Tlong :: nil) (Some Tsingle) cc_default. +Definition sig_f_l := mksignature (Tfloat :: nil) (Some Tlong) cc_default. +Definition sig_ll_l := mksignature (Tlong :: Tlong :: nil) (Some Tlong) cc_default. +Definition sig_li_l := mksignature (Tlong :: Tint :: nil) (Some Tlong) cc_default. +Definition sig_ii_l := mksignature (Tint :: Tint :: nil) (Some Tlong) cc_default. Section SELECT. diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index f12efa3..4cac92c 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -143,39 +143,6 @@ let globals_for_strings globs = (fun s id l -> global_for_string s id :: l) stringTable globs -(** ** Declaration of special external functions *) - -let special_externals_table : (string, fundef) Hashtbl.t = Hashtbl.create 47 - -let register_special_external name ef targs tres = - if not (Hashtbl.mem special_externals_table name) then - Hashtbl.add special_externals_table name (External(ef, targs, tres)) - -let declare_special_externals k = - Hashtbl.fold - (fun name fd k -> (intern_string name, Gfun fd) :: k) - special_externals_table k - -(** ** Handling of stubs for variadic functions *) - -let register_stub_function name tres targs = - let rec letters_of_type = function - | Tnil -> [] - | Tcons(Tfloat _, tl) -> "f" :: letters_of_type tl - | Tcons(Tlong _, tl) -> "l" :: letters_of_type tl - | Tcons(_, tl) -> "i" :: letters_of_type tl in - let rec types_of_types = function - | Tnil -> Tnil - | Tcons(Tfloat _, tl) -> Tcons(Tfloat(F64, noattr), types_of_types tl) - | Tcons(Tlong _, tl) -> Tcons(Tlong(Signed, noattr), types_of_types tl) - | Tcons(_, tl) -> Tcons(Tpointer(Tvoid, noattr), types_of_types tl) in - let stub_name = - name ^ "$" ^ String.concat "" (letters_of_type targs) in - let targs = types_of_types targs in - let ef = EF_external(intern_string stub_name, signature_of_type targs tres) in - register_special_external stub_name ef targs tres; - (stub_name, Tfunction (targs, tres)) - (** ** Handling of inlined memcpy functions *) let make_builtin_memcpy args = @@ -230,11 +197,16 @@ let mergeTypAttr ty a2 = | Tlong(sg, a1) -> Tlong(sg, mergeAttr a1 a2) | Tpointer(ty', a1) -> Tpointer(ty', mergeAttr a1 a2) | Tarray(ty', sz, a1) -> Tarray(ty', sz, mergeAttr a1 a2) - | Tfunction(targs, tres) -> ty + | Tfunction(targs, tres, cc) -> ty | Tstruct(id, fld, a1) -> Tstruct(id, fld, mergeAttr a1 a2) | Tunion(id, fld, a1) -> Tunion(id, fld, mergeAttr a1 a2) | Tcomp_ptr(id, a1) -> Tcomp_ptr(id, mergeAttr a1 a2) +let convertCallconv va attr = + let sr = + Cutil.find_custom_attributes ["structreturn"; "__structreturn"] attr in + { cc_vararg = va; cc_structret = sr <> [] } + (** Types *) let convertIkind = function @@ -293,14 +265,15 @@ let convertTyp env t = | C.TArray(ty, Some sz, a) -> Tarray(convertTyp seen ty, convertInt sz, convertAttr a) | C.TFun(tres, targs, va, a) -> - if va then unsupported "variadic function type"; + (* if va then unsupported "variadic function type"; *) if Cutil.is_composite_type env tres then unsupported "return type is a struct or union"; Tfunction(begin match targs with | None -> (*warning "un-prototyped function type";*) Tnil | Some tl -> convertParams seen tl end, - convertTyp seen tres) + convertTyp seen tres, + convertCallconv va a) | C.TNamed _ -> assert false | C.TStruct(id, a) -> @@ -347,9 +320,20 @@ let convertTyp env t = in convertTyp [] t +(* let rec convertTypList env = function | [] -> Tnil | t1 :: tl -> Tcons(convertTyp env t1, convertTypList env tl) +*) + +let rec convertTypArgs env tl el = + match tl, el with + | _, [] -> Tnil + | [], e1 :: el -> + Tcons(convertTyp env (Cutil.default_argument_conversion env e1.etyp), + convertTypArgs env [] el) + | (id, t1) :: tl, e1 :: el -> + Tcons(convertTyp env t1, convertTypArgs env tl el) let cacheCompositeDef env su id attr flds = let ty = @@ -358,12 +342,6 @@ let cacheCompositeDef env su id attr flds = | C.Union -> C.TUnion(id, attr) in Hashtbl.add compositeCache id (convertTyp env ty) -let rec projFunType env ty = - match Cutil.unroll env ty with - | TFun(res, args, vararg, attr) -> Some(res, args, vararg) - | TPtr(ty', attr) -> projFunType env ty' - | _ -> None - let string_of_type ty = let b = Buffer.create 20 in let fb = Format.formatter_of_buffer b in @@ -544,10 +522,7 @@ let rec convertExpr env e = | C.ECall({edesc = C.EVar {name = "__builtin_annot"}}, args) -> begin match args with | {edesc = C.EConst(CStr txt)} :: args1 -> - let targs1 = - convertTypList env - (List.map (fun e -> Cutil.default_argument_conversion env e.etyp) - args1) in + let targs1 = convertTypArgs env [] args1 in Ebuiltin( EF_annot(intern_string txt, List.map (fun t -> AA_arg t) (typlist_of_typelist targs1)), @@ -575,36 +550,19 @@ let rec convertExpr env e = | C.ECall({edesc = C.EVar {name = "__builtin_fabs"}}, [arg]) -> Eunop(Oabsfloat, convertExpr env arg, ty) + | C.ECall({edesc = C.EVar {name = "printf"}}, args) + when !Clflags.option_interp -> + let targs = + convertTypArgs env [] args in + let sg = + signature_of_type targs ty {cc_vararg = true; cc_structret = false} in + Ebuiltin(EF_external(intern_string "printf", sg), + targs, convertExprList env args, ty) + | C.ECall(fn, args) -> if not (supported_return_type env e.etyp) then unsupported ("function returning a result of type " ^ string_of_type e.etyp); - match projFunType env fn.etyp with - | None -> - error "wrong type for function part of a call"; ezero - | Some(tres, targs, false) -> - (* Non-variadic function *) - if targs = None then - unsupported "call to non-prototyped function"; - Ecall(convertExpr env fn, convertExprList env args, ty) - | Some(tres, targs, true) -> - (* Variadic function: generate a call to a stub function with - the appropriate number and types of arguments. Works only if - the function expression e is a global variable. *) - let fun_name = - match fn with - | {edesc = C.EVar id} when !Clflags.option_fvararg_calls -> - (*warning "emulating call to variadic function"; *) - id.name - | _ -> - unsupported "call to variadic function"; - "<error>" in - let targs = convertTypList env (List.map (fun e -> e.etyp) args) in - let tres = convertTyp env tres in - let (stub_fun_name, stub_fun_typ) = - register_stub_function fun_name tres targs in - Ecall(Evalof(Evar(intern_string stub_fun_name, stub_fun_typ), - stub_fun_typ), - convertExprList env args, ty) + Ecall(convertExpr env fn, convertExprList env args, ty) and convertLvalue env e = let ty = convertTyp env e.etyp in @@ -787,25 +745,28 @@ let convertFundef loc env fd = a_access = Sections.Access_default; a_inline = fd.fd_inline; a_loc = loc }; - (id', Gfun(Internal {fn_return = ret; fn_params = params; - fn_vars = vars; fn_body = body'})) + (id', Gfun(Internal {fn_return = ret; + fn_callconv = convertCallconv fd.fd_vararg fd.fd_attrib; + fn_params = params; + fn_vars = vars; + fn_body = body'})) (** External function declaration *) let convertFundecl env (sto, id, ty, optinit) = - let (args, res) = + let (args, res, cconv) = match convertTyp env ty with - | Tfunction(args, res) -> (args, res) + | Tfunction(args, res, cconv) -> (args, res, cconv) | _ -> assert false in let id' = intern_string id.name in - let sg = signature_of_type args res in + let sg = signature_of_type args res cconv in let ef = if id.name = "malloc" then EF_malloc else if id.name = "free" then EF_free else if List.mem_assoc id.name builtins.functions then EF_builtin(id', sg) else EF_external(id', sg) in - (id', Gfun(External(ef, args, res))) + (id', Gfun(External(ef, args, res, cconv))) (** Initializers *) @@ -894,16 +855,13 @@ let rec convertGlobdecls env res gl = match g.gdesc with | C.Gdecl((sto, id, ty, optinit) as d) -> (* Prototyped functions become external declarations. - Variadic functions are skipped. Other types become variable declarations. *) begin match Cutil.unroll env ty with - | TFun(_, Some _, false, _) -> + | TFun(_, Some _, _, _) -> convertGlobdecls env (convertFundecl env d :: res) gl' - | TFun(_, None, false, _) -> + | TFun(_, None, _, _) -> unsupported ("'" ^ id.name ^ "' is declared without a function prototype"); convertGlobdecls env res gl' - | TFun(_, _, true, _) -> - convertGlobdecls env res gl' | _ -> convertGlobdecls env (convertGlobvar g.gloc env d :: res) gl' end @@ -1002,15 +960,13 @@ let convertProgram p = Hashtbl.clear decl_atom; Hashtbl.clear stringTable; Hashtbl.clear compositeCache; - Hashtbl.clear special_externals_table; let p = Builtins.declarations() @ p in try let gl1 = convertGlobdecls (translEnv Env.empty p) [] (cleanupGlobals p) in - let gl2 = declare_special_externals gl1 in - let gl3 = globals_for_strings gl2 in + let gl2 = globals_for_strings gl1 in if !numErrors > 0 then None - else Some { AST.prog_defs = gl3; + else Some { AST.prog_defs = gl2; AST.prog_main = intern_string "main" } with Env.Error msg -> error (Env.error_message msg); None diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v index 79dd26f..9593afd 100644 --- a/cfrontend/Cexec.v +++ b/cfrontend/Cexec.v @@ -887,10 +887,10 @@ Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr := match is_val r1, is_val_list rargs with | Some(vf, tyf), Some vtl => match classify_fun tyf with - | fun_case_f tyargs tyres => + | fun_case_f tyargs tyres cconv => do fd <- Genv.find_funct ge vf; do vargs <- sem_cast_arguments vtl tyargs; - check type_eq (type_of_fundef fd) (Tfunction tyargs tyres); + check type_eq (type_of_fundef fd) (Tfunction tyargs tyres cconv); topred (Callred fd vargs ty m) | _ => stuck end @@ -1020,14 +1020,14 @@ Definition invert_expr_prop (a: expr) (m: mem) : Prop := exists v, sem_cast v1 ty1 ty = Some v | Ecall (Eval vf tyf) rargs ty => exprlist_all_values rargs -> - exists tyargs, exists tyres, exists fd, exists vl, - classify_fun tyf = fun_case_f tyargs tyres + exists tyargs tyres cconv fd vl, + classify_fun tyf = fun_case_f tyargs tyres cconv /\ Genv.find_funct ge vf = Some fd /\ cast_arguments rargs tyargs vl - /\ type_of_fundef fd = Tfunction tyargs tyres + /\ type_of_fundef fd = Tfunction tyargs tyres cconv | Ebuiltin ef tyargs rargs ty => exprlist_all_values rargs -> - exists vargs, exists t, exists vres, exists m', exists w', + exists vargs t vres m' w', cast_arguments rargs tyargs vargs /\ external_call ef ge vargs m t vres m' /\ possible_trace w t w' @@ -1069,7 +1069,7 @@ Lemma callred_invert: invert_expr_prop r m. Proof. intros. inv H. simpl. - intros. exists tyargs; exists tyres; exists fd; exists args; auto. + intros. exists tyargs, tyres, cconv, fd, args; auto. Qed. Scheme context_ind2 := Minimality for context Sort Prop @@ -1513,10 +1513,10 @@ Proof with (try (apply not_invert_ok; simpl; intro; myinv; intuition congruence; destruct (is_val_list rargs) as [vtl | ] eqn:?. rewrite (is_val_inv _ _ _ Heqo). exploit is_val_list_all_values; eauto. intros ALLVAL. (* top *) - destruct (classify_fun tyf) as [tyargs tyres|] eqn:?... + destruct (classify_fun tyf) as [tyargs tyres cconv|] eqn:?... destruct (Genv.find_funct ge vf) as [fd|] eqn:?... destruct (sem_cast_arguments vtl tyargs) as [vargs|] eqn:?... - destruct (type_eq (type_of_fundef fd) (Tfunction tyargs tyres))... + destruct (type_eq (type_of_fundef fd) (Tfunction tyargs tyres cconv))... apply topred_ok; auto. red. split; auto. eapply red_Ecall; eauto. eapply sem_cast_arguments_sound; eauto. apply not_invert_ok; simpl; intros; myinv. specialize (H ALLVAL). myinv. congruence. @@ -2049,7 +2049,7 @@ Definition do_step (w: world) (s: state) : list (trace * state) := let (e,m1) := do_alloc_variables empty_env m (f.(fn_params) ++ f.(fn_vars)) in do m2 <- sem_bind_parameters w e m1 f.(fn_params) vargs; ret (State f f.(fn_body) k e m2) - | Callstate (External ef _ _) vargs k m => + | Callstate (External ef _ _ _) vargs k m => match do_external ef w vargs m with | None => nil | Some(w',t,v,m') => (t, Returnstate v k m') :: nil @@ -2215,7 +2215,7 @@ Definition do_initial_state (p: program): option (genv * state) := do m0 <- Genv.init_mem p; do b <- Genv.find_symbol ge p.(prog_main); do f <- Genv.find_funct_ptr ge b; - check (type_eq (type_of_fundef f) (Tfunction Tnil type_int32s)); + check (type_eq (type_of_fundef f) (Tfunction Tnil type_int32s cc_default)); Some (ge, Callstate f nil Kstop m0). Definition at_final_state (S: state): option int := diff --git a/cfrontend/Clight.v b/cfrontend/Clight.v index 137decc..f402ac2 100644 --- a/cfrontend/Clight.v +++ b/cfrontend/Clight.v @@ -132,6 +132,7 @@ Definition Sfor (s1: statement) (e2: expr) (s3: statement) (s4: statement) := Record function : Type := mkfunction { fn_return: type; + fn_callconv: calling_convention; fn_params: list (ident * type); fn_vars: list (ident * type); fn_temps: list (ident * type); @@ -146,17 +147,17 @@ Definition var_names (vars: list(ident * type)) : list ident := Inductive fundef : Type := | Internal: function -> fundef - | External: external_function -> typelist -> type -> fundef. + | External: external_function -> typelist -> type -> calling_convention -> fundef. (** The type of a function definition. *) Definition type_of_function (f: function) : type := - Tfunction (type_of_params (fn_params f)) (fn_return f). + Tfunction (type_of_params (fn_params f)) (fn_return f) (fn_callconv f). Definition type_of_fundef (f: fundef) : type := match f with | Internal fd => type_of_function fd - | External id args res => Tfunction args res + | External id args res cc => Tfunction args res cc end. (** ** Programs *) @@ -556,12 +557,12 @@ Inductive step: state -> trace -> state -> Prop := step (State f (Sset id a) k e le m) E0 (State f Sskip k e (PTree.set id v le) m) - | step_call: forall f optid a al k e le m tyargs tyres vf vargs fd, - classify_fun (typeof a) = fun_case_f tyargs tyres -> + | step_call: forall f optid a al k e le m tyargs tyres cconv vf vargs fd, + classify_fun (typeof a) = fun_case_f tyargs tyres cconv -> eval_expr e le m a vf -> eval_exprlist e le m al tyargs vargs -> Genv.find_funct ge vf = Some fd -> - type_of_fundef fd = Tfunction tyargs tyres -> + type_of_fundef fd = Tfunction tyargs tyres cconv -> step (State f (Scall optid a al) k e le m) E0 (Callstate fd vargs (Kcall optid f e le k) m) @@ -649,9 +650,9 @@ Inductive step: state -> trace -> state -> Prop := step (Callstate (Internal f) vargs k m) E0 (State f f.(fn_body) k e le m1) - | step_external_function: forall ef targs tres vargs k m vres t m', + | step_external_function: forall ef targs tres cconv vargs k m vres t m', external_call ef ge vargs m t vres m' -> - step (Callstate (External ef targs tres) vargs k m) + step (Callstate (External ef targs tres cconv) vargs k m) t (Returnstate vres k m') | step_returnstate: forall v optid f e le k m, @@ -671,7 +672,7 @@ Inductive initial_state (p: program): state -> Prop := Genv.init_mem p = Some m0 -> Genv.find_symbol ge p.(prog_main) = Some b -> Genv.find_funct_ptr ge b = Some f -> - type_of_fundef f = Tfunction Tnil type_int32s -> + type_of_fundef f = Tfunction Tnil type_int32s cc_default -> initial_state p (Callstate f nil Kstop m0). (** A final state is a [Returnstate] with an empty continuation. *) diff --git a/cfrontend/ClightBigstep.v b/cfrontend/ClightBigstep.v index 4d10c62..f7a0e18 100644 --- a/cfrontend/ClightBigstep.v +++ b/cfrontend/ClightBigstep.v @@ -89,12 +89,12 @@ Inductive exec_stmt: env -> temp_env -> mem -> statement -> trace -> temp_env -> eval_expr ge e le m a v -> exec_stmt e le m (Sset id a) E0 (PTree.set id v le) m Out_normal - | exec_Scall: forall e le m optid a al tyargs tyres vf vargs f t m' vres, - classify_fun (typeof a) = fun_case_f tyargs tyres -> + | exec_Scall: forall e le m optid a al tyargs tyres cconv vf vargs f t m' vres, + classify_fun (typeof a) = fun_case_f tyargs tyres cconv -> eval_expr ge e le m a vf -> eval_exprlist ge e le m al tyargs vargs -> Genv.find_funct ge vf = Some f -> - type_of_fundef f = Tfunction tyargs tyres -> + type_of_fundef f = Tfunction tyargs tyres cconv -> eval_funcall m f vargs t m' vres -> exec_stmt e le m (Scall optid a al) t (set_opttemp optid vres le) m' Out_normal @@ -170,9 +170,9 @@ with eval_funcall: mem -> fundef -> list val -> trace -> mem -> val -> Prop := outcome_result_value out f.(fn_return) vres -> Mem.free_list m3 (blocks_of_env e) = Some m4 -> eval_funcall m (Internal f) vargs t m4 vres - | eval_funcall_external: forall m ef targs tres vargs t vres m', + | eval_funcall_external: forall m ef targs tres cconv vargs t vres m', external_call ef ge vargs m t vres m' -> - eval_funcall m (External ef targs tres) vargs t m' vres. + eval_funcall m (External ef targs tres cconv) vargs t m' vres. Scheme exec_stmt_ind2 := Minimality for exec_stmt Sort Prop with eval_funcall_ind2 := Minimality for eval_funcall Sort Prop. @@ -186,12 +186,12 @@ Combined Scheme exec_stmt_funcall_ind from exec_stmt_ind2, eval_funcall_ind2. trace of observable events performed during the execution. *) CoInductive execinf_stmt: env -> temp_env -> mem -> statement -> traceinf -> Prop := - | execinf_Scall: forall e le m optid a al vf tyargs tyres vargs f t, - classify_fun (typeof a) = fun_case_f tyargs tyres -> + | execinf_Scall: forall e le m optid a al vf tyargs tyres cconv vargs f t, + classify_fun (typeof a) = fun_case_f tyargs tyres cconv -> eval_expr ge e le m a vf -> eval_exprlist ge e le m al tyargs vargs -> Genv.find_funct ge vf = Some f -> - type_of_fundef f = Tfunction tyargs tyres -> + type_of_fundef f = Tfunction tyargs tyres cconv -> evalinf_funcall m f vargs t -> execinf_stmt e le m (Scall optid a al) t | execinf_Sseq_1: forall e le m s1 s2 t, @@ -246,7 +246,7 @@ Inductive bigstep_program_terminates (p: program): trace -> int -> Prop := Genv.init_mem p = Some m0 -> Genv.find_symbol ge p.(prog_main) = Some b -> Genv.find_funct_ptr ge b = Some f -> - type_of_fundef f = Tfunction Tnil type_int32s -> + type_of_fundef f = Tfunction Tnil type_int32s cc_default -> eval_funcall ge m0 f nil t m1 (Vint r) -> bigstep_program_terminates p t r. @@ -256,7 +256,7 @@ Inductive bigstep_program_diverges (p: program): traceinf -> Prop := Genv.init_mem p = Some m0 -> Genv.find_symbol ge p.(prog_main) = Some b -> Genv.find_funct_ptr ge b = Some f -> - type_of_fundef f = Tfunction Tnil type_int32s -> + type_of_fundef f = Tfunction Tnil type_int32s cc_default -> evalinf_funcall ge m0 f nil t -> bigstep_program_diverges p t. diff --git a/cfrontend/Cop.v b/cfrontend/Cop.v index 31643a9..fec540b 100644 --- a/cfrontend/Cop.v +++ b/cfrontend/Cop.v @@ -92,14 +92,14 @@ Inductive classify_cast_cases : Type := Definition classify_cast (tfrom tto: type) : classify_cast_cases := match tto, tfrom with - | Tint I32 si2 _, (Tint _ _ _ | Tpointer _ _ | Tcomp_ptr _ _ | Tarray _ _ _ | Tfunction _ _) => cast_case_neutral + | Tint I32 si2 _, (Tint _ _ _ | Tpointer _ _ | Tcomp_ptr _ _ | Tarray _ _ _ | Tfunction _ _ _) => cast_case_neutral | Tint IBool _ _, Tfloat _ _ => cast_case_f2bool - | Tint IBool _ _, (Tpointer _ _ | Tcomp_ptr _ _ | Tarray _ _ _ | Tfunction _ _) => cast_case_p2bool + | Tint IBool _ _, (Tpointer _ _ | Tcomp_ptr _ _ | Tarray _ _ _ | Tfunction _ _ _) => cast_case_p2bool | Tint sz2 si2 _, Tint sz1 si1 _ => cast_case_i2i sz2 si2 | Tint sz2 si2 _, Tfloat sz1 _ => cast_case_f2i sz2 si2 | Tfloat sz2 _, Tfloat sz1 _ => cast_case_f2f sz2 | Tfloat sz2 _, Tint sz1 si1 _ => cast_case_i2f si1 sz2 - | (Tpointer _ _ | Tcomp_ptr _ _), (Tint _ _ _ | Tpointer _ _ | Tcomp_ptr _ _ | Tarray _ _ _ | Tfunction _ _) => cast_case_neutral + | (Tpointer _ _ | Tcomp_ptr _ _), (Tint _ _ _ | Tpointer _ _ | Tcomp_ptr _ _ | Tarray _ _ _ | Tfunction _ _ _) => cast_case_neutral | Tlong _ _, Tlong _ _ => cast_case_l2l | Tlong _ _, Tint sz1 si1 _ => cast_case_i2l si1 | Tint IBool _ _, Tlong _ _ => cast_case_l2bool @@ -107,7 +107,7 @@ Definition classify_cast (tfrom tto: type) : classify_cast_cases := | Tlong si2 _, Tfloat sz1 _ => cast_case_f2l si2 | Tfloat sz2 _, Tlong si1 _ => cast_case_l2f si1 sz2 | (Tpointer _ _ | Tcomp_ptr _ _), Tlong _ _ => cast_case_l2i I32 Unsigned - | Tlong si2 _, (Tpointer _ _ | Tcomp_ptr _ _ | Tarray _ _ _ | Tfunction _ _) => cast_case_i2l si2 + | Tlong si2 _, (Tpointer _ _ | Tcomp_ptr _ _ | Tarray _ _ _ | Tfunction _ _ _) => cast_case_i2l si2 | Tstruct id2 fld2 _, Tstruct id1 fld1 _ => cast_case_struct id1 fld1 id2 fld2 | Tunion id2 fld2 _, Tunion id1 fld1 _ => cast_case_union id1 fld1 id2 fld2 | Tvoid, _ => cast_case_void @@ -326,7 +326,7 @@ Proof. assert (A: classify_bool t = match t with | Tint _ _ _ => bool_case_i - | Tpointer _ _ | Tcomp_ptr _ _ | Tarray _ _ _ | Tfunction _ _ => bool_case_p + | Tpointer _ _ | Tcomp_ptr _ _ | Tarray _ _ _ | Tfunction _ _ _ => bool_case_p | Tfloat _ _ => bool_case_f | Tlong _ _ => bool_case_l | _ => bool_default @@ -833,13 +833,13 @@ Definition sem_cmp (c:comparison) (** ** Function applications *) Inductive classify_fun_cases : Type:= - | fun_case_f (targs: typelist) (tres: type) (**r (pointer to) function *) + | fun_case_f (targs: typelist) (tres: type) (cc: calling_convention) (**r (pointer to) function *) | fun_default. Definition classify_fun (ty: type) := match ty with - | Tfunction args res => fun_case_f args res - | Tpointer (Tfunction args res) _ => fun_case_f args res + | Tfunction args res cc => fun_case_f args res cc + | Tpointer (Tfunction args res cc) _ => fun_case_f args res cc | _ => fun_default end. diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v index be3ee4b..2eedbd8 100644 --- a/cfrontend/Csem.v +++ b/cfrontend/Csem.v @@ -322,11 +322,11 @@ Inductive rred: expr -> mem -> trace -> expr -> mem -> Prop := (More exactly, identification of function calls that can reduce.) *) Inductive callred: expr -> fundef -> list val -> type -> Prop := - | red_Ecall: forall vf tyf tyargs tyres el ty fd vargs, + | red_Ecall: forall vf tyf tyargs tyres cconv el ty fd vargs, Genv.find_funct ge vf = Some fd -> cast_arguments el tyargs vargs -> - type_of_fundef fd = Tfunction tyargs tyres -> - classify_fun tyf = fun_case_f tyargs tyres -> + type_of_fundef fd = Tfunction tyargs tyres cconv -> + classify_fun tyf = fun_case_f tyargs tyres cconv -> callred (Ecall (Eval vf tyf) el ty) fd vargs ty. @@ -754,9 +754,9 @@ Inductive sstep: state -> trace -> state -> Prop := sstep (Callstate (Internal f) vargs k m) E0 (State f f.(fn_body) k e m2) - | step_external_function: forall ef targs tres vargs k m vres t m', + | step_external_function: forall ef targs tres cc vargs k m vres t m', external_call ef ge vargs m t vres m' -> - sstep (Callstate (External ef targs tres) vargs k m) + sstep (Callstate (External ef targs tres cc) vargs k m) t (Returnstate vres k m') | step_returnstate: forall v f e C ty k m, @@ -781,7 +781,7 @@ Inductive initial_state (p: program): state -> Prop := Genv.init_mem p = Some m0 -> Genv.find_symbol ge p.(prog_main) = Some b -> Genv.find_funct_ptr ge b = Some f -> - type_of_fundef f = Tfunction Tnil type_int32s -> + type_of_fundef f = Tfunction Tnil type_int32s cc_default -> initial_state p (Callstate f nil Kstop m0). (** A final state is a [Returnstate] with an empty continuation. *) diff --git a/cfrontend/Csharpminor.v b/cfrontend/Csharpminor.v index 6ae33a6..4b2e915 100644 --- a/cfrontend/Csharpminor.v +++ b/cfrontend/Csharpminor.v @@ -475,7 +475,7 @@ Inductive initial_state (p: program): state -> Prop := Genv.init_mem p = Some m0 -> Genv.find_symbol ge p.(prog_main) = Some b -> Genv.find_funct_ptr ge b = Some f -> - funsig f = mksignature nil (Some Tint) -> + funsig f = signature_main -> initial_state p (Callstate f nil Kstop m0). (** A final state is a [Returnstate] with an empty continuation. *) diff --git a/cfrontend/Cshmgen.v b/cfrontend/Cshmgen.v index 0ed008f..1380695 100644 --- a/cfrontend/Cshmgen.v +++ b/cfrontend/Cshmgen.v @@ -443,10 +443,28 @@ Fixpoint transl_arglist (al: list Clight.expr) (tyl: typelist) do ta1' <- make_cast (typeof a1) ty1 ta1; do ta2 <- transl_arglist a2 ty2; OK (ta1' :: ta2) + | a1 :: a2, Tnil => + (* Tolerance for calls to K&R or variadic functions *) + do ta1 <- transl_expr a1; + do ta2 <- transl_arglist a2 Tnil; + OK (ta1 :: ta2) | _, _ => Error(msg "Cshmgen.transl_arglist: arity mismatch") end. +(** Compute the argument signature that corresponds to a function application. *) + +Fixpoint typlist_of_arglist (al: list Clight.expr) (tyl: typelist) + {struct al}: list AST.typ := + match al, tyl with + | nil, _ => nil + | a1 :: a2, Tcons ty1 ty2 => + typ_of_type ty1 :: typlist_of_arglist a2 ty2 + | a1 :: a2, Tnil => + (* Tolerance for calls to K&R or variadic functions *) + typ_of_type_default (typeof a1) :: typlist_of_arglist a2 Tnil + end. + (** * Translation of statements *) (** [transl_statement nbrk ncnt s] returns a Csharpminor statement @@ -487,10 +505,13 @@ Fixpoint transl_statement (tyret: type) (nbrk ncnt: nat) OK(Sset x tb) | Clight.Scall x b cl => match classify_fun (typeof b) with - | fun_case_f args res => + | fun_case_f args res cconv => do tb <- transl_expr b; do tcl <- transl_arglist cl args; - OK(Scall x (signature_of_type args res) tb tcl) + OK(Scall x {| sig_args := typlist_of_arglist cl args; + sig_res := opttyp_of_type res; + sig_cc := cconv |} + tb tcl) | _ => Error(msg "Cshmgen.transl_stmt(call)") end | Clight.Sbuiltin x ef tyargs bl => @@ -547,8 +568,9 @@ with transl_lbl_stmt (tyret: type) (nbrk ncnt: nat) Definition transl_var (v: ident * type) := (fst v, sizeof (snd v)). Definition signature_of_function (f: Clight.function) := - mksignature (map typ_of_type (map snd (Clight.fn_params f))) - (opttyp_of_type (Clight.fn_return f)). + {| sig_args := map typ_of_type (map snd (Clight.fn_params f)); + sig_res := opttyp_of_type (Clight.fn_return f); + sig_cc := Clight.fn_callconv f |}. Definition transl_function (f: Clight.function) : res function := do tbody <- transl_statement f.(Clight.fn_return) 1%nat 0%nat (Clight.fn_body f); @@ -563,9 +585,8 @@ Definition transl_fundef (f: Clight.fundef) : res fundef := match f with | Clight.Internal g => do tg <- transl_function g; OK(AST.Internal tg) - | Clight.External ef args res => - if list_typ_eq (sig_args (ef_sig ef)) (typlist_of_typelist args) - && opt_typ_eq (sig_res (ef_sig ef)) (opttyp_of_type res) + | Clight.External ef args res cconv => + if signature_eq (ef_sig ef) (signature_of_type args res cconv) then OK(AST.External ef) else Error(msg "Cshmgen.transl_fundef: wrong external signature") end. diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v index 220d907..d6e881e 100644 --- a/cfrontend/Cshmgenproof.v +++ b/cfrontend/Cshmgenproof.v @@ -40,28 +40,24 @@ Proof. Qed. Lemma transl_fundef_sig1: - forall f tf args res, + forall f tf args res cc, transl_fundef f = OK tf -> - classify_fun (type_of_fundef f) = fun_case_f args res -> - funsig tf = signature_of_type args res. + classify_fun (type_of_fundef f) = fun_case_f args res cc -> + funsig tf = signature_of_type args res cc. Proof. intros. destruct f; simpl in *. monadInv H. monadInv EQ. simpl. inversion H0. unfold signature_of_function, signature_of_type. f_equal. apply transl_params_types. - destruct (list_typ_eq (sig_args (ef_sig e)) (typlist_of_typelist t)); simpl in H. - destruct (opt_typ_eq (sig_res (ef_sig e)) (opttyp_of_type t0)); simpl in H. - inv H. simpl. destruct (ef_sig e); simpl in *. inv H0. - unfold signature_of_type. auto. - congruence. - congruence. + destruct (signature_eq (ef_sig e) (signature_of_type t t0 c)); inv H. + simpl. congruence. Qed. Lemma transl_fundef_sig2: - forall f tf args res, + forall f tf args res cc, transl_fundef f = OK tf -> - type_of_fundef f = Tfunction args res -> - funsig tf = signature_of_type args res. + type_of_fundef f = Tfunction args res cc -> + funsig tf = signature_of_type args res cc. Proof. intros. eapply transl_fundef_sig1; eauto. rewrite H0; reflexivity. @@ -982,6 +978,16 @@ Proof. eapply make_cast_correct; eauto. eapply transl_expr_correct; eauto. auto. Qed. +Lemma typlist_of_arglist_eq: + forall al tyl vl, + Clight.eval_exprlist ge e le m al tyl vl -> + typlist_of_arglist al tyl = typlist_of_typelist tyl. +Proof. + induction 1; simpl. + auto. + f_equal; auto. +Qed. + End EXPR. (** ** Semantic preservation for statements *) @@ -1064,11 +1070,11 @@ Inductive match_states: Clight.state -> Csharpminor.state -> Prop := match_states (Clight.State f s k e le m) (State tf ts' tk' te le m) | match_callstate: - forall fd args k m tfd tk targs tres + forall fd args k m tfd tk targs tres cconv (TR: transl_fundef fd = OK tfd) (MK: match_cont Tvoid 0%nat 0%nat k tk) (ISCC: Clight.is_call_cont k) - (TY: type_of_fundef fd = Tfunction targs tres), + (TY: type_of_fundef fd = Tfunction targs tres cconv), match_states (Clight.Callstate fd args k m) (Callstate tfd args tk m) | match_returnstate: @@ -1232,13 +1238,14 @@ Proof. (* call *) revert TR. simpl. case_eq (classify_fun (typeof a)); try congruence. - intros targs tres CF TR. monadInv TR. inv MTR. + intros targs tres cc CF TR. monadInv TR. inv MTR. exploit functions_translated; eauto. intros [tfd [FIND TFD]]. rewrite H in CF. simpl in CF. inv CF. econstructor; split. apply plus_one. econstructor; eauto. exploit transl_expr_correct; eauto. exploit transl_arglist_correct; eauto. + erewrite typlist_of_arglist_eq by eauto. eapply transl_fundef_sig1; eauto. rewrite H3. auto. econstructor; eauto. @@ -1422,9 +1429,7 @@ Proof. (* external function *) simpl in TR. - destruct (list_typ_eq (sig_args (ef_sig ef)) (typlist_of_typelist targs) && - opt_typ_eq (sig_res (ef_sig ef)) (opttyp_of_type tres)); - monadInv TR. + destruct (signature_eq (ef_sig ef) (signature_of_type targs tres cconv)); inv TR. exploit match_cont_is_call_cont; eauto. intros [A B]. econstructor; split. apply plus_one. constructor. eauto. @@ -1451,7 +1456,7 @@ Proof. rewrite symbols_preserved. replace (prog_main tprog) with (prog_main prog). auto. symmetry. unfold transl_program in TRANSL. eapply transform_partial_program2_main; eauto. - assert (funsig tf = signature_of_type Tnil type_int32s). + assert (funsig tf = signature_of_type Tnil type_int32s cc_default). eapply transl_fundef_sig2; eauto. econstructor; split. econstructor; eauto. eapply Genv.init_mem_transf_partial2; eauto. diff --git a/cfrontend/Cstrategy.v b/cfrontend/Cstrategy.v index 7988dfa..b1fbebe 100644 --- a/cfrontend/Cstrategy.v +++ b/cfrontend/Cstrategy.v @@ -359,13 +359,13 @@ Inductive estep: state -> trace -> state -> Prop := estep (ExprState f (C (Eparen r ty)) k e m) E0 (ExprState f (C (Eval v ty)) k e m) - | step_call: forall f C rf rargs ty k e m targs tres vf vargs fd, + | step_call: forall f C rf rargs ty k e m targs tres cconv vf vargs fd, leftcontext RV RV C -> - classify_fun (typeof rf) = fun_case_f targs tres -> + classify_fun (typeof rf) = fun_case_f targs tres cconv -> eval_simple_rvalue e m rf vf -> eval_simple_list e m rargs targs vargs -> Genv.find_funct ge vf = Some fd -> - type_of_fundef fd = Tfunction targs tres -> + type_of_fundef fd = Tfunction targs tres cconv -> estep (ExprState f (C (Ecall rf rargs ty)) k e m) E0 (Callstate fd vargs (Kcall f e C ty k) m) @@ -562,11 +562,11 @@ Definition invert_expr_prop (a: expr) (m: mem) : Prop := exists v, sem_cast v1 ty1 ty = Some v | Ecall (Eval vf tyf) rargs ty => exprlist_all_values rargs -> - exists tyargs, exists tyres, exists fd, exists vl, - classify_fun tyf = fun_case_f tyargs tyres + exists tyargs tyres cconv fd vl, + classify_fun tyf = fun_case_f tyargs tyres cconv /\ Genv.find_funct ge vf = Some fd /\ cast_arguments rargs tyargs vl - /\ type_of_fundef fd = Tfunction tyargs tyres + /\ type_of_fundef fd = Tfunction tyargs tyres cconv | Ebuiltin ef tyargs rargs ty => exprlist_all_values rargs -> exists vargs, exists t, exists vres, exists m', @@ -610,7 +610,7 @@ Lemma callred_invert: invert_expr_prop r m. Proof. intros. inv H. simpl. - intros. exists tyargs; exists tyres; exists fd; exists args; auto. + intros. exists tyargs, tyres, cconv, fd, args; auto. Qed. Scheme context_ind2 := Minimality for context Sort Prop @@ -1369,7 +1369,7 @@ Proof. eapply safe_steps. eexact S1. apply (eval_simple_list_steps f k e m rargs vl E2 C'); auto. simpl. intros X. exploit X. eapply rval_list_all_values. - intros [tyargs [tyres [fd [vargs [P [Q [U V]]]]]]]. + intros [tyargs [tyres [cconv [fd [vargs [P [Q [U V]]]]]]]]. econstructor; econstructor; eapply step_call; eauto. eapply can_eval_simple_list; eauto. (* builtin *) pose (C' := fun x => C(Ebuiltin ef tyargs x ty)). @@ -1756,13 +1756,13 @@ with eval_expr: env -> mem -> kind -> expr -> trace -> mem -> expr -> Prop := ty = typeof r2 -> eval_expr e m RV (Ecomma r1 r2 ty) (t1**t2) m2 r2' | eval_call: forall e m rf rargs ty t1 m1 rf' t2 m2 rargs' vf vargs - targs tres fd t3 m3 vres, + targs tres cconv fd t3 m3 vres, eval_expr e m RV rf t1 m1 rf' -> eval_exprlist e m1 rargs t2 m2 rargs' -> eval_simple_rvalue ge e m2 rf' vf -> eval_simple_list ge e m2 rargs' targs vargs -> - classify_fun (typeof rf) = fun_case_f targs tres -> + classify_fun (typeof rf) = fun_case_f targs tres cconv -> Genv.find_funct ge vf = Some fd -> - type_of_fundef fd = Tfunction targs tres -> + type_of_fundef fd = Tfunction targs tres cconv -> eval_funcall m2 fd vargs t3 m3 vres -> eval_expr e m RV (Ecall rf rargs ty) (t1**t2**t3) m3 (Eval vres ty) @@ -1901,9 +1901,9 @@ with eval_funcall: mem -> fundef -> list val -> trace -> mem -> val -> Prop := outcome_result_value out f.(fn_return) vres -> Mem.free_list m3 (blocks_of_env e) = Some m4 -> eval_funcall m (Internal f) vargs t m4 vres - | eval_funcall_external: forall m ef targs tres vargs t vres m', + | eval_funcall_external: forall m ef targs tres cconv vargs t vres m', external_call ef ge vargs m t vres m' -> - eval_funcall m (External ef targs tres) vargs t m' vres. + eval_funcall m (External ef targs tres cconv) vargs t m' vres. Scheme eval_expression_ind5 := Minimality for eval_expression Sort Prop with eval_expr_ind5 := Minimality for eval_expr Sort Prop @@ -1999,13 +1999,13 @@ CoInductive evalinf_expr: env -> mem -> kind -> expr -> traceinf -> Prop := evalinf_exprlist e m1 a2 t2 -> evalinf_expr e m RV (Ecall a1 a2 ty) (t1 *** t2) | evalinf_call: forall e m rf rargs ty t1 m1 rf' t2 m2 rargs' vf vargs - targs tres fd t3, + targs tres cconv fd t3, eval_expr e m RV rf t1 m1 rf' -> eval_exprlist e m1 rargs t2 m2 rargs' -> eval_simple_rvalue ge e m2 rf' vf -> eval_simple_list ge e m2 rargs' targs vargs -> - classify_fun (typeof rf) = fun_case_f targs tres -> + classify_fun (typeof rf) = fun_case_f targs tres cconv -> Genv.find_funct ge vf = Some fd -> - type_of_fundef fd = Tfunction targs tres -> + type_of_fundef fd = Tfunction targs tres cconv -> evalinf_funcall m2 fd vargs t3 -> evalinf_expr e m RV (Ecall rf rargs ty) (t1***t2***t3) @@ -3034,7 +3034,7 @@ Inductive bigstep_program_terminates (p: program): trace -> int -> Prop := Genv.init_mem p = Some m0 -> Genv.find_symbol ge p.(prog_main) = Some b -> Genv.find_funct_ptr ge b = Some f -> - type_of_fundef f = Tfunction Tnil type_int32s -> + type_of_fundef f = Tfunction Tnil type_int32s cc_default -> eval_funcall ge m0 f nil t m1 (Vint r) -> bigstep_program_terminates p t r. @@ -3044,7 +3044,7 @@ Inductive bigstep_program_diverges (p: program): traceinf -> Prop := Genv.init_mem p = Some m0 -> Genv.find_symbol ge p.(prog_main) = Some b -> Genv.find_funct_ptr ge b = Some f -> - type_of_fundef f = Tfunction Tnil type_int32s -> + type_of_fundef f = Tfunction Tnil type_int32s cc_default -> evalinf_funcall ge m0 f nil t -> bigstep_program_diverges p t. diff --git a/cfrontend/Csyntax.v b/cfrontend/Csyntax.v index 8b98556..ea1bd86 100644 --- a/cfrontend/Csyntax.v +++ b/cfrontend/Csyntax.v @@ -177,6 +177,7 @@ with labeled_statements : Type := (**r cases of a [switch] *) Record function : Type := mkfunction { fn_return: type; + fn_callconv: calling_convention; fn_params: list (ident * type); fn_vars: list (ident * type); fn_body: statement @@ -190,17 +191,17 @@ Definition var_names (vars: list(ident * type)) : list ident := Inductive fundef : Type := | Internal: function -> fundef - | External: external_function -> typelist -> type -> fundef. + | External: external_function -> typelist -> type -> calling_convention -> fundef. (** The type of a function definition. *) Definition type_of_function (f: function) : type := - Tfunction (type_of_params (fn_params f)) (fn_return f). + Tfunction (type_of_params (fn_params f)) (fn_return f) (fn_callconv f). Definition type_of_fundef (f: fundef) : type := match f with | Internal fd => type_of_function fd - | External id args res => Tfunction args res + | External id args res cc => Tfunction args res cc end. (** ** Programs *) diff --git a/cfrontend/Ctypes.v b/cfrontend/Ctypes.v index c9ef996..2b409ab 100644 --- a/cfrontend/Ctypes.v +++ b/cfrontend/Ctypes.v @@ -97,7 +97,7 @@ Inductive type : Type := | Tfloat: floatsize -> attr -> type (**r floating-point types *) | Tpointer: type -> attr -> type (**r pointer types ([*ty]) *) | Tarray: type -> Z -> attr -> type (**r array types ([ty[len]]) *) - | Tfunction: typelist -> type -> type (**r function types *) + | Tfunction: typelist -> type -> calling_convention -> type (**r function types *) | Tstruct: ident -> fieldlist -> attr -> type (**r struct types *) | Tunion: ident -> fieldlist -> attr -> type (**r union types *) | Tcomp_ptr: ident -> attr -> type (**r pointer to named struct or union *) @@ -119,11 +119,11 @@ Proof. assert (forall (x y: floatsize), {x=y} + {x<>y}) by decide equality. assert (forall (x y: attr), {x=y} + {x<>y}). { decide equality. decide equality. apply N.eq_dec. apply bool_dec. } - generalize ident_eq zeq. intros E1 E2. + generalize ident_eq zeq bool_dec. intros E1 E2 E3. decide equality. decide equality. - generalize ident_eq. intros E1. decide equality. + generalize ident_eq. intros E1. decide equality. Defined. Opaque type_eq typelist_eq fieldlist_eq. @@ -138,7 +138,7 @@ Definition attr_of_type (ty: type) := | Tfloat sz a => a | Tpointer elt a => a | Tarray elt sz a => a - | Tfunction args res => noattr + | Tfunction args res cc => noattr | Tstruct id fld a => a | Tunion id fld a => a | Tcomp_ptr id a => a @@ -154,7 +154,7 @@ Definition typeconv (ty: type) : type := match ty with | Tint (I8 | I16 | IBool) _ a => Tint I32 Signed a | Tarray t sz a => Tpointer t a - | Tfunction _ _ => Tpointer ty noattr + | Tfunction _ _ _ => Tpointer ty noattr | _ => ty end. @@ -177,7 +177,7 @@ Fixpoint alignof (t: type) : Z := | Tfloat F64 _ => 8 | Tpointer _ _ => 4 | Tarray t' _ _ => alignof t' - | Tfunction _ _ => 1 + | Tfunction _ _ _ => 1 | Tstruct _ fld _ => alignof_fields fld | Tunion _ fld _ => alignof_fields fld | Tcomp_ptr _ _ => 4 @@ -252,7 +252,7 @@ Fixpoint sizeof (t: type) : Z := | Tfloat F64 _ => 8 | Tpointer _ _ => 4 | Tarray t' n _ => sizeof t' * Zmax 1 n - | Tfunction _ _ => 1 + | Tfunction _ _ _ => 1 | Tstruct _ fld _ => align (Zmax 1 (sizeof_struct fld 0)) (alignof t) | Tunion _ fld _ => align (Zmax 1 (sizeof_union fld)) (alignof t) | Tcomp_ptr _ _ => 4 @@ -302,7 +302,7 @@ Fixpoint naturally_aligned (t: type) : Prop := attr_alignas a = None | Tarray t' _ a => attr_alignas a = None /\ naturally_aligned t' - | Tvoid | Tfunction _ _ | Tstruct _ _ _ | Tunion _ _ _ => + | Tvoid | Tfunction _ _ _ | Tstruct _ _ _ | Tunion _ _ _ => True end. @@ -478,7 +478,7 @@ Definition access_mode (ty: type) : mode := | Tvoid => By_nothing | Tpointer _ _ => By_value Mint32 | Tarray _ _ _ => By_reference - | Tfunction _ _ => By_reference + | Tfunction _ _ _ => By_reference | Tstruct _ _ _ => By_copy | Tunion _ _ _ => By_copy | Tcomp_ptr _ _ => By_nothing @@ -510,7 +510,7 @@ Fixpoint unroll_composite (ty: type) : type := | Tfloat _ _ => ty | Tpointer t1 a => Tpointer (unroll_composite t1) a | Tarray t1 sz a => Tarray (unroll_composite t1) sz a - | Tfunction t1 t2 => Tfunction (unroll_composite_list t1) (unroll_composite t2) + | Tfunction t1 t2 a => Tfunction (unroll_composite_list t1) (unroll_composite t2) a | Tstruct id fld a => if ident_eq id cid then ty else Tstruct id (unroll_composite_fields fld) a | Tunion id fld a => if ident_eq id cid then ty else Tunion id (unroll_composite_fields fld) a | Tcomp_ptr id a => if ident_eq id cid then Tpointer comp a else ty @@ -586,7 +586,7 @@ Fixpoint alignof_blockcopy (t: type) : Z := | Tfloat F64 _ => 8 | Tpointer _ _ => 4 | Tarray t' _ _ => alignof_blockcopy t' - | Tfunction _ _ => 1 + | Tfunction _ _ _ => 1 | Tstruct _ fld _ => Zmin 8 (alignof t) | Tunion _ fld _ => Zmin 8 (alignof t) | Tcomp_ptr _ _ => 4 @@ -681,5 +681,15 @@ Fixpoint typlist_of_typelist (tl: typelist) : list AST.typ := | Tcons hd tl => typ_of_type hd :: typlist_of_typelist tl end. -Definition signature_of_type (args: typelist) (res: type) : signature := - mksignature (typlist_of_typelist args) (opttyp_of_type res). +Definition signature_of_type (args: typelist) (res: type) (cc: calling_convention): signature := + mksignature (typlist_of_typelist args) (opttyp_of_type res) cc. + +(** Like [typ_of_type], but apply default argument promotion. *) + +Definition typ_of_type_default (t: type) : AST.typ := + match t with + | Tfloat _ _ => AST.Tfloat + | Tlong _ _ => AST.Tlong + | _ => AST.Tint + end. + diff --git a/cfrontend/Initializersproof.v b/cfrontend/Initializersproof.v index 5db4718..b6fc728 100644 --- a/cfrontend/Initializersproof.v +++ b/cfrontend/Initializersproof.v @@ -680,7 +680,7 @@ Qed. (** A semantics for general initializers *) -Definition dummy_function := mkfunction Tvoid nil nil Sskip. +Definition dummy_function := mkfunction Tvoid cc_default nil nil Sskip. Fixpoint fields_of_struct (id: ident) (ty: type) (fl: fieldlist) (pos: Z) : list (Z * type) := match fl with diff --git a/cfrontend/PrintClight.ml b/cfrontend/PrintClight.ml index 78ab7fc..376707a 100644 --- a/cfrontend/PrintClight.ml +++ b/cfrontend/PrintClight.ml @@ -229,7 +229,7 @@ and print_stmt_for p s = let print_function p id f = fprintf p "%s@ " (name_cdecl (name_function_parameters (extern_atom id) - f.fn_params) + f.fn_params f.fn_callconv) f.fn_return); fprintf p "@[<v 2>{@ "; List.iter @@ -245,10 +245,10 @@ let print_function p id f = let print_fundef p id fd = match fd with - | External(EF_external(_,_), args, res) -> + | External(EF_external(_,_), args, res, cconv) -> fprintf p "extern %s;@ @ " - (name_cdecl (extern_atom id) (Tfunction(args, res))) - | External(_, _, _) -> + (name_cdecl (extern_atom id) (Tfunction(args, res, cconv))) + | External(_, _, _, _) -> () | Internal f -> print_function p id f @@ -309,7 +309,7 @@ let collect_function f = let collect_globdef (id, gd) = match gd with - | Gfun(External(_, args, res)) -> collect_type_list args; collect_type res + | Gfun(External(_, args, res, _)) -> collect_type_list args; collect_type res | Gfun(Internal f) -> collect_function f | Gvar v -> collect_type v.gvar_info diff --git a/cfrontend/PrintCsyntax.ml b/cfrontend/PrintCsyntax.ml index 4db8976..758323e 100644 --- a/cfrontend/PrintCsyntax.ml +++ b/cfrontend/PrintCsyntax.ml @@ -88,11 +88,6 @@ let attributes a = let name_optid id = if id = "" then "" else " " ^ id -(* -let parenthesize_if_pointer id = - if String.length id > 0 && id.[0] = '*' then "(" ^ id ^ ")" else id -*) - let rec name_cdecl id ty = match ty with | Tvoid -> @@ -111,24 +106,26 @@ let rec name_cdecl id ty = name_cdecl id' t | Tarray(t, n, a) -> name_cdecl (sprintf "%s[%ld]" id (camlint_of_coqint n)) t - | Tfunction(args, res) -> + | Tfunction(args, res, cconv) -> let b = Buffer.create 20 in if id = "" then Buffer.add_string b "(*)" else Buffer.add_string b id; Buffer.add_char b '('; - begin match args with + let rec add_args first = function | Tnil -> - Buffer.add_string b "void" - | _ -> - let rec add_args first = function - | Tnil -> () - | Tcons(t1, tl) -> - if not first then Buffer.add_string b ", "; - Buffer.add_string b (name_cdecl "" t1); - add_args false tl in - add_args true args - end; + if first then + Buffer.add_string b + (if cconv.cc_vararg then "..." else "void") + else if cconv.cc_vararg then + Buffer.add_string b ", ..." + else + () + | Tcons(t1, tl) -> + if not first then Buffer.add_string b ", "; + Buffer.add_string b (name_cdecl "" t1); + add_args false tl in + add_args true args; Buffer.add_char b ')'; name_cdecl (Buffer.contents b) res | Tstruct(name, fld, a) -> @@ -351,16 +348,17 @@ and print_stmt_for p s = | _ -> fprintf p "({ %a })" print_stmt s -let name_function_parameters fun_name params = +let name_function_parameters fun_name params cconv = let b = Buffer.create 20 in Buffer.add_string b fun_name; Buffer.add_char b '('; begin match params with | [] -> - Buffer.add_string b "void" + Buffer.add_string b (if cconv.cc_vararg then "..." else "void") | _ -> let rec add_params first = function - | [] -> () + | [] -> + if cconv.cc_vararg then Buffer.add_string b "..." | (id, ty) :: rem -> if not first then Buffer.add_string b ", "; Buffer.add_string b (name_cdecl (extern_atom id) ty); @@ -373,7 +371,7 @@ let name_function_parameters fun_name params = let print_function p id f = fprintf p "%s@ " (name_cdecl (name_function_parameters (extern_atom id) - f.fn_params) + f.fn_params f.fn_callconv) f.fn_return); fprintf p "@[<v 2>{@ "; List.iter @@ -385,10 +383,10 @@ let print_function p id f = let print_fundef p id fd = match fd with - | External(EF_external(_,_), args, res) -> + | External(EF_external(_,_), args, res, cconv) -> fprintf p "extern %s;@ @ " - (name_cdecl (extern_atom id) (Tfunction(args, res))) - | External(_, _, _) -> + (name_cdecl (extern_atom id) (Tfunction(args, res, cconv))) + | External(_, _, _, _) -> () | Internal f -> print_function p id f @@ -474,7 +472,7 @@ let rec collect_type = function | Tlong _ -> () | Tpointer(t, _) -> collect_type t | Tarray(t, _, _) -> collect_type t - | Tfunction(args, res) -> collect_type_list args; collect_type res + | Tfunction(args, res, _) -> collect_type_list args; collect_type res | Tstruct(id, fld, _) | Tunion(id, fld, _) -> let s = extern_atom id in if not (StructUnion.mem s !struct_unions) then begin @@ -552,7 +550,7 @@ let collect_function f = let collect_globdef (id, gd) = match gd with - | Gfun(External(_, args, res)) -> collect_type_list args; collect_type res + | Gfun(External(_, args, res, _)) -> collect_type_list args; collect_type res | Gfun(Internal f) -> collect_function f | Gvar v -> collect_type v.gvar_info diff --git a/cfrontend/SimplExpr.v b/cfrontend/SimplExpr.v index 1ead0ae..01f304e 100644 --- a/cfrontend/SimplExpr.v +++ b/cfrontend/SimplExpr.v @@ -504,6 +504,7 @@ Definition transl_function (f: Csyntax.function) : mon function := do temps <- get_trail; ret (mkfunction f.(Csyntax.fn_return) + f.(Csyntax.fn_callconv) f.(Csyntax.fn_params) f.(Csyntax.fn_vars) temps @@ -513,8 +514,8 @@ Definition transl_fundef (fd: Csyntax.fundef) : mon fundef := match fd with | Csyntax.Internal f => do tf <- transl_function f; ret (Internal tf) - | Csyntax.External ef targs tres => - ret (External ef targs tres) + | Csyntax.External ef targs tres cconv => + ret (External ef targs tres cconv) end. Local Open Scope error_monad_scope. diff --git a/cfrontend/SimplExprproof.v b/cfrontend/SimplExprproof.v index b3c861e..9134e11 100644 --- a/cfrontend/SimplExprproof.v +++ b/cfrontend/SimplExprproof.v @@ -2166,9 +2166,9 @@ Proof. inv H7. inversion H3; subst. econstructor; split. left; apply plus_one. eapply step_internal_function. econstructor. - rewrite H5; rewrite H6; auto. - rewrite H5; rewrite H6. eapply alloc_variables_preserved; eauto. - rewrite H5. eapply bind_parameters_preserved; eauto. + rewrite H6; rewrite H7; auto. + rewrite H6; rewrite H7. eapply alloc_variables_preserved; eauto. + rewrite H6. eapply bind_parameters_preserved; eauto. eauto. constructor; auto. diff --git a/cfrontend/SimplExprspec.v b/cfrontend/SimplExprspec.v index 9dfa42e..3dae7ab 100644 --- a/cfrontend/SimplExprspec.v +++ b/cfrontend/SimplExprspec.v @@ -1090,6 +1090,7 @@ Inductive tr_function: Csyntax.function -> Clight.function -> Prop := | tr_function_intro: forall f tf, tr_stmt f.(Csyntax.fn_body) tf.(fn_body) -> fn_return tf = Csyntax.fn_return f -> + fn_callconv tf = Csyntax.fn_callconv f -> fn_params tf = Csyntax.fn_params f -> fn_vars tf = Csyntax.fn_vars f -> tr_function f tf. @@ -1098,8 +1099,8 @@ Inductive tr_fundef: Csyntax.fundef -> Clight.fundef -> Prop := | tr_internal: forall f tf, tr_function f tf -> tr_fundef (Csyntax.Internal f) (Clight.Internal tf) - | tr_external: forall ef targs tres, - tr_fundef (Csyntax.External ef targs tres) (External ef targs tres). + | tr_external: forall ef targs tres cconv, + tr_fundef (Csyntax.External ef targs tres cconv) (External ef targs tres cconv). Lemma transl_function_spec: forall f tf g g' i, diff --git a/cfrontend/SimplLocals.v b/cfrontend/SimplLocals.v index 95ff9ed..2956508 100644 --- a/cfrontend/SimplLocals.v +++ b/cfrontend/SimplLocals.v @@ -229,6 +229,7 @@ Definition transf_function (f: function) : res function := assertion (list_disjoint_dec ident_eq (var_names f.(fn_params)) (var_names f.(fn_temps))); do body' <- simpl_stmt cenv f.(fn_body); OK {| fn_return := f.(fn_return); + fn_callconv := f.(fn_callconv); fn_params := f.(fn_params); fn_vars := remove_lifted cenv (f.(fn_params) ++ f.(fn_vars)); fn_temps := add_lifted cenv f.(fn_vars) f.(fn_temps); @@ -239,7 +240,7 @@ Definition transf_function (f: function) : res function := Definition transf_fundef (fd: fundef) : res fundef := match fd with | Internal f => do tf <- transf_function f; OK (Internal tf) - | External ef targs tres => OK (External ef targs tres) + | External ef targs tres cconv => OK (External ef targs tres cconv) end. Definition transf_program (p: program) : res program := diff --git a/cfrontend/SimplLocalsproof.v b/cfrontend/SimplLocalsproof.v index 552c991..ae98130 100644 --- a/cfrontend/SimplLocalsproof.v +++ b/cfrontend/SimplLocalsproof.v @@ -1710,12 +1710,12 @@ Inductive match_states: state -> state -> Prop := match_states (State f s k e le m) (State tf ts tk te tle tm) | match_call_state: - forall fd vargs k m tfd tvargs tk tm j targs tres + forall fd vargs k m tfd tvargs tk tm j targs tres cconv (TRFD: transf_fundef fd = OK tfd) (MCONT: forall cenv, match_cont j cenv k tk m (Mem.nextblock m) (Mem.nextblock tm)) (MINJ: Mem.inject j m tm) (AINJ: val_list_inject j vargs tvargs) - (FUNTY: type_of_fundef fd = Tfunction targs tres) + (FUNTY: type_of_fundef fd = Tfunction targs tres cconv) (ANORM: val_casted_list vargs targs), match_states (Callstate fd vargs k m) (Callstate tfd tvargs tk tm) diff --git a/checklink/Check.ml b/checklink/Check.ml index c51e090..8e8afd1 100644 --- a/checklink/Check.ml +++ b/checklink/Check.ml @@ -195,13 +195,10 @@ let mark_covered_fun_sym_ndx (ndx: int) ffw: f_framework = ) >>> (ff_sf ^%= check_fun_symtab ffw.this_ident ndx) -(** Taken from CompCert *) -let re_variadic_stub: Str.regexp = Str.regexp "\\(.*\\)\\$[if]*$" - (** Tries to refine the mapping for key [k] in [ident_to_sym_ndx] so that it is mapped to [vaddr]. Fails if no symbol in [k]'s mapping has that virtual - address, unless the symbol is a stub from CompCert. Otherwise, it filters - out all symbols whose virtual address does not match [vaddr]. + address. Otherwise, it filters out all symbols whose virtual + address does not match [vaddr]. *) let idmap_unify (k: P.t) (vaddr: int32) (sfw: s_framework) : s_framework or_err = @@ -215,39 +212,16 @@ let idmap_unify (k: P.t) (vaddr: int32) (sfw: s_framework) with | [] -> (* no symbol has that virtual address *) - let ident_name = Hashtbl.find sfw.ident_to_name k in - if Str.string_match re_variadic_stub ident_name 0 - then (* this ident needs a stub, whose address is [vaddr] *) - try ( - (* fetch the registered virtual address for this stub *) - let v = PosMap.find k sfw.stub_ident_to_vaddr in - (* if there is one, we're good if it's the same as [vaddr] *) - if vaddr = v - then OK(sfw) - else ERR( - Printf.sprintf - "Incoherent constraints for stub: %s" - (Hashtbl.find sfw.ident_to_name k) - ) - ) - with Not_found -> - (* if the stub has no previously registered virtual address, - register [vaddr] *) - OK( - sfw - >>> (stub_ident_to_vaddr ^%= PosMap.add k vaddr) + ERR( + Printf.sprintf + "Incoherent constraints for ident %s with value %s and candidates [%s]" + (Hashtbl.find sfw.ident_to_name k) + (string_of_int32 vaddr) + (string_of_list + (fun ndx -> string_of_int32 sfw.ef.elf.e_symtab.(ndx).st_value) + ", " id_ndxes ) - else (* not a stub, so this is a real error *) - ERR( - Printf.sprintf - "Incoherent constraints for ident %s with value %s and candidates [%s]" - (Hashtbl.find sfw.ident_to_name k) - (string_of_int32 vaddr) - (string_of_list - (fun ndx -> string_of_int32 sfw.ef.elf.e_symtab.(ndx).st_value) - ", " id_ndxes - ) - ) + ) | ndxes -> if id_ndxes = ndxes then OK(sfw) @@ -595,6 +569,20 @@ let rec match_jmptbl lbllist vaddr size ffw = end end +(** Matches [ecode] against the expected CR6 magic before a function call. +*) +let match_set_cr6 sg ecode = + if sg.sig_cc.cc_vararg then + if List.mem Tfloat sg.sig_args then + match ecode with + | CREQV(6, 6, 6) :: ecode' -> Some ecode' + | _ -> None + else + match ecode with + | CRXOR(6, 6, 6) :: ecode' -> Some ecode' + | _ -> None + else Some ecode + (** Matches [ecode] agains the expected code for a small memory copy pseudo-instruction. Returns a triple containing the updated framework, the remaining ELF code, and the updated program counter. @@ -1022,8 +1010,8 @@ let rec compare_code ccode ecode pc: checker = fun fw -> | _ -> error end | Pbctr sg -> - begin match ecode with - | BCCTRx(bo, bi, lk) :: es -> + begin match match_set_cr6 sg ecode with + | Some(BCCTRx(bo, bi, lk) :: es) -> OK(fw) >>= match_bo_ctr bo >>= match_ints 0 bi @@ -1032,8 +1020,8 @@ let rec compare_code ccode ecode pc: checker = fun fw -> | _ -> error end | Pbctrl sg -> - begin match ecode with - | BCCTRx(bo, bi, lk) :: es -> + begin match match_set_cr6 sg ecode with + | Some(BCCTRx(bo, bi, lk) :: es) -> OK(fw) >>= match_bo_ctr bo >>= match_ints 0 bi @@ -1070,8 +1058,8 @@ let rec compare_code ccode ecode pc: checker = fun fw -> | _ -> error end | Pbl(ident, sg) -> - begin match ecode with - | Bx(li, aa, lk) :: es -> + begin match match_set_cr6 sg ecode with + | Some(Bx(li, aa, lk) :: es) -> let dest = Int32.(add pc (mul 4l (exts li))) in OK(fw) >>= (ff_sf ^%=? idmap_unify ident dest) @@ -1091,8 +1079,8 @@ let rec compare_code ccode ecode pc: checker = fun fw -> | _ -> error end | Pbs(ident, sg) -> - begin match ecode with - | Bx(li, aa, lk) :: es -> + begin match match_set_cr6 sg ecode with + | Some(Bx(li, aa, lk) :: es) -> let dest = Int32.(add pc (mul 4l (exts li))) in OK(fw) >>= match_bools false aa @@ -2911,87 +2899,6 @@ let check_data (pv: (ident * unit globvar) list) (sfw: s_framework) (* Empty lists mean the symbol is external, no need for check *) (List.filter (fun (_, gv) -> gv.gvar_init <> []) pv) -(** Checks that everything that has been assimiled as a stub during checks - indeed looks like a stub. -*) -let check_stubs sfw = - let check cond msg sfw = - sfw - >>> (if cond then id else (sf_ef ^%= add_log (ERROR(msg)))) - in - let check_eq msg a b = check (a = b) msg in - let match_bools = check_eq "match_bools" in - let match_ints = check_eq "match_ints" in - let check_stub ident vaddr sfw = - let fundef = List.find (fun (i, _) -> i = ident) sfw.program.prog_defs in - let elf = sfw.ef.elf in - let stub_ecode = from_some (code_at_vaddr elf vaddr 2) in - let stub_offset = from_some (physical_offset_of_vaddr elf vaddr) in - begin match fundef with - | (_, Gfun(External(EF_external(dest_ident, _) as ef))) -> - let args = (ef_sig ef).sig_args in - if List.mem Tfloat args - then - begin match stub_ecode with - | CREQV(crbD, crbA, crbB) :: (* vaddr *) - Bx(li, aa, lk) :: (* vaddr + 4 *) - [] -> - let dest_vaddr = Int32.(add (add vaddr 4l) (mul 4l (exts li))) in - begin match idmap_unify dest_ident dest_vaddr sfw with - | ERR(s) -> - sfw - >>> (sf_ef ^%= add_log (ERROR( - "Couldn't match stub, " ^ s - ))) - | OK(sfw) -> - sfw - >>> match_ints 6 crbD - >>> match_ints 6 crbA - >>> match_ints 6 crbB - >>> match_bools false aa - >>> match_bools false lk - >>> (sf_ef ^%= - add_range stub_offset 8l 4 - (Stub(Hashtbl.find sfw.ident_to_name ident)) - ) - end - | _ -> - sfw - >>> (sf_ef ^%= add_log (ERROR("Couldn't match stub"))) - end - else - begin match stub_ecode with - | CRXOR(crbD, crbA, crbB) :: (* vaddr *) - Bx(li, aa, lk) :: (* vaddr + 4 *) - [] -> - let dest_vaddr = Int32.(add (add vaddr 4l) (mul 4l (exts li))) in - begin match idmap_unify dest_ident dest_vaddr sfw with - | ERR(s) -> - sfw - >>> (sf_ef ^%= add_log (ERROR( - "Couldn't match stub, " ^ s - ))) - | OK(sfw) -> - sfw - >>> match_ints 6 crbD - >>> match_ints 6 crbA - >>> match_ints 6 crbB - >>> match_bools false aa - >>> match_bools false lk - >>> (sf_ef ^%= - add_range stub_offset 8l 4 - (Stub(Hashtbl.find sfw.ident_to_name ident)) - ) - end - | _ -> - sfw - >>> (sf_ef ^%= add_log (ERROR("Couldn't match stub"))) - end - | _ -> fatal "Unexpected fundef in check_stubs, please report." - end - in - PosMap.fold check_stub sfw.stub_ident_to_vaddr sfw - (** Read a .sdump file *) let sdump_magic_number = "CompCertSDUMP" ^ Configuration.version @@ -3065,17 +2972,11 @@ let process_sdump efw sdump: e_framework = ; program = prog ; ident_to_name = names ; ident_to_sym_ndx = ident_to_sym_ndx - ; stub_ident_to_vaddr = PosMap.empty ; atoms = atoms } ) >>> worklist_process wl >>> (fun sfw -> - print_debug "Checking stubs"; - sfw - ) - >>> check_stubs - >>> (fun sfw -> print_debug "Checking data"; sfw ) diff --git a/checklink/Frameworks.ml b/checklink/Frameworks.ml index 35144dc..ec11412 100644 --- a/checklink/Frameworks.ml +++ b/checklink/Frameworks.ml @@ -84,9 +84,6 @@ type s_framework = { as we learn more about the contents of the symbol. *) ident_to_sym_ndx: (int list) PosMap.t; - (** CompCert generates stubs for some functions, which we will aggregate as we - discover them. *) - stub_ident_to_vaddr: int32 PosMap.t; (** This structure is imported from CompCert's .sdump, and describes each atom. *) atoms: (ident, C2C.atom_info) Hashtbl.t; @@ -140,11 +137,6 @@ let ident_to_sym_ndx = { set = (fun i sf -> { sf with ident_to_sym_ndx = i }); } -let stub_ident_to_vaddr = { - get = (fun sf -> sf.stub_ident_to_vaddr); - set = (fun i sf -> { sf with stub_ident_to_vaddr = i }); -} - (** Adds a range to the checked bytes list. *) let add_range (start: int32) (length: int32) (align: int) (bcd: byte_chunk_desc) diff --git a/common/AST.v b/common/AST.v index 1b1e872..5eee291 100644 --- a/common/AST.v +++ b/common/AST.v @@ -83,14 +83,26 @@ Fixpoint subtype_list (tyl1 tyl2: list typ) : bool := end. (** Additionally, function definitions and function calls are annotated - by function signatures indicating the number and types of arguments, - as well as the type of the returned value if any. These signatures - are used in particular to determine appropriate calling conventions - for the function. *) + by function signatures indicating: +- the number and types of arguments; +- the type of the returned value, if any; +- additional information on which calling convention to use. + +These signatures are used in particular to determine appropriate +calling conventions for the function. *) + +Record calling_convention : Type := mkcallconv { + cc_vararg: bool; + cc_structret: bool +}. + +Definition cc_default := + {| cc_vararg := false; cc_structret := false |}. Record signature : Type := mksignature { sig_args: list typ; - sig_res: option typ + sig_res: option typ; + sig_cc: calling_convention }. Definition proj_sig_res (s: signature) : typ := @@ -100,9 +112,15 @@ Definition proj_sig_res (s: signature) : typ := end. Definition signature_eq: forall (s1 s2: signature), {s1=s2} + {s1<>s2}. -Proof. generalize opt_typ_eq, list_typ_eq; intros; decide equality. Defined. +Proof. + generalize opt_typ_eq, list_typ_eq; intros; decide equality. + generalize bool_dec; intros. decide equality. +Defined. Global Opaque signature_eq. +Definition signature_main := + {| sig_args := nil; sig_res := Some Tint; sig_cc := cc_default |}. + (** Memory accesses (load and store instructions) are annotated by a ``memory chunk'' indicating the type, size and signedness of the chunk of memory being accessed. *) @@ -570,16 +588,16 @@ Definition ef_sig (ef: external_function): signature := match ef with | EF_external name sg => sg | EF_builtin name sg => sg - | EF_vload chunk => mksignature (Tint :: nil) (Some (type_of_chunk chunk)) - | EF_vstore chunk => mksignature (Tint :: type_of_chunk chunk :: nil) None - | EF_vload_global chunk _ _ => mksignature nil (Some (type_of_chunk chunk)) - | EF_vstore_global chunk _ _ => mksignature (type_of_chunk chunk :: nil) None - | EF_malloc => mksignature (Tint :: nil) (Some Tint) - | EF_free => mksignature (Tint :: nil) None - | EF_memcpy sz al => mksignature (Tint :: Tint :: nil) None - | EF_annot text targs => mksignature (annot_args_typ targs) None - | EF_annot_val text targ => mksignature (targ :: nil) (Some targ) - | EF_inline_asm text => mksignature nil None + | EF_vload chunk => mksignature (Tint :: nil) (Some (type_of_chunk chunk)) cc_default + | EF_vstore chunk => mksignature (Tint :: type_of_chunk chunk :: nil) None cc_default + | EF_vload_global chunk _ _ => mksignature nil (Some (type_of_chunk chunk)) cc_default + | EF_vstore_global chunk _ _ => mksignature (type_of_chunk chunk :: nil) None cc_default + | EF_malloc => mksignature (Tint :: nil) (Some Tint) cc_default + | EF_free => mksignature (Tint :: nil) None cc_default + | EF_memcpy sz al => mksignature (Tint :: Tint :: nil) None cc_default + | EF_annot text targs => mksignature (annot_args_typ targs) None cc_default + | EF_annot_val text targ => mksignature (targ :: nil) (Some targ) cc_default + | EF_inline_asm text => mksignature nil None cc_default end. (** Whether an external function should be inlined by the compiler. *) diff --git a/common/Events.v b/common/Events.v index 24c03dc..cf57650 100644 --- a/common/Events.v +++ b/common/Events.v @@ -764,7 +764,7 @@ Qed. Lemma volatile_load_ok: forall chunk, extcall_properties (volatile_load_sem chunk) - (mksignature (Tint :: nil) (Some (type_of_chunk chunk))). + (mksignature (Tint :: nil) (Some (type_of_chunk chunk)) cc_default). Proof. intros; constructor; intros. (* well typed *) @@ -826,7 +826,7 @@ Qed. Lemma volatile_load_global_ok: forall chunk id ofs, extcall_properties (volatile_load_global_sem chunk id ofs) - (mksignature nil (Some (type_of_chunk chunk))). + (mksignature nil (Some (type_of_chunk chunk)) cc_default). Proof. intros; constructor; intros. (* well typed *) @@ -967,7 +967,7 @@ Qed. Lemma volatile_store_ok: forall chunk, extcall_properties (volatile_store_sem chunk) - (mksignature (Tint :: type_of_chunk chunk :: nil) None). + (mksignature (Tint :: type_of_chunk chunk :: nil) None cc_default). Proof. intros; constructor; intros. (* well typed *) @@ -1022,7 +1022,7 @@ Qed. Lemma volatile_store_global_ok: forall chunk id ofs, extcall_properties (volatile_store_global_sem chunk id ofs) - (mksignature (type_of_chunk chunk :: nil) None). + (mksignature (type_of_chunk chunk :: nil) None cc_default). Proof. intros; constructor; intros. (* well typed *) @@ -1070,7 +1070,7 @@ Inductive extcall_malloc_sem (F V: Type) (ge: Genv.t F V): Lemma extcall_malloc_ok: extcall_properties extcall_malloc_sem - (mksignature (Tint :: nil) (Some Tint)). + (mksignature (Tint :: nil) (Some Tint) cc_default). Proof. assert (UNCHANGED: forall (P: block -> Z -> Prop) m n m' b m'', @@ -1145,7 +1145,7 @@ Inductive extcall_free_sem (F V: Type) (ge: Genv.t F V): Lemma extcall_free_ok: extcall_properties extcall_free_sem - (mksignature (Tint :: nil) None). + (mksignature (Tint :: nil) None cc_default). Proof. constructor; intros. (* well typed *) @@ -1241,7 +1241,7 @@ Inductive extcall_memcpy_sem (sz al: Z) (F V: Type) (ge: Genv.t F V): list val - Lemma extcall_memcpy_ok: forall sz al, - extcall_properties (extcall_memcpy_sem sz al) (mksignature (Tint :: Tint :: nil) None). + extcall_properties (extcall_memcpy_sem sz al) (mksignature (Tint :: Tint :: nil) None cc_default). Proof. intros. constructor. (* return type *) @@ -1337,7 +1337,7 @@ Inductive extcall_annot_sem (text: ident) (targs: list annot_arg) (F V: Type) (g Lemma extcall_annot_ok: forall text targs, - extcall_properties (extcall_annot_sem text targs) (mksignature (annot_args_typ targs) None). + extcall_properties (extcall_annot_sem text targs) (mksignature (annot_args_typ targs) None cc_default). Proof. intros; constructor; intros. (* well typed *) @@ -1381,7 +1381,7 @@ Inductive extcall_annot_val_sem (text: ident) (targ: typ) (F V: Type) (ge: Genv. Lemma extcall_annot_val_ok: forall text targ, - extcall_properties (extcall_annot_val_sem text targ) (mksignature (targ :: nil) (Some targ)). + extcall_properties (extcall_annot_val_sem text targ) (mksignature (targ :: nil) (Some targ) cc_default). Proof. intros; constructor; intros. (* well typed *) @@ -1433,7 +1433,7 @@ Axiom external_functions_properties: Parameter inline_assembly_sem: ident -> extcall_sem. Axiom inline_assembly_properties: - forall id, extcall_properties (inline_assembly_sem id) (mksignature nil None). + forall id, extcall_properties (inline_assembly_sem id) (mksignature nil None cc_default). (** ** Combined semantics of external calls *) diff --git a/cparser/C.mli b/cparser/C.mli index 5d90407..b1e44eb 100644 --- a/cparser/C.mli +++ b/cparser/C.mli @@ -231,7 +231,8 @@ type fundef = { fd_storage: storage; fd_inline: bool; fd_name: ident; - fd_ret: typ; (* return type *) + fd_attrib: attributes; + fd_ret: typ; (* return type *) fd_params: (ident * typ) list; (* formal parameters *) fd_vararg: bool; (* variable arguments? *) fd_locals: decl list; (* local variables *) diff --git a/cparser/Cprint.ml b/cparser/Cprint.ml index c6864ff..0bbea68 100644 --- a/cparser/Cprint.ml +++ b/cparser/Cprint.ml @@ -458,7 +458,8 @@ let fundef pp f = fprintf pp "@[<hov 2>%s%a" (if f.fd_inline then "inline " else "") storage f.fd_storage; - simple_decl pp (f.fd_name, TFun(f.fd_ret, Some f.fd_params, f.fd_vararg, [])); + simple_decl pp (f.fd_name, + TFun(f.fd_ret, Some f.fd_params, f.fd_vararg, f.fd_attrib)); fprintf pp "@]@ @[<v 2>{@ "; List.iter (fun d -> fprintf pp "%a@ " full_decl d) f.fd_locals; stmt_block pp f.fd_body; diff --git a/cparser/Cutil.ml b/cparser/Cutil.ml index 70ca8bc..ea4a905 100644 --- a/cparser/Cutil.ml +++ b/cparser/Cutil.ml @@ -453,7 +453,7 @@ let int_representable v nbits sgn = (* Type of a function definition *) let fundef_typ fd = - TFun(fd.fd_ret, Some fd.fd_params, fd.fd_vararg, []) + TFun(fd.fd_ret, Some fd.fd_params, fd.fd_vararg, fd.fd_attrib) (* Signedness of integer kinds *) diff --git a/cparser/Elab.ml b/cparser/Elab.ml index d0e1b28..313569b 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -1567,9 +1567,9 @@ let elab_fundef env (spec, name) body loc1 loc2 = | TFun(ty_ret, None, vararg, attr) -> TFun(ty_ret, Some [], vararg, attr) | _ -> ty in (* Extract info from type *) - let (ty_ret, params, vararg) = + let (ty_ret, params, vararg, attr) = match ty with - | TFun(ty_ret, Some params, vararg, attr) -> (ty_ret, params, vararg) + | TFun(ty_ret, Some params, vararg, attr) -> (ty_ret, params, vararg, attr) | _ -> fatal_error loc1 "wrong type for function definition" in (* Enter function in the environment, for recursive references *) let (fun_id, env1) = enter_or_refine_ident false loc1 env s sto ty in @@ -1584,6 +1584,7 @@ let elab_fundef env (spec, name) body loc1 loc2 = { fd_storage = sto; fd_inline = inline; fd_name = fun_id; + fd_attrib = attr; fd_ret = ty_ret; fd_params = params; fd_vararg = vararg; diff --git a/cparser/Rename.ml b/cparser/Rename.ml index 59b7bd7..f4bab8e 100644 --- a/cparser/Rename.ml +++ b/cparser/Rename.ml @@ -190,6 +190,7 @@ let fundef env f = ( { fd_storage = f.fd_storage; fd_inline = f.fd_inline; fd_name = name'; + fd_attrib = f.fd_attrib; fd_ret = typ env0 f.fd_ret; fd_params = params'; fd_vararg = f.fd_vararg; diff --git a/driver/Clflags.ml b/driver/Clflags.ml index 442ca68..4f41bf6 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -48,6 +48,7 @@ let option_E = ref false let option_S = ref false let option_c = ref false let option_v = ref false +let option_interp = ref false let option_small_data = ref (if Configuration.arch = "powerpc" && Configuration.variant = "eabi" diff --git a/driver/Driver.ml b/driver/Driver.ml index bb9ac7c..44037b2 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -234,8 +234,6 @@ let linker exe_name files = (* Processing of a .c file *) -let option_interp = ref false - let process_c_file sourcename = if !option_E then begin preprocess sourcename (output_filename_default "-"); diff --git a/driver/Interp.ml b/driver/Interp.ml index 5fcca0b..4f9debd 100644 --- a/driver/Interp.ml +++ b/driver/Interp.ml @@ -361,14 +361,10 @@ let do_printf m fmt args = (* Implementation of external functions *) -let re_stub = Str.regexp "\\$[ifl]*$" - -let chop_stub name = Str.replace_first re_stub "" name - let (>>=) opt f = match opt with None -> None | Some arg -> f arg let do_external_function id sg ge w args m = - match chop_stub(extern_atom id), args with + match extern_atom id, args with | "printf", Vptr(b, ofs) :: args' -> extract_string m b ofs >>= fun fmt -> print_string (do_printf m fmt args'); @@ -594,7 +590,8 @@ let change_main_function p old_main old_main_ty = let body = Sreturn(Some(Ecall(old_main, Econs(arg1, Econs(arg2, Enil)), type_int32s))) in let new_main_fn = - { fn_return = type_int32s; fn_params = []; fn_vars = []; fn_body = body } in + { fn_return = type_int32s; fn_callconv = cc_default; + fn_params = []; fn_vars = []; fn_body = body } in let new_main_id = intern_string "___main" in { prog_main = new_main_id; prog_defs = (new_main_id, Gfun(Internal new_main_fn)) :: p.prog_defs } @@ -611,10 +608,10 @@ let fixup_main p = None | Some main_fd -> match type_of_fundef main_fd with - | Tfunction(Tnil, Tint(I32, Signed, _)) -> + | Tfunction(Tnil, Tint(I32, Signed, _), _) -> Some p | Tfunction(Tcons(Tint _, Tcons(Tpointer(Tpointer(Tint(I8,_,_),_),_), Tnil)), - Tint _) as ty -> + Tint _, _) as ty -> Some (change_main_function p p.prog_main ty) | _ -> fprintf err_formatter "ERROR: wrong type for main() function"; diff --git a/ia32/PrintAsm.ml b/ia32/PrintAsm.ml index 3badbfc..1e65ee8 100644 --- a/ia32/PrintAsm.ml +++ b/ia32/PrintAsm.ml @@ -61,13 +61,8 @@ let raw_symbol oc s = | ELF -> fprintf oc "%s" s | MacOS | Cygwin -> fprintf oc "_%s" s -let re_variadic_stub = Str.regexp "\\(.*\\)\\$[ifl]*$" - let symbol oc symb = - let s = extern_atom symb in - if Str.string_match re_variadic_stub s 0 - then raw_symbol oc (Str.matched_group 1 s) - else raw_symbol oc s + raw_symbol oc (extern_atom symb) let symbol_offset oc (symb, ofs) = symbol oc symb; diff --git a/powerpc/PrintAsm.ml b/powerpc/PrintAsm.ml index 87d22f2..830a502 100644 --- a/powerpc/PrintAsm.ml +++ b/powerpc/PrintAsm.ml @@ -48,12 +48,6 @@ let transl_label lbl = Hashtbl.add current_function_labels lbl lbl'; lbl' -(* Record identifiers of functions that need a special stub *) - -module IdentSet = Set.Make(struct type t = ident let compare = compare end) - -let stubbed_functions = ref IdentSet.empty - (* Basic printing functions *) let coqint oc n = @@ -63,9 +57,7 @@ let raw_symbol oc s = fprintf oc "%s" s let symbol oc symb = - if IdentSet.mem symb !stubbed_functions - then fprintf oc ".L%s$stub" (extern_atom symb) - else fprintf oc "%s" (extern_atom symb) + fprintf oc "%s" (extern_atom symb) let symbol_offset oc (symb, ofs) = symbol oc symb; @@ -619,6 +611,16 @@ let print_builtin_inline oc name args res = end; fprintf oc "%s end builtin %s\n" comment name +(* Calls to variadic functions: condition bit 6 must be set + if at least one argument is a float; clear otherwise *) + +let set_cr6 oc sg = + if sg.sig_cc.cc_vararg then begin + if List.mem Tfloat sg.sig_args + then fprintf oc " creqv 6, 6, 6\n" + else fprintf oc " crxor 6, 6, 6\n" + end + (* Determine if the displacement of a conditional branch fits the short form *) let short_cond_branch tbl pc lbl_dest = @@ -669,8 +671,10 @@ let print_instruction oc tbl pc fallthrough = function | Pb lbl -> fprintf oc " b %a\n" label (transl_label lbl) | Pbctr sg -> + set_cr6 oc sg; fprintf oc " bctr\n" | Pbctrl sg -> + set_cr6 oc sg; fprintf oc " bctrl\n" | Pbf(bit, lbl) -> if !Clflags.option_faligncondbranchs > 0 then @@ -684,8 +688,10 @@ let print_instruction oc tbl pc fallthrough = function fprintf oc "%a:\n" label next end | Pbl(s, sg) -> + set_cr6 oc sg; fprintf oc " bl %a\n" symbol s | Pbs(s, sg) -> + set_cr6 oc sg; fprintf oc " b %a\n" symbol s | Pblr -> fprintf oc " blr\n" @@ -1043,49 +1049,15 @@ let print_function oc name fn = jumptables := [] end -(* Generation of stub functions *) - -let re_variadic_stub = Str.regexp "\\(.*\\)\\$[ifl]*$" - -(* Stubs for EABI *) - -let variadic_stub oc stub_name fun_name args = - section oc Section_text; - fprintf oc " .balign 4\n"; - fprintf oc ".L%s$stub:\n" stub_name; - (* bit 6 must be set if at least one argument is a float; clear otherwise *) - if List.mem Tfloat args - then fprintf oc " creqv 6, 6, 6\n" - else fprintf oc " crxor 6, 6, 6\n"; - fprintf oc " b %s\n" fun_name - -let stub_function oc name sg = - let name = extern_atom name in - (* Only variadic functions need a stub *) - if Str.string_match re_variadic_stub name 0 - then variadic_stub oc name (Str.matched_group 1 name) sg.sig_args - -let function_needs_stub name = - Str.string_match re_variadic_stub (extern_atom name) 0 - (* Generation of whole programs *) let print_fundef oc name defn = match defn with | Internal code -> print_function oc name code - | External ((EF_external _ | EF_malloc | EF_free) as ef) -> - if function_needs_stub name then stub_function oc name (ef_sig ef) | External _ -> () -let record_extfun (name, gd) = - match gd with - | Gfun(External (EF_external _ | EF_malloc | EF_free)) -> - if function_needs_stub name then - stubbed_functions := IdentSet.add name !stubbed_functions - | _ -> () - let print_init oc = function | Init_int8 n -> fprintf oc " .byte %ld\n" (camlint_of_coqint n) @@ -1171,8 +1143,6 @@ let print_prologue oc = fprintf oc " .xopt asm-debug-on\n" let print_program oc p = - stubbed_functions := IdentSet.empty; - List.iter record_extfun p.prog_defs; reset_file_line(); print_prologue oc; List.iter (print_globdef oc) p.prog_defs |