diff options
| author |  xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2008-12-21 13:32:24 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2008-12-21 13:32:24 +0000 |
| commit | dc4bed2cf06f46687225275131f411c86c773598 (patch) | |
| tree | 9d99e759d906d061b6f213e0b20cb4bd53580ea6 /backend/Locations.v | |
| parent | ec6d00d94bcb1a0adc5c698367634b5e2f370c6e (diff) | |
Revised back-end so that only 2 integer registers are reserved for reloading.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@925 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'backend/Locations.v')
| -rw-r--r-- | backend/Locations.v | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/backend/Locations.v b/backend/Locations.v index 1373887..b03657c 100644 --- a/backend/Locations.v +++ b/backend/Locations.v @@ -30,10 +30,10 @@ Require Import Values. - 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]). +- 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. *) @@ -56,7 +56,7 @@ Inductive mreg: Set := | 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 *) + | IT1: mreg (* R11 *) | IT2: mreg (* R0 *) (** Float temporaries *) | FT1: mreg (* F11 *) | FT2: mreg (* F12 *) | FT3: mreg (* F0 *). @@ -79,7 +79,7 @@ Definition mreg_type (r: mreg): typ := | 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 + | IT1 => Tint | IT2 => Tint | FT1 => Tfloat | FT2 => Tfloat | FT3 => Tfloat end. @@ -104,8 +104,8 @@ Module IndexedMreg <: INDEXED_TYPE. | 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 + | IT1 => 56 | IT2 => 57 + | FT1 => 58 | FT2 => 59 | FT3 => 60 end. Lemma index_inj: forall r1 r2, index r1 = index r2 -> r1 = r2. |