From 9ab3738ae87a554fb742420b8c81ced4cd3c66c7 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Tue, 8 Sep 2020 13:56:01 +0200 Subject: Changed cc_varargs to an option type Instead of being a simple boolean we now use an option type to record the number of fixed (non-vararg) arguments. Hence, `None` means not vararg, and `Some n` means `n` fixed arguments followed with varargs. --- riscV/Asmexpand.ml | 6 +++--- riscV/Conventions1.v | 3 ++- 2 files changed, 5 insertions(+), 4 deletions(-) (limited to 'riscV') diff --git a/riscV/Asmexpand.ml b/riscV/Asmexpand.ml index 810514a3..80e33b2b 100644 --- a/riscV/Asmexpand.ml +++ b/riscV/Asmexpand.ml @@ -100,7 +100,7 @@ let rec fixup_variadic_call ri rf tyl = end let fixup_call sg = - if sg.sig_cc.cc_vararg then fixup_variadic_call 0 0 sg.sig_args + if (sg.sig_cc.cc_vararg <> None) then fixup_variadic_call 0 0 sg.sig_args (* Handling of annotations *) @@ -588,7 +588,7 @@ let expand_instruction instr = | Pallocframe (sz, ofs) -> let sg = get_current_function_sig() in emit (Pmv (X30, X2)); - if sg.sig_cc.cc_vararg then begin + if (sg.sig_cc.cc_vararg <> None) then begin let n = arguments_size sg in let extra_sz = if n >= 8 then 0 else align ((8 - n) * wordsize) 16 in let full_sz = Z.add sz (Z.of_uint extra_sz) in @@ -606,7 +606,7 @@ let expand_instruction instr = | Pfreeframe (sz, ofs) -> let sg = get_current_function_sig() in let extra_sz = - if sg.sig_cc.cc_vararg then begin + if (sg.sig_cc.cc_vararg <> None) then begin let n = arguments_size sg in if n >= 8 then 0 else align ((8 - n) * wordsize) 16 end else 0 in diff --git a/riscV/Conventions1.v b/riscV/Conventions1.v index 17326139..74c99d07 100644 --- a/riscV/Conventions1.v +++ b/riscV/Conventions1.v @@ -281,7 +281,8 @@ Fixpoint loc_arguments_rec (va: bool) 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 0. + 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. (** Argument locations are either non-temporary registers or [Outgoing] stack slots at nonnegative offsets. *) -- cgit 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 From aba0e740f25ffa5c338dfa76cab71144802cebc2 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sun, 21 Jun 2020 18:22:00 +0200 Subject: Replace `omega` tactic with `lia` Since Coq 8.12, `omega` is flagged as deprecated and scheduled for removal. Also replace CompCert's homemade tactics `omegaContradiction`, `xomega`, and `xomegaContradiction` with `lia` and `extlia`. Turn back on the deprecation warning for uses of `omega`. Make the proof of `Ctypes.sizeof_pos` more robust to variations in `lia`. --- riscV/Asm.v | 2 +- riscV/Asmgenproof.v | 12 ++++++------ riscV/Asmgenproof1.v | 20 +++++++++---------- riscV/ConstpropOpproof.v | 2 +- riscV/Conventions1.v | 22 ++++++++++----------- riscV/NeedOp.v | 4 ++-- riscV/SelectLongproof.v | 6 +++--- riscV/SelectOpproof.v | 34 ++++++++++++++++---------------- riscV/Stacklayout.v | 50 ++++++++++++++++++++++++------------------------ 9 files changed, 76 insertions(+), 76 deletions(-) (limited to 'riscV') diff --git a/riscV/Asm.v b/riscV/Asm.v index dc410a3b..30b128ec 100644 --- a/riscV/Asm.v +++ b/riscV/Asm.v @@ -1157,7 +1157,7 @@ Ltac Equalities := split. auto. intros. destruct B; auto. subst. auto. - (* trace length *) red; intros. inv H; simpl. - omega. + lia. eapply external_call_trace_length; eauto. eapply external_call_trace_length; eauto. - (* initial states *) diff --git a/riscV/Asmgenproof.v b/riscV/Asmgenproof.v index 5ec57886..ab07d071 100644 --- a/riscV/Asmgenproof.v +++ b/riscV/Asmgenproof.v @@ -67,7 +67,7 @@ Lemma transf_function_no_overflow: transf_function f = OK tf -> list_length_z tf.(fn_code) <= Ptrofs.max_unsigned. Proof. intros. monadInv H. destruct (zlt Ptrofs.max_unsigned (list_length_z x.(fn_code))); inv EQ0. - omega. + lia. Qed. Lemma exec_straight_exec: @@ -432,8 +432,8 @@ Proof. split. unfold goto_label. rewrite P. rewrite H1. auto. split. rewrite Pregmap.gss. constructor; auto. rewrite Ptrofs.unsigned_repr. replace (pos' - 0) with pos' in Q. - auto. omega. - generalize (transf_function_no_overflow _ _ H0). omega. + auto. lia. + generalize (transf_function_no_overflow _ _ H0). lia. intros. apply Pregmap.gso; auto. Qed. @@ -948,10 +948,10 @@ Local Transparent destroyed_by_op. rewrite <- (sp_val _ _ _ AG). rewrite chunk_of_Tptr in F. rewrite F. reflexivity. reflexivity. eexact U. } - exploit exec_straight_steps_2; eauto using functions_transl. omega. constructor. + exploit exec_straight_steps_2; eauto using functions_transl. lia. constructor. intros (ofs' & X & Y). left; exists (State rs3 m3'); split. - eapply exec_straight_steps_1; eauto. omega. constructor. + eapply exec_straight_steps_1; eauto. lia. constructor. econstructor; eauto. rewrite X; econstructor; eauto. apply agree_exten with rs2; eauto with asmgen. @@ -980,7 +980,7 @@ Local Transparent destroyed_at_function_entry. - (* return *) inv STACKS. simpl in *. - right. split. omega. split. auto. + right. split. lia. split. auto. rewrite <- ATPC in H5. econstructor; eauto. congruence. Qed. diff --git a/riscV/Asmgenproof1.v b/riscV/Asmgenproof1.v index c20c4e49..253e769f 100644 --- a/riscV/Asmgenproof1.v +++ b/riscV/Asmgenproof1.v @@ -35,7 +35,7 @@ Proof. - set (m := Int.sub n lo). assert (A: eqmod (two_p 12) (Int.unsigned lo) (Int.unsigned n)) by (apply Int.eqmod_sign_ext'; compute; auto). assert (B: eqmod (two_p 12) (Int.unsigned n - Int.unsigned lo) 0). - { replace 0 with (Int.unsigned n - Int.unsigned n) by omega. + { replace 0 with (Int.unsigned n - Int.unsigned n) by lia. auto using eqmod_sub, eqmod_refl. } assert (C: eqmod (two_p 12) (Int.unsigned m) 0). { apply eqmod_trans with (Int.unsigned n - Int.unsigned lo); auto. @@ -45,7 +45,7 @@ Proof. { apply eqmod_mod_eq in C. unfold Int.modu. change (Int.unsigned (Int.repr 4096)) with (two_p 12). rewrite C. reflexivity. - apply two_p_gt_ZERO; omega. } + apply two_p_gt_ZERO; lia. } rewrite <- (Int.divu_pow2 m (Int.repr 4096) (Int.repr 12)) by auto. rewrite Int.shl_mul_two_p. change (two_p (Int.unsigned (Int.repr 12))) with 4096. @@ -684,18 +684,18 @@ Proof. unfold Val.cmp; destruct (rs#r1); simpl; auto. rewrite B1. unfold Int.lt. rewrite zlt_false. auto. change (Int.signed (Int.repr Int.max_signed)) with Int.max_signed. - generalize (Int.signed_range i); omega. + generalize (Int.signed_range i); lia. * exploit (opimm32_correct Psltw Psltiw (Val.cmp Clt)); eauto. intros (rs1 & A1 & B1 & C1). exists rs1; split. eexact A1. split; auto. rewrite B1. unfold Val.cmp; simpl; destruct (rs#r1); simpl; auto. unfold Int.lt. replace (Int.signed (Int.add n Int.one)) with (Int.signed n + 1). destruct (zlt (Int.signed n) (Int.signed i)). - rewrite zlt_false by omega. auto. - rewrite zlt_true by omega. auto. + rewrite zlt_false by lia. auto. + rewrite zlt_true by lia. auto. rewrite Int.add_signed. symmetry; apply Int.signed_repr. assert (Int.signed n <> Int.max_signed). { red; intros E. elim H1. rewrite <- (Int.repr_signed n). rewrite E. auto. } - generalize (Int.signed_range n); omega. + generalize (Int.signed_range n); lia. + apply DFL. + apply DFL. Qed. @@ -782,18 +782,18 @@ Proof. unfold Val.cmpl; destruct (rs#r1); simpl; auto. rewrite B1. unfold Int64.lt. rewrite zlt_false. auto. change (Int64.signed (Int64.repr Int64.max_signed)) with Int64.max_signed. - generalize (Int64.signed_range i); omega. + generalize (Int64.signed_range i); lia. * exploit (opimm64_correct Psltl Psltil (fun v1 v2 => Val.maketotal (Val.cmpl Clt v1 v2))); eauto. intros (rs1 & A1 & B1 & C1). exists rs1; split. eexact A1. split; auto. rewrite B1. unfold Val.cmpl; simpl; destruct (rs#r1); simpl; auto. unfold Int64.lt. replace (Int64.signed (Int64.add n Int64.one)) with (Int64.signed n + 1). destruct (zlt (Int64.signed n) (Int64.signed i)). - rewrite zlt_false by omega. auto. - rewrite zlt_true by omega. auto. + rewrite zlt_false by lia. auto. + rewrite zlt_true by lia. auto. rewrite Int64.add_signed. symmetry; apply Int64.signed_repr. assert (Int64.signed n <> Int64.max_signed). { red; intros E. elim H1. rewrite <- (Int64.repr_signed n). rewrite E. auto. } - generalize (Int64.signed_range n); omega. + generalize (Int64.signed_range n); lia. + apply DFL. + apply DFL. Qed. diff --git a/riscV/ConstpropOpproof.v b/riscV/ConstpropOpproof.v index 765aa035..8445e55f 100644 --- a/riscV/ConstpropOpproof.v +++ b/riscV/ConstpropOpproof.v @@ -333,7 +333,7 @@ Proof. Int.bit_solve. destruct (zlt i0 n0). replace (Int.testbit n i0) with (negb (Int.testbit Int.zero i0)). rewrite Int.bits_zero. simpl. rewrite andb_true_r. auto. - rewrite <- EQ. rewrite Int.bits_zero_ext by omega. rewrite zlt_true by auto. + rewrite <- EQ. rewrite Int.bits_zero_ext by lia. rewrite zlt_true by auto. rewrite Int.bits_not by auto. apply negb_involutive. rewrite H6 by auto. auto. econstructor; split; eauto. auto. diff --git a/riscV/Conventions1.v b/riscV/Conventions1.v index 0fc8295e..5dd50a4c 100644 --- a/riscV/Conventions1.v +++ b/riscV/Conventions1.v @@ -320,14 +320,14 @@ Proof. assert (AL: forall ofs ty, ofs >= 0 -> align ofs (typesize ty) >= 0). { intros. assert (ofs <= align ofs (typesize ty)) by (apply align_le; apply typesize_pos). - omega. } + lia. } assert (ALD: forall ofs ty, ofs >= 0 -> (typealign ty | align ofs (typesize ty))). { intros. eapply Z.divide_trans. apply typealign_typesize. apply align_divides. apply typesize_pos. } assert (SK: (if Archi.ptr64 then 2 else 1) > 0). - { destruct Archi.ptr64; omega. } + { destruct Archi.ptr64; lia. } assert (SKK: forall ty, (if Archi.ptr64 then 2 else typesize ty) > 0). - { intros. destruct Archi.ptr64. omega. apply typesize_pos. } + { intros. destruct Archi.ptr64. lia. apply typesize_pos. } 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. @@ -336,7 +336,7 @@ Proof. - eapply OF; eauto. - subst p; simpl. auto using align_divides, typealign_pos. - eapply OF; [idtac|eauto]. - generalize (AL ofs ty OO) (SKK ty); omega. + generalize (AL ofs ty OO) (SKK ty); lia. } assert (B: forall va ri rf ofs ty f, OKF f -> ofs >= 0 -> OK (float_arg va ri rf ofs ty f)). @@ -347,12 +347,12 @@ Proof. + subst p; simpl. apply CSF. eapply list_nth_z_in; eauto. + eapply OF; eauto. + subst p; repeat split; auto. - + eapply OF; [idtac|eauto]. generalize (AL ofs ty OO) (SKK ty); omega. + + eapply OF; [idtac|eauto]. generalize (AL ofs ty OO) (SKK ty); lia. + subst p; simpl. apply CSF. eapply list_nth_z_in; eauto. + eapply OF; eauto. - destruct H. + subst p; repeat split; auto. - + eapply OF; [idtac|eauto]. generalize (AL ofs ty OO) (SKK ty); omega. + + eapply OF; [idtac|eauto]. generalize (AL ofs ty OO) (SKK ty); lia. } assert (C: forall va ri rf ofs f, OKF f -> ofs >= 0 -> OK (split_long_arg va ri rf ofs f)). @@ -364,13 +364,13 @@ Proof. [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. + + eapply OF; [idtac|eauto]. lia. - 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. + + eapply OF; [idtac|eauto]. lia. - red; simpl; intros; destruct H. - + subst p; repeat split; auto using Z.divide_1_l. omega. - + eapply OF; [idtac|eauto]. omega. + + subst p; repeat split; auto using Z.divide_1_l. lia. + + eapply OF; [idtac|eauto]. lia. } cut (forall tyl fixed ri rf ofs, ofs >= 0 -> OK (loc_arguments_rec tyl fixed ri rf ofs)). unfold OK. eauto. @@ -392,7 +392,7 @@ Lemma loc_arguments_acceptable: forall (s: signature) (p: rpair loc), In p (loc_arguments s) -> forall_rpair loc_argument_acceptable p. Proof. - unfold loc_arguments; intros. eapply loc_arguments_rec_charact; eauto. omega. + unfold loc_arguments; intros. eapply loc_arguments_rec_charact; eauto. lia. Qed. Lemma loc_arguments_main: diff --git a/riscV/NeedOp.v b/riscV/NeedOp.v index 117bbcb4..4070431a 100644 --- a/riscV/NeedOp.v +++ b/riscV/NeedOp.v @@ -164,8 +164,8 @@ Lemma operation_is_redundant_sound: vagree v arg1' nv. Proof. intros. destruct op; simpl in *; try discriminate; inv H1; FuncInv; subst. -- apply sign_ext_redundant_sound; auto. omega. -- apply sign_ext_redundant_sound; auto. omega. +- apply sign_ext_redundant_sound; auto. lia. +- apply sign_ext_redundant_sound; auto. lia. - apply andimm_redundant_sound; auto. - apply orimm_redundant_sound; auto. Qed. diff --git a/riscV/SelectLongproof.v b/riscV/SelectLongproof.v index 78a1935d..3794e050 100644 --- a/riscV/SelectLongproof.v +++ b/riscV/SelectLongproof.v @@ -502,8 +502,8 @@ Proof. assert (LTU2: Int.ltu (Int.sub Int64.iwordsize' n) Int64.iwordsize' = true). { unfold Int.ltu; apply zlt_true. unfold Int.sub. change (Int.unsigned Int64.iwordsize') with 64. - rewrite Int.unsigned_repr. omega. - assert (64 < Int.max_unsigned) by reflexivity. omega. } + rewrite Int.unsigned_repr. lia. + assert (64 < Int.max_unsigned) by reflexivity. lia. } assert (X: eval_expr ge sp e m le (Eop (Oshrlimm (Int.repr (Int64.zwordsize - 1))) (a ::: Enil)) (Vlong (Int64.shr' i (Int.repr (Int64.zwordsize - 1))))). @@ -514,7 +514,7 @@ Proof. TrivialExists. constructor. EvalOp. simpl; eauto. constructor. simpl. unfold Int.ltu; rewrite zlt_true. rewrite Int64.shrx'_shr_2 by auto. reflexivity. - change (Int.unsigned Int64.iwordsize') with 64; omega. + change (Int.unsigned Int64.iwordsize') with 64; lia. *) Qed. diff --git a/riscV/SelectOpproof.v b/riscV/SelectOpproof.v index 593be1ed..b0b4b794 100644 --- a/riscV/SelectOpproof.v +++ b/riscV/SelectOpproof.v @@ -365,20 +365,20 @@ Proof. change (Int.ltu (Int.repr 32) Int64.iwordsize') with true; simpl. apply Val.lessdef_same. f_equal. transitivity (Int.repr (Z.shiftr (Int.signed i * Int.signed i0) 32)). - unfold Int.mulhs; f_equal. rewrite Zshiftr_div_two_p by omega. reflexivity. + unfold Int.mulhs; f_equal. rewrite Zshiftr_div_two_p by lia. reflexivity. apply Int.same_bits_eq; intros n N. change Int.zwordsize with 32 in *. - assert (N1: 0 <= n < 64) by omega. + assert (N1: 0 <= n < 64) by lia. rewrite Int64.bits_loword by auto. rewrite Int64.bits_shr' by auto. change (Int.unsigned (Int.repr 32)) with 32. change Int64.zwordsize with 64. - rewrite zlt_true by omega. + rewrite zlt_true by lia. rewrite Int.testbit_repr by auto. - unfold Int64.mul. rewrite Int64.testbit_repr by (change Int64.zwordsize with 64; omega). + unfold Int64.mul. rewrite Int64.testbit_repr by (change Int64.zwordsize with 64; lia). transitivity (Z.testbit (Int.signed i * Int.signed i0) (n + 32)). - rewrite Z.shiftr_spec by omega. auto. + rewrite Z.shiftr_spec by lia. auto. apply Int64.same_bits_eqm. apply Int64.eqm_mult; apply Int64.eqm_unsigned_repr. - change Int64.zwordsize with 64; omega. + change Int64.zwordsize with 64; lia. - TrivialExists. Qed. @@ -393,20 +393,20 @@ Proof. change (Int.ltu (Int.repr 32) Int64.iwordsize') with true; simpl. apply Val.lessdef_same. f_equal. transitivity (Int.repr (Z.shiftr (Int.unsigned i * Int.unsigned i0) 32)). - unfold Int.mulhu; f_equal. rewrite Zshiftr_div_two_p by omega. reflexivity. + unfold Int.mulhu; f_equal. rewrite Zshiftr_div_two_p by lia. reflexivity. apply Int.same_bits_eq; intros n N. change Int.zwordsize with 32 in *. - assert (N1: 0 <= n < 64) by omega. + assert (N1: 0 <= n < 64) by lia. rewrite Int64.bits_loword by auto. rewrite Int64.bits_shru' by auto. change (Int.unsigned (Int.repr 32)) with 32. change Int64.zwordsize with 64. - rewrite zlt_true by omega. + rewrite zlt_true by lia. rewrite Int.testbit_repr by auto. - unfold Int64.mul. rewrite Int64.testbit_repr by (change Int64.zwordsize with 64; omega). + unfold Int64.mul. rewrite Int64.testbit_repr by (change Int64.zwordsize with 64; lia). transitivity (Z.testbit (Int.unsigned i * Int.unsigned i0) (n + 32)). - rewrite Z.shiftr_spec by omega. auto. + rewrite Z.shiftr_spec by lia. auto. apply Int64.same_bits_eqm. apply Int64.eqm_mult; apply Int64.eqm_unsigned_repr. - change Int64.zwordsize with 64; omega. + change Int64.zwordsize with 64; lia. - TrivialExists. Qed. @@ -563,8 +563,8 @@ Proof. assert (LTU2: Int.ltu (Int.sub Int.iwordsize n) Int.iwordsize = true). { unfold Int.ltu; apply zlt_true. unfold Int.sub. change (Int.unsigned Int.iwordsize) with 32. - rewrite Int.unsigned_repr. omega. - assert (32 < Int.max_unsigned) by reflexivity. omega. } + rewrite Int.unsigned_repr. lia. + assert (32 < Int.max_unsigned) by reflexivity. lia. } assert (X: eval_expr ge sp e m le (Eop (Oshrimm (Int.repr (Int.zwordsize - 1))) (a ::: Enil)) (Vint (Int.shr i (Int.repr (Int.zwordsize - 1))))). @@ -575,7 +575,7 @@ Proof. TrivialExists. constructor. EvalOp. simpl; eauto. constructor. simpl. unfold Int.ltu; rewrite zlt_true. rewrite Int.shrx_shr_2 by auto. reflexivity. - change (Int.unsigned Int.iwordsize) with 32; omega. + change (Int.unsigned Int.iwordsize) with 32; lia. *) Qed. @@ -763,7 +763,7 @@ Qed. Theorem eval_cast8unsigned: unary_constructor_sound cast8unsigned (Val.zero_ext 8). Proof. red; intros until x. unfold cast8unsigned. - rewrite Val.zero_ext_and. apply eval_andimm. omega. + rewrite Val.zero_ext_and. apply eval_andimm. lia. Qed. Theorem eval_cast16signed: unary_constructor_sound cast16signed (Val.sign_ext 16). @@ -776,7 +776,7 @@ Qed. Theorem eval_cast16unsigned: unary_constructor_sound cast16unsigned (Val.zero_ext 16). Proof. red; intros until x. unfold cast8unsigned. - rewrite Val.zero_ext_and. apply eval_andimm. omega. + rewrite Val.zero_ext_and. apply eval_andimm. lia. Qed. Theorem eval_intoffloat: diff --git a/riscV/Stacklayout.v b/riscV/Stacklayout.v index d0c6a526..25f02aab 100644 --- a/riscV/Stacklayout.v +++ b/riscV/Stacklayout.v @@ -68,15 +68,15 @@ Local Opaque Z.add Z.mul sepconj range. set (ol := align (size_callee_save_area b ocs) 8). set (ostkdata := align (ol + 4 * b.(bound_local)) 8). replace (size_chunk Mptr) with w by (rewrite size_chunk_Mptr; auto). - assert (0 < w) by (unfold w; destruct Archi.ptr64; omega). + assert (0 < w) by (unfold w; destruct Archi.ptr64; lia). generalize b.(bound_local_pos) b.(bound_outgoing_pos) b.(bound_stack_data_pos); intros. - assert (0 <= 4 * b.(bound_outgoing)) by omega. - assert (4 * b.(bound_outgoing) <= olink) by (apply align_le; omega). - assert (olink + w <= oretaddr) by (unfold oretaddr; omega). - assert (oretaddr + w <= ocs) by (unfold ocs; omega). + assert (0 <= 4 * b.(bound_outgoing)) by lia. + assert (4 * b.(bound_outgoing) <= olink) by (apply align_le; lia). + assert (olink + w <= oretaddr) by (unfold oretaddr; lia). + assert (oretaddr + w <= ocs) by (unfold ocs; lia). assert (ocs <= size_callee_save_area b ocs) by (apply size_callee_save_area_incr). - assert (size_callee_save_area b ocs <= ol) by (apply align_le; omega). - assert (ol + 4 * b.(bound_local) <= ostkdata) by (apply align_le; omega). + assert (size_callee_save_area b ocs <= ol) by (apply align_le; lia). + assert (ol + 4 * b.(bound_local) <= ostkdata) by (apply align_le; lia). (* Reorder as: outgoing back link @@ -89,11 +89,11 @@ Local Opaque Z.add Z.mul sepconj range. rewrite sep_swap45. (* Apply range_split and range_split2 repeatedly *) unfold fe_ofs_arg. - apply range_split_2. fold olink; omega. omega. - apply range_split. omega. - apply range_split. omega. - apply range_split_2. fold ol. omega. omega. - apply range_drop_right with ostkdata. omega. + apply range_split_2. fold olink; lia. lia. + apply range_split. lia. + apply range_split. lia. + apply range_split_2. fold ol. lia. lia. + apply range_drop_right with ostkdata. lia. eapply sep_drop2. eexact H. Qed. @@ -109,16 +109,16 @@ Proof. set (ocs := oretaddr + w). set (ol := align (size_callee_save_area b ocs) 8). set (ostkdata := align (ol + 4 * b.(bound_local)) 8). - assert (0 < w) by (unfold w; destruct Archi.ptr64; omega). + assert (0 < w) by (unfold w; destruct Archi.ptr64; lia). generalize b.(bound_local_pos) b.(bound_outgoing_pos) b.(bound_stack_data_pos); intros. - assert (0 <= 4 * b.(bound_outgoing)) by omega. - assert (4 * b.(bound_outgoing) <= olink) by (apply align_le; omega). - assert (olink + w <= oretaddr) by (unfold oretaddr; omega). - assert (oretaddr + w <= ocs) by (unfold ocs; omega). + assert (0 <= 4 * b.(bound_outgoing)) by lia. + assert (4 * b.(bound_outgoing) <= olink) by (apply align_le; lia). + assert (olink + w <= oretaddr) by (unfold oretaddr; lia). + assert (oretaddr + w <= ocs) by (unfold ocs; lia). assert (ocs <= size_callee_save_area b ocs) by (apply size_callee_save_area_incr). - assert (size_callee_save_area b ocs <= ol) by (apply align_le; omega). - assert (ol + 4 * b.(bound_local) <= ostkdata) by (apply align_le; omega). - split. omega. apply align_le. omega. + assert (size_callee_save_area b ocs <= ol) by (apply align_le; lia). + assert (ol + 4 * b.(bound_local) <= ostkdata) by (apply align_le; lia). + split. lia. apply align_le. lia. Qed. Lemma frame_env_aligned: @@ -137,11 +137,11 @@ Proof. set (ocs := oretaddr + w). set (ol := align (size_callee_save_area b ocs) 8). set (ostkdata := align (ol + 4 * b.(bound_local)) 8). - assert (0 < w) by (unfold w; destruct Archi.ptr64; omega). + assert (0 < w) by (unfold w; destruct Archi.ptr64; lia). replace (align_chunk Mptr) with w by (rewrite align_chunk_Mptr; auto). split. apply Z.divide_0_r. - split. apply align_divides; omega. - split. apply align_divides; omega. - split. apply align_divides; omega. - apply Z.divide_add_r. apply align_divides; omega. apply Z.divide_refl. + split. apply align_divides; lia. + split. apply align_divides; lia. + split. apply align_divides; lia. + apply Z.divide_add_r. apply align_divides; lia. apply Z.divide_refl. Qed. -- cgit From e81d015e3cc2cb0c352792d0cac12f1594281bc2 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sun, 10 Jan 2021 14:34:58 +0100 Subject: RISC-V: wrong fixup code generated for vararg calls with fixed FP args This is a follow-up to 2076a3bb3. Integer registers were wrongly reserved for fixed FP arguments, causing variadic FP arguments to end up in the wrong integer registers. Added regression test in test/regression/varargs2.c --- riscV/Asmexpand.ml | 30 ++++++++++++++++++------------ 1 file changed, 18 insertions(+), 12 deletions(-) (limited to 'riscV') diff --git a/riscV/Asmexpand.ml b/riscV/Asmexpand.ml index f01ecb23..da97c4a8 100644 --- a/riscV/Asmexpand.ml +++ b/riscV/Asmexpand.ml @@ -72,27 +72,33 @@ let rec fixup_variadic_call fixed ri rf tyl = | (Tint | Tany32) :: tyl -> fixup_variadic_call (fixed - 1) (ri + 1) rf tyl | Tsingle :: tyl -> - if fixed <= 0 then begin + if fixed > 0 then + fixup_variadic_call (fixed - 1) ri (rf + 1) tyl + else 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 + emit (Pfmvxs(rd, rs)); + fixup_variadic_call (fixed - 1) (ri + 1) (rf + 1) tyl + end | Tlong :: tyl -> let ri' = if Archi.ptr64 then ri + 1 else align ri 2 + 2 in fixup_variadic_call (fixed - 1) ri' rf tyl | (Tfloat | Tany64) :: tyl -> if Archi.ptr64 then begin - if fixed <= 0 then begin + if fixed > 0 then + fixup_variadic_call (fixed - 1) ri (rf + 1) tyl + else 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 + emit (Pfmvxd(rd, rs)); + fixup_variadic_call (fixed - 1) (ri + 1) (rf + 1) tyl + end end else begin let ri = align ri 2 in if ri < 8 then begin - if fixed <= 0 then begin + if fixed > 0 then + fixup_variadic_call (fixed - 1) ri (rf + 1) tyl + else begin let rs = float_param_regs.(rf) and rd1 = int_param_regs.(ri) and rd2 = int_param_regs.(ri + 1) in @@ -100,9 +106,9 @@ let rec fixup_variadic_call fixed ri rf tyl = 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 + emit (Paddiw(X2, X X2, _16)); + fixup_variadic_call (fixed - 1) (ri + 2) (rf + 1) tyl + end end end -- cgit From 88567ce6d247562a9fa9151eaa32f7ad63ea37c0 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Mon, 11 Jan 2021 18:04:25 +0100 Subject: 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. --- riscV/Asm.v | 4 + riscV/Asmexpand.ml | 194 +++++++++++++++++++++++++++++-------------------- riscV/Conventions1.v | 86 ++++++++++++---------- riscV/TargetPrinter.ml | 4 + 4 files changed, 171 insertions(+), 117 deletions(-) (limited to 'riscV') 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 _ _ _ diff --git a/riscV/Asmexpand.ml b/riscV/Asmexpand.ml index da97c4a8..e8c142e9 100644 --- a/riscV/Asmexpand.ml +++ b/riscV/Asmexpand.ml @@ -24,6 +24,7 @@ open Asmexpandaux open AST open Camlcoq open! Integers +open Locations exception Error of string @@ -50,6 +51,86 @@ let expand_addptrofs dst src n = let expand_storeind_ptr src base ofs = List.iter emit (Asmgen.storeind_ptr src base ofs []) +(* Fix-up code around function calls and function entry. + Some floating-point arguments residing in FP registers need to be + moved to integer registers or register pairs. + Symmetrically, some floating-point parameter passed in integer + registers or register pairs need to be moved to FP registers. *) + +let int_param_regs = [| X10; X11; X12; X13; X14; X15; X16; X17 |] + +let move_single_arg fr i = + emit (Pfmvxs(int_param_regs.(i), fr)) + +let move_double_arg fr i = + if Archi.ptr64 then begin + emit (Pfmvxd(int_param_regs.(i), fr)) + end else begin + emit (Paddiw(X2, X X2, Integers.Int.neg _16)); + emit (Pfsd(fr, X2, Ofsimm _0)); + emit (Plw(int_param_regs.(i), X2, Ofsimm _0)); + if i < 7 then begin + emit (Plw(int_param_regs.(i + 1), X2, Ofsimm _4)) + end else begin + emit (Plw(X31, X2, Ofsimm _4)); + emit (Psw(X31, X2, Ofsimm _16)) + end; + emit (Paddiw(X2, X X2, _16)) + end + +let move_single_param fr i = + emit (Pfmvsx(fr, int_param_regs.(i))) + +let move_double_param fr i = + if Archi.ptr64 then begin + emit (Pfmvdx(fr, int_param_regs.(i))) + end else begin + emit (Paddiw(X2, X X2, Integers.Int.neg _16)); + emit (Psw(int_param_regs.(i), X2, Ofsimm _0)); + if i < 7 then begin + emit (Psw(int_param_regs.(i + 1), X2, Ofsimm _4)) + end else begin + emit (Plw(X31, X2, Ofsimm _16)); + emit (Psw(X31, X2, Ofsimm _4)) + end; + emit (Pfld(fr, X2, Ofsimm _0)); + emit (Paddiw(X2, X X2, _16)) + end + +let float_extra_index = function + | Machregs.F0 -> Some (F0, 0) + | Machregs.F1 -> Some (F1, 1) + | Machregs.F2 -> Some (F2, 2) + | Machregs.F3 -> Some (F3, 3) + | Machregs.F4 -> Some (F4, 4) + | Machregs.F5 -> Some (F5, 5) + | Machregs.F6 -> Some (F6, 6) + | Machregs.F7 -> Some (F7, 7) + | _ -> None + +let fixup_gen single double sg = + let fixup ty loc = + match ty, loc with + | Tsingle, One (R r) -> + begin match float_extra_index r with + | Some(r, i) -> single r i + | None -> () + end + | (Tfloat | Tany64), One (R r) -> + begin match float_extra_index r with + | Some(r, i) -> double r i + | None -> () + end + | _, _ -> () + in + List.iter2 fixup sg.sig_args (Conventions1.loc_arguments sg) + +let fixup_call sg = + fixup_gen move_single_arg move_double_arg sg + +let fixup_function_entry sg = + fixup_gen move_single_param move_double_param sg + (* Built-ins. They come in two flavors: - annotation statements: take their arguments in registers or stack locations; generate no code; @@ -57,66 +138,6 @@ let expand_storeind_ptr src base ofs = 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 fixed ri rf tyl = - if ri < 8 then - match tyl with - | [] -> - () - | (Tint | Tany32) :: tyl -> - fixup_variadic_call (fixed - 1) (ri + 1) rf tyl - | Tsingle :: tyl -> - if fixed > 0 then - fixup_variadic_call (fixed - 1) ri (rf + 1) tyl - else begin - let rs = float_param_regs.(rf) - and rd = int_param_regs.(ri) in - emit (Pfmvxs(rd, rs)); - fixup_variadic_call (fixed - 1) (ri + 1) (rf + 1) tyl - end - | Tlong :: tyl -> - let ri' = if Archi.ptr64 then ri + 1 else align ri 2 + 2 in - fixup_variadic_call (fixed - 1) ri' rf tyl - | (Tfloat | Tany64) :: tyl -> - if Archi.ptr64 then begin - if fixed > 0 then - fixup_variadic_call (fixed - 1) ri (rf + 1) tyl - else begin - let rs = float_param_regs.(rf) - and rd = int_param_regs.(ri) in - emit (Pfmvxd(rd, rs)); - fixup_variadic_call (fixed - 1) (ri + 1) (rf + 1) tyl - end - end else begin - let ri = align ri 2 in - if ri < 8 then begin - if fixed > 0 then - fixup_variadic_call (fixed - 1) ri (rf + 1) tyl - else 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 (fixed - 1) (ri + 2) (rf + 1) tyl - end - end - end - -let fixup_call sg = - 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 *) let expand_annot_val kind txt targ args res = @@ -323,37 +344,49 @@ let expand_builtin_vstore chunk args = (* 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 +let arg_int_size ri rf ofs k = + if ri < 8 + then k (ri + 1) rf ofs + else k ri rf (ofs + 1) + +let arg_single_size ri rf ofs k = + if rf < 8 + then k ri (rf + 1) ofs + else arg_int_size ri rf ofs k + +let arg_long_size ri rf ofs k = + if Archi.ptr64 then + if ri < 8 + then k (ri + 1) rf ofs + else k ri rf (ofs + 1) + else + if ri < 7 then k (ri + 2) rf ofs + else if ri = 7 then k (ri + 1) rf (ofs + 1) + else k ri rf (align ofs 2 + 2) + +let arg_double_size ri rf ofs k = + if rf < 8 + then k ri (rf + 1) ofs + else arg_long_size ri rf ofs k + +let rec args_size l ri rf ofs = + match l with | [] -> (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 + arg_int_size ri rf ofs (args_size l) | Tsingle :: l -> - if rf < 8 - then args_size ri (rf + 1) ofs l - else args_size ri rf (ofs + 1) l + arg_single_size ri rf ofs (args_size 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 + arg_long_size ri rf ofs (args_size 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 + arg_double_size ri rf ofs (args_size 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 = - let (ri, _, ofs) = args_size 0 0 0 sg.sig_args in + let (ri, _, ofs) = args_size sg.sig_args 0 0 0 in ri + ofs let save_arguments first_reg base_ofs = @@ -744,6 +777,7 @@ let preg_to_dwarf = function let expand_function id fn = try set_current_function fn; + fixup_function_entry fn.fn_sig; expand id (* sp= *) 2 preg_to_dwarf expand_instruction fn.fn_code; Errors.OK (get_current_function ()) with Error s -> diff --git a/riscV/Conventions1.v b/riscV/Conventions1.v index 5dd50a4c..6cb06c61 100644 --- a/riscV/Conventions1.v +++ b/riscV/Conventions1.v @@ -176,20 +176,21 @@ Qed. - 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. + (fa1...fa8: float_param_regs) then in integer registers (a1...a8), + and the remaining arguments on the stack, in 8-byte slots. -- 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. +- RV32: same, but arguments of size 64 bits that must be passed in + integer registers 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. For variadic functions, the fixed arguments are passed as described above, then the variadic arguments receive special treatment: -- RV64: all variadic arguments, including FP arguments, - are passed in the remaining integer registers (a1...a8), - then on the stack, in 8-byte slots. +- RV64: FP registers are not used for passing variadic arguments. + 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 @@ -207,6 +208,15 @@ Definition int_param_regs := Definition float_param_regs := F10 :: F11 :: F12 :: F13 :: F14 :: F15 :: F16 :: F17 :: nil. +(** To evaluate FP arguments that must be passed in integer registers, + we can use any FP caller-save register that is not already used to pass + a fixed FP argument. Since there are 8 integer registers for argument + passing, we need at most 8 extra more FP registers for these FP + arguments. *) + +Definition float_extra_param_regs := + F0 :: F1 :: F2 :: F3 :: F4 :: F5 :: F6 :: F7 :: nil. + 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 @@ -220,26 +230,27 @@ Definition int_arg (ri rf ofs: Z) (ty: typ) 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 + match list_nth_z (if va then nil else 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 *) + One (R r) :: rec ri (rf + 1) ofs + | None => + (* We are out of FP registers, or cannot use them because vararg, + so try to put the argument in an extra FP register while + reserving an integer register or register pair into which + fixup code will move the extra FP register. *) + let regpair := negb Archi.ptr64 && zeq (typesize ty) 2 in + let ri' := if va && regpair then align ri 2 else ri in + match list_nth_z float_extra_param_regs ri' with + | Some r => + let ri'' := ri' + (if Archi.ptr64 then 1 else typesize ty) in + let ofs'' := if regpair && zeq ri' 7 then ofs + 1 else ofs in + One (R r) :: rec ri'' rf ofs'' + | None => + (* We are out of integer registers, pass argument on stack *) let ofs := align ofs (typesize 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 (typesize ty) in - One(S Outgoing ofs ty) - :: rec ri rf (ofs + (if Archi.ptr64 then 2 else typesize ty)) + :: rec ri' rf (ofs + (if Archi.ptr64 then 2 else typesize ty)) + end end. Definition split_long_arg (va: bool) (ri rf ofs: Z) @@ -317,6 +328,8 @@ Proof. { decide_goal. } assert (CSF: forall r, In r float_param_regs -> is_callee_save r = false). { decide_goal. } + assert (CSFX: forall r, In r float_extra_param_regs -> is_callee_save r = false). + { decide_goal. } assert (AL: forall ofs ty, ofs >= 0 -> align ofs (typesize ty) >= 0). { intros. assert (ofs <= align ofs (typesize ty)) by (apply align_le; apply typesize_pos). @@ -341,18 +354,17 @@ Proof. 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. - + eapply OF; [idtac|eauto]. generalize (AL ofs ty OO) (SKK ty); lia. - + subst p; simpl. apply CSF. eapply list_nth_z_in; eauto. - + eapply OF; eauto. + destruct (list_nth_z (if va then nil else float_param_regs) rf) as [r|] eqn:NTH. - destruct H. - + subst p; repeat split; auto. - + eapply OF; [idtac|eauto]. generalize (AL ofs ty OO) (SKK ty); lia. + + subst p; simpl. apply CSF. destruct va. simpl in NTH; discriminate. eapply list_nth_z_in; eauto. + + eapply OF; eauto. + - set (regpair := negb Archi.ptr64 && zeq (typesize ty) 2) in *. + set (ri' := if va && regpair then align ri 2 else ri) in *. + destruct (list_nth_z float_extra_param_regs ri') as [r|] eqn:NTH'; destruct H. + + subst p; simpl. apply CSFX. eapply list_nth_z_in; eauto. + + eapply OF; [|eauto]. destruct (regpair && zeq ri' 7); lia. + + subst p; simpl. auto. + + eapply OF; [|eauto]. generalize (AL ofs ty OO) (SKK ty); lia. } assert (C: forall va ri rf ofs f, OKF f -> ofs >= 0 -> OK (split_long_arg va ri rf ofs f)). diff --git a/riscV/TargetPrinter.ml b/riscV/TargetPrinter.ml index 64bcea4c..5cd47b46 100644 --- a/riscV/TargetPrinter.ml +++ b/riscV/TargetPrinter.ml @@ -392,8 +392,12 @@ module Target : TARGET = fprintf oc " fmv.d %a, %a\n" freg fd freg fs | Pfmvxs (rd,fs) -> fprintf oc " fmv.x.s %a, %a\n" ireg rd freg fs + | Pfmvsx (fd,rs) -> + fprintf oc " fmv.s.x %a, %a\n" freg fd ireg rs | Pfmvxd (rd,fs) -> fprintf oc " fmv.x.d %a, %a\n" ireg rd freg fs + | Pfmvdx (fd,rs) -> + fprintf oc " fmv.d.x %a, %a\n" freg fd ireg rs (* 32-bit (single-precision) floating point *) | Pfls (fd, ra, ofs) -> -- cgit From 478ece46d8323ea182ded96a531309becf7445bb Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sat, 16 Jan 2021 15:27:02 +0100 Subject: Support re-normalization of function parameters at function entry This is complementary to 28f235806 Some ABIs leave more flexibility concerning function parameters than CompCert expects. For instance, the AArch64/ELF ABI allow the caller of a function to leave unspecified the "padding bits" of function parameters. As an example, a parameter of type "unsigned char" may not have zeros in bits 8 to 63, but may have any bits there. When the caller is compiled by CompCert, it normalizes argument values to the parameter types before the call, so padding bits are always correct w.r.t. the type of the argument. This is no longer guaranteed in interoperability scenarios, when the caller is not compiled by CompCert. This commit adds a general mechanism to insert "re-normalization" conversions on the parameters of a function, at function entry. This is controlled by the platform-dependent function Convention1.return_value_needs_normalization. The semantic preservation proof is still conducted against the CompCert model, where the argument values of functions are already normalized. What the proof shows is that the extra conversions have no effect in this case. In future work we could relax the CompCert model, allowing functions to pass arguments that are not normalized. --- riscV/Conventions1.v | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'riscV') diff --git a/riscV/Conventions1.v b/riscV/Conventions1.v index 6cb06c61..eeaae3c4 100644 --- a/riscV/Conventions1.v +++ b/riscV/Conventions1.v @@ -413,8 +413,9 @@ Proof. reflexivity. Qed. -(** ** Normalization of function results *) +(** ** Normalization of function results and parameters *) (** No normalization needed. *) Definition return_value_needs_normalization (t: rettype) := false. +Definition parameter_needs_normalization (t: rettype) := false. -- cgit From fc82b6c80fd3feeb4ef9478e6faa16b5b1104593 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Thu, 21 Jan 2021 15:44:09 +0100 Subject: Qualify `Hint` as `Global Hint` where appropriate This avoids a new warning of Coq 8.13. Eventually these `Global Hint` should become `#[export] Hint`, with a cleaner but different meaning than `Global Hint`. --- riscV/Asmgenproof1.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'riscV') diff --git a/riscV/Asmgenproof1.v b/riscV/Asmgenproof1.v index 253e769f..8195ce44 100644 --- a/riscV/Asmgenproof1.v +++ b/riscV/Asmgenproof1.v @@ -88,7 +88,7 @@ Proof. intros. apply ireg_of_not_X31 in H. congruence. Qed. -Hint Resolve ireg_of_not_X31 ireg_of_not_X31': asmgen. +Global Hint Resolve ireg_of_not_X31 ireg_of_not_X31': asmgen. (** Useful simplification tactic *) -- cgit From 30feb31c6d6e9235acad42ec5d09d14f3919cc36 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Wed, 30 Dec 2020 11:41:10 +0100 Subject: Introduce and use PrintAsmaux.variable_section This is a generalization of the previous PrintAsmaux.common_section function that - handles initialized variables in addition to uninitialized variables; - can be used for Section_const, not just for Section_data. --- riscV/TargetPrinter.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'riscV') diff --git a/riscV/TargetPrinter.ml b/riscV/TargetPrinter.ml index 5cd47b46..d8137f84 100644 --- a/riscV/TargetPrinter.ml +++ b/riscV/TargetPrinter.ml @@ -108,9 +108,9 @@ module Target : TARGET = let name_of_section = function | Section_text -> ".text" | Section_data i | Section_small_data i -> - if i then ".data" else common_section () + variable_section ~sec:".data" ~bss:".bss" i | Section_const i | Section_small_const i -> - if i || (not !Clflags.option_fcommon) then ".section .rodata" else "COMM" + variable_section ~sec:".section .rodata" i | Section_string -> ".section .rodata" | Section_literal -> ".section .rodata" | Section_jumptable -> ".section .rodata" -- cgit