On Thu, Jun 6, 2024 at 4:39 PM Eduard Zingerman <eddyz87@xxxxxxxxx> wrote:
>
> On Thu, 2024-06-06 at 15:19 -0700, Eduard Zingerman wrote:
>
> [...]
>
> > For the following C code:
> >
> > long arr1[1024];
> >
> > SEC("socket")
> > __success
> > int test1(const void *ctx)
> > {
> > long i;
> >
> > for (i = 0; i < 1024 && can_loop; i++)
> > arr1[i] = i;
> > return 0;
> > }
> >
> > clang generates the following BPF code:
> >
> > 0000000000000340 <test1>:
> > 104: r1 = 0x0
> > 105: r2 = 0x0 ll
> >
> > 0000000000000358 <LBB28_1>:
> > 107: may_goto +0x4 <LBB28_3>
> > 108: *(u64 *)(r2 + 0x0) = r1
> > 109: r2 += 0x8
> > 110: r1 += 0x1
> > 111: if r1 != 0x400 goto -0x5 <LBB28_1>
> >
> > 0000000000000380 <LBB28_3>:
> > 112: w0 = 0x0
> > 113: exit
>
> [...]
>
> I've also took a look why the same program could be verified w/o
> can_loop, but fails with can_loop (with this series applied):
>
> 0000000000000358 <LBB28_1>:
> 107: may_goto +0x4 <LBB28_3>
> 108: *(u64 *)(r2 + 0x0) = r1
> 109: r2 += 0x8
> 110: r1 += 0x1
> 111: if r1 != 0x400 goto -0x5 <LBB28_1>
> ^^
> r1 is no longer marked precise,
> thus maybe_widen_reg() forgets the range for it
> when widen_imprecise_scalars() is called from
> may_goto processing logic.
>
> As a result, verifier enumerates states
> {r2=0P,r1=scalar()}, {r2=8P,r1=scalar()}, {r2=16P,r1=scalar()}, ...
> eventually hitting the value of r2 that does not fit in 'arr1' bounds.
That's correct.
As I was arguing couple emails ago the existing
maybe_widen_reg() logic is just as damaging heuristic
as this new widen_reg() logic.
With this hack:
diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c
index 79e356ac02ab..23892759f05e 100644
--- a/kernel/bpf/verifier.c
+++ b/kernel/bpf/verifier.c
@@ -7928,7 +7928,7 @@ static void maybe_widen_reg(struct bpf_verifier_env *env,
return;
if (rold->precise || rcur->precise || regs_exact(rold, rcur, idmap))
return;
- __mark_reg_unknown(env, rcur);
+// __mark_reg_unknown(env, rcur);
}
the above test is passing.
Though widen_reg() widened the range the bounded loop logic still works.
The loop now looks like
r1=[1,999] r2=8
r1=[2,999] r2=16
..
and eventually the verifier goes to check all 1k iterations of the loop
and passes.
Should I disable old maybe_widen_reg() when new widen_reg() kicks in? ;)
My point is that we had good and bad heuristics. The new one
helps arena. Is it perfect? No. But based on this particular
test it's arguable which one is worse.
Anyway, I think I'm going to tighten it a bit more.
pw-bot: cr
