Skip to content

Commit 6f4d26e

Browse files
bongjunjbongjunj
authored
[Cranelift] a < b && a > b = false (#11997)
* [Cranelift] `a < b && a > b = false` * add comm
1 parent ec9b62a commit 6f4d26e

File tree

3 files changed

+202
-1
lines changed

3 files changed

+202
-1
lines changed

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

Lines changed: 38 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -302,8 +302,45 @@
302302
(rule (simplify (ult cty (bnot ty x) (bnot ty y))) (ugt cty x y))
303303
(rule (simplify (slt cty (bnot ty x) (bnot ty y))) (sgt cty x y))
304304

305-
306305
;; a < b ^^ a > b => (a ≠ b)
307306
(rule (simplify (bxor ty (slt cty x y) (sgt cty x y))) (ne cty x y))
308307
(rule (simplify (bxor ty (ult cty x y) (ugt cty x y))) (ne cty x y))
309308

309+
;; a < b && a > b = false
310+
(rule (simplify (band ty (sgt ty x y) (slt ty x y))) (iconst_u ty 0))
311+
(rule (simplify (band ty (slt ty x y) (sgt ty x y))) (iconst_u ty 0))
312+
(rule (simplify (band ty (ugt ty x y) (ult ty x y))) (iconst_u ty 0))
313+
(rule (simplify (band ty (ult ty x y) (ugt ty x y))) (iconst_u ty 0))
314+
(rule
315+
(simplify (band ty (sgt ty x (iconst_s _ y)) (ult ty x (iconst_s _ y))))
316+
(if-let true (i64_gt_eq y 0))
317+
(iconst_u ty 0))
318+
(rule
319+
(simplify (band ty (sgt ty (iconst_s _ x) y) (ult ty (iconst_s _ x) y)))
320+
(if-let true (i64_lt x 0))
321+
(iconst_u ty 0))
322+
(rule
323+
(simplify (band ty (slt ty x (iconst_s _ y)) (ugt ty x (iconst_s _ y))))
324+
(if-let true (i64_lt y 0))
325+
(iconst_u ty 0))
326+
(rule
327+
(simplify (band ty (slt ty (iconst_s _ x) y) (ugt ty (iconst_s _ x) y)))
328+
(if-let true (i64_gt_eq x 0))
329+
(iconst_u ty 0))
330+
(rule
331+
(simplify (band ty (ugt ty x (iconst_s _ y)) (slt ty x (iconst_s _ y))))
332+
(if-let true (i64_lt y 0))
333+
(iconst_u ty 0))
334+
(rule
335+
(simplify (band ty (ugt ty (iconst_s _ x) y) (slt ty (iconst_s _ x) y)))
336+
(if-let true (i64_gt_eq x 0))
337+
(iconst_u ty 0))
338+
(rule
339+
(simplify (band ty (ult ty x (iconst_s _ y)) (sgt ty x (iconst_s _ y))))
340+
(if-let true (i64_gt_eq y 0))
341+
(iconst_u ty 0))
342+
(rule
343+
(simplify (band ty (ult ty (iconst_s _ x) y) (sgt ty (iconst_s _ x) y)))
344+
(if-let true (i64_lt x 0))
345+
(iconst_u ty 0))
346+

‎cranelift/filetests/filetests/egraph/icmp.clif‎

Lines changed: 94 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -311,3 +311,97 @@ block0(v0: i32, v1: i32):
311311
; return v5
312312
; }
313313

314+
;; Rule 1: (x <_s y) & (x >_s y) => false
315+
function %test_slt_sgt(i32, i32) -> i8 fast {
316+
block0(v0: i32, v1: i32):
317+
v2 = icmp slt v0, v1
318+
v3 = icmp sgt v0, v1
319+
v4 = band v2, v3
320+
return v4
321+
}
322+
323+
; function %test_slt_sgt(i32, i32) -> i8 fast {
324+
; block0(v0: i32, v1: i32):
325+
; v5 = iconst.i8 0
326+
; return v5 ; v5 = 0
327+
; }
328+
329+
;; Rule 2: (x <_u y) & (x >_u y) => false
330+
function %test_ult_ugt(i32, i32) -> i8 fast {
331+
block0(v0: i32, v1: i32):
332+
v2 = icmp ult v0, v1
333+
v3 = icmp ugt v0, v1
334+
v4 = band v2, v3
335+
return v4
336+
}
337+
338+
; function %test_ult_ugt(i32, i32) -> i8 fast {
339+
; block0(v0: i32, v1: i32):
340+
; v5 = iconst.i8 0
341+
; return v5 ; v5 = 0
342+
; }
343+
344+
;; Rule 3: (x <_s y_const) & (x >_u y_const) => false, if y_const < 0
345+
function %test_slt_ugt_neg_const_y(i32) -> i8 fast {
346+
block0(v0: i32):
347+
v1 = iconst.i32 -10
348+
v2 = icmp slt v0, v1
349+
v3 = icmp ugt v0, v1
350+
v4 = band v2, v3
351+
return v4
352+
}
353+
354+
; function %test_slt_ugt_neg_const_y(i32) -> i8 fast {
355+
; block0(v0: i32):
356+
; v5 = iconst.i8 0
357+
; return v5 ; v5 = 0
358+
; }
359+
360+
;; Rule 4: (x_const <_s y) & (x_const >_u y) => false, if x_const >= 0
361+
function %test_slt_ugt_pos_const_x(i32) -> i8 fast {
362+
block0(v0: i32):
363+
v1 = iconst.i32 10
364+
v2 = icmp slt v1, v0
365+
v3 = icmp ugt v1, v0
366+
v4 = band v2, v3
367+
return v4
368+
}
369+
370+
; function %test_slt_ugt_pos_const_x(i32) -> i8 fast {
371+
; block0(v0: i32):
372+
; v9 = iconst.i8 0
373+
; return v9 ; v9 = 0
374+
; }
375+
376+
;; Rule 5: (x <_u y_const) & (x >_s y_const) => false, if y_const >= 0
377+
function %test_ult_sgt_pos_const_y(i32) -> i8 fast {
378+
block0(v0: i32):
379+
v1 = iconst.i32 10
380+
v2 = icmp ult v0, v1
381+
v3 = icmp sgt v0, v1
382+
v4 = band v2, v3
383+
return v4
384+
}
385+
386+
; function %test_ult_sgt_pos_const_y(i32) -> i8 fast {
387+
; block0(v0: i32):
388+
; v5 = iconst.i8 0
389+
; return v5 ; v5 = 0
390+
; }
391+
392+
;; Rule 6: (x_const <_u y) & (x_const >_s y) => false, if x_const < 0
393+
function %test_ult_sgt_neg_const_x(i32) -> i8 fast {
394+
block0(v0: i32):
395+
v1 = iconst.i32 -10
396+
v2 = icmp ult v1, v0
397+
v3 = icmp sgt v1, v0
398+
v4 = band v2, v3
399+
return v4
400+
}
401+
402+
; function %test_ult_sgt_neg_const_x(i32) -> i8 fast {
403+
; block0(v0: i32):
404+
; v9 = iconst.i8 0
405+
; return v9 ; v9 = 0
406+
; }
407+

‎cranelift/filetests/filetests/runtests/icmp.clif‎

Lines changed: 70 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -89,3 +89,73 @@ block0(v0: i32, v1: i32):
8989
; run: %test_bxor_ult_ugt(1, 1) == 0
9090
; run: %test_bxor_ult_ugt(1, 3) == 1
9191

92+
;; Rule 1: (x <_s y) & (x >_s y) => false
93+
function %test_slt_sgt(i32, i32) -> i8 fast {
94+
block0(v0: i32, v1: i32):
95+
v2 = icmp slt v0, v1 ; (x <_s y)
96+
v3 = icmp sgt v0, v1 ; (x >_s y)
97+
v4 = band v2, v3 ; (x <_s y) & (x >_s y)
98+
return v4
99+
}
100+
101+
; run: %test_slt_sgt(42, 24) == 0
102+
103+
;; Rule 2: (x <_u y) & (x >_u y) => false
104+
function %test_ult_ugt(i32, i32) -> i8 fast {
105+
block0(v0: i32, v1: i32):
106+
v2 = icmp ult v0, v1 ; (x <_u y)
107+
v3 = icmp ugt v0, v1 ; (x >_u y)
108+
v4 = band v2, v3 ; (x <_u y) & (x >_u y)
109+
return v4
110+
}
111+
112+
; run: %test_ult_ugt(42, 24) == 0
113+
114+
;; Rule 3: (x <_s y_const) & (x >_u y_const) => false, if y_const < 0
115+
function %test_slt_ugt_neg_const_y(i32) -> i8 fast {
116+
block0(v0: i32):
117+
v1 = iconst.i32 -10 ; y_const = -10. Triggers (i64_lt y 0)
118+
v2 = icmp slt v0, v1 ; (x <_s -10)
119+
v3 = icmp ugt v0, v1 ; (x >_u -10)
120+
v4 = band v2, v3
121+
return v4
122+
}
123+
124+
; run: %test_slt_ugt_neg_const_y(42) == 0
125+
126+
;; Rule 4: (x_const <_s y) & (x_const >_u y) => false, if x_const >= 0
127+
function %test_slt_ugt_pos_const_x(i32) -> i8 fast {
128+
block0(v0: i32):
129+
v1 = iconst.i32 10
130+
v2 = icmp slt v1, v0
131+
v3 = icmp ugt v1, v0
132+
v4 = band v2, v3
133+
return v4
134+
}
135+
136+
; run: %test_slt_ugt_pos_const_x(42) == 0
137+
138+
;; Rule 5: (x <_u y_const) & (x >_s y_const) => false, if y_const >= 0
139+
function %test_ult_sgt_pos_const_y(i32) -> i8 fast {
140+
block0(v0: i32):
141+
v1 = iconst.i32 10
142+
v2 = icmp ult v0, v1
143+
v3 = icmp sgt v0, v1
144+
v4 = band v2, v3
145+
return v4
146+
}
147+
148+
; run: %test_ult_sgt_pos_const_y(42) == 0
149+
150+
;; Rule 6: (x_const <_u y) & (x_const >_s y) => false, if x_const < 0
151+
function %test_ult_sgt_neg_const_x(i32) -> i8 fast {
152+
block0(v0: i32):
153+
v1 = iconst.i32 -10
154+
v2 = icmp ult v1, v0
155+
v3 = icmp sgt v1, v0
156+
v4 = band v2, v3
157+
return v4
158+
}
159+
160+
; run: %test_ult_sgt_neg_const_x(42) == 0
161+

0 commit comments

Comments
 (0)