Revised handling of annotation statements, and more generally built-in functions, and more generally external functions

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

5 files changed, 200 insertions, 61 deletions

diff --git a/powerpc/Asm.v b/powerpc/Asm.v
index d698524d..fc29db04 100644
--- a/powerpc/Asm.v
+++ b/powerpc/Asm.v
@@ -130,7 +130,7 @@ Inductive instruction : Type :=
   | Paddi: ireg -> ireg -> constant -> instruction            (**r add immediate *)
   | Paddis: ireg -> ireg -> constant -> instruction           (**r add immediate high *)
   | Paddze: ireg -> ireg -> instruction                       (**r add Carry bit *)
-  | Pallocframe: Z -> int -> instruction                 (**r allocate new stack frame *)
+  | Pallocframe: Z -> int -> instruction                      (**r allocate new stack frame *)
   | Pand_: ireg -> ireg -> ireg -> instruction                (**r bitwise and *)
   | Pandc: ireg -> ireg -> ireg -> instruction                (**r bitwise and-complement *)
   | Pandi_: ireg -> ireg -> constant -> instruction           (**r and immediate and set conditions *)
@@ -154,7 +154,7 @@ Inductive instruction : Type :=
   | Peqv: ireg -> ireg -> ireg -> instruction                 (**r bitwise not-xor *)
   | Pextsb: ireg -> ireg -> instruction                       (**r 8-bit sign extension *)
   | Pextsh: ireg -> ireg -> instruction                       (**r 16-bit sign extension *)
-  | Pfreeframe: Z -> int -> instruction                  (**r deallocate stack frame and restore previous frame *)
+  | Pfreeframe: Z -> int -> instruction                       (**r deallocate stack frame and restore previous frame *)
   | Pfabs: freg -> freg -> instruction                        (**r float absolute value *)
   | Pfadd: freg -> freg -> freg -> instruction                (**r float addition *)
   | Pfcmpu: freg -> freg -> instruction                       (**r float comparison *)
@@ -215,7 +215,12 @@ Inductive instruction : Type :=
   | Pxori: ireg -> ireg -> constant -> instruction            (**r bitwise xor with immediate *)
   | Pxoris: ireg -> ireg -> constant -> instruction           (**r bitwise xor with immediate high *)
   | Plabel: label -> instruction                              (**r define a code label *)
-  | Pbuiltin: external_function -> list preg -> preg -> instruction. (**r built-in *)
+  | Pbuiltin: external_function -> list preg -> preg -> instruction (**r built-in function *)
+  | Pannot: external_function -> list annot_param -> instruction (**r annotation statement *)
+
+with annot_param : Type :=
+  | APreg: preg -> annot_param
+  | APstack: memory_chunk -> Z -> annot_param.
 
 (** The pseudo-instructions are the following:
 
@@ -740,6 +745,8 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome
       OK (nextinstr rs) m
   | Pbuiltin ef args res =>
       Error    (**r treated specially below *)
+  | Pannot ef args =>
+      Error    (**r treated specially below *)
   end.
 
 (** Translation of the LTL/Linear/Mach view of machine registers
@@ -803,20 +810,27 @@ Inductive extcall_arg (rs: regset) (m: mem): loc -> val -> Prop :=
       Mem.loadv Mfloat64 m (Val.add (rs (IR GPR1)) (Vint (Int.repr bofs))) = Some v ->
       extcall_arg rs m (S (Outgoing ofs Tfloat)) v.
 
-Inductive extcall_args (rs: regset) (m: mem): list loc -> list val -> Prop :=
-  | extcall_args_nil:
-      extcall_args rs m nil nil
-  | extcall_args_cons: forall l1 ll v1 vl,
-      extcall_arg rs m l1 v1 -> extcall_args rs m ll vl ->
-      extcall_args rs m (l1 :: ll) (v1 :: vl).
-
 Definition extcall_arguments
     (rs: regset) (m: mem) (sg: signature) (args: list val) : Prop :=
-  extcall_args rs m (loc_arguments sg) args.
+  list_forall2 (extcall_arg rs m) (loc_arguments sg) args.
 
 Definition loc_external_result (sg: signature) : preg :=
   preg_of (loc_result sg).
 
+(** Extract the values of the arguments of an annotation. *)
+
+Inductive annot_arg (rs: regset) (m: mem): annot_param -> val -> Prop :=
+  | annot_arg_reg: forall r,
+      annot_arg rs m (APreg r) (rs r)
+  | annot_arg_stack: forall chunk ofs stk base v,
+      rs (IR GPR1) = Vptr stk base ->
+      Mem.load chunk m stk (Int.unsigned base + ofs) = Some v ->
+      annot_arg rs m (APstack chunk ofs) v.
+
+Definition annot_arguments
+    (rs: regset) (m: mem) (params: list annot_param) (args: list val) : Prop :=
+  list_forall2 (annot_arg rs m) params args.
+
 (** Execution of the instruction at [rs#PC]. *)
 
 Inductive state: Type :=
@@ -841,6 +855,15 @@ Inductive step: state -> trace -> state -> Prop :=
                                 #FPR12 <- Vundef #FPR13 <- Vundef
                                 #FPR0 <- Vundef #CTR <- Vundef
                                 #res <- v)) m')
+  | exec_step_annot:
+      forall b ofs c ef args rs m vargs t v m',
+      rs PC = Vptr b ofs ->
+      Genv.find_funct_ptr ge b = Some (Internal c) ->
+      find_instr (Int.unsigned ofs) c = Some (Pannot ef args) ->
+      annot_arguments rs m args vargs ->
+      external_call ef ge vargs m t v m' ->
+      step (State rs m) t
+           (State (nextinstr rs) m')
   | exec_step_external:
       forall b ef args res rs m t rs' m',
       rs PC = Vptr b Int.zero ->
diff --git a/powerpc/Asmgen.v b/powerpc/Asmgen.v
index 6b47d750..4370753b 100644
--- a/powerpc/Asmgen.v
+++ b/powerpc/Asmgen.v
@@ -399,6 +399,14 @@ Definition transl_load_store
       (* should not happen *) k
   end.
 
+(** Translation of arguments to annotations *)
+
+Definition transl_annot_param (p: Mach.annot_param) : Asm.annot_param :=
+  match p with
+  | Mach.APreg r => APreg (preg_of r)
+  | Mach.APstack chunk ofs => APstack chunk ofs
+  end.
+
 (** Translation of a Mach instruction. *)
 
 Definition transl_instr (f: Mach.function) (i: Mach.instruction) (k: code) :=
@@ -478,6 +486,8 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction) (k: code) :=
       Pbs symb :: k
   | Mbuiltin ef args res =>
       Pbuiltin ef (map preg_of args) (preg_of res) :: k
+  | Mannot ef args =>
+      Pannot ef (map transl_annot_param args) :: k
   | Mlabel lbl =>
       Plabel lbl :: k
   | Mgoto lbl =>
diff --git a/powerpc/Asmgenproof.v b/powerpc/Asmgenproof.v
index 3846a6cc..0efe646d 100644
--- a/powerpc/Asmgenproof.v
+++ b/powerpc/Asmgenproof.v
@@ -447,6 +447,7 @@ Proof.
   destruct op; destruct args; try (destruct args); try (destruct args); try (destruct args);
   try reflexivity; autorewrite with labels; try reflexivity.
   case (mreg_type m); reflexivity.
+  case (symbol_is_small_data i i0); reflexivity.
   case (Int.eq (high_s i) Int.zero); autorewrite with labels; reflexivity.
   case (Int.eq (high_s i) Int.zero); autorewrite with labels; reflexivity.
 Qed.
@@ -1126,6 +1127,35 @@ Proof.
   intros. repeat rewrite Pregmap.gso; auto. 
 Qed.
 
+Lemma exec_Mannot_prop:
+  forall (s : list stackframe) (f : block) (sp : val)
+         (ms : Mach.regset) (m : mem) (ef : external_function)
+         (args : list Mach.annot_param) (b : list Mach.instruction)
+         (vargs: list val) (t : trace) (v : val) (m' : mem),
+  Machsem.annot_arguments ms m sp args vargs ->
+  external_call ef ge vargs m t v m' ->
+  exec_instr_prop (Machsem.State s f sp (Mannot ef args :: b) ms m) t
+                  (Machsem.State s f sp b ms m').
+Proof.
+  intros; red; intros; inv MS.
+  inv AT. simpl in H3.
+  generalize (functions_transl _ _ FIND); intro FN.
+  generalize (functions_transl_no_overflow _ _ FIND); intro NOOV.
+  exploit annot_arguments_match; eauto. intros [vargs' [P Q]]. 
+  exploit external_call_mem_extends; eauto.
+  intros [vres' [m2' [A [B [C D]]]]].
+  left. econstructor; split. apply plus_one. 
+  eapply exec_step_annot. eauto. eauto.
+  eapply find_instr_tail; eauto. eauto.
+  eapply external_call_symbols_preserved; eauto.
+  exact symbols_preserved. exact varinfo_preserved.
+  econstructor; eauto with coqlib.
+  unfold nextinstr. rewrite Pregmap.gss. 
+  rewrite <- H1; simpl. econstructor; auto.
+  eapply code_tail_next_int; eauto. 
+  apply agree_nextinstr. auto.
+Qed.
+
 Lemma exec_Mgoto_prop:
   forall (s : list stackframe) (fb : block) (f : function) (sp : val)
          (lbl : Mach.label) (c : list Mach.instruction) (ms : Mach.regset)
@@ -1458,6 +1488,7 @@ Proof
            exec_Mcall_prop
            exec_Mtailcall_prop
            exec_Mbuiltin_prop
+           exec_Mannot_prop
            exec_Mgoto_prop
            exec_Mcond_true_prop
            exec_Mcond_false_prop
diff --git a/powerpc/Asmgenproof1.v b/powerpc/Asmgenproof1.v
index 8f6f7255..ee3aa38a 100644
--- a/powerpc/Asmgenproof1.v
+++ b/powerpc/Asmgenproof1.v
@@ -503,13 +503,13 @@ Qed.
 Lemma extcall_args_match:
   forall ms sp rs m m', agree ms sp rs -> Mem.extends m m' ->
   forall ll vl,
-  Machsem.extcall_args ms m sp ll vl ->
-  exists vl', Asm.extcall_args rs m' ll vl' /\ Val.lessdef_list vl vl'.
+  list_forall2 (Machsem.extcall_arg ms m sp) ll vl ->
+  exists vl', list_forall2 (Asm.extcall_arg rs m') ll vl' /\ Val.lessdef_list vl vl'.
 Proof.
   induction 3; intros. 
   exists (@nil val); split. constructor. constructor.
   exploit extcall_arg_match; eauto. intros [v1' [A B]].
-  exploit IHextcall_args; eauto. intros [vl' [C D]].
+  destruct IHlist_forall2 as [vl' [C D]].
   exists (v1' :: vl'); split; constructor; auto.
 Qed.
 
@@ -523,6 +523,38 @@ Proof.
   eapply extcall_args_match; eauto.
 Qed.
 
+(** Translation of arguments to annotations. *)
+
+Lemma annot_arg_match:
+  forall ms sp rs m m' p v,
+  agree ms sp rs ->
+  Mem.extends m m' ->
+  Machsem.annot_arg ms m sp p v ->
+  exists v', Asm.annot_arg rs m' (transl_annot_param p) v' /\ Val.lessdef v v'.
+Proof.
+  intros. inv H1; simpl.
+(* reg *)
+  exists (rs (preg_of r)); split. constructor. eapply preg_val; eauto.
+(* stack *)
+  exploit Mem.load_extends; eauto. intros [v' [A B]].
+  exists v'; split; auto. 
+  inv H. econstructor; eauto. 
+Qed.
+
+Lemma annot_arguments_match:
+  forall ms sp rs m m', agree ms sp rs -> Mem.extends m m' ->
+  forall pl vl,
+  Machsem.annot_arguments ms m sp pl vl ->
+  exists vl', Asm.annot_arguments rs m' (map transl_annot_param pl) vl'
+           /\ Val.lessdef_list vl vl'.
+Proof.
+  induction 3; intros. 
+  exists (@nil val); split. constructor. constructor.
+  exploit annot_arg_match; eauto. intros [v1' [A B]].
+  destruct IHlist_forall2 as [vl' [C D]].
+  exists (v1' :: vl'); split; constructor; auto.
+Qed.
+
 (** * Execution of straight-line code *)
 
 Section STRAIGHTLINE.
diff --git a/powerpc/PrintAsm.ml b/powerpc/PrintAsm.ml
index ef53411b..0c199322 100644
--- a/powerpc/PrintAsm.ml
+++ b/powerpc/PrintAsm.ml
@@ -17,6 +17,7 @@ open Datatypes
 open Camlcoq
 open Sections
 open AST
+open Memdata
 open Asm
 
 (* Recognition of target ABI and asm syntax *)
@@ -264,7 +265,9 @@ let rec log2 n =
   assert (n > 0);
   if n = 1 then 0 else 1 + log2 (n lsr 1)
 
-(* Built-ins.  They come in two flavors: 
+(* Built-ins.  They come in three flavors: 
+   - annotation statements: take their arguments in registers or stack
+     locations; generate no code;
    - inlined by the compiler: take their arguments in arbitrary
      registers; preserve all registers except the temporaries
      (GPR0, GPR11, GPR12,  FPR0, FPR12, FPR13);
@@ -272,13 +275,11 @@ let rec log2 n =
      locations dictated by the calling conventions; preserve
      callee-save regs only. *)
 
-(* Handling of __builtin_annotation *)
-
-let re_builtin_annotation = Str.regexp "__builtin_annotation_\"\\(.*\\)\"$"
+(* Handling of annotations *)
 
 let re_annot_param = Str.regexp "%%\\|%[1-9][0-9]*"
 
-let print_annotation oc txt args res =
+let print_annot_text print_arg oc txt args =
   fprintf oc "%s annotation: " comment;
   let print_fragment = function
   | Str.Text s ->
@@ -288,23 +289,29 @@ let print_annotation oc txt args res =
   | Str.Delim s ->
       let n = int_of_string (String.sub s 1 (String.length s - 1)) in
       try
-        preg oc (List.nth args (n-1))
+        print_arg oc (List.nth args (n-1))
       with Failure _ ->
         fprintf oc "<bad parameter %s>" s in
   List.iter print_fragment (Str.full_split re_annot_param txt);
-  fprintf oc "\n";
+  fprintf oc "\n"
+
+let print_annot_stmt oc txt args =
+  let print_annot_param oc = function
+  | APreg r -> preg oc r
+  | APstack(chunk, ofs) ->
+      fprintf oc "mem(R1 + %a, %a)" coqint ofs coqint (size_chunk chunk) in
+  print_annot_text print_annot_param oc txt args
+
+let print_annot_val oc txt args res =
+  print_annot_text preg oc txt args;
   match args, res with
-  | [], _ -> ()
   | IR src :: _, IR dst ->
       if dst <> src then fprintf oc "	mr	%a, %a\n" ireg dst ireg src 
   | FR src :: _, FR dst ->
       if dst <> src then fprintf oc "	fmr	%a, %a\n" freg dst freg src 
   | _, _ -> assert false
 
-(* Handling of __builtin_memcpy_alX_szY *)
-
-let re_builtin_memcpy =
-   Str.regexp "__builtin_memcpy\\(_al\\([248]\\)\\)?_sz\\([0-9]+\\)$"
+(* Handling of memcpy *)
 
 (* On the PowerPC, unaligned accesses to 16- and 32-bit integers are
    fast, but unaligned accesses to 64-bit floats can be slow
@@ -312,7 +319,9 @@ let re_builtin_memcpy =
    So, use 64-bit accesses only if alignment >= 8.
    Note that lfd and stfd cannot trap on ill-formed floats. *)
 
-let print_builtin_memcpy oc sz al dst src =
+let print_builtin_memcpy oc sz al args =
+  let (dst, src) =
+    match args with [IR d; IR s] -> (d, s) | _ -> assert false in
   let rec copy ofs sz =
     if sz >= 8 && al >= 8 then begin
       fprintf oc "	lfd	%a, %d(%a)\n" freg FPR0 ofs ireg src;
@@ -331,42 +340,61 @@ let print_builtin_memcpy oc sz al dst src =
       fprintf oc "	stb	%a, %d(%a)\n" ireg GPR0 ofs ireg dst;
       copy (ofs + 1) (sz - 1)
     end in
-  copy 0 sz
+  fprintf oc "%s begin builtin __builtin_memcpy, size = %d, alignment = %d\n"
+          comment sz al;
+  copy 0 sz;
+  fprintf oc "%s end builtin __builtin_memcpy\n" comment
 
-(* Handling of compiler-inlined builtins *)
+(* Handling of volatile reads and writes *)
 
-let print_builtin_inlined oc name args res =
-  fprintf oc "%s begin builtin %s\n" comment name;
-  (* Can use as temporaries: GPR0, GPR11, GPR12,  FPR0, FPR12, FPR13 *)
-  begin match name, args, res with
-  (* Volatile reads *)
-  | "__builtin_volatile_read_int8unsigned", [IR addr], IR res ->
+let print_builtin_vload oc chunk args res =
+  fprintf oc "%s begin builtin __builtin_volatile_read\n" comment;
+  begin match chunk, args, res with
+  | Mint8unsigned, [IR addr], IR res ->
       fprintf oc "	lbz	%a, 0(%a)\n" ireg res ireg addr
-  | "__builtin_volatile_read_int8signed", [IR addr], IR res ->
+  | Mint8signed, [IR addr], IR res ->
       fprintf oc "	lbz	%a, 0(%a)\n" ireg res ireg addr;
       fprintf oc "	extsb	%a, %a\n" ireg res ireg res
-  | "__builtin_volatile_read_int16unsigned", [IR addr], IR res ->
+  | Mint16unsigned, [IR addr], IR res ->
       fprintf oc "	lhz	%a, 0(%a)\n" ireg res ireg addr
-  | "__builtin_volatile_read_int16signed", [IR addr], IR res ->
+  | Mint16signed, [IR addr], IR res ->
       fprintf oc "	lha	%a, 0(%a)\n" ireg res ireg addr
-  | ("__builtin_volatile_read_int32"|"__builtin_volatile_read_pointer"), [IR addr], IR res ->
+  | Mint32, [IR addr], IR res ->
       fprintf oc "	lwz	%a, 0(%a)\n" ireg res ireg addr
-  | "__builtin_volatile_read_float32", [IR addr], FR res ->
+  | Mfloat32, [IR addr], FR res ->
       fprintf oc "	lfs	%a, 0(%a)\n" freg res ireg addr
-  | "__builtin_volatile_read_float64", [IR addr], FR res ->
+  | Mfloat64, [IR addr], FR res ->
       fprintf oc "	lfd	%a, 0(%a)\n" freg res ireg addr
-  (* Volatile writes *)
-  | ("__builtin_volatile_write_int8unsigned"|"__builtin_volatile_write_int8signed"), [IR addr; IR src], _ ->
+  | _ ->
+      assert false
+  end;
+  fprintf oc "%s end builtin __builtin_volatile_read\n" comment
+
+let print_builtin_vstore oc chunk args =
+  fprintf oc "%s begin builtin __builtin_volatile_write\n" comment;
+  begin match chunk, args with
+  | (Mint8signed | Mint8unsigned), [IR addr; IR src] ->
       fprintf oc "	stb	%a, 0(%a)\n" ireg src ireg addr
-  | ("__builtin_volatile_write_int16unsigned"|"__builtin_volatile_write_int16signed"), [IR addr; IR src], _ ->
+  | (Mint16signed | Mint16unsigned), [IR addr; IR src] ->
       fprintf oc "	sth	%a, 0(%a)\n" ireg src ireg addr
-  | ("__builtin_volatile_write_int32"|"__builtin_volatile_write_pointer"), [IR addr; IR src], _ ->
+  | Mint32, [IR addr; IR src] ->
       fprintf oc "	stw	%a, 0(%a)\n" ireg src ireg addr
-  | "__builtin_volatile_write_float32", [IR addr; FR src], _ ->
+  | Mfloat32, [IR addr; FR src] ->
       fprintf oc "	frsp	%a, %a\n" freg FPR13 freg src;
       fprintf oc "	stfs	%a, 0(%a)\n" freg FPR13 ireg addr
-  | "__builtin_volatile_write_float64", [IR addr; FR src], _ ->
+  | Mfloat64, [IR addr; FR src] ->
       fprintf oc "	stfd	%a, 0(%a)\n" freg src ireg addr
+  | _ ->
+      assert false
+  end;
+  fprintf oc "%s end builtin __builtin_volatile_write\n" comment
+
+(* Handling of compiler-inlined builtins *)
+
+let print_builtin_inline oc name args res =
+  fprintf oc "%s begin builtin %s\n" comment name;
+  (* Can use as temporaries: GPR0, GPR11, GPR12,  FPR0, FPR12, FPR13 *)
+  begin match name, args, res with
   (* Integer arithmetic *)
   | "__builtin_mulhw", [IR a1; IR a2], IR res ->
       fprintf oc "	mulhw	%a, %a, %a\n" ireg res ireg a1 ireg a2
@@ -407,11 +435,6 @@ let print_builtin_inlined oc name args res =
       fprintf oc "	isync\n"
   | "__builtin_trap", [], _ ->
       fprintf oc "	trap\n"
-  (* Inlined memcpy *)
-  | name, [IR dst; IR src], _ when Str.string_match re_builtin_memcpy name 0 ->
-      let sz = int_of_string (Str.matched_group 3 name) in
-      let al = try int_of_string (Str.matched_group 2 name) with Not_found -> 1 in
-      print_builtin_memcpy oc sz al dst src
   (* Catch-all *)
   | _ ->
       invalid_arg ("unrecognized builtin " ^ name)
@@ -707,10 +730,28 @@ let print_instruction oc = function
   | Plabel lbl ->
       fprintf oc "%a:\n" label (transl_label lbl)
   | Pbuiltin(ef, args, res) ->
-      let name = extern_atom ef.ef_id in
-      if Str.string_match re_builtin_annotation name 0
-      then print_annotation oc (Str.matched_group 1 name) args res
-      else print_builtin_inlined oc name args res
+      begin match ef with
+      | EF_builtin(name, sg) ->
+          print_builtin_inline oc (extern_atom name) args res
+      | EF_vload chunk ->
+          print_builtin_vload oc chunk args res
+      | EF_vstore chunk ->
+          print_builtin_vstore oc chunk args
+      | EF_memcpy(sz, al) ->
+          print_builtin_memcpy oc (Int32.to_int (camlint_of_coqint sz))
+                                  (Int32.to_int (camlint_of_coqint al)) args
+      | EF_annot_val(txt, targ) ->
+          print_annot_val oc (extern_atom txt) args res
+      | _ ->
+          assert false
+      end
+  | Pannot(ef, args) ->
+      begin match ef with
+      | EF_annot(txt, targs) ->
+          print_annot_stmt oc (extern_atom txt) args
+      | _ ->
+          assert false
+      end
 
 let print_literal oc (lbl, n) =
   let nlo = Int64.to_int32 n
@@ -740,11 +781,13 @@ let print_function oc name code =
   end;
   if !float_literals <> [] then begin
     section oc lit;
+    fprintf oc "	.align 3\n";
     List.iter (print_literal oc) !float_literals;
     float_literals := []
   end;
   if !jumptables <> [] then begin
     section oc jmptbl;
+    fprintf oc "	.align 2\n";
     List.iter (print_jumptable oc) !jumptables;
     jumptables := []
   end
@@ -849,13 +892,13 @@ let non_variadic_stub oc name =
   fprintf oc "	.indirect_symbol _%s\n" name;
   fprintf oc "	.long	0\n"
 
-let stub_function oc name ef =
+let stub_function oc name sg =
   let name = extern_atom name in
   section oc Section_text;
   fprintf oc "	.align 2\n";
   fprintf oc "L%s$stub:\n" name;
   if Str.string_match re_variadic_stub name 0
-  then variadic_stub oc name (Str.matched_group 1 name) (ef_sig ef).sig_args
+  then variadic_stub oc name (Str.matched_group 1 name) sg.sig_args
   else non_variadic_stub oc name
 
 let function_needs_stub name = true
@@ -876,11 +919,11 @@ let variadic_stub oc stub_name fun_name args =
   else fprintf oc "	crxor	6, 6, 6\n";
   fprintf oc "	b	%s\n" fun_name
 
-let stub_function oc name ef =
+let stub_function oc name sg =
   let name = extern_atom name in
   (* Only variadic functions need a stub *)
   if Str.string_match re_variadic_stub name 0
-  then variadic_stub oc name (Str.matched_group 1 name) (ef_sig ef).sig_args
+  then variadic_stub oc name (Str.matched_group 1 name) sg.sig_args
 
 let function_needs_stub name =
   Str.string_match re_variadic_stub (extern_atom name) 0
@@ -902,7 +945,7 @@ let print_fundef oc (Coq_pair(name, defn)) =
   | Internal code ->
       print_function oc name code
   | External ef ->
-      if not (is_builtin_function name) then stub_function oc name ef
+      if not (is_builtin_function name) then stub_function oc name (ef_sig ef)
 
 let record_extfun (Coq_pair(name, defn)) =
   match defn with