### Example related to packet access/offset domain:
**Example by Lucas**
*C code*
```
unsigned char pkt_refinements(struct xdp_md* ctx) {
void * begin = (void *)(long)ctx->data; // entry
void * end = (void *)(long)ctx->data_end;
void * ptr = begin;
unsigned char protocol;
if (ptr + sizeof(struct ethhdr) <= end) { // 5:6
struct ethhdr * eth = ptr;
if (bpf_ntohs(eth->h_proto) == ETH_P_IP) { // 10:11
ptr = ptr + sizeof(struct ethhdr);
struct iphdr * ip = ptr;
if (ptr + sizeof(struct iphdr) <= end) { // 13:14
protocol = ip->protocol;
ptr = ptr + sizeof(struct iphdr);
} else { // 13:15
protocol = 0;
}
} else { // 10:15
protocol = 0;
}
} else { // 5:15
protocol = 0;
}
return protocol;
}
```
*(Typed) Bytecode*
```
\Gamma = {
r1 : ctx_p<0>
v_begin = {v : pkt | v = begin <= end}
}
entry:
1. r0 : snumber<0> = 0
4. r2 : {v : pkt | v = end} = *(u32 *)(r1 + 4)
7. r1 : {v : pkt | v = begin} = *(u32 *)(r1 + 0)
8. r3 : {v : pkt | v = begin} = r1
10. r3 : {v : pkt | v = begin+14} += 14
goto 5:6,5:15;
5:15:
1. assume r3 > r2 // v_begin = {v : pkt | v = begin <= end}
goto 15;
5:6:
1. assume r3 <= r2 // v_begin = {v : pkt | v = begin < begin+14 <= end}
3. assert valid_access(r1.offset+13, width=1) for read
4. r3 : snumber<[0, 255]> = *(u8 *)(r1 + 13)
6. r3 : snumber<[0, 65280]> <<= 8
8. assert valid_access(r1.offset+12, width=1) for read
9. r4 : snumber<[0, 255]> = *(u8 *)(r1 + 12)
11. r3 : snumber<[0, 65535]> |= r4
goto 10:11,10:15;
10:15:
1. assume r3 != 8
goto 15;
10:11:
1. assume r3 == 8
2. r3 : {v : pkt | v = begin} = r1
4. r3 : {v : pkt | v = begin+34} += 34
goto 13:14,13:15;
13:15:
1. assume r3 > r2 // v_begin = {v : pkt | v = begin < begin+14 <= end}
goto 15;
13:14:
1. assume r3 <= r2 // v_begin = {v : pkt | v = begin < begin+34 <= end}
3. assert valid_access(r1.offset+23, width=1) for read
4. r0 : snumber<[0, 255]> = *(u8 *)(r1 + 23)
goto 15;
15: // v_begin = {v : pkt | v = begin <= end}
goto exit;
exit:
```
**Benchmark linux/xdp1_kern.o xdp1**
```
ctx: {
0: {v : pkt | v = begin}
4: {v : pkt | v = end}
}
```
*Example (1)* *
```
\Gamma = {
r1 : ctx_p<0>,
v_begin : {v : pkt | v = begin}
}
```
pre-state: <img src="https://hackmd.io/_uploads/S1TpNn2aa.png" alt="initial" width="200"/>
```
entry:
r2 : {v : pkt | v = end} = *(u32 *)(r1 + 4) // ctx-load
r1 : {v : pkt | v = begin} = *(u32 *)(r1 + 0) // ctx-load
r3 : {v : pkt | v = begin} = r1
r3 : {v : pkt | v = begin+14} += 14
goto 4:5, 4:59;
```
post-state: <img src="https://hackmd.io/_uploads/S1TpNn2aa.png" alt="initial" width="200"/>
pre-state: <img src="https://hackmd.io/_uploads/S1TpNn2aa.png" alt="initial" width="200"/>
```
4:5:
assume r3 <= r2
v_begin : {v : pkt | v = begin & begin + 14 <= end}
```
<img src="https://hackmd.io/_uploads/B1_HS32aT.png" alt="initial" width="200"/>
```
assert valid_access(r1+12, width=1)
r1 : {v : pkt | v = begin}
cst = begin + 12 + 1 <= end
cst' = neg(cst) = begin + 12 + 1 > end
cst' = end <= begin + 12
v_check : {v : pkt | v = begin}
v_check : {v : pkt | v = begin < begin + 14 <= end} // propagate from v_begin
v_check : {v : pkt | v = begin < begin + 14 <= end & cst'}
v_check : {v : pkt | v = begin < begin + 14 <= end <= begin + 12}
begin + 14 <= begin + 12 -- contradiction
v_check : bot -- valid access
assert valid_access(r1+13, width=1)
r1 : {v : pkt | v = begin}
cst = begin + 13 + 1 <= end
cst' = neg(cst) = begin + 13 + 1 > end
cst' = end <= begin + 13
v_check : {v : pkt | v = begin < begin + 14 <= end} // copy from v_begin?
v_check : {v : pkt | v = begin < begin + 14 <= end & cst'}
v_check : {v : pkt | v = begin < begin + 14 <= end <= begin + 13}
begin + 14 <= begin + 13 -- contradiction
v_check : bot -- valid access
```
post-state: <img src="https://hackmd.io/_uploads/B1_HS32aT.png" alt="initial" width="200"/>
pre-state: <img src="https://hackmd.io/_uploads/S1TpNn2aa.png" alt="initial" width="200"/>
```
4:59:
assume r3 > r2
v_begin : {v : pkt | v = begin >= end - 13}
```
post-state: <img src="https://hackmd.io/_uploads/Syxr9BATp.png" alt="initial" width="300"/>
*Example (2)* *
```
\Gamma = {
v_begin : {v : pkt | v = begin < begin + 14 <= end}
r1 : {v : pkt | v = begin}
}
```
pre-state: <img src="https://hackmd.io/_uploads/B1_HS32aT.png" alt="initial" width="200"/>
```
12:
r3 : {v : pkt | v = begin} = r1
r3 : {v : pkt | v = begin + 18} += 18
goto 14:15, 14:59;
```
post-state: <img src="https://hackmd.io/_uploads/B1_HS32aT.png" alt="initial" width="200"/>
pre-state: <img src="https://hackmd.io/_uploads/B1_HS32aT.png" alt="initial" width="200"/>
```
14:15:
assume r3 <= r2
v_begin : {v : pkt | v = begin < begin + 14 < begin + 18 <= end}
v_begin : {v : pkt | v = begin < begin + 18 <= end}
```
<img src="https://hackmd.io/_uploads/HyTTSn2p6.png" alt="initial" width="200"/>
```
assert valid_access(r1+16, width=2)
r1 : {v : pkt | v = begin}
cst = begin + 16 + 2 <= end
cst' = neg(cst) = begin + 18 > end
cst' = end < begin + 18
cst' = end <= begin + 17
v_check : {v : pkt | v = begin < begin + 18 <= end & cst'}
v_check : {v : pkt | v = begin < begin + 18 <= end <= begin + 17}
begin + 18 <= begin + 17 -- contradiction
v_check : bot -- valid access
```
post-state: <img src="https://hackmd.io/_uploads/HyTTSn2p6.png" alt="initial" width="200"/>
pre-state: <img src="https://hackmd.io/_uploads/B1_HS32aT.png" alt="initial" width="200"/>
```
14:59:
assume r3 > r2
v_begin : {v : pkt | v = begin < begin + 14 <= end & begin + 18 > end}
v_begin : {v : pkt | v = begin < begin + 14 <= end <= begin + 17}
```
post-state: <img src="https://hackmd.io/_uploads/HkZwMLAp6.png" alt="initial" width="300"/>
*Example (3)* *
```
\Gamma_1 = {
r1 : {v : pkt | v = begin}
r3 : {v : num | v = a_0}
a_0 : {v : num | v > 0}
v_begin : {v : pkt | v = begin < begin + 18 <= end}
}
```
<img src="https://hackmd.io/_uploads/HyTTSn2p6.png" alt="initial" width="200"/>
```
\Gamma_2 = {
r1 : {v : pkt | v = begin}
r3 : {v : num | v = a_1}
a_1 : {v : num | v > 0}
v_begin : {v : pkt | v = begin < begin + 14 <= end}
}
```
<img src="https://hackmd.io/_uploads/B1_HS32aT.png" alt="initial" width="200"/>
```
\Gamma = \Gamma_1 | \Gamma_2
\Gamma[r1] = {v : pkt | v = begin}
\Gamma[r3] = {v : num | v = a_0} | {v : num | v = a_1}
(given a_0 : {v : num | v > 0}, a_1 : {v : num | v > 0})
= {v : num | v > 0}
= {v : num | v = a_2}
(a_2 : {v : num | v > 0})
\Gamma[v_begin] = {v : pkt | v = begin < begin + 18 <= end} | {v : pkt | v = begin < begin + 14 <= end}
= {v : pkt | v = begin < begin + 14 <= end} -- how to get this systematically?
\Gamma = {
r1 : {v : pkt | v = begin}
r3 : {v : num | v = a_2}
a_2 : {v : num | v > 0}
v_begin : {v : pkt | v = begin < begin + 14 <= end}
}
```
pre-state: <img src="https://hackmd.io/_uploads/B1_HS32aT.png" alt="initial" width="200"/>
```
21:
r5 : {v : num | v = a_2} = r3
r5 : {v : num | v = a_2 + 4} += 4
r4 : {v : pkt | v = begin} = r1
r4 : {v : pkt | v = begin + a_2 + 4} += r5
goto 25:26, 25:59;
```
post-state: <img src="https://hackmd.io/_uploads/B1_HS32aT.png" alt="initial" width="200"/>
pre-state: <img src="https://hackmd.io/_uploads/B1_HS32aT.png" alt="initial" width="200"/>
```
25:26:
assume r4 <= r2
v_begin : {v : pkt | v = begin < begin + 14 <= end & begin + a_2 + 4 <= end}
```
<img src="https://hackmd.io/_uploads/HJO6v3npp.png" alt="initial" width="350"/>
```
r4 : {v : pkt | v = begin} = r1
r4 : {v : pkt | v = begin + a_2} += r3
assert valid_access(r4+2, width = 2)
cst = begin + a_2 + 2 + 2 <= end
cst = begin + a_2 + 4 <= end
cst' = neg(cst) = begin + a_2 + 4 > end
cst' = end <= begin + a_2 + 3
v_check : {v : pkt | v = begin < begin + 14 <= end & begin + a_2 + 4 <= end}
v_check : {v : pkt | v = begin < begin + 14 <= end & begin + a_2 + 4 <= end & cst'}
v_check : {v : pkt | v = begin < begin + 14 <= end & begin + a_2 + 4 <= end <= begin + a_2 + 3}
begin + a_2 + 4 <= end <= begin + a_2 + 3 -- contradiction
v_check : bot -- valid access
```
post-state: <img src="https://hackmd.io/_uploads/HJO6v3npp.png" alt="initial" width="350"/>
pre-state: <img src="https://hackmd.io/_uploads/B1_HS32aT.png" alt="initial" width="200"/>
```
25:59:
assume r4 > r2
v_begin : {v : pkt | v = begin < begin + 14 <= end & begin + a_2 + 4 > end}
v_begin : {v : pkt | v = begin < begin + 14 <= end <= begin + a_2 + 3}
```
post-state: <img src="https://hackmd.io/_uploads/H1Uy6L0p6.png" alt="initial" width="400"/>
*Example (3.5)*
```
\Gamma_1 = {
r1 : {v : pkt | v = begin}
r3 : {v : num | v = a_2}
a_2 : {v : num | v > 0}
v_begin : {v : pkt | v = begin < begin + 14 <= end}
}
```
<img src="https://hackmd.io/_uploads/B1_HS32aT.png" alt="initial" width="200"/>
```
\Gamma_2 = {
r1 : {v : pkt | v = begin}
r3 : {v : num | v = a_2}
a_2 : {v : num | v > 0}
v_begin : {v : pkt | v = begin < begin + 14 <= end & begin + a_0 + 4 <= end}
}
```
<img src="https://hackmd.io/_uploads/HJO6v3npp.png" alt="initial" width="350"/>
```
\Gamma = \Gamma_1 | \Gamma_2
\Gamma = {
r1 : {v : pkt | v = begin}
r3 : {v : num | v = a_2}
a_2 : {v : num | v > 0}
v_begin : {v : pkt | v = begin < begin + 14 <= end}
}
```
pre-state: <img src="https://hackmd.io/_uploads/B1_HS32aT.png" alt="initial" width="200"/>
```
30:
goto 31:40, 32:33
```
post-state: <img src="https://hackmd.io/_uploads/B1_HS32aT.png" alt="initial" width="200"/>
*Example (4)*
```
\Gamma = {
r1 : {v : pkt | v = begin}
r3 : {v : num | v = a_2}
a_2 : {v : num | v > 0}
v_begin : {v : pkt | v = begin < begin + 14 <= end}
}
```
pre-state: <img src="https://hackmd.io/_uploads/B1_HS32aT.png" alt="initial" width="200"/>
```
31:40:
r1 : {v : pkt | v = begin + a_2} += r3
a_2 : {v : num | v > 0}
r4 : {v : pkt | v = begin + a_2} = r1
r4 : {v : pkt | v = begin + a_2 + 40} += 40
goto 44:45, 44, 46;
```
post-state: <img src="https://hackmd.io/_uploads/B1_HS32aT.png" alt="initial" width="200"/>
pre-state: <img src="https://hackmd.io/_uploads/B1_HS32aT.png" alt="initial" width="200"/>
```
44:45:
assume r4 <= r2
v_begin : {v : pkt | v = begin < begin + 14 <= end & begin + a_2 + 40 <= end}
```
<img src="https://hackmd.io/_uploads/Hkuo_IyCT.png" alt="initial" width="350"/>
```
assert valid_access(r1+6, width = 1)
r1 : {v : pkt | v = begin + a_2}
cst = begin + a_2 + 16 + 1 <= end
cst' = neg(cst) = begin + a_2 + 17 > end
cst' = end <= begin + a_2 + 16
v_check : {v : pkt | v = begin < begin + 14 <= end & begin + a_2 + 40 <= end}
v_check : {v : pkt | v = begin < begin + 14 <= end & begin + a_2 + 40 <= end & cst'}
v_check : {v : pkt | v = begin < begin + 14 <= end & begin + a_2 + 40 <= end <= begin + a_2 + 16}
begin + a_2 + 40 <= begin + a_2 + 16 -- inconsistent
v_check : bot -- valid access
```
post-state: <img src="https://hackmd.io/_uploads/Hkuo_IyCT.png" alt="initial" width="350"/>
pre-state: <img src="https://hackmd.io/_uploads/B1_HS32aT.png" alt="initial" width="200"/>
```
44:46:
assume r4 > r2
v_begin : {v : pkt | v = begin < begin+14 <= end & begin + a_2 + 40 > end}
v_begin : {v : pkt | v = begin < begin+14 <= end <= begin + a_2 + 39}
```
post-state: <img src="https://hackmd.io/_uploads/B1X20UJAp.png" alt="initial" width="450"/>
*Example (5)* *
```
\Gamma = {
r1 : {v : pkt | v = begin}
r3 : {v : num | v = a_2}
a_2 : {v : num | v > 0}
v_begin : {v : pkt | v = begin < begin + 14 <= end}
}
```
pre-state: <img src="https://hackmd.io/_uploads/B1_HS32aT.png" alt="initial" width="200"/>
```
32:33:
r1 : {v : pkt | v = begin + a_2} += r3
r4 : {v : pkt | v = begin + a_2} = r1
r4 : {v : pkt | v = begin + a_2 + 20} += 20
goto 37:38, 37:46;
```
post-state: <img src="https://hackmd.io/_uploads/B1_HS32aT.png" alt="initial" width="200"/>
pre-state: <img src="https://hackmd.io/_uploads/B1_HS32aT.png" alt="initial" width="200"/>
```
37:38:
assume r4 <= r2
v_begin : {v : pkt | v = begin < begin + 14 <= end & begin+a_2+20 <= end}
```
<img src="https://hackmd.io/_uploads/ByCl4PyAT.png" alt="initial" width="400"/>
```
assert valid_access(r1+9, width = 1)
r1 : {v : pkt | v = begin + a_2}
cst = begin + a_2 + 9 + 1 <= end
cst' = neg(cst) = begin + a_2 + 10 > end
cst' = end <= begin + a_2 + 9
v_check : {v : pkt | v = begin < begin + 14 <= end & begin+a_2+20 <= end}
v_check : {v : pkt | v = begin < begin + 14 <= end & begin+a_2+20 <= end & cst'}
v_check : {v : pkt | v = begin < begin + 14 <= end & begin+a_2+20 <= end & end <= begin + a_2 + 9}
v_check : {v : pkt | v = begin < begin + 14 <= end & begin+a_2+20 <= end <= begin + a_2 + 9}
begin + a_2 + 20 <= begin + a_2 + 9 -- inconsistent
v_check : bot -- valid access
```
post-state: <img src="https://hackmd.io/_uploads/ByCl4PyAT.png" alt="initial" width="400"/>
pre-state: <img src="https://hackmd.io/_uploads/B1_HS32aT.png" alt="initial" width="200"/>
```
37:46:
assume r4 > r2
v_begin : {v : pkt | v = begin < begin + 14 <= end & end < begin + a_2 + 20}
v_begin : {v : pkt | v = begin < begin + 14 <= end & end <= begin + a_2 + 19}
```
post-state: <img src="https://hackmd.io/_uploads/BkppHDyAp.png" alt="initial" width="400"/>
**Benchmark linux/xdp2_kern.o xdp1**
```
ctx: {
4: {v : pkt | v = begin}
8: {v : pkt | v = end}
}
```
*Example (6)*
```
\Gamma = {
v_begin : {v : pkt | v = begin}
v_end : {v : pkt | v = end}
r1 : ctx_p<0>
}
entry:
r2 : {v : pkt | v = end} = *(u32 *)(r1 + 4) // ctx-load
r7 : {v : pkt | v = begin} = *(u32 *)(r1 + 0) // ctx-load
r1 : {v : pkt | v = begin} = r7
r1 : {v : pkt | v = begin+14} += 14
goto 5:6,5:76;
```
```
5:6:
assume r1 <= r2 v_begin : {v : pkt | v = begin < begin+14 <= end}
assert valid_access(r7+12, width=1)
r7 : {v : pkt | v = begin}
r7+12 : {v : pkt | v = begin+12}
r7+12 : {v : pkt | v = begin+12 < begin+14 <= end} // propagated
begin <= begin+12 <= begin+12+1 <= end
begin <= begin+12 <= begin+12+1 <= begin+14 -> holds
assert valid_access(r7+13, width=1)
r7 : {v : pkt | v = begin}
r7+13 : {v : pkt | v = begin+13}
r7+13 : {v : pkt | v = begin+13 < begin+14 <= end} // propagated
begin <= begin+13 <= begin+13+1 <= end
begin <= begin+13 <= begin+13+1 <= begin+14 -> holds
goto 76;
```
```
5:76:
assume r1 > r2 v_begin : {v : pkt | v = begin}
goto 76;
```
```
\Gamma = {
v_begin : {v : pkt | v = begin}
}
76:
goto exit;
```
*Example (7)*
```
\Gamma = {
r7 : {v : pkt | v = begin}
v_begin : {v : pkt | v = begin < begin + 14 <= end}
}
13:
r1 : {v : pkt | v = begin} = r7
r1 += 18
goto 15:16,15:76;
```
```
15:16:
assume r1 <= r2 v_begin : {v : pkt | v = begin < begin+18 <= end}
assert valid_access(r7+16, width = 2)
r7 : {v : pkt | v = begin}
r7+16 : {v : pkt | v = begin+16}
r7+16 : {v : pkt | v = begin+16 < begin+18 <= end} // propagated
begin <= begin+16 <= begin+16+2 <= end
begin <= begin+16 <= begin+16+2 <= begin+18 -> holds
```
```
15:76:
assume r1 > r2 v_begin : {v : pkt | v = begin < begin+14 <= end}
```
*Example (8)*
```
\Gamma = {
r1 : {v : num | v = a_0 & a_0 = [14, 18]}
r7 : {v : pkt | v = begin}
v_begin : {v : pkt | v = begin < begin + 18 <= end}
}
22:
r4 : {v : num | v = a_0 & a_0 = [14, 18]} = r1
r4 : {v : num | v = a_0 + 4 & a_0 = [14, 18]} += 4
r3 : {v : pkt | v = begin} = r7
r3 : {v : pkt | v = begin + a_0 + 4 & a_0 = [14, 18]} += r4
goto 26:27, 26:76
```
```
26:27:
assume r3 <= r2 v_begin : {v : pkt | v = begin < begin+a_0+4 <= end & a_0 = [14, 18]}
r3 : {v : pkt | v = begin} = r7
r3 : {v : pkt | v = begin + a_0 & a_0 = [14, 18]} += r1
assert valid_access(r3+2, width = 2)
r3 : {v : pkt | v = begin + a_0 & a_0 = [14, 18]}
r3+2 : {v : pkt | v = begin + a_0 + 2 & a_0 = [14, 18]}
r3+2 : {v : pkt | v = begin + a_0 + 2 < begin+a_0+4 <= end & a_0 = [14, 18]} // propagated
begin <= begin+a_0+2 <= begin+a_0+2+2 <= end
begin <= begin+a_0+2 <= begin+a_0+2+2 <= begin+a_0+4 -> holds
```
```
26:76:
assume r3 > r2 v_begin : {v : pkt | v = begin < begin+14 <= end}
```
*Example (9)*
```
\Gamma = {
r1 : {v : num | v = a_1 & a_1 = [14, 22]}
r7 : {v : pkt | v = begin}
v_begin : {v : pkt | v = begin < begin + 14 <= end}
}
32:42:
r3 : {v : pkt | v = begin} = r7
r3 : {v : pkt | v = begin + a_1 & a_1 = [14, 22]} += r1
r4 : {v : pkt | v = begin + a_1 & a_1 = [14, 22]} = r3
r4 : {v : pkt | v = begin + a_1 + 40 & a_1 = [14, 22]} += 40
goto 47:48,47:51;
```
```
47:48:
assume r4 <= r2 v_begin : {v : pkt | v = begin < begin+a_1+40 <= end & a_1 = [14, 22]}
assert valid_access(r3+6, width = 1)
r3 : {v : pkt | v = begin + a_1 & a_1 = [14, 22]}
r3+6 : {v : pkt | v = begin + a_1 + 6 & a_1 = [14, 22]}
r3+6 : {v : pkt | v = begin + a_1 + 6 < begin+a_1+40 <= end & a_1 = [14, 22]} // propagated
begin <= begin+a_1+6 <= begin+a_1+6+1 <= end
begin <= begin+a_1+6 <= begin+a_1+6+1 <= begin+a_1+40 -> holds
```
```
47:51:
assume r4 > r2 v_begin : {v : pkt | v = begin & begin+14 <= end}
```
*Example (10)*
```
\Gamma = {
r1 : {v : num | v = a_1 & a_1 = [14, 22]}
r7 : {v : pkt | v = begin}
v_begin : {v : pkt | v = begin < begin + 14 <= end}
}
33:34:
r3 : {v : pkt | v = begin} = r7
r3 : {v : pkt | v = begin + a_1 & a_1 = [14, 22]} += r1
r4 : {v : pkt | v = begin + a_1 & a_1 = [14, 22]} = r3
r4 : {v : pkt | v = begin + a_1 + 20 & a_1 = [14, 22]} += 20
goto 39:40,39:51;
```
```
39:40:
assume r4 <= r2 v_begin : {v : pkt | v = begin < begin+a_1+20 <= end & a_1 = [14, 22]}
assert valid_access(r3+9, width = 1)
r3 : {v : pkt | v = begin + a_1 & a_1 = [14, 22]}
r3+9 : {v : pkt | v = begin + a_1 + 9 & a_1 = [14, 22]}
r3+9 : {v : pkt | v = begin + a_1 + 9 < begin+a_1+20 <= end & a_1 = [14, 22]} // propagated
begin <= begin+a_1+9 <= begin+a_1+9+1 <= end
begin <= begin+a_1+9 <= begin+a_1+9+1 <= begin+a_1+20 -> holds
```
```
39:51:
assume r4 > r2 v_begin : {v : pkt | v = begin < begin+14 <= end}
```
*Example (11)*
```
\Gamma = {
r7 : {v : pkt | v = begin}
v_begin : {v : pkt | v = begin < begin + 14 <= end}
}
62:63:
assert valid_access(r7, width = 2)
r7 : {v : pkt | v = begin}
r7+0 : {v : pkt | v = begin}
r7+0 : {v : pkt | v = begin & begin+14 <= end} // propagated
begin <= begin <= begin+2 <= end
begin <= begin <= begin+2 <= begin+14 -> holds
assert valid_access(r7+6, width = 2)
r7 : {v : pkt | v = begin}
r7+6 : {v : pkt | v = begin + 6}
r7+6 : {v : pkt | v = begin + 6 < begin+14 <= end} // propagated
begin <= begin+6 <= begin+6+2 <= end
begin <= begin+6 <= begin+6+2 <= begin+14 -> holds
... (many valid_access asserts)
assert valid_access(r7+10, width = 2)
r7 : {v : pkt | v = begin}
r7+10 : {v : pkt | v = begin + 10}
r7+10 : {v : pkt | v = begin + 10 < begin+14 <= end} // propagated
begin <= begin+10 <= begin+10+2 <= end
begin <= begin+10 <= begin+10+2 <= begin+14 -> holds
```
**Benchmark linux/xdp_redirect_cpu_kern.o xdp_cpu_map3_proto_separate**
This program is similar to *linux/xdp1_kern.o xdp1* except for the following case:
*Example (12)* * -- join
```
\Gamma_1 = {
r1 : {v : pkt | v = begin+a_1+40}
r2 : {v : pkt | v = begin+a_1}
r3 : {v : pkt | v = end}
a_1 : {v : num | v > 0}
v_begin : {v : pkt | v = begin}
}
```
pre-state: <img src="https://hackmd.io/_uploads/S1TpNn2aa.png" alt="initial" width="200"/>
```
70:71:
assume r1 <= r3
v_begin : {v : pkt | v = begin < begin + a_1 + 40 <= end}
```
<img src="https://hackmd.io/_uploads/rkz1Kty0p.png" alt="initial" width="300"/>
```
r2 : {v : pkt | v = begin+a_1+6} += 6
goto 72;
```
post-state: <img src="https://hackmd.io/_uploads/rkz1Kty0p.png" alt="initial" width="300"/>
```
\Gamma_2 = {
r1 : {v : pkt | v = begin+a_1+20}
r2 : {v : pkt | v = begin+a_1}
r3 : {v : pkt | v = end}
a_1 : {v : num | v > 0}
v_begin : {v : pkt | v = begin}
}
```
pre-state: <img src="https://hackmd.io/_uploads/S1TpNn2aa.png" alt="initial" width="200"/>
```
58:59:
assume r1 <= r3
```
<img src="https://hackmd.io/_uploads/Hy1T9Yk0p.png" alt="initial" width="300"/>
```
r2 : {v : pkt | v = begin+a_1+9} += 9
goto 72;
```
post-state: <img src="https://hackmd.io/_uploads/Hy1T9Yk0p.png" alt="initial" width="300"/>
```
\Gamma = \Gamma_1 | \Gamma_2
\Gamma = {
r1 : {v : pkt | v = begin+a_1+[20,40]}
r2 : {v : pkt | v = begin+a_1+[6,9]}
r3 : {v : pkt | v = end}
v_begin : {v : pkt | v = begin+a_1+20 <= end}
}
```
pre-state: <img src="https://hackmd.io/_uploads/Hy1T9Yk0p.png" alt="initial" width="300"/>
```
72:
assert valid_access(r2, width = 1)
r2 : {v : pkt | v = begin+a_1+[6,9]}
cst = begin + a_1 + 9 + 1 <= end
cst' = neg(cst) = begin + a_1 + 9 >= end
cst' = end <= begin + a_1 + 9
v_check : {v : pkt | v = begin+a_1+20 <= end}
v_check : {v : pkt | v = begin+a_1+20 <= end & cst'}
v_check : {v : pkt | v = begin+a_1+20 <= end <= begin + a_1 + 9}
begin+a_1+20 <= begin + a_1 + 9 -- inconsistent
v_check : bot -- access holds
```
post-state: <img src="https://hackmd.io/_uploads/Hy1T9Yk0p.png" alt="initial" width="300"/>
**Benchmark linux/xdp_redirect_cpu_kern.o xdp_cpu_map4_ddos_filter_pktgen**
*Example (13)*
```
\Gamma = {
r1 : {v : num | v = a_1 = [14, 22]}
r7 : ctx_p<0>
v_begin : {v : pkt | v = begin}
}
63:
r3 : {v : pkt | v = begin} = *(u32 *)(r7 + 0); // ctx-load
r3 : {v : pkt | v = begin+a_1 & a_1 = [14, 22]} += r1
r1 : {v : pkt | v = begin+a_1 & a_1 = [14, 22]} = r3
r1 : {v : pkt | v = begin+a_1+20 & a_1 = [14, 22]} += 20
r2 : {v : pkt | v = end} = *(u32 *)(r7 + 4); // ctx-load
goto 70:71,70:101;
```
```
70:71:
assume r1 <= r2 // v_begin : {v : pkt | v = begin+a_1+20 <= end & a_1 = [14, 22]}
assert valid_access(r3+9, width = 1) -> holds
begin <= begin+a_1+9 <= begin+a_1+9+1 <= begin+a_1+20
```
```
70:101: // v_begin : {v : pkt | v = begin}
```
**Benchmark build/packet_overflow.o xdp**
*Example (14)*
```
\Gamma = {
r1 : ctx_p<0>
v_begin : {v : pkt | v = begin}
}
```
pre-state: <img src="https://hackmd.io/_uploads/S1TpNn2aa.png" alt="initial" width="200"/>
```
entry:
r2 : {v : pkt | v = begin} = *(u32 *)(r1 + 0)
r1 : {v : pkt | v = end} = *(u32 *)(r1 + 4)
goto 3:4, 3:8;
```
post-state: <img src="https://hackmd.io/_uploads/S1TpNn2aa.png" alt="initial" width="200"/>
```
3:4:
assume r2 <= r1
v_begin : {v : pkt | v = begin <= end}
```
<img src="https://hackmd.io/_uploads/ryIxg9JA6.png" alt="initial" width="300"/>
```
assert valid_access(r2, width=4)
r2 : {v : pkt | v = begin}
cst = begin + 4 <= end
cst' = neg(cst) = begin + 4 > end
cst' = end <= begin + 3
v_check : {v : pkt | v = begin <= end}
v_check : {v : pkt | v = begin <= end & cst'}
v_check : {v : pkt | v = begin <= end <= begin + 3}
begin <= begin + 3 -- satisfiable
v_check : {v : pkt | v = begin <= end <= begin + 3} -- invalid access
```
**Benchmark suricata/xdp_filter.o xdp**
*Example* *
```
\Gamma = {
v_begin : {v : pkt<i> | i = begin}
r9 : {v : pkt<i> | i = end}
r8 : {v : pkt<i> | i = begin + a_0 + [0, 4]}
a_0 : {v : num | v = [14, 18]}
} -> rewrite
\Gamma = {
v_begin : {v : pkt<i> | i = begin}
r9 : {v : pkt<i> | i = end}
r8 : {v : pkt<i> | i = begin + a_1}
a_1 : {v : num | v = [14, 22]}
}
```
```
33:34:
r1 : {v : pkt<i> | i = begin + a_1} = r8
r1 : {v : pkt<i> | i = begin + a_1 + 20} += 20
goto 46:46,46:324;
```
```
46:47:
assume r1 <= r9
v_begin : {v : pkt<i> | i = begin < begin + a_1 + 20 <= end}
assert valid_access(r8+9, width=1)
assert valid_access(r8+12, width=4)
assert valid_access(r8+16, width=4)
cst = begin + a_1 + 16 + 4 <= end
cst' = neg(cst) = end <= begin + a_1 + 19
v_begin : {v : pkt<i> | i = begin & begin + a_1 + 20 <= end <= begin + a_1 + 19}
v_begin : {v : pkt<i> | bot} -- valid access
```
(Old examples)
**Benchmark cilium/bpf_xdp_dsr_linux.o 2/21**
```
ctx: {
76: packet_p<begin+0>
80: packet_p<end>
}
r4 : packet_p<begin+0> = *(u32 *)(r1 + 76) // ctx-load
r2 : packet_p<end> = *(u32 *)(r1 + 80) // ctx-load
r3 : packet_p<begin+0> = r4;
r3 : packet_p<begin+12> += 12;
r3 : packet_p<begin+12>
r2 : packet_p<end> // [0, 64K]
316:317:
assume r3 <= r2 begin+12 <= end;
or begin+12+s = end; s >= 0;
r1 : packet_p<begin>
r1 : packet_p<begin+12>+= 12
r4 : packet_p<begin+12> = r1
r1 : packet_p<begin+14> += 2
goto 338:339, 338,341
```
```
r1 : packet_p<begin+14>
r2 : packet_p<end>
begin+12 <= end
338:339:
assume r1 <= r2 begin+14 <= end
goto 342;
```
```
r1 : packet_p<begin+14>
r2 : packet_p<end>
begin+12 <= end
338:341:
assume r1 > r2
goto 342;
```
```
r4 : packet_p<begin+12>
begin+12 <= end
342:
assert valid_access(r4.offset, width=2) for write
```
**Another example**
```
r4 : packet_p<begin+[14,18]>
r2 : packet_p<end>
bb1:
assume r4 <= r2 begin+14 <= end
goto bb;
```
```
r4 : packet_p<begin+[14,18]>
r2 : packet_p<end>
bb1:
assume r4 > r2
goto bb;
```
```
bb:
goto exit;
```
Sign in with Wallet
Connect another wallet