On Mon, 2024-02-19 at 16:25 -0800, Yonghong Song wrote: > 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. Will do. [...] > 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? I think you are correct.