RISC-V: revised calling conventions for variadic functions

Fixed (non-variadic) arguments follow the standard calling conventions.
It's only the variadic arguments that need special treatment.

2 files changed, 105 insertions, 63 deletions

diff --git a/riscV/Asmexpand.ml b/riscV/Asmexpand.ml
index 80e33b2b..f01ecb23 100644
--- a/riscV/Asmexpand.ml
+++ b/riscV/Asmexpand.ml
@@ -57,50 +57,59 @@ let expand_storeind_ptr src base ofs =
      registers.
 *)
 
-(* Fix-up code around calls to variadic functions.  Floating-point arguments
-   residing in FP registers need to be moved to integer registers. *)
+(* Fix-up code around calls to variadic functions.
+   Floating-point variadic arguments residing in FP registers need to
+   be moved to integer registers. *)
 
 let int_param_regs   = [| X10; X11; X12; X13; X14; X15; X16; X17 |]
 let float_param_regs = [| F10; F11; F12; F13; F14; F15; F16; F17 |]
 
-let rec fixup_variadic_call ri rf tyl =
+let rec fixup_variadic_call fixed ri rf tyl =
   if ri < 8 then
     match tyl with
     | [] ->
         ()
     | (Tint | Tany32) :: tyl ->
-        fixup_variadic_call (ri + 1) rf tyl
+        fixup_variadic_call (fixed - 1) (ri + 1) rf tyl
     | Tsingle :: tyl ->
-        let rs = float_param_regs.(rf)
-        and rd = int_param_regs.(ri) in
-        emit (Pfmvxs(rd, rs));
-        fixup_variadic_call (ri + 1) (rf + 1) tyl
+        if fixed <= 0 then begin
+          let rs = float_param_regs.(rf)
+          and rd = int_param_regs.(ri) in
+          emit (Pfmvxs(rd, rs))
+        end;
+        fixup_variadic_call (fixed - 1) (ri + 1) (rf + 1) tyl
     | Tlong :: tyl ->
         let ri' = if Archi.ptr64 then ri + 1 else align ri 2 + 2 in
-        fixup_variadic_call ri' rf tyl
+        fixup_variadic_call (fixed - 1) ri' rf tyl
     | (Tfloat | Tany64) :: tyl ->
         if Archi.ptr64 then begin
-          let rs = float_param_regs.(rf)
-          and rd = int_param_regs.(ri) in
-          emit (Pfmvxd(rd, rs));
-          fixup_variadic_call (ri + 1) (rf + 1) tyl
+          if fixed <= 0 then begin
+            let rs = float_param_regs.(rf)
+            and rd = int_param_regs.(ri) in
+            emit (Pfmvxd(rd, rs))
+          end;
+          fixup_variadic_call (fixed - 1) (ri + 1) (rf + 1) tyl
         end else begin
           let ri = align ri 2 in
           if ri < 8 then begin
-            let rs = float_param_regs.(rf)
-            and rd1 = int_param_regs.(ri)
-            and rd2 = int_param_regs.(ri + 1) in
-            emit (Paddiw(X2, X X2, Integers.Int.neg _16));
-            emit (Pfsd(rs, X2, Ofsimm _0));
-            emit (Plw(rd1, X2, Ofsimm _0));
-            emit (Plw(rd2, X2, Ofsimm _4));
-            emit (Paddiw(X2, X X2, _16));
-            fixup_variadic_call (ri + 2) (rf + 1) tyl
+            if fixed <= 0 then begin
+              let rs = float_param_regs.(rf)
+              and rd1 = int_param_regs.(ri)
+              and rd2 = int_param_regs.(ri + 1) in
+              emit (Paddiw(X2, X X2, Integers.Int.neg _16));
+              emit (Pfsd(rs, X2, Ofsimm _0));
+              emit (Plw(rd1, X2, Ofsimm _0));
+              emit (Plw(rd2, X2, Ofsimm _4));
+              emit (Paddiw(X2, X X2, _16))
+            end;
+            fixup_variadic_call (fixed - 1) (ri + 2) (rf + 1) tyl
           end
         end
         
 let fixup_call sg =
-  if (sg.sig_cc.cc_vararg <> None) then fixup_variadic_call 0 0 sg.sig_args
+  match sg.sig_cc.cc_vararg with
+  | None -> ()
+  | Some fixed -> fixup_variadic_call (Z.to_int fixed) 0 0 sg.sig_args
 
 (* Handling of annotations *)
 
@@ -305,18 +314,41 @@ let expand_builtin_vstore chunk args =
 
 (* Handling of varargs *)
 
-(* Size in words of the arguments to a function.  This includes both
-   arguments passed in registers and arguments passed on stack. *)
+(* Number of integer registers, FP registers, and stack words
+   used to pass the (fixed) arguments to a function. *)
+
+let rec args_size ri rf ofs = function
+  | [] -> (ri, rf, ofs)
+  | (Tint | Tany32) :: l ->
+      if ri < 8
+      then args_size (ri + 1) rf ofs l
+      else args_size ri rf (ofs + 1) l
+  | Tsingle :: l ->
+      if rf < 8
+      then args_size ri (rf + 1) ofs l
+      else args_size ri rf (ofs + 1) l
+  | Tlong :: l ->
+      if Archi.ptr64 then
+        if ri < 8
+        then args_size (ri + 1) rf ofs l
+        else args_size ri rf (ofs + 1) l
+      else
+        if ri < 7 then args_size (ri + 2) rf ofs l
+        else if ri = 7 then args_size (ri + 1) rf (ofs + 1) l
+        else args_size ri rf (align ofs 2 + 2) l
+  | (Tfloat | Tany64) :: l ->
+      if rf < 8
+      then args_size ri (rf + 1) ofs l
+      else let ofs' = if Archi.ptr64 then ofs + 1 else align ofs 2 + 2 in 
+           args_size ri rf ofs' l
 
-let rec args_size sz = function
-  | [] -> sz
-  | (Tint | Tsingle | Tany32) :: l ->
-      args_size (sz + 1) l
-  | (Tlong | Tfloat | Tany64) :: l ->
-      args_size (if Archi.ptr64 then sz + 1 else align sz 2 + 2) l
+(* Size in words of the arguments to a function.  This includes both
+   arguments passed in integer registers and arguments passed on stack,
+   but not arguments passed in FP registers. *)
 
 let arguments_size sg =
-  args_size 0 sg.sig_args
+  let (ri, _, ofs) = args_size 0 0 0 sg.sig_args in
+  ri + ofs
 
 let save_arguments first_reg base_ofs =
   for i = first_reg to 7 do
diff --git a/riscV/Conventions1.v b/riscV/Conventions1.v
index 74c99d07..0fc8295e 100644
--- a/riscV/Conventions1.v
+++ b/riscV/Conventions1.v
@@ -172,25 +172,28 @@ Qed.
 (** ** Location of function arguments *)
 
 (** The RISC-V ABI states the following conventions for passing arguments
-  to a function:
+  to a function.  First for non-variadic functions:
 
-- RV64, not variadic: pass the first 8 integer arguments in
-  integer registers (a1...a8: int_param_regs), the first 8 FP arguments
-  in FP registers (fa1...fa8: float_param_regs), and the remaining
-  arguments on the stack, in 8-byte slots.
+- RV64: pass the first 8 integer arguments in integer registers
+  (a1...a8: int_param_regs), the first 8 FP arguments in FP registers
+  (fa1...fa8: float_param_regs), and the remaining arguments on the
+  stack, in 8-byte slots.
 
-- RV32, not variadic: same, but arguments of 64-bit integer type
-  are passed in two consecutive integer registers (a(i), a(i+1))
-  or in a(8) and on a 32-bit word on the stack.  Stack-allocated
-  arguments are aligned to their natural alignment.
+- RV32: same, but arguments of 64-bit integer type are passed in two
+  consecutive integer registers (a(i), a(i+1)) or in a(8) and on a
+  32-bit word on the stack.  Stack-allocated arguments are aligned to
+  their natural alignment.
 
-- RV64, variadic: pass the first 8 arguments in integer registers
-  (a1...a8), including FP arguments; pass the remaining arguments on
-  the stack, in 8-byte slots.
+For variadic functions, the fixed arguments are passed as described
+above, then the variadic arguments receive special treatment:
 
-- RV32, variadic: same, but arguments of 64-bit types (integers as well
+- RV64: all variadic arguments, including FP arguments,
+  are passed in the remaining integer registers (a1...a8),
+  then on the stack, in 8-byte slots.
+
+- RV32: likewise, but arguments of 64-bit types (integers as well
   as floats) are passed in two consecutive aligned integer registers
-  (a(2i), a(2i+1)).  
+  (a(2i), a(2i+1)), or on the stack, in aligned 8-byte slots.
 
 The passing of FP arguments to variadic functions in integer registers
 doesn't quite fit CompCert's model.  We do our best by passing the FP
@@ -253,36 +256,43 @@ Definition split_long_arg (va: bool) (ri rf ofs: Z)
       rec ri rf (ofs + 2)
   end.
 
-Fixpoint loc_arguments_rec (va: bool)
-    (tyl: list typ) (ri rf ofs: Z) {struct tyl} : list (rpair loc) :=
+Fixpoint loc_arguments_rec
+    (tyl: list typ) (fixed ri rf ofs: Z) {struct tyl} : list (rpair loc) :=
   match tyl with
   | nil => nil
   | (Tint | Tany32) as ty :: tys =>
       (* pass in one integer register or on stack *)
-      int_arg ri rf ofs ty (loc_arguments_rec va tys)
+      int_arg ri rf ofs ty (loc_arguments_rec tys (fixed - 1))
   | Tsingle as ty :: tys =>
       (* pass in one FP register or on stack.
          If vararg, reserve 1 integer register. *)
-      float_arg va ri rf ofs ty (loc_arguments_rec va tys)
+      float_arg (zle fixed 0) ri rf ofs ty (loc_arguments_rec tys (fixed - 1))
   | Tlong as ty :: tys =>
       if Archi.ptr64 then
         (* pass in one integer register or on stack *)
-        int_arg ri rf ofs ty (loc_arguments_rec va tys)
+        int_arg ri rf ofs ty (loc_arguments_rec tys (fixed - 1))
       else
         (* pass in register pair or on stack; align register pair if vararg *)
-        split_long_arg va ri rf ofs(loc_arguments_rec va tys)
+        split_long_arg (zle fixed 0) ri rf ofs(loc_arguments_rec tys (fixed - 1))
   | (Tfloat | Tany64) as ty :: tys =>
       (* pass in one FP register or on stack.
          If vararg, reserve 1 or 2 integer registers. *)
-      float_arg va ri rf ofs ty (loc_arguments_rec va tys)
+      float_arg (zle fixed 0) ri rf ofs ty (loc_arguments_rec tys (fixed - 1))
+  end.
+
+(** Number of fixed arguments for a function with signature [s]. *)
+
+Definition fixed_arguments (s: signature) : Z :=
+  match s.(sig_cc).(cc_vararg) with
+  | Some n => n
+  | None => list_length_z s.(sig_args)
   end.
 
 (** [loc_arguments s] returns the list of locations where to store arguments
   when calling a function with signature [s].  *)
 
 Definition loc_arguments (s: signature) : list (rpair loc) :=
-  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.
+  loc_arguments_rec s.(sig_args) (fixed_arguments s) 0 0 0.
 
 (** Argument locations are either non-temporary registers or [Outgoing]
   stack slots at nonnegative offsets. *)
@@ -362,20 +372,20 @@ Proof.
     + subst p; repeat split; auto using Z.divide_1_l. omega. 
     + eapply OF; [idtac|eauto]. omega.
   }
-  cut (forall va tyl ri rf ofs, ofs >= 0 -> OK (loc_arguments_rec va tyl ri rf ofs)).
+  cut (forall tyl fixed ri rf ofs, ofs >= 0 -> OK (loc_arguments_rec tyl fixed ri rf ofs)).
   unfold OK. eauto.
   induction tyl as [ | ty1 tyl]; intros until ofs; intros OO; simpl.
 - red; simpl; tauto.
 - destruct ty1.
-+ (* int *) apply A; auto.
-+ (* float *) apply B; auto.
++ (* int *) apply A; unfold OKF; auto.
++ (* float *) apply B; unfold OKF; auto.
 + (* long *)
   destruct Archi.ptr64.
-  apply A; auto.
-  apply C; auto.
-+ (* single *) apply B; auto.
-+ (* any32 *) apply A; auto.
-+ (* any64 *) apply B; auto.
+  apply A; unfold OKF; auto.
+  apply C; unfold OKF; auto.
++ (* single *) apply B; unfold OKF; auto.
++ (* any32 *) apply A; unfold OKF; auto.
++ (* any64 *) apply B; unfold OKF; auto.
 Qed.
 
 Lemma loc_arguments_acceptable: