Commit f7fc7fb
selftests/bpf: test cases for bpf_loop SCC and state graph backedges
Test for state graph backedges accumulation for SCCs formed bt
bpf_loop(). Equivalent to the following C program:
int main(void) {
1: fp[-8] = bpf_get_prandom_u32();
2: fp[-16] = -32; // used in a memory access below
3: bpf_loop(7, loop_cb4, fp, 0);
4: return 0;
}
int loop_cb4(int i, void *ctx) {
5: if (unlikely(ctx[-8] > bpf_get_prandom_u32()))
6: *(u64 *)(fp + ctx[-16]) = 42; // aligned access expected
7: if (unlikely(fp[-8] > bpf_get_prandom_u32()))
8: ctx[-16] = -31; // makes said access unaligned
9: return 0;
}
If state graph backedges are not accumulated properly at SCC formed by
loop_cb4() call from bpf_loop(), the state {ctx[-16]=-32} injected at
9 on verification path 1,2,3,5,7,9,4 would be considered as complete
and lack precision mark for ctx[-16]. Leading to early pruning of
verification path 1,2,3,5,7,8,9 in state {ctx[-16]=-31}.
Leading to an assumption that the above program is safe.
Signed-off-by: Eduard Zingerman <eddyz87@gmail.com>1 parent 64ccd8d commit f7fc7fb
1 file changed
+75
-0
lines changed| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
1926 | 1926 | | |
1927 | 1927 | | |
1928 | 1928 | | |
| 1929 | + | |
| 1930 | + | |
| 1931 | + | |
| 1932 | + | |
| 1933 | + | |
| 1934 | + | |
| 1935 | + | |
| 1936 | + | |
| 1937 | + | |
| 1938 | + | |
| 1939 | + | |
| 1940 | + | |
| 1941 | + | |
| 1942 | + | |
| 1943 | + | |
| 1944 | + | |
| 1945 | + | |
| 1946 | + | |
| 1947 | + | |
| 1948 | + | |
| 1949 | + | |
| 1950 | + | |
| 1951 | + | |
| 1952 | + | |
| 1953 | + | |
| 1954 | + | |
| 1955 | + | |
| 1956 | + | |
| 1957 | + | |
| 1958 | + | |
| 1959 | + | |
| 1960 | + | |
| 1961 | + | |
| 1962 | + | |
| 1963 | + | |
| 1964 | + | |
| 1965 | + | |
| 1966 | + | |
| 1967 | + | |
| 1968 | + | |
| 1969 | + | |
| 1970 | + | |
| 1971 | + | |
| 1972 | + | |
| 1973 | + | |
| 1974 | + | |
| 1975 | + | |
| 1976 | + | |
| 1977 | + | |
| 1978 | + | |
| 1979 | + | |
| 1980 | + | |
| 1981 | + | |
| 1982 | + | |
| 1983 | + | |
| 1984 | + | |
| 1985 | + | |
| 1986 | + | |
| 1987 | + | |
| 1988 | + | |
| 1989 | + | |
| 1990 | + | |
| 1991 | + | |
| 1992 | + | |
| 1993 | + | |
| 1994 | + | |
| 1995 | + | |
| 1996 | + | |
| 1997 | + | |
| 1998 | + | |
| 1999 | + | |
| 2000 | + | |
| 2001 | + | |
| 2002 | + | |
| 2003 | + | |
1929 | 2004 | | |
0 commit comments