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 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.