From 6d25b4f3fc23601b3a84b4a70aab40ba429ac4b9 Mon Sep 17 00:00:00 2001 From: xleroy Date: Tue, 30 Dec 2008 14:48:33 +0000 Subject: Reorganized the development, modularizing away machine-dependent parts. Started to merge the ARM code generator. Started to add support for PowerPC/EABI. Use ocamlbuild to construct executable from Caml files. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@930 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- powerpc/Machregs.v | 107 +++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 107 insertions(+) create mode 100644 powerpc/Machregs.v (limited to 'powerpc/Machregs.v') diff --git a/powerpc/Machregs.v b/powerpc/Machregs.v new file mode 100644 index 0000000..260a0e8 --- /dev/null +++ b/powerpc/Machregs.v @@ -0,0 +1,107 @@ +(* *********************************************************************) +(* *) +(* 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 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 (* 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 + | 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 + | FT1 => 58 | FT2 => 59 | FT3 => 60 + 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 v1.2.3