Skip to content

Commit a4fef42

Browse files
myunbinmyunbin
authored
[Cranelift] add simplification rules (#12948)
1 parent 29a27cf commit a4fef42

8 files changed

Lines changed: 491 additions & 16 deletions

File tree

‎cranelift/codegen/src/opts/arithmetic.isle‎

Lines changed: 51 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -386,5 +386,54 @@
386386
(rule (simplify (eq (ty_int ty) (iadd cty y x) (iadd cty y x))) (iconst_u ty 1))
387387

388388
;; (x - y) != x --> y != 0
389-
(rule (simplify (ne cty (isub (ty_int ty) x y) x)) (ne cty y (iconst_u ty 0)))
390-
(rule (simplify (ne cty x (isub (ty_int ty) x y))) (ne cty y (iconst_u ty 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)))
391+
392+
;; (x - y) == x --> y == 0
393+
(rule (simplify (eq cty (isub ty x y) x)) (eq cty y (iconst_u ty 0)))
394+
(rule (simplify (eq cty x (isub ty x y))) (eq cty y (iconst_u ty 0)))
395+
396+
;; (x + y) == y --> x == 0
397+
(rule (simplify (eq cty (iadd ty x y) y)) (eq cty x (iconst_u ty 0)))
398+
(rule (simplify (eq cty (iadd ty y x) y)) (eq cty x (iconst_u ty 0)))
399+
(rule (simplify (eq cty y (iadd ty x y))) (eq cty x (iconst_u ty 0)))
400+
(rule (simplify (eq cty y (iadd ty y x))) (eq cty x (iconst_u ty 0)))
401+
402+
;; -x == -y --> x == y
403+
(rule (simplify (eq ty (ineg ty x) (ineg ty y))) (eq ty x y))
404+
405+
;; -((-y) * x) --> x * y
406+
(rule (simplify (ineg ty (imul ty (ineg ty y) x))) (imul ty x y))
407+
(rule (simplify (ineg ty (imul ty x (ineg ty y)))) (imul ty x y))
408+
409+
;; ireduce(xext(a) + xext(b)) --> a + b
410+
(rule (simplify (ireduce ty (iadd cty (sextend cty x) (sextend cty y)))) (iadd ty x y))
411+
(rule (simplify (ireduce ty (iadd cty (sextend cty x) (uextend cty y)))) (iadd ty x y))
412+
(rule (simplify (ireduce ty (iadd cty (uextend cty x) (sextend cty y)))) (iadd ty x y))
413+
(rule (simplify (ireduce ty (iadd cty (uextend cty x) (uextend cty y)))) (iadd ty x y))
414+
415+
;; ireduce(xext(a) - xext(b)) --> a - b
416+
(rule (simplify (ireduce ty (isub cty (sextend cty x) (sextend cty y)))) (isub ty x y))
417+
(rule (simplify (ireduce ty (isub cty (sextend cty x) (uextend cty y)))) (isub ty x y))
418+
(rule (simplify (ireduce ty (isub cty (uextend cty x) (sextend cty y)))) (isub ty x y))
419+
(rule (simplify (ireduce ty (isub cty (uextend cty x) (uextend cty y)))) (isub ty x y))
420+
421+
;; max(x, y) >= x
422+
(rule (simplify (sge ty (smax ty x y) x)) (iconst_u ty 1))
423+
(rule (simplify (sge ty (smax ty y x) x)) (iconst_u ty 1))
424+
(rule (simplify (sle ty x (smax ty x y))) (iconst_u ty 1))
425+
(rule (simplify (sle ty x (smax ty y x))) (iconst_u ty 1))
426+
(rule (simplify (uge ty (umax ty x y) x)) (iconst_u ty 1))
427+
(rule (simplify (uge ty (umax ty y x) x)) (iconst_u ty 1))
428+
(rule (simplify (ule ty x (umax ty x y))) (iconst_u ty 1))
429+
(rule (simplify (ule ty x (umax ty y x))) (iconst_u ty 1))
430+
431+
;; x >= min(x, y)
432+
(rule (simplify (sge ty x (smin ty x y))) (iconst_u ty 1))
433+
(rule (simplify (sge ty x (smin ty y x))) (iconst_u ty 1))
434+
(rule (simplify (sle ty (smin ty x y) x)) (iconst_u ty 1))
435+
(rule (simplify (sle ty (smin ty y x) x)) (iconst_u ty 1))
436+
(rule (simplify (uge ty x (umin ty x y))) (iconst_u ty 1))
437+
(rule (simplify (uge ty x (umin ty y x))) (iconst_u ty 1))
438+
(rule (simplify (ule ty (umin ty x y) x)) (iconst_u ty 1))
439+
(rule (simplify (ule ty (umin ty y x) x)) (iconst_u ty 1))

‎cranelift/codegen/src/opts/bitops.isle‎

Lines changed: 19 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -696,4 +696,22 @@
696696
(rule (simplify (bxor ty (bor ty y (bnot ty x)) (bxor ty x y))) (bor ty x (bnot ty y)))
697697
(rule (simplify (bxor ty (bxor ty x y) (bor ty y (bnot ty x)))) (bor ty x (bnot ty y)))
698698
(rule (simplify (bxor ty (bor ty y (bnot ty x)) (bxor ty y x))) (bor ty x (bnot ty y)))
699-
(rule (simplify (bxor ty (bxor ty y x) (bor ty y (bnot ty x)))) (bor ty x (bnot ty y)))
699+
(rule (simplify (bxor ty (bxor ty y x) (bor ty y (bnot ty x)))) (bor ty x (bnot ty y)))
700+
701+
;; (x & ~y) == ~y <=> (x | y) == -1
702+
(rule (simplify (eq rty (band cty (bnot cty y) x) (bnot cty y))) (eq rty (bor cty y x) (iconst_s cty -1)))
703+
(rule (simplify (eq rty (band cty x (bnot cty y)) (bnot cty y))) (eq rty (bor cty y x) (iconst_s cty -1)))
704+
(rule (simplify (eq rty (bnot cty y) (band cty (bnot cty y) x))) (eq rty (bor cty y x) (iconst_s cty -1)))
705+
(rule (simplify (eq rty (bnot cty y) (band cty x (bnot cty y)))) (eq rty (bor cty y x) (iconst_s cty -1)))
706+
707+
;; x >=_u (x & y), and (x & y) <=_u x, are always true.
708+
(rule (simplify (uge ty x (band ty x y))) (iconst_u ty 1))
709+
(rule (simplify (uge ty x (band ty y x))) (iconst_u ty 1))
710+
(rule (simplify (ule ty (band ty x y) x)) (iconst_u ty 1))
711+
(rule (simplify (ule ty (band ty y x) x)) (iconst_u ty 1))
712+
713+
;; (x | y) >=_u x, and x <=_u (x | y), are always true.
714+
(rule (simplify (uge ty (bor ty x y) x)) (iconst_u ty 1))
715+
(rule (simplify (uge ty (bor ty y x) x)) (iconst_u ty 1))
716+
(rule (simplify (ule ty x (bor ty x y))) (iconst_u ty 1))
717+
(rule (simplify (ule ty x (bor ty y x))) (iconst_u ty 1))

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

Lines changed: 162 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -264,17 +264,171 @@ block0(v0: i32, v1: i32):
264264
; return v5
265265
; }
266266

267-
;; (x - y) != x --> y != 0 (vector)
268-
function %simplify_vector_icmp_ne_isub_x(i32x4, i32x4) -> i32x4 fast {
269-
block0(v0: i32x4, v1: i32x4):
267+
;; (x - y) == x --> y == 0
268+
function %test_eq_isub_same(i32, i32) -> i8 fast {
269+
block0(v0: i32, v1: i32):
270270
v2 = isub v0, v1
271-
v3 = icmp ne v2, v0
271+
v3 = icmp eq v2, v0
272272
return v3
273273
}
274274

275-
; function %simplify_vector_icmp_ne_isub_x(i32x4, i32x4) -> i32x4 fast {
276-
; block0(v0: i32x4, v1: i32x4):
277-
; v2 = isub v0, v1
278-
; v3 = icmp ne v2, v0
275+
; function %test_eq_isub_same(i32, i32) -> i8 fast {
276+
; block0(v0: i32, v1: i32):
277+
; v4 = iconst.i32 0
278+
; v5 = icmp eq v1, v4 ; v4 = 0
279+
; return v5
280+
; }
281+
282+
;; (x + y) == y --> x == 0
283+
function %test_eq_iadd_same_rhs(i32, i32) -> i8 fast {
284+
block0(v0: i32, v1: i32):
285+
v2 = iadd v0, v1
286+
v3 = icmp eq v2, v1
287+
return v3
288+
}
289+
290+
; function %test_eq_iadd_same_rhs(i32, i32) -> i8 fast {
291+
; block0(v0: i32, v1: i32):
292+
; v4 = iconst.i32 0
293+
; v5 = icmp eq v0, v4 ; v4 = 0
294+
; return v5
295+
; }
296+
297+
;; -x == -y --> x == y
298+
function %test_eq_ineg_ineg(i32, i32) -> i8 fast {
299+
block0(v0: i32, v1: i32):
300+
v2 = ineg v0
301+
v3 = ineg v1
302+
v4 = icmp eq v2, v3
303+
return v4
304+
}
305+
306+
; function %test_eq_ineg_ineg(i32, i32) -> i8 fast {
307+
; block0(v0: i32, v1: i32):
308+
; v2 = ineg v0
309+
; v3 = ineg v1
310+
; v4 = icmp eq v2, v3
311+
; return v4
312+
; }
313+
314+
;; -((-y) * x) --> x * y
315+
function %test_ineg_imul_ineg_lhs(i32, i32) -> i32 fast {
316+
block0(v0: i32, v1: i32):
317+
v2 = ineg v1
318+
v3 = imul v2, v0
319+
v4 = ineg v3
320+
return v4
321+
}
322+
323+
; function %test_ineg_imul_ineg_lhs(i32, i32) -> i32 fast {
324+
; block0(v0: i32, v1: i32):
325+
; v5 = imul v0, v1
326+
; return v5
327+
; }
328+
329+
function %test_ineg_imul_ineg_rhs(i32, i32) -> i32 fast {
330+
block0(v0: i32, v1: i32):
331+
v2 = ineg v1
332+
v3 = imul v0, v2
333+
v4 = ineg v3
334+
return v4
335+
}
336+
337+
; function %test_ineg_imul_ineg_rhs(i32, i32) -> i32 fast {
338+
; block0(v0: i32, v1: i32):
339+
; v5 = imul v0, v1
340+
; return v5
341+
; }
342+
343+
;; ireduce(sextend(x) + uextend(y)) --> x + y
344+
function %test_ireduce_iadd_extends(i8, i8) -> i8 fast {
345+
block0(v0: i8, v1: i8):
346+
v2 = sextend.i16 v0
347+
v3 = uextend.i16 v1
348+
v4 = iadd v2, v3
349+
v5 = ireduce.i8 v4
350+
return v5
351+
}
352+
353+
; function %test_ireduce_iadd_extends(i8, i8) -> i8 fast {
354+
; block0(v0: i8, v1: i8):
355+
; v6 = iadd v0, v1
356+
; return v6
357+
; }
358+
359+
;; ireduce(sextend(x) - uextend(y)) --> x - y
360+
function %test_ireduce_isub_extends(i8, i8) -> i8 fast {
361+
block0(v0: i8, v1: i8):
362+
v2 = sextend.i16 v0
363+
v3 = uextend.i16 v1
364+
v4 = isub v2, v3
365+
v5 = ireduce.i8 v4
366+
return v5
367+
}
368+
369+
; function %test_ireduce_isub_extends(i8, i8) -> i8 fast {
370+
; block0(v0: i8, v1: i8):
371+
; v6 = isub v0, v1
372+
; return v6
373+
; }
374+
375+
;; smax(x, y) >= x --> true
376+
function %test_sge_smax_x(i32, i32) -> i8 fast {
377+
block0(v0: i32, v1: i32):
378+
v2 = smax v0, v1
379+
v3 = icmp sge v2, v0
380+
return v3
381+
}
382+
383+
; function %test_sge_smax_x(i32, i32) -> i8 fast {
384+
; block0(v0: i32, v1: i32):
385+
; v2 = smax v0, v1
386+
; v3 = icmp sge v2, v0
387+
; return v3
388+
; }
389+
390+
;; x <=_u umax(x, y) --> true
391+
function %test_ule_x_umax(i32, i32) -> i8 fast {
392+
block0(v0: i32, v1: i32):
393+
v2 = umax v0, v1
394+
v3 = icmp ule v0, v2
395+
return v3
396+
}
397+
398+
; function %test_ule_x_umax(i32, i32) -> i8 fast {
399+
; block0(v0: i32, v1: i32):
400+
; v2 = umax v0, v1
401+
; v3 = icmp ule v0, v2
279402
; return v3
280403
; }
404+
405+
;; x >= smin(x, y) --> true
406+
function %test_sge_x_smin(i32, i32) -> i8 fast {
407+
block0(v0: i32, v1: i32):
408+
v2 = smin v0, v1
409+
v3 = icmp sge v0, v2
410+
return v3
411+
}
412+
413+
; function %test_sge_x_smin(i32, i32) -> i8 fast {
414+
; block0(v0: i32, v1: i32):
415+
; v2 = smin v0, v1
416+
; v3 = icmp sge v0, v2
417+
; return v3
418+
; }
419+
420+
;; umin(x, y) <=_u x --> true
421+
function %test_ule_umin_x(i32, i32) -> i8 fast {
422+
block0(v0: i32, v1: i32):
423+
v2 = umin v0, v1
424+
v3 = icmp ule v2, v0
425+
return v3
426+
}
427+
428+
; function %test_ule_umin_x(i32, i32) -> i8 fast {
429+
; block0(v0: i32, v1: i32):
430+
; v2 = umin v0, v1
431+
; v3 = icmp ule v2, v0
432+
; return v3
433+
; }
434+

‎cranelift/filetests/filetests/egraph/arithmetic.clif‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -363,8 +363,8 @@ block0(v0: i16, v1: i16, v2: i16):
363363
return v8
364364
}
365365

366-
; check: v12 = iadd v0, v1
367-
; check: v15 = iadd v12, v2
366+
; check: v10 = iadd v0, v1
367+
; check: v15 = iadd v10, v2
368368
; check: return v15
369369

370370
;; or(x, C) + (-C) --> and(x, ~C)

‎cranelift/filetests/filetests/egraph/extends.clif‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -179,8 +179,8 @@ block0(v0: i16, v1: i16):
179179
return v5
180180
}
181181

182-
; check: v8 = iadd v0, v1
183-
; check: return v8
182+
; check: v6 = iadd v0, v1
183+
; check: return v6
184184

185185
function %extend_bxor_reduce(i64, i64) -> i64 {
186186
block0(v0: i64, v1: i64):

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

Lines changed: 77 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -494,3 +494,80 @@ block0(v0: i32, v1: i32):
494494
; return v7
495495
; }
496496

497+
;; (x & ~y) == ~y --> (x | y) == -1
498+
function %test_eq_band_bnot_fullmask(i32, i32) -> i8 fast {
499+
block0(v0: i32, v1: i32):
500+
v2 = bnot v1
501+
v3 = band v0, v2
502+
v4 = icmp eq v3, v2
503+
return v4
504+
}
505+
506+
; function %test_eq_band_bnot_fullmask(i32, i32) -> i8 fast {
507+
; block0(v0: i32, v1: i32):
508+
; v5 = bor v1, v0
509+
; v6 = iconst.i32 -1
510+
; v7 = icmp eq v5, v6 ; v6 = -1
511+
; return v7
512+
; }
513+
514+
;; x >=_u (x & y) --> true
515+
function %test_uge_x_band(i32, i32) -> i8 fast {
516+
block0(v0: i32, v1: i32):
517+
v2 = band v0, v1
518+
v3 = icmp uge v0, v2
519+
return v3
520+
}
521+
522+
; function %test_uge_x_band(i32, i32) -> i8 fast {
523+
; block0(v0: i32, v1: i32):
524+
; v2 = band v0, v1
525+
; v3 = icmp uge v0, v2
526+
; return v3
527+
; }
528+
529+
;; (x & y) <=_u x --> true
530+
function %test_ule_band_x(i32, i32) -> i8 fast {
531+
block0(v0: i32, v1: i32):
532+
v2 = band v0, v1
533+
v3 = icmp ule v2, v0
534+
return v3
535+
}
536+
537+
; function %test_ule_band_x(i32, i32) -> i8 fast {
538+
; block0(v0: i32, v1: i32):
539+
; v2 = band v0, v1
540+
; v3 = icmp ule v2, v0
541+
; return v3
542+
; }
543+
544+
;; (x | y) >=_u x --> true
545+
function %test_uge_bor_x(i32, i32) -> i8 fast {
546+
block0(v0: i32, v1: i32):
547+
v2 = bor v0, v1
548+
v3 = icmp uge v2, v0
549+
return v3
550+
}
551+
552+
; function %test_uge_bor_x(i32, i32) -> i8 fast {
553+
; block0(v0: i32, v1: i32):
554+
; v2 = bor v0, v1
555+
; v3 = icmp uge v2, v0
556+
; return v3
557+
; }
558+
559+
;; x <=_u (x | y) --> true
560+
function %test_ule_x_bor(i32, i32) -> i8 fast {
561+
block0(v0: i32, v1: i32):
562+
v2 = bor v0, v1
563+
v3 = icmp ule v0, v2
564+
return v3
565+
}
566+
567+
; function %test_ule_x_bor(i32, i32) -> i8 fast {
568+
; block0(v0: i32, v1: i32):
569+
; v2 = bor v0, v1
570+
; v3 = icmp ule v0, v2
571+
; return v3
572+
; }
573+

0 commit comments

Comments
 (0)