1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
;; GENERATED BY `isaspec`. DO NOT EDIT!!!
(attr MInst.VecLanes (tag isaspec_generated))
(spec
(MInst.VecLanes op rd rn size)
(provide
(match
size
((Size32x4)
(match
op
((Uminv)
(with
(t1 t10 t11 t12 t2 t3 t4 t5 t6 t7 t8 t9)
(and
(= t1 (bvsle (zero_ext 64 (extract 31 0 rn)) (zero_ext 64 (extract 63 32 rn))))
(if t1 (= t2 (extract 31 0 rn)) (= t3 (extract 63 32 rn)))
(= t4 (if t1 t2 t3))
(= t5 (bvsle (zero_ext 64 t4) (zero_ext 64 (extract 95 64 rn))))
(if t5 (= t6 t4) (= t7 (extract 95 64 rn)))
(= t8 (if t5 t6 t7))
(= t9 (bvsle (zero_ext 64 t8) (zero_ext 64 (extract 127 96 rn))))
(if t9 (= t10 t8) (= t11 (extract 127 96 rn)))
(= t12 (if t9 t10 t11))
(= rd (zero_ext 128 t12))
)
)
)
((Addv)
(=
rd
(zero_ext 128 (bvadd (bvadd (extract 31 0 rn) (extract 63 32 rn)) (bvadd (extract 95 64 rn) (extract 127 96 rn))))
)
)
)
)
((Size16x8)
(match
op
((Uminv)
(with
(t1 t10 t11 t12 t13 t14 t15 t16 t17 t18 t19 t2 t20 t21 t22 t23 t24 t25 t26 t27 t28 t3 t4 t5 t6 t7 t8 t9)
(and
(= t1 (bvsle (zero_ext 32 (extract 15 0 rn)) (zero_ext 32 (extract 31 16 rn))))
(if t1 (= t2 (extract 15 0 rn)) (= t3 (extract 31 16 rn)))
(= t4 (if t1 t2 t3))
(= t5 (bvsle (zero_ext 32 t4) (zero_ext 32 (extract 47 32 rn))))
(if t5 (= t6 t4) (= t7 (extract 47 32 rn)))
(= t8 (if t5 t6 t7))
(= t9 (bvsle (zero_ext 32 t8) (zero_ext 32 (extract 63 48 rn))))
(if t9 (= t10 t8) (= t11 (extract 63 48 rn)))
(= t12 (if t9 t10 t11))
(= t13 (bvsle (zero_ext 32 t12) (zero_ext 32 (extract 79 64 rn))))
(if t13 (= t14 t12) (= t15 (extract 79 64 rn)))
(= t16 (if t13 t14 t15))
(= t17 (bvsle (zero_ext 32 t16) (zero_ext 32 (extract 95 80 rn))))
(if t17 (= t18 t16) (= t19 (extract 95 80 rn)))
(= t20 (if t17 t18 t19))
(= t21 (bvsle (zero_ext 32 t20) (zero_ext 32 (extract 111 96 rn))))
(if t21 (= t22 t20) (= t23 (extract 111 96 rn)))
(= t24 (if t21 t22 t23))
(= t25 (bvsle (zero_ext 32 t24) (zero_ext 32 (extract 127 112 rn))))
(if t25 (= t26 t24) (= t27 (extract 127 112 rn)))
(= t28 (if t25 t26 t27))
(= rd (zero_ext 128 t28))
)
)
)
((Addv)
(=
rd
(zero_ext
128
(bvadd
(bvadd (bvadd (extract 15 0 rn) (extract 31 16 rn)) (bvadd (extract 47 32 rn) (extract 63 48 rn)))
(bvadd (bvadd (extract 79 64 rn) (extract 95 80 rn)) (bvadd (extract 111 96 rn) (extract 127 112 rn)))
)
)
)
)
)
)
((Size16x4)
(match
op
((Uminv)
(with
(t1 t10 t11 t12 t2 t3 t4 t5 t6 t7 t8 t9)
(and
(= t1 (bvsle (zero_ext 32 (extract 15 0 rn)) (zero_ext 32 (extract 31 16 rn))))
(if t1 (= t2 (extract 15 0 rn)) (= t3 (extract 31 16 rn)))
(= t4 (if t1 t2 t3))
(= t5 (bvsle (zero_ext 32 t4) (zero_ext 32 (extract 47 32 rn))))
(if t5 (= t6 t4) (= t7 (extract 47 32 rn)))
(= t8 (if t5 t6 t7))
(= t9 (bvsle (zero_ext 32 t8) (zero_ext 32 (extract 63 48 rn))))
(if t9 (= t10 t8) (= t11 (extract 63 48 rn)))
(= t12 (if t9 t10 t11))
(= rd (zero_ext 128 t12))
)
)
)
((Addv)
(= rd (zero_ext 128 (bvadd (bvadd (extract 15 0 rn) (extract 31 16 rn)) (bvadd (extract 47 32 rn) (extract 63 48 rn)))))
)
)
)
((Size8x16)
(match
op
((Uminv)
(with
(t1
t10
t11
t12
t13
t14
t15
t16
t17
t18
t19
t2
t20
t21
t22
t23
t24
t25
t26
t27
t28
t29
t3
t30
t31
t32
t33
t34
t35
t36
t37
t38
t39
t4
t40
t41
t42
t43
t44
t45
t46
t47
t48
t49
t5
t50
t51
t52
t53
t54
t55
t56
t57
t58
t59
t6
t60
t7
t8
t9
)
(and
(= t1 (bvsle (zero_ext 16 (extract 7 0 rn)) (zero_ext 16 (extract 15 8 rn))))
(if t1 (= t2 (extract 7 0 rn)) (= t3 (extract 15 8 rn)))
(= t4 (if t1 t2 t3))
(= t5 (bvsle (zero_ext 16 t4) (zero_ext 16 (extract 23 16 rn))))
(if t5 (= t6 t4) (= t7 (extract 23 16 rn)))
(= t8 (if t5 t6 t7))
(= t9 (bvsle (zero_ext 16 t8) (zero_ext 16 (extract 31 24 rn))))
(if t9 (= t10 t8) (= t11 (extract 31 24 rn)))
(= t12 (if t9 t10 t11))
(= t13 (bvsle (zero_ext 16 t12) (zero_ext 16 (extract 39 32 rn))))
(if t13 (= t14 t12) (= t15 (extract 39 32 rn)))
(= t16 (if t13 t14 t15))
(= t17 (bvsle (zero_ext 16 t16) (zero_ext 16 (extract 47 40 rn))))
(if t17 (= t18 t16) (= t19 (extract 47 40 rn)))
(= t20 (if t17 t18 t19))
(= t21 (bvsle (zero_ext 16 t20) (zero_ext 16 (extract 55 48 rn))))
(if t21 (= t22 t20) (= t23 (extract 55 48 rn)))
(= t24 (if t21 t22 t23))
(= t25 (bvsle (zero_ext 16 t24) (zero_ext 16 (extract 63 56 rn))))
(if t25 (= t26 t24) (= t27 (extract 63 56 rn)))
(= t28 (if t25 t26 t27))
(= t29 (bvsle (zero_ext 16 t28) (zero_ext 16 (extract 71 64 rn))))
(if t29 (= t30 t28) (= t31 (extract 71 64 rn)))
(= t32 (if t29 t30 t31))
(= t33 (bvsle (zero_ext 16 t32) (zero_ext 16 (extract 79 72 rn))))
(if t33 (= t34 t32) (= t35 (extract 79 72 rn)))
(= t36 (if t33 t34 t35))
(= t37 (bvsle (zero_ext 16 t36) (zero_ext 16 (extract 87 80 rn))))
(if t37 (= t38 t36) (= t39 (extract 87 80 rn)))
(= t40 (if t37 t38 t39))
(= t41 (bvsle (zero_ext 16 t40) (zero_ext 16 (extract 95 88 rn))))
(if t41 (= t42 t40) (= t43 (extract 95 88 rn)))
(= t44 (if t41 t42 t43))
(= t45 (bvsle (zero_ext 16 t44) (zero_ext 16 (extract 103 96 rn))))
(if t45 (= t46 t44) (= t47 (extract 103 96 rn)))
(= t48 (if t45 t46 t47))
(= t49 (bvsle (zero_ext 16 t48) (zero_ext 16 (extract 111 104 rn))))
(if t49 (= t50 t48) (= t51 (extract 111 104 rn)))
(= t52 (if t49 t50 t51))
(= t53 (bvsle (zero_ext 16 t52) (zero_ext 16 (extract 119 112 rn))))
(if t53 (= t54 t52) (= t55 (extract 119 112 rn)))
(= t56 (if t53 t54 t55))
(= t57 (bvsle (zero_ext 16 t56) (zero_ext 16 (extract 127 120 rn))))
(if t57 (= t58 t56) (= t59 (extract 127 120 rn)))
(= t60 (if t57 t58 t59))
(= rd (zero_ext 128 t60))
)
)
)
((Addv)
(=
rd
(zero_ext
128
(bvadd
(bvadd
(bvadd (bvadd (extract 7 0 rn) (extract 15 8 rn)) (bvadd (extract 23 16 rn) (extract 31 24 rn)))
(bvadd (bvadd (extract 39 32 rn) (extract 47 40 rn)) (bvadd (extract 55 48 rn) (extract 63 56 rn)))
)
(bvadd
(bvadd (bvadd (extract 71 64 rn) (extract 79 72 rn)) (bvadd (extract 87 80 rn) (extract 95 88 rn)))
(bvadd (bvadd (extract 103 96 rn) (extract 111 104 rn)) (bvadd (extract 119 112 rn) (extract 127 120 rn)))
)
)
)
)
)
)
)
((Size8x8)
(match
op
((Uminv)
(with
(t1 t10 t11 t12 t13 t14 t15 t16 t17 t18 t19 t2 t20 t21 t22 t23 t24 t25 t26 t27 t28 t3 t4 t5 t6 t7 t8 t9)
(and
(= t1 (bvsle (zero_ext 16 (extract 7 0 rn)) (zero_ext 16 (extract 15 8 rn))))
(if t1 (= t2 (extract 7 0 rn)) (= t3 (extract 15 8 rn)))
(= t4 (if t1 t2 t3))
(= t5 (bvsle (zero_ext 16 t4) (zero_ext 16 (extract 23 16 rn))))
(if t5 (= t6 t4) (= t7 (extract 23 16 rn)))
(= t8 (if t5 t6 t7))
(= t9 (bvsle (zero_ext 16 t8) (zero_ext 16 (extract 31 24 rn))))
(if t9 (= t10 t8) (= t11 (extract 31 24 rn)))
(= t12 (if t9 t10 t11))
(= t13 (bvsle (zero_ext 16 t12) (zero_ext 16 (extract 39 32 rn))))
(if t13 (= t14 t12) (= t15 (extract 39 32 rn)))
(= t16 (if t13 t14 t15))
(= t17 (bvsle (zero_ext 16 t16) (zero_ext 16 (extract 47 40 rn))))
(if t17 (= t18 t16) (= t19 (extract 47 40 rn)))
(= t20 (if t17 t18 t19))
(= t21 (bvsle (zero_ext 16 t20) (zero_ext 16 (extract 55 48 rn))))
(if t21 (= t22 t20) (= t23 (extract 55 48 rn)))
(= t24 (if t21 t22 t23))
(= t25 (bvsle (zero_ext 16 t24) (zero_ext 16 (extract 63 56 rn))))
(if t25 (= t26 t24) (= t27 (extract 63 56 rn)))
(= t28 (if t25 t26 t27))
(= rd (zero_ext 128 t28))
)
)
)
((Addv)
(=
rd
(zero_ext
128
(bvadd
(bvadd (bvadd (extract 7 0 rn) (extract 15 8 rn)) (bvadd (extract 23 16 rn) (extract 31 24 rn)))
(bvadd (bvadd (extract 39 32 rn) (extract 47 40 rn)) (bvadd (extract 55 48 rn) (extract 63 56 rn)))
)
)
)
)
)
)
)
)
(require
(match
size
((Size32x4) (match op ((Uminv) true) ((Addv) true)))
((Size16x8) (match op ((Uminv) true) ((Addv) true)))
((Size16x4) (match op ((Uminv) true) ((Addv) true)))
((Size8x16) (match op ((Uminv) true) ((Addv) true)))
((Size8x8) (match op ((Uminv) true) ((Addv) true)))
)
)
)