On Sat, Oct 21, 2023 at 6:08 PM Eduard Zingerman <eddyz87@xxxxxxxxx> wrote:
>
> It turns out that .branches > 0 in is_state_visited() is not a
> sufficient condition to identify if two verifier states form a loop
> when iterators convergence is computed. This commit adds logic to
> distinguish situations like below:
>
> (I) initial (II) initial
> | |
> V V
> .---------> hdr ..
> | | |
> | V V
> | .------... .------..
> | | | | |
> | V V V V
> | ... ... .-> hdr ..
> | | | | | |
> | V V | V V
> | succ <- cur | succ <- cur
> | | | |
> | V | V
> | ... | ...
> | | | |
> '----' '----'
>
> For both (I) and (II) successor 'succ' of the current state 'cur' was
> previously explored and has branches count at 0. However, loop entry
> 'hdr' corresponding to 'succ' might be a part of current DFS path.
> If that is the case 'succ' and 'cur' are members of the same loop
> and have to be compared exactly.
>
> Co-developed-by: Andrii Nakryiko <andrii.nakryiko@xxxxxxxxx>
> Co-developed-by: Alexei Starovoitov <alexei.starovoitov@xxxxxxxxx>
> Signed-off-by: Eduard Zingerman <eddyz87@xxxxxxxxx>
> ---
> include/linux/bpf_verifier.h | 15 +++
> kernel/bpf/verifier.c | 207 ++++++++++++++++++++++++++++++++++-
> 2 files changed, 218 insertions(+), 4 deletions(-)
>
LGTM, but see the note below about state being its own loop_entry. It
feels like a bit better approach would be to use "loop_entry_ref_cnt"
instead of just a bool used_as_loop_entry, and do a proper accounting
when child state is freed and when propagating loop_entries. But
perhaps that can be done in a follow up, if you think it's a good
idea.
Reviewed-by: Andrii Nakryiko <andrii@xxxxxxxxxx>
> diff --git a/include/linux/bpf_verifier.h b/include/linux/bpf_verifier.h
> index 38b788228594..24213a99cc79 100644
> --- a/include/linux/bpf_verifier.h
> +++ b/include/linux/bpf_verifier.h
[...]
> + * To adapt this algorithm for use with verifier:
> + * - use st->branch == 0 as a signal that DFS of succ had been finished
> + * and cur's loop entry has to be updated (case A), handle this in
> + * update_branch_counts();
> + * - use st->branch > 0 as a signal that st is in the current DFS path;
> + * - handle cases B and C in is_state_visited();
> + * - update topmost loop entry for intermediate states in get_loop_entry().
> + */
> +static struct bpf_verifier_state *get_loop_entry(struct bpf_verifier_state *st)
> +{
> + struct bpf_verifier_state *topmost = st->loop_entry, *old;
> +
> + while (topmost && topmost->loop_entry && topmost != topmost->loop_entry)
> + topmost = topmost->loop_entry;
> + /* Update loop entries for intermediate states to avoid this
> + * traversal in future get_loop_entry() calls.
> + */
> + while (st && st->loop_entry != topmost) {
> + old = st->loop_entry;
> + st->loop_entry = topmost;
> + st = old;
> + }
> + return topmost;
> +}
> +
> +static void update_loop_entry(struct bpf_verifier_state *cur, struct bpf_verifier_state *hdr)
> +{
> + struct bpf_verifier_state *cur1, *hdr1;
> +
> + cur1 = get_loop_entry(cur) ?: cur;
> + hdr1 = get_loop_entry(hdr) ?: hdr;
> + /* The head1->branches check decides between cases B and C in
> + * comment for get_loop_entry(). If hdr1->branches == 0 then
> + * head's topmost loop entry is not in current DFS path,
> + * hence 'cur' and 'hdr' are not in the same loop and there is
> + * no need to update cur->loop_entry.
> + */
> + if (hdr1->branches && hdr1->dfs_depth <= cur1->dfs_depth) {
> + cur->loop_entry = hdr;
> + hdr->used_as_loop_entry = true;
> + }
> +}
> +
> static void update_branch_counts(struct bpf_verifier_env *env, struct bpf_verifier_state *st)
> {
> while (st) {
> u32 br = --st->branches;
>
> + /* br == 0 signals that DFS exploration for 'st' is finished,
> + * thus it is necessary to update parent's loop entry if it
> + * turned out that st is a part of some loop.
> + * This is a part of 'case A' in get_loop_entry() comment.
> + */
> + if (br == 0 && st->parent && st->loop_entry)
> + update_loop_entry(st->parent, st->loop_entry);
> +
> /* WARN_ON(br > 1) technically makes sense here,
> * but see comment in push_stack(), hence:
> */
> @@ -16649,10 +16815,11 @@ static int is_state_visited(struct bpf_verifier_env *env, int insn_idx)
> {
> struct bpf_verifier_state_list *new_sl;
> struct bpf_verifier_state_list *sl, **pprev;
> - struct bpf_verifier_state *cur = env->cur_state, *new;
> + struct bpf_verifier_state *cur = env->cur_state, *new, *loop_entry;
> int i, j, err, states_cnt = 0;
> bool force_new_state = env->test_state_freq || is_force_checkpoint(env, insn_idx);
> bool add_new_state = force_new_state;
> + bool force_exact;
>
> /* bpf progs typically have pruning point every 4 instructions
> * http://vger.kernel.org/bpfconf2019.html#session-1
> @@ -16747,8 +16914,10 @@ static int is_state_visited(struct bpf_verifier_env *env, int insn_idx)
> */
> spi = __get_spi(iter_reg->off + iter_reg->var_off.value);
> iter_state = &func(env, iter_reg)->stack[spi].spilled_ptr;
> - if (iter_state->iter.state == BPF_ITER_STATE_ACTIVE)
> + if (iter_state->iter.state == BPF_ITER_STATE_ACTIVE) {
> + update_loop_entry(cur, &sl->state);
> goto hit;
> + }
> }
> goto skip_inf_loop_check;
> }
> @@ -16779,7 +16948,36 @@ static int is_state_visited(struct bpf_verifier_env *env, int insn_idx)
> add_new_state = false;
> goto miss;
> }
> - if (states_equal(env, &sl->state, cur, false)) {
> + /* If sl->state is a part of a loop and this loop's entry is a part of
> + * current verification path then states have to be compared exactly.
> + * 'force_exact' is needed to catch the following case:
> + *
> + * initial Here state 'succ' was processed first,
> + * | it was eventually tracked to produce a
> + * V state identical to 'hdr'.
> + * .---------> hdr All branches from 'succ' had been explored
> + * | | and thus 'succ' has its .branches == 0.
> + * | V
> + * | .------... Suppose states 'cur' and 'succ' correspond
> + * | | | to the same instruction + callsites.
> + * | V V In such case it is necessary to check
> + * | ... ... if 'succ' and 'cur' are states_equal().
> + * | | | If 'succ' and 'cur' are a part of the
> + * | V V same loop exact flag has to be set.
> + * | succ <- cur To check if that is the case, verify
> + * | | if loop entry of 'succ' is in current
> + * | V DFS path.
> + * | ...
> + * | |
> + * '----'
> + *
> + * Additional details are in the comment before get_loop_entry().
> + */
> + loop_entry = get_loop_entry(&sl->state);
> + force_exact = loop_entry && loop_entry->branches > 0;
> + if (states_equal(env, &sl->state, cur, force_exact)) {
> + if (force_exact)
> + update_loop_entry(cur, loop_entry);
> hit:
> sl->hit_cnt++;
> /* reached equivalent register/stack state,
> @@ -16825,7 +17023,8 @@ static int is_state_visited(struct bpf_verifier_env *env, int insn_idx)
> * speed up verification
> */
> *pprev = sl->next;
> - if (sl->state.frame[0]->regs[0].live & REG_LIVE_DONE) {
> + if (sl->state.frame[0]->regs[0].live & REG_LIVE_DONE &&
> + !sl->state.used_as_loop_entry) {
In get_loop_entry() you have an additional `topmost !=
topmost->loop_entry` check, suggesting that state can be its own
loop_entry. Can that happen? And if yes, should we account for that
here?
> u32 br = sl->state.branches;
>
> WARN_ONCE(br,
> --
> 2.42.0
>
