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

1 files changed, 31 insertions, 4 deletions

diff --git a/ia32/SelectOp.vp b/ia32/SelectOp.vp
index 214608e..b6aef72 100644
--- a/ia32/SelectOp.vp
+++ b/ia32/SelectOp.vp
@@ -346,6 +346,12 @@ Definition addf (e1 e2: expr) :=  Eop Oaddf (e1 ::: e2 ::: Enil).
 Definition subf (e1 e2: expr) :=  Eop Osubf (e1 ::: e2 ::: Enil).
 Definition mulf (e1 e2: expr) :=  Eop Omulf (e1 ::: e2 ::: Enil).
 
+Definition negfs (e: expr) :=  Eop Onegfs (e ::: Enil).
+Definition absfs (e: expr) :=  Eop Oabsfs (e ::: Enil).
+Definition addfs (e1 e2: expr) :=  Eop Oaddfs (e1 ::: e2 ::: Enil).
+Definition subfs (e1 e2: expr) :=  Eop Osubfs (e1 ::: e2 ::: Enil).
+Definition mulfs (e1 e2: expr) :=  Eop Omulfs (e1 ::: e2 ::: Enil).
+
 (** ** Comparisons *)
 
 Nondetfunction compimm (default: comparison -> int -> condition)
@@ -405,6 +411,9 @@ Nondetfunction compu (c: comparison) (e1: expr) (e2: expr) :=
 Definition compf (c: comparison) (e1: expr) (e2: expr) :=
   Eop (Ocmp (Ccompf c)) (e1 ::: e2 ::: Enil).
 
+Definition compfs (c: comparison) (e1: expr) (e2: expr) :=
+  Eop (Ocmp (Ccompfs c)) (e1 ::: e2 ::: Enil).
+
 (** ** Integer conversions *)
 
 Nondetfunction cast8unsigned (e: expr) := 
@@ -446,32 +455,50 @@ Nondetfunction cast16signed (e: expr) :=
 (** Floating-point conversions *)
 
 Definition singleoffloat (e: expr) := Eop Osingleoffloat (e ::: Enil).
+Definition floatofsingle (e: expr) := Eop Ofloatofsingle (e ::: Enil).
+
 Definition intoffloat (e: expr) := Eop Ointoffloat (e ::: Enil).
 
 Nondetfunction floatofint (e: expr) :=
   match e with
-  | Eop (Ointconst n) Enil => Eop (Ofloatconst (Float.floatofint n)) Enil
+  | Eop (Ointconst n) Enil => Eop (Ofloatconst (Float.of_int n)) Enil
   | _ => Eop Ofloatofint (e ::: Enil)
   end.
 
 Definition intuoffloat (e: expr) :=
   Elet e
-    (Elet (Eop (Ofloatconst (Float.floatofintu Float.ox8000_0000)) Enil)
+    (Elet (Eop (Ofloatconst (Float.of_intu Float.ox8000_0000)) Enil)
       (Econdition (CEcond (Ccompf Clt) (Eletvar 1 ::: Eletvar 0 ::: Enil))
         (intoffloat (Eletvar 1))
         (addimm Float.ox8000_0000 (intoffloat (subf (Eletvar 1) (Eletvar 0))))))%nat.
 
 Nondetfunction floatofintu (e: expr) :=
   match e with
-  | Eop (Ointconst n) Enil => Eop (Ofloatconst (Float.floatofintu n)) Enil
+  | Eop (Ointconst n) Enil => Eop (Ofloatconst (Float.of_intu n)) Enil
   | _ =>
-    let f := Eop (Ofloatconst (Float.floatofintu Float.ox8000_0000)) Enil in
+    let f := Eop (Ofloatconst (Float.of_intu Float.ox8000_0000)) Enil in
     Elet e
       (Econdition (CEcond (Ccompuimm Clt Float.ox8000_0000) (Eletvar O ::: Enil))
         (floatofint (Eletvar O))
         (addf (floatofint (addimm (Int.neg Float.ox8000_0000) (Eletvar O))) f))
   end.
 
+Definition intofsingle (e: expr) := Eop Ointofsingle (e ::: Enil).
+
+Nondetfunction singleofint (e: expr) :=
+  match e with
+  | Eop (Ointconst n) Enil => Eop (Osingleconst (Float32.of_int n)) Enil
+  | _ => Eop Osingleofint (e ::: Enil)
+  end.
+
+Definition intuofsingle (e: expr) := intuoffloat (floatofsingle e).
+
+Nondetfunction singleofintu (e: expr) :=
+  match e with
+  | Eop (Ointconst n) Enil => Eop (Osingleconst (Float32.of_intu n)) Enil
+  | _ => singleoffloat (floatofintu e)
+  end.
+
 (** ** Addressing modes *)
 
 Nondetfunction addressing (chunk: memory_chunk) (e: expr) :=