path: root/backend/Locations.v

(** 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.