On Wed, May 22, 2024 at 2:09 PM Alexei Starovoitov
<alexei.starovoitov@xxxxxxxxx> wrote:
>
> On Wed, May 22, 2024 at 10:33 AM Andrii Nakryiko
> <andrii.nakryiko@xxxxxxxxx> wrote:
> >
> > On Tue, May 21, 2024 at 7:47 PM Alexei Starovoitov
> > <alexei.starovoitov@xxxxxxxxx> wrote:
> > >
> > > From: Alexei Starovoitov <ast@xxxxxxxxxx>
> > >
> > > Motivation for the patch
> > > ------------------------
> > > Open coded iterators and may_goto is a great mechanism to implement loops,
> > > but counted loops are problematic. For example:
> > > for (i = 0; i < 100 && can_loop; i++)
> > > is verified as a bounded loop, since i < 100 condition forces the verifier
> > > to mark 'i' as precise and loop states at different iterations are not equivalent.
> > > That removes the benefit of open coded iterators and may_goto.
> > > The workaround is to do:
> > > int zero = 0; /* global or volatile variable */
> > > for (i = zero; i < 100 && can_loop; i++)
> > > to hide from the verifier the value of 'i'.
> > > It's unnatural and so far users didn't learn such odd programming pattern.
> > >
> > > This patch aims to improve the verifier to support
> > > for (i = 0; i < 100000 && can_loop; i++)
> > > as open coded iter loop (when 'i' doesn't need to be precise).
> > >
> > > Algorithm
> > > ---------
> > > First of all:
> > > if (is_may_goto_insn_at(env, insn_idx)) {
> > > + update_loop_entry(cur, &sl->state);
> > > if (states_equal(env, &sl->state, cur, RANGE_WITHIN)) {
> > > - update_loop_entry(cur, &sl->state);
> > >
> > > This should be correct, since reaching the same insn should
> > > satisfy "if h1 in path" requirement of update_loop_entry() algorithm.
> > > It's too conservative to update loop_entry only on a state match.
> > >
> > > With that the get_loop_entry() can be used to gate is_branch_taken() logic.
> > > When 'if (i < 1000)' is done within open coded iterator or in a loop with may_goto
> > > don't invoke is_branch_taken() logic.
> > > When it's skipped don't do reg_bounds_sanity_check(), since it will surely
> > > see range violations.
> > >
> > > Now, consider progs/iters_task_vma.c that has the following logic:
> > > bpf_for_each(...) {
> > > if (i > 1000)
> >
> > I'm wondering, maybe we should change rules around handling inequality
> > (>, >=, <, <=) comparisons for register(s) that have a constant value
> > (or maybe actually any value).
> >
> > My reasoning is the following. When we have something like this `if (i
> > > 1000)` condition, that means that for fallthrough branch whether i
> > is 0, or 1, or 2, or whatever doesn't really matter, because the code
> > presumably works for any value in [0, 999] range, right? So maybe in
> > addition to marking it precise and keeping i's range estimate the
> > same, we should extend this range according to inequality condition?
> >
> > That is, even if we know on first iteration that i is 0 (!precise),
> > when we simulate this conditional jump instruction, adjust i's range
> > to be [0, 999] (precise) in the fallthrough branch, and [1000,
> > U64_MAX] in the true branch?
> >
> > I.e., make conditional jumps into "range widening" instructions?
> >
> > Have you thought about this approach? Do you think it will work in
> > practice? I'm sure it can't be as simple, but still, worth
> > considering. Curious also to hear Eduard's opinion as well, he's dealt
> > with this a lot in the past.
>
> I looked into doing exactly that [0, 999] and [1000, max],
> then on the next iteration i+=1 insn will adjust it to
> [1, 1000], but the next i < 1000 will widen it back to
> [0, 999] and the state equivalence will be happy.
> But my excitement was short lived, since both gcc and llvm
> optimize the loop exit condition to !=
> and they do it in the middle end.
> Backends cannot influence this optimization.
> I don't think it's practical to undo it in the backend.
> So most of the loops written as:
> for (i = 0; i < 1000; i++)
> are compiled as
> for (i = 0; i != 1000; i++)
> for x86, arm, bpf, etc.
>
> so if there is arr[i] inside the loop the verifier
> have to rely on bounded loop logic and check i=0, 1, 2, ... 999
> one by one, since nothing else inside the loop
> makes the array index bounded.
So I've decided to implement this idea anyway to see whether
it can be salvaged for some cases.
It turned out that it's not that bad. With extra heuristic
it's almost working. Stay tuned.
