bpf: Finish the insn in the state that maybe_fork_scalars() splits off

When a register is -1 or 0, maybe_fork_scalars() splits the state in two
before an 'and' or an 'or' with a constant. The result is more accurate for
each value alone. The verifier continues with -1. It pushes a copy of the
state with 0 and verifies the copy later, from the same insn.

           today                              this patch

  N:   r1 &= 8    r1 is -1 or 0      N:   r1 &= 8    r1 is -1 or 0
        /     \                            /     \
    r1 = -1   r1 = 0                   r1 = -1   r1 = 0
    r1 &= 8   push to N                r1 &= 8   r1 &= 8
       |                                  |      push to N+1
  N+1: ...                           N+1: ...

At insn N the copy is a part of the state that it came from: 0 is in
[-1, 0]. If pruning compares the two states, it drops the copy, and no one
verifies the case r1 = 0.

The first state has branches that are not explored. Usually pruning does
not use such states. In a loop that scalar evolution counted it does, and
the head of such a loop always keeps its state. Thus a fork at the head of
a counted loop loses the case r1 = 0:

     r9 = a map value of 8 bytes
     r6 = -1
  1: r6 &= 8                  r6 is -1 or 0, only -1 is verified: 8
     r6 ^= 8                  0. It is 8 when r6 was 0.
     r1 = r9
     r1 += r6
     r0 = *(u8 *)(r1 + 0)
     r6 = -1 or 0
     r7 += 1
     if r7 < 100 goto 1b

  from 11 to 11: safe

The verifier accepts this prog. The prog reads the byte that follows the
map value. With a constant of 64 Tbyte in a register it reads an address
that is not mapped, and the kernel crashes.

Do the insn in the copy too, and push the copy to the next insn. All other
code that pushes a state does the same.

No verdict changes in selftests, Cilium and scx. Each fork processes one
insn less, and the sequence in which the verifier explores states changes
slightly. 62 of 161 progs of Cilium process a different number of insns,
from -0.7% to +3.3%. The total is 986970 -> 987013. 2 of 563 progs of scx
process one insn less.

Fixes: 6ccf49f79327 ("bpf: Use SCEV to widen bounded loops")
Signed-off-by: Alexei Starovoitov <ast@kernel.org>
Link: https://patch.msgid.link/20261027190314.1440199-17-alexei.starovoitov@gmail.com

0 files changed, 0 insertions, 0 deletions