diff options
Diffstat (limited to 'arm/linux/Conventions1.v')
| -rw-r--r-- | arm/linux/Conventions1.v | 391 |
1 files changed, 148 insertions, 243 deletions
diff --git a/arm/linux/Conventions1.v b/arm/linux/Conventions1.v index fdccf75..842ccbf 100644 --- a/arm/linux/Conventions1.v +++ b/arm/linux/Conventions1.v @@ -35,13 +35,13 @@ Definition int_caller_save_regs := R0 :: R1 :: R2 :: R3 :: nil. Definition float_caller_save_regs := - F0 :: F1 :: nil. + F0 :: F1 :: F2 :: F3 :: F4 :: F5 :: nil. Definition int_callee_save_regs := R4 :: R5 :: R6 :: R7 :: R8 :: R9 :: R11 :: nil. Definition float_callee_save_regs := - F4 :: F5 :: F6 :: F7 :: nil. + F8 :: F9 :: F10 :: F11 :: F12 :: F13 :: F14 :: F15 :: nil. Definition destroyed_at_call_regs := int_caller_save_regs ++ float_caller_save_regs. @@ -73,7 +73,8 @@ Definition index_int_callee_save (r: mreg) := Definition index_float_callee_save (r: mreg) := match r with - | F4 => 0 | F5 => 1 | F6 => 2 | F7 => 3 + | F8 => 0 | F9 => 1 | F10 => 2 | F11 => 3 + | F12 => 4 | F13 => 5 | F14 => 6 | F15 => 7 | _ => -1 end. @@ -240,9 +241,13 @@ Qed. proved in this section (such as no overlapping between the locations 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 PowerPC compiler, we - implement the standard conventions defined in the PowerPC application - binary interface. *) + compiler with libraries compiled by another ARM EABI compiler, we + implement *almost* the standard conventions defined in the ARM EABI application + binary interface, with two exceptions: +- Double-precision arguments and results are passed in VFP double registers + instead of pairs of integer registers. +- Single-precision arguments and results are passed as double-precision floats. +*) (** ** Location of function result *) @@ -284,92 +289,59 @@ Qed. (** ** Location of function arguments *) -(** We use the following calling conventions, adapted from the ARM ABI: +(** We use the following calling conventions, adapted from the ARM EABI: - The first 4 integer arguments are passed in registers [R0] to [R3]. - The first 2 float arguments are passed in registers [F0] and [F1]. -- Each float argument passed in a float register ``consumes'' two - integer arguments. +- Each float argument passed in a float register ``consumes'' an aligned pair + of two integer registers. - Extra arguments are passed on the stack, in [Outgoing] slots, consecutively assigned (1 word for an integer argument, 2 words for a float), starting at word offset 0. - -These conventions are somewhat baroque, but they are mandated by the ABI. *) -Fixpoint loc_arguments_rec - (tyl: list typ) (iregl: list mreg) (fregl: list mreg) - (ofs: Z) {struct tyl} : list loc := +Function ireg_param (n: Z) : mreg := + if zeq n (-4) then R0 + else if zeq n (-3) then R1 + else if zeq n (-2) then R2 + else if zeq n (-1) then R3 + else R4. (**r should not happen *) + +Function freg_param (n: Z) : mreg := + if zeq n (-4) then F0 + else if zeq n (-3) then F1 + else if zeq n (-2) then F1 + else F2. (**r should not happen *) + + +Fixpoint loc_arguments_rec (tyl: list typ) (ofs: Z) {struct tyl} : list loc := match tyl with | nil => nil | Tint :: tys => - match iregl with - | nil => - S (Outgoing ofs Tint) :: loc_arguments_rec tys nil fregl (ofs + 1) - | ireg :: iregs => - R ireg :: loc_arguments_rec tys iregs fregl ofs - end + (if zle 0 ofs then S (Outgoing ofs Tint) else R (ireg_param ofs)) + :: loc_arguments_rec tys (ofs + 1) | Tfloat :: tys => - match fregl with - | nil => - S (Outgoing ofs Tfloat) :: - loc_arguments_rec tys iregl nil (ofs + 2) - | freg :: fregs => - match iregl with - | nil => - S (Outgoing ofs Tfloat) :: - loc_arguments_rec tys nil fregl (ofs + 2) - | ireg :: nil => - R freg :: - loc_arguments_rec tys nil fregs (ofs + 1) - | ireg1 :: ireg2 :: iregs => - R freg :: - loc_arguments_rec tys iregs fregs ofs - end - end + (if zle (-1) ofs then S (Outgoing (align ofs 2) Tfloat) else R (freg_param ofs)) + :: loc_arguments_rec tys (align ofs 2 + 2) end. -Definition int_param_regs := - R0 :: R1 :: R2 :: R3 :: nil. -Definition float_param_regs := - F0 :: F1 :: nil. - (** [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 := - loc_arguments_rec s.(sig_args) int_param_regs float_param_regs 0. + loc_arguments_rec s.(sig_args) (-4). (** [size_arguments s] returns the number of [Outgoing] slots used to call a function with signature [s]. *) -Fixpoint size_arguments_rec - (tyl: list typ) (iregl: list mreg) (fregl: list mreg) - (ofs: Z) {struct tyl} : Z := +Fixpoint size_arguments_rec (tyl: list typ) (ofs: Z) {struct tyl} : Z := match tyl with | nil => ofs - | Tint :: tys => - match iregl with - | nil => size_arguments_rec tys nil fregl (ofs + 1) - | ireg :: iregs => size_arguments_rec tys iregs fregl ofs - end - | Tfloat :: tys => - match fregl with - | nil => - size_arguments_rec tys iregl nil (ofs + 2) - | freg :: fregs => - match iregl with - | nil => - size_arguments_rec tys nil fregl (ofs + 2) - | ireg :: nil => - size_arguments_rec tys nil fregs (ofs + 1) - | ireg1 :: ireg2 :: iregs => - size_arguments_rec tys iregs fregs ofs - end - end + | Tint :: tys => size_arguments_rec tys (ofs + 1) + | Tfloat :: tys => size_arguments_rec tys (align ofs 2 + 2) end. Definition size_arguments (s: signature) : Z := - size_arguments_rec s.(sig_args) int_param_regs float_param_regs 0. + Zmax 0 (size_arguments_rec s.(sig_args) (-4)). (** Argument locations are either non-temporary registers or [Outgoing] stack slots at nonnegative offsets. *) @@ -381,172 +353,122 @@ Definition loc_argument_acceptable (l: loc) : Prop := | _ => False end. +Lemma align_monotone: + forall x1 x2 y, y > 0 -> x1 <= x2 -> align x1 y <= align x2 y. +Proof. + intros. unfold align. apply Zmult_le_compat_r. apply Z_div_le. + omega. omega. omega. +Qed. + Remark loc_arguments_rec_charact: - forall tyl iregl fregl ofs l, - In l (loc_arguments_rec tyl iregl fregl ofs) -> + forall tyl ofs l, + In l (loc_arguments_rec tyl ofs) -> match l with - | R r => In r iregl \/ In r fregl - | S (Outgoing ofs' ty) => ofs' >= ofs + | R r => + (exists n, ofs <= n < 0 /\ r = ireg_param n) + \/ (exists n, ofs <= n < -1 /\ r = freg_param n) + | S (Outgoing ofs' ty) => ofs' >= 0 /\ ofs' >= ofs | S _ => False end. Proof. induction tyl; simpl loc_arguments_rec; intros. elim H. - destruct a. - destruct iregl; elim H; intro. - subst l. omega. - generalize (IHtyl _ _ _ _ H0). destruct l; auto. destruct s; auto. omega. - subst l. auto with coqlib. - generalize (IHtyl _ _ _ _ H0). destruct l; auto. simpl; intuition. - destruct fregl. - elim H; intro. - subst l. omega. - generalize (IHtyl _ _ _ _ H0). destruct l; auto. destruct s; auto. omega. - destruct iregl. - elim H; intro. - subst l. omega. - generalize (IHtyl _ _ _ _ H0). destruct l; auto. destruct s; auto. omega. - destruct iregl. - elim H; intro. - subst l. auto with coqlib. - generalize (IHtyl _ _ _ _ H0). destruct l; auto. - intros [A|B]. elim A. auto with coqlib. - destruct s; auto. omega. - elim H; intro. - subst l. auto with coqlib. - generalize (IHtyl _ _ _ _ H0). destruct l; auto. - intros [A|B]; auto with coqlib. + destruct a; elim H; intro. + subst l. destruct (zle 0 ofs). omega. + left. exists ofs; split; auto; omega. + generalize (IHtyl _ _ H0). + destruct l. intros [[n A] | [n A]]; [left|right]; exists n; intuition omega. + destruct s; auto; omega. + subst l. destruct (zle (-1) ofs). + split. apply Zle_ge. change 0 with (align (-1) 2). apply align_monotone; omega. + apply Zle_ge. apply align_le. omega. + right. exists ofs. intuition. + assert (ofs <= align ofs 2) by (apply align_le; omega). + generalize (IHtyl _ _ H0). + destruct l. intros [[n A] | [n A]]; [left|right]; exists n; intuition omega. + destruct s; auto; omega. Qed. -Lemma loc_arguments_acceptable: - forall (s: signature) (r: loc), - In r (loc_arguments s) -> loc_argument_acceptable r. -Proof. - unfold loc_arguments; intros. - generalize (loc_arguments_rec_charact _ _ _ _ _ H). - destruct r. - intro H0; elim H0. simpl. unfold not. ElimOrEq; NotOrEq. - simpl. unfold not. ElimOrEq; NotOrEq. - destruct s0; try contradiction. - simpl. omega. -Qed. -Hint Resolve loc_arguments_acceptable: locs. - -(** Arguments are parwise disjoint (in the sense of [Loc.norepet]). *) - -Remark loc_arguments_rec_notin_reg: - forall tyl iregl fregl ofs r, - ~(In r iregl) -> ~(In r fregl) -> - Loc.notin (R r) (loc_arguments_rec tyl iregl fregl ofs). +Lemma loc_notin_in_diff: + forall l ll, + Loc.notin l ll <-> (forall l', In l' ll -> Loc.diff l l'). Proof. - induction tyl; simpl; intros. - auto. - destruct a. - destruct iregl; simpl. auto. - simpl in H. split. apply sym_not_equal. tauto. - apply IHtyl. tauto. tauto. - destruct fregl; simpl. auto. simpl in H0. - destruct iregl; simpl. auto. - destruct iregl; simpl. - split. apply sym_not_equal. tauto. apply IHtyl. hnf. tauto. tauto. - split. apply sym_not_equal. tauto. apply IHtyl. - red; intro. apply H. auto with coqlib. tauto. + induction ll; simpl; intuition. subst l'. auto. Qed. - + Remark loc_arguments_rec_notin_local: - forall tyl iregl fregl ofs ofs0 ty0, - Loc.notin (S (Local ofs0 ty0)) (loc_arguments_rec tyl iregl fregl ofs). + forall tyl ofs ofs0 ty0, + Loc.notin (S (Local ofs0 ty0)) (loc_arguments_rec tyl ofs). Proof. - induction tyl; simpl; intros. - auto. - destruct a. - destruct iregl; simpl; auto. - destruct fregl; simpl; auto. - destruct iregl; simpl; auto. - destruct iregl; simpl; auto. + intros. rewrite loc_notin_in_diff. intros. + exploit loc_arguments_rec_charact; eauto. + destruct l'; intros; simpl; auto. destruct s; auto; contradiction. Qed. -Remark loc_arguments_rec_notin_outgoing: - forall tyl iregl fregl ofs ofs0 ty0, - ofs0 + typesize ty0 <= ofs -> - Loc.notin (S (Outgoing ofs0 ty0)) (loc_arguments_rec tyl iregl fregl ofs). +Lemma loc_arguments_acceptable: + forall (s: signature) (r: loc), + In r (loc_arguments s) -> loc_argument_acceptable r. Proof. - induction tyl; simpl; intros. - auto. - destruct a. - destruct iregl; simpl. - split. omega. eapply IHtyl. omega. - auto. - destruct fregl; simpl. - split. omega. eapply IHtyl. omega. - destruct iregl; simpl. - split. omega. eapply IHtyl. omega. - destruct iregl; simpl. - split; auto. eapply IHtyl. omega. - split; auto. + unfold loc_arguments; intros. + generalize (loc_arguments_rec_charact _ _ _ H). + destruct r; simpl. + intros [[n [A B]] | [n [A B]]]; subst m. + functional induction (ireg_param n); intuition congruence. + functional induction (freg_param n); intuition congruence. + destruct s0; tauto. Qed. +Hint Resolve loc_arguments_acceptable: locs. + +(** Arguments are parwise disjoint (in the sense of [Loc.norepet]). *) Lemma loc_arguments_norepet: forall (s: signature), Loc.norepet (loc_arguments s). Proof. - assert (forall tyl iregl fregl ofs, - list_norepet iregl -> - list_norepet fregl -> - list_disjoint iregl fregl -> - Loc.norepet (loc_arguments_rec tyl iregl fregl ofs)). - induction tyl; simpl; intros. - constructor. - destruct a. - destruct iregl; constructor. - apply loc_arguments_rec_notin_outgoing. simpl; omega. auto. - apply loc_arguments_rec_notin_reg. inversion H. auto. - apply list_disjoint_notin with (m :: iregl); auto with coqlib. - apply IHtyl. inv H; auto. auto. - eapply list_disjoint_cons_left; eauto. - - destruct fregl. constructor. - apply loc_arguments_rec_notin_outgoing. simpl; omega. auto. - destruct iregl. constructor. - apply loc_arguments_rec_notin_outgoing. simpl; omega. auto. - destruct iregl; constructor. - apply loc_arguments_rec_notin_reg. - red; intro. apply (H1 m m). auto with coqlib. auto with coqlib. auto. - inv H0; auto. - apply IHtyl. constructor. inv H0; auto. - red; intros. elim H2. - apply loc_arguments_rec_notin_reg. - red; intros. elim (H1 m m); auto with coqlib. - inv H0; auto. - apply IHtyl. inv H. inv H5. auto. inv H0; auto. - red; intros. apply H1; auto with coqlib. - - intro. unfold loc_arguments. apply H. - unfold int_param_regs. NoRepet. - unfold float_param_regs. NoRepet. - red; intros x y; simpl. ElimOrEq; ElimOrEq; discriminate. + unfold loc_arguments; intros. + assert (forall tyl ofs, -4 <= ofs -> Loc.norepet (loc_arguments_rec tyl ofs)). + induction tyl; simpl; intros. + constructor. + destruct a; constructor. + rewrite loc_notin_in_diff. intros. exploit loc_arguments_rec_charact; eauto. + destruct (zle 0 ofs); destruct l'; simpl; auto. + destruct s0; intuition. + intros [[n [A B]] | [n [A B]]]; subst m. + functional induction (ireg_param ofs); functional induction (ireg_param n); congruence || omegaContradiction. + functional induction (ireg_param ofs); functional induction (freg_param n); congruence || omegaContradiction. + apply IHtyl. omega. + rewrite loc_notin_in_diff. intros. exploit loc_arguments_rec_charact; eauto. + destruct (zle (-1) ofs); destruct l'; simpl; auto. + destruct s0; intuition. + intros [[n [A B]] | [n [A B]]]; subst m. + functional induction (freg_param ofs); functional induction (ireg_param n); congruence || omegaContradiction. + functional induction (freg_param ofs); functional induction (freg_param n); try (congruence || omegaContradiction). + compute in A. intuition. + compute in A. intuition. + compute in A. intuition. + compute in A. intuition. + compute in A. intuition. + apply IHtyl. assert (ofs <= align ofs 2) by (apply align_le; omega). omega. + apply H. omega. Qed. (** The offsets of [Outgoing] arguments are below [size_arguments s]. *) Remark size_arguments_rec_above: - forall tyl iregl fregl ofs0, - ofs0 <= size_arguments_rec tyl iregl fregl ofs0. + forall tyl ofs, + ofs <= size_arguments_rec tyl ofs. Proof. induction tyl; simpl; intros. omega. destruct a. - destruct iregl. apply Zle_trans with (ofs0 + 1); auto; omega. auto. - destruct fregl. apply Zle_trans with (ofs0 + 2); auto; omega. - destruct iregl. apply Zle_trans with (ofs0 + 2); auto; omega. - destruct iregl. apply Zle_trans with (ofs0 + 1); auto; omega. - auto. + apply Zle_trans with (ofs + 1); auto; omega. + assert (ofs <= align ofs 2) by (apply align_le; omega). + apply Zle_trans with (align ofs 2 + 2); auto; omega. Qed. Lemma size_arguments_above: forall s, size_arguments s >= 0. Proof. - intros; unfold size_arguments. apply Zle_ge. - apply size_arguments_rec_above. + intros; unfold size_arguments. apply Zle_ge. apply Zmax1. Qed. Lemma loc_arguments_bounded: @@ -555,23 +477,24 @@ Lemma loc_arguments_bounded: ofs + typesize ty <= size_arguments s. Proof. intros. - assert (forall tyl iregl fregl ofs0, - In (S (Outgoing ofs ty)) (loc_arguments_rec tyl iregl fregl ofs0) -> - ofs + typesize ty <= size_arguments_rec tyl iregl fregl ofs0). + assert (forall tyl ofs0, + 0 <= ofs0 -> + ofs0 <= Zmax 0 (size_arguments_rec tyl ofs0)). + intros. generalize (size_arguments_rec_above tyl ofs0). intros. + rewrite Zmax_spec. rewrite zlt_false. auto. omega. + assert (forall tyl ofs0, + In (S (Outgoing ofs ty)) (loc_arguments_rec tyl ofs0) -> + ofs + typesize ty <= Zmax 0 (size_arguments_rec tyl ofs0)). induction tyl; simpl; intros. - elim H0. - destruct a. destruct iregl; elim H0; intro. - inv H1. simpl. apply size_arguments_rec_above. auto. - discriminate. auto. - destruct fregl. elim H0; intro. - inv H1. simpl. apply size_arguments_rec_above. auto. - destruct iregl. elim H0; intro. - inv H1. simpl. apply size_arguments_rec_above. auto. - destruct iregl. - elim H0; intro. inv H1. auto. - elim H0; intro. inv H1. auto. + elim H1. + destruct a; elim H1; intros. + destruct (zle 0 ofs0); inv H2. apply H0. omega. auto. + destruct (zle (-1) ofs0); inv H2. apply H0. + assert (align (-1) 2 <= align ofs0 2). apply align_monotone. omega. auto. + change (align (-1) 2) with 0 in H2. omega. + auto. - unfold size_arguments. eapply H0. unfold loc_arguments in H. eauto. + unfold size_arguments. apply H1. auto. Qed. (** Temporary registers do not overlap with argument locations. *) @@ -579,12 +502,10 @@ Qed. Lemma loc_arguments_not_temporaries: forall sig, Loc.disjoint (loc_arguments sig) temporaries. Proof. - intros; red; intros x1 x2 H. - generalize (loc_arguments_rec_charact _ _ _ _ _ H). - destruct x1. - intro H0; elim H0; simpl; (ElimOrEq; ElimOrEq; congruence). - destruct s; try contradiction. intro. - simpl; ElimOrEq; auto. + intros; red; intros x1 x2 A B. + exploit loc_arguments_acceptable; eauto. unfold loc_argument_acceptable. + destruct x1; intros. simpl. destruct x2; auto. intuition congruence. + destruct s; try contradiction. revert B. simpl. ElimOrEq; auto. Qed. Hint Resolve loc_arguments_not_temporaries: locs. @@ -595,9 +516,9 @@ Lemma arguments_caller_save: In (R r) (loc_arguments sig) -> In (R r) destroyed_at_call. Proof. unfold loc_arguments; intros. - elim (loc_arguments_rec_charact _ _ _ _ _ H); simpl. - ElimOrEq; intuition. - ElimOrEq; intuition. + destruct (loc_arguments_rec_charact _ _ _ H) as [[n [A B]] | [n [A B]]]; subst r. + functional induction (ireg_param n); simpl; auto. omegaContradiction. + functional induction (freg_param n); simpl; auto 10. Qed. (** Argument locations agree in number with the function signature. *) @@ -606,15 +527,10 @@ Lemma loc_arguments_length: forall sig, List.length (loc_arguments sig) = List.length sig.(sig_args). Proof. - assert (forall tyl iregl fregl ofs, - List.length (loc_arguments_rec tyl iregl fregl ofs) = List.length tyl). + assert (forall tyl ofs, List.length (loc_arguments_rec tyl ofs) = List.length tyl). induction tyl; simpl; intros. auto. - destruct a. - destruct iregl; simpl; decEq; auto. - destruct fregl; simpl; decEq; auto. - destruct iregl; simpl. decEq; auto. - destruct iregl; simpl; decEq; auto. + destruct a; simpl; decEq; auto. intros. unfold loc_arguments. auto. Qed. @@ -624,23 +540,12 @@ Qed. Lemma loc_arguments_type: forall sig, List.map Loc.type (loc_arguments sig) = sig.(sig_args). Proof. - assert (forall tyl iregl fregl ofs, - (forall r, In r iregl -> mreg_type r = Tint) -> - (forall r, In r fregl -> mreg_type r = Tfloat) -> - List.map Loc.type (loc_arguments_rec tyl iregl fregl ofs) = tyl). + assert (forall tyl ofs, List.map Loc.type (loc_arguments_rec tyl ofs) = tyl). induction tyl; simpl; intros. auto. - destruct a. - destruct iregl; simpl; f_equal; eauto with coqlib. - destruct fregl; simpl. - f_equal; eauto with coqlib. - destruct iregl; simpl. - f_equal; eauto with coqlib. - destruct iregl; simpl; f_equal; eauto with coqlib. - apply IHtyl. simpl; tauto. auto with coqlib. - apply IHtyl. auto with coqlib. auto with coqlib. + destruct a; simpl; decEq; auto. + destruct (zle 0 ofs). auto. functional induction (ireg_param ofs); auto. + destruct (zle (-1) ofs). auto. functional induction (freg_param ofs); auto. intros. unfold loc_arguments. apply H. - intro; simpl. ElimOrEq; reflexivity. - intro; simpl. ElimOrEq; reflexivity. Qed. |