Skip to content

Commit 1578325

Browse files
authored
[Cranelift] add simplification rules (#12926)
[Cranelift] Add arithmetic simplification rules
1 parent 96b47c7 commit 1578325

6 files changed

Lines changed: 520 additions & 1 deletion

File tree

cranelift/codegen/src/opts/arithmetic.isle

Lines changed: 64 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -324,3 +324,67 @@
324324

325325
(rule (simplify (iadd $I128 (bnot $I128 x) x)) (sextend $I128 (iconst_s $I64 -1)))
326326
(rule (simplify (iadd $I128 x (bnot $I128 x))) (sextend $I128 (iconst_s $I64 -1)))
327+
328+
;; ((x + y) - (x + z)) --> (y - z)
329+
(rule (simplify (isub ty (iadd ty x y) (iadd ty x z))) (isub ty y z))
330+
(rule (simplify (isub ty (iadd ty x y) (iadd ty z x))) (isub ty y z))
331+
(rule (simplify (isub ty (iadd ty y x) (iadd ty x z))) (isub ty y z))
332+
(rule (simplify (isub ty (iadd ty y x) (iadd ty z x))) (isub ty y z))
333+
334+
;; ((x - z) - (y - z)) --> (x - y)
335+
(rule (simplify (isub ty (isub ty x z) (isub ty y z))) (isub ty x y))
336+
337+
;; ((x - y) - (x - z)) --> (z - y)
338+
(rule (simplify (isub ty (isub ty x y) (isub ty x z))) (isub ty z y))
339+
340+
;; umin(x, y) + umax(x, y) --> x + y
341+
(rule (simplify (iadd ty (umin ty x y) (umax ty x y))) (iadd ty x y))
342+
(rule (simplify (iadd ty (umax ty x y) (umin ty x y))) (iadd ty x y))
343+
(rule (simplify (iadd ty (umin ty x y) (umax ty y x))) (iadd ty x y))
344+
(rule (simplify (iadd ty (umax ty y x) (umin ty x y))) (iadd ty x y))
345+
(rule (simplify (iadd ty (umin ty y x) (umax ty x y))) (iadd ty x y))
346+
(rule (simplify (iadd ty (umax ty x y) (umin ty y x))) (iadd ty x y))
347+
(rule (simplify (iadd ty (umin ty y x) (umax ty y x))) (iadd ty x y))
348+
(rule (simplify (iadd ty (umax ty y x) (umin ty y x))) (iadd ty x y))
349+
350+
;; smin(x, y) + smax(x, y) --> x + y
351+
(rule (simplify (iadd ty (smin ty x y) (smax ty x y))) (iadd ty x y))
352+
(rule (simplify (iadd ty (smax ty x y) (smin ty x y))) (iadd ty x y))
353+
(rule (simplify (iadd ty (smin ty x y) (smax ty y x))) (iadd ty x y))
354+
(rule (simplify (iadd ty (smax ty y x) (smin ty x y))) (iadd ty x y))
355+
(rule (simplify (iadd ty (smin ty y x) (smax ty x y))) (iadd ty x y))
356+
(rule (simplify (iadd ty (smax ty x y) (smin ty y x))) (iadd ty x y))
357+
(rule (simplify (iadd ty (smin ty y x) (smax ty y x))) (iadd ty x y))
358+
(rule (simplify (iadd ty (smax ty y x) (smin ty y x))) (iadd ty x y))
359+
360+
;; ((x + z) - (y + z)) --> (x - y)
361+
(rule (simplify (isub ty (iadd ty x z) (iadd ty y z))) (isub ty x y))
362+
(rule (simplify (isub ty (iadd ty x z) (iadd ty z y))) (isub ty x y))
363+
(rule (simplify (isub ty (iadd ty z x) (iadd ty y z))) (isub ty x y))
364+
(rule (simplify (isub ty (iadd ty z x) (iadd ty z y))) (isub ty x y))
365+
366+
;; ((x - y) + (y + z)) --> (x + z)
367+
(rule (simplify (iadd ty (isub ty x y) (iadd ty y z))) (iadd ty x z))
368+
(rule (simplify (iadd ty (iadd ty y z) (isub ty x y))) (iadd ty x z))
369+
(rule (simplify (iadd ty (isub ty x y) (iadd ty z y))) (iadd ty x z))
370+
(rule (simplify (iadd ty (iadd ty z y) (isub ty x y))) (iadd ty x z))
371+
372+
;; (x - (x + y)) --> -y
373+
(rule (simplify (isub ty x (iadd ty x y))) (ineg ty y))
374+
(rule (simplify (isub ty x (iadd ty y x))) (ineg ty y))
375+
376+
;; (x + (y + (z - x))) --> (y + z)
377+
(rule (simplify (iadd ty x (iadd ty y (isub ty z x)))) (iadd ty y z))
378+
(rule (simplify (iadd ty (iadd ty y (isub ty z x)) x)) (iadd ty y z))
379+
(rule (simplify (iadd ty x (iadd ty (isub ty z x) y))) (iadd ty y z))
380+
(rule (simplify (iadd ty (iadd ty (isub ty z x) y) x)) (iadd ty y z))
381+
382+
;; (x + y) == (y + x) --> true
383+
(rule (simplify (eq ty (iadd cty x y) (iadd cty y x))) (iconst_u ty 1))
384+
(rule (simplify (eq ty (iadd cty y x) (iadd cty x y))) (iconst_u ty 1))
385+
(rule (simplify (eq ty (iadd cty x y) (iadd cty x y))) (iconst_u ty 1))
386+
(rule (simplify (eq ty (iadd cty y x) (iadd cty y x))) (iconst_u ty 1))
387+
388+
;; (x - y) != x --> y != 0
389+
(rule (simplify (ne cty (isub ty x y) x)) (ne cty y (iconst_u ty 0)))
390+
(rule (simplify (ne cty x (isub ty x y))) (ne cty y (iconst_u ty 0)))

cranelift/codegen/src/opts/bitops.isle

Lines changed: 35 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -545,3 +545,38 @@
545545
(rule (simplify (bor ty y (band ty x (bnot ty y)))) (bor ty y x))
546546
(rule (simplify (bor ty (band ty x (bnot ty y)) y)) (bor ty y x))
547547

548+
;; ((x & ~y) - (x & y)) --> ((x ^ y) - y)
549+
(rule (simplify (isub ty (band ty x (bnot ty y)) (band ty x y))) (isub ty (bxor ty x y) y))
550+
(rule (simplify (isub ty (band ty x (bnot ty y)) (band ty y x))) (isub ty (bxor ty x y) y))
551+
(rule (simplify (isub ty (band ty (bnot ty y) x) (band ty x y))) (isub ty (bxor ty x y) y))
552+
(rule (simplify (isub ty (band ty (bnot ty y) x) (band ty y x))) (isub ty (bxor ty x y) y))
553+
(rule (simplify (isub ty (band ty x y) (band ty x (bnot ty y)))) (isub ty y (bxor ty x y)))
554+
(rule (simplify (isub ty (band ty x y) (band ty (bnot ty y) x))) (isub ty y (bxor ty x y)))
555+
(rule (simplify (isub ty (band ty y x) (band ty x (bnot ty y)))) (isub ty y (bxor ty x y)))
556+
(rule (simplify (isub ty (band ty y x) (band ty (bnot ty y) x))) (isub ty y (bxor ty x y)))
557+
558+
;; (x & ~y) | (~x & y) --> (x ^ y)
559+
(rule (simplify (bor ty (band ty x (bnot ty y)) (band ty (bnot ty x) y))) (bxor ty x y))
560+
(rule (simplify (bor ty (band ty (bnot ty x) y) (band ty x (bnot ty y)))) (bxor ty x y))
561+
(rule (simplify (bor ty (band ty x (bnot ty y)) (band ty y (bnot ty x)))) (bxor ty x y))
562+
(rule (simplify (bor ty (band ty y (bnot ty x)) (band ty x (bnot ty y)))) (bxor ty x y))
563+
(rule (simplify (bor ty (band ty (bnot ty y) x) (band ty (bnot ty x) y))) (bxor ty x y))
564+
(rule (simplify (bor ty (band ty (bnot ty x) y) (band ty (bnot ty y) x))) (bxor ty x y))
565+
(rule (simplify (bor ty (band ty (bnot ty y) x) (band ty y (bnot ty x)))) (bxor ty x y))
566+
(rule (simplify (bor ty (band ty y (bnot ty x)) (band ty (bnot ty y) x))) (bxor ty x y))
567+
568+
;; (x & ~y) | (x ^ y) --> (x ^ y)
569+
(rule (simplify (bor ty (band ty x (bnot ty y)) (bxor ty x y))) (bxor ty x y))
570+
(rule (simplify (bor ty (bxor ty x y) (band ty x (bnot ty y)))) (bxor ty x y))
571+
(rule (simplify (bor ty (band ty x (bnot ty y)) (bxor ty y x))) (bxor ty x y))
572+
(rule (simplify (bor ty (bxor ty y x) (band ty x (bnot ty y)))) (bxor ty x y))
573+
(rule (simplify (bor ty (band ty (bnot ty y) x) (bxor ty x y))) (bxor ty x y))
574+
(rule (simplify (bor ty (bxor ty x y) (band ty (bnot ty y) x))) (bxor ty x y))
575+
(rule (simplify (bor ty (band ty (bnot ty y) x) (bxor ty y x))) (bxor ty x y))
576+
(rule (simplify (bor ty (bxor ty y x) (band ty (bnot ty y) x))) (bxor ty x y))
577+
578+
;; (x & ~y) ^ ~x --> ~(x & y)
579+
(rule (simplify (bxor ty (band ty x (bnot ty y)) (bnot ty x))) (bnot ty (band ty x y)))
580+
(rule (simplify (bxor ty (bnot ty x) (band ty x (bnot ty y)))) (bnot ty (band ty x y)))
581+
(rule (simplify (bxor ty (band ty (bnot ty y) x) (bnot ty x))) (bnot ty (band ty x y)))
582+
(rule (simplify (bxor ty (bnot ty x) (band ty (bnot ty y) x))) (bnot ty (band ty x y)))

cranelift/filetests/filetests/egraph/arithmetic-precise.clif

Lines changed: 164 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -83,4 +83,168 @@ block0(v0: i128):
8383
; v3 = iconst.i64 -1
8484
; v4 = sextend.i128 v3 ; v3 = -1
8585
; return v4
86+
; }
87+
88+
;; ((x + y) - (x + z)) --> (y - z)
89+
function %test_isub_iadd_iadd_cancel(i32, i32, i32) -> i32 fast {
90+
block0(v0: i32, v1: i32, v2: i32):
91+
v3 = iadd v0, v1
92+
v4 = iadd v0, v2
93+
v5 = isub v3, v4
94+
return v5
95+
}
96+
97+
; function %test_isub_iadd_iadd_cancel(i32, i32, i32) -> i32 fast {
98+
; block0(v0: i32, v1: i32, v2: i32):
99+
; v6 = isub v1, v2
100+
; return v6
101+
; }
102+
103+
;; ((x - z) - (y - z)) --> (x - y)
104+
function %test_isub_isub_isub_cancel(i32, i32, i32) -> i32 fast {
105+
block0(v0: i32, v1: i32, v2: i32):
106+
v3 = isub v0, v2
107+
v4 = isub v1, v2
108+
v5 = isub v3, v4
109+
return v5
110+
}
111+
112+
; function %test_isub_isub_isub_cancel(i32, i32, i32) -> i32 fast {
113+
; block0(v0: i32, v1: i32, v2: i32):
114+
; v6 = isub v0, v1
115+
; return v6
116+
; }
117+
118+
;; ((x - y) - (x - z)) --> (z - y)
119+
function %test_isub_isub_isub_swap_cancel(i32, i32, i32) -> i32 fast {
120+
block0(v0: i32, v1: i32, v2: i32):
121+
v3 = isub v0, v1
122+
v4 = isub v0, v2
123+
v5 = isub v3, v4
124+
return v5
125+
}
126+
127+
; function %test_isub_isub_isub_swap_cancel(i32, i32, i32) -> i32 fast {
128+
; block0(v0: i32, v1: i32, v2: i32):
129+
; v6 = isub v2, v1
130+
; return v6
131+
; }
132+
133+
;; umin(x, y) + umax(x, y) --> x + y
134+
function %test_iadd_umin_umax(i32, i32) -> i32 fast {
135+
block0(v0: i32, v1: i32):
136+
v2 = umin v0, v1
137+
v3 = umax v0, v1
138+
v4 = iadd v2, v3
139+
return v4
140+
}
141+
142+
; function %test_iadd_umin_umax(i32, i32) -> i32 fast {
143+
; block0(v0: i32, v1: i32):
144+
; v6 = iadd v1, v0
145+
; return v6
146+
; }
147+
148+
;; smin(x, y) + smax(x, y) --> x + y
149+
function %test_iadd_smin_smax(i32, i32) -> i32 fast {
150+
block0(v0: i32, v1: i32):
151+
v2 = smin v0, v1
152+
v3 = smax v0, v1
153+
v4 = iadd v2, v3
154+
return v4
155+
}
156+
157+
; function %test_iadd_smin_smax(i32, i32) -> i32 fast {
158+
; block0(v0: i32, v1: i32):
159+
; v6 = iadd v1, v0
160+
; return v6
161+
; }
162+
163+
;; ((x + z) - (y + z)) --> (x - y)
164+
function %test_isub_iadd_iadd_common_rhs(i32, i32, i32) -> i32 fast {
165+
block0(v0: i32, v1: i32, v2: i32):
166+
v3 = iadd v0, v2
167+
v4 = iadd v1, v2
168+
v5 = isub v3, v4
169+
return v5
170+
}
171+
172+
; function %test_isub_iadd_iadd_common_rhs(i32, i32, i32) -> i32 fast {
173+
; block0(v0: i32, v1: i32, v2: i32):
174+
; v6 = isub v0, v1
175+
; return v6
176+
; }
177+
178+
;; ((x - y) + (y + z)) --> (x + z)
179+
function %test_iadd_isub_iadd_cancel(i32, i32, i32) -> i32 fast {
180+
block0(v0: i32, v1: i32, v2: i32):
181+
v3 = isub v0, v1
182+
v4 = iadd v1, v2
183+
v5 = iadd v3, v4
184+
return v5
185+
}
186+
187+
; function %test_iadd_isub_iadd_cancel(i32, i32, i32) -> i32 fast {
188+
; block0(v0: i32, v1: i32, v2: i32):
189+
; v6 = iadd v0, v2
190+
; return v6
191+
; }
192+
193+
;; (x - (x + y)) --> -y
194+
function %test_isub_iadd_to_ineg(i32, i32) -> i32 fast {
195+
block0(v0: i32, v1: i32):
196+
v2 = iadd v0, v1
197+
v3 = isub v0, v2
198+
return v3
199+
}
200+
201+
; function %test_isub_iadd_to_ineg(i32, i32) -> i32 fast {
202+
; block0(v0: i32, v1: i32):
203+
; v4 = ineg v1
204+
; return v4
205+
; }
206+
207+
;; (x + (y + (z - x))) --> (y + z)
208+
function %test_iadd_iadd_isub_cancel(i32, i32, i32) -> i32 fast {
209+
block0(v0: i32, v1: i32, v2: i32):
210+
v3 = isub v2, v0
211+
v4 = iadd v1, v3
212+
v5 = iadd v0, v4
213+
return v5
214+
}
215+
216+
; function %test_iadd_iadd_isub_cancel(i32, i32, i32) -> i32 fast {
217+
; block0(v0: i32, v1: i32, v2: i32):
218+
; v6 = iadd v1, v2
219+
; return v6
220+
; }
221+
222+
;; (eq ty (iadd cty x y) (iadd cty y x)) -> 1
223+
function %simplify_icmp_eq_iadd_commute(i32, i32) -> i8 fast {
224+
block0(v0: i32, v1: i32):
225+
v2 = iadd v0, v1
226+
v3 = iadd v1, v0
227+
v4 = icmp eq v2, v3
228+
return v4
229+
}
230+
231+
; function %simplify_icmp_eq_iadd_commute(i32, i32) -> i8 fast {
232+
; block0(v0: i32, v1: i32):
233+
; v5 = iconst.i8 1
234+
; return v5 ; v5 = 1
235+
; }
236+
237+
;; (x - y) != x --> y != 0
238+
function %simplify_icmp_ne_isub_x(i32, i32) -> i8 fast {
239+
block0(v0: i32, v1: i32):
240+
v2 = isub v0, v1
241+
v3 = icmp ne v2, v0
242+
return v3
243+
}
244+
245+
; function %simplify_icmp_ne_isub_x(i32, i32) -> i8 fast {
246+
; block0(v0: i32, v1: i32):
247+
; v4 = iconst.i32 0
248+
; v5 = icmp ne v1, v4 ; v4 = 0
249+
; return v5
86250
; }

cranelift/filetests/filetests/egraph/fold-bitops.clif

Lines changed: 67 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -200,3 +200,70 @@ block0(v0: i32, v1: i32):
200200
; return v8
201201
; }
202202

203+
204+
;; ((x & ~y) - (x & y)) --> ((x ^ y) - y)
205+
function %test_isub_band_band_bnot(i32, i32) -> i32 fast {
206+
block0(v0: i32, v1: i32):
207+
v2 = bnot v1
208+
v3 = band v0, v2
209+
v4 = band v0, v1
210+
v5 = isub v3, v4
211+
return v5
212+
}
213+
214+
; function %test_isub_band_band_bnot(i32, i32) -> i32 fast {
215+
; block0(v0: i32, v1: i32):
216+
; v6 = bxor v0, v1
217+
; v7 = isub v6, v1
218+
; return v7
219+
; }
220+
221+
;; (x & ~y) | (~x & y) --> (x ^ y)
222+
function %test_bor_band_bnot_to_bxor(i32, i32) -> i32 fast {
223+
block0(v0: i32, v1: i32):
224+
v2 = bnot v1
225+
v3 = band v0, v2
226+
v4 = bnot v0
227+
v5 = band v4, v1
228+
v6 = bor v3, v5
229+
return v6
230+
}
231+
232+
; function %test_bor_band_bnot_to_bxor(i32, i32) -> i32 fast {
233+
; block0(v0: i32, v1: i32):
234+
; v8 = bxor v1, v0
235+
; return v8
236+
; }
237+
238+
;; (x & ~y) | (x ^ y) --> (x ^ y)
239+
function %test_bor_band_bnot_bxor_absorb(i32, i32) -> i32 fast {
240+
block0(v0: i32, v1: i32):
241+
v2 = bnot v1
242+
v3 = band v0, v2
243+
v4 = bxor v0, v1
244+
v5 = bor v3, v4
245+
return v5
246+
}
247+
248+
; function %test_bor_band_bnot_bxor_absorb(i32, i32) -> i32 fast {
249+
; block0(v0: i32, v1: i32):
250+
; v4 = bxor v0, v1
251+
; return v4
252+
; }
253+
254+
;; (x & ~y) ^ ~x --> ~(x & y)
255+
function %test_bxor_band_bnot_to_bnot_band(i32, i32) -> i32 fast {
256+
block0(v0: i32, v1: i32):
257+
v2 = bnot v1
258+
v3 = band v0, v2
259+
v4 = bnot v0
260+
v5 = bxor v3, v4
261+
return v5
262+
}
263+
264+
; function %test_bxor_band_bnot_to_bnot_band(i32, i32) -> i32 fast {
265+
; block0(v0: i32, v1: i32):
266+
; v6 = band v0, v1
267+
; v7 = bnot v6
268+
; return v7
269+
; }

0 commit comments

Comments
 (0)