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,18 @@
 [![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.
+
+
+## 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 +34,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,10 +162,72 @@ 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, generate C++ for the Fibonacci benchmark:
+
+```sh
+sbt 'runMain genwasym.GenWasym --input benchmarks/wasm/fib.wat --output target/genwasym/fib.cpp --print-result'
+```
+
+The CLI writes C++ source. Build the GenWasym runtime, then compile and link the
+generated program with `libgenwasym.a` and Z3. 
+GenWasym uses Z3 for constraint solving and requires Z3 have been installed. Set `Z3_PREFIX` to the absolute
+path of your Z3 installation, containing `include/` and `lib/`:
+
+```sh
+Z3_PREFIX="/absolute/path/to/z3"
+make -C genwasym_runtime Z3_PREFIX="$Z3_PREFIX"
+
+clang++ -std=c++17 -DUSE_IMM \
+  -Igenwasym_runtime/include -Iheaders -Ithird-party/immer \
+  -I"$Z3_PREFIX/include" \
+  target/genwasym/fib.cpp genwasym_runtime/build/libgenwasym.a \
+  -L"$Z3_PREFIX/lib" -Wl,-rpath,"$Z3_PREFIX/lib" -lz3 \
+  -o target/genwasym/fib
+./target/genwasym/fib
+```
+
+This example prints the result `144` along with runtime statistics. The runtime
+is compiled once and reused across generated programs. Its public headers are
+in `genwasym_runtime/include`. Keep `-DUSE_IMM` consistent between the runtime
+and generated programs because it determines the layout of runtime types; the
+runtime Makefile enables it by default.
+
+Use `--main NAME` to select an exported Wasm function, or omit it to use the
+module's start function.
+
+To compile a directory of `.wat` files, use `--input-dir DIR --output-dir DIR`.
+Add `--recursive` to include subdirectories and preserve their layout in the
+output directory. Scala callers can use `genwasym.GenWasym.compileFile`
+and `compileDirectory` directly.
+
+## Publications
+
+If you would like to mention GenSym in research papers, please cite this paper:
 * 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)  

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();

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{};

headers/wasm/symbolic_decl.hpp

@@ -13,7 +13,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)
@@ -58,8 +58,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)
       : id(id), _width(width), _kind(kind) {}
   int get_id() const { return id; }

headers/wasm/symval_decl.hpp

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

src/main/java/wasm/WatLexer.java → src/main/java/genwasym/WatLexer.java

@@ -1,5 +1,5 @@
 // Generated from WatLexer.g4 by ANTLR 4.13.0
-package gensym.wasm;
+package genwasym;
 import org.antlr.v4.runtime.Lexer;
 import org.antlr.v4.runtime.CharStream;
 import org.antlr.v4.runtime.Token;

src/main/java/wasm/WatParser.java → src/main/java/genwasym/WatParser.java

@@ -1,5 +1,5 @@
 // Generated from WatParser.g4 by ANTLR 4.13.0
-package gensym.wasm;
+package genwasym;
 import org.antlr.v4.runtime.atn.*;
 import org.antlr.v4.runtime.dfa.DFA;
 import org.antlr.v4.runtime.*;

src/main/java/wasm/WatParserBaseListener.java → src/main/java/genwasym/WatParserBaseListener.java

@@ -1,5 +1,5 @@
 // Generated from WatParser.g4 by ANTLR 4.13.0
-package gensym.wasm;
+package genwasym;
 
 import org.antlr.v4.runtime.ParserRuleContext;
 import org.antlr.v4.runtime.tree.ErrorNode;

src/main/java/wasm/WatParserBaseVisitor.java → src/main/java/genwasym/WatParserBaseVisitor.java

@@ -1,5 +1,5 @@
 // Generated from WatParser.g4 by ANTLR 4.13.0
-package gensym.wasm;
+package genwasym;
 import org.antlr.v4.runtime.tree.AbstractParseTreeVisitor;
 
 /**

src/main/java/wasm/WatParserListener.java → src/main/java/genwasym/WatParserListener.java

@@ -1,5 +1,5 @@
 // Generated from WatParser.g4 by ANTLR 4.13.0
-package gensym.wasm;
+package genwasym;
 import org.antlr.v4.runtime.tree.ParseTreeListener;
 
 /**

src/main/java/wasm/WatParserVisitor.java → src/main/java/genwasym/WatParserVisitor.java

@@ -1,5 +1,5 @@
 // Generated from WatParser.g4 by ANTLR 4.13.0
-package gensym.wasm;
+package genwasym;
 import org.antlr.v4.runtime.tree.ParseTreeVisitor;
 
 /**

src/main/scala/wasm/AST.scala → src/main/scala/genwasym/AST.scala

@@ -1,8 +1,8 @@
-package gensym.wasm.ast
+package genwasym.ast
 
 import scala.collection.mutable.HashMap
-import gensym.wasm.miniwasm.ModuleInstance
-import gensym.wasm.source._
+import genwasym.miniwasm.ModuleInstance
+import genwasym.source._
 
 abstract class WIR
 
@@ -33,7 +33,6 @@ case class ElemListExpr(exprs: List[List[Instr]]) extends ElemList
 abstract class FuncField extends WIR
 case class FuncBodyDef(tipe: FuncType, localNames: List[String], locals: List[ValueType], body: List[Instr])
     extends FuncField
-// TODO: FunInline was never used
 case class FunInlineImport(mod: String, name: String, typeUse: Option[Int], imports: Any /*FIXME*/ ) extends FuncField
 case class FunInlineExport(fd: List[FuncDef]) extends FuncField
 
@@ -148,7 +147,6 @@ case class RefFunc(func: Int) extends Instr
 case class CallRef(ty: Int) extends Instr
 
 case class Resume(ty: Int, ons: List[Handler]) extends Instr
-// TODO: make sure this class wants to extend WIR
 case class Handler(tag: Int, label: Int) extends WIR
 
 // resumable try-catch:
@@ -292,17 +290,15 @@ case class ExportGlobal(i: Int) extends ExportDesc
 
 case class Script(cmds: List[Cmd]) extends WIR
 abstract class Cmd extends WIR
-// TODO: can we turn abstract class sealed?
 case class CmdModule(module: Module) extends Cmd
-// TODO: extend if needed
 case class CMdInstnace() extends Cmd
 
 abstract class Action extends Cmd
 case class Invoke(instName: Option[String], name: String, args: List[Value]) extends Action
 
 abstract class Assertion extends Cmd
 case class AssertInvalid() extends Assertion
-case class AssertReturn(action: Action, expect: List[Num] /* TODO: support multiple expect result type*/)
+case class AssertReturn(action: Action, expect: List[Num])
     extends Assertion
 case class AssertTrap(action: Action, message: String) extends Assertion
 
@@ -347,4 +343,3 @@ case class RefExternV(externAddr: Int) extends Ref {
 }
 
 case class RTGlobal(ty: GlobalType, var value: Value)
-

src/main/scala/wasm/ConcolicDriver.scala → src/main/scala/genwasym/ConcolicDriver.scala

@@ -1,9 +1,9 @@
-package gensym.wasm.concolicdriver
+package genwasym.concolicdriver
 
-import gensym.wasm.concolicminiwasm._
-import gensym.wasm.ast._
-import gensym.wasm.parser._
-import gensym.wasm.symbolic._
+import genwasym.concolicminiwasm._
+import genwasym.ast._
+import genwasym.parser._
+import genwasym.symbolic._
 
 import scala.collection.immutable.Queue
 import scala.collection.mutable.{HashMap, HashSet}

src/main/scala/wasm/ConcolicMemory.scala → src/main/scala/genwasym/ConcolicMemory.scala

@@ -1,7 +1,7 @@
-package gensym.wasm.concolicmemory
+package genwasym.concolicmemory
 
-import gensym.wasm.symbolic._
-import gensym.wasm.ast._
+import genwasym.symbolic._
+import genwasym.ast._
 
 import scala.collection.mutable.HashMap