On Wed, May 22, 2024 at 5:02 PM Eduard Zingerman <eddyz87@xxxxxxxxx> wrote:
>
> On Tue, 2024-05-21 at 19:47 -0700, Alexei Starovoitov wrote:
>
> [...]
>
> > Skipping precision mark at if (i > 1000) keeps 'i' imprecise,
> > but arr[i] will mark 'i' as precise anyway, because 'arr' is a map.
> > On the next iteration of the loop the patch does copy_precision()
> > that copies precision markings for top of the loop into next state
> > of the loop. So on the next iteration 'i' will be seen as precise.
>
> Could you please elaborate a bit on why copy_precision() is necessary?
> In general, the main idea of the patch is to skip precision marks in
> certain cases, meaning that strictly more branches would be explored,
> and it does not seem that copy_precision() is needed for safety reasons.
>
> I tried turning copy_precision() off and see a single test failing:
>
> $ ./test_progs -vvv -a iters/task_vma
> ...
> ; bpf_for_each(task_vma, vma, task, 0) { @ iters_task_vma.c:30
> 35: (55) if r0 != 0x0 goto pc-15 21: R0_w=ptr_vm_area_struct(id=1002) R6=1000 R10=fp0 fp-8=iter_task_vma(ref_id=1,state=active,depth=1001) refs=1
> ; if (bpf_cmp_unlikely(seen, >=, 1000)) @ iters_task_vma.c:31
> 21: (35) if r6 >= 0x3e8 goto pc+14 ; R6=1000 refs=1
> ; vm_ranges[seen].vm_start = vma->vm_start; @ iters_task_vma.c:34
> 22: (bf) r1 = r6
> REG INVARIANTS VIOLATION (alu): range bounds violation u64=[0x3e8, 0x3e7] s64=[0x3e8, 0x3e7] u32=[0x3e8, 0x3e7] s32=[0x3e8, 0x3e8] var_off=(0x3e8, 0x0)
> 23: R1_w=1000 R6=1000 refs=1
> 23: (67) r1 <<= 4 ; R1_w=16000 refs=1
> 24: (18) r2 = 0xffffc90000342008 ; R2_w=map_value(map=iters_ta.bss,ks=4,vs=16008,off=8) refs=1
> 26: (0f) r2 += r1 ; R1_w=16000 R2_w=map_value(map=iters_ta.bss,ks=4,vs=16008,off=16008) refs=1
> 27: (79) r1 = *(u64 *)(r0 +0) ; R0_w=ptr_vm_area_struct(id=1002) R1_w=scalar() refs=1
> 28: (7b) *(u64 *)(r2 +0) = r1
> invalid access to map value, value_size=16008 off=16008 size=8
> R2 min value is outside of the allowed memory range
> processed 27035 insns (limit 1000000) max_states_per_insn 65 total_states 2003 peak_states 1008 mark_read 2
Exactly. It's failing without copy_precision().
I didn't add an additional selftest, but I tried to explain
the idea in the commit log.
That's the case where the verifier processes open coded iter
with a bounded loop logic.
Try:
- if (bpf_cmp_unlikely(seen, >=, 1000))
+ if (bpf_cmp_unlikely(seen, ==, 1000))
and it will also pass.
In both cases there will be 27038 processed insn.
All 1k iterations will be checked by the verifier.
That's the main idea.
Let users right normal loops for (i=0; i < 1000 && can_loop; ...)
and if there is no map value access through 'i' the loop
will converge quickly as may_goto.
If not bounded loop logic will quick in for arr[i].
Just like it did for vm_ranges[seen] in this test.
> I wonder, what if we forgo the 'ignore_bad_range' flag and instead
> consider branches with invalid range as impossible?
> E.g. when pred == -2. Or when prediction says that branch would be
> taken and another branch leads to invalid range.
That sounds pretty much like is_branch_taken.
If we don't explore another branch we have to mark the register as precise.
> I'll give it a try later this evening, but still curious about the
> reasoning behind copy_precision().
copy_precision() is kinda the main idea.
Once loop iteration copies precision from header of the loop
the if (dst_reg->precise || src_reg->precise) logic kicks in and
is_branch_taken() starts to work and it becomes bounded loop like
where every iteration states are different.
