From f64792d74af901dcdf264f26cd301581baf0ad58 Mon Sep 17 00:00:00 2001
From: linsyking <kxiang@umich.edu>
Date: Thu, 11 Jul 2024 22:48:38 -0400
Subject: [PATCH 01/24] feat: add load imm support

---
 IR/bpf_ir.c         | 23 ++++++++++++++++++++++-
 IR/include/passes.h |  2 +-
 IR/probe.c          |  6 +++---
 3 files changed, 26 insertions(+), 5 deletions(-)

diff --git a/IR/bpf_ir.c b/IR/bpf_ir.c
index a0a9257f..a8751fdd 100644
--- a/IR/bpf_ir.c
+++ b/IR/bpf_ir.c
@@ -555,7 +555,28 @@ void transform_bb(struct ssa_transform_env *env, struct pre_ir_basic_block *bb)
         } else if (BPF_CLASS(code) == BPF_LD && BPF_MODE(code) == BPF_IMM &&
                    BPF_SIZE(code) == BPF_DW) {
             // 64-bit immediate load
-            // TODO
+            if (insn.src_reg == 0x0) {
+                // TODO
+                struct ir_insn *new_insn = create_insn_back(bb->ir_bb);
+                new_insn->op             = IR_INSN_LOADRAW;
+                struct ir_address_value addr_val;
+                struct ir_value imm_ptr;
+                imm_ptr.type = IR_VALUE_CONSTANT;
+                imm_ptr.data.constant_d.type = IR_CONSTANT_U64;
+                imm_ptr.data.constant_d.data.u64_d = insn.imm64;
+                addr_val.value = imm_ptr;
+                add_user(env, new_insn, addr_val.value);
+                addr_val.offset    = 0;
+                new_insn->vr_type  = IR_VR_TYPE_U64;
+                new_insn->addr_val = addr_val;
+
+                struct ir_value new_val;
+                new_val.type        = IR_VALUE_INSN;
+                new_val.data.insn_d = new_insn;
+                write_variable(env, insn.dst_reg, bb, new_val);
+            } else {
+                CRITICAL("Not supported");
+            }
         } else if (BPF_CLASS(code) == BPF_LDX && BPF_MODE(code) == BPF_MEMSX) {
             // dst = *(signed size *) (src + offset)
             // https://www.kernel.org/doc/html/v6.6/bpf/standardization/instruction-set.html#sign-extension-load-operations
diff --git a/IR/include/passes.h b/IR/include/passes.h
index c43e200d..7d5e2d9e 100644
--- a/IR/include/passes.h
+++ b/IR/include/passes.h
@@ -11,7 +11,7 @@
 static void (*passes[])(struct ir_function *fun) = {
     gen_reachable_bbs,
     remove_trivial_phi,
-    add_counter,
+    // add_counter,
 };
 
 #endif
diff --git a/IR/probe.c b/IR/probe.c
index b36337b2..b523b900 100644
--- a/IR/probe.c
+++ b/IR/probe.c
@@ -6,9 +6,9 @@ void run(struct bpf_insn *insns, size_t len) {
     printf("CLASS\tSIZE\tMODE\tOP\tSRC\tIMM\n");
     for (size_t i = 0; i < len; ++i) {
         __u8 code = insns[i].code;
-        if (code == 0) {
-            continue;
-        }
+        // if (code == 0) {
+        //     continue;
+        // }
         printf("%02x\t%02x\t%02x\t%02x\t%02x\t%d\n", BPF_CLASS(code), BPF_SIZE(code),
                BPF_MODE(code), BPF_OP(code), BPF_SRC(code), insns[i].imm);
     }

From eee721ff4a630fc5cf16d4e017f68413eabe2987 Mon Sep 17 00:00:00 2001
From: linsyking <kxiang@umich.edu>
Date: Mon, 15 Jul 2024 16:22:25 -0400
Subject: [PATCH 02/24] feat: refactor

---
 .gitignore                 |   3 +
 IR/Readme.md               |  16 +++-
 IR/tests/Makefile          |  16 ++++
 IR/tests/b2b.c             |  22 ++++++
 IR/tests/loop1.c           |  17 +++++
 IR/tests/test_asm.c        |  46 ++++++++++++
 docs/Constraints.md        |   1 +
 rejected/custom/b2b.s      |  40 ----------
 rejected/custom/complex.s  | 116 ----------------------------
 rejected/custom/loop1.s    |  26 -------
 rejected/custom/test_asm.s | 150 -------------------------------------
 11 files changed, 117 insertions(+), 336 deletions(-)
 create mode 100644 IR/tests/Makefile
 create mode 100644 IR/tests/b2b.c
 create mode 100644 IR/tests/loop1.c
 create mode 100644 IR/tests/test_asm.c
 create mode 100644 docs/Constraints.md
 delete mode 100644 rejected/custom/b2b.s
 delete mode 100644 rejected/custom/complex.s
 delete mode 100644 rejected/custom/loop1.s
 delete mode 100644 rejected/custom/test_asm.s

diff --git a/.gitignore b/.gitignore
index c6127b38..2673917d 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,3 +1,6 @@
+# Assembly code
+*.s
+
 # Prerequisites
 *.d
 
diff --git a/IR/Readme.md b/IR/Readme.md
index d04ca805..b2a6e5cc 100644
--- a/IR/Readme.md
+++ b/IR/Readme.md
@@ -1,7 +1,15 @@
-# TODO
+# Verifier
+
+We design a form of constraint that could describe all types of ebpf verifier rules. The verifier will generate a "constaint set" based on static analysis information (e.g. BTF) and that doesn't need any simulation.
+
+Then this constaint set will be passed to our IR and we will add check for those constaints. Since currently our IR is typeless so we can only use some raw constaint generated from the verifier.
 
-## BB users
+To start with, a simple constaint would be "range constraint", meaning a register (at a specific position) must be within a range.
 
-Used in PHI nodes.
+One opinion, one benefit of designing the raw constraint from is that our runtime-check system will not depend heavily on the current linux verifier and will be portable to other verifiers.
+
+# TODO
 
-## Type checker
+- More instructions
+- bpf-to-bpf calls
+- tail calls
diff --git a/IR/tests/Makefile b/IR/tests/Makefile
new file mode 100644
index 00000000..7a2968ee
--- /dev/null
+++ b/IR/tests/Makefile
@@ -0,0 +1,16 @@
+$(NAME).o: $(NAME).c
+	clang -O2 -I/usr/include/$(shell uname -m)-linux-gnu -g -target bpf -c $< -o $@
+
+$(NAME).s: $(NAME).o
+	# clang -O2 -I/usr/include/$(shell uname -m)-linux-gnu -target bpf -S -o $(NAME).s $(NAME).c
+	llvm-objdump -S $< > $@
+
+sobj: $(NAME).S
+	llvm-mc -triple bpf -filetype=obj -o $(NAME).o $(NAME).S
+
+load:
+	sudo bpftool prog load $(NAME).o /sys/fs/bpf/$(NAME)
+
+clean:
+	rm -f $(NAME).o $(NAME).S
+	sudo rm /sys/fs/bpf/$(NAME)
diff --git a/IR/tests/b2b.c b/IR/tests/b2b.c
new file mode 100644
index 00000000..3772ba87
--- /dev/null
+++ b/IR/tests/b2b.c
@@ -0,0 +1,22 @@
+#include <linux/bpf.h>
+#include <bpf/bpf_helpers.h>
+
+void __noinline call1() {
+    bpf_trace_printk("hello world", 2);
+}
+
+void __noinline call2() {
+    bpf_trace_printk("world", 6);
+}
+
+SEC("xdp")
+int prog(void *ctx) {
+    // char s1[] = "hello world my friend";
+    char s1[] = "1";
+    bpf_trace_printk(s1, sizeof(s1));
+    call1();
+    call2();
+    return 0;
+}
+
+char _license[] SEC("license") = "GPL";
diff --git a/IR/tests/loop1.c b/IR/tests/loop1.c
new file mode 100644
index 00000000..b0a0d0a1
--- /dev/null
+++ b/IR/tests/loop1.c
@@ -0,0 +1,17 @@
+#include <linux/bpf.h>
+#include <bpf/bpf_helpers.h>
+
+/**
+    Calling external function results in verifier halt
+ */
+
+SEC("xdp")
+int prog(void *ctx) {
+    __u64 t = bpf_ktime_get_ns();
+    for (int i = 0; i < t; ++i) {
+        bpf_trace_printk("s", 1);
+    }
+    return 0;
+}
+
+char _license[] SEC("license") = "GPL";
diff --git a/IR/tests/test_asm.c b/IR/tests/test_asm.c
new file mode 100644
index 00000000..4307c70d
--- /dev/null
+++ b/IR/tests/test_asm.c
@@ -0,0 +1,46 @@
+#include <linux/bpf.h>
+#include <bpf/bpf_helpers.h>
+
+int __noinline spill(int cr, int ci) {
+    int i  = 0;
+    int zr = 0;
+    int zi = 0;
+    int zk = 0;
+    int zl = 0;
+
+    while (i < 100 && zr * zr + zi * zi + zk * zk - zl * zl * (zi - 1) < 4) {
+        int t = zr * zr - zi * zi + cr;
+        zi    = 2 * zr * zi + ci;
+        zr    = t;
+        zk    = 3 * zr - zi * zi * zk * zr;
+        zl    = zl + 1;
+
+        i = i + 1;
+    }
+    return i;
+}
+
+void __noinline pk(char s) {
+    bpf_trace_printk("%c", 1, s);
+}
+
+void __noinline pk_l(char *s) {
+    bpf_trace_printk("%s", 1, s);
+}
+
+SEC("xdp")
+int prog(void *ctx) {
+    int s = spill(1, 2);
+    static char ores[10] = "helloggg";
+    static char res[10] = "helloworld";
+    for (int i = 0; i < 10; ++i) {
+        pk(res[i]);
+    }
+    pk_l(res);
+    pk_l(ores);
+    pk(res[0]);
+    res[0] = s;
+    return 0;
+}
+
+char _license[] SEC("license") = "GPL";
diff --git a/docs/Constraints.md b/docs/Constraints.md
new file mode 100644
index 00000000..10239039
--- /dev/null
+++ b/docs/Constraints.md
@@ -0,0 +1 @@
+# Constraint
diff --git a/rejected/custom/b2b.s b/rejected/custom/b2b.s
deleted file mode 100644
index 39c0f0aa..00000000
--- a/rejected/custom/b2b.s
+++ /dev/null
@@ -1,40 +0,0 @@
-
-b2b.o:	file format elf64-bpf
-
-Disassembly of section .text:
-
-0000000000000000 <call1>:
-;     bpf_trace_printk("hello world", 2);
-       0:	18 01 00 00 00 00 00 00 00 00 00 00 00 00 00 00	r1 = 0x0 ll
-       2:	b7 02 00 00 02 00 00 00	r2 = 0x2
-       3:	85 00 00 00 06 00 00 00	call 0x6
-; }
-       4:	95 00 00 00 00 00 00 00	exit
-
-0000000000000028 <call2>:
-;     bpf_trace_printk("world", 6);
-       5:	18 01 00 00 0c 00 00 00 00 00 00 00 00 00 00 00	r1 = 0xc ll
-       7:	b7 02 00 00 06 00 00 00	r2 = 0x6
-       8:	85 00 00 00 06 00 00 00	call 0x6
-; }
-       9:	95 00 00 00 00 00 00 00	exit
-
-Disassembly of section xdp:
-
-0000000000000000 <prog>:
-; int prog(void *ctx) {
-       0:	b7 01 00 00 31 00 00 00	r1 = 0x31
-;     char s1[] = "1";
-       1:	6b 1a fe ff 00 00 00 00	*(u16 *)(r10 - 0x2) = r1
-       2:	bf a1 00 00 00 00 00 00	r1 = r10
-       3:	07 01 00 00 fe ff ff ff	r1 += -0x2
-;     bpf_trace_printk(s1, sizeof(s1));
-       4:	b7 02 00 00 02 00 00 00	r2 = 0x2
-       5:	85 00 00 00 06 00 00 00	call 0x6
-;     call1();
-       6:	85 10 00 00 ff ff ff ff	call -0x1
-;     call2();
-       7:	85 10 00 00 ff ff ff ff	call -0x1
-;     return 0;
-       8:	b7 00 00 00 00 00 00 00	r0 = 0x0
-       9:	95 00 00 00 00 00 00 00	exit
diff --git a/rejected/custom/complex.s b/rejected/custom/complex.s
deleted file mode 100644
index 7daf57ce..00000000
--- a/rejected/custom/complex.s
+++ /dev/null
@@ -1,116 +0,0 @@
-
-complex.o:	file format elf64-bpf
-
-Disassembly of section xdp:
-
-0000000000000000 <collect_ips_prog>:
-; int collect_ips_prog(struct xdp_md *ctx) {
-       0:	b7 05 00 00 00 00 00 00	r5 = 0x0
-;     char *data              = (char *)(long)ctx->data;
-       1:	61 12 00 00 00 00 00 00	r2 = *(u32 *)(r1 + 0x0)
-;     char *data_end          = (char *)(long)ctx->data_end;
-       2:	61 11 04 00 00 00 00 00	r1 = *(u32 *)(r1 + 0x4)
-       3:	b7 03 00 00 fa 01 00 00	r3 = 0x1fa
-
-0000000000000020 <LBB0_1>:
-       4:	bf 54 00 00 00 00 00 00	r4 = r5
-;         if (data_end < data + HEADER_LEN) {
-       5:	bf 25 00 00 00 00 00 00	r5 = r2
-       6:	07 05 00 00 06 00 00 00	r5 += 0x6
-       7:	2d 15 48 00 00 00 00 00	if r5 > r1 goto +0x48 <LBB0_13>
-;         if (data[0] == 'H' && data[1] == 'o' && data[2] == 's' && data[3] == 't' &&
-       8:	71 25 00 00 00 00 00 00	r5 = *(u8 *)(r2 + 0x0)
-       9:	55 05 0a 00 48 00 00 00	if r5 != 0x48 goto +0xa <LBB0_8>
-      10:	71 25 01 00 00 00 00 00	r5 = *(u8 *)(r2 + 0x1)
-      11:	55 05 08 00 6f 00 00 00	if r5 != 0x6f goto +0x8 <LBB0_8>
-      12:	71 25 02 00 00 00 00 00	r5 = *(u8 *)(r2 + 0x2)
-      13:	55 05 06 00 73 00 00 00	if r5 != 0x73 goto +0x6 <LBB0_8>
-      14:	71 25 03 00 00 00 00 00	r5 = *(u8 *)(r2 + 0x3)
-      15:	55 05 04 00 74 00 00 00	if r5 != 0x74 goto +0x4 <LBB0_8>
-;             data[4] == ':' && data[5] == ' ') {
-      16:	71 25 04 00 00 00 00 00	r5 = *(u8 *)(r2 + 0x4)
-      17:	55 05 02 00 3a 00 00 00	if r5 != 0x3a goto +0x2 <LBB0_8>
-      18:	71 25 05 00 00 00 00 00	r5 = *(u8 *)(r2 + 0x5)
-;         if (data[0] == 'H' && data[1] == 'o' && data[2] == 's' && data[3] == 't' &&
-      19:	15 05 06 00 20 00 00 00	if r5 == 0x20 goto +0x6 <LBB0_9>
-
-00000000000000a0 <LBB0_8>:
-;     for (__u16 i = 0; i <= 512 - HEADER_LEN; i++) {
-      20:	bf 45 00 00 00 00 00 00	r5 = r4
-      21:	07 05 00 00 01 00 00 00	r5 += 0x1
-;         data++;
-      22:	07 02 00 00 01 00 00 00	r2 += 0x1
-;     for (__u16 i = 0; i <= 512 - HEADER_LEN; i++) {
-      23:	57 04 00 00 ff ff 00 00	r4 &= 0xffff
-      24:	2d 43 eb ff 00 00 00 00	if r3 > r4 goto -0x15 <LBB0_1>
-      25:	05 00 36 00 00 00 00 00	goto +0x36 <LBB0_13>
-
-00000000000000d0 <LBB0_9>:
-      26:	b7 03 00 00 00 00 00 00	r3 = 0x0
-;         struct server_name sn = {"a", 0};
-      27:	6b 3a f8 ff 00 00 00 00	*(u16 *)(r10 - 0x8) = r3
-      28:	7b 3a f0 ff 00 00 00 00	*(u64 *)(r10 - 0x10) = r3
-      29:	7b 3a e8 ff 00 00 00 00	*(u64 *)(r10 - 0x18) = r3
-      30:	7b 3a e0 ff 00 00 00 00	*(u64 *)(r10 - 0x20) = r3
-      31:	7b 3a d8 ff 00 00 00 00	*(u64 *)(r10 - 0x28) = r3
-      32:	7b 3a d0 ff 00 00 00 00	*(u64 *)(r10 - 0x30) = r3
-      33:	7b 3a c8 ff 00 00 00 00	*(u64 *)(r10 - 0x38) = r3
-      34:	7b 3a c0 ff 00 00 00 00	*(u64 *)(r10 - 0x40) = r3
-      35:	7b 3a b8 ff 00 00 00 00	*(u64 *)(r10 - 0x48) = r3
-      36:	7b 3a b0 ff 00 00 00 00	*(u64 *)(r10 - 0x50) = r3
-      37:	7b 3a a8 ff 00 00 00 00	*(u64 *)(r10 - 0x58) = r3
-      38:	7b 3a a0 ff 00 00 00 00	*(u64 *)(r10 - 0x60) = r3
-      39:	7b 3a 98 ff 00 00 00 00	*(u64 *)(r10 - 0x68) = r3
-      40:	7b 3a 90 ff 00 00 00 00	*(u64 *)(r10 - 0x70) = r3
-      41:	7b 3a 88 ff 00 00 00 00	*(u64 *)(r10 - 0x78) = r3
-      42:	7b 3a 80 ff 00 00 00 00	*(u64 *)(r10 - 0x80) = r3
-      43:	7b 3a 78 ff 00 00 00 00	*(u64 *)(r10 - 0x88) = r3
-      44:	7b 3a 70 ff 00 00 00 00	*(u64 *)(r10 - 0x90) = r3
-      45:	7b 3a 68 ff 00 00 00 00	*(u64 *)(r10 - 0x98) = r3
-      46:	7b 3a 60 ff 00 00 00 00	*(u64 *)(r10 - 0xa0) = r3
-      47:	7b 3a 58 ff 00 00 00 00	*(u64 *)(r10 - 0xa8) = r3
-      48:	7b 3a 50 ff 00 00 00 00	*(u64 *)(r10 - 0xb0) = r3
-      49:	7b 3a 48 ff 00 00 00 00	*(u64 *)(r10 - 0xb8) = r3
-      50:	7b 3a 40 ff 00 00 00 00	*(u64 *)(r10 - 0xc0) = r3
-      51:	7b 3a 38 ff 00 00 00 00	*(u64 *)(r10 - 0xc8) = r3
-      52:	7b 3a 30 ff 00 00 00 00	*(u64 *)(r10 - 0xd0) = r3
-      53:	7b 3a 28 ff 00 00 00 00	*(u64 *)(r10 - 0xd8) = r3
-      54:	7b 3a 20 ff 00 00 00 00	*(u64 *)(r10 - 0xe0) = r3
-      55:	7b 3a 18 ff 00 00 00 00	*(u64 *)(r10 - 0xe8) = r3
-      56:	7b 3a 10 ff 00 00 00 00	*(u64 *)(r10 - 0xf0) = r3
-      57:	7b 3a 08 ff 00 00 00 00	*(u64 *)(r10 - 0xf8) = r3
-      58:	7b 3a 00 ff 00 00 00 00	*(u64 *)(r10 - 0x100) = r3
-      59:	7b 3a f8 fe 00 00 00 00	*(u64 *)(r10 - 0x108) = r3
-      60:	b7 04 00 00 61 00 00 00	r4 = 0x61
-      61:	73 4a f8 fe 00 00 00 00	*(u8 *)(r10 - 0x108) = r4
-      62:	bf 24 00 00 00 00 00 00	r4 = r2
-      63:	07 04 00 00 07 00 00 00	r4 += 0x7
-;         for (__u16 j = 0; j < MAX_SERVER_NAME_LENGTH; j++) {
-      64:	2d 14 0f 00 00 00 00 00	if r4 > r1 goto +0xf <LBB0_13>
-
-0000000000000208 <LBB0_10>:
-;             if (*data == '\r') {
-      65:	bf 24 00 00 00 00 00 00	r4 = r2
-      66:	0f 34 00 00 00 00 00 00	r4 += r3
-      67:	71 45 06 00 00 00 00 00	r5 = *(u8 *)(r4 + 0x6)
-      68:	15 05 0b 00 0d 00 00 00	if r5 == 0xd goto +0xb <LBB0_13>
-      69:	bf a0 00 00 00 00 00 00	r0 = r10
-      70:	07 00 00 00 f8 fe ff ff	r0 += -0x108
-;             sn.server_name[j] = *data++;
-      71:	0f 30 00 00 00 00 00 00	r0 += r3
-      72:	73 50 00 00 00 00 00 00	*(u8 *)(r0 + 0x0) = r5
-;             sn.length++;
-      73:	69 a5 f8 ff 00 00 00 00	r5 = *(u16 *)(r10 - 0x8)
-      74:	07 05 00 00 01 00 00 00	r5 += 0x1
-      75:	6b 5a f8 ff 00 00 00 00	*(u16 *)(r10 - 0x8) = r5
-;         for (__u16 j = 0; j < MAX_SERVER_NAME_LENGTH; j++) {
-      76:	25 03 03 00 fb 00 00 00	if r3 > 0xfb goto +0x3 <LBB0_13>
-      77:	07 03 00 00 01 00 00 00	r3 += 0x1
-      78:	07 04 00 00 08 00 00 00	r4 += 0x8
-;         for (__u16 j = 0; j < MAX_SERVER_NAME_LENGTH; j++) {
-      79:	3d 41 f1 ff 00 00 00 00	if r1 >= r4 goto -0xf <LBB0_10>
-
-0000000000000280 <LBB0_13>:
-; }
-      80:	b7 00 00 00 02 00 00 00	r0 = 0x2
-      81:	95 00 00 00 00 00 00 00	exit
diff --git a/rejected/custom/loop1.s b/rejected/custom/loop1.s
deleted file mode 100644
index 45da2c3e..00000000
--- a/rejected/custom/loop1.s
+++ /dev/null
@@ -1,26 +0,0 @@
-
-loop1.o:	file format elf64-bpf
-
-Disassembly of section xdp:
-
-0000000000000000 <prog>:
-;     __u64 t = bpf_ktime_get_ns();
-       0:	85 00 00 00 05 00 00 00	call 0x5
-       1:	bf 06 00 00 00 00 00 00	r6 = r0
-;     for (int i = 0; i < t; ++i) {
-       2:	15 06 07 00 00 00 00 00	if r6 == 0x0 goto +0x7 <LBB0_3>
-       3:	b7 07 00 00 00 00 00 00	r7 = 0x0
-
-0000000000000020 <LBB0_2>:
-;         bpf_trace_printk("s", 1);
-       4:	18 01 00 00 00 00 00 00 00 00 00 00 00 00 00 00	r1 = 0x0 ll
-       6:	b7 02 00 00 01 00 00 00	r2 = 0x1
-       7:	85 00 00 00 06 00 00 00	call 0x6
-;     for (int i = 0; i < t; ++i) {
-       8:	07 07 00 00 01 00 00 00	r7 += 0x1
-       9:	2d 76 fa ff 00 00 00 00	if r6 > r7 goto -0x6 <LBB0_2>
-
-0000000000000050 <LBB0_3>:
-;     return 0;
-      10:	b7 00 00 00 00 00 00 00	r0 = 0x0
-      11:	95 00 00 00 00 00 00 00	exit
diff --git a/rejected/custom/test_asm.s b/rejected/custom/test_asm.s
deleted file mode 100644
index b93a9c23..00000000
--- a/rejected/custom/test_asm.s
+++ /dev/null
@@ -1,150 +0,0 @@
-
-test_asm.o:	file format elf64-bpf
-
-Disassembly of section .text:
-
-0000000000000000 <spill>:
-; int __noinline spill(int cr, int ci) {
-       0:	7b 2a f8 ff 00 00 00 00	*(u64 *)(r10 - 0x8) = r2
-       1:	b7 03 00 00 00 00 00 00	r3 = 0x0
-       2:	b7 05 00 00 00 00 00 00	r5 = 0x0
-       3:	b7 02 00 00 00 00 00 00	r2 = 0x0
-       4:	b7 06 00 00 00 00 00 00	r6 = 0x0
-;     while (i < 100 && zr * zr + zi * zi + zk * zk - zl * zl * (zi - 1) < 4) {
-       5:	bf 64 00 00 00 00 00 00	r4 = r6
-
-0000000000000030 <LBB0_1>:
-       6:	b7 00 00 00 01 00 00 00	r0 = 0x1
-       7:	1f 20 00 00 00 00 00 00	r0 -= r2
-       8:	2f 30 00 00 00 00 00 00	r0 *= r3
-       9:	2f 30 00 00 00 00 00 00	r0 *= r3
-      10:	bf 59 00 00 00 00 00 00	r9 = r5
-      11:	2f 99 00 00 00 00 00 00	r9 *= r9
-      12:	2f 44 00 00 00 00 00 00	r4 *= r4
-      13:	bf 27 00 00 00 00 00 00	r7 = r2
-      14:	2f 77 00 00 00 00 00 00	r7 *= r7
-      15:	bf 78 00 00 00 00 00 00	r8 = r7
-      16:	0f 48 00 00 00 00 00 00	r8 += r4
-      17:	0f 98 00 00 00 00 00 00	r8 += r9
-      18:	0f 08 00 00 00 00 00 00	r8 += r0
-      19:	67 08 00 00 20 00 00 00	r8 <<= 0x20
-      20:	c7 08 00 00 20 00 00 00	r8 s>>= 0x20
-      21:	bf 30 00 00 00 00 00 00	r0 = r3
-      22:	65 08 14 00 03 00 00 00	if r8 s> 0x3 goto +0x14 <LBB0_3>
-;         zi    = 2 * zr * zi + ci;
-      23:	2f 26 00 00 00 00 00 00	r6 *= r2
-      24:	67 06 00 00 01 00 00 00	r6 <<= 0x1
-      25:	79 a2 f8 ff 00 00 00 00	r2 = *(u64 *)(r10 - 0x8)
-      26:	0f 26 00 00 00 00 00 00	r6 += r2
-;         zk    = 3 * zr - zi * zi * zk * zr;
-      27:	bf 62 00 00 00 00 00 00	r2 = r6
-      28:	2f 52 00 00 00 00 00 00	r2 *= r5
-      29:	2f 62 00 00 00 00 00 00	r2 *= r6
-      30:	b7 05 00 00 03 00 00 00	r5 = 0x3
-      31:	1f 25 00 00 00 00 00 00	r5 -= r2
-;         int t = zr * zr - zi * zi + cr;
-      32:	1f 74 00 00 00 00 00 00	r4 -= r7
-      33:	0f 14 00 00 00 00 00 00	r4 += r1
-      34:	b7 00 00 00 64 00 00 00	r0 = 0x64
-;         zk    = 3 * zr - zi * zi * zk * zr;
-      35:	2f 45 00 00 00 00 00 00	r5 *= r4
-;         i = i + 1;
-      36:	07 03 00 00 01 00 00 00	r3 += 0x1
-      37:	bf 37 00 00 00 00 00 00	r7 = r3
-      38:	67 07 00 00 20 00 00 00	r7 <<= 0x20
-      39:	77 07 00 00 20 00 00 00	r7 >>= 0x20
-      40:	bf 62 00 00 00 00 00 00	r2 = r6
-      41:	bf 46 00 00 00 00 00 00	r6 = r4
-;     while (i < 100 && zr * zr + zi * zi + zk * zk - zl * zl * (zi - 1) < 4) {
-      42:	55 07 db ff 64 00 00 00	if r7 != 0x64 goto -0x25 <LBB0_1>
-
-0000000000000158 <LBB0_3>:
-;     return i;
-      43:	95 00 00 00 00 00 00 00	exit
-
-0000000000000160 <pk>:
-; void __noinline pk(char s) {
-      44:	bf 13 00 00 00 00 00 00	r3 = r1
-;     bpf_trace_printk("%c", 1, s);
-      45:	18 01 00 00 00 00 00 00 00 00 00 00 00 00 00 00	r1 = 0x0 ll
-      47:	b7 02 00 00 01 00 00 00	r2 = 0x1
-      48:	85 00 00 00 06 00 00 00	call 0x6
-; }
-      49:	95 00 00 00 00 00 00 00	exit
-
-0000000000000190 <pk_l>:
-; void __noinline pk_l(char *s) {
-      50:	bf 13 00 00 00 00 00 00	r3 = r1
-;     bpf_trace_printk("%s", 1, s);
-      51:	18 01 00 00 03 00 00 00 00 00 00 00 00 00 00 00	r1 = 0x3 ll
-      53:	b7 02 00 00 01 00 00 00	r2 = 0x1
-      54:	85 00 00 00 06 00 00 00	call 0x6
-; }
-      55:	95 00 00 00 00 00 00 00	exit
-
-Disassembly of section xdp:
-
-0000000000000000 <prog>:
-;     int s = spill(1, 2);
-       0:	b7 01 00 00 01 00 00 00	r1 = 0x1
-       1:	b7 02 00 00 02 00 00 00	r2 = 0x2
-       2:	85 10 00 00 ff ff ff ff	call -0x1
-       3:	bf 06 00 00 00 00 00 00	r6 = r0
-;         pk(res[i]);
-       4:	18 07 00 00 0a 00 00 00 00 00 00 00 00 00 00 00	r7 = 0xa ll
-       6:	71 71 00 00 00 00 00 00	r1 = *(u8 *)(r7 + 0x0)
-       7:	67 01 00 00 38 00 00 00	r1 <<= 0x38
-       8:	c7 01 00 00 38 00 00 00	r1 s>>= 0x38
-       9:	85 10 00 00 ff ff ff ff	call -0x1
-      10:	71 71 01 00 00 00 00 00	r1 = *(u8 *)(r7 + 0x1)
-      11:	67 01 00 00 38 00 00 00	r1 <<= 0x38
-      12:	c7 01 00 00 38 00 00 00	r1 s>>= 0x38
-      13:	85 10 00 00 ff ff ff ff	call -0x1
-      14:	71 71 02 00 00 00 00 00	r1 = *(u8 *)(r7 + 0x2)
-      15:	67 01 00 00 38 00 00 00	r1 <<= 0x38
-      16:	c7 01 00 00 38 00 00 00	r1 s>>= 0x38
-      17:	85 10 00 00 ff ff ff ff	call -0x1
-      18:	71 71 03 00 00 00 00 00	r1 = *(u8 *)(r7 + 0x3)
-      19:	67 01 00 00 38 00 00 00	r1 <<= 0x38
-      20:	c7 01 00 00 38 00 00 00	r1 s>>= 0x38
-      21:	85 10 00 00 ff ff ff ff	call -0x1
-      22:	71 71 04 00 00 00 00 00	r1 = *(u8 *)(r7 + 0x4)
-      23:	67 01 00 00 38 00 00 00	r1 <<= 0x38
-      24:	c7 01 00 00 38 00 00 00	r1 s>>= 0x38
-      25:	85 10 00 00 ff ff ff ff	call -0x1
-      26:	71 71 05 00 00 00 00 00	r1 = *(u8 *)(r7 + 0x5)
-      27:	67 01 00 00 38 00 00 00	r1 <<= 0x38
-      28:	c7 01 00 00 38 00 00 00	r1 s>>= 0x38
-      29:	85 10 00 00 ff ff ff ff	call -0x1
-      30:	71 71 06 00 00 00 00 00	r1 = *(u8 *)(r7 + 0x6)
-      31:	67 01 00 00 38 00 00 00	r1 <<= 0x38
-      32:	c7 01 00 00 38 00 00 00	r1 s>>= 0x38
-      33:	85 10 00 00 ff ff ff ff	call -0x1
-      34:	71 71 07 00 00 00 00 00	r1 = *(u8 *)(r7 + 0x7)
-      35:	67 01 00 00 38 00 00 00	r1 <<= 0x38
-      36:	c7 01 00 00 38 00 00 00	r1 s>>= 0x38
-      37:	85 10 00 00 ff ff ff ff	call -0x1
-      38:	71 71 08 00 00 00 00 00	r1 = *(u8 *)(r7 + 0x8)
-      39:	67 01 00 00 38 00 00 00	r1 <<= 0x38
-      40:	c7 01 00 00 38 00 00 00	r1 s>>= 0x38
-      41:	85 10 00 00 ff ff ff ff	call -0x1
-      42:	71 71 09 00 00 00 00 00	r1 = *(u8 *)(r7 + 0x9)
-      43:	67 01 00 00 38 00 00 00	r1 <<= 0x38
-      44:	c7 01 00 00 38 00 00 00	r1 s>>= 0x38
-      45:	85 10 00 00 ff ff ff ff	call -0x1
-;     pk_l(res);
-      46:	18 01 00 00 0a 00 00 00 00 00 00 00 00 00 00 00	r1 = 0xa ll
-      48:	85 10 00 00 ff ff ff ff	call -0x1
-;     pk_l(ores);
-      49:	18 01 00 00 00 00 00 00 00 00 00 00 00 00 00 00	r1 = 0x0 ll
-      51:	85 10 00 00 ff ff ff ff	call -0x1
-;     pk(res[0]);
-      52:	71 71 00 00 00 00 00 00	r1 = *(u8 *)(r7 + 0x0)
-      53:	67 01 00 00 38 00 00 00	r1 <<= 0x38
-      54:	c7 01 00 00 38 00 00 00	r1 s>>= 0x38
-      55:	85 10 00 00 ff ff ff ff	call -0x1
-;     res[0] = s;
-      56:	73 67 00 00 00 00 00 00	*(u8 *)(r7 + 0x0) = r6
-;     return 0;
-      57:	b7 00 00 00 00 00 00 00	r0 = 0x0
-      58:	95 00 00 00 00 00 00 00	exit

From e1de487e916c929e90d72deedb0b5f268af3c389 Mon Sep 17 00:00:00 2001
From: linsyking <kxiang@umich.edu>
Date: Mon, 15 Jul 2024 17:40:41 -0400
Subject: [PATCH 03/24] feat: test check

---
 IR/tests/Makefile | 10 +++++-----
 IR/tests/mem1.c   | 24 ++++++++++++++++++++++++
 IR/tests/mem2.c   | 37 +++++++++++++++++++++++++++++++++++++
 3 files changed, 66 insertions(+), 5 deletions(-)
 create mode 100644 IR/tests/mem1.c
 create mode 100644 IR/tests/mem2.c

diff --git a/IR/tests/Makefile b/IR/tests/Makefile
index 7a2968ee..2a4654df 100644
--- a/IR/tests/Makefile
+++ b/IR/tests/Makefile
@@ -5,12 +5,12 @@ $(NAME).s: $(NAME).o
 	# clang -O2 -I/usr/include/$(shell uname -m)-linux-gnu -target bpf -S -o $(NAME).s $(NAME).c
 	llvm-objdump -S $< > $@
 
-sobj: $(NAME).S
-	llvm-mc -triple bpf -filetype=obj -o $(NAME).o $(NAME).S
+sobj: $(NAME).s
+	llvm-mc -triple bpf -filetype=obj -o $(NAME).o $(NAME).s
 
-load:
+load: clean $(NAME).o
 	sudo bpftool prog load $(NAME).o /sys/fs/bpf/$(NAME)
 
 clean:
-	rm -f $(NAME).o $(NAME).S
-	sudo rm /sys/fs/bpf/$(NAME)
+	rm -f $(NAME).o $(NAME).s
+	-sudo rm /sys/fs/bpf/$(NAME)
diff --git a/IR/tests/mem1.c b/IR/tests/mem1.c
new file mode 100644
index 00000000..d090449f
--- /dev/null
+++ b/IR/tests/mem1.c
@@ -0,0 +1,24 @@
+#include <linux/bpf.h>
+#include <bpf/bpf_helpers.h>
+
+/**
+    Invalid memory access
+
+    Err: math between fp pointer and register with unbounded min value is not allowed
+ */
+
+SEC("xdp")
+int prog(void *ctx) {
+    int id = bpf_ktime_get_ns() % 10;
+    int arr[10] = {};
+    for (int i = 0; i < 10; ++i) {
+        arr[i] = i;
+    }
+    if (id > 10 || id < 0) {
+        return 0;
+    }
+    bpf_trace_printk("%d", 1, arr[id]);
+    return 0;
+}
+
+char _license[] SEC("license") = "GPL";
diff --git a/IR/tests/mem2.c b/IR/tests/mem2.c
new file mode 100644
index 00000000..7ec8d47c
--- /dev/null
+++ b/IR/tests/mem2.c
@@ -0,0 +1,37 @@
+#include <linux/bpf.h>
+#include <bpf/bpf_helpers.h>
+
+int __noinline call(__u64 i) {
+    if (i > 100) {
+        return -1;
+    }
+    bpf_trace_printk("i: %d\n", 4, i);
+    return 0;
+}
+
+/**
+    Invalid memory access
+
+    Err: invalid unbounded variable-offset write to stack R2
+ */
+
+SEC("xdp")
+int prog(struct xdp_md *ctx) {
+    __u64 arr[10] = {};
+    for (__u32 i = 0; i < 10; ++i) {
+        arr[i] = i;
+    }
+    call(arr[9]);  // Pass
+    // call(arr[10]);  // Not Pass
+    // call(arr[11]);  // Not Pass
+    int id = bpf_ktime_get_ns() % 20;
+    if (id > 9 || id < 0) { // Work
+        goto end;
+    }
+    __u64 res = arr[id];
+    call(res);  // Not Pass
+end:
+    return XDP_DROP;
+}
+
+char _license[] SEC("license") = "GPL";

From b0a991217c0bcb875f74ce0526430de43ececf39 Mon Sep 17 00:00:00 2001
From: linsyking <kxiang@umich.edu>
Date: Mon, 15 Jul 2024 17:41:00 -0400
Subject: [PATCH 04/24] chore: comment

---
 IR/tests/mem2.c | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/IR/tests/mem2.c b/IR/tests/mem2.c
index 7ec8d47c..130fe6b3 100644
--- a/IR/tests/mem2.c
+++ b/IR/tests/mem2.c
@@ -29,7 +29,7 @@ int prog(struct xdp_md *ctx) {
         goto end;
     }
     __u64 res = arr[id];
-    call(res);  // Not Pass
+    call(res);
 end:
     return XDP_DROP;
 }

From abd295df4f887e49fe01dedce5c263ccf9adaf03 Mon Sep 17 00:00:00 2001
From: linsyking <kxiang@umich.edu>
Date: Mon, 15 Jul 2024 17:42:16 -0400
Subject: [PATCH 05/24] fix: pos

---
 IR/tests/mem2.c | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/IR/tests/mem2.c b/IR/tests/mem2.c
index 130fe6b3..cd9f5649 100644
--- a/IR/tests/mem2.c
+++ b/IR/tests/mem2.c
@@ -17,6 +17,7 @@ int __noinline call(__u64 i) {
 
 SEC("xdp")
 int prog(struct xdp_md *ctx) {
+    int id = bpf_ktime_get_ns() % 20;
     __u64 arr[10] = {};
     for (__u32 i = 0; i < 10; ++i) {
         arr[i] = i;
@@ -24,7 +25,6 @@ int prog(struct xdp_md *ctx) {
     call(arr[9]);  // Pass
     // call(arr[10]);  // Not Pass
     // call(arr[11]);  // Not Pass
-    int id = bpf_ktime_get_ns() % 20;
     if (id > 9 || id < 0) { // Work
         goto end;
     }

From 94b40e2f018b809e91152912018324f09d7bae9d Mon Sep 17 00:00:00 2001
From: linsyking <kxiang@umich.edu>
Date: Mon, 15 Jul 2024 17:50:38 -0400
Subject: [PATCH 06/24] feat: test programs

---
 IR/tests/mem2.c | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/IR/tests/mem2.c b/IR/tests/mem2.c
index cd9f5649..7ddbab01 100644
--- a/IR/tests/mem2.c
+++ b/IR/tests/mem2.c
@@ -30,6 +30,10 @@ int prog(struct xdp_md *ctx) {
     }
     __u64 res = arr[id];
     call(res);
+    #pragma nounroll
+    for (__u32 i = 0; i < 10; ++i) {
+        call(arr[i]);
+    }
 end:
     return XDP_DROP;
 }

From d4abb3d08712645375caad71a106e9b3fb9f0f41 Mon Sep 17 00:00:00 2001
From: linsyking <kxiang@umich.edu>
Date: Mon, 15 Jul 2024 17:52:05 -0400
Subject: [PATCH 07/24] chore: add comment about error

---
 IR/tests/mem2.c | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/IR/tests/mem2.c b/IR/tests/mem2.c
index 7ddbab01..0e6c4735 100644
--- a/IR/tests/mem2.c
+++ b/IR/tests/mem2.c
@@ -17,7 +17,7 @@ int __noinline call(__u64 i) {
 
 SEC("xdp")
 int prog(struct xdp_md *ctx) {
-    int id = bpf_ktime_get_ns() % 20;
+    int id = bpf_ktime_get_ns() % 20;   // We cannot use 10 here
     __u64 arr[10] = {};
     for (__u32 i = 0; i < 10; ++i) {
         arr[i] = i;

From e41ee8ca8e632f6b2f11eac69798d6e5fe543b7e Mon Sep 17 00:00:00 2001
From: linsyking <kxiang@umich.edu>
Date: Mon, 15 Jul 2024 17:54:12 -0400
Subject: [PATCH 08/24] fix: test

---
 IR/tests/mem2.c | 1 +
 1 file changed, 1 insertion(+)

diff --git a/IR/tests/mem2.c b/IR/tests/mem2.c
index 0e6c4735..d21be52d 100644
--- a/IR/tests/mem2.c
+++ b/IR/tests/mem2.c
@@ -33,6 +33,7 @@ int prog(struct xdp_md *ctx) {
     #pragma nounroll
     for (__u32 i = 0; i < 10; ++i) {
         call(arr[i]);
+        arr[i] = i + 1;
     }
 end:
     return XDP_DROP;

From 9ee774dd9c256f7287fc9b4bdbc9bb7155c54478 Mon Sep 17 00:00:00 2001
From: linsyking <kxiang@umich.edu>
Date: Tue, 16 Jul 2024 16:46:52 -0400
Subject: [PATCH 09/24] feat: add nop

---
 IR/tests/Makefile   |  6 ++++++
 IR/tests/mem1.c     |  2 +-
 IR/tests/mem3_nop.c | 26 ++++++++++++++++++++++++++
 3 files changed, 33 insertions(+), 1 deletion(-)
 create mode 100644 IR/tests/mem3_nop.c

diff --git a/IR/tests/Makefile b/IR/tests/Makefile
index 2a4654df..4952306c 100644
--- a/IR/tests/Makefile
+++ b/IR/tests/Makefile
@@ -1,6 +1,9 @@
 $(NAME).o: $(NAME).c
 	clang -O2 -I/usr/include/$(shell uname -m)-linux-gnu -g -target bpf -c $< -o $@
 
+$(NAME).nop.o: $(NAME).c
+	clang -O0 -I/usr/include/$(shell uname -m)-linux-gnu -g -target bpf -c $< -o $@
+
 $(NAME).s: $(NAME).o
 	# clang -O2 -I/usr/include/$(shell uname -m)-linux-gnu -target bpf -S -o $(NAME).s $(NAME).c
 	llvm-objdump -S $< > $@
@@ -11,6 +14,9 @@ sobj: $(NAME).s
 load: clean $(NAME).o
 	sudo bpftool prog load $(NAME).o /sys/fs/bpf/$(NAME)
 
+loadnop: clean $(NAME).nop.o
+	sudo bpftool prog load $(NAME).nop.o /sys/fs/bpf/$(NAME)
+
 clean:
 	rm -f $(NAME).o $(NAME).s
 	-sudo rm /sys/fs/bpf/$(NAME)
diff --git a/IR/tests/mem1.c b/IR/tests/mem1.c
index d090449f..2ab003eb 100644
--- a/IR/tests/mem1.c
+++ b/IR/tests/mem1.c
@@ -9,7 +9,7 @@
 
 SEC("xdp")
 int prog(void *ctx) {
-    int id = bpf_ktime_get_ns() % 10;
+    int id = bpf_ktime_get_ns() % 20;
     int arr[10] = {};
     for (int i = 0; i < 10; ++i) {
         arr[i] = i;
diff --git a/IR/tests/mem3_nop.c b/IR/tests/mem3_nop.c
new file mode 100644
index 00000000..4bf4f66d
--- /dev/null
+++ b/IR/tests/mem3_nop.c
@@ -0,0 +1,26 @@
+#include <linux/bpf.h>
+#include <bpf/bpf_helpers.h>
+
+int __noinline call(__u64 i) {
+    if (i > 100) {
+        return -1;
+    }
+    bpf_trace_printk("i: %d\n", 4, i);
+    return 0;
+}
+
+/**
+    Invalid memory access
+
+    Err: invalid read from stack R10 off=72 size=8
+ */
+
+SEC("xdp")
+int prog(struct xdp_md *ctx) {
+    __u64 arr[10] = {};
+    call(arr[20]);  // Not Pass
+    call(arr[11]);  // Not Pass
+    return XDP_DROP;
+}
+
+char _license[] SEC("license") = "GPL";

From 1fdb4f7b1b353024e0a27e7f52cc04739768d5f0 Mon Sep 17 00:00:00 2001
From: linsyking <kxiang@umich.edu>
Date: Tue, 16 Jul 2024 21:19:15 -0400
Subject: [PATCH 10/24] refactor: bpf_ret 0

---
 IR/bpf_ir.c | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

diff --git a/IR/bpf_ir.c b/IR/bpf_ir.c
index a8751fdd..9d3b6d78 100644
--- a/IR/bpf_ir.c
+++ b/IR/bpf_ir.c
@@ -5,6 +5,7 @@
 #include <stdlib.h>
 #include <stddef.h>
 #include "array.h"
+#include "ir_insn.h"
 #include "list.h"
 #include "dbg.h"
 #include "passes.h"
@@ -649,10 +650,7 @@ void transform_bb(struct ssa_transform_env *env, struct pre_ir_basic_block *bb)
                 new_insn->bb1            = get_ir_bb_from_position(env, pos);
             } else if (BPF_OP(code) == BPF_EXIT) {
                 // Exit
-                struct ir_insn *new_insn = create_insn_back(bb->ir_bb);
-                new_insn->op             = IR_INSN_RET;
-                new_insn->values[0]      = read_variable(env, BPF_REG_0, bb);
-                new_insn->value_num      = 1;
+                create_ret_insn_bb(bb->ir_bb, read_variable(env, BPF_REG_0, bb), INSERT_BACK);
             } else if (BPF_OP(code) == BPF_JEQ) {
                 // PC += offset if dst == src
                 struct ir_insn *new_insn = create_insn_back(bb->ir_bb);

From 880bfe42d97a4df91e6f372789edb729e85484a8 Mon Sep 17 00:00:00 2001
From: linsyking <kxiang@umich.edu>
Date: Tue, 16 Jul 2024 22:07:29 -0400
Subject: [PATCH 11/24] feat: add stack offset

---
 IR/add_stack_offset.c         | 48 +++++++++++++++++++++++++++++++++++
 IR/include/add_stack_offset.h |  9 +++++++
 IR/tests/Makefile             |  4 ++-
 IR/tests/alu64.c              | 15 +++++++++++
 4 files changed, 75 insertions(+), 1 deletion(-)
 create mode 100644 IR/add_stack_offset.c
 create mode 100644 IR/include/add_stack_offset.h
 create mode 100644 IR/tests/alu64.c

diff --git a/IR/add_stack_offset.c b/IR/add_stack_offset.c
new file mode 100644
index 00000000..b51f6c6f
--- /dev/null
+++ b/IR/add_stack_offset.c
@@ -0,0 +1,48 @@
+#include "add_stack_offset.h"
+#include "array.h"
+#include "bpf_ir.h"
+#include "ir_insn.h"
+
+void add_stack_offset(struct ir_function *fun, __s16 offset) {
+    struct array     users = fun->sp_users;
+    struct ir_insn **pos;
+    array_for(pos, users) {
+        struct ir_insn *insn = *pos;
+
+        if (insn->op == IR_INSN_LOADRAW || insn->op == IR_INSN_STORERAW) {
+            insn->addr_val.offset += offset;
+        }
+
+        for (__u8 j = 0; j < insn->value_num; ++j) {
+            if (insn->values[j].type == IR_VALUE_STACK_PTR) {
+                // Stack pointer as value
+                struct ir_value val;
+                val.type                       = IR_VALUE_CONSTANT;
+                val.data.constant_d.type       = IR_CONSTANT_S16;
+                val.data.constant_d.data.s16_d = offset;
+                struct ir_insn *new_insn =
+                    create_add_insn(insn, insn->values[j], val, INSERT_FRONT);
+                val.type        = IR_VALUE_INSN;
+                val.data.insn_d = new_insn;
+                insn->values[j] = val;
+            }
+        }
+        if (insn->op == IR_INSN_PHI) {
+            struct phi_value *pv_pos2;
+            array_for(pv_pos2, insn->phi) {
+                if (pv_pos2->value.type == IR_VALUE_STACK_PTR) {
+                    // Stack pointer as value
+                    struct ir_value val;
+                    val.type                       = IR_VALUE_CONSTANT;
+                    val.data.constant_d.type       = IR_CONSTANT_S16;
+                    val.data.constant_d.data.s16_d = offset;
+                    struct ir_insn *new_insn =
+                        create_add_insn(insn, pv_pos2->value, val, INSERT_FRONT);
+                    val.type        = IR_VALUE_INSN;
+                    val.data.insn_d = new_insn;
+                    pv_pos2->value = val;
+                }
+            }
+        }
+    }
+}
diff --git a/IR/include/add_stack_offset.h b/IR/include/add_stack_offset.h
new file mode 100644
index 00000000..b4b6c938
--- /dev/null
+++ b/IR/include/add_stack_offset.h
@@ -0,0 +1,9 @@
+#ifndef __BPF_IR_ADD_STACK_OFFSET_H__
+#define __BPF_IR_ADD_STACK_OFFSET_H__
+
+#include "bpf_ir.h"
+
+// Add stack offset to all stack access
+void add_stack_offset(struct ir_function *fun, __s16 offset);
+
+#endif
diff --git a/IR/tests/Makefile b/IR/tests/Makefile
index 4952306c..deb52e02 100644
--- a/IR/tests/Makefile
+++ b/IR/tests/Makefile
@@ -4,8 +4,10 @@ $(NAME).o: $(NAME).c
 $(NAME).nop.o: $(NAME).c
 	clang -O0 -I/usr/include/$(shell uname -m)-linux-gnu -g -target bpf -c $< -o $@
 
+$(NAME).nop.s: $(NAME).nop.o
+	llvm-objdump -S $< > $@
+
 $(NAME).s: $(NAME).o
-	# clang -O2 -I/usr/include/$(shell uname -m)-linux-gnu -target bpf -S -o $(NAME).s $(NAME).c
 	llvm-objdump -S $< > $@
 
 sobj: $(NAME).s
diff --git a/IR/tests/alu64.c b/IR/tests/alu64.c
new file mode 100644
index 00000000..465701f9
--- /dev/null
+++ b/IR/tests/alu64.c
@@ -0,0 +1,15 @@
+#include <linux/bpf.h>
+#include <bpf/bpf_helpers.h>
+
+
+SEC("xdp")
+int prog(void *ctx) {
+    // char s1[] = "hello world my friend";
+    // bpf_trace_printk(s1, sizeof(s1));
+    __u64 i1 = 0x3456789abcdef0;
+    __u64 i2 = 0x76543210fedcba;
+    __u64 ans = i1+i2;
+    return 0;
+}
+
+char _license[] SEC("license") = "GPL";

From 7b5f6a5209d2747b6be29e39df9e80d2085d5b92 Mon Sep 17 00:00:00 2001
From: linsyking <kxiang@umich.edu>
Date: Tue, 16 Jul 2024 22:24:44 -0400
Subject: [PATCH 12/24] fix: alu 64

---
 IR/add_stack_offset.c |  1 +
 IR/array.c            |  1 +
 IR/bpf_ir.c           | 11 ++++++-----
 IR/ir_helper.c        | 12 ++++++------
 IR/tests/alu64.c      |  4 ++++
 5 files changed, 18 insertions(+), 11 deletions(-)

diff --git a/IR/add_stack_offset.c b/IR/add_stack_offset.c
index b51f6c6f..433f357d 100644
--- a/IR/add_stack_offset.c
+++ b/IR/add_stack_offset.c
@@ -45,4 +45,5 @@ void add_stack_offset(struct ir_function *fun, __s16 offset) {
             }
         }
     }
+    array_free(&fun->sp_users);
 }
diff --git a/IR/array.c b/IR/array.c
index 6b6bf574..5997589d 100644
--- a/IR/array.c
+++ b/IR/array.c
@@ -67,4 +67,5 @@ void array_erase(struct array *arr, size_t idx) {
 
 void array_free(struct array *arr) {
     __free(arr->data);
+    *arr = array_null();
 }
diff --git a/IR/bpf_ir.c b/IR/bpf_ir.c
index 9d3b6d78..cf888d19 100644
--- a/IR/bpf_ir.c
+++ b/IR/bpf_ir.c
@@ -193,7 +193,8 @@ struct bb_info gen_bb(struct bpf_insn *insns, size_t len) {
             new_insn.off     = insn.off;
             new_insn.pos     = pos;
             if (pos + 1 < real_bb->end_pos && insns[pos + 1].code == 0) {
-                new_insn.imm64 = ((__s64)(insns[pos + 1].imm) << 32) | insn.imm;
+                __u64 imml = (__u64)insn.imm & 0xFFFFFFFF;
+                new_insn.imm64 = ((__s64)(insns[pos + 1].imm) << 32) | imml;
                 pos++;
             }
             real_bb->pre_insns[bb_pos] = new_insn;
@@ -561,11 +562,11 @@ void transform_bb(struct ssa_transform_env *env, struct pre_ir_basic_block *bb)
                 struct ir_insn *new_insn = create_insn_back(bb->ir_bb);
                 new_insn->op             = IR_INSN_LOADRAW;
                 struct ir_address_value addr_val;
-                struct ir_value imm_ptr;
-                imm_ptr.type = IR_VALUE_CONSTANT;
-                imm_ptr.data.constant_d.type = IR_CONSTANT_U64;
+                struct ir_value         imm_ptr;
+                imm_ptr.type                       = IR_VALUE_CONSTANT;
+                imm_ptr.data.constant_d.type       = IR_CONSTANT_U64;
                 imm_ptr.data.constant_d.data.u64_d = insn.imm64;
-                addr_val.value = imm_ptr;
+                addr_val.value                     = imm_ptr;
                 add_user(env, new_insn, addr_val.value);
                 addr_val.offset    = 0;
                 new_insn->vr_type  = IR_VR_TYPE_U64;
diff --git a/IR/ir_helper.c b/IR/ir_helper.c
index 1fd6c962..db97acc7 100644
--- a/IR/ir_helper.c
+++ b/IR/ir_helper.c
@@ -36,22 +36,22 @@ void clean_id(struct ir_function *fun) {
 void print_constant(struct ir_constant d) {
     switch (d.type) {
         case IR_CONSTANT_S32:
-            printf("%d", d.data.s32_d);
+            printf("%x", d.data.s32_d);
             break;
         case IR_CONSTANT_U32:
-            printf("%u", d.data.u32_d);
+            printf("%x", d.data.u32_d);
             break;
         case IR_CONSTANT_U64:
-            printf("%llu", d.data.u64_d);
+            printf("%llx", d.data.u64_d);
             break;
         case IR_CONSTANT_S64:
-            printf("%lld", d.data.s64_d);
+            printf("%llx", d.data.s64_d);
             break;
         case IR_CONSTANT_S16:
-            printf("%d", d.data.s16_d);
+            printf("%x", d.data.s16_d);
             break;
         case IR_CONSTANT_U16:
-            printf("%u", d.data.u16_d);
+            printf("%x", d.data.u16_d);
             break;
         default:
             CRITICAL("Unknown constant type");
diff --git a/IR/tests/alu64.c b/IR/tests/alu64.c
index 465701f9..2ffd4791 100644
--- a/IR/tests/alu64.c
+++ b/IR/tests/alu64.c
@@ -9,6 +9,10 @@ int prog(void *ctx) {
     __u64 i1 = 0x3456789abcdef0;
     __u64 i2 = 0x76543210fedcba;
     __u64 ans = i1+i2;
+    // char s[10] = {};
+
+    // int i = 2;
+    // s[i]++;
     return 0;
 }
 

From 250e489cd30f64b87f032f41dbe9e3fe35a2c0ae Mon Sep 17 00:00:00 2001
From: linsyking <kxiang@umich.edu>
Date: Tue, 16 Jul 2024 22:32:06 -0400
Subject: [PATCH 13/24] feat: add LSH instruction

---
 IR/bpf_ir.c         | 18 ++++++++++++++++--
 IR/include/bpf_ir.h |  2 ++
 IR/ir_helper.c      | 18 ++++++++++++------
 3 files changed, 30 insertions(+), 8 deletions(-)

diff --git a/IR/bpf_ir.c b/IR/bpf_ir.c
index cf888d19..e5b62710 100644
--- a/IR/bpf_ir.c
+++ b/IR/bpf_ir.c
@@ -193,7 +193,7 @@ struct bb_info gen_bb(struct bpf_insn *insns, size_t len) {
             new_insn.off     = insn.off;
             new_insn.pos     = pos;
             if (pos + 1 < real_bb->end_pos && insns[pos + 1].code == 0) {
-                __u64 imml = (__u64)insn.imm & 0xFFFFFFFF;
+                __u64 imml     = (__u64)insn.imm & 0xFFFFFFFF;
                 new_insn.imm64 = ((__s64)(insns[pos + 1].imm) << 32) | imml;
                 pos++;
             }
@@ -549,7 +549,21 @@ void transform_bb(struct ssa_transform_env *env, struct pre_ir_basic_block *bb)
             } else if (BPF_OP(code) == BPF_MOV) {
                 // Do not create instructions
                 write_variable(env, insn.dst_reg, bb, get_src_value(env, bb, insn));
-            } else {
+            } else if (BPF_OP(code) == BPF_LSH) {
+                struct ir_insn *new_insn = create_insn_back(bb->ir_bb);
+                new_insn->op             = IR_INSN_LSH;
+                new_insn->values[0]      = read_variable(env, insn.dst_reg, bb);
+                new_insn->values[1]      = get_src_value(env, bb, insn);
+                new_insn->value_num      = 2;
+                add_user(env, new_insn, new_insn->values[0]);
+                add_user(env, new_insn, new_insn->values[1]);
+                struct ir_value new_val;
+                new_val.type        = IR_VALUE_INSN;
+                new_val.data.insn_d = new_insn;
+                write_variable(env, insn.dst_reg, bb, new_val);
+            }
+
+            else {
                 // TODO
                 CRITICAL("Error");
             }
diff --git a/IR/include/bpf_ir.h b/IR/include/bpf_ir.h
index 2fc24dac..b03bf7ea 100644
--- a/IR/include/bpf_ir.h
+++ b/IR/include/bpf_ir.h
@@ -107,6 +107,7 @@ enum ir_vr_type {
         | ADD <value>, <value>
         | SUB <value>, <value>
         | MUL <value>, <value>
+        | LSH <value>, <value>
         | CALL <function id> <arg_num> <values...>
         | RET <value>
         | JA <bb>
@@ -147,6 +148,7 @@ struct ir_insn {
         IR_INSN_ADD,
         IR_INSN_SUB,
         IR_INSN_MUL,
+        IR_INSN_LSH,
         // CALL EXIT
         IR_INSN_CALL,
         IR_INSN_RET,
diff --git a/IR/ir_helper.c b/IR/ir_helper.c
index db97acc7..874048b0 100644
--- a/IR/ir_helper.c
+++ b/IR/ir_helper.c
@@ -36,22 +36,22 @@ void clean_id(struct ir_function *fun) {
 void print_constant(struct ir_constant d) {
     switch (d.type) {
         case IR_CONSTANT_S32:
-            printf("%x", d.data.s32_d);
+            printf("0x%x", d.data.s32_d);
             break;
         case IR_CONSTANT_U32:
-            printf("%x", d.data.u32_d);
+            printf("0x%x", d.data.u32_d);
             break;
         case IR_CONSTANT_U64:
-            printf("%llx", d.data.u64_d);
+            printf("0x%llx", d.data.u64_d);
             break;
         case IR_CONSTANT_S64:
-            printf("%llx", d.data.s64_d);
+            printf("0x%llx", d.data.s64_d);
             break;
         case IR_CONSTANT_S16:
-            printf("%x", d.data.s16_d);
+            printf("0x%x", d.data.s16_d);
             break;
         case IR_CONSTANT_U16:
-            printf("%x", d.data.u16_d);
+            printf("0x%x", d.data.u16_d);
             break;
         default:
             CRITICAL("Unknown constant type");
@@ -284,6 +284,12 @@ void print_ir_insn(struct ir_insn *insn) {
             printf("phi");
             print_phi(&insn->phi);
             break;
+        case IR_INSN_LSH:
+            printf("lsh ");
+            print_ir_value(insn->values[0]);
+            printf(", ");
+            print_ir_value(insn->values[1]);
+            break;
         default:
             CRITICAL("Unknown IR insn");
     }

From 08c23b3ff0efd5a1652ece8cfcc08229d643170f Mon Sep 17 00:00:00 2001
From: linsyking <kxiang@umich.edu>
Date: Tue, 16 Jul 2024 22:36:01 -0400
Subject: [PATCH 14/24] feat: add mod & sign

---
 IR/bpf_ir.c         | 13 +++++++++++++
 IR/include/bpf_ir.h |  2 ++
 IR/ir_helper.c      | 24 +++++++++++++++++++++---
 3 files changed, 36 insertions(+), 3 deletions(-)

diff --git a/IR/bpf_ir.c b/IR/bpf_ir.c
index e5b62710..5591518c 100644
--- a/IR/bpf_ir.c
+++ b/IR/bpf_ir.c
@@ -561,6 +561,19 @@ void transform_bb(struct ssa_transform_env *env, struct pre_ir_basic_block *bb)
                 new_val.type        = IR_VALUE_INSN;
                 new_val.data.insn_d = new_insn;
                 write_variable(env, insn.dst_reg, bb, new_val);
+            } else if (BPF_OP(code) == BPF_MOD) {
+                // dst = (src != 0) ? (dst % src) : dst
+                struct ir_insn *new_insn = create_insn_back(bb->ir_bb);
+                new_insn->op             = IR_INSN_MOD;
+                new_insn->values[0]      = read_variable(env, insn.dst_reg, bb);
+                new_insn->values[1]      = get_src_value(env, bb, insn);
+                new_insn->value_num      = 2;
+                add_user(env, new_insn, new_insn->values[0]);
+                add_user(env, new_insn, new_insn->values[1]);
+                struct ir_value new_val;
+                new_val.type        = IR_VALUE_INSN;
+                new_val.data.insn_d = new_insn;
+                write_variable(env, insn.dst_reg, bb, new_val);
             }
 
             else {
diff --git a/IR/include/bpf_ir.h b/IR/include/bpf_ir.h
index b03bf7ea..df6db8d8 100644
--- a/IR/include/bpf_ir.h
+++ b/IR/include/bpf_ir.h
@@ -108,6 +108,7 @@ enum ir_vr_type {
         | SUB <value>, <value>
         | MUL <value>, <value>
         | LSH <value>, <value>
+        | MOD <value>, <value>
         | CALL <function id> <arg_num> <values...>
         | RET <value>
         | JA <bb>
@@ -149,6 +150,7 @@ struct ir_insn {
         IR_INSN_SUB,
         IR_INSN_MUL,
         IR_INSN_LSH,
+        IR_INSN_MOD,
         // CALL EXIT
         IR_INSN_CALL,
         IR_INSN_RET,
diff --git a/IR/ir_helper.c b/IR/ir_helper.c
index 874048b0..d39859a3 100644
--- a/IR/ir_helper.c
+++ b/IR/ir_helper.c
@@ -36,7 +36,11 @@ void clean_id(struct ir_function *fun) {
 void print_constant(struct ir_constant d) {
     switch (d.type) {
         case IR_CONSTANT_S32:
-            printf("0x%x", d.data.s32_d);
+            if (d.data.s32_d < 0) {
+                printf("-0x%x", -d.data.s32_d);
+            } else {
+                printf("0x%x", d.data.s32_d);
+            }
             break;
         case IR_CONSTANT_U32:
             printf("0x%x", d.data.u32_d);
@@ -45,10 +49,18 @@ void print_constant(struct ir_constant d) {
             printf("0x%llx", d.data.u64_d);
             break;
         case IR_CONSTANT_S64:
-            printf("0x%llx", d.data.s64_d);
+            if (d.data.s64_d < 0) {
+                printf("-0x%llx", -d.data.s64_d);
+            } else {
+                printf("0x%llx", d.data.s64_d);
+            }
             break;
         case IR_CONSTANT_S16:
-            printf("0x%x", d.data.s16_d);
+            if (d.data.s16_d < 0) {
+                printf("-0x%x", -d.data.s16_d);
+            } else {
+                printf("0x%x", d.data.s16_d);
+            }
             break;
         case IR_CONSTANT_U16:
             printf("0x%x", d.data.u16_d);
@@ -290,6 +302,12 @@ void print_ir_insn(struct ir_insn *insn) {
             printf(", ");
             print_ir_value(insn->values[1]);
             break;
+        case IR_INSN_MOD:
+            printf("mod ");
+            print_ir_value(insn->values[0]);
+            printf(", ");
+            print_ir_value(insn->values[1]);
+            break;
         default:
             CRITICAL("Unknown IR insn");
     }

From f4edf3051318aca2f9f8456d3ccc27c9f6a171b6 Mon Sep 17 00:00:00 2001
From: linsyking <kxiang@umich.edu>
Date: Tue, 16 Jul 2024 22:39:27 -0400
Subject: [PATCH 15/24] feat: test offset

---
 IR/CMakeLists.txt | 1 +
 IR/bpf_ir.c       | 6 ++++++
 2 files changed, 7 insertions(+)

diff --git a/IR/CMakeLists.txt b/IR/CMakeLists.txt
index 7df24e83..8d651cf3 100644
--- a/IR/CMakeLists.txt
+++ b/IR/CMakeLists.txt
@@ -13,6 +13,7 @@ add_executable(
     phi_pass.c
     reachable_bb.c
     add_counter_pass.c
+    add_stack_offset.c
 )
 
 add_executable(probe probe.c read.c array.c)
diff --git a/IR/bpf_ir.c b/IR/bpf_ir.c
index 5591518c..bc47aa17 100644
--- a/IR/bpf_ir.c
+++ b/IR/bpf_ir.c
@@ -4,6 +4,7 @@
 #include <stdio.h>
 #include <stdlib.h>
 #include <stddef.h>
+#include "add_stack_offset.h"
 #include "array.h"
 #include "ir_insn.h"
 #include "list.h"
@@ -883,6 +884,11 @@ void run(struct bpf_insn *insns, size_t len) {
     printf("--------------------\n");
     print_ir_prog(&fun);
 
+    // Test
+    add_stack_offset(&fun, -8);
+    printf("--------------------\n");
+    print_ir_prog(&fun);
+
     // Free the memory
     free_function(&fun);
 }

From dad8480772d4bc1110e568c2105d39fa47a6b60e Mon Sep 17 00:00:00 2001
From: linsyking <kxiang@umich.edu>
Date: Tue, 16 Jul 2024 22:55:09 -0400
Subject: [PATCH 16/24] fix: alu64

---
 IR/bpf_ir.c      | 30 +++++++++---------------------
 IR/tests/alu64.c | 12 ++++++------
 2 files changed, 15 insertions(+), 27 deletions(-)

diff --git a/IR/bpf_ir.c b/IR/bpf_ir.c
index bc47aa17..ad0b0063 100644
--- a/IR/bpf_ir.c
+++ b/IR/bpf_ir.c
@@ -586,24 +586,12 @@ void transform_bb(struct ssa_transform_env *env, struct pre_ir_basic_block *bb)
                    BPF_SIZE(code) == BPF_DW) {
             // 64-bit immediate load
             if (insn.src_reg == 0x0) {
-                // TODO
-                struct ir_insn *new_insn = create_insn_back(bb->ir_bb);
-                new_insn->op             = IR_INSN_LOADRAW;
-                struct ir_address_value addr_val;
-                struct ir_value         imm_ptr;
-                imm_ptr.type                       = IR_VALUE_CONSTANT;
-                imm_ptr.data.constant_d.type       = IR_CONSTANT_U64;
-                imm_ptr.data.constant_d.data.u64_d = insn.imm64;
-                addr_val.value                     = imm_ptr;
-                add_user(env, new_insn, addr_val.value);
-                addr_val.offset    = 0;
-                new_insn->vr_type  = IR_VR_TYPE_U64;
-                new_insn->addr_val = addr_val;
-
-                struct ir_value new_val;
-                new_val.type        = IR_VALUE_INSN;
-                new_val.data.insn_d = new_insn;
-                write_variable(env, insn.dst_reg, bb, new_val);
+                // immediate value
+                struct ir_value imm_val;
+                imm_val.type                       = IR_VALUE_CONSTANT;
+                imm_val.data.constant_d.type       = IR_CONSTANT_U64;
+                imm_val.data.constant_d.data.u64_d = insn.imm64;
+                write_variable(env, insn.dst_reg, bb, imm_val);
             } else {
                 CRITICAL("Not supported");
             }
@@ -885,9 +873,9 @@ void run(struct bpf_insn *insns, size_t len) {
     print_ir_prog(&fun);
 
     // Test
-    add_stack_offset(&fun, -8);
-    printf("--------------------\n");
-    print_ir_prog(&fun);
+    // add_stack_offset(&fun, -8);
+    // printf("--------------------\n");
+    // print_ir_prog(&fun);
 
     // Free the memory
     free_function(&fun);
diff --git a/IR/tests/alu64.c b/IR/tests/alu64.c
index 2ffd4791..04f77f2c 100644
--- a/IR/tests/alu64.c
+++ b/IR/tests/alu64.c
@@ -1,18 +1,18 @@
 #include <linux/bpf.h>
 #include <bpf/bpf_helpers.h>
 
-
 SEC("xdp")
 int prog(void *ctx) {
-    // char s1[] = "hello world my friend";
+    char s2[] = "1";
+    bpf_trace_printk(s2, sizeof(s2));
+    char s1[] = "hello world\n";
     // bpf_trace_printk(s1, sizeof(s1));
-    __u64 i1 = 0x3456789abcdef0;
-    __u64 i2 = 0x76543210fedcba;
-    __u64 ans = i1+i2;
+    __u64 i1  = 0x3456789abcdef0;
+    __u64 i2  = 0x76543210fedcba;
+    __u64 ans = i1 + i2;
     // char s[10] = {};
 
     // int i = 2;
-    // s[i]++;
     return 0;
 }
 

From 4dd8512a3cfeb1fd059f03830083482a67f90c51 Mon Sep 17 00:00:00 2001
From: linsyking <kxiang@umich.edu>
Date: Tue, 16 Jul 2024 23:04:46 -0400
Subject: [PATCH 17/24] feat: binary ins

---
 IR/add_counter_pass.c |  2 +-
 IR/add_stack_offset.c |  4 +-
 IR/include/bpf_ir.h   | 92 +++++++++++++++++++++++--------------------
 IR/include/ir_insn.h  |  9 +++--
 IR/ir_insn.c          | 19 ++++-----
 5 files changed, 67 insertions(+), 59 deletions(-)

diff --git a/IR/add_counter_pass.c b/IR/add_counter_pass.c
index e0c18c20..8f2ab632 100644
--- a/IR/add_counter_pass.c
+++ b/IR/add_counter_pass.c
@@ -34,7 +34,7 @@ void add_counter(struct ir_function *fun) {
         struct ir_value val2;
         val2.type                         = IR_VALUE_INSN;
         val2.data.insn_d                  = load_insn;
-        struct ir_insn *added             = create_add_insn(load_insn, val1, val2, INSERT_BACK);
+        struct ir_insn *added             = create_bin_insn(load_insn, val1, val2, INSERT_BACK);
         val.data.insn_d                   = added;
         struct ir_insn        *store_back = create_store_insn(added, alloc_insn, val, INSERT_BACK);
         struct ir_basic_block *new_bb     = split_bb(fun, store_back);
diff --git a/IR/add_stack_offset.c b/IR/add_stack_offset.c
index 433f357d..f26a01bf 100644
--- a/IR/add_stack_offset.c
+++ b/IR/add_stack_offset.c
@@ -21,7 +21,7 @@ void add_stack_offset(struct ir_function *fun, __s16 offset) {
                 val.data.constant_d.type       = IR_CONSTANT_S16;
                 val.data.constant_d.data.s16_d = offset;
                 struct ir_insn *new_insn =
-                    create_add_insn(insn, insn->values[j], val, INSERT_FRONT);
+                    create_bin_insn(insn, insn->values[j], val, INSERT_FRONT);
                 val.type        = IR_VALUE_INSN;
                 val.data.insn_d = new_insn;
                 insn->values[j] = val;
@@ -37,7 +37,7 @@ void add_stack_offset(struct ir_function *fun, __s16 offset) {
                     val.data.constant_d.type       = IR_CONSTANT_S16;
                     val.data.constant_d.data.s16_d = offset;
                     struct ir_insn *new_insn =
-                        create_add_insn(insn, pv_pos2->value, val, INSERT_FRONT);
+                        create_bin_insn(insn, pv_pos2->value, val, INSERT_FRONT);
                     val.type        = IR_VALUE_INSN;
                     val.data.insn_d = new_insn;
                     pv_pos2->value = val;
diff --git a/IR/include/bpf_ir.h b/IR/include/bpf_ir.h
index df6db8d8..81137fab 100644
--- a/IR/include/bpf_ir.h
+++ b/IR/include/bpf_ir.h
@@ -23,6 +23,15 @@ struct pre_ir_insn {
     size_t pos;  // Original position
 };
 
+enum ir_constant_type {
+    IR_CONSTANT_U16,
+    IR_CONSTANT_S16,
+    IR_CONSTANT_U32,
+    IR_CONSTANT_S32,
+    IR_CONSTANT_U64,
+    IR_CONSTANT_S64,
+};
+
 /**
     IR Constants
  */
@@ -35,14 +44,15 @@ struct ir_constant {
         __u64 u64_d;
         __s64 s64_d;
     } data;
-    enum {
-        IR_CONSTANT_U16,
-        IR_CONSTANT_S16,
-        IR_CONSTANT_U32,
-        IR_CONSTANT_S32,
-        IR_CONSTANT_U64,
-        IR_CONSTANT_S64,
-    } type;
+    enum ir_constant_type type;
+};
+
+enum ir_value_type {
+    IR_VALUE_CONSTANT,
+    IR_VALUE_FUNCTIONARG,
+    IR_VALUE_INSN,
+    IR_VALUE_STACK_PTR,
+    IR_VALUE_UNDEF,
 };
 
 /**
@@ -56,13 +66,7 @@ struct ir_value {
         struct ir_insn    *insn_d;
         __u8               arg_id;
     } data;
-    enum {
-        IR_VALUE_CONSTANT,
-        IR_VALUE_FUNCTIONARG,
-        IR_VALUE_INSN,
-        IR_VALUE_STACK_PTR,
-        IR_VALUE_UNDEF,
-    } type;
+    enum ir_value_type type;
 };
 
 /**
@@ -97,6 +101,33 @@ enum ir_vr_type {
     IR_VR_TYPE_PTR,
 };
 
+enum ir_insn_type {
+    IR_INSN_ALLOC,
+    IR_INSN_STORE,
+    IR_INSN_LOAD,
+    IR_INSN_STORERAW,
+    IR_INSN_LOADRAW,
+    // ALU
+    IR_INSN_ADD,
+    IR_INSN_SUB,
+    IR_INSN_MUL,
+    IR_INSN_LSH,
+    IR_INSN_MOD,
+    // CALL EXIT
+    IR_INSN_CALL,
+    IR_INSN_RET,
+    // JMP
+    IR_INSN_JA,
+    IR_INSN_JEQ,
+    IR_INSN_JGT,
+    IR_INSN_JGE,
+    IR_INSN_JLT,
+    IR_INSN_JLE,
+    IR_INSN_JNE,
+    // PHI
+    IR_INSN_PHI
+};
+
 /**
     INSN =
           ALLOC <ir_vr_type>
@@ -137,34 +168,9 @@ struct ir_insn {
     // Array of phi_value
     struct array phi;
 
-    __s32 fid;
-    __u32 f_arg_num;
-    enum {
-        IR_INSN_ALLOC,
-        IR_INSN_STORE,
-        IR_INSN_LOAD,
-        IR_INSN_STORERAW,
-        IR_INSN_LOADRAW,
-        // ALU
-        IR_INSN_ADD,
-        IR_INSN_SUB,
-        IR_INSN_MUL,
-        IR_INSN_LSH,
-        IR_INSN_MOD,
-        // CALL EXIT
-        IR_INSN_CALL,
-        IR_INSN_RET,
-        // JMP
-        IR_INSN_JA,
-        IR_INSN_JEQ,
-        IR_INSN_JGT,
-        IR_INSN_JGE,
-        IR_INSN_JLT,
-        IR_INSN_JLE,
-        IR_INSN_JNE,
-        // PHI
-        IR_INSN_PHI
-    } op;
+    __s32             fid;
+    __u32             f_arg_num;
+    enum ir_insn_type op;
 
     // Linked list
     struct list_head list_ptr;
diff --git a/IR/include/ir_insn.h b/IR/include/ir_insn.h
index 63f7f6a7..55043d66 100644
--- a/IR/include/ir_insn.h
+++ b/IR/include/ir_insn.h
@@ -27,11 +27,12 @@ struct ir_insn *create_load_insn(struct ir_insn *insn, enum ir_vr_type ty, struc
 struct ir_insn *create_load_insn_bb(struct ir_basic_block *bb, enum ir_vr_type ty,
                                     struct ir_value val, enum insert_position pos);
 
-struct ir_insn *create_add_insn(struct ir_insn *insn, struct ir_value val1, struct ir_value val2,
-                                enum insert_position pos);
+struct ir_insn *create_bin_insn(struct ir_insn *insn, struct ir_value val1, struct ir_value val2,
+                                enum ir_insn_type ty, enum insert_position pos);
 
-struct ir_insn *create_add_insn_bb(struct ir_basic_block *bb, struct ir_value val1,
-                                   struct ir_value val2, enum insert_position pos);
+struct ir_insn *create_bin_insn_bb(struct ir_basic_block *bb, struct ir_value val1,
+                                   struct ir_value val2, enum ir_insn_type ty,
+                                   enum insert_position pos);
 
 struct ir_insn *create_jlt_insn(struct ir_insn *insn, struct ir_value val1, struct ir_value val2,
                                 struct ir_basic_block *to_bb1, struct ir_basic_block *to_bb2,
diff --git a/IR/ir_insn.c b/IR/ir_insn.c
index 190f2928..e524c9e5 100644
--- a/IR/ir_insn.c
+++ b/IR/ir_insn.c
@@ -115,10 +115,10 @@ struct ir_insn *create_load_insn_bb(struct ir_basic_block *bb, enum ir_vr_type t
     return new_insn;
 }
 
-struct ir_insn *create_add_insn_base(struct ir_basic_block *bb, struct ir_value val1,
-                                     struct ir_value val2) {
+struct ir_insn *create_bin_insn_base(struct ir_basic_block *bb, struct ir_value val1,
+                                     struct ir_value val2, enum ir_insn_type ty) {
     struct ir_insn *new_insn = create_insn_base(bb);
-    new_insn->op             = IR_INSN_ADD;
+    new_insn->op             = ty;
     new_insn->values[0]      = val1;
     new_insn->values[1]      = val2;
     val_add_user(val1, new_insn);
@@ -126,16 +126,17 @@ struct ir_insn *create_add_insn_base(struct ir_basic_block *bb, struct ir_value
     return new_insn;
 }
 
-struct ir_insn *create_add_insn(struct ir_insn *insn, struct ir_value val1, struct ir_value val2,
-                                enum insert_position pos) {
-    struct ir_insn *new_insn = create_add_insn_base(insn->parent_bb, val1, val2);
+struct ir_insn *create_bin_insn(struct ir_insn *insn, struct ir_value val1, struct ir_value val2,
+                                enum ir_insn_type ty, enum insert_position pos) {
+    struct ir_insn *new_insn = create_bin_insn_base(insn->parent_bb, val1, val2, ty);
     insert_at(new_insn, insn, pos);
     return new_insn;
 }
 
-struct ir_insn *create_add_insn_bb(struct ir_basic_block *bb, struct ir_value val1,
-                                   struct ir_value val2, enum insert_position pos) {
-    struct ir_insn *new_insn = create_add_insn_base(bb, val1, val2);
+struct ir_insn *create_bin_insn_bb(struct ir_basic_block *bb, struct ir_value val1,
+                                   struct ir_value val2, enum ir_insn_type ty,
+                                   enum insert_position pos) {
+    struct ir_insn *new_insn = create_bin_insn_base(bb, val1, val2, ty);
     insert_at_bb(new_insn, bb, pos);
     return new_insn;
 }

From a3ff563a2f0d30a421dd58b8c744d3ddb714ce30 Mon Sep 17 00:00:00 2001
From: linsyking <kxiang@umich.edu>
Date: Tue, 16 Jul 2024 23:12:32 -0400
Subject: [PATCH 18/24] refactor: use IR helper functions to build IR

---
 IR/add_counter_pass.c |  8 +++----
 IR/add_stack_offset.c |  6 +++---
 IR/bpf_ir.c           | 50 +++++++++++++------------------------------
 3 files changed, 22 insertions(+), 42 deletions(-)

diff --git a/IR/add_counter_pass.c b/IR/add_counter_pass.c
index 8f2ab632..9cd3d663 100644
--- a/IR/add_counter_pass.c
+++ b/IR/add_counter_pass.c
@@ -32,10 +32,10 @@ void add_counter(struct ir_function *fun) {
         val1.data.constant_d.type       = IR_CONSTANT_U64;
         val1.data.constant_d.data.u64_d = len;
         struct ir_value val2;
-        val2.type                         = IR_VALUE_INSN;
-        val2.data.insn_d                  = load_insn;
-        struct ir_insn *added             = create_bin_insn(load_insn, val1, val2, INSERT_BACK);
-        val.data.insn_d                   = added;
+        val2.type             = IR_VALUE_INSN;
+        val2.data.insn_d      = load_insn;
+        struct ir_insn *added = create_bin_insn(load_insn, val1, val2, IR_INSN_ADD, INSERT_BACK);
+        val.data.insn_d       = added;
         struct ir_insn        *store_back = create_store_insn(added, alloc_insn, val, INSERT_BACK);
         struct ir_basic_block *new_bb     = split_bb(fun, store_back);
         val2.data.insn_d                  = added;
diff --git a/IR/add_stack_offset.c b/IR/add_stack_offset.c
index f26a01bf..2ee976db 100644
--- a/IR/add_stack_offset.c
+++ b/IR/add_stack_offset.c
@@ -21,7 +21,7 @@ void add_stack_offset(struct ir_function *fun, __s16 offset) {
                 val.data.constant_d.type       = IR_CONSTANT_S16;
                 val.data.constant_d.data.s16_d = offset;
                 struct ir_insn *new_insn =
-                    create_bin_insn(insn, insn->values[j], val, INSERT_FRONT);
+                    create_bin_insn(insn, insn->values[j], val, IR_INSN_ADD, INSERT_FRONT);
                 val.type        = IR_VALUE_INSN;
                 val.data.insn_d = new_insn;
                 insn->values[j] = val;
@@ -37,10 +37,10 @@ void add_stack_offset(struct ir_function *fun, __s16 offset) {
                     val.data.constant_d.type       = IR_CONSTANT_S16;
                     val.data.constant_d.data.s16_d = offset;
                     struct ir_insn *new_insn =
-                        create_bin_insn(insn, pv_pos2->value, val, INSERT_FRONT);
+                        create_bin_insn(insn, pv_pos2->value, val,IR_INSN_ADD, INSERT_FRONT);
                     val.type        = IR_VALUE_INSN;
                     val.data.insn_d = new_insn;
-                    pv_pos2->value = val;
+                    pv_pos2->value  = val;
                 }
             }
         }
diff --git a/IR/bpf_ir.c b/IR/bpf_ir.c
index ad0b0063..f0e33533 100644
--- a/IR/bpf_ir.c
+++ b/IR/bpf_ir.c
@@ -510,39 +510,27 @@ void transform_bb(struct ssa_transform_env *env, struct pre_ir_basic_block *bb)
             // 32-bit ALU class
             // TODO: 64-bit ALU class
             if (BPF_OP(code) == BPF_ADD) {
-                struct ir_insn *new_insn = create_insn_back(bb->ir_bb);
-                new_insn->op             = IR_INSN_ADD;
-                new_insn->values[0]      = read_variable(env, insn.dst_reg, bb);
-                new_insn->values[1]      = get_src_value(env, bb, insn);
-                new_insn->value_num      = 2;
-                add_user(env, new_insn, new_insn->values[0]);
-                add_user(env, new_insn, new_insn->values[1]);
+                struct ir_insn *new_insn =
+                    create_bin_insn_bb(bb->ir_bb, read_variable(env, insn.dst_reg, bb),
+                                       get_src_value(env, bb, insn), IR_INSN_ADD, INSERT_BACK);
 
                 struct ir_value new_val;
                 new_val.type        = IR_VALUE_INSN;
                 new_val.data.insn_d = new_insn;
                 write_variable(env, insn.dst_reg, bb, new_val);
             } else if (BPF_OP(code) == BPF_SUB) {
-                struct ir_insn *new_insn = create_insn_back(bb->ir_bb);
-                new_insn->op             = IR_INSN_SUB;
-                new_insn->values[0]      = read_variable(env, insn.dst_reg, bb);
-                new_insn->values[1]      = get_src_value(env, bb, insn);
-                new_insn->value_num      = 2;
-                add_user(env, new_insn, new_insn->values[0]);
-                add_user(env, new_insn, new_insn->values[1]);
+                struct ir_insn *new_insn =
+                    create_bin_insn_bb(bb->ir_bb, read_variable(env, insn.dst_reg, bb),
+                                       get_src_value(env, bb, insn), IR_INSN_SUB, INSERT_BACK);
 
                 struct ir_value new_val;
                 new_val.type        = IR_VALUE_INSN;
                 new_val.data.insn_d = new_insn;
                 write_variable(env, insn.dst_reg, bb, new_val);
             } else if (BPF_OP(code) == BPF_MUL) {
-                struct ir_insn *new_insn = create_insn_back(bb->ir_bb);
-                new_insn->op             = IR_INSN_MUL;
-                new_insn->values[0]      = read_variable(env, insn.dst_reg, bb);
-                new_insn->values[1]      = get_src_value(env, bb, insn);
-                new_insn->value_num      = 2;
-                add_user(env, new_insn, new_insn->values[0]);
-                add_user(env, new_insn, new_insn->values[1]);
+                struct ir_insn *new_insn =
+                    create_bin_insn_bb(bb->ir_bb, read_variable(env, insn.dst_reg, bb),
+                                       get_src_value(env, bb, insn), IR_INSN_MUL, INSERT_BACK);
                 struct ir_value new_val;
                 new_val.type        = IR_VALUE_INSN;
                 new_val.data.insn_d = new_insn;
@@ -551,26 +539,18 @@ void transform_bb(struct ssa_transform_env *env, struct pre_ir_basic_block *bb)
                 // Do not create instructions
                 write_variable(env, insn.dst_reg, bb, get_src_value(env, bb, insn));
             } else if (BPF_OP(code) == BPF_LSH) {
-                struct ir_insn *new_insn = create_insn_back(bb->ir_bb);
-                new_insn->op             = IR_INSN_LSH;
-                new_insn->values[0]      = read_variable(env, insn.dst_reg, bb);
-                new_insn->values[1]      = get_src_value(env, bb, insn);
-                new_insn->value_num      = 2;
-                add_user(env, new_insn, new_insn->values[0]);
-                add_user(env, new_insn, new_insn->values[1]);
+                struct ir_insn *new_insn =
+                    create_bin_insn_bb(bb->ir_bb, read_variable(env, insn.dst_reg, bb),
+                                       get_src_value(env, bb, insn), IR_INSN_LSH, INSERT_BACK);
                 struct ir_value new_val;
                 new_val.type        = IR_VALUE_INSN;
                 new_val.data.insn_d = new_insn;
                 write_variable(env, insn.dst_reg, bb, new_val);
             } else if (BPF_OP(code) == BPF_MOD) {
                 // dst = (src != 0) ? (dst % src) : dst
-                struct ir_insn *new_insn = create_insn_back(bb->ir_bb);
-                new_insn->op             = IR_INSN_MOD;
-                new_insn->values[0]      = read_variable(env, insn.dst_reg, bb);
-                new_insn->values[1]      = get_src_value(env, bb, insn);
-                new_insn->value_num      = 2;
-                add_user(env, new_insn, new_insn->values[0]);
-                add_user(env, new_insn, new_insn->values[1]);
+                struct ir_insn *new_insn =
+                    create_bin_insn_bb(bb->ir_bb, read_variable(env, insn.dst_reg, bb),
+                                       get_src_value(env, bb, insn), IR_INSN_MOD, INSERT_BACK);
                 struct ir_value new_val;
                 new_val.type        = IR_VALUE_INSN;
                 new_val.data.insn_d = new_insn;

From bf27179db385eb2b4543049b8f4faf2b94ac0e5d Mon Sep 17 00:00:00 2001
From: linsyking <kxiang@umich.edu>
Date: Tue, 16 Jul 2024 23:53:59 -0400
Subject: [PATCH 19/24] feat: constraint model

---
 IR/format.sh                  |  3 +++
 IR/include/add_counter_pass.h |  2 +-
 IR/include/add_stack_offset.h |  2 +-
 IR/include/bpf_ir.h           | 22 ----------------------
 IR/include/constraint.h       | 25 +++++++++++++++++++++++++
 IR/include/ir_bb.h            |  1 +
 IR/include/ir_fun.h           | 30 ++++++++++++++++++++++++++++++
 IR/include/passes.h           |  1 +
 IR/include/phi_pass.h         |  2 +-
 IR/include/reachable_bb.h     |  3 ++-
 IR/ir_helper.c                |  1 +
 11 files changed, 66 insertions(+), 26 deletions(-)
 create mode 100644 IR/format.sh
 create mode 100644 IR/include/constraint.h
 create mode 100644 IR/include/ir_fun.h

diff --git a/IR/format.sh b/IR/format.sh
new file mode 100644
index 00000000..2849228d
--- /dev/null
+++ b/IR/format.sh
@@ -0,0 +1,3 @@
+#!/bin/bash
+
+find . -iname '*.h' -o -iname '*.c' | xargs clang-format -i
diff --git a/IR/include/add_counter_pass.h b/IR/include/add_counter_pass.h
index 7f1b77d8..e37f669e 100644
--- a/IR/include/add_counter_pass.h
+++ b/IR/include/add_counter_pass.h
@@ -1,7 +1,7 @@
 #ifndef __BPF_IR_ADD_COUNTER_PASS_H__
 #define __BPF_IR_ADD_COUNTER_PASS_H__
 
-#include "bpf_ir.h"
+#include "ir_fun.h"
 
 void add_counter(struct ir_function *fun);
 
diff --git a/IR/include/add_stack_offset.h b/IR/include/add_stack_offset.h
index b4b6c938..82305924 100644
--- a/IR/include/add_stack_offset.h
+++ b/IR/include/add_stack_offset.h
@@ -1,7 +1,7 @@
 #ifndef __BPF_IR_ADD_STACK_OFFSET_H__
 #define __BPF_IR_ADD_STACK_OFFSET_H__
 
-#include "bpf_ir.h"
+#include "ir_fun.h"
 
 // Add stack offset to all stack access
 void add_stack_offset(struct ir_function *fun, __s16 offset);
diff --git a/IR/include/bpf_ir.h b/IR/include/bpf_ir.h
index 81137fab..91dbf052 100644
--- a/IR/include/bpf_ir.h
+++ b/IR/include/bpf_ir.h
@@ -279,22 +279,6 @@ struct ssa_transform_env {
     struct array sp_users;
 };
 
-struct ir_function {
-    size_t arg_num;
-
-    // Array of struct pre_ir_basic_block *, no entrance information anymore
-    struct array all_bbs;
-
-    // The entry block
-    struct ir_basic_block *entry;
-
-    // Store any information about the function
-    struct array reachable_bbs;
-
-    // Stack pointer (r10) users. Should be readonly. No more manual stack access should be allowed.
-    struct array sp_users;
-};
-
 // helper functions
 
 void write_variable(struct ssa_transform_env *env, __u8 reg, struct pre_ir_basic_block *bb,
@@ -318,12 +302,6 @@ struct ir_insn *create_insn_front(struct ir_basic_block *bb);
 
 void add_user(struct ssa_transform_env *env, struct ir_insn *user, struct ir_value val);
 
-void clean_env(struct ir_function *);
-
-void clean_id(struct ir_function *);
-
-void print_ir_prog(struct ir_function *);
-
 void print_ir_insn(struct ir_insn *);
 
 void print_ir_value(struct ir_value v);
diff --git a/IR/include/constraint.h b/IR/include/constraint.h
new file mode 100644
index 00000000..2deb3a52
--- /dev/null
+++ b/IR/include/constraint.h
@@ -0,0 +1,25 @@
+#ifndef __BPF_IR_CONSTRAINT_H__
+#define __BPF_IR_CONSTRAINT_H__
+
+#include "bpf_ir.h"
+
+enum constraint_type {
+    CONSTRAINT_TYPE_VALUE_EQUAL,
+    CONSTRAINT_TYPE_VALUE_RANGE
+};
+
+struct ir_constraint {
+    enum constraint_type type;
+
+    // Range: [start, start + size)
+    __u64 start;
+    __u64 size;
+
+    // Constrain value
+    __u64 cval;
+
+    // Real value to be compared
+    struct ir_value val;
+};
+
+#endif
diff --git a/IR/include/ir_bb.h b/IR/include/ir_bb.h
index 9c18d8cc..60a4c664 100644
--- a/IR/include/ir_bb.h
+++ b/IR/include/ir_bb.h
@@ -2,6 +2,7 @@
 #define __BPF_IR_BB_H__
 
 #include "bpf_ir.h"
+#include "ir_fun.h"
 
 /// Get the number of instructions in a basic block
 size_t bb_len(struct ir_basic_block *);
diff --git a/IR/include/ir_fun.h b/IR/include/ir_fun.h
new file mode 100644
index 00000000..1763546d
--- /dev/null
+++ b/IR/include/ir_fun.h
@@ -0,0 +1,30 @@
+#ifndef __BPF_IR_FUN_H__
+#define __BPF_IR_FUN_H__
+
+#include "bpf_ir.h"
+
+struct ir_function {
+    size_t arg_num;
+
+    // Array of struct pre_ir_basic_block *, no entrance information anymore
+    struct array all_bbs;
+
+    // The entry block
+    struct ir_basic_block *entry;
+
+    // Store any information about the function
+    struct array reachable_bbs;
+
+    // Stack pointer (r10) users. Should be readonly. No more manual stack access should be allowed.
+    struct array sp_users;
+};
+
+// Helper functions
+
+void clean_env(struct ir_function *);
+
+void clean_id(struct ir_function *);
+
+void print_ir_prog(struct ir_function *);
+
+#endif
diff --git a/IR/include/passes.h b/IR/include/passes.h
index 7d5e2d9e..1cde07ed 100644
--- a/IR/include/passes.h
+++ b/IR/include/passes.h
@@ -4,6 +4,7 @@
 #include "phi_pass.h"
 #include "reachable_bb.h"
 #include "add_counter_pass.h"
+#include "ir_fun.h"
 
 /**
     All function passes.
diff --git a/IR/include/phi_pass.h b/IR/include/phi_pass.h
index db2eaba8..6776dda3 100644
--- a/IR/include/phi_pass.h
+++ b/IR/include/phi_pass.h
@@ -1,7 +1,7 @@
 #ifndef __BPF_IR_PHI_PASS_H__
 #define __BPF_IR_PHI_PASS_H__
 
-#include "bpf_ir.h"
+#include "ir_fun.h"
 
 void remove_trivial_phi(struct ir_function *fun);
 
diff --git a/IR/include/reachable_bb.h b/IR/include/reachable_bb.h
index 79f59584..edd0cca0 100644
--- a/IR/include/reachable_bb.h
+++ b/IR/include/reachable_bb.h
@@ -1,7 +1,8 @@
 #ifndef __BPF_IR_REACHABLE_BB_H__
 #define __BPF_IR_REACHABLE_BB_H__
 
-#include "bpf_ir.h"
+#include "ir_fun.h"
+
 void gen_reachable_bbs(struct ir_function *);
 
 #endif
diff --git a/IR/ir_helper.c b/IR/ir_helper.c
index d39859a3..91c0a5ab 100644
--- a/IR/ir_helper.c
+++ b/IR/ir_helper.c
@@ -4,6 +4,7 @@
 #include "bpf_ir.h"
 #include "dbg.h"
 #include "list.h"
+#include "ir_fun.h"
 
 /// Reset visited flag
 void clean_env(struct ir_function *fun) {

From ab2e7e8cbf3f2f1ddafc675704130bb277919b84 Mon Sep 17 00:00:00 2001
From: linsyking <kxiang@umich.edu>
Date: Tue, 16 Jul 2024 23:54:23 -0400
Subject: [PATCH 20/24] chore: format

---
 IR/add_stack_offset.c | 2 +-
 IR/format.sh          | 0
 IR/include/list.h     | 6 ++----
 IR/include/passes.h   | 3 +--
 IR/tests/mem1.c       | 2 +-
 IR/tests/mem2.c       | 6 +++---
 IR/tests/test_asm.c   | 4 ++--
 7 files changed, 10 insertions(+), 13 deletions(-)
 mode change 100644 => 100755 IR/format.sh

diff --git a/IR/add_stack_offset.c b/IR/add_stack_offset.c
index 2ee976db..590f6d0b 100644
--- a/IR/add_stack_offset.c
+++ b/IR/add_stack_offset.c
@@ -37,7 +37,7 @@ void add_stack_offset(struct ir_function *fun, __s16 offset) {
                     val.data.constant_d.type       = IR_CONSTANT_S16;
                     val.data.constant_d.data.s16_d = offset;
                     struct ir_insn *new_insn =
-                        create_bin_insn(insn, pv_pos2->value, val,IR_INSN_ADD, INSERT_FRONT);
+                        create_bin_insn(insn, pv_pos2->value, val, IR_INSN_ADD, INSERT_FRONT);
                     val.type        = IR_VALUE_INSN;
                     val.data.insn_d = new_insn;
                     pv_pos2->value  = val;
diff --git a/IR/format.sh b/IR/format.sh
old mode 100644
new mode 100755
diff --git a/IR/include/list.h b/IR/include/list.h
index 4692adfa..2401e870 100644
--- a/IR/include/list.h
+++ b/IR/include/list.h
@@ -62,8 +62,7 @@ struct list_head {
     struct list_head *next, *prev;
 };
 
-#define LIST_HEAD_INIT(name) \
-    { &(name), &(name) }
+#define LIST_HEAD_INIT(name) {&(name), &(name)}
 
 #define LIST_HEAD(name) struct list_head name = LIST_HEAD_INIT(name)
 
@@ -346,8 +345,7 @@ struct hlist_node {
     struct hlist_node *next, **pprev;
 };
 
-#define HLIST_HEAD_INIT \
-    { .first = NULL }
+#define HLIST_HEAD_INIT      {.first = NULL}
 #define HLIST_HEAD(name)     struct hlist_head name = {.first = NULL}
 #define INIT_HLIST_HEAD(ptr) ((ptr)->first = NULL)
 #define INIT_HLIST_NODE(ptr) ((ptr)->next = NULL, (ptr)->pprev = NULL)
diff --git a/IR/include/passes.h b/IR/include/passes.h
index 1cde07ed..92431ad7 100644
--- a/IR/include/passes.h
+++ b/IR/include/passes.h
@@ -10,8 +10,7 @@
     All function passes.
  */
 static void (*passes[])(struct ir_function *fun) = {
-    gen_reachable_bbs,
-    remove_trivial_phi,
+    gen_reachable_bbs, remove_trivial_phi,
     // add_counter,
 };
 
diff --git a/IR/tests/mem1.c b/IR/tests/mem1.c
index 2ab003eb..a4daefcd 100644
--- a/IR/tests/mem1.c
+++ b/IR/tests/mem1.c
@@ -9,7 +9,7 @@
 
 SEC("xdp")
 int prog(void *ctx) {
-    int id = bpf_ktime_get_ns() % 20;
+    int id      = bpf_ktime_get_ns() % 20;
     int arr[10] = {};
     for (int i = 0; i < 10; ++i) {
         arr[i] = i;
diff --git a/IR/tests/mem2.c b/IR/tests/mem2.c
index d21be52d..d26b8337 100644
--- a/IR/tests/mem2.c
+++ b/IR/tests/mem2.c
@@ -17,7 +17,7 @@ int __noinline call(__u64 i) {
 
 SEC("xdp")
 int prog(struct xdp_md *ctx) {
-    int id = bpf_ktime_get_ns() % 20;   // We cannot use 10 here
+    int   id      = bpf_ktime_get_ns() % 20;  // We cannot use 10 here
     __u64 arr[10] = {};
     for (__u32 i = 0; i < 10; ++i) {
         arr[i] = i;
@@ -25,12 +25,12 @@ int prog(struct xdp_md *ctx) {
     call(arr[9]);  // Pass
     // call(arr[10]);  // Not Pass
     // call(arr[11]);  // Not Pass
-    if (id > 9 || id < 0) { // Work
+    if (id > 9 || id < 0) {  // Work
         goto end;
     }
     __u64 res = arr[id];
     call(res);
-    #pragma nounroll
+#pragma nounroll
     for (__u32 i = 0; i < 10; ++i) {
         call(arr[i]);
         arr[i] = i + 1;
diff --git a/IR/tests/test_asm.c b/IR/tests/test_asm.c
index 4307c70d..833ff61a 100644
--- a/IR/tests/test_asm.c
+++ b/IR/tests/test_asm.c
@@ -30,9 +30,9 @@ void __noinline pk_l(char *s) {
 
 SEC("xdp")
 int prog(void *ctx) {
-    int s = spill(1, 2);
+    int         s        = spill(1, 2);
     static char ores[10] = "helloggg";
-    static char res[10] = "helloworld";
+    static char res[10]  = "helloworld";
     for (int i = 0; i < 10; ++i) {
         pk(res[i]);
     }

From 5fe4ee1c99260173c8b6a3b3f4087d67516b0919 Mon Sep 17 00:00:00 2001
From: linsyking <kxiang@umich.edu>
Date: Wed, 17 Jul 2024 00:01:26 -0400
Subject: [PATCH 21/24] feat: add pass

---
 IR/add_constraint_pass.c         | 10 ++++++++++
 IR/bpf_ir.c                      | 14 +++++++-------
 IR/include/add_constraint_pass.h |  8 ++++++++
 IR/include/array.h               |  2 ++
 IR/include/ir_fun.h              |  5 +++++
 5 files changed, 32 insertions(+), 7 deletions(-)
 create mode 100644 IR/add_constraint_pass.c
 create mode 100644 IR/include/add_constraint_pass.h

diff --git a/IR/add_constraint_pass.c b/IR/add_constraint_pass.c
new file mode 100644
index 00000000..73d2eb63
--- /dev/null
+++ b/IR/add_constraint_pass.c
@@ -0,0 +1,10 @@
+#include "add_constraint_pass.h"
+#include "array.h"
+#include "constraint.h"
+
+// Initialize some testing constraints
+void init_test_constraints(struct ir_function *fun) {
+    fun->value_constraints = INIT_ARRAY(struct ir_constraint);
+}
+
+void add_constraint(struct ir_function *fun) {}
diff --git a/IR/bpf_ir.c b/IR/bpf_ir.c
index f0e33533..bd94206d 100644
--- a/IR/bpf_ir.c
+++ b/IR/bpf_ir.c
@@ -785,11 +785,11 @@ void free_function(struct ir_function *fun) {
 }
 
 struct ir_function gen_function(struct ssa_transform_env *env) {
-    struct ir_function func;
-    func.arg_num  = 1;
-    func.entry    = env->info.entry->ir_bb;
-    func.sp_users = env->sp_users;
-    func.all_bbs  = array_init(sizeof(struct ir_basic_block *));
+    struct ir_function fun;
+    fun.arg_num  = 1;
+    fun.entry    = env->info.entry->ir_bb;
+    fun.sp_users = env->sp_users;
+    fun.all_bbs  = array_init(sizeof(struct ir_basic_block *));
     for (size_t i = 0; i < MAX_BPF_REG; ++i) {
         struct array *currentDef = &env->currentDef[i];
         array_free(currentDef);
@@ -800,10 +800,10 @@ struct ir_function gen_function(struct ssa_transform_env *env) {
         array_free(&bb->succs);
         free(bb->pre_insns);
         bb->ir_bb->user_data = NULL;
-        array_push(&func.all_bbs, &bb->ir_bb);
+        array_push(&fun.all_bbs, &bb->ir_bb);
         free(bb);
     }
-    return func;
+    return fun;
 }
 
 __u8 ir_value_equal(struct ir_value a, struct ir_value b) {
diff --git a/IR/include/add_constraint_pass.h b/IR/include/add_constraint_pass.h
new file mode 100644
index 00000000..06b79668
--- /dev/null
+++ b/IR/include/add_constraint_pass.h
@@ -0,0 +1,8 @@
+#ifndef __BPF_IR_ADD_CONSTRAINT_PASS_H__
+#define __BPF_IR_ADD_CONSTRAINT_PASS_H__
+
+#include "ir_fun.h"
+
+void add_constraint(struct ir_function *fun);
+
+#endif
diff --git a/IR/include/array.h b/IR/include/array.h
index 282e9eb5..f56dc939 100644
--- a/IR/include/array.h
+++ b/IR/include/array.h
@@ -23,4 +23,6 @@ void         __free(void *ptr);
 #define array_for(pos, arr) \
     for (pos = ((typeof(pos))(arr.data)); pos < (typeof(pos))(arr.data) + arr.num_elem; pos++)
 
+#define INIT_ARRAY(type) array_init(sizeof(type))
+
 #endif
diff --git a/IR/include/ir_fun.h b/IR/include/ir_fun.h
index 1763546d..f0434b3f 100644
--- a/IR/include/ir_fun.h
+++ b/IR/include/ir_fun.h
@@ -17,10 +17,15 @@ struct ir_function {
 
     // Stack pointer (r10) users. Should be readonly. No more manual stack access should be allowed.
     struct array sp_users;
+
+    // Array of struct ir_constraint. Value constraints.
+    struct array value_constraints;
 };
 
 // Helper functions
 
+struct ir_function gen_function(struct ssa_transform_env *env);
+
 void clean_env(struct ir_function *);
 
 void clean_id(struct ir_function *);

From 0abe50288ac6880006ddfbed5c0628d9d8dbdc80 Mon Sep 17 00:00:00 2001
From: linsyking <kxiang@umich.edu>
Date: Wed, 17 Jul 2024 00:13:27 -0400
Subject: [PATCH 22/24] feat: add constraint pass

---
 IR/CMakeLists.txt        | 1 +
 IR/add_constraint_pass.c | 4 +++-
 IR/include/passes.h      | 3 ++-
 3 files changed, 6 insertions(+), 2 deletions(-)

diff --git a/IR/CMakeLists.txt b/IR/CMakeLists.txt
index 8d651cf3..8fc5001d 100644
--- a/IR/CMakeLists.txt
+++ b/IR/CMakeLists.txt
@@ -14,6 +14,7 @@ add_executable(
     reachable_bb.c
     add_counter_pass.c
     add_stack_offset.c
+    add_constraint_pass.c
 )
 
 add_executable(probe probe.c read.c array.c)
diff --git a/IR/add_constraint_pass.c b/IR/add_constraint_pass.c
index 73d2eb63..736f7f71 100644
--- a/IR/add_constraint_pass.c
+++ b/IR/add_constraint_pass.c
@@ -7,4 +7,6 @@ void init_test_constraints(struct ir_function *fun) {
     fun->value_constraints = INIT_ARRAY(struct ir_constraint);
 }
 
-void add_constraint(struct ir_function *fun) {}
+void add_constraint(struct ir_function *fun) {
+    init_test_constraints(fun);
+}
diff --git a/IR/include/passes.h b/IR/include/passes.h
index 92431ad7..2a792c5f 100644
--- a/IR/include/passes.h
+++ b/IR/include/passes.h
@@ -1,6 +1,7 @@
 #ifndef __BPF_IR_PASSES_H__
 #define __BPF_IR_PASSES_H__
 
+#include "add_constraint_pass.h"
 #include "phi_pass.h"
 #include "reachable_bb.h"
 #include "add_counter_pass.h"
@@ -10,7 +11,7 @@
     All function passes.
  */
 static void (*passes[])(struct ir_function *fun) = {
-    gen_reachable_bbs, remove_trivial_phi,
+    gen_reachable_bbs, remove_trivial_phi, add_constraint,
     // add_counter,
 };
 

From 9395d8fd466720e4465a24bdf1bc27f648fc8a65 Mon Sep 17 00:00:00 2001
From: linsyking <kxiang@umich.edu>
Date: Wed, 17 Jul 2024 10:45:30 -0400
Subject: [PATCH 23/24] feat: add constraint test pass

---
 IR/add_constraint_pass.c | 32 ++++++++++++++++++++++++++-
 IR/add_counter_pass.c    |  2 +-
 IR/include/bpf_ir.h      | 14 +++++++-----
 IR/include/constraint.h  |  9 ++++----
 IR/include/ir_bb.h       |  1 +
 IR/include/ir_insn.h     | 19 +++++++++++-----
 IR/ir_insn.c             | 47 ++++++++++++++++++++++++++++++----------
 7 files changed, 94 insertions(+), 30 deletions(-)

diff --git a/IR/add_constraint_pass.c b/IR/add_constraint_pass.c
index 736f7f71..08d3dea9 100644
--- a/IR/add_constraint_pass.c
+++ b/IR/add_constraint_pass.c
@@ -1,6 +1,10 @@
 #include "add_constraint_pass.h"
 #include "array.h"
+#include "bpf_ir.h"
 #include "constraint.h"
+#include "dbg.h"
+#include "ir_bb.h"
+#include "ir_insn.h"
 
 // Initialize some testing constraints
 void init_test_constraints(struct ir_function *fun) {
@@ -8,5 +12,31 @@ void init_test_constraints(struct ir_function *fun) {
 }
 
 void add_constraint(struct ir_function *fun) {
-    init_test_constraints(fun);
+    init_test_constraints(fun);  // For testing purpose
+
+    struct ir_basic_block *err_bb = create_bb(fun);
+    struct ir_value        val;
+    val.type                       = IR_VALUE_CONSTANT;
+    val.data.constant_d.type       = IR_CONSTANT_U64;
+    val.data.constant_d.data.u64_d = 1;
+    create_ret_insn_bb(err_bb, val, INSERT_BACK);
+
+    struct ir_constraint *pos;
+    array_for(pos, fun->value_constraints) {
+        struct ir_constraint c = *pos;
+        if (c.type == CONSTRAINT_TYPE_VALUE_EQUAL) {
+            struct ir_basic_block *newbb = split_bb(fun, c.pos);
+            create_jbin_insn(c.pos, c.val, c.cval, newbb, err_bb, IR_INSN_JNE, INSERT_FRONT);
+            connect_bb(c.pos->parent_bb, err_bb);
+        } else if (c.type == CONSTRAINT_TYPE_VALUE_RANGE) {
+            struct ir_basic_block *newbb = split_bb(fun, c.pos);
+            create_jbin_insn(c.pos, c.val, c.start, newbb, err_bb, IR_INSN_JLT, INSERT_FRONT);
+            connect_bb(c.pos->parent_bb, err_bb);
+            struct ir_basic_block *newbb2 = split_bb(fun, c.pos);
+            create_jbin_insn(c.pos, c.val, c.end, newbb2, err_bb, IR_INSN_JGE, INSERT_FRONT);
+            connect_bb(c.pos->parent_bb, err_bb);
+        } else {
+            CRITICAL("Error");
+        }
+    }
 }
diff --git a/IR/add_counter_pass.c b/IR/add_counter_pass.c
index 9cd3d663..49396156 100644
--- a/IR/add_counter_pass.c
+++ b/IR/add_counter_pass.c
@@ -40,7 +40,7 @@ void add_counter(struct ir_function *fun) {
         struct ir_basic_block *new_bb     = split_bb(fun, store_back);
         val2.data.insn_d                  = added;
         val1.data.constant_d.data.u64_d   = 0x10000;
-        create_jlt_insn(store_back, val1, val2, new_bb, err_bb, INSERT_BACK);
+        create_jbin_insn(store_back, val1, val2, new_bb, err_bb, IR_INSN_JLT, INSERT_BACK);
         // Manually connect BBs
         connect_bb(bb, err_bb);
     }
diff --git a/IR/include/bpf_ir.h b/IR/include/bpf_ir.h
index 91dbf052..e736315e 100644
--- a/IR/include/bpf_ir.h
+++ b/IR/include/bpf_ir.h
@@ -143,13 +143,15 @@ enum ir_insn_type {
         | CALL <function id> <arg_num> <values...>
         | RET <value>
         | JA <bb>
-        | JEQ <value>, <value>, <bb>, <bb>
-        | JGT <value>, <value>, <bb>, <bb>
-        | JGE <value>, <value>, <bb>, <bb>
-        | JLT <value>, <value>, <bb>, <bb>
-        | JLE <value>, <value>, <bb>, <bb>
-        | JNE <value>, <value>, <bb>, <bb>
+        | JEQ <value>, <value>, <bb_next>, <bb>
+        | JGT <value>, <value>, <bb_next>, <bb>
+        | JGE <value>, <value>, <bb_next>, <bb>
+        | JLT <value>, <value>, <bb_next>, <bb>
+        | JLE <value>, <value>, <bb_next>, <bb>
+        | JNE <value>, <value>, <bb_next>, <bb>
         | PHI <phi_value>
+    
+    Note. <bb_next> must be the next basic block.
  */
 struct ir_insn {
     struct ir_value values[MAX_FUNC_ARG];
diff --git a/IR/include/constraint.h b/IR/include/constraint.h
index 2deb3a52..aa95ee4e 100644
--- a/IR/include/constraint.h
+++ b/IR/include/constraint.h
@@ -11,15 +11,16 @@ enum constraint_type {
 struct ir_constraint {
     enum constraint_type type;
 
-    // Range: [start, start + size)
-    __u64 start;
-    __u64 size;
+    // Range: [start, end)
+    struct ir_value start;
+    struct ir_value end;
 
     // Constrain value
-    __u64 cval;
+    struct ir_value cval;
 
     // Real value to be compared
     struct ir_value val;
+    struct ir_insn *pos;
 };
 
 #endif
diff --git a/IR/include/ir_bb.h b/IR/include/ir_bb.h
index 60a4c664..d526a73f 100644
--- a/IR/include/ir_bb.h
+++ b/IR/include/ir_bb.h
@@ -13,6 +13,7 @@ void connect_bb(struct ir_basic_block *from, struct ir_basic_block *to);
 
 void disconnect_bb(struct ir_basic_block *from, struct ir_basic_block *to);
 
+/// Split a BB after an instruction
 struct ir_basic_block *split_bb(struct ir_function *fun, struct ir_insn *insn);
 
 struct ir_insn *get_last_insn(struct ir_basic_block *bb);
diff --git a/IR/include/ir_insn.h b/IR/include/ir_insn.h
index 55043d66..09ff74f8 100644
--- a/IR/include/ir_insn.h
+++ b/IR/include/ir_insn.h
@@ -34,13 +34,20 @@ struct ir_insn *create_bin_insn_bb(struct ir_basic_block *bb, struct ir_value va
                                    struct ir_value val2, enum ir_insn_type ty,
                                    enum insert_position pos);
 
-struct ir_insn *create_jlt_insn(struct ir_insn *insn, struct ir_value val1, struct ir_value val2,
-                                struct ir_basic_block *to_bb1, struct ir_basic_block *to_bb2,
-                                enum insert_position pos);
+struct ir_insn *create_ja_insn(struct ir_insn *insn, struct ir_basic_block *to_bb,
+                               enum insert_position pos);
+
+struct ir_insn *create_ja_insn_bb(struct ir_basic_block *bb, struct ir_basic_block *to_bb,
+                                  enum insert_position pos);
+
+struct ir_insn *create_jbin_insn(struct ir_insn *insn, struct ir_value val1, struct ir_value val2,
+                                 struct ir_basic_block *to_bb1, struct ir_basic_block *to_bb2,
+                                 enum ir_insn_type ty, enum insert_position pos);
 
-struct ir_insn *create_jlt_insn_bb(struct ir_basic_block *bb, struct ir_value val1,
-                                   struct ir_value val2, struct ir_basic_block *to_bb1,
-                                   struct ir_basic_block *to_bb2, enum insert_position pos);
+struct ir_insn *create_jbin_insn_bb(struct ir_basic_block *bb, struct ir_value val1,
+                                    struct ir_value val2, struct ir_basic_block *to_bb1,
+                                    struct ir_basic_block *to_bb2, enum ir_insn_type ty,
+                                    enum insert_position pos);
 
 struct ir_insn *create_ret_insn(struct ir_insn *insn, struct ir_value val,
                                 enum insert_position pos);
diff --git a/IR/ir_insn.c b/IR/ir_insn.c
index e524c9e5..c020dedb 100644
--- a/IR/ir_insn.c
+++ b/IR/ir_insn.c
@@ -149,11 +149,32 @@ struct ir_insn *prev_insn(struct ir_insn *insn) {
     return list_entry(prev, struct ir_insn, list_ptr);
 }
 
-struct ir_insn *create_jlt_insn_base(struct ir_basic_block *bb, struct ir_value val1,
-                                     struct ir_value val2, struct ir_basic_block *to_bb1,
-                                     struct ir_basic_block *to_bb2) {
+struct ir_insn *create_ja_insn_base(struct ir_basic_block *bb, struct ir_basic_block *to_bb) {
     struct ir_insn *new_insn = create_insn_base(bb);
-    new_insn->op             = IR_INSN_JLT;
+    new_insn->op             = IR_INSN_JA;
+    new_insn->bb1            = to_bb;
+    return new_insn;
+}
+
+struct ir_insn *create_ja_insn(struct ir_insn *insn, struct ir_basic_block *to_bb,
+                               enum insert_position pos) {
+    struct ir_insn *new_insn = create_ja_insn_base(insn->parent_bb, to_bb);
+    insert_at(new_insn, insn, pos);
+    return new_insn;
+}
+
+struct ir_insn *create_ja_insn_bb(struct ir_basic_block *bb, struct ir_basic_block *to_bb,
+                                  enum insert_position pos) {
+    struct ir_insn *new_insn = create_ja_insn_base(bb, to_bb);
+    insert_at_bb(new_insn, bb, pos);
+    return new_insn;
+}
+
+struct ir_insn *create_jbin_insn_base(struct ir_basic_block *bb, struct ir_value val1,
+                                      struct ir_value val2, struct ir_basic_block *to_bb1,
+                                      struct ir_basic_block *to_bb2, enum ir_insn_type ty) {
+    struct ir_insn *new_insn = create_insn_base(bb);
+    new_insn->op             = ty;
     new_insn->values[0]      = val1;
     new_insn->values[1]      = val2;
     new_insn->bb1            = to_bb1;
@@ -163,18 +184,20 @@ struct ir_insn *create_jlt_insn_base(struct ir_basic_block *bb, struct ir_value
     return new_insn;
 }
 
-struct ir_insn *create_jlt_insn(struct ir_insn *insn, struct ir_value val1, struct ir_value val2,
-                                struct ir_basic_block *to_bb1, struct ir_basic_block *to_bb2,
-                                enum insert_position pos) {
-    struct ir_insn *new_insn = create_jlt_insn_base(insn->parent_bb, val1, val2, to_bb1, to_bb2);
+struct ir_insn *create_jbin_insn(struct ir_insn *insn, struct ir_value val1, struct ir_value val2,
+                                 struct ir_basic_block *to_bb1, struct ir_basic_block *to_bb2,
+                                 enum ir_insn_type ty, enum insert_position pos) {
+    struct ir_insn *new_insn =
+        create_jbin_insn_base(insn->parent_bb, val1, val2, to_bb1, to_bb2, ty);
     insert_at(new_insn, insn, pos);
     return new_insn;
 }
 
-struct ir_insn *create_jlt_insn_bb(struct ir_basic_block *bb, struct ir_value val1,
-                                   struct ir_value val2, struct ir_basic_block *to_bb1,
-                                   struct ir_basic_block *to_bb2, enum insert_position pos) {
-    struct ir_insn *new_insn = create_jlt_insn_base(bb, val1, val2, to_bb1, to_bb2);
+struct ir_insn *create_jbin_insn_bb(struct ir_basic_block *bb, struct ir_value val1,
+                                    struct ir_value val2, struct ir_basic_block *to_bb1,
+                                    struct ir_basic_block *to_bb2, enum ir_insn_type ty,
+                                    enum insert_position pos) {
+    struct ir_insn *new_insn = create_jbin_insn_base(bb, val1, val2, to_bb1, to_bb2, ty);
     insert_at_bb(new_insn, bb, pos);
     return new_insn;
 }

From 0f58417338589c8eabcce7e951d19e0045cd8c4a Mon Sep 17 00:00:00 2001
From: linsyking <kxiang@umich.edu>
Date: Wed, 17 Jul 2024 10:54:56 -0400
Subject: [PATCH 24/24] fix: remove constraint pass

---
 IR/include/passes.h | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/IR/include/passes.h b/IR/include/passes.h
index 2a792c5f..5c0a38a8 100644
--- a/IR/include/passes.h
+++ b/IR/include/passes.h
@@ -11,7 +11,8 @@
     All function passes.
  */
 static void (*passes[])(struct ir_function *fun) = {
-    gen_reachable_bbs, remove_trivial_phi, add_constraint,
+    gen_reachable_bbs, remove_trivial_phi,
+    // add_constraint,
     // add_counter,
 };