relative jumps handling

[etsal]

Is it possible to have relative jumps (goto pc+0xXX) highlight the instruction they point to?

[theihor]

I am not sure what you'd like to be highlighted.

In the verifier log the next instruction immediately after goto is the one that was jumped to in the given verification path. For example:

2827: (15) if r6 == 0x0 goto pc+43    ; R6_w=scalar(id=5800,umin=1)
2828: (b7) r1 = 0                     ; R1_w=0

This means the goto didn't happen (so r6 != 0).

2984: (e5) may_goto pc+3
; btn = (bt_node *)btn->values[ind]; @ btree.bpf.c:151
2988: (67) r4 <<= 3                   ; frame1: R4_w=32

And here the jump did happen: note pc changing from 2984 to 2988 (that is pc+3).

So do you mean highlighting the next instruction? Or maybe every log line with the target PC (in the example: every instance of the instruction at line 2988)?

[etsal]

I was thinking the latter, highlighting every log line with the target PC. That would help follow the branching logic a bit more easily.

[etsal]

I've been thinking a bit about this, and maybe the better option would be to have a step mode similar to that of a debugger to see the paths taken by the verifier. We already have the lines corresponding to the BPF asm instructions in the log, so if there was an option to upload the source file and highlight the line being verified we would more easily see how the verifier goes through the program without having to manually cross-reference. Also, a "next" button to go through the verifier log one instruction at a time would let us step through the log more easily.

[theihor]

I've been thinking a bit about this, and maybe the better option would be to have a step mode similar to that of a debugger to see the paths taken by the verifier. We already have the lines corresponding to the BPF asm instructions in the log, so if there was an option to upload the source file and highlight the line being verified we would more easily see how the verifier goes through the program without having to manually cross-reference. Also, a "next" button to go through the verifier log one instruction at a time would let us step through the log more easily.

Allowing user to paste the C source sounds like a great idea, since the snippents within the log are incomplete, and also we can't indent the re-constructed C properly (but the user-pasted code will be formatted).
Matching the instructions to that code is a challenge however. If we rely on file.c:123 annotations, then pasted code needs to be exactly the same. We could try matching code strings, but that still is no guarantee. Also, multiple files might be referenced...

As for "next" button, right now you can use arrows to navigate, but it will go through ignorable lines too. It's easy to change the meaning of up/down arrows to "next instruction line", is that what you have in mind?

[etsal]

I've been thinking a bit about this, and maybe the better option would be to have a step mode similar to that of a debugger to see the paths taken by the verifier. We already have the lines corresponding to the BPF asm instructions in the log, so if there was an option to upload the source file and highlight the line being verified we would more easily see how the verifier goes through the program without having to manually cross-reference. Also, a "next" button to go through the verifier log one instruction at a time would let us step through the log more easily.

Allowing user to paste the C source sounds like a great idea, since the snippents within the log are incomplete, and also we can't indent the re-constructed C properly (but the user-pasted code will be formatted). Matching the instructions to that code is a challenge however. If we rely on file.c:123 annotations, then pasted code needs to be exactly the same. We could try matching code strings, but that still is no guarantee. Also, multiple files might be referenced...

Wrt matching C file lines in the verifier output to an uploaded C file: Would it not be a reasonable assumption? If someone is uploading a verifier error to bpfvv they are probably live debugging their code, so they have the source code at hand. It's similar to passing the source code to a debugger in my view. Of course, this may only match my own workflow.

For multiple files it would for sure be harder, but the tool can just try to match the verifier with the source only for the uploaded file, and ignore lines from other files. That would still be very useful.

As for "next" button, right now you can use arrows to navigate, but it will go through ignorable lines too. It's easy to change the meaning of up/down arrows to "next instruction line", is that what you have in mind?

Exactly! Maybe adding a radio button that switches between stepping one BPF instruction at a time and stepping one C line at a time would be the best of both worlds.

[jordalgo]

Exactly! Maybe adding a radio button that switches between stepping one BPF instruction at a time and stepping one C line at a time would be the best of both worlds.

I think if we add a c source line view then perhaps the up/down arrows should just, by default, navigate to the next BPF instruction (passing over ignored lines like c source lines) when the main log line panel is in focus. Then users can click on the c-source-line view and navigate there separately.

[etsal]

Exactly! Maybe adding a radio button that switches between stepping one BPF instruction at a time and stepping one C line at a time would be the best of both worlds.

I think if we add a c source line view then perhaps the up/down arrows should just, by default, navigate to the next BPF instruction (passing over ignored lines like c source lines) when the main log line panel is in focus. Then users can click on the c-source-line view and navigate there separately.

That makes sense, as long as there is also a way to step into which C lines the verifier goes through in sequence.