Simpler, more robust emulation of calls to variadic functions:

- C function types and Cminor signatures annotated by calling conventions.
  esp. vararg / not vararg
- Cshmgen: generate correct code for function call where there are
  more arguments than listed in the function prototype.  This is
  still undefined behavior according to the formal semantics,
  but correct code is generated.
- C2C, */PrintAsm.ml: remove "printf$iif" hack.
- powerpc/, checklink/: don't generate stubs for variadic functions.


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2386 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

2 files changed, 44 insertions, 26 deletions

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 *)