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/SelectOp.vp | 41 ++++++++++++++--------------------------- 1 file changed, 14 insertions(+), 27 deletions(-) (limited to 'arm/SelectOp.vp') diff --git a/arm/SelectOp.vp b/arm/SelectOp.vp index d81328b0..4cd09d1b 100644 --- a/arm/SelectOp.vp +++ b/arm/SelectOp.vp @@ -272,33 +272,20 @@ Definition mod_aux (divop: operation) (e1 e2: expr) := Enil) ::: Enil))). -Definition divs (e1: expr) (e2: expr) := Eop Odiv (e1:::e2:::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 => Eop (Oandimm (Int.sub n Int.one)) (e ::: Enil) - | None => mod_aux Odivu e (Eop (Ointconst n) Enil) - end. - -Nondetfunction modu (e1: expr) (e2: expr) := - match e2 with - | Eop (Ointconst n2) Enil => moduimm e1 n2 - | _ => mod_aux Odivu e1 e2 - 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. + +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). (** ** General shifts *) -- cgit