R2 max value is outside of the allowed memory range after explicit bounds checking

Question

I've been trying to understand how the eBPF Verifier works, but I don't have enough experience with reading its output properly. I perform explicit bounds checking on the index, and llvm-objdump shows that the compiled object has it as well.

---

eBPF Program:

int a[5],b=3,i=2;

SEC("xdp")
int hello(void *ctx){
    if(i > 0 && i < sizeof(a)){
        a[i] = b;
    }
    return XDP_PASS;
}

---

llvm-objdump -S output:

my-prog.xdp.o:  file format elf64-bpf

Disassembly of section xdp:

0000000000000000 <hello>:
;     if(i > 0 && i < sizeof(a)){
       0:       18 01 00 00 00 00 00 00 00 00 00 00 00 00 00 00 r1 = 0x0 ll
       2:       61 11 00 00 00 00 00 00 r1 = *(u32 *)(r1 + 0x0)
       3:       bf 12 00 00 00 00 00 00 r2 = r1
       4:       67 02 00 00 20 00 00 00 r2 <<= 0x20
       5:       c7 02 00 00 20 00 00 00 r2 s>>= 0x20
       6:       b7 03 00 00 01 00 00 00 r3 = 0x1
       7:       6d 23 09 00 00 00 00 00 if r3 s> r2 goto +0x9 <LBB0_3>
       8:       25 01 08 00 13 00 00 00 if r1 > 0x13 goto +0x8 <LBB0_3>
;         a[i] = b;
       9:       67 01 00 00 02 00 00 00 r1 <<= 0x2
      10:       18 02 00 00 00 00 00 00 00 00 00 00 00 00 00 00 r2 = 0x0 ll
      12:       0f 12 00 00 00 00 00 00 r2 += r1
      13:       18 01 00 00 00 00 00 00 00 00 00 00 00 00 00 00 r1 = 0x0 ll
      15:       61 11 00 00 00 00 00 00 r1 = *(u32 *)(r1 + 0x0)
      16:       63 12 00 00 00 00 00 00 *(u32 *)(r2 + 0x0) = r1

0000000000000088 <LBB0_3>:
;     return XDP_PASS;
      17:       b7 00 00 00 02 00 00 00 r0 = 0x2
      18:       95 00 00 00 00 00 00 00 exit

---

Relevant Verifier output after trying to load with bpftool -d:

libbpf: prog 'hello': -- BEGIN PROG LOAD LOG --
func#0 @0
reg type unsupported for arg#0 function hello#4
0: R1=ctx(off=0,imm=0) R10=fp0
; if(i > 0 && i < sizeof(a)){
0: (18) r1 = 0xffffb59ac0fa2004       ; R1_w=map_value(off=4,ks=4,vs=8,imm=0)
2: (61) r1 = *(u32 *)(r1 +0)          ; R1_w=scalar(umax=4294967295,var_off=(0x0; 0xffffffff))
3: (bf) r2 = r1                       ; R1_w=scalar(id=1,umax=4294967295,var_off=(0x0; 0xffffffff)) R2_w=scalar(id=1,umax=4294967295,var_off=(0x0; 0xffffffff))
4: (67) r2 <<= 32                     ; R2_w=scalar(smax=9223372032559808512,umax=18446744069414584320,var_off=(0x0; 0xffffffff00000000),s32_min=0,s32_max=0,u32_max=0)
5: (c7) r2 s>>= 32                    ; R2_w=scalar(smin=-2147483648,smax=2147483647)
6: (b7) r3 = 1                        ; R3_w=1
; if(i > 0 && i < sizeof(a)){
7: (6d) if r3 s> r2 goto pc+9         ; R2_w=scalar(umin=1,umax=2147483647,var_off=(0x0; 0x7fffffff)) R3_w=1
; if(i > 0 && i < sizeof(a)){
8: (25) if r1 > 0x13 goto pc+8        ; R1_w=scalar(id=1,umax=19,var_off=(0x0; 0x1f))
; a[i] = b;
9: (67) r1 <<= 2                      ; R1_w=scalar(umax=76,var_off=(0x0; 0x7c))
10: (18) r2 = 0xffffb59ac0faa000      ; R2_w=map_value(off=0,ks=4,vs=20,imm=0)
12: (0f) r2 += r1
mark_precise: frame0: last_idx 12 first_idx 0 subseq_idx -1 
mark_precise: frame0: regs=r1 stack= before 10: (18) r2 = 0xffffb59ac0faa000
mark_precise: frame0: regs=r1 stack= before 9: (67) r1 <<= 2
mark_precise: frame0: regs=r1 stack= before 8: (25) if r1 > 0x13 goto pc+8
mark_precise: frame0: regs=r1 stack= before 7: (6d) if r3 s> r2 goto pc+9
mark_precise: frame0: regs=r1 stack= before 6: (b7) r3 = 1
mark_precise: frame0: regs=r1 stack= before 5: (c7) r2 s>>= 32
mark_precise: frame0: regs=r1 stack= before 4: (67) r2 <<= 32
mark_precise: frame0: regs=r1 stack= before 3: (bf) r2 = r1
mark_precise: frame0: regs=r1 stack= before 2: (61) r1 = *(u32 *)(r1 +0)
13: R1_w=scalar(umax=76,var_off=(0x0; 0x7c)) R2_w=map_value(off=0,ks=4,vs=20,umax=76,var_off=(0x0; 0x7c),s32_max=124,u32_max=124)
; a[i] = b;
13: (18) r1 = 0xffffb59ac0fa2000      ; R1_w=map_value(off=0,ks=4,vs=8,imm=0)
15: (61) r1 = *(u32 *)(r1 +0)         ; R1_w=scalar(umax=4294967295,var_off=(0x0; 0xffffffff))
; a[i] = b;
16: (63) *(u32 *)(r2 +0) = r1
invalid access to map value, value_size=20 off=76 size=4
R2 max value is outside of the allowed memory range
verification time 119 usec
stack depth 0
processed 14 insns (limit 1000000) max_states_per_insn 0 total_states 0 peak_states 0 mark_read 0
-- END PROG LOAD LOG --

I also don't understand what the bitshifts in the compiled object file are present for (r2 <<= 0x20).

Thanks for stopping by!