From 255cee09b71255051c2b40eae0c88bffce1f6f32 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 20 Apr 2013 07:54:52 +0000 Subject: Big merge of the newregalloc-int64 branch. Lots of changes in two directions: 1- new register allocator (+ live range splitting, spilling&reloading, etc) based on a posteriori validation using the Rideau-Leroy algorithm 2- support for 64-bit integer arithmetic (type "long long"). git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2200 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- arm/Machregs.v | 105 ++++++++++++++++++++++++++++++++++++++++++++------------- 1 file changed, 81 insertions(+), 24 deletions(-) (limited to 'arm/Machregs.v') diff --git a/arm/Machregs.v b/arm/Machregs.v index 317515c3..4906eb0b 100644 --- a/arm/Machregs.v +++ b/arm/Machregs.v @@ -13,6 +13,7 @@ Require Import Coqlib. Require Import Maps. Require Import AST. +Require Import Op. (** ** Machine registers *) @@ -21,43 +22,36 @@ Require Import AST. - 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 ([ITx]). -- Two float registers, not allocatable, reserved as temporaries for - spilling and reloading ([FTx]). - The type [mreg] does not include special-purpose machine registers - such as the stack pointer and the condition codes. *) + The type [mreg] does not include reserved machine registers + such as the stack pointer, the link register, and the condition codes. *) Inductive mreg: Type := (** Allocatable integer regs *) | R0: mreg | R1: mreg | R2: mreg | R3: mreg | R4: mreg | R5: mreg | R6: mreg | R7: mreg - | R8: mreg | R9: mreg | R11: mreg + | R8: mreg | R9: mreg | R10: mreg | R11: mreg + | R12: mreg (** Allocatable double-precision float regs *) | F0: mreg | F1: mreg | F2: mreg | F3: mreg - | F4: mreg | F5: mreg + | F4: mreg | F5: mreg | F6: mreg | F7: mreg | F8: mreg | F9: mreg | F10: mreg | F11: mreg - | F12: mreg | F13: mreg | F14: mreg | F15: mreg - (** Integer temporaries *) - | IT1: mreg (* R10 *) | IT2: mreg (* R12 *) - (** Float temporaries *) - | FT1: mreg (* F6 *) | FT2: mreg (* F7 *). + | F12: mreg | F13: mreg | F14: mreg | F15: mreg. Lemma mreg_eq: forall (r1 r2: mreg), {r1 = r2} + {r1 <> r2}. Proof. decide equality. Defined. +Global Opaque mreg_eq. Definition mreg_type (r: mreg): typ := match r with | R0 => Tint | R1 => Tint | R2 => Tint | R3 => Tint | R4 => Tint | R5 => Tint | R6 => Tint | R7 => Tint - | R8 => Tint | R9 => Tint | R11 => Tint + | R8 => Tint | R9 => Tint | R10 => Tint | R11 => Tint + | R12 => Tint | F0 => Tfloat | F1 => Tfloat | F2 => Tfloat | F3 => Tfloat - | F4 => Tfloat| F5 => Tfloat + | F4 => Tfloat| F5 => Tfloat | F6 => Tfloat | F7 => Tfloat | F8 => Tfloat | F9 => Tfloat | F10 => Tfloat | F11 => Tfloat | F12 => Tfloat | F13 => Tfloat | F14 => Tfloat | F15 => Tfloat - | IT1 => Tint | IT2 => Tint - | FT1 => Tfloat | FT2 => Tfloat end. Open Scope positive_scope. @@ -69,13 +63,12 @@ Module IndexedMreg <: INDEXED_TYPE. match r with | R0 => 1 | R1 => 2 | R2 => 3 | R3 => 4 | R4 => 5 | R5 => 6 | R6 => 7 | R7 => 8 - | R8 => 9 | R9 => 10 | R11 => 11 - | F0 => 12 | F1 => 13 | F2 => 14 | F3 => 15 - | F4 => 16 | F5 => 17 - | F8 => 18 | F9 => 19 | F10 => 20 | F11 => 21 - | F12 => 22 | F13 => 23 | F14 => 24 | F15 => 25 - | IT1 => 26 | IT2 => 27 - | FT1 => 28 | FT2 => 29 + | R8 => 9 | R9 => 10 | R10 => 11 | R11 => 12 + | R12 => 13 + | F0 => 14 | F1 => 15 | F2 => 16 | F3 => 17 + | F4 => 18 | F5 => 19 | F6 => 20 | F7 => 21 + | F8 => 22 | F9 => 23 | F10 => 24 | F11 => 25 + | F12 => 26 | F13 => 27 | F14 => 28 | F15 => 29 end. Lemma index_inj: forall r1 r2, index r1 = index r2 -> r1 = r2. @@ -84,3 +77,67 @@ Module IndexedMreg <: INDEXED_TYPE. Qed. End IndexedMreg. +(** ** Destroyed registers, preferred registers *) + +Definition destroyed_by_op (op: operation): list mreg := + match op with + | Odiv | Odivu => R0 :: R1 :: R2 :: R3 :: R12 :: nil + | Ointoffloat | Ointuoffloat => F6 :: nil + | _ => nil + end. + +Definition destroyed_by_load (chunk: memory_chunk) (addr: addressing): list mreg := + nil. + +Definition destroyed_by_store (chunk: memory_chunk) (addr: addressing): list mreg := + match chunk with + | Mfloat32 => F6 :: nil + | _ => nil + end. + +Definition destroyed_by_cond (cond: condition): list mreg := + nil. + +Definition destroyed_by_jumptable: list mreg := + nil. + +Definition destroyed_by_builtin (ef: external_function): list mreg := + match ef with + | EF_memcpy sz al => if zle sz 32 then nil else R2 :: R3 :: R12 :: nil + | _ => R12 :: F6 :: nil + end. + +Definition destroyed_at_function_entry: list mreg := + R12 :: nil. + +Definition temp_for_parent_frame: mreg := + R12. + +Definition mregs_for_operation (op: operation): list (option mreg) * option mreg := + match op with + | Odiv | Odivu => (Some R0 :: Some R1 :: nil, Some R0) + | _ => (nil, None) + end. + +Definition mregs_for_builtin (ef: external_function): list (option mreg) * list(option mreg) := + match ef with + | EF_memcpy sz al => + if zle sz 32 then (nil, nil) else (Some R3 :: Some R2 :: nil, nil) + | _ => (nil, nil) + end. + +Global Opaque + destroyed_by_op destroyed_by_load destroyed_by_store + destroyed_by_cond destroyed_by_jumptable destroyed_by_builtin + destroyed_at_function_entry temp_for_parent_frame + mregs_for_operation mregs_for_builtin. + +(** Two-address operations. Return [true] if the first argument and + the result must be in the same location *and* are unconstrained + by [mregs_for_operation]. There are none for ARM. *) + +Definition two_address_op (op: operation) : bool := + false. + +Global Opaque two_address_op. + -- cgit