1;; `icmp`-related rewrites
2
3;; `x == x` is always true for integers; `x != x` is false. Strict
4;; inequalities are false, and loose inequalities are true.
5(rule (simplify (eq  (ty_int ty) x x)) (subsume (iconst_u ty 1)))
6(rule (simplify (ne  (ty_int ty) x x)) (subsume (iconst_u ty 0)))
7(rule (simplify (ugt (ty_int ty) x x)) (subsume (iconst_u ty 0)))
8(rule (simplify (uge (ty_int ty) x x)) (subsume (iconst_u ty 1)))
9(rule (simplify (sgt (ty_int ty) x x)) (subsume (iconst_u ty 0)))
10(rule (simplify (sge (ty_int ty) x x)) (subsume (iconst_u ty 1)))
11(rule (simplify (ult (ty_int ty) x x)) (subsume (iconst_u ty 0)))
12(rule (simplify (ule (ty_int ty) x x)) (subsume (iconst_u ty 1)))
13(rule (simplify (slt (ty_int ty) x x)) (subsume (iconst_u ty 0)))
14(rule (simplify (sle (ty_int ty) x x)) (subsume (iconst_u ty 1)))
15
16;; For integers, adding the same thing on both sides of an equality check
17;; (or an inequality check) doesn't change the result.
18;; This applies for arbitrary expressions, not just constants, so we need to
19;; check all possible orderings since nothing normalizes it.
20
21(rule (simplify (eq ty (iadd _ a k) (iadd _ b k)))
22      (subsume (eq ty a b)))
23(rule (simplify (eq ty (iadd _ a k) (iadd _ k b)))
24      (subsume (eq ty a b)))
25(rule (simplify (eq ty (iadd _ k a) (iadd _ b k)))
26      (subsume (eq ty a b)))
27(rule (simplify (eq ty (iadd _ k a) (iadd _ k b)))
28      (subsume (eq ty a b)))
29(rule (simplify (ne ty (iadd _ a k) (iadd _ b k)))
30      (subsume (ne ty a b)))
31(rule (simplify (ne ty (iadd _ a k) (iadd _ k b)))
32      (subsume (ne ty a b)))
33(rule (simplify (ne ty (iadd _ k a) (iadd _ b k)))
34      (subsume (ne ty a b)))
35(rule (simplify (ne ty (iadd _ k a) (iadd _ k b)))
36      (subsume (ne ty a b)))
37
38;; To avoid repeating all the above rules again, normalize isub to iadd
39;; (a - b) == (c - d) ⟹ (a + d) == (c + b)
40
41(rule (simplify (eq ty1 (isub ty2 a b) (isub ty3 c d)))
42      (eq ty1 (iadd ty2 a d) (iadd ty3 c b)))
43(rule (simplify (ne ty1 (isub ty2 a b) (isub ty3 c d)))
44      (ne ty1 (iadd ty2 a d) (iadd ty3 c b)))
45
46;; Optimize icmp-of-icmp.
47;; ne(icmp(ty, cc, x, y), 0) == icmp(ty, cc, x, y)
48;; e.g. neq(ugt(x, y), 0) == ugt(x, y)
49(rule (simplify (ne ty
50                      (uextend_maybe _ inner @ (icmp ty _ _ _))
51                      (iconst_u _ 0)))
52      (subsume inner))
53
54;; Likewise for icmp-of-fcmp.
55;; ne(fcmp(ty, cc, x, y), 0) == fcmp(ty, cc, x, y)
56(rule (simplify (ne ty
57                      (uextend_maybe _ inner @ (fcmp ty _ _ _))
58                      (iconst_u _ 0)))
59      (subsume inner))
60
61;; eq(icmp(ty, cc, x, y), 0) == icmp(ty, cc_complement, x, y)
62;; e.g. eq(ugt(x, y), 0) == ule(x, y)
63(rule (simplify (eq ty
64                      (uextend_maybe _ (icmp ty cc x y))
65                      (iconst_u _ 0)))
66      (subsume (icmp ty (intcc_complement cc) x y)))
67
68;; ne(icmp(ty, cc, x, y), 1) == icmp(ty, cc_complement, x, y)
69;; e.g. ne(ugt(x, y), 1) == ule(x, y)
70(rule (simplify (ne ty
71                      (uextend_maybe _ (icmp ty cc x y))
72                      (iconst_u _ 1)))
73      (subsume (icmp ty (intcc_complement cc) x y)))
74
75;; eq(icmp(ty, cc, x, y), 1) == icmp(ty, cc, x, y)
76;; e.g. eq(ugt(x, y), 1) == ugt(x, y)
77(rule (simplify (eq ty
78                      (uextend_maybe _ inner @ (icmp _ _ _ _))
79                      (iconst_u _ 1)))
80      (subsume inner))
81
82;; Optimize select-of-uextend-of-icmp to select-of-icmp, because
83;; select can take an I8 condition too.
84(rule (simplify
85       (select ty (uextend _ c @ (icmp _ _ _ _)) x y))
86      (select ty c x y))
87(rule (simplify
88       (select ty (uextend _ c @ (icmp _ _ _ _)) x y))
89      (select ty c x y))
90
91;; Masking the result of a comparison with 1 always results in the comparison
92;; itself. Note that comparisons in wasm may sometimes be hidden behind
93;; extensions.
94(rule (simplify
95       (band (ty_int _)
96             cmp @ (icmp _ _ _ _)
97             (iconst_u _ 1)))
98      cmp)
99(rule (simplify
100       (band (ty_int _)
101             extend @ (uextend _ (icmp _ _ _ _))
102             (iconst_u _ 1)))
103      extend)
104
105;; Comparisons against largest/smallest signed/unsigned values:
106;; ult(x, 0) == false.
107(rule (simplify (ult (fits_in_64 (ty_int bty)) x zero @ (iconst_u _ 0)))
108      (subsume (iconst_u bty 0)))
109
110;; ule(x, 0) == eq(x, 0)
111(rule (simplify (ule (fits_in_64 (ty_int bty)) x zero @ (iconst_u _ 0)))
112      (eq bty x zero))
113
114;; ugt(x, 0) == ne(x, 0).
115(rule (simplify (ugt (fits_in_64 (ty_int bty)) x zero @ (iconst_u _ 0)))
116      (ne bty x zero))
117
118;; uge(x, 0) == true.
119(rule (simplify (uge (fits_in_64 (ty_int bty)) x zero @ (iconst_u _ 0)))
120      (subsume (iconst_u bty 1)))
121
122;; ult(x, UMAX) == ne(x, UMAX).
123(rule (simplify (ult (fits_in_64 (ty_int bty)) x umax @ (iconst_u cty y)))
124       (if-let true (u64_eq y (ty_umax cty)))
125       (ne bty x umax))
126
127;; ule(x, UMAX) == true.
128(rule (simplify (ule (fits_in_64 (ty_int bty)) x umax @ (iconst_u cty y)))
129       (if-let true (u64_eq y (ty_umax cty)))
130       (subsume (iconst_u bty 1)))
131
132;; ugt(x, UMAX) == false.
133(rule (simplify (ugt (fits_in_64 (ty_int bty)) x umax @ (iconst_u cty y)))
134       (if-let true (u64_eq y (ty_umax cty)))
135       (subsume (iconst_u bty 0)))
136
137;; uge(x, UMAX) == eq(x, UMAX).
138(rule (simplify (uge (fits_in_64 (ty_int bty)) x umax @ (iconst_u cty y)))
139       (if-let true (u64_eq y (ty_umax cty)))
140       (eq bty x umax))
141
142;; slt(x, SMIN) == false.
143(rule (simplify (slt (fits_in_64 (ty_int bty)) x smin @ (iconst_u cty y)))
144       (if-let true (u64_eq y (ty_smin cty)))
145       (subsume (iconst_u bty 0)))
146
147;; sle(x, SMIN) == eq(x, SMIN).
148(rule (simplify (sle (fits_in_64 (ty_int bty)) x smin @ (iconst_u cty y)))
149       (if-let true (u64_eq y (ty_smin cty)))
150       (eq bty x smin))
151
152;; sgt(x, SMIN) == ne(x, SMIN).
153(rule (simplify (sgt (fits_in_64 (ty_int bty)) x smin @ (iconst_u cty y)))
154       (if-let true (u64_eq y (ty_smin cty)))
155       (ne bty x smin))
156
157;; sge(x, SMIN) == true.
158(rule (simplify (sge (fits_in_64 (ty_int bty)) x smin @ (iconst_u cty y)))
159       (if-let true (u64_eq y (ty_smin cty)))
160       (subsume (iconst_u bty 1)))
161
162;; slt(x, SMAX) == ne(x, SMAX).
163(rule (simplify (slt (fits_in_64 (ty_int bty)) x smax @ (iconst_u cty y)))
164       (if-let true (u64_eq y (ty_smax cty)))
165       (ne bty x smax))
166
167;; sle(x, SMAX) == true.
168(rule (simplify (sle (fits_in_64 (ty_int bty)) x smax @ (iconst_u cty y)))
169       (if-let true (u64_eq y (ty_smax cty)))
170       (subsume (iconst_u bty 1)))
171
172;; sgt(x, SMAX) == false.
173(rule (simplify (sgt (fits_in_64 (ty_int bty)) x smax @ (iconst_u cty y)))
174       (if-let true (u64_eq y (ty_smax cty)))
175       (subsume (iconst_u bty 0)))
176
177;; sge(x, SMAX) == eq(x, SMAX).
178(rule (simplify (sge (fits_in_64 (ty_int bty)) x smax @ (iconst_u cty y)))
179       (if-let true (u64_eq y (ty_smax cty)))
180       (eq bty x smax))
181
182;; `band`/`bor` of 2 comparisons:
183(rule (simplify (band (fits_in_64 ty) (icmp ty cc1 x y) (icmp ty cc2 x y)))
184  (if-let signed (intcc_comparable cc1 cc2))
185  (compose_icmp ty (u64_and (decompose_intcc cc1) (decompose_intcc cc2)) signed x y))
186
187(rule (simplify (bor (fits_in_64 ty) (icmp ty cc1 x y) (icmp ty cc2 x y)))
188  (if-let signed (intcc_comparable cc1 cc2))
189  (compose_icmp ty (u64_or (decompose_intcc cc1) (decompose_intcc cc2)) signed x y))
190
191;; Prefer comparing against zero
192;; uge(x, 1) == ne(x, 0)
193(rule (simplify (uge ty x (iconst_u cty 1)))
194      (ne ty x (iconst_u cty 0)))
195;; ult(x, 1) == eq(x, 0)
196(rule (simplify (ult ty x (iconst_u cty 1)))
197      (eq ty x (iconst_u cty 0)))
198;; sge(x, 1) == sgt(x, 0)
199(rule (simplify (sge ty x (iconst_s cty 1)))
200      (sgt ty x (iconst_s cty 0)))
201;; slt(x, 1) == sle(x, 0)
202(rule (simplify (slt ty x (iconst_s cty 1)))
203      (sle ty x (iconst_s cty 0)))
204;; sgt(x, -1) == sge(x, 0)
205(rule (simplify (sgt ty x (iconst_s cty -1)))
206      (sge ty x (iconst_s cty 0)))
207;; sle(x, -1) == slt(x, 0)
208(rule (simplify (sle ty x (iconst_s cty -1)))
209      (slt ty x (iconst_s cty 0)))
210
211(decl pure partial intcc_comparable (IntCC IntCC) bool)
212(rule (intcc_comparable x y)
213  (if-let (u64_extract_non_zero class) (u64_and (intcc_class x) (intcc_class y)))
214  (u64_eq 2 class))
215
216(decl pure decompose_intcc (IntCC) u64)
217(rule (decompose_intcc (IntCC.Equal)) 1)
218(rule (decompose_intcc (IntCC.UnsignedLessThan)) 2)
219(rule (decompose_intcc (IntCC.SignedLessThan)) 2)
220(rule (decompose_intcc (IntCC.UnsignedLessThanOrEqual)) 3)
221(rule (decompose_intcc (IntCC.SignedLessThanOrEqual)) 3)
222(rule (decompose_intcc (IntCC.UnsignedGreaterThan)) 4)
223(rule (decompose_intcc (IntCC.SignedGreaterThan)) 4)
224(rule (decompose_intcc (IntCC.UnsignedGreaterThanOrEqual)) 5)
225(rule (decompose_intcc (IntCC.SignedGreaterThanOrEqual)) 5)
226(rule (decompose_intcc (IntCC.NotEqual)) 6)
227
228(decl compose_icmp (Type u64 bool Value Value) Value)
229(rule (compose_icmp ty 0 _ _ _) (subsume (iconst_u ty 0)))
230(rule (compose_icmp ty 1 _ x y) (icmp ty (IntCC.Equal) x y))
231(rule (compose_icmp ty 2 false x y) (icmp ty (IntCC.UnsignedLessThan) x y))
232(rule (compose_icmp ty 2 true x y) (icmp ty (IntCC.SignedLessThan) x y))
233(rule (compose_icmp ty 3 false x y) (icmp ty (IntCC.UnsignedLessThanOrEqual) x y))
234(rule (compose_icmp ty 3 true x y) (icmp ty (IntCC.SignedLessThanOrEqual) x y))
235(rule (compose_icmp ty 4 false x y) (icmp ty (IntCC.UnsignedGreaterThan) x y))
236(rule (compose_icmp ty 4 true x y) (icmp ty (IntCC.SignedGreaterThan) x y))
237(rule (compose_icmp ty 5 false x y) (icmp ty (IntCC.UnsignedGreaterThanOrEqual) x y))
238(rule (compose_icmp ty 5 true x y) (icmp ty (IntCC.SignedGreaterThanOrEqual) x y))
239(rule (compose_icmp ty 6 _ x y) (icmp ty (IntCC.NotEqual) x y))
240(rule (compose_icmp ty 7 _ _ _) (subsume (iconst_u ty 1)))
241
242(decl pure intcc_class (IntCC) u64)
243(rule (intcc_class (IntCC.UnsignedLessThan)) 1)
244(rule (intcc_class (IntCC.UnsignedLessThanOrEqual)) 1)
245(rule (intcc_class (IntCC.UnsignedGreaterThan)) 1)
246(rule (intcc_class (IntCC.UnsignedGreaterThanOrEqual)) 1)
247(rule (intcc_class (IntCC.SignedLessThan)) 2)
248(rule (intcc_class (IntCC.SignedLessThanOrEqual)) 2)
249(rule (intcc_class (IntCC.SignedGreaterThan)) 2)
250(rule (intcc_class (IntCC.SignedGreaterThanOrEqual)) 2)
251(rule (intcc_class (IntCC.Equal)) 3)
252(rule (intcc_class (IntCC.NotEqual)) 3)
253
254;; Pattern-match what LLVM emits today for 128-bit comparisons into actual
255;; 128-bit comparisons. Platforms like x64 and aarch64 have more optimal
256;; lowerings for 128-bit arithmetic than the default structure.
257(rule (simplify (select ty (eq _   a_hi @ (value_type $I64) b_hi @ (value_type $I64))
258                           (uge ty a_lo @ (value_type $I64) b_lo @ (value_type $I64))
259                           (uge ty a_hi b_hi)))
260      (uge ty (iconcat $I64 a_lo a_hi) (iconcat $I64 b_lo b_hi)))
261
262(rule (simplify (select ty (eq _   a_hi @ (value_type $I64) b_hi @ (value_type $I64))
263                           (uge ty a_lo @ (value_type $I64) b_lo @ (value_type $I64))
264                           (sge ty a_hi b_hi)))
265      (sge ty (iconcat $I64 a_lo a_hi) (iconcat $I64 b_lo b_hi)))
266
267(rule (simplify (select ty (eq _   a_hi @ (value_type $I64) b_hi @ (value_type $I64))
268                           (ugt ty a_lo @ (value_type $I64) b_lo @ (value_type $I64))
269                           (ugt ty a_hi b_hi)))
270      (ugt ty (iconcat $I64 a_lo a_hi) (iconcat $I64 b_lo b_hi)))
271
272(rule (simplify (select ty (eq _   a_hi @ (value_type $I64) b_hi @ (value_type $I64))
273                           (ugt ty a_lo @ (value_type $I64) b_lo @ (value_type $I64))
274                           (sgt ty a_hi b_hi)))
275      (sgt ty (iconcat $I64 a_lo a_hi) (iconcat $I64 b_lo b_hi)))
276
277(rule (simplify (select ty (eq _   a_hi @ (value_type $I64) b_hi @ (value_type $I64))
278                           (ule ty a_lo @ (value_type $I64) b_lo @ (value_type $I64))
279                           (ule ty a_hi b_hi)))
280      (ule ty (iconcat $I64 a_lo a_hi) (iconcat $I64 b_lo b_hi)))
281
282(rule (simplify (select ty (eq _   a_hi @ (value_type $I64) b_hi @ (value_type $I64))
283                           (ule ty a_lo @ (value_type $I64) b_lo @ (value_type $I64))
284                           (sle ty a_hi b_hi)))
285      (sle ty (iconcat $I64 a_lo a_hi) (iconcat $I64 b_lo b_hi)))
286
287(rule (simplify (select ty (eq _   a_hi @ (value_type $I64) b_hi @ (value_type $I64))
288                           (ult ty a_lo @ (value_type $I64) b_lo @ (value_type $I64))
289                           (ult ty a_hi b_hi)))
290      (ult ty (iconcat $I64 a_lo a_hi) (iconcat $I64 b_lo b_hi)))
291
292(rule (simplify (select ty (eq _   a_hi @ (value_type $I64) b_hi @ (value_type $I64))
293                           (ult ty a_lo @ (value_type $I64) b_lo @ (value_type $I64))
294                           (slt ty a_hi b_hi)))
295      (slt ty (iconcat $I64 a_lo a_hi) (iconcat $I64 b_lo b_hi)))
296
297
298(rule (simplify (eq cty x (bxor (ty_int bty) x y))) (subsume (eq cty y (iconst_u bty 0))))
299(rule (simplify (ne cty x (bxor (ty_int bty) x y))) (subsume (ne cty y (iconst_u bty 0))))
300
301; (x - y) > x == y > x
302(rule (simplify (ugt cty (isub ty x y) x)) (ugt cty y x))
303(rule (simplify (ule cty (isub ty x y) x)) (ule cty y x))
304
305;; (x < y) ? x : y != x == x > y, for both signed and unsigned.
306(rule (simplify (ne cty (select ty (slt cty x y) x y) x)) (sgt cty x y))
307(rule (simplify (ne cty (select ty (ult cty x y) x y) x)) (ugt cty x y))
308
309(rule (simplify (ult cty (bnot ty x) (bnot ty y))) (ugt cty x y))
310(rule (simplify (slt cty (bnot ty x) (bnot ty y))) (sgt cty x y))
311
312;; a < b ^^ a > b => (a ≠ b)
313(rule (simplify (bxor ty (sgt ty x y) (sgt ty y x))) (ne ty x y))
314(rule (simplify (bxor ty (sgt ty x y) (slt ty x y))) (ne ty x y))
315(rule (simplify (bxor ty (slt ty x y) (sgt ty x y))) (ne ty x y))
316(rule (simplify (bxor ty (slt ty x y) (slt ty y x))) (ne ty x y))
317(rule (simplify (bxor ty (ugt ty x y) (ugt ty y x))) (ne ty x y))
318(rule (simplify (bxor ty (ugt ty x y) (ult ty x y))) (ne ty x y))
319(rule (simplify (bxor ty (ult ty x y) (ugt ty x y))) (ne ty x y))
320(rule (simplify (bxor ty (ult ty x y) (ult ty y x))) (ne ty x y))
321
322;; a < b && a > b = false
323(rule (simplify (band (fits_in_64 ty) (sgt ty x y) (slt ty x y))) (iconst_u ty 0))
324(rule (simplify (band (fits_in_64 ty) (slt ty x y) (sgt ty x y))) (iconst_u ty 0))
325(rule (simplify (band (fits_in_64 ty) (ugt ty x y) (ult ty x y))) (iconst_u ty 0))
326(rule (simplify (band (fits_in_64 ty) (ult ty x y) (ugt ty x y))) (iconst_u ty 0))
327(rule
328  (simplify (band ty (sgt ty x (iconst_s _ y)) (ult ty x (iconst_s _ y))))
329  (if-let true (i64_gt_eq y 0))
330  (iconst_u ty 0))
331(rule
332  (simplify (band ty (sgt ty (iconst_s _ x) y) (ult ty (iconst_s _ x) y)))
333  (if-let true (i64_lt x 0))
334  (iconst_u ty 0))
335(rule
336  (simplify (band ty (slt ty x (iconst_s _ y)) (ugt ty x (iconst_s _ y))))
337  (if-let true (i64_lt y 0))
338  (iconst_u ty 0))
339(rule
340  (simplify (band ty (slt ty (iconst_s _ x) y) (ugt ty (iconst_s _ x) y)))
341  (if-let true (i64_gt_eq x 0))
342  (iconst_u ty 0))
343(rule
344  (simplify (band ty (ugt ty x (iconst_s _ y)) (slt ty x (iconst_s _ y))))
345  (if-let true (i64_lt y 0))
346  (iconst_u ty 0))
347(rule
348  (simplify (band ty (ugt ty (iconst_s _ x) y) (slt ty (iconst_s _ x) y)))
349  (if-let true (i64_gt_eq x 0))
350  (iconst_u ty 0))
351(rule
352  (simplify (band ty (ult ty x (iconst_s _ y)) (sgt ty x (iconst_s _ y))))
353  (if-let true (i64_gt_eq y 0))
354  (iconst_u ty 0))
355(rule
356  (simplify (band ty (ult ty (iconst_s _ x) y) (sgt ty (iconst_s _ x) y)))
357  (if-let true (i64_lt x 0))
358  (iconst_u ty 0))
359
360;; (x < y) & (x ≠ -1) = (x < y)
361(rule
362  (simplify (band ty (ne ty x (iconst_s _ -1)) (ugt ty y x)))
363   (ult ty x y))
364(rule
365  (simplify (band ty (ne ty x (iconst_s _ -1)) (ult ty x z)))
366   (ult ty x z))
367(rule
368  (simplify (band ty (ne ty (iconst_s _ -1) x) (ugt ty y x)))
369   (ult ty x y))
370(rule
371  (simplify (band ty (ne ty (iconst_s _ -1) x) (ult ty x z)))
372   (ult ty x z))
373(rule
374  (simplify (band ty (ugt ty x y) (ne ty y (iconst_s _ -1))))
375   (ult ty y x))
376(rule
377  (simplify (band ty (ugt ty x y) (ne ty (iconst_s _ -1) y)))
378   (ult ty y x))
379(rule
380  (simplify (band ty (ult ty x y) (ne ty x (iconst_s _ -1))))
381   (ult ty x y))
382(rule
383  (simplify (band ty (ult ty x y) (ne ty (iconst_s _ -1) x)))
384   (ult ty x y))
385
386;; icmp on select with two constant inputs compared with one of the two
387;; constants can directly use the inner select condition.
388;; See: https://github.com/bytecodealliance/wasmtime/issues/11578
389(rule (simplify (eq _
390  (select select_ty inner_cond @ (value_type inner_ty)
391    (iconst_u _ k1)
392    (iconst_u _ k2))
393  (iconst_u _ k1)))
394  (if-let false (u64_eq k1 k2))
395  (ne select_ty inner_cond (iconst_u inner_ty 0)))
396
397(rule (simplify (eq _
398  (select select_ty inner_cond @ (value_type inner_ty)
399    (iconst_u _ k1)
400    (iconst_u _ k2))
401  (iconst_u _ k2)))
402  (if-let false (u64_eq k1 k2))
403  (eq select_ty inner_cond (iconst_u inner_ty 0)))
404
405(rule (simplify (ne _
406  (select select_ty inner_cond @ (value_type inner_ty)
407    (iconst_u _ k1)
408    (iconst_u _ k2))
409  (iconst_u _ k1)))
410  (if-let false (u64_eq k1 k2))
411  (eq select_ty inner_cond (iconst_u inner_ty 0)))
412
413(rule (simplify (ne _
414  (select select_ty inner_cond @ (value_type inner_ty)
415    (iconst_u _ k1)
416    (iconst_u _ k2))
417  (iconst_u _ k2)))
418  (if-let false (u64_eq k1 k2))
419  (ne select_ty inner_cond (iconst_u inner_ty 0)))
420