@@ -1863,4 +1863,141 @@ l1_%=: r0 = 1; \
18631863 : __clobber_all );
18641864}
18651865
1866+ /* This test covers the bounds deduction when the u64 range and the tnum
1867+ * overlap only at umax. After instruction 3, the ranges look as follows:
1868+ *
1869+ * 0 umin=0xe01 umax=0xf00 U64_MAX
1870+ * | [xxxxxxxxxxxxxx] |
1871+ * |----------------------------|------------------------------|
1872+ * | x x | tnum values
1873+ *
1874+ * The verifier can therefore deduce that the R0=0xf0=240.
1875+ */
1876+ SEC ("socket" )
1877+ __description ("bounds refinement with single-value tnum on umax" )
1878+ __msg ("3: (15) if r0 == 0xe0 {{.*}} R0=240" )
1879+ __success __log_level (2 )
1880+ __flag (BPF_F_TEST_REG_INVARIANTS )
1881+ __naked void bounds_refinement_tnum_umax (void * ctx )
1882+ {
1883+ asm volatile (" \
1884+ call %[bpf_get_prandom_u32]; \
1885+ r0 |= 0xe0; \
1886+ r0 &= 0xf0; \
1887+ if r0 == 0xe0 goto +2; \
1888+ if r0 == 0xf0 goto +1; \
1889+ r10 = 0; \
1890+ exit; \
1891+ " :
1892+ : __imm (bpf_get_prandom_u32 )
1893+ : __clobber_all );
1894+ }
1895+
1896+ /* This test covers the bounds deduction when the u64 range and the tnum
1897+ * overlap only at umin. After instruction 3, the ranges look as follows:
1898+ *
1899+ * 0 umin=0xe00 umax=0xeff U64_MAX
1900+ * | [xxxxxxxxxxxxxx] |
1901+ * |----------------------------|------------------------------|
1902+ * | x x | tnum values
1903+ *
1904+ * The verifier can therefore deduce that the R0=0xe0=224.
1905+ */
1906+ SEC ("socket" )
1907+ __description ("bounds refinement with single-value tnum on umin" )
1908+ __msg ("3: (15) if r0 == 0xf0 {{.*}} R0=224" )
1909+ __success __log_level (2 )
1910+ __flag (BPF_F_TEST_REG_INVARIANTS )
1911+ __naked void bounds_refinement_tnum_umin (void * ctx )
1912+ {
1913+ asm volatile (" \
1914+ call %[bpf_get_prandom_u32]; \
1915+ r0 |= 0xe0; \
1916+ r0 &= 0xf0; \
1917+ if r0 == 0xf0 goto +2; \
1918+ if r0 == 0xe0 goto +1; \
1919+ r10 = 0; \
1920+ exit; \
1921+ " :
1922+ : __imm (bpf_get_prandom_u32 )
1923+ : __clobber_all );
1924+ }
1925+
1926+ /* This test covers the bounds deduction when the only possible tnum value is
1927+ * in the middle of the u64 range. After instruction 3, the ranges look as
1928+ * follows:
1929+ *
1930+ * 0 umin=0x7cf umax=0x7df U64_MAX
1931+ * | [xxxxxxxxxxxx] |
1932+ * |----------------------------|------------------------------|
1933+ * | x x x x x | tnum values
1934+ * | +--- 0x7e0
1935+ * +--- 0x7d0
1936+ *
1937+ * Since the lower four bits are zero, the tnum and the u64 range only overlap
1938+ * in R0=0x7d0=2000. Instruction 5 is therefore dead code.
1939+ */
1940+ SEC ("socket" )
1941+ __description ("bounds refinement with single-value tnum in middle of range" )
1942+ __msg ("3: (a5) if r0 < 0x7cf {{.*}} R0=2000" )
1943+ __success __log_level (2 )
1944+ __naked void bounds_refinement_tnum_middle (void * ctx )
1945+ {
1946+ asm volatile (" \
1947+ call %[bpf_get_prandom_u32]; \
1948+ if r0 & 0x0f goto +4; \
1949+ if r0 > 0x7df goto +3; \
1950+ if r0 < 0x7cf goto +2; \
1951+ if r0 == 0x7d0 goto +1; \
1952+ r10 = 0; \
1953+ exit; \
1954+ " :
1955+ : __imm (bpf_get_prandom_u32 )
1956+ : __clobber_all );
1957+ }
1958+
1959+ /* This test cover the negative case for the tnum/u64 overlap. Since
1960+ * they contain the same two values (i.e., {0, 1}), we can't deduce
1961+ * anything more.
1962+ */
1963+ SEC ("socket" )
1964+ __description ("bounds refinement: several overlaps between tnum and u64" )
1965+ __msg ("2: (25) if r0 > 0x1 {{.*}} R0=scalar(smin=smin32=0,smax=umax=smax32=umax32=1,var_off=(0x0; 0x1))" )
1966+ __failure __log_level (2 )
1967+ __naked void bounds_refinement_several_overlaps (void * ctx )
1968+ {
1969+ asm volatile (" \
1970+ call %[bpf_get_prandom_u32]; \
1971+ if r0 < 0 goto +3; \
1972+ if r0 > 1 goto +2; \
1973+ if r0 == 1 goto +1; \
1974+ r10 = 0; \
1975+ exit; \
1976+ " :
1977+ : __imm (bpf_get_prandom_u32 )
1978+ : __clobber_all );
1979+ }
1980+
1981+ /* This test cover the negative case for the tnum/u64 overlap. Since
1982+ * they overlap in the two values contained by the u64 range (i.e.,
1983+ * {0xf, 0x10}), we can't deduce anything more.
1984+ */
1985+ SEC ("socket" )
1986+ __description ("bounds refinement: multiple overlaps between tnum and u64" )
1987+ __msg ("2: (25) if r0 > 0x10 {{.*}} R0=scalar(smin=umin=smin32=umin32=15,smax=umax=smax32=umax32=16,var_off=(0x0; 0x1f))" )
1988+ __failure __log_level (2 )
1989+ __naked void bounds_refinement_multiple_overlaps (void * ctx )
1990+ {
1991+ asm volatile (" \
1992+ call %[bpf_get_prandom_u32]; \
1993+ if r0 < 0xf goto +3; \
1994+ if r0 > 0x10 goto +2; \
1995+ if r0 == 0x10 goto +1; \
1996+ r10 = 0; \
1997+ exit; \
1998+ " :
1999+ : __imm (bpf_get_prandom_u32 )
2000+ : __clobber_all );
2001+ }
2002+
18662003char _license [] SEC ("license" ) = "GPL" ;
0 commit comments