From c8a892a09e9f61c3af7dae30d39509558f77462a Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Wed, 28 May 2014 14:55:10 +0000
Subject: Instead of having two expansions of shrximm (one in SelectOp, one in
 Asmgen), move the most efficient expansion to Asmgen.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2504 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 arm/SelectOp.vp | 9 +--------
 1 file changed, 1 insertion(+), 8 deletions(-)

(limited to 'arm/SelectOp.vp')

diff --git a/arm/SelectOp.vp b/arm/SelectOp.vp
index efd9e482..e4005c92 100644
--- a/arm/SelectOp.vp
+++ b/arm/SelectOp.vp
@@ -291,14 +291,7 @@ Definition divu_base (e1: expr) (e2: expr) := Eop Odivu (e1:::e2:::Enil).
 Definition modu_base := mod_aux Odivu.
 
 Definition shrximm (e1: expr) (n2: int) :=
-  if Int.eq n2 Int.zero
-  then e1
-  else Elet e1
-         (shrimm
-             (add (Eletvar O)
-                  (shruimm (shrimm (Eletvar O) (Int.repr 31))
-                           (Int.sub Int.iwordsize n2)))
-             n2).
+  if Int.eq n2 Int.zero then e1 else Eop (Oshrximm n2) (e1:::Enil).
 
 (** ** General shifts *)
 
-- 
cgit