On Mon, 2023-10-23 at 22:58 -0700, Andrii Nakryiko wrote: > On Mon, Oct 23, 2023 at 5:09 PM Eduard Zingerman <eddyz87@xxxxxxxxx> wrote: > > > > Iterator convergence logic in is_state_visited() uses state_equals() > > for states with branches counter > 0 to check if iterator based loop > > converges. This is not fully correct because state_equals() relies on > > presence of read and precision marks on registers. These marks are not > > guaranteed to be finalized while state has branches. > > Commit message for patch #3 describes a program that exhibits such > > behavior. > > > > This patch-set aims to fix iterator convergence logic by adding notion > > of exact states comparison. Exact comparison does not rely on presence > > of read or precision marks and thus is more strict. > > As explained in commit message for patch #3 exact comparisons require > > addition of speculative register bounds widening. The end result for > > BPF verifier users could be summarized as follows: > > > > (!) After this update verifier would reject programs that conjure an > > imprecise value on the first loop iteration and use it as precise > > on the second (for iterator based loops). > > > > I urge people to at least skim over the commit message for patch #3. > > > > Patches are organized as follows: > > - patches #1,2: moving/extracting utility functions; > > - patch #3: introduces exact mode for states comparison and adds > > widening heuristic; > > - patch #4: adds test-cases that demonstrate why the series is > > necessary; > > - patch #5: extends patch #3 with a notion of state loop entries, > > these entries have to be tracked to correctly identify that > > different verifier states belong to the same states loop; > > - patch #6: adds a test-case that demonstrates a program > > which requires loop entry tracking for correct verification; > > - patch #7: just adds a few debug prints. > > > > The following actions are planned as a followup for this patch-set: > > - implementation has to be adapted for callbacks handling logic as a > > part of a fix for [1]; > > - it is necessary to explore ways to improve widening heuristic to > > handle iters_task_vma test w/o need to insert barrier_var() calls; > > - explored states eviction logic on cache miss has to be extended > > to either: > > - allow eviction of checkpoint states -or- > > - be sped up in case if there are many active checkpoints associated > > with the same instruction. > > > > The patch-set is a followup for mailing list discussion [1]. > > > > Changelog: > > - V2 [3] -> V3: > > - correct check for stack spills in widen_imprecise_scalars(), > > added test case progs/iters.c:widen_spill to check the behavior > > (suggested by Andrii); > > - allow eviction of checkpoint states in is_state_visited() to avoid > > pathological verifier performance when iterator based loop does not > > converge (discussion with Alexei). > > - V1 [2] -> V2, applied changes suggested by Alexei offlist: > > - __explored_state() function removed; > > - same_callsites() function is now used in clean_live_states(); > > - patches #1,2 are added as preparatory code movement; > > - in process_iter_next_call() a safeguard is added to verify that > > cur_st->parent exists and has expected insn index / call sites. > > > > [1] https://lore.kernel.org/bpf/97a90da09404c65c8e810cf83c94ac703705dc0e.camel@xxxxxxxxx/ > > [2] https://lore.kernel.org/bpf/20231021005939.1041-1-eddyz87@xxxxxxxxx/ > > [3] https://lore.kernel.org/bpf/20231022010812.9201-1-eddyz87@xxxxxxxxx/ > > > > Eduard Zingerman (7): > > bpf: move explored_state() closer to the beginning of verifier.c > > bpf: extract same_callsites() as utility function > > bpf: exact states comparison for iterator convergence checks > > selftests/bpf: tests with delayed read/precision makrs in loop body > > bpf: correct loop detection for iterators convergence > > selftests/bpf: test if state loops are detected in a tricky case > > bpf: print full verifier states on infinite loop detection > > > > include/linux/bpf_verifier.h | 16 + > > kernel/bpf/verifier.c | 475 ++++++++++-- > > tools/testing/selftests/bpf/progs/iters.c | 695 ++++++++++++++++++ > > .../selftests/bpf/progs/iters_task_vma.c | 1 + > > 4 files changed, 1133 insertions(+), 54 deletions(-) > > > > -- > > 2.42.0 > > > > Thanks a lot for working on this and getting it to the end despite > many setbacks and ambiguity, great work! Thank you and Alexei for working on it as well. We'll see if this patch-set is good enough or the idea with computing fixed point for read and precision marks has to be finalized.
