xref: /linux/tools/testing/selftests/bpf/progs/verifier_div_mod_bounds.c (revision f17b474e36647c23801ef8fdaf2255ab66dd2973)
1 // SPDX-License-Identifier: GPL-2.0
2 
3 #include <linux/bpf.h>
4 #include <limits.h>
5 #include <bpf/bpf_helpers.h>
6 #include "bpf_misc.h"
7 
8 /* This file contains unit tests for signed/unsigned division and modulo
9  * operations (with divisor as a constant), focusing on verifying whether
10  * BPF verifier's range tracking module soundly and precisely computes
11  * the results.
12  */
13 
14 SEC("socket")
15 __description("UDIV32, positive divisor")
16 __success __retval(0) __log_level(2)
17 __msg("w1 /= 3 {{.*}}; R1=scalar(smin=smin32=0,smax=umax=smax32=umax32=3,var_off=(0x0; 0x3))")
18 __naked void udiv32_pos_divisor(void)
19 {
20 	asm volatile ("					\
21 	call %[bpf_get_prandom_u32];			\
22 	w1 = w0;					\
23 	w1 &= 8;					\
24 	w1 |= 1;					\
25 	w1 /= 3;					\
26 	if w1 > 3 goto l0_%=;				\
27 	r0 = 0;						\
28 	exit;						\
29 l0_%=:	r0 = *(u64 *)(r1 + 0);				\
30 	exit;						\
31 "	:
32 	: __imm(bpf_get_prandom_u32)
33 	: __clobber_all);
34 }
35 
36 SEC("socket")
37 __description("UDIV32, zero divisor")
38 __success __retval(0) __log_level(2)
39 __msg("w1 /= w2 {{.*}}; R1=0 R2=0")
40 __naked void udiv32_zero_divisor(void)
41 {
42 	asm volatile ("					\
43 	call %[bpf_get_prandom_u32];			\
44 	w1 = w0;					\
45 	w1 &= 8;					\
46 	w1 |= 1;					\
47 	w2 = 0;						\
48 	w1 /= w2;					\
49 	if w1 != 0 goto l0_%=;				\
50 	r0 = 0;						\
51 	exit;						\
52 l0_%=:	r0 = *(u64 *)(r1 + 0);				\
53 	exit;						\
54 "	:
55 	: __imm(bpf_get_prandom_u32)
56 	: __clobber_all);
57 }
58 
59 SEC("socket")
60 __description("UDIV64, positive divisor")
61 __success __retval(0) __log_level(2)
62 __msg("r1 /= 3 {{.*}}; R1=scalar(smin=smin32=0,smax=umax=smax32=umax32=3,var_off=(0x0; 0x3))")
63 __naked void udiv64_pos_divisor(void)
64 {
65 	asm volatile ("					\
66 	call %[bpf_get_prandom_u32];			\
67 	r1 = r0;					\
68 	r1 &= 8;					\
69 	r1 |= 1;					\
70 	r1 /= 3;					\
71 	if r1 > 3 goto l0_%=;				\
72 	r0 = 0;						\
73 	exit;						\
74 l0_%=:	r0 = *(u64 *)(r1 + 0);				\
75 	exit;						\
76 "	:
77 	: __imm(bpf_get_prandom_u32)
78 	: __clobber_all);
79 }
80 
81 SEC("socket")
82 __description("UDIV64, zero divisor")
83 __success __retval(0) __log_level(2)
84 __msg("r1 /= r2 {{.*}}; R1=0 R2=0")
85 __naked void udiv64_zero_divisor(void)
86 {
87 	asm volatile ("					\
88 	call %[bpf_get_prandom_u32];			\
89 	r1 = r0;					\
90 	r1 &= 8;					\
91 	r1 |= 1;					\
92 	r2 = 0;						\
93 	r1 /= r2;					\
94 	if r1 != 0 goto l0_%=;				\
95 	r0 = 0;						\
96 	exit;						\
97 l0_%=:	r0 = *(u64 *)(r1 + 0);				\
98 	exit;						\
99 "	:
100 	: __imm(bpf_get_prandom_u32)
101 	: __clobber_all);
102 }
103 
104 SEC("socket")
105 __description("SDIV32, positive divisor, positive dividend")
106 __success __retval(0) __log_level(2)
107 __msg("w1 s/= 3 {{.*}}; R1=scalar(smin=umin=smin32=umin32=2,smax=umax=smax32=umax32=3,var_off=(0x2; 0x1))")
108 __naked void sdiv32_pos_divisor_1(void)
109 {
110 	asm volatile ("					\
111 	call %[bpf_get_prandom_u32];			\
112 	w1 = w0;					\
113 	if w1 s< 8 goto l0_%=;				\
114 	if w1 s> 10 goto l0_%=;				\
115 	w1 s/= 3;					\
116 	if w1 s< 2 goto l1_%=;				\
117 	if w1 s> 3 goto l1_%=;				\
118 l0_%=:	r0 = 0;						\
119 	exit;						\
120 l1_%=:	r0 = *(u64 *)(r1 + 0);				\
121 	exit;						\
122 "	:
123 	: __imm(bpf_get_prandom_u32)
124 	: __clobber_all);
125 }
126 
127 SEC("socket")
128 __description("SDIV32, positive divisor, negative dividend")
129 __success __retval(0) __log_level(2)
130 __msg("w1 s/= 3 {{.*}}; R1=scalar(smin=umin=umin32=0xfffffffd,smax=umax=umax32=0xfffffffe,smin32=-3,smax32=-2,var_off=(0xfffffffc; 0x3))")
131 __naked void sdiv32_pos_divisor_2(void)
132 {
133 	asm volatile ("					\
134 	call %[bpf_get_prandom_u32];			\
135 	w1 = w0;					\
136 	if w1 s> -8 goto l0_%=;				\
137 	if w1 s< -10 goto l0_%=;			\
138 	w1 s/= 3;					\
139 	if w1 s< -3 goto l1_%=;				\
140 	if w1 s> -2 goto l1_%=;				\
141 l0_%=:	r0 = 0;						\
142 	exit;						\
143 l1_%=:	r0 = *(u64 *)(r1 + 0);				\
144 	exit;						\
145 "	:
146 	: __imm(bpf_get_prandom_u32)
147 	: __clobber_all);
148 }
149 
150 SEC("socket")
151 __description("SDIV32, positive divisor, mixed sign dividend")
152 __success __retval(0) __log_level(2)
153 __msg("w1 s/= 3 {{.*}}; R1=scalar(smin=0,smax=umax=0xffffffff,smin32=-2,smax32=3,var_off=(0x0; 0xffffffff))")
154 __naked void sdiv32_pos_divisor_3(void)
155 {
156 	asm volatile ("					\
157 	call %[bpf_get_prandom_u32];			\
158 	w1 = w0;					\
159 	if w1 s< -8 goto l0_%=;				\
160 	if w1 s> 10 goto l0_%=;				\
161 	w1 s/= 3;					\
162 	if w1 s< -2 goto l1_%=;				\
163 	if w1 s> 3 goto l1_%=;				\
164 l0_%=:	r0 = 0;						\
165 	exit;						\
166 l1_%=:	r0 = *(u64 *)(r1 + 0);				\
167 	exit;						\
168 "	:
169 	: __imm(bpf_get_prandom_u32)
170 	: __clobber_all);
171 }
172 
173 SEC("socket")
174 __description("SDIV32, negative divisor, positive dividend")
175 __success __retval(0) __log_level(2)
176 __msg("w1 s/= -3 {{.*}}; R1=scalar(smin=umin=umin32=0xfffffffd,smax=umax=umax32=0xfffffffe,smin32=-3,smax32=-2,var_off=(0xfffffffc; 0x3))")
177 __naked void sdiv32_neg_divisor_1(void)
178 {
179 	asm volatile ("					\
180 	call %[bpf_get_prandom_u32];			\
181 	w1 = w0;					\
182 	if w1 s< 8 goto l0_%=;				\
183 	if w1 s> 10 goto l0_%=;				\
184 	w1 s/= -3;					\
185 	if w1 s< -3 goto l1_%=;				\
186 	if w1 s> -2 goto l1_%=;				\
187 l0_%=:	r0 = 0;						\
188 	exit;						\
189 l1_%=:	r0 = *(u64 *)(r1 + 0);				\
190 	exit;						\
191 "	:
192 	: __imm(bpf_get_prandom_u32)
193 	: __clobber_all);
194 }
195 
196 SEC("socket")
197 __description("SDIV32, negative divisor, positive dividend")
198 __success __retval(0) __log_level(2)
199 __msg("w1 s/= -3 {{.*}}; R1=scalar(smin=umin=smin32=umin32=2,smax=umax=smax32=umax32=3,var_off=(0x2; 0x1))")
200 __naked void sdiv32_neg_divisor_2(void)
201 {
202 	asm volatile ("					\
203 	call %[bpf_get_prandom_u32];			\
204 	w1 = w0;					\
205 	if w1 s> -8 goto l0_%=;				\
206 	if w1 s< -10 goto l0_%=;			\
207 	w1 s/= -3;					\
208 	if w1 s< 2 goto l1_%=;				\
209 	if w1 s> 3 goto l1_%=;				\
210 l0_%=:	r0 = 0;						\
211 	exit;						\
212 l1_%=:	r0 = *(u64 *)(r1 + 0);				\
213 	exit;						\
214 "	:
215 	: __imm(bpf_get_prandom_u32)
216 	: __clobber_all);
217 }
218 
219 SEC("socket")
220 __description("SDIV32, negative divisor, mixed sign dividend")
221 __success __retval(0) __log_level(2)
222 __msg("w1 s/= -3 {{.*}}; R1=scalar(smin=0,smax=umax=0xffffffff,smin32=-3,smax32=2,var_off=(0x0; 0xffffffff))")
223 __naked void sdiv32_neg_divisor_3(void)
224 {
225 	asm volatile ("					\
226 	call %[bpf_get_prandom_u32];			\
227 	w1 = w0;					\
228 	if w1 s< -8 goto l0_%=;				\
229 	if w1 s> 10 goto l0_%=;				\
230 	w1 s/= -3;					\
231 	if w1 s< -3 goto l1_%=;				\
232 	if w1 s> 2 goto l1_%=;				\
233 l0_%=:	r0 = 0;						\
234 	exit;						\
235 l1_%=:	r0 = *(u64 *)(r1 + 0);				\
236 	exit;						\
237 "	:
238 	: __imm(bpf_get_prandom_u32)
239 	: __clobber_all);
240 }
241 
242 SEC("socket")
243 __description("SDIV32, zero divisor")
244 __success __retval(0) __log_level(2)
245 __msg("w1 s/= w2 {{.*}}; R1=0 R2=0")
246 __naked void sdiv32_zero_divisor(void)
247 {
248 	asm volatile ("					\
249 	call %[bpf_get_prandom_u32];			\
250 	w1 = w0;					\
251 	w1 &= 8;					\
252 	w1 |= 1;					\
253 	w2 = 0;						\
254 	w1 s/= w2;					\
255 	if w1 != 0 goto l0_%=;				\
256 	r0 = 0;						\
257 	exit;						\
258 l0_%=:	r0 = *(u64 *)(r1 + 0);				\
259 	exit;						\
260 "	:
261 	: __imm(bpf_get_prandom_u32)
262 	: __clobber_all);
263 }
264 
265 SEC("socket")
266 __description("SDIV32, overflow (S32_MIN/-1)")
267 __success __retval(0) __log_level(2)
268 __msg("w1 s/= -1 {{.*}}; R1=scalar(smin=0,smax=umax=0xffffffff,var_off=(0x0; 0xffffffff))")
269 __naked void sdiv32_overflow_1(void)
270 {
271 	asm volatile ("					\
272 	call %[bpf_get_prandom_u32];			\
273 	w1 = w0;					\
274 	w2 = %[int_min];				\
275 	w2 += 10;					\
276 	if w1 s> w2 goto l0_%=;				\
277 	w1 s/= -1;					\
278 l0_%=:	r0 = 0;						\
279 	exit;						\
280 "	:
281 	: __imm_const(int_min, INT_MIN),
282 	  __imm(bpf_get_prandom_u32)
283 	: __clobber_all);
284 }
285 
286 SEC("socket")
287 __description("SDIV32, overflow (S32_MIN/-1), constant dividend")
288 __success __retval(0) __log_level(2)
289 __msg("w1 s/= -1 {{.*}}; R1=0x80000000")
290 __naked void sdiv32_overflow_2(void)
291 {
292 	asm volatile ("					\
293 	w1 = %[int_min];				\
294 	w1 s/= -1;					\
295 	if w1 != %[int_min] goto l0_%=;			\
296 	r0 = 0;						\
297 	exit;						\
298 l0_%=:	r0 = *(u64 *)(r1 + 0);				\
299 	exit;						\
300 "	:
301 	: __imm_const(int_min, INT_MIN)
302 	: __clobber_all);
303 }
304 
305 SEC("socket")
306 __description("SDIV64, positive divisor, positive dividend")
307 __success __retval(0) __log_level(2)
308 __msg("r1 s/= 3 {{.*}}; R1=scalar(smin=umin=smin32=umin32=2,smax=umax=smax32=umax32=3,var_off=(0x2; 0x1))")
309 __naked void sdiv64_pos_divisor_1(void)
310 {
311 	asm volatile ("					\
312 	call %[bpf_get_prandom_u32];			\
313 	r1 = r0;					\
314 	if r1 s< 8 goto l0_%=;				\
315 	if r1 s> 10 goto l0_%=;				\
316 	r1 s/= 3;					\
317 	if r1 s< 2 goto l1_%=;				\
318 	if r1 s> 3 goto l1_%=;				\
319 l0_%=:	r0 = 0;						\
320 	exit;						\
321 l1_%=:	r0 = *(u64 *)(r1 + 0);				\
322 	exit;						\
323 "	:
324 	: __imm(bpf_get_prandom_u32)
325 	: __clobber_all);
326 }
327 
328 SEC("socket")
329 __description("SDIV64, positive divisor, negative dividend")
330 __success __retval(0) __log_level(2)
331 __msg("r1 s/= 3 {{.*}}; R1=scalar(smin=smin32=-3,smax=smax32=-2,umin=0xfffffffffffffffd,umax=0xfffffffffffffffe,umin32=0xfffffffd,umax32=0xfffffffe,var_off=(0xfffffffffffffffc; 0x3))")
332 __naked void sdiv64_pos_divisor_2(void)
333 {
334 	asm volatile ("					\
335 	call %[bpf_get_prandom_u32];			\
336 	r1 = r0;					\
337 	if r1 s> -8 goto l0_%=;				\
338 	if r1 s< -10 goto l0_%=;			\
339 	r1 s/= 3;					\
340 	if r1 s< -3 goto l1_%=;				\
341 	if r1 s> -2 goto l1_%=;				\
342 l0_%=:	r0 = 0;						\
343 	exit;						\
344 l1_%=:	r0 = *(u64 *)(r1 + 0);				\
345 	exit;						\
346 "	:
347 	: __imm(bpf_get_prandom_u32)
348 	: __clobber_all);
349 }
350 
351 SEC("socket")
352 __description("SDIV64, positive divisor, mixed sign dividend")
353 __success __retval(0) __log_level(2)
354 __msg("r1 s/= 3 {{.*}}; R1=scalar(smin=smin32=-2,smax=smax32=3)")
355 __naked void sdiv64_pos_divisor_3(void)
356 {
357 	asm volatile ("					\
358 	call %[bpf_get_prandom_u32];			\
359 	r1 = r0;					\
360 	if r1 s< -8 goto l0_%=;				\
361 	if r1 s> 10 goto l0_%=;				\
362 	r1 s/= 3;					\
363 	if r1 s< -2 goto l1_%=;				\
364 	if r1 s> 3 goto l1_%=;				\
365 l0_%=:	r0 = 0;						\
366 	exit;						\
367 l1_%=:	r0 = *(u64 *)(r1 + 0);				\
368 	exit;						\
369 "	:
370 	: __imm(bpf_get_prandom_u32)
371 	: __clobber_all);
372 }
373 
374 SEC("socket")
375 __description("SDIV64, negative divisor, positive dividend")
376 __success __retval(0) __log_level(2)
377 __msg("r1 s/= -3 {{.*}}; R1=scalar(smin=smin32=-3,smax=smax32=-2,umin=0xfffffffffffffffd,umax=0xfffffffffffffffe,umin32=0xfffffffd,umax32=0xfffffffe,var_off=(0xfffffffffffffffc; 0x3))")
378 __naked void sdiv64_neg_divisor_1(void)
379 {
380 	asm volatile ("					\
381 	call %[bpf_get_prandom_u32];			\
382 	r1 = r0;					\
383 	if r1 s< 8 goto l0_%=;				\
384 	if r1 s> 10 goto l0_%=;				\
385 	r1 s/= -3;					\
386 	if r1 s< -3 goto l1_%=;				\
387 	if r1 s> -2 goto l1_%=;				\
388 l0_%=:	r0 = 0;						\
389 	exit;						\
390 l1_%=:	r0 = *(u64 *)(r1 + 0);				\
391 	exit;						\
392 "	:
393 	: __imm(bpf_get_prandom_u32)
394 	: __clobber_all);
395 }
396 
397 SEC("socket")
398 __description("SDIV64, negative divisor, positive dividend")
399 __success __retval(0) __log_level(2)
400 __msg("r1 s/= -3 {{.*}}; R1=scalar(smin=umin=smin32=umin32=2,smax=umax=smax32=umax32=3,var_off=(0x2; 0x1))")
401 __naked void sdiv64_neg_divisor_2(void)
402 {
403 	asm volatile ("					\
404 	call %[bpf_get_prandom_u32];			\
405 	r1 = r0;					\
406 	if r1 s> -8 goto l0_%=;				\
407 	if r1 s< -10 goto l0_%=;			\
408 	r1 s/= -3;					\
409 	if r1 s< 2 goto l1_%=;				\
410 	if r1 s> 3 goto l1_%=;				\
411 l0_%=:	r0 = 0;						\
412 	exit;						\
413 l1_%=:	r0 = *(u64 *)(r1 + 0);				\
414 	exit;						\
415 "	:
416 	: __imm(bpf_get_prandom_u32)
417 	: __clobber_all);
418 }
419 
420 SEC("socket")
421 __description("SDIV64, negative divisor, mixed sign dividend")
422 __success __retval(0) __log_level(2)
423 __msg("r1 s/= -3 {{.*}}; R1=scalar(smin=smin32=-3,smax=smax32=2)")
424 __naked void sdiv64_neg_divisor_3(void)
425 {
426 	asm volatile ("					\
427 	call %[bpf_get_prandom_u32];			\
428 	r1 = r0;					\
429 	if r1 s< -8 goto l0_%=;				\
430 	if r1 s> 10 goto l0_%=;				\
431 	r1 s/= -3;					\
432 	if r1 s< -3 goto l1_%=;				\
433 	if r1 s> 2 goto l1_%=;				\
434 l0_%=:	r0 = 0;						\
435 	exit;						\
436 l1_%=:	r0 = *(u64 *)(r1 + 0);				\
437 	exit;						\
438 "	:
439 	: __imm(bpf_get_prandom_u32)
440 	: __clobber_all);
441 }
442 
443 SEC("socket")
444 __description("SDIV64, zero divisor")
445 __success __retval(0) __log_level(2)
446 __msg("r1 s/= r2 {{.*}}; R1=0 R2=0")
447 __naked void sdiv64_zero_divisor(void)
448 {
449 	asm volatile ("					\
450 	call %[bpf_get_prandom_u32];			\
451 	r1 = r0;					\
452 	r1 &= 8;					\
453 	r1 |= 1;					\
454 	r2 = 0;						\
455 	r1 s/= r2;					\
456 	if r1 != 0 goto l0_%=;				\
457 	r0 = 0;						\
458 	exit;						\
459 l0_%=:	r0 = *(u64 *)(r1 + 0);				\
460 	exit;						\
461 "	:
462 	: __imm(bpf_get_prandom_u32)
463 	: __clobber_all);
464 }
465 
466 SEC("socket")
467 __description("SDIV64, overflow (S64_MIN/-1)")
468 __success __retval(0) __log_level(2)
469 __msg("r1 s/= -1 {{.*}}; R1=scalar()")
470 __naked void sdiv64_overflow_1(void)
471 {
472 	asm volatile ("					\
473 	call %[bpf_ktime_get_ns];			\
474 	r1 = r0;					\
475 	r2 = %[llong_min] ll;				\
476 	r2 += 10;					\
477 	if r1 s> r2 goto l0_%=;				\
478 	r1 s/= -1;					\
479 l0_%=:	r0 = 0;						\
480 	exit;						\
481 "	:
482 	: __imm_const(llong_min, LLONG_MIN),
483 	  __imm(bpf_ktime_get_ns)
484 	: __clobber_all);
485 }
486 
487 SEC("socket")
488 __description("SDIV64, overflow (S64_MIN/-1), constant dividend")
489 __success __retval(0) __log_level(2)
490 __msg("r1 s/= -1 {{.*}}; R1=0x8000000000000000")
491 __naked void sdiv64_overflow_2(void)
492 {
493 	asm volatile ("					\
494 	r1 = %[llong_min] ll;				\
495 	r1 s/= -1;					\
496 	r2 = %[llong_min] ll;				\
497 	if r1 != r2 goto l0_%=;				\
498 	r0 = 0;						\
499 	exit;						\
500 l0_%=:	r0 = *(u64 *)(r1 + 0);				\
501 	exit;						\
502 "	:
503 	: __imm_const(llong_min, LLONG_MIN)
504 	: __clobber_all);
505 }
506 
507 SEC("socket")
508 __description("UMOD32, positive divisor")
509 __success __retval(0) __log_level(2)
510 __msg("w1 %= 3 {{.*}}; R1=scalar(smin=smin32=0,smax=umax=smax32=umax32=2,var_off=(0x0; 0x3))")
511 __naked void umod32_pos_divisor(void)
512 {
513 	asm volatile ("					\
514 	call %[bpf_get_prandom_u32];			\
515 	w1 = w0;					\
516 	w1 &= 8;					\
517 	w1 |= 1;					\
518 	w1 %%= 3;					\
519 	if w1 > 3 goto l0_%=;				\
520 	r0 = 0;						\
521 	exit;						\
522 l0_%=:	r0 = *(u64 *)(r1 + 0);				\
523 	exit;						\
524 "	:
525 	: __imm(bpf_get_prandom_u32)
526 	: __clobber_all);
527 }
528 
529 SEC("socket")
530 __description("UMOD32, positive divisor, small dividend")
531 __success __retval(0) __log_level(2)
532 __msg("w1 %= 10 {{.*}}; R1=scalar(smin=umin=smin32=umin32=1,smax=umax=smax32=umax32=9,var_off=(0x1; 0x8))")
533 __naked void umod32_pos_divisor_unchanged(void)
534 {
535 	asm volatile ("					\
536 	call %[bpf_get_prandom_u32];			\
537 	w1 = w0;					\
538 	w1 &= 8;					\
539 	w1 |= 1;					\
540 	w1 %%= 10;					\
541 	if w1 < 1 goto l0_%=;				\
542 	if w1 > 9 goto l0_%=;				\
543 	if w1 & 1 != 1 goto l0_%=;			\
544 	r0 = 0;						\
545 	exit;						\
546 l0_%=:	r0 = *(u64 *)(r1 + 0);				\
547 	exit;						\
548 "	:
549 	: __imm(bpf_get_prandom_u32)
550 	: __clobber_all);
551 }
552 
553 SEC("socket")
554 __description("UMOD32, zero divisor")
555 __success __retval(0) __log_level(2)
556 __msg("w1 %= w2 {{.*}}; R1=scalar(smin=umin=smin32=umin32=1,smax=umax=smax32=umax32=9,var_off=(0x1; 0x8)) R2=0")
557 __naked void umod32_zero_divisor(void)
558 {
559 	asm volatile ("					\
560 	call %[bpf_get_prandom_u32];			\
561 	w1 = w0;					\
562 	w1 &= 8;					\
563 	w1 |= 1;					\
564 	w2 = 0;						\
565 	w1 %%= w2;					\
566 	if w1 < 1 goto l0_%=;				\
567 	if w1 > 9 goto l0_%=;				\
568 	if w1 & 1 != 1 goto l0_%=;			\
569 	r0 = 0;						\
570 	exit;						\
571 l0_%=:	r0 = *(u64 *)(r1 + 0);				\
572 	exit;						\
573 "	:
574 	: __imm(bpf_get_prandom_u32)
575 	: __clobber_all);
576 }
577 
578 SEC("socket")
579 __description("UMOD64, positive divisor")
580 __success __retval(0) __log_level(2)
581 __msg("r1 %= 3 {{.*}}; R1=scalar(smin=smin32=0,smax=umax=smax32=umax32=2,var_off=(0x0; 0x3))")
582 __naked void umod64_pos_divisor(void)
583 {
584 	asm volatile ("					\
585 	call %[bpf_get_prandom_u32];			\
586 	r1 = r0;					\
587 	r1 &= 8;					\
588 	r1 |= 1;					\
589 	r1 %%= 3;					\
590 	if r1 > 3 goto l0_%=;				\
591 	r0 = 0;						\
592 	exit;						\
593 l0_%=:	r0 = *(u64 *)(r1 + 0);				\
594 	exit;						\
595 "	:
596 	: __imm(bpf_get_prandom_u32)
597 	: __clobber_all);
598 }
599 
600 SEC("socket")
601 __description("UMOD64, positive divisor, small dividend")
602 __success __retval(0) __log_level(2)
603 __msg("r1 %= 10 {{.*}}; R1=scalar(smin=umin=smin32=umin32=1,smax=umax=smax32=umax32=9,var_off=(0x1; 0x8))")
604 __naked void umod64_pos_divisor_unchanged(void)
605 {
606 	asm volatile ("					\
607 	call %[bpf_get_prandom_u32];			\
608 	r1 = r0;					\
609 	r1 &= 8;					\
610 	r1 |= 1;					\
611 	r1 %%= 10;					\
612 	if r1 < 1 goto l0_%=;				\
613 	if r1 > 9 goto l0_%=;				\
614 	if r1 & 1 != 1 goto l0_%=;			\
615 	r0 = 0;						\
616 	exit;						\
617 l0_%=:	r0 = *(u64 *)(r1 + 0);				\
618 	exit;						\
619 "	:
620 	: __imm(bpf_get_prandom_u32)
621 	: __clobber_all);
622 }
623 
624 SEC("socket")
625 __description("UMOD64, zero divisor")
626 __success __retval(0) __log_level(2)
627 __msg("r1 %= r2 {{.*}}; R1=scalar(smin=umin=smin32=umin32=1,smax=umax=smax32=umax32=9,var_off=(0x1; 0x8)) R2=0")
628 __naked void umod64_zero_divisor(void)
629 {
630 	asm volatile ("					\
631 	call %[bpf_get_prandom_u32];			\
632 	r1 = r0;					\
633 	r1 &= 8;					\
634 	r1 |= 1;					\
635 	r2 = 0;						\
636 	r1 %%= r2;					\
637 	if r1 < 1 goto l0_%=;				\
638 	if r1 > 9 goto l0_%=;				\
639 	if r1 & 1 != 1 goto l0_%=;			\
640 	r0 = 0;						\
641 	exit;						\
642 l0_%=:	r0 = *(u64 *)(r1 + 0);				\
643 	exit;						\
644 "	:
645 	: __imm(bpf_get_prandom_u32)
646 	: __clobber_all);
647 }
648 
649 SEC("socket")
650 __description("SMOD32, positive divisor, positive dividend")
651 __success __retval(0) __log_level(2)
652 __msg("w1 s%= 3 {{.*}}; R1=scalar(smin=smin32=0,smax=umax=smax32=umax32=2,var_off=(0x0; 0x3))")
653 __naked void smod32_pos_divisor_1(void)
654 {
655 	asm volatile ("					\
656 	call %[bpf_get_prandom_u32];			\
657 	w1 = w0;					\
658 	if w1 s< 8 goto l0_%=;				\
659 	if w1 s> 10 goto l0_%=;				\
660 	w1 s%%= 3;					\
661 	if w1 s< 0 goto l1_%=;				\
662 	if w1 s> 2 goto l1_%=;				\
663 l0_%=:	r0 = 0;						\
664 	exit;						\
665 l1_%=:	r0 = *(u64 *)(r1 + 0);				\
666 	exit;						\
667 "	:
668 	: __imm(bpf_get_prandom_u32)
669 	: __clobber_all);
670 }
671 
672 SEC("socket")
673 __description("SMOD32, positive divisor, negative dividend")
674 __success __retval(0) __log_level(2)
675 __msg("w1 s%= 3 {{.*}}; R1=scalar(smin=0,smax=umax=0xffffffff,smin32=-2,smax32=0,var_off=(0x0; 0xffffffff))")
676 __naked void smod32_pos_divisor_2(void)
677 {
678 	asm volatile ("					\
679 	call %[bpf_get_prandom_u32];			\
680 	w1 = w0;					\
681 	if w1 s> -8 goto l0_%=;				\
682 	if w1 s< -10 goto l0_%=;			\
683 	w1 s%%= 3;					\
684 	if w1 s< -2 goto l1_%=;				\
685 	if w1 s> 0 goto l1_%=;				\
686 l0_%=:	r0 = 0;						\
687 	exit;						\
688 l1_%=:	r0 = *(u64 *)(r1 + 0);				\
689 	exit;						\
690 "	:
691 	: __imm(bpf_get_prandom_u32)
692 	: __clobber_all);
693 }
694 
695 SEC("socket")
696 __description("SMOD32, positive divisor, mixed sign dividend")
697 __success __retval(0) __log_level(2)
698 __msg("w1 s%= 3 {{.*}}; R1=scalar(smin=0,smax=umax=0xffffffff,smin32=-2,smax32=2,var_off=(0x0; 0xffffffff))")
699 __naked void smod32_pos_divisor_3(void)
700 {
701 	asm volatile ("					\
702 	call %[bpf_get_prandom_u32];			\
703 	w1 = w0;					\
704 	if w1 s< -8 goto l0_%=;				\
705 	if w1 s> 10 goto l0_%=;				\
706 	w1 s%%= 3;					\
707 	if w1 s< -2 goto l1_%=;				\
708 	if w1 s> 2 goto l1_%=;				\
709 l0_%=:	r0 = 0;						\
710 	exit;						\
711 l1_%=:	r0 = *(u64 *)(r1 + 0);				\
712 	exit;						\
713 "	:
714 	: __imm(bpf_get_prandom_u32)
715 	: __clobber_all);
716 }
717 
718 SEC("socket")
719 __description("SMOD32, positive divisor, small dividend")
720 __success __retval(0) __log_level(2)
721 __msg("w1 s%= 11 {{.*}}; R1=scalar(smin=0,smax=umax=0xffffffff,smin32=-8,smax32=10,var_off=(0x0; 0xffffffff))")
722 __naked void smod32_pos_divisor_unchanged(void)
723 {
724 	asm volatile ("					\
725 	call %[bpf_get_prandom_u32];			\
726 	w1 = w0;					\
727 	if w1 s< -8 goto l0_%=;				\
728 	if w1 s> 10 goto l0_%=;				\
729 	w1 s%%= 11;					\
730 	if w1 s< -8 goto l1_%=;				\
731 	if w1 s> 10 goto l1_%=;				\
732 l0_%=:	r0 = 0;						\
733 	exit;						\
734 l1_%=:	r0 = *(u64 *)(r1 + 0);				\
735 	exit;						\
736 "	:
737 	: __imm(bpf_get_prandom_u32)
738 	: __clobber_all);
739 }
740 
741 SEC("socket")
742 __description("SMOD32, negative divisor, positive dividend")
743 __success __retval(0) __log_level(2)
744 __msg("w1 s%= -3 {{.*}}; R1=scalar(smin=smin32=0,smax=umax=smax32=umax32=2,var_off=(0x0; 0x3))")
745 __naked void smod32_neg_divisor_1(void)
746 {
747 	asm volatile ("					\
748 	call %[bpf_get_prandom_u32];			\
749 	w1 = w0;					\
750 	if w1 s< 8 goto l0_%=;				\
751 	if w1 s> 10 goto l0_%=;				\
752 	w1 s%%= -3;					\
753 	if w1 s< 0 goto l1_%=;				\
754 	if w1 s> 2 goto l1_%=;				\
755 l0_%=:	r0 = 0;						\
756 	exit;						\
757 l1_%=:	r0 = *(u64 *)(r1 + 0);				\
758 	exit;						\
759 "	:
760 	: __imm(bpf_get_prandom_u32)
761 	: __clobber_all);
762 }
763 
764 SEC("socket")
765 __description("SMOD32, negative divisor, negative dividend")
766 __success __retval(0) __log_level(2)
767 __msg("w1 s%= -3 {{.*}}; R1=scalar(smin=0,smax=umax=0xffffffff,smin32=-2,smax32=0,var_off=(0x0; 0xffffffff))")
768 __naked void smod32_neg_divisor_2(void)
769 {
770 	asm volatile ("					\
771 	call %[bpf_get_prandom_u32];			\
772 	w1 = w0;					\
773 	if w1 s> -8 goto l0_%=;				\
774 	if w1 s< -10 goto l0_%=;			\
775 	w1 s%%= -3;					\
776 	if w1 s< -2 goto l1_%=;				\
777 	if w1 s> 0 goto l1_%=;				\
778 l0_%=:	r0 = 0;						\
779 	exit;						\
780 l1_%=:	r0 = *(u64 *)(r1 + 0);				\
781 	exit;						\
782 "	:
783 	: __imm(bpf_get_prandom_u32)
784 	: __clobber_all);
785 }
786 
787 SEC("socket")
788 __description("SMOD32, negative divisor, mixed sign dividend")
789 __success __retval(0) __log_level(2)
790 __msg("w1 s%= -3 {{.*}}; R1=scalar(smin=0,smax=umax=0xffffffff,smin32=-2,smax32=2,var_off=(0x0; 0xffffffff))")
791 __naked void smod32_neg_divisor_3(void)
792 {
793 	asm volatile ("					\
794 	call %[bpf_get_prandom_u32];			\
795 	w1 = w0;					\
796 	if w1 s< -8 goto l0_%=;				\
797 	if w1 s> 10 goto l0_%=;				\
798 	w1 s%%= -3;					\
799 	if w1 s< -2 goto l1_%=;				\
800 	if w1 s> 2 goto l1_%=;				\
801 l0_%=:	r0 = 0;						\
802 	exit;						\
803 l1_%=:	r0 = *(u64 *)(r1 + 0);				\
804 	exit;						\
805 "	:
806 	: __imm(bpf_get_prandom_u32)
807 	: __clobber_all);
808 }
809 
810 SEC("socket")
811 __description("SMOD32, negative divisor, small dividend")
812 __success __retval(0) __log_level(2)
813 __msg("w1 s%= -11 {{.*}}; R1=scalar(smin=0,smax=umax=0xffffffff,smin32=-8,smax32=10,var_off=(0x0; 0xffffffff))")
814 __naked void smod32_neg_divisor_unchanged(void)
815 {
816 	asm volatile ("					\
817 	call %[bpf_get_prandom_u32];			\
818 	w1 = w0;					\
819 	if w1 s< -8 goto l0_%=;				\
820 	if w1 s> 10 goto l0_%=;				\
821 	w1 s%%= -11;					\
822 	if w1 s< -8 goto l1_%=;				\
823 	if w1 s> 10 goto l1_%=;				\
824 l0_%=:	r0 = 0;						\
825 	exit;						\
826 l1_%=:	r0 = *(u64 *)(r1 + 0);				\
827 	exit;						\
828 "	:
829 	: __imm(bpf_get_prandom_u32)
830 	: __clobber_all);
831 }
832 
833 SEC("socket")
834 __description("SMOD32, zero divisor")
835 __success __retval(0) __log_level(2)
836 __msg("w1 s%= w2 {{.*}}; R1=scalar(smin=0,smax=umax=0xffffffff,smin32=-8,smax32=10,var_off=(0x0; 0xffffffff)) R2=0")
837 __naked void smod32_zero_divisor(void)
838 {
839 	asm volatile ("					\
840 	call %[bpf_get_prandom_u32];			\
841 	w1 = w0;					\
842 	if w1 s< -8 goto l0_%=;				\
843 	if w1 s> 10 goto l0_%=;				\
844 	w2 = 0;						\
845 	w1 s%%= w2;					\
846 	if w1 s< -8 goto l1_%=;				\
847 	if w1 s> 10 goto l1_%=;				\
848 l0_%=:	r0 = 0;						\
849 	exit;						\
850 l1_%=:	r0 = *(u64 *)(r1 + 0);				\
851 	exit;						\
852 "	:
853 	: __imm(bpf_get_prandom_u32)
854 	: __clobber_all);
855 }
856 
857 SEC("socket")
858 __description("SMOD32, overflow (S32_MIN%-1)")
859 __success __retval(0) __log_level(2)
860 __msg("w1 s%= -1 {{.*}}; R1=0")
861 __naked void smod32_overflow_1(void)
862 {
863 	asm volatile ("					\
864 	call %[bpf_get_prandom_u32];			\
865 	w1 = w0;					\
866 	w2 = %[int_min];				\
867 	w2 += 10;					\
868 	if w1 s> w2 goto l0_%=;				\
869 	w1 s%%= -1;					\
870 	if w1 != 0 goto l1_%=;				\
871 l0_%=:	r0 = 0;						\
872 	exit;						\
873 l1_%=:	r0 = *(u64 *)(r1 + 0);				\
874 	exit;						\
875 "	:
876 	: __imm_const(int_min, INT_MIN),
877 	  __imm(bpf_get_prandom_u32)
878 	: __clobber_all);
879 }
880 
881 SEC("socket")
882 __description("SMOD32, overflow (S32_MIN%-1), constant dividend")
883 __success __retval(0) __log_level(2)
884 __msg("w1 s%= -1 {{.*}}; R1=0")
885 __naked void smod32_overflow_2(void)
886 {
887 	asm volatile ("					\
888 	w1 = %[int_min];				\
889 	w1 s%%= -1;					\
890 	if w1 != 0 goto l0_%=;				\
891 	r0 = 0;						\
892 	exit;						\
893 l0_%=:	r0 = *(u64 *)(r1 + 0);				\
894 	exit;						\
895 "	:
896 	: __imm_const(int_min, INT_MIN)
897 	: __clobber_all);
898 }
899 
900 SEC("socket")
901 __description("SMOD64, positive divisor, positive dividend")
902 __success __retval(0) __log_level(2)
903 __msg("r1 s%= 3 {{.*}}; R1=scalar(smin=smin32=0,smax=umax=smax32=umax32=2,var_off=(0x0; 0x3))")
904 __naked void smod64_pos_divisor_1(void)
905 {
906 	asm volatile ("					\
907 	call %[bpf_get_prandom_u32];			\
908 	r1 = r0;					\
909 	if r1 s< 8 goto l0_%=;				\
910 	if r1 s> 10 goto l0_%=;				\
911 	r1 s%%= 3;					\
912 	if r1 s< 0 goto l1_%=;				\
913 	if r1 s> 2 goto l1_%=;				\
914 l0_%=:	r0 = 0;						\
915 	exit;						\
916 l1_%=:	r0 = *(u64 *)(r1 + 0);				\
917 	exit;						\
918 "	:
919 	: __imm(bpf_get_prandom_u32)
920 	: __clobber_all);
921 }
922 
923 SEC("socket")
924 __description("SMOD64, positive divisor, negative dividend")
925 __success __retval(0) __log_level(2)
926 __msg("r1 s%= 3 {{.*}}; R1=scalar(smin=smin32=-2,smax=smax32=0)")
927 __naked void smod64_pos_divisor_2(void)
928 {
929 	asm volatile ("					\
930 	call %[bpf_get_prandom_u32];			\
931 	r1 = r0;					\
932 	if r1 s> -8 goto l0_%=;				\
933 	if r1 s< -10 goto l0_%=;			\
934 	r1 s%%= 3;					\
935 	if r1 s< -2 goto l1_%=;				\
936 	if r1 s> 0 goto l1_%=;				\
937 l0_%=:	r0 = 0;						\
938 	exit;						\
939 l1_%=:	r0 = *(u64 *)(r1 + 0);				\
940 	exit;						\
941 "	:
942 	: __imm(bpf_get_prandom_u32)
943 	: __clobber_all);
944 }
945 
946 SEC("socket")
947 __description("SMOD64, positive divisor, mixed sign dividend")
948 __success __retval(0) __log_level(2)
949 __msg("r1 s%= 3 {{.*}}; R1=scalar(smin=smin32=-2,smax=smax32=2)")
950 __naked void smod64_pos_divisor_3(void)
951 {
952 	asm volatile ("					\
953 	call %[bpf_get_prandom_u32];			\
954 	r1 = r0;					\
955 	if r1 s< -8 goto l0_%=;				\
956 	if r1 s> 10 goto l0_%=;				\
957 	r1 s%%= 3;					\
958 	if r1 s< -2 goto l1_%=;				\
959 	if r1 s> 2 goto l1_%=;				\
960 l0_%=:	r0 = 0;						\
961 	exit;						\
962 l1_%=:	r0 = *(u64 *)(r1 + 0);				\
963 	exit;						\
964 "	:
965 	: __imm(bpf_get_prandom_u32)
966 	: __clobber_all);
967 }
968 
969 SEC("socket")
970 __description("SMOD64, positive divisor, small dividend")
971 __success __retval(0) __log_level(2)
972 __msg("r1 s%= 11 {{.*}}; R1=scalar(smin=smin32=-8,smax=smax32=10)")
973 __naked void smod64_pos_divisor_unchanged(void)
974 {
975 	asm volatile ("					\
976 	call %[bpf_get_prandom_u32];			\
977 	r1 = r0;					\
978 	if r1 s< -8 goto l0_%=;				\
979 	if r1 s> 10 goto l0_%=;				\
980 	r1 s%%= 11;					\
981 	if r1 s< -8 goto l1_%=;				\
982 	if r1 s> 10 goto l1_%=;				\
983 l0_%=:	r0 = 0;						\
984 	exit;						\
985 l1_%=:	r0 = *(u64 *)(r1 + 0);				\
986 	exit;						\
987 "	:
988 	: __imm(bpf_get_prandom_u32)
989 	: __clobber_all);
990 }
991 
992 SEC("socket")
993 __description("SMOD64, negative divisor, positive dividend")
994 __success __retval(0) __log_level(2)
995 __msg("r1 s%= -3 {{.*}}; R1=scalar(smin=smin32=0,smax=umax=smax32=umax32=2,var_off=(0x0; 0x3))")
996 __naked void smod64_neg_divisor_1(void)
997 {
998 	asm volatile ("					\
999 	call %[bpf_get_prandom_u32];			\
1000 	r1 = r0;					\
1001 	if r1 s< 8 goto l0_%=;				\
1002 	if r1 s> 10 goto l0_%=;				\
1003 	r1 s%%= -3;					\
1004 	if r1 s< 0 goto l1_%=;				\
1005 	if r1 s> 2 goto l1_%=;				\
1006 l0_%=:	r0 = 0;						\
1007 	exit;						\
1008 l1_%=:	r0 = *(u64 *)(r1 + 0);				\
1009 	exit;						\
1010 "	:
1011 	: __imm(bpf_get_prandom_u32)
1012 	: __clobber_all);
1013 }
1014 
1015 SEC("socket")
1016 __description("SMOD64, negative divisor, negative dividend")
1017 __success __retval(0) __log_level(2)
1018 __msg("r1 s%= -3 {{.*}}; R1=scalar(smin=smin32=-2,smax=smax32=0)")
1019 __naked void smod64_neg_divisor_2(void)
1020 {
1021 	asm volatile ("					\
1022 	call %[bpf_get_prandom_u32];			\
1023 	r1 = r0;					\
1024 	if r1 s> -8 goto l0_%=;				\
1025 	if r1 s< -10 goto l0_%=;			\
1026 	r1 s%%= -3;					\
1027 	if r1 s< -2 goto l1_%=;				\
1028 	if r1 s> 0 goto l1_%=;				\
1029 l0_%=:	r0 = 0;						\
1030 	exit;						\
1031 l1_%=:	r0 = *(u64 *)(r1 + 0);				\
1032 	exit;						\
1033 "	:
1034 	: __imm(bpf_get_prandom_u32)
1035 	: __clobber_all);
1036 }
1037 
1038 SEC("socket")
1039 __description("SMOD64, negative divisor, mixed sign dividend")
1040 __success __retval(0) __log_level(2)
1041 __msg("r1 s%= -3 {{.*}}; R1=scalar(smin=smin32=-2,smax=smax32=2)")
1042 __naked void smod64_neg_divisor_3(void)
1043 {
1044 	asm volatile ("					\
1045 	call %[bpf_get_prandom_u32];			\
1046 	r1 = r0;					\
1047 	if r1 s< -8 goto l0_%=;				\
1048 	if r1 s> 10 goto l0_%=;				\
1049 	r1 s%%= -3;					\
1050 	if r1 s< -2 goto l1_%=;				\
1051 	if r1 s> 2 goto l1_%=;				\
1052 l0_%=:	r0 = 0;						\
1053 	exit;						\
1054 l1_%=:	r0 = *(u64 *)(r1 + 0);				\
1055 	exit;						\
1056 "	:
1057 	: __imm(bpf_get_prandom_u32)
1058 	: __clobber_all);
1059 }
1060 
1061 SEC("socket")
1062 __description("SMOD64, negative divisor, small dividend")
1063 __success __retval(0) __log_level(2)
1064 __msg("r1 s%= -11 {{.*}}; R1=scalar(smin=smin32=-8,smax=smax32=10)")
1065 __naked void smod64_neg_divisor_unchanged(void)
1066 {
1067 	asm volatile ("					\
1068 	call %[bpf_get_prandom_u32];			\
1069 	r1 = r0;					\
1070 	if r1 s< -8 goto l0_%=;				\
1071 	if r1 s> 10 goto l0_%=;				\
1072 	r1 s%%= -11;					\
1073 	if r1 s< -8 goto l1_%=;				\
1074 	if r1 s> 10 goto l1_%=;				\
1075 l0_%=:	r0 = 0;						\
1076 	exit;						\
1077 l1_%=:	r0 = *(u64 *)(r1 + 0);				\
1078 	exit;						\
1079 "	:
1080 	: __imm(bpf_get_prandom_u32)
1081 	: __clobber_all);
1082 }
1083 
1084 SEC("socket")
1085 __description("SMOD64, zero divisor")
1086 __success __retval(0) __log_level(2)
1087 __msg("r1 s%= r2 {{.*}}; R1=scalar(smin=smin32=-8,smax=smax32=10) R2=0")
1088 __naked void smod64_zero_divisor(void)
1089 {
1090 	asm volatile ("					\
1091 	call %[bpf_get_prandom_u32];			\
1092 	r1 = r0;					\
1093 	if r1 s< -8 goto l0_%=;				\
1094 	if r1 s> 10 goto l0_%=;				\
1095 	r2 = 0;						\
1096 	r1 s%%= r2;					\
1097 	if r1 s< -8 goto l1_%=;				\
1098 	if r1 s> 10 goto l1_%=;				\
1099 l0_%=:	r0 = 0;						\
1100 	exit;						\
1101 l1_%=:	r0 = *(u64 *)(r1 + 0);				\
1102 	exit;						\
1103 "	:
1104 	: __imm(bpf_get_prandom_u32)
1105 	: __clobber_all);
1106 }
1107 
1108 SEC("socket")
1109 __description("SMOD64, overflow (S64_MIN%-1)")
1110 __success __retval(0) __log_level(2)
1111 __msg("r1 s%= -1 {{.*}}; R1=0")
1112 __naked void smod64_overflow_1(void)
1113 {
1114 	asm volatile ("					\
1115 	call %[bpf_ktime_get_ns];			\
1116 	r1 = r0;					\
1117 	r2 = %[llong_min] ll;				\
1118 	r2 += 10;					\
1119 	if r1 s> r2 goto l0_%=;				\
1120 	r1 s%%= -1;					\
1121 	if r1 != 0 goto l1_%=;				\
1122 l0_%=:	r0 = 0;						\
1123 	exit;						\
1124 l1_%=:	r0 = *(u64 *)(r1 + 0);				\
1125 	exit;						\
1126 "	:
1127 	: __imm_const(llong_min, LLONG_MIN),
1128 	  __imm(bpf_ktime_get_ns)
1129 	: __clobber_all);
1130 }
1131 
1132 SEC("socket")
1133 __description("SMOD64, overflow (S64_MIN%-1), constant dividend")
1134 __success __retval(0) __log_level(2)
1135 __msg("r1 s%= -1 {{.*}}; R1=0")
1136 __naked void smod64_overflow_2(void)
1137 {
1138 	asm volatile ("					\
1139 	r1 = %[llong_min] ll;				\
1140 	r1 s%%= -1;					\
1141 	if r1 != 0 goto l0_%=;				\
1142 	r0 = 0;						\
1143 	exit;						\
1144 l0_%=:	r0 = *(u64 *)(r1 + 0);				\
1145 	exit;						\
1146 "	:
1147 	: __imm_const(llong_min, LLONG_MIN)
1148 	: __clobber_all);
1149 }
1150