---
# System prepended metadata

title: prototype-kernel-xdp_vlan01_kern xdp_vlan_remove_outer2
tags: [ebpf]

---

###### tags: `ebpf`

# prototype-kernel-xdp_vlan01_kern xdp_vlan_remove_outer2


### pointer

```
using pointer_uck<l,u,s> = { v : u32 | l <= v-start(s) <= u };

using pointer<l,u,s> = { v : pointer_uck<l,u,s> | v-start(s) <= sizeof(s)};
```

### packet
  ```
constant packet_size : { v : u32 | v < 65536 };

struct packet_t { 
    blob : [u8;packet_size];
  }

variable packet : packet_t;

using packet_p<off> = pointer<off,off,packet>;

using packet_p_uck<Off> = pointer_uck<Off, Off, packet>;

using packet_p<l,u> = pointer<l,u,packet>;

using packet_start_p = packet_p<0>;

using packet_end_p = packet_p<sizeof(packet)>;
```

### ctx
  ```
constant ctx_size : {v : u32 | v >= 8};

struct ctx_t {
    data : packet_start_p;
    data_end : packet_end_p; 
    blob : [u8;ctx_size-8];
  }
  
  variable ctx : ctx_t;
  
  using ctx_p<off> = pointer<off, off, ctx>;
  
  using ctx_start_p = ctx_p<0>;
  
  using ctx_end_p = ctx_p<sizeof(ctx)>;
```

### Regions
```
using typed_reg = stack | ctx;
using untyped_reg = packet | shared;
```

### register inits
```
variable r1 : ctx_start_p;
``` 
=================================
### code
```
entry:
  ...
  let r3:packet_end_p = *(r1:ctx_start_p + 4);
      
  let r2:packet_start_p = *(r1:ctx_start_p + 0);
      
  let r4:packet_start_p = r2:packet_start_p;
      
  let r4:pointer_uck<22,22,packet> = r4:packet_start_p + 22;

  goto 5:6,5:21;
```

```
5:6:
  assume r4:pointer<22,22,packet> <= r3:packet_end_p;
      22 >= sizeof(packet)
      
  let r4:u8 = *(u8 *)(r2:packet_start_p + 12);
      
  let r3:u8 = *(u8 *)(r2:packet_start_p + 13);

  ...
  goto 11:12,11:13;
```
  
```
5:21:
  assume r4:pointer_uck<22,22,packet> > r3:packet_end_p;
  
  goto 21;
```
  
```
11:12:
  ...
  goto 12:13,12:21;
```

```
11:13:
  ...
  goto 13;
```

```
12:13:
  ...
  goto 13;
```

```
12:21:
  ...
  goto 21;
```

```
13:
  let r3:u32 = *(u32 *)(r2:packet_start_p + 8);
      
  *(r2:packet_start_p + 12) = r3:u32;
      
  let r3:u32 = *(u32 *)(r2:packet_start_p + 4);
      
  let r4:u32 = *(u32 *)(r2:packet_start_p + 0);
      
  *(r2:packet_start_p + 4) = r4:u32;
      
  *(r2:packet_start_p + 8) = r3:u32;
      
  ...
  goto 21;
```

```
21:
  ...
  exit;
  goto exit;
```

```
exit:
```
