xref: /linux/tools/testing/selftests/bpf/progs/verifier_div_mod_bounds.c (revision c4dde411bc366f568dbe33366253bbfea049e8ea)
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")
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")
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")
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 	r2 = r1;					\
279 l0_%=:	r0 = 0;						\
280 	exit;						\
281 "	:
282 	: __imm_const(int_min, INT_MIN),
283 	  __imm(bpf_get_prandom_u32)
284 	: __clobber_all);
285 }
286 
287 SEC("socket")
288 __description("SDIV32, overflow (S32_MIN/-1), constant dividend")
289 __success __retval(0) __log_level(2)
290 __msg("w1 s/= -1 {{.*}}; R1=0x80000000")
291 __naked void sdiv32_overflow_2(void)
292 {
293 	asm volatile ("					\
294 	w1 = %[int_min];				\
295 	w1 s/= -1;					\
296 	if w1 != %[int_min] goto l0_%=;			\
297 	r0 = 0;						\
298 	exit;						\
299 l0_%=:	r0 = *(u64 *)(r1 + 0);				\
300 	exit;						\
301 "	:
302 	: __imm_const(int_min, INT_MIN)
303 	: __clobber_all);
304 }
305 
306 SEC("socket")
307 __description("SDIV64, positive divisor, positive dividend")
308 __success __retval(0) __log_level(2)
309 __msg("r1 s/= 3 {{.*}}; R1=scalar(smin=umin=smin32=umin32=2,smax=umax=smax32=umax32=3,var_off=(0x2; 0x1))")
310 __naked void sdiv64_pos_divisor_1(void)
311 {
312 	asm volatile ("					\
313 	call %[bpf_get_prandom_u32];			\
314 	r1 = r0;					\
315 	if r1 s< 8 goto l0_%=;				\
316 	if r1 s> 10 goto l0_%=;				\
317 	r1 s/= 3;					\
318 	if r1 s< 2 goto l1_%=;				\
319 	if r1 s> 3 goto l1_%=;				\
320 l0_%=:	r0 = 0;						\
321 	exit;						\
322 l1_%=:	r0 = *(u64 *)(r1 + 0);				\
323 	exit;						\
324 "	:
325 	: __imm(bpf_get_prandom_u32)
326 	: __clobber_all);
327 }
328 
329 SEC("socket")
330 __description("SDIV64, positive divisor, negative dividend")
331 __success __retval(0) __log_level(2)
332 __msg("r1 s/= 3 {{.*}}; R1=scalar(smin=smin32=-3,smax=smax32=-2,umin=0xfffffffffffffffd,umax=0xfffffffffffffffe,umin32=0xfffffffd,umax32=0xfffffffe,var_off=(0xfffffffffffffffc; 0x3))")
333 __naked void sdiv64_pos_divisor_2(void)
334 {
335 	asm volatile ("					\
336 	call %[bpf_get_prandom_u32];			\
337 	r1 = r0;					\
338 	if r1 s> -8 goto l0_%=;				\
339 	if r1 s< -10 goto l0_%=;			\
340 	r1 s/= 3;					\
341 	if r1 s< -3 goto l1_%=;				\
342 	if r1 s> -2 goto l1_%=;				\
343 l0_%=:	r0 = 0;						\
344 	exit;						\
345 l1_%=:	r0 = *(u64 *)(r1 + 0);				\
346 	exit;						\
347 "	:
348 	: __imm(bpf_get_prandom_u32)
349 	: __clobber_all);
350 }
351 
352 SEC("socket")
353 __description("SDIV64, positive divisor, mixed sign dividend")
354 __success __retval(0) __log_level(2)
355 __msg("r1 s/= 3 {{.*}}; R1=scalar(smin=smin32=-2,smax=smax32=3)")
356 __naked void sdiv64_pos_divisor_3(void)
357 {
358 	asm volatile ("					\
359 	call %[bpf_get_prandom_u32];			\
360 	r1 = r0;					\
361 	if r1 s< -8 goto l0_%=;				\
362 	if r1 s> 10 goto l0_%=;				\
363 	r1 s/= 3;					\
364 	if r1 s< -2 goto l1_%=;				\
365 	if r1 s> 3 goto l1_%=;				\
366 l0_%=:	r0 = 0;						\
367 	exit;						\
368 l1_%=:	r0 = *(u64 *)(r1 + 0);				\
369 	exit;						\
370 "	:
371 	: __imm(bpf_get_prandom_u32)
372 	: __clobber_all);
373 }
374 
375 SEC("socket")
376 __description("SDIV64, negative divisor, positive dividend")
377 __success __retval(0) __log_level(2)
378 __msg("r1 s/= -3 {{.*}}; R1=scalar(smin=smin32=-3,smax=smax32=-2,umin=0xfffffffffffffffd,umax=0xfffffffffffffffe,umin32=0xfffffffd,umax32=0xfffffffe,var_off=(0xfffffffffffffffc; 0x3))")
379 __naked void sdiv64_neg_divisor_1(void)
380 {
381 	asm volatile ("					\
382 	call %[bpf_get_prandom_u32];			\
383 	r1 = r0;					\
384 	if r1 s< 8 goto l0_%=;				\
385 	if r1 s> 10 goto l0_%=;				\
386 	r1 s/= -3;					\
387 	if r1 s< -3 goto l1_%=;				\
388 	if r1 s> -2 goto l1_%=;				\
389 l0_%=:	r0 = 0;						\
390 	exit;						\
391 l1_%=:	r0 = *(u64 *)(r1 + 0);				\
392 	exit;						\
393 "	:
394 	: __imm(bpf_get_prandom_u32)
395 	: __clobber_all);
396 }
397 
398 SEC("socket")
399 __description("SDIV64, negative divisor, positive dividend")
400 __success __retval(0) __log_level(2)
401 __msg("r1 s/= -3 {{.*}}; R1=scalar(smin=umin=smin32=umin32=2,smax=umax=smax32=umax32=3,var_off=(0x2; 0x1))")
402 __naked void sdiv64_neg_divisor_2(void)
403 {
404 	asm volatile ("					\
405 	call %[bpf_get_prandom_u32];			\
406 	r1 = r0;					\
407 	if r1 s> -8 goto l0_%=;				\
408 	if r1 s< -10 goto l0_%=;			\
409 	r1 s/= -3;					\
410 	if r1 s< 2 goto l1_%=;				\
411 	if r1 s> 3 goto l1_%=;				\
412 l0_%=:	r0 = 0;						\
413 	exit;						\
414 l1_%=:	r0 = *(u64 *)(r1 + 0);				\
415 	exit;						\
416 "	:
417 	: __imm(bpf_get_prandom_u32)
418 	: __clobber_all);
419 }
420 
421 SEC("socket")
422 __description("SDIV64, negative divisor, mixed sign dividend")
423 __success __retval(0) __log_level(2)
424 __msg("r1 s/= -3 {{.*}}; R1=scalar(smin=smin32=-3,smax=smax32=2)")
425 __naked void sdiv64_neg_divisor_3(void)
426 {
427 	asm volatile ("					\
428 	call %[bpf_get_prandom_u32];			\
429 	r1 = r0;					\
430 	if r1 s< -8 goto l0_%=;				\
431 	if r1 s> 10 goto l0_%=;				\
432 	r1 s/= -3;					\
433 	if r1 s< -3 goto l1_%=;				\
434 	if r1 s> 2 goto l1_%=;				\
435 l0_%=:	r0 = 0;						\
436 	exit;						\
437 l1_%=:	r0 = *(u64 *)(r1 + 0);				\
438 	exit;						\
439 "	:
440 	: __imm(bpf_get_prandom_u32)
441 	: __clobber_all);
442 }
443 
444 SEC("socket")
445 __description("SDIV64, zero divisor")
446 __success __retval(0) __log_level(2)
447 __msg("r1 s/= r2 {{.*}}; R1=0")
448 __naked void sdiv64_zero_divisor(void)
449 {
450 	asm volatile ("					\
451 	call %[bpf_get_prandom_u32];			\
452 	r1 = r0;					\
453 	r1 &= 8;					\
454 	r1 |= 1;					\
455 	r2 = 0;						\
456 	r1 s/= r2;					\
457 	if r1 != 0 goto l0_%=;				\
458 	r0 = 0;						\
459 	exit;						\
460 l0_%=:	r0 = *(u64 *)(r1 + 0);				\
461 	exit;						\
462 "	:
463 	: __imm(bpf_get_prandom_u32)
464 	: __clobber_all);
465 }
466 
467 SEC("socket")
468 __description("SDIV64, overflow (S64_MIN/-1)")
469 __success __retval(0) __log_level(2)
470 __msg("r1 s/= -1 {{.*}}; R1=scalar()")
471 __naked void sdiv64_overflow_1(void)
472 {
473 	asm volatile ("					\
474 	call %[bpf_ktime_get_ns];			\
475 	r1 = r0;					\
476 	r2 = %[llong_min] ll;				\
477 	r2 += 10;					\
478 	if r1 s> r2 goto l0_%=;				\
479 	r1 s/= -1;					\
480 	r2 = r1;					\
481 l0_%=:	r0 = 0;						\
482 	exit;						\
483 "	:
484 	: __imm_const(llong_min, LLONG_MIN),
485 	  __imm(bpf_ktime_get_ns)
486 	: __clobber_all);
487 }
488 
489 SEC("socket")
490 __description("SDIV64, overflow (S64_MIN/-1), constant dividend")
491 __success __retval(0) __log_level(2)
492 __msg("r1 s/= -1 {{.*}}; R1=0x8000000000000000")
493 __naked void sdiv64_overflow_2(void)
494 {
495 	asm volatile ("					\
496 	r1 = %[llong_min] ll;				\
497 	r1 s/= -1;					\
498 	r2 = %[llong_min] ll;				\
499 	if r1 != r2 goto l0_%=;				\
500 	r0 = 0;						\
501 	exit;						\
502 l0_%=:	r0 = *(u64 *)(r1 + 0);				\
503 	exit;						\
504 "	:
505 	: __imm_const(llong_min, LLONG_MIN)
506 	: __clobber_all);
507 }
508 
509 SEC("socket")
510 __description("UMOD32, positive divisor")
511 __success __retval(0) __log_level(2)
512 __msg("w1 %= 3 {{.*}}; R1=scalar(smin=smin32=0,smax=umax=smax32=umax32=2,var_off=(0x0; 0x3))")
513 __naked void umod32_pos_divisor(void)
514 {
515 	asm volatile ("					\
516 	call %[bpf_get_prandom_u32];			\
517 	w1 = w0;					\
518 	w1 &= 8;					\
519 	w1 |= 1;					\
520 	w1 %%= 3;					\
521 	if w1 > 3 goto l0_%=;				\
522 	r0 = 0;						\
523 	exit;						\
524 l0_%=:	r0 = *(u64 *)(r1 + 0);				\
525 	exit;						\
526 "	:
527 	: __imm(bpf_get_prandom_u32)
528 	: __clobber_all);
529 }
530 
531 SEC("socket")
532 __description("UMOD32, positive divisor, small dividend")
533 __success __retval(0) __log_level(2)
534 __msg("w1 %= 10 {{.*}}; R1=scalar(smin=umin=smin32=umin32=1,smax=umax=smax32=umax32=9,var_off=(0x1; 0x8))")
535 __naked void umod32_pos_divisor_unchanged(void)
536 {
537 	asm volatile ("					\
538 	call %[bpf_get_prandom_u32];			\
539 	w1 = w0;					\
540 	w1 &= 8;					\
541 	w1 |= 1;					\
542 	w1 %%= 10;					\
543 	if w1 < 1 goto l0_%=;				\
544 	if w1 > 9 goto l0_%=;				\
545 	if w1 & 1 != 1 goto l0_%=;			\
546 	r0 = 0;						\
547 	exit;						\
548 l0_%=:	r0 = *(u64 *)(r1 + 0);				\
549 	exit;						\
550 "	:
551 	: __imm(bpf_get_prandom_u32)
552 	: __clobber_all);
553 }
554 
555 SEC("socket")
556 __description("UMOD32, zero divisor")
557 __success __retval(0) __log_level(2)
558 __msg("w1 %= w2 {{.*}}; R1=scalar(smin=umin=smin32=umin32=1,smax=umax=smax32=umax32=9,var_off=(0x1; 0x8))")
559 __naked void umod32_zero_divisor(void)
560 {
561 	asm volatile ("					\
562 	call %[bpf_get_prandom_u32];			\
563 	w1 = w0;					\
564 	w1 &= 8;					\
565 	w1 |= 1;					\
566 	w2 = 0;						\
567 	w1 %%= w2;					\
568 	if w1 < 1 goto l0_%=;				\
569 	if w1 > 9 goto l0_%=;				\
570 	if w1 & 1 != 1 goto l0_%=;			\
571 	r0 = 0;						\
572 	exit;						\
573 l0_%=:	r0 = *(u64 *)(r1 + 0);				\
574 	exit;						\
575 "	:
576 	: __imm(bpf_get_prandom_u32)
577 	: __clobber_all);
578 }
579 
580 SEC("socket")
581 __description("UMOD64, positive divisor")
582 __success __retval(0) __log_level(2)
583 __msg("r1 %= 3 {{.*}}; R1=scalar(smin=smin32=0,smax=umax=smax32=umax32=2,var_off=(0x0; 0x3))")
584 __naked void umod64_pos_divisor(void)
585 {
586 	asm volatile ("					\
587 	call %[bpf_get_prandom_u32];			\
588 	r1 = r0;					\
589 	r1 &= 8;					\
590 	r1 |= 1;					\
591 	r1 %%= 3;					\
592 	if r1 > 3 goto l0_%=;				\
593 	r0 = 0;						\
594 	exit;						\
595 l0_%=:	r0 = *(u64 *)(r1 + 0);				\
596 	exit;						\
597 "	:
598 	: __imm(bpf_get_prandom_u32)
599 	: __clobber_all);
600 }
601 
602 SEC("socket")
603 __description("UMOD64, positive divisor, small dividend")
604 __success __retval(0) __log_level(2)
605 __msg("r1 %= 10 {{.*}}; R1=scalar(smin=umin=smin32=umin32=1,smax=umax=smax32=umax32=9,var_off=(0x1; 0x8))")
606 __naked void umod64_pos_divisor_unchanged(void)
607 {
608 	asm volatile ("					\
609 	call %[bpf_get_prandom_u32];			\
610 	r1 = r0;					\
611 	r1 &= 8;					\
612 	r1 |= 1;					\
613 	r1 %%= 10;					\
614 	if r1 < 1 goto l0_%=;				\
615 	if r1 > 9 goto l0_%=;				\
616 	if r1 & 1 != 1 goto l0_%=;			\
617 	r0 = 0;						\
618 	exit;						\
619 l0_%=:	r0 = *(u64 *)(r1 + 0);				\
620 	exit;						\
621 "	:
622 	: __imm(bpf_get_prandom_u32)
623 	: __clobber_all);
624 }
625 
626 SEC("socket")
627 __description("UMOD64, zero divisor")
628 __success __retval(0) __log_level(2)
629 __msg("r1 %= r2 {{.*}}; R1=scalar(smin=umin=smin32=umin32=1,smax=umax=smax32=umax32=9,var_off=(0x1; 0x8))")
630 __naked void umod64_zero_divisor(void)
631 {
632 	asm volatile ("					\
633 	call %[bpf_get_prandom_u32];			\
634 	r1 = r0;					\
635 	r1 &= 8;					\
636 	r1 |= 1;					\
637 	r2 = 0;						\
638 	r1 %%= r2;					\
639 	if r1 < 1 goto l0_%=;				\
640 	if r1 > 9 goto l0_%=;				\
641 	if r1 & 1 != 1 goto l0_%=;			\
642 	r0 = 0;						\
643 	exit;						\
644 l0_%=:	r0 = *(u64 *)(r1 + 0);				\
645 	exit;						\
646 "	:
647 	: __imm(bpf_get_prandom_u32)
648 	: __clobber_all);
649 }
650 
651 SEC("socket")
652 __description("SMOD32, positive divisor, positive dividend")
653 __success __retval(0) __log_level(2)
654 __msg("w1 s%= 3 {{.*}}; R1=scalar(smin=smin32=0,smax=umax=smax32=umax32=2,var_off=(0x0; 0x3))")
655 __naked void smod32_pos_divisor_1(void)
656 {
657 	asm volatile ("					\
658 	call %[bpf_get_prandom_u32];			\
659 	w1 = w0;					\
660 	if w1 s< 8 goto l0_%=;				\
661 	if w1 s> 10 goto l0_%=;				\
662 	w1 s%%= 3;					\
663 	if w1 s< 0 goto l1_%=;				\
664 	if w1 s> 2 goto l1_%=;				\
665 l0_%=:	r0 = 0;						\
666 	exit;						\
667 l1_%=:	r0 = *(u64 *)(r1 + 0);				\
668 	exit;						\
669 "	:
670 	: __imm(bpf_get_prandom_u32)
671 	: __clobber_all);
672 }
673 
674 SEC("socket")
675 __description("SMOD32, positive divisor, negative dividend")
676 __success __retval(0) __log_level(2)
677 __msg("w1 s%= 3 {{.*}}; R1=scalar(smin=0,smax=umax=0xffffffff,smin32=-2,smax32=0,var_off=(0x0; 0xffffffff))")
678 __naked void smod32_pos_divisor_2(void)
679 {
680 	asm volatile ("					\
681 	call %[bpf_get_prandom_u32];			\
682 	w1 = w0;					\
683 	if w1 s> -8 goto l0_%=;				\
684 	if w1 s< -10 goto l0_%=;			\
685 	w1 s%%= 3;					\
686 	if w1 s< -2 goto l1_%=;				\
687 	if w1 s> 0 goto l1_%=;				\
688 l0_%=:	r0 = 0;						\
689 	exit;						\
690 l1_%=:	r0 = *(u64 *)(r1 + 0);				\
691 	exit;						\
692 "	:
693 	: __imm(bpf_get_prandom_u32)
694 	: __clobber_all);
695 }
696 
697 SEC("socket")
698 __description("SMOD32, positive divisor, mixed sign dividend")
699 __success __retval(0) __log_level(2)
700 __msg("w1 s%= 3 {{.*}}; R1=scalar(smin=0,smax=umax=0xffffffff,smin32=-2,smax32=2,var_off=(0x0; 0xffffffff))")
701 __naked void smod32_pos_divisor_3(void)
702 {
703 	asm volatile ("					\
704 	call %[bpf_get_prandom_u32];			\
705 	w1 = w0;					\
706 	if w1 s< -8 goto l0_%=;				\
707 	if w1 s> 10 goto l0_%=;				\
708 	w1 s%%= 3;					\
709 	if w1 s< -2 goto l1_%=;				\
710 	if w1 s> 2 goto l1_%=;				\
711 l0_%=:	r0 = 0;						\
712 	exit;						\
713 l1_%=:	r0 = *(u64 *)(r1 + 0);				\
714 	exit;						\
715 "	:
716 	: __imm(bpf_get_prandom_u32)
717 	: __clobber_all);
718 }
719 
720 SEC("socket")
721 __description("SMOD32, positive divisor, small dividend")
722 __success __retval(0) __log_level(2)
723 __msg("w1 s%= 11 {{.*}}; R1=scalar(smin=0,smax=umax=0xffffffff,smin32=-8,smax32=10,var_off=(0x0; 0xffffffff))")
724 __naked void smod32_pos_divisor_unchanged(void)
725 {
726 	asm volatile ("					\
727 	call %[bpf_get_prandom_u32];			\
728 	w1 = w0;					\
729 	if w1 s< -8 goto l0_%=;				\
730 	if w1 s> 10 goto l0_%=;				\
731 	w1 s%%= 11;					\
732 	if w1 s< -8 goto l1_%=;				\
733 	if w1 s> 10 goto l1_%=;				\
734 l0_%=:	r0 = 0;						\
735 	exit;						\
736 l1_%=:	r0 = *(u64 *)(r1 + 0);				\
737 	exit;						\
738 "	:
739 	: __imm(bpf_get_prandom_u32)
740 	: __clobber_all);
741 }
742 
743 SEC("socket")
744 __description("SMOD32, negative divisor, positive dividend")
745 __success __retval(0) __log_level(2)
746 __msg("w1 s%= -3 {{.*}}; R1=scalar(smin=smin32=0,smax=umax=smax32=umax32=2,var_off=(0x0; 0x3))")
747 __naked void smod32_neg_divisor_1(void)
748 {
749 	asm volatile ("					\
750 	call %[bpf_get_prandom_u32];			\
751 	w1 = w0;					\
752 	if w1 s< 8 goto l0_%=;				\
753 	if w1 s> 10 goto l0_%=;				\
754 	w1 s%%= -3;					\
755 	if w1 s< 0 goto l1_%=;				\
756 	if w1 s> 2 goto l1_%=;				\
757 l0_%=:	r0 = 0;						\
758 	exit;						\
759 l1_%=:	r0 = *(u64 *)(r1 + 0);				\
760 	exit;						\
761 "	:
762 	: __imm(bpf_get_prandom_u32)
763 	: __clobber_all);
764 }
765 
766 SEC("socket")
767 __description("SMOD32, negative divisor, negative dividend")
768 __success __retval(0) __log_level(2)
769 __msg("w1 s%= -3 {{.*}}; R1=scalar(smin=0,smax=umax=0xffffffff,smin32=-2,smax32=0,var_off=(0x0; 0xffffffff))")
770 __naked void smod32_neg_divisor_2(void)
771 {
772 	asm volatile ("					\
773 	call %[bpf_get_prandom_u32];			\
774 	w1 = w0;					\
775 	if w1 s> -8 goto l0_%=;				\
776 	if w1 s< -10 goto l0_%=;			\
777 	w1 s%%= -3;					\
778 	if w1 s< -2 goto l1_%=;				\
779 	if w1 s> 0 goto l1_%=;				\
780 l0_%=:	r0 = 0;						\
781 	exit;						\
782 l1_%=:	r0 = *(u64 *)(r1 + 0);				\
783 	exit;						\
784 "	:
785 	: __imm(bpf_get_prandom_u32)
786 	: __clobber_all);
787 }
788 
789 SEC("socket")
790 __description("SMOD32, negative divisor, mixed sign dividend")
791 __success __retval(0) __log_level(2)
792 __msg("w1 s%= -3 {{.*}}; R1=scalar(smin=0,smax=umax=0xffffffff,smin32=-2,smax32=2,var_off=(0x0; 0xffffffff))")
793 __naked void smod32_neg_divisor_3(void)
794 {
795 	asm volatile ("					\
796 	call %[bpf_get_prandom_u32];			\
797 	w1 = w0;					\
798 	if w1 s< -8 goto l0_%=;				\
799 	if w1 s> 10 goto l0_%=;				\
800 	w1 s%%= -3;					\
801 	if w1 s< -2 goto l1_%=;				\
802 	if w1 s> 2 goto l1_%=;				\
803 l0_%=:	r0 = 0;						\
804 	exit;						\
805 l1_%=:	r0 = *(u64 *)(r1 + 0);				\
806 	exit;						\
807 "	:
808 	: __imm(bpf_get_prandom_u32)
809 	: __clobber_all);
810 }
811 
812 SEC("socket")
813 __description("SMOD32, negative divisor, small dividend")
814 __success __retval(0) __log_level(2)
815 __msg("w1 s%= -11 {{.*}}; R1=scalar(smin=0,smax=umax=0xffffffff,smin32=-8,smax32=10,var_off=(0x0; 0xffffffff))")
816 __naked void smod32_neg_divisor_unchanged(void)
817 {
818 	asm volatile ("					\
819 	call %[bpf_get_prandom_u32];			\
820 	w1 = w0;					\
821 	if w1 s< -8 goto l0_%=;				\
822 	if w1 s> 10 goto l0_%=;				\
823 	w1 s%%= -11;					\
824 	if w1 s< -8 goto l1_%=;				\
825 	if w1 s> 10 goto l1_%=;				\
826 l0_%=:	r0 = 0;						\
827 	exit;						\
828 l1_%=:	r0 = *(u64 *)(r1 + 0);				\
829 	exit;						\
830 "	:
831 	: __imm(bpf_get_prandom_u32)
832 	: __clobber_all);
833 }
834 
835 SEC("socket")
836 __description("SMOD32, zero divisor")
837 __success __retval(0) __log_level(2)
838 __msg("w1 s%= w2 {{.*}}; R1=scalar(smin=0,smax=umax=0xffffffff,smin32=-8,smax32=10,var_off=(0x0; 0xffffffff))")
839 __naked void smod32_zero_divisor(void)
840 {
841 	asm volatile ("					\
842 	call %[bpf_get_prandom_u32];			\
843 	w1 = w0;					\
844 	if w1 s< -8 goto l0_%=;				\
845 	if w1 s> 10 goto l0_%=;				\
846 	w2 = 0;						\
847 	w1 s%%= w2;					\
848 	if w1 s< -8 goto l1_%=;				\
849 	if w1 s> 10 goto l1_%=;				\
850 l0_%=:	r0 = 0;						\
851 	exit;						\
852 l1_%=:	r0 = *(u64 *)(r1 + 0);				\
853 	exit;						\
854 "	:
855 	: __imm(bpf_get_prandom_u32)
856 	: __clobber_all);
857 }
858 
859 SEC("socket")
860 __description("SMOD32, overflow (S32_MIN%-1)")
861 __success __retval(0) __log_level(2)
862 __msg("w1 s%= -1 {{.*}}; R1=0")
863 __naked void smod32_overflow_1(void)
864 {
865 	asm volatile ("					\
866 	call %[bpf_get_prandom_u32];			\
867 	w1 = w0;					\
868 	w2 = %[int_min];				\
869 	w2 += 10;					\
870 	if w1 s> w2 goto l0_%=;				\
871 	w1 s%%= -1;					\
872 	if w1 != 0 goto l1_%=;				\
873 l0_%=:	r0 = 0;						\
874 	exit;						\
875 l1_%=:	r0 = *(u64 *)(r1 + 0);				\
876 	exit;						\
877 "	:
878 	: __imm_const(int_min, INT_MIN),
879 	  __imm(bpf_get_prandom_u32)
880 	: __clobber_all);
881 }
882 
883 SEC("socket")
884 __description("SMOD32, overflow (S32_MIN%-1), constant dividend")
885 __success __retval(0) __log_level(2)
886 __msg("w1 s%= -1 {{.*}}; R1=0")
887 __naked void smod32_overflow_2(void)
888 {
889 	asm volatile ("					\
890 	w1 = %[int_min];				\
891 	w1 s%%= -1;					\
892 	if w1 != 0 goto l0_%=;				\
893 	r0 = 0;						\
894 	exit;						\
895 l0_%=:	r0 = *(u64 *)(r1 + 0);				\
896 	exit;						\
897 "	:
898 	: __imm_const(int_min, INT_MIN)
899 	: __clobber_all);
900 }
901 
902 SEC("socket")
903 __description("SMOD64, positive divisor, positive dividend")
904 __success __retval(0) __log_level(2)
905 __msg("r1 s%= 3 {{.*}}; R1=scalar(smin=smin32=0,smax=umax=smax32=umax32=2,var_off=(0x0; 0x3))")
906 __naked void smod64_pos_divisor_1(void)
907 {
908 	asm volatile ("					\
909 	call %[bpf_get_prandom_u32];			\
910 	r1 = r0;					\
911 	if r1 s< 8 goto l0_%=;				\
912 	if r1 s> 10 goto l0_%=;				\
913 	r1 s%%= 3;					\
914 	if r1 s< 0 goto l1_%=;				\
915 	if r1 s> 2 goto l1_%=;				\
916 l0_%=:	r0 = 0;						\
917 	exit;						\
918 l1_%=:	r0 = *(u64 *)(r1 + 0);				\
919 	exit;						\
920 "	:
921 	: __imm(bpf_get_prandom_u32)
922 	: __clobber_all);
923 }
924 
925 SEC("socket")
926 __description("SMOD64, positive divisor, negative dividend")
927 __success __retval(0) __log_level(2)
928 __msg("r1 s%= 3 {{.*}}; R1=scalar(smin=smin32=-2,smax=smax32=0)")
929 __naked void smod64_pos_divisor_2(void)
930 {
931 	asm volatile ("					\
932 	call %[bpf_get_prandom_u32];			\
933 	r1 = r0;					\
934 	if r1 s> -8 goto l0_%=;				\
935 	if r1 s< -10 goto l0_%=;			\
936 	r1 s%%= 3;					\
937 	if r1 s< -2 goto l1_%=;				\
938 	if r1 s> 0 goto l1_%=;				\
939 l0_%=:	r0 = 0;						\
940 	exit;						\
941 l1_%=:	r0 = *(u64 *)(r1 + 0);				\
942 	exit;						\
943 "	:
944 	: __imm(bpf_get_prandom_u32)
945 	: __clobber_all);
946 }
947 
948 SEC("socket")
949 __description("SMOD64, positive divisor, mixed sign dividend")
950 __success __retval(0) __log_level(2)
951 __msg("r1 s%= 3 {{.*}}; R1=scalar(smin=smin32=-2,smax=smax32=2)")
952 __naked void smod64_pos_divisor_3(void)
953 {
954 	asm volatile ("					\
955 	call %[bpf_get_prandom_u32];			\
956 	r1 = r0;					\
957 	if r1 s< -8 goto l0_%=;				\
958 	if r1 s> 10 goto l0_%=;				\
959 	r1 s%%= 3;					\
960 	if r1 s< -2 goto l1_%=;				\
961 	if r1 s> 2 goto l1_%=;				\
962 l0_%=:	r0 = 0;						\
963 	exit;						\
964 l1_%=:	r0 = *(u64 *)(r1 + 0);				\
965 	exit;						\
966 "	:
967 	: __imm(bpf_get_prandom_u32)
968 	: __clobber_all);
969 }
970 
971 SEC("socket")
972 __description("SMOD64, positive divisor, small dividend")
973 __success __retval(0) __log_level(2)
974 __msg("r1 s%= 11 {{.*}}; R1=scalar(smin=smin32=-8,smax=smax32=10)")
975 __naked void smod64_pos_divisor_unchanged(void)
976 {
977 	asm volatile ("					\
978 	call %[bpf_get_prandom_u32];			\
979 	r1 = r0;					\
980 	if r1 s< -8 goto l0_%=;				\
981 	if r1 s> 10 goto l0_%=;				\
982 	r1 s%%= 11;					\
983 	if r1 s< -8 goto l1_%=;				\
984 	if r1 s> 10 goto l1_%=;				\
985 l0_%=:	r0 = 0;						\
986 	exit;						\
987 l1_%=:	r0 = *(u64 *)(r1 + 0);				\
988 	exit;						\
989 "	:
990 	: __imm(bpf_get_prandom_u32)
991 	: __clobber_all);
992 }
993 
994 SEC("socket")
995 __description("SMOD64, negative divisor, positive dividend")
996 __success __retval(0) __log_level(2)
997 __msg("r1 s%= -3 {{.*}}; R1=scalar(smin=smin32=0,smax=umax=smax32=umax32=2,var_off=(0x0; 0x3))")
998 __naked void smod64_neg_divisor_1(void)
999 {
1000 	asm volatile ("					\
1001 	call %[bpf_get_prandom_u32];			\
1002 	r1 = r0;					\
1003 	if r1 s< 8 goto l0_%=;				\
1004 	if r1 s> 10 goto l0_%=;				\
1005 	r1 s%%= -3;					\
1006 	if r1 s< 0 goto l1_%=;				\
1007 	if r1 s> 2 goto l1_%=;				\
1008 l0_%=:	r0 = 0;						\
1009 	exit;						\
1010 l1_%=:	r0 = *(u64 *)(r1 + 0);				\
1011 	exit;						\
1012 "	:
1013 	: __imm(bpf_get_prandom_u32)
1014 	: __clobber_all);
1015 }
1016 
1017 SEC("socket")
1018 __description("SMOD64, negative divisor, negative dividend")
1019 __success __retval(0) __log_level(2)
1020 __msg("r1 s%= -3 {{.*}}; R1=scalar(smin=smin32=-2,smax=smax32=0)")
1021 __naked void smod64_neg_divisor_2(void)
1022 {
1023 	asm volatile ("					\
1024 	call %[bpf_get_prandom_u32];			\
1025 	r1 = r0;					\
1026 	if r1 s> -8 goto l0_%=;				\
1027 	if r1 s< -10 goto l0_%=;			\
1028 	r1 s%%= -3;					\
1029 	if r1 s< -2 goto l1_%=;				\
1030 	if r1 s> 0 goto l1_%=;				\
1031 l0_%=:	r0 = 0;						\
1032 	exit;						\
1033 l1_%=:	r0 = *(u64 *)(r1 + 0);				\
1034 	exit;						\
1035 "	:
1036 	: __imm(bpf_get_prandom_u32)
1037 	: __clobber_all);
1038 }
1039 
1040 SEC("socket")
1041 __description("SMOD64, negative divisor, mixed sign dividend")
1042 __success __retval(0) __log_level(2)
1043 __msg("r1 s%= -3 {{.*}}; R1=scalar(smin=smin32=-2,smax=smax32=2)")
1044 __naked void smod64_neg_divisor_3(void)
1045 {
1046 	asm volatile ("					\
1047 	call %[bpf_get_prandom_u32];			\
1048 	r1 = r0;					\
1049 	if r1 s< -8 goto l0_%=;				\
1050 	if r1 s> 10 goto l0_%=;				\
1051 	r1 s%%= -3;					\
1052 	if r1 s< -2 goto l1_%=;				\
1053 	if r1 s> 2 goto l1_%=;				\
1054 l0_%=:	r0 = 0;						\
1055 	exit;						\
1056 l1_%=:	r0 = *(u64 *)(r1 + 0);				\
1057 	exit;						\
1058 "	:
1059 	: __imm(bpf_get_prandom_u32)
1060 	: __clobber_all);
1061 }
1062 
1063 SEC("socket")
1064 __description("SMOD64, negative divisor, small dividend")
1065 __success __retval(0) __log_level(2)
1066 __msg("r1 s%= -11 {{.*}}; R1=scalar(smin=smin32=-8,smax=smax32=10)")
1067 __naked void smod64_neg_divisor_unchanged(void)
1068 {
1069 	asm volatile ("					\
1070 	call %[bpf_get_prandom_u32];			\
1071 	r1 = r0;					\
1072 	if r1 s< -8 goto l0_%=;				\
1073 	if r1 s> 10 goto l0_%=;				\
1074 	r1 s%%= -11;					\
1075 	if r1 s< -8 goto l1_%=;				\
1076 	if r1 s> 10 goto l1_%=;				\
1077 l0_%=:	r0 = 0;						\
1078 	exit;						\
1079 l1_%=:	r0 = *(u64 *)(r1 + 0);				\
1080 	exit;						\
1081 "	:
1082 	: __imm(bpf_get_prandom_u32)
1083 	: __clobber_all);
1084 }
1085 
1086 SEC("socket")
1087 __description("SMOD64, zero divisor")
1088 __success __retval(0) __log_level(2)
1089 __msg("r1 s%= r2 {{.*}}; R1=scalar(smin=smin32=-8,smax=smax32=10)")
1090 __naked void smod64_zero_divisor(void)
1091 {
1092 	asm volatile ("					\
1093 	call %[bpf_get_prandom_u32];			\
1094 	r1 = r0;					\
1095 	if r1 s< -8 goto l0_%=;				\
1096 	if r1 s> 10 goto l0_%=;				\
1097 	r2 = 0;						\
1098 	r1 s%%= r2;					\
1099 	if r1 s< -8 goto l1_%=;				\
1100 	if r1 s> 10 goto l1_%=;				\
1101 l0_%=:	r0 = 0;						\
1102 	exit;						\
1103 l1_%=:	r0 = *(u64 *)(r1 + 0);				\
1104 	exit;						\
1105 "	:
1106 	: __imm(bpf_get_prandom_u32)
1107 	: __clobber_all);
1108 }
1109 
1110 SEC("socket")
1111 __description("SMOD64, overflow (S64_MIN%-1)")
1112 __success __retval(0) __log_level(2)
1113 __msg("r1 s%= -1 {{.*}}; R1=0")
1114 __naked void smod64_overflow_1(void)
1115 {
1116 	asm volatile ("					\
1117 	call %[bpf_ktime_get_ns];			\
1118 	r1 = r0;					\
1119 	r2 = %[llong_min] ll;				\
1120 	r2 += 10;					\
1121 	if r1 s> r2 goto l0_%=;				\
1122 	r1 s%%= -1;					\
1123 	if r1 != 0 goto l1_%=;				\
1124 l0_%=:	r0 = 0;						\
1125 	exit;						\
1126 l1_%=:	r0 = *(u64 *)(r1 + 0);				\
1127 	exit;						\
1128 "	:
1129 	: __imm_const(llong_min, LLONG_MIN),
1130 	  __imm(bpf_ktime_get_ns)
1131 	: __clobber_all);
1132 }
1133 
1134 SEC("socket")
1135 __description("SMOD64, overflow (S64_MIN%-1), constant dividend")
1136 __success __retval(0) __log_level(2)
1137 __msg("r1 s%= -1 {{.*}}; R1=0")
1138 __naked void smod64_overflow_2(void)
1139 {
1140 	asm volatile ("					\
1141 	r1 = %[llong_min] ll;				\
1142 	r1 s%%= -1;					\
1143 	if r1 != 0 goto l0_%=;				\
1144 	r0 = 0;						\
1145 	exit;						\
1146 l0_%=:	r0 = *(u64 *)(r1 + 0);				\
1147 	exit;						\
1148 "	:
1149 	: __imm_const(llong_min, LLONG_MIN)
1150 	: __clobber_all);
1151 }
1152