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.
