Skip to content

ISLE opts for x ± a == y ± b #10489

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
cfallin merged 3 commits into from
Mar 30, 2025
Merged

ISLE opts for x ± a == y ± b #10489

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
2df12fa
ISLE opts for `x ± a == y ± b`
scottmcm Mar 30, 2025
5ad157d
Don't reassociate across `==` without a reason
scottmcm Mar 30, 2025
ec68ada
Subsume when we made it strictly better, and handle more orderings
scottmcm Mar 30, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
18 changes: 18 additions & 0 deletions cranelift/codegen/src/opts/cprop.isle
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -172,6 +172,24 @@
(rule (simplify (select ty (iconst_u _ 0) _ y))
(subsume y))

;; Reassociate across `==`/`!=` when we can simplify a constant
;; `x + K1 == K2` --> `x == K2 - K1`
(rule (simplify (eq ty1 (iadd ty2 x k1@(iconst _ _)) k2@(iconst _ _)))
(eq ty1 x (isub ty2 k2 k1)))
(rule (simplify (ne ty1 (iadd ty2 x k1@(iconst _ _)) k2@(iconst _ _)))
(ne ty1 x (isub ty2 k2 k1)))
;; `x - K1 == K2` --> `x == K2 + K1`
(rule (simplify (eq ty1 (isub ty2 x k1@(iconst _ _)) k2@(iconst _ _)))
(eq ty1 x (iadd ty2 k2 k1)))
(rule (simplify (ne ty1 (isub ty2 x k1@(iconst _ _)) k2@(iconst _ _)))
(ne ty1 x (iadd ty2 k2 k1)))
;; `x + K1 == y + K2` --> `x == y + (K2 - K1)`
(rule (simplify (eq ty1 (iadd ty2 x k1@(iconst _ _)) (iadd ty3 y k2@(iconst _ _))))
(eq ty1 x (iadd ty2 y (isub ty3 k2 k1))))
(rule (simplify (ne ty1 (iadd ty2 x k1@(iconst _ _)) (iadd ty3 y k2@(iconst _ _))))
(ne ty1 x (iadd ty2 y (isub ty3 k2 k1))))
;; An icmp rule normalizes (eq sub sub), so we don't need to handle it here.

;; Replace subtraction by a "negative" constant with addition.
;; Notably, this gives `x - (-1) == x + 1`, so other patterns don't have to
;; match the subtract-negative-one version too.
Expand Down
30 changes: 30 additions & 0 deletions cranelift/codegen/src/opts/icmp.isle
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,6 +13,36 @@
(rule (simplify (slt (ty_int ty) x x)) (subsume (iconst_u ty 0)))
(rule (simplify (sle (ty_int ty) x x)) (subsume (iconst_u ty 1)))

;; For integers, adding the same thing on both sides of an equality check
;; (or an inequality check) doesn't change the result.
;; This applies for arbitrary expressions, not just constants, so we need to
;; check all possible orderings since nothing normalizes it.

(rule (simplify (eq ty (iadd _ a k) (iadd _ b k)))
(subsume (eq ty a b)))
(rule (simplify (eq ty (iadd _ a k) (iadd _ k b)))
(subsume (eq ty a b)))
(rule (simplify (eq ty (iadd _ k a) (iadd _ b k)))
(subsume (eq ty a b)))
(rule (simplify (eq ty (iadd _ k a) (iadd _ k b)))
(subsume (eq ty a b)))
(rule (simplify (ne ty (iadd _ a k) (iadd _ b k)))
(subsume (ne ty a b)))
(rule (simplify (ne ty (iadd _ a k) (iadd _ k b)))
(subsume (ne ty a b)))
(rule (simplify (ne ty (iadd _ k a) (iadd _ b k)))
(subsume (ne ty a b)))
(rule (simplify (ne ty (iadd _ k a) (iadd _ k b)))
(subsume (ne ty a b)))

;; To avoid repeating all the above rules again, normalize isub to iadd
;; (a - b) == (c - d) ⟹ (a + d) == (c + b)

(rule (simplify (eq ty1 (isub ty2 a b) (isub ty3 c d)))
(eq ty1 (iadd ty2 a d) (iadd ty3 c b)))
(rule (simplify (ne ty1 (isub ty2 a b) (isub ty3 c d)))
(ne ty1 (iadd ty2 a d) (iadd ty3 c b)))

;; Optimize icmp-of-icmp.
;; ne(icmp(ty, cc, x, y), 0) == icmp(ty, cc, x, y)
;; e.g. neq(ugt(x, y), 0) == ugt(x, y)
Expand Down
11 changes: 11 additions & 0 deletions cranelift/filetests/filetests/egraph/arithmetic.clif
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -124,6 +124,17 @@ block0(v0: i32):
; check: return v6
}

function %mul2_ne_add(i32, i32) -> i8 {
block0(v0: i32, v1: i32):
v2 = iconst.i32 2
v3 = imul v0, v2
v4 = iadd v1, v0
v5 = icmp ne v3, v4
return v5
; check: v11 = icmp ne v0, v1
; check: return v11
}

function %mul_minus_one(i32) -> i32 {
block0(v0: i32):
v1 = iconst.i32 0xffff_ffff ; -1
Expand Down
52 changes: 52 additions & 0 deletions cranelift/filetests/filetests/egraph/cprop.clif
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -231,6 +231,58 @@ block0:
; check: v3 = iconst.i8 0
; nextln: return v3

function %icmp_sums_same_addend(i32, i32, i32) -> i8 {
block0(v0: i32, v1: i32, v2: i32):
v3 = iadd v0, v2
v4 = iadd v1, v2
v5 = icmp eq v3, v4
return v5
}

; check: v6 = icmp eq v0, v1
; nextln: return v6

function %icmp_subs_same_minuend(i32, i32, i32) -> i8 {
block0(v0: i32, v1: i32, v2: i32):
v3 = isub v0, v1
v4 = isub v0, v2
v5 = icmp eq v3, v4
return v5
}

; check: v9 = icmp eq v2, v1
; nextln: return v9

function %icmp_sums_const_addends(i32, i32) -> i8 {
block0(v0: i32, v1: i32):
v3 = iconst.i32 123
v4 = iconst.i32 456
v5 = iadd v0, v3
v6 = iadd v1, v4
v7 = icmp eq v5, v6
return v7
}

; check: v9 = iconst.i32 333
; check: v19 = iadd v1, v9
; check: v20 = icmp eq v0, v19
; nextln: return v20

function %icmp_subs_const_addends(i32, i32) -> i8 {
block0(v0: i32, v1: i32):
v3 = iconst.i32 123
v4 = iconst.i32 456
v5 = isub v3, v0
v6 = isub v4, v1
v7 = icmp eq v5, v6
return v7
}

; check: v42 = iconst.i32 333
; check: v51 = iadd v0, v42
; check: v52 = icmp eq v1, v51
; nextln: return v52

function %ireduce_iconst() -> i8 {
block0:
v1 = iconst.i16 -10
Expand Down
47 changes: 23 additions & 24 deletions tests/disas/gc/drc/externref-globals.wat
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -108,46 +108,45 @@
;; @003b v39 = load.i64 notrap aligned readonly can_move v0+40
;; @003b v20 = iadd v39, v16
;; @003b v21 = load.i64 notrap aligned v20
;; v67 = iconst.i64 1
;; @003b v22 = iadd v21, v67 ; v67 = 1
;; v73 = iconst.i64 1
;; @003b v22 = iadd v21, v73 ; v73 = 1
;; @003b store notrap aligned v22, v20
;; @003b jump block3
;;
;; block3:
;; v72 = iadd.i64 v0, v64 ; v64 = 80
;; @003b store.i32 notrap aligned v2, v72
;; v73 = iconst.i32 1
;; v74 = band.i32 v5, v73 ; v73 = 1
;; v75 = iconst.i32 0
;; v76 = icmp.i32 eq v5, v75 ; v75 = 0
;; @003b v36 = uextend.i32 v76
;; @003b v37 = bor v74, v36
;; v85 = iadd.i64 v0, v64 ; v64 = 80
;; @003b store.i32 notrap aligned v2, v85
;; v86 = iconst.i32 1
;; v87 = band.i32 v5, v86 ; v86 = 1
;; v88 = iconst.i32 0
;; v89 = icmp.i32 eq v5, v88 ; v88 = 0
;; @003b v36 = uextend.i32 v89
;; @003b v37 = bor v87, v36
;; @003b brif v37, block7, block4
;;
;; block4:
;; @003b v42 = uextend.i64 v5
;; v77 = iconst.i64 8
;; @003b v44 = uadd_overflow_trap v42, v77, user1 ; v77 = 8
;; @003b v46 = uadd_overflow_trap v44, v77, user1 ; v77 = 8
;; v78 = load.i64 notrap aligned readonly can_move v0+48
;; @003b v47 = icmp ule v46, v78
;; v90 = iconst.i64 8
;; @003b v44 = uadd_overflow_trap v42, v90, user1 ; v90 = 8
;; @003b v46 = uadd_overflow_trap v44, v90, user1 ; v90 = 8
;; v91 = load.i64 notrap aligned readonly can_move v0+48
;; @003b v47 = icmp ule v46, v91
;; @003b trapz v47, user1
;; v79 = load.i64 notrap aligned readonly can_move v0+40
;; @003b v48 = iadd v79, v44
;; v92 = load.i64 notrap aligned readonly can_move v0+40
;; @003b v48 = iadd v92, v44
;; @003b v49 = load.i64 notrap aligned v48
;; v70 = iconst.i64 -1
;; @003b v50 = iadd v49, v70 ; v70 = -1
;; v71 = iconst.i64 0
;; @003b v51 = icmp eq v50, v71 ; v71 = 0
;; @003b brif v51, block5, block6
;; v93 = iconst.i64 1
;; v83 = icmp eq v49, v93 ; v93 = 1
;; @003b brif v83, block5, block6
Comment on lines -138 to +140
Copy link
Contributor Author

@scottmcm scottmcm Mar 30, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

A case in the wild, here: was a + -1 == 0, now a == 1.

;;
;; block5 cold:
;; @003b call fn0(v0, v5)
;; @003b jump block7
;;
;; block6:
;; v80 = iadd.i64 v49, v70 ; v70 = -1
;; @003b store notrap aligned v80, v48
;; v70 = iconst.i64 -1
;; @003b v50 = iadd.i64 v49, v70 ; v70 = -1
;; @003b store notrap aligned v50, v48
;; @003b jump block7
;;
;; block7:
Expand Down
35 changes: 17 additions & 18 deletions tests/disas/gc/drc/struct-set.wat
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -110,43 +110,42 @@
;; @004a trapz v30, user1
;; @004a v31 = iadd.i64 v6, v27
;; @004a v32 = load.i64 notrap aligned v31
;; v77 = iconst.i64 1
;; @004a v33 = iadd v32, v77 ; v77 = 1
;; v84 = iconst.i64 1
;; @004a v33 = iadd v32, v84 ; v84 = 1
;; @004a store notrap aligned v33, v31
;; @004a jump block3
;;
;; block3:
;; @004a store.i32 notrap aligned little v3, v15
;; v83 = iconst.i32 1
;; v84 = band.i32 v16, v83 ; v83 = 1
;; v85 = iconst.i32 0
;; v86 = icmp.i32 eq v16, v85 ; v85 = 0
;; @004a v47 = uextend.i32 v86
;; @004a v48 = bor v84, v47
;; v96 = iconst.i32 1
;; v97 = band.i32 v16, v96 ; v96 = 1
;; v98 = iconst.i32 0
;; v99 = icmp.i32 eq v16, v98 ; v98 = 0
;; @004a v47 = uextend.i32 v99
;; @004a v48 = bor v97, v47
;; @004a brif v48, block7, block4
;;
;; block4:
;; @004a v53 = uextend.i64 v16
;; v87 = iconst.i64 8
;; @004a v55 = uadd_overflow_trap v53, v87, user1 ; v87 = 8
;; @004a v57 = uadd_overflow_trap v55, v87, user1 ; v87 = 8
;; v100 = iconst.i64 8
;; @004a v55 = uadd_overflow_trap v53, v100, user1 ; v100 = 8
;; @004a v57 = uadd_overflow_trap v55, v100, user1 ; v100 = 8
;; @004a v58 = icmp ule v57, v8
;; @004a trapz v58, user1
;; @004a v59 = iadd.i64 v6, v55
;; @004a v60 = load.i64 notrap aligned v59
;; v80 = iconst.i64 -1
;; @004a v61 = iadd v60, v80 ; v80 = -1
;; v81 = iconst.i64 0
;; @004a v62 = icmp eq v61, v81 ; v81 = 0
;; @004a brif v62, block5, block6
;; v101 = iconst.i64 1
;; v94 = icmp eq v60, v101 ; v101 = 1
;; @004a brif v94, block5, block6
;;
;; block5 cold:
;; @004a call fn0(v0, v16)
;; @004a jump block7
;;
;; block6:
;; v88 = iadd.i64 v60, v80 ; v80 = -1
;; @004a store notrap aligned v88, v59
;; v80 = iconst.i64 -1
;; @004a v61 = iadd.i64 v60, v80 ; v80 = -1
;; @004a store notrap aligned v61, v59
;; @004a jump block7
;;
;; block7:
Expand Down
17 changes: 8 additions & 9 deletions tests/disas/pulley/memory-inbounds.wat
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -64,15 +64,14 @@
;;
;; wasm[0]::function[6]::offset_just_bad_v2:
;; push_frame
;; xload64le_o32 x10, x0, 88
;; xsub64_u32 x10, x10, 65536
;; xzero x11
;; xload64le_o32 x12, x0, 80
;; xadd64_u32 x12, x12, 65533
;; xzero x8
;; xeq64 x10, x10, x8
;; xselect64 x12, x10, x11, x12
;; xload32le_z x0, x12, 0
;; xload64le_o32 x9, x0, 88
;; xzero x10
;; xload64le_o32 x11, x0, 80
;; xadd64_u32 x11, x11, 65533
;; xconst32 x7, 65536
;; xeq64 x9, x9, x7
;; xselect64 x11, x9, x10, x11
;; xload32le_z x0, x11, 0
;; pop_frame
;; ret
;;
Expand Down