Readme update & Cleanup

.github/workflows/scala.yml

@@ -81,8 +81,8 @@ jobs:
         sbt 'testOnly gensym.TestImpCPSGS_Z3'
         sbt 'testOnly gensym.TestLibrary'
         sbt 'testOnly gensym.CoverageGraphTest'
-        sbt 'testOnly gensym.wasm.TestEval'
-        sbt 'testOnly gensym.wasm.TestScriptRun'
-        sbt 'testOnly gensym.wasm.TestConcolic'
-        sbt 'testOnly gensym.wasm.TestDriver'
-        sbt 'testOnly gensym.wasm.TestStagedConcolicEval'
+        sbt 'testOnly genwasym.TestEval'
+        sbt 'testOnly genwasym.TestScriptRun'
+        sbt 'testOnly genwasym.TestConcolic'
+        sbt 'testOnly genwasym.TestDriver'
+        sbt 'testOnly genwasym.TestStagedConcolicEval'

README.md

@@ -1,8 +1,27 @@
 [![Scala CI](https://github.com/Generative-Program-Analysis/GenSym/actions/workflows/scala.yml/badge.svg?branch=main)](https://github.com/Generative-Program-Analysis/GenSym/actions/workflows/scala.yml)
 
-# GenSym
+# GenSym: Generative Symbolic Execution
 
-GenSym is a high-performance, parallel symbolic execution engine for LLVM IR.
+GenSym project is a tool set for **Gen**erative **Sym**bolic execution. There
+are two tools in the GenSym:
+
+1. `GenSym`: A symbolic execution engine for LLVM IR programs.
+2. `GenWasym`: A concolic execution engine for WebAssembly programs.
+
+Both tools achieve high performance by the usage of advanced compiler
+technologies and applying continuations for different optimization.
+
+## Table of contents
+
+- [GenSym](#gensym---symbolic-execution-engine-for-llvm-ir)
+  - [Usage of GenSym](#usage-of-gensym)
+  - [Demonstration](#demonstration)
+  - [Precompiled native runtime](#precompiled-native-runtime)
+- [GenWasym](#genwasym---concolic-execution-engine-for-webassembly)
+  - [Usage of GenWasym](#usage-of-genwasym)
+- [Publications](#publications)
+
+## GenSym - Symbolic Execution Engine for LLVM IR
 
 - GenSym's high performance is achieved by making use of advanced
 compiler technologies that given an input LLVM IR program, it
@@ -24,7 +43,7 @@ of real-world programs (e.g. programs from GNU Coreutils).
 See our [ICSE 2023 paper](https://continuation.passing.style/static/papers/icse23.pdf) 
 for detailed evaluation.
 
-### Usage
+### Usage of GenSym
 
 The easiest way to try GenSym is to use the Docker image we build for the [accompanying ICSE 23 artifact](https://github.com/Generative-Program-Analysis/icse23-artifact-evaluation), which has all dependencies installed.
 
@@ -152,15 +171,142 @@ play with it, you can check those options by `./branch --help`.
 
 The generated tests and an archived log file can be found under `gensym-DDMMYYYY-HHMMSS/tests` for further inspection.
 
-### Publications
 
-If you would like to mention GenSym in research papers, please cite this paper:
+## GenWasym - Concolic Execution Engine for WebAssembly
+
+- GenWasym achieves efficient concolic execution of WebAssembly by compiling the
+WebAssembly program to an optimized C++ code that performs concolic execution.
+Unlike interpretative implementations, the C++ code generated by GenWasym does
+not need to constantly dispatch on different WebAssembly instructions, thus it
+is free of interpretation overhead.
+
+- Using the generated C++ code in continuation-passing style, GenWasym
+can efficiently support snapshot reuse, a technique that allows the concolic
+execution engine to reuse a previous execution state (snapshot) to avoid
+re-executing the same instructions.
+
+GenWasym has an accompanying evaluated artifact available on
+[Zenodo](https://doi.org/10.5281/zenodo.21517229).
+
+### Usage of GenWasym
+
+Run the GenWasym CLI from the repository root:
+
+```sh
+sbt 'runMain genwasym.GenWasym --help'
+```
+
+For example, [the test case](benchmarks/wasm/concolic-branch.wat) explores
+different paths through a function with two symbolic integer inputs.
+
+The `real_main` wrapper creates the symbolic inputs by `i32.symbolic` and calls
+`f`. The complete WAT source is:
+
+```wat
+(module
+  (type (func (param i32 i32) (result i32)))
+  (type (func (result i32)))
+
+  ;; Parameters 0 and 1 are x and y.
+  (func $f (type 0) (param i32 i32) (result i32)
+    ;; if (x <= 0 || y <= 0) return -1;
+    ;; Short-circuit: test y only when x > 0.
+    local.get 0
+    i32.const 0
+    i32.le_s
+    if (result i32)
+      i32.const -1  ;; x <= 0: return -1.
+    else
+      local.get 1
+      i32.const 0
+      i32.le_s
+      if (result i32)
+        i32.const -1  ;; x > 0 and y <= 0: return -1.
+      else
+        ;; if (x * x + y * y == 25) return 1;
+        local.get 0
+        local.get 0
+        i32.mul
+        local.get 1
+        local.get 1
+        i32.mul
+        i32.add
+        i32.const 25
+        i32.eq
+        if (result i32)
+          i32.const 1  ;; The sum of squares is 25: return 1.
+        else
+          i32.const 0  ;; Otherwise, return 0.
+        end
+      end
+    end)
+
+  (func $real_main (type 1) (result i32)
+    ;; Create symbolic x with identifier 0.
+    i32.const 0
+    i32.symbolic
+    ;; Create symbolic y with identifier 1.
+    i32.const 1
+    i32.symbolic
+    call 0)  ;; Call f(x, y).
+
+  (export "real_main" (func 1)))
+```
 
+Generate C++ for the concolic execution, selecting `real_main` as the entrypoint:
+
+```sh
+sbt 'runMain genwasym.GenWasym --input benchmarks/wasm/concolic-branch.wat --output target/genwasym/branch.cpp --main real_main --print-result'
+```
+
+Build the runtime, then compile and link the generated C++ with `libgenwasym.a`
+and Z3. Set `Z3_PREFIX` to your Z3 installation directory (containing `include/`
+and `lib/`):
+
+```sh
+# Build the runtime library.
+Z3_PREFIX="/absolute/path/to/z3"
+make -C genwasym_runtime Z3_PREFIX="$Z3_PREFIX"
+# Compile and link the generated C++ code with the runtime library and Z3.
+clang++ -std=c++17 -DUSE_IMM \
+  -Igenwasym_runtime/include -Iheaders -Ithird-party/immer \
+  -I"$Z3_PREFIX/include" \
+  target/genwasym/branch.cpp genwasym_runtime/build/libgenwasym.a \
+  -L"$Z3_PREFIX/lib" -Wl,-rpath,"$Z3_PREFIX/lib" -lz3 \
+  -o target/genwasym/branch
+./target/genwasym/branch
+```
+
+Running the executable explores four paths with no failures. Example output:
+
+```text
+...
+Execution finished successfully
+Explore Tree Overall Result:
+  Unexplored paths: 0
+  Finished paths: 4
+  Failed paths: 0
+  Unreachable paths: 0
+  NotToExplore paths: 0
+Number of calls to solver: 7
+Execution Kind Summary:
+Total RESTART executions: 1
+Total FROMSNAPSHOT executions: 3
+```
+
+## Publications
+
+If you would like to mention GenSym/GenWasym in research papers, please cite the following papers:
 * Compiling Parallel Symbolic Execution with Continuations  
   Guannan Wei, Songlin Jia, Ruiqi Gao, Haotian Deng, Shangyin Tan, Oliver Bračevac, Tiark Rompf  
   The 45th International Conference on Software Engineering (ICSE 2023)  
   [PDF](https://continuation.passing.style/static/papers/icse23.pdf)
 
+* Compiling WebAssembly Concolic Execution with Staging, Continuations, and Snapshots  
+  Dinghong Zhong, Alexander Bai, Mikail Khan, Guannan Wei  
+  Proceedings of the ACM on Programming Languages, Volume 10 (OOPSLA 2026)  
+  [PDF](https://continuation.passing.style/static/papers/zhong26.pdf)
+
 Other related publications:
 
 * Towards Partially Evaluating Symbolic Interpreters for All  

benchmarks/wasm/concolic-branch.wat

@@ -0,0 +1,48 @@
+(module
+  (type (func (param i32 i32) (result i32)))
+  (type (func (result i32)))
+
+  ;; Parameters 0 and 1 are x and y.
+  (func $f (type 0) (param i32 i32) (result i32)
+    ;; if (x <= 0 || y <= 0) return -1;
+    ;; Short-circuit: test y only when x > 0.
+    local.get 0
+    i32.const 0
+    i32.le_s
+    if (result i32)
+      i32.const -1  ;; x <= 0: return -1.
+    else
+      local.get 1
+      i32.const 0
+      i32.le_s
+      if (result i32)
+        i32.const -1  ;; x > 0 and y <= 0: return -1.
+      else
+        ;; if (x * x + y * y == 25) return 1;
+        local.get 0
+        local.get 0
+        i32.mul
+        local.get 1
+        local.get 1
+        i32.mul
+        i32.add
+        i32.const 25
+        i32.eq
+        if (result i32)
+          i32.const 1  ;; The sum of squares is 25: return 1.
+        else
+          i32.const 0  ;; Otherwise, return 0.
+        end
+      end
+    end)
+
+  (func $real_main (type 1) (result i32)
+    ;; Create symbolic x with identifier 0.
+    i32.const 0
+    i32.symbolic
+    ;; Create symbolic y with identifier 1.
+    i32.const 1
+    i32.symbolic
+    call 0)  ;; Call f(x, y).
+
+  (export "real_main" (func 1)))

genwasym_runtime/Makefile

@@ -1,12 +1,18 @@
 CXX = clang++
 
-CXXFLAGS = -std=c++17 -Wall -Iinclude -I../headers -I../third-party/immer -I../third-party/z3/build/z3_install/usr/local/include -fPIC -DUSE_IMM
+CXXFLAGS = -std=c++17 -Wall -Iinclude -I../headers -I../third-party/immer -fPIC -DUSE_IMM
 
 BUILD_DIR = build
 
-Z3_LIB_DIR = ../third-party/z3/build/z3_install/usr/local/lib
+Z3_PREFIX ?=
+Z3_INCLUDE_DIR ?= $(if $(strip $(Z3_PREFIX)),$(Z3_PREFIX)/include)
+Z3_LIB_DIR ?= $(if $(strip $(Z3_PREFIX)),$(Z3_PREFIX)/lib)
 
-LDFLAGS = -L$(Z3_LIB_DIR) -Wl,-rpath,$(Z3_LIB_DIR)
+Z3_CPPFLAGS = $(if $(strip $(Z3_INCLUDE_DIR)),-I"$(Z3_INCLUDE_DIR)")
+Z3_LDFLAGS =
+ifneq ($(strip $(Z3_LIB_DIR)),)
+Z3_LDFLAGS = -L"$(Z3_LIB_DIR)" -Wl,-rpath,"$(Z3_LIB_DIR)"
+endif
 
 LDLIBS = -lz3
 
@@ -34,13 +40,13 @@ $(BUILD_DIR):
 	mkdir -p $(BUILD_DIR)
 
 $(BUILD_DIR)/%.o: lib/%.cpp | $(BUILD_DIR)
-	$(CXX) $(CXXFLAGS) -MMD -MP -c $< -o $@
+	$(CXX) $(CPPFLAGS) $(Z3_CPPFLAGS) $(CXXFLAGS) -MMD -MP -c $< -o $@
 
 $(STATIC_LIB): $(OBJ)
 	ar rcs $(STATIC_LIB) $(OBJ)
 
 $(SHARED_LIB): $(OBJ)
-	$(CXX) -shared $(SHARED_PLATFORM_FLAGS) $(LDFLAGS) -o $(SHARED_LIB) $(OBJ) $(LDLIBS)
+	$(CXX) -shared $(SHARED_PLATFORM_FLAGS) $(LDFLAGS) $(Z3_LDFLAGS) -o $(SHARED_LIB) $(OBJ) $(LDLIBS)
 
 -include $(OBJ:.o=.d)
 

genwasym_runtime/include/wasm/heap_mem_bookkeeper.hpp

@@ -4,10 +4,6 @@
 #include <memory>
 #include <set>
 
-// Todo: remove this later, this is just a workaround to make sure that the
-// SymVals' memory will not be freed during the main execution.
-// We can leave the SymVal's memory unmanaged if reference counting is not
-// performant
 template <typename T> struct MemBookKeeper {
   std::set<std::shared_ptr<T>> allocated;
 
@@ -21,4 +17,4 @@ template <typename T> struct MemBookKeeper {
   void clear() { allocated.clear(); }
 };
 
-#endif // HEAP_MEM_BOOKKEEPER_HPP
+#endif // HEAP_MEM_BOOKKEEPER_HPP

genwasym_runtime/include/wasm/symbolic.hpp

@@ -17,7 +17,7 @@ enum BinOperation {
   DIV_U,    // Unsigned division
   AND,      // Logical AND
   OR,       // Logical OR
-  EQ_BOOL,  // Equal (return a boolean) TODO: remove bv version of comparison ops
+  EQ_BOOL,  // Equal (return a boolean)
   NEQ_BOOL, // Not equal (return a boolean)
   LT_BOOL,  // Less than (return a boolean)
   LTU_BOOL, // Unsigned less than (return a boolean)
@@ -63,8 +63,6 @@ class Symbolic {
 
 class Symbol : public Symbolic {
 public:
-  // TODO: add type information to determine the size of bitvector
-  // for now we just assume that only i32 will be used
   Symbol(int id, int width, ValueKind kind);
 
   int get_id() const;

genwasym_runtime/include/wasm/symval.hpp

@@ -66,7 +66,6 @@ struct SymVal {
   // only for i32 symbolic values, extend to i64 by sign extension
   SymVal extend_to_i64() const;
 
-  // TODO: add bitwise operations, and use the underlying bitvector theory
   bool is_concrete() const;
 
   static SymVal get_witness_symbol();

genwasym_runtime/lib/symval_factory.cpp

@@ -430,7 +430,7 @@ SymVal make_binary(BinOperation op, const SymVal &lhs, const SymVal &rhs) {
     return result;
   }
 
-  if ((op == GT_BOOL || op == LT_BOOL || NEQ_BOOL) && lhs == rhs) {
+  if ((op == GT_BOOL || op == LT_BOOL || op == NEQ_BOOL) && lhs == rhs) {
     auto result = SVFactory::make_concrete_bool(false);
     BinaryOperationStore.insert({key, result});
     return result;
@@ -639,4 +639,4 @@ SymVal make_concat(const SymVal &lhs, const SymVal &rhs) {
   return SVFactory::make_binary(CONCAT, lhs, rhs);
 }
 
-} // namespace SVFactory
+} // namespace SVFactory

grammar/Makefile

@@ -3,9 +3,9 @@ ANTLR4 = antlr-4.13.0-complete.jar
 
 CURRENT_DIR := $(shell pwd)
 LLVM_OUTPUT = $(CURRENT_DIR)/../src/main/java/llvm
-WASM_OUTPUT = $(CURRENT_DIR)/../src/main/java/wasm
+WASM_OUTPUT = $(CURRENT_DIR)/../src/main/java/genwasym
 LLVM_PACKAGE = gensym.llvm
-WASM_PACKAGE = gensym.wasm
+WASM_PACKAGE = genwasym
 
 llvm:
 	java -jar $(ANTLR4) -o $(LLVM_OUTPUT) -package $(LLVM_PACKAGE) LLVMLexer.g4

headers/wasm/heap_mem_bookkeeper.hpp

@@ -4,10 +4,6 @@
 #include <memory>
 #include <set>
 
-// Todo: remove this later, this is just a workaround to make sure that the
-// SymVals' memory will not be freed during the main execution.
-// We can leave the SymVal's memory unmanaged if reference counting is not
-// performant
 template <typename T> struct MemBookKeeper {
   std::set<std::shared_ptr<T>> allocated;
 
@@ -21,4 +17,4 @@ template <typename T> struct MemBookKeeper {
   void clear() { allocated.clear(); }
 };
 
-#endif // HEAP_MEM_BOOKKEEPER_HPP
+#endif // HEAP_MEM_BOOKKEEPER_HPP

headers/wasm/smt_solver.hpp

@@ -73,8 +73,7 @@ struct GroupResult {
 };
 
 static std::optional<int> group_of_symval(const SymVal &sym, UnionFind &uf) {
-  // TODO: This process is un optimized and slow, just want to see if the idea
-  // of independent resolving works
+  // Group symbols connected by an expression for independent constraint solving.
   if (auto symbol = dynamic_cast<Symbol *>(sym.symptr.get())) {
     return symbol->get_id();
   } else if (auto concrete = dynamic_cast<SymConcrete *>(sym.symptr.get())) {
@@ -101,9 +100,7 @@ static std::optional<int> group_of_symval(const SymVal &sym, UnionFind &uf) {
 }
 
 static VectorGroupMap build_group_map(const std::vector<SymVal> &conditions) {
-  // TODO: This is a slow temporary solution which only used for validating the
-  // idea of independent constraint resolving, the intermediate result of
-  // independent solving is reusable
+  // Build independent groups of constraints. Grouping is recomputed on each call.
   ManagedTimer timer(TimeProfileKind::SPLIT_CONDITIONS);
   if (conditions.empty()) {
     return VectorGroupMap{};