diff options
Diffstat (limited to 'ia32/Machregs.v')
| -rw-r--r-- | ia32/Machregs.v | 367 |
1 files changed, 0 insertions, 367 deletions
diff --git a/ia32/Machregs.v b/ia32/Machregs.v deleted file mode 100644 index 741081a6..00000000 --- a/ia32/Machregs.v +++ /dev/null @@ -1,367 +0,0 @@ -(* *********************************************************************) -(* *) -(* 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 String. -Require Import Coqlib. -Require Import Decidableplus. -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. -- 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 | BX | CX | DX | SI | DI | BP - | R8 | R9 | R10 | R11 | R12 | R13 | R14 | R15 (**r only in 64-bit mode *) - (** Allocatable float regs *) - | X0 | X1 | X2 | X3 | X4 | X5 | X6 | X7 - | X8 | X9 | X10 | X11 | X12 | X13 | X14 | X15 (**r only in 64-bit mode *) - (** Special float reg *) - | FP0. - -Lemma mreg_eq: forall (r1 r2: mreg), {r1 = r2} + {r1 <> r2}. -Proof. decide equality. Defined. -Global Opaque mreg_eq. - -Definition all_mregs := - AX :: BX :: CX :: DX :: SI :: DI :: BP - :: R8 :: R9 :: R10 :: R11 :: R12 :: R13 :: R14 :: R15 - :: X0 :: X1 :: X2 :: X3 :: X4 :: X5 :: X6 :: X7 - :: X8 :: X9 :: X10 :: X11 :: X12 :: X13 :: X14 :: X15 - :: FP0 :: nil. - -Lemma all_mregs_complete: - forall (r: mreg), In r all_mregs. -Proof. - assert (forall r, proj_sumbool (In_dec mreg_eq r all_mregs) = true) by (destruct r; reflexivity). - intros. specialize (H r). InvBooleans. auto. -Qed. - -Instance Decidable_eq_mreg : forall (x y: mreg), Decidable (eq x y) := Decidable_eq mreg_eq. - -Instance Finite_mreg : Finite mreg := { - Finite_elements := all_mregs; - Finite_elements_spec := all_mregs_complete -}. - -Definition mreg_type (r: mreg): typ := - match r with - | AX | BX | CX | DX | SI | DI | BP => if Archi.ptr64 then Tany64 else Tany32 - | R8 | R9 | R10 | R11 | R12 | R13 | R14 | R15 => Tany64 - | X0 | X1 | X2 | X3 | X4 | X5 | X6 | X7 => Tany64 - | X8 | X9 | X10 | X11 | X12 | X13 | X14 | X15 => Tany64 - | FP0 => Tany64 - end. - -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 | CX => 3 | DX => 4 | SI => 5 | DI => 6 | BP => 7 - | R8 => 8 | R9 => 9 | R10 => 10 | R11 => 11 | R12 => 12 | R13 => 13 | R14 => 14 | R15 => 15 - | X0 => 16 | X1 => 17 | X2 => 18 | X3 => 19 | X4 => 20 | X5 => 21 | X6 => 22 | X7 => 23 - | X8 => 24 | X9 => 25 | X10 => 26 | X11 => 27 | X12 => 28 | X13 => 29 | X14 => 30 | X15 => 31 - | FP0 => 32 - end. - Lemma index_inj: - forall r1 r2, index r1 = index r2 -> r1 = r2. - Proof. - decide_goal. - Qed. -End IndexedMreg. - -Definition is_stack_reg (r: mreg) : bool := - match r with FP0 => true | _ => false end. - -(** ** Names of registers *) - -Local Open Scope string_scope. - -Definition register_names := - ("RAX", AX) :: ("RBX", BX) :: ("RCX", CX) :: ("RDX", DX) :: - ("RSI", SI) :: ("RDI", DI) :: ("RBP", BP) :: - ("EAX", AX) :: ("EBX", BX) :: ("ECX", CX) :: ("EDX", DX) :: - ("ESI", SI) :: ("EDI", DI) :: ("EBP", BP) :: - ("R8", R8) :: ("R9", R9) :: ("R10", R10) :: ("R11", R11) :: - ("R12", R12) :: ("R13", R13) :: ("R14", R14) :: ("R15", R15) :: - ("XMM0", X0) :: ("XMM1", X1) :: ("XMM2", X2) :: ("XMM3", X3) :: - ("XMM4", X4) :: ("XMM5", X5) :: ("XMM6", X6) :: ("XMM7", X7) :: - ("XMM8", X8) :: ("XMM9", X9) :: ("XMM10", X10) :: ("XMM11", X11) :: - ("XMM12", X12) :: ("XMM13", X13) :: ("XMM14", X14) :: ("XMM15", X15) :: - ("ST0", FP0) :: nil. - -Definition register_by_name (s: string) : option mreg := - let fix assoc (l: list (string * mreg)) : option mreg := - match l with - | nil => None - | (s1, r1) :: l' => if string_dec s s1 then Some r1 else assoc l' - end - in assoc register_names. - -(** ** Destroyed registers, preferred registers *) - -Definition destroyed_by_op (op: operation): list mreg := - match op with - | Ocast8signed | Ocast8unsigned => AX :: nil - | Omulhs => AX :: DX :: nil - | Omulhu => AX :: DX :: nil - | Odiv => AX :: DX :: nil - | Odivu => AX :: DX :: nil - | Omod => AX :: DX :: nil - | Omodu => AX :: DX :: nil - | Oshrximm _ => CX :: nil - | Omullhs => AX :: DX :: nil - | Omullhu => AX :: DX :: nil - | Odivl => AX :: DX :: nil - | Odivlu => AX :: DX :: nil - | Omodl => AX :: DX :: nil - | Omodlu => AX :: DX :: nil - | Oshrxlimm _ => DX :: 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 => if Archi.ptr64 then nil else AX :: CX :: nil - | _ => nil - end. - -Definition destroyed_by_cond (cond: condition): list mreg := - nil. - -Definition destroyed_by_jumptable: list mreg := - AX :: DX :: nil. - -Fixpoint destroyed_by_clobber (cl: list string): list mreg := - match cl with - | nil => nil - | c1 :: cl => - match register_by_name c1 with - | Some r => r :: destroyed_by_clobber cl - | None => destroyed_by_clobber cl - end - end. - -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_vstore (Mint8unsigned|Mint8signed) => - if Archi.ptr64 then nil else AX :: CX :: nil - | EF_builtin name sg => - if string_dec name "__builtin_va_start" then AX :: nil - else if string_dec name "__builtin_write16_reversed" - || string_dec name "__builtin_write32_reversed" - then CX :: DX :: nil - else nil - | EF_inline_asm txt sg clob => destroyed_by_clobber clob - | _ => nil - end. - -Definition destroyed_at_function_entry: list mreg := - (* must include [destroyed_by_setstack ty] *) - AX :: FP0 :: nil. - -Definition destroyed_by_setstack (ty: typ): list mreg := - match ty with - | Tfloat | Tsingle => FP0 :: nil - | _ => nil - end. - -Definition destroyed_at_indirect_call: list mreg := - nil. - -Definition temp_for_parent_frame: mreg := - AX. - -Definition mregs_for_operation (op: operation): list (option mreg) * option mreg := - match op with - | Omulhs => (Some AX :: None :: nil, Some DX) - | Omulhu => (Some AX :: None :: nil, Some DX) - | 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) - | Omullhs => (Some AX :: None :: nil, Some DX) - | Omullhu => (Some AX :: None :: nil, Some DX) - | Odivl => (Some AX :: Some CX :: nil, Some AX) - | Odivlu => (Some AX :: Some CX :: nil, Some AX) - | Omodl => (Some AX :: Some CX :: nil, Some DX) - | Omodlu => (Some AX :: Some CX :: nil, Some DX) - | Oshll => (None :: Some CX :: nil, None) - | Oshrl => (None :: Some CX :: nil, None) - | Oshrlu => (None :: Some CX :: nil, None) - | Oshrxlimm _ => (Some AX :: nil, Some AX) - | _ => (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 (Some AX :: Some DX :: nil, nil) else (Some DI :: Some SI :: nil, nil) - | EF_builtin name sg => - if string_dec name "__builtin_negl" then - (Some DX :: Some AX :: nil, Some DX :: Some AX :: nil) - else if string_dec name "__builtin_addl" - || string_dec name "__builtin_subl" then - (Some DX :: Some AX :: Some CX :: Some BX :: nil, Some DX :: Some AX :: nil) - else if string_dec name "__builtin_mull" then - (Some AX :: Some DX :: nil, Some DX :: Some AX :: nil) - else if string_dec name "__builtin_va_start" then - (Some DX :: nil, nil) - else if (negb Archi.ptr64) && string_dec name "__builtin_bswap64" 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_by_setstack 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 - | Olongconst _ => false - | Ofloatconst _ => false - | Osingleconst _ => false - | Oindirectsymbol _ => false - | Ocast8signed => false - | Ocast8unsigned => false - | Ocast16signed => false - | Ocast16unsigned => false - | Oneg => true - | Osub => true - | Omul => true - | Omulimm _ => true - | Omulhs => false - | Omulhu => false - | Odiv => false - | Odivu => false - | Omod => false - | Omodu => false - | Oand => true - | Oandimm _ => true - | Oor => true - | Oorimm _ => true - | Oxor => true - | Oxorimm _ => true - | Onot => true - | Oshl => true - | Oshlimm _ => true - | Oshr => true - | Oshrimm _ => true - | Oshrximm _ => false - | Oshru => true - | Oshruimm _ => true - | Ororimm _ => true - | Oshldimm _ => true - | Olea addr => false - | Omakelong => true - | Olowlong => true - | Ohighlong => true - | Ocast32signed => false - | Ocast32unsigned => false - | Onegl => true - | Oaddlimm _ => true - | Osubl => true - | Omull => true - | Omullimm _ => true - | Omullhs => false - | Omullhu => false - | Odivl => false - | Odivlu => false - | Omodl => false - | Omodlu => false - | Oandl => true - | Oandlimm _ => true - | Oorl => true - | Oorlimm _ => true - | Oxorl => true - | Oxorlimm _ => true - | Onotl => true - | Oshll => true - | Oshllimm _ => true - | Oshrl => true - | Oshrlimm _ => true - | Oshrxlimm _ => false - | Oshrlu => true - | Oshrluimm _ => true - | Ororlimm _ => true - | Oleal addr => false - | Onegf => true - | Oabsf => true - | Oaddf => true - | Osubf => true - | Omulf => true - | Odivf => true - | Onegfs => true - | Oabsfs => true - | Oaddfs => true - | Osubfs => true - | Omulfs => true - | Odivfs => true - | Osingleoffloat => false - | Ofloatofsingle => false - | Ointoffloat => false - | Ofloatofint => false - | Ointofsingle => false - | Osingleofint => false - | Olongoffloat => false - | Ofloatoflong => false - | Olongofsingle => false - | Osingleoflong => false - | Ocmp c => false - end. - -(* Constraints on constant propagation for builtins *) - -Definition builtin_constraints (ef: external_function) : - list builtin_arg_constraint := - match ef with - | EF_vload _ => OK_addrany :: nil - | EF_vstore _ => OK_addrany :: OK_default :: nil - | EF_memcpy _ _ => OK_addrany :: OK_addrany :: nil - | EF_annot txt targs => map (fun _ => OK_all) targs - | EF_debug kind txt targs => map (fun _ => OK_all) targs - | _ => nil - end. |