bpf.vger.kernel.org archive mirror
 help / color / mirror / Atom feed
* [PATCH bpf-next 0/7] bpf: Improve verifier for cond_op and spilled loop index variables
@ 2023-03-30  5:56 Yonghong Song
  2023-03-30  5:56 ` [PATCH bpf-next 1/7] bpf: Improve verifier JEQ/JNE insn branch taken checking Yonghong Song
                   ` (7 more replies)
  0 siblings, 8 replies; 26+ messages in thread
From: Yonghong Song @ 2023-03-30  5:56 UTC (permalink / raw)
  To: bpf
  Cc: Alexei Starovoitov, Andrii Nakryiko, Daniel Borkmann,
	kernel-team, Martin KaFai Lau

LLVM commit [1] introduced hoistMinMax optimization like
  (i < VIRTIO_MAX_SGS) && (i < out_sgs)
to
  upper = MIN(VIRTIO_MAX_SGS, out_sgs)
  ... i < upper ...
and caused the verification failure. Commit [2] workarounded the issue by
adding some bpf assembly code to prohibit the above optimization.
This patch improved verifier such that verification can succeed without
the above workaround.

Without [2], the current verifier will hit the following failures:
  ...
  119: (15) if r1 == 0x0 goto pc+1      
  The sequence of 8193 jumps is too complex.
  verification time 525829 usec
  stack depth 64
  processed 156616 insns (limit 1000000) max_states_per_insn 8 total_states 1754 peak_states 1712 mark_read 12
  -- END PROG LOAD LOG --
  libbpf: prog 'trace_virtqueue_add_sgs': failed to load: -14
  libbpf: failed to load object 'loop6.bpf.o'
  ...
The failure is due to verifier inadequately handling '<const> <cond_op> <non_const>' which will
go through both pathes and generate the following verificaiton states:
  ...
  89: (07) r2 += 1                      ; R2_w=5
  90: (79) r8 = *(u64 *)(r10 -48)       ; R8_w=scalar() R10=fp0
  91: (79) r1 = *(u64 *)(r10 -56)       ; R1_w=scalar(umax=5,var_off=(0x0; 0x7)) R10=fp0
  92: (ad) if r2 < r1 goto pc+41        ; R0_w=scalar() R1_w=scalar(umin=6,umax=5,var_off=(0x4; 0x3))
      R2_w=5 R6_w=scalar(id=385) R7_w=0 R8_w=scalar() R9_w=scalar(umax=21474836475,var_off=(0x0; 0x7ffffffff))
      R10=fp0 fp-8=mmmmmmmm fp-16=mmmmmmmm fp-24=mmmm???? fp-32= fp-40_w=4 fp-48=mmmmmmmm fp-56= fp-64=mmmmmmmm    
  ...
  89: (07) r2 += 1                      ; R2_w=6
  90: (79) r8 = *(u64 *)(r10 -48)       ; R8_w=scalar() R10=fp0
  91: (79) r1 = *(u64 *)(r10 -56)       ; R1_w=scalar(umax=5,var_off=(0x0; 0x7)) R10=fp0
  92: (ad) if r2 < r1 goto pc+41        ; R0_w=scalar() R1_w=scalar(umin=7,umax=5,var_off=(0x4; 0x3))
      R2_w=6 R6=scalar(id=388) R7=0 R8_w=scalar() R9_w=scalar(umax=25769803770,var_off=(0x0; 0x7ffffffff))
      R10=fp0 fp-8=mmmmmmmm fp-16=mmmmmmmm fp-24=mmmm???? fp-32= fp-40=5 fp-48=mmmmmmmm fp-56= fp-64=mmmmmmmm
    ...
  89: (07) r2 += 1                      ; R2_w=4088
  90: (79) r8 = *(u64 *)(r10 -48)       ; R8_w=scalar() R10=fp0
  91: (79) r1 = *(u64 *)(r10 -56)       ; R1_w=scalar(umax=5,var_off=(0x0; 0x7)) R10=fp0
  92: (ad) if r2 < r1 goto pc+41        ; R0=scalar() R1=scalar(umin=4089,umax=5,var_off=(0x0; 0x7))
      R2=4088 R6=scalar(id=12634) R7=0 R8=scalar() R9=scalar(umax=17557826301960,var_off=(0x0; 0xfffffffffff))
      R10=fp0 fp-8=mmmmmmmm fp-16=mmmmmmmm fp-24=mmmm???? fp-32= fp-40=4087 fp-48=mmmmmmmm fp-56= fp-64=mmmmmmmm

Patch 3 fixed the above issue by handling '<const> <cond_op> <non_const>' properly.
During developing selftests for Patch 3, I found some issues with bound deduction with
BPF_EQ/BPF_NE and fixed the issue in Patch 1.

After the above issue is fixed, the second issue shows up.
  ...
  67: (07) r1 += -16                    ; R1_w=fp-16
  ; bpf_probe_read_kernel(&sgp, sizeof(sgp), sgs + i);
  68: (b4) w2 = 8                       ; R2_w=8
  69: (85) call bpf_probe_read_kernel#113       ; R0_w=scalar() fp-16=mmmmmmmm
  ; return sgp;
  70: (79) r6 = *(u64 *)(r10 -16)       ; R6=scalar() R10=fp0
  ; for (n = 0, sgp = get_sgp(sgs, i); sgp && (n < SG_MAX);
  71: (15) if r6 == 0x0 goto pc-49      ; R6=scalar()
  72: (b4) w1 = 0                       ; R1_w=0
  73: (05) goto pc-46
  ; for (i = 0; (i < VIRTIO_MAX_SGS) && (i < out_sgs); i++) {
  28: (bc) w7 = w1                      ; R1_w=0 R7_w=0
  ; bpf_probe_read_kernel(&len, sizeof(len), &sgp->length);
  ...
  23: (79) r3 = *(u64 *)(r10 -40)       ; R3_w=2 R10=fp0
  ; for (i = 0; (i < VIRTIO_MAX_SGS) && (i < out_sgs); i++) {
  24: (07) r3 += 1                      ; R3_w=3
  ; for (i = 0; (i < VIRTIO_MAX_SGS) && (i < out_sgs); i++) {
  25: (79) r1 = *(u64 *)(r10 -56)       ; R1_w=scalar(umax=5,var_off=(0x0; 0x7)) R10=fp0
  26: (ad) if r3 < r1 goto pc+34 61: R0=scalar() R1_w=scalar(umin=4,umax=5,var_off=(0x4; 0x1)) R3_w=3 R6=scalar(id=1658)
     R7=0 R8=scalar(id=1653) R9=scalar(umax=4294967295,var_off=(0x0; 0xffffffff)) R10=fp0 fp-8=mmmmmmmm fp-16=mmmmmmmm
     fp-24=mmmm???? fp-32= fp-40=2 fp-56= fp-64=mmmmmmmm
  ; if (sg_is_chain(&sg))               
  61: (7b) *(u64 *)(r10 -40) = r3       ; R3_w=3 R10=fp0 fp-40_w=3
    ...
  67: (07) r1 += -16                    ; R1_w=fp-16
  ; bpf_probe_read_kernel(&sgp, sizeof(sgp), sgs + i);
  68: (b4) w2 = 8                       ; R2_w=8
  69: (85) call bpf_probe_read_kernel#113       ; R0_w=scalar() fp-16=mmmmmmmm
  ; return sgp;
  70: (79) r6 = *(u64 *)(r10 -16)       
  ; for (n = 0, sgp = get_sgp(sgs, i); sgp && (n < SG_MAX);
  infinite loop detected at insn 71     
  verification time 90800 usec
  stack depth 64
  processed 25017 insns (limit 1000000) max_states_per_insn 20 total_states 491 peak_states 169 mark_read 12
  -- END PROG LOAD LOG --
  libbpf: prog 'trace_virtqueue_add_sgs': failed to load: -22

Further analysis found the index variable 'i' is spilled but since it is not marked as precise, regsafe will ignore
comparison since they are scalar values.

Since it is hard for verifier to determine whether a particular scalar is index variable or not, Patch 5 implemented
a heuristic such that if both old and new reg states are constant, mark the old one as precise to force scalar value
comparison and this fixed the problem.

The rest of patches are selftests related.

  [1] https://reviews.llvm.org/D143726
  [2] Commit 3c2611bac08a ("selftests/bpf: Fix trace_virtqueue_add_sgs test issue with LLVM 17.")

Yonghong Song (7):
  bpf: Improve verifier JEQ/JNE insn branch taken checking
  selftests/bpf: Add tests for non-constant cond_op NE/EQ bound
    deduction
  bpf: Improve handling of pattern '<const> <cond_op> <non_const>' in
    verifier
  selftests/bpf: Add verifier tests for code pattern '<const> <cond_op>
    <non_const>'
  bpf: Mark potential spilled loop index variable as precise
  selftests/bpf: Remove previous workaround for test verif_scale_loop6
  selftests/bpf: Add a new test based on loop6.c

 kernel/bpf/verifier.c                         |  40 +-
 .../bpf/prog_tests/bpf_verif_scale.c          |   5 +
 .../selftests/bpf/prog_tests/verifier.c       |   2 +
 tools/testing/selftests/bpf/progs/loop6.c     |   2 -
 tools/testing/selftests/bpf/progs/loop7.c     | 102 ++++
 .../verifier_bounds_deduction_non_const.c     | 553 ++++++++++++++++++
 .../progs/verifier_bounds_mix_sign_unsign.c   |   2 +-
 7 files changed, 701 insertions(+), 5 deletions(-)
 create mode 100644 tools/testing/selftests/bpf/progs/loop7.c
 create mode 100644 tools/testing/selftests/bpf/progs/verifier_bounds_deduction_non_const.c

-- 
2.34.1


^ permalink raw reply	[flat|nested] 26+ messages in thread

* [PATCH bpf-next 1/7] bpf: Improve verifier JEQ/JNE insn branch taken checking
  2023-03-30  5:56 [PATCH bpf-next 0/7] bpf: Improve verifier for cond_op and spilled loop index variables Yonghong Song
@ 2023-03-30  5:56 ` Yonghong Song
  2023-03-30 21:14   ` Dave Marchevsky
  2023-03-30  5:56 ` [PATCH bpf-next 2/7] selftests/bpf: Add tests for non-constant cond_op NE/EQ bound deduction Yonghong Song
                   ` (6 subsequent siblings)
  7 siblings, 1 reply; 26+ messages in thread
From: Yonghong Song @ 2023-03-30  5:56 UTC (permalink / raw)
  To: bpf
  Cc: Alexei Starovoitov, Andrii Nakryiko, Daniel Borkmann,
	kernel-team, Martin KaFai Lau

Currently, for BPF_JEQ/BPF_JNE insn, verifier determines
whether the branch is taken or not only if both operands
are constants. Therefore, for the following code snippet,
  0: (85) call bpf_ktime_get_ns#5       ; R0_w=scalar()
  1: (a5) if r0 < 0x3 goto pc+2         ; R0_w=scalar(umin=3)
  2: (b7) r2 = 2                        ; R2_w=2
  3: (1d) if r0 == r2 goto pc+2 6

At insn 3, since r0 is not a constant, verifier assumes both branch
can be taken which may lead inproper verification failure.

Add comparing umin value and the constant. If the umin value
is greater than the constant, for JEQ the branch must be
not-taken, and for JNE the branch must be taken.
The jmp32 mode JEQ/JNE branch taken checking is also
handled similarly.

Signed-off-by: Yonghong Song <yhs@fb.com>
---
 kernel/bpf/verifier.c | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c
index 20eb2015842f..90bb6d25bc9c 100644
--- a/kernel/bpf/verifier.c
+++ b/kernel/bpf/verifier.c
@@ -12597,10 +12597,14 @@ static int is_branch32_taken(struct bpf_reg_state *reg, u32 val, u8 opcode)
 	case BPF_JEQ:
 		if (tnum_is_const(subreg))
 			return !!tnum_equals_const(subreg, val);
+		else if (reg->u32_min_value > val)
+			return 0;
 		break;
 	case BPF_JNE:
 		if (tnum_is_const(subreg))
 			return !tnum_equals_const(subreg, val);
+		else if (reg->u32_min_value > val)
+			return 1;
 		break;
 	case BPF_JSET:
 		if ((~subreg.mask & subreg.value) & val)
@@ -12670,10 +12674,14 @@ static int is_branch64_taken(struct bpf_reg_state *reg, u64 val, u8 opcode)
 	case BPF_JEQ:
 		if (tnum_is_const(reg->var_off))
 			return !!tnum_equals_const(reg->var_off, val);
+		else if (reg->umin_value > val)
+			return 0;
 		break;
 	case BPF_JNE:
 		if (tnum_is_const(reg->var_off))
 			return !tnum_equals_const(reg->var_off, val);
+		else if (reg->umin_value > val)
+			return 1;
 		break;
 	case BPF_JSET:
 		if ((~reg->var_off.mask & reg->var_off.value) & val)
-- 
2.34.1


^ permalink raw reply related	[flat|nested] 26+ messages in thread

* [PATCH bpf-next 2/7] selftests/bpf: Add tests for non-constant cond_op NE/EQ bound deduction
  2023-03-30  5:56 [PATCH bpf-next 0/7] bpf: Improve verifier for cond_op and spilled loop index variables Yonghong Song
  2023-03-30  5:56 ` [PATCH bpf-next 1/7] bpf: Improve verifier JEQ/JNE insn branch taken checking Yonghong Song
@ 2023-03-30  5:56 ` Yonghong Song
  2023-03-30  5:56 ` [PATCH bpf-next 3/7] bpf: Improve handling of pattern '<const> <cond_op> <non_const>' in verifier Yonghong Song
                   ` (5 subsequent siblings)
  7 siblings, 0 replies; 26+ messages in thread
From: Yonghong Song @ 2023-03-30  5:56 UTC (permalink / raw)
  To: bpf
  Cc: Alexei Starovoitov, Andrii Nakryiko, Daniel Borkmann,
	kernel-team, Martin KaFai Lau

Add various tests for code pattern '<non-const> NE/EQ <const>' implemented
in the previous verifier patch. Without the verifier patch, these new
tests will fail.

Signed-off-by: Yonghong Song <yhs@fb.com>
---
 .../selftests/bpf/prog_tests/verifier.c       |  2 +
 .../verifier_bounds_deduction_non_const.c     | 93 +++++++++++++++++++
 2 files changed, 95 insertions(+)
 create mode 100644 tools/testing/selftests/bpf/progs/verifier_bounds_deduction_non_const.c

diff --git a/tools/testing/selftests/bpf/prog_tests/verifier.c b/tools/testing/selftests/bpf/prog_tests/verifier.c
index efc8cf2e18d0..73dff693d411 100644
--- a/tools/testing/selftests/bpf/prog_tests/verifier.c
+++ b/tools/testing/selftests/bpf/prog_tests/verifier.c
@@ -7,6 +7,7 @@
 #include "verifier_array_access.skel.h"
 #include "verifier_basic_stack.skel.h"
 #include "verifier_bounds_deduction.skel.h"
+#include "verifier_bounds_deduction_non_const.skel.h"
 #include "verifier_bounds_mix_sign_unsign.skel.h"
 #include "verifier_cfg.skel.h"
 #include "verifier_cgroup_inv_retcode.skel.h"
@@ -70,6 +71,7 @@ void test_verifier_and(void)                  { RUN(verifier_and); }
 void test_verifier_array_access(void)         { RUN(verifier_array_access); }
 void test_verifier_basic_stack(void)          { RUN(verifier_basic_stack); }
 void test_verifier_bounds_deduction(void)     { RUN(verifier_bounds_deduction); }
+void test_verifier_bounds_deduction_non_const(void)     { RUN(verifier_bounds_deduction_non_const); }
 void test_verifier_bounds_mix_sign_unsign(void) { RUN(verifier_bounds_mix_sign_unsign); }
 void test_verifier_cfg(void)                  { RUN(verifier_cfg); }
 void test_verifier_cgroup_inv_retcode(void)   { RUN(verifier_cgroup_inv_retcode); }
diff --git a/tools/testing/selftests/bpf/progs/verifier_bounds_deduction_non_const.c b/tools/testing/selftests/bpf/progs/verifier_bounds_deduction_non_const.c
new file mode 100644
index 000000000000..c07af47c489e
--- /dev/null
+++ b/tools/testing/selftests/bpf/progs/verifier_bounds_deduction_non_const.c
@@ -0,0 +1,93 @@
+// SPDX-License-Identifier: GPL-2.0
+
+#include <linux/bpf.h>
+#include <bpf/bpf_helpers.h>
+#include "bpf_misc.h"
+
+SEC("socket")
+__description("check deducing bounds from non-const, jmp64, <non_const> == <const>")
+__success __retval(0)
+__naked void deducing_bounds_from_non_const_1(void)
+{
+	asm volatile ("					\
+	call %[bpf_ktime_get_ns];			\
+	if r0 < 3 goto l0_%=;				\
+	r2 = 2;						\
+	if r0 == r2 goto l1_%=;				\
+l0_%=:							\
+	r0 = 0;						\
+	exit;						\
+l1_%=:							\
+	r0 -= r1;					\
+	exit;						\
+"	:
+	: __imm(bpf_ktime_get_ns)
+	: __clobber_all);
+}
+
+SEC("socket")
+__description("check deducing bounds from non-const, jmp64, <non_const> != <const>")
+__success __retval(0)
+__naked void deducing_bounds_from_non_const_2(void)
+{
+	asm volatile ("					\
+	call %[bpf_ktime_get_ns];			\
+	if r0 < 3 goto l0_%=;				\
+	r2 = 2;						\
+	if r0 != r2 goto l0_%=;				\
+	goto l1_%=;					\
+l0_%=:							\
+	r0 = 0;						\
+	exit;						\
+l1_%=:							\
+	r0 -= r1;					\
+	exit;						\
+"	:
+	: __imm(bpf_ktime_get_ns)
+	: __clobber_all);
+}
+
+SEC("socket")
+__description("check deducing bounds from non-const, jmp32, <non_const> == <const>")
+__success __retval(0)
+__naked void deducing_bounds_from_non_const_3(void)
+{
+	asm volatile ("					\
+	call %[bpf_ktime_get_ns];			\
+	if w0 < 4 goto l0_%=;				\
+	w2 = 3;						\
+	if w0 == w2 goto l1_%=;				\
+l0_%=:							\
+	r0 = 0;						\
+	exit;						\
+l1_%=:							\
+	r0 -= r1;					\
+	exit;						\
+"	:
+	: __imm(bpf_ktime_get_ns)
+	: __clobber_all);
+}
+
+SEC("socket")
+__description("check deducing bounds from non-const, jmp32, <non_const> != <const>")
+__success __retval(0)
+__naked void deducing_bounds_from_non_const_4(void)
+{
+	asm volatile ("					\
+	call %[bpf_ktime_get_ns];			\
+	if w0 < 3 goto l0_%=;				\
+	w2 = 2;						\
+	if w0 != w2 goto l0_%=;				\
+	goto l1_%=;					\
+l0_%=:							\
+	r0 = 0;						\
+	exit;						\
+l1_%=:							\
+	r0 -= r1;					\
+	exit;						\
+"	:
+	: __imm(bpf_ktime_get_ns)
+	: __clobber_all);
+}
+
+char _license[] SEC("license") = "GPL";
-- 
2.34.1


^ permalink raw reply related	[flat|nested] 26+ messages in thread

* [PATCH bpf-next 3/7] bpf: Improve handling of pattern '<const> <cond_op> <non_const>' in verifier
  2023-03-30  5:56 [PATCH bpf-next 0/7] bpf: Improve verifier for cond_op and spilled loop index variables Yonghong Song
  2023-03-30  5:56 ` [PATCH bpf-next 1/7] bpf: Improve verifier JEQ/JNE insn branch taken checking Yonghong Song
  2023-03-30  5:56 ` [PATCH bpf-next 2/7] selftests/bpf: Add tests for non-constant cond_op NE/EQ bound deduction Yonghong Song
@ 2023-03-30  5:56 ` Yonghong Song
  2023-03-30 22:54   ` Dave Marchevsky
  2023-03-30  5:56 ` [PATCH bpf-next 4/7] selftests/bpf: Add verifier tests for code pattern '<const> <cond_op> <non_const>' Yonghong Song
                   ` (4 subsequent siblings)
  7 siblings, 1 reply; 26+ messages in thread
From: Yonghong Song @ 2023-03-30  5:56 UTC (permalink / raw)
  To: bpf
  Cc: Alexei Starovoitov, Andrii Nakryiko, Daniel Borkmann,
	kernel-team, Martin KaFai Lau

Currently, the verifier does not handle '<const> <cond_op> <non_const>' well.
For example,
  ...
  10: (79) r1 = *(u64 *)(r10 -16)       ; R1_w=scalar() R10=fp0
  11: (b7) r2 = 0                       ; R2_w=0
  12: (2d) if r2 > r1 goto pc+2
  13: (b7) r0 = 0
  14: (95) exit
  15: (65) if r1 s> 0x1 goto pc+3
  16: (0f) r0 += r1
  ...
At insn 12, verifier decides both true and false branch are possible, but
actually only false branch is possible.

Currently, the verifier already supports patterns '<non_const> <cond_op> <const>.
Add support for patterns '<const> <cond_op> <non_const>' in a similar way.

Also fix selftest 'verifier_bounds_mix_sign_unsign/bounds checks mixing signed and unsigned, variant 10'
due to this change.

Signed-off-by: Yonghong Song <yhs@fb.com>
---
 kernel/bpf/verifier.c                                | 12 ++++++++++++
 .../bpf/progs/verifier_bounds_mix_sign_unsign.c      |  2 +-
 2 files changed, 13 insertions(+), 1 deletion(-)

diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c
index 90bb6d25bc9c..d070943a8ba1 100644
--- a/kernel/bpf/verifier.c
+++ b/kernel/bpf/verifier.c
@@ -13302,6 +13302,18 @@ static int check_cond_jmp_op(struct bpf_verifier_env *env,
 				       src_reg->var_off.value,
 				       opcode,
 				       is_jmp32);
+	} else if (dst_reg->type == SCALAR_VALUE &&
+		   is_jmp32 && tnum_is_const(tnum_subreg(dst_reg->var_off))) {
+		pred = is_branch_taken(src_reg,
+				       tnum_subreg(dst_reg->var_off).value,
+				       flip_opcode(opcode),
+				       is_jmp32);
+	} else if (dst_reg->type == SCALAR_VALUE &&
+		   !is_jmp32 && tnum_is_const(dst_reg->var_off)) {
+		pred = is_branch_taken(src_reg,
+				       dst_reg->var_off.value,
+				       flip_opcode(opcode),
+				       is_jmp32);
 	} else if (reg_is_pkt_pointer_any(dst_reg) &&
 		   reg_is_pkt_pointer_any(src_reg) &&
 		   !is_jmp32) {
diff --git a/tools/testing/selftests/bpf/progs/verifier_bounds_mix_sign_unsign.c b/tools/testing/selftests/bpf/progs/verifier_bounds_mix_sign_unsign.c
index 91a66357896a..4f40144748a5 100644
--- a/tools/testing/selftests/bpf/progs/verifier_bounds_mix_sign_unsign.c
+++ b/tools/testing/selftests/bpf/progs/verifier_bounds_mix_sign_unsign.c
@@ -354,7 +354,7 @@ __naked void signed_and_unsigned_variant_10(void)
 	call %[bpf_map_lookup_elem];			\
 	if r0 == 0 goto l0_%=;				\
 	r1 = *(u64*)(r10 - 16);				\
-	r2 = 0;						\
+	r2 = -1;						\
 	if r2 > r1 goto l1_%=;				\
 	r0 = 0;						\
 	exit;						\
-- 
2.34.1


^ permalink raw reply related	[flat|nested] 26+ messages in thread

* [PATCH bpf-next 4/7] selftests/bpf: Add verifier tests for code pattern '<const> <cond_op> <non_const>'
  2023-03-30  5:56 [PATCH bpf-next 0/7] bpf: Improve verifier for cond_op and spilled loop index variables Yonghong Song
                   ` (2 preceding siblings ...)
  2023-03-30  5:56 ` [PATCH bpf-next 3/7] bpf: Improve handling of pattern '<const> <cond_op> <non_const>' in verifier Yonghong Song
@ 2023-03-30  5:56 ` Yonghong Song
  2023-03-30  5:56 ` [PATCH bpf-next 5/7] bpf: Mark potential spilled loop index variable as precise Yonghong Song
                   ` (3 subsequent siblings)
  7 siblings, 0 replies; 26+ messages in thread
From: Yonghong Song @ 2023-03-30  5:56 UTC (permalink / raw)
  To: bpf
  Cc: Alexei Starovoitov, Andrii Nakryiko, Daniel Borkmann,
	kernel-team, Martin KaFai Lau

Add various tests for code pattern '<const> <cond_op> <non_const>' to
exercise the previous verifier patch.

Signed-off-by: Yonghong Song <yhs@fb.com>
---
 .../verifier_bounds_deduction_non_const.c     | 460 ++++++++++++++++++
 1 file changed, 460 insertions(+)

diff --git a/tools/testing/selftests/bpf/progs/verifier_bounds_deduction_non_const.c b/tools/testing/selftests/bpf/progs/verifier_bounds_deduction_non_const.c
index c07af47c489e..3cb7763869bc 100644
--- a/tools/testing/selftests/bpf/progs/verifier_bounds_deduction_non_const.c
+++ b/tools/testing/selftests/bpf/progs/verifier_bounds_deduction_non_const.c
@@ -90,4 +90,464 @@ l1_%=:							\
 	: __clobber_all);
 }
 
+SEC("socket")
+__description("check deducing bounds from non-const, jmp64, <const> > <non_const>, 1")
+__success __retval(0)
+__naked void deducing_bounds_from_non_const_5(void)
+{
+	asm volatile ("					\
+	call %[bpf_ktime_get_ns];			\
+	r2 = 0;						\
+	if r2 > r0 goto l0_%=;				\
+	r0 = 0;						\
+	exit;						\
+l0_%=:							\
+	r0 -= r1;					\
+	exit;						\
+"	:
+	: __imm(bpf_ktime_get_ns)
+	: __clobber_all);
+}
+
+SEC("socket")
+__description("check deducing bounds from non-const, jmp64, <const> > <non_const>, 2")
+__success __retval(0)
+__naked void deducing_bounds_from_non_const_6(void)
+{
+	asm volatile ("					\
+	call %[bpf_ktime_get_ns];			\
+	if r0 < 4 goto l0_%=;				\
+	r2 = 4;						\
+	if r2 > r0 goto l1_%=;				\
+l0_%=:							\
+	r0 = 0;						\
+	exit;						\
+l1_%=:							\
+	r0 -= r1;					\
+	exit;						\
+"	:
+	: __imm(bpf_ktime_get_ns)
+	: __clobber_all);
+}
+
+SEC("socket")
+__description("check deducing bounds from non-const, jmp64, <const> >= <non_const>")
+__success __retval(0)
+__naked void deducing_bounds_from_non_const_7(void)
+{
+	asm volatile ("					\
+	call %[bpf_ktime_get_ns];			\
+	if r0 < 4 goto l0_%=;				\
+	r2 = 3;						\
+	if r2 >= r0 goto l1_%=;				\
+l0_%=:							\
+	r0 = 0;						\
+	exit;						\
+l1_%=:							\
+	r0 -= r1;					\
+	exit;						\
+"	:
+	: __imm(bpf_ktime_get_ns)
+	: __clobber_all);
+}
+
+SEC("socket")
+__description("check deducing bounds from non-const, jmp64, <const> < <non_const>")
+__success __retval(0)
+__naked void deducing_bounds_from_non_const_8(void)
+{
+	asm volatile ("					\
+	call %[bpf_ktime_get_ns];			\
+	if r0 > 4 goto l0_%=;				\
+	r2 = 4;						\
+	if r2 < r0 goto l1_%=;				\
+l0_%=:							\
+	r0 = 0;						\
+	exit;						\
+l1_%=:							\
+	r0 -= r1;					\
+	exit;						\
+"	:
+	: __imm(bpf_ktime_get_ns)
+	: __clobber_all);
+}
+
+SEC("socket")
+__description("check deducing bounds from non-const, jmp64, <const> <= <non_const>")
+__success __retval(0)
+__naked void deducing_bounds_from_non_const_9(void)
+{
+	asm volatile ("					\
+	call %[bpf_ktime_get_ns];			\
+	if r0 >= 4 goto l0_%=;				\
+	r2 = 4;						\
+	if r2 <= r0 goto l1_%=;				\
+l0_%=:							\
+	r0 = 0;						\
+	exit;						\
+l1_%=:							\
+	r0 -= r1;					\
+	exit;						\
+"	:
+	: __imm(bpf_ktime_get_ns)
+	: __clobber_all);
+}
+
+SEC("socket")
+__description("check deducing bounds from non-const, jmp64, <const> == <non_const>")
+__success __retval(0)
+__naked void deducing_bounds_from_non_const_10(void)
+{
+	asm volatile ("					\
+	call %[bpf_ktime_get_ns];			\
+	if r0 < 3 goto l0_%=;				\
+	r2 = 2;						\
+	if r2 == r0 goto l1_%=;				\
+l0_%=:							\
+	r0 = 0;						\
+	exit;						\
+l1_%=:							\
+	r0 -= r1;					\
+	exit;						\
+"	:
+	: __imm(bpf_ktime_get_ns)
+	: __clobber_all);
+}
+
+SEC("socket")
+__description("check deducing bounds from non-const, jmp64, <const> s> <non_const>")
+__success __retval(0)
+__naked void deducing_bounds_from_non_const_11(void)
+{
+	asm volatile ("					\
+	call %[bpf_ktime_get_ns];			\
+	if r0 s< 4 goto l0_%=;				\
+	r2 = 4;						\
+	if r2 s> r0 goto l1_%=;				\
+l0_%=:							\
+	r0 = 0;						\
+	exit;						\
+l1_%=:							\
+	r0 -= r1;					\
+	exit;						\
+"	:
+	: __imm(bpf_ktime_get_ns)
+	: __clobber_all);
+}
+
+SEC("socket")
+__description("check deducing bounds from non-const, jmp64, <const> s>= <non_const>")
+__success __retval(0)
+__naked void deducing_bounds_from_non_const_12(void)
+{
+	asm volatile ("					\
+	call %[bpf_ktime_get_ns];			\
+	if r0 s< 4 goto l0_%=;				\
+	r2 = 3;						\
+	if r2 s>= r0 goto l1_%=;				\
+l0_%=:							\
+	r0 = 0;						\
+	exit;						\
+l1_%=:							\
+	r0 -= r1;					\
+	exit;						\
+"	:
+	: __imm(bpf_ktime_get_ns)
+	: __clobber_all);
+}
+
+SEC("socket")
+__description("check deducing bounds from non-const, jmp64, <const> s< <non_const>")
+__success __retval(0)
+__naked void deducing_bounds_from_non_const_13(void)
+{
+	asm volatile ("					\
+	call %[bpf_ktime_get_ns];			\
+	if r0 s> 4 goto l0_%=;				\
+	r2 = 4;						\
+	if r2 s< r0 goto l1_%=;				\
+l0_%=:							\
+	r0 = 0;						\
+	exit;						\
+l1_%=:							\
+	r0 -= r1;					\
+	exit;						\
+"	:
+	: __imm(bpf_ktime_get_ns)
+	: __clobber_all);
+}
+
+SEC("socket")
+__description("check deducing bounds from non-const, jmp64, <const> s<= <non_const>")
+__success __retval(0)
+__naked void deducing_bounds_from_non_const_14(void)
+{
+	asm volatile ("					\
+	call %[bpf_ktime_get_ns];			\
+	if r0 s> 4 goto l0_%=;				\
+	r2 = 5;						\
+	if r2 s<= r0 goto l1_%=;				\
+l0_%=:							\
+	r0 = 0;						\
+	exit;						\
+l1_%=:							\
+	r0 -= r1;					\
+	exit;						\
+"	:
+	: __imm(bpf_ktime_get_ns)
+	: __clobber_all);
+}
+
+SEC("socket")
+__description("check deducing bounds from non-const, jmp64, <const> != <non_const>")
+__success __retval(0)
+__naked void deducing_bounds_from_non_const_15(void)
+{
+	asm volatile ("					\
+	call %[bpf_ktime_get_ns];			\
+	if r0 < 3 goto l0_%=;				\
+	r2 = 2;						\
+	if r2 != r0 goto l0_%=;				\
+	goto l1_%=;					\
+l0_%=:							\
+	r0 = 0;						\
+	exit;						\
+l1_%=:							\
+	r0 -= r1;					\
+	exit;						\
+"	:
+	: __imm(bpf_ktime_get_ns)
+	: __clobber_all);
+}
+
+SEC("socket")
+__description("check deducing bounds from non-const, jmp32, <const> > <non_const>, 1")
+__success __retval(0)
+__naked void deducing_bounds_from_non_const_16(void)
+{
+	asm volatile ("					\
+	call %[bpf_ktime_get_ns];			\
+	w2 = 0;						\
+	if w2 > w0 goto l0_%=;				\
+	r0 = 0;						\
+	exit;						\
+l0_%=:							\
+	r0 -= r1;					\
+	exit;						\
+"	:
+	: __imm(bpf_ktime_get_ns)
+	: __clobber_all);
+}
+
+SEC("socket")
+__description("check deducing bounds from non-const, jmp32, <const> > <non_const>, 2")
+__success __retval(0)
+__naked void deducing_bounds_from_non_const_17(void)
+{
+	asm volatile ("					\
+	call %[bpf_ktime_get_ns];			\
+	if w0 < 4 goto l0_%=;				\
+	w2 = 4;						\
+	if w2 > w0 goto l1_%=;				\
+l0_%=:							\
+	r0 = 0;						\
+	exit;						\
+l1_%=:							\
+	r0 -= r1;					\
+	exit;						\
+"	:
+	: __imm(bpf_ktime_get_ns)
+	: __clobber_all);
+}
+
+SEC("socket")
+__description("check deducing bounds from non-const, jmp32, <const> >= <non_const>")
+__success __retval(0)
+__naked void deducing_bounds_from_non_const_18(void)
+{
+	asm volatile ("					\
+	call %[bpf_ktime_get_ns];			\
+	if w0 < 4 goto l0_%=;				\
+	w2 = 3;						\
+	if w2 >= w0 goto l1_%=;				\
+l0_%=:							\
+	r0 = 0;						\
+	exit;						\
+l1_%=:							\
+	r0 -= r1;					\
+	exit;						\
+"	:
+	: __imm(bpf_ktime_get_ns)
+	: __clobber_all);
+}
+
+SEC("socket")
+__description("check deducing bounds from non-const, jmp32, <const> < <non_const>")
+__success __retval(0)
+__naked void deducing_bounds_from_non_const_19(void)
+{
+	asm volatile ("					\
+	call %[bpf_ktime_get_ns];			\
+	if w0 > 4 goto l0_%=;				\
+	w2 = 4;						\
+	if w2 < w0 goto l1_%=;				\
+l0_%=:							\
+	r0 = 0;						\
+	exit;						\
+l1_%=:							\
+	r0 -= r1;					\
+	exit;						\
+"	:
+	: __imm(bpf_ktime_get_ns)
+	: __clobber_all);
+}
+
+SEC("socket")
+__description("check deducing bounds from non-const, jmp32, <const> <= <non_const>")
+__success __retval(0)
+__naked void deducing_bounds_from_non_const_20(void)
+{
+	asm volatile ("					\
+	call %[bpf_ktime_get_ns];			\
+	if w0 >= 4 goto l0_%=;				\
+	w2 = 4;						\
+	if w2 <= w0 goto l1_%=;				\
+l0_%=:							\
+	r0 = 0;						\
+	exit;						\
+l1_%=:							\
+	r0 -= r1;					\
+	exit;						\
+"	:
+	: __imm(bpf_ktime_get_ns)
+	: __clobber_all);
+}
+
+SEC("socket")
+__description("check deducing bounds from non-const, jmp32, <const> == <non_const>")
+__success __retval(0)
+__naked void deducing_bounds_from_non_const_21(void)
+{
+	asm volatile ("					\
+	call %[bpf_ktime_get_ns];			\
+	if w0 < 4 goto l0_%=;				\
+	w2 = 3;						\
+	if w2 == w0 goto l1_%=;				\
+l0_%=:							\
+	r0 = 0;						\
+	exit;						\
+l1_%=:							\
+	r0 -= r1;					\
+	exit;						\
+"	:
+	: __imm(bpf_ktime_get_ns)
+	: __clobber_all);
+}
+
+SEC("socket")
+__description("check deducing bounds from non-const, jmp32, <const> s> <non_const>")
+__success __retval(0)
+__naked void deducing_bounds_from_non_const_22(void)
+{
+	asm volatile ("					\
+	call %[bpf_ktime_get_ns];			\
+	if w0 s< 4 goto l0_%=;				\
+	w2 = 4;						\
+	if w2 s> w0 goto l1_%=;				\
+l0_%=:							\
+	r0 = 0;						\
+	exit;						\
+l1_%=:							\
+	r0 -= r1;					\
+	exit;						\
+"	:
+	: __imm(bpf_ktime_get_ns)
+	: __clobber_all);
+}
+
+SEC("socket")
+__description("check deducing bounds from non-const, jmp32, <const> s>= <non_const>")
+__success __retval(0)
+__naked void deducing_bounds_from_non_const_23(void)
+{
+	asm volatile ("					\
+	call %[bpf_ktime_get_ns];			\
+	if w0 s< 4 goto l0_%=;				\
+	w2 = 3;						\
+	if w2 s>= w0 goto l1_%=;				\
+l0_%=:							\
+	r0 = 0;						\
+	exit;						\
+l1_%=:							\
+	r0 -= r1;					\
+	exit;						\
+"	:
+	: __imm(bpf_ktime_get_ns)
+	: __clobber_all);
+}
+
+SEC("socket")
+__description("check deducing bounds from non-const, jmp32, <const> s< <non_const>")
+__success __retval(0)
+__naked void deducing_bounds_from_non_const_24(void)
+{
+	asm volatile ("					\
+	call %[bpf_ktime_get_ns];			\
+	if w0 s> 4 goto l0_%=;				\
+	w2 = 5;						\
+	if w2 s< w0 goto l1_%=;				\
+l0_%=:							\
+	r0 = 0;						\
+	exit;						\
+l1_%=:							\
+	r0 -= r1;					\
+	exit;						\
+"	:
+	: __imm(bpf_ktime_get_ns)
+	: __clobber_all);
+}
+
+SEC("socket")
+__description("check deducing bounds from non-const, jmp32, <const> s<= <non_const>")
+__success __retval(0)
+__naked void deducing_bounds_from_non_const_25(void)
+{
+	asm volatile ("					\
+	call %[bpf_ktime_get_ns];			\
+	if w0 s>= 4 goto l0_%=;				\
+	w2 = 4;						\
+	if w2 s<= w0 goto l1_%=;				\
+l0_%=:							\
+	r0 = 0;						\
+	exit;						\
+l1_%=:							\
+	r0 -= r1;					\
+	exit;						\
+"	:
+	: __imm(bpf_ktime_get_ns)
+	: __clobber_all);
+}
+
+SEC("socket")
+__description("check deducing bounds from non-const, jmp32, <const> != <non_const>")
+__success __retval(0)
+__naked void deducing_bounds_from_non_const_26(void)
+{
+	asm volatile ("					\
+	call %[bpf_ktime_get_ns];			\
+	if w0 < 3 goto l0_%=;				\
+	w2 = 2;						\
+	if w2 != w0 goto l0_%=;				\
+	goto l1_%=;					\
+l0_%=:							\
+	r0 = 0;						\
+	exit;						\
+l1_%=:							\
+	r0 -= r1;					\
+	exit;						\
+"	:
+	: __imm(bpf_ktime_get_ns)
+	: __clobber_all);
+}
+
 char _license[] SEC("license") = "GPL";
-- 
2.34.1


^ permalink raw reply related	[flat|nested] 26+ messages in thread

* [PATCH bpf-next 5/7] bpf: Mark potential spilled loop index variable as precise
  2023-03-30  5:56 [PATCH bpf-next 0/7] bpf: Improve verifier for cond_op and spilled loop index variables Yonghong Song
                   ` (3 preceding siblings ...)
  2023-03-30  5:56 ` [PATCH bpf-next 4/7] selftests/bpf: Add verifier tests for code pattern '<const> <cond_op> <non_const>' Yonghong Song
@ 2023-03-30  5:56 ` Yonghong Song
  2023-03-31 21:54   ` Eduard Zingerman
  2023-04-04 22:09   ` Andrii Nakryiko
  2023-03-30  5:56 ` [PATCH bpf-next 6/7] selftests/bpf: Remove previous workaround for test verif_scale_loop6 Yonghong Song
                   ` (2 subsequent siblings)
  7 siblings, 2 replies; 26+ messages in thread
From: Yonghong Song @ 2023-03-30  5:56 UTC (permalink / raw)
  To: bpf
  Cc: Alexei Starovoitov, Andrii Nakryiko, Daniel Borkmann,
	kernel-team, Martin KaFai Lau

For a loop, if loop index variable is spilled and between loop
iterations, the only reg/spill state difference is spilled loop
index variable, then verifier may assume an infinite loop which
cause verification failure. In such cases, we should mark
spilled loop index variable as precise to differentiate states
between loop iterations.

Since verifier is not able to accurately identify loop index
variable, add a heuristic such that if both old reg state and
new reg state are consts, mark old reg state as precise which
will trigger constant value comparison later.

Signed-off-by: Yonghong Song <yhs@fb.com>
---
 kernel/bpf/verifier.c | 20 ++++++++++++++++++--
 1 file changed, 18 insertions(+), 2 deletions(-)

diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c
index d070943a8ba1..d1aa2c7ae7c0 100644
--- a/kernel/bpf/verifier.c
+++ b/kernel/bpf/verifier.c
@@ -14850,6 +14850,23 @@ static bool stacksafe(struct bpf_verifier_env *env, struct bpf_func_state *old,
 		/* Both old and cur are having same slot_type */
 		switch (old->stack[spi].slot_type[BPF_REG_SIZE - 1]) {
 		case STACK_SPILL:
+			/* sometime loop index variable is spilled and the spill
+			 * is not marked as precise. If only state difference
+			 * between two iterations are spilled loop index, the
+			 * "infinite loop detected at insn" error will be hit.
+			 * Mark spilled constant as precise so it went through value
+			 * comparison.
+			 */
+			old_reg = &old->stack[spi].spilled_ptr;
+			cur_reg = &cur->stack[spi].spilled_ptr;
+			if (!old_reg->precise) {
+				if (old_reg->type == SCALAR_VALUE &&
+				    cur_reg->type == SCALAR_VALUE &&
+				    tnum_is_const(old_reg->var_off) &&
+				    tnum_is_const(cur_reg->var_off))
+					old_reg->precise = true;
+			}
+
 			/* when explored and current stack slot are both storing
 			 * spilled registers, check that stored pointers types
 			 * are the same as well.
@@ -14860,8 +14877,7 @@ static bool stacksafe(struct bpf_verifier_env *env, struct bpf_func_state *old,
 			 * such verifier states are not equivalent.
 			 * return false to continue verification of this path
 			 */
-			if (!regsafe(env, &old->stack[spi].spilled_ptr,
-				     &cur->stack[spi].spilled_ptr, idmap))
+			if (!regsafe(env, old_reg, cur_reg, idmap))
 				return false;
 			break;
 		case STACK_DYNPTR:
-- 
2.34.1


^ permalink raw reply related	[flat|nested] 26+ messages in thread

* [PATCH bpf-next 6/7] selftests/bpf: Remove previous workaround for test verif_scale_loop6
  2023-03-30  5:56 [PATCH bpf-next 0/7] bpf: Improve verifier for cond_op and spilled loop index variables Yonghong Song
                   ` (4 preceding siblings ...)
  2023-03-30  5:56 ` [PATCH bpf-next 5/7] bpf: Mark potential spilled loop index variable as precise Yonghong Song
@ 2023-03-30  5:56 ` Yonghong Song
  2023-03-30  5:56 ` [PATCH bpf-next 7/7] selftests/bpf: Add a new test based on loop6.c Yonghong Song
  2023-04-04 21:46 ` [PATCH bpf-next 0/7] bpf: Improve verifier for cond_op and spilled loop index variables Andrii Nakryiko
  7 siblings, 0 replies; 26+ messages in thread
From: Yonghong Song @ 2023-03-30  5:56 UTC (permalink / raw)
  To: bpf
  Cc: Alexei Starovoitov, Andrii Nakryiko, Daniel Borkmann,
	kernel-team, Martin KaFai Lau

Commit 3c2611bac08a("selftests/bpf: Fix trace_virtqueue_add_sgs test issue with LLVM 17")
workarounds the verification failure by using asm code with '__sink' macro to
prevent certain llvm optimization.

This patch added proper support in verifier so workaround is not
necessary any more. So remove these workarounds.

Signed-off-by: Yonghong Song <yhs@fb.com>
---
 tools/testing/selftests/bpf/progs/loop6.c | 2 --
 1 file changed, 2 deletions(-)

diff --git a/tools/testing/selftests/bpf/progs/loop6.c b/tools/testing/selftests/bpf/progs/loop6.c
index e4ff97fbcce1..a13bee928b27 100644
--- a/tools/testing/selftests/bpf/progs/loop6.c
+++ b/tools/testing/selftests/bpf/progs/loop6.c
@@ -77,7 +77,6 @@ int BPF_KPROBE(trace_virtqueue_add_sgs, void *unused, struct scatterlist **sgs,
 		return 0;
 
 	for (i = 0; (i < VIRTIO_MAX_SGS) && (i < out_sgs); i++) {
-		__sink(out_sgs);
 		for (n = 0, sgp = get_sgp(sgs, i); sgp && (n < SG_MAX);
 		     sgp = __sg_next(sgp)) {
 			bpf_probe_read_kernel(&len, sizeof(len), &sgp->length);
@@ -87,7 +86,6 @@ int BPF_KPROBE(trace_virtqueue_add_sgs, void *unused, struct scatterlist **sgs,
 	}
 
 	for (i = 0; (i < VIRTIO_MAX_SGS) && (i < in_sgs); i++) {
-		__sink(in_sgs);
 		for (n = 0, sgp = get_sgp(sgs, i); sgp && (n < SG_MAX);
 		     sgp = __sg_next(sgp)) {
 			bpf_probe_read_kernel(&len, sizeof(len), &sgp->length);
-- 
2.34.1


^ permalink raw reply related	[flat|nested] 26+ messages in thread

* [PATCH bpf-next 7/7] selftests/bpf: Add a new test based on loop6.c
  2023-03-30  5:56 [PATCH bpf-next 0/7] bpf: Improve verifier for cond_op and spilled loop index variables Yonghong Song
                   ` (5 preceding siblings ...)
  2023-03-30  5:56 ` [PATCH bpf-next 6/7] selftests/bpf: Remove previous workaround for test verif_scale_loop6 Yonghong Song
@ 2023-03-30  5:56 ` Yonghong Song
  2023-04-03  1:39   ` Alexei Starovoitov
  2023-04-04 21:46 ` [PATCH bpf-next 0/7] bpf: Improve verifier for cond_op and spilled loop index variables Andrii Nakryiko
  7 siblings, 1 reply; 26+ messages in thread
From: Yonghong Song @ 2023-03-30  5:56 UTC (permalink / raw)
  To: bpf
  Cc: Alexei Starovoitov, Andrii Nakryiko, Daniel Borkmann,
	kernel-team, Martin KaFai Lau

With LLVM commit [1], loop6.c will fail verification without Commit 3c2611bac08a
("selftests/bpf: Fix trace_virtqueue_add_sgs test issue with LLVM 17.").
Also, there is an effort to fix LLVM since LLVM17 may be used by old kernels
for bpf development.

A new test is added by manually doing similar transformation in [1]
so it can be used to test related verifier changes.

  [1] https://reviews.llvm.org/D143726

Signed-off-by: Yonghong Song <yhs@fb.com>
---
 .../bpf/prog_tests/bpf_verif_scale.c          |   5 +
 tools/testing/selftests/bpf/progs/loop7.c     | 102 ++++++++++++++++++
 2 files changed, 107 insertions(+)
 create mode 100644 tools/testing/selftests/bpf/progs/loop7.c

diff --git a/tools/testing/selftests/bpf/prog_tests/bpf_verif_scale.c b/tools/testing/selftests/bpf/prog_tests/bpf_verif_scale.c
index 731c343897d8..cb708235e654 100644
--- a/tools/testing/selftests/bpf/prog_tests/bpf_verif_scale.c
+++ b/tools/testing/selftests/bpf/prog_tests/bpf_verif_scale.c
@@ -180,6 +180,11 @@ void test_verif_scale_loop6()
 	scale_test("loop6.bpf.o", BPF_PROG_TYPE_KPROBE, false);
 }
 
+void test_verif_scale_loop7()
+{
+	scale_test("loop7.bpf.o", BPF_PROG_TYPE_KPROBE, false);
+}
+
 void test_verif_scale_strobemeta()
 {
 	/* partial unroll. 19k insn in a loop.
diff --git a/tools/testing/selftests/bpf/progs/loop7.c b/tools/testing/selftests/bpf/progs/loop7.c
new file mode 100644
index 000000000000..b234ed6f0038
--- /dev/null
+++ b/tools/testing/selftests/bpf/progs/loop7.c
@@ -0,0 +1,102 @@
+// SPDX-License-Identifier: GPL-2.0
+
+#include <linux/ptrace.h>
+#include <stddef.h>
+#include <linux/bpf.h>
+#include <bpf/bpf_helpers.h>
+#include <bpf/bpf_tracing.h>
+#include "bpf_misc.h"
+
+char _license[] SEC("license") = "GPL";
+
+/* typically virtio scsi has max SGs of 6 */
+#define VIRTIO_MAX_SGS	6
+
+/* Verifier will fail with SG_MAX = 128. The failure can be
+ * workarounded with a smaller SG_MAX, e.g. 10.
+ */
+#define WORKAROUND
+#ifdef WORKAROUND
+#define SG_MAX		10
+#else
+/* typically virtio blk has max SEG of 128 */
+#define SG_MAX		128
+#endif
+
+#define SG_CHAIN	0x01UL
+#define SG_END		0x02UL
+
+struct scatterlist {
+	unsigned long   page_link;
+	unsigned int    offset;
+	unsigned int    length;
+};
+
+#define sg_is_chain(sg)		((sg)->page_link & SG_CHAIN)
+#define sg_is_last(sg)		((sg)->page_link & SG_END)
+#define sg_chain_ptr(sg)	\
+	((struct scatterlist *) ((sg)->page_link & ~(SG_CHAIN | SG_END)))
+
+static inline struct scatterlist *__sg_next(struct scatterlist *sgp)
+{
+	struct scatterlist sg;
+
+	bpf_probe_read_kernel(&sg, sizeof(sg), sgp);
+	if (sg_is_last(&sg))
+		return NULL;
+
+	sgp++;
+
+	bpf_probe_read_kernel(&sg, sizeof(sg), sgp);
+	if (sg_is_chain(&sg))
+		sgp = sg_chain_ptr(&sg);
+
+	return sgp;
+}
+
+static inline struct scatterlist *get_sgp(struct scatterlist **sgs, int i)
+{
+	struct scatterlist *sgp;
+
+	bpf_probe_read_kernel(&sgp, sizeof(sgp), sgs + i);
+	return sgp;
+}
+
+int config = 0;
+int result = 0;
+
+SEC("kprobe/virtqueue_add_sgs")
+int BPF_KPROBE(trace_virtqueue_add_sgs, void *unused, struct scatterlist **sgs,
+	       unsigned int out_sgs, unsigned int in_sgs)
+{
+	struct scatterlist *sgp = NULL;
+	__u64 length1 = 0, length2 = 0;
+	unsigned int i, n, len, upper;
+
+	if (config != 0)
+		return 0;
+
+	upper = out_sgs < VIRTIO_MAX_SGS ? out_sgs : VIRTIO_MAX_SGS;
+	for (i = 0; i < upper; i++) {
+		for (n = 0, sgp = get_sgp(sgs, i); sgp && (n < SG_MAX);
+		     sgp = __sg_next(sgp)) {
+			bpf_probe_read_kernel(&len, sizeof(len), &sgp->length);
+			length1 += len;
+			n++;
+		}
+	}
+
+	upper = in_sgs < VIRTIO_MAX_SGS ? in_sgs : VIRTIO_MAX_SGS;
+	for (i = 0; i < upper; i++) {
+		for (n = 0, sgp = get_sgp(sgs, i); sgp && (n < SG_MAX);
+		     sgp = __sg_next(sgp)) {
+			bpf_probe_read_kernel(&len, sizeof(len), &sgp->length);
+			length2 += len;
+			n++;
+		}
+	}
+
+	config = 1;
+	result = length2 - length1;
+	return 0;
+}
-- 
2.34.1


^ permalink raw reply related	[flat|nested] 26+ messages in thread

* Re: [PATCH bpf-next 1/7] bpf: Improve verifier JEQ/JNE insn branch taken checking
  2023-03-30  5:56 ` [PATCH bpf-next 1/7] bpf: Improve verifier JEQ/JNE insn branch taken checking Yonghong Song
@ 2023-03-30 21:14   ` Dave Marchevsky
  2023-03-31  6:40     ` Yonghong Song
  0 siblings, 1 reply; 26+ messages in thread
From: Dave Marchevsky @ 2023-03-30 21:14 UTC (permalink / raw)
  To: Yonghong Song, bpf
  Cc: Alexei Starovoitov, Andrii Nakryiko, Daniel Borkmann,
	kernel-team, Martin KaFai Lau



On 3/30/23 1:56 AM, Yonghong Song wrote:
> Currently, for BPF_JEQ/BPF_JNE insn, verifier determines
> whether the branch is taken or not only if both operands
> are constants. Therefore, for the following code snippet,
>   0: (85) call bpf_ktime_get_ns#5       ; R0_w=scalar()
>   1: (a5) if r0 < 0x3 goto pc+2         ; R0_w=scalar(umin=3)
>   2: (b7) r2 = 2                        ; R2_w=2
>   3: (1d) if r0 == r2 goto pc+2 6
> 
> At insn 3, since r0 is not a constant, verifier assumes both branch
> can be taken which may lead inproper verification failure.
> 
> Add comparing umin value and the constant. If the umin value
> is greater than the constant, for JEQ the branch must be
> not-taken, and for JNE the branch must be taken.
> The jmp32 mode JEQ/JNE branch taken checking is also
> handled similarly.
> 
> Signed-off-by: Yonghong Song <yhs@fb.com>
> ---
>  kernel/bpf/verifier.c | 8 ++++++++
>  1 file changed, 8 insertions(+)
> 
> diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c
> index 20eb2015842f..90bb6d25bc9c 100644
> --- a/kernel/bpf/verifier.c
> +++ b/kernel/bpf/verifier.c
> @@ -12597,10 +12597,14 @@ static int is_branch32_taken(struct bpf_reg_state *reg, u32 val, u8 opcode)
>  	case BPF_JEQ:
>  		if (tnum_is_const(subreg))
>  			return !!tnum_equals_const(subreg, val);
> +		else if (reg->u32_min_value > val)
> +			return 0;
>  		break;

The explanation makes sense to me, and I see similar min_value logic elsewhere
in the switch for other jmp types. But those other jmp types are bounding the
value from one side. Since JEQ and JNE test equality, can't we also add logic
for u32_max_value here? e.g.

        case BPF_JEQ:
                if (tnum_is_const(subreg))
                        return !!tnum_equals_const(subreg, val);
                else if (reg->u32_min_value > val || reg->u32_max_value < val)
                        return 0;
                break;

Similar comment for rest of additions.

>  	case BPF_JNE:
>  		if (tnum_is_const(subreg))
>  			return !tnum_equals_const(subreg, val);
> +		else if (reg->u32_min_value > val)
> +			return 1;
>  		break;
>  	case BPF_JSET:
>  		if ((~subreg.mask & subreg.value) & val)
> @@ -12670,10 +12674,14 @@ static int is_branch64_taken(struct bpf_reg_state *reg, u64 val, u8 opcode)
>  	case BPF_JEQ:
>  		if (tnum_is_const(reg->var_off))
>  			return !!tnum_equals_const(reg->var_off, val);
> +		else if (reg->umin_value > val)
> +			return 0;
>  		break;
>  	case BPF_JNE:
>  		if (tnum_is_const(reg->var_off))
>  			return !tnum_equals_const(reg->var_off, val);
> +		else if (reg->umin_value > val)
> +			return 1;
>  		break;
>  	case BPF_JSET:
>  		if ((~reg->var_off.mask & reg->var_off.value) & val)

^ permalink raw reply	[flat|nested] 26+ messages in thread

* Re: [PATCH bpf-next 3/7] bpf: Improve handling of pattern '<const> <cond_op> <non_const>' in verifier
  2023-03-30  5:56 ` [PATCH bpf-next 3/7] bpf: Improve handling of pattern '<const> <cond_op> <non_const>' in verifier Yonghong Song
@ 2023-03-30 22:54   ` Dave Marchevsky
  2023-03-31 15:26     ` Yonghong Song
  2023-04-04 22:04     ` Andrii Nakryiko
  0 siblings, 2 replies; 26+ messages in thread
From: Dave Marchevsky @ 2023-03-30 22:54 UTC (permalink / raw)
  To: Yonghong Song, bpf
  Cc: Alexei Starovoitov, Andrii Nakryiko, Daniel Borkmann,
	kernel-team, Martin KaFai Lau

On 3/30/23 1:56 AM, Yonghong Song wrote:
> Currently, the verifier does not handle '<const> <cond_op> <non_const>' well.
> For example,
>   ...
>   10: (79) r1 = *(u64 *)(r10 -16)       ; R1_w=scalar() R10=fp0
>   11: (b7) r2 = 0                       ; R2_w=0
>   12: (2d) if r2 > r1 goto pc+2
>   13: (b7) r0 = 0
>   14: (95) exit
>   15: (65) if r1 s> 0x1 goto pc+3
>   16: (0f) r0 += r1
>   ...
> At insn 12, verifier decides both true and false branch are possible, but
> actually only false branch is possible.
> 
> Currently, the verifier already supports patterns '<non_const> <cond_op> <const>.
> Add support for patterns '<const> <cond_op> <non_const>' in a similar way.
> 
> Also fix selftest 'verifier_bounds_mix_sign_unsign/bounds checks mixing signed and unsigned, variant 10'
> due to this change.
> 
> Signed-off-by: Yonghong Song <yhs@fb.com>
> ---
>  kernel/bpf/verifier.c                                | 12 ++++++++++++
>  .../bpf/progs/verifier_bounds_mix_sign_unsign.c      |  2 +-
>  2 files changed, 13 insertions(+), 1 deletion(-)
> 
> diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c
> index 90bb6d25bc9c..d070943a8ba1 100644
> --- a/kernel/bpf/verifier.c
> +++ b/kernel/bpf/verifier.c
> @@ -13302,6 +13302,18 @@ static int check_cond_jmp_op(struct bpf_verifier_env *env,
>  				       src_reg->var_off.value,
>  				       opcode,
>  				       is_jmp32);
> +	} else if (dst_reg->type == SCALAR_VALUE &&
> +		   is_jmp32 && tnum_is_const(tnum_subreg(dst_reg->var_off))) {
> +		pred = is_branch_taken(src_reg,
> +				       tnum_subreg(dst_reg->var_off).value,
> +				       flip_opcode(opcode),
> +				       is_jmp32);
> +	} else if (dst_reg->type == SCALAR_VALUE &&
> +		   !is_jmp32 && tnum_is_const(dst_reg->var_off)) {
> +		pred = is_branch_taken(src_reg,
> +				       dst_reg->var_off.value,
> +				       flip_opcode(opcode),
> +				       is_jmp32);
>  	} else if (reg_is_pkt_pointer_any(dst_reg) &&
>  		   reg_is_pkt_pointer_any(src_reg) &&
>  		   !is_jmp32) {

Looking at the two SCALAR_VALUE 'else if's above these added lines, these
additions make sense. Having four separate 'else if' checks for essentially
similar logic makes this hard to read, though, maybe it's an opportunity to
refactor a bit.

While trying to make sense of the logic here I attempted to simplify with
a helper:

@@ -13234,6 +13234,21 @@ static void find_equal_scalars(struct bpf_verifier_state *vstate,
        }));
 }

+static int maybe_const_operand_branch(struct tnum maybe_const_op,
+                                     struct bpf_reg_state *other_op_reg,
+                                     u8 opcode, bool is_jmp32)
+{
+       struct tnum jmp_tnum = is_jmp32 ? tnum_subreg(maybe_const_op) :
+                                         maybe_const_op;
+       if (!tnum_is_const(jmp_tnum))
+               return -1;
+
+       return is_branch_taken(other_op_reg,
+                              jmp_tnum.value,
+                              opcode,
+                              is_jmp32);
+}
+
 static int check_cond_jmp_op(struct bpf_verifier_env *env,
                             struct bpf_insn *insn, int *insn_idx)
 {
@@ -13287,18 +13302,12 @@ static int check_cond_jmp_op(struct bpf_verifier_env *env,

        if (BPF_SRC(insn->code) == BPF_K) {
                pred = is_branch_taken(dst_reg, insn->imm, opcode, is_jmp32);
-       } else if (src_reg->type == SCALAR_VALUE &&
-                  is_jmp32 && tnum_is_const(tnum_subreg(src_reg->var_off))) {
-               pred = is_branch_taken(dst_reg,
-                                      tnum_subreg(src_reg->var_off).value,
-                                      opcode,
-                                      is_jmp32);
-       } else if (src_reg->type == SCALAR_VALUE &&
-                  !is_jmp32 && tnum_is_const(src_reg->var_off)) {
-               pred = is_branch_taken(dst_reg,
-                                      src_reg->var_off.value,
-                                      opcode,
-                                      is_jmp32);
+       } else if (src_reg->type == SCALAR_VALUE) {
+               pred = maybe_const_operand_branch(src_reg->var_off, dst_reg,
+                                                 opcode, is_jmp32);
+       } else if (dst_reg->type == SCALAR_VALUE) {
+               pred = maybe_const_operand_branch(dst_reg->var_off, src_reg,
+                                                 flip_opcode(opcode), is_jmp32);
        } else if (reg_is_pkt_pointer_any(dst_reg) &&
                   reg_is_pkt_pointer_any(src_reg) &&
                   !is_jmp32) {


I think the resultant logic is the same as your patch, but it's easier to
understand, for me at least. Note that I didn't test the above.

^ permalink raw reply	[flat|nested] 26+ messages in thread

* Re: [PATCH bpf-next 1/7] bpf: Improve verifier JEQ/JNE insn branch taken checking
  2023-03-30 21:14   ` Dave Marchevsky
@ 2023-03-31  6:40     ` Yonghong Song
  0 siblings, 0 replies; 26+ messages in thread
From: Yonghong Song @ 2023-03-31  6:40 UTC (permalink / raw)
  To: Dave Marchevsky, Yonghong Song, bpf
  Cc: Alexei Starovoitov, Andrii Nakryiko, Daniel Borkmann,
	kernel-team, Martin KaFai Lau



On 3/30/23 2:14 PM, Dave Marchevsky wrote:
> 
> 
> On 3/30/23 1:56 AM, Yonghong Song wrote:
>> Currently, for BPF_JEQ/BPF_JNE insn, verifier determines
>> whether the branch is taken or not only if both operands
>> are constants. Therefore, for the following code snippet,
>>    0: (85) call bpf_ktime_get_ns#5       ; R0_w=scalar()
>>    1: (a5) if r0 < 0x3 goto pc+2         ; R0_w=scalar(umin=3)
>>    2: (b7) r2 = 2                        ; R2_w=2
>>    3: (1d) if r0 == r2 goto pc+2 6
>>
>> At insn 3, since r0 is not a constant, verifier assumes both branch
>> can be taken which may lead inproper verification failure.
>>
>> Add comparing umin value and the constant. If the umin value
>> is greater than the constant, for JEQ the branch must be
>> not-taken, and for JNE the branch must be taken.
>> The jmp32 mode JEQ/JNE branch taken checking is also
>> handled similarly.
>>
>> Signed-off-by: Yonghong Song <yhs@fb.com>
>> ---
>>   kernel/bpf/verifier.c | 8 ++++++++
>>   1 file changed, 8 insertions(+)
>>
>> diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c
>> index 20eb2015842f..90bb6d25bc9c 100644
>> --- a/kernel/bpf/verifier.c
>> +++ b/kernel/bpf/verifier.c
>> @@ -12597,10 +12597,14 @@ static int is_branch32_taken(struct bpf_reg_state *reg, u32 val, u8 opcode)
>>   	case BPF_JEQ:
>>   		if (tnum_is_const(subreg))
>>   			return !!tnum_equals_const(subreg, val);
>> +		else if (reg->u32_min_value > val)
>> +			return 0;
>>   		break;
> 
> The explanation makes sense to me, and I see similar min_value logic elsewhere
> in the switch for other jmp types. But those other jmp types are bounding the
> value from one side. Since JEQ and JNE test equality, can't we also add logic
> for u32_max_value here? e.g.
> 
>          case BPF_JEQ:
>                  if (tnum_is_const(subreg))
>                          return !!tnum_equals_const(subreg, val);
>                  else if (reg->u32_min_value > val || reg->u32_max_value < val)
>                          return 0;
>                  break;
> 
> Similar comment for rest of additions.
> 

Sounds good. I agree reg->u32_max_value < val should ensure the branch
not taken too. Will accommodate this change in the next revision.

>>   	case BPF_JNE:
>>   		if (tnum_is_const(subreg))
>>   			return !tnum_equals_const(subreg, val);
>> +		else if (reg->u32_min_value > val)
>> +			return 1;
>>   		break;
>>   	case BPF_JSET:
>>   		if ((~subreg.mask & subreg.value) & val)
>> @@ -12670,10 +12674,14 @@ static int is_branch64_taken(struct bpf_reg_state *reg, u64 val, u8 opcode)
>>   	case BPF_JEQ:
>>   		if (tnum_is_const(reg->var_off))
>>   			return !!tnum_equals_const(reg->var_off, val);
>> +		else if (reg->umin_value > val)
>> +			return 0;
>>   		break;
>>   	case BPF_JNE:
>>   		if (tnum_is_const(reg->var_off))
>>   			return !tnum_equals_const(reg->var_off, val);
>> +		else if (reg->umin_value > val)
>> +			return 1;
>>   		break;
>>   	case BPF_JSET:
>>   		if ((~reg->var_off.mask & reg->var_off.value) & val)

^ permalink raw reply	[flat|nested] 26+ messages in thread

* Re: [PATCH bpf-next 3/7] bpf: Improve handling of pattern '<const> <cond_op> <non_const>' in verifier
  2023-03-30 22:54   ` Dave Marchevsky
@ 2023-03-31 15:26     ` Yonghong Song
  2023-04-04 22:04     ` Andrii Nakryiko
  1 sibling, 0 replies; 26+ messages in thread
From: Yonghong Song @ 2023-03-31 15:26 UTC (permalink / raw)
  To: Dave Marchevsky, Yonghong Song, bpf
  Cc: Alexei Starovoitov, Andrii Nakryiko, Daniel Borkmann,
	kernel-team, Martin KaFai Lau



On 3/30/23 3:54 PM, Dave Marchevsky wrote:
> On 3/30/23 1:56 AM, Yonghong Song wrote:
>> Currently, the verifier does not handle '<const> <cond_op> <non_const>' well.
>> For example,
>>    ...
>>    10: (79) r1 = *(u64 *)(r10 -16)       ; R1_w=scalar() R10=fp0
>>    11: (b7) r2 = 0                       ; R2_w=0
>>    12: (2d) if r2 > r1 goto pc+2
>>    13: (b7) r0 = 0
>>    14: (95) exit
>>    15: (65) if r1 s> 0x1 goto pc+3
>>    16: (0f) r0 += r1
>>    ...
>> At insn 12, verifier decides both true and false branch are possible, but
>> actually only false branch is possible.
>>
>> Currently, the verifier already supports patterns '<non_const> <cond_op> <const>.
>> Add support for patterns '<const> <cond_op> <non_const>' in a similar way.
>>
>> Also fix selftest 'verifier_bounds_mix_sign_unsign/bounds checks mixing signed and unsigned, variant 10'
>> due to this change.
>>
>> Signed-off-by: Yonghong Song <yhs@fb.com>
>> ---
>>   kernel/bpf/verifier.c                                | 12 ++++++++++++
>>   .../bpf/progs/verifier_bounds_mix_sign_unsign.c      |  2 +-
>>   2 files changed, 13 insertions(+), 1 deletion(-)
>>
>> diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c
>> index 90bb6d25bc9c..d070943a8ba1 100644
>> --- a/kernel/bpf/verifier.c
>> +++ b/kernel/bpf/verifier.c
>> @@ -13302,6 +13302,18 @@ static int check_cond_jmp_op(struct bpf_verifier_env *env,
>>   				       src_reg->var_off.value,
>>   				       opcode,
>>   				       is_jmp32);
>> +	} else if (dst_reg->type == SCALAR_VALUE &&
>> +		   is_jmp32 && tnum_is_const(tnum_subreg(dst_reg->var_off))) {
>> +		pred = is_branch_taken(src_reg,
>> +				       tnum_subreg(dst_reg->var_off).value,
>> +				       flip_opcode(opcode),
>> +				       is_jmp32);
>> +	} else if (dst_reg->type == SCALAR_VALUE &&
>> +		   !is_jmp32 && tnum_is_const(dst_reg->var_off)) {
>> +		pred = is_branch_taken(src_reg,
>> +				       dst_reg->var_off.value,
>> +				       flip_opcode(opcode),
>> +				       is_jmp32);
>>   	} else if (reg_is_pkt_pointer_any(dst_reg) &&
>>   		   reg_is_pkt_pointer_any(src_reg) &&
>>   		   !is_jmp32) {
> 
> Looking at the two SCALAR_VALUE 'else if's above these added lines, these
> additions make sense. Having four separate 'else if' checks for essentially
> similar logic makes this hard to read, though, maybe it's an opportunity to
> refactor a bit.
> 
> While trying to make sense of the logic here I attempted to simplify with
> a helper:
> 
> @@ -13234,6 +13234,21 @@ static void find_equal_scalars(struct bpf_verifier_state *vstate,
>          }));
>   }
> 
> +static int maybe_const_operand_branch(struct tnum maybe_const_op,
> +                                     struct bpf_reg_state *other_op_reg,
> +                                     u8 opcode, bool is_jmp32)
> +{
> +       struct tnum jmp_tnum = is_jmp32 ? tnum_subreg(maybe_const_op) :
> +                                         maybe_const_op;
> +       if (!tnum_is_const(jmp_tnum))
> +               return -1;
> +
> +       return is_branch_taken(other_op_reg,
> +                              jmp_tnum.value,
> +                              opcode,
> +                              is_jmp32);
> +}
> +
>   static int check_cond_jmp_op(struct bpf_verifier_env *env,
>                               struct bpf_insn *insn, int *insn_idx)
>   {
> @@ -13287,18 +13302,12 @@ static int check_cond_jmp_op(struct bpf_verifier_env *env,
> 
>          if (BPF_SRC(insn->code) == BPF_K) {
>                  pred = is_branch_taken(dst_reg, insn->imm, opcode, is_jmp32);
> -       } else if (src_reg->type == SCALAR_VALUE &&
> -                  is_jmp32 && tnum_is_const(tnum_subreg(src_reg->var_off))) {
> -               pred = is_branch_taken(dst_reg,
> -                                      tnum_subreg(src_reg->var_off).value,
> -                                      opcode,
> -                                      is_jmp32);
> -       } else if (src_reg->type == SCALAR_VALUE &&
> -                  !is_jmp32 && tnum_is_const(src_reg->var_off)) {
> -               pred = is_branch_taken(dst_reg,
> -                                      src_reg->var_off.value,
> -                                      opcode,
> -                                      is_jmp32);
> +       } else if (src_reg->type == SCALAR_VALUE) {
> +               pred = maybe_const_operand_branch(src_reg->var_off, dst_reg,
> +                                                 opcode, is_jmp32);
> +       } else if (dst_reg->type == SCALAR_VALUE) {
> +               pred = maybe_const_operand_branch(dst_reg->var_off, src_reg,
> +                                                 flip_opcode(opcode), is_jmp32);
>          } else if (reg_is_pkt_pointer_any(dst_reg) &&
>                     reg_is_pkt_pointer_any(src_reg) &&
>                     !is_jmp32) {
> 
> 
> I think the resultant logic is the same as your patch, but it's easier to
> understand, for me at least. Note that I didn't test the above.

Thanks. Will do refactoring to simplify logic in the next revision.

^ permalink raw reply	[flat|nested] 26+ messages in thread

* Re: [PATCH bpf-next 5/7] bpf: Mark potential spilled loop index variable as precise
  2023-03-30  5:56 ` [PATCH bpf-next 5/7] bpf: Mark potential spilled loop index variable as precise Yonghong Song
@ 2023-03-31 21:54   ` Eduard Zingerman
  2023-03-31 23:39     ` Yonghong Song
  2023-04-04 22:09   ` Andrii Nakryiko
  1 sibling, 1 reply; 26+ messages in thread
From: Eduard Zingerman @ 2023-03-31 21:54 UTC (permalink / raw)
  To: Yonghong Song, bpf
  Cc: Alexei Starovoitov, Andrii Nakryiko, Daniel Borkmann,
	kernel-team, Martin KaFai Lau

On Wed, 2023-03-29 at 22:56 -0700, Yonghong Song wrote:
> For a loop, if loop index variable is spilled and between loop
> iterations, the only reg/spill state difference is spilled loop
> index variable, then verifier may assume an infinite loop which
> cause verification failure. In such cases, we should mark
> spilled loop index variable as precise to differentiate states
> between loop iterations.
> 
> Since verifier is not able to accurately identify loop index
> variable, add a heuristic such that if both old reg state and
> new reg state are consts, mark old reg state as precise which
> will trigger constant value comparison later.
> 
> Signed-off-by: Yonghong Song <yhs@fb.com>
> ---
>  kernel/bpf/verifier.c | 20 ++++++++++++++++++--
>  1 file changed, 18 insertions(+), 2 deletions(-)
> 
> diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c
> index d070943a8ba1..d1aa2c7ae7c0 100644
> --- a/kernel/bpf/verifier.c
> +++ b/kernel/bpf/verifier.c
> @@ -14850,6 +14850,23 @@ static bool stacksafe(struct bpf_verifier_env *env, struct bpf_func_state *old,
>  		/* Both old and cur are having same slot_type */
>  		switch (old->stack[spi].slot_type[BPF_REG_SIZE - 1]) {
>  		case STACK_SPILL:
> +			/* sometime loop index variable is spilled and the spill
> +			 * is not marked as precise. If only state difference
> +			 * between two iterations are spilled loop index, the
> +			 * "infinite loop detected at insn" error will be hit.
> +			 * Mark spilled constant as precise so it went through value
> +			 * comparison.
> +			 */
> +			old_reg = &old->stack[spi].spilled_ptr;
> +			cur_reg = &cur->stack[spi].spilled_ptr;
> +			if (!old_reg->precise) {
> +				if (old_reg->type == SCALAR_VALUE &&
> +				    cur_reg->type == SCALAR_VALUE &&
> +				    tnum_is_const(old_reg->var_off) &&
> +				    tnum_is_const(cur_reg->var_off))
> +					old_reg->precise = true;
> +			}
> +
>  			/* when explored and current stack slot are both storing
>  			 * spilled registers, check that stored pointers types
>  			 * are the same as well.
> @@ -14860,8 +14877,7 @@ static bool stacksafe(struct bpf_verifier_env *env, struct bpf_func_state *old,
>  			 * such verifier states are not equivalent.
>  			 * return false to continue verification of this path
>  			 */
> -			if (!regsafe(env, &old->stack[spi].spilled_ptr,
> -				     &cur->stack[spi].spilled_ptr, idmap))
> +			if (!regsafe(env, old_reg, cur_reg, idmap))
>  				return false;
>  			break;
>  		case STACK_DYNPTR:

Hi Yonghong,

If you are going for v2 of this patch-set, could you please consider
adding a parameter to regsafe() instead of modifying old state?
Maybe it's just me, but having old state immutable seems simpler to understand.
E.g., as in the patch in the end of this email (it's a patch on top of your series).

Interestingly, the version without old state modification also performs
better in veristat, although I did not analyze the reasons for this.

$ ./veristat -e file,prog,insns,states -f 'insns_pct>5' -C master-baseline.log modify-old.log 
File           Program                           Insns (A)  Insns (B)  Insns    (DIFF)  States (A)  States (B)  States  (DIFF)
-------------  --------------------------------  ---------  ---------  ---------------  ----------  ----------  --------------
bpf_host.o     tail_handle_ipv4_from_host             3391       3738   +347 (+10.23%)         231         249    +18 (+7.79%)
bpf_host.o     tail_handle_ipv6_from_host             4108       5131  +1023 (+24.90%)         244         278   +34 (+13.93%)
bpf_lxc.o      tail_ipv4_ct_egress                    5068       5931   +863 (+17.03%)         262         291   +29 (+11.07%)
bpf_lxc.o      tail_ipv4_ct_ingress                   5088       5958   +870 (+17.10%)         262         291   +29 (+11.07%)
bpf_lxc.o      tail_ipv4_ct_ingress_policy_only       5088       5958   +870 (+17.10%)         262         291   +29 (+11.07%)
bpf_lxc.o      tail_ipv6_ct_egress                    4593       5239   +646 (+14.06%)         194         214   +20 (+10.31%)
bpf_lxc.o      tail_ipv6_ct_ingress                   4606       5256   +650 (+14.11%)         194         214   +20 (+10.31%)
bpf_lxc.o      tail_ipv6_ct_ingress_policy_only       4606       5256   +650 (+14.11%)         194         214   +20 (+10.31%)
bpf_overlay.o  tail_rev_nodeport_lb6                  2865       4704  +1839 (+64.19%)         167         283  +116 (+69.46%)
loop6.bpf.o    trace_virtqueue_add_sgs               25017      29035  +4018 (+16.06%)         491         579   +88 (+17.92%)
loop7.bpf.o    trace_virtqueue_add_sgs               24379      28652  +4273 (+17.53%)         486         570   +84 (+17.28%)
-------------  --------------------------------  ---------  ---------  ---------------  ----------  ----------  --------------

$ ./veristat -e file,prog,insns,states -f 'insns_pct>5' -C master-baseline.log do-not-modify-old.log 
File           Program                     Insns (A)  Insns (B)  Insns    (DIFF)  States (A)  States (B)  States (DIFF)
-------------  --------------------------  ---------  ---------  ---------------  ----------  ----------  -------------
bpf_host.o     cil_to_netdev                    5996       6296    +300 (+5.00%)         362         380   +18 (+4.97%)
bpf_host.o     tail_handle_ipv4_from_host       3391       3738   +347 (+10.23%)         231         249   +18 (+7.79%)
bpf_host.o     tail_handle_ipv6_from_host       4108       5131  +1023 (+24.90%)         244         278  +34 (+13.93%)
bpf_overlay.o  tail_rev_nodeport_lb6            2865       3064    +199 (+6.95%)         167         181   +14 (+8.38%)
loop6.bpf.o    trace_virtqueue_add_sgs         25017      29035  +4018 (+16.06%)         491         579  +88 (+17.92%)
loop7.bpf.o    trace_virtqueue_add_sgs         24379      28652  +4273 (+17.53%)         486         570  +84 (+17.28%)
-------------  --------------------------  ---------  ---------  ---------------  ----------  ----------  -------------

(To do the veristat comparison I used the programs listed in tools/testing/selftests/bpf/veristat.cfg
 and a set of Cilium programs from git@github.com:anakryiko/cilium.git)

Thanks,
Eduard

---

diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c
index b189a5cf54d2..7ce0ef02d03d 100644
--- a/kernel/bpf/verifier.c
+++ b/kernel/bpf/verifier.c
@@ -14711,7 +14711,8 @@ static bool regs_exact(const struct bpf_reg_state *rold,
 
 /* Returns true if (rold safe implies rcur safe) */
 static bool regsafe(struct bpf_verifier_env *env, struct bpf_reg_state *rold,
-		    struct bpf_reg_state *rcur, struct bpf_id_pair *idmap)
+		    struct bpf_reg_state *rcur, struct bpf_id_pair *idmap,
+		    bool force_precise_const)
 {
 	if (!(rold->live & REG_LIVE_READ))
 		/* explored state didn't use this */
@@ -14752,7 +14753,9 @@ static bool regsafe(struct bpf_verifier_env *env, struct bpf_reg_state *rold,
 			return true;
 		if (env->explore_alu_limits)
 			return false;
-		if (!rold->precise)
+		if (!rold->precise && !(force_precise_const &&
+					tnum_is_const(rold->var_off) &&
+					tnum_is_const(rcur->var_off)))
 			return true;
 		/* new val must satisfy old val knowledge */
 		return range_within(rold, rcur) &&
@@ -14863,13 +14866,6 @@ static bool stacksafe(struct bpf_verifier_env *env, struct bpf_func_state *old,
 			 */
 			old_reg = &old->stack[spi].spilled_ptr;
 			cur_reg = &cur->stack[spi].spilled_ptr;
-			if (!old_reg->precise) {
-				if (old_reg->type == SCALAR_VALUE &&
-				    cur_reg->type == SCALAR_VALUE &&
-				    tnum_is_const(old_reg->var_off) &&
-				    tnum_is_const(cur_reg->var_off))
-					old_reg->precise = true;
-			}
 
 			/* when explored and current stack slot are both storing
 			 * spilled registers, check that stored pointers types
@@ -14881,7 +14877,7 @@ static bool stacksafe(struct bpf_verifier_env *env, struct bpf_func_state *old,
 			 * such verifier states are not equivalent.
 			 * return false to continue verification of this path
 			 */
-			if (!regsafe(env, old_reg, cur_reg, idmap))
+			if (!regsafe(env, old_reg, cur_reg, idmap, true))
 				return false;
 			break;
 		case STACK_DYNPTR:
@@ -14969,7 +14965,7 @@ static bool func_states_equal(struct bpf_verifier_env *env, struct bpf_func_stat
 
 	for (i = 0; i < MAX_BPF_REG; i++)
 		if (!regsafe(env, &old->regs[i], &cur->regs[i],
-			     env->idmap_scratch))
+			     env->idmap_scratch, false))
 			return false;
 
 	if (!stacksafe(env, old, cur, env->idmap_scratch))

^ permalink raw reply related	[flat|nested] 26+ messages in thread

* Re: [PATCH bpf-next 5/7] bpf: Mark potential spilled loop index variable as precise
  2023-03-31 21:54   ` Eduard Zingerman
@ 2023-03-31 23:39     ` Yonghong Song
  2023-04-03  1:48       ` Alexei Starovoitov
  0 siblings, 1 reply; 26+ messages in thread
From: Yonghong Song @ 2023-03-31 23:39 UTC (permalink / raw)
  To: Eduard Zingerman, Yonghong Song, bpf
  Cc: Alexei Starovoitov, Andrii Nakryiko, Daniel Borkmann,
	kernel-team, Martin KaFai Lau



On 3/31/23 2:54 PM, Eduard Zingerman wrote:
> On Wed, 2023-03-29 at 22:56 -0700, Yonghong Song wrote:
>> For a loop, if loop index variable is spilled and between loop
>> iterations, the only reg/spill state difference is spilled loop
>> index variable, then verifier may assume an infinite loop which
>> cause verification failure. In such cases, we should mark
>> spilled loop index variable as precise to differentiate states
>> between loop iterations.
>>
>> Since verifier is not able to accurately identify loop index
>> variable, add a heuristic such that if both old reg state and
>> new reg state are consts, mark old reg state as precise which
>> will trigger constant value comparison later.
>>
>> Signed-off-by: Yonghong Song <yhs@fb.com>
>> ---
>>   kernel/bpf/verifier.c | 20 ++++++++++++++++++--
>>   1 file changed, 18 insertions(+), 2 deletions(-)
>>
>> diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c
>> index d070943a8ba1..d1aa2c7ae7c0 100644
>> --- a/kernel/bpf/verifier.c
>> +++ b/kernel/bpf/verifier.c
>> @@ -14850,6 +14850,23 @@ static bool stacksafe(struct bpf_verifier_env *env, struct bpf_func_state *old,
>>   		/* Both old and cur are having same slot_type */
>>   		switch (old->stack[spi].slot_type[BPF_REG_SIZE - 1]) {
>>   		case STACK_SPILL:
>> +			/* sometime loop index variable is spilled and the spill
>> +			 * is not marked as precise. If only state difference
>> +			 * between two iterations are spilled loop index, the
>> +			 * "infinite loop detected at insn" error will be hit.
>> +			 * Mark spilled constant as precise so it went through value
>> +			 * comparison.
>> +			 */
>> +			old_reg = &old->stack[spi].spilled_ptr;
>> +			cur_reg = &cur->stack[spi].spilled_ptr;
>> +			if (!old_reg->precise) {
>> +				if (old_reg->type == SCALAR_VALUE &&
>> +				    cur_reg->type == SCALAR_VALUE &&
>> +				    tnum_is_const(old_reg->var_off) &&
>> +				    tnum_is_const(cur_reg->var_off))
>> +					old_reg->precise = true;
>> +			}
>> +
>>   			/* when explored and current stack slot are both storing
>>   			 * spilled registers, check that stored pointers types
>>   			 * are the same as well.
>> @@ -14860,8 +14877,7 @@ static bool stacksafe(struct bpf_verifier_env *env, struct bpf_func_state *old,
>>   			 * such verifier states are not equivalent.
>>   			 * return false to continue verification of this path
>>   			 */
>> -			if (!regsafe(env, &old->stack[spi].spilled_ptr,
>> -				     &cur->stack[spi].spilled_ptr, idmap))
>> +			if (!regsafe(env, old_reg, cur_reg, idmap))
>>   				return false;
>>   			break;
>>   		case STACK_DYNPTR:
> 
> Hi Yonghong,
> 
> If you are going for v2 of this patch-set, could you please consider
> adding a parameter to regsafe() instead of modifying old state?
> Maybe it's just me, but having old state immutable seems simpler to understand.
> E.g., as in the patch in the end of this email (it's a patch on top of your series).
> 
> Interestingly, the version without old state modification also performs
> better in veristat, although I did not analyze the reasons for this.

Thanks for suggestion. Agree that my change may cause other side effects
as I explicit marked 'old_reg' as precise. Do not mark 'old_reg' with 
precise should minimize the impact.
Will make the change in the next revision.

> 
> $ ./veristat -e file,prog,insns,states -f 'insns_pct>5' -C master-baseline.log modify-old.log
> File           Program                           Insns (A)  Insns (B)  Insns    (DIFF)  States (A)  States (B)  States  (DIFF)
> -------------  --------------------------------  ---------  ---------  ---------------  ----------  ----------  --------------
> bpf_host.o     tail_handle_ipv4_from_host             3391       3738   +347 (+10.23%)         231         249    +18 (+7.79%)
> bpf_host.o     tail_handle_ipv6_from_host             4108       5131  +1023 (+24.90%)         244         278   +34 (+13.93%)
> bpf_lxc.o      tail_ipv4_ct_egress                    5068       5931   +863 (+17.03%)         262         291   +29 (+11.07%)
> bpf_lxc.o      tail_ipv4_ct_ingress                   5088       5958   +870 (+17.10%)         262         291   +29 (+11.07%)
> bpf_lxc.o      tail_ipv4_ct_ingress_policy_only       5088       5958   +870 (+17.10%)         262         291   +29 (+11.07%)
> bpf_lxc.o      tail_ipv6_ct_egress                    4593       5239   +646 (+14.06%)         194         214   +20 (+10.31%)
> bpf_lxc.o      tail_ipv6_ct_ingress                   4606       5256   +650 (+14.11%)         194         214   +20 (+10.31%)
> bpf_lxc.o      tail_ipv6_ct_ingress_policy_only       4606       5256   +650 (+14.11%)         194         214   +20 (+10.31%)
> bpf_overlay.o  tail_rev_nodeport_lb6                  2865       4704  +1839 (+64.19%)         167         283  +116 (+69.46%)
> loop6.bpf.o    trace_virtqueue_add_sgs               25017      29035  +4018 (+16.06%)         491         579   +88 (+17.92%)
> loop7.bpf.o    trace_virtqueue_add_sgs               24379      28652  +4273 (+17.53%)         486         570   +84 (+17.28%)
> -------------  --------------------------------  ---------  ---------  ---------------  ----------  ----------  --------------
> 
> $ ./veristat -e file,prog,insns,states -f 'insns_pct>5' -C master-baseline.log do-not-modify-old.log
> File           Program                     Insns (A)  Insns (B)  Insns    (DIFF)  States (A)  States (B)  States (DIFF)
> -------------  --------------------------  ---------  ---------  ---------------  ----------  ----------  -------------
> bpf_host.o     cil_to_netdev                    5996       6296    +300 (+5.00%)         362         380   +18 (+4.97%)
> bpf_host.o     tail_handle_ipv4_from_host       3391       3738   +347 (+10.23%)         231         249   +18 (+7.79%)
> bpf_host.o     tail_handle_ipv6_from_host       4108       5131  +1023 (+24.90%)         244         278  +34 (+13.93%)
> bpf_overlay.o  tail_rev_nodeport_lb6            2865       3064    +199 (+6.95%)         167         181   +14 (+8.38%)
> loop6.bpf.o    trace_virtqueue_add_sgs         25017      29035  +4018 (+16.06%)         491         579  +88 (+17.92%)
> loop7.bpf.o    trace_virtqueue_add_sgs         24379      28652  +4273 (+17.53%)         486         570  +84 (+17.28%)
> -------------  --------------------------  ---------  ---------  ---------------  ----------  ----------  -------------
> 
> (To do the veristat comparison I used the programs listed in tools/testing/selftests/bpf/veristat.cfg
>   and a set of Cilium programs from git@github.com:anakryiko/cilium.git)
> 
> Thanks,
> Eduard
> 
> ---
> 
> diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c
> index b189a5cf54d2..7ce0ef02d03d 100644
> --- a/kernel/bpf/verifier.c
> +++ b/kernel/bpf/verifier.c
> @@ -14711,7 +14711,8 @@ static bool regs_exact(const struct bpf_reg_state *rold,
>   
>   /* Returns true if (rold safe implies rcur safe) */
>   static bool regsafe(struct bpf_verifier_env *env, struct bpf_reg_state *rold,
> -		    struct bpf_reg_state *rcur, struct bpf_id_pair *idmap)
> +		    struct bpf_reg_state *rcur, struct bpf_id_pair *idmap,
> +		    bool force_precise_const)
>   {
>   	if (!(rold->live & REG_LIVE_READ))
>   		/* explored state didn't use this */
> @@ -14752,7 +14753,9 @@ static bool regsafe(struct bpf_verifier_env *env, struct bpf_reg_state *rold,
>   			return true;
>   		if (env->explore_alu_limits)
>   			return false;
> -		if (!rold->precise)
> +		if (!rold->precise && !(force_precise_const &&
> +					tnum_is_const(rold->var_off) &&
> +					tnum_is_const(rcur->var_off)))
>   			return true;
>   		/* new val must satisfy old val knowledge */
>   		return range_within(rold, rcur) &&
> @@ -14863,13 +14866,6 @@ static bool stacksafe(struct bpf_verifier_env *env, struct bpf_func_state *old,
>   			 */
>   			old_reg = &old->stack[spi].spilled_ptr;
>   			cur_reg = &cur->stack[spi].spilled_ptr;
> -			if (!old_reg->precise) {
> -				if (old_reg->type == SCALAR_VALUE &&
> -				    cur_reg->type == SCALAR_VALUE &&
> -				    tnum_is_const(old_reg->var_off) &&
> -				    tnum_is_const(cur_reg->var_off))
> -					old_reg->precise = true;
> -			}
>   
>   			/* when explored and current stack slot are both storing
>   			 * spilled registers, check that stored pointers types
> @@ -14881,7 +14877,7 @@ static bool stacksafe(struct bpf_verifier_env *env, struct bpf_func_state *old,
>   			 * such verifier states are not equivalent.
>   			 * return false to continue verification of this path
>   			 */
> -			if (!regsafe(env, old_reg, cur_reg, idmap))
> +			if (!regsafe(env, old_reg, cur_reg, idmap, true))
>   				return false;
>   			break;
>   		case STACK_DYNPTR:
> @@ -14969,7 +14965,7 @@ static bool func_states_equal(struct bpf_verifier_env *env, struct bpf_func_stat
>   
>   	for (i = 0; i < MAX_BPF_REG; i++)
>   		if (!regsafe(env, &old->regs[i], &cur->regs[i],
> -			     env->idmap_scratch))
> +			     env->idmap_scratch, false))
>   			return false;
>   
>   	if (!stacksafe(env, old, cur, env->idmap_scratch))

^ permalink raw reply	[flat|nested] 26+ messages in thread

* Re: [PATCH bpf-next 7/7] selftests/bpf: Add a new test based on loop6.c
  2023-03-30  5:56 ` [PATCH bpf-next 7/7] selftests/bpf: Add a new test based on loop6.c Yonghong Song
@ 2023-04-03  1:39   ` Alexei Starovoitov
  2023-04-03  3:59     ` Yonghong Song
  0 siblings, 1 reply; 26+ messages in thread
From: Alexei Starovoitov @ 2023-04-03  1:39 UTC (permalink / raw)
  To: Yonghong Song
  Cc: bpf, Alexei Starovoitov, Andrii Nakryiko, Daniel Borkmann,
	kernel-team, Martin KaFai Lau

On Wed, Mar 29, 2023 at 10:56:36PM -0700, Yonghong Song wrote:
> With LLVM commit [1], loop6.c will fail verification without Commit 3c2611bac08a
> ("selftests/bpf: Fix trace_virtqueue_add_sgs test issue with LLVM 17.").
> Also, there is an effort to fix LLVM since LLVM17 may be used by old kernels
> for bpf development.
> 
> A new test is added by manually doing similar transformation in [1]
> so it can be used to test related verifier changes.
> 
>   [1] https://reviews.llvm.org/D143726
> 
> Signed-off-by: Yonghong Song <yhs@fb.com>
> ---
>  .../bpf/prog_tests/bpf_verif_scale.c          |   5 +
>  tools/testing/selftests/bpf/progs/loop7.c     | 102 ++++++++++++++++++
>  2 files changed, 107 insertions(+)
>  create mode 100644 tools/testing/selftests/bpf/progs/loop7.c
> 
> diff --git a/tools/testing/selftests/bpf/prog_tests/bpf_verif_scale.c b/tools/testing/selftests/bpf/prog_tests/bpf_verif_scale.c
> index 731c343897d8..cb708235e654 100644
> --- a/tools/testing/selftests/bpf/prog_tests/bpf_verif_scale.c
> +++ b/tools/testing/selftests/bpf/prog_tests/bpf_verif_scale.c
> @@ -180,6 +180,11 @@ void test_verif_scale_loop6()
>  	scale_test("loop6.bpf.o", BPF_PROG_TYPE_KPROBE, false);
>  }
>  
> +void test_verif_scale_loop7()
> +{
> +	scale_test("loop7.bpf.o", BPF_PROG_TYPE_KPROBE, false);
> +}
> +
>  void test_verif_scale_strobemeta()
>  {
>  	/* partial unroll. 19k insn in a loop.
> diff --git a/tools/testing/selftests/bpf/progs/loop7.c b/tools/testing/selftests/bpf/progs/loop7.c
> new file mode 100644
> index 000000000000..b234ed6f0038
> --- /dev/null
> +++ b/tools/testing/selftests/bpf/progs/loop7.c
> @@ -0,0 +1,102 @@
> +// SPDX-License-Identifier: GPL-2.0
> +
> +#include <linux/ptrace.h>
> +#include <stddef.h>
> +#include <linux/bpf.h>
> +#include <bpf/bpf_helpers.h>
> +#include <bpf/bpf_tracing.h>
> +#include "bpf_misc.h"
> +
> +char _license[] SEC("license") = "GPL";
> +
> +/* typically virtio scsi has max SGs of 6 */
> +#define VIRTIO_MAX_SGS	6
> +
> +/* Verifier will fail with SG_MAX = 128. The failure can be
> + * workarounded with a smaller SG_MAX, e.g. 10.
> + */
> +#define WORKAROUND
> +#ifdef WORKAROUND
> +#define SG_MAX		10
> +#else
> +/* typically virtio blk has max SEG of 128 */
> +#define SG_MAX		128
> +#endif
> +
> +#define SG_CHAIN	0x01UL
> +#define SG_END		0x02UL
> +
> +struct scatterlist {
> +	unsigned long   page_link;
> +	unsigned int    offset;
> +	unsigned int    length;
> +};
> +
> +#define sg_is_chain(sg)		((sg)->page_link & SG_CHAIN)
> +#define sg_is_last(sg)		((sg)->page_link & SG_END)
> +#define sg_chain_ptr(sg)	\
> +	((struct scatterlist *) ((sg)->page_link & ~(SG_CHAIN | SG_END)))
> +
> +static inline struct scatterlist *__sg_next(struct scatterlist *sgp)
> +{
> +	struct scatterlist sg;
> +
> +	bpf_probe_read_kernel(&sg, sizeof(sg), sgp);
> +	if (sg_is_last(&sg))
> +		return NULL;
> +
> +	sgp++;
> +
> +	bpf_probe_read_kernel(&sg, sizeof(sg), sgp);
> +	if (sg_is_chain(&sg))
> +		sgp = sg_chain_ptr(&sg);
> +
> +	return sgp;
> +}
> +
> +static inline struct scatterlist *get_sgp(struct scatterlist **sgs, int i)
> +{
> +	struct scatterlist *sgp;
> +
> +	bpf_probe_read_kernel(&sgp, sizeof(sgp), sgs + i);
> +	return sgp;
> +}
> +
> +int config = 0;
> +int result = 0;
> +
> +SEC("kprobe/virtqueue_add_sgs")
> +int BPF_KPROBE(trace_virtqueue_add_sgs, void *unused, struct scatterlist **sgs,
> +	       unsigned int out_sgs, unsigned int in_sgs)
> +{
> +	struct scatterlist *sgp = NULL;
> +	__u64 length1 = 0, length2 = 0;
> +	unsigned int i, n, len, upper;
> +
> +	if (config != 0)
> +		return 0;
> +
> +	upper = out_sgs < VIRTIO_MAX_SGS ? out_sgs : VIRTIO_MAX_SGS;
> +	for (i = 0; i < upper; i++) {

since this test is doing manual hoistMinMax, let's keep __sink() in test 6,
so we guaranteed to have both flavors regardless of compiler choices?

^ permalink raw reply	[flat|nested] 26+ messages in thread

* Re: [PATCH bpf-next 5/7] bpf: Mark potential spilled loop index variable as precise
  2023-03-31 23:39     ` Yonghong Song
@ 2023-04-03  1:48       ` Alexei Starovoitov
  2023-04-03  4:04         ` Yonghong Song
  0 siblings, 1 reply; 26+ messages in thread
From: Alexei Starovoitov @ 2023-04-03  1:48 UTC (permalink / raw)
  To: Yonghong Song
  Cc: Eduard Zingerman, Yonghong Song, bpf, Alexei Starovoitov,
	Andrii Nakryiko, Daniel Borkmann, kernel-team, Martin KaFai Lau

On Fri, Mar 31, 2023 at 04:39:29PM -0700, Yonghong Song wrote:
> 
> 
> On 3/31/23 2:54 PM, Eduard Zingerman wrote:
> > On Wed, 2023-03-29 at 22:56 -0700, Yonghong Song wrote:
> > > For a loop, if loop index variable is spilled and between loop
> > > iterations, the only reg/spill state difference is spilled loop
> > > index variable, then verifier may assume an infinite loop which
> > > cause verification failure. In such cases, we should mark
> > > spilled loop index variable as precise to differentiate states
> > > between loop iterations.
> > > 
> > > Since verifier is not able to accurately identify loop index
> > > variable, add a heuristic such that if both old reg state and
> > > new reg state are consts, mark old reg state as precise which
> > > will trigger constant value comparison later.
> > > 
> > > Signed-off-by: Yonghong Song <yhs@fb.com>
> > > ---
> > >   kernel/bpf/verifier.c | 20 ++++++++++++++++++--
> > >   1 file changed, 18 insertions(+), 2 deletions(-)
> > > 
> > > diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c
> > > index d070943a8ba1..d1aa2c7ae7c0 100644
> > > --- a/kernel/bpf/verifier.c
> > > +++ b/kernel/bpf/verifier.c
> > > @@ -14850,6 +14850,23 @@ static bool stacksafe(struct bpf_verifier_env *env, struct bpf_func_state *old,
> > >   		/* Both old and cur are having same slot_type */
> > >   		switch (old->stack[spi].slot_type[BPF_REG_SIZE - 1]) {
> > >   		case STACK_SPILL:
> > > +			/* sometime loop index variable is spilled and the spill
> > > +			 * is not marked as precise. If only state difference
> > > +			 * between two iterations are spilled loop index, the
> > > +			 * "infinite loop detected at insn" error will be hit.
> > > +			 * Mark spilled constant as precise so it went through value
> > > +			 * comparison.
> > > +			 */
> > > +			old_reg = &old->stack[spi].spilled_ptr;
> > > +			cur_reg = &cur->stack[spi].spilled_ptr;
> > > +			if (!old_reg->precise) {
> > > +				if (old_reg->type == SCALAR_VALUE &&
> > > +				    cur_reg->type == SCALAR_VALUE &&
> > > +				    tnum_is_const(old_reg->var_off) &&
> > > +				    tnum_is_const(cur_reg->var_off))
> > > +					old_reg->precise = true;
> > > +			}
> > > +
> > >   			/* when explored and current stack slot are both storing
> > >   			 * spilled registers, check that stored pointers types
> > >   			 * are the same as well.
> > > @@ -14860,8 +14877,7 @@ static bool stacksafe(struct bpf_verifier_env *env, struct bpf_func_state *old,
> > >   			 * such verifier states are not equivalent.
> > >   			 * return false to continue verification of this path
> > >   			 */
> > > -			if (!regsafe(env, &old->stack[spi].spilled_ptr,
> > > -				     &cur->stack[spi].spilled_ptr, idmap))
> > > +			if (!regsafe(env, old_reg, cur_reg, idmap))
> > >   				return false;
> > >   			break;
> > >   		case STACK_DYNPTR:
> > 
> > Hi Yonghong,
> > 
> > If you are going for v2 of this patch-set, could you please consider
> > adding a parameter to regsafe() instead of modifying old state?
> > Maybe it's just me, but having old state immutable seems simpler to understand.
> > E.g., as in the patch in the end of this email (it's a patch on top of your series).
> > 
> > Interestingly, the version without old state modification also performs
> > better in veristat, although I did not analyze the reasons for this.
> 
> Thanks for suggestion. Agree that my change may cause other side effects
> as I explicit marked 'old_reg' as precise. Do not mark 'old_reg' with
> precise should minimize the impact.
> Will make the change in the next revision.

Could you also post veristat before/after difference after patch 1, 3 and 5.
I suspect there should be minimal delta for 1 and 3, but 5 can make both positive
and negative effect.

> > +		if (!rold->precise && !(force_precise_const &&
> > +					tnum_is_const(rold->var_off) &&
> > +					tnum_is_const(rcur->var_off)))

... and if there are negative consequences for patch 5 we might tighten this heuristic.
Like check that rcur->var_off.value - rold->var_off.value == 1 or -1 or bounded
by some small number. If it's truly index var it shouldn't have enormous delta.
But if patch 5 doesn't cause negative effect it would be better to keep it as-is.

^ permalink raw reply	[flat|nested] 26+ messages in thread

* Re: [PATCH bpf-next 7/7] selftests/bpf: Add a new test based on loop6.c
  2023-04-03  1:39   ` Alexei Starovoitov
@ 2023-04-03  3:59     ` Yonghong Song
  0 siblings, 0 replies; 26+ messages in thread
From: Yonghong Song @ 2023-04-03  3:59 UTC (permalink / raw)
  To: Alexei Starovoitov, Yonghong Song
  Cc: bpf, Alexei Starovoitov, Andrii Nakryiko, Daniel Borkmann,
	kernel-team, Martin KaFai Lau



On 4/2/23 6:39 PM, Alexei Starovoitov wrote:
> On Wed, Mar 29, 2023 at 10:56:36PM -0700, Yonghong Song wrote:
>> With LLVM commit [1], loop6.c will fail verification without Commit 3c2611bac08a
>> ("selftests/bpf: Fix trace_virtqueue_add_sgs test issue with LLVM 17.").
>> Also, there is an effort to fix LLVM since LLVM17 may be used by old kernels
>> for bpf development.
>>
>> A new test is added by manually doing similar transformation in [1]
>> so it can be used to test related verifier changes.
>>
>>    [1] https://reviews.llvm.org/D143726
>>
>> Signed-off-by: Yonghong Song <yhs@fb.com>
>> ---
>>   .../bpf/prog_tests/bpf_verif_scale.c          |   5 +
>>   tools/testing/selftests/bpf/progs/loop7.c     | 102 ++++++++++++++++++
>>   2 files changed, 107 insertions(+)
>>   create mode 100644 tools/testing/selftests/bpf/progs/loop7.c
>>
>> diff --git a/tools/testing/selftests/bpf/prog_tests/bpf_verif_scale.c b/tools/testing/selftests/bpf/prog_tests/bpf_verif_scale.c
>> index 731c343897d8..cb708235e654 100644
>> --- a/tools/testing/selftests/bpf/prog_tests/bpf_verif_scale.c
>> +++ b/tools/testing/selftests/bpf/prog_tests/bpf_verif_scale.c
>> @@ -180,6 +180,11 @@ void test_verif_scale_loop6()
>>   	scale_test("loop6.bpf.o", BPF_PROG_TYPE_KPROBE, false);
>>   }
>>   
>> +void test_verif_scale_loop7()
>> +{
>> +	scale_test("loop7.bpf.o", BPF_PROG_TYPE_KPROBE, false);
>> +}
>> +
>>   void test_verif_scale_strobemeta()
>>   {
>>   	/* partial unroll. 19k insn in a loop.
>> diff --git a/tools/testing/selftests/bpf/progs/loop7.c b/tools/testing/selftests/bpf/progs/loop7.c
>> new file mode 100644
>> index 000000000000..b234ed6f0038
>> --- /dev/null
>> +++ b/tools/testing/selftests/bpf/progs/loop7.c
>> @@ -0,0 +1,102 @@
>> +// SPDX-License-Identifier: GPL-2.0
>> +
>> +#include <linux/ptrace.h>
>> +#include <stddef.h>
>> +#include <linux/bpf.h>
>> +#include <bpf/bpf_helpers.h>
>> +#include <bpf/bpf_tracing.h>
>> +#include "bpf_misc.h"
>> +
>> +char _license[] SEC("license") = "GPL";
>> +
>> +/* typically virtio scsi has max SGs of 6 */
>> +#define VIRTIO_MAX_SGS	6
>> +
>> +/* Verifier will fail with SG_MAX = 128. The failure can be
>> + * workarounded with a smaller SG_MAX, e.g. 10.
>> + */
>> +#define WORKAROUND
>> +#ifdef WORKAROUND
>> +#define SG_MAX		10
>> +#else
>> +/* typically virtio blk has max SEG of 128 */
>> +#define SG_MAX		128
>> +#endif
>> +
>> +#define SG_CHAIN	0x01UL
>> +#define SG_END		0x02UL
>> +
>> +struct scatterlist {
>> +	unsigned long   page_link;
>> +	unsigned int    offset;
>> +	unsigned int    length;
>> +};
>> +
>> +#define sg_is_chain(sg)		((sg)->page_link & SG_CHAIN)
>> +#define sg_is_last(sg)		((sg)->page_link & SG_END)
>> +#define sg_chain_ptr(sg)	\
>> +	((struct scatterlist *) ((sg)->page_link & ~(SG_CHAIN | SG_END)))
>> +
>> +static inline struct scatterlist *__sg_next(struct scatterlist *sgp)
>> +{
>> +	struct scatterlist sg;
>> +
>> +	bpf_probe_read_kernel(&sg, sizeof(sg), sgp);
>> +	if (sg_is_last(&sg))
>> +		return NULL;
>> +
>> +	sgp++;
>> +
>> +	bpf_probe_read_kernel(&sg, sizeof(sg), sgp);
>> +	if (sg_is_chain(&sg))
>> +		sgp = sg_chain_ptr(&sg);
>> +
>> +	return sgp;
>> +}
>> +
>> +static inline struct scatterlist *get_sgp(struct scatterlist **sgs, int i)
>> +{
>> +	struct scatterlist *sgp;
>> +
>> +	bpf_probe_read_kernel(&sgp, sizeof(sgp), sgs + i);
>> +	return sgp;
>> +}
>> +
>> +int config = 0;
>> +int result = 0;
>> +
>> +SEC("kprobe/virtqueue_add_sgs")
>> +int BPF_KPROBE(trace_virtqueue_add_sgs, void *unused, struct scatterlist **sgs,
>> +	       unsigned int out_sgs, unsigned int in_sgs)
>> +{
>> +	struct scatterlist *sgp = NULL;
>> +	__u64 length1 = 0, length2 = 0;
>> +	unsigned int i, n, len, upper;
>> +
>> +	if (config != 0)
>> +		return 0;
>> +
>> +	upper = out_sgs < VIRTIO_MAX_SGS ? out_sgs : VIRTIO_MAX_SGS;
>> +	for (i = 0; i < upper; i++) {
> 
> since this test is doing manual hoistMinMax, let's keep __sink() in test 6,
> so we guaranteed to have both flavors regardless of compiler choices?

Sounds good to me. Will drop patch 6.

^ permalink raw reply	[flat|nested] 26+ messages in thread

* Re: [PATCH bpf-next 5/7] bpf: Mark potential spilled loop index variable as precise
  2023-04-03  1:48       ` Alexei Starovoitov
@ 2023-04-03  4:04         ` Yonghong Song
  0 siblings, 0 replies; 26+ messages in thread
From: Yonghong Song @ 2023-04-03  4:04 UTC (permalink / raw)
  To: Alexei Starovoitov
  Cc: Eduard Zingerman, Yonghong Song, bpf, Alexei Starovoitov,
	Andrii Nakryiko, Daniel Borkmann, kernel-team, Martin KaFai Lau



On 4/2/23 6:48 PM, Alexei Starovoitov wrote:
> On Fri, Mar 31, 2023 at 04:39:29PM -0700, Yonghong Song wrote:
>>
>>
>> On 3/31/23 2:54 PM, Eduard Zingerman wrote:
>>> On Wed, 2023-03-29 at 22:56 -0700, Yonghong Song wrote:
>>>> For a loop, if loop index variable is spilled and between loop
>>>> iterations, the only reg/spill state difference is spilled loop
>>>> index variable, then verifier may assume an infinite loop which
>>>> cause verification failure. In such cases, we should mark
>>>> spilled loop index variable as precise to differentiate states
>>>> between loop iterations.
>>>>
>>>> Since verifier is not able to accurately identify loop index
>>>> variable, add a heuristic such that if both old reg state and
>>>> new reg state are consts, mark old reg state as precise which
>>>> will trigger constant value comparison later.
>>>>
>>>> Signed-off-by: Yonghong Song <yhs@fb.com>
>>>> ---
>>>>    kernel/bpf/verifier.c | 20 ++++++++++++++++++--
>>>>    1 file changed, 18 insertions(+), 2 deletions(-)
>>>>
>>>> diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c
>>>> index d070943a8ba1..d1aa2c7ae7c0 100644
>>>> --- a/kernel/bpf/verifier.c
>>>> +++ b/kernel/bpf/verifier.c
>>>> @@ -14850,6 +14850,23 @@ static bool stacksafe(struct bpf_verifier_env *env, struct bpf_func_state *old,
>>>>    		/* Both old and cur are having same slot_type */
>>>>    		switch (old->stack[spi].slot_type[BPF_REG_SIZE - 1]) {
>>>>    		case STACK_SPILL:
>>>> +			/* sometime loop index variable is spilled and the spill
>>>> +			 * is not marked as precise. If only state difference
>>>> +			 * between two iterations are spilled loop index, the
>>>> +			 * "infinite loop detected at insn" error will be hit.
>>>> +			 * Mark spilled constant as precise so it went through value
>>>> +			 * comparison.
>>>> +			 */
>>>> +			old_reg = &old->stack[spi].spilled_ptr;
>>>> +			cur_reg = &cur->stack[spi].spilled_ptr;
>>>> +			if (!old_reg->precise) {
>>>> +				if (old_reg->type == SCALAR_VALUE &&
>>>> +				    cur_reg->type == SCALAR_VALUE &&
>>>> +				    tnum_is_const(old_reg->var_off) &&
>>>> +				    tnum_is_const(cur_reg->var_off))
>>>> +					old_reg->precise = true;
>>>> +			}
>>>> +
>>>>    			/* when explored and current stack slot are both storing
>>>>    			 * spilled registers, check that stored pointers types
>>>>    			 * are the same as well.
>>>> @@ -14860,8 +14877,7 @@ static bool stacksafe(struct bpf_verifier_env *env, struct bpf_func_state *old,
>>>>    			 * such verifier states are not equivalent.
>>>>    			 * return false to continue verification of this path
>>>>    			 */
>>>> -			if (!regsafe(env, &old->stack[spi].spilled_ptr,
>>>> -				     &cur->stack[spi].spilled_ptr, idmap))
>>>> +			if (!regsafe(env, old_reg, cur_reg, idmap))
>>>>    				return false;
>>>>    			break;
>>>>    		case STACK_DYNPTR:
>>>
>>> Hi Yonghong,
>>>
>>> If you are going for v2 of this patch-set, could you please consider
>>> adding a parameter to regsafe() instead of modifying old state?
>>> Maybe it's just me, but having old state immutable seems simpler to understand.
>>> E.g., as in the patch in the end of this email (it's a patch on top of your series).
>>>
>>> Interestingly, the version without old state modification also performs
>>> better in veristat, although I did not analyze the reasons for this.
>>
>> Thanks for suggestion. Agree that my change may cause other side effects
>> as I explicit marked 'old_reg' as precise. Do not mark 'old_reg' with
>> precise should minimize the impact.
>> Will make the change in the next revision.
> 
> Could you also post veristat before/after difference after patch 1, 3 and 5.
> I suspect there should be minimal delta for 1 and 3, but 5 can make both positive
> and negative effect.
> 
>>> +		if (!rold->precise && !(force_precise_const &&
>>> +					tnum_is_const(rold->var_off) &&
>>> +					tnum_is_const(rcur->var_off)))
> 
> ... and if there are negative consequences for patch 5 we might tighten this heuristic.
> Like check that rcur->var_off.value - rold->var_off.value == 1 or -1 or bounded
> by some small number. If it's truly index var it shouldn't have enormous delta.
> But if patch 5 doesn't cause negative effect it would be better to keep it as-is.

Sounds good. Will further experiment with more tightening like 
difference with a small +/- number, which should further reduce the 
number of processed states. But as you said we can decide whether this 
is needed based on how much it will further save.

^ permalink raw reply	[flat|nested] 26+ messages in thread

* Re: [PATCH bpf-next 0/7] bpf: Improve verifier for cond_op and spilled loop index variables
  2023-03-30  5:56 [PATCH bpf-next 0/7] bpf: Improve verifier for cond_op and spilled loop index variables Yonghong Song
                   ` (6 preceding siblings ...)
  2023-03-30  5:56 ` [PATCH bpf-next 7/7] selftests/bpf: Add a new test based on loop6.c Yonghong Song
@ 2023-04-04 21:46 ` Andrii Nakryiko
  2023-04-06 16:49   ` Yonghong Song
  7 siblings, 1 reply; 26+ messages in thread
From: Andrii Nakryiko @ 2023-04-04 21:46 UTC (permalink / raw)
  To: Yonghong Song
  Cc: bpf, Alexei Starovoitov, Andrii Nakryiko, Daniel Borkmann,
	kernel-team, Martin KaFai Lau

On Wed, Mar 29, 2023 at 10:56 PM Yonghong Song <yhs@fb.com> wrote:
>
> LLVM commit [1] introduced hoistMinMax optimization like
>   (i < VIRTIO_MAX_SGS) && (i < out_sgs)
> to
>   upper = MIN(VIRTIO_MAX_SGS, out_sgs)
>   ... i < upper ...
> and caused the verification failure. Commit [2] workarounded the issue by
> adding some bpf assembly code to prohibit the above optimization.
> This patch improved verifier such that verification can succeed without
> the above workaround.
>
> Without [2], the current verifier will hit the following failures:
>   ...
>   119: (15) if r1 == 0x0 goto pc+1
>   The sequence of 8193 jumps is too complex.
>   verification time 525829 usec
>   stack depth 64
>   processed 156616 insns (limit 1000000) max_states_per_insn 8 total_states 1754 peak_states 1712 mark_read 12
>   -- END PROG LOAD LOG --
>   libbpf: prog 'trace_virtqueue_add_sgs': failed to load: -14
>   libbpf: failed to load object 'loop6.bpf.o'
>   ...
> The failure is due to verifier inadequately handling '<const> <cond_op> <non_const>' which will
> go through both pathes and generate the following verificaiton states:
>   ...
>   89: (07) r2 += 1                      ; R2_w=5
>   90: (79) r8 = *(u64 *)(r10 -48)       ; R8_w=scalar() R10=fp0
>   91: (79) r1 = *(u64 *)(r10 -56)       ; R1_w=scalar(umax=5,var_off=(0x0; 0x7)) R10=fp0
>   92: (ad) if r2 < r1 goto pc+41        ; R0_w=scalar() R1_w=scalar(umin=6,umax=5,var_off=(0x4; 0x3))

offtopic, but if this is a real output, then something is wrong with
scratching register logic for conditional, it should have emitted
states of R1 and R2, maybe you can take a look while working on this
patch set?

>       R2_w=5 R6_w=scalar(id=385) R7_w=0 R8_w=scalar() R9_w=scalar(umax=21474836475,var_off=(0x0; 0x7ffffffff))
>       R10=fp0 fp-8=mmmmmmmm fp-16=mmmmmmmm fp-24=mmmm???? fp-32= fp-40_w=4 fp-48=mmmmmmmm fp-56= fp-64=mmmmmmmm
>   ...
>   89: (07) r2 += 1                      ; R2_w=6
>   90: (79) r8 = *(u64 *)(r10 -48)       ; R8_w=scalar() R10=fp0
>   91: (79) r1 = *(u64 *)(r10 -56)       ; R1_w=scalar(umax=5,var_off=(0x0; 0x7)) R10=fp0
>   92: (ad) if r2 < r1 goto pc+41        ; R0_w=scalar() R1_w=scalar(umin=7,umax=5,var_off=(0x4; 0x3))
>       R2_w=6 R6=scalar(id=388) R7=0 R8_w=scalar() R9_w=scalar(umax=25769803770,var_off=(0x0; 0x7ffffffff))
>       R10=fp0 fp-8=mmmmmmmm fp-16=mmmmmmmm fp-24=mmmm???? fp-32= fp-40=5 fp-48=mmmmmmmm fp-56= fp-64=mmmmmmmm
>     ...
>   89: (07) r2 += 1                      ; R2_w=4088
>   90: (79) r8 = *(u64 *)(r10 -48)       ; R8_w=scalar() R10=fp0
>   91: (79) r1 = *(u64 *)(r10 -56)       ; R1_w=scalar(umax=5,var_off=(0x0; 0x7)) R10=fp0
>   92: (ad) if r2 < r1 goto pc+41        ; R0=scalar() R1=scalar(umin=4089,umax=5,var_off=(0x0; 0x7))
>       R2=4088 R6=scalar(id=12634) R7=0 R8=scalar() R9=scalar(umax=17557826301960,var_off=(0x0; 0xfffffffffff))
>       R10=fp0 fp-8=mmmmmmmm fp-16=mmmmmmmm fp-24=mmmm???? fp-32= fp-40=4087 fp-48=mmmmmmmm fp-56= fp-64=mmmmmmmm
>
> Patch 3 fixed the above issue by handling '<const> <cond_op> <non_const>' properly.
> During developing selftests for Patch 3, I found some issues with bound deduction with
> BPF_EQ/BPF_NE and fixed the issue in Patch 1.
>
> After the above issue is fixed, the second issue shows up.
>   ...
>   67: (07) r1 += -16                    ; R1_w=fp-16
>   ; bpf_probe_read_kernel(&sgp, sizeof(sgp), sgs + i);
>   68: (b4) w2 = 8                       ; R2_w=8
>   69: (85) call bpf_probe_read_kernel#113       ; R0_w=scalar() fp-16=mmmmmmmm
>   ; return sgp;
>   70: (79) r6 = *(u64 *)(r10 -16)       ; R6=scalar() R10=fp0
>   ; for (n = 0, sgp = get_sgp(sgs, i); sgp && (n < SG_MAX);
>   71: (15) if r6 == 0x0 goto pc-49      ; R6=scalar()
>   72: (b4) w1 = 0                       ; R1_w=0
>   73: (05) goto pc-46
>   ; for (i = 0; (i < VIRTIO_MAX_SGS) && (i < out_sgs); i++) {
>   28: (bc) w7 = w1                      ; R1_w=0 R7_w=0
>   ; bpf_probe_read_kernel(&len, sizeof(len), &sgp->length);
>   ...
>   23: (79) r3 = *(u64 *)(r10 -40)       ; R3_w=2 R10=fp0
>   ; for (i = 0; (i < VIRTIO_MAX_SGS) && (i < out_sgs); i++) {
>   24: (07) r3 += 1                      ; R3_w=3
>   ; for (i = 0; (i < VIRTIO_MAX_SGS) && (i < out_sgs); i++) {
>   25: (79) r1 = *(u64 *)(r10 -56)       ; R1_w=scalar(umax=5,var_off=(0x0; 0x7)) R10=fp0
>   26: (ad) if r3 < r1 goto pc+34 61: R0=scalar() R1_w=scalar(umin=4,umax=5,var_off=(0x4; 0x1)) R3_w=3 R6=scalar(id=1658)
>      R7=0 R8=scalar(id=1653) R9=scalar(umax=4294967295,var_off=(0x0; 0xffffffff)) R10=fp0 fp-8=mmmmmmmm fp-16=mmmmmmmm
>      fp-24=mmmm???? fp-32= fp-40=2 fp-56= fp-64=mmmmmmmm
>   ; if (sg_is_chain(&sg))
>   61: (7b) *(u64 *)(r10 -40) = r3       ; R3_w=3 R10=fp0 fp-40_w=3
>     ...
>   67: (07) r1 += -16                    ; R1_w=fp-16
>   ; bpf_probe_read_kernel(&sgp, sizeof(sgp), sgs + i);
>   68: (b4) w2 = 8                       ; R2_w=8
>   69: (85) call bpf_probe_read_kernel#113       ; R0_w=scalar() fp-16=mmmmmmmm
>   ; return sgp;
>   70: (79) r6 = *(u64 *)(r10 -16)
>   ; for (n = 0, sgp = get_sgp(sgs, i); sgp && (n < SG_MAX);
>   infinite loop detected at insn 71
>   verification time 90800 usec
>   stack depth 64
>   processed 25017 insns (limit 1000000) max_states_per_insn 20 total_states 491 peak_states 169 mark_read 12
>   -- END PROG LOAD LOG --
>   libbpf: prog 'trace_virtqueue_add_sgs': failed to load: -22
>
> Further analysis found the index variable 'i' is spilled but since it is not marked as precise, regsafe will ignore
> comparison since they are scalar values.
>
> Since it is hard for verifier to determine whether a particular scalar is index variable or not, Patch 5 implemented
> a heuristic such that if both old and new reg states are constant, mark the old one as precise to force scalar value
> comparison and this fixed the problem.
>
> The rest of patches are selftests related.
>
>   [1] https://reviews.llvm.org/D143726
>   [2] Commit 3c2611bac08a ("selftests/bpf: Fix trace_virtqueue_add_sgs test issue with LLVM 17.")
>
> Yonghong Song (7):
>   bpf: Improve verifier JEQ/JNE insn branch taken checking
>   selftests/bpf: Add tests for non-constant cond_op NE/EQ bound
>     deduction
>   bpf: Improve handling of pattern '<const> <cond_op> <non_const>' in
>     verifier
>   selftests/bpf: Add verifier tests for code pattern '<const> <cond_op>
>     <non_const>'
>   bpf: Mark potential spilled loop index variable as precise
>   selftests/bpf: Remove previous workaround for test verif_scale_loop6
>   selftests/bpf: Add a new test based on loop6.c
>
>  kernel/bpf/verifier.c                         |  40 +-
>  .../bpf/prog_tests/bpf_verif_scale.c          |   5 +
>  .../selftests/bpf/prog_tests/verifier.c       |   2 +
>  tools/testing/selftests/bpf/progs/loop6.c     |   2 -
>  tools/testing/selftests/bpf/progs/loop7.c     | 102 ++++
>  .../verifier_bounds_deduction_non_const.c     | 553 ++++++++++++++++++
>  .../progs/verifier_bounds_mix_sign_unsign.c   |   2 +-
>  7 files changed, 701 insertions(+), 5 deletions(-)
>  create mode 100644 tools/testing/selftests/bpf/progs/loop7.c
>  create mode 100644 tools/testing/selftests/bpf/progs/verifier_bounds_deduction_non_const.c
>
> --
> 2.34.1
>

^ permalink raw reply	[flat|nested] 26+ messages in thread

* Re: [PATCH bpf-next 3/7] bpf: Improve handling of pattern '<const> <cond_op> <non_const>' in verifier
  2023-03-30 22:54   ` Dave Marchevsky
  2023-03-31 15:26     ` Yonghong Song
@ 2023-04-04 22:04     ` Andrii Nakryiko
  2023-04-06 16:51       ` Yonghong Song
  1 sibling, 1 reply; 26+ messages in thread
From: Andrii Nakryiko @ 2023-04-04 22:04 UTC (permalink / raw)
  To: Dave Marchevsky
  Cc: Yonghong Song, bpf, Alexei Starovoitov, Andrii Nakryiko,
	Daniel Borkmann, kernel-team, Martin KaFai Lau

On Thu, Mar 30, 2023 at 3:55 PM Dave Marchevsky <davemarchevsky@meta.com> wrote:
>
> On 3/30/23 1:56 AM, Yonghong Song wrote:
> > Currently, the verifier does not handle '<const> <cond_op> <non_const>' well.
> > For example,
> >   ...
> >   10: (79) r1 = *(u64 *)(r10 -16)       ; R1_w=scalar() R10=fp0
> >   11: (b7) r2 = 0                       ; R2_w=0
> >   12: (2d) if r2 > r1 goto pc+2
> >   13: (b7) r0 = 0
> >   14: (95) exit
> >   15: (65) if r1 s> 0x1 goto pc+3
> >   16: (0f) r0 += r1
> >   ...
> > At insn 12, verifier decides both true and false branch are possible, but
> > actually only false branch is possible.
> >
> > Currently, the verifier already supports patterns '<non_const> <cond_op> <const>.
> > Add support for patterns '<const> <cond_op> <non_const>' in a similar way.
> >
> > Also fix selftest 'verifier_bounds_mix_sign_unsign/bounds checks mixing signed and unsigned, variant 10'
> > due to this change.
> >
> > Signed-off-by: Yonghong Song <yhs@fb.com>
> > ---
> >  kernel/bpf/verifier.c                                | 12 ++++++++++++
> >  .../bpf/progs/verifier_bounds_mix_sign_unsign.c      |  2 +-
> >  2 files changed, 13 insertions(+), 1 deletion(-)
> >
> > diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c
> > index 90bb6d25bc9c..d070943a8ba1 100644
> > --- a/kernel/bpf/verifier.c
> > +++ b/kernel/bpf/verifier.c
> > @@ -13302,6 +13302,18 @@ static int check_cond_jmp_op(struct bpf_verifier_env *env,
> >                                      src_reg->var_off.value,
> >                                      opcode,
> >                                      is_jmp32);
> > +     } else if (dst_reg->type == SCALAR_VALUE &&
> > +                is_jmp32 && tnum_is_const(tnum_subreg(dst_reg->var_off))) {
> > +             pred = is_branch_taken(src_reg,
> > +                                    tnum_subreg(dst_reg->var_off).value,
> > +                                    flip_opcode(opcode),
> > +                                    is_jmp32);
> > +     } else if (dst_reg->type == SCALAR_VALUE &&
> > +                !is_jmp32 && tnum_is_const(dst_reg->var_off)) {
> > +             pred = is_branch_taken(src_reg,
> > +                                    dst_reg->var_off.value,
> > +                                    flip_opcode(opcode),
> > +                                    is_jmp32);
> >       } else if (reg_is_pkt_pointer_any(dst_reg) &&
> >                  reg_is_pkt_pointer_any(src_reg) &&
> >                  !is_jmp32) {
>
> Looking at the two SCALAR_VALUE 'else if's above these added lines, these
> additions make sense. Having four separate 'else if' checks for essentially
> similar logic makes this hard to read, though, maybe it's an opportunity to
> refactor a bit.
>
> While trying to make sense of the logic here I attempted to simplify with
> a helper:
>
> @@ -13234,6 +13234,21 @@ static void find_equal_scalars(struct bpf_verifier_state *vstate,
>         }));
>  }
>
> +static int maybe_const_operand_branch(struct tnum maybe_const_op,
> +                                     struct bpf_reg_state *other_op_reg,
> +                                     u8 opcode, bool is_jmp32)
> +{
> +       struct tnum jmp_tnum = is_jmp32 ? tnum_subreg(maybe_const_op) :
> +                                         maybe_const_op;
> +       if (!tnum_is_const(jmp_tnum))
> +               return -1;
> +
> +       return is_branch_taken(other_op_reg,
> +                              jmp_tnum.value,
> +                              opcode,
> +                              is_jmp32);
> +}
> +
>  static int check_cond_jmp_op(struct bpf_verifier_env *env,
>                              struct bpf_insn *insn, int *insn_idx)
>  {
> @@ -13287,18 +13302,12 @@ static int check_cond_jmp_op(struct bpf_verifier_env *env,
>
>         if (BPF_SRC(insn->code) == BPF_K) {
>                 pred = is_branch_taken(dst_reg, insn->imm, opcode, is_jmp32);
> -       } else if (src_reg->type == SCALAR_VALUE &&
> -                  is_jmp32 && tnum_is_const(tnum_subreg(src_reg->var_off))) {
> -               pred = is_branch_taken(dst_reg,
> -                                      tnum_subreg(src_reg->var_off).value,
> -                                      opcode,
> -                                      is_jmp32);
> -       } else if (src_reg->type == SCALAR_VALUE &&
> -                  !is_jmp32 && tnum_is_const(src_reg->var_off)) {
> -               pred = is_branch_taken(dst_reg,
> -                                      src_reg->var_off.value,
> -                                      opcode,
> -                                      is_jmp32);
> +       } else if (src_reg->type == SCALAR_VALUE) {
> +               pred = maybe_const_operand_branch(src_reg->var_off, dst_reg,
> +                                                 opcode, is_jmp32);
> +       } else if (dst_reg->type == SCALAR_VALUE) {
> +               pred = maybe_const_operand_branch(dst_reg->var_off, src_reg,
> +                                                 flip_opcode(opcode), is_jmp32);
>         } else if (reg_is_pkt_pointer_any(dst_reg) &&
>                    reg_is_pkt_pointer_any(src_reg) &&
>                    !is_jmp32) {
>
>
> I think the resultant logic is the same as your patch, but it's easier to
> understand, for me at least. Note that I didn't test the above.

should we push it half a step further and have

if (src_reg->type == SCALAR_VALUE || dst_reg->type == SCALAR_VALUE)
  pred = is_branch_taken_regs(src_reg, dst_reg, opcode, is_jmp32)

seems even clearer like that. All the tnum subreg, const vs non-const,
and dst/src flip can be handled internally in one nicely isolated
place.

^ permalink raw reply	[flat|nested] 26+ messages in thread

* Re: [PATCH bpf-next 5/7] bpf: Mark potential spilled loop index variable as precise
  2023-03-30  5:56 ` [PATCH bpf-next 5/7] bpf: Mark potential spilled loop index variable as precise Yonghong Song
  2023-03-31 21:54   ` Eduard Zingerman
@ 2023-04-04 22:09   ` Andrii Nakryiko
  2023-04-06 16:55     ` Yonghong Song
  1 sibling, 1 reply; 26+ messages in thread
From: Andrii Nakryiko @ 2023-04-04 22:09 UTC (permalink / raw)
  To: Yonghong Song
  Cc: bpf, Alexei Starovoitov, Andrii Nakryiko, Daniel Borkmann,
	kernel-team, Martin KaFai Lau

On Wed, Mar 29, 2023 at 10:56 PM Yonghong Song <yhs@fb.com> wrote:
>
> For a loop, if loop index variable is spilled and between loop
> iterations, the only reg/spill state difference is spilled loop
> index variable, then verifier may assume an infinite loop which
> cause verification failure. In such cases, we should mark
> spilled loop index variable as precise to differentiate states
> between loop iterations.
>
> Since verifier is not able to accurately identify loop index
> variable, add a heuristic such that if both old reg state and
> new reg state are consts, mark old reg state as precise which
> will trigger constant value comparison later.
>
> Signed-off-by: Yonghong Song <yhs@fb.com>
> ---
>  kernel/bpf/verifier.c | 20 ++++++++++++++++++--
>  1 file changed, 18 insertions(+), 2 deletions(-)
>
> diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c
> index d070943a8ba1..d1aa2c7ae7c0 100644
> --- a/kernel/bpf/verifier.c
> +++ b/kernel/bpf/verifier.c
> @@ -14850,6 +14850,23 @@ static bool stacksafe(struct bpf_verifier_env *env, struct bpf_func_state *old,
>                 /* Both old and cur are having same slot_type */
>                 switch (old->stack[spi].slot_type[BPF_REG_SIZE - 1]) {
>                 case STACK_SPILL:
> +                       /* sometime loop index variable is spilled and the spill
> +                        * is not marked as precise. If only state difference
> +                        * between two iterations are spilled loop index, the
> +                        * "infinite loop detected at insn" error will be hit.
> +                        * Mark spilled constant as precise so it went through value
> +                        * comparison.
> +                        */
> +                       old_reg = &old->stack[spi].spilled_ptr;
> +                       cur_reg = &cur->stack[spi].spilled_ptr;
> +                       if (!old_reg->precise) {
> +                               if (old_reg->type == SCALAR_VALUE &&
> +                                   cur_reg->type == SCALAR_VALUE &&
> +                                   tnum_is_const(old_reg->var_off) &&
> +                                   tnum_is_const(cur_reg->var_off))
> +                                       old_reg->precise = true;
> +                       }
> +

I'm very worried about heuristics like this. Thinking in abstract, if
scalar's value is important for some loop invariant and would
guarantee some jump to be always taken or not taken, then jump
instruction prediction logic should mark register (and then by
precision backtrack stack slot) as precise. But if precise values
don't guarantee only one branch being taken, then marking the slot as
precise makes no sense.

Let's be very diligent with changes like this. I think your other
patches should help already with marking necessary slots as precise,
can you double check that this issue still happens. And if yes, let's
address them as a separate feature. The rest of verifier logic changes
in this patch set look good to me and make total sense.


>                         /* when explored and current stack slot are both storing
>                          * spilled registers, check that stored pointers types
>                          * are the same as well.
> @@ -14860,8 +14877,7 @@ static bool stacksafe(struct bpf_verifier_env *env, struct bpf_func_state *old,
>                          * such verifier states are not equivalent.
>                          * return false to continue verification of this path
>                          */
> -                       if (!regsafe(env, &old->stack[spi].spilled_ptr,
> -                                    &cur->stack[spi].spilled_ptr, idmap))
> +                       if (!regsafe(env, old_reg, cur_reg, idmap))
>                                 return false;
>                         break;
>                 case STACK_DYNPTR:
> --
> 2.34.1
>

^ permalink raw reply	[flat|nested] 26+ messages in thread

* Re: [PATCH bpf-next 0/7] bpf: Improve verifier for cond_op and spilled loop index variables
  2023-04-04 21:46 ` [PATCH bpf-next 0/7] bpf: Improve verifier for cond_op and spilled loop index variables Andrii Nakryiko
@ 2023-04-06 16:49   ` Yonghong Song
  2023-04-06 18:38     ` Andrii Nakryiko
  0 siblings, 1 reply; 26+ messages in thread
From: Yonghong Song @ 2023-04-06 16:49 UTC (permalink / raw)
  To: Andrii Nakryiko, Yonghong Song
  Cc: bpf, Alexei Starovoitov, Andrii Nakryiko, Daniel Borkmann,
	kernel-team, Martin KaFai Lau



On 4/4/23 2:46 PM, Andrii Nakryiko wrote:
> On Wed, Mar 29, 2023 at 10:56 PM Yonghong Song <yhs@fb.com> wrote:
>>
>> LLVM commit [1] introduced hoistMinMax optimization like
>>    (i < VIRTIO_MAX_SGS) && (i < out_sgs)
>> to
>>    upper = MIN(VIRTIO_MAX_SGS, out_sgs)
>>    ... i < upper ...
>> and caused the verification failure. Commit [2] workarounded the issue by
>> adding some bpf assembly code to prohibit the above optimization.
>> This patch improved verifier such that verification can succeed without
>> the above workaround.
>>
>> Without [2], the current verifier will hit the following failures:
>>    ...
>>    119: (15) if r1 == 0x0 goto pc+1
>>    The sequence of 8193 jumps is too complex.
>>    verification time 525829 usec
>>    stack depth 64
>>    processed 156616 insns (limit 1000000) max_states_per_insn 8 total_states 1754 peak_states 1712 mark_read 12
>>    -- END PROG LOAD LOG --
>>    libbpf: prog 'trace_virtqueue_add_sgs': failed to load: -14
>>    libbpf: failed to load object 'loop6.bpf.o'
>>    ...
>> The failure is due to verifier inadequately handling '<const> <cond_op> <non_const>' which will
>> go through both pathes and generate the following verificaiton states:
>>    ...
>>    89: (07) r2 += 1                      ; R2_w=5
>>    90: (79) r8 = *(u64 *)(r10 -48)       ; R8_w=scalar() R10=fp0
>>    91: (79) r1 = *(u64 *)(r10 -56)       ; R1_w=scalar(umax=5,var_off=(0x0; 0x7)) R10=fp0
>>    92: (ad) if r2 < r1 goto pc+41        ; R0_w=scalar() R1_w=scalar(umin=6,umax=5,var_off=(0x4; 0x3))
> 
> offtopic, but if this is a real output, then something is wrong with
> scratching register logic for conditional, it should have emitted
> states of R1 and R2, maybe you can take a look while working on this
> patch set?

Yes, this is the real output. Yes, the above R1_w should be an 
impossible state. This is what this patch tries to fix.
I am not what verifier should do if this state indeed happens,
return an -EFAULT or something?

> 
>>        R2_w=5 R6_w=scalar(id=385) R7_w=0 R8_w=scalar() R9_w=scalar(umax=21474836475,var_off=(0x0; 0x7ffffffff))
>>        R10=fp0 fp-8=mmmmmmmm fp-16=mmmmmmmm fp-24=mmmm???? fp-32= fp-40_w=4 fp-48=mmmmmmmm fp-56= fp-64=mmmmmmmm
>>    ...
>>    89: (07) r2 += 1                      ; R2_w=6
>>    90: (79) r8 = *(u64 *)(r10 -48)       ; R8_w=scalar() R10=fp0
>>    91: (79) r1 = *(u64 *)(r10 -56)       ; R1_w=scalar(umax=5,var_off=(0x0; 0x7)) R10=fp0
>>    92: (ad) if r2 < r1 goto pc+41        ; R0_w=scalar() R1_w=scalar(umin=7,umax=5,var_off=(0x4; 0x3))
>>        R2_w=6 R6=scalar(id=388) R7=0 R8_w=scalar() R9_w=scalar(umax=25769803770,var_off=(0x0; 0x7ffffffff))
>>        R10=fp0 fp-8=mmmmmmmm fp-16=mmmmmmmm fp-24=mmmm???? fp-32= fp-40=5 fp-48=mmmmmmmm fp-56= fp-64=mmmmmmmm
>>      ...
>>    89: (07) r2 += 1                      ; R2_w=4088
>>    90: (79) r8 = *(u64 *)(r10 -48)       ; R8_w=scalar() R10=fp0
>>    91: (79) r1 = *(u64 *)(r10 -56)       ; R1_w=scalar(umax=5,var_off=(0x0; 0x7)) R10=fp0
>>    92: (ad) if r2 < r1 goto pc+41        ; R0=scalar() R1=scalar(umin=4089,umax=5,var_off=(0x0; 0x7))
>>        R2=4088 R6=scalar(id=12634) R7=0 R8=scalar() R9=scalar(umax=17557826301960,var_off=(0x0; 0xfffffffffff))
>>        R10=fp0 fp-8=mmmmmmmm fp-16=mmmmmmmm fp-24=mmmm???? fp-32= fp-40=4087 fp-48=mmmmmmmm fp-56= fp-64=mmmmmmmm
>>
>> Patch 3 fixed the above issue by handling '<const> <cond_op> <non_const>' properly.
>> During developing selftests for Patch 3, I found some issues with bound deduction with
>> BPF_EQ/BPF_NE and fixed the issue in Patch 1.
[...]

^ permalink raw reply	[flat|nested] 26+ messages in thread

* Re: [PATCH bpf-next 3/7] bpf: Improve handling of pattern '<const> <cond_op> <non_const>' in verifier
  2023-04-04 22:04     ` Andrii Nakryiko
@ 2023-04-06 16:51       ` Yonghong Song
  0 siblings, 0 replies; 26+ messages in thread
From: Yonghong Song @ 2023-04-06 16:51 UTC (permalink / raw)
  To: Andrii Nakryiko, Dave Marchevsky
  Cc: Yonghong Song, bpf, Alexei Starovoitov, Andrii Nakryiko,
	Daniel Borkmann, kernel-team, Martin KaFai Lau



On 4/4/23 3:04 PM, Andrii Nakryiko wrote:
> On Thu, Mar 30, 2023 at 3:55 PM Dave Marchevsky <davemarchevsky@meta.com> wrote:
>>
>> On 3/30/23 1:56 AM, Yonghong Song wrote:
>>> Currently, the verifier does not handle '<const> <cond_op> <non_const>' well.
>>> For example,
>>>    ...
>>>    10: (79) r1 = *(u64 *)(r10 -16)       ; R1_w=scalar() R10=fp0
>>>    11: (b7) r2 = 0                       ; R2_w=0
>>>    12: (2d) if r2 > r1 goto pc+2
>>>    13: (b7) r0 = 0
>>>    14: (95) exit
>>>    15: (65) if r1 s> 0x1 goto pc+3
>>>    16: (0f) r0 += r1
>>>    ...
>>> At insn 12, verifier decides both true and false branch are possible, but
>>> actually only false branch is possible.
>>>
>>> Currently, the verifier already supports patterns '<non_const> <cond_op> <const>.
>>> Add support for patterns '<const> <cond_op> <non_const>' in a similar way.
>>>
>>> Also fix selftest 'verifier_bounds_mix_sign_unsign/bounds checks mixing signed and unsigned, variant 10'
>>> due to this change.
>>>
>>> Signed-off-by: Yonghong Song <yhs@fb.com>
>>> ---
>>>   kernel/bpf/verifier.c                                | 12 ++++++++++++
>>>   .../bpf/progs/verifier_bounds_mix_sign_unsign.c      |  2 +-
>>>   2 files changed, 13 insertions(+), 1 deletion(-)
>>>
>>> diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c
>>> index 90bb6d25bc9c..d070943a8ba1 100644
>>> --- a/kernel/bpf/verifier.c
>>> +++ b/kernel/bpf/verifier.c
>>> @@ -13302,6 +13302,18 @@ static int check_cond_jmp_op(struct bpf_verifier_env *env,
>>>                                       src_reg->var_off.value,
>>>                                       opcode,
>>>                                       is_jmp32);
>>> +     } else if (dst_reg->type == SCALAR_VALUE &&
>>> +                is_jmp32 && tnum_is_const(tnum_subreg(dst_reg->var_off))) {
>>> +             pred = is_branch_taken(src_reg,
>>> +                                    tnum_subreg(dst_reg->var_off).value,
>>> +                                    flip_opcode(opcode),
>>> +                                    is_jmp32);
>>> +     } else if (dst_reg->type == SCALAR_VALUE &&
>>> +                !is_jmp32 && tnum_is_const(dst_reg->var_off)) {
>>> +             pred = is_branch_taken(src_reg,
>>> +                                    dst_reg->var_off.value,
>>> +                                    flip_opcode(opcode),
>>> +                                    is_jmp32);
>>>        } else if (reg_is_pkt_pointer_any(dst_reg) &&
>>>                   reg_is_pkt_pointer_any(src_reg) &&
>>>                   !is_jmp32) {
>>
>> Looking at the two SCALAR_VALUE 'else if's above these added lines, these
>> additions make sense. Having four separate 'else if' checks for essentially
>> similar logic makes this hard to read, though, maybe it's an opportunity to
>> refactor a bit.
>>
>> While trying to make sense of the logic here I attempted to simplify with
>> a helper:
>>
>> @@ -13234,6 +13234,21 @@ static void find_equal_scalars(struct bpf_verifier_state *vstate,
>>          }));
>>   }
>>
>> +static int maybe_const_operand_branch(struct tnum maybe_const_op,
>> +                                     struct bpf_reg_state *other_op_reg,
>> +                                     u8 opcode, bool is_jmp32)
>> +{
>> +       struct tnum jmp_tnum = is_jmp32 ? tnum_subreg(maybe_const_op) :
>> +                                         maybe_const_op;
>> +       if (!tnum_is_const(jmp_tnum))
>> +               return -1;
>> +
>> +       return is_branch_taken(other_op_reg,
>> +                              jmp_tnum.value,
>> +                              opcode,
>> +                              is_jmp32);
>> +}
>> +
>>   static int check_cond_jmp_op(struct bpf_verifier_env *env,
>>                               struct bpf_insn *insn, int *insn_idx)
>>   {
>> @@ -13287,18 +13302,12 @@ static int check_cond_jmp_op(struct bpf_verifier_env *env,
>>
>>          if (BPF_SRC(insn->code) == BPF_K) {
>>                  pred = is_branch_taken(dst_reg, insn->imm, opcode, is_jmp32);
>> -       } else if (src_reg->type == SCALAR_VALUE &&
>> -                  is_jmp32 && tnum_is_const(tnum_subreg(src_reg->var_off))) {
>> -               pred = is_branch_taken(dst_reg,
>> -                                      tnum_subreg(src_reg->var_off).value,
>> -                                      opcode,
>> -                                      is_jmp32);
>> -       } else if (src_reg->type == SCALAR_VALUE &&
>> -                  !is_jmp32 && tnum_is_const(src_reg->var_off)) {
>> -               pred = is_branch_taken(dst_reg,
>> -                                      src_reg->var_off.value,
>> -                                      opcode,
>> -                                      is_jmp32);
>> +       } else if (src_reg->type == SCALAR_VALUE) {
>> +               pred = maybe_const_operand_branch(src_reg->var_off, dst_reg,
>> +                                                 opcode, is_jmp32);
>> +       } else if (dst_reg->type == SCALAR_VALUE) {
>> +               pred = maybe_const_operand_branch(dst_reg->var_off, src_reg,
>> +                                                 flip_opcode(opcode), is_jmp32);
>>          } else if (reg_is_pkt_pointer_any(dst_reg) &&
>>                     reg_is_pkt_pointer_any(src_reg) &&
>>                     !is_jmp32) {
>>
>>
>> I think the resultant logic is the same as your patch, but it's easier to
>> understand, for me at least. Note that I didn't test the above.
> 
> should we push it half a step further and have
> 
> if (src_reg->type == SCALAR_VALUE || dst_reg->type == SCALAR_VALUE)
>    pred = is_branch_taken_regs(src_reg, dst_reg, opcode, is_jmp32)
> 
> seems even clearer like that. All the tnum subreg, const vs non-const,
> and dst/src flip can be handled internally in one nicely isolated
> place.

I kept my original logic. I think it is more clean. In many cases,
both src_reg and dst_reg are scalar values. What we really want is to
test whether src_reg or dst_reg are constant or not and act
accordingly.


^ permalink raw reply	[flat|nested] 26+ messages in thread

* Re: [PATCH bpf-next 5/7] bpf: Mark potential spilled loop index variable as precise
  2023-04-04 22:09   ` Andrii Nakryiko
@ 2023-04-06 16:55     ` Yonghong Song
  0 siblings, 0 replies; 26+ messages in thread
From: Yonghong Song @ 2023-04-06 16:55 UTC (permalink / raw)
  To: Andrii Nakryiko, Yonghong Song
  Cc: bpf, Alexei Starovoitov, Andrii Nakryiko, Daniel Borkmann,
	kernel-team, Martin KaFai Lau



On 4/4/23 3:09 PM, Andrii Nakryiko wrote:
> On Wed, Mar 29, 2023 at 10:56 PM Yonghong Song <yhs@fb.com> wrote:
>>
>> For a loop, if loop index variable is spilled and between loop
>> iterations, the only reg/spill state difference is spilled loop
>> index variable, then verifier may assume an infinite loop which
>> cause verification failure. In such cases, we should mark
>> spilled loop index variable as precise to differentiate states
>> between loop iterations.
>>
>> Since verifier is not able to accurately identify loop index
>> variable, add a heuristic such that if both old reg state and
>> new reg state are consts, mark old reg state as precise which
>> will trigger constant value comparison later.
>>
>> Signed-off-by: Yonghong Song <yhs@fb.com>
>> ---
>>   kernel/bpf/verifier.c | 20 ++++++++++++++++++--
>>   1 file changed, 18 insertions(+), 2 deletions(-)
>>
>> diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c
>> index d070943a8ba1..d1aa2c7ae7c0 100644
>> --- a/kernel/bpf/verifier.c
>> +++ b/kernel/bpf/verifier.c
>> @@ -14850,6 +14850,23 @@ static bool stacksafe(struct bpf_verifier_env *env, struct bpf_func_state *old,
>>                  /* Both old and cur are having same slot_type */
>>                  switch (old->stack[spi].slot_type[BPF_REG_SIZE - 1]) {
>>                  case STACK_SPILL:
>> +                       /* sometime loop index variable is spilled and the spill
>> +                        * is not marked as precise. If only state difference
>> +                        * between two iterations are spilled loop index, the
>> +                        * "infinite loop detected at insn" error will be hit.
>> +                        * Mark spilled constant as precise so it went through value
>> +                        * comparison.
>> +                        */
>> +                       old_reg = &old->stack[spi].spilled_ptr;
>> +                       cur_reg = &cur->stack[spi].spilled_ptr;
>> +                       if (!old_reg->precise) {
>> +                               if (old_reg->type == SCALAR_VALUE &&
>> +                                   cur_reg->type == SCALAR_VALUE &&
>> +                                   tnum_is_const(old_reg->var_off) &&
>> +                                   tnum_is_const(cur_reg->var_off))
>> +                                       old_reg->precise = true;
>> +                       }
>> +
> 
> I'm very worried about heuristics like this. Thinking in abstract, if
> scalar's value is important for some loop invariant and would
> guarantee some jump to be always taken or not taken, then jump
> instruction prediction logic should mark register (and then by
> precision backtrack stack slot) as precise. But if precise values
> don't guarantee only one branch being taken, then marking the slot as
> precise makes no sense.
> 
> Let's be very diligent with changes like this. I think your other
> patches should help already with marking necessary slots as precise,
> can you double check that this issue still happens. And if yes, let's
> address them as a separate feature. The rest of verifier logic changes
> in this patch set look good to me and make total sense.

Yes, this is a heuristic so it will mark precise for non-induction 
variables as well. Let me do a little more study on this. Just posted v2 
without this patch and its corresponding tests.

> 
> 
>>                          /* when explored and current stack slot are both storing
>>                           * spilled registers, check that stored pointers types
>>                           * are the same as well.
>> @@ -14860,8 +14877,7 @@ static bool stacksafe(struct bpf_verifier_env *env, struct bpf_func_state *old,
>>                           * such verifier states are not equivalent.
>>                           * return false to continue verification of this path
>>                           */
>> -                       if (!regsafe(env, &old->stack[spi].spilled_ptr,
>> -                                    &cur->stack[spi].spilled_ptr, idmap))
>> +                       if (!regsafe(env, old_reg, cur_reg, idmap))
>>                                  return false;
>>                          break;
>>                  case STACK_DYNPTR:
>> --
>> 2.34.1
>>

^ permalink raw reply	[flat|nested] 26+ messages in thread

* Re: [PATCH bpf-next 0/7] bpf: Improve verifier for cond_op and spilled loop index variables
  2023-04-06 16:49   ` Yonghong Song
@ 2023-04-06 18:38     ` Andrii Nakryiko
  2023-04-06 19:54       ` Alexei Starovoitov
  0 siblings, 1 reply; 26+ messages in thread
From: Andrii Nakryiko @ 2023-04-06 18:38 UTC (permalink / raw)
  To: Yonghong Song
  Cc: Yonghong Song, bpf, Alexei Starovoitov, Andrii Nakryiko,
	Daniel Borkmann, kernel-team, Martin KaFai Lau

On Thu, Apr 6, 2023 at 9:49 AM Yonghong Song <yhs@meta.com> wrote:
>
>
>
> On 4/4/23 2:46 PM, Andrii Nakryiko wrote:
> > On Wed, Mar 29, 2023 at 10:56 PM Yonghong Song <yhs@fb.com> wrote:
> >>
> >> LLVM commit [1] introduced hoistMinMax optimization like
> >>    (i < VIRTIO_MAX_SGS) && (i < out_sgs)
> >> to
> >>    upper = MIN(VIRTIO_MAX_SGS, out_sgs)
> >>    ... i < upper ...
> >> and caused the verification failure. Commit [2] workarounded the issue by
> >> adding some bpf assembly code to prohibit the above optimization.
> >> This patch improved verifier such that verification can succeed without
> >> the above workaround.
> >>
> >> Without [2], the current verifier will hit the following failures:
> >>    ...
> >>    119: (15) if r1 == 0x0 goto pc+1
> >>    The sequence of 8193 jumps is too complex.
> >>    verification time 525829 usec
> >>    stack depth 64
> >>    processed 156616 insns (limit 1000000) max_states_per_insn 8 total_states 1754 peak_states 1712 mark_read 12
> >>    -- END PROG LOAD LOG --
> >>    libbpf: prog 'trace_virtqueue_add_sgs': failed to load: -14
> >>    libbpf: failed to load object 'loop6.bpf.o'
> >>    ...
> >> The failure is due to verifier inadequately handling '<const> <cond_op> <non_const>' which will
> >> go through both pathes and generate the following verificaiton states:
> >>    ...
> >>    89: (07) r2 += 1                      ; R2_w=5
> >>    90: (79) r8 = *(u64 *)(r10 -48)       ; R8_w=scalar() R10=fp0
> >>    91: (79) r1 = *(u64 *)(r10 -56)       ; R1_w=scalar(umax=5,var_off=(0x0; 0x7)) R10=fp0
> >>    92: (ad) if r2 < r1 goto pc+41        ; R0_w=scalar() R1_w=scalar(umin=6,umax=5,var_off=(0x4; 0x3))
> >
> > offtopic, but if this is a real output, then something is wrong with
> > scratching register logic for conditional, it should have emitted
> > states of R1 and R2, maybe you can take a look while working on this
> > patch set?
>
> Yes, this is the real output. Yes, the above R1_w should be an
> impossible state. This is what this patch tries to fix.
> I am not what verifier should do if this state indeed happens,
> return an -EFAULT or something?

no-no, that's not what I'm talking about. Look at the instruction, it
compares R1 and R2, yet we print the state of R0 and R1, as if that
instruction worked with R0 and R1 instead. That's confusing and wrong.
There is some off-by-one error in mark_register_scratched() call, or
something like that.

>
> >
> >>        R2_w=5 R6_w=scalar(id=385) R7_w=0 R8_w=scalar() R9_w=scalar(umax=21474836475,var_off=(0x0; 0x7ffffffff))
> >>        R10=fp0 fp-8=mmmmmmmm fp-16=mmmmmmmm fp-24=mmmm???? fp-32= fp-40_w=4 fp-48=mmmmmmmm fp-56= fp-64=mmmmmmmm
> >>    ...
> >>    89: (07) r2 += 1                      ; R2_w=6
> >>    90: (79) r8 = *(u64 *)(r10 -48)       ; R8_w=scalar() R10=fp0
> >>    91: (79) r1 = *(u64 *)(r10 -56)       ; R1_w=scalar(umax=5,var_off=(0x0; 0x7)) R10=fp0
> >>    92: (ad) if r2 < r1 goto pc+41        ; R0_w=scalar() R1_w=scalar(umin=7,umax=5,var_off=(0x4; 0x3))
> >>        R2_w=6 R6=scalar(id=388) R7=0 R8_w=scalar() R9_w=scalar(umax=25769803770,var_off=(0x0; 0x7ffffffff))
> >>        R10=fp0 fp-8=mmmmmmmm fp-16=mmmmmmmm fp-24=mmmm???? fp-32= fp-40=5 fp-48=mmmmmmmm fp-56= fp-64=mmmmmmmm
> >>      ...
> >>    89: (07) r2 += 1                      ; R2_w=4088
> >>    90: (79) r8 = *(u64 *)(r10 -48)       ; R8_w=scalar() R10=fp0
> >>    91: (79) r1 = *(u64 *)(r10 -56)       ; R1_w=scalar(umax=5,var_off=(0x0; 0x7)) R10=fp0
> >>    92: (ad) if r2 < r1 goto pc+41        ; R0=scalar() R1=scalar(umin=4089,umax=5,var_off=(0x0; 0x7))
> >>        R2=4088 R6=scalar(id=12634) R7=0 R8=scalar() R9=scalar(umax=17557826301960,var_off=(0x0; 0xfffffffffff))
> >>        R10=fp0 fp-8=mmmmmmmm fp-16=mmmmmmmm fp-24=mmmm???? fp-32= fp-40=4087 fp-48=mmmmmmmm fp-56= fp-64=mmmmmmmm
> >>
> >> Patch 3 fixed the above issue by handling '<const> <cond_op> <non_const>' properly.
> >> During developing selftests for Patch 3, I found some issues with bound deduction with
> >> BPF_EQ/BPF_NE and fixed the issue in Patch 1.
> [...]

^ permalink raw reply	[flat|nested] 26+ messages in thread

* Re: [PATCH bpf-next 0/7] bpf: Improve verifier for cond_op and spilled loop index variables
  2023-04-06 18:38     ` Andrii Nakryiko
@ 2023-04-06 19:54       ` Alexei Starovoitov
  0 siblings, 0 replies; 26+ messages in thread
From: Alexei Starovoitov @ 2023-04-06 19:54 UTC (permalink / raw)
  To: Andrii Nakryiko
  Cc: Yonghong Song, Yonghong Song, bpf, Alexei Starovoitov,
	Andrii Nakryiko, Daniel Borkmann, Kernel Team, Martin KaFai Lau

On Thu, Apr 6, 2023 at 11:39 AM Andrii Nakryiko
<andrii.nakryiko@gmail.com> wrote:
>
> On Thu, Apr 6, 2023 at 9:49 AM Yonghong Song <yhs@meta.com> wrote:
> >
> >
> >
> > On 4/4/23 2:46 PM, Andrii Nakryiko wrote:
> > > On Wed, Mar 29, 2023 at 10:56 PM Yonghong Song <yhs@fb.com> wrote:
> > >>
> > >> LLVM commit [1] introduced hoistMinMax optimization like
> > >>    (i < VIRTIO_MAX_SGS) && (i < out_sgs)
> > >> to
> > >>    upper = MIN(VIRTIO_MAX_SGS, out_sgs)
> > >>    ... i < upper ...
> > >> and caused the verification failure. Commit [2] workarounded the issue by
> > >> adding some bpf assembly code to prohibit the above optimization.
> > >> This patch improved verifier such that verification can succeed without
> > >> the above workaround.
> > >>
> > >> Without [2], the current verifier will hit the following failures:
> > >>    ...
> > >>    119: (15) if r1 == 0x0 goto pc+1
> > >>    The sequence of 8193 jumps is too complex.
> > >>    verification time 525829 usec
> > >>    stack depth 64
> > >>    processed 156616 insns (limit 1000000) max_states_per_insn 8 total_states 1754 peak_states 1712 mark_read 12
> > >>    -- END PROG LOAD LOG --
> > >>    libbpf: prog 'trace_virtqueue_add_sgs': failed to load: -14
> > >>    libbpf: failed to load object 'loop6.bpf.o'
> > >>    ...
> > >> The failure is due to verifier inadequately handling '<const> <cond_op> <non_const>' which will
> > >> go through both pathes and generate the following verificaiton states:
> > >>    ...
> > >>    89: (07) r2 += 1                      ; R2_w=5
> > >>    90: (79) r8 = *(u64 *)(r10 -48)       ; R8_w=scalar() R10=fp0
> > >>    91: (79) r1 = *(u64 *)(r10 -56)       ; R1_w=scalar(umax=5,var_off=(0x0; 0x7)) R10=fp0
> > >>    92: (ad) if r2 < r1 goto pc+41        ; R0_w=scalar() R1_w=scalar(umin=6,umax=5,var_off=(0x4; 0x3))
> > >
> > > offtopic, but if this is a real output, then something is wrong with
> > > scratching register logic for conditional, it should have emitted
> > > states of R1 and R2, maybe you can take a look while working on this
> > > patch set?
> >
> > Yes, this is the real output. Yes, the above R1_w should be an
> > impossible state. This is what this patch tries to fix.
> > I am not what verifier should do if this state indeed happens,
> > return an -EFAULT or something?
>
> no-no, that's not what I'm talking about. Look at the instruction, it
> compares R1 and R2, yet we print the state of R0 and R1, as if that
> instruction worked with R0 and R1 instead. That's confusing and wrong.
> There is some off-by-one error in mark_register_scratched() call, or
> something like that.

I suspect Yonghong just trimmed the output.
Line 92 has both R1 and R2 below.
Why R0, R6, R7, R8 are also there... is indeed wrong.
I've looked at scratch marking logic and don't an obvious bug.
Something to investigate.

> >
> > >
> > >>        R2_w=5 R6_w=scalar(id=385) R7_w=0 R8_w=scalar() R9_w=scalar(umax=21474836475,var_off=(0x0; 0x7ffffffff))
> > >>        R10=fp0 fp-8=mmmmmmmm fp-16=mmmmmmmm fp-24=mmmm???? fp-32= fp-40_w=4 fp-48=mmmmmmmm fp-56= fp-64=mmmmmmmm
> > >>    ...
> > >>    89: (07) r2 += 1                      ; R2_w=6
> > >>    90: (79) r8 = *(u64 *)(r10 -48)       ; R8_w=scalar() R10=fp0
> > >>    91: (79) r1 = *(u64 *)(r10 -56)       ; R1_w=scalar(umax=5,var_off=(0x0; 0x7)) R10=fp0
> > >>    92: (ad) if r2 < r1 goto pc+41        ; R0_w=scalar() R1_w=scalar(umin=7,umax=5,var_off=(0x4; 0x3))
> > >>        R2_w=6 R6=scalar(id=388) R7=0 R8_w=scalar() R9_w=scalar(umax=25769803770,var_off=(0x0; 0x7ffffffff))
> > >>        R10=fp0 fp-8=mmmmmmmm fp-16=mmmmmmmm fp-24=mmmm???? fp-32= fp-40=5 fp-48=mmmmmmmm fp-56= fp-64=mmmmmmmm
> > >>      ...
> > >>    89: (07) r2 += 1                      ; R2_w=4088
> > >>    90: (79) r8 = *(u64 *)(r10 -48)       ; R8_w=scalar() R10=fp0
> > >>    91: (79) r1 = *(u64 *)(r10 -56)       ; R1_w=scalar(umax=5,var_off=(0x0; 0x7)) R10=fp0
> > >>    92: (ad) if r2 < r1 goto pc+41        ; R0=scalar() R1=scalar(umin=4089,umax=5,var_off=(0x0; 0x7))
> > >>        R2=4088 R6=scalar(id=12634) R7=0 R8=scalar() R9=scalar(umax=17557826301960,var_off=(0x0; 0xfffffffffff))
> > >>        R10=fp0 fp-8=mmmmmmmm fp-16=mmmmmmmm fp-24=mmmm???? fp-32= fp-40=4087 fp-48=mmmmmmmm fp-56= fp-64=mmmmmmmm
> > >>
> > >> Patch 3 fixed the above issue by handling '<const> <cond_op> <non_const>' properly.
> > >> During developing selftests for Patch 3, I found some issues with bound deduction with
> > >> BPF_EQ/BPF_NE and fixed the issue in Patch 1.
> > [...]

^ permalink raw reply	[flat|nested] 26+ messages in thread

end of thread, other threads:[~2023-04-06 19:55 UTC | newest]

Thread overview: 26+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2023-03-30  5:56 [PATCH bpf-next 0/7] bpf: Improve verifier for cond_op and spilled loop index variables Yonghong Song
2023-03-30  5:56 ` [PATCH bpf-next 1/7] bpf: Improve verifier JEQ/JNE insn branch taken checking Yonghong Song
2023-03-30 21:14   ` Dave Marchevsky
2023-03-31  6:40     ` Yonghong Song
2023-03-30  5:56 ` [PATCH bpf-next 2/7] selftests/bpf: Add tests for non-constant cond_op NE/EQ bound deduction Yonghong Song
2023-03-30  5:56 ` [PATCH bpf-next 3/7] bpf: Improve handling of pattern '<const> <cond_op> <non_const>' in verifier Yonghong Song
2023-03-30 22:54   ` Dave Marchevsky
2023-03-31 15:26     ` Yonghong Song
2023-04-04 22:04     ` Andrii Nakryiko
2023-04-06 16:51       ` Yonghong Song
2023-03-30  5:56 ` [PATCH bpf-next 4/7] selftests/bpf: Add verifier tests for code pattern '<const> <cond_op> <non_const>' Yonghong Song
2023-03-30  5:56 ` [PATCH bpf-next 5/7] bpf: Mark potential spilled loop index variable as precise Yonghong Song
2023-03-31 21:54   ` Eduard Zingerman
2023-03-31 23:39     ` Yonghong Song
2023-04-03  1:48       ` Alexei Starovoitov
2023-04-03  4:04         ` Yonghong Song
2023-04-04 22:09   ` Andrii Nakryiko
2023-04-06 16:55     ` Yonghong Song
2023-03-30  5:56 ` [PATCH bpf-next 6/7] selftests/bpf: Remove previous workaround for test verif_scale_loop6 Yonghong Song
2023-03-30  5:56 ` [PATCH bpf-next 7/7] selftests/bpf: Add a new test based on loop6.c Yonghong Song
2023-04-03  1:39   ` Alexei Starovoitov
2023-04-03  3:59     ` Yonghong Song
2023-04-04 21:46 ` [PATCH bpf-next 0/7] bpf: Improve verifier for cond_op and spilled loop index variables Andrii Nakryiko
2023-04-06 16:49   ` Yonghong Song
2023-04-06 18:38     ` Andrii Nakryiko
2023-04-06 19:54       ` Alexei Starovoitov

This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).