From ef16a51223a4b73eed74c40ce9938248ab6b4b8a Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Fri, 22 May 2015 11:13:23 +0200 Subject: In AST.calling_conventions, record whether the original C function was "old-style" unprototyped. Use this info in printing function types for Csyntax and Clight. --- cfrontend/C2C.ml | 20 +++++++++++--------- cfrontend/Ctyping.v | 22 ++++++++++++---------- cfrontend/PrintCsyntax.ml | 2 +- common/AST.v | 7 ++++--- 4 files changed, 28 insertions(+), 23 deletions(-) diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index a0e6b259..71328c71 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -437,10 +437,10 @@ let convertAttr a = let n = Cutil.alignas_attribute a in if n > 0 then Some (N.of_int (log2 n)) else None } -let convertCallconv va attr = +let convertCallconv va unproto attr = let sr = Cutil.find_custom_attributes ["structreturn"; "__structreturn"] attr in - { cc_vararg = va; cc_structret = sr <> [] } + { cc_vararg = va; cc_unproto = unproto; cc_structret = sr <> [] } (** Types *) @@ -494,7 +494,7 @@ let rec convertTyp env t = | Some tl -> convertParams env tl end, convertTyp env tres, - convertCallconv va a) + convertCallconv va (targs = None) a) | C.TNamed _ -> convertTyp env (Cutil.unroll env t) | C.TStruct(id, a) -> @@ -796,7 +796,8 @@ let rec convertExpr env e = let targs = convertTypArgs env [] args and tres = convertTyp env e.etyp in let sg = - signature_of_type targs tres {cc_vararg = true; cc_structret = false} in + signature_of_type targs tres + {cc_vararg = true; cc_unproto = false; cc_structret = false} in Ebuiltin(EF_external(intern_string "printf", sg), targs, convertExprList env args, tres) @@ -1031,11 +1032,12 @@ let convertFundef loc env fd = a_access = Sections.Access_default; a_inline = fd.fd_inline && not fd.fd_vararg; (* PR#15 *) a_loc = loc }; - (id', Gfun(Internal {fn_return = ret; - fn_callconv = convertCallconv fd.fd_vararg fd.fd_attrib; - fn_params = params; - fn_vars = vars; - fn_body = body'})) + (id', Gfun(Internal + {fn_return = ret; + fn_callconv = convertCallconv fd.fd_vararg false fd.fd_attrib; + fn_params = params; + fn_vars = vars; + fn_body = body'})) (** External function declaration *) diff --git a/cfrontend/Ctyping.v b/cfrontend/Ctyping.v index d726a525..cde9ad11 100644 --- a/cfrontend/Ctyping.v +++ b/cfrontend/Ctyping.v @@ -179,8 +179,13 @@ Proof. decide equality. Defined. Definition floatsize_eq: forall (x y: floatsize), {x=y} + {x<>y}. Proof. decide equality. Defined. -Definition callconv_eq: forall (x y: calling_convention), {x=y} + {x<>y}. -Proof. decide equality; apply bool_dec. Defined. +Definition callconv_combine (cc1 cc2: calling_convention) : res calling_convention := + if bool_eq cc1.(cc_vararg) cc2.(cc_vararg) then + OK {| cc_vararg := cc1.(cc_vararg); + cc_unproto := cc1.(cc_unproto) && cc2.(cc_unproto); + cc_structret := cc1.(cc_structret) |} + else + Error (msg "incompatible calling conventions"). Fixpoint type_combine (ty1 ty2: type) : res type := match ty1, ty2 with @@ -207,14 +212,11 @@ Fixpoint type_combine (ty1 ty2: type) : res type := | Tfunction args1 res1 cc1, Tfunction args2 res2 cc2 => do res <- type_combine res1 res2; do args <- - match args1, args2 with - | Tnil, _ => OK args2 (* tolerance for unprototyped functions *) - | _, Tnil => OK args1 - | _, _ => typelist_combine args1 args2 - end; - if callconv_eq cc1 cc2 - then OK (Tfunction args res cc1) - else Error (msg "incompatible function types") + (if cc1.(cc_unproto) then OK args2 else + if cc2.(cc_unproto) then OK args1 else + typelist_combine args1 args2); + do cc <- callconv_combine cc1 cc2; + OK (Tfunction args res cc) | Tstruct id1 a1, Tstruct id2 a2 => if ident_eq id1 id2 then OK (Tstruct id1 (attr_combine a1 a2)) diff --git a/cfrontend/PrintCsyntax.ml b/cfrontend/PrintCsyntax.ml index bde61cc7..d890c820 100644 --- a/cfrontend/PrintCsyntax.ml +++ b/cfrontend/PrintCsyntax.ml @@ -123,7 +123,7 @@ let rec name_cdecl id ty = if not first then Buffer.add_string b ", "; Buffer.add_string b (name_cdecl "" t1); add_args false tl in - add_args true args; + if not cconv.cc_unproto then add_args true args; Buffer.add_char b ')'; name_cdecl (Buffer.contents b) res | Tstruct(name, a) -> diff --git a/common/AST.v b/common/AST.v index 08a19789..387eb6b2 100644 --- a/common/AST.v +++ b/common/AST.v @@ -100,12 +100,13 @@ 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 + cc_vararg: bool; (**r variable-arity function *) + cc_unproto: bool; (**r old-style unprototyped function *) + cc_structret: bool (**r function returning a struct *) }. Definition cc_default := - {| cc_vararg := false; cc_structret := false |}. + {| cc_vararg := false; cc_unproto := false; cc_structret := false |}. Record signature : Type := mksignature { sig_args: list typ; -- cgit