bpf: Compute scalar evolution expressions for loops

Assign algebraic expressions to loop variables (registers and stack
spills), describing how their values evolve across iterations. These
summaries provide symbolic input for the subsequent widening patch.

The algorithm draws on ideas from the following papers:

- "Symbolic Evaluation of Chains of Recurrences for Loop Optimization"
  Robert A. van Engelen, 2000
- "The CR# Algebra and its Application in Loop Analysis and Optimization"
  Robert A. van Engelen, 2004

The analysis proceeds in two phases:

- Compute expressions for one symbolic iteration: start each variable
  with a reference to its input value, apply instruction effects and
  join expressions where control-flow paths merge.
- Convert the resulting backedge updates to recurrences at the header,
  then substitute these recurrences into expressions at the latch.

Analyze loops innermost first. Within each loop, visit blocks in
topological order (reverse postorder, with backedges ignored and nested
loops collapsed). Treat each nested loop as an opaque operation:
preserve its invariant values, forget the others and continue at its
exits, without expanding its iterations.

For example, using 64-bit arithmetic:

    0: r7 = 5;
    1: r6 = 0;
    2: do {                // header
    3:     if (r6 == 1)
    4:         r7 = 10;
    5:     r6 += 1;
    6: } while (r6 < 3);   // latch

Expressions use symbolic inputs r6 and r7; the concrete values from
lines 0-1 are supplied later by the main verifier.

First phase:
------------

At each instruction, an environment maps register numbers to their
current expressions. Transfer functions update this mapping, while
joins merge the environments arriving along different paths.

For illustration, follow each branch separately to the backedge:

- At 3, take the path skipping 4: r6 = r6, r7 = r7.
- At 5, transfer(r6 += 1): r6 = r6 -> r6 = (+ r6 1).
- At 2, the first path contributes r6 = (+ r6 1), r7 = r7.
- At 4, on the other path from 3, transfer(r7 = 10):
  r7 = r7 -> r7 = 10.
- At 5, transfer(r6 += 1): r6 = r6 -> r6 = (+ r6 1).
- At 2, join the two paths' contributions:
  join((+ r6 1), (+ r6 1)) = (+ r6 1) for r6;
  join(r7, 10) = (any r7 10) for r7.

Equal expressions stay unchanged; different expressions become ANY
alternatives. These summarize one iteration, without unrolling the loop.

Second phase:
-------------

The update r6 = (+ r6 1) says that each iteration adds 1 to r6.
Repeating this update n times gives r6_entry + n, a linear recurrence.

- At header 2, r6 = (+ r6 1) becomes (linear r6 1), meaning
  r6_entry + n, where n counts iterations from zero.
- At latch 6, substitute this recurrence into (+ r6 1):
  (+ (linear r6 1) 1) simplifies to (linear (+ r6 1) 1),
  meaning r6_entry + 1 + n.
- At both points, r7 retains (any r7 10): either its entry value
  or 10. ANY records alternatives, not numeric ranges or the path
  conditions selecting them. Unchanged variables retain their inputs.

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-33-bcba9bc53ac9@gmail.com

1 files changed, 7 insertions, 0 deletions

diff --git a/include/linux/bpf_verifier.h b/include/linux/bpf_verifier.h
index 963106328791..52f72e92eb0c 100644
--- a/include/linux/bpf_verifier.h
+++ b/include/linux/bpf_verifier.h
@@ -745,6 +745,7 @@ struct bpf_insn_aux_data {
 	bool call_with_percpu_alloc_ptr; /* {this,per}_cpu_ptr() with prog percpu alloc */
 	bool arena_scalar; /* ldx/stx/st/atomic through a number, it's an address in arena */
 	bool bb_end; /* last instruction of a basic block */
+	bool need_scev;
 	u8 alu_state; /* used in combination with alu_limit */
 	/* true if STX or LDX instruction is a part of a spill/fill
 	 * pattern for a bpf_fastcall call.
@@ -1000,6 +1001,7 @@ struct bpf_scc_info {
 };
 
 struct bpf_liveness;
+struct scev;
 
 struct bpf_fd_array {
 	union {
@@ -1164,6 +1166,7 @@ struct bpf_verifier_env {
 	struct bpf_iarray *succ;
 	struct bpf_iarray *gotox_tmp_buf;
 	int *idoms;
+	struct scev *scev;
 };
 
 static inline struct bpf_func_info_aux *subprog_aux(struct bpf_verifier_env *env, int subprog)
@@ -1964,4 +1967,8 @@ int bpf_compute_loops(struct bpf_verifier_env *env);
 int bpf_loop_at_index(struct bpf_verifier_env *env, u32 idx);
 bool bpf_is_nested_loop(struct bpf_verifier_env *env, int inner_header, int outer_header);
 
+int bpf_init_scev(struct bpf_verifier_env *env);
+void bpf_free_scev(struct bpf_verifier_env *env);
+int bpf_compute_scev(struct bpf_verifier_env *env);
+
 #endif /* _LINUX_BPF_VERIFIER_H */