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
---
 arm/ConstpropOp.vp | 30 ++++++++++++++++++++++++------
 1 file changed, 24 insertions(+), 6 deletions(-)

(limited to 'arm/ConstpropOp.vp')

diff --git a/arm/ConstpropOp.vp b/arm/ConstpropOp.vp
index 2b658a4e..4f4bf5aa 100644
--- a/arm/ConstpropOp.vp
+++ b/arm/ConstpropOp.vp
@@ -70,6 +70,22 @@ Nondetfunction cond_strength_reduction
       if Float.eq_dec n2 Float.zero
       then (Cnotcompfzero c, r1 :: nil)
       else (cond, args)
+  | Ccompfs c, r1 :: r2 :: nil, FS n1 :: v2 :: nil =>
+      if Float32.eq_dec n1 Float32.zero
+      then (Ccompfszero (swap_comparison c), r2 :: nil)
+      else (cond, args)
+  | Ccompfs c, r1 :: r2 :: nil, v1 :: FS n2 :: nil =>
+      if Float32.eq_dec n2 Float32.zero
+      then (Ccompfszero c, r1 :: nil)
+      else (cond, args)
+  | Cnotcompfs c, r1 :: r2 :: nil, FS n1 :: v2 :: nil =>
+      if Float32.eq_dec n1 Float32.zero
+      then (Cnotcompfszero (swap_comparison c), r2 :: nil)
+      else (cond, args)
+  | Cnotcompfs c, r1 :: r2 :: nil, v1 :: FS n2 :: nil =>
+      if Float32.eq_dec n2 Float32.zero
+      then (Cnotcompfszero c, r1 :: nil)
+      else (cond, args)
   | _, _, _ => 
       (cond, args)
   end.
@@ -164,18 +180,19 @@ Definition make_xorimm (n: int) (r: reg) :=
   else (Oxorimm n, r :: nil).
 
 Definition make_mulfimm (n: float) (r r1 r2: reg) :=
-  if Float.eq_dec n (Float.floatofint (Int.repr 2))
+  if Float.eq_dec n (Float.of_int (Int.repr 2))
   then (Oaddf, r :: r :: nil)
   else (Omulf, r1 :: r2 :: nil).
 
+Definition make_mulfsimm (n: float32) (r r1 r2: reg) :=
+  if Float32.eq_dec n (Float32.of_int (Int.repr 2))
+  then (Oaddfs, r :: r :: nil)
+  else (Omulfs, r1 :: r2 :: nil).
+
 Definition make_cast8signed (r: reg) (a: aval) :=
   if vincl a (Sgn 8) then (Omove, r :: nil) else (Ocast8signed, r :: nil).
 Definition make_cast16signed (r: reg) (a: aval) :=
   if vincl a (Sgn 16) then (Omove, r :: nil) else (Ocast16signed, r :: nil).
-Definition make_singleoffloat (r: reg) (a: aval) :=
-  if vincl a Fsingle && generate_float_constants tt
-  then (Omove, r :: nil)
-  else (Osingleoffloat, r :: nil).
 
 Nondetfunction op_strength_reduction 
               (op: operation) (args: list reg) (vl: list aval) :=
@@ -207,10 +224,11 @@ Nondetfunction op_strength_reduction
   | Oshl, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_shlimm n2 r1 r2
   | Oshr, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_shrimm n2 r1 r2
   | Oshru, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_shruimm n2 r1 r2
-  | Osingleoffloat, r1 :: nil, v1 :: nil => make_singleoffloat r1 v1
   | Ocmp c, args, vl => make_cmp c args vl
   | Omulf, r1 :: r2 :: nil, v1 :: F n2 :: nil => make_mulfimm n2 r1 r1 r2
   | Omulf, r1 :: r2 :: nil, F n1 :: v2 :: nil => make_mulfimm n1 r2 r1 r2
+  | Omulfs, r1 :: r2 :: nil, v1 :: FS n2 :: nil => make_mulfsimm n2 r1 r1 r2
+  | Omulfs, r1 :: r2 :: nil, FS n1 :: v2 :: nil => make_mulfsimm n1 r2 r1 r2
   | _, _, _ => (op, args)
   end.
 
-- 
cgit