On 2/16/24 6:27 AM, Eduard Zingerman wrote:
On Wed, 2024-02-14 at 09:42 -0800, Yonghong Song wrote:
.------------------------------------- Checkpoint / State name
| .-------------------------------- Code point number
| | .---------------------------- Stack state {ctx.a,ctx.b,ctx.c}
| | | .------------------- Callback depth in frame #0
v v v v
1 - (0) {7P,7P,7},depth=0
2 - (3) {7P,7P,7},depth=1
3 - (0) {7P,7P,42},depth=1
(a) - (3) {7P,7,42},depth=2
4 - (0) {7P,7,42},depth=2 loop terminates because of depth limit
5 - (4) {7P,7,42},depth=0 predicted false, ctx.a marked precise
6 - (6) exit
7 - (2) {7P,7,42},depth=2
8 - (0) {7P,42,42},depth=2 loop terminates because of depth limit
9 - (4) {7P,42,42},depth=0 predicted false, ctx.a marked precise
10 - (6) exit
(b) - (1) {7P,7P,42},depth=2
11 - (0) {42P,7P,42},depth=2 loop terminates because of depth limit
12 - (4) {42P,7P,42},depth=0 predicted false, ctx.{a,b} marked precise
13 - (6) exit
14 - (2) {7P,7,7},depth=1
15 - (0) {7P,42,7},depth=1 considered safe, pruned using checkpoint (a)
(c) - (1) {7P,7P,7},depth=1 considered safe, pruned using checkpoint (b)
For the above line
(c) - (1) {7P,7P,7},depth=1 considered safe, pruned using checkpoint (b)
I would change to
(c) - (1) {7P,7P,7},depth=1
- (0) {42P, 7P, 7},depth = 1 considered safe, pruned using checkpoint (11)
At that point:
- there is a checkpoint at (1) with state {7P,7P,42}
- verifier is at (1) in state {7,7,7}
Thus, verifier won't proceed to (0) because {7,7,7} is states_equal to {7P,7P,42}.
Okay, I think the above example has BPF_F_TEST_STATE_FREQ set as in Patch 3. It will
be great if you can explicitly mention this (BPF_F_TEST_STATE_FREQ) in the commit message.
With this flag,
(c) - (1) {7P,7P,7},depth=1 considered safe, pruned using checkpoint (b)
is correct.
But then for
14 - (2) {7P,7,7},depth=1
15 - (0) {7P,42,7},depth=1 considered safe, pruned using checkpoint (a)
The state
14 - (2) {7P,7,7},depth=1
will have state equal to
7 - (2) {7P,7,42},depth=2
right?
For
14 - (2) {7P,7,7},depth=1
15 - (0) {7P,42,7},depth=1 considered safe, pruned using checkpoint (a)
I suspect for line 15, the pruning uses checking point at line (8).
Right, because checkpoints for a particular insn form a stack. My bad.
Other than the above, the diagram LGTM.
Thank you for the feedback, I'll post v2 shortly.
