---
# System prepended metadata

title: eBPF Offset Domain examples
tags: [ebpf]

---

### 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;
```
