Skip to content

Commit 3468026

Browse files
scottmcmscottmcm
authored
ISLE opts for x ± a == y ± b (#10489)
* ISLE opts for `x ± a == y ± b` * Don't reassociate across `==` without a reason Thinking more, it doesn't seem worth it to just change `x + 1 == y` to `x == y - 1` *always*. * Subsume when we made it strictly better, and handle more orderings
1 parent a968b7d commit 3468026

File tree

7 files changed

+159
-51
lines changed

7 files changed

+159
-51
lines changed

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

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -172,6 +172,24 @@
172172
(rule (simplify (select ty (iconst_u _ 0) _ y))
173173
(subsume y))
174174

175+
;; Reassociate across `==`/`!=` when we can simplify a constant
176+
;; `x + K1 == K2` --> `x == K2 - K1`
177+
(rule (simplify (eq ty1 (iadd ty2 x k1@(iconst _ _)) k2@(iconst _ _)))
178+
(eq ty1 x (isub ty2 k2 k1)))
179+
(rule (simplify (ne ty1 (iadd ty2 x k1@(iconst _ _)) k2@(iconst _ _)))
180+
(ne ty1 x (isub ty2 k2 k1)))
181+
;; `x - K1 == K2` --> `x == K2 + K1`
182+
(rule (simplify (eq ty1 (isub ty2 x k1@(iconst _ _)) k2@(iconst _ _)))
183+
(eq ty1 x (iadd ty2 k2 k1)))
184+
(rule (simplify (ne ty1 (isub ty2 x k1@(iconst _ _)) k2@(iconst _ _)))
185+
(ne ty1 x (iadd ty2 k2 k1)))
186+
;; `x + K1 == y + K2` --> `x == y + (K2 - K1)`
187+
(rule (simplify (eq ty1 (iadd ty2 x k1@(iconst _ _)) (iadd ty3 y k2@(iconst _ _))))
188+
(eq ty1 x (iadd ty2 y (isub ty3 k2 k1))))
189+
(rule (simplify (ne ty1 (iadd ty2 x k1@(iconst _ _)) (iadd ty3 y k2@(iconst _ _))))
190+
(ne ty1 x (iadd ty2 y (isub ty3 k2 k1))))
191+
;; An icmp rule normalizes (eq sub sub), so we don't need to handle it here.
192+
175193
;; Replace subtraction by a "negative" constant with addition.
176194
;; Notably, this gives `x - (-1) == x + 1`, so other patterns don't have to
177195
;; match the subtract-negative-one version too.

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

Lines changed: 30 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -13,6 +13,36 @@
1313
(rule (simplify (slt (ty_int ty) x x)) (subsume (iconst_u ty 0)))
1414
(rule (simplify (sle (ty_int ty) x x)) (subsume (iconst_u ty 1)))
1515

16+
;; For integers, adding the same thing on both sides of an equality check
17+
;; (or an inequality check) doesn't change the result.
18+
;; This applies for arbitrary expressions, not just constants, so we need to
19+
;; check all possible orderings since nothing normalizes it.
20+
21+
(rule (simplify (eq ty (iadd _ a k) (iadd _ b k)))
22+
(subsume (eq ty a b)))
23+
(rule (simplify (eq ty (iadd _ a k) (iadd _ k b)))
24+
(subsume (eq ty a b)))
25+
(rule (simplify (eq ty (iadd _ k a) (iadd _ b k)))
26+
(subsume (eq ty a b)))
27+
(rule (simplify (eq ty (iadd _ k a) (iadd _ k b)))
28+
(subsume (eq ty a b)))
29+
(rule (simplify (ne ty (iadd _ a k) (iadd _ b k)))
30+
(subsume (ne ty a b)))
31+
(rule (simplify (ne ty (iadd _ a k) (iadd _ k b)))
32+
(subsume (ne ty a b)))
33+
(rule (simplify (ne ty (iadd _ k a) (iadd _ b k)))
34+
(subsume (ne ty a b)))
35+
(rule (simplify (ne ty (iadd _ k a) (iadd _ k b)))
36+
(subsume (ne ty a b)))
37+
38+
;; To avoid repeating all the above rules again, normalize isub to iadd
39+
;; (a - b) == (c - d) ⟹ (a + d) == (c + b)
40+
41+
(rule (simplify (eq ty1 (isub ty2 a b) (isub ty3 c d)))
42+
(eq ty1 (iadd ty2 a d) (iadd ty3 c b)))
43+
(rule (simplify (ne ty1 (isub ty2 a b) (isub ty3 c d)))
44+
(ne ty1 (iadd ty2 a d) (iadd ty3 c b)))
45+
1646
;; Optimize icmp-of-icmp.
1747
;; ne(icmp(ty, cc, x, y), 0) == icmp(ty, cc, x, y)
1848
;; e.g. neq(ugt(x, y), 0) == ugt(x, y)

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

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -124,6 +124,17 @@ block0(v0: i32):
124124
; check: return v6
125125
}
126126

127+
function %mul2_ne_add(i32, i32) -> i8 {
128+
block0(v0: i32, v1: i32):
129+
v2 = iconst.i32 2
130+
v3 = imul v0, v2
131+
v4 = iadd v1, v0
132+
v5 = icmp ne v3, v4
133+
return v5
134+
; check: v11 = icmp ne v0, v1
135+
; check: return v11
136+
}
137+
127138
function %mul_minus_one(i32) -> i32 {
128139
block0(v0: i32):
129140
v1 = iconst.i32 0xffff_ffff ; -1

‎cranelift/filetests/filetests/egraph/cprop.clif‎

Lines changed: 52 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -231,6 +231,58 @@ block0:
231231
; check: v3 = iconst.i8 0
232232
; nextln: return v3
233233

234+
function %icmp_sums_same_addend(i32, i32, i32) -> i8 {
235+
block0(v0: i32, v1: i32, v2: i32):
236+
v3 = iadd v0, v2
237+
v4 = iadd v1, v2
238+
v5 = icmp eq v3, v4
239+
return v5
240+
}
241+
242+
; check: v6 = icmp eq v0, v1
243+
; nextln: return v6
244+
245+
function %icmp_subs_same_minuend(i32, i32, i32) -> i8 {
246+
block0(v0: i32, v1: i32, v2: i32):
247+
v3 = isub v0, v1
248+
v4 = isub v0, v2
249+
v5 = icmp eq v3, v4
250+
return v5
251+
}
252+
253+
; check: v9 = icmp eq v2, v1
254+
; nextln: return v9
255+
256+
function %icmp_sums_const_addends(i32, i32) -> i8 {
257+
block0(v0: i32, v1: i32):
258+
v3 = iconst.i32 123
259+
v4 = iconst.i32 456
260+
v5 = iadd v0, v3
261+
v6 = iadd v1, v4
262+
v7 = icmp eq v5, v6
263+
return v7
264+
}
265+
266+
; check: v9 = iconst.i32 333
267+
; check: v19 = iadd v1, v9
268+
; check: v20 = icmp eq v0, v19
269+
; nextln: return v20
270+
271+
function %icmp_subs_const_addends(i32, i32) -> i8 {
272+
block0(v0: i32, v1: i32):
273+
v3 = iconst.i32 123
274+
v4 = iconst.i32 456
275+
v5 = isub v3, v0
276+
v6 = isub v4, v1
277+
v7 = icmp eq v5, v6
278+
return v7
279+
}
280+
281+
; check: v42 = iconst.i32 333
282+
; check: v51 = iadd v0, v42
283+
; check: v52 = icmp eq v1, v51
284+
; nextln: return v52
285+
234286
function %ireduce_iconst() -> i8 {
235287
block0:
236288
v1 = iconst.i16 -10

‎tests/disas/gc/drc/externref-globals.wat‎

Lines changed: 23 additions & 24 deletions
Original file line numberDiff line numberDiff line change
@@ -108,46 +108,45 @@
108108
;; @003b v39 = load.i64 notrap aligned readonly can_move v0+40
109109
;; @003b v20 = iadd v39, v16
110110
;; @003b v21 = load.i64 notrap aligned v20
111-
;; v67 = iconst.i64 1
112-
;; @003b v22 = iadd v21, v67 ; v67 = 1
111+
;; v73 = iconst.i64 1
112+
;; @003b v22 = iadd v21, v73 ; v73 = 1
113113
;; @003b store notrap aligned v22, v20
114114
;; @003b jump block3
115115
;;
116116
;; block3:
117-
;; v72 = iadd.i64 v0, v64 ; v64 = 80
118-
;; @003b store.i32 notrap aligned v2, v72
119-
;; v73 = iconst.i32 1
120-
;; v74 = band.i32 v5, v73 ; v73 = 1
121-
;; v75 = iconst.i32 0
122-
;; v76 = icmp.i32 eq v5, v75 ; v75 = 0
123-
;; @003b v36 = uextend.i32 v76
124-
;; @003b v37 = bor v74, v36
117+
;; v85 = iadd.i64 v0, v64 ; v64 = 80
118+
;; @003b store.i32 notrap aligned v2, v85
119+
;; v86 = iconst.i32 1
120+
;; v87 = band.i32 v5, v86 ; v86 = 1
121+
;; v88 = iconst.i32 0
122+
;; v89 = icmp.i32 eq v5, v88 ; v88 = 0
123+
;; @003b v36 = uextend.i32 v89
124+
;; @003b v37 = bor v87, v36
125125
;; @003b brif v37, block7, block4
126126
;;
127127
;; block4:
128128
;; @003b v42 = uextend.i64 v5
129-
;; v77 = iconst.i64 8
130-
;; @003b v44 = uadd_overflow_trap v42, v77, user1 ; v77 = 8
131-
;; @003b v46 = uadd_overflow_trap v44, v77, user1 ; v77 = 8
132-
;; v78 = load.i64 notrap aligned readonly can_move v0+48
133-
;; @003b v47 = icmp ule v46, v78
129+
;; v90 = iconst.i64 8
130+
;; @003b v44 = uadd_overflow_trap v42, v90, user1 ; v90 = 8
131+
;; @003b v46 = uadd_overflow_trap v44, v90, user1 ; v90 = 8
132+
;; v91 = load.i64 notrap aligned readonly can_move v0+48
133+
;; @003b v47 = icmp ule v46, v91
134134
;; @003b trapz v47, user1
135-
;; v79 = load.i64 notrap aligned readonly can_move v0+40
136-
;; @003b v48 = iadd v79, v44
135+
;; v92 = load.i64 notrap aligned readonly can_move v0+40
136+
;; @003b v48 = iadd v92, v44
137137
;; @003b v49 = load.i64 notrap aligned v48
138-
;; v70 = iconst.i64 -1
139-
;; @003b v50 = iadd v49, v70 ; v70 = -1
140-
;; v71 = iconst.i64 0
141-
;; @003b v51 = icmp eq v50, v71 ; v71 = 0
142-
;; @003b brif v51, block5, block6
138+
;; v93 = iconst.i64 1
139+
;; v83 = icmp eq v49, v93 ; v93 = 1
140+
;; @003b brif v83, block5, block6
143141
;;
144142
;; block5 cold:
145143
;; @003b call fn0(v0, v5)
146144
;; @003b jump block7
147145
;;
148146
;; block6:
149-
;; v80 = iadd.i64 v49, v70 ; v70 = -1
150-
;; @003b store notrap aligned v80, v48
147+
;; v70 = iconst.i64 -1
148+
;; @003b v50 = iadd.i64 v49, v70 ; v70 = -1
149+
;; @003b store notrap aligned v50, v48
151150
;; @003b jump block7
152151
;;
153152
;; block7:

‎tests/disas/gc/drc/struct-set.wat‎

Lines changed: 17 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -110,43 +110,42 @@
110110
;; @004a trapz v30, user1
111111
;; @004a v31 = iadd.i64 v6, v27
112112
;; @004a v32 = load.i64 notrap aligned v31
113-
;; v77 = iconst.i64 1
114-
;; @004a v33 = iadd v32, v77 ; v77 = 1
113+
;; v84 = iconst.i64 1
114+
;; @004a v33 = iadd v32, v84 ; v84 = 1
115115
;; @004a store notrap aligned v33, v31
116116
;; @004a jump block3
117117
;;
118118
;; block3:
119119
;; @004a store.i32 notrap aligned little v3, v15
120-
;; v83 = iconst.i32 1
121-
;; v84 = band.i32 v16, v83 ; v83 = 1
122-
;; v85 = iconst.i32 0
123-
;; v86 = icmp.i32 eq v16, v85 ; v85 = 0
124-
;; @004a v47 = uextend.i32 v86
125-
;; @004a v48 = bor v84, v47
120+
;; v96 = iconst.i32 1
121+
;; v97 = band.i32 v16, v96 ; v96 = 1
122+
;; v98 = iconst.i32 0
123+
;; v99 = icmp.i32 eq v16, v98 ; v98 = 0
124+
;; @004a v47 = uextend.i32 v99
125+
;; @004a v48 = bor v97, v47
126126
;; @004a brif v48, block7, block4
127127
;;
128128
;; block4:
129129
;; @004a v53 = uextend.i64 v16
130-
;; v87 = iconst.i64 8
131-
;; @004a v55 = uadd_overflow_trap v53, v87, user1 ; v87 = 8
132-
;; @004a v57 = uadd_overflow_trap v55, v87, user1 ; v87 = 8
130+
;; v100 = iconst.i64 8
131+
;; @004a v55 = uadd_overflow_trap v53, v100, user1 ; v100 = 8
132+
;; @004a v57 = uadd_overflow_trap v55, v100, user1 ; v100 = 8
133133
;; @004a v58 = icmp ule v57, v8
134134
;; @004a trapz v58, user1
135135
;; @004a v59 = iadd.i64 v6, v55
136136
;; @004a v60 = load.i64 notrap aligned v59
137-
;; v80 = iconst.i64 -1
138-
;; @004a v61 = iadd v60, v80 ; v80 = -1
139-
;; v81 = iconst.i64 0
140-
;; @004a v62 = icmp eq v61, v81 ; v81 = 0
141-
;; @004a brif v62, block5, block6
137+
;; v101 = iconst.i64 1
138+
;; v94 = icmp eq v60, v101 ; v101 = 1
139+
;; @004a brif v94, block5, block6
142140
;;
143141
;; block5 cold:
144142
;; @004a call fn0(v0, v16)
145143
;; @004a jump block7
146144
;;
147145
;; block6:
148-
;; v88 = iadd.i64 v60, v80 ; v80 = -1
149-
;; @004a store notrap aligned v88, v59
146+
;; v80 = iconst.i64 -1
147+
;; @004a v61 = iadd.i64 v60, v80 ; v80 = -1
148+
;; @004a store notrap aligned v61, v59
150149
;; @004a jump block7
151150
;;
152151
;; block7:

‎tests/disas/pulley/memory-inbounds.wat‎

Lines changed: 8 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -64,15 +64,14 @@
6464
;;
6565
;; wasm[0]::function[6]::offset_just_bad_v2:
6666
;; push_frame
67-
;; xload64le_o32 x10, x0, 88
68-
;; xsub64_u32 x10, x10, 65536
69-
;; xzero x11
70-
;; xload64le_o32 x12, x0, 80
71-
;; xadd64_u32 x12, x12, 65533
72-
;; xzero x8
73-
;; xeq64 x10, x10, x8
74-
;; xselect64 x12, x10, x11, x12
75-
;; xload32le_z x0, x12, 0
67+
;; xload64le_o32 x9, x0, 88
68+
;; xzero x10
69+
;; xload64le_o32 x11, x0, 80
70+
;; xadd64_u32 x11, x11, 65533
71+
;; xconst32 x7, 65536
72+
;; xeq64 x9, x9, x7
73+
;; xselect64 x11, x9, x10, x11
74+
;; xload32le_z x0, x11, 0
7675
;; pop_frame
7776
;; ret
7877
;;

0 commit comments

Comments
 (0)