1;; Rewrites for `band`, `bnot`, `bor`, `bxor`
2
3;; x | 0 == x | x == x.
4(rule (simplify (bor ty
5                     x
6                     (iconst_u ty 0)))
7      (subsume x))
8(rule (simplify (bor ty x x))
9      (subsume x))
10
11;; x ^ 0 == x.
12(rule (simplify (bxor ty
13                     x
14                     (iconst_u ty 0)))
15      (subsume x))
16
17;; x ^ x == 0.
18(rule (simplify (bxor (ty_int ty) x x))
19      (subsume (iconst_u ty 0)))
20
21;; x ^ not(x) == not(x) ^ x == x | not(x) == not(x) | x == -1.
22;; This identity also holds for non-integer types, vectors, and wider types.
23(rule (simplify (bxor (ty_int ty) x (bnot ty x))) (subsume (iconst_s ty -1)))
24(rule (simplify (bxor (ty_int ty) (bnot ty x) x)) (subsume (iconst_s ty -1)))
25(rule (simplify (bor (ty_int ty) x (bnot ty x))) (subsume (iconst_s ty -1)))
26(rule (simplify (bor (ty_int ty) (bnot ty x) x)) (subsume (iconst_s ty -1)))
27
28;; x & x == x & -1 == x.
29(rule (simplify (band ty x x)) (subsume x))
30(rule (simplify (band ty x (iconst_s ty -1)))
31      (subsume x))
32
33;; x & 0 == x & not(x) == not(x) & x == 0.
34(rule (simplify (band ty _ zero @ (iconst_u ty 0))) (subsume zero))
35(rule (simplify (band (ty_int ty) x (bnot ty x))) (subsume (iconst_u ty 0)))
36(rule (simplify (band (ty_int ty) (bnot ty x) x)) (subsume (iconst_u ty 0)))
37
38;; (x & y) ^ (x ^ y) == x | y
39(rule (simplify (bxor ty (band ty X Y) (bxor ty X Y))) (bor ty X Y))
40
41;; not(not(x)) == x.
42(rule (simplify (bnot ty (bnot ty x))) (subsume x))
43
44;; `or(and(x, y), not(y)) == or(x, not(y))`
45(rule (simplify (bor ty
46                     (band ty x y)
47                     z @ (bnot ty y)))
48      (bor ty x z))
49;; Duplicate the rule but swap the `bor` operands because `bor` is
50;; commutative. We could, of course, add a `simplify` rule to do the commutative
51;; swap for all `bor`s but this will bloat the e-graph with many e-nodes. It is
52;; cheaper to have additional rules, rather than additional e-nodes, because we
53;; amortize their cost via ISLE's smart codegen.
54(rule (simplify (bor ty
55                     z @ (bnot ty y)
56                     (band ty x y)))
57      (bor ty x z))
58
59;; `or(and(x, y), not(y)) == or(x, not(y))` specialized for constants, since
60;; otherwise we may not know that `z == not(y)` since we don't generally expand
61;; constants in the e-graph.
62;;
63;; (No need to duplicate for commutative `bor` for this constant version because
64;; we move constants to the right.)
65(rule (simplify (bor ty
66                     (band ty x (iconst_u ty y))
67                     z @ (iconst_u ty zk)))
68      (if-let true (u64_eq (u64_and (ty_mask ty) zk)
69                            (u64_and (ty_mask ty) (u64_not y))))
70      (bor ty x z))
71
72;; (x ^ -1) can be replaced with the `bnot` instruction
73(rule (simplify (bxor ty x (iconst_s ty -1)))
74  (bnot ty x))
75
76;; sshr((x | -x), N) == bmask(x) where N = ty_bits(ty) - 1.
77;;
78;; (x | -x) sets the sign bit to 1 if x is nonzero, and 0 if x is zero. sshr propagates
79;; the sign bit to the rest of the value.
80(rule (simplify (sshr ty (bor ty x (ineg ty x)) (iconst_u ty shift_amt)))
81      (if-let true (u64_eq shift_amt (ty_shift_mask ty)))
82      (bmask ty x))
83
84(rule (simplify (sshr ty (bor ty (ineg ty x) x) (iconst_u ty shift_amt)))
85      (if-let true (u64_eq shift_amt (ty_shift_mask ty)))
86      (bmask ty x))
87
88;; Since icmp is always 0 or 1, bmask is just a negation.
89;; TODO: Explore whether this makes sense for things needing extension too.
90(rule (simplify (bmask $I8 cmp@(icmp $I8 _ _ _)))
91      (ineg $I8 cmp))
92
93;; Matches any expressions that preserve "truthiness".
94;; i.e. If the input is zero it remains zero, and if it is nonzero it can have
95;; a different value as long as it is still nonzero.
96(decl pure multi truthy (Value) Value)
97(rule (truthy (sextend _ x)) x)
98(rule (truthy (uextend _ x)) x)
99(rule (truthy (bmask _ x)) x)
100(rule (truthy (ineg _ x)) x)
101(rule (truthy (bswap _ x)) x)
102(rule (truthy (bitrev _ x)) x)
103(rule (truthy (popcnt _ x)) x)
104(rule (truthy (rotl _ x _)) x)
105(rule (truthy (rotr _ x _)) x)
106(rule (truthy (select _ x (iconst_u _ (u64_when_non_zero)) (iconst_u _ 0))) x)
107;; (ne ty (iconst 0) v) is also canonicalized into this form via another rule
108(rule (truthy (ne _ x (iconst_u _ 0))) x)
109
110;; All of these expressions don't care about their input as long as it is truthy.
111;; so we can remove expressions that preserve that property from the input.
112(rule (simplify (bmask ty v)) (if-let x (truthy v)) (bmask ty x))
113(rule (simplify (select ty v t f)) (if-let c (truthy v)) (select ty c t f))
114;; (ne ty (iconst 0) v) is also canonicalized into this form via another rule
115(rule (simplify (ne cty v (iconst_u _ 0)))
116      (if-let c (truthy v))
117      (if-let (value_type (ty_int_ref_scalar_64 ty)) c)
118      (ne cty c (iconst_u ty 0)))
119
120
121
122;; (sextend (bmask x)) can be replaced with (bmask x) since bmask
123;; supports any size of output type, regardless of input.
124;; Same with `ireduce`
125(rule (simplify (sextend ty (bmask _ x))) (bmask ty x))
126(rule (simplify (ireduce ty (bmask _ x))) (bmask ty x))
127
128;; (bswap (bswap x)) == x
129(rule (simplify (bswap ty (bswap ty x))) (subsume x))
130
131;; (bitrev (bitrev x)) == x
132(rule (simplify (bitrev ty (bitrev ty x))) (subsume x))
133
134;; WebAssembly doesn't have a native byte-swapping instruction at this time so
135;; languages which have a byte-swapping operation will compile it down to bit
136;; shifting and twiddling. This attempts to pattern match what LLVM currently
137;; generates today for the Rust code `a.swap_bytes()`. This might be a bit
138;; brittle over time and/or with other possible LLVM backend optimizations, but
139;; it's at least one way to generate a byte swap.
140;;
141;; Technically this could be permuted quite a few ways and currently there's no
142;; easy way to match all of them, so only one is matched here.
143(rule (simplify (bor ty @ $I32
144    (bor ty
145      (ishl ty x (iconst_u ty 24))
146      (ishl ty
147        (band ty x (iconst_u ty 0xff00))
148        (iconst_u ty 8)))
149    (bor ty
150      (band ty
151        (ushr ty x (iconst_u ty 8))
152        (iconst_u ty 0xff00))
153      (ushr ty x (iconst_u ty 24)))))
154  (bswap ty x))
155
156(rule (simplify (bor ty @ $I64
157    (bor ty
158      (bor ty
159        (ishl ty x (iconst_u ty 56))
160        (ishl ty
161          (band ty x (iconst_u ty 0xff00))
162          (iconst_u ty 40)))
163      (bor ty
164        (ishl ty
165          (band ty x (iconst_u ty 0xff_0000))
166          (iconst_u ty 24))
167        (ishl ty
168          (band ty x (iconst_u ty 0xff00_0000))
169          (iconst_u ty 8))))
170    (bor ty
171      (bor ty
172        (band ty
173          (ushr ty x (iconst_u ty 8))
174          (iconst_u ty 0xff00_0000))
175        (band ty
176          (ushr ty x (iconst_u ty 24))
177          (iconst_u ty 0xff_0000)))
178      (bor ty
179        (band ty
180          (ushr ty x (iconst_u ty 40))
181          (iconst_u ty 0xff00))
182        (ushr ty x (iconst_u ty 56))))))
183  (bswap ty x))
184
185(rule (simplify (bxor ty (bor ty x y) (band ty x y))) (bxor ty x y))
186
187
188(rule (simplify (bor ty (bor ty x y) x)) (bor ty x y))
189(rule (simplify (bor ty (bor ty x y) y)) (bor ty x y))
190(rule (simplify (bor ty x (bor ty x y))) (bor ty x y))
191(rule (simplify (bor ty y (bor ty x y))) (bor ty x y))
192
193(rule (simplify (band ty (band ty x y) x)) (band ty x y))
194(rule (simplify (band ty (band ty x y) y)) (band ty x y))
195(rule (simplify (band ty x (band ty x y))) (band ty x y))
196(rule (simplify (band ty y (band ty x y))) (band ty x y))
197
198;; (x ^ ~y) & x --> x & y
199(rule (simplify (band ty (bxor ty x (bnot ty y)) x)) (band ty x y))
200(rule (simplify (band ty (bxor ty (bnot ty y) x) x)) (band ty x y))
201(rule (simplify (band ty x (bxor ty x (bnot ty y)))) (band ty x y))
202(rule (simplify (band ty x (bxor ty (bnot ty y) x))) (band ty x y))
203
204; (x & y) + (x ^ y) --> x | y
205(rule (simplify (iadd ty (band ty x y) (bxor ty x y))) (bor ty x y))
206(rule (simplify (iadd ty (bxor ty x y) (band ty x y))) (bor ty x y))
207
208; (x | y) + (x & y) --> x + y
209(rule (simplify (iadd ty (bor ty x y) (band ty x y))) (iadd ty x y))
210(rule (simplify (iadd ty (band ty x y) (bor ty x y))) (iadd ty x y))
211
212; (x & y) | x --> x
213(rule (simplify (bor ty (band ty x y) x)) x)
214(rule (simplify (bor ty x (band ty x y))) x)
215
216; (x ^ y) ^ y --> x
217(rule (simplify (bxor ty (bxor ty x y) y)) x)
218(rule (simplify (bxor ty y (bxor ty x y))) x)
219
220; (x & y) | ~x -> y | ~x
221(rule (simplify (bor ty (band ty x y) (bnot ty x))) (bor ty y (bnot ty x)))
222(rule (simplify (bor ty (bnot ty x) (band ty x y))) (bor ty y (bnot ty x)))
223
224; (z & x) ^ (z & y) => z & (x ^ y)
225(rule (simplify
226  (bxor ty (band ty z x) (band ty z y)))
227	(band ty z (bxor ty x y)))
228
229; (x & y) | ~(x ^ y) => ~(x ^ y)
230(rule (simplify (bor ty (band ty x y) (bnot ty (bxor ty x y)))) (bnot ty (bxor ty x y)))
231(rule (simplify (bor ty (bnot ty (bxor ty x y)) (band ty x y))) (bnot ty (bxor ty x y)))
232(rule (simplify (bor ty (band ty x y) (bnot ty (bxor ty y x)))) (bnot ty (bxor ty x y)))
233(rule (simplify (bor ty (bnot ty (bxor ty y x)) (band ty x y))) (bnot ty (bxor ty x y)))
234(rule (simplify (bor ty (band ty y x) (bnot ty (bxor ty x y)))) (bnot ty (bxor ty x y)))
235(rule (simplify (bor ty (bnot ty (bxor ty x y)) (band ty y x))) (bnot ty (bxor ty x y)))
236(rule (simplify (bor ty (band ty y x) (bnot ty (bxor ty y x)))) (bnot ty (bxor ty x y)))
237(rule (simplify (bor ty (bnot ty (bxor ty y x)) (band ty y x))) (bnot ty (bxor ty x y)))
238
239; (x | y) + (-y) --> x & ~y
240(rule (simplify (iadd ty (bor ty x y) (ineg ty y)))
241      (band ty x (bnot ty y)))
242(rule (simplify (iadd ty (ineg ty y) (bor ty x y)))
243      (band ty x (bnot ty y)))
244(rule (simplify (iadd ty (bor ty y x) (ineg ty y)))
245      (band ty x (bnot ty y)))
246(rule (simplify (iadd ty (ineg ty y) (bor ty y x)))
247      (band ty x (bnot ty y)))
248
249; x & (x | y) --> x
250(rule (simplify (band ty (bor ty x y) x)) x)
251(rule (simplify (band ty x (bor ty x y))) x)
252(rule (simplify (band ty (bor ty y x) x)) x)
253(rule (simplify (band ty x (bor ty y x))) x)
254
255; (x | z) & (y | z) --> (x & y) | z
256(rule (simplify (band ty (bor ty x z) (bor ty y z))) (bor ty (band ty x y) z))
257(rule (simplify (band ty (bor ty y z) (bor ty x z))) (bor ty (band ty x y) z))
258(rule (simplify (band ty (bor ty x z) (bor ty z y))) (bor ty (band ty x y) z))
259(rule (simplify (band ty (bor ty z y) (bor ty x z))) (bor ty (band ty x y) z))
260(rule (simplify (band ty (bor ty z x) (bor ty y z))) (bor ty (band ty x y) z))
261(rule (simplify (band ty (bor ty y z) (bor ty z x))) (bor ty (band ty x y) z))
262(rule (simplify (band ty (bor ty z x) (bor ty z y))) (bor ty (band ty x y) z))
263(rule (simplify (band ty (bor ty z y) (bor ty z x))) (bor ty (band ty x y) z))
264
265; (x & z) | (y & z) --> (x | y) & z
266(rule (simplify (bor ty (band ty x z) (band ty y z))) (band ty (bor ty x y) z))
267(rule (simplify (bor ty (band ty y z) (band ty x z))) (band ty (bor ty x y) z))
268(rule (simplify (bor ty (band ty x z) (band ty z y))) (band ty (bor ty x y) z))
269(rule (simplify (bor ty (band ty z y) (band ty x z))) (band ty (bor ty x y) z))
270(rule (simplify (bor ty (band ty z x) (band ty y z))) (band ty (bor ty x y) z))
271(rule (simplify (bor ty (band ty y z) (band ty z x))) (band ty (bor ty x y) z))
272(rule (simplify (bor ty (band ty z x) (band ty z y))) (band ty (bor ty x y) z))
273(rule (simplify (bor ty (band ty z y) (band ty z x))) (band ty (bor ty x y) z))
274
275; (x | y) ^ (x | ~y) --> ~x
276(rule (simplify (bxor ty (bor ty x y) (bor ty x (bnot ty y)))) (bnot ty x))
277(rule (simplify (bxor ty (bor ty x (bnot ty y)) (bor ty x y))) (bnot ty x))
278(rule (simplify (bxor ty (bor ty x y) (bor ty (bnot ty y) x))) (bnot ty x))
279(rule (simplify (bxor ty (bor ty (bnot ty y) x) (bor ty x y))) (bnot ty x))
280(rule (simplify (bxor ty (bor ty y x) (bor ty x (bnot ty y)))) (bnot ty x))
281(rule (simplify (bxor ty (bor ty x (bnot ty y)) (bor ty y x))) (bnot ty x))
282(rule (simplify (bxor ty (bor ty y x) (bor ty (bnot ty y) x))) (bnot ty x))
283(rule (simplify (bxor ty (bor ty (bnot ty y) x) (bor ty y x))) (bnot ty x))
284
285; (~x) & (~y) --> ~(x | y)
286(rule (simplify (band ty (bnot ty x) (bnot ty y))) (bnot ty (bor ty x y)))
287(rule (simplify (band ty (bnot ty y) (bnot ty x))) (bnot ty (bor ty x y)))
288
289; (~x) | (~y) --> ~(x & y)
290(rule (simplify (bor ty (bnot ty x) (bnot ty y))) (bnot ty (band ty x y)))
291(rule (simplify (bor ty (bnot ty y) (bnot ty x))) (bnot ty (band ty x y)))