1 files changed, 76 insertions, 0 deletions
diff --git a/ia32/Machregs.v b/ia32/Machregs.v
new file mode 100644
index 0000000..9935efa
--- /dev/null
+++ b/ia32/Machregs.v
@@ -0,0 +1,76 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
+(*                                                                     *)
+(*  Copyright Institut National de Recherche en Informatique et en     *)
+(*  Automatique.  All rights reserved.  This file is distributed       *)
+(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+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 *)
+  | AX: mreg | BX: mreg | SI: mreg | DI: mreg | BP: mreg
+  (** Allocatable float regs *)
+  | X0: mreg | X1: mreg | X2: mreg | X3: mreg | X4: mreg | X5: mreg
+  (** Integer temporaries *)
+  | IT1: mreg (* DX *) | IT2: mreg (* CX *)
+  (** Float temporaries *)
+  | FT1: mreg (* X6 *) | FT2: mreg (* X7 *) | FP0: mreg (* top of FP stack *).
+
+Lemma mreg_eq: forall (r1 r2: mreg), {r1 = r2} + {r1 <> r2}.
+Proof. decide equality. Qed.
+
+Definition mreg_type (r: mreg): typ :=
+  match r with
+  | AX => Tint | BX => Tint | SI => Tint | DI => Tint | BP => Tint
+  (** Allocatable float regs *)
+  | X0 => Tfloat | X1 => Tfloat | X2 => Tfloat
+  | X3 => Tfloat | X4 => Tfloat | X5 => Tfloat
+  (** 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.
+