diff --git a/.github/workflows/scala.yml b/.github/workflows/scala.yml index 1d86e7632..c23aa14c2 100644 --- a/.github/workflows/scala.yml +++ b/.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' diff --git a/README.md b/README.md index f168077eb..f29c1a4a7 100644 --- a/README.md +++ b/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) diff --git a/genwasym_runtime/Makefile b/genwasym_runtime/Makefile index 5cc6772a3..4a577a126 100644 --- a/genwasym_runtime/Makefile +++ b/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) diff --git a/genwasym_runtime/include/wasm/heap_mem_bookkeeper.hpp b/genwasym_runtime/include/wasm/heap_mem_bookkeeper.hpp index c4cc7313f..801af5007 100644 --- a/genwasym_runtime/include/wasm/heap_mem_bookkeeper.hpp +++ b/genwasym_runtime/include/wasm/heap_mem_bookkeeper.hpp @@ -4,10 +4,6 @@ #include #include -// 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 struct MemBookKeeper { std::set> allocated; @@ -21,4 +17,4 @@ template struct MemBookKeeper { void clear() { allocated.clear(); } }; -#endif // HEAP_MEM_BOOKKEEPER_HPP \ No newline at end of file +#endif // HEAP_MEM_BOOKKEEPER_HPP diff --git a/genwasym_runtime/include/wasm/symbolic.hpp b/genwasym_runtime/include/wasm/symbolic.hpp index e0079297c..3c4de5957 100644 --- a/genwasym_runtime/include/wasm/symbolic.hpp +++ b/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; diff --git a/genwasym_runtime/include/wasm/symval.hpp b/genwasym_runtime/include/wasm/symval.hpp index afe15eee3..ec0a8f2f2 100644 --- a/genwasym_runtime/include/wasm/symval.hpp +++ b/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(); diff --git a/grammar/Makefile b/grammar/Makefile index e079ec24f..4045d1776 100644 --- a/grammar/Makefile +++ b/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 diff --git a/headers/wasm/heap_mem_bookkeeper.hpp b/headers/wasm/heap_mem_bookkeeper.hpp index c4cc7313f..801af5007 100644 --- a/headers/wasm/heap_mem_bookkeeper.hpp +++ b/headers/wasm/heap_mem_bookkeeper.hpp @@ -4,10 +4,6 @@ #include #include -// 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 struct MemBookKeeper { std::set> allocated; @@ -21,4 +17,4 @@ template struct MemBookKeeper { void clear() { allocated.clear(); } }; -#endif // HEAP_MEM_BOOKKEEPER_HPP \ No newline at end of file +#endif // HEAP_MEM_BOOKKEEPER_HPP diff --git a/headers/wasm/smt_solver.hpp b/headers/wasm/smt_solver.hpp index 08d3ea4c0..4c805a1e6 100644 --- a/headers/wasm/smt_solver.hpp +++ b/headers/wasm/smt_solver.hpp @@ -73,8 +73,7 @@ struct GroupResult { }; static std::optional 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(sym.symptr.get())) { return symbol->get_id(); } else if (auto concrete = dynamic_cast(sym.symptr.get())) { @@ -101,9 +100,7 @@ static std::optional group_of_symval(const SymVal &sym, UnionFind &uf) { } static VectorGroupMap build_group_map(const std::vector &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{}; diff --git a/headers/wasm/symbolic_decl.hpp b/headers/wasm/symbolic_decl.hpp index 22bd4c03a..07dc924e5 100644 --- a/headers/wasm/symbolic_decl.hpp +++ b/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; } diff --git a/headers/wasm/symval_decl.hpp b/headers/wasm/symval_decl.hpp index b3739692b..d9adeb560 100644 --- a/headers/wasm/symval_decl.hpp +++ b/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; diff --git a/src/main/java/wasm/WatLexer.java b/src/main/java/genwasym/WatLexer.java similarity index 99% rename from src/main/java/wasm/WatLexer.java rename to src/main/java/genwasym/WatLexer.java index 960bbdddf..d70b7a3de 100644 --- a/src/main/java/wasm/WatLexer.java +++ b/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; diff --git a/src/main/java/wasm/WatParser.java b/src/main/java/genwasym/WatParser.java similarity index 99% rename from src/main/java/wasm/WatParser.java rename to src/main/java/genwasym/WatParser.java index 62e5f40b7..dfb5cbf0b 100644 --- a/src/main/java/wasm/WatParser.java +++ b/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.*; diff --git a/src/main/java/wasm/WatParserBaseListener.java b/src/main/java/genwasym/WatParserBaseListener.java similarity index 99% rename from src/main/java/wasm/WatParserBaseListener.java rename to src/main/java/genwasym/WatParserBaseListener.java index df9be1847..c03d469e5 100644 --- a/src/main/java/wasm/WatParserBaseListener.java +++ b/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; diff --git a/src/main/java/wasm/WatParserBaseVisitor.java b/src/main/java/genwasym/WatParserBaseVisitor.java similarity index 99% rename from src/main/java/wasm/WatParserBaseVisitor.java rename to src/main/java/genwasym/WatParserBaseVisitor.java index 8631f4f33..1d45638df 100644 --- a/src/main/java/wasm/WatParserBaseVisitor.java +++ b/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; /** diff --git a/src/main/java/wasm/WatParserListener.java b/src/main/java/genwasym/WatParserListener.java similarity index 99% rename from src/main/java/wasm/WatParserListener.java rename to src/main/java/genwasym/WatParserListener.java index 96c38c0f5..8374d262b 100644 --- a/src/main/java/wasm/WatParserListener.java +++ b/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; /** diff --git a/src/main/java/wasm/WatParserVisitor.java b/src/main/java/genwasym/WatParserVisitor.java similarity index 99% rename from src/main/java/wasm/WatParserVisitor.java rename to src/main/java/genwasym/WatParserVisitor.java index 61713ea07..c4cf163cb 100644 --- a/src/main/java/wasm/WatParserVisitor.java +++ b/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; /** diff --git a/src/main/scala/wasm/AST.scala b/src/main/scala/genwasym/AST.scala similarity index 97% rename from src/main/scala/wasm/AST.scala rename to src/main/scala/genwasym/AST.scala index 60cf0c4fb..76b203bc3 100644 --- a/src/main/scala/wasm/AST.scala +++ b/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,9 +290,7 @@ 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 @@ -302,7 +298,7 @@ case class Invoke(instName: Option[String], name: String, args: List[Value]) ext 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) - diff --git a/src/main/scala/wasm/ConcolicDriver.scala b/src/main/scala/genwasym/ConcolicDriver.scala similarity index 97% rename from src/main/scala/wasm/ConcolicDriver.scala rename to src/main/scala/genwasym/ConcolicDriver.scala index 42f9707aa..8f62556ec 100644 --- a/src/main/scala/wasm/ConcolicDriver.scala +++ b/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} diff --git a/src/main/scala/wasm/ConcolicMemory.scala b/src/main/scala/genwasym/ConcolicMemory.scala similarity index 95% rename from src/main/scala/wasm/ConcolicMemory.scala rename to src/main/scala/genwasym/ConcolicMemory.scala index f6e29c4c9..9d2fae04a 100644 --- a/src/main/scala/wasm/ConcolicMemory.scala +++ b/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 diff --git a/src/main/scala/wasm/ConcolicMiniWasm.scala b/src/main/scala/genwasym/ConcolicMiniWasm.scala similarity index 99% rename from src/main/scala/wasm/ConcolicMiniWasm.scala rename to src/main/scala/genwasym/ConcolicMiniWasm.scala index fec869fea..cf6e7edf8 100644 --- a/src/main/scala/wasm/ConcolicMiniWasm.scala +++ b/src/main/scala/genwasym/ConcolicMiniWasm.scala @@ -1,11 +1,11 @@ -package gensym.wasm.concolicminiwasm - -import gensym.wasm.ast._ -import gensym.wasm.source._ -// import gensym.wasm.memory._ -import gensym.wasm.concolicmemory._ -import gensym.wasm.symbolic._ -import gensym.wasm.parser._ +package genwasym.concolicminiwasm + +import genwasym.ast._ +import genwasym.source._ +// import genwasym.memory._ +import genwasym.concolicmemory._ +import genwasym.symbolic._ +import genwasym.parser._ import scala.util.Random diff --git a/src/main/scala/genwasym/GenWasym.scala b/src/main/scala/genwasym/GenWasym.scala new file mode 100644 index 000000000..941fa1422 --- /dev/null +++ b/src/main/scala/genwasym/GenWasym.scala @@ -0,0 +1,199 @@ +package genwasym + +import java.nio.charset.StandardCharsets +import java.nio.file.{Files, Path, Paths} + +import scala.collection.JavaConverters._ +import scala.util.control.NonFatal + +import genwasym.miniwasm.ModuleInstance +import genwasym.parser.Parser +import genwasym.stagedconcolicminiwasm.WasmToCppCompiler + +/** Public Scala and command-line entry point for the GenWasym compiler. */ +object GenWasym { + final case class CliConfig( + input: Option[Path] = None, + inputDir: Option[Path] = None, + output: Option[Path] = None, + outputDir: Option[Path] = None, + mainExport: Option[String] = None, + printResult: Boolean = false, + recursive: Boolean = false) + + val usage: String = + """Usage: + | GenWasym --input FILE [--output FILE | --output-dir DIR] + | [--main EXPORT] [--print-result] + | + | GenWasym --input-dir DIR --output-dir DIR [--recursive] + | [--main EXPORT] [--print-result] + | + |Options: + | -i, --input FILE Compile one WebAssembly text file. + | --input-dir DIR Compile every .wat file in a directory. + | -o, --output FILE C++ output path for a single input file. + | --output-dir DIR Directory for generated C++ files. + | -m, --main EXPORT Use this exported Wasm function as the entry. + | Without it, use the module start function. + | --recursive Recurse below --input-dir and preserve layout. + | --print-result Emit generated code that prints the final stack. + | -h, --help Show this help. + |""".stripMargin + + /** + * Parse one `.wat` file, stage the concolic evaluator, and write C++. + * + * @return the normalized path of the generated C++ file + */ + def compileFile( + input: Path, + output: Option[Path] = None, + mainExport: Option[String] = None, + printResult: Boolean = false): Path = { + val inputPath = input.toAbsolutePath.normalize + if (!Files.isRegularFile(inputPath)) { + throw new IllegalArgumentException(s"Input is not a file: $inputPath") + } + if (!inputPath.getFileName.toString.endsWith(".wat")) { + throw new IllegalArgumentException(s"Input must be a .wat file: $inputPath") + } + + val outputPath = output + .map(_.toAbsolutePath.normalize) + .getOrElse(Paths.get(inputPath.toString + ".cpp")) + Option(outputPath.getParent).foreach(path => Files.createDirectories(path)) + + println(s"Parsing WebAssembly text: $inputPath") + val ast = Parser.parseFile(inputPath.toString) + val moduleInstance = ModuleInstance(ast) + + println(s"Staging concolic executor with entry: ${mainExport.getOrElse("")}") + val generated = WasmToCppCompiler.compile(moduleInstance, mainExport, printResult) + + Files.write(outputPath, generated.source.getBytes(StandardCharsets.UTF_8)) + println(s"Generated C++: $outputPath") + outputPath + } + + /** Compile a directory of `.wat` files, optionally recursively. */ + def compileDirectory( + inputDir: Path, + outputDir: Path, + mainExport: Option[String] = None, + printResult: Boolean = false, + recursive: Boolean = false): Seq[Path] = { + val inputRoot = inputDir.toAbsolutePath.normalize + val outputRoot = outputDir.toAbsolutePath.normalize + if (!Files.isDirectory(inputRoot)) { + throw new IllegalArgumentException(s"Input directory does not exist: $inputRoot") + } + Files.createDirectories(outputRoot) + + val paths = if (recursive) Files.walk(inputRoot) else Files.list(inputRoot) + val inputs = try { + paths.iterator.asScala + .filter(path => Files.isRegularFile(path) && path.getFileName.toString.endsWith(".wat")) + .toVector + .sortBy(_.toString) + } finally { + paths.close() + } + + if (inputs.isEmpty) { + throw new IllegalArgumentException(s"No .wat files found in: $inputRoot") + } + + inputs.map { inputPath => + val relative = inputRoot.relativize(inputPath) + val outputPath = outputRoot.resolve(relative.toString + ".cpp") + compileFile(inputPath, Some(outputPath), mainExport, printResult) + } + } + + private def parseArgs(args: List[String], config: CliConfig = CliConfig()): Either[String, CliConfig] = + args match { + case Nil => Right(config) + case ("--input" | "-i") :: value :: rest => + parseArgs(rest, config.copy(input = Some(Paths.get(value)))) + case "--input-dir" :: value :: rest => + parseArgs(rest, config.copy(inputDir = Some(Paths.get(value)))) + case ("--output" | "-o") :: value :: rest => + parseArgs(rest, config.copy(output = Some(Paths.get(value)))) + case "--output-dir" :: value :: rest => + parseArgs(rest, config.copy(outputDir = Some(Paths.get(value)))) + case ("--main" | "-m") :: value :: rest => + parseArgs(rest, config.copy(mainExport = Some(value))) + case "--print-result" :: rest => + parseArgs(rest, config.copy(printResult = true)) + case "--recursive" :: rest => + parseArgs(rest, config.copy(recursive = true)) + case option :: Nil if Set("--input", "-i", "--input-dir", "--output", "-o", "--output-dir", "--main", "-m").contains(option) => + Left(s"Missing value for $option") + case unknown :: _ => Left(s"Unknown argument: $unknown") + } + + private def compile(config: CliConfig): Either[String, Seq[Path]] = + (config.input, config.inputDir) match { + case (Some(_), Some(_)) => + Left("Use either --input or --input-dir, not both") + case (None, None) => + Left("Missing --input or --input-dir") + case (Some(input), None) => + if (config.output.nonEmpty && config.outputDir.nonEmpty) { + Left("Use either --output or --output-dir, not both") + } else if (config.recursive) { + Left("--recursive requires --input-dir") + } else { + val output = config.output.orElse(config.outputDir.map { directory => + directory.resolve(input.getFileName.toString + ".cpp") + }) + Right(Seq(compileFile(input, output, config.mainExport, config.printResult))) + } + case (None, Some(inputDir)) => + if (config.output.nonEmpty) { + Left("--output is only valid with --input; use --output-dir") + } else { + config.outputDir match { + case None => Left("--input-dir requires --output-dir") + case Some(outputDir) => + Right(compileDirectory( + inputDir, + outputDir, + config.mainExport, + config.printResult, + config.recursive)) + } + } + } + + def main(args: Array[String]): Unit = { + if (args.contains("--help") || args.contains("-h")) { + println(usage) + return + } + + parseArgs(args.toList) match { + case Left(message) => + Console.err.println(s"GenWasym: $message") + Console.err.println(usage) + System.exit(2) + case Right(config) => + try { + compile(config) match { + case Left(message) => + Console.err.println(s"GenWasym: $message") + Console.err.println(usage) + System.exit(2) + case Right(outputs) => + println(s"Compiled ${outputs.size} WebAssembly file(s).") + } + } catch { + case NonFatal(error) => + val detail = Option(error.getMessage).getOrElse(error.getClass.getSimpleName) + Console.err.println(s"GenWasym compilation failed: $detail") + System.exit(1) + } + } + } +} diff --git a/src/main/scala/wasm/Memory.scala b/src/main/scala/genwasym/Memory.scala similarity index 99% rename from src/main/scala/wasm/Memory.scala rename to src/main/scala/genwasym/Memory.scala index fed359773..0fd9fe1c3 100644 --- a/src/main/scala/wasm/Memory.scala +++ b/src/main/scala/genwasym/Memory.scala @@ -1,4 +1,4 @@ -package gensym.wasm.memory +package genwasym.memory import scala.collection.mutable.ArrayBuffer diff --git a/src/main/scala/wasm/MiniWasm.scala b/src/main/scala/genwasym/MiniWasm.scala similarity index 99% rename from src/main/scala/wasm/MiniWasm.scala rename to src/main/scala/genwasym/MiniWasm.scala index 4b672bd4f..29ed7db0c 100644 --- a/src/main/scala/wasm/MiniWasm.scala +++ b/src/main/scala/genwasym/MiniWasm.scala @@ -1,8 +1,8 @@ -package gensym.wasm.miniwasm +package genwasym.miniwasm -import gensym.wasm.ast._ -import gensym.wasm.source._ -import gensym.wasm.memory._ +import genwasym.ast._ +import genwasym.source._ +import genwasym.memory._ import scala.collection.mutable.ArrayBuffer import scala.collection.mutable.HashMap diff --git a/src/main/scala/wasm/MiniWasmScript.scala b/src/main/scala/genwasym/MiniWasmScript.scala similarity index 95% rename from src/main/scala/wasm/MiniWasmScript.scala rename to src/main/scala/genwasym/MiniWasmScript.scala index c9bd50185..7d6506270 100644 --- a/src/main/scala/wasm/MiniWasmScript.scala +++ b/src/main/scala/genwasym/MiniWasmScript.scala @@ -1,7 +1,7 @@ -package gensym.wasm.miniwasmscript +package genwasym.miniwasmscript -import gensym.wasm.miniwasm._ -import gensym.wasm.ast._ +import genwasym.miniwasm._ +import genwasym.ast._ import scala.collection.mutable.{ListBuffer, Map, ArrayBuffer} sealed class ScriptRunner { diff --git a/src/main/scala/wasm/Parser.scala b/src/main/scala/genwasym/Parser.scala similarity index 98% rename from src/main/scala/wasm/Parser.scala rename to src/main/scala/genwasym/Parser.scala index 9206451c8..5f3cc89ab 100644 --- a/src/main/scala/wasm/Parser.scala +++ b/src/main/scala/genwasym/Parser.scala @@ -1,7 +1,7 @@ -package gensym.wasm.parser +package genwasym.parser -import gensym.wasm.ast._ -import gensym.wasm.source._ +import genwasym.ast._ +import genwasym.source._ import scala.util.Try import scala.util.parsing.combinator._ @@ -13,7 +13,7 @@ import org.antlr.v4.runtime._ import scala.collection.JavaConverters._ import collection.mutable.{HashMap, ListBuffer} -import gensym.wasm._ +import genwasym._ import java.io.OutputStream @@ -149,7 +149,7 @@ class GSWasmVisitor extends WatParserBaseVisitor[WIR] { if (ctx.defType.FUNC != null) { TypeDef(getVar(ctx.bindVar()), visit(ctx.defType.funcType).asInstanceOf[FuncType]) } else if (ctx.defType.CONT != null) { - // TODO: here, the getVar is more link the typeUse one, although it uses the IdxContext one + // The index refers to the function type used by the continuation. TypeDef(getVar(ctx.bindVar()), ContType(getVar(ctx.defType.idx).toInt)) } else { error @@ -293,7 +293,6 @@ class GSWasmVisitor extends WatParserBaseVisitor[WIR] { F32V(parsedValue) case F64Type => - // TODO: not processed at all val parsedValue = ctx.FLOAT.getText.toDouble F64V(parsedValue) } @@ -771,8 +770,6 @@ class GSWasmVisitor extends WatParserBaseVisitor[WIR] { else error } - // TODO: we instantiate the module no matter what, might want to change the - // behavior in the future override def visitScriptModule(ctx: ScriptModuleContext): Module = { if (ctx.module_ != null) { visitModule_(ctx.module_).asInstanceOf[Module] diff --git a/src/main/scala/wasm/Source.scala b/src/main/scala/genwasym/Source.scala similarity index 86% rename from src/main/scala/wasm/Source.scala rename to src/main/scala/genwasym/Source.scala index f54f3030d..685c2167a 100644 --- a/src/main/scala/wasm/Source.scala +++ b/src/main/scala/genwasym/Source.scala @@ -1,4 +1,4 @@ -package gensym.wasm.source +package genwasym.source import scala.util.parsing.input.{Positional, Position} diff --git a/src/main/scala/wasm/StagedConcolicMiniWasm.scala b/src/main/scala/genwasym/StagedConcolicMiniWasm.scala similarity index 99% rename from src/main/scala/wasm/StagedConcolicMiniWasm.scala rename to src/main/scala/genwasym/StagedConcolicMiniWasm.scala index c7fad9a8b..3aecdbec8 100644 --- a/src/main/scala/wasm/StagedConcolicMiniWasm.scala +++ b/src/main/scala/genwasym/StagedConcolicMiniWasm.scala @@ -1,4 +1,4 @@ -package gensym.wasm.stagedconcolicminiwasm +package genwasym.stagedconcolicminiwasm import scala.collection.mutable.{ArrayBuffer, HashMap} @@ -10,13 +10,13 @@ import lms.core.Backend._ import lms.core.Backend.{Block => LMSBlock, Const => LMSConst} import lms.core.Graph -import gensym.wasm.ast._ -import gensym.wasm.ast.{Const => WasmConst, Block => WasmBlock} -import gensym.wasm.miniwasm.{ModuleInstance} -import gensym.wasm.symbolic.{SymVal} +import genwasym.ast._ +import genwasym.ast.{Const => WasmConst, Block => WasmBlock} +import genwasym.miniwasm.{ModuleInstance} +import genwasym.symbolic.{SymVal} import gensym.lmsx.{SAIDriver, StringOps, SAIOps, SAICodeGenBase, CppSAIDriver, CppSAICodeGenBase} -import gensym.wasm.symbolic.Concrete -import gensym.wasm.symbolic.ExploreTree +import genwasym.symbolic.Concrete +import genwasym.symbolic.ExploreTree import gensym.structure.freer.Explore object Counter { @@ -1754,7 +1754,6 @@ trait StagedWasmEvaluator extends SAIOps } // When moving the cursor to a branch, we mark another branch as // snapshotNode (this is done by moveCursor's runtime implementation) - // TODO: store snapshot into this snapshot node def thnK: Rep[Cont[Unit]] = topFun((_: Rep[Unit]) => { info(s"Entering the true branch $id of the br_table") Stack.popC(ty) @@ -2025,7 +2024,7 @@ trait StagedWasmEvaluator extends SAIOps case Mul(_) => v1 * v2 case Sub(_) => v1 - v2 case Shl(_) => v1 << v2 - case ShrS(_) => v1 shrS v2 // TODO: signed shift right + case ShrS(_) => v1 shrS v2 case ShrU(_) => v1 shrU v2 case And(_) => v1 & v2 case DivS(_) => v1 divs v2 @@ -2050,7 +2049,7 @@ trait StagedWasmEvaluator extends SAIOps case Mul(_) => v1 * v2 case Sub(_) => v1 - v2 case Shl(_) => v1 << v2 - case ShrS(_) => v1 shrS v2 // TODO: signed shift right + case ShrS(_) => v1 shrS v2 case ShrU(_) => v1 shrU v2 case And(_) => v1 & v2 case DivS(_) => v1 divs v2 diff --git a/src/main/scala/wasm/StagedMiniWasm.scala b/src/main/scala/genwasym/StagedMiniWasm.scala similarity index 99% rename from src/main/scala/wasm/StagedMiniWasm.scala rename to src/main/scala/genwasym/StagedMiniWasm.scala index ea9dc9c6f..2f050bcc3 100644 --- a/src/main/scala/wasm/StagedMiniWasm.scala +++ b/src/main/scala/genwasym/StagedMiniWasm.scala @@ -1,4 +1,4 @@ -package gensym.wasm.stagedminiwasm +package genwasym.stagedminiwasm import scala.collection.mutable.{ArrayBuffer, HashMap} @@ -10,9 +10,9 @@ import lms.core.Backend._ import lms.core.Backend.{Block => LMSBlock, Const => LMSConst} import lms.core.Graph -import gensym.wasm.ast._ -import gensym.wasm.ast.{Const => WasmConst, Block => WasmBlock} -import gensym.wasm.miniwasm.ModuleInstance +import genwasym.ast._ +import genwasym.ast.{Const => WasmConst, Block => WasmBlock} +import genwasym.miniwasm.ModuleInstance import gensym.lmsx.{SAIDriver, StringOps, SAIOps, SAICodeGenBase, CppSAIDriver, CppSAICodeGenBase} @virtualize diff --git a/src/main/scala/wasm/Symbolic.scala b/src/main/scala/genwasym/Symbolic.scala similarity index 98% rename from src/main/scala/wasm/Symbolic.scala rename to src/main/scala/genwasym/Symbolic.scala index c2333fa0d..fa8b323e3 100644 --- a/src/main/scala/wasm/Symbolic.scala +++ b/src/main/scala/genwasym/Symbolic.scala @@ -1,5 +1,5 @@ -package gensym.wasm.symbolic -import gensym.wasm.ast._ +package genwasym.symbolic +import genwasym.ast._ import z3.scala._ import scala.collection.mutable.HashMap diff --git a/src/main/scala/wasm/attic/Eval.scala b/src/main/scala/genwasym/attic/Eval.scala similarity index 99% rename from src/main/scala/wasm/attic/Eval.scala rename to src/main/scala/genwasym/attic/Eval.scala index 6cff3a0e2..4ec218d09 100644 --- a/src/main/scala/wasm/attic/Eval.scala +++ b/src/main/scala/genwasym/attic/Eval.scala @@ -1,9 +1,9 @@ /* -package gensym.wasm.eval +package genwasym.eval -import gensym.wasm.ast._ -import gensym.wasm.source._ -import gensym.wasm.memory._ +import genwasym.ast._ +import genwasym.source._ +import genwasym.memory._ import scala.collection.mutable.ArrayBuffer diff --git a/src/main/scala/wasm/attic/LearnStaging.scala b/src/main/scala/genwasym/attic/LearnStaging.scala similarity index 99% rename from src/main/scala/wasm/attic/LearnStaging.scala rename to src/main/scala/genwasym/attic/LearnStaging.scala index 2c4273ff9..83bce4d46 100644 --- a/src/main/scala/wasm/attic/LearnStaging.scala +++ b/src/main/scala/genwasym/attic/LearnStaging.scala @@ -1,4 +1,4 @@ -package gensym.wasm.learnstaging +package genwasym.learnstaging import lms.core.stub._ import lms.macros.SourceContext diff --git a/src/main/scala/wasm/attic/NewStagedEvalCPS.scala b/src/main/scala/genwasym/attic/NewStagedEvalCPS.scala similarity index 98% rename from src/main/scala/wasm/attic/NewStagedEvalCPS.scala rename to src/main/scala/genwasym/attic/NewStagedEvalCPS.scala index 31fdec929..e523e4a68 100644 --- a/src/main/scala/wasm/attic/NewStagedEvalCPS.scala +++ b/src/main/scala/genwasym/attic/NewStagedEvalCPS.scala @@ -1,12 +1,12 @@ -package gensym.wasm.newstagedevalcps +package genwasym.newstagedevalcps import scala.collection.mutable.HashMap -import gensym.wasm.ast.{Const => Konst, _} -//import gensym.wasm.values.{I32 => I32C} -//import gensym.wasm.types._ -import gensym.wasm.memory._ -//import gensym.wasm.globals._ +import genwasym.ast.{Const => Konst, _} +//import genwasym.values.{I32 => I32C} +//import genwasym.types._ +import genwasym.memory._ +//import genwasym.globals._ import lms.core._ import lms.core.stub._ @@ -384,7 +384,7 @@ trait StagedEvalCPS extends SAIOps { } // Numeric Instructions - case gensym.wasm.ast.Const(I32V(n)) => { + case genwasym.ast.Const(I32V(n)) => { State.pushStack(I32(n)) k(ss, kk) } @@ -680,7 +680,7 @@ object StagedEvalCPSTest extends App { val module = { val file = scala.io.Source.fromFile("./benchmarks/wasm/test_rs.wat").mkString - gensym.wasm.parser.Parser.parse(file) + genwasym.parser.Parser.parse(file) } val moduleInst = { diff --git a/src/main/scala/wasm/attic/StagedEval.scala b/src/main/scala/genwasym/attic/StagedEval.scala similarity index 98% rename from src/main/scala/wasm/attic/StagedEval.scala rename to src/main/scala/genwasym/attic/StagedEval.scala index 7677f2ae1..d38f2cdf8 100644 --- a/src/main/scala/wasm/attic/StagedEval.scala +++ b/src/main/scala/genwasym/attic/StagedEval.scala @@ -1,12 +1,12 @@ -package gensym.wasm.stagedeval +package genwasym.stagedeval /* -//import gensym.wasm.ast.{Const => Konst, _} -//import gensym.wasm.values.{I32 => I32C} -import gensym.wasm.types._ -import gensym.wasm.memory._ -import gensym.wasm.globals._ +//import genwasym.ast.{Const => Konst, _} +//import genwasym.values.{I32 => I32C} +import genwasym.types._ +import genwasym.memory._ +import genwasym.globals._ import lms.core._ import lms.core.stub._ @@ -216,7 +216,7 @@ trait StagedEval extends SAIOps { } // Numeric Instructions - case gensym.wasm.ast.Const(I32V(n)) => this.eval(state.withStack(I32(n) :: stack), instrs.tail) + case genwasym.ast.Const(I32V(n)) => this.eval(state.withStack(I32(n) :: stack), instrs.tail) case Binary(op) => { val (v2, v1) = (stack(0), stack(1)) val newStack = stack.drop(2) diff --git a/src/main/scala/wasm/attic/StagedEvalCPS.scala b/src/main/scala/genwasym/attic/StagedEvalCPS.scala similarity index 98% rename from src/main/scala/wasm/attic/StagedEvalCPS.scala rename to src/main/scala/genwasym/attic/StagedEvalCPS.scala index 06455ee08..fa5f8d064 100644 --- a/src/main/scala/wasm/attic/StagedEvalCPS.scala +++ b/src/main/scala/genwasym/attic/StagedEvalCPS.scala @@ -1,12 +1,12 @@ -// package gensym.wasm.stagedevalcps +// package genwasym.stagedevalcps // import scala.collection.mutable.HashMap -// import gensym.wasm.ast.{Const => Konst, _} -// import gensym.wasm.values.{I32 => I32C} -// import gensym.wasm.types._ -// import gensym.wasm.memory._ -// import gensym.wasm.globals._ +// import genwasym.ast.{Const => Konst, _} +// import genwasym.values.{I32 => I32C} +// import genwasym.types._ +// import genwasym.memory._ +// import genwasym.globals._ // import lms.core._ // import lms.core.stub._ @@ -585,7 +585,7 @@ // val module = { // val file = scala.io.Source.fromFile("./benchmarks/wasm/test.wat").mkString -// gensym.wasm.parser.Parser.parseString(file) +// genwasym.parser.Parser.parseString(file) // } // val moduleInst = { diff --git a/src/main/scala/wasm/attic/StagedMiniWasm.scala b/src/main/scala/genwasym/attic/StagedMiniWasm.scala similarity index 98% rename from src/main/scala/wasm/attic/StagedMiniWasm.scala rename to src/main/scala/genwasym/attic/StagedMiniWasm.scala index 437a376f2..dd0a3c1c2 100644 --- a/src/main/scala/wasm/attic/StagedMiniWasm.scala +++ b/src/main/scala/genwasym/attic/StagedMiniWasm.scala @@ -1,13 +1,13 @@ -package gensym.wasm.miniwasm.staged +package genwasym.miniwasm.staged import scala.collection.mutable.HashMap import scala.collection.immutable.{List => StaticList} -import gensym.wasm.ast.{Const => Konst, _} -//import gensym.wasm.values.{I32 => I32C} -//import gensym.wasm.types._ -import gensym.wasm.memory._ -//import gensym.wasm.globals._ +import genwasym.ast.{Const => Konst, _} +//import genwasym.values.{I32 => I32C} +//import genwasym.types._ +import genwasym.memory._ +//import genwasym.globals._ import lms.core._ import lms.core.stub._ @@ -405,7 +405,7 @@ object StagedEvalCPSTest extends App { val module = { val file = scala.io.Source.fromFile("./benchmarks/wasm/test.wat").mkString - gensym.wasm.parser.Parser.parse(file) + genwasym.parser.Parser.parse(file) } val moduleInst = { val types = List() diff --git a/src/main/scala/wasm/attic/parser.md b/src/main/scala/genwasym/attic/parser.md similarity index 100% rename from src/main/scala/wasm/attic/parser.md rename to src/main/scala/genwasym/attic/parser.md diff --git a/src/test/scala/genwasym/CppCompilationTestBase.scala b/src/test/scala/genwasym/CppCompilationTestBase.scala index aaf8e8f53..d4bc5c1e8 100644 --- a/src/test/scala/genwasym/CppCompilationTestBase.scala +++ b/src/test/scala/genwasym/CppCompilationTestBase.scala @@ -1,4 +1,4 @@ -package gensym.wasm +package genwasym import java.io.{File, PrintWriter} import org.scalatest.FunSuite diff --git a/src/test/scala/genwasym/TestBenchmark.scala b/src/test/scala/genwasym/TestBenchmark.scala index ee88e7287..c5a286350 100644 --- a/src/test/scala/genwasym/TestBenchmark.scala +++ b/src/test/scala/genwasym/TestBenchmark.scala @@ -1,12 +1,12 @@ -package gensym.wasm +package genwasym import org.scalatest.FunSuite import lms.core.stub.Adapter -import gensym.wasm.miniwasm.{ModuleInstance} -import gensym.wasm.parser._ -import gensym.wasm.stagedconcolicminiwasm._ +import genwasym.miniwasm.{ModuleInstance} +import genwasym.parser._ +import genwasym.stagedconcolicminiwasm._ // This 'test file' is not intended to test functionality, but to generate compiled code for btree benchmarks class TestBenchmark extends FunSuite { diff --git a/src/test/scala/genwasym/TestConcolic.scala b/src/test/scala/genwasym/TestConcolic.scala index 767b8443c..8f2b48730 100644 --- a/src/test/scala/genwasym/TestConcolic.scala +++ b/src/test/scala/genwasym/TestConcolic.scala @@ -1,11 +1,11 @@ -package gensym.wasm +package genwasym -import gensym.wasm.ast._ -import gensym.wasm.source._ -import gensym.wasm.parser._ -import gensym.wasm.memory._ -import gensym.wasm.symbolic._ -import gensym.wasm.concolicminiwasm._ +import genwasym.ast._ +import genwasym.source._ +import genwasym.parser._ +import genwasym.memory._ +import genwasym.symbolic._ +import genwasym.concolicminiwasm._ import org.scalatest.FunSuite class TestConcolic extends FunSuite { @@ -29,7 +29,7 @@ class TestConcolic extends FunSuite { } class TestDriver extends FunSuite { - import gensym.wasm.concolicdriver._ + import genwasym.concolicdriver._ import scala.collection.mutable.{HashMap, HashSet} import z3.scala._ @@ -53,19 +53,19 @@ class TestDriver extends FunSuite { } -// TODO: from: GenSym/src/main/scala/wasm/tests/TestConcolicWasm.scala +// Legacy tests from TestConcolicWasm.scala. -// package gensym.wasm.test +// package genwasym.test -// import gensym.wasm.ast._ -// import gensym.wasm.source._ -// import gensym.wasm.parser._ -// import gensym.wasm.memory._ -// import gensym.wasm.symbolic._ +// import genwasym.ast._ +// import genwasym.source._ +// import genwasym.parser._ +// import genwasym.memory._ +// import genwasym.symbolic._ // object ConcolicWasmTest { // def fileTestConcolicEval(file: String, mainFun: String) = { -// import gensym.wasm.concolicminiwasm._ +// import genwasym.concolicminiwasm._ // import collection.mutable.ArrayBuffer // val module = Parser.parseFile(file) // Evaluator.execWholeProgram(module, mainFun) diff --git a/src/test/scala/genwasym/TestEval.scala b/src/test/scala/genwasym/TestEval.scala index e96f3b594..27ac7af76 100644 --- a/src/test/scala/genwasym/TestEval.scala +++ b/src/test/scala/genwasym/TestEval.scala @@ -1,15 +1,12 @@ -// TODO: maybe rename this to genwasym? -// need to rewrite everything in src/main/scala/wasm tho +package genwasym -package gensym.wasm - -import gensym.wasm.ast._ -import gensym.wasm.source._ -import gensym.wasm.parser._ -import gensym.wasm.memory._ -import gensym.wasm.symbolic._ -import gensym.wasm.miniwasm._ -import gensym.wasm.miniwasmscript.ScriptRunner +import genwasym.ast._ +import genwasym.source._ +import genwasym.parser._ +import genwasym.memory._ +import genwasym.symbolic._ +import genwasym.miniwasm._ +import genwasym.miniwasmscript.ScriptRunner import collection.mutable.ArrayBuffer import org.scalatest.FunSuite @@ -43,9 +40,8 @@ class TestEval extends FunSuite { runner.run(script) } - // TODO: the power test can be used to test the stack - // For now: 2^10 works, 2^100 results in 0 (TODO: why?), - // and 2^1000 results in a stack overflow + // The power test exercises the stack. i32 arithmetic wraps 2^100 to zero; + // deep recursion (for example, 2^1000) can overflow the interpreter's stack. test("ack") { testFile("./benchmarks/wasm/ack.wat", Some("real_main"), ExpInt(7)) } test("power") { testFile("./benchmarks/wasm/pow.wat", Some("real_main"), ExpInt(1024)) } test("start") { testFile("./benchmarks/wasm/start.wat") } @@ -58,7 +54,7 @@ class TestEval extends FunSuite { test("tribonacci") { testFile("./benchmarks/wasm/tribonacci.wat", None, ExpInt(504)) } test("return") { - intercept[gensym.wasm.miniwasm.Trap] { + intercept[genwasym.miniwasm.Trap] { testFile("./benchmarks/wasm/return.wat", Some("$real_main")) } } diff --git a/src/test/scala/genwasym/TestScriptRun.scala b/src/test/scala/genwasym/TestScriptRun.scala index c2b791562..2bd4b4083 100644 --- a/src/test/scala/genwasym/TestScriptRun.scala +++ b/src/test/scala/genwasym/TestScriptRun.scala @@ -1,7 +1,7 @@ -package gensym.wasm +package genwasym -import gensym.wasm.parser.Parser -import gensym.wasm.miniwasmscript.ScriptRunner +import genwasym.parser.Parser +import genwasym.miniwasmscript.ScriptRunner import org.scalatest.FunSuite diff --git a/src/test/scala/genwasym/TestStagedConcolicEval.scala b/src/test/scala/genwasym/TestStagedConcolicEval.scala index da2cac1d6..2a90bedf6 100644 --- a/src/test/scala/genwasym/TestStagedConcolicEval.scala +++ b/src/test/scala/genwasym/TestStagedConcolicEval.scala @@ -1,10 +1,10 @@ -package gensym.wasm +package genwasym import lms.core.stub.Adapter -import gensym.wasm.miniwasm.{ModuleInstance} -import gensym.wasm.parser._ -import gensym.wasm.stagedconcolicminiwasm._ +import genwasym.miniwasm.{ModuleInstance} +import genwasym.parser._ +import genwasym.stagedconcolicminiwasm._ class TestStagedConcolicEval extends CppCompilationTestBase { private def runConcolicExe(exePath: String, extraEnv: (String, String)*): String = @@ -150,7 +150,6 @@ class TestStagedConcolicEval extends CppCompilationTestBase { // test("loop - concrete") { testFileConcreteCpp("./benchmarks/wasm/loop.wat", None, expect=Some(List(10))) } test("even-odd - concrete") { testFileConcreteCpp("./benchmarks/wasm/even_odd.wat", None, expect=Some(List(1))) } test("global - concrete") { testFileConcreteCpp("./benchmarks/wasm/global-sym.wat", None) } - // TODO: Waiting symbolic memory's implementations test("load - concrete") { testFileConcreteCpp("./benchmarks/wasm/load.wat", None, expect=Some(List(1))) } test("select - concrete") { testFileConcreteCpp("./benchmarks/wasm/select.wat", Some("real_main")) } test("load overflow 1 - concrete") { testFileConcreteCpp("./benchmarks/wasm/load-overflow1.wat", None, expect=Some(List(1))) } diff --git a/src/test/scala/genwasym/TestStagedEval.scala b/src/test/scala/genwasym/TestStagedEval.scala index f824ef60e..696560bdd 100644 --- a/src/test/scala/genwasym/TestStagedEval.scala +++ b/src/test/scala/genwasym/TestStagedEval.scala @@ -1,10 +1,10 @@ -package gensym.wasm +package genwasym import lms.core.stub.Adapter -import gensym.wasm.parser._ -import gensym.wasm.miniwasm._ -import gensym.wasm.stagedminiwasm._ +import genwasym.parser._ +import genwasym.miniwasm._ +import genwasym.stagedminiwasm._ class TestStagedEval extends CppCompilationTestBase { def testFileToScala(filename: String, main: Option[String] = None, printRes: Boolean = false) = { diff --git a/src/test/scala/genwasym/TestSyntax.scala b/src/test/scala/genwasym/TestSyntax.scala index 8fecf874e..d3b9f65ee 100644 --- a/src/test/scala/genwasym/TestSyntax.scala +++ b/src/test/scala/genwasym/TestSyntax.scala @@ -1,6 +1,6 @@ -package gensym.wasm +package genwasym -import gensym.wasm.parser.Parser +import genwasym.parser.Parser import org.scalatest.FunSuite class TestSyntax extends FunSuite { @@ -11,7 +11,6 @@ class TestSyntax extends FunSuite { } test("basic script") { - testFile("./benchmarks/wasm/script/script_basic.wabt") + testFile("./benchmarks/wasm/script/script_basic.wast") } } -