On Mon, 2024-10-21 at 19:18 -0700, Alexei Starovoitov wrote:
[...]
> > 0: r7 = *(u16 *)(r1 +0);"
> > 1: r7 += 0x1ab064b9;"
> > 2: if r7 & 0x702000 goto 1b;
> > 3: r7 &= 0x1ee60e;"
> > 4: r7 += r1;"
> > 5: if r7 s> 0x37d2 goto +0;"
> > 6: r0 = 0;"
> > 7: exit;"
[...]
> > And observe verification log:
> >
> > ...
> > is_state_visited: new checkpoint at 5, resetting env->jmps_processed
> > 5: R1=ctx() R7=ctx(...)
> > 5: (65) if r7 s> 0x37d2 goto pc+0 ; R7=ctx(...)
> > 6: (b7) r0 = 0 ; R0_w=0
> > 7: (95) exit
> >
> > from 5 to 6: R1=ctx() R7=ctx(...) R10=fp0
> > 6: R1=ctx() R7=ctx(...) R10=fp0
> > 6: (b7) r0 = 0 ; R0_w=0
> > 7: (95) exit
> > is_state_visited: suppressing checkpoint at 1, 3 jmps processed, cur->jmp_history_cnt is 74
> >
> > from 2 to 1: R1=ctx() R7_w=scalar(...) R10=fp0
> > 1: R1=ctx() R7_w=scalar(...) R10=fp0
> > 1: (07) r7 += 447767737
> > is_state_visited: suppressing checkpoint at 2, 3 jmps processed, cur->jmp_history_cnt is 75
> > 2: R7_w=scalar(...)
> > 2: (45) if r7 & 0x702000 goto pc-2
> > ... mark_precise 152 steps for r7 ...
> > 2: R7_w=scalar(...)
> > is_state_visited: suppressing checkpoint at 1, 4 jmps processed, cur->jmp_history_cnt is 75
> > 1: (07) r7 += 447767737
> > is_state_visited: suppressing checkpoint at 2, 4 jmps processed, cur->jmp_history_cnt is 76
> > 2: R7_w=scalar(...)
> > 2: (45) if r7 & 0x702000 goto pc-2
> > ...
> > BPF program is too large. Processed 257 insn
> >
> > The log output shows that checkpoint at label (1) is never created,
> > because it is suppressed by `skip_inf_loop_check` logic:
> > a. When 'if' at (2) is processed it pushes a state with insn_idx (1)
> > onto stack and proceeds to (3);
> > b. At (5) checkpoint is created, and this resets
> > env->{jmps,insns}_processed.
> > c. Verification proceeds and reaches `exit`;
> > d. State saved at step (a) is popped from stack and is_state_visited()
> > considers if checkpoint needs to be added, but because
> > env->{jmps,insns}_processed had been just reset at step (b)
> > the `skip_inf_loop_check` logic forces `add_new_state` to false.
> > e. Verifier proceeds with current state, which slowly accumulates
> > more and more entries in the jump history.
>
> I'm still not sure why it grew to thousands of entries in jmp_history.
> Looking at the above trace jmps_processed grows 1 to 1 with jmp_history_cnt.
> Also cur->jmp_history_cnt is reset to zero at the same time as
> jmps processed.
> So in the above test 75 vs 4 difference came from jmp_history
> entries that were there before the loop ?
0: r7 = *(u16 *)(r1 +0);"
1: r7 += 0x1ab064b9;"
2: if r7 & 0x702000 goto 1b;
3: r7 &= 0x1ee60e;"
4: r7 += r1;"
5: if r7 s> 0x37d2 goto +0;"
6: r0 = 0;"
7: exit;"
- When 'if' at (2) is processed current state is copied (let's call
this copy C), copy is put to the stack for later processing,
it's jump history is not cleared.
- Then current state proceeds verifying 3-5-6-7. At (5) checkpoint is
created and env->{jmps,insns}_processed are reset.
- Then state C is popped from the stack, it goes back to (1) and then (2),
at (2) a copy C1 is created but no checkpoint, as env->{jmps,insns}_processed
do not meet thresholds. C1's jmp_history is one entry longer then C's.
- Whole thing repeats until ENOMEM.
