From: Eduard Zingerman <eddyz87@gmail.com>
To: bpf@vger.kernel.org, ast@kernel.org
Cc: andrii@kernel.org, daniel@iogearbox.net, martin.lau@linux.dev,
kernel-team@fb.com, yonghong.song@linux.dev
Subject: Re: [PATCH bpf-next v1 1/2] bpf: states with loop entry have incomplete read/precision marks
Date: Fri, 14 Mar 2025 10:41:16 -0700 [thread overview]
Message-ID: <9190c8821684a6c75c524c58c6d54f7d9b2366e3.camel@gmail.com> (raw)
In-Reply-To: <3c6ac16b7578406e2ddd9ba889ce955748fe636b.camel@gmail.com>
On Thu, 2025-03-13 at 12:28 -0700, Eduard Zingerman wrote:
[...]
> Which makes me wonder.
> If read/precision marks for B are not final and some state D outside
> of the loop becomes equal to B, the read/precision marks for that
> state would be incomplete as well:
>
> D------. // as some read/precision marks are missing from C
> | // propagate_liveness() won't copy all necessary
> .-> A --. | // marks to D.
> | | | |
> | v v |
> '-- B C |
> ^ |
> '------'
>
> This makes comparison with 'loop_entry' states contagious,
> propagating incomplete read/precision mark flag up to the root state.
> This will have verification performance implications.
>
> Alternatively read/precision marks need to be propagated in the state
> graph until fixed point is reached. Like with DFA analysis.
>
> Решето.
And below is an example that verifier does not catch.
Another possibility is to forgo loop entries altogether and upon
states_equal(cached, cur, RANGE_WITHIN) mark all registers in the
`cached` state as read and precise, propagating this info in `cur`.
I'll try this as well.
--- 8< --------------------------------
SEC("?raw_tp")
__flag(BPF_F_TEST_STATE_FREQ)
__failure __msg("misaligned stack access off 0+-31+0 size 8")
__naked int absent_mark_in_the_middle_state2(void)
{
asm volatile (
"call %[bpf_get_prandom_u32];"
"r8 = r0;"
"r7 = 0;"
"r6 = -32;"
"r0 = 0;"
"*(u64 *)(r10 - 16) = r0;"
"r1 = r10;"
"r1 += -8;"
"r2 = 0;"
"r3 = 10;"
"call %[bpf_iter_num_new];"
"call %[bpf_get_prandom_u32];"
"if r0 == r8 goto change_r6_%=;"
"call %[bpf_get_prandom_u32];"
"before_loop_%=:"
"if r0 == r8 goto jump_into_loop_%=;"
"loop_%=:"
"r1 = r10;"
"r1 += -8;"
"call %[bpf_iter_num_next];"
"if r0 == 0 goto loop_end_%=;"
"call %[bpf_get_prandom_u32];"
"if r0 == r8 goto use_r6_%=;"
"goto loop_%=;"
"loop_end_%=:"
"r1 = r10;"
"r1 += -8;"
"call %[bpf_iter_num_destroy];"
"r0 = 0;"
"exit;"
"use_r6_%=:"
"r0 = r10;"
"r0 += r6;"
"r1 = 7;"
"*(u64 *)(r0 + 0) = r1;"
"goto loop_%=;"
"change_r6_%=:"
"r6 = -31;"
"jump_into_loop_%=: "
"goto +0;"
"goto loop_%=;"
:
: __imm(bpf_iter_num_new),
__imm(bpf_iter_num_next),
__imm(bpf_iter_num_destroy),
__imm(bpf_get_prandom_u32)
: __clobber_all
);
}
-------------------------------- >8 ---
[...]
next prev parent reply other threads:[~2025-03-14 17:41 UTC|newest]
Thread overview: 9+ messages / expand[flat|nested] mbox.gz Atom feed top
2025-03-12 3:13 [PATCH bpf-next v1 1/2] bpf: states with loop entry have incomplete read/precision marks Eduard Zingerman
2025-03-12 3:13 ` [PATCH bpf-next v1 2/2] selftests/bpf: test case with missing read/precision mark Eduard Zingerman
2025-03-13 19:28 ` [PATCH bpf-next v1 1/2] bpf: states with loop entry have incomplete read/precision marks Eduard Zingerman
2025-03-14 17:41 ` Eduard Zingerman [this message]
2025-03-15 2:51 ` Alexei Starovoitov
2025-03-15 6:04 ` Eduard Zingerman
2025-03-17 20:28 ` Eduard Zingerman
2025-03-17 21:46 ` Alexei Starovoitov
2025-03-21 20:02 ` Eduard Zingerman
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to=9190c8821684a6c75c524c58c6d54f7d9b2366e3.camel@gmail.com \
--to=eddyz87@gmail.com \
--cc=andrii@kernel.org \
--cc=ast@kernel.org \
--cc=bpf@vger.kernel.org \
--cc=daniel@iogearbox.net \
--cc=kernel-team@fb.com \
--cc=martin.lau@linux.dev \
--cc=yonghong.song@linux.dev \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox