Hello,
For the following program,
0: R1=ctx() R10=fp0
; asm volatile (" \ @
verifier_spill_fill.c:19
0: (b7) r1 = 1024 ; R1_w=1024
1: (63) *(u32 *)(r10 -12) = r1 ; R1_w=1024 R10=fp0 fp-16=mmmm????
2: (61) r1 = *(u32 *)(r10 -12) ;
R1_w=scalar(smin=0,smax=umax=0xffffffff,var_off=(0x0; 0xffffffff))
R10=fp0 fp-16=mmmm????
3: (95) exit
R0 !read_ok
processed 4 insns (limit 1000000) max_states_per_insn 0 total_states 0
peak_states 0 mark_read 0
This is a reduced test case from a real world sched-ext scheduler when
a 32-byte array was maintained on the stack to store some values,
whose values were then used in bounds checking. A known constant was
stored in the array and later refilled into a reg to perform a bounds
check, similar to the example above.
Like in the example, the verifier loses precision for the value r1,
i.e. when it is loaded back from the 4-byte aligned stack slot, the
precise value is lost.
For the actual program, this meant that bounds check produced an
error, as after the fill of the u32 from the u32[N] array, the
verifier didn't see the exact value.
I understand why the verifier has to behave this way, since each
spilled bpf_reg_state maps to one stack slot, and the stack slot maps
to an 8-byte region.
My question is whether this is something that people are interested in
improving longer term, or is it better to suggest people to workaround
such cases?
The real code of course can be "fixed" by making the array u64
instead, and using 8-byte values everywhere, but this doubles the
stack usage (which then has other workarounds, like moving the array
to a map etc.).
Thanks for your response.
