From 82f9d1f96b30106a338e77ec83b7321c2c65f929 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Tue, 17 May 2016 15:37:56 +0200 Subject: Introduce register pairs to describe calling conventions more precisely This commit changes the loc_arguments and loc_result functions that describe calling conventions so that each argument/result can be mapped either to a single location or (in the case of a 64-bit integer) to a pair of two 32-bit locations. In the current CompCert, all arguments/results of type Tlong are systematically split in two 32-bit halves. We will need to change this in the future to support 64-bit processors. The alternative approach implemented by this commit enables the loc_arguments and loc_result functions to describe precisely which arguments need splitting. Eventually, the remainder of CompCert should not assume anything about splitting 64-bit types in two halves. Summary of changes: - AST: introduce the type "rpair A" of register pairs - Conventions1, Conventions: use it when describing calling conventions - LTL, Linear, Mach, Asm: honor the new calling conventions when observing external calls - Events: suppress external_call', no longer useful - All passes from Allocation to Asmgen: adapt accordingly. --- arm/Conventions1.v | 262 ++++++++++++++++++++++++----------------------------- 1 file changed, 119 insertions(+), 143 deletions(-) (limited to 'arm/Conventions1.v') diff --git a/arm/Conventions1.v b/arm/Conventions1.v index abd28b18..3eae50ef 100644 --- a/arm/Conventions1.v +++ b/arm/Conventions1.v @@ -88,33 +88,43 @@ Definition dummy_float_reg := F0. (**r Used in [Coloring]. *) so we have code in [arm/PrintAsm.ml] that inserts additional moves to/from [F0]. *) -Definition loc_result (s: signature) : list mreg := +Definition loc_result (s: signature) : rpair mreg := match s.(sig_res) with - | None => R0 :: nil - | Some (Tint | Tany32) => R0 :: nil - | Some (Tfloat | Tsingle | Tany64) => F0 :: nil - | Some Tlong => R1 :: R0 :: nil + | None => One R0 + | Some (Tint | Tany32) => One R0 + | Some (Tfloat | Tsingle | Tany64) => One F0 + | Some Tlong => Twolong R1 R0 end. (** The result registers have types compatible with that given in the signature. *) Lemma loc_result_type: forall sig, - subtype_list (proj_sig_res' sig) (map mreg_type (loc_result sig)) = true. + subtype (proj_sig_res sig) (typ_rpair mreg_type (loc_result sig)) = true. Proof. - intros. unfold proj_sig_res', loc_result. destruct (sig_res sig) as [[]|]; auto. + intros. unfold proj_sig_res, loc_result. destruct (sig_res sig) as [[]|]; auto. Qed. (** The result locations are caller-save registers *) Lemma loc_result_caller_save: - forall (s: signature) (r: mreg), - In r (loc_result s) -> is_callee_save r = false. + forall (s: signature), + forall_rpair (fun r => is_callee_save r = false) (loc_result s). Proof. intros. - assert (r = R0 \/ r = R1 \/ r = F0). - unfold loc_result in H. destruct (sig_res s); [destruct t|idtac]; simpl in H; intuition. - destruct H0 as [A | [A | A]]; subst r; auto. + unfold loc_result. destruct (sig_res s) as [[]|]; simpl; auto. +Qed. + +(** If the result is in a pair of registers, those registers are distinct and have type [Tint] at least. *) + +Lemma loc_result_pair: + forall sg, + match loc_result sg with + | One _ => True + | Twolong r1 r2 => r1 <> r2 /\ sg.(sig_res) = Some Tlong /\ subtype Tint (mreg_type r1) = true /\ subtype Tint (mreg_type r2) = true + end. +Proof. + intros; unfold loc_result; destruct (sig_res sg) as [[]|]; auto. intuition congruence. Qed. (** ** Location of function arguments *) @@ -149,28 +159,28 @@ Definition freg_param (n: Z) : mreg := match list_nth_z float_param_regs n with Some r => r | None => F0 end. Fixpoint loc_arguments_hf - (tyl: list typ) (ir fr ofs: Z) {struct tyl} : list loc := + (tyl: list typ) (ir fr ofs: Z) {struct tyl} : list (rpair loc) := match tyl with | nil => nil | (Tint | Tany32) as ty :: tys => if zlt ir 4 - then R (ireg_param ir) :: loc_arguments_hf tys (ir + 1) fr ofs - else S Outgoing ofs ty :: loc_arguments_hf tys ir fr (ofs + 1) + then One (R (ireg_param ir)) :: loc_arguments_hf tys (ir + 1) fr ofs + else One (S Outgoing ofs ty) :: loc_arguments_hf tys ir fr (ofs + 1) | (Tfloat | Tany64) as ty :: tys => if zlt fr 8 - then R (freg_param fr) :: loc_arguments_hf tys ir (fr + 1) ofs + then One (R (freg_param fr)) :: loc_arguments_hf tys ir (fr + 1) ofs else let ofs := align ofs 2 in - S Outgoing ofs ty :: loc_arguments_hf tys ir fr (ofs + 2) + One (S Outgoing ofs ty) :: loc_arguments_hf tys ir fr (ofs + 2) | Tsingle :: tys => if zlt fr 8 - then R (freg_param fr) :: loc_arguments_hf tys ir (fr + 1) ofs - else S Outgoing ofs Tsingle :: loc_arguments_hf tys ir fr (ofs + 1) + then One (R (freg_param fr)) :: loc_arguments_hf tys ir (fr + 1) ofs + else One (S Outgoing ofs Tsingle) :: loc_arguments_hf tys ir fr (ofs + 1) | Tlong :: tys => let ir := align ir 2 in if zlt ir 4 - then R (ireg_param (ir + 1)) :: R (ireg_param ir) :: loc_arguments_hf tys (ir + 2) fr ofs + then Twolong (R (ireg_param (ir + 1))) (R (ireg_param ir)) :: loc_arguments_hf tys (ir + 2) fr ofs else let ofs := align ofs 2 in - S Outgoing (ofs + 1) Tint :: S Outgoing ofs Tint :: loc_arguments_hf tys ir fr (ofs + 2) + Twolong (S Outgoing (ofs + 1) Tint) (S Outgoing ofs Tint) :: loc_arguments_hf tys ir fr (ofs + 2) end. (** For the "softfloat" configuration, as well as for variable-argument functions @@ -194,30 +204,30 @@ we insert additional code around function calls and returns that moves data appropriately. *) Fixpoint loc_arguments_sf - (tyl: list typ) (ofs: Z) {struct tyl} : list loc := + (tyl: list typ) (ofs: Z) {struct tyl} : list (rpair loc) := match tyl with | nil => nil | (Tint|Tany32) as ty :: tys => - (if zlt ofs 0 then R (ireg_param (ofs + 4)) else S Outgoing ofs ty) + One (if zlt ofs 0 then R (ireg_param (ofs + 4)) else S Outgoing ofs ty) :: loc_arguments_sf tys (ofs + 1) | (Tfloat|Tany64) as ty :: tys => let ofs := align ofs 2 in - (if zlt ofs 0 then R (freg_param (ofs + 4)) else S Outgoing ofs ty) + One (if zlt ofs 0 then R (freg_param (ofs + 4)) else S Outgoing ofs ty) :: loc_arguments_sf tys (ofs + 2) | Tsingle :: tys => - (if zlt ofs 0 then R (freg_param (ofs + 4)) else S Outgoing ofs Tsingle) + One (if zlt ofs 0 then R (freg_param (ofs + 4)) else S Outgoing ofs Tsingle) :: loc_arguments_sf tys (ofs + 1) | Tlong :: tys => let ofs := align ofs 2 in - (if zlt ofs 0 then R (ireg_param (ofs+1+4)) else S Outgoing (ofs+1) Tint) - :: (if zlt ofs 0 then R (ireg_param (ofs+4)) else S Outgoing ofs Tint) + Twolong (if zlt ofs 0 then R (ireg_param (ofs+1+4)) else S Outgoing (ofs+1) Tint) + (if zlt ofs 0 then R (ireg_param (ofs+4)) else S Outgoing ofs Tint) :: loc_arguments_sf tys (ofs + 2) 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 loc := +Definition loc_arguments (s: signature) : list (rpair loc) := match Archi.abi with | Archi.Softfloat => loc_arguments_sf s.(sig_args) (-4) @@ -279,185 +289,151 @@ Definition loc_argument_acceptable (l: loc) : Prop := | _ => False end. -Remark ireg_param_in_params: forall n, In (ireg_param n) int_param_regs. +Definition loc_argument_charact (ofs: Z) (l: loc) : Prop := + match l with + | R r => is_callee_save r = false + | S Outgoing ofs' ty => ofs' >= ofs /\ typealign ty = 1 + | _ => False + end. + +Remark ireg_param_caller_save: forall n, is_callee_save (ireg_param n) = false. Proof. unfold ireg_param; intros. + assert (A: forall r, In r int_param_regs -> is_callee_save r = false) by decide_goal. destruct (list_nth_z int_param_regs n) as [r|] eqn:NTH. - eapply list_nth_z_in; eauto. - simpl; auto. + apply A. eapply list_nth_z_in; eauto. + auto. Qed. -Remark freg_param_in_params: forall n, In (freg_param n) float_param_regs. +Remark freg_param_caller_save: forall n, is_callee_save (freg_param n) = false. Proof. unfold freg_param; intros. + assert (A: forall r, In r float_param_regs -> is_callee_save r = false) by decide_goal. destruct (list_nth_z float_param_regs n) as [r|] eqn:NTH. - eapply list_nth_z_in; eauto. - simpl; auto. + apply A. eapply list_nth_z_in; eauto. + auto. Qed. Remark loc_arguments_hf_charact: - forall tyl ir fr ofs l, - In l (loc_arguments_hf tyl ir fr ofs) -> - match l with - | R r => In r int_param_regs \/ In r float_param_regs - | S Outgoing ofs' ty => ofs' >= ofs /\ typealign ty = 1 - | S _ _ _ => False - end. + forall tyl ir fr ofs p, + In p (loc_arguments_hf tyl ir fr ofs) -> forall_rpair (loc_argument_charact ofs) p. Proof. - assert (INCR: forall l ofs1 ofs2, - match l with - | R r => In r int_param_regs \/ In r float_param_regs - | S Outgoing ofs' ty => ofs' >= ofs2 /\ typealign ty = 1 - | S _ _ _ => False - end -> - ofs1 <= ofs2 -> - match l with - | R r => In r int_param_regs \/ In r float_param_regs - | S Outgoing ofs' ty => ofs' >= ofs1 /\ typealign ty = 1 - | S _ _ _ => False - end). - { - intros. destruct l; auto. destruct sl; auto. intuition omega. - } + assert (X: forall ofs1 ofs2 l, loc_argument_charact ofs2 l -> ofs1 <= ofs2 -> loc_argument_charact ofs1 l). + { destruct l; simpl; intros; auto. destruct sl; auto. intuition omega. } + assert (Y: forall ofs1 ofs2 p, forall_rpair (loc_argument_charact ofs2) p -> ofs1 <= ofs2 -> forall_rpair (loc_argument_charact ofs1) p). + { destruct p; simpl; intuition eauto. } induction tyl; simpl loc_arguments_hf; intros. elim H. destruct a. - (* int *) destruct (zlt ir 4); destruct H. - subst. left; apply ireg_param_in_params. + subst. apply ireg_param_caller_save. eapply IHtyl; eauto. subst. split; [omega | auto]. - eapply INCR. eapply IHtyl; eauto. omega. + eapply Y; eauto. omega. - (* float *) destruct (zlt fr 8); destruct H. - subst. right; apply freg_param_in_params. + subst. apply freg_param_caller_save. eapply IHtyl; eauto. subst. split. apply Zle_ge. apply align_le. omega. auto. - eapply INCR. eapply IHtyl; eauto. - apply Zle_trans with (align ofs 2). apply align_le; omega. omega. + eapply Y; eauto. apply Zle_trans with (align ofs 2). apply align_le; omega. omega. - (* long *) set (ir' := align ir 2) in *. assert (ofs <= align ofs 2) by (apply align_le; omega). destruct (zlt ir' 4). - destruct H. subst l; left; apply ireg_param_in_params. - destruct H. subst l; left; apply ireg_param_in_params. + destruct H. subst p. split; apply ireg_param_caller_save. eapply IHtyl; eauto. - destruct H. subst l; split; [ omega | auto ]. - destruct H. subst l; split; [ omega | auto ]. - eapply INCR. eapply IHtyl; eauto. omega. + destruct H. subst p. split; (split; [ omega | auto ]). + eapply Y. eapply IHtyl; eauto. omega. - (* single *) destruct (zlt fr 8); destruct H. - subst. right; apply freg_param_in_params. + subst. apply freg_param_caller_save. eapply IHtyl; eauto. - subst. split; [omega | auto]. - eapply INCR. eapply IHtyl; eauto. omega. + subst. split; [omega|auto]. + eapply Y; eauto. omega. - (* any32 *) destruct (zlt ir 4); destruct H. - subst. left; apply ireg_param_in_params. + subst. apply ireg_param_caller_save. eapply IHtyl; eauto. subst. split; [omega | auto]. - eapply INCR. eapply IHtyl; eauto. omega. + eapply Y; eauto. omega. - (* any64 *) destruct (zlt fr 8); destruct H. - subst. right; apply freg_param_in_params. + subst. apply freg_param_caller_save. eapply IHtyl; eauto. subst. split. apply Zle_ge. apply align_le. omega. auto. - eapply INCR. eapply IHtyl; eauto. - apply Zle_trans with (align ofs 2). apply align_le; omega. omega. + eapply Y; eauto. apply Zle_trans with (align ofs 2). apply align_le; omega. omega. Qed. Remark loc_arguments_sf_charact: - forall tyl ofs l, - In l (loc_arguments_sf tyl ofs) -> - match l with - | R r => In r int_param_regs \/ In r float_param_regs - | S Outgoing ofs' ty => ofs' >= Zmax 0 ofs /\ typealign ty = 1 - | S _ _ _ => False - end. + forall tyl ofs p, + In p (loc_arguments_sf tyl ofs) -> forall_rpair (loc_argument_charact (Zmax 0 ofs)) p. Proof. - assert (INCR: forall l ofs1 ofs2, - match l with - | R r => In r int_param_regs \/ In r float_param_regs - | S Outgoing ofs' ty => ofs' >= Zmax 0 ofs2 /\ typealign ty = 1 - | S _ _ _ => False - end -> - ofs1 <= ofs2 -> - match l with - | R r => In r int_param_regs \/ In r float_param_regs - | S Outgoing ofs' ty => ofs' >= Zmax 0 ofs1 /\ typealign ty = 1 - | S _ _ _ => False - end). - { - intros. destruct l; auto. destruct sl; auto. intuition xomega. - } + assert (X: forall ofs1 ofs2 l, loc_argument_charact (Zmax 0 ofs2) l -> ofs1 <= ofs2 -> loc_argument_charact (Zmax 0 ofs1) l). + { destruct l; simpl; intros; auto. destruct sl; auto. intuition xomega. } + assert (Y: forall ofs1 ofs2 p, forall_rpair (loc_argument_charact (Zmax 0 ofs2)) p -> ofs1 <= ofs2 -> forall_rpair (loc_argument_charact (Zmax 0 ofs1)) p). + { destruct p; simpl; intuition eauto. } induction tyl; simpl loc_arguments_sf; intros. elim H. destruct a. - (* int *) destruct H. - destruct (zlt ofs 0); subst l. - left; apply ireg_param_in_params. - split. xomega. auto. - eapply INCR. eapply IHtyl; eauto. omega. + destruct (zlt ofs 0); subst p. + apply ireg_param_caller_save. + split; [xomega|auto]. + eapply Y; eauto. omega. - (* float *) set (ofs' := align ofs 2) in *. assert (ofs <= ofs') by (apply align_le; omega). destruct H. - destruct (zlt ofs' 0); subst l. - right; apply freg_param_in_params. - split. xomega. auto. - eapply INCR. eapply IHtyl; eauto. omega. + destruct (zlt ofs' 0); subst p. + apply freg_param_caller_save. + split; [xomega|auto]. + eapply Y. eapply IHtyl; eauto. omega. - (* long *) set (ofs' := align ofs 2) in *. assert (ofs <= ofs') by (apply align_le; omega). destruct H. - destruct (zlt ofs' 0); subst l. - left; apply ireg_param_in_params. - split. xomega. auto. - destruct H. - destruct (zlt ofs' 0); subst l. - left; apply ireg_param_in_params. - split. xomega. auto. - eapply INCR. eapply IHtyl; eauto. omega. + destruct (zlt ofs' 0); subst p. + split; apply ireg_param_caller_save. + split; (split; [xomega|auto]). + eapply Y. eapply IHtyl; eauto. omega. - (* single *) destruct H. - destruct (zlt ofs 0); subst l. - right; apply freg_param_in_params. - split. xomega. auto. - eapply INCR. eapply IHtyl; eauto. omega. + destruct (zlt ofs 0); subst p. + apply freg_param_caller_save. + split; [xomega|auto]. + eapply Y; eauto. omega. - (* any32 *) destruct H. - destruct (zlt ofs 0); subst l. - left; apply ireg_param_in_params. - split. xomega. auto. - eapply INCR. eapply IHtyl; eauto. omega. + destruct (zlt ofs 0); subst p. + apply ireg_param_caller_save. + split; [xomega|auto]. + eapply Y; eauto. omega. - (* any64 *) set (ofs' := align ofs 2) in *. assert (ofs <= ofs') by (apply align_le; omega). destruct H. - destruct (zlt ofs' 0); subst l. - right; apply freg_param_in_params. - split. xomega. auto. - eapply INCR. eapply IHtyl; eauto. omega. + destruct (zlt ofs' 0); subst p. + apply freg_param_caller_save. + split; [xomega|auto]. + eapply Y. eapply IHtyl; eauto. omega. Qed. Lemma loc_arguments_acceptable: - forall (s: signature) (l: loc), - In l (loc_arguments s) -> loc_argument_acceptable l. + forall (s: signature) (p: rpair loc), + In p (loc_arguments s) -> forall_rpair loc_argument_acceptable p. Proof. unfold loc_arguments; intros. - assert (A: forall r, In r int_param_regs -> is_callee_save r = false) by decide_goal. - assert (B: forall r, In r float_param_regs -> is_callee_save r = false) by decide_goal. - assert (C: forall r, In r int_param_regs \/ In r float_param_regs -> is_callee_save r = false). - { intros. destruct H0; auto. } - assert (In l (loc_arguments_sf (sig_args s) (-4)) -> loc_argument_acceptable l). - { intros. red. exploit loc_arguments_sf_charact; eauto. - destruct l as [r | [] ofs ty]; auto. - intros [P Q]. rewrite Q; split. auto. apply Z.divide_1_l. } - assert (In l (loc_arguments_hf (sig_args s) 0 0 0) -> loc_argument_acceptable l). - { intros. red. exploit loc_arguments_hf_charact; eauto. - destruct l as [r | [] ofs ty]; auto. - intros [P Q]. rewrite Q; split. auto. apply Z.divide_1_l. } + assert (X: forall l, loc_argument_charact 0 l -> loc_argument_acceptable l). + { unfold loc_argument_charact, loc_argument_acceptable. + destruct l as [r | [] ofs ty]; auto. intros (A & B); split; auto. rewrite B; apply Z.divide_1_l. } + assert (Y: forall p, forall_rpair (loc_argument_charact 0) p -> forall_rpair loc_argument_acceptable p). + { destruct p0; simpl; intuition auto. } + assert (In p (loc_arguments_sf (sig_args s) (-4)) -> forall_rpair loc_argument_acceptable p). + { intros. exploit loc_arguments_sf_charact; eauto. } + assert (In p (loc_arguments_hf (sig_args s) 0 0 0) -> forall_rpair loc_argument_acceptable p). + { intros. exploit loc_arguments_hf_charact; eauto. } destruct Archi.abi; [ | destruct (cc_vararg (sig_cc s)) ]; auto. Qed. @@ -516,7 +492,7 @@ Qed. Lemma loc_arguments_hf_bounded: forall ofs ty tyl ir fr ofs0, - In (S Outgoing ofs ty) (loc_arguments_hf tyl ir fr ofs0) -> + In (S Outgoing ofs ty) (regs_of_rpairs (loc_arguments_hf tyl ir fr ofs0)) -> ofs + typesize ty <= size_arguments_hf tyl ir fr ofs0. Proof. induction tyl; simpl; intros. @@ -564,7 +540,7 @@ Qed. Lemma loc_arguments_sf_bounded: forall ofs ty tyl ofs0, - In (S Outgoing ofs ty) (loc_arguments_sf tyl ofs0) -> + In (S Outgoing ofs ty) (regs_of_rpairs (loc_arguments_sf tyl ofs0)) -> Zmax 0 (ofs + typesize ty) <= size_arguments_sf tyl ofs0. Proof. induction tyl; simpl; intros. @@ -602,14 +578,14 @@ Qed. Lemma loc_arguments_bounded: forall (s: signature) (ofs: Z) (ty: typ), - In (S Outgoing ofs ty) (loc_arguments s) -> + In (S Outgoing ofs ty) (regs_of_rpairs (loc_arguments s)) -> ofs + typesize ty <= size_arguments s. Proof. unfold loc_arguments, size_arguments; intros. - assert (In (S Outgoing ofs ty) (loc_arguments_sf (sig_args s) (-4)) -> + assert (In (S Outgoing ofs ty) (regs_of_rpairs (loc_arguments_sf (sig_args s) (-4))) -> ofs + typesize ty <= size_arguments_sf (sig_args s) (-4)). { intros. eapply Zle_trans. 2: eapply loc_arguments_sf_bounded; eauto. xomega. } - assert (In (S Outgoing ofs ty) (loc_arguments_hf (sig_args s) 0 0 0) -> + assert (In (S Outgoing ofs ty) (regs_of_rpairs (loc_arguments_hf (sig_args s) 0 0 0)) -> ofs + typesize ty <= size_arguments_hf (sig_args s) 0 0 0). { intros. eapply loc_arguments_hf_bounded; eauto. } destruct Archi.abi; [ | destruct (cc_vararg (sig_cc s)) ]; eauto. -- cgit