Received-SPF: pass (google.com: domain of linux-kernel-owner@vger.kernel.org designates 2620:137:e000::3:8 as permitted sender) client-ip=2620:137:e000::3:8;
MIME-Version: 1.0
References: <CACkBjsbj4y4EhqpV-ZVt645UtERJRTxfEab21jXD1ahPyzH4_g@mail.gmail.com>
 <CAEf4BzZ0xidVCqB47XnkXcNhkPWF6_nTV7yt+_Lf0kcFEut2Mg@mail.gmail.com>
 <CACkBjsaEQxCaZ0ERRnBXduBqdw3MXB5r7naJx_anqxi0Wa-M_Q@mail.gmail.com> <480a5cfefc23446f7c82c5b87eef6306364132b9.camel@gmail.com>
In-Reply-To: <480a5cfefc23446f7c82c5b87eef6306364132b9.camel@gmail.com>
From:   Andrii Nakryiko <andrii.nakryiko@gmail.com>
Date:   Wed, 13 Dec 2023 15:40:34 -0800
Message-ID: <CAEf4BzbfF=aNa-jAkka6YrK6Vbisi=v7PFsEDR-RFuHtAub2Xw@mail.gmail.com>
Subject: Re: [Bug Report] bpf: incorrectly pruning runtime execution path
To:     Eduard Zingerman <eddyz87@gmail.com>
Cc:     Hao Sun <sunhao.th@gmail.com>, Alexei Starovoitov <ast@kernel.org>,
        Andrii Nakryiko <andrii@kernel.org>,
        Daniel Borkmann <daniel@iogearbox.net>,
        bpf <bpf@vger.kernel.org>,
        Linux Kernel Mailing List <linux-kernel@vger.kernel.org>
Content-Type: text/plain; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable
Precedence: bulk

On Wed, Dec 13, 2023 at 3:35=E2=80=AFPM Eduard Zingerman <eddyz87@gmail.com=
> wrote:
>
> On Wed, 2023-12-13 at 11:25 +0100, Hao Sun wrote:
> [...]
>
> > I tried to convert the repro to a valid test case in inline asm, but se=
ems
> > JSET (if r0 & 0xfffffffe goto pc+3) is currently not supported in clang=
-17.
> > Will try after clang-18 is released.
> >
> > #30 is expected to be executed, see below where everything after ";" is
> > the runtime value:
> >    ...
> >    6: (36) if w8 >=3D 0x69 goto pc+1    ; w8 =3D 0xbe, always taken
> >    ...
> >   11: (45) if r0 & 0xfffffffe goto pc+3  ; r0 =3D 0x616, taken
> >   ...
> >   18: (56) if w8 !=3D 0xf goto pc+3     ; w8 not touched, taken
> >   ...
> >   23: (bf) r5 =3D r8     ; w5 =3D 0xbe
> >   24: (18) r2 =3D 0x4
> >   26: (7e) if w8 s>=3D w0 goto pc+5    ; non-taken
> >   27: (4f) r8 |=3D r8
> >   28: (0f) r8 +=3D r8
> >   29: (d6) if w5 s<=3D 0x1d goto pc+2  ; non-taken
> >   30: (18) r0 =3D 0x4      ; executed
> >
> > Since the verifier prunes at #26, #30 is dead and eliminated. So, #30
> > is executed after manually commenting out the dead code rewrite pass.
> >
> > From my understanding, I think r0 should be marked as precise when
> > first backtrack from #29, because r5 range at this point depends on w0
> > as r8 and r5 share the same id at #26.
>
> Hi Hao, Andrii,
>
> I converted program in question to a runnable test, here is a link to
> the patch adding it and disabling dead code removal:
> https://gist.github.com/eddyz87/e888ad70c947f28f94146a47e33cd378
>
> Run the test as follows:
>   ./test_progs -vvv -a verifier_and/pruning_test
>
> And inspect the retval:
>   do_prog_test_run:PASS:bpf_prog_test_run 0 nsec
>   run_subtest:FAIL:647 Unexpected retval: 1353935089 !=3D 4
>
> Note that I tried this test with two functions:
> - bpf_get_current_cgroup_id, with this function I get retval 2, not 4 :)
> - bpf_get_prandom_u32, with this function I get a random retval each time=
.
>
> What is the expectation when 'bpf_get_current_cgroup_id' is used?
> That it is some known (to us) number, but verifier treats it as unknown s=
calar?
>
> Also, I find this portion of the verification log strange:
>
>     ...
>     13: (0f) r0 +=3D r0                     ; R0_w=3Dscalar(smin=3Dsmin32=
=3D0,smax=3Dumax=3Dsmax32=3Dumax32=3D2,
>                                                         var_off=3D(0x0; 0=
x3))
>     14: (2f) r4 *=3D r4                     ; R4_w=3Dscalar()
>     15: (18) r3 =3D 0x1f00000034            ; R3_w=3D0x1f00000034
>     17: (c4) w4 s>>=3D 29                   ; R4_w=3Dscalar(smin=3D0,smax=
=3Dumax=3D0xffffffff,smin32=3D-4,smax32=3D3,
>                                                         var_off=3D(0x0; 0=
xffffffff))
>     18: (56) if w8 !=3D 0xf goto pc+3       ; R8_w=3Dscalar(smin=3D0x8000=
00000000000f,smax=3D0x7fffffff0000000f,
>                                                         umin=3Dsmin32=3Du=
min32=3D15,umax=3D0xffffffff0000000f,
>                                                         smax32=3Dumax32=
=3D15,var_off=3D(0xf; 0xffffffff00000000))
>     19: (d7) r3 =3D bswap32 r3              ; R3_w=3Dscalar()
>     20: (18) r2 =3D 0x1c                    ; R2=3D28
>     22: (67) r4 <<=3D 2                     ; R4_w=3Dscalar(smin=3D0,smax=
=3Dumax=3D0x3fffffffc,
>                                                         smax32=3D0x7fffff=
fc,umax32=3D0xfffffffc,
>                                                         var_off=3D(0x0; 0=
x3fffffffc))
>     23: (bf) r5 =3D r8                      ; R5_w=3Dscalar(id=3D1,smin=
=3D0x800000000000000f,
>                                                         smax=3D0x7fffffff=
0000000f,
>                                                         umin=3Dsmin32=3Du=
min32=3D15,
>                                                         umax=3D0xffffffff=
0000000f,
>                                                         smax32=3Dumax32=
=3D15,
>                                                         var_off=3D(0xf; 0=
xffffffff00000000))
>                                             R8=3Dscalar(id=3D1,smin=3D0x8=
00000000000000f,
>                                                       smax=3D0x7fffffff00=
00000f,
>                                                       umin=3Dsmin32=3Dumi=
n32=3D15,
>                                                       umax=3D0xffffffff00=
00000f,
>                                                       smax32=3Dumax32=3D1=
5,
>                                                       var_off=3D(0xf; 0xf=
fffffff00000000))
>     24: (18) r2 =3D 0x4                     ; R2_w=3D4
>     26: (7e) if w8 s>=3D w0 goto pc+5
>     mark_precise: frame0: last_idx 26 first_idx 22 subseq_idx -1
>     mark_precise: frame0: regs=3Dr5,r8 stack=3D before 24: (18) r2 =3D 0x=
4
>     ...                   ^^^^^^^^^^
>                           ^^^^^^^^^^
> Here w8 =3D=3D 15, w0 in range [0, 2], so the jump is being predicted,
> but for some reason R0 is not among the registers that would be marked pr=
ecise.

It is, as a second step. There are two concatenated precision logs:

mark_precise: frame0: last_idx 26 first_idx 22 subseq_idx -1
mark_precise: frame0: regs=3Dr0 stack=3D before 24: (18) r2 =3D 0x4
mark_precise: frame0: regs=3Dr0 stack=3D before 23: (bf) r5 =3D r8
mark_precise: frame0: regs=3Dr0 stack=3D before 22: (67) r4 <<=3D 2


The issue is elsewhere, see my last email.