From 2a0168fea37b68ad14e2cb60bf215111e49d4870 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Wed, 23 Jul 2014 08:54:56 +0000
Subject: 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
---
 ia32/Machregs.v | 30 ++++++++++++++++--------------
 1 file changed, 16 insertions(+), 14 deletions(-)

(limited to 'ia32/Machregs.v')

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
-- 
cgit