On Mon, 2024-02-12 at 17:20 -0800, Yonghong Song wrote:
[...]
Hi Yonghong,
Thank you for the feedback, I put updated description at the end of
the email, below are the answers to your questions.
> > - (0) {7P,7,7}
>
> Why we have '7P' here?
Precision is propagated because of the check in the "-> to end" branch,
made it more clear in the updated description.
> > - (3) {7P,7,7}
>
> So here when (3) is hit, we have callback_depth = 1, right?
Yes, made callback depth explicit.
> > - (0) {7P,7,42} (checkpoint #1):
>
> So for below (3)/(2)/(1) we have callback_depth = 2, right?
Yes.
> > - (3) {7P,7,42}
> > - (0) {7P,7,42} -> to end
> > - (2) {7P,7,42}
> > - (0) {7P,42,42} -> to end
> > - (1) {7P,7,42} (checkpoint #2)
> > - (0) {42P,7P,42} -> to end
> > - (2) {7P,7,7}
>
> So now we back to callback_depth = 1.
Yes.
[...]
> > While the last branch of the tree has callback_depth of 0, and thus
> > could yet explore the state {42,42,7} if not pruned prematurely.
>
> which 'last branch'?
Gave it a name.
> It would be good if the commit message mentions what will change
> for the above digram if this commit is applied, so people can understand
> why this commit helps.
Added.
--- 8< ---------------------------------
struct ctx {
__u64 a;
__u64 b;
__u64 c;
};
static void loop_cb(int i, struct ctx *ctx)
{
/* assume that generated code is "fallthrough-first":
* if ... == 1 goto
* if ... == 2 goto
* <default>
*/
switch (bpf_get_prandom_u32()) {
case 1: /* 1 */ ctx->a = 42; return 0; break;
case 2: /* 2 */ ctx->b = 42; return 0; break;
default: /* 3 */ ctx->c = 42; return 0; break;
}
}
SEC("tc")
__failure
__flag(BPF_F_TEST_STATE_FREQ)
int test(struct __sk_buff *skb)
{
struct ctx ctx = { 7, 7, 7 };
/* 0 */ bpf_loop(2, loop_cb, &ctx, 0);
if (/* 4 */ ctx.a == 42 && ctx.b == 42 && ctx.c == 7)
/* 5 */ asm volatile("r0 /= 0;":::"r0");
/* 6 */ return 0;
}
Prior to this commit verifier built the following checkpoint tree for
this example:
.------------------------------------- checkpoint / state name
| .-------------------------------- code point number
| | .---------------------------- stack state {ctx.a,ctx.b,ctx.c}
| | | .------------------- callback depth in frame #0
v v v v
- (0) {7P,7P,7},depth=0
- (3) {7P,7,7},depth=1
(a) - (0) {7P,7,42},depth=1
- (3) {7P,7,42},depth=2
- (0) {7P,7,42},depth=2 loop terminates because of depth limit
- (4) {7P,7,42},depth=0 predicted false, ctx.a marked precise
- (6) exit
- (2) {7P,7,42},depth=2
- (0) {7P,42,42},depth=2 loop terminates because of depth limit
- (4) {7P,42,42},depth=0 predicted false, ctx.a marked precise
- (6) exit
(b) - (1) {7P,7P,42},depth=2
- (0) {42P,7P,42},depth=2 loop terminates because of depth limit
- (4) {42P,7P,42},depth=0 predicted false, ctx.{a,b} marked precise
- (6) exit
- (2) {7P,7,7},depth=1
- (0) {7P,42,7},depth=1 considered safe, pruned using checkpoint (a)
(c) - (1) {7,7,7},depth=1 considered safe, pruned using checkpoint (b)
Here checkpoint (b) has callback_depth of 2, meaning that it would
never reach state {42,42,7}.
While checkpoint (c) has callback_depth of 1, and thus
could yet explore the state {42,42,7} if not pruned prematurely.
This commit makes forbids such premature pruning,
allowing verifier to explore states sub-tree starting at (c):
(c) - (1) {7,7,7P},depth=1
- (0) {42P,7,7P},depth=1
...
- (2) {42,7,7},depth=2
- (0) {42,42,7},depth=2 loop terminates because of depth limit
- (4) {42,42,7},depth=0 predicted true, ctx.{a,b,c} marked precise
- (5) division by zero
--------------------------------- >8 ---
Wdyt?
