On Fri, 2024-05-24 at 20:11 -0700, Alexei Starovoitov wrote:
> From: Alexei Starovoitov <ast@xxxxxxxxxx>
[...]
> With that the get_loop_entry() can be used to gate is_branch_taken() logic.
> When the verifier sees 'r1 > 1000' inside the loop and it can predict it
> instead of marking r1 as precise it widens both branches, so r1 becomes
> [0, 1000] in fallthrough and [1001, UMAX] in other_branch.
>
> Consider the loop:
> bpf_for_each(...) {
> if (r1 > 1000)
> break;
>
> arr[r1] = ..;
> }
> At arr[r1] access the r1 is bounded and the loop can quickly converge.
>
> Unfortunately compilers (both GCC and LLVM) often optimize loop exit
> condition to equality, so
> for (i = 0; i < 100; i++) arr[i] = 1
> becomes
> for (i = 0; i != 100; i++) arr[1] = 1
>
> Hence treat != and == conditions specially in the verifier.
> Widen only not-predicted branch and keep predict branch as is. Example:
> r1 = 0
> goto L1
> L2:
> arr[r1] = 1
> r1++
> L1:
> if r1 != 100 goto L2
> fallthrough: r1=100 after widening
> other_branch: r1 stays as-is (0, 1, 2, ..)
[...]
I'm not sure how much of a deal-breaker this is, but proposed
heuristics precludes verification for the following program:
char arr[10];
SEC("socket")
__success __flag(BPF_F_TEST_STATE_FREQ)
int simple_loop(const void *ctx)
{
struct bpf_iter_num it;
int *v, sum = 0, i = 0;
bpf_iter_num_new(&it, 0, 10);
while ((v = bpf_iter_num_next(&it))) {
if (i < 5)
sum += arr[i++];
}
bpf_iter_num_destroy(&it);
return sum;
}
The presence of the loop with bpf_iter_num creates a set of states
with non-null loop_header, which in turn switches-off predictions for
comparison operations inside the loop.
This looks like a bad a compose-ability of verifier features to me.
--
Instead of heuristics, maybe rely on hints from the programmer?
E.g. add a kfunc `u64 bpf_widen(u64)` which will be compiled as an
identity function, but would instruct verifier to drop precision for a
specific value. When work on no_caller_saved_registers finishes this
even could be available w/o runtime cost.
(And at the moment could be emulated by something like `rX /= 1`).
