diff options
| author |  xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-07-09 13:43:41 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-07-09 13:43:41 +0000 |
| commit | 576d79403ecb81d2be41e802790a5236f6fcf521 (patch) | |
| tree | 7931c9338c6e80019021825f9a28b3116c17ad83 /powerpc/SelectOp.vp | |
| parent | c72b9a5bf321bfc05419eae50a5a27be03739bda (diff) | |
Micro-optimization of (x & mask) >>s amount into a rolm when mask >= 0.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1963 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'powerpc/SelectOp.vp')
| -rw-r--r-- | powerpc/SelectOp.vp | 19 |
1 files changed, 13 insertions, 6 deletions
diff --git a/powerpc/SelectOp.vp b/powerpc/SelectOp.vp index a1457df..d913958 100644 --- a/powerpc/SelectOp.vp +++ b/powerpc/SelectOp.vp @@ -179,12 +179,6 @@ Definition shlimm (e1: expr) (n2: int) := else Eop Oshl (e1:::Eop (Ointconst n2) Enil:::Enil). -Definition shrimm (e1: expr) (n2: int) := - if Int.eq n2 Int.zero then - e1 - else - Eop (Oshrimm n2) (e1:::Enil). - Definition shruimm (e1: expr) (n2: int) := if Int.eq n2 Int.zero then e1 @@ -193,6 +187,19 @@ Definition shruimm (e1: expr) (n2: int) := else Eop Oshru (e1:::Eop (Ointconst n2) Enil:::Enil). +Nondetfunction shrimm (e1: expr) (n2: int) := + if Int.eq n2 Int.zero then + e1 + else + match e1 with + | Eop (Oandimm mask1) (t1:::Enil) => + if Int.lt mask1 Int.zero + then Eop (Oshrimm n2) (e1:::Enil) + else shruimm e1 n2 + | _ => + Eop (Oshrimm n2) (e1:::Enil) + end. + (** ** Integer multiply *) Definition mulimm_base (n1: int) (e2: expr) := |