From 2076a3bb31daf5bc3663fce25de6d837ace3f952 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Tue, 22 Dec 2020 15:06:19 +0100 Subject: 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. --- riscV/Asmexpand.ml | 96 ++++++++++++++++++++++++++++++++++------------------ riscV/Conventions1.v | 72 ++++++++++++++++++++++----------------- 2 files changed, 105 insertions(+), 63 deletions(-) (limited to 'riscV') 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: -- cgit