On Tue, Dec 6, 2022 at 2:19 PM John Fastabend <john.fastabend@xxxxxxxxx> wrote:
>
> Andrii Nakryiko wrote:
> > Don't mark some instructions as jump points when there are actually no
> > jumps and instructions are just processed sequentially. Such case is
> > handled naturally by precision backtracking logic without the need to
> > update jump history.
> >
>
> Sorry having trouble matching up commit message with code below.
Sorry, not clear which part? I'm referring to the logic in
get_prev_insn_idx() here, where we go linearly one instruction
backwards, unless last jmp_history entry matches current instruction.
In the latter case we go to the st->jmp_history[cnt - 1].prev_idx
(non-linear case).
>
> > Also remove both jump and prune point marking for instruction right
> > after unconditional jumps, as program flow can get to the instruction
> > right after unconditional jump instruction only if there is a jump to
> > that instruction from somewhere else in the program. In such case we'll
> > mark such instruction as prune/jump point because it's a destination of
> > a jump.
> >
> > This change has no changes in terms of number of instructions or states
> > processes across Cilium and selftests programs.
> >
> > Signed-off-by: Andrii Nakryiko <andrii@xxxxxxxxxx>
> > ---
> > kernel/bpf/verifier.c | 24 ++++--------------------
> > 1 file changed, 4 insertions(+), 20 deletions(-)
> >
> > diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c
> > index 75a56ded5aca..03c2cc116292 100644
> > --- a/kernel/bpf/verifier.c
> > +++ b/kernel/bpf/verifier.c
> > @@ -12209,13 +12209,10 @@ static int visit_func_call_insn(int t, int insn_cnt,
> > if (ret)
> > return ret;
> >
> > - if (t + 1 < insn_cnt) {
> > - mark_prune_point(env, t + 1);
> > - mark_jmp_point(env, t + 1);
> > - }
> > + mark_prune_point(env, t + 1);
I'm now thinking that maybe here we actually need to keep jmp_point,
as we don't record a jump point for the target of EXIT instruction in
subprog. I'll add this back.
> > +
> > if (visit_callee) {
> > mark_prune_point(env, t);
> > - mark_jmp_point(env, t);
> > ret = push_insn(t, t + insns[t].imm + 1, BRANCH, env,
> > /* It's ok to allow recursion from CFG point of
> > * view. __check_func_call() will do the actual
> > @@ -12249,15 +12246,13 @@ static int visit_insn(int t, int insn_cnt, struct bpf_verifier_env *env)
> > return DONE_EXPLORING;
> >
> > case BPF_CALL:
> > - if (insns[t].imm == BPF_FUNC_timer_set_callback) {
> > + if (insns[t].imm == BPF_FUNC_timer_set_callback)
> > /* Mark this call insn to trigger is_state_visited() check
>
> maybe fix the comment here?
It's not broken, but would you like me to explicitly state "Mark this
call insn as a prune point to trigger..."?
>
> > * before call itself is processed by __check_func_call().
> > * Otherwise new async state will be pushed for further
> > * exploration.
> > */
> > mark_prune_point(env, t);
> > - mark_jmp_point(env, t);
> > - }
> > return visit_func_call_insn(t, insn_cnt, insns, env,
> > insns[t].src_reg == BPF_PSEUDO_CALL);
> >
> > @@ -12271,26 +12266,15 @@ static int visit_insn(int t, int insn_cnt, struct bpf_verifier_env *env)
> > if (ret)
> > return ret;
> >
> > - /* unconditional jmp is not a good pruning point,
> > - * but it's marked, since backtracking needs
> > - * to record jmp history in is_state_visited().
> > - */
> > mark_prune_point(env, t + insns[t].off + 1);
> > mark_jmp_point(env, t + insns[t].off + 1);
> > - /* tell verifier to check for equivalent states
> > - * after every call and jump
> > - */
> > - if (t + 1 < insn_cnt) {
> > - mark_prune_point(env, t + 1);
> > - mark_jmp_point(env, t + 1);
>
> This makes sense to me its unconditional jmp. So no need to
> add jmp point.
>
yep
> > - }
> >
> > return ret;
> >
> > default:
> > /* conditional jump with two edges */
> > mark_prune_point(env, t);
> > - mark_jmp_point(env, t);
>
> ^^^^^^^^^^^^^^^^^^^^^^^
>
> Specifically, try to see why we dropped this jmp_point?
Because there is nothing special about current instruction (which is a
conditional jump instruction). If we got here sequentially, no need to
record jmp_history. If we jumped here from somewhere non-linearly, we
should have already marked this instruction as jmp_point in push_insn
(with e == BRANCH).
So jmp_point is completely irrelevant, the goal here is to force state
checkpointing before we process jump instruction.
Also keep in mind that we mark *destination* of non-linear jump as a
jump point. So target of function call, jump, etc, but not call
instruction or jump instruction itself.
>
> > +
> > ret = push_insn(t, t + 1, FALLTHROUGH, env, true);
> > if (ret)
> > return ret;
> > --
> > 2.30.2
> >
>
>
