Module Machregs

Require Import Coqlib.
Require Import Maps.
Require Import AST.

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).
Two integer registers, not allocatable, reserved as temporaries for spilling and reloading (IT1, IT2).
Two float registers, not allocatable, reserved as temporaries for spilling and reloading (FT1, FT2).

The type mreg does not include special-purpose or reserved machine registers such as the stack pointer and the condition codes.

Inductive mreg: Type :=

Allocatable integer regs

Allocatable float regs

Integer temporaries

| IT1: mreg | IT2: mreg

Float temporaries

| FT1: mreg | FT2: mreg | FP0: mreg .

Lemma mreg_eq: forall (r1 r2: mreg), {r1 = r2} + {r1 <> r2}.

Proof.

decide equality. Qed.

Allocatable float regs

Integer temporaries

| IT1 => Tint | IT2 => Tint

Float temporaries

  | FT1 => Tfloat | FT2 => Tfloat | FP0 => 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
    | AX => 1 | BX => 2 | SI => 3 | DI => 4 | BP => 5
    | X0 => 6 | X1 => 7 | X2 => 8
    | X3 => 9 | X4 => 10 | X5 => 11
    | IT1 => 12 | IT2 => 13
    | FT1 => 14 | FT2 => 15 | FP0 => 16
    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.