Re: [PATCH v3 bpf-next 1/2] bpf: Relax precision marking in open coded iters and may_goto loop.

[Eduard Zingerman <eddyz87@gmail.com>]

On Fri, 2024-05-24 at 20:11 -0700, Alexei Starovoitov wrote:
> From: Alexei Starovoitov <ast@kernel.org>

[...]

> 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`).