update sym_assert and timer

Author: butterunderflow

headers/wasm/concolic_driver.hpp

@@ -31,7 +31,6 @@ class ConcolicDriver {
 
 private:
   void main_exploration_loop();
-  Solver solver;
   std::function<void()> entrypoint;
   std::optional<std::string> tree_file;
   std::vector<NodeBox *> work_list;

headers/wasm/profile.hpp

@@ -7,6 +7,7 @@
 #include <chrono>
 #include <iomanip>
 #include <variant>
+#include <vector>
 
 enum class StepProfileKind {
   PUSH,
@@ -157,8 +158,7 @@ class Profile_t {
          << std::setprecision(15)
          << time_count[static_cast<std::size_t>(TimeProfileKind::INSTR)]
          << ",\n";
-      os << "    \"total_time_solver_s\": "
-         << std::setprecision(15)
+      os << "    \"total_time_solver_s\": " << std::setprecision(15)
          << time_count[static_cast<std::size_t>(TimeProfileKind::SOLVER)]
          << ",\n";
       os << "    \"total_time_resuming_from_snapshot_s\": "
@@ -191,23 +191,50 @@ class Profile_t {
 
 static Profile_t Profile;
 
-class ManagedTimer {
+class Timer {
 public:
-  ManagedTimer() = delete;
-  ManagedTimer(TimeProfileKind kind) : kind(kind) {
+  Timer() = delete;
+  Timer(TimeProfileKind kind) : kind(kind) {
+    elapsed = std::chrono::duration<double>::zero();
     start = std::chrono::high_resolution_clock::now();
   }
-  ~ManagedTimer() {
+  ~Timer() {
     auto end = std::chrono::high_resolution_clock::now();
-    std::chrono::duration<double> elapsed = end - start;
+    elapsed += end - start;
     Profile.add_instruction_time(kind, elapsed.count());
   }
+  void stop() { elapsed += std::chrono::high_resolution_clock::now() - start; }
+  void resume() { start = std::chrono::high_resolution_clock::now(); }
 
 private:
+  std::chrono::duration<double> elapsed;
   TimeProfileKind kind;
   std::chrono::high_resolution_clock::time_point start;
 };
 
+static std::vector<Timer> TimerStack = []() {
+  std::vector<Timer> v;
+  v.reserve(3); // initial capacity
+  return v;
+}();
+
+class ManagedTimer {
+public:
+  ManagedTimer() = delete;
+  ManagedTimer(TimeProfileKind kind) {
+    if (TimerStack.size() > 0) {
+      TimerStack.back().stop();
+    }
+    TimerStack.emplace_back(kind);
+  }
+  ~ManagedTimer() {
+    TimerStack.pop_back();
+    if (TimerStack.size() > 0) {
+      TimerStack.back().resume();
+    }
+  }
+};
+
 struct CostManager_t {
   int instr_cost;
 

headers/wasm/smt_solver.hpp

@@ -11,6 +11,7 @@
 #include <set>
 #include <string>
 #include <tuple>
+#include <variant>
 #include <vector>
 
 class Solver {
@@ -73,11 +74,11 @@ class Solver {
 
   z3::context z3_ctx;
   z3::expr build_z3_expr(SymVal &sym_val);
-
-private:
   z3::expr build_z3_expr_aux(SymVal &sym_val);
 };
 
+static Solver solver;
+
 inline z3::expr Solver::build_z3_expr_aux(SymVal &sym_val) {
   if (auto sym = std::dynamic_pointer_cast<Symbol>(sym_val.symptr)) {
     return z3_ctx.bv_const(("s_" + std::to_string(sym->get_id())).c_str(), 32);
@@ -164,4 +165,16 @@ inline z3::expr Solver::build_z3_expr(SymVal &sym_val) {
   sym_val.z3_expr = std::make_shared<z3::expr>(e);
   return e;
 }
+
+inline std::monostate GENSYM_SYM_ASSERT(SymVal &sym_cond) {
+  std::vector<SymVal> conds = ExploreTree.collect_current_path_conds();
+  conds.push_back(sym_cond.negate());
+  auto result = solver.solve(conds);
+  if (result.has_value()) {
+    std::cout << "Symbolic assertion failed" << std::endl;
+    throw std::runtime_error("Symbolic assertion failed");
+  }
+  return std::monostate{};
+}
+
 #endif // SMT_SOLVER_HPP

headers/wasm/symbolic_rt.hpp

@@ -957,6 +957,10 @@ class ExploreTree_t {
     return cursor->fillNotToExploreNode();
   }
 
+  std::vector<SymVal> collect_current_path_conds() {
+    return cursor->collect_path_conds();
+  }
+
   bool worth_to_create_snapshot() {
     if (!ENABLE_COST_MODEL) {
       return REUSE_SNAPSHOT;

src/main/scala/wasm/StagedConcolicMiniWasm.scala

@@ -576,7 +576,11 @@ trait StagedWasmEvaluator extends SAIOps {
         }
         ()
       case Import("i32", "sym_assert", _) =>
-        // TODO: implement sym_assert
+        val (condTy, newCtx) = ctx.pop()
+        val v = Stack.popC(condTy)
+        val s = Stack.popS(condTy)
+        runtimeSymAssert(s)
+        runtimeAssert(v.toInt != 0)
         eval(rest, kont, mkont, trail)(ctx.pop()._2)
       case Import(m, f, _) => throw new Exception(s"Unknown import $m.$f at $funcIndex")
       case _               => throw new Exception(s"Definition at $funcIndex is not callable")
@@ -715,6 +719,10 @@ trait StagedWasmEvaluator extends SAIOps {
     "assert-true".reflectCtrlWith[Unit](b)
   }
 
+  def runtimeSymAssert(s: StagedSymbolicNum): Rep[Unit] = {
+    "sym-assert-true".reflectCtrlWith[Unit](s.s)
+  }
+
   // stack operations
   object Stack {
     def shiftC(offset: Int, size: Int) = {
@@ -1578,6 +1586,8 @@ trait StagedWasmCppGen extends CGenBase with CppSAICodeGenBase {
       emit("SymEnv.read("); shallow(sym); emit(")")
     case Node(_, "assert-true", List(cond), _) =>
       emit("GENSYM_ASSERT("); shallow(cond); emit(")")
+    case Node(_, "sym-assert-true", List(s_cond), _) =>
+      emit("GENSYM_SYM_ASSERT("); shallow(s_cond); emit(")")
     case Node(_, "tree-fill-if-else", List(sym, id), _) =>
       emit("ExploreTree.fillIfElseNode("); shallow(sym); emit(", "); emit(id.toString); emit(")")
     case Node(_, "tree-fill-not-to-explore", List(), _) =>