Re: [PATCH bpf-next 0/7] bpf: Improve verifier for cond_op and spilled loop index variables

[Yonghong Song <yhs@meta.com>]

On 4/4/23 2:46 PM, Andrii Nakryiko wrote:
> On Wed, Mar 29, 2023 at 10:56 PM Yonghong Song <yhs@fb.com> wrote:
>>
>> LLVM commit [1] introduced hoistMinMax optimization like
>>    (i < VIRTIO_MAX_SGS) && (i < out_sgs)
>> to
>>    upper = MIN(VIRTIO_MAX_SGS, out_sgs)
>>    ... i < upper ...
>> and caused the verification failure. Commit [2] workarounded the issue by
>> adding some bpf assembly code to prohibit the above optimization.
>> This patch improved verifier such that verification can succeed without
>> the above workaround.
>>
>> Without [2], the current verifier will hit the following failures:
>>    ...
>>    119: (15) if r1 == 0x0 goto pc+1
>>    The sequence of 8193 jumps is too complex.
>>    verification time 525829 usec
>>    stack depth 64
>>    processed 156616 insns (limit 1000000) max_states_per_insn 8 total_states 1754 peak_states 1712 mark_read 12
>>    -- END PROG LOAD LOG --
>>    libbpf: prog 'trace_virtqueue_add_sgs': failed to load: -14
>>    libbpf: failed to load object 'loop6.bpf.o'
>>    ...
>> The failure is due to verifier inadequately handling '<const> <cond_op> <non_const>' which will
>> go through both pathes and generate the following verificaiton states:
>>    ...
>>    89: (07) r2 += 1                      ; R2_w=5
>>    90: (79) r8 = *(u64 *)(r10 -48)       ; R8_w=scalar() R10=fp0
>>    91: (79) r1 = *(u64 *)(r10 -56)       ; R1_w=scalar(umax=5,var_off=(0x0; 0x7)) R10=fp0
>>    92: (ad) if r2 < r1 goto pc+41        ; R0_w=scalar() R1_w=scalar(umin=6,umax=5,var_off=(0x4; 0x3))
> 
> offtopic, but if this is a real output, then something is wrong with
> scratching register logic for conditional, it should have emitted
> states of R1 and R2, maybe you can take a look while working on this
> patch set?

Yes, this is the real output. Yes, the above R1_w should be an 
impossible state. This is what this patch tries to fix.
I am not what verifier should do if this state indeed happens,
return an -EFAULT or something?

> 
>>        R2_w=5 R6_w=scalar(id=385) R7_w=0 R8_w=scalar() R9_w=scalar(umax=21474836475,var_off=(0x0; 0x7ffffffff))
>>        R10=fp0 fp-8=mmmmmmmm fp-16=mmmmmmmm fp-24=mmmm???? fp-32= fp-40_w=4 fp-48=mmmmmmmm fp-56= fp-64=mmmmmmmm
>>    ...
>>    89: (07) r2 += 1                      ; R2_w=6
>>    90: (79) r8 = *(u64 *)(r10 -48)       ; R8_w=scalar() R10=fp0
>>    91: (79) r1 = *(u64 *)(r10 -56)       ; R1_w=scalar(umax=5,var_off=(0x0; 0x7)) R10=fp0
>>    92: (ad) if r2 < r1 goto pc+41        ; R0_w=scalar() R1_w=scalar(umin=7,umax=5,var_off=(0x4; 0x3))
>>        R2_w=6 R6=scalar(id=388) R7=0 R8_w=scalar() R9_w=scalar(umax=25769803770,var_off=(0x0; 0x7ffffffff))
>>        R10=fp0 fp-8=mmmmmmmm fp-16=mmmmmmmm fp-24=mmmm???? fp-32= fp-40=5 fp-48=mmmmmmmm fp-56= fp-64=mmmmmmmm
>>      ...
>>    89: (07) r2 += 1                      ; R2_w=4088
>>    90: (79) r8 = *(u64 *)(r10 -48)       ; R8_w=scalar() R10=fp0
>>    91: (79) r1 = *(u64 *)(r10 -56)       ; R1_w=scalar(umax=5,var_off=(0x0; 0x7)) R10=fp0
>>    92: (ad) if r2 < r1 goto pc+41        ; R0=scalar() R1=scalar(umin=4089,umax=5,var_off=(0x0; 0x7))
>>        R2=4088 R6=scalar(id=12634) R7=0 R8=scalar() R9=scalar(umax=17557826301960,var_off=(0x0; 0xfffffffffff))
>>        R10=fp0 fp-8=mmmmmmmm fp-16=mmmmmmmm fp-24=mmmm???? fp-32= fp-40=4087 fp-48=mmmmmmmm fp-56= fp-64=mmmmmmmm
>>
>> Patch 3 fixed the above issue by handling '<const> <cond_op> <non_const>' properly.
>> During developing selftests for Patch 3, I found some issues with bound deduction with
>> BPF_EQ/BPF_NE and fixed the issue in Patch 1.
[...]