summaryrefslogtreecommitdiff
path: root/powerpc/ConstpropOp.vp
diff options
context:
space:
mode:
authorGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2014-04-09 13:26:16 +0000
committerGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2014-04-09 13:26:16 +0000
commit336a1f906a9c617e68e9d43e244bf42e9bdbae64 (patch)
tree47c65aa1aa9c9eadbd98ec0e443ad0105bb0b268 /powerpc/ConstpropOp.vp
parent76f49ca6af4ffbc77c0ba7965d409c3de04011bd (diff)
Constprop: use "not" for "xorimm(-1)"; optimize == 1 and != 0 comparisons over booleans.
Select*: more systematic constant propagation; don't CP shifts by amounts outside of [0..31]. Driver: timer for whole compilation. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2452 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'powerpc/ConstpropOp.vp')
-rw-r--r--powerpc/ConstpropOp.vp24
1 files changed, 20 insertions, 4 deletions
diff --git a/powerpc/ConstpropOp.vp b/powerpc/ConstpropOp.vp
index 6aa0925..e1e1960 100644
--- a/powerpc/ConstpropOp.vp
+++ b/powerpc/ConstpropOp.vp
@@ -46,6 +46,23 @@ Nondetfunction cond_strength_reduction
(cond, args)
end.
+Definition make_cmp_base (c: condition) (args: list reg) (vl: list aval) :=
+ let (c', args') := cond_strength_reduction c args vl in (Ocmp c', args').
+
+Nondetfunction make_cmp (c: condition) (args: list reg) (vl: list aval) :=
+ match c, args, vl with
+ | Ccompimm Ceq n, r1 :: nil, v1 :: nil =>
+ if Int.eq_dec n Int.one && vincl v1 (Uns 1) then (Omove, r1 :: nil)
+ else if Int.eq_dec n Int.zero && vincl v1 (Uns 1) then (Oxorimm Int.one, r1 :: nil)
+ else make_cmp_base c args vl
+ | Ccompimm Cne n, r1 :: nil, v1 :: nil =>
+ if Int.eq_dec n Int.zero && vincl v1 (Uns 1) then (Omove, r1 :: nil)
+ else if Int.eq_dec n Int.one && vincl v1 (Uns 1) then (Oxorimm Int.one, r1 :: nil)
+ else make_cmp_base c args vl
+ | _, _, _ =>
+ make_cmp_base c args vl
+ end.
+
Definition make_addimm (n: int) (r: reg) :=
if Int.eq n Int.zero
then (Omove, r :: nil)
@@ -114,8 +131,8 @@ Definition make_orimm (n: int) (r: reg) :=
else (Oorimm n, r :: nil).
Definition make_xorimm (n: int) (r: reg) :=
- if Int.eq n Int.zero
- then (Omove, r :: nil)
+ if Int.eq n Int.zero then (Omove, r :: nil)
+ else if Int.eq n Int.mone then (Onot, r :: nil)
else (Oxorimm n, r :: nil).
Definition make_mulfimm (n: float) (r r1 r2: reg) :=
@@ -158,8 +175,7 @@ Nondetfunction op_strength_reduction
| Oshr, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_shrimm n2 r1 r2
| Oshru, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_shruimm n2 r1 r2
| Osingleoffloat, r1 :: nil, v1 :: nil => make_singleoffloat r1 v1
- | Ocmp c, args, vl =>
- let (c', args') := cond_strength_reduction c args vl in (Ocmp c', args')
+ | Ocmp c, args, vl => make_cmp c args vl
| Omulf, r1 :: r2 :: nil, v1 :: F n2 :: nil => make_mulfimm n2 r1 r1 r2
| Omulf, r1 :: r2 :: nil, F n1 :: v2 :: nil => make_mulfimm n1 r2 r1 r2
| _, _, _ => (op, args)