Optimize integer divisions by positive constants, turning them into

multiply-high and shifts.


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2300 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 7 insertions, 4 deletions

diff --git a/ia32/SelectOp.vp b/ia32/SelectOp.vp
index 2d1ab48..209147e 100644
--- a/ia32/SelectOp.vp
+++ b/ia32/SelectOp.vp
@@ -299,10 +299,13 @@ Nondetfunction xor (e1: expr) (e2: expr) :=
 
 (** ** Integer division and modulus *)
 
-Definition divu (e1: expr) (e2: expr) := Eop Odivu (e1:::e2:::Enil).
-Definition modu (e1: expr) (e2: expr) := Eop Omodu (e1:::e2:::Enil).
-Definition divs (e1: expr) (e2: expr) := Eop Odiv (e1:::e2:::Enil).
-Definition mods (e1: expr) (e2: expr) := Eop Omod (e1:::e2:::Enil).
+Definition divu_base (e1: expr) (e2: expr) := Eop Odivu (e1:::e2:::Enil).
+Definition modu_base (e1: expr) (e2: expr) := Eop Omodu (e1:::e2:::Enil).
+Definition divs_base (e1: expr) (e2: expr) := Eop Odiv (e1:::e2:::Enil).
+Definition mods_base (e1: expr) (e2: expr) := Eop Omod (e1:::e2:::Enil).
+
+Definition shrximm (e1: expr) (n2: int) :=
+  if Int.eq n2 Int.zero then e1 else Eop (Oshrximm n2) (e1:::Enil).
 
 (** ** General shifts *)