Cupertino Miranda writes: > Alexei Starovoitov writes: > >> On Fri, Apr 5, 2024 at 3:08 PM Cupertino Miranda >> <cupertino.miranda@xxxxxxxxxx> wrote: >>> >>> Hi everyone, >>> >>> This email is a follow up on the problem identified in >>> https://github.com/systemd/systemd/issues/31888. >>> This problem first shown as a result of a GCC compilation for BPF that ends >>> converting a condition based decision tree, into a logic based one (making use >>> of XOR), in order to compute expected return value for the function. >>> >>> This issue was also reported in >>> https://gcc.gnu.org/bugzilla/show_bug.cgi?id=114523 and contains both >>> the original reproducer pattern and some other that also fails within clang. >>> >>> I have included a patch that contains a possible fix (I wonder) and a test case >>> that reproduces the issue in attach. >>> The execution of the test without the included fix results in: >>> >>> VERIFIER LOG: >>> ============= >>> Global function reg32_0_reg32_xor_reg_01() doesn't return scalar. Only those are supported. >>> 0: R1=ctx() R10=fp0 >>> ; asm volatile (" \ @ verifier_bounds.c:755 >>> 0: (85) call bpf_get_prandom_u32#7 ; R0_w=scalar() >>> 1: (bf) r6 = r0 ; R0_w=scalar(id=1) R6_w=scalar(id=1) >>> 2: (b7) r1 = 0 ; R1_w=0 >>> 3: (7b) *(u64 *)(r10 -8) = r1 ; R1_w=0 R10=fp0 fp-8_w=0 >>> 4: (bf) r2 = r10 ; R2_w=fp0 R10=fp0 >>> 5: (07) r2 += -8 ; R2_w=fp-8 >>> 6: (18) r1 = 0xffff8e8ec3b99000 ; R1_w=map_ptr(map=map_hash_8b,ks=8,vs=8) >>> 8: (85) call bpf_map_lookup_elem#1 ; R0=map_value_or_null(id=2,map=map_hash_8b,ks=8,vs=8) >>> 9: (55) if r0 != 0x0 goto pc+1 11: R0=map_value(map=map_hash_8b,ks=8,vs=8) R6=scalar(id=1) R10=fp0 fp-8=mmmmmmmm >>> 11: (b4) w1 = 0 ; R1_w=0 >>> 12: (77) r6 >>= 63 ; R6_w=scalar(smin=smin32=0,smax=umax=smax32=umax32=1,var_off=(0x0; 0x1)) >>> 13: (ac) w1 ^= w6 ; R1_w=scalar() R6_w=scalar(smin=smin32=0,smax=umax=smax32=umax32=1,var_off=(0x0; 0x1)) >>> 14: (16) if w1 == 0x0 goto pc+2 ; R1_w=scalar(smin=0x8000000000000001,umin=umin32=1) >>> 15: (16) if w1 == 0x1 goto pc+1 ; R1_w=scalar(smin=0x8000000000000002,umin=umin32=2) >>> 16: (79) r0 = *(u64 *)(r0 +8) >>> invalid access to map value, value_size=8 off=8 size=8 >>> R0 min value is outside of the allowed memory range >>> processed 16 insns (limit 1000000) max_states_per_insn 0 total_states 1 peak_states 1 mark_read 1 >>> ============= >>> >>> The test collects a random number and shifts it right by 63 bits to reduce its >>> range to (0,1), which will then xor to compute the value of w1, checking >>> if the value is either 0 or 1 after. >>> By analysing the code and the ranges computations, one can easily deduce >>> that the result of the XOR is also within the range (0,1), however: >>> >>> 11: (b4) w1 = 0 ; R1_w=0 >>> 12: (77) r6 >>= 63 ; R6_w=scalar(smin=smin32=0,smax=umax=smax32=umax32=1,var_off=(0x0; 0x1)) >>> 13: (ac) w1 ^= w6 ; R1_w=scalar() R6_w=scalar(smin=smin32=0,smax=umax=smax32=umax32=1,var_off=(0x0; 0x1)) >>> ^ >>> |___ No range is computed for R1 >>> >> >> I'm missing why gcc generates insn 11 and 13 ? >> The later checks can compare r6 directly, right? >> The bugzilla links are too long to read. > > The code above is just some inline assembly in my patch that reproduces > the specific GCC issue in the verifier. > If you want to see the code GCC produces you can check in the systemd > github issue. > > Thanks, > Cupertino > Here is the log of the verifier from the code that GCC emitted. Mär 26 23:57:12 H systemd[1]: 0: R1=ctx(off=0,imm=0) R10=fp0 Mär 26 23:57:12 H systemd[1]: 0: (61) r0 = *(u32 *)(r1 +40) ; R0_w=scalar(smin=0,smax=umax=4294967295,var_off=(0x0; 0xffffffff)) R1=ctx(off=0,imm=0) Mär 26 23:57:12 H systemd[1]: 1: (bf) r2 = r10 ; R2_w=fp0 R10=fp0 Mär 26 23:57:12 H systemd[1]: 2: (18) r1 = 0xffff8ef68fd28400 ; R1_w=map_ptr(off=0,ks=4,vs=1,imm=0) Mär 26 23:57:12 H systemd[1]: 4: (07) r2 += -4 ; R2_w=fp-4 Mär 26 23:57:12 H systemd[1]: 5: (63) *(u32 *)(r10 -4) = r0 ; R0_w=scalar(smin=0,smax=umax=4294967295,var_off=(0x0; 0xffffffff)) R10=fp0 fp-8=mmmm???? Mär 26 23:57:12 H systemd[1]: 6: (85) call bpf_map_lookup_elem#1 ; R0_w=map_value_or_null(id=1,off=0,ks=4,vs=1,imm=0) Mär 26 23:57:12 H systemd[1]: 7: (18) r1 = 0xffffb290805b6000 ; R1_w=map_value(off=0,ks=4,vs=1,imm=0) Mär 26 23:57:12 H systemd[1]: 9: (71) r3 = *(u8 *)(r1 +0) ; R1_w=map_value(off=0,ks=4,vs=1,imm=0) R3_w=1 Mär 26 23:57:12 H systemd[1]: 10: (bf) r2 = r0 ; R0_w=map_value_or_null(id=1,off=0,ks=4,vs=1,imm=0) R2_w=map_value_or_null(id=1,off=0,ks=4,vs=1,imm=0) Mär 26 23:57:12 H systemd[1]: 11: (57) r3 &= 255 ; R3_w=1 Mär 26 23:57:12 H systemd[1]: 12: (b7) r0 = 1 ; R0_w=1 Mär 26 23:57:12 H systemd[1]: 13: (15) if r2 == 0x0 goto pc+1 ; R2_w=map_value(off=0,ks=4,vs=1,imm=0) Mär 26 23:57:12 H systemd[1]: 14: (b7) r0 = 0 ; R0=0 Mär 26 23:57:12 H systemd[1]: 15: (87) r3 = -r3 ; R3_w=scalar() Mär 26 23:57:12 H systemd[1]: 16: (77) r3 >>= 63 ; R3_w=scalar(smin=smin32=0,smax=umax=smax32=umax32=1,var_off=(0x0; 0x1)) Mär 26 23:57:12 H systemd[1]: 17: (ac) w0 ^= w3 ; R0_w=scalar() R3_w=scalar(smin=smin32=0,smax=umax=smax32=umax32=1,var_off=(0x0; 0x1)) Mär 26 23:57:12 H systemd[1]: 18: (57) r0 &= 255 ; R0_w=scalar(smin=smin32=0,smax=umax=smax32=umax32=255,var_off=(0x0; 0xff)) Mär 26 23:57:12 H systemd[1]: 19: (95) exit Mär 26 23:57:12 H systemd[1]: At program exit the register R0 has value (0x0; 0xff) should have been in (0x0; 0x3) Mär 26 23:57:12 H systemd[1]: processed 18 insns (limit 1000000) max_states_per_insn 0 total_states 1 peak_states 1 mark_read 1 Mär 26 23:57:12 H systemd[1]: -- END PROG LOAD LOG -- > >> >>> Is this really a requirement for XOR (and OR) ? >> >> As Yonghong said, no one had the use case to make the verifier smarter, >> so pls send an official patch.
