aboutsummaryrefslogtreecommitdiffstats
path: root/powerpc/ConstpropOp.vp
diff options
context:
space:
mode:
authorXavier Leroy <xavierleroy@users.noreply.github.com>2018-02-16 10:38:15 +0100
committerGitHub <noreply@github.com>2018-02-16 10:38:15 +0100
commit16608ca8c91d51fb48a6a55f22d392420d727b63 (patch)
tree399276d97a2442a854f4bc277e22d51fab69b128 /powerpc/ConstpropOp.vp
parentd2c5701fb538ec175b3fa2266d795ba63d795b3b (diff)
downloadcompcert-kvx-16608ca8c91d51fb48a6a55f22d392420d727b63.tar.gz
compcert-kvx-16608ca8c91d51fb48a6a55f22d392420d727b63.zip
Improve strength reduction of unsigned comparisons x ==u 0, x !=u 0, etc (#59)
When x is known to be either 0 or 1, comparisons such as x == 0 x != 0 x == 1 x != 1 can be optimized away. This optimization was already performed for signed comparisons. This commit extends the optimization to unsigned comparisons as well. Additionally, for PowerPC only, some unsigned (dis)equality comparisons are turned into signed comparisons when we know it makes no difference, i.e. when both arguments are guaranteed not to be pointers. The reason is that Asmgen can produce shorter instruction sequences for some signed equality comparisons than for the corresponding unsigned comparisons. It's important to optimize unsigned integer comparisons because casts to the C99 type _Bool are compiled as x !=u 0 unsigned comparisons. In particular, cascades of casts to _Bool are now reduced to a single cast much more often than before.
Diffstat (limited to 'powerpc/ConstpropOp.vp')
-rw-r--r--powerpc/ConstpropOp.vp16
1 files changed, 16 insertions, 0 deletions
diff --git a/powerpc/ConstpropOp.vp b/powerpc/ConstpropOp.vp
index f18a72e9..2d492b66 100644
--- a/powerpc/ConstpropOp.vp
+++ b/powerpc/ConstpropOp.vp
@@ -65,6 +65,12 @@ Nondetfunction cond_strength_reduction
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').
+Definition is_an_integer (v: aval) : bool :=
+ match v with
+ | Vbot | I _ | Uns _ _ | Sgn _ _ => true
+ | _ => false
+ end.
+
Nondetfunction make_cmp (c: condition) (args: list reg) (vl: list aval) :=
match c, args, vl with
| Ccompimm Ceq n, r1 :: nil, v1 :: nil =>
@@ -75,6 +81,16 @@ Nondetfunction make_cmp (c: condition) (args: list reg) (vl: list aval) :=
if Int.eq_dec n Int.zero && vincl v1 (Uns Ptop 1) then (Omove, r1 :: nil)
else if Int.eq_dec n Int.one && vincl v1 (Uns Ptop 1) then (Oxorimm Int.one, r1 :: nil)
else make_cmp_base c args vl
+ | Ccompuimm Ceq n, r1 :: nil, v1 :: nil =>
+ if Int.eq_dec n Int.one && vincl v1 (Uns Ptop 1) then (Omove, r1 :: nil)
+ else if Int.eq_dec n Int.zero && vincl v1 (Uns Ptop 1) then (Oxorimm Int.one, r1 :: nil)
+ else if is_an_integer v1 then make_cmp_base (Ccompimm Ceq n) args vl
+ else make_cmp_base c args vl
+ | Ccompuimm Cne n, r1 :: nil, v1 :: nil =>
+ if Int.eq_dec n Int.zero && vincl v1 (Uns Ptop 1) then (Omove, r1 :: nil)
+ else if Int.eq_dec n Int.one && vincl v1 (Uns Ptop 1) then (Oxorimm Int.one, r1 :: nil)
+ else if is_an_integer v1 then make_cmp_base (Ccompimm Cne n) args vl
+ else make_cmp_base c args vl
| _, _, _ =>
make_cmp_base c args vl
end.