On Sun, Mar 3, 2024 at 6:12 AM Eduard Zingerman <eddyz87@xxxxxxxxx> wrote:
>
> On Fri, 2024-03-01 at 18:00 -0800, Alexei Starovoitov wrote:
> > From: Alexei Starovoitov <ast@xxxxxxxxxx>
> >
> > 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@xxxxxxxxxx>
>
> 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().
No doubt, there will be improvements here and there. For iters.bpf.o:
Insns (A) Insns (B) Insns (DIFF) States (A) States (B) States
(DIFF) Program
--------- --------- ------------- ---------- ----------
------------- -------------------------------
858 823 -35 (-4.08%) 81 79 -2
(-2.47%) iter_nested_iters
137 110 -27 (-19.71%) 12 10 -2
(-16.67%) iter_obfuscate_counter
1161 1109 -52 (-4.48%) 92 88 -4
(-4.35%) iter_subprog_iters
62 35 -27 (-43.55%) 5 3 -2
(-40.00%) triple_continue
the rest in this file didn't change. No change for pyperf either.
> [...]
>
> > @@ -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".
Good point. Will change. It should help as well.
