From 5003b8d93c2a20821b776f7f74f5096a308a03cf Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Wed, 26 Feb 2020 16:49:50 +0100 Subject: 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. --- riscV/Asmexpand.ml | 36 ++++---- riscV/Conventions1.v | 250 +++++++++++++++++++++++++++------------------------ 2 files changed, 149 insertions(+), 137 deletions(-) (limited to 'riscV') 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: -- cgit