RISC-V: fix FP calling conventions

This is a follow-up to e81d015e3.

In the RISC-V ABI, FP arguments to functions are passed in integer registers
(or pairs of integer registers) in two cases:
1- the FP argument is a variadic argument
2- the FP argument is a fixed argument but all 8 FP registers reserved for
   parameter passing have been used already.

The previous implementation handled only case 1, with some problems.

This commit implements both 1 and 2.  To this end, 8 extra FP
caller-save registers are used to hold the values of the FP arguments
that must be passed in integer registers.  Fixup code moves these FP
registers to integer registers / register pairs.  Symmetrically, at
function entry, the integer registers / register pairs are moved back
to the FP registers.

8 extra FP registers is enough because there are only 8 integer
registers used for parameter passing, so at most 8 FP arguments may
need to be moved to integer registers.

1 files changed, 4 insertions, 0 deletions

diff --git a/riscV/Asm.v b/riscV/Asm.v
index 30b128ec..7e1b1fc8 100644
--- a/riscV/Asm.v
+++ b/riscV/Asm.v
@@ -256,7 +256,9 @@ Inductive instruction : Type :=
   (* floating point register move *)
   | Pfmv     (rd: freg) (rs: freg)                  (**r move *)
   | Pfmvxs   (rd: ireg) (rs: freg)                  (**r move FP single to integer register *)
+  | Pfmvsx   (rd: freg) (rs: ireg)                  (**r move integer register to FP single *)
   | Pfmvxd   (rd: ireg) (rs: freg)                  (**r move FP double to integer register *)
+  | Pfmvdx   (rd: freg) (rs: ireg)                  (**r move integer register to FP double *)
 
   (* 32-bit (single-precision) floating point *)
   | Pfls     (rd: freg) (ra: ireg) (ofs: offset)    (**r load float *)
@@ -969,7 +971,9 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
   | Pfence
 
   | Pfmvxs _ _
+  | Pfmvsx _ _
   | Pfmvxd _ _
+  | Pfmvdx _ _
 
   | Pfmins _ _ _
   | Pfmaxs _ _ _