diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-04-20 07:54:52 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-04-20 07:54:52 +0000 |
commit | 255cee09b71255051c2b40eae0c88bffce1f6f32 (patch) | |
tree | 7951b1b13e8fd5e525b9223e8be0580e83550f55 /ia32/Machregs.v | |
parent | 6e5041958df01c56762e90770abd704b95a36e5d (diff) | |
download | compcert-255cee09b71255051c2b40eae0c88bffce1f6f32.tar.gz compcert-255cee09b71255051c2b40eae0c88bffce1f6f32.zip |
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
Diffstat (limited to 'ia32/Machregs.v')
-rw-r--r-- | ia32/Machregs.v | 192 |
1 files changed, 165 insertions, 27 deletions
diff --git a/ia32/Machregs.v b/ia32/Machregs.v index df963935..3b84aa5f 100644 --- a/ia32/Machregs.v +++ b/ia32/Machregs.v @@ -10,34 +10,32 @@ (* *) (* *********************************************************************) +Require Import String. Require Import Coqlib. Require Import Maps. Require Import AST. +Require Import Integers. +Require Import Op. (** ** 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]). +- Integer registers that can be allocated to RTL pseudo-registers. +- Floating-point registers that can be allocated to RTL pseudo-registers. +- The special [FP0] register denoting the top of the X87 float stack. 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 + | AX: mreg | BX: mreg | CX: mreg | DX: 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 *). + | X0: mreg | X1: mreg | X2: mreg | X3: mreg + | X4: mreg | X5: mreg | X6: mreg | X7: mreg + (** Special float reg *) + | FP0: mreg (**r top of x87 FP stack *). Lemma mreg_eq: forall (r1 r2: mreg), {r1 = r2} + {r1 <> r2}. Proof. decide equality. Defined. @@ -45,28 +43,24 @@ Global Opaque mreg_eq. 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 + | AX => Tint | BX => Tint | CX => Tint | DX => Tint + | SI => Tint | DI => Tint | BP => Tint + | X0 => Tfloat | X1 => Tfloat | X2 => Tfloat | X3 => Tfloat + | X4 => Tfloat | X5 => Tfloat | X6 => Tfloat | X7 => Tfloat + | FP0 => Tfloat end. -Open Scope positive_scope. +Local 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 + | AX => 1 | BX => 2 | CX => 3 | DX => 4 | SI => 5 | DI => 6 | BP => 7 + | X0 => 8 | X1 => 9 | X2 => 10 | X3 => 11 + | X4 => 12 | X5 => 13 | X6 => 14 | X7 => 15 + | FP0 => 16 end. Lemma index_inj: forall r1 r2, index r1 = index r2 -> r1 = r2. @@ -75,3 +69,147 @@ Module IndexedMreg <: INDEXED_TYPE. Qed. End IndexedMreg. +(** ** Destroyed registers, preferred registers *) + +Definition destroyed_by_op (op: operation): list mreg := + match op with + | Omove => FP0 :: nil + | Ocast8signed | Ocast8unsigned | Ocast16signed | Ocast16unsigned => AX :: nil + | Odiv => AX :: DX :: nil + | Odivu => AX :: DX :: nil + | Omod => AX :: DX :: nil + | Omodu => AX :: DX :: nil + | Oshrximm _ => CX :: nil + | Ocmp _ => AX :: CX :: 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 + | Mint8signed | Mint8unsigned => AX :: CX :: nil + | Mint16signed | Mint16unsigned | Mint32 | Mint64 => nil + | Mfloat32 => X7 :: nil + | Mfloat64 | Mfloat64al32 => FP0 :: 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 CX :: X7 :: nil else CX :: SI :: DI :: nil + | EF_vload _ => nil + | EF_vload_global _ _ _ => nil + | EF_vstore _ => AX :: CX :: X7 :: nil + | EF_vstore_global _ _ _ => AX :: X7 :: nil + | _ => AX :: CX :: X7 :: FP0 :: nil + end. + +Definition destroyed_at_function_entry: list mreg := + DX :: FP0 :: nil. (* must include destroyed_by_op Omove *) + +Definition temp_for_parent_frame: mreg := + DX. + +Definition mregs_for_operation (op: operation): list (option mreg) * option mreg := + match op with + | Odiv => (Some AX :: Some CX :: nil, Some AX) + | Odivu => (Some AX :: Some CX :: nil, Some AX) + | Omod => (Some AX :: Some CX :: nil, Some DX) + | Omodu => (Some AX :: Some CX :: nil, Some DX) + | Oshl => (None :: Some CX :: nil, None) + | Oshr => (None :: Some CX :: nil, None) + | Oshru => (None :: Some CX :: nil, None) + | Oshrximm _ => (Some AX :: nil, Some AX) + | _ => (nil, None) + end. + +Local Open Scope string_scope. + +Definition builtin_negl := ident_of_string "__builtin_negl". +Definition builtin_addl := ident_of_string "__builtin_addl". +Definition builtin_subl := ident_of_string "__builtin_subl". +Definition builtin_mull := ident_of_string "__builtin_mull". + +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 (Some AX :: Some DX :: nil, nil) else (Some DI :: Some SI :: nil, nil) + | EF_builtin id sg => + if ident_eq id builtin_negl then + (Some DX :: Some AX :: nil, Some DX :: Some AX :: nil) + else if ident_eq id builtin_addl || ident_eq id builtin_subl then + (Some DX :: Some AX :: Some CX :: Some BX :: nil, Some DX :: Some AX :: nil) + else if ident_eq id builtin_mull then + (Some AX :: Some DX :: nil, Some DX :: Some AX :: nil) + else + (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]. *) + +Definition two_address_op (op: operation) : bool := + match op with + | Omove => false + | Ointconst _ => false + | Ofloatconst _ => false + | Oindirectsymbol _ => false + | Ocast8signed => false + | Ocast8unsigned => false + | Ocast16signed => false + | Ocast16unsigned => false + | Oneg => true + | Osub => true + | Omul => true + | Omulimm _ => true + | Odiv => false + | Odivu => false + | Omod => false + | Omodu => false + | Oand => true + | Oandimm _ => true + | Oor => true + | Oorimm _ => true + | Oxor => true + | Oxorimm _ => true + | Oshl => true + | Oshlimm _ => true + | Oshr => true + | Oshrimm _ => true + | Oshrximm _ => false + | Oshru => true + | Oshruimm _ => true + | Ororimm _ => true + | Oshldimm _ => true + | Olea addr => false + | Onegf => true + | Oabsf => true + | Oaddf => true + | Osubf => true + | Omulf => true + | Odivf => true + | Osingleoffloat => false + | Ointoffloat => false + | Ofloatofint => false + | Omakelong => false + | Olowlong => false + | Ohighlong => false + | Ocmp c => false + end. + |