Re: [PATCH v4 bpf-next 2/4] bpf: Recognize that two registers are safe when their ranges match

[Eduard Zingerman <eddyz87@gmail.com>]

On Fri, 2024-03-01 at 18:00 -0800, Alexei Starovoitov wrote:
> From: Alexei Starovoitov <ast@kernel.org>
> 
> When open code iterators, bpf_loop or may_goto is used the following two states
> are equivalent and safe to prune the search:
> 
> cur state: fp-8_w=scalar(id=3,smin=umin=smin32=umin32=2,smax=umax=smax32=umax32=11,var_off=(0x0; 0xf))
> old state: fp-8_rw=scalar(id=2,smin=umin=smin32=umin32=1,smax=umax=smax32=umax32=11,var_off=(0x0; 0xf))
> 
> In other words "exact" state match should ignore liveness and precision marks,
> since open coded iterator logic didn't complete their propagation,
> but range_within logic that applies to scalars, ptr_to_mem, map_value, pkt_ptr
> is safe to rely on.
>
> Avoid doing such comparison when regular infinite loop detection logic is used,
> otherwise bounded loop logic will declare such "infinite loop" as false
> positive. Such example is in progs/verifier_loops1.c not_an_inifinite_loop().
>
> Signed-off-by: Alexei Starovoitov <ast@kernel.org>

I think this makes sense, don't see counter-examples at the moment.
One nit below.

Also, I'm curious if there is veristat results impact,
could be huge for some cases with bpf_loop().

[...]

> @@ -17257,7 +17263,7 @@ static int is_state_visited(struct bpf_verifier_env *env, int insn_idx)
>  		 */
>  		loop_entry = get_loop_entry(&sl->state);
>  		force_exact = loop_entry && loop_entry->branches > 0;
> -		if (states_equal(env, &sl->state, cur, force_exact)) {
> +		if (states_equal(env, &sl->state, cur, force_exact ? EXACT : NOT_EXACT)) {

Logically this checks same condition as checks for calls_callback() or
is_iter_next_insn() above: whether current state is equivalent to some
old state, where old state had not been tracked to 'exit' for each
possible path yet.
Thus, 'exact' flags used in these checks should be the same:
"force_exact ? RANGE_WITHIN : NOT_EXACT".

>  			if (force_exact)
>  				update_loop_entry(cur, loop_entry);
>  hit: