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, 6 insertions, 26 deletions

diff --git a/powerpc/SelectOp.vp b/powerpc/SelectOp.vp
index 7b15ccc8..bc9b6772 100644
--- a/powerpc/SelectOp.vp
+++ b/powerpc/SelectOp.vp
@@ -290,8 +290,6 @@ Nondetfunction xor (e1: expr) (e2: expr) :=
 
 (** ** Integer division and modulus *)
 
-Definition divs (e1: expr) (e2: expr) := Eop Odiv (e1:::e2:::Enil).
-
 Definition mod_aux (divop: operation) (e1 e2: expr) :=
   Elet e1
     (Elet (lift e2)
@@ -301,31 +299,13 @@ Definition mod_aux (divop: operation) (e1 e2: expr) :=
                            Enil) :::
                  Enil))).
 
-Definition mods := mod_aux Odiv.
-
-Definition divuimm (e: expr) (n: int) :=
-  match Int.is_power2 n with
-  | Some l => shruimm e l
-  | None   => Eop Odivu (e ::: Eop (Ointconst n) Enil ::: Enil)
-  end.
-
-Nondetfunction divu (e1: expr) (e2: expr) :=
-  match e2 with
-  | Eop (Ointconst n2) Enil => divuimm e1 n2
-  | _ => Eop Odivu (e1:::e2:::Enil)
-  end.
-
-Definition moduimm (e: expr) (n: int) :=
-  match Int.is_power2 n with
-  | Some l => andimm (Int.sub n Int.one) e
-  | None   => mod_aux Odivu e (Eop (Ointconst n) Enil)
-  end.
+Definition divs_base (e1: expr) (e2: expr) := Eop Odiv (e1:::e2:::Enil).
+Definition mods_base := mod_aux Odiv.
+Definition divu_base (e1: expr) (e2: expr) := Eop Odivu (e1:::e2:::Enil).
+Definition modu_base := mod_aux Odivu.
 
-Nondetfunction modu (e1: expr) (e2: expr) :=
-  match e2 with
-  | Eop (Ointconst n2) Enil => moduimm e1 n2
-  | _ => mod_aux Odivu e1 e2
-  end.
+Definition shrximm (e1: expr) (n2: int) :=
+  if Int.eq n2 Int.zero then e1 else Eop (Oshrximm n2) (e1:::Enil).
 
 (** ** General shifts *)