mirror of
https://github.com/torvalds/linux.git
synced 2026-11-07 06:17:02 +01:00
bpf: Use SCEV to widen bounded loops
Loop-bound computation and register widening
===========================================
During the main verification pass, use SCEV expressions and register
values at the entry to the loop to estimate the number of iterations
the loop might execute. Use this number to widen loop induction variables.
For example:
0: r7 = 5;
1: r6 = 0;
2: while (r6 < 3) { // latch
3: if (r6 == 1)
4: r7 = 10;
5: r6 += 1;
6: }
8: use(r7);
- Scalar evolution expressions (SCEVs) at the latch are:
- r6 = (linear r6 1)
- r7 = (any r7 10)
- For this pre-condition loop, this corresponds to the linear inequality
`r6_entry + n < 3`. With r6_entry = 0, the inequality is `n < 3`.
- Hence infer that r6's range at line 2 is [0,3], including the final
failed test. The body starts with r6 in [0,2].
- r7's (any r7 10) expression means that its initial value 5 from line 0
is joined with 10 from line 4: it is widened to [5,10] within
and after the loop.
Currently such inference is supported for:
- Reducible loops with one backedge and complete backedge/exit lists.
- A linear latch dominating the backedge, with one successor exiting
the loop. Additional exits are allowed; they can shorten execution.
- 64-bit arithmetic and comparisons whose continuation condition
normalizes to signed/unsigned < or <=, or !=.
- Initial counter, latch offset, slope and bound evaluable as constants
at loop entry, yielding a finite, representable iteration bound.
- Values with an eligible type at loop entry, e.g. SCALAR_VALUE or
PTR_TO_STACK, but not PTR_TO_CTX.
In order for widening to proceed, every register live at the loop
entry has to have a SCEV that can be widened. Currently, the following
expressions are supported:
- (linear <self> <step>): entry value + iteration# * constant step.
- (reg <self>): loop invariant; keep its entry value unchanged.
- (any ...): join the entry value with immediates or invariant registers;
types must match, and immediates require SCALAR_VALUE.
Main verification loop integration
==================================
Before proceeding with the usual instruction processing, do_check()
takes the following steps at loop entries (H):
- Checks whether the loop can be widened and obtains its
iteration bound (scev.c:bpf_compute_loop_iters()).
- If it can, saves an unwidened checkpoint E0, which will be used as
a base for deriving widened values throughout this invocation of
the loop.
- Widens registers in the current state using E0 and SCEV expressions
computed for H (scev.c:bpf_widen_scev_regs()).
- Pushes a per-frame loop-stack record to the current verifier state.
For terminating loops, the record stores E0 and the iteration bounds.
- Lets is_state_visited() create a new checkpoint W at the same
header, now containing the widened values, and proceeds with
normal checking.
- On an exit edge, pops the loop record and verifies the exit
path normally.
is_state_visited() treats a loop proven to terminate like an
iterator-based loop: RANGE_WITHIN comparison attempts to establish
convergence against a checkpoint whose exploration is still
in progress.
For example:
r0 = 0;
H: r0 += 1;
if (r0 != 3) goto H;
exit;
first H: prove H_count = 3; save E0(r0 = 0)
widen r0 to [0,2]; push the loop record
save W(r0 = [0,2])
body: r0 becomes [1,3]; fork at the conditional
exit: r0 = 3; pop the loop record and check exit
backedge: r0 = [1,2]; clamp, then match with W and prune
Clamping
--------
Independent register ranges lose correlations between induction
variables. For example:
r6 = 0; r7 = 0;
do { r6 += 1; r7 += 2; } while (r6 < 3);
use(r7);
header: r6 in [0,2], r7 in {0,2,4}
body: r6 in [1,3], r7 in {2,4,6}
backedge: r6 in [1,2], r7 still in {2,4,6}
The latch narrows r6 but does not propagate this refinement to r7.
To account for this, before comparing states on a backedge,
scev.c:bpf_clamp_scev_regs() recomputes r7's range from E0 and the
saved iteration bound, then intersects the current range {2,4,6}
with the recomputed {0,2,4}, arriving at {2,4}.
Signed-off-by: Eduard Zingerman <eddyz87@gmail.com>
Signed-off-by: Alexei Starovoitov <ast@kernel.org>
Link: https://patch.msgid.link/20261009-scev-minimal-rebase-v3-34-bcba9bc53ac9@gmail.com
This commit is contained in:
parent
1501b53681
commit
6ccf49f793
|
|
@ -328,6 +328,25 @@ struct bpf_retval_range {
|
||||||
bool return_32bit;
|
bool return_32bit;
|
||||||
};
|
};
|
||||||
|
|
||||||
|
/* SCEV/widening register space: r0..r10 plus every stack slot of a frame. */
|
||||||
|
#define BPF_SCEV_REGS_NUM (MAX_BPF_REG + MAX_BPF_STACK_SLOTS)
|
||||||
|
|
||||||
|
struct bpf_loop_iters {
|
||||||
|
u32 min_header_count; /* min number of times header is executed */
|
||||||
|
u32 max_header_count; /* max number of times header is executed */
|
||||||
|
unsigned long precise_regs[BITS_TO_LONGS(BPF_SCEV_REGS_NUM)];
|
||||||
|
};
|
||||||
|
|
||||||
|
struct loop_stack_entry {
|
||||||
|
struct bpf_verifier_state *entry_state;
|
||||||
|
u32 min_header_count;
|
||||||
|
u32 max_header_count;
|
||||||
|
u32 loop_id:31;
|
||||||
|
u32 terminates:1;
|
||||||
|
};
|
||||||
|
|
||||||
|
#define LOOP_STACK_SIZE 16
|
||||||
|
|
||||||
/* state of the program:
|
/* state of the program:
|
||||||
* type of all registers and stack info
|
* type of all registers and stack info
|
||||||
*/
|
*/
|
||||||
|
|
@ -373,6 +392,11 @@ struct bpf_func_state {
|
||||||
u32 callback_depth;
|
u32 callback_depth;
|
||||||
/* Instructions processed in this frame and callees on the current path. */
|
/* Instructions processed in this frame and callees on the current path. */
|
||||||
u32 insns_subtotal;
|
u32 insns_subtotal;
|
||||||
|
/*
|
||||||
|
* Control-flow loop nesting at the current insn within this frame's
|
||||||
|
* subprogram (loops never cross subprogram boundaries).
|
||||||
|
*/
|
||||||
|
u32 loop_stack_cnt;
|
||||||
|
|
||||||
/* The following fields should be last. See copy_func_state() */
|
/* The following fields should be last. See copy_func_state() */
|
||||||
/* The state of the stack. Each element of the array describes BPF_REG_SIZE
|
/* The state of the stack. Each element of the array describes BPF_REG_SIZE
|
||||||
|
|
@ -390,6 +414,7 @@ struct bpf_func_state {
|
||||||
|
|
||||||
u16 out_stack_arg_cnt; /* Number of outgoing on-stack argument slots */
|
u16 out_stack_arg_cnt; /* Number of outgoing on-stack argument slots */
|
||||||
struct bpf_reg_state *stack_arg_regs; /* Outgoing on-stack arguments */
|
struct bpf_reg_state *stack_arg_regs; /* Outgoing on-stack arguments */
|
||||||
|
struct loop_stack_entry *loop_stack;
|
||||||
};
|
};
|
||||||
|
|
||||||
#define MAX_CALL_FRAMES 16
|
#define MAX_CALL_FRAMES 16
|
||||||
|
|
@ -436,6 +461,7 @@ static_assert(MAX_BPF_STACK_SLOTS <= (1 << 12));
|
||||||
#define MAX_STACK_ARG_SLOTS (MAX_BPF_FUNC_ARGS - MAX_BPF_FUNC_REG_ARGS)
|
#define MAX_STACK_ARG_SLOTS (MAX_BPF_FUNC_ARGS - MAX_BPF_FUNC_REG_ARGS)
|
||||||
#define BPF_ID_MAP_SIZE ((MAX_BPF_REG + MAX_BPF_STACK_SLOTS + MAX_STACK_ARG_SLOTS) * \
|
#define BPF_ID_MAP_SIZE ((MAX_BPF_REG + MAX_BPF_STACK_SLOTS + MAX_STACK_ARG_SLOTS) * \
|
||||||
MAX_CALL_FRAMES)
|
MAX_CALL_FRAMES)
|
||||||
|
|
||||||
struct bpf_verifier_state {
|
struct bpf_verifier_state {
|
||||||
/* call stack tracking */
|
/* call stack tracking */
|
||||||
struct bpf_func_state *frame[MAX_CALL_FRAMES];
|
struct bpf_func_state *frame[MAX_CALL_FRAMES];
|
||||||
|
|
@ -1971,4 +1997,11 @@ int bpf_init_scev(struct bpf_verifier_env *env);
|
||||||
void bpf_free_scev(struct bpf_verifier_env *env);
|
void bpf_free_scev(struct bpf_verifier_env *env);
|
||||||
int bpf_compute_scev(struct bpf_verifier_env *env);
|
int bpf_compute_scev(struct bpf_verifier_env *env);
|
||||||
|
|
||||||
|
int bpf_compute_loop_iters(struct bpf_verifier_env *env, struct bpf_verifier_state *st,
|
||||||
|
struct bpf_loop_iters *iters);
|
||||||
|
int bpf_widen_scev_regs(struct bpf_verifier_env *env, struct bpf_verifier_state *st,
|
||||||
|
struct bpf_verifier_state *loop_entry, struct bpf_loop_iters *iters);
|
||||||
|
int bpf_clamp_scev_regs(struct bpf_verifier_env *env, struct bpf_func_state *st, u32 insn_idx,
|
||||||
|
struct bpf_verifier_state *entry_state, u32 max_header_count);
|
||||||
|
|
||||||
#endif /* _LINUX_BPF_VERIFIER_H */
|
#endif /* _LINUX_BPF_VERIFIER_H */
|
||||||
|
|
|
||||||
|
|
@ -792,6 +792,11 @@ void print_verifier_state(struct bpf_verifier_env *env, const struct bpf_verifie
|
||||||
verbose(env, " cb");
|
verbose(env, " cb");
|
||||||
if (state->in_async_callback_fn)
|
if (state->in_async_callback_fn)
|
||||||
verbose(env, " async_cb");
|
verbose(env, " async_cb");
|
||||||
|
if (state->loop_stack_cnt) {
|
||||||
|
verbose(env, " loop_stack=");
|
||||||
|
for (i = 0; i < state->loop_stack_cnt; i++)
|
||||||
|
verbose(env, "%s%d", i ? "," : "", state->loop_stack[i].loop_id);
|
||||||
|
}
|
||||||
verbose(env, "\n");
|
verbose(env, "\n");
|
||||||
if (!print_all)
|
if (!print_all)
|
||||||
mark_verifier_state_clean(env);
|
mark_verifier_state_clean(env);
|
||||||
|
|
|
||||||
1039
kernel/bpf/scev.c
1039
kernel/bpf/scev.c
File diff suppressed because it is too large
Load Diff
|
|
@ -936,6 +936,27 @@ static bool refsafe(struct bpf_verifier_state *old, struct bpf_verifier_state *c
|
||||||
return true;
|
return true;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
static bool loop_stack_safe(struct bpf_verifier_env *env, struct bpf_func_state *old,
|
||||||
|
struct bpf_func_state *cur)
|
||||||
|
{
|
||||||
|
struct loop_stack_entry *old_stack = old->loop_stack;
|
||||||
|
struct loop_stack_entry *cur_stack = cur->loop_stack;
|
||||||
|
u32 i;
|
||||||
|
|
||||||
|
if (old->loop_stack_cnt != cur->loop_stack_cnt)
|
||||||
|
return false;
|
||||||
|
|
||||||
|
for (i = 0; i < old->loop_stack_cnt; i++) {
|
||||||
|
if (old_stack[i].loop_id == cur_stack[i].loop_id &&
|
||||||
|
old_stack[i].max_header_count == cur_stack[i].max_header_count &&
|
||||||
|
old_stack[i].terminates == cur_stack[i].terminates)
|
||||||
|
continue;
|
||||||
|
return false;
|
||||||
|
}
|
||||||
|
|
||||||
|
return true;
|
||||||
|
}
|
||||||
|
|
||||||
/* compare two verifier states
|
/* compare two verifier states
|
||||||
*
|
*
|
||||||
* all states stored in state_list are known to be valid, since
|
* all states stored in state_list are known to be valid, since
|
||||||
|
|
@ -986,6 +1007,9 @@ static bool func_states_equal(struct bpf_verifier_env *env, struct bpf_func_stat
|
||||||
if (!stack_arg_safe(env, old, cur, &env->idmap_scratch, exact))
|
if (!stack_arg_safe(env, old, cur, &env->idmap_scratch, exact))
|
||||||
return false;
|
return false;
|
||||||
|
|
||||||
|
if (!loop_stack_safe(env, old, cur))
|
||||||
|
return false;
|
||||||
|
|
||||||
return true;
|
return true;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
@ -1032,6 +1056,7 @@ static bool states_equal(struct bpf_verifier_env *env,
|
||||||
if (!func_states_equal(env, old->frame[i], cur->frame[i], insn_idx, exact))
|
if (!func_states_equal(env, old->frame[i], cur->frame[i], insn_idx, exact))
|
||||||
return false;
|
return false;
|
||||||
}
|
}
|
||||||
|
|
||||||
return true;
|
return true;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
@ -1314,15 +1339,40 @@ int bpf_split_cur_state(struct bpf_verifier_env *env)
|
||||||
return 0;
|
return 0;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
/* Force a checkpoint upon reaching a loop header for a terminating loop. */
|
||||||
|
static bool need_loop_checkpoint(struct bpf_verifier_env *env, int insn_idx)
|
||||||
|
{
|
||||||
|
struct bpf_verifier_state *cur = env->cur_state;
|
||||||
|
struct bpf_func_state *frame = cur->frame[cur->curframe];
|
||||||
|
struct loop_stack_entry *top;
|
||||||
|
|
||||||
|
if (bpf_loop_at_index(env, insn_idx) != insn_idx || !frame->loop_stack_cnt)
|
||||||
|
return false;
|
||||||
|
top = &frame->loop_stack[frame->loop_stack_cnt - 1];
|
||||||
|
return top->loop_id == insn_idx && top->terminates;
|
||||||
|
}
|
||||||
|
|
||||||
|
static struct loop_stack_entry *current_loop(struct bpf_verifier_state *st)
|
||||||
|
{
|
||||||
|
struct bpf_func_state *frame = st->frame[st->curframe];
|
||||||
|
|
||||||
|
if (frame->loop_stack_cnt == 0)
|
||||||
|
return NULL;
|
||||||
|
return &frame->loop_stack[frame->loop_stack_cnt - 1];
|
||||||
|
}
|
||||||
|
|
||||||
int bpf_is_state_visited(struct bpf_verifier_env *env, int insn_idx)
|
int bpf_is_state_visited(struct bpf_verifier_env *env, int insn_idx)
|
||||||
{
|
{
|
||||||
|
struct loop_stack_entry *old_loop, *cur_loop;
|
||||||
struct bpf_verifier_state_list *sl;
|
struct bpf_verifier_state_list *sl;
|
||||||
struct bpf_verifier_state *cur = env->cur_state;
|
struct bpf_verifier_state *cur = env->cur_state;
|
||||||
bool force_new_state, add_new_state, loop;
|
bool force_new_state, add_new_state, loop, loop_checkpoint;
|
||||||
int n, err, states_cnt = 0;
|
int n, err, states_cnt = 0;
|
||||||
struct list_head *pos, *tmp, *head;
|
struct list_head *pos, *tmp, *head;
|
||||||
|
|
||||||
|
loop_checkpoint = need_loop_checkpoint(env, insn_idx);
|
||||||
force_new_state = env->test_state_freq || bpf_is_force_checkpoint(env, insn_idx) ||
|
force_new_state = env->test_state_freq || bpf_is_force_checkpoint(env, insn_idx) ||
|
||||||
|
loop_checkpoint ||
|
||||||
/* Avoid accumulating infinitely long jmp history */
|
/* Avoid accumulating infinitely long jmp history */
|
||||||
cur->jmp_history_cnt > 40;
|
cur->jmp_history_cnt > 40;
|
||||||
|
|
||||||
|
|
@ -1353,10 +1403,10 @@ int bpf_is_state_visited(struct bpf_verifier_env *env, int insn_idx)
|
||||||
continue;
|
continue;
|
||||||
|
|
||||||
if (sl->state.branches) {
|
if (sl->state.branches) {
|
||||||
struct bpf_func_state *frame = sl->state.frame[0];
|
struct bpf_func_state *old_top_frame = sl->state.frame[0];
|
||||||
|
|
||||||
if (frame->in_async_callback_fn &&
|
if (old_top_frame->in_async_callback_fn &&
|
||||||
frame->async_entry_cnt != cur->frame[0]->async_entry_cnt) {
|
old_top_frame->async_entry_cnt != cur->frame[0]->async_entry_cnt) {
|
||||||
/* Different async_entry_cnt means that the verifier is
|
/* Different async_entry_cnt means that the verifier is
|
||||||
* processing another entry into async callback.
|
* processing another entry into async callback.
|
||||||
* Seeing the same state is not an indication of infinite
|
* Seeing the same state is not an indication of infinite
|
||||||
|
|
@ -1455,6 +1505,33 @@ int bpf_is_state_visited(struct bpf_verifier_env *env, int insn_idx)
|
||||||
}
|
}
|
||||||
goto skip_inf_loop_check;
|
goto skip_inf_loop_check;
|
||||||
}
|
}
|
||||||
|
/*
|
||||||
|
* If old state belongs to a control flow loop that we know terminates,
|
||||||
|
* it should be safe to prune current state. However, account for the
|
||||||
|
* following situation:
|
||||||
|
*
|
||||||
|
* for (;;) {
|
||||||
|
* for (i = 0; i < 10; i++)
|
||||||
|
* ...
|
||||||
|
* }
|
||||||
|
*
|
||||||
|
* Here a backedge to a non-terminating outer loop is dominated by an exit
|
||||||
|
* from the inner loop. Pruning at a re-entry to the inner loop therefore
|
||||||
|
* would hide the fact that outer loop is non-terminating.
|
||||||
|
* Hence, only allow pruning states within the same entry state.
|
||||||
|
*/
|
||||||
|
old_loop = current_loop(&sl->state);
|
||||||
|
cur_loop = current_loop(cur);
|
||||||
|
if (old_loop && cur_loop &&
|
||||||
|
old_loop->terminates && cur_loop->terminates &&
|
||||||
|
old_loop->entry_state == cur_loop->entry_state) {
|
||||||
|
if (states_equal(env, &sl->state, cur, RANGE_WITHIN)) {
|
||||||
|
loop = true;
|
||||||
|
goto hit;
|
||||||
|
}
|
||||||
|
goto skip_inf_loop_check;
|
||||||
|
}
|
||||||
|
|
||||||
/* attempt to detect infinite loop to avoid unnecessary doomed work */
|
/* attempt to detect infinite loop to avoid unnecessary doomed work */
|
||||||
if (states_maybe_looping(&sl->state, cur) &&
|
if (states_maybe_looping(&sl->state, cur) &&
|
||||||
states_equal(env, &sl->state, cur, EXACT) &&
|
states_equal(env, &sl->state, cur, EXACT) &&
|
||||||
|
|
@ -1613,7 +1690,8 @@ int bpf_is_state_visited(struct bpf_verifier_env *env, int insn_idx)
|
||||||
* Use bigger 'n' for checkpoints because evicting checkpoint states
|
* Use bigger 'n' for checkpoints because evicting checkpoint states
|
||||||
* too early would hinder iterator convergence.
|
* too early would hinder iterator convergence.
|
||||||
*/
|
*/
|
||||||
n = bpf_is_force_checkpoint(env, insn_idx) && sl->state.branches > 0 ? 64 : 3;
|
n = (bpf_is_force_checkpoint(env, insn_idx) || loop_checkpoint) &&
|
||||||
|
sl->state.branches > 0 ? 64 : 3;
|
||||||
if (sl->miss_cnt > sl->hit_cnt * n + n) {
|
if (sl->miss_cnt > sl->hit_cnt * n + n) {
|
||||||
/* the state is unlikely to be useful. Remove it to
|
/* the state is unlikely to be useful. Remove it to
|
||||||
* speed up verification
|
* speed up verification
|
||||||
|
|
|
||||||
|
|
@ -1681,6 +1681,7 @@ static void free_func_state(struct bpf_func_state *state)
|
||||||
{
|
{
|
||||||
if (!state)
|
if (!state)
|
||||||
return;
|
return;
|
||||||
|
kfree(state->loop_stack);
|
||||||
kfree(state->stack_arg_regs);
|
kfree(state->stack_arg_regs);
|
||||||
kfree(state->stack);
|
kfree(state->stack);
|
||||||
kfree(state);
|
kfree(state);
|
||||||
|
|
@ -1717,6 +1718,10 @@ static int copy_func_state(struct bpf_func_state *dst,
|
||||||
memcpy(dst, src, offsetof(struct bpf_func_state, stack));
|
memcpy(dst, src, offsetof(struct bpf_func_state, stack));
|
||||||
/* Instruction accounting is path-local, not part of verifier state. */
|
/* Instruction accounting is path-local, not part of verifier state. */
|
||||||
dst->insns_subtotal = 0;
|
dst->insns_subtotal = 0;
|
||||||
|
dst->loop_stack = copy_array(dst->loop_stack, src->loop_stack, src->loop_stack_cnt,
|
||||||
|
sizeof(*src->loop_stack), GFP_KERNEL_ACCOUNT);
|
||||||
|
if (!dst->loop_stack)
|
||||||
|
return -ENOMEM;
|
||||||
return copy_stack_state(dst, src);
|
return copy_stack_state(dst, src);
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
@ -19916,6 +19921,178 @@ static int do_check_insn(struct bpf_verifier_env *env, bool *do_print_state)
|
||||||
return -EFAULT;
|
return -EFAULT;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
/*
|
||||||
|
* Push the loop entered at insn_idx onto the stack. Usually this adds a single
|
||||||
|
* entry on top of its enclosing loop. However, an edge may enter an inner loop
|
||||||
|
* directly, bypassing the header(s) of its enclosing loop(s), e.g.:
|
||||||
|
*
|
||||||
|
* 1: for (...): // enclosing loop, header at 1
|
||||||
|
* 2: for (...): // inner loop, header at 2
|
||||||
|
* ...
|
||||||
|
* 3: if ...:
|
||||||
|
* goto 2b; // enters loop 2 without going through header 1
|
||||||
|
*
|
||||||
|
* Such a bypass makes the enclosing loop irreducible, so its header is missing
|
||||||
|
* from the stack and both headers (1) and (2) need to be pushed onto stack.
|
||||||
|
* Only the innermost loop (the one actually entered at insn_idx) carries SCEV bounds;
|
||||||
|
* the bypassed ancestors are irreducible and pushed as non-terminating.
|
||||||
|
*
|
||||||
|
* Assumes loop_stack_pop() has already truncated the stack to the common ancestor
|
||||||
|
* of the bpf_loop_at_index(env->insn_idx) and whatever was at the top of the loop stack.
|
||||||
|
*/
|
||||||
|
static int loop_stack_push(struct bpf_verifier_env *env, bool *pushed)
|
||||||
|
{
|
||||||
|
struct bpf_insn_aux_data *aux = env->insn_aux_data;
|
||||||
|
struct bpf_func_state *frame = cur_func(env);
|
||||||
|
struct loop_stack_entry *loop_stack = frame->loop_stack;
|
||||||
|
u32 missing_headers[LOOP_STACK_SIZE];
|
||||||
|
u32 cnt = frame->loop_stack_cnt;
|
||||||
|
u32 num_missing = 0;
|
||||||
|
int h;
|
||||||
|
|
||||||
|
*pushed = false;
|
||||||
|
|
||||||
|
for (h = bpf_loop_at_index(env, env->insn_idx); h >= 0; h = aux[h].loop_header, num_missing++) {
|
||||||
|
if (cnt && loop_stack[cnt - 1].loop_id == h)
|
||||||
|
break;
|
||||||
|
if (num_missing == LOOP_STACK_SIZE)
|
||||||
|
goto e2big;
|
||||||
|
missing_headers[num_missing] = h;
|
||||||
|
}
|
||||||
|
|
||||||
|
if (num_missing == 0)
|
||||||
|
return 0;
|
||||||
|
if (cnt + num_missing > LOOP_STACK_SIZE)
|
||||||
|
goto e2big;
|
||||||
|
frame->loop_stack = realloc_array(frame->loop_stack, cnt, cnt + num_missing,
|
||||||
|
sizeof(*frame->loop_stack));
|
||||||
|
if (!frame->loop_stack)
|
||||||
|
return -ENOMEM;
|
||||||
|
loop_stack = frame->loop_stack;
|
||||||
|
|
||||||
|
for (; num_missing; num_missing--, cnt++) {
|
||||||
|
h = missing_headers[num_missing - 1];
|
||||||
|
loop_stack[cnt] = (struct loop_stack_entry){ .loop_id = h };
|
||||||
|
if (env->log.level & BPF_LOG_LEVEL2)
|
||||||
|
verbose(env, "entering loop %d\n", h);
|
||||||
|
*pushed = true;
|
||||||
|
}
|
||||||
|
frame->loop_stack_cnt = cnt;
|
||||||
|
return 0;
|
||||||
|
|
||||||
|
e2big:
|
||||||
|
verbose(env, "Too many nested loops (%d/%d) at %d\n", cnt, num_missing, env->insn_idx);
|
||||||
|
return -E2BIG;
|
||||||
|
}
|
||||||
|
|
||||||
|
/*
|
||||||
|
* An exit from a loop can cross several nested loops, e.g.:
|
||||||
|
*
|
||||||
|
* 1: for (...):
|
||||||
|
* 2: for (...):
|
||||||
|
* 3: for (...):
|
||||||
|
* if ...: // before goto the loop stack is [1, 2, 3 <top>]
|
||||||
|
* goto 1b; // after goto it should become [1]
|
||||||
|
*/
|
||||||
|
static int loop_stack_pop(struct bpf_verifier_env *env)
|
||||||
|
{
|
||||||
|
struct bpf_insn_aux_data *aux = env->insn_aux_data;
|
||||||
|
struct bpf_func_state *frame = cur_func(env);
|
||||||
|
int new_cnt = 0;
|
||||||
|
int h, i;
|
||||||
|
|
||||||
|
/*
|
||||||
|
* Walk the loop nest of insn_idx outwards (innermost first) and stop at
|
||||||
|
* the first loop that is present on the stack - that loop is the common
|
||||||
|
* ancestor and becomes the new top. If no enclosing loop is on the
|
||||||
|
* stack, drop all loops.
|
||||||
|
*/
|
||||||
|
for (h = bpf_loop_at_index(env, env->insn_idx); h >= 0; h = aux[h].loop_header) {
|
||||||
|
for (i = frame->loop_stack_cnt - 1; i >= 0; i--) {
|
||||||
|
if (frame->loop_stack[i].loop_id == h) {
|
||||||
|
new_cnt = i + 1;
|
||||||
|
goto pop;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
pop:
|
||||||
|
if (env->log.level & BPF_LOG_LEVEL2)
|
||||||
|
for (i = frame->loop_stack_cnt - 1; i >= new_cnt; i--)
|
||||||
|
verbose(env, "exiting loop %d\n", frame->loop_stack[i].loop_id);
|
||||||
|
frame->loop_stack_cnt = new_cnt;
|
||||||
|
return 0;
|
||||||
|
}
|
||||||
|
|
||||||
|
static int maybe_clamp_scev_regs(struct bpf_verifier_env *env)
|
||||||
|
{
|
||||||
|
struct bpf_func_state *frame = cur_func(env);
|
||||||
|
struct loop_stack_entry *entry;
|
||||||
|
|
||||||
|
if (frame->loop_stack_cnt == 0) {
|
||||||
|
verifier_bug(env, "%s: loop stack empty at %d", __FUNCTION__, env->insn_idx);
|
||||||
|
return -EFAULT;
|
||||||
|
}
|
||||||
|
|
||||||
|
entry = &frame->loop_stack[frame->loop_stack_cnt - 1];
|
||||||
|
if (!entry->terminates)
|
||||||
|
return 0;
|
||||||
|
|
||||||
|
return bpf_clamp_scev_regs(env, frame, env->insn_idx, entry->entry_state,
|
||||||
|
entry->max_header_count);
|
||||||
|
}
|
||||||
|
|
||||||
|
static int handle_loop_entry_exit(struct bpf_verifier_env *env)
|
||||||
|
{
|
||||||
|
struct bpf_verifier_state *cur = env->cur_state;
|
||||||
|
struct bpf_func_state *frame = cur_func(env);
|
||||||
|
struct loop_stack_entry *entry;
|
||||||
|
struct bpf_loop_iters iters;
|
||||||
|
bool pushed, terminates;
|
||||||
|
int err;
|
||||||
|
|
||||||
|
err = loop_stack_pop(env);
|
||||||
|
if (err)
|
||||||
|
return err;
|
||||||
|
|
||||||
|
err = loop_stack_push(env, &pushed);
|
||||||
|
if (err)
|
||||||
|
return err;
|
||||||
|
|
||||||
|
if (frame->loop_stack_cnt == 0)
|
||||||
|
return 0;
|
||||||
|
|
||||||
|
entry = &frame->loop_stack[frame->loop_stack_cnt - 1];
|
||||||
|
if (env->insn_idx != entry->loop_id)
|
||||||
|
return 0;
|
||||||
|
|
||||||
|
/* If nothing was pushed and env->insn_idx is a loop header, we've taken a backedge. */
|
||||||
|
if (!pushed)
|
||||||
|
return maybe_clamp_scev_regs(env);
|
||||||
|
|
||||||
|
err = bpf_compute_loop_iters(env, env->cur_state, &iters);
|
||||||
|
if (err < 0)
|
||||||
|
return err;
|
||||||
|
|
||||||
|
terminates = err == 1;
|
||||||
|
if (!terminates)
|
||||||
|
return 0;
|
||||||
|
|
||||||
|
/* Create a loop_entry checkpoint before widening */
|
||||||
|
err = bpf_split_cur_state(env);
|
||||||
|
if (err)
|
||||||
|
return err;
|
||||||
|
|
||||||
|
entry->min_header_count = iters.min_header_count;
|
||||||
|
entry->max_header_count = iters.max_header_count;
|
||||||
|
entry->entry_state = cur->parent;
|
||||||
|
entry->terminates = true;
|
||||||
|
err = bpf_widen_scev_regs(env, cur, cur->parent, &iters);
|
||||||
|
if (err < 0)
|
||||||
|
return err;
|
||||||
|
return 0;
|
||||||
|
}
|
||||||
|
|
||||||
static int do_check(struct bpf_verifier_env *env)
|
static int do_check(struct bpf_verifier_env *env)
|
||||||
{
|
{
|
||||||
bool pop_log = !(env->log.level & BPF_LOG_LEVEL2);
|
bool pop_log = !(env->log.level & BPF_LOG_LEVEL2);
|
||||||
|
|
@ -19930,6 +20107,12 @@ static int do_check(struct bpf_verifier_env *env)
|
||||||
struct bpf_insn_aux_data *insn_aux;
|
struct bpf_insn_aux_data *insn_aux;
|
||||||
int err;
|
int err;
|
||||||
|
|
||||||
|
if (signal_pending(current))
|
||||||
|
return -EAGAIN;
|
||||||
|
|
||||||
|
if (need_resched())
|
||||||
|
cond_resched();
|
||||||
|
|
||||||
/* reset current history entry on each new instruction */
|
/* reset current history entry on each new instruction */
|
||||||
env->cur_hist_ent = NULL;
|
env->cur_hist_ent = NULL;
|
||||||
|
|
||||||
|
|
@ -19976,6 +20159,15 @@ static int do_check(struct bpf_verifier_env *env)
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
/*
|
||||||
|
* Possibly widen the registers before creating a checkpoint
|
||||||
|
* in bpf_is_state_visited(). The next loop iteration will
|
||||||
|
* have a chance to hit this checkpoint and converge.
|
||||||
|
*/
|
||||||
|
err = handle_loop_entry_exit(env);
|
||||||
|
if (err)
|
||||||
|
return err;
|
||||||
|
|
||||||
if (bpf_is_prune_point(env, env->insn_idx)) {
|
if (bpf_is_prune_point(env, env->insn_idx)) {
|
||||||
err = bpf_is_state_visited(env, env->insn_idx);
|
err = bpf_is_state_visited(env, env->insn_idx);
|
||||||
if (err < 0)
|
if (err < 0)
|
||||||
|
|
@ -20001,12 +20193,6 @@ static int do_check(struct bpf_verifier_env *env)
|
||||||
return err;
|
return err;
|
||||||
}
|
}
|
||||||
|
|
||||||
if (signal_pending(current))
|
|
||||||
return -EAGAIN;
|
|
||||||
|
|
||||||
if (need_resched())
|
|
||||||
cond_resched();
|
|
||||||
|
|
||||||
if (env->log.level & BPF_LOG_LEVEL2 && do_print_state) {
|
if (env->log.level & BPF_LOG_LEVEL2 && do_print_state) {
|
||||||
verbose(env, "\nfrom %d to %d%s:",
|
verbose(env, "\nfrom %d to %d%s:",
|
||||||
env->prev_insn_idx, env->insn_idx,
|
env->prev_insn_idx, env->insn_idx,
|
||||||
|
|
@ -20016,6 +20202,13 @@ static int do_check(struct bpf_verifier_env *env)
|
||||||
do_print_state = false;
|
do_print_state = false;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
if (bpf_loop_at_index(env, env->insn_idx) >= 0 &&
|
||||||
|
cur_func(env)->loop_stack_cnt == 0) {
|
||||||
|
verifier_bug(env, "loop stack empty at %d, while inside the loop %d\n",
|
||||||
|
env->insn_idx, bpf_loop_at_index(env, env->insn_idx));
|
||||||
|
return -EFAULT;
|
||||||
|
}
|
||||||
|
|
||||||
if (env->log.level & BPF_LOG_LEVEL) {
|
if (env->log.level & BPF_LOG_LEVEL) {
|
||||||
if (verifier_state_scratched(env))
|
if (verifier_state_scratched(env))
|
||||||
print_insn_state(env, state, state->curframe);
|
print_insn_state(env, state, state->curframe);
|
||||||
|
|
|
||||||
|
|
@ -511,7 +511,7 @@ __naked void too_many_gotox_edges(void)
|
||||||
|
|
||||||
SEC("socket")
|
SEC("socket")
|
||||||
__description("gotox-edges-at-limit")
|
__description("gotox-edges-at-limit")
|
||||||
__success __retval(0)
|
__failure __msg("Too many nested loops")
|
||||||
__naked void gotox_edges_at_limit(void)
|
__naked void gotox_edges_at_limit(void)
|
||||||
{
|
{
|
||||||
asm volatile (
|
asm volatile (
|
||||||
|
|
@ -519,6 +519,10 @@ __naked void gotox_edges_at_limit(void)
|
||||||
* 1000 gotox * 1000 targets = 1,000,000 CFG edges. At run
|
* 1000 gotox * 1000 targets = 1,000,000 CFG edges. At run
|
||||||
* time, each block loads the next table entry and jumps to
|
* time, each block loads the next table entry and jumps to
|
||||||
* the following block, so the program terminates.
|
* the following block, so the program terminates.
|
||||||
|
*
|
||||||
|
* Every block can jump to every later block, so the CFG is
|
||||||
|
* a nest of ~1000 irreducible loops, deeper than the
|
||||||
|
* verifier's loop stack; the program is rejected.
|
||||||
*/
|
*/
|
||||||
GOTOX_TABLE_BEGIN(1000)
|
GOTOX_TABLE_BEGIN(1000)
|
||||||
".rept 1000;"
|
".rept 1000;"
|
||||||
|
|
|
||||||
Loading…
Reference in New Issue
Block a user