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 --- ia32/SelectOp.vp | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) (limited to 'ia32/SelectOp.vp') diff --git a/ia32/SelectOp.vp b/ia32/SelectOp.vp index 2d1ab483..209147e3 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 *) -- cgit