On Thu, 2023-09-21 at 19:48 -0700, Andrii Nakryiko wrote:
> Yes, my gut feeling was that if this idea works at all, then ordering
> for this won't matter. The question is if the idea itself is sound.
> Basically, I need to convince myself that subsequent iterations won't
> add any new read/precise marks. You are good at counter examples, so
> maybe you can come up with an example where input state into iteration
> #1 will get more precision marks only at iteration #2 or deeper. If
> that's the case, then this whole idea of postponing loop convergence
> checks probably doesn't work.
Consider the following code:
1. SEC("fentry/" SYS_PREFIX "sys_nanosleep")
2. int num_iter_bug(const void *ctx) {
3. struct bpf_iter_num it;
4. __u64 val = 0;
5. __u64 *ptr = &val;
6. __u64 rnd = bpf_get_current_pid_tgid();
7.
8. bpf_iter_num_new(&it, 0, 10);
9. while (bpf_iter_num_next(&it)) {
10. rnd++;
11. if (rnd == 42) {
12. ptr = (void*)(0xdead);
13. continue;
14. }
15. if (!bpf_iter_num_next(&it))
16. break;
17. bpf_probe_read_user(ptr, 8, (void*)(0xdeadbeef));
18. }
19. bpf_iter_num_destroy(&it);
20. return 0;
21. }
As far as I understand the following verification paths would be
explored (ignoring traces with drained iterators):
- entry:
- 8,9,10,11,12,13:
- at 9 checkpoint (C1) would be created with it{.depth=0,.state=active},ptr=&val;
- at 11 branch (B1) would be created with it{.depth=0,.state=active},ptr=&val;
- jump from 13 to 9 would be postponed with state
it{.depth=0,.state=active},ptr=0xdead as proceeding would increase 'it' depth;
- jump from 11 to 15 (branch B1):
- 15:
- checkpoint would be created with it{.depth=0,.state=active};
- jump from 15 to 17 would be postponed with state
it{.depth=0,.state=active} as proceeding would increase 'it' depth.
- at this point verifier would run out of paths that don't increase
iterators depth and there are two choices:
- (a) jump from 13 to 9 with state it{.depth=0,.state=active},ptr=0xdead;
- (b) jump from 15 to 17 with state it{.depth=0,.state=active},ptr=&val.
If (a) would be processed first there would be no read mark for
'ptr' in C1 yet and verifier runs into to the same issue as with
original example.
Do I miss something or is it a legit counter-example?
> I can't say I understand what exactly you are proposing and how you
> are going to determine these conservative precision marks. But I'd
> like to learn some new ideas, so please elaborate :)
I'll send a follow-up email, trying to figure out what to do with pointers.
