On Tue, Oct 3, 2023 at 8:33 AM Eduard Zingerman <eddyz87@xxxxxxxxx> wrote: > > > Would lead to an infinite loop when using the patch shared in [1]. yeah. the first hacky patch was too buggy. Attached is a better version, but the same idea. It passes all existing tests and accurately detects num_iter_bug, Then I took 5 from: https://github.com/kernel-patches/bpf/commit/379c865e6b99302d69392d4f224b5c540247bcb2 It does the right thing for all of them including iter_precision_fixed_point[12] except loop_state_deps1. > > Note, that removal of `elem->st.looping_state = false;` from > push_stack() is not safe either, precision marks and unsafe values > could be concealed in nested iteration states as shown in example [2], > so we are risking pruning some states too early. it's loop_state_deps1, right? fp-25 is a tricky one. > SEC("?raw_tp") > __success > __naked int loop1(void) > { > asm volatile ( > "r1 = r10;" > "r1 += -8;" > "r2 = 0;" > "r3 = 10;" > "call %[bpf_iter_num_new];" > "loop_%=:" > "r1 = r10;" > "r1 += -8;" > "call %[bpf_iter_num_next];" > "if r0 == 0 goto loop_end_%=;" > "call %[bpf_get_prandom_u32];" > "if r0 != 42 goto loop_%=;" > "r0 += 0;" > "goto loop_%=;" > "loop_end_%=:" > "r1 = r10;" > "r1 += -8;" > "call %[bpf_iter_num_destroy];" > "r0 = 0;" > "exit;" > : > : __imm(bpf_get_prandom_u32), > __imm(bpf_iter_num_new), > __imm(bpf_iter_num_next), > __imm(bpf_iter_num_destroy) > : __clobber_all > ); > } this one loads fine with the attached patch. I still prefer to avoid two stack hacks if one is enough. The key idea of the patch is: @@ -7733,7 +7743,8 @@ static int process_iter_next_call(struct bpf_verifier_env *env, int insn_idx, queued_st = push_stack(env, insn_idx + 1, insn_idx, false); if (!queued_st) return -ENOMEM; - + queued_st->looping_states++; + queued_st->branches--; so deferred looping state from process_iter_next_call() are not considered branches in _that_ state. The push_stack still did branches++ in the parent. So the verifier will process everything after process_iter_next_call() before reducing its branches to zer0 and making it eligible for state equality comparison.
Attachment:
0001-iter-hack-2.patch
Description: Binary data
