Changed cc_varargs to an option type

Instead of being a simple boolean we now use an option type to record
the number of fixed (non-vararg) arguments.  Hence, `None` means
not vararg, and `Some n` means `n` fixed arguments followed with varargs.

12 files changed, 36 insertions, 27 deletions

diff --git a/arm/Asmexpand.ml b/arm/Asmexpand.ml
index f4e79a37..15cbebec 100644
--- a/arm/Asmexpand.ml
+++ b/arm/Asmexpand.ml
@@ -545,7 +545,7 @@ module FixupHF = struct
       end
 
   let fixup_arguments dir sg =
-    if sg.sig_cc.cc_vararg then
+    if sg.sig_cc.cc_vararg <> None then
       FixupEABI.fixup_arguments dir sg
     else begin
       let act = fixup_actions (Array.make 16 false) 0 sg.sig_args in
@@ -555,7 +555,7 @@ module FixupHF = struct
     end
 
   let fixup_result dir sg =
-    if sg.sig_cc.cc_vararg then
+    if sg.sig_cc.cc_vararg <> None then
       FixupEABI.fixup_result dir sg
 end
 
diff --git a/backend/Asmexpandaux.ml b/backend/Asmexpandaux.ml
index 0530abe4..f7feb303 100644
--- a/backend/Asmexpandaux.ml
+++ b/backend/Asmexpandaux.ml
@@ -54,7 +54,7 @@ let get_current_function_args () =
   (!current_function).fn_sig.sig_args
 
 let is_current_function_variadic () =
-  (!current_function).fn_sig.sig_cc.cc_vararg
+  (!current_function).fn_sig.sig_cc.cc_vararg <> None
 
 let get_current_function_sig () =
   (!current_function).fn_sig
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index ef028255..186c3155 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.ml
@@ -552,10 +552,16 @@ 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 unproto attr =
+let convertCallconv _tres targs va attr =
+  let vararg =
+    match targs with
+    | None -> None
+    | Some tl -> if va then Some (Z.of_uint (List.length tl)) else None in
   let sr =
     Cutil.find_custom_attributes ["structreturn"; "__structreturn"] attr in
-  {  AST.cc_vararg = va; cc_unproto = unproto; cc_structret = sr <> [] }
+  {  AST.cc_vararg = vararg;
+     AST.cc_unproto = (targs = None);
+     AST.cc_structret = (sr <> []) }
 
 (** Types *)
 
@@ -623,7 +629,7 @@ let rec convertTyp env t =
                 | Some tl -> convertParams env tl
                 end,
                 convertTyp env tres,
-                convertCallconv va (targs = None) a)
+                convertCallconv tres targs va a)
   | C.TNamed _ ->
       convertTyp env (Cutil.unroll env t)
   | C.TStruct(id, a) ->
@@ -989,7 +995,7 @@ let rec convertExpr env e =
       and tres = convertTyp env e.etyp in
       let sg =
         signature_of_type targs tres
-           { AST.cc_vararg = true; cc_unproto = false; cc_structret = false} in
+           { AST.cc_vararg = Some (coqint_of_camlint 1l); cc_unproto = false; cc_structret = false} in
       Ebuiltin( AST.EF_external(coqstring_of_camlstring "printf", sg),
                targs, convertExprList env args, tres)
 
@@ -1256,7 +1262,8 @@ let convertFundef loc env fd =
       a_loc = loc };
   (id',  AST.Gfun(Ctypes.Internal
           {fn_return = ret;
-           fn_callconv = convertCallconv fd.fd_vararg false fd.fd_attrib;
+           fn_callconv = convertCallconv fd.fd_ret (Some fd.fd_params)
+                                         fd.fd_vararg fd.fd_attrib;
            fn_params = params;
            fn_vars = vars;
            fn_body = body'}))
diff --git a/cfrontend/Ctypes.v b/cfrontend/Ctypes.v
index 664a60c5..7ce50525 100644
--- a/cfrontend/Ctypes.v
+++ b/cfrontend/Ctypes.v
@@ -94,6 +94,7 @@ Proof.
   decide equality.
   decide equality.
   decide equality.
+  decide equality.
 Defined.
 
 Opaque type_eq typelist_eq.
diff --git a/cfrontend/Ctyping.v b/cfrontend/Ctyping.v
index 00fcf8ab..d9637b6a 100644
--- a/cfrontend/Ctyping.v
+++ b/cfrontend/Ctyping.v
@@ -170,7 +170,7 @@ Definition floatsize_eq: forall (x y: floatsize), {x=y} + {x<>y}.
 Proof. decide equality. Defined.
 
 Definition callconv_combine (cc1 cc2: calling_convention) : res calling_convention :=
-  if bool_eq cc1.(cc_vararg) cc2.(cc_vararg) then
+  if option_eq Z.eq_dec 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) |}
diff --git a/cfrontend/PrintCsyntax.ml b/cfrontend/PrintCsyntax.ml
index 97a00b09..c49f6cd4 100644
--- a/cfrontend/PrintCsyntax.ml
+++ b/cfrontend/PrintCsyntax.ml
@@ -111,8 +111,8 @@ let rec name_cdecl id ty =
       | Tnil ->
           if first then
             Buffer.add_string b
-               (if cconv.cc_vararg then "..." else "void")
-          else if cconv.cc_vararg then
+               (if cconv.cc_vararg <> None then "..." else "void")
+          else if cconv.cc_vararg <> None then
             Buffer.add_string b ", ..."
           else
             ()
@@ -400,11 +400,11 @@ let name_function_parameters name_param fun_name params cconv =
   Buffer.add_char b '(';
   begin match params with
   | [] ->
-      Buffer.add_string b (if cconv.cc_vararg then "..." else "void")
+      Buffer.add_string b (if cconv.cc_vararg <> None then "..." else "void")
   | _ ->
       let rec add_params first = function
       | [] ->
-          if cconv.cc_vararg then Buffer.add_string b ",..."
+          if cconv.cc_vararg <> None then Buffer.add_string b ",..."
       | (id, ty) :: rem ->
           if not first then Buffer.add_string b ", ";
           Buffer.add_string b (name_cdecl (name_param id) ty);
diff --git a/common/AST.v b/common/AST.v
index ddd10ede..4f954c5c 100644
--- a/common/AST.v
+++ b/common/AST.v
@@ -122,17 +122,17 @@ These signatures are used in particular to determine appropriate
 calling conventions for the function. *)
 
 Record calling_convention : Type := mkcallconv {
-  cc_vararg: bool;                      (**r variable-arity function *)
-  cc_unproto: bool;                     (**r old-style unprototyped function *)
-  cc_structret: bool                    (**r function returning a struct  *)
+  cc_vararg: option Z;  (**r variable-arity function (+ number of fixed args) *)
+  cc_unproto: bool;     (**r old-style unprototyped function *)
+  cc_structret: bool    (**r function returning a struct  *)
 }.
 
 Definition cc_default :=
-  {| cc_vararg := false; cc_unproto := false; cc_structret := false |}.
+  {| cc_vararg := None; cc_unproto := false; cc_structret := false |}.
 
 Definition calling_convention_eq (x y: calling_convention) : {x=y} + {x<>y}.
 Proof.
-  decide equality; apply bool_dec.
+  decide equality; try (apply bool_dec). decide equality; apply Z.eq_dec.
 Defined.
 Global Opaque calling_convention_eq.
 
diff --git a/exportclight/ExportClight.ml b/exportclight/ExportClight.ml
index 4ff901eb..7604175e 100644
--- a/exportclight/ExportClight.ml
+++ b/exportclight/ExportClight.ml
@@ -216,8 +216,8 @@ and typlist p = function
 and callconv p cc =
   if cc = cc_default
   then fprintf p "cc_default"
-  else fprintf p "{|cc_vararg:=%b; cc_unproto:=%b; cc_structret:=%b|}"
-                  cc.cc_vararg cc.cc_unproto cc.cc_structret
+  else fprintf p "{|cc_vararg:=%a; cc_unproto:=%b; cc_structret:=%b|}"
+                  (print_option coqZ) cc.cc_vararg cc.cc_unproto cc.cc_structret
 
 (* External functions *)
 
diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml
index cb6a659f..fcd7c426 100644
--- a/powerpc/Asmexpand.ml
+++ b/powerpc/Asmexpand.ml
@@ -830,7 +830,7 @@ let expand_builtin_inline name args res =
    function is unprototyped. *)
 
 let set_cr6 sg =
-  if sg.sig_cc.cc_vararg || sg.sig_cc.cc_unproto then begin
+  if (sg.sig_cc.cc_vararg <> None) || sg.sig_cc.cc_unproto then begin
     if List.exists (function Tfloat | Tsingle -> true | _ -> false) sg.sig_args
     then emit (Pcreqv(CRbit_6, CRbit_6, CRbit_6))
     else emit (Pcrxor(CRbit_6, CRbit_6, CRbit_6))
diff --git a/riscV/Asmexpand.ml b/riscV/Asmexpand.ml
index 810514a3..80e33b2b 100644
--- a/riscV/Asmexpand.ml
+++ b/riscV/Asmexpand.ml
@@ -100,7 +100,7 @@ let rec fixup_variadic_call ri rf tyl =
         end
         
 let fixup_call sg =
-  if sg.sig_cc.cc_vararg then fixup_variadic_call 0 0 sg.sig_args
+  if (sg.sig_cc.cc_vararg <> None) then fixup_variadic_call 0 0 sg.sig_args
 
 (* Handling of annotations *)
 
@@ -588,7 +588,7 @@ let expand_instruction instr =
   | Pallocframe (sz, ofs) ->
       let sg = get_current_function_sig() in
       emit (Pmv (X30, X2));
-      if sg.sig_cc.cc_vararg then begin
+      if (sg.sig_cc.cc_vararg <> None) then begin
         let n = arguments_size sg in
         let extra_sz = if n >= 8 then 0 else align ((8 - n) * wordsize) 16 in
         let full_sz = Z.add sz (Z.of_uint extra_sz) in
@@ -606,7 +606,7 @@ let expand_instruction instr =
   | Pfreeframe (sz, ofs) ->
      let sg = get_current_function_sig() in
      let extra_sz =
-      if sg.sig_cc.cc_vararg then begin
+      if (sg.sig_cc.cc_vararg <> None) then begin
         let n = arguments_size sg in
         if n >= 8 then 0 else align ((8 - n) * wordsize) 16
       end else 0 in
diff --git a/riscV/Conventions1.v b/riscV/Conventions1.v
index 17326139..74c99d07 100644
--- a/riscV/Conventions1.v
+++ b/riscV/Conventions1.v
@@ -281,7 +281,8 @@ Fixpoint loc_arguments_rec (va: bool)
   when calling a function with signature [s].  *)
 
 Definition loc_arguments (s: signature) : list (rpair loc) :=
-  loc_arguments_rec s.(sig_cc).(cc_vararg) s.(sig_args) 0 0 0.
+  let va := match s.(sig_cc).(cc_vararg) with Some _ => true | None => false end in
+  loc_arguments_rec va s.(sig_args) 0 0 0.
 
 (** Argument locations are either non-temporary registers or [Outgoing]
   stack slots at nonnegative offsets. *)
diff --git a/x86/Asmexpand.ml b/x86/Asmexpand.ml
index 73efc3c5..14cbb373 100644
--- a/x86/Asmexpand.ml
+++ b/x86/Asmexpand.ml
@@ -500,7 +500,7 @@ let expand_builtin_inline name args res =
    unprototyped. *)
 
 let fixup_funcall_elf64 sg =
-  if sg.sig_cc.cc_vararg || sg.sig_cc.cc_unproto then begin
+  if sg.sig_cc.cc_vararg <> None || sg.sig_cc.cc_unproto then begin
     let (ir, fr, ofs) = next_arg_locations 0 0 0 sg.sig_args in
     emit (Pmovl_ri (RAX, coqint_of_camlint (Int32.of_int fr)))
   end
@@ -521,7 +521,7 @@ let rec copy_fregs_to_iregs args fr ir =
       ()
 
 let fixup_funcall_win64 sg =
-  if sg.sig_cc.cc_vararg then
+  if sg.sig_cc.cc_vararg <> None then
     copy_fregs_to_iregs sg.sig_args [XMM0; XMM1; XMM2; XMM3] [RCX; RDX; R8; R9]
 
 let fixup_funcall sg =