diff mbox series

[bpf-next,5/7] bpf: Mark potential spilled loop index variable as precise

Message ID 20230330055625.92148-1-yhs@fb.com (mailing list archive)
State Superseded
Delegated to: BPF
Headers show
Series bpf: Improve verifier for cond_op and spilled loop index variables | expand

Checks

Context Check Description
netdev/series_format success Posting correctly formatted
netdev/tree_selection success Clearly marked for bpf-next, async
netdev/fixes_present success Fixes tag not required for -next series
netdev/header_inline success No static functions without inline keyword in header files
netdev/build_32bit success Errors and warnings before: 28 this patch: 28
netdev/cc_maintainers warning 7 maintainers not CCed: song@kernel.org sdf@google.com haoluo@google.com john.fastabend@gmail.com kpsingh@kernel.org jolsa@kernel.org martin.lau@linux.dev
netdev/build_clang success Errors and warnings before: 18 this patch: 18
netdev/verify_signedoff success Signed-off-by tag matches author and committer
netdev/deprecated_api success None detected
netdev/check_selftest success No net selftest shell script
netdev/verify_fixes success No Fixes tag
netdev/build_allmodconfig_warn success Errors and warnings before: 28 this patch: 28
netdev/checkpatch warning WARNING: line length of 84 exceeds 80 columns
netdev/kdoc success Errors and warnings before: 0 this patch: 0
netdev/source_inline success Was 0 now: 0
bpf/vmtest-bpf-next-VM_Test-10 fail Logs for test_maps on s390x with gcc
bpf/vmtest-bpf-next-VM_Test-15 success Logs for test_progs on s390x with gcc
bpf/vmtest-bpf-next-PR success PR summary
bpf/vmtest-bpf-next-VM_Test-1 success Logs for ShellCheck
bpf/vmtest-bpf-next-VM_Test-2 success Logs for build for aarch64 with gcc
bpf/vmtest-bpf-next-VM_Test-3 success Logs for build for aarch64 with llvm-16
bpf/vmtest-bpf-next-VM_Test-5 success Logs for build for x86_64 with gcc
bpf/vmtest-bpf-next-VM_Test-6 success Logs for build for x86_64 with llvm-16
bpf/vmtest-bpf-next-VM_Test-7 success Logs for set-matrix
bpf/vmtest-bpf-next-VM_Test-4 success Logs for build for s390x with gcc
bpf/vmtest-bpf-next-VM_Test-8 success Logs for test_maps on aarch64 with gcc
bpf/vmtest-bpf-next-VM_Test-9 success Logs for test_maps on aarch64 with llvm-16
bpf/vmtest-bpf-next-VM_Test-11 success Logs for test_maps on x86_64 with gcc
bpf/vmtest-bpf-next-VM_Test-12 success Logs for test_maps on x86_64 with llvm-16
bpf/vmtest-bpf-next-VM_Test-17 success Logs for test_progs on x86_64 with llvm-16
bpf/vmtest-bpf-next-VM_Test-18 success Logs for test_progs_no_alu32 on aarch64 with gcc
bpf/vmtest-bpf-next-VM_Test-19 success Logs for test_progs_no_alu32 on aarch64 with llvm-16
bpf/vmtest-bpf-next-VM_Test-21 success Logs for test_progs_no_alu32 on x86_64 with gcc
bpf/vmtest-bpf-next-VM_Test-22 success Logs for test_progs_no_alu32 on x86_64 with llvm-16
bpf/vmtest-bpf-next-VM_Test-23 success Logs for test_progs_no_alu32_parallel on aarch64 with gcc
bpf/vmtest-bpf-next-VM_Test-24 success Logs for test_progs_no_alu32_parallel on aarch64 with llvm-16
bpf/vmtest-bpf-next-VM_Test-25 success Logs for test_progs_no_alu32_parallel on x86_64 with gcc
bpf/vmtest-bpf-next-VM_Test-26 success Logs for test_progs_no_alu32_parallel on x86_64 with llvm-16
bpf/vmtest-bpf-next-VM_Test-27 success Logs for test_progs_parallel on aarch64 with gcc
bpf/vmtest-bpf-next-VM_Test-28 success Logs for test_progs_parallel on aarch64 with llvm-16
bpf/vmtest-bpf-next-VM_Test-29 success Logs for test_progs_parallel on x86_64 with gcc
bpf/vmtest-bpf-next-VM_Test-30 success Logs for test_progs_parallel on x86_64 with llvm-16
bpf/vmtest-bpf-next-VM_Test-31 success Logs for test_verifier on aarch64 with gcc
bpf/vmtest-bpf-next-VM_Test-32 success Logs for test_verifier on aarch64 with llvm-16
bpf/vmtest-bpf-next-VM_Test-34 success Logs for test_verifier on x86_64 with gcc
bpf/vmtest-bpf-next-VM_Test-35 success Logs for test_verifier on x86_64 with llvm-16
bpf/vmtest-bpf-next-VM_Test-13 success Logs for test_progs on aarch64 with gcc
bpf/vmtest-bpf-next-VM_Test-14 success Logs for test_progs on aarch64 with llvm-16
bpf/vmtest-bpf-next-VM_Test-16 success Logs for test_progs on x86_64 with gcc
bpf/vmtest-bpf-next-VM_Test-20 success Logs for test_progs_no_alu32 on s390x with gcc
bpf/vmtest-bpf-next-VM_Test-33 success Logs for test_verifier on s390x with gcc

Commit Message

Yonghong Song March 30, 2023, 5:56 a.m. UTC 
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(-)

Comments

Eduard Zingerman March 31, 2023, 9:54 p.m. UTC | #1 
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))
Yonghong Song March 31, 2023, 11:39 p.m. UTC | #2 
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))
Alexei Starovoitov April 3, 2023, 1:48 a.m. UTC | #3 
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.
Yonghong Song April 3, 2023, 4:04 a.m. UTC | #4 
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.
Andrii Nakryiko April 4, 2023, 10:09 p.m. UTC | #5 
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
>
Yonghong Song April 6, 2023, 4:55 p.m. UTC | #6 
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
>>
diff mbox series

Patch

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: