Re: [PATCH bpf-next 2/4] bpf: Track delta between "linked" registers.

[Eduard Zingerman <eddyz87@gmail.com>]

On Fri, 2024-06-07 at 17:44 -0700, Alexei Starovoitov wrote:
> From: Alexei Starovoitov <ast@kernel.org>
> 
> Compilers can generate the code
>   r1 = r2
>   r1 += 0x1
>   if r2 < 1000 goto ...
>   use knowledge of r2 range in subsequent r1 operations
> 
> So remember constant delta between r2 and r1 and update r1 after 'if' condition.
> 
> Unfortunately LLVM still uses this pattern for loops with 'can_loop' construct:
> for (i = 0; i < 1000 && can_loop; i++)
> 
> The "undo" pass was introduced in LLVM
> https://reviews.llvm.org/D121937
> to prevent this optimization, but it cannot cover all cases.
> Instead of fighting middle end optimizer in BPF backend teach the verifier
> about this pattern.

I like this idea.
In theory it could be generalized to handle situations when LLVM
uses two counters in parallel:

r0 = 0 // as an index
r1 = 0 // as a pointer
...
r0 += 1
r1 += 8

> 
> Signed-off-by: Alexei Starovoitov <ast@kernel.org>
> ---

[...]

> @@ -15088,13 +15130,43 @@ static bool try_match_pkt_pointers(const struct bpf_insn *insn,
>  static void find_equal_scalars(struct bpf_verifier_state *vstate,
>  			       struct bpf_reg_state *known_reg)
>  {
> +	struct bpf_reg_state fake_reg;
>  	struct bpf_func_state *state;
>  	struct bpf_reg_state *reg;
>  
>  	bpf_for_each_reg_in_vstate(vstate, state, reg, ({
> -		if (reg->type == SCALAR_VALUE && reg->id == known_reg->id)
> +		if (reg->type != SCALAR_VALUE || reg == known_reg)
> +			continue;
> +		if ((reg->id & ~BPF_ADD_CONST) != (known_reg->id & ~BPF_ADD_CONST))
> +			continue;
> +		if ((reg->id & BPF_ADD_CONST) == (known_reg->id & BPF_ADD_CONST)) {
>  			copy_register_state(reg, known_reg);
> +		} else if ((reg->id & BPF_ADD_CONST) && reg->off) {
> +			/* reg = known_reg; reg += const */
> +			copy_register_state(reg, known_reg);
> +
> +			fake_reg.type = SCALAR_VALUE;
> +			__mark_reg_known(&fake_reg, reg->off);
> +			scalar32_min_max_add(reg, &fake_reg);
> +			scalar_min_max_add(reg, &fake_reg);
> +			reg->var_off = tnum_add(reg->var_off, fake_reg.var_off);
> +			reg->off = 0;
> +			reg->id &= ~BPF_ADD_CONST;
> +		} else if ((known_reg->id & BPF_ADD_CONST) && known_reg->off) {
> +			/* reg = known_reg; reg -= const' */
> +			copy_register_state(reg, known_reg);
> +
> +			fake_reg.type = SCALAR_VALUE;
> +			__mark_reg_known(&fake_reg, known_reg->off);
> +			scalar32_min_max_sub(reg, &fake_reg);
> +			scalar_min_max_sub(reg, &fake_reg);
> +			reg->var_off = tnum_sub(reg->var_off, fake_reg.var_off);
> +		}

I think that copy_register_state logic is off here,
the copy overwrites reg->off before it is used to update the value.
The following test is marked as safe for me, while it should not:

char buf[10] SEC(".data.buf");

SEC("socket")
__failure
__msg("*(u8 *)(r7 +0) = r0")
__msg("invalid access to map value, value_size=10 off=9 size=1")
__naked void check_add_const_3regs(void)
{
	asm volatile (
	"r6 = %[buf];"
	"r7 = %[buf];"
	"call %[bpf_ktime_get_ns];"
	"r1 = r0;"		/* link r0.id == r1.id == r2.id */
	"r2 = r0;"
	"r1 += 1;"		/* r1 == r0+1 */
	"r2 += 2;"		/* r2 == r0+2 */
	"if r0 > 8 goto 1f;"	/* r0 range [0, 8]  */
	"r6 += r1;"		/* r1 range [1, 9]  */
	"r7 += r2;"		/* r2 range [2, 10] */
	"*(u8 *)(r6 +0) = r0;"	/* safe, within bounds   */
	"*(u8 *)(r7 +0) = r0;"	/* unsafe, out of bounds */
	"1: exit;"
	:
	: __imm(bpf_ktime_get_ns),
	  __imm_ptr(buf)
	: __clobber_common);
}

The conditional r0 > 8 propagates same range for r{0,1,2}:

7: (07) r1 += 1                       ; R1_w=scalar(id=1+1)
8: (07) r2 += 2                       ; R2_w=scalar(id=1+2)
9: (25) if r0 > 0x8 goto pc+4         ; R0_w=scalar(id=1,smin=smin32=0,smax=umax=smax32=umax32=8,var_off=(0x0; 0xf))
10: (0f) r6 += r1
11: R1_w=scalar(id=1,smin=smin32=0,smax=umax=smax32=umax32=8,var_off=(0x0; 0xf)) R6_w=...
11: (0f) r7 += r2
12: R2_w=scalar(id=1,smin=smin32=0,smax=umax=smax32=umax32=8,var_off=(0x0; 0xf)) R7_w=...


>  	}));
> +	if (known_reg->id & BPF_ADD_CONST) {
> +		known_reg->id = 0;
> +		known_reg->off = 0;
> +	}
>  }
>  
>  static int check_cond_jmp_op(struct bpf_verifier_env *env,