diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2014-07-23 08:54:56 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2014-07-23 08:54:56 +0000 |
commit | 2a0168fea37b68ad14e2cb60bf215111e49d4870 (patch) | |
tree | 2f59373790d8ce3a5df66ef7a692271cf0666c6c /ia32/Machregs.v | |
parent | 00805153cf9b88aa07cc6694b17d93f5ba2e7de8 (diff) | |
download | compcert-2a0168fea37b68ad14e2cb60bf215111e49d4870.tar.gz compcert-2a0168fea37b68ad14e2cb60bf215111e49d4870.zip |
Merge of "newspilling" branch:
- Support single-precision floats as first-class values
- Introduce chunks Many32, Many64 and types Tany32, Tany64 to
support saving and restoring registers without knowing
the exact types (int/single/float) of their contents, just
their sizes.
- Memory model: generalize the opaque encoding of pointers to
apply to any value, not just pointers, if chunks Many32/Many64
are selected.
- More properties of FP arithmetic proved.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2537 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'ia32/Machregs.v')
-rw-r--r-- | ia32/Machregs.v | 30 |
1 files changed, 16 insertions, 14 deletions
diff --git a/ia32/Machregs.v b/ia32/Machregs.v index da80a6ed..a9f2b6c4 100644 --- a/ia32/Machregs.v +++ b/ia32/Machregs.v @@ -43,11 +43,8 @@ Global Opaque mreg_eq. Definition mreg_type (r: mreg): typ := match r with - | 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 + | AX | BX | CX | DX | SI | DI | BP => Tany32 + | X0 | X1 | X2 | X3 | X4 | X5 | X6 | X7 | FP0 => Tany64 end. Local Open Scope positive_scope. @@ -76,7 +73,6 @@ Definition is_stack_reg (r: mreg) : bool := Definition destroyed_by_op (op: operation): list mreg := match op with - | Omove => FP0 :: nil | Ocast8signed | Ocast8unsigned | Ocast16signed | Ocast16unsigned => AX :: nil | Omulhs => AX :: DX :: nil | Omulhu => AX :: DX :: nil @@ -95,9 +91,7 @@ Definition destroyed_by_load (chunk: memory_chunk) (addr: addressing): list mreg 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 => FP0 :: nil + | _ => nil end. Definition destroyed_by_cond (cond: condition): list mreg := @@ -116,9 +110,7 @@ Definition destroyed_by_builtin (ef: external_function): list mreg := | EF_memcpy sz al => if zle sz 32 then CX :: X7 :: nil else CX :: SI :: DI :: nil | EF_vstore (Mint8unsigned|Mint8signed) => AX :: CX :: nil - | EF_vstore Mfloat32 => X7 :: nil | EF_vstore_global (Mint8unsigned|Mint8signed) _ _ => AX :: nil - | EF_vstore_global Mfloat32 _ _ => X7 :: nil | EF_builtin id sg => if ident_eq id builtin_write16_reversed || ident_eq id builtin_write32_reversed @@ -127,12 +119,12 @@ Definition destroyed_by_builtin (ef: external_function): list mreg := end. Definition destroyed_at_function_entry: list mreg := - DX :: FP0 :: nil. (* must include destroyed_by_op Omove *) + (* must include [destroyed_by_setstack ty] *) + DX :: FP0 :: nil. Definition destroyed_by_setstack (ty: typ): list mreg := match ty with - | Tfloat => FP0 :: nil - | Tsingle => X7 :: FP0 :: nil + | Tfloat | Tsingle => FP0 :: nil | _ => nil end. @@ -190,6 +182,7 @@ Definition two_address_op (op: operation) : bool := | Omove => false | Ointconst _ => false | Ofloatconst _ => false + | Osingleconst _ => false | Oindirectsymbol _ => false | Ocast8signed => false | Ocast8unsigned => false @@ -228,9 +221,18 @@ Definition two_address_op (op: operation) : bool := | 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 | Omakelong => false | Olowlong => false | Ohighlong => false |