Skip to content

Commit 7861a07

Browse files
myunbinbongjunj
myunbin
authored and
bongjunj
committed
[Cranelift] add bit operation simplification rules (bytecodealliance#12782)
* [Cranelift] add bit operation simplification rules * [Cranelift] filetest error resolve
1 parent 969fc63 commit 7861a07

4 files changed

Lines changed: 1145 additions & 18 deletions

File tree

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

Lines changed: 257 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -288,4 +288,260 @@
288288

289289
; (~x) | (~y) --> ~(x & y)
290290
(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)))
291+
(rule (simplify (bor ty (bnot ty y) (bnot ty x))) (bnot ty (band ty x y)))
292+
293+
; x | ((x ^ y) ^ z) --> x | (y ^ z)
294+
(rule (simplify (bor ty (bxor ty (bxor ty x y) z) x)) (bor ty (bxor ty y z) x))
295+
(rule (simplify (bor ty x (bxor ty (bxor ty x y) z))) (bor ty (bxor ty y z) x))
296+
(rule (simplify (bor ty (bxor ty z (bxor ty x y)) x)) (bor ty (bxor ty y z) x))
297+
(rule (simplify (bor ty x (bxor ty z (bxor ty x y)))) (bor ty (bxor ty y z) x))
298+
(rule (simplify (bor ty (bxor ty (bxor ty y x) z) x)) (bor ty (bxor ty y z) x))
299+
(rule (simplify (bor ty x (bxor ty (bxor ty y x) z))) (bor ty (bxor ty y z) x))
300+
(rule (simplify (bor ty (bxor ty z (bxor ty y x)) x)) (bor ty (bxor ty y z) x))
301+
(rule (simplify (bor ty x (bxor ty z (bxor ty y x)))) (bor ty (bxor ty y z) x))
302+
303+
; (x ^ z) == (y ^ z) --> x == y
304+
(rule (simplify (eq ty (bxor cty x z) (bxor cty y z))) (eq ty x y))
305+
(rule (simplify (eq ty (bxor cty y z) (bxor cty x z))) (eq ty x y))
306+
(rule (simplify (eq ty (bxor cty x z) (bxor cty z y))) (eq ty x y))
307+
(rule (simplify (eq ty (bxor cty z y) (bxor cty x z))) (eq ty x y))
308+
(rule (simplify (eq ty (bxor cty z x) (bxor cty y z))) (eq ty x y))
309+
(rule (simplify (eq ty (bxor cty y z) (bxor cty z x))) (eq ty x y))
310+
(rule (simplify (eq ty (bxor cty z x) (bxor cty z y))) (eq ty x y))
311+
(rule (simplify (eq ty (bxor cty z y) (bxor cty z x))) (eq ty x y))
312+
313+
; y | ~(x | y) --> y | ~x
314+
(rule (simplify (bor ty y (bnot ty (bor ty x y)))) (bor ty y (bnot ty x)))
315+
(rule (simplify (bor ty (bnot ty (bor ty x y)) y)) (bor ty y (bnot ty x)))
316+
(rule (simplify (bor ty y (bnot ty (bor ty y x)))) (bor ty y (bnot ty x)))
317+
(rule (simplify (bor ty (bnot ty (bor ty y x)) y)) (bor ty y (bnot ty x)))
318+
319+
; y & ~(x & y) --> y & ~x
320+
(rule (simplify (band ty y (bnot ty (band ty x y)))) (band ty y (bnot ty x)))
321+
(rule (simplify (band ty (bnot ty (band ty x y)) y)) (band ty y (bnot ty x)))
322+
(rule (simplify (band ty y (bnot ty (band ty y x)))) (band ty y (bnot ty x)))
323+
(rule (simplify (band ty (bnot ty (band ty y x)) y)) (band ty y (bnot ty x)))
324+
325+
; (~x) ^ (x | y) --> x | ~y
326+
(rule (simplify (bxor ty (bnot ty x) (bor ty x y))) (bor ty x (bnot ty y)))
327+
(rule (simplify (bxor ty (bor ty x y) (bnot ty x))) (bor ty x (bnot ty y)))
328+
(rule (simplify (bxor ty (bnot ty x) (bor ty y x))) (bor ty x (bnot ty y)))
329+
(rule (simplify (bxor ty (bor ty y x) (bnot ty x))) (bor ty x (bnot ty y)))
330+
331+
; (x < y) | (x > y) --> x != y
332+
(rule (simplify (bor ty (slt ty x y) (sgt ty x y))) (ne ty x y))
333+
(rule (simplify (bor ty (sgt ty x y) (slt ty x y))) (ne ty x y))
334+
(rule (simplify (bor ty (slt ty x y) (slt ty y x))) (ne ty x y))
335+
(rule (simplify (bor ty (slt ty y x) (slt ty x y))) (ne ty x y))
336+
(rule (simplify (bor ty (sgt ty y x) (sgt ty x y))) (ne ty x y))
337+
(rule (simplify (bor ty (sgt ty x y) (sgt ty y x))) (ne ty x y))
338+
(rule (simplify (bor ty (sgt ty y x) (slt ty y x))) (ne ty x y))
339+
(rule (simplify (bor ty (slt ty y x) (sgt ty y x))) (ne ty x y))
340+
341+
; (x <_u y) | (x >_u y) --> x != y
342+
(rule (simplify (bor ty (ult ty x y) (ugt ty x y))) (ne ty x y))
343+
(rule (simplify (bor ty (ugt ty x y) (ult ty x y))) (ne ty x y))
344+
(rule (simplify (bor ty (ult ty x y) (ult ty y x))) (ne ty x y))
345+
(rule (simplify (bor ty (ult ty y x) (ult ty x y))) (ne ty x y))
346+
(rule (simplify (bor ty (ugt ty y x) (ugt ty x y))) (ne ty x y))
347+
(rule (simplify (bor ty (ugt ty x y) (ugt ty y x))) (ne ty x y))
348+
(rule (simplify (bor ty (ugt ty y x) (ult ty y x))) (ne ty x y))
349+
(rule (simplify (bor ty (ult ty y x) (ugt ty y x))) (ne ty x y))
350+
351+
; ~((~x) & y) --> x | ~y
352+
(rule (simplify (bnot ty (band ty (bnot ty x) y))) (bor ty x (bnot ty y)))
353+
(rule (simplify (bnot ty (band ty y (bnot ty x)))) (bor ty x (bnot ty y)))
354+
355+
; ~((~x) | y) --> x & ~y
356+
(rule (simplify (bnot ty (bor ty (bnot ty x) y))) (band ty x (bnot ty y)))
357+
(rule (simplify (bnot ty (bor ty y (bnot ty x)))) (band ty x (bnot ty y)))
358+
359+
; (x <_u y) | (x == y) --> (x <=_u y)
360+
(rule (simplify (bor ty (ult ty x y) (eq ty x y))) (ule ty x y))
361+
(rule (simplify (bor ty (eq ty x y) (ult ty x y))) (ule ty x y))
362+
(rule (simplify (bor ty (ult ty x y) (eq ty y x))) (ule ty x y))
363+
(rule (simplify (bor ty (eq ty y x) (ult ty x y))) (ule ty x y))
364+
365+
; (y >_u x) | (x == y) --> (x <=_u y)
366+
(rule (simplify (bor ty (ugt ty y x) (eq ty x y))) (ule ty x y))
367+
(rule (simplify (bor ty (eq ty x y) (ugt ty y x))) (ule ty x y))
368+
(rule (simplify (bor ty (ugt ty y x) (eq ty y x))) (ule ty x y))
369+
(rule (simplify (bor ty (eq ty y x) (ugt ty y x))) (ule ty x y))
370+
371+
; (x < y) | (x == y) --> (x <= y)
372+
(rule (simplify (bor ty (slt ty x y) (eq ty x y))) (sle ty x y))
373+
(rule (simplify (bor ty (eq ty x y) (slt ty x y))) (sle ty x y))
374+
(rule (simplify (bor ty (slt ty x y) (eq ty y x))) (sle ty x y))
375+
(rule (simplify (bor ty (eq ty y x) (slt ty x y))) (sle ty x y))
376+
377+
; (y > x) | (x == y) --> (x <= y)
378+
(rule (simplify (bor ty (sgt ty y x) (eq ty x y))) (sle ty x y))
379+
(rule (simplify (bor ty (eq ty x y) (sgt ty y x))) (sle ty x y))
380+
(rule (simplify (bor ty (sgt ty y x) (eq ty y x))) (sle ty x y))
381+
(rule (simplify (bor ty (eq ty y x) (sgt ty y x))) (sle ty x y))
382+
383+
; (x ^ z) | (((x ^ z) ^ y)) --> (x ^ z) | y
384+
(rule (simplify (bor ty (bxor ty x z) (bxor ty (bxor ty x z) y))) (bor ty (bxor ty x z) y))
385+
(rule (simplify (bor ty (bxor ty (bxor ty x z) y) (bxor ty x z))) (bor ty (bxor ty x z) y))
386+
(rule (simplify (bor ty (bxor ty x z) (bxor ty y (bxor ty x z)))) (bor ty (bxor ty x z) y))
387+
(rule (simplify (bor ty (bxor ty y (bxor ty x z)) (bxor ty x z))) (bor ty (bxor ty x z) y))
388+
389+
(rule (simplify (bor ty (bxor ty x z) (bxor ty (bxor ty z x) y))) (bor ty (bxor ty x z) y))
390+
(rule (simplify (bor ty (bxor ty (bxor ty z x) y) (bxor ty x z))) (bor ty (bxor ty x z) y))
391+
(rule (simplify (bor ty (bxor ty x z) (bxor ty y (bxor ty z x)))) (bor ty (bxor ty x z) y))
392+
(rule (simplify (bor ty (bxor ty y (bxor ty z x)) (bxor ty x z))) (bor ty (bxor ty x z) y))
393+
394+
(rule (simplify (bor ty (bxor ty z x) (bxor ty (bxor ty x z) y))) (bor ty (bxor ty x z) y))
395+
(rule (simplify (bor ty (bxor ty (bxor ty x z) y) (bxor ty z x))) (bor ty (bxor ty x z) y))
396+
(rule (simplify (bor ty (bxor ty z x) (bxor ty y (bxor ty x z)))) (bor ty (bxor ty x z) y))
397+
(rule (simplify (bor ty (bxor ty y (bxor ty x z)) (bxor ty z x))) (bor ty (bxor ty x z) y))
398+
399+
(rule (simplify (bor ty (bxor ty z x) (bxor ty (bxor ty z x) y))) (bor ty (bxor ty x z) y))
400+
(rule (simplify (bor ty (bxor ty (bxor ty z x) y) (bxor ty z x))) (bor ty (bxor ty x z) y))
401+
(rule (simplify (bor ty (bxor ty z x) (bxor ty y (bxor ty z x)))) (bor ty (bxor ty x z) y))
402+
(rule (simplify (bor ty (bxor ty y (bxor ty z x)) (bxor ty z x))) (bor ty (bxor ty x z) y))
403+
404+
; x | (x ^ y) --> x | y
405+
(rule (simplify (bor ty x (bxor ty x y))) (bor ty x y))
406+
(rule (simplify (bor ty (bxor ty x y) x)) (bor ty x y))
407+
(rule (simplify (bor ty x (bxor ty y x))) (bor ty x y))
408+
(rule (simplify (bor ty (bxor ty y x) x)) (bor ty x y))
409+
410+
; ~((~x) + y) --> x - y
411+
(rule (simplify (bnot ty (iadd ty (bnot ty x) y))) (isub ty x y))
412+
(rule (simplify (bnot ty (iadd ty y (bnot ty x)))) (isub ty x y))
413+
414+
; (x ^ z) | (y | x) --> (y | x) | z
415+
(rule (simplify (bor ty (bxor ty x z) (bor ty y x))) (bor ty (bor ty y x) z))
416+
(rule (simplify (bor ty (bor ty y x) (bxor ty x z))) (bor ty (bor ty y x) z))
417+
(rule (simplify (bor ty (bxor ty x z) (bor ty x y))) (bor ty (bor ty y x) z))
418+
(rule (simplify (bor ty (bor ty x y) (bxor ty x z))) (bor ty (bor ty y x) z))
419+
(rule (simplify (bor ty (bxor ty z x) (bor ty y x))) (bor ty (bor ty y x) z))
420+
(rule (simplify (bor ty (bor ty y x) (bxor ty z x))) (bor ty (bor ty y x) z))
421+
(rule (simplify (bor ty (bxor ty z x) (bor ty x y))) (bor ty (bor ty y x) z))
422+
(rule (simplify (bor ty (bor ty x y) (bxor ty z x))) (bor ty (bor ty y x) z))
423+
424+
; (x | y) ^ (x ^ y) --> x & y
425+
(rule (simplify (bxor ty (bor ty y x) (bxor ty y x))) (band ty x y))
426+
(rule (simplify (bxor ty (bxor ty y x) (bor ty y x))) (band ty x y))
427+
(rule (simplify (bxor ty (bor ty y x) (bxor ty x y))) (band ty x y))
428+
(rule (simplify (bxor ty (bxor ty x y) (bor ty y x))) (band ty x y))
429+
(rule (simplify (bxor ty (bor ty x y) (bxor ty y x))) (band ty x y))
430+
(rule (simplify (bxor ty (bxor ty y x) (bor ty x y))) (band ty x y))
431+
(rule (simplify (bxor ty (bor ty x y) (bxor ty x y))) (band ty x y))
432+
(rule (simplify (bxor ty (bxor ty x y) (bor ty x y))) (band ty x y))
433+
434+
; x | (z & (x ^ y)) --> x | (z & y)
435+
(rule (simplify (bor ty (band ty (bxor ty y x) z) x)) (bor ty (band ty y z) x))
436+
(rule (simplify (bor ty x (band ty (bxor ty y x) z))) (bor ty (band ty y z) x))
437+
(rule (simplify (bor ty (band ty z (bxor ty y x)) x)) (bor ty (band ty y z) x))
438+
(rule (simplify (bor ty x (band ty z (bxor ty y x)))) (bor ty (band ty y z) x))
439+
(rule (simplify (bor ty (band ty (bxor ty x y) z) x)) (bor ty (band ty y z) x))
440+
(rule (simplify (bor ty x (band ty (bxor ty x y) z))) (bor ty (band ty y z) x))
441+
(rule (simplify (bor ty (band ty z (bxor ty x y)) x)) (bor ty (band ty y z) x))
442+
(rule (simplify (bor ty x (band ty z (bxor ty x y)))) (bor ty (band ty y z) x))
443+
444+
; (x | y) | (x ^ z) --> (x | y) | z
445+
(rule (simplify (bor ty (bor ty x y) (bxor ty x z))) (bor ty (bor ty x y) z))
446+
(rule (simplify (bor ty (bxor ty x z) (bor ty x y))) (bor ty (bor ty x y) z))
447+
(rule (simplify (bor ty (bor ty x y) (bxor ty z x))) (bor ty (bor ty x y) z))
448+
(rule (simplify (bor ty (bxor ty z x) (bor ty x y))) (bor ty (bor ty x y) z))
449+
(rule (simplify (bor ty (bor ty y x) (bxor ty x z))) (bor ty (bor ty x y) z))
450+
(rule (simplify (bor ty (bxor ty x z) (bor ty y x))) (bor ty (bor ty x y) z))
451+
(rule (simplify (bor ty (bor ty y x) (bxor ty z x))) (bor ty (bor ty x y) z))
452+
(rule (simplify (bor ty (bxor ty z x) (bor ty y x))) (bor ty (bor ty x y) z))
453+
454+
; (x ^ z) != (y ^ z) --> x != y
455+
(rule (simplify (ne ty (bxor cty x z) (bxor cty y z))) (ne ty x y))
456+
(rule (simplify (ne ty (bxor cty y z) (bxor cty x z))) (ne ty x y))
457+
(rule (simplify (ne ty (bxor cty x z) (bxor cty z y))) (ne ty x y))
458+
(rule (simplify (ne ty (bxor cty z y) (bxor cty x z))) (ne ty x y))
459+
(rule (simplify (ne ty (bxor cty z x) (bxor cty y z))) (ne ty x y))
460+
(rule (simplify (ne ty (bxor cty y z) (bxor cty z x))) (ne ty x y))
461+
(rule (simplify (ne ty (bxor cty z x) (bxor cty z y))) (ne ty x y))
462+
(rule (simplify (ne ty (bxor cty z y) (bxor cty z x))) (ne ty x y))
463+
464+
; (x & y) | (x & ~y) --> x
465+
(rule (simplify (bor ty (band ty x y) (band ty x (bnot ty y)))) x)
466+
(rule (simplify (bor ty (band ty x (bnot ty y)) (band ty x y))) x)
467+
(rule (simplify (bor ty (band ty x y) (band ty (bnot ty y) x))) x)
468+
(rule (simplify (bor ty (band ty (bnot ty y) x) (band ty x y))) x)
469+
(rule (simplify (bor ty (band ty y x) (band ty x (bnot ty y)))) x)
470+
(rule (simplify (bor ty (band ty x (bnot ty y)) (band ty y x))) x)
471+
(rule (simplify (bor ty (band ty y x) (band ty (bnot ty y) x))) x)
472+
(rule (simplify (bor ty (band ty (bnot ty y) x) (band ty y x))) x)
473+
474+
; (x | y) & (x | ~y) --> x
475+
(rule (simplify (band ty (bor ty x y) (bor ty x (bnot ty y)))) x)
476+
(rule (simplify (band ty (bor ty x (bnot ty y)) (bor ty x y))) x)
477+
(rule (simplify (band ty (bor ty x y) (bor ty (bnot ty y) x))) x)
478+
(rule (simplify (band ty (bor ty (bnot ty y) x) (bor ty x y))) x)
479+
(rule (simplify (band ty (bor ty y x) (bor ty x (bnot ty y)))) x)
480+
(rule (simplify (band ty (bor ty x (bnot ty y)) (bor ty y x))) x)
481+
(rule (simplify (band ty (bor ty y x) (bor ty (bnot ty y) x))) x)
482+
(rule (simplify (band ty (bor ty (bnot ty y) x) (bor ty y x))) x)
483+
484+
; (x ^ y) | ~x --> ~(x & y)
485+
(rule (simplify (bor ty (bxor ty y x) (bnot ty x))) (bnot ty (band ty y x)))
486+
(rule (simplify (bor ty (bnot ty x) (bxor ty y x))) (bnot ty (band ty y x)))
487+
(rule (simplify (bor ty (bxor ty x y) (bnot ty x))) (bnot ty (band ty y x)))
488+
(rule (simplify (bor ty (bnot ty x) (bxor ty x y))) (bnot ty (band ty y x)))
489+
490+
; (x ^ y) ^ x --> y
491+
(rule (simplify (bxor ty (bxor ty x y) x)) y)
492+
(rule (simplify (bxor ty x (bxor ty x y))) y)
493+
(rule (simplify (bxor ty (bxor ty y x) x)) y)
494+
(rule (simplify (bxor ty x (bxor ty y x))) y)
495+
496+
; y | (x & (y | z)) --> y | (x & z)
497+
(rule (simplify (bor ty (band ty x (bor ty y z)) y)) (bor ty (band ty x z) y))
498+
(rule (simplify (bor ty y (band ty x (bor ty y z)))) (bor ty (band ty x z) y))
499+
(rule (simplify (bor ty (band ty (bor ty y z) x) y)) (bor ty (band ty x z) y))
500+
(rule (simplify (bor ty y (band ty (bor ty y z) x))) (bor ty (band ty x z) y))
501+
(rule (simplify (bor ty (band ty x (bor ty z y)) y)) (bor ty (band ty x z) y))
502+
(rule (simplify (bor ty y (band ty x (bor ty z y)))) (bor ty (band ty x z) y))
503+
(rule (simplify (bor ty (band ty (bor ty z y) x) y)) (bor ty (band ty x z) y))
504+
(rule (simplify (bor ty y (band ty (bor ty z y) x))) (bor ty (band ty x z) y))
505+
506+
; y & (x | (y & z)) --> y & (x | z)
507+
(rule (simplify (band ty (bor ty x (band ty y z)) y)) (band ty (bor ty x z) y))
508+
(rule (simplify (band ty y (bor ty x (band ty y z)))) (band ty (bor ty x z) y))
509+
(rule (simplify (band ty (bor ty (band ty y z) x) y)) (band ty (bor ty x z) y))
510+
(rule (simplify (band ty y (bor ty (band ty y z) x))) (band ty (bor ty x z) y))
511+
(rule (simplify (band ty (bor ty x (band ty z y)) y)) (band ty (bor ty x z) y))
512+
(rule (simplify (band ty y (bor ty x (band ty z y)))) (band ty (bor ty x z) y))
513+
(rule (simplify (band ty (bor ty (band ty z y) x) y)) (band ty (bor ty x z) y))
514+
(rule (simplify (band ty y (bor ty (band ty z y) x))) (band ty (bor ty x z) y))
515+
516+
; y | (x ^ (y & z)) --> x | y
517+
(rule (simplify (bor ty (bxor ty x (band ty y z)) y)) (bor ty x y))
518+
(rule (simplify (bor ty y (bxor ty x (band ty y z)))) (bor ty x y))
519+
(rule (simplify (bor ty (bxor ty (band ty y z) x) y)) (bor ty x y))
520+
(rule (simplify (bor ty y (bxor ty (band ty y z) x))) (bor ty x y))
521+
(rule (simplify (bor ty (bxor ty x (band ty z y)) y)) (bor ty x y))
522+
(rule (simplify (bor ty y (bxor ty x (band ty z y)))) (bor ty x y))
523+
(rule (simplify (bor ty (bxor ty (band ty z y) x) y)) (bor ty x y))
524+
(rule (simplify (bor ty y (bxor ty (band ty z y) x))) (bor ty x y))
525+
526+
; ((x & y) ^ y) + z --> (y + z) - (x & y)
527+
(rule (simplify (iadd ty (bxor ty (band ty x y) y) z)) (isub ty (iadd ty y z) (band ty x y)))
528+
(rule (simplify (iadd ty z (bxor ty (band ty x y) y))) (isub ty (iadd ty y z) (band ty x y)))
529+
(rule (simplify (iadd ty (bxor ty y (band ty x y)) z)) (isub ty (iadd ty y z) (band ty x y)))
530+
(rule (simplify (iadd ty z (bxor ty y (band ty x y)))) (isub ty (iadd ty y z) (band ty x y)))
531+
(rule (simplify (iadd ty (bxor ty (band ty y x) y) z)) (isub ty (iadd ty y z) (band ty x y)))
532+
(rule (simplify (iadd ty z (bxor ty (band ty y x) y))) (isub ty (iadd ty y z) (band ty x y)))
533+
(rule (simplify (iadd ty (bxor ty y (band ty y x)) z)) (isub ty (iadd ty y z) (band ty x y)))
534+
(rule (simplify (iadd ty z (bxor ty y (band ty y x)))) (isub ty (iadd ty y z) (band ty x y)))
535+
536+
; y & (~y | x) --> y & x
537+
(rule (simplify (band ty y (bor ty (bnot ty y) x))) (band ty y x))
538+
(rule (simplify (band ty (bor ty (bnot ty y) x) y)) (band ty y x))
539+
(rule (simplify (band ty y (bor ty x (bnot ty y)))) (band ty y x))
540+
(rule (simplify (band ty (bor ty x (bnot ty y)) y)) (band ty y x))
541+
542+
; y | (~y & x) --> y | x
543+
(rule (simplify (bor ty y (band ty (bnot ty y) x))) (bor ty y x))
544+
(rule (simplify (bor ty (band ty (bnot ty y) x) y)) (bor ty y x))
545+
(rule (simplify (bor ty y (band ty x (bnot ty y)))) (bor ty y x))
546+
(rule (simplify (bor ty (band ty x (bnot ty y)) y)) (bor ty y x))
547+

0 commit comments

Comments
 (0)