From 265fa07b34a813ba9d8249ddad82d71e6002c10d Mon Sep 17 00:00:00 2001 From: xleroy Date: Thu, 2 Sep 2010 12:42:19 +0000 Subject: Merge of the reuse-temps branch: - Reload temporaries are marked as destroyed (set to Vundef) across operations in the semantics of LTL, LTLin, Linear and Mach, allowing Asmgen to reuse them. - Added IA32 port. - Cleaned up float conversions and axiomatization of floats. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1499 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- ia32/Machregs.v | 76 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 76 insertions(+) create mode 100644 ia32/Machregs.v (limited to 'ia32/Machregs.v') diff --git a/ia32/Machregs.v b/ia32/Machregs.v new file mode 100644 index 00000000..9935efae --- /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. + -- cgit