Commit 2076a3bb authored by Xavier Leroy's avatar Xavier Leroy
Browse files

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.
parent 9ab3738a
......@@ -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
......
......@@ -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:
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment