diff options
author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-05-29 12:40:28 +0200 |
---|---|---|
committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-05-29 12:40:28 +0200 |
commit | e503983cdc99c6038ada0d0b94f32f02d13210c8 (patch) | |
tree | 76a65ebe3add61f270bd3234bfc925f98497b5a5 | |
parent | 026f2fc382ba4f768ab985fa4c8afe9c0cd3b13b (diff) | |
parent | ef16a51223a4b73eed74c40ce9938248ab6b4b8a (diff) | |
download | compcert-e503983cdc99c6038ada0d0b94f32f02d13210c8.tar.gz compcert-e503983cdc99c6038ada0d0b94f32f02d13210c8.zip |
Merge branch 'master' into json_export
-rw-r--r-- | cfrontend/C2C.ml | 20 | ||||
-rw-r--r-- | cfrontend/Ctyping.v | 31 | ||||
-rw-r--r-- | cfrontend/PrintCsyntax.ml | 2 | ||||
-rw-r--r-- | common/AST.v | 7 |
4 files changed, 31 insertions, 29 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 834895bc..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)) @@ -243,7 +245,8 @@ Definition is_void (ty: type) : bool := Definition type_conditional (ty1 ty2: type) : res type := match typeconv ty1, typeconv ty2 with - | (Tint _ _ _ | Tfloat _ _), (Tint _ _ _ | Tfloat _ _) => + | (Tint _ _ _ | Tlong _ _ | Tfloat _ _), + (Tint _ _ _ | Tlong _ _ | Tfloat _ _) => binarith_type ty1 ty2 "conditional expression" | Tpointer t1 a1, Tpointer t2 a2 => let t := @@ -1011,13 +1014,9 @@ Proof. apply A. apply A. } clear A. unfold type_conditional in H. destruct (typeconv t1) eqn:T1; try discriminate; - destruct (typeconv t2) eqn:T2; inv H; auto using D. -- eapply binarith_type_cast; eauto. -- eapply binarith_type_cast; eauto. + destruct (typeconv t2) eqn:T2; inv H; eauto using D, binarith_type_cast. - split; apply typeconv_cast; unfold wt_cast. rewrite T1; simpl; congruence. rewrite T2; simpl; congruence. -- eapply binarith_type_cast; eauto. -- eapply binarith_type_cast; eauto. - split; apply typeconv_cast; unfold wt_cast. rewrite T1; simpl; congruence. rewrite T2; simpl; congruence. - split; apply typeconv_cast; unfold wt_cast. 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; |