11// RUN: mlir-opt -allow-unregistered-dialect %s -split-input-file -simplify-affine-structures | FileCheck %s
22
3- // CHECK-DAG: [[SET_EMPTY_2D:#set[0-9]+]] = affine_set<(d0, d1) : (1 == 0)>
4- // CHECK-DAG: #set1 = affine_set<(d0, d1) : (d0 - 100 == 0, d1 - 10 == 0, -d0 + 100 >= 0, d1 >= 0)>
5- // CHECK-DAG: #set2 = affine_set<(d0, d1)[s0, s1] : (1 == 0)>
6- // CHECK-DAG: #set3 = affine_set<(d0, d1)[s0, s1] : (d0 * 7 + d1 * 5 + s0 * 11 + s1 == 0, d0 * 5 - d1 * 11 + s0 * 7 + s1 == 0, d0 * 11 + d1 * 7 - s0 * 5 + s1 == 0, d0 * 7 + d1 * 5 + s0 * 11 + s1 == 0)>
7- // CHECK-DAG: [[SET_EMPTY_1D:#set[0-9]+]] = affine_set<(d0) : (1 == 0)>
8- // CHECK-DAG: [[SET_EMPTY_1D_2S:#set[0-9]+]] = affine_set<(d0)[s0, s1] : (1 == 0)>
9- // CHECK-DAG: [[SET_EMPTY_3D:#set[0-9]+]] = affine_set<(d0, d1, d2) : (1 == 0)>
10-
11- // Set for test case: test_gaussian_elimination_non_empty_set2
12- // #set2 = affine_set<(d0, d1) : (d0 - 100 == 0, d1 - 10 == 0, -d0 + 100 >= 0, d1 >= 0, d1 + 101 >= 0)>
13- #set2 = affine_set <(d0 , d1 ) : (d0 - 100 == 0 , d1 - 10 == 0 , -d0 + 100 >= 0 , d1 >= 0 , d1 + 101 >= 0 )>
14-
15- // Set for test case: test_gaussian_elimination_empty_set3
16- // #set3 = affine_set<(d0, d1)[s0, s1] : (1 == 0)>
17- #set3 = affine_set <(d0 , d1 )[s0 , s1 ] : (d0 - s0 == 0 , d0 + s0 == 0 , s0 - 1 == 0 )>
18-
19- // Set for test case: test_gaussian_elimination_non_empty_set4
20- #set4 = affine_set <(d0 , d1 )[s0 , s1 ] : (d0 * 7 + d1 * 5 + s0 * 11 + s1 == 0 ,
21- d0 * 5 - d1 * 11 + s0 * 7 + s1 == 0 ,
22- d0 * 11 + d1 * 7 - s0 * 5 + s1 == 0 ,
23- d0 * 7 + d1 * 5 + s0 * 11 + s1 == 0 )>
24-
25- // Add invalid constraints to previous non-empty set to make it empty.
26- // Set for test case: test_gaussian_elimination_empty_set5
27- #set5 = affine_set <(d0 , d1 )[s0 , s1 ] : (d0 * 7 + d1 * 5 + s0 * 11 + s1 == 0 ,
28- d0 * 5 - d1 * 11 + s0 * 7 + s1 == 0 ,
29- d0 * 11 + d1 * 7 - s0 * 5 + s1 == 0 ,
30- d0 * 7 + d1 * 5 + s0 * 11 + s1 == 0 ,
31- d0 - 1 == 0 , d0 + 2 == 0 )>
32-
33- // This is an artificially created system to exercise the worst case behavior of
34- // FM elimination - as a safeguard against improperly constructed constraint
35- // systems or fuzz input.
36- #set_fuzz_virus = affine_set <(d0 , d1 , d2 , d3 , d4 , d5 ) : (
37- 1089234 *d0 + 203472 *d1 + 82342 >= 0 ,
38- -55 *d0 + 24 *d1 + 238 *d2 - 234 *d3 - 9743 >= 0 ,
39- -5445 *d0 - 284 *d1 + 23 *d2 + 34 *d3 - 5943 >= 0 ,
40- -5445 *d0 + 284 *d1 + 238 *d2 - 34 *d3 >= 0 ,
41- 445 *d0 + 284 *d1 + 238 *d2 + 39 *d3 >= 0 ,
42- -545 *d0 + 214 *d1 + 218 *d2 - 94 *d3 >= 0 ,
43- 44 *d0 - 184 *d1 - 231 *d2 + 14 *d3 >= 0 ,
44- -45 *d0 + 284 *d1 + 138 *d2 - 39 *d3 >= 0 ,
45- 154 *d0 - 84 *d1 + 238 *d2 - 34 *d3 >= 0 ,
46- 54 *d0 - 284 *d1 - 223 *d2 + 384 *d3 >= 0 ,
47- -55 *d0 + 284 *d1 + 23 *d2 + 34 *d3 >= 0 ,
48- 54 *d0 - 84 *d1 + 28 *d2 - 34 *d3 >= 0 ,
49- 54 *d0 - 24 *d1 - 23 *d2 + 34 *d3 >= 0 ,
50- -55 *d0 + 24 *d1 + 23 *d2 + 4 *d3 >= 0 ,
51- 15 *d0 - 84 *d1 + 238 *d2 - 3 *d3 >= 0 ,
52- 5 *d0 - 24 *d1 - 223 *d2 + 84 *d3 >= 0 ,
53- -5 *d0 + 284 *d1 + 23 *d2 - 4 *d3 >= 0 ,
54- 14 *d0 + 4 *d2 + 7234 >= 0 ,
55- -174 *d0 - 534 *d2 + 9834 >= 0 ,
56- 194 *d0 - 954 *d2 + 9234 >= 0 ,
57- 47 *d0 - 534 *d2 + 9734 >= 0 ,
58- -194 *d0 - 934 *d2 + 984 >= 0 ,
59- -947 *d0 - 953 *d2 + 234 >= 0 ,
60- 184 *d0 - 884 *d2 + 884 >= 0 ,
61- -174 *d0 + 834 *d2 + 234 >= 0 ,
62- 844 *d0 + 634 *d2 + 9874 >= 0 ,
63- -797 *d2 - 79 *d3 + 257 >= 0 ,
64- 2039 *d0 + 793 *d2 - 99 *d3 - 24 *d4 + 234 *d5 >= 0 ,
65- 78 *d2 - 788 *d5 + 257 >= 0 ,
66- d3 - (d5 + 97 *d0 ) floordiv 423 >= 0 ,
67- 234 * (d0 + d3 mod 5 floordiv 2342 ) mod 2309
68- + (d0 + 2038 *d3 ) floordiv 208 >= 0 ,
69- 239 * (d0 + 2300 * d3 ) floordiv 2342
70- mod 2309 mod 239423 == 0 ,
71- d0 + d3 mod 2642 + (d3 + 2 *d0 ) mod 1247
72- mod 2038 mod 2390 mod 2039 floordiv 55 >= 0
73- )>
3+ // CHECK-DAG: #[[SET_EMPTY_2D:.*]] = affine_set<(d0, d1) : (1 == 0)>
4+ // CHECK-DAG: #[[SET_2D:.*]] = affine_set<(d0, d1) : (d0 - 100 == 0, d1 - 10 == 0, -d0 + 100 >= 0, d1 >= 0)>
5+ // CHECK-DAG: #[[SET_EMPTY_2D_2S:.*]] = affine_set<(d0, d1)[s0, s1] : (1 == 0)>
6+ // CHECK-DAG: #[[SET_2D_2S:.*]] = affine_set<(d0, d1)[s0, s1] : (d0 * 7 + d1 * 5 + s0 * 11 + s1 == 0, d0 * 5 - d1 * 11 + s0 * 7 + s1 == 0, d0 * 11 + d1 * 7 - s0 * 5 + s1 == 0, d0 * 7 + d1 * 5 + s0 * 11 + s1 == 0)>
7+ // CHECK-DAG: #[[SET_EMPTY_1D:.*]] = affine_set<(d0) : (1 == 0)>
8+ // CHECK-DAG: #[[SET_EMPTY_1D_2S:.*]] = affine_set<(d0)[s0, s1] : (1 == 0)>
9+ // CHECK-DAG: #[[SET_EMPTY_3D:.*]] = affine_set<(d0, d1, d2) : (1 == 0)>
7410
7511// CHECK-LABEL: func @test_gaussian_elimination_empty_set0() {
7612func @test_gaussian_elimination_empty_set0 () {
@@ -100,8 +36,8 @@ func @test_gaussian_elimination_empty_set1() {
10036func @test_gaussian_elimination_non_empty_set2 () {
10137 affine.for %arg0 = 1 to 10 {
10238 affine.for %arg1 = 1 to 100 {
103- // CHECK: #set1 (%arg0, %arg1)
104- affine.if #set2 (%arg0 , %arg1 ) {
39+ // CHECK: #[[SET_2D]] (%arg0, %arg1)
40+ affine.if affine_set <( d0 , d1 ) : ( d0 - 100 == 0 , d1 - 10 == 0 , - d0 + 100 >= 0 , d1 >= 0 , d1 + 101 >= 0 )> (%arg0 , %arg1 ) {
10541 }
10642 }
10743 }
@@ -114,42 +50,98 @@ func @test_gaussian_elimination_empty_set3() {
11450 %c11 = constant 11 : index
11551 affine.for %arg0 = 1 to 10 {
11652 affine.for %arg1 = 1 to 100 {
117- // CHECK: #set2 (%arg0, %arg1)[%c7, %c11]
118- affine.if #set3 (%arg0 , %arg1 )[%c7 , %c11 ] {
53+ // CHECK: #[[SET_EMPTY_2D_2S]] (%arg0, %arg1)[%c7, %c11]
54+ affine.if affine_set <( d0 , d1 )[ s0 , s1 ] : ( d0 - s0 == 0 , d0 + s0 == 0 , s0 - 1 == 0 )> (%arg0 , %arg1 )[%c7 , %c11 ] {
11955 }
12056 }
12157 }
12258 return
12359}
12460
61+ // Set for test case: test_gaussian_elimination_non_empty_set4
62+ #set_2d_non_empty = affine_set <(d0 , d1 )[s0 , s1 ] : (d0 * 7 + d1 * 5 + s0 * 11 + s1 == 0 ,
63+ d0 * 5 - d1 * 11 + s0 * 7 + s1 == 0 ,
64+ d0 * 11 + d1 * 7 - s0 * 5 + s1 == 0 ,
65+ d0 * 7 + d1 * 5 + s0 * 11 + s1 == 0 )>
66+
12567// CHECK-LABEL: func @test_gaussian_elimination_non_empty_set4() {
12668func @test_gaussian_elimination_non_empty_set4 () {
12769 %c7 = constant 7 : index
12870 %c11 = constant 11 : index
12971 affine.for %arg0 = 1 to 10 {
13072 affine.for %arg1 = 1 to 100 {
131- // CHECK: #set3 (%arg0, %arg1)[%c7, %c11]
132- affine.if #set4 (%arg0 , %arg1 )[%c7 , %c11 ] {
73+ // CHECK: #[[SET_2D_2S]] (%arg0, %arg1)[%c7, %c11]
74+ affine.if #set_2d_non_empty (%arg0 , %arg1 )[%c7 , %c11 ] {
13375 }
13476 }
13577 }
13678 return
13779}
13880
81+ // Add invalid constraints to previous non-empty set to make it empty.
82+ // Set for test case: test_gaussian_elimination_empty_set5
83+ #set_2d_empty = affine_set <(d0 , d1 )[s0 , s1 ] : (d0 * 7 + d1 * 5 + s0 * 11 + s1 == 0 ,
84+ d0 * 5 - d1 * 11 + s0 * 7 + s1 == 0 ,
85+ d0 * 11 + d1 * 7 - s0 * 5 + s1 == 0 ,
86+ d0 * 7 + d1 * 5 + s0 * 11 + s1 == 0 ,
87+ d0 - 1 == 0 , d0 + 2 == 0 )>
88+
13989// CHECK-LABEL: func @test_gaussian_elimination_empty_set5() {
14090func @test_gaussian_elimination_empty_set5 () {
14191 %c7 = constant 7 : index
14292 %c11 = constant 11 : index
14393 affine.for %arg0 = 1 to 10 {
14494 affine.for %arg1 = 1 to 100 {
145- // CHECK: #set2 (%arg0, %arg1)[%c7, %c11]
146- affine.if #set5 (%arg0 , %arg1 )[%c7 , %c11 ] {
95+ // CHECK: #[[SET_EMPTY_2D_2S]] (%arg0, %arg1)[%c7, %c11]
96+ affine.if #set_2d_empty (%arg0 , %arg1 )[%c7 , %c11 ] {
14797 }
14898 }
14999 }
150100 return
151101}
152102
103+ // This is an artificially created system to exercise the worst case behavior of
104+ // FM elimination - as a safeguard against improperly constructed constraint
105+ // systems or fuzz input.
106+ #set_fuzz_virus = affine_set <(d0 , d1 , d2 , d3 , d4 , d5 ) : (
107+ 1089234 *d0 + 203472 *d1 + 82342 >= 0 ,
108+ -55 *d0 + 24 *d1 + 238 *d2 - 234 *d3 - 9743 >= 0 ,
109+ -5445 *d0 - 284 *d1 + 23 *d2 + 34 *d3 - 5943 >= 0 ,
110+ -5445 *d0 + 284 *d1 + 238 *d2 - 34 *d3 >= 0 ,
111+ 445 *d0 + 284 *d1 + 238 *d2 + 39 *d3 >= 0 ,
112+ -545 *d0 + 214 *d1 + 218 *d2 - 94 *d3 >= 0 ,
113+ 44 *d0 - 184 *d1 - 231 *d2 + 14 *d3 >= 0 ,
114+ -45 *d0 + 284 *d1 + 138 *d2 - 39 *d3 >= 0 ,
115+ 154 *d0 - 84 *d1 + 238 *d2 - 34 *d3 >= 0 ,
116+ 54 *d0 - 284 *d1 - 223 *d2 + 384 *d3 >= 0 ,
117+ -55 *d0 + 284 *d1 + 23 *d2 + 34 *d3 >= 0 ,
118+ 54 *d0 - 84 *d1 + 28 *d2 - 34 *d3 >= 0 ,
119+ 54 *d0 - 24 *d1 - 23 *d2 + 34 *d3 >= 0 ,
120+ -55 *d0 + 24 *d1 + 23 *d2 + 4 *d3 >= 0 ,
121+ 15 *d0 - 84 *d1 + 238 *d2 - 3 *d3 >= 0 ,
122+ 5 *d0 - 24 *d1 - 223 *d2 + 84 *d3 >= 0 ,
123+ -5 *d0 + 284 *d1 + 23 *d2 - 4 *d3 >= 0 ,
124+ 14 *d0 + 4 *d2 + 7234 >= 0 ,
125+ -174 *d0 - 534 *d2 + 9834 >= 0 ,
126+ 194 *d0 - 954 *d2 + 9234 >= 0 ,
127+ 47 *d0 - 534 *d2 + 9734 >= 0 ,
128+ -194 *d0 - 934 *d2 + 984 >= 0 ,
129+ -947 *d0 - 953 *d2 + 234 >= 0 ,
130+ 184 *d0 - 884 *d2 + 884 >= 0 ,
131+ -174 *d0 + 834 *d2 + 234 >= 0 ,
132+ 844 *d0 + 634 *d2 + 9874 >= 0 ,
133+ -797 *d2 - 79 *d3 + 257 >= 0 ,
134+ 2039 *d0 + 793 *d2 - 99 *d3 - 24 *d4 + 234 *d5 >= 0 ,
135+ 78 *d2 - 788 *d5 + 257 >= 0 ,
136+ d3 - (d5 + 97 *d0 ) floordiv 423 >= 0 ,
137+ 234 * (d0 + d3 mod 5 floordiv 2342 ) mod 2309
138+ + (d0 + 2038 *d3 ) floordiv 208 >= 0 ,
139+ 239 * (d0 + 2300 * d3 ) floordiv 2342
140+ mod 2309 mod 239423 == 0 ,
141+ d0 + d3 mod 2642 + (d3 + 2 *d0 ) mod 1247
142+ mod 2038 mod 2390 mod 2039 floordiv 55 >= 0
143+ )>
144+
153145// CHECK-LABEL: func @test_fuzz_explosion
154146func @test_fuzz_explosion (%arg0 : index , %arg1 : index , %arg2 : index , %arg3 : index ) {
155147 affine.for %arg4 = 1 to 10 {
@@ -161,38 +153,37 @@ func @test_fuzz_explosion(%arg0 : index, %arg1 : index, %arg2 : index, %arg3 : i
161153 return
162154}
163155
164-
165156// CHECK-LABEL: func @test_empty_set(%arg0: index) {
166157func @test_empty_set (%N : index ) {
167158 affine.for %i = 0 to 10 {
168159 affine.for %j = 0 to 10 {
169- // CHECK: affine.if [[SET_EMPTY_2D]](%arg1, %arg2)
160+ // CHECK: affine.if # [[SET_EMPTY_2D]](%arg1, %arg2)
170161 affine.if affine_set <(d0 , d1 ) : (d0 - d1 >= 0 , d1 - d0 - 1 >= 0 )>(%i , %j ) {
171162 " foo" () : () -> ()
172163 }
173- // CHECK: affine.if [[SET_EMPTY_1D]](%arg1)
164+ // CHECK: affine.if # [[SET_EMPTY_1D]](%arg1)
174165 affine.if affine_set <(d0 ) : (d0 >= 0 , -d0 - 1 >= 0 )>(%i ) {
175166 " bar" () : () -> ()
176167 }
177- // CHECK: affine.if [[SET_EMPTY_1D]](%arg1)
168+ // CHECK: affine.if # [[SET_EMPTY_1D]](%arg1)
178169 affine.if affine_set <(d0 ) : (d0 >= 0 , -d0 - 1 >= 0 )>(%i ) {
179170 " foo" () : () -> ()
180171 }
181- // CHECK: affine.if [[SET_EMPTY_1D_2S]](%arg1)[%arg0, %arg0]
172+ // CHECK: affine.if # [[SET_EMPTY_1D_2S]](%arg1)[%arg0, %arg0]
182173 affine.if affine_set <(d0 )[s0 , s1 ] : (d0 >= 0 , -d0 + s0 - 1 >= 0 , -s0 >= 0 )>(%i )[%N , %N ] {
183174 " bar" () : () -> ()
184175 }
185- // CHECK: affine.if [[SET_EMPTY_3D]](%arg1, %arg2, %arg0)
176+ // CHECK: affine.if # [[SET_EMPTY_3D]](%arg1, %arg2, %arg0)
186177 // The set below implies d0 = d1; so d1 >= d0, but d0 >= d1 + 1.
187178 affine.if affine_set <(d0 , d1 , d2 ) : (d0 - d1 == 0 , d2 - d0 >= 0 , d0 - d1 - 1 >= 0 )>(%i , %j , %N ) {
188179 " foo" () : () -> ()
189180 }
190- // CHECK: affine.if [[SET_EMPTY_2D]](%arg1, %arg2)
181+ // CHECK: affine.if # [[SET_EMPTY_2D]](%arg1, %arg2)
191182 // The set below has rational solutions but no integer solutions; GCD test catches it.
192183 affine.if affine_set <(d0 , d1 ) : (d0 *2 -d1 *2 - 1 == 0 , d0 >= 0 , -d0 + 100 >= 0 , d1 >= 0 , -d1 + 100 >= 0 )>(%i , %j ) {
193184 " foo" () : () -> ()
194185 }
195- // CHECK: affine.if [[SET_EMPTY_2D]](%arg1, %arg2)
186+ // CHECK: affine.if # [[SET_EMPTY_2D]](%arg1, %arg2)
196187 affine.if affine_set <(d0 , d1 ) : (d1 == 0 , d0 - 1 >= 0 , - d0 - 1 >= 0 )>(%i , %j ) {
197188 " foo" () : () -> ()
198189 }
@@ -202,33 +193,33 @@ func @test_empty_set(%N : index) {
202193 affine.for %k = 0 to 10 {
203194 affine.for %l = 0 to 10 {
204195 // Empty because no multiple of 8 lies between 4 and 7.
205- // CHECK: affine.if [[SET_EMPTY_1D]](%arg1)
196+ // CHECK: affine.if # [[SET_EMPTY_1D]](%arg1)
206197 affine.if affine_set <(d0 ) : (8 *d0 - 4 >= 0 , -8 *d0 + 7 >= 0 )>(%k ) {
207198 " foo" () : () -> ()
208199 }
209200 // Same as above but with equalities and inequalities.
210- // CHECK: affine.if [[SET_EMPTY_2D]](%arg1, %arg2)
201+ // CHECK: affine.if # [[SET_EMPTY_2D]](%arg1, %arg2)
211202 affine.if affine_set <(d0 , d1 ) : (d0 - 4 *d1 == 0 , 4 *d1 - 5 >= 0 , -4 *d1 + 7 >= 0 )>(%k , %l ) {
212203 " foo" () : () -> ()
213204 }
214205 // Same as above but with a combination of multiple identifiers. 4*d0 +
215206 // 8*d1 here is a multiple of 4, and so can't lie between 9 and 11. GCD
216207 // tightening will tighten constraints to 4*d0 + 8*d1 >= 12 and 4*d0 +
217208 // 8*d1 <= 8; hence infeasible.
218- // CHECK: affine.if [[SET_EMPTY_2D]](%arg1, %arg2)
209+ // CHECK: affine.if # [[SET_EMPTY_2D]](%arg1, %arg2)
219210 affine.if affine_set <(d0 , d1 ) : (4 *d0 + 8 *d1 - 9 >= 0 , -4 *d0 - 8 *d1 + 11 >= 0 )>(%k , %l ) {
220211 " foo" () : () -> ()
221212 }
222213 // Same as above but with equalities added into the mix.
223- // CHECK: affine.if [[SET_EMPTY_3D]](%arg1, %arg1, %arg2)
214+ // CHECK: affine.if # [[SET_EMPTY_3D]](%arg1, %arg1, %arg2)
224215 affine.if affine_set <(d0 , d1 , d2 ) : (d0 - 4 *d2 == 0 , d0 + 8 *d1 - 9 >= 0 , -d0 - 8 *d1 + 11 >= 0 )>(%k , %k , %l ) {
225216 " foo" () : () -> ()
226217 }
227218 }
228219 }
229220
230221 affine.for %m = 0 to 10 {
231- // CHECK: affine.if [[SET_EMPTY_1D]](%arg{{[0-9]+}})
222+ // CHECK: affine.if # [[SET_EMPTY_1D]](%arg{{[0-9]+}})
232223 affine.if affine_set <(d0 ) : (d0 mod 2 - 3 == 0 )> (%m ) {
233224 " foo" () : () -> ()
234225 }
@@ -239,19 +230,19 @@ func @test_empty_set(%N : index) {
239230
240231// -----
241232
242- // CHECK-DAG: #[[SET1 :.*]] = affine_set<(d0, d1) : (d0 >= 0, -d0 + 50 >= 0)
243- // CHECK-DAG: #[[SET2 :.*]] = affine_set<(d0, d1) : (1 == 0)
244- // CHECK-DAG: #[[SET3 :.*]] = affine_set<(d0, d1) : (0 == 0)
233+ // CHECK-DAG: #[[SET_2D :.*]] = affine_set<(d0, d1) : (d0 >= 0, -d0 + 50 >= 0)
234+ // CHECK-DAG: #[[SET_EMPTY :.*]] = affine_set<(d0, d1) : (1 == 0)
235+ // CHECK-DAG: #[[SET_UNIV :.*]] = affine_set<(d0, d1) : (0 == 0)
245236
246237// CHECK-LABEL: func @simplify_set
247238func @simplify_set (%a : index , %b : index ) {
248- // CHECK: affine.if #[[SET1 ]]
239+ // CHECK: affine.if #[[SET_2D ]]
249240 affine.if affine_set <(d0 , d1 ) : (d0 - d1 + d1 + d0 >= 0 , 2 >= 0 , d0 >= 0 , -d0 + 50 >= 0 , -d0 + 100 >= 0 )>(%a , %b ) {
250241 }
251- // CHECK: affine.if #[[SET2 ]]
242+ // CHECK: affine.if #[[SET_EMPTY ]]
252243 affine.if affine_set <(d0 , d1 ) : (d0 mod 2 - 1 == 0 , d0 - 2 * (d0 floordiv 2 ) == 0 )>(%a , %b ) {
253244 }
254- // CHECK: affine.if #[[SET3 ]]
245+ // CHECK: affine.if #[[SET_UNIV ]]
255246 affine.if affine_set <(d0 , d1 ) : (1 >= 0 , 3 >= 0 )>(%a , %b ) {
256247 }
257248 return
0 commit comments