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, 15 insertions, 0 deletions

diff --git a/backend/Selection.v b/backend/Selection.v
index f62a888e..9bd37ef5 100644
--- a/backend/Selection.v
+++ b/backend/Selection.v
@@ -70,6 +70,7 @@ Definition sel_constant (cst: Cminor.constant) : expr :=
   match cst with
   | Cminor.Ointconst n => Eop (Ointconst n) Enil
   | Cminor.Ofloatconst f => Eop (Ofloatconst f) Enil
+  | Cminor.Osingleconst f => Eop (Osingleconst f) Enil
   | Cminor.Olongconst n => longconst n
   | Cminor.Oaddrsymbol id ofs => addrsymbol id ofs
   | Cminor.Oaddrstack ofs => addrstack ofs
@@ -85,11 +86,18 @@ Definition sel_unop (op: Cminor.unary_operation) (arg: expr) : expr :=
   | Cminor.Onotint => notint arg
   | Cminor.Onegf => negf arg
   | Cminor.Oabsf => absf arg
+  | Cminor.Onegfs => negfs arg
+  | Cminor.Oabsfs => absfs arg
   | Cminor.Osingleoffloat => singleoffloat arg
+  | Cminor.Ofloatofsingle => floatofsingle arg
   | Cminor.Ointoffloat => intoffloat arg
   | Cminor.Ointuoffloat => intuoffloat arg
   | Cminor.Ofloatofint => floatofint arg
   | Cminor.Ofloatofintu => floatofintu arg
+  | Cminor.Ointofsingle => intofsingle arg
+  | Cminor.Ointuofsingle => intuofsingle arg
+  | Cminor.Osingleofint => singleofint arg
+  | Cminor.Osingleofintu => singleofintu arg
   | Cminor.Onegl => negl hf arg
   | Cminor.Onotl => notl arg
   | Cminor.Ointoflong => intoflong arg
@@ -99,6 +107,8 @@ Definition sel_unop (op: Cminor.unary_operation) (arg: expr) : expr :=
   | Cminor.Olonguoffloat => longuoffloat hf arg
   | Cminor.Ofloatoflong => floatoflong hf arg
   | Cminor.Ofloatoflongu => floatoflongu hf arg
+  | Cminor.Olongofsingle => longofsingle hf arg
+  | Cminor.Olonguofsingle => longuofsingle hf arg
   | Cminor.Osingleoflong => singleoflong hf arg
   | Cminor.Osingleoflongu => singleoflongu hf arg
   end.
@@ -122,6 +132,10 @@ Definition sel_binop (op: Cminor.binary_operation) (arg1 arg2: expr) : expr :=
   | Cminor.Osubf => subf arg1 arg2
   | Cminor.Omulf => mulf arg1 arg2
   | Cminor.Odivf => divf arg1 arg2
+  | Cminor.Oaddfs => addfs arg1 arg2
+  | Cminor.Osubfs => subfs arg1 arg2
+  | Cminor.Omulfs => mulfs arg1 arg2
+  | Cminor.Odivfs => divfs arg1 arg2
   | Cminor.Oaddl => addl hf arg1 arg2
   | Cminor.Osubl => subl hf arg1 arg2
   | Cminor.Omull => mull hf arg1 arg2
@@ -138,6 +152,7 @@ Definition sel_binop (op: Cminor.binary_operation) (arg1 arg2: expr) : expr :=
   | Cminor.Ocmp c => comp c arg1 arg2
   | Cminor.Ocmpu c => compu c arg1 arg2
   | Cminor.Ocmpf c => compf c arg1 arg2
+  | Cminor.Ocmpfs c => compfs c arg1 arg2
   | Cminor.Ocmpl c => cmpl c arg1 arg2
   | Cminor.Ocmplu c => cmplu c arg1 arg2
   end.