This RFC introduces an algorithm called tnum_step that can be used to
detect when a tnum and the range have an empty intersection. This can
help the verifier avoid walking dead branches that lead to range
invariant violations. I am sending this as a patchset to keep the
motivation (this email) separate from the details of algorithm
(following email).

Several fuzzing campaigns have reported programs that trigger "REG
INVARIANTS VIOLATION" errors in the verifier [1, 2, 3, 4]. These
invariant violations happen when the verifier refines register bounds in
a branch that is actually dead. When reg_bounds_sync() attempts to
update the tnum and the range in such a dead branch, it can produce
inconsistent ranges, for example, a register state with umin > umax or
var_off values incompatible with the range bounds.

There is a solution is in the works by Eduard [5] to modify verifier's
logic to use the fact that the register's tnum and range bounds are
incompatible to detect that a branch cannot be taken. Detecting an empty
intersection between the range and the tnum could be a useful primitive
to detect incompatiblity.

* Detecting Empty Intersections

Consider a range r [umin, umax] and a tnum t (tval, tmask). A simple way
to check if the range and the tnum intersect is to compare their
bounds:

	tmin = tval
	tmax = tval | tmask

	if (tmin > umax || tmax < umin)
		return -1;  // no intersection

However, this approach fails when the tnum represents a non-contiguous
set of values, and the range lies entirely "in-between". For example:

	t = x0x1	{1, 3, 9, 11}
	r = [4, 8]	{4, 5, 6, 7, 8}

Here, tmin <= umax && tmax >= umin, yet the two sets have no
intersection.

To implement set intersection for tnum and ranges, it would be useful to
have the ability to walk through the values in the tnum. If the next
valid tnum value after umin already jumps past umax, then there is no
value of t in [umin, umax]. In other words, we need a "step" function
for tnums that can determine the next numerically larger concrete value
that is contained in the tnum's set.

* The tnum_step() primitive

To correctly detect these cases, we introduce a new helper:

    u64 tnum_step(struct tnum t, u64 z);

This function returns the smallest number greater than z that is
representable by the tnum t. Using tnum_step(), intersection detection
can be implemented as:

	if (tmin > umax || tmax < umin)
		return -1;  // no intersection

	/* next valid tnum value after umin already jumps past umax,
	* implying there's no value of t in [umin, umax].
	*/
	if (tnum_step(t, umin) > umax)
		return -1;  // no intersection

	return 1;  // intersection exists

* A sound and complete procedure that runs in constant time

At first glance, one might expect that computing tnum_step() would
require iterating over the individual bits of t and z. However, the
procedure for tnum_step(), introduced in the next patch, derives the
next tnum value greater than z purely through bitwise operations, and
thus runs in constant time.

Importantly, using the tnum_step() primitive we can construct a
range-tnum intersection test (as shown) that is both *sound and
complete*: it never reports "no intersection" when there is one, and
does not miss any cases of "no intersection".

* Usage in the verifier and next steps

The tnum_step() procedure is self-contained and can be incorporated
as-is.

Regarding incorporating the range-tnum intersection test, as it
stands, if is_branch_taken() cannot determine that a branch is dead,
reg_set_min_max()->regs_refine_cond_op() are called to update the
register bounds.

We can incorporate the range-tnum intersection test after the calls to
regs_refine_cond_op() or the calls to reg_bounds_sync(). If there is no
intersection between the ranges and the tnum, we are on a dead branch.

Alternatively, the range-tnum intersection check could be incorporated
as part of Eduard's upcoming patchset, which is expected to rework the
logic in reg_set_min_max() and is_branch_taken().

Looking forward to hearing any feedback and suggestions.

[1] https://lore.kernel.org/bpf/aKWytdZ8mRegBE0H@mail.gmail.com/
[2] https://lore.kernel.org/bpf/75b3af3d315d60c1c5bfc8e3929ac69bb57d5cea.1752099022.git.paul.chaignon@gmail.com/
[3] https://lore.kernel.org/bpf/CACkBjsZen6AA1jXqgmA=uoZZJt5bLu+7Hz3nx3BrvLAP=CqGuA@mail.gmail.com/T/#e6604e4092656b192cf617c98f9a00b16c67aad87
[4] https://lore.kernel.org/bpf/aPJZs5h7ihqOb-e6@mail.gmail.com/
[5] https://lore.kernel.org/bpf/CAEf4BzY_f=iNKC2CVz-myfe_OERN9XWHiuNG6vng43-MXUAvSw@mail.gmail.com/

Harishankar Vishwanathan (1):
  bpf, verifier: Introduce tnum_step to step through tnum's members

 include/linux/tnum.h |  3 ++-
 kernel/bpf/tnum.c    | 52 ++++++++++++++++++++++++++++++++++++++++++++
 2 files changed, 54 insertions(+), 1 deletion(-)

-- 
2.45.2

On Fri, Nov 07, 2025 at 02:23:27PM -0500, Harishankar Vishwanathan wrote:
> This RFC introduces an algorithm called tnum_step that can be used to
> detect when a tnum and the range have an empty intersection. This can
> help the verifier avoid walking dead branches that lead to range
> invariant violations. I am sending this as a patchset to keep the
> motivation (this email) separate from the details of algorithm
> (following email).
> 
> Several fuzzing campaigns have reported programs that trigger "REG
> INVARIANTS VIOLATION" errors in the verifier [1, 2, 3, 4]. These
> invariant violations happen when the verifier refines register bounds in
> a branch that is actually dead. When reg_bounds_sync() attempts to
> update the tnum and the range in such a dead branch, it can produce
> inconsistent ranges, for example, a register state with umin > umax or
> var_off values incompatible with the range bounds.

I think an open question here is whether such patterns of tnum/ranges
happen in practice, outside of syzkaller. We probably don't want to
introduce additional logic for something that doesn't help "real"
programs. I'm happy to check the impact on Cilium for example, but that
would require a patch to actually start using the new tnum helper.

> 
> There is a solution is in the works by Eduard [5] to modify verifier's
> logic to use the fact that the register's tnum and range bounds are
> incompatible to detect that a branch cannot be taken. Detecting an empty
> intersection between the range and the tnum could be a useful primitive
> to detect incompatiblity.
> 
> * Detecting Empty Intersections

[...]

> * Usage in the verifier and next steps
> 
> The tnum_step() procedure is self-contained and can be incorporated
> as-is.
> 
> Regarding incorporating the range-tnum intersection test, as it
> stands, if is_branch_taken() cannot determine that a branch is dead,
> reg_set_min_max()->regs_refine_cond_op() are called to update the
> register bounds.
> 
> We can incorporate the range-tnum intersection test after the calls to
> regs_refine_cond_op() or the calls to reg_bounds_sync(). If there is no
> intersection between the ranges and the tnum, we are on a dead branch.

Couldn't we incorporate such a test in is_branch_taken() today?

> 
> Alternatively, the range-tnum intersection check could be incorporated
> as part of Eduard's upcoming patchset, which is expected to rework the
> logic in reg_set_min_max() and is_branch_taken().
> 
> Looking forward to hearing any feedback and suggestions.
> 
> [1] https://lore.kernel.org/bpf/aKWytdZ8mRegBE0H@mail.gmail.com/
> [2] https://lore.kernel.org/bpf/75b3af3d315d60c1c5bfc8e3929ac69bb57d5cea.1752099022.git.paul.chaignon@gmail.com/
> [3] https://lore.kernel.org/bpf/CACkBjsZen6AA1jXqgmA=uoZZJt5bLu+7Hz3nx3BrvLAP=CqGuA@mail.gmail.com/T/#e6604e4092656b192cf617c98f9a00b16c67aad87
> [4] https://lore.kernel.org/bpf/aPJZs5h7ihqOb-e6@mail.gmail.com/
> [5] https://lore.kernel.org/bpf/CAEf4BzY_f=iNKC2CVz-myfe_OERN9XWHiuNG6vng43-MXUAvSw@mail.gmail.com/
> 
> Harishankar Vishwanathan (1):
>   bpf, verifier: Introduce tnum_step to step through tnum's members
> 
>  include/linux/tnum.h |  3 ++-
>  kernel/bpf/tnum.c    | 52 ++++++++++++++++++++++++++++++++++++++++++++
>  2 files changed, 54 insertions(+), 1 deletion(-)
> 
> -- 
> 2.45.2
>

On Thu, Nov 13, 2025 at 12:17 PM Paul Chaignon <paul.chaignon@gmail.com> wrote:
>
> On Fri, Nov 07, 2025 at 02:23:27PM -0500, Harishankar Vishwanathan wrote:
> > This RFC introduces an algorithm called tnum_step that can be used to
> > detect when a tnum and the range have an empty intersection. This can
> > help the verifier avoid walking dead branches that lead to range
> > invariant violations. I am sending this as a patchset to keep the
> > motivation (this email) separate from the details of algorithm
> > (following email).
> >
> > Several fuzzing campaigns have reported programs that trigger "REG
> > INVARIANTS VIOLATION" errors in the verifier [1, 2, 3, 4]. These
> > invariant violations happen when the verifier refines register bounds in
> > a branch that is actually dead. When reg_bounds_sync() attempts to
> > update the tnum and the range in such a dead branch, it can produce
> > inconsistent ranges, for example, a register state with umin > umax or
> > var_off values incompatible with the range bounds.
>
> I think an open question here is whether such patterns of tnum/ranges
> happen in practice, outside of syzkaller. We probably don't want to
> introduce additional logic for something that doesn't help "real"
> programs. I'm happy to check the impact on Cilium for example, but that
> would require a patch to actually start using the new tnum helper.
>

Fair point. But I wanted to highlight the completeness of this approach,
in addition to the soundness. The check:

    if (tmin > umax || tmax < umin || tnum_step(t, umin) > umax)

detects *all* possible cases of "no intersection" betweeen tnums and u64
ranges. If future updates to the regs_refine_cond_op() logic take the
tnum and ranges to any incompatible case, this check will detect them.

[...]
> > * Usage in the verifier and next steps
> >
> > The tnum_step() procedure is self-contained and can be incorporated
> > as-is.
> >
> > Regarding incorporating the range-tnum intersection test, as it
> > stands, if is_branch_taken() cannot determine that a branch is dead,
> > reg_set_min_max()->regs_refine_cond_op() are called to update the
> > register bounds.
> >
> > We can incorporate the range-tnum intersection test after the calls to
> > regs_refine_cond_op() or the calls to reg_bounds_sync(). If there is no
> > intersection between the ranges and the tnum, we are on a dead branch.
>
> Couldn't we incorporate such a test in is_branch_taken() today?

The idea behind suggesting the test in reg_set_min_max() and not
is_branch_taken() was that the empty intersection typically happens
after the call to reg_bounds_sync(), which updates the bounds so that
tnums and ranges become incompatible.

At this point however, the verifier has already forked new
bpf_verifier_states (via push_stack()). Once we detect an impossible
branch using the new check, we will need to clean up the states
corresponding to the impossible branch.

I was hoping for some comments on whether this approach is
feasible.

> >
> > Alternatively, the range-tnum intersection check could be incorporated
> > as part of Eduard's upcoming patchset, which is expected to rework the
> > logic in reg_set_min_max() and is_branch_taken().
> >
> > Looking forward to hearing any feedback and suggestions.
> >
> > [1] https://lore.kernel.org/bpf/aKWytdZ8mRegBE0H@mail.gmail.com/
> > [2] https://lore.kernel.org/bpf/75b3af3d315d60c1c5bfc8e3929ac69bb57d5cea.1752099022.git.paul.chaignon@gmail.com/
> > [3] https://lore.kernel.org/bpf/CACkBjsZen6AA1jXqgmA=uoZZJt5bLu+7Hz3nx3BrvLAP=CqGuA@mail.gmail.com/T/#e6604e4092656b192cf617c98f9a00b16c67aad87
> > [4] https://lore.kernel.org/bpf/aPJZs5h7ihqOb-e6@mail.gmail.com/
> > [5] https://lore.kernel.org/bpf/CAEf4BzY_f=iNKC2CVz-myfe_OERN9XWHiuNG6vng43-MXUAvSw@mail.gmail.com/
> >
> > Harishankar Vishwanathan (1):
> >   bpf, verifier: Introduce tnum_step to step through tnum's members
> >
> >  include/linux/tnum.h |  3 ++-
> >  kernel/bpf/tnum.c    | 52 ++++++++++++++++++++++++++++++++++++++++++++
> >  2 files changed, 54 insertions(+), 1 deletion(-)
> >
> > --
> > 2.45.2
> >