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@xxxxxx>
> ---
> 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@xxxxxxxxxx: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))
