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, 14 insertions, 4 deletions

diff --git a/arm/Asmgen.v b/arm/Asmgen.v
index 6645149..3707b7f 100644
--- a/arm/Asmgen.v
+++ b/arm/Asmgen.v
@@ -299,12 +299,22 @@ Definition transl_op
       OK (if negb (ireg_eq r r1) then Pmla r r1 r2 r3 :: k
           else if negb (ireg_eq r r2) then Pmla r r2 r1 r3 :: k
           else Pmla IR14 r1 r2 r3 :: Pmov r (SOreg IR14) :: k)
-  | Odiv, a1 :: a2 :: nil =>
+  | Omulhs, a1 :: a2 :: nil =>
       do r <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
-      OK (Psdiv r r1 r2 :: k)
-  | Odivu, a1 :: a2 :: nil =>
+      OK (Psmull IR14 r r1 r2 :: k)
+  | Omulhu, a1 :: a2 :: nil =>
       do r <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
-      OK (Pudiv r r1 r2 :: k)
+      OK (Pumull IR14 r r1 r2 :: k)
+  | Odiv, a1 :: a2 :: nil =>
+      assertion (mreg_eq res R0);
+      assertion (mreg_eq a1 R0);
+      assertion (mreg_eq a2 R1);
+      OK (Psdiv :: k)
+  | Odivu, a1 :: a2 :: nil =>
+      assertion (mreg_eq res R0);
+      assertion (mreg_eq a1 R0);
+      assertion (mreg_eq a2 R1);
+      OK (Pudiv :: k)
   | Oand, a1 :: a2 :: nil =>
       do r <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
       OK (Pand r r1 (SOreg r2) :: k)