Within an iterator or callback based loop, it should be safe to prune
the current state if the old state stack slot is marked as
STACK_INVALID or STACK_MISC:
- either all branches of the old state lead to a program exit;
- or some branch of the old state leads the current state.
This is the same logic as applied in non-loop cases when
states_equal() is called in NOT_EXACT mode.
The test case that exercises stacksafe() and demonstrates the
difference in verification performance is included in the next patch.
I'm not sure if it is possible to prepare a test case that exercises
regsafe(); it appears that the compute_live_registers() pass makes
this impossible.
Nevertheless, for code readability reasons, I think that stacksafe()
and regsafe() should handle STACK_INVALID / NOT_INIT symmetrically.
Hence, this commit changes both functions.
Signed-off-by: Eduard Zingerman <eddyz87@gmail.com>
Link: https://lore.kernel.org/r/20251230-loop-stack-misc-pruning-v1-1-585cfd6cec51@gmail.com
Signed-off-by: Alexei Starovoitov <ast@kernel.org>
if (exact == EXACT)
return regs_exact(rold, rcur, idmap);
- if (rold->type == NOT_INIT) {
- if (exact == NOT_EXACT || rcur->type == NOT_INIT)
- /* explored state can't have used this */
- return true;
- }
+ if (rold->type == NOT_INIT)
+ /* explored state can't have used this */
+ return true;
/* Enforce that register types have to match exactly, including their
* modifiers (like PTR_MAYBE_NULL, MEM_RDONLY, etc), as a general
spi = i / BPF_REG_SIZE;
- if (exact != NOT_EXACT &&
+ if (exact == EXACT &&
(i >= cur->allocated_stack ||
old->stack[spi].slot_type[i % BPF_REG_SIZE] !=
cur->stack[spi].slot_type[i % BPF_REG_SIZE]))