On Mon, Jul 7, 2025 at 5:37 PM Eduard Zingerman <eddyz87@xxxxxxxxx> wrote:
>
> On Mon, 2025-07-07 at 16:29 -0700, Eduard Zingerman wrote:
> > On Tue, 2025-07-08 at 00:30 +0200, Paul Chaignon wrote:
> >
> > [...]
> >
> > > This is really nice! I think we can extend it to detect some
> > > always-true branches as well, and thus handle the initial case reported
> > > by syzbot.
> > >
> > > - if a_min == 0: we don't deduce anything
> > > - bits that may be set in 'a' are: possible_a = or_range(a_min, a_max)
> > > - bits that are always set in 'b' are: always_b = b_value & ~b_mask
> > > - if possible_a & always_b == possible_a: only true branch is possible
> > > - otherwise, we can't deduce anything
> > >
> > > For BPF_X case, we probably want to also check the reverse with
> > > possible_b & always_a.
> >
> > So, this would extend existing predictions:
> > - [old] always_a & always_b -> infer always true
> > - [old] !(possible_a & possible_b) -> infer always false
> > - [new] if possible_a & always_b == possible_a -> infer true
> > (but make sure 0 is not in possible_a)
> >
> > And it so happens, that it covers example at hand.
> > Note that or_range(1, (u64)-1) == (u64)-1, so maybe tnum would be
> > sufficient, w/o the need for or_range().
> >
> > The part of the verifier that narrows the range after prediction:
> >
> > regs_refine_cond_op:
> >
> > case BPF_JSET | BPF_X: /* reverse of BPF_JSET, see rev_opcode() */
> > if (!is_reg_const(reg: reg2, subreg32: is_jmp32))
> > swap(reg1, reg2);
> > if (!is_reg_const(reg: reg2, subreg32: is_jmp32))
> > break;
> > val = reg_const_value(reg: reg2, subreg32: is_jmp32);
> > ...
> > reg1->var_off = tnum_and(a: reg1->var_off, b: tnum_const(value: ~val));
> > ...
> > break;
> >
> > And after suggested change this part would be executed only if tnum
> > bounds can be changed by jset. So, this eliminates at-least a
> > sub-class of a problem.
>
> But I think the program below would still be problematic:
>
> SEC("socket")
> __success
> __retval(0)
> __naked void jset_bug1(void)
> {
> asm volatile (" \
> call %[bpf_get_prandom_u32]; \
> if r0 < 2 goto 1f; \
> r0 |= 1; \
> if r0 & -2 goto 1f; \
> 1: r0 = 0; \
> exit; \
> " :
> : __imm(bpf_get_prandom_u32)
> : __clobber_all);
> }
>
> The possible_r0 would be changed by `if r0 & -2`, so new rule will not hit.
> And the problem remains unsolved. I think we need to reset min/max
> bounds in regs_refine_cond_op for JSET:
> - in some cases range is more precise than tnum
> - in these cases range cannot be compressed to a tnum
> - predictions in jset are done for a tnum
> - to avoid issues when narrowing tnum after prediction, forget the
> range.
You're digging too deep. llvm doesn't generate JSET insn,
so this is syzbot only issue. Let's address it with minimal changes.
Do not introduce fancy branch taken analysis.
I would be fine with reverting this particular verifier_bug() hunk.
