Generative-Program-Analysis · Kraks · Aug 15, 2026 · Jul 24, 2026 · Aug 15, 2026 · Aug 15, 2026
diff --git a/.devcontainer/Dockerfile b/.devcontainer/Dockerfile
@@ -57,8 +57,12 @@ RUN apt-get update && apt-get install -y --no-install-recommends \
         perl \
         minisat \
         clang-11 \
+        llvm-11 \
         unzip \
         build-essential \
+    && if [ "$(dpkg --print-architecture)" != "amd64" ]; then \
+         apt-get install -y --no-install-recommends libc6-dev-amd64-cross; \
+       fi \
     && rm -rf /var/lib/apt/lists/*
 
 # ── Rust (required for third-party/wasmfx-tools) ─────────────────────────────

diff --git a/.github/workflows/scala.yml b/.github/workflows/scala.yml
@@ -32,7 +32,7 @@ jobs:
       run: |
         sudo apt-get update
         sudo DEBIAN_FRONTEND=noninteractive apt-get install -y git g++ cmake bison flex libboost-all-dev 2to3 python-is-python3
-        sudo DEBIAN_FRONTEND=noninteractive apt-get install -y perl minisat curl gnupg2 locales clang-11 wget
+        sudo DEBIAN_FRONTEND=noninteractive apt-get install -y perl minisat curl gnupg2 locales clang-11 llvm-11 wget
     - name: Generate test files (LLVM IR)
       run: |
         cd benchmarks/llvm

diff --git a/.gitignore b/.gitignore
@@ -12,6 +12,7 @@
 .vscode
 .bsp
 target
+runtime/build/
 klee-out-*
 gs_gen
 output

diff --git a/README.md b/README.md
@@ -127,6 +127,26 @@ This steps generates the executable `branch`, then running the executable file p
 ```
 
 The generated executable file also has several runtime options.
+
+### Precompiled native runtime
+
+The active LLVM ImpCPS backend links generated programs with
+`runtime/build/libgensym_runtime.a`.  The public generated-code interface is the
+standard-library-only header `headers/gensym/runtime.hpp`; Immer, solver details,
+the filesystem model, scheduler, and monitor implementation are compiled once
+inside the runtime archive.
+
+Build the runtime explicitly with:
+
+```sh
+make -C runtime
+```
+
+Generated Makefiles also invoke this incremental build automatically.  If the
+runtime sources and private headers are unchanged, subsequent generated programs
+reuse the existing archive without recompiling it.  `make clean` in a generated
+program removes only that program.  To force a runtime rebuild, run
+`make -C runtime clean all` from the repository root.
 For most of users, it suffices to use the default options. However if you would like to
 play with it, you can check those options by `./branch --help`.
 

diff --git a/benchmarks/demo-benchmarks/Makefile b/benchmarks/demo-benchmarks/Makefile
@@ -1,6 +1,6 @@
 SRC_FILES := $(wildcard ./*.c)
 
-CC := clang-11
+include ../llvm-toolchain.mk
 
 FLAGS := -emit-llvm -O0 -Xclang -disable-O0-optnone -c
 KLEE_FLAGS := -D KLEE -g -I $(KLEE_INCL)
@@ -21,13 +21,13 @@ klee: $(KLEE_TARGET)
 klee-exe: $(KLEE_REPLAY_TARGET)
 
 $(KLEE_TARGET): %.bc : %.c
-	$(CC) $(KLEE_FLAGS) $(FLAGS) -o $@ $<
+	$(LLVM_CC) $(KLEE_FLAGS) $(FLAGS) -o $@ $<
 
 $(KLEE_REPLAY_TARGET): %-replay : %.c
 	$(CC) $(KLEE_FLAGS) -o $@ $< -lkleeRuntest
 
 $(GS_TARGET): %.ll : %.c
-	$(CC) $(GS_FLAGS) $(FLAGS) -o $@ $<
+	$(LLVM_CC) $(GS_FLAGS) $(FLAGS) -o $@ $<
 
 clean:
 	$(RM) -rf $(KLEE_TARGET) $(KLEE_REPLAY_TARGET) $(KLEE_GEN) $(GS_TARGET)
diff --git a/benchmarks/external-lib/Makefile b/benchmarks/external-lib/Makefile
@@ -1,6 +1,6 @@
 SRC_FILES := $(wildcard ./*.c)
 
-CC := clang-11
+include ../llvm-toolchain.mk
 
 FLAGS := -emit-llvm -O0 -Xclang -disable-O0-optnone -c -S
 KLEE_FLAGS := -D KLEE -g
@@ -21,13 +21,13 @@ klee: $(KLEE_TARGET)
 klee-exe: $(KLEE_REPLAY_TARGET)
 
 $(KLEE_TARGET): %-klee.ll : %.c
-	$(CC) $(KLEE_FLAGS) $(FLAGS) -o $@ $<
+	$(LLVM_CC) $(KLEE_FLAGS) $(FLAGS) -o $@ $<
 
 $(KLEE_REPLAY_TARGET): %-replay : %.c
 	$(CC) $(KLEE_FLAGS) -o $@ $< -lkleeRuntest
 
 $(GS_TARGET): %.ll : %.c
-	$(CC) $(GS_FLAGS) $(FLAGS) -o $@ $<
+	$(LLVM_CC) $(GS_FLAGS) $(FLAGS) -o $@ $<
 
 clean:
 	$(RM) -rf $(KLEE_TARGET) $(KLEE_REPLAY_TARGET) $(KLEE_GEN) $(GS_TARGET) *.ll
diff --git a/benchmarks/klee-examples/Makefile b/benchmarks/klee-examples/Makefile
@@ -1,13 +1,14 @@
 SRC_FILES := $(wildcard ./*.c)
+include ../llvm-toolchain.mk
 
 all:
 	for SRC in $(SRC_FILES) ; do \
-	  clang-11 $$SRC -O0 -emit-llvm -S -fno-discard-value-names ; \
+	  $(LLVM_CC) $$SRC -O0 -emit-llvm -S -fno-discard-value-names ; \
 	done
 
 allO1:
 	for SRC in $(SRC_FILES) ; do \
-	  clang-11 $$SRC -O1 -emit-llvm -S -fno-discard-value-names -D__NO_STRING_INLINES  -D_FORTIFY_SOURCE=0 -U__OPTIMIZE__ ; \
+	  $(LLVM_CC) $$SRC -O1 -emit-llvm -S -fno-discard-value-names -D__NO_STRING_INLINES  -D_FORTIFY_SOURCE=0 -U__OPTIMIZE__ ; \
 	done
 
 clean:

diff --git a/benchmarks/klee-posix-fs/Makefile b/benchmarks/klee-posix-fs/Makefile
@@ -1,6 +1,6 @@
 SRC_FILES := $(wildcard ./fd_init.c ./fd.c ./fd_64.c  ./gensym.c  ./test.c)
 
-CC := clang-11
+include ../llvm-toolchain.mk
 
 FLAGS := -emit-llvm -O0 -disable-O0-optnone -c
 #FLAGS := -emit-llvm -Os -c
@@ -24,7 +24,7 @@ gensym: $(GS_LINK_TARGET)
 #klee-exe: $(KLEE_REPLAY_TARGET)
 
 $(GS_TARGET): %.ll : %.c
-	$(CC) $(GS_FLAGS) $(FLAGS) -o $@ $<
+	$(LLVM_CC) $(GS_FLAGS) $(FLAGS) -o $@ $<
 
 $(GS_LINK_TARGET): $(GS_TARGET)
 	llvm-link-11 -S $(GS_TARGET) -o klee_lib_64.ll

diff --git a/benchmarks/llvm-toolchain.mk b/benchmarks/llvm-toolchain.mk
@@ -0,0 +1,18 @@
+# GenSym models the x86-64 Linux ABI. Keep LLVM input on that ABI while
+# compiling the generated C++ runtime natively for the host architecture.
+GENSYM_HOST_ARCH ?= $(shell uname -m)
+GENSYM_LLVM_TARGET ?= x86_64-unknown-linux-gnu
+GENSYM_LLVM_SYSROOT ?= /usr/x86_64-linux-gnu
+
+CC := clang-11
+
+ifneq ($(filter x86_64 amd64,$(GENSYM_HOST_ARCH)),)
+LLVM_TARGET_FLAGS :=
+else
+ifeq ($(wildcard $(GENSYM_LLVM_SYSROOT)/include),)
+$(error Missing x86-64 cross headers at $(GENSYM_LLVM_SYSROOT)/include; rebuild the devcontainer)
+endif
+LLVM_TARGET_FLAGS := --target=$(GENSYM_LLVM_TARGET) --sysroot=$(GENSYM_LLVM_SYSROOT)
+endif
+
+LLVM_CC = $(CC) $(LLVM_TARGET_FLAGS)
diff --git a/benchmarks/llvm/Makefile b/benchmarks/llvm/Makefile
@@ -1,6 +1,6 @@
 SRC_FILES := $(wildcard ./*.c)
 
-CC := clang-11
+include ../llvm-toolchain.mk
 
 FLAGS := -emit-llvm -O0 -Xclang -disable-O0-optnone -c
 KLEE_FLAGS := -D KLEE -g -I $(KLEE_INCL)
@@ -21,13 +21,13 @@ klee: $(KLEE_TARGET)
 klee-exe: $(KLEE_REPLAY_TARGET)
 
 $(KLEE_TARGET): %.bc : %.c
-	$(CC) $(KLEE_FLAGS) $(FLAGS) -o $@ $<
+	$(LLVM_CC) $(KLEE_FLAGS) $(FLAGS) -o $@ $<
 
 $(KLEE_REPLAY_TARGET): %-replay : %.c
 	$(CC) $(KLEE_FLAGS) -o $@ $< -lkleeRuntest
 
 $(GS_TARGET): %.ll : %.c
-	$(CC) $(GS_FLAGS) $(FLAGS) -o $@ $<
+	$(LLVM_CC) $(GS_FLAGS) $(FLAGS) -o $@ $<
 
 clean:
 	$(RM) -rf $(KLEE_TARGET) $(KLEE_REPLAY_TARGET) $(KLEE_GEN) $(GS_TARGET) *.ll
diff --git a/benchmarks/llvm/new_multipath/Makefile b/benchmarks/llvm/new_multipath/Makefile
@@ -1,13 +1,14 @@
+include ../../llvm-toolchain.mk
+
 all:
-	clang multi_path_1024_sym.c -g -O0 -emit-llvm -S -fno-discard-value-names -o multi_path_1024_sym.ll
-	clang multi_path_65536_sym.c -g -O0 -emit-llvm -S -fno-discard-value-names -o multi_path_65536_sym.ll
-	clang multi_path_1048576_sym.c -g -O0 -emit-llvm -S -fno-discard-value-names -o multi_path_1048576_sym.ll
-	clang -I /home/kraks/research/klee_experiment/klee-2.1/include -g -Xclang -disable-O0-optnone -c -emit-llvm multi_path_1024_klee.c -o multi_path_1024_klee.bc
-	clang -I /home/kraks/research/klee_experiment/klee-2.1/include -g -Xclang -disable-O0-optnone -c -emit-llvm multi_path_65536_klee.c -o multi_path_65536_klee.bc
-	clang -I /home/kraks/research/klee_experiment/klee-2.1/include -g -Xclang -disable-O0-optnone -c -emit-llvm multi_path_65536_klee_single.c -o multi_path_65536_klee_single.bc
-	clang -I /home/kraks/research/klee_experiment/klee-2.1/include -g -Xclang -disable-O0-optnone -c -emit-llvm multi_path_1048576_klee.c -o multi_path_1048576_klee.bc
+	$(LLVM_CC) multi_path_1024_sym.c -g -O0 -emit-llvm -S -fno-discard-value-names -o multi_path_1024_sym.ll
+	$(LLVM_CC) multi_path_65536_sym.c -g -O0 -emit-llvm -S -fno-discard-value-names -o multi_path_65536_sym.ll
+	$(LLVM_CC) multi_path_1048576_sym.c -g -O0 -emit-llvm -S -fno-discard-value-names -o multi_path_1048576_sym.ll
+	$(LLVM_CC) -I $(KLEE_INCL) -g -Xclang -disable-O0-optnone -c -emit-llvm multi_path_1024_klee.c -o multi_path_1024_klee.bc
+	$(LLVM_CC) -I $(KLEE_INCL) -g -Xclang -disable-O0-optnone -c -emit-llvm multi_path_65536_klee.c -o multi_path_65536_klee.bc
+	$(LLVM_CC) -I $(KLEE_INCL) -g -Xclang -disable-O0-optnone -c -emit-llvm multi_path_65536_klee_single.c -o multi_path_65536_klee_single.bc
+	$(LLVM_CC) -I $(KLEE_INCL) -g -Xclang -disable-O0-optnone -c -emit-llvm multi_path_1048576_klee.c -o multi_path_1048576_klee.bc
 
 clean:
 	rm *.bc
 	rm *.ll
-
diff --git a/benchmarks/oopsla20/Makefile b/benchmarks/oopsla20/Makefile
@@ -1,20 +1,20 @@
 KLEE_INCLUDE = ../../../../klee_experiment/klee-2.1/include
+include ../llvm-toolchain.mk
 
 all: generate_sse
 
 generate_sse:
-	clang-11 multipath_1024_sym.c -O0 -emit-llvm -S -fno-discard-value-names -o multipath_1024_sym.ll
-	clang-11 multipath_65536_sym.c -O0 -emit-llvm -S -fno-discard-value-names -o multipath_65536_sym.ll
-	clang-11 multipath_1048576_sym.c -O0 -emit-llvm -S -fno-discard-value-names -o multipath_1048576_sym.ll
-	clang-11 maze_test.c -O0 -emit-llvm -S -fno-discard-value-names -o maze_test.ll
+	$(LLVM_CC) multipath_1024_sym.c -O0 -emit-llvm -S -fno-discard-value-names -o multipath_1024_sym.ll
+	$(LLVM_CC) multipath_65536_sym.c -O0 -emit-llvm -S -fno-discard-value-names -o multipath_65536_sym.ll
+	$(LLVM_CC) multipath_1048576_sym.c -O0 -emit-llvm -S -fno-discard-value-names -o multipath_1048576_sym.ll
+	$(LLVM_CC) maze_test.c -O0 -emit-llvm -S -fno-discard-value-names -o maze_test.ll
 
 generate_klee:
-	clang-11 -I $(KLEE_INCLUDE) -g -Xclang -disable-O0-optnone -c -emit-llvm multipath_1024_klee.c -o multipath_1024_klee.bc
-	clang-11 -I $(KLEE_INCLUDE) -g -Xclang -disable-O0-optnone -c -emit-llvm multipath_65536_klee.c -o multipath_65536_klee.bc
-	clang-11 -I $(KLEE_INCLUDE) -g -Xclang -disable-O0-optnone -c -emit-llvm multipath_1048576_klee.c -o multipath_1048576_klee.bc
-	clang-11 -I $(KLEE_INCLUDE) -g -Xclang -disable-O0-optnone -c -emit-llvm maze_test_klee.c -o maze_test_klee.bc
+	$(LLVM_CC) -I $(KLEE_INCLUDE) -g -Xclang -disable-O0-optnone -c -emit-llvm multipath_1024_klee.c -o multipath_1024_klee.bc
+	$(LLVM_CC) -I $(KLEE_INCLUDE) -g -Xclang -disable-O0-optnone -c -emit-llvm multipath_65536_klee.c -o multipath_65536_klee.bc
+	$(LLVM_CC) -I $(KLEE_INCLUDE) -g -Xclang -disable-O0-optnone -c -emit-llvm multipath_1048576_klee.c -o multipath_1048576_klee.bc
+	$(LLVM_CC) -I $(KLEE_INCLUDE) -g -Xclang -disable-O0-optnone -c -emit-llvm maze_test_klee.c -o maze_test_klee.bc
 
 clean:
 	rm *.bc
 	rm *.ll
-
diff --git a/benchmarks/opt-experiments/Makefile b/benchmarks/opt-experiments/Makefile
@@ -1,6 +1,6 @@
 SRC_FILES := $(wildcard ./*.c)
 
-CC := clang-11
+include ../llvm-toolchain.mk
 
 FLAGS := -emit-llvm -O0 -Xclang -disable-O0-optnone -c
 KLEE_FLAGS := -D KLEE -g -I $(KLEE_INCL)
@@ -21,13 +21,13 @@ klee: $(KLEE_TARGET)
 klee-exe: $(KLEE_REPLAY_TARGET)
 
 $(KLEE_TARGET): %.bc : %.c
-	$(CC) $(KLEE_FLAGS) $(FLAGS) -o $@ $<
+	$(LLVM_CC) $(KLEE_FLAGS) $(FLAGS) -o $@ $<
 
 $(KLEE_REPLAY_TARGET): %-replay : %.c
 	$(CC) $(KLEE_FLAGS) -o $@ $< -lkleeRuntest
 
 $(GS_TARGET): %.ll : %.c
-	$(CC) $(GS_FLAGS) $(FLAGS) -o $@ $<
+	$(LLVM_CC) $(GS_FLAGS) $(FLAGS) -o $@ $<
 
 clean:
 	$(RM) -rf $(KLEE_TARGET) $(KLEE_REPLAY_TARGET) $(KLEE_GEN) $(GS_TARGET)
diff --git a/benchmarks/pepm22/ccbse/Makefile b/benchmarks/pepm22/ccbse/Makefile
@@ -1,15 +1,16 @@
 SRC_FILES := $(wildcard ./*.c)
 KLEE_INCLUDE := ../../../../klee_experiment/klee-2.1/include
+include ../../llvm-toolchain.mk
 all: llsc
 
 llsc:
 	for SRC in $(SRC_FILES) ; do \
-	  clang-11 $$SRC -O0 -emit-llvm -S -disable-O0-optnone -fno-discard-value-names ; \
+	  $(LLVM_CC) $$SRC -O0 -emit-llvm -S -disable-O0-optnone -fno-discard-value-names ; \
 	done
 
 klee:
 	for SRC in $(SRC_FILES) ; do \
-		clang-11 -D KLEE -I $(KLEE_INCLUDE) -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone $$SRC ; \
+		$(LLVM_CC) -D KLEE -I $(KLEE_INCLUDE) -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone $$SRC ; \
 	done
 
 clean:

diff --git a/benchmarks/pepm22/concolic/conc/Makefile b/benchmarks/pepm22/concolic/conc/Makefile
@@ -1,9 +1,10 @@
 SRC_FILES := $(wildcard ./*.c)
+include ../../../llvm-toolchain.mk
 all: llsc
 
 llsc:
 	for SRC in $(SRC_FILES) ; do \
-	  clang-11 $$SRC -O0 -emit-llvm -S -disable-O0-optnone -fno-discard-value-names ; \
+	  $(LLVM_CC) $$SRC -O0 -emit-llvm -S -disable-O0-optnone -fno-discard-value-names ; \
 	done
 
 clean:

diff --git a/benchmarks/perf-mon/Makefile b/benchmarks/perf-mon/Makefile
@@ -1,6 +1,6 @@
 SRC_FILES := $(wildcard ./*.c)
 
-CC := clang-11
+include ../llvm-toolchain.mk
 
 FLAGS := -emit-llvm -O0 -Xclang -disable-O0-optnone -c
 KLEE_FLAGS := -D KLEE -g -I $(KLEE_INCL)
@@ -21,13 +21,13 @@ klee: $(KLEE_TARGET)
 klee-exe: $(KLEE_REPLAY_TARGET)
 
 $(KLEE_TARGET): %.bc : %.c
-	$(CC) $(KLEE_FLAGS) $(FLAGS) -o $@ $<
+	$(LLVM_CC) $(KLEE_FLAGS) $(FLAGS) -o $@ $<
 
 $(KLEE_REPLAY_TARGET): %-replay : %.c
 	$(CC) $(KLEE_FLAGS) -o $@ $< -lkleeRuntest
 
 $(GS_TARGET): %.ll : %.c Makefile
-	$(CC) $(GS_FLAGS) $(FLAGS) -o $@ $<
+	$(LLVM_CC) $(GS_FLAGS) $(FLAGS) -o $@ $<
 
 clean:
 	$(RM) -rf $(KLEE_TARGET) $(KLEE_REPLAY_TARGET) $(KLEE_GEN) $(GS_TARGET)
diff --git a/benchmarks/test-comp/array-examples/Makefile b/benchmarks/test-comp/array-examples/Makefile
@@ -1,6 +1,6 @@
 SRC_FILES := $(wildcard ./*.c)
 
-CC := clang-11
+include ../../llvm-toolchain.mk
 
 FLAGS := -emit-llvm -O2 -Xclang -disable-O0-optnone -c -fno-vectorize
 GS_FLAGS := -fno-discard-value-names -S
@@ -12,7 +12,7 @@ all: gensym
 gensym: $(GS_TARGET)
 
 $(GS_TARGET): %.ll : %.c
-	$(CC) $(GS_FLAGS) $(FLAGS) -o $@ $<
+	$(LLVM_CC) $(GS_FLAGS) $(FLAGS) -o $@ $<
 
 clean:
 	$(RM) -rf $(GS_TARGET)
diff --git a/benchmarks/test-comp/array-programs/Makefile b/benchmarks/test-comp/array-programs/Makefile
@@ -1,6 +1,6 @@
 SRC_FILES := $(wildcard ./*.c)
 
-CC := clang-11
+include ../../llvm-toolchain.mk
 
 FLAGS := -emit-llvm -O2 -Xclang -disable-O0-optnone -c -fno-vectorize
 GS_FLAGS := -fno-discard-value-names -S
@@ -12,7 +12,7 @@ all: gensym
 gensym: $(GS_TARGET)
 
 $(GS_TARGET): %.ll : %.c
-	$(CC) $(GS_FLAGS) $(FLAGS) -o $@ $<
+	$(LLVM_CC) $(GS_FLAGS) $(FLAGS) -o $@ $<
 
 clean:
 	$(RM) -rf $(GS_TARGET)
diff --git a/headers/gensym/auxiliary.hpp b/headers/gensym/auxiliary.hpp
@@ -22,15 +22,15 @@
 #   define ASSERT(condition, message) do { } while (false)
 #endif
 
-#ifdef DEBUG
-#   define INFO(message) \
-    do { \
+inline bool runtime_debug = false;
+#undef INFO
+#define INFO(message) \
+  do { \
+    if (runtime_debug) { \
       std::cout << "[Info] " << __FILE__ << " line " << __LINE__ \
                 << ": " << message << std::endl; \
-    } while (false)
-#else
-#   define INFO(message) do { } while (false)
-#endif
+    } \
+  } while (false)
 
 #define MAX(a, b) ((a) > (b)) ? (a) : (b)
 #define MIN(a, b) ((a) < (b)) ? (a) : (b)
@@ -129,9 +129,7 @@ inline uint32_t rand_uint32() {
 
 inline int rand_int(int ub) {
   int r =  (rng32() % ub) + 1; // [1, ub]
-#ifdef DEBUG
-  std::cout << "Generate a rand number: " << r << std::endl;
-#endif
+  if (runtime_debug) std::cout << "Generate a rand number: " << r << std::endl;
   return r;
 }
 

diff --git a/headers/gensym/branch.hpp b/headers/gensym/branch.hpp
@@ -228,7 +228,9 @@ sym_exec_br_k(SS& ss, unsigned int block_id, PtrVal t_cond, PtrVal f_cond,
               std::function<std::monostate(SS&, std::function<std::monostate(SS&, PtrVal)>)> tf,
               std::function<std::monostate(SS&, std::function<std::monostate(SS&, PtrVal)>)> ff,
               std::function<std::monostate(SS&, PtrVal)> k) {
+  INFO("Before solver call");
   auto [tbr_sat, fbr_sat] = check_branch(ss.get_PC(), t_cond);
+  INFO("After solver call");
   if ((tbr_sat == solver_result::sat) && (fbr_sat == solver_result::sat)) {
     // both branches are sat
     cov().inc_path(1);
-Original file line number
+Diff line change
@@ Expand Up / @@ -12,6 +12,7 @@ @@
     .vscode
     .bsp
     target
+    runtime/build/
     klee-out-*
     gs_gen
     output
@@ Expand Down @@