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
---
 backend/Selection.v | 15 +++++++++++++++
 1 file changed, 15 insertions(+)

(limited to 'backend/Selection.v')

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