Update the RISC-V calling conventions (#221)

We were implementing the ABI described in the RISC-V Instruction Set
Manual, version 2.1.  However, this ABI was superseded by the RISC-V
ELF psABI specification.

This commit changes the calling conventions to better match the ELF psABI
specification.  This should greatly improve interoperability with code
compiled by other RISC-V compilers.

One incompatibility remains: when all 8 FP argument registers have been used, further FP arguments should be passed in integer argument registers if available, while this PR passes them on stack.

2 files changed, 149 insertions, 137 deletions

diff --git a/riscV/Asmexpand.ml b/riscV/Asmexpand.ml
index d36b6230..7e36abf8 100644
--- a/riscV/Asmexpand.ml
+++ b/riscV/Asmexpand.ml
@@ -63,44 +63,44 @@ let expand_storeind_ptr src base ofs =
 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 pos tyl =
-  if pos < 8 then
+let rec fixup_variadic_call ri rf tyl =
+  if ri < 8 then
     match tyl with
     | [] ->
         ()
     | (Tint | Tany32) :: tyl ->
-        fixup_variadic_call (pos + 1) tyl
+        fixup_variadic_call (ri + 1) rf tyl
     | Tsingle :: tyl ->
-        let rs =float_param_regs.(pos)
-        and rd = int_param_regs.(pos) in
+        let rs = float_param_regs.(rf)
+        and rd = int_param_regs.(ri) in
         emit (Pfmvxs(rd, rs));
-        fixup_variadic_call (pos + 1) tyl
+        fixup_variadic_call (ri + 1) (rf + 1) tyl
     | Tlong :: tyl ->
-        let pos' = if Archi.ptr64 then pos + 1 else align pos 2 + 2 in
-        fixup_variadic_call pos' tyl
+        let ri' = if Archi.ptr64 then ri + 1 else align ri 2 + 2 in
+        fixup_variadic_call ri' rf tyl
     | (Tfloat | Tany64) :: tyl ->
         if Archi.ptr64 then begin
-          let rs = float_param_regs.(pos)
-          and rd = int_param_regs.(pos) in
+          let rs = float_param_regs.(rf)
+          and rd = int_param_regs.(ri) in
           emit (Pfmvxd(rd, rs));
-          fixup_variadic_call (pos + 1) tyl
+          fixup_variadic_call (ri + 1) (rf + 1) tyl
         end else begin
-          let pos = align pos 2 in
-          if pos < 8 then begin
-            let rs = float_param_regs.(pos)
-            and rd1 = int_param_regs.(pos)
-            and rd2 = int_param_regs.(pos + 1) in
+          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 (pos + 2) tyl
+            fixup_variadic_call (ri + 2) (rf + 1) tyl
           end
         end
         
 let fixup_call sg =
-  if sg.sig_cc.cc_vararg then fixup_variadic_call 0 sg.sig_args
+  if sg.sig_cc.cc_vararg then fixup_variadic_call 0 0 sg.sig_args
 
 (* Handling of annotations *)
 
diff --git a/riscV/Conventions1.v b/riscV/Conventions1.v
index a705c954..7f8048f6 100644
--- a/riscV/Conventions1.v
+++ b/riscV/Conventions1.v
@@ -105,7 +105,9 @@ Definition is_float_reg (r: mreg) :=
   of function arguments), but this leaves much liberty in choosing actual
   locations.  To ensure binary interoperability of code generated by our
   compiler with libraries compiled by another compiler, we
-  implement the standard RISC-V conventions.  *)
+  implement the standard RISC-V conventions as found here:
+  https://github.com/riscv/riscv-elf-psabi-doc/blob/master/riscv-elf.md
+*)
 
 (** ** Location of function result *)
 
@@ -169,38 +171,32 @@ Qed.
 
 (** ** Location of function arguments *)
 
-(** The RISC-V ABI states the following convention for passing arguments
+(** The RISC-V ABI states the following conventions for passing arguments
   to a function:
 
-- Arguments are passed in registers when possible.
-
-- Up to eight integer registers (ai: int_param_regs) and up to eight
-  floating-point registers (fai: float_param_regs) are used for this
-  purpose.
-
-- If the arguments to a function are conceptualized as fields of a C
-  struct, each with pointer alignment, the argument registers are a
-  shadow of the first eight pointer-words of that struct. If argument
-  i < 8 is a floating-point type, it is passed in floating-point
-  register fa_i; otherwise, it is passed in integer register a_i.
-
-- When primitive arguments twice the size of a pointer-word are passed
-  on the stack, they are naturally aligned. When they are passed in the
-  integer registers, they reside in an aligned even-odd register pair,
-  with the even register holding the least-significant bits.
-
-- Floating-point arguments to variadic functions (except those that
-  are explicitly named in the parameter list) are passed in integer
-  registers.
-
-- The portion of the conceptual struct that is not passed in argument
-  registers is passed on the stack. The stack pointer sp points to the
-  first argument not passed in a register.
-
-The bit about variadic functions doesn't quite fit CompCert's model.
-We do our best by passing the FP arguments in registers, as usual,
-and reserving the corresponding integer registers, so that fixup
-code can be introduced in the Asmexpand pass.
+- 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.
+
+- 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.
+
+- 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.
+
+- RV32, variadic: same, but arguments of 64-bit types (integers as well
+  as floats) are passed in two consecutive aligned integer registers
+  (a(2i), a(2i+1)).  
+
+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
+arguments in registers, as usual, and reserving the corresponding
+integer registers, so that fixup code can be introduced in the
+Asmexpand pass.
 *)
 
 Definition int_param_regs :=
@@ -208,62 +204,84 @@ Definition int_param_regs :=
 Definition float_param_regs :=
   F10 :: F11 :: F12 :: F13 :: F14 :: F15 :: F16 :: F17 :: nil.
 
-Definition one_arg (regs: list mreg) (rn: Z) (ofs: Z) (ty: typ)
-                           (rec: Z -> Z -> list (rpair loc)) :=
-  match list_nth_z regs rn with
+Definition int_arg (ri rf ofs: Z) (ty: typ)
+                   (rec: Z -> Z -> Z -> list (rpair loc)) :=
+  match list_nth_z int_param_regs ri with
   | Some r =>
-      One(R r) :: rec (rn + 1) ofs
+      One(R r) :: rec (ri + 1) rf ofs
   | None   =>
       let ofs := align ofs (typealign ty) in
-      One(S Outgoing ofs ty) :: rec rn (ofs + (if Archi.ptr64 then 2 else typesize ty))
+      One(S Outgoing ofs ty)
+      :: rec ri rf (ofs + (if Archi.ptr64 then 2 else typesize ty))
   end.
 
-Definition two_args (regs: list mreg) (rn: Z) (ofs: Z)
-                    (rec: Z -> Z -> list (rpair loc)) :=
-  let rn := align rn 2 in
-  match list_nth_z regs rn, list_nth_z regs (rn + 1) with
-  | Some r1, Some r2 =>
-      Twolong (R r2) (R r1) :: rec (rn + 2) ofs
-  | _, _ =>
-      let ofs := align ofs 2 in
-      Twolong (S Outgoing (ofs + 1) Tint) (S Outgoing ofs Tint) ::
-      rec rn (ofs + 2)
+Definition float_arg (va: bool) (ri rf ofs: Z) (ty: typ)
+                     (rec: Z -> Z -> Z -> list (rpair loc)) :=
+  match list_nth_z float_param_regs rf with
+  | Some r =>
+      if va then
+       (let ri' :=  (* reserve 1 or 2 aligned integer registers *)
+          if Archi.ptr64 || zeq (typesize ty) 1 then ri + 1 else align ri 2 + 2 in
+        if zle ri' 8 then
+            (* we have enough integer registers, put argument in FP reg
+               and fixup code will put it in one or two integer regs *)
+            One (R r) :: rec ri' (rf + 1) ofs
+        else
+            (* we are out of integer registers, pass argument on stack *)
+            let ofs := align ofs (typealign ty) in
+            One(S Outgoing ofs ty)
+            :: rec ri' rf (ofs + (if Archi.ptr64 then 2 else typesize ty)))
+      else
+        One (R r) :: rec ri (rf + 1) ofs
+  | None   =>
+      let ofs := align ofs (typealign ty) in
+      One(S Outgoing ofs ty)
+      :: rec ri rf (ofs + (if Archi.ptr64 then 2 else typesize ty))
   end.
 
-Definition hybrid_arg (regs: list mreg) (rn: Z) (ofs: Z) (ty: typ)
-                      (rec: Z -> Z -> list (rpair loc)) :=
-  let rn := align rn 2 in
-  match list_nth_z regs rn with
-  | Some r =>
-      One (R r) :: rec (rn + 2) ofs
-  | None =>
+Definition split_long_arg (va: bool) (ri rf ofs: Z)
+                          (rec: Z -> Z -> Z -> list (rpair loc)) :=
+  let ri := if va then align ri 2 else ri in
+  match list_nth_z int_param_regs ri, list_nth_z int_param_regs (ri + 1) with
+  | Some r1, Some r2 =>
+      Twolong (R r2) (R r1) :: rec (ri + 2) rf ofs
+  | Some r1, None =>
+      Twolong (S Outgoing ofs Tint) (R r1) :: rec (ri + 1) rf (ofs + 1)
+  | None, _ =>
       let ofs := align ofs 2 in
-      One (S Outgoing ofs ty) :: rec rn (ofs + 2)
+      Twolong (S Outgoing (ofs + 1) Tint) (S Outgoing ofs Tint) ::
+      rec ri rf (ofs + 2)
   end.
 
 Fixpoint loc_arguments_rec (va: bool)
-    (tyl: list typ) (r ofs: Z) {struct tyl} : list (rpair loc) :=
+    (tyl: list typ) (ri rf ofs: Z) {struct tyl} : list (rpair loc) :=
   match tyl with
   | nil => nil
   | (Tint | Tany32) as ty :: tys =>
-      one_arg int_param_regs r ofs ty (loc_arguments_rec va tys)
+      (* pass in one integer register or on stack *)
+      int_arg ri rf ofs ty (loc_arguments_rec va tys)
   | Tsingle as ty :: tys =>
-      one_arg float_param_regs r ofs ty (loc_arguments_rec va 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)
   | Tlong as ty :: tys =>
-      if Archi.ptr64
-      then one_arg int_param_regs r ofs ty (loc_arguments_rec va tys)
-      else two_args int_param_regs r ofs  (loc_arguments_rec va tys)
+      if Archi.ptr64 then
+        (* pass in one integer register or on stack *)
+        int_arg ri rf ofs ty (loc_arguments_rec va tys)
+      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)
   | (Tfloat | Tany64) as ty :: tys =>
-      if va && negb Archi.ptr64
-      then hybrid_arg float_param_regs r ofs ty (loc_arguments_rec va tys)
-      else one_arg float_param_regs r ofs ty (loc_arguments_rec va 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)
   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) :=
-  loc_arguments_rec s.(sig_cc).(cc_vararg) s.(sig_args) 0 0.
+  loc_arguments_rec s.(sig_cc).(cc_vararg) s.(sig_args) 0 0 0.
 
 (** Argument locations are either non-temporary registers or [Outgoing]
   stack slots at nonnegative offsets. *)
@@ -276,15 +294,18 @@ Definition loc_argument_acceptable (l: loc) : Prop :=
   end.
 
 Lemma loc_arguments_rec_charact:
-  forall va tyl rn ofs p,
+  forall va tyl ri rf ofs p,
   ofs >= 0 ->
-  In p (loc_arguments_rec va tyl rn ofs) -> forall_rpair loc_argument_acceptable p.
+  In p (loc_arguments_rec va tyl ri rf ofs) -> forall_rpair loc_argument_acceptable p.
 Proof.
   set (OK := fun (l: list (rpair loc)) =>
              forall p, In p l -> forall_rpair loc_argument_acceptable p).
-  set (OKF := fun (f: Z -> Z -> list (rpair loc)) =>
-              forall rn ofs, ofs >= 0 -> OK (f rn ofs)).
-  set (OKREGS := fun (l: list mreg) => forall r, In r l -> is_callee_save r = false).
+  set (OKF := fun (f: Z -> Z -> Z -> list (rpair loc)) =>
+              forall ri rf ofs, ofs >= 0 -> OK (f ri rf ofs)).
+  assert (CSI: forall r, In r int_param_regs -> is_callee_save r = false).
+  { decide_goal. }
+  assert (CSF: forall r, In r float_param_regs -> is_callee_save r = false).
+  { decide_goal. }
   assert (AL: forall ofs ty, ofs >= 0 -> align ofs (typealign ty) >= 0).
   { intros. 
     assert (ofs <= align ofs (typealign ty)) by (apply align_le; apply typealign_pos).
@@ -293,73 +314,64 @@ Proof.
   { destruct Archi.ptr64; omega. }
   assert (SKK: forall ty, (if Archi.ptr64 then 2 else typesize ty) > 0).
   { intros. destruct Archi.ptr64. omega. apply typesize_pos.  }
-  assert (A: forall regs rn ofs ty f,
-             OKREGS regs -> OKF f -> ofs >= 0 -> OK (one_arg regs rn ofs ty f)).
-  { intros until f; intros OR OF OO; red; unfold one_arg; intros.
-    destruct (list_nth_z regs rn) as [r|] eqn:NTH; destruct H.
-  - subst p; simpl. apply OR. eapply list_nth_z_in; eauto. 
+  assert (A: forall ri rf ofs ty f,
+             OKF f -> ofs >= 0 -> OK (int_arg ri rf ofs ty f)).
+  { intros until f; intros OF OO; red; unfold int_arg; intros.
+    destruct (list_nth_z int_param_regs ri) as [r|] eqn:NTH; destruct H.
+  - subst p; simpl. apply CSI. eapply list_nth_z_in; eauto. 
   - eapply OF; eauto. 
   - subst p; simpl. auto using align_divides, typealign_pos.
   - eapply OF; [idtac|eauto].
     generalize (AL ofs ty OO) (SKK ty); omega.
   }
-  assert (B: forall regs rn ofs f,
-             OKREGS regs -> OKF f -> ofs >= 0 -> OK (two_args regs rn ofs f)).
-  { intros until f; intros OR OF OO; unfold two_args.
-    set (rn' := align rn 2).
+  assert (B: forall va ri rf ofs ty f,
+             OKF f -> ofs >= 0 -> OK (float_arg va ri rf ofs ty f)).
+  { intros until f; intros OF OO; red; unfold float_arg; intros.
+    destruct (list_nth_z float_param_regs rf) as [r|] eqn:NTH.
+  - set (ri' := if Archi.ptr64 || zeq (typesize ty) 1 then ri + 1 else align ri 2 + 2) in *.
+    destruct va; [destruct (zle ri' 8)|idtac]; destruct H.
+    + subst p; simpl. apply CSF. eapply list_nth_z_in; eauto.
+    + eapply OF; eauto.
+    + subst p; repeat split; auto using align_divides, typealign_pos.
+    + eapply OF; [idtac|eauto]. generalize (AL ofs ty OO) (SKK ty); omega.
+    + subst p; simpl. apply CSF. eapply list_nth_z_in; eauto.
+    + eapply OF; eauto.
+  - destruct H.
+    + subst p; repeat split; auto using align_divides, typealign_pos.
+    + eapply OF; [idtac|eauto]. generalize (AL ofs ty OO) (SKK ty); omega.
+  }
+  assert (C: forall va ri rf ofs f,
+             OKF f -> ofs >= 0 -> OK (split_long_arg va ri rf ofs f)).
+  { intros until f; intros OF OO; unfold split_long_arg.
+    set (ri' := if va then align ri 2 else ri).
     set (ofs' := align ofs 2).
     assert (OO': ofs' >= 0) by (apply (AL ofs Tlong); auto).
-    assert (DFL: OK (Twolong (S Outgoing (ofs' + 1) Tint) (S Outgoing ofs' Tint)
-                     :: f rn' (ofs' + 2))).
-    { red; simpl; intros. destruct H.
-    - subst p; simpl. 
-      repeat split; auto using Z.divide_1_l. omega.
-    - eapply OF; [idtac|eauto]. omega.
-    }
-    destruct (list_nth_z regs rn') as [r1|] eqn:NTH1;
-    destruct (list_nth_z regs (rn' + 1)) as [r2|] eqn:NTH2;
-    try apply DFL.
-    red; simpl; intros; destruct H.
-  - subst p; simpl. split; apply OR; eauto using list_nth_z_in.  
-  - eapply OF; [idtac|eauto]. auto.
-  }
-  assert (C: forall regs rn ofs ty f,
-             OKREGS regs -> OKF f -> ofs >= 0 -> typealign ty = 1 -> OK (hybrid_arg regs rn ofs ty f)).
-  { intros until f; intros OR OF OO OTY; unfold hybrid_arg; red; intros.
-    set (rn' := align rn 2) in *.
-    destruct (list_nth_z regs rn') as [r|] eqn:NTH; destruct H.
-  - subst p; simpl. apply OR. eapply list_nth_z_in; eauto. 
-  - eapply OF; eauto. 
-  - subst p; simpl. rewrite OTY. split. apply (AL ofs Tlong OO). apply Z.divide_1_l. 
-  - eapply OF; [idtac|eauto]. generalize (AL ofs Tlong OO); simpl; omega.
+    destruct (list_nth_z int_param_regs ri') as [r1|] eqn:NTH1;
+    [destruct (list_nth_z int_param_regs (ri'+1)) as [r2|] eqn:NTH2 | idtac].
+  - red; simpl; intros; destruct H.
+    + subst p; split; apply CSI; eauto using list_nth_z_in.
+    + eapply OF; [idtac|eauto]. omega.
+  - red; simpl; intros; destruct H.
+    + subst p; split. split; auto using Z.divide_1_l. apply CSI; eauto using list_nth_z_in.
+    + eapply OF; [idtac|eauto]. omega.
+  - red; simpl; intros; destruct H.
+    + subst p; repeat split; auto using Z.divide_1_l. omega. 
+    + eapply OF; [idtac|eauto]. omega.
   }
-  assert (D: OKREGS int_param_regs).
-  { red. decide_goal. }
-  assert (E: OKREGS float_param_regs).
-  { red. decide_goal. }
-
-  cut (forall va tyl rn ofs, ofs >= 0 -> OK (loc_arguments_rec va tyl rn ofs)).
+  cut (forall va tyl ri rf ofs, ofs >= 0 -> OK (loc_arguments_rec va tyl 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 *) 
-  destruct (va && negb Archi.ptr64).
-  apply C; auto.
-  apply A; auto.
++ (* float *) apply B; auto.
 + (* long *)
   destruct Archi.ptr64.
   apply A; auto.
-  apply B; auto.
-+ (* single *)
-  apply A; auto.
-+ (* any32 *)
-  apply A; auto.
-+ (* any64 *)
-  destruct (va && negb Archi.ptr64).
   apply C; auto.
-  apply A; auto.
++ (* single *) apply B; auto.
++ (* any32 *) apply A; auto.
++ (* any64 *) apply B; auto.
 Qed.
 
 Lemma loc_arguments_acceptable: