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

(limited to 'powerpc/ConstpropOp.vp')

diff --git a/powerpc/ConstpropOp.vp b/powerpc/ConstpropOp.vp
index 6aa09254..e1e19601 100644
--- a/powerpc/ConstpropOp.vp
+++ b/powerpc/ConstpropOp.vp
@@ -46,6 +46,23 @@ Nondetfunction cond_strength_reduction
       (cond, args)
   end.
 
+Definition make_cmp_base (c: condition) (args: list reg) (vl: list aval) :=
+  let (c', args') := cond_strength_reduction c args vl in (Ocmp c', args').
+
+Nondetfunction make_cmp (c: condition) (args: list reg) (vl: list aval) :=
+  match c, args, vl with
+  | Ccompimm Ceq n, r1 :: nil, v1 :: nil =>
+      if Int.eq_dec n Int.one && vincl v1 (Uns 1) then (Omove, r1 :: nil)
+      else if Int.eq_dec n Int.zero && vincl v1 (Uns 1) then (Oxorimm Int.one, r1 :: nil)
+      else make_cmp_base c args vl
+  | Ccompimm Cne n, r1 :: nil, v1 :: nil =>
+      if Int.eq_dec n Int.zero && vincl v1 (Uns 1) then (Omove, r1 :: nil)
+      else if Int.eq_dec n Int.one && vincl v1 (Uns 1) then (Oxorimm Int.one, r1 :: nil)
+      else make_cmp_base c args vl
+  | _, _, _ =>
+      make_cmp_base c args vl
+  end.
+
 Definition make_addimm (n: int) (r: reg) :=
   if Int.eq n Int.zero
   then (Omove, r :: nil)
@@ -114,8 +131,8 @@ Definition make_orimm (n: int) (r: reg) :=
   else (Oorimm n, r :: nil).
 
 Definition make_xorimm (n: int) (r: reg) :=
-  if Int.eq n Int.zero
-  then (Omove, r :: nil)
+  if Int.eq n Int.zero then (Omove, r :: nil)
+  else if Int.eq n Int.mone then (Onot, r :: nil)
   else (Oxorimm n, r :: nil).
 
 Definition make_mulfimm (n: float) (r r1 r2: reg) :=
@@ -158,8 +175,7 @@ Nondetfunction op_strength_reduction
   | 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 =>
-      let (c', args') := cond_strength_reduction c args vl in (Ocmp c', args')
+  | 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
   | _, _, _ => (op, args)
-- 
cgit