Understanding the ebpf-verifier output

[amurgZainar]

Hello,

I'm trying to understand better the output of the verifier:

1:2: Code is unreachable after 1:2
12:15: Code is unreachable after 12:15
14:15: Code is unreachable after 14:15
64:77: Upper bound must be at most 28 (valid_access(r9.offset+30, width=2) for read)
313:363: Upper bound must be at most 28 (valid_access(r9.offset+28, width=2) for read)

1:2: Code is unreachable after 1:2
12:15: Code is unreachable after 12:15
14:15: Code is unreachable after 14:15

1,1.25919
Program terminates within 2100 instructions

From this line 1,1.25919, I understand that the verification process is successful, but I'm trying to understand whether the rest of the logs are benign or not and whether they should be ignored or not.

For example, I remember that output like the one below (probably on older versions of Prevail) was causing the verifier to fail to terminate successfully, but now, it seems that the verification is successful even though these logs still appear:

64:77: Upper bound must be at most 28 (valid_access(r9.offset+30, width=2) for read)
313:363: Upper bound must be at most 28 (valid_access(r9.offset+28, width=2) for read)

, while the logs like the one below were causing the verifier to succeed, even though it was shown in the output:

1:2: Code is unreachable after 1:2

Also, what do these numbers represent 64:77: . Do they represent the the line number that's triggering the log in the source code or in the assembly code?

Finally, I'm wondering if there are methods that would allow me to debug the cause of these logs further.

Sorry to the long discussion. I'm still learning about eBPF, please have merci :)!

Thanks!

[amurgZainar]

OK, so from the O'Reilly eBPF book I understand that the 64:77 to instruction 64 in the eBPF bytecode of the resulted source code of the eBPF program. It's still unclear the reason of this verifier log though 64:77: Upper bound must be at most 28 (valid_access(r9.offset+30, width=2) for read).