From 336a1f906a9c617e68e9d43e244bf42e9bdbae64 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Wed, 9 Apr 2014 13:26:16 +0000
Subject: Constprop: use "not" for "xorimm(-1)"; optimize == 1 and != 0
 comparisons over booleans. Select*: more systematic constant propagation;
 don't CP shifts by amounts outside of [0..31]. Driver: timer for whole
 compilation.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2452 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 powerpc/SelectOp.vp | 57 +++++++++++++++++++++++++++++++++++++++++++----------
 1 file changed, 47 insertions(+), 10 deletions(-)

(limited to 'powerpc/SelectOp.vp')

diff --git a/powerpc/SelectOp.vp b/powerpc/SelectOp.vp
index ad4f3b92..371a08a4 100644
--- a/powerpc/SelectOp.vp
+++ b/powerpc/SelectOp.vp
@@ -68,6 +68,7 @@ Nondetfunction notint (e: expr) :=
   | Eop Onxor (t1:::t2:::Enil) => Eop Oxor (t1:::t2:::Enil)
   | Eop Oandc (t1:::t2:::Enil) => Eop Oorc (t2:::t1:::Enil)
   | Eop Oorc (t1:::t2:::Enil) => Eop Oandc (t2:::t1:::Enil)
+  | Eop (Oxorimm n) (t1:::Enil) => Eop (Oxorimm (Int.not n)) (t1:::Enil)
   | _ => Eop Onot (e:::Enil)
   end.
 
@@ -121,10 +122,22 @@ Nondetfunction add (e1: expr) (e2: expr) :=
 
 (** ** Integer and pointer subtraction *)
 
+Nondetfunction subimm (n1: int) (e: expr) :=
+  match e with
+  | Eop (Ointconst n2) Enil =>
+      Eop (Ointconst (Int.sub n1 n2)) Enil
+  | Eop (Oaddimm n2) (t2:::Enil) =>
+      Eop (Osubimm (Int.sub n1 n2)) (t2 ::: Enil)
+  | _ =>
+      Eop (Osubimm n1) (e ::: Enil)
+  end.
+
 Nondetfunction sub (e1: expr) (e2: expr) :=
   match e1, e2 with
   | t1, Eop (Ointconst n2) Enil =>
       addimm (Int.neg n2) t1
+  | Eop (Ointconst n1) Enil, t2 =>
+      subimm n1 t2
   | Eop (Oaddimm n1) (t1:::Enil), Eop (Oaddimm n2) (t2:::Enil) =>
       addimm (Int.sub n1 n2) (Eop Osub (t1:::t2:::Enil))
   | Eop (Oaddimm n1) (t1:::Enil), t2 =>
@@ -135,7 +148,7 @@ Nondetfunction sub (e1: expr) (e2: expr) :=
       Eop Osub (e1:::e2:::Enil)
   end.
 
-Definition negint (e: expr) := Eop (Osubimm Int.zero) (e ::: Enil).
+Definition negint (e: expr) := subimm Int.zero e.
 
 (** ** Rotates and immediate shifts *)
 
@@ -174,8 +187,12 @@ Definition shruimm (e1: expr) (n2: int) :=
 Nondetfunction shrimm (e1: expr) (n2: int) :=
   if Int.eq n2 Int.zero then
     e1
+  else if negb (Int.ltu n2 Int.iwordsize) then
+    Eop Oshr (e1:::Eop (Ointconst n2) Enil:::Enil)
   else
     match e1 with
+    | Eop (Ointconst n1) Enil =>
+        Eop (Ointconst (Int.shr n1 n2)) Enil
     | Eop (Oandimm mask1) (t1:::Enil) =>
         if Int.lt mask1 Int.zero
         then Eop (Oshrimm n2) (e1:::Enil)
@@ -293,9 +310,11 @@ Nondetfunction or (e1: expr) (e2: expr) :=
 
 Nondetfunction xorimm (n1: int) (e2: expr) :=
   if Int.eq n1 Int.zero then e2 else
+  if Int.eq n1 Int.mone then notint e2 else
   match e2 with
   | Eop (Ointconst n2) Enil => Eop (Ointconst (Int.xor n1 n2)) Enil
   | Eop (Oxorimm n2) (t2:::Enil) => Eop (Oxorimm (Int.xor n1 n2)) (t2:::Enil)
+  | Eop Onot (t2:::Enil) => Eop (Oxorimm (Int.not n1)) (t2:::Enil)
   | _ => Eop (Oxorimm n1) (e2:::Enil)
   end.
 
@@ -418,11 +437,19 @@ Definition compf (c: comparison) (e1: expr) (e2: expr) :=
 
 Definition cast8unsigned (e: expr) := andimm (Int.repr 255) e.
 
-Definition cast8signed (e: expr) := Eop Ocast8signed (e ::: Enil).
+Nondetfunction cast8signed (e: expr) :=
+  match e with
+  | Eop (Ointconst n) Enil => Eop (Ointconst (Int.sign_ext 8 n)) Enil
+  | _ => Eop Ocast8signed (e ::: Enil)
+  end.
 
 Definition cast16unsigned (e: expr) := andimm (Int.repr 65535) e.
 
-Definition cast16signed (e: expr) := Eop Ocast16signed (e ::: Enil).
+Nondetfunction cast16signed (e: expr) :=
+  match e with
+  | Eop (Ointconst n) Enil => Eop (Ointconst (Int.sign_ext 16 n)) Enil
+  | _ => Eop Ocast16signed (e ::: Enil)
+  end.
 
 (** ** Floating-point conversions *)
 
@@ -435,14 +462,24 @@ Definition intuoffloat (e: expr) :=
       (intoffloat (Eletvar 1))
       (addimm Float.ox8000_0000 (intoffloat (subf (Eletvar 1) (Eletvar 0))))))%nat.
 
-Definition floatofintu (e: expr) :=
-  subf (Eop Ofloatofwords (Eop (Ointconst Float.ox4330_0000) Enil ::: e ::: Enil))
-       (Eop (Ofloatconst (Float.from_words Float.ox4330_0000 Int.zero)) Enil).
+Nondetfunction floatofintu (e: expr) :=
+  match e with
+  | Eop (Ointconst n) Enil =>
+      Eop (Ofloatconst (Float.floatofintu n)) Enil
+  | _ =>
+      subf (Eop Ofloatofwords (Eop (Ointconst Float.ox4330_0000) Enil ::: e ::: Enil))
+           (Eop (Ofloatconst (Float.from_words Float.ox4330_0000 Int.zero)) Enil)
+  end.
 
-Definition floatofint (e: expr) :=
-  subf (Eop Ofloatofwords (Eop (Ointconst Float.ox4330_0000) Enil
-                           ::: addimm Float.ox8000_0000 e ::: Enil))
-       (Eop (Ofloatconst (Float.from_words Float.ox4330_0000 Float.ox8000_0000)) Enil).
+Nondetfunction floatofint (e: expr) :=
+  match e with
+  | Eop (Ointconst n) Enil =>
+      Eop (Ofloatconst (Float.floatofint n)) Enil
+  | _ =>
+      subf (Eop Ofloatofwords (Eop (Ointconst Float.ox4330_0000) Enil
+                               ::: addimm Float.ox8000_0000 e ::: Enil))
+           (Eop (Ofloatconst (Float.from_words Float.ox4330_0000 Float.ox8000_0000)) Enil)
+  end.
 
 Definition singleoffloat (e: expr) := Eop Osingleoffloat (e ::: Enil).
 
-- 
cgit