Move header-only C++ runtime to dedicated runtime library

.gitignore

@@ -27,5 +27,6 @@ conc_gen/*
 ccbse_gen/*
 headers/gensym/external.hpp
 grammar/.antlr/
+genwasym_runtime/build
 *.interp
 *.tokens

genwasym_runtime/Makefile

@@ -0,0 +1,32 @@
+CXX = g++
+CXXFLAGS = -std=c++17 -Wall -Iinclude -I../headers -I../third-party/immer -I../third-party/z3/build/z3_install/usr/local/include -fPIC
+BUILD_DIR = build
+
+Z3_LIB_DIR = ../third-party/z3/build/z3_install/usr/local/lib
+LDFLAGS = -L$(Z3_LIB_DIR) -Wl,-rpath,$(Z3_LIB_DIR)
+LDLIBS = -lz3
+
+SRC = $(filter-out lib/wasm_state_continue.cpp,$(wildcard lib/*.cpp))
+OBJ = $(patsubst lib/%.cpp,$(BUILD_DIR)/%.o,$(SRC))
+
+STATIC_LIB = $(BUILD_DIR)/libgenwasym.a
+SHARED_LIB = $(BUILD_DIR)/libgenwasym.so
+
+.PHONY: all clean
+
+all: $(BUILD_DIR) $(STATIC_LIB) $(SHARED_LIB)
+
+$(BUILD_DIR):
+	mkdir -p $(BUILD_DIR)
+
+$(BUILD_DIR)/%.o: lib/%.cpp | $(BUILD_DIR)
+	$(CXX) $(CXXFLAGS) -c $< -o $@
+
+$(STATIC_LIB): $(OBJ)
+	ar rcs $(STATIC_LIB) $(OBJ)
+
+$(SHARED_LIB): $(OBJ)
+	$(CXX) -shared -Wl,-install_name,@rpath/libgenwasym.so $(LDFLAGS) -o $(SHARED_LIB) $(OBJ) $(LDLIBS)
+
+clean:
+	rm -rf $(BUILD_DIR)

genwasym_runtime/include/genwasym.h

@@ -0,0 +1,4 @@
+#pragma once
+
+int genwasym_dummy();
+

genwasym_runtime/include/wasm.hpp

@@ -0,0 +1,11 @@
+#ifndef WASM_HEADERS
+#define WASM_HEADERS
+
+#include "wasm/concolic_driver.hpp"
+#include "wasm/concrete_rt.hpp"
+#include "wasm/controls.hpp"
+#include "wasm/profile.hpp"
+#include "wasm/sym_rt.hpp"
+#include "wasm/utils.hpp"
+
+#endif

genwasym_runtime/include/wasm/concolic_driver.hpp

@@ -0,0 +1,184 @@
+#ifndef CONCOLIC_DRIVER_HPP
+#define CONCOLIC_DRIVER_HPP
+
+#include "concrete_rt.hpp"
+#include "config.hpp"
+#include "output_report.hpp"
+#include "profile.hpp"
+#include "smt_solver.hpp"
+#include "sym_rt.hpp"
+#include "utils.hpp"
+#include "z3++.h"
+#include <cassert>
+#include <chrono>
+#include <functional>
+#include <optional>
+#include <ostream>
+#include <set>
+#include <stdexcept>
+#include <string>
+#include <vector>
+
+class ConcolicDriver {
+  friend class ManagedConcolicCleanup;
+
+public:
+  ConcolicDriver(std::function<void()> entrypoint,
+                 std::optional<std::string> tree_file, int branchCount);
+  void run();
+
+private:
+  void main_exploration_loop();
+  std::optional<QueryResult> get_new_input();
+  std::vector<std::vector<SymVal>> collect_all_unexplored_path_conds();
+  std::function<void()> entrypoint;
+  std::optional<std::string> tree_file;
+  std::vector<NodeBox *> work_list;
+  std::set<NodeBox *> visited;
+};
+
+class ManagedConcolicCleanup {
+  const ConcolicDriver &driver;
+
+public:
+  ManagedConcolicCleanup(const ConcolicDriver &driver);
+  ~ManagedConcolicCleanup();
+};
+
+static std::monostate reset_stacks();
+
+// A PathFrontier represents the frontier of an unexplored path. From this
+// frontier, we can explore the path by executing the program from the beginning
+// with the model stored in QueryResult.
+struct PathFrontier {
+  QueryResult query_result;
+  NodeBox *node;
+};
+
+class PathPicker {
+public:
+  PathPicker(std::vector<NodeBox *> &unexplored_paths,
+             std::set<NodeBox *> &visited);
+
+  virtual std::optional<PathFrontier> pick_path() = 0;
+
+protected:
+  std::vector<NodeBox *> &unexplored_paths;
+  std::set<NodeBox *> &visited;
+};
+
+class DefaultPathPicker : public PathPicker {
+public:
+  DefaultPathPicker(std::vector<NodeBox *> &unexplored_paths,
+                    std::set<NodeBox *> &visited);
+
+  std::optional<PathFrontier> pick_path() override;
+};
+
+class RandomPathPicker : public PathPicker {
+public:
+  RandomPathPicker(std::vector<NodeBox *> &unexplored_paths,
+                   std::set<NodeBox *> &visited);
+
+  std::optional<PathFrontier> pick_path() override;
+};
+
+inline void ConcolicDriver::main_exploration_loop() {
+
+  // Register a collector to ExploreTree to add new nodes to work_list
+  ExploreTree.register_new_node_collector([&](NodeBox *new_node) {
+    if (std::find(work_list.begin(), work_list.end(), new_node) ==
+        work_list.end())
+      work_list.push_back(new_node);
+  });
+
+  assert(ExploreTree.get_root()->isUnexplored() &&
+         "Before main loop, root should be unexplored!");
+  work_list.push_back(ExploreTree.get_root());
+
+  PathPicker &&picker = DefaultPathPicker(work_list, visited);
+
+  while (!work_list.empty()) {
+    if (INTERACTIVE_MODE) {
+      std::cout << "Press Enter to continue to the next path..." << std::endl;
+      std::cin.get();
+    }
+    ManagedConcolicCleanup cleanup{*this};
+    ManagedTimer timer(TimeProfileKind::MAIN_LOOP);
+    // Pick a frontier of an unexplored path from the work list
+    auto frontier = picker.pick_path();
+    if (!frontier.has_value()) {
+      continue;
+    }
+
+    auto &node = frontier.value().node;
+
+    const NumMap &new_env = *frontier.value().query_result.map_box;
+    z3::model &model = frontier.value().query_result.model;
+
+    // update global symbolic environment from SMT solved model
+    SymEnv.update(new_env);
+    try {
+      GENSYM_INFO("Now execute the program with symbolic environment: ");
+      GENSYM_INFO(SymEnv.to_string());
+      auto snapshot = dynamic_cast<SnapshotNode *>(node->node.get());
+      if (REUSE_SNAPSHOT && snapshot && snapshot->worth_to_reuse()) {
+        assert(REUSE_SNAPSHOT);
+        Profile.incr_fromsnapshot_count();
+        auto snap = snapshot->get_snapshot();
+        snap.resume_execution_by_model(node, model);
+      } else {
+        Profile.incr_restart_count();
+        auto timer = ManagedTimer(TimeProfileKind::INSTR);
+        ExploreTree.reset_cursor();
+        reset_stacks();
+        CostManager.reset_timer();
+        entrypoint();
+      }
+
+      GENSYM_INFO("Execution finished successfully");
+    } catch (std::runtime_error &e) {
+      std::cout << "Caught runtime error: " << e.what() << std::endl;
+      ExploreTree.fillFailedNode();
+
+      if (std::string(e.what()) == "Symbolic assertion failed") {
+        GENSYM_INFO("Symbolic assertion failed, continuing to next path...");
+        continue;
+      }
+
+      GENSYM_INFO("Caught runtime error during execution");
+      switch (EXPLORE_MODE) {
+      case ExploreMode::EarlyExit:
+        return;
+      case ExploreMode::ExitByCoverage:
+        if (ExploreTree.all_branch_covered()) {
+          GENSYM_INFO("All branches covered, exiting...");
+          return;
+        } else {
+          GENSYM_INFO(
+              "Found a bug, but not all branches covered, continuing...");
+        }
+        std::cout << e.what() << std::endl;
+      }
+    }
+#if defined(RUN_ONCE)
+    return;
+#endif
+  }
+}
+
+static void start_concolic_execution_with(
+    std::function<std::monostate(std::monostate)> entrypoint, int branchCount) {
+
+  const char *env_tree_file = std::getenv("TREE_FILE");
+
+  auto tree_file =
+      env_tree_file ? std::make_optional(env_tree_file) : std::nullopt;
+
+  ConcolicDriver driver = ConcolicDriver(
+      [=]() { entrypoint(std::monostate{}); }, tree_file, branchCount);
+  driver.run();
+  std::quick_exit(0);
+}
+
+#endif // CONCOLIC_DRIVER_HPP

genwasym_runtime/include/wasm/concrete_num.hpp

@@ -0,0 +1,142 @@
+#ifndef WASM_CONCRETE_NUM_HPP
+#define WASM_CONCRETE_NUM_HPP
+
+#include <cstdint>
+
+struct Num {
+  Num(int64_t value);
+  Num();
+
+  int64_t value;
+
+  int32_t toInt() const;
+  uint32_t toUInt() const;
+  int64_t toInt64() const;
+  uint64_t toUInt64() const;
+  float toF32() const;
+  double toF64() const;
+
+  static void debug_print(const char *op, const Num &a, const Num &b,
+                          const Num &res);
+
+  Num WasmBool(bool condition) const;
+
+  Num i32_eq(const Num &other) const;
+  Num i32_ne(const Num &other) const;
+  Num i32_lt_s(const Num &other) const;
+  Num i32_lt_u(const Num &other) const;
+  Num i32_le_s(const Num &other) const;
+  Num i32_le_u(const Num &other) const;
+  Num i32_gt_s(const Num &other) const;
+  Num i32_gt_u(const Num &other) const;
+  Num i32_ge_s(const Num &other) const;
+  Num i32_ge_u(const Num &other) const;
+
+  Num i32_add(const Num &other) const;
+  Num i32_sub(const Num &other) const;
+  Num i32_mul(const Num &other) const;
+  Num i32_div_s(const Num &other) const;
+  Num i32_div_u(const Num &other) const;
+  Num i32_rem_s(const Num &other) const;
+  Num i32_rem_u(const Num &other) const;
+
+  Num i32_shl(const Num &other) const;
+  Num i32_shr_s(const Num &other) const;
+  Num i32_shr_u(const Num &other) const;
+  Num i32_and(const Num &other) const;
+  Num i32_xor(const Num &other) const;
+  Num i32_or(const Num &other) const;
+
+  Num i32_extend_to_i64_s() const;
+  Num i32_extend_to_i64_u() const;
+
+  Num i64_eq(const Num &other) const;
+  Num i64_ne(const Num &other) const;
+  Num i64_lt_s(const Num &other) const;
+  Num i64_lt_u(const Num &other) const;
+  Num i64_le_s(const Num &other) const;
+  Num i64_le_u(const Num &other) const;
+  Num i64_gt_s(const Num &other) const;
+  Num i64_gt_u(const Num &other) const;
+  Num i64_ge_s(const Num &other) const;
+  Num i64_ge_u(const Num &other) const;
+
+  Num i64_add(const Num &other) const;
+  Num i64_sub(const Num &other) const;
+  Num i64_mul(const Num &other) const;
+  Num i64_div_s(const Num &other) const;
+  Num i64_div_u(const Num &other) const;
+  Num i64_rem_s(const Num &other) const;
+  Num i64_rem_u(const Num &other) const;
+
+  Num i64_shl(const Num &other) const;
+  Num i64_shr_s(const Num &other) const;
+  Num i64_shr_u(const Num &other) const;
+  Num i64_and(const Num &other) const;
+  Num i64_xor(const Num &other) const;
+  Num i64_or(const Num &other) const;
+
+  static float f32_from_bits(uint32_t bits);
+  static uint32_t f32_to_bits(float f);
+  static bool f32_is_nan(uint32_t bits);
+
+  Num f32_add(const Num &other) const;
+  Num f32_sub(const Num &other) const;
+  Num f32_mul(const Num &other) const;
+  Num f32_div(const Num &other) const;
+  Num f32_eq(const Num &other) const;
+  Num f32_ne(const Num &other) const;
+  Num f32_lt(const Num &other) const;
+  Num f32_le(const Num &other) const;
+  Num f32_gt(const Num &other) const;
+  Num f32_ge(const Num &other) const;
+  Num f32_abs() const;
+  Num f32_neg() const;
+
+  Num convert_i32_to_f32_s() const;
+  Num convert_i32_to_f32_u() const;
+  Num convert_i64_to_f32_s() const;
+  Num convert_i64_to_f32_u() const;
+
+  Num f32_min(const Num &other) const;
+  Num f32_max(const Num &other) const;
+  Num f32_copysign(const Num &other) const;
+
+  static double f64_from_bits(uint64_t bits);
+  static uint64_t f64_to_bits(double d);
+  static bool f64_is_nan(uint64_t bits);
+
+  Num f64_add(const Num &other) const;
+  Num f64_sub(const Num &other) const;
+  Num f64_mul(const Num &other) const;
+  Num f64_div(const Num &other) const;
+  Num f64_eq(const Num &other) const;
+  Num f64_ne(const Num &other) const;
+  Num f64_lt(const Num &other) const;
+  Num f64_le(const Num &other) const;
+  Num f64_gt(const Num &other) const;
+  Num f64_ge(const Num &other) const;
+  Num f64_abs() const;
+  Num f64_neg() const;
+
+  Num convert_i32_to_f64_s() const;
+  Num convert_i32_to_f64_u() const;
+  Num convert_i64_to_f64_s() const;
+  Num convert_i64_to_f64_u() const;
+
+  Num trunc_f64_to_i32_u() const;
+
+  Num f64_min(const Num &other) const;
+  Num f64_max(const Num &other) const;
+  Num f64_copysign(const Num &other) const;
+
+  bool logical_and(const Num &other) const;
+  bool logical_or(const Num &other) const;
+};
+
+Num I32V(int v);
+Num I64V(int64_t v);
+Num F32V(float f);
+Num F64V(double d);
+
+#endif // WASM_CONCRETE_NUM_HPP