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

9 files changed, 26 insertions, 25 deletions

diff --git a/backend/CMparser.mly b/backend/CMparser.mly
index b28578e1..5d93b84a 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 9f7244b9..c12c6fce 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 c80f424d..db414a2c 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 e60600a2..dd79c8e3 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 3c524368..56d1eb99 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 f0fb56ae..ff72a828 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 33c38f56..4c53c5ea 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 b2e1e89c..045250da 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 76cc79d2..09f29afc 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.