From 576d79403ecb81d2be41e802790a5236f6fcf521 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Mon, 9 Jul 2012 13:43:41 +0000
Subject: Micro-optimization of (x & mask) >>s amount into a rolm when mask >=
 0.

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

(limited to 'powerpc/SelectOp.vp')

diff --git a/powerpc/SelectOp.vp b/powerpc/SelectOp.vp
index a1457df..d913958 100644
--- a/powerpc/SelectOp.vp
+++ b/powerpc/SelectOp.vp
@@ -179,12 +179,6 @@ Definition shlimm (e1: expr) (n2: int) :=
   else
     Eop Oshl (e1:::Eop (Ointconst n2) Enil:::Enil).
 
-Definition shrimm (e1: expr) (n2: int) :=
-  if Int.eq n2 Int.zero then
-    e1
-  else
-    Eop (Oshrimm n2) (e1:::Enil).
-
 Definition shruimm (e1: expr) (n2: int) :=
   if Int.eq n2 Int.zero then
     e1
@@ -193,6 +187,19 @@ Definition shruimm (e1: expr) (n2: int) :=
   else
     Eop Oshru (e1:::Eop (Ointconst n2) Enil:::Enil).
 
+Nondetfunction shrimm (e1: expr) (n2: int) :=
+  if Int.eq n2 Int.zero then
+    e1
+  else
+    match e1 with
+    | Eop (Oandimm mask1) (t1:::Enil) =>
+        if Int.lt mask1 Int.zero
+        then Eop (Oshrimm n2) (e1:::Enil)
+        else shruimm e1 n2
+    | _ =>
+        Eop (Oshrimm n2) (e1:::Enil)
+    end.
+
 (** ** Integer multiply *)
 
 Definition mulimm_base (n1: int) (e2: expr) :=
-- 
cgit v1.2.3