###### tags: `ebpf`

# linux test_cgrp2_tc_kern filter

### 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 {
    blob0 : [u8;76];
    data : packet_start_p;
    data_end : packet_end_p; 
    blob1 : [u8;ctx_size-76-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)>;

### stack

constant stack_size : u32 = 512;
  
struct stack_t { 
    f48 : u64;  // offset stack_end-48
    f40 : u32;  // offset stack_end-40
    f36 : u16;  // offset stack_end-36
    blob1 : [u8;2];
    f32 : u64;  // offset stack_end-32
    f24 : u64;  // offset stack_end-24
    f16 : u16;  // offset stack_end-16
    f14 : u8;   // offset stack_end-14
    blob0 : [u8;14]; 
  }
  
  variable stack : stack_t;
  
  using stack_p<off> = pointer<off, off, stack>;
  
  using stack_start_p = stack_p<0>;
  
  using stack_end_p = stack_p<sizeof(stack)>;

### Regions

using typed_reg = stack | ctx;
using untyped_reg = packet | shared;

### register inits

variable r1 : ctx_start_p;

variable r10 : stack_end_p;

=================================
### code

entry:
  let r3:packet_end_p = *(r1:ctx_start_p + 80);
      Gamma: { r3:packet_end_p, r1:ctx_start_p, r10:stack_end_p }
      
  let r2:packet_start_p = *(r1:ctx_start_p + 76);
      Gamma: { r3:packet_end_p, r1:ctx_start_p, r2:packet_start_p, r10:stack_end_p }
      
  r4:T4 = 2660;
  *(r10:stack_end_p - 16) = r4:T4;
      T4 <: u16
      Gamma: { r3:packet_end_p, r1:ctx_start_p, r2:packet_start_p, r10:stack_end_p }
      
  let r4:T5 = 807739493 ll;
  *(r10:stack_end_p - 24) = r4:T5;
      T5 <: u64
      Gamma: { r3:packet_end_p, r1:ctx_start_p, r2:packet_start_p, r10:stack_end_p }
      
  let r4:T7 = 1953394532 ll;
  *(r10:stack_end_p - 32) = r4:T7;
      T7 <: u64
      Gamma: { r3:packet_end_p, r1:ctx_start_p, r2:packet_start_p, r10:stack_end_p }
      
  let r6:T6 = 0;
  *(r10:stack_end_p - 14) = r6:T6;
      T6 <: u8
      Gamma: { r3:packet_end_p, r1:ctx_start_p, r2:packet_start_p, r10:stack_end_p }
      
  let r4:T8 = 10;
  *(r10:stack_end_p - 36) = r4:T8;
      T8 <: u16
      Gamma: { r3:packet_end_p, r1:ctx_start_p, r2:packet_start_p, r10:stack_end_p }
      
  let r4:T9 = 1936941424;
  *(r10:stack_end_p - 40) = r4;
      T9 <: u32
      Gamma: { r3:packet_end_p, r1:ctx_start_p, r2:packet_start_p, r10:stack_end_p }
      
  let r4:T11 = 1701471602 ll;
  *(r10:stack_end_p - 48) = r4:T11;
      T11 <: u64
      Gamma: { r3:packet_end_p, r1:ctx_start_p, r2:packet_start_p, r10:stack_end_p }
      
  let r4:packet_start_p = r2:packet_start_p;
      Gamma: { r3:packet_end_p, r1:ctx_start_p, r2:packet_start_p, r10:stack_end_p, r4:packet_start_p }
      
  let r4:pointer_uck<54,54,packet> = r4:packet_start_p + 54;
      Gamma: { r3:packet_end_p, r1:ctx_start_p, r2:packet_start_p, r10:stack_end_p, r4:pointer_uck<54,54,packet> }
  goto 21:22,21:49;

21:22:
  assume r4:pointer<54,54,packet> <= r3:packet_end_p;
      Gamma: { r3:packet_end_p, r1:ctx_start_p, r2:packet_start_p, r10:stack_end_p, r4:pointer<54,54,packet> }
      54 <= sizeof_region(packet)
      
  let r4:u8 = *(u8 *)(r2:packet_start_p + 20);
  let r3:u16 = *(u16 *)(r2:packet_start_p + 12);
  goto 24:25,24:26;

21:49:
  assume r4:pointer_uck<54,54,packet> > r3:packet_end_p;
      Gamma: { r3:packet_end_p, r1:ctx_start_p, r2:packet_start_p, r10:stack_end_p, r4:pointer_uck<54,54,packet> }
      
  goto 49;

24:25:
  assume r3:T16 == 56710;
  goto 25:26,25:31;

24:26:
  assume r3:T16 != 56710;
  goto 26;

25:26:
  assume r4:T15 != 58;
  goto 26;

25:31:
  assume r4:T15 == 58;
      Gamma: { r3:packet_end_p, r1:ctx_start_p, r2:packet_start_p, r10:stack_end_p, r4:pointer<54,54,packet> }
      
  let r6:T17 = 0;
  let r2:T18 = map_fd 1;
  let r3:T19 = 0;
  let r0:T20 = skb_under_cgroup:33(ctx r1, map_fd r2, uint64_t r3);
      Gamma: { r3:packet_end_p, r1:ctx_start_p, r2:packet_start_p, r10:stack_end_p, r4:pointer<54,54,packet> }
      
  let r0:T21 = r0:T20 << 32;
  let r0:T22 = r0:T21 >> 32;
  goto 38:39,38:44;

26:
  let r1:stack_end_p = r10:stack_end_p;
      Gamma: { r3:packet_end_p, r1:stack_end_p, r2:packet_start_p, r10:stack_end_p, r4:pointer<54,54,packet> }
      
  let r1:pointer<512-32,512-32,stack> = r1:stack_end_p-32;
      Gamma: { r3:packet_end_p, r1:pointer<512-32,512-32,stack>, r2:packet_start_p, r10:stack_end_p, r4:pointer<54,54,packet> }
      
  let r2:T25 = 19;
  let r0:T26 = trace_printk:6(mem r1:pointer<512-32,512-32,stack>[r2:T25], uint64_t r2);
      Gamma: { r3:packet_end_p, r1:pointer<512-32,512-32,stack>, r2:packet_start_p, r10:stack_end_p, r4:pointer<54,54,packet> }
      
  goto 49;

38:39:
  assume r0:T22 != 1;
      Gamma: { r3:packet_end_p, r1:ctx_start_p, r2:packet_start_p, r10:stack_end_p, r4:pointer<54,54,packet> }
      
  let r1:stack_end_p = r10:stack_end_p;
      Gamma: { r3:packet_end_p, r1:stack_end_p, r2:packet_start_p, r10:stack_end_p, r4:pointer<54,54,packet> }
      
  let r1:pointer<512-40,512-40,stack> = r1:stack_end_p-40;
      Gamma: { r3:packet_end_p, r1:pointer<512-40,512-40,stack>, r2:packet_start_p, r10:stack_end_p, r4:pointer<54,54,packet> }
      
  let r2:T28 = 6;
  let r0:T29 = trace_printk:6(mem r1:pointer<512-40,512-40,stack>[r2:T28], uint64_t r2);
      Gamma: { r3:packet_end_p, r1:pointer<512-40,512-40,stack>, r2:packet_start_p, r10:stack_end_p, r4:pointer<54,54,packet> }
      
  goto 49;

38:44:
  assume r0:T22 == 1;
      Gamma: { r3:packet_end_p, r1:ctx_start_p, r2:packet_start_p, r10:stack_end_p, r4:pointer<54,54,packet> }
      
  let r1:stack_end_p = r10:stack_end_p;
      Gamma: { r3:packet_end_p, r1:stack_end_p, r2:packet_start_p, r10:stack_end_p, r4:pointer<54,54,packet> }
      
  let r1:pointer<512-48,512-48,stack> = r1:stack_end_p-48;
      Gamma: { r3:packet_end_p, r1:pointer<512-48,512-48,stack>, r2:packet_start_p, r10:stack_end_p, r4:pointer<54,54,packet> }
      
  let r2:T31 = 8;
  let r0:T32 = trace_printk:6(mem pointer<512-48,512-48,stack>[r2:T31], uint64_t r2);
      Gamma: { r3:packet_end_p, r1:pointer<512-48,512-48,stack>, r2:packet_start_p, r10:stack_end_p, r4:pointer<54,54,packet> }
      
  let r6:T32 = 2;
  goto 49;

49:
  let r0:T33 = r6:T32;
  exit;
  goto exit;

exit: