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. > 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.
