Re: [PATCH bpf v1 0/2] Fix map value pruning check

[Edward Cree <ecree.xilinx@gmail.com>]

On 11/11/2022 20:27, Kumar Kartikeya Dwivedi wrote:
> However, looking more closely, it seems to me that the logic of
> check_ids is broken as well.
> 
> Edward, given you introduced the idmap, can you provide a little more
> historical context on what the idea behind check_ids was, since it seems
> to be doing the wrong thing as far as I understood things. I think we
> need to compare the ids directly everywhere.

reg->id has two different kinds of usage/semantics.  One, which was
 the only one when idmap was introduced, is pairing with other regs
 within state (including stack slots and caller frames); for this,
 check_ids() is fine (the comment above it explains why).
The other, added by d83525ca62cf ("bpf: introduce bpf_spin_lock"),
 pairs not with other regs' ids but with state->active_spin_lock;
 currently states_equal() requires this to be numerically identical
 between old and cur, rather than running it through the idmap; this
 would appear to be the origin of the bug.

Alexei, is there any valid world in which there's an active_spin_lock
 but the corresponding id does not exist anywhere in the state's
 regs, stack etc.?  If not then I think it suffices to
 check_ids(old->active_spin_lock, cur->active_spin_lock,
           env->idmap_scratch);
 in func_states_equal() of the leaf frame (only leaf frame can be
 holding a spinlock), and remove the existing check from
 states_equal().
Because what we want to know isn't "Do both of these spinlocks come
 from the same original ID derivation", but "do all registers that
 hold a value that could be used to unlock the spinlock in the
 continuation-to-exit of the old state also hold such a value in the
 current state", which means that we want the pair <old_asl, new_asl>
 in the idmap when we walk the regs and stack.

While we *could* implement that by requiring IDs to match numerically
 as in Kumar's patch, that's needlessly strict and will miss pruning
 opportunities.

-ed