From 255cee09b71255051c2b40eae0c88bffce1f6f32 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 20 Apr 2013 07:54:52 +0000 Subject: Big merge of the newregalloc-int64 branch. Lots of changes in two directions: 1- new register allocator (+ live range splitting, spilling&reloading, etc) based on a posteriori validation using the Rideau-Leroy algorithm 2- support for 64-bit integer arithmetic (type "long long"). git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2200 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/Locations.v | 401 +++++++++++++++++++++++++++++----------------------- 1 file changed, 223 insertions(+), 178 deletions(-) (limited to 'backend/Locations.v') diff --git a/backend/Locations.v b/backend/Locations.v index 2381fea0..2f2dae84 100644 --- a/backend/Locations.v +++ b/backend/Locations.v @@ -13,7 +13,10 @@ (** Locations are a refinement of RTL pseudo-registers, used to reflect the results of register allocation (file [Allocation]). *) +Require Import OrderedType. Require Import Coqlib. +Require Import Maps. +Require Import Ordered. Require Import AST. Require Import Values. Require Export Machregs. @@ -42,9 +45,9 @@ Require Export Machregs. calling conventions. *) Inductive slot: Type := - | Local: Z -> typ -> slot - | Incoming: Z -> typ -> slot - | Outgoing: Z -> typ -> slot. + | Local + | Incoming + | Outgoing. (** Morally, the [Incoming] slots of a function are the [Outgoing] slots of its caller function. @@ -56,46 +59,17 @@ as 32-bit integers/pointers (type [Tint]) or as 64-bit floats (type [Tfloat]). The offset of a slot, combined with its type and its kind, identifies uniquely the slot and will determine later where it resides within the memory-allocated activation record. Offsets are always positive. - -Conceptually, slots will be mapped to four non-overlapping memory areas -within activation records: -- The area for [Local] slots of type [Tint]. The offset is interpreted - as a 4-byte word index. -- The area for [Local] slots of type [Tfloat]. The offset is interpreted - as a 8-byte word index. Thus, two [Local] slots always refer either - to the same memory chunk (if they have the same types and offsets) - or to non-overlapping memory chunks (if the types or offsets differ). -- The area for [Outgoing] slots. The offset is a 4-byte word index. - Unlike [Local] slots, the PowerPC calling conventions demand that - integer and float [Outgoing] slots reside in the same memory area. - Therefore, [Outgoing Tint 0] and [Outgoing Tfloat 0] refer to - overlapping memory chunks and cannot be used simultaneously: one will - lose its value when the other is assigned. We will reflect this - overlapping behaviour in the environments mapping locations to values - defined later in this file. -- The area for [Incoming] slots. Same structure as the [Outgoing] slots. *) -Definition slot_type (s: slot): typ := - match s with - | Local ofs ty => ty - | Incoming ofs ty => ty - | Outgoing ofs ty => ty - end. - Lemma slot_eq: forall (p q: slot), {p = q} + {p <> q}. Proof. - assert (typ_eq: forall (t1 t2: typ), {t1 = t2} + {t1 <> t2}). - decide equality. - generalize zeq; intro. decide equality. Defined. -Global Opaque slot_eq. Open Scope Z_scope. Definition typesize (ty: typ) : Z := - match ty with Tint => 1 | Tfloat => 2 end. + match ty with Tint => 1 | Tlong => 2 | Tfloat => 2 end. Lemma typesize_pos: forall (ty: typ), typesize ty > 0. @@ -109,20 +83,24 @@ Qed. activation record slots. *) Inductive loc : Type := - | R: mreg -> loc - | S: slot -> loc. + | R (r: mreg) + | S (sl: slot) (pos: Z) (ty: typ). Module Loc. Definition type (l: loc) : typ := match l with | R r => mreg_type r - | S s => slot_type s + | S sl pos ty => ty end. Lemma eq: forall (p q: loc), {p = q} + {p <> q}. Proof. - decide equality. apply mreg_eq. apply slot_eq. + decide equality. + apply mreg_eq. + apply typ_eq. + apply zeq. + apply slot_eq. Defined. (** As mentioned previously, two locations can be different (in the sense @@ -138,13 +116,10 @@ Module Loc. *) Definition diff (l1 l2: loc) : Prop := match l1, l2 with - | R r1, R r2 => r1 <> r2 - | S (Local d1 t1), S (Local d2 t2) => - d1 <> d2 \/ t1 <> t2 - | S (Incoming d1 t1), S (Incoming d2 t2) => - d1 + typesize t1 <= d2 \/ d2 + typesize t2 <= d1 - | S (Outgoing d1 t1), S (Outgoing d2 t2) => - d1 + typesize t1 <= d2 \/ d2 + typesize t2 <= d1 + | R r1, R r2 => + r1 <> r2 + | S s1 d1 t1, S s2 d2 t2 => + s1 <> s2 \/ d1 + typesize t1 <= d2 \/ d2 + typesize t2 <= d1 | _, _ => True end. @@ -152,11 +127,8 @@ Module Loc. Lemma same_not_diff: forall l, ~(diff l l). Proof. - destruct l; unfold diff; try tauto. - destruct s. - tauto. - generalize (typesize_pos t); omega. - generalize (typesize_pos t); omega. + destruct l; unfold diff; auto. + red; intros. destruct H; auto. generalize (typesize_pos ty); omega. Qed. Lemma diff_not_eq: @@ -169,124 +141,22 @@ Module Loc. forall l1 l2, diff l1 l2 -> diff l2 l1. Proof. destruct l1; destruct l2; unfold diff; auto. - destruct s; auto. - destruct s; destruct s0; intuition auto. - Qed. - - Lemma diff_reg_right: - forall l r, l <> R r -> diff (R r) l. - Proof. - intros. simpl. destruct l. congruence. auto. - Qed. - - Lemma diff_reg_left: - forall l r, l <> R r -> diff l (R r). - Proof. - intros. apply diff_sym. apply diff_reg_right. auto. - Qed. - -(** [Loc.overlap l1 l2] returns [false] if [l1] and [l2] are different and - non-overlapping, and [true] otherwise: either [l1 = l2] or they partially - overlap. *) - - Definition overlap_aux (t1: typ) (d1 d2: Z) : bool := - if zeq d1 d2 then true else - match t1 with - | Tint => false - | Tfloat => if zeq (d1 + 1) d2 then true else false - end. - - Definition overlap (l1 l2: loc) : bool := - match l1, l2 with - | S (Incoming d1 t1), S (Incoming d2 t2) => - overlap_aux t1 d1 d2 || overlap_aux t2 d2 d1 - | S (Outgoing d1 t1), S (Outgoing d2 t2) => - overlap_aux t1 d1 d2 || overlap_aux t2 d2 d1 - | _, _ => false - end. - - Lemma overlap_aux_true_1: - forall d1 t1 d2 t2, - overlap_aux t1 d1 d2 = true -> - ~(d1 + typesize t1 <= d2 \/ d2 + typesize t2 <= d1). - Proof. - intros until t2. - generalize (typesize_pos t1); intro. - generalize (typesize_pos t2); intro. - unfold overlap_aux. - case (zeq d1 d2). - intros. omega. - case t1. intros; discriminate. - case (zeq (d1 + 1) d2); intros. - subst d2. simpl. omega. - discriminate. - Qed. - - Lemma overlap_aux_true_2: - forall d1 t1 d2 t2, - overlap_aux t2 d2 d1 = true -> - ~(d1 + typesize t1 <= d2 \/ d2 + typesize t2 <= d1). - Proof. - intros. generalize (overlap_aux_true_1 d2 t2 d1 t1 H). - tauto. + intuition. Qed. - Lemma overlap_not_diff: - forall l1 l2, overlap l1 l2 = true -> ~(diff l1 l2). + Definition diff_dec (l1 l2: loc) : { Loc.diff l1 l2 } + { ~Loc.diff l1 l2 }. Proof. - unfold overlap, diff; destruct l1; destruct l2; intros; try discriminate. - destruct s; discriminate. - destruct s; destruct s0; try discriminate. - elim (orb_true_elim _ _ H); intro. - apply overlap_aux_true_1; auto. - apply overlap_aux_true_2; auto. - elim (orb_true_elim _ _ H); intro. - apply overlap_aux_true_1; auto. - apply overlap_aux_true_2; auto. - Qed. - - Lemma overlap_aux_false_1: - forall t1 d1 t2 d2, - overlap_aux t1 d1 d2 || overlap_aux t2 d2 d1 = false -> - d1 + typesize t1 <= d2 \/ d2 + typesize t2 <= d1. - Proof. - intros until d2. intro OV. - generalize (orb_false_elim _ _ OV). intro OV'. elim OV'. - unfold overlap_aux. - case (zeq d1 d2); intro. - intros; discriminate. - case (zeq d2 d1); intro. - intros; discriminate. - case t1; case t2; simpl. - intros; omega. - case (zeq (d2 + 1) d1); intros. discriminate. omega. - case (zeq (d1 + 1) d2); intros. discriminate. omega. - case (zeq (d1 + 1) d2); intros H1 H2. discriminate. - case (zeq (d2 + 1) d1); intros. discriminate. omega. - Qed. - - Lemma non_overlap_diff: - forall l1 l2, l1 <> l2 -> overlap l1 l2 = false -> diff l1 l2. - Proof. - intros. unfold diff; destruct l1; destruct l2. - congruence. - auto. - destruct s; auto. - destruct s; destruct s0; auto. - case (zeq z z0); intro. - compare t t0; intro. - congruence. tauto. tauto. - apply overlap_aux_false_1. exact H0. - apply overlap_aux_false_1. exact H0. - Qed. - - Definition diff_dec (l1 l2: loc) : { Loc.diff l1 l2 } + {~Loc.diff l1 l2}. - Proof. - intros. case (eq l1 l2); intros. - right. rewrite e. apply same_not_diff. - case_eq (overlap l1 l2); intros. - right. apply overlap_not_diff; auto. - left. apply non_overlap_diff; auto. + intros. destruct l1; destruct l2; simpl. + - destruct (mreg_eq r r0). right; tauto. left; auto. + - left; auto. + - left; auto. + - destruct (slot_eq sl sl0). + destruct (zle (pos + typesize ty) pos0). + left; auto. + destruct (zle (pos0 + typesize ty0) pos). + left; auto. + right; red; intros [P | [P | P]]. congruence. omega. omega. + left; auto. Defined. (** We now redefine some standard notions over lists, using the [Loc.diff] @@ -316,12 +186,16 @@ Module Loc. elim (diff_not_eq l l); auto. Qed. - Lemma reg_notin: - forall r ll, ~(In (R r) ll) -> notin (R r) ll. + Lemma notin_dec (l: loc) (ll: list loc) : {notin l ll} + {~notin l ll}. Proof. - intros. rewrite notin_iff; intros. - destruct l'; simpl. congruence. auto. - Qed. + induction ll; simpl. + left; auto. + destruct (diff_dec l a). + destruct IHll. + left; auto. + right; tauto. + right; tauto. + Defined. (** [Loc.disjoint l1 l2] is true if the locations in list [l1] are different from all locations in list [l2]. *) @@ -376,6 +250,17 @@ Module Loc. | norepet_cons: forall hd tl, notin hd tl -> norepet tl -> norepet (hd :: tl). + Lemma norepet_dec (ll: list loc) : {norepet ll} + {~norepet ll}. + Proof. + induction ll. + left; constructor. + destruct (notin_dec a ll). + destruct IHll. + left; constructor; auto. + right; red; intros P; inv P; contradiction. + right; red; intros P; inv P; contradiction. + Defined. + (** [Loc.no_overlap l1 l2] holds if elements of [l1] never overlap partially with elements of [l2]. *) @@ -384,8 +269,6 @@ Module Loc. End Loc. -Global Opaque Loc.eq Loc.diff_dec. - (** * Mappings from locations to values *) (** The [Locmap] module defines mappings from locations to values, @@ -413,20 +296,20 @@ Module Locmap. Definition set (l: loc) (v: val) (m: t) : t := fun (p: loc) => - if Loc.eq l p then v else if Loc.overlap l p then Vundef else m p. + if Loc.eq l p then v else if Loc.diff_dec l p then m p else Vundef. Lemma gss: forall l v m, (set l v m) l = v. Proof. - intros. unfold set. case (Loc.eq l l); tauto. + intros. unfold set. rewrite dec_eq_true. auto. Qed. Lemma gso: forall l v m p, Loc.diff l p -> (set l v m) p = m p. Proof. - intros. unfold set. case (Loc.eq l p); intro. - subst p. elim (Loc.same_not_diff _ H). - caseEq (Loc.overlap l p); intro. - elim (Loc.overlap_not_diff _ _ H0 H). + intros. unfold set. destruct (Loc.eq l p). + subst p. elim (Loc.same_not_diff _ H). + destruct (Loc.diff_dec l p). auto. + contradiction. Qed. Fixpoint undef (ll: list loc) (m: t) {struct ll} : t := @@ -446,10 +329,172 @@ Module Locmap. assert (P: forall ll l m, m l = Vundef -> (undef ll m) l = Vundef). induction ll; simpl; intros. auto. apply IHll. unfold set. destruct (Loc.eq a l); auto. - destruct (Loc.overlap a l); auto. + destruct (Loc.diff_dec a l); auto. induction ll; simpl; intros. contradiction. destruct H. apply P. subst a. apply gss. auto. Qed. + Fixpoint setlist (ll: list loc) (vl: list val) (m: t) {struct ll} : t := + match ll, vl with + | l1 :: ls, v1 :: vs => setlist ls vs (set l1 v1 m) + | _, _ => m + end. + + Lemma gsetlisto: forall l ll vl m, Loc.notin l ll -> (setlist ll vl m) l = m l. + Proof. + induction ll; simpl; intros. + auto. + destruct vl; auto. destruct H. rewrite IHll; auto. apply gso; auto. apply Loc.diff_sym; auto. + Qed. + End Locmap. + +(** * Total ordering over locations *) + +Module IndexedTyp <: INDEXED_TYPE. + Definition t := typ. + Definition index (x: t) := + match x with Tint => 1%positive | Tfloat => 2%positive | Tlong => 3%positive end. + Lemma index_inj: forall x y, index x = index y -> x = y. + Proof. destruct x; destruct y; simpl; congruence. Qed. + Definition eq := typ_eq. +End IndexedTyp. + +Module OrderedTyp := OrderedIndexed(IndexedTyp). + +Module IndexedSlot <: INDEXED_TYPE. + Definition t := slot. + Definition index (x: t) := + match x with Local => 1%positive | Incoming => 2%positive | Outgoing => 3%positive end. + Lemma index_inj: forall x y, index x = index y -> x = y. + Proof. destruct x; destruct y; simpl; congruence. Qed. + Definition eq := slot_eq. +End IndexedSlot. + +Module OrderedSlot := OrderedIndexed(IndexedSlot). + +Module OrderedLoc <: OrderedType. + Definition t := loc. + Definition eq (x y: t) := x = y. + Definition lt (x y: t) := + match x, y with + | R r1, R r2 => Plt (IndexedMreg.index r1) (IndexedMreg.index r2) + | R _, S _ _ _ => True + | S _ _ _, R _ => False + | S sl1 ofs1 ty1, S sl2 ofs2 ty2 => + OrderedSlot.lt sl1 sl2 \/ (sl1 = sl2 /\ + (ofs1 < ofs2 \/ (ofs1 = ofs2 /\ OrderedTyp.lt ty1 ty2))) + end. + Lemma eq_refl : forall x : t, eq x x. + Proof (@refl_equal t). + Lemma eq_sym : forall x y : t, eq x y -> eq y x. + Proof (@sym_equal t). + Lemma eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z. + Proof (@trans_equal t). + Lemma lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z. + Proof. + unfold lt; intros. + destruct x; destruct y; destruct z; try tauto. + eapply Plt_trans; eauto. + destruct H. + destruct H0. left; eapply OrderedSlot.lt_trans; eauto. + destruct H0. subst sl0. auto. + destruct H. subst sl. + destruct H0. auto. + destruct H. + right. split. auto. + intuition. + right; split. congruence. eapply OrderedTyp.lt_trans; eauto. + Qed. + Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y. + Proof. + unfold lt, eq; intros; red; intros. subst y. + destruct x. + eelim Plt_strict; eauto. + destruct H. eelim OrderedSlot.lt_not_eq; eauto. red; auto. + destruct H. destruct H0. omega. + destruct H0. eelim OrderedTyp.lt_not_eq; eauto. red; auto. + Qed. + Definition compare : forall x y : t, Compare lt eq x y. + Proof. + intros. destruct x; destruct y. + - destruct (OrderedPositive.compare (IndexedMreg.index r) (IndexedMreg.index r0)). + + apply LT. red. auto. + + apply EQ. red. f_equal. apply IndexedMreg.index_inj. auto. + + apply GT. red. auto. + - apply LT. red; auto. + - apply GT. red; auto. + - destruct (OrderedSlot.compare sl sl0). + + apply LT. red; auto. + + destruct (OrderedZ.compare pos pos0). + * apply LT. red. auto. + * destruct (OrderedTyp.compare ty ty0). + apply LT. red; auto. + apply EQ. red; red in e; red in e0; red in e1. congruence. + apply GT. red; auto. + * apply GT. red. auto. + + apply GT. red; auto. + Defined. + Definition eq_dec := Loc.eq. + +(** Connection between the ordering defined here and the [Loc.diff] predicate. *) + + Definition diff_low_bound (l: loc) : loc := + match l with + | R mr => l + | S sl ofs ty => S sl (ofs - 1) Tfloat + end. + + Definition diff_high_bound (l: loc) : loc := + match l with + | R mr => l + | S sl ofs ty => S sl (ofs + typesize ty - 1) Tlong + end. + + Lemma outside_interval_diff: + forall l l', lt l' (diff_low_bound l) \/ lt (diff_high_bound l) l' -> Loc.diff l l'. + Proof. + intros. + destruct l as [mr | sl ofs ty]; destruct l' as [mr' | sl' ofs' ty']; simpl in *; auto. + - assert (IndexedMreg.index mr <> IndexedMreg.index mr'). + { destruct H. apply sym_not_equal. apply Plt_ne; auto. apply Plt_ne; auto. } + congruence. + - assert (RANGE: forall ty, 1 <= typesize ty <= 2). + { intros; unfold typesize. destruct ty0; omega. } + destruct H. + + destruct H. left. apply sym_not_equal. apply OrderedSlot.lt_not_eq; auto. + destruct H. right. + destruct H0. right. generalize (RANGE ty'); omega. + destruct H0. + assert (ty' = Tint). + { unfold OrderedTyp.lt in H1. destruct ty'; compute in H1; congruence. } + subst ty'. right. simpl typesize. omega. + + destruct H. left. apply OrderedSlot.lt_not_eq; auto. + destruct H. right. + destruct H0. left; omega. + destruct H0. exfalso. destruct ty'; compute in H1; congruence. + Qed. + + Lemma diff_outside_interval: + forall l l', Loc.diff l l' -> lt l' (diff_low_bound l) \/ lt (diff_high_bound l) l'. + Proof. + intros. + destruct l as [mr | sl ofs ty]; destruct l' as [mr' | sl' ofs' ty']; simpl in *; auto. + - unfold Plt, Pos.lt. destruct (Pos.compare (IndexedMreg.index mr) (IndexedMreg.index mr')) eqn:C. + elim H. apply IndexedMreg.index_inj. apply Pos.compare_eq_iff. auto. + auto. + rewrite Pos.compare_antisym. rewrite C. auto. + - destruct (OrderedSlot.compare sl sl'); auto. + destruct H. contradiction. + destruct H. + right; right; split; auto. left; omega. + left; right; split; auto. destruct ty'; simpl in *. + destruct (zlt ofs' (ofs - 1)). left; auto. + right; split. omega. compute. auto. + left; omega. + left; omega. + Qed. + +End OrderedLoc. + -- cgit