From 41b7ecb127b93b1aecc29a298ec21dc94603e6fa Mon Sep 17 00:00:00 2001 From: xleroy Date: Mon, 29 Jul 2013 12:10:11 +0000 Subject: 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 --- arm/Asmgen.v | 18 ++++++++++++++---- 1 file changed, 14 insertions(+), 4 deletions(-) (limited to 'arm/Asmgen.v') diff --git a/arm/Asmgen.v b/arm/Asmgen.v index 66451490..3707b7f2 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) -- cgit