Skip to content

Commit 2a09928

Browse files
eddyz87Alexei Starovoitov
eddyz87
authored and
Alexei Starovoitov
committed
bpf: correct loop detection for iterators convergence
It turns out that .branches > 0 in is_state_visited() is not a sufficient condition to identify if two verifier states form a loop when iterators convergence is computed. This commit adds logic to distinguish situations like below: (I) initial (II) initial | | V V .---------> hdr .. | | | | V V | .------... .------.. | | | | | | V V V V | ... ... .-> hdr .. | | | | | | | V V | V V | succ <- cur | succ <- cur | | | | | V | V | ... | ... | | | | '----' '----' For both (I) and (II) successor 'succ' of the current state 'cur' was previously explored and has branches count at 0. However, loop entry 'hdr' corresponding to 'succ' might be a part of current DFS path. If that is the case 'succ' and 'cur' are members of the same loop and have to be compared exactly. Co-developed-by: Andrii Nakryiko <[email protected]> Co-developed-by: Alexei Starovoitov <[email protected]> Reviewed-by: Andrii Nakryiko <[email protected]> Signed-off-by: Eduard Zingerman <[email protected]> Link: https://lore.kernel.org/r/[email protected] Signed-off-by: Alexei Starovoitov <[email protected]>
1 parent 389ede0 commit 2a09928

File tree

2 files changed

+218
-4
lines changed

2 files changed

+218
-4
lines changed

‎include/linux/bpf_verifier.h‎

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -373,10 +373,25 @@ struct bpf_verifier_state {
373373
struct bpf_active_lock active_lock;
374374
bool speculative;
375375
bool active_rcu_lock;
376+
/* If this state was ever pointed-to by other state's loop_entry field
377+
* this flag would be set to true. Used to avoid freeing such states
378+
* while they are still in use.
379+
*/
380+
bool used_as_loop_entry;
376381

377382
/* first and last insn idx of this verifier state */
378383
u32 first_insn_idx;
379384
u32 last_insn_idx;
385+
/* If this state is a part of states loop this field points to some
386+
* parent of this state such that:
387+
* - it is also a member of the same states loop;
388+
* - DFS states traversal starting from initial state visits loop_entry
389+
* state before this state.
390+
* Used to compute topmost loop entry for state loops.
391+
* State loops might appear because of open coded iterators logic.
392+
* See get_loop_entry() for more information.
393+
*/
394+
struct bpf_verifier_state *loop_entry;
380395
/* jmp history recorded from first to last.
381396
* backtracking is using it to go from last to first.
382397
* For most states jmp_history_cnt is [0-3].

‎kernel/bpf/verifier.c‎

Lines changed: 203 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1803,6 +1803,7 @@ static int copy_verifier_state(struct bpf_verifier_state *dst_state,
18031803
dst_state->first_insn_idx = src->first_insn_idx;
18041804
dst_state->last_insn_idx = src->last_insn_idx;
18051805
dst_state->dfs_depth = src->dfs_depth;
1806+
dst_state->used_as_loop_entry = src->used_as_loop_entry;
18061807
for (i = 0; i <= src->curframe; i++) {
18071808
dst = dst_state->frame[i];
18081809
if (!dst) {
@@ -1845,11 +1846,176 @@ static bool same_callsites(struct bpf_verifier_state *a, struct bpf_verifier_sta
18451846
return true;
18461847
}
18471848

1849+
/* Open coded iterators allow back-edges in the state graph in order to
1850+
* check unbounded loops that iterators.
1851+
*
1852+
* In is_state_visited() it is necessary to know if explored states are
1853+
* part of some loops in order to decide whether non-exact states
1854+
* comparison could be used:
1855+
* - non-exact states comparison establishes sub-state relation and uses
1856+
* read and precision marks to do so, these marks are propagated from
1857+
* children states and thus are not guaranteed to be final in a loop;
1858+
* - exact states comparison just checks if current and explored states
1859+
* are identical (and thus form a back-edge).
1860+
*
1861+
* Paper "A New Algorithm for Identifying Loops in Decompilation"
1862+
* by Tao Wei, Jian Mao, Wei Zou and Yu Chen [1] presents a convenient
1863+
* algorithm for loop structure detection and gives an overview of
1864+
* relevant terminology. It also has helpful illustrations.
1865+
*
1866+
* [1] https://api.semanticscholar.org/CorpusID:15784067
1867+
*
1868+
* We use a similar algorithm but because loop nested structure is
1869+
* irrelevant for verifier ours is significantly simpler and resembles
1870+
* strongly connected components algorithm from Sedgewick's textbook.
1871+
*
1872+
* Define topmost loop entry as a first node of the loop traversed in a
1873+
* depth first search starting from initial state. The goal of the loop
1874+
* tracking algorithm is to associate topmost loop entries with states
1875+
* derived from these entries.
1876+
*
1877+
* For each step in the DFS states traversal algorithm needs to identify
1878+
* the following situations:
1879+
*
1880+
* initial initial initial
1881+
* | | |
1882+
* V V V
1883+
* ... ... .---------> hdr
1884+
* | | | |
1885+
* V V | V
1886+
* cur .-> succ | .------...
1887+
* | | | | | |
1888+
* V | V | V V
1889+
* succ '-- cur | ... ...
1890+
* | | |
1891+
* | V V
1892+
* | succ <- cur
1893+
* | |
1894+
* | V
1895+
* | ...
1896+
* | |
1897+
* '----'
1898+
*
1899+
* (A) successor state of cur (B) successor state of cur or it's entry
1900+
* not yet traversed are in current DFS path, thus cur and succ
1901+
* are members of the same outermost loop
1902+
*
1903+
* initial initial
1904+
* | |
1905+
* V V
1906+
* ... ...
1907+
* | |
1908+
* V V
1909+
* .------... .------...
1910+
* | | | |
1911+
* V V V V
1912+
* .-> hdr ... ... ...
1913+
* | | | | |
1914+
* | V V V V
1915+
* | succ <- cur succ <- cur
1916+
* | | |
1917+
* | V V
1918+
* | ... ...
1919+
* | | |
1920+
* '----' exit
1921+
*
1922+
* (C) successor state of cur is a part of some loop but this loop
1923+
* does not include cur or successor state is not in a loop at all.
1924+
*
1925+
* Algorithm could be described as the following python code:
1926+
*
1927+
* traversed = set() # Set of traversed nodes
1928+
* entries = {} # Mapping from node to loop entry
1929+
* depths = {} # Depth level assigned to graph node
1930+
* path = set() # Current DFS path
1931+
*
1932+
* # Find outermost loop entry known for n
1933+
* def get_loop_entry(n):
1934+
* h = entries.get(n, None)
1935+
* while h in entries and entries[h] != h:
1936+
* h = entries[h]
1937+
* return h
1938+
*
1939+
* # Update n's loop entry if h's outermost entry comes
1940+
* # before n's outermost entry in current DFS path.
1941+
* def update_loop_entry(n, h):
1942+
* n1 = get_loop_entry(n) or n
1943+
* h1 = get_loop_entry(h) or h
1944+
* if h1 in path and depths[h1] <= depths[n1]:
1945+
* entries[n] = h1
1946+
*
1947+
* def dfs(n, depth):
1948+
* traversed.add(n)
1949+
* path.add(n)
1950+
* depths[n] = depth
1951+
* for succ in G.successors(n):
1952+
* if succ not in traversed:
1953+
* # Case A: explore succ and update cur's loop entry
1954+
* # only if succ's entry is in current DFS path.
1955+
* dfs(succ, depth + 1)
1956+
* h = get_loop_entry(succ)
1957+
* update_loop_entry(n, h)
1958+
* else:
1959+
* # Case B or C depending on `h1 in path` check in update_loop_entry().
1960+
* update_loop_entry(n, succ)
1961+
* path.remove(n)
1962+
*
1963+
* To adapt this algorithm for use with verifier:
1964+
* - use st->branch == 0 as a signal that DFS of succ had been finished
1965+
* and cur's loop entry has to be updated (case A), handle this in
1966+
* update_branch_counts();
1967+
* - use st->branch > 0 as a signal that st is in the current DFS path;
1968+
* - handle cases B and C in is_state_visited();
1969+
* - update topmost loop entry for intermediate states in get_loop_entry().
1970+
*/
1971+
static struct bpf_verifier_state *get_loop_entry(struct bpf_verifier_state *st)
1972+
{
1973+
struct bpf_verifier_state *topmost = st->loop_entry, *old;
1974+
1975+
while (topmost && topmost->loop_entry && topmost != topmost->loop_entry)
1976+
topmost = topmost->loop_entry;
1977+
/* Update loop entries for intermediate states to avoid this
1978+
* traversal in future get_loop_entry() calls.
1979+
*/
1980+
while (st && st->loop_entry != topmost) {
1981+
old = st->loop_entry;
1982+
st->loop_entry = topmost;
1983+
st = old;
1984+
}
1985+
return topmost;
1986+
}
1987+
1988+
static void update_loop_entry(struct bpf_verifier_state *cur, struct bpf_verifier_state *hdr)
1989+
{
1990+
struct bpf_verifier_state *cur1, *hdr1;
1991+
1992+
cur1 = get_loop_entry(cur) ?: cur;
1993+
hdr1 = get_loop_entry(hdr) ?: hdr;
1994+
/* The head1->branches check decides between cases B and C in
1995+
* comment for get_loop_entry(). If hdr1->branches == 0 then
1996+
* head's topmost loop entry is not in current DFS path,
1997+
* hence 'cur' and 'hdr' are not in the same loop and there is
1998+
* no need to update cur->loop_entry.
1999+
*/
2000+
if (hdr1->branches && hdr1->dfs_depth <= cur1->dfs_depth) {
2001+
cur->loop_entry = hdr;
2002+
hdr->used_as_loop_entry = true;
2003+
}
2004+
}
2005+
18482006
static void update_branch_counts(struct bpf_verifier_env *env, struct bpf_verifier_state *st)
18492007
{
18502008
while (st) {
18512009
u32 br = --st->branches;
18522010

2011+
/* br == 0 signals that DFS exploration for 'st' is finished,
2012+
* thus it is necessary to update parent's loop entry if it
2013+
* turned out that st is a part of some loop.
2014+
* This is a part of 'case A' in get_loop_entry() comment.
2015+
*/
2016+
if (br == 0 && st->parent && st->loop_entry)
2017+
update_loop_entry(st->parent, st->loop_entry);
2018+
18532019
/* WARN_ON(br > 1) technically makes sense here,
18542020
* but see comment in push_stack(), hence:
18552021
*/
@@ -16650,10 +16816,11 @@ static int is_state_visited(struct bpf_verifier_env *env, int insn_idx)
1665016816
{
1665116817
struct bpf_verifier_state_list *new_sl;
1665216818
struct bpf_verifier_state_list *sl, **pprev;
16653-
struct bpf_verifier_state *cur = env->cur_state, *new;
16819+
struct bpf_verifier_state *cur = env->cur_state, *new, *loop_entry;
1665416820
int i, j, n, err, states_cnt = 0;
1665516821
bool force_new_state = env->test_state_freq || is_force_checkpoint(env, insn_idx);
1665616822
bool add_new_state = force_new_state;
16823+
bool force_exact;
1665716824

1665816825
/* bpf progs typically have pruning point every 4 instructions
1665916826
* http://vger.kernel.org/bpfconf2019.html#session-1
@@ -16748,8 +16915,10 @@ static int is_state_visited(struct bpf_verifier_env *env, int insn_idx)
1674816915
*/
1674916916
spi = __get_spi(iter_reg->off + iter_reg->var_off.value);
1675016917
iter_state = &func(env, iter_reg)->stack[spi].spilled_ptr;
16751-
if (iter_state->iter.state == BPF_ITER_STATE_ACTIVE)
16918+
if (iter_state->iter.state == BPF_ITER_STATE_ACTIVE) {
16919+
update_loop_entry(cur, &sl->state);
1675216920
goto hit;
16921+
}
1675316922
}
1675416923
goto skip_inf_loop_check;
1675516924
}
@@ -16780,7 +16949,36 @@ static int is_state_visited(struct bpf_verifier_env *env, int insn_idx)
1678016949
add_new_state = false;
1678116950
goto miss;
1678216951
}
16783-
if (states_equal(env, &sl->state, cur, false)) {
16952+
/* If sl->state is a part of a loop and this loop's entry is a part of
16953+
* current verification path then states have to be compared exactly.
16954+
* 'force_exact' is needed to catch the following case:
16955+
*
16956+
* initial Here state 'succ' was processed first,
16957+
* | it was eventually tracked to produce a
16958+
* V state identical to 'hdr'.
16959+
* .---------> hdr All branches from 'succ' had been explored
16960+
* | | and thus 'succ' has its .branches == 0.
16961+
* | V
16962+
* | .------... Suppose states 'cur' and 'succ' correspond
16963+
* | | | to the same instruction + callsites.
16964+
* | V V In such case it is necessary to check
16965+
* | ... ... if 'succ' and 'cur' are states_equal().
16966+
* | | | If 'succ' and 'cur' are a part of the
16967+
* | V V same loop exact flag has to be set.
16968+
* | succ <- cur To check if that is the case, verify
16969+
* | | if loop entry of 'succ' is in current
16970+
* | V DFS path.
16971+
* | ...
16972+
* | |
16973+
* '----'
16974+
*
16975+
* Additional details are in the comment before get_loop_entry().
16976+
*/
16977+
loop_entry = get_loop_entry(&sl->state);
16978+
force_exact = loop_entry && loop_entry->branches > 0;
16979+
if (states_equal(env, &sl->state, cur, force_exact)) {
16980+
if (force_exact)
16981+
update_loop_entry(cur, loop_entry);
1678416982
hit:
1678516983
sl->hit_cnt++;
1678616984
/* reached equivalent register/stack state,
@@ -16829,7 +17027,8 @@ static int is_state_visited(struct bpf_verifier_env *env, int insn_idx)
1682917027
* speed up verification
1683017028
*/
1683117029
*pprev = sl->next;
16832-
if (sl->state.frame[0]->regs[0].live & REG_LIVE_DONE) {
17030+
if (sl->state.frame[0]->regs[0].live & REG_LIVE_DONE &&
17031+
!sl->state.used_as_loop_entry) {
1683317032
u32 br = sl->state.branches;
1683417033

1683517034
WARN_ONCE(br,

0 commit comments

Comments
 (0)