diff options
Diffstat (limited to 'backend/Locations.v')
-rw-r--r-- | backend/Locations.v | 476 |
1 files changed, 476 insertions, 0 deletions
diff --git a/backend/Locations.v b/backend/Locations.v new file mode 100644 index 00000000..c97855ea --- /dev/null +++ b/backend/Locations.v @@ -0,0 +1,476 @@ +(** Locations are a refinement of RTL pseudo-registers, used to reflect + the results of register allocation (file [Allocation]). *) + +Require Import Coqlib. +Require Import Maps. +Require Import AST. +Require Import Values. + +(** * Representation of locations *) + +(** A location is either a processor register or (an abstract designation of) + a slot in the activation record of the current function. *) + +(** ** Machine registers *) + +(** The following type defines the machine registers that can be referenced + as locations. These include: +- Integer registers that can be allocated to RTL pseudo-registers ([Rxx]). +- Floating-point registers that can be allocated to RTL pseudo-registers + ([Fxx]). +- Three integer registers, not allocatable, reserved as temporaries for + spilling and reloading ([ITx]). +- Three float registers, not allocatable, reserved as temporaries for + spilling and reloading ([FTx]). + + The type [mreg] does not include special-purpose machine registers + such as the stack pointer and the condition codes. *) + +Inductive mreg: Set := + (** Allocatable integer regs *) + | R3: mreg | R4: mreg | R5: mreg | R6: mreg + | R7: mreg | R8: mreg | R9: mreg | R10: mreg + | R13: mreg | R14: mreg | R15: mreg | R16: mreg + | R17: mreg | R18: mreg | R19: mreg | R20: mreg + | R21: mreg | R22: mreg | R23: mreg | R24: mreg + | R25: mreg | R26: mreg | R27: mreg | R28: mreg + | R29: mreg | R30: mreg | R31: mreg + (** Allocatable float regs *) + | F1: mreg | F2: mreg | F3: mreg | F4: mreg + | F5: mreg | F6: mreg | F7: mreg | F8: mreg + | F9: mreg | F10: mreg | F14: mreg | F15: mreg + | F16: mreg | F17: mreg | F18: mreg | F19: mreg + | F20: mreg | F21: mreg | F22: mreg | F23: mreg + | F24: mreg | F25: mreg | F26: mreg | F27: mreg + | F28: mreg | F29: mreg | F30: mreg | F31: mreg + (** Integer temporaries *) + | IT1: mreg (* R11 *) | IT2: mreg (* R12 *) | IT3: mreg (* R0 *) + (** Float temporaries *) + | FT1: mreg (* F11 *) | FT2: mreg (* F12 *) | FT3: mreg (* F0 *). + +Lemma mreg_eq: forall (r1 r2: mreg), {r1 = r2} + {r1 <> r2}. +Proof. decide equality. Qed. + +Definition mreg_type (r: mreg): typ := + match r with + | R3 => Tint | R4 => Tint | R5 => Tint | R6 => Tint + | R7 => Tint | R8 => Tint | R9 => Tint | R10 => Tint + | R13 => Tint | R14 => Tint | R15 => Tint | R16 => Tint + | R17 => Tint | R18 => Tint | R19 => Tint | R20 => Tint + | R21 => Tint | R22 => Tint | R23 => Tint | R24 => Tint + | R25 => Tint | R26 => Tint | R27 => Tint | R28 => Tint + | R29 => Tint | R30 => Tint | R31 => Tint + | F1 => Tfloat | F2 => Tfloat | F3 => Tfloat | F4 => Tfloat + | F5 => Tfloat | F6 => Tfloat | F7 => Tfloat | F8 => Tfloat + | F9 => Tfloat | F10 => Tfloat | F14 => Tfloat | F15 => Tfloat + | F16 => Tfloat | F17 => Tfloat | F18 => Tfloat | F19 => Tfloat + | F20 => Tfloat | F21 => Tfloat | F22 => Tfloat | F23 => Tfloat + | F24 => Tfloat | F25 => Tfloat | F26 => Tfloat | F27 => Tfloat + | F28 => Tfloat | F29 => Tfloat | F30 => Tfloat | F31 => Tfloat + | IT1 => Tint | IT2 => Tint | IT3 => Tint + | FT1 => Tfloat | FT2 => Tfloat | FT3 => Tfloat + end. + +Open Scope positive_scope. + +Module IndexedMreg <: INDEXED_TYPE. + Definition t := mreg. + Definition eq := mreg_eq. + Definition index (r: mreg): positive := + match r with + | R3 => 1 | R4 => 2 | R5 => 3 | R6 => 4 + | R7 => 5 | R8 => 6 | R9 => 7 | R10 => 8 + | R13 => 9 | R14 => 10 | R15 => 11 | R16 => 12 + | R17 => 13 | R18 => 14 | R19 => 15 | R20 => 16 + | R21 => 17 | R22 => 18 | R23 => 19 | R24 => 20 + | R25 => 21 | R26 => 22 | R27 => 23 | R28 => 24 + | R29 => 25 | R30 => 26 | R31 => 27 + | F1 => 28 | F2 => 29 | F3 => 30 | F4 => 31 + | F5 => 32 | F6 => 33 | F7 => 34 | F8 => 35 + | F9 => 36 | F10 => 37 | F14 => 38 | F15 => 39 + | F16 => 40 | F17 => 41 | F18 => 42 | F19 => 43 + | F20 => 44 | F21 => 45 | F22 => 46 | F23 => 47 + | F24 => 48 | F25 => 49 | F26 => 50 | F27 => 51 + | F28 => 52 | F29 => 53 | F30 => 54 | F31 => 55 + | IT1 => 56 | IT2 => 57 | IT3 => 58 + | FT1 => 59 | FT2 => 60 | FT3 => 61 + end. + Lemma index_inj: + forall r1 r2, index r1 = index r2 -> r1 = r2. + Proof. + destruct r1; destruct r2; simpl; intro; discriminate || reflexivity. + Qed. +End IndexedMreg. + +(** ** Slots in activation records *) + +(** A slot in an activation record is designated abstractly by a kind, + a type and an integer offset. Three kinds are considered: +- [Local]: these are the slots used by register allocation for + pseudo-registers that cannot be assigned a hardware register. +- [Incoming]: used to store the parameters of the current function + that cannot reside in hardware registers, as determined by the + calling conventions. +- [Outgoing]: used to store arguments to called functions that + cannot reside in hardware registers, as determined by the + calling conventions. *) + +Inductive slot: Set := + | Local: Z -> typ -> slot + | Incoming: Z -> typ -> slot + | Outgoing: Z -> typ -> slot. + +(** Morally, the [Incoming] slots of a function are the [Outgoing] +slots of its caller function. + +The type of a slot indicates how it will be accessed later once mapped to +actual memory locations inside a memory-allocated activation record: +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. +Qed. + +Open Scope Z_scope. + +Definition typesize (ty: typ) : Z := + match ty with Tint => 1 | Tfloat => 2 end. + +Lemma typesize_pos: + forall (ty: typ), typesize ty > 0. +Proof. + destruct ty; compute; auto. +Qed. + +(** ** Locations *) + +(** Locations are just the disjoint union of machine registers and + activation record slots. *) + +Inductive loc : Set := + | R: mreg -> loc + | S: slot -> loc. + +Module Loc. + + Definition type (l: loc) : typ := + match l with + | R r => mreg_type r + | S s => slot_type s + end. + + Lemma eq: forall (p q: loc), {p = q} + {p <> q}. + Proof. + decide equality. apply mreg_eq. apply slot_eq. + Qed. + +(** As mentioned previously, two locations can be different (in the sense + of the [<>] mathematical disequality), yet denote + overlapping memory chunks within the activation record. + Given two locations, three cases are possible: +- They are equal (in the sense of the [=] equality) +- They are different and non-overlapping. +- They are different but overlapping. + + The second case (different and non-overlapping) is characterized + by the following [Loc.diff] predicate. +*) + 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 + | _, _ => + True + end. + + 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. + Qed. + + Lemma diff_not_eq: + forall l1 l2, diff l1 l2 -> l1 <> l2. + Proof. + unfold not; intros. subst l2. elim (same_not_diff l1 H). + Qed. + + Lemma diff_sym: + 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. + +(** [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. + Qed. + + Lemma overlap_not_diff: + forall l1 l2, overlap l1 l2 = true -> ~(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. + +(** We now redefine some standard notions over lists, using the [Loc.diff] + predicate instead of standard disequality [<>]. + + [Loc.notin l ll] holds if the location [l] is different from all locations + in the list [ll]. *) + + Fixpoint notin (l: loc) (ll: list loc) {struct ll} : Prop := + match ll with + | nil => True + | l1 :: ls => diff l l1 /\ notin l ls + end. + + Lemma notin_not_in: + forall l ll, notin l ll -> ~(In l ll). + Proof. + unfold not; induction ll; simpl; intros. + auto. + elim H; intros. elim H0; intro. + subst l. exact (same_not_diff a H1). + auto. + Qed. + +(** [Loc.disjoint l1 l2] is true if the locations in list [l1] + are different from all locations in list [l2]. *) + + Definition disjoint (l1 l2: list loc) : Prop := + forall x1 x2, In x1 l1 -> In x2 l2 -> diff x1 x2. + + Lemma disjoint_cons_left: + forall a l1 l2, + disjoint (a :: l1) l2 -> disjoint l1 l2. + Proof. + unfold disjoint; intros. auto with coqlib. + Qed. + Lemma disjoint_cons_right: + forall a l1 l2, + disjoint l1 (a :: l2) -> disjoint l1 l2. + Proof. + unfold disjoint; intros. auto with coqlib. + Qed. + + Lemma disjoint_sym: + forall l1 l2, disjoint l1 l2 -> disjoint l2 l1. + Proof. + unfold disjoint; intros. apply diff_sym; auto. + Qed. + + Lemma in_notin_diff: + forall l1 l2 ll, notin l1 ll -> In l2 ll -> diff l1 l2. + Proof. + induction ll; simpl; intros. + elim H0. + elim H0; intro. subst a. tauto. apply IHll; tauto. + Qed. + + Lemma notin_disjoint: + forall l1 l2, + (forall x, In x l1 -> notin x l2) -> disjoint l1 l2. + Proof. + unfold disjoint; induction l1; intros. + elim H0. + elim H0; intro. + subst x1. eapply in_notin_diff. apply H. auto with coqlib. auto. + eapply IHl1; eauto. intros. apply H. auto with coqlib. + Qed. + + Lemma disjoint_notin: + forall l1 l2 x, disjoint l1 l2 -> In x l1 -> notin x l2. + Proof. + unfold disjoint; induction l2; simpl; intros. + auto. + split. apply H. auto. tauto. + apply IHl2. intros. apply H. auto. tauto. auto. + Qed. + +(** [Loc.norepet ll] holds if the locations in list [ll] are pairwise + different. *) + + Inductive norepet : list loc -> Prop := + | norepet_nil: + norepet nil + | norepet_cons: + forall hd tl, notin hd tl -> norepet tl -> norepet (hd :: tl). + + Definition no_overlap (l1 l2 : list loc) := + forall r, In r l1 -> forall s, In s l2 -> r = s \/ Loc.diff r s. + +End Loc. + +(** * Mappings from locations to values *) + +(** The [Locmap] module defines mappings from locations to values, + used as evaluation environments for the semantics of the [LTL] + and [Linear] intermediate languages. *) + +Set Implicit Arguments. + +Module Locmap. + + Definition t := loc -> val. + + Definition init (x: val) : t := fun (_: loc) => x. + + Definition get (l: loc) (m: t) : val := m l. + + (** The [set] operation over location mappings reflects the overlapping + properties of locations: changing the value of a location [l] + invalidates (sets to [Vundef]) the locations that partially overlap + with [l]. In other terms, the result of [set l v m] + maps location [l] to value [v], locations that overlap with [l] + to [Vundef], and locations that are different (and non-overlapping) + from [l] to their previous values in [m]. This is apparent in the + ``good variables'' properties [Locmap.gss] and [Locmap.gso]. *) + + 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. + + Lemma gss: forall l v m, (set l v m) l = v. + Proof. + intros. unfold set. case (Loc.eq l l); tauto. + 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). + auto. + Qed. + +End Locmap. |