config header; fix extract evaluation; capture by value in lambda

butterunderflow · butterunderflow · commit 2d82a0f0491c · 2025-10-05T12:22:01.000-04:00
diff --git a/headers/wasm/concolic_driver.hpp b/headers/wasm/concolic_driver.hpp
@@ -2,10 +2,11 @@
 #define CONCOLIC_DRIVER_HPP
 
 #include "concrete_rt.hpp"
+#include "config.hpp"
+#include "profile.hpp"
 #include "smt_solver.hpp"
 #include "symbolic_rt.hpp"
 #include "utils.hpp"
-#include "wasm/profile.hpp"
 #include <cassert>
 #include <chrono>
 #include <functional>
@@ -15,16 +16,6 @@
 #include <string>
 #include <vector>
 
-enum class ExploreMode { EarlyExit, ExitByCoverage };
-
-#ifdef EARLY_EXIT
-static const ExploreMode EXPLORE_MODE = ExploreMode::EarlyExit;
-#elif defined(BY_COVERAGE)
-static const ExploreMode EXPLORE_MODE = ExploreMode::ExitByCoverage;
-#else
-static const ExploreMode EXPLORE_MODE = ExploreMode::EarlyExit;
-#endif
-
 class ConcolicDriver {
   friend class ManagedConcolicCleanup;
 
@@ -107,12 +98,14 @@ inline void ConcolicDriver::main_exploration_loop() {
     try {
       GENSYM_INFO("Now execute the program with symbolic environment: ");
       GENSYM_INFO(SymEnv.to_string());
-      if (auto snapshot_node =
-              dynamic_cast<SnapshotNode *>(node->node.get())) {
+      if (auto snapshot_node = dynamic_cast<SnapshotNode *>(node->node.get())) {
+        assert(REUSE_SNAPSHOT);
+        auto timer = ManagedTimer();
         snapshot_node->get_snapshot().resume_execution(SymEnv, node);
       } else {
         auto timer = ManagedTimer();
         reset_stacks();
+        ExploreTree.reset_cursor();
         entrypoint();
       }
 
@@ -134,6 +127,7 @@ inline void ConcolicDriver::main_exploration_loop() {
           GENSYM_INFO(
               "Found a bug, but not all branches covered, continuing...");
         }
+        std::cout << e.what() << std::endl;
       }
     }
 #if defined(RUN_ONCE)
@@ -143,18 +137,18 @@ inline void ConcolicDriver::main_exploration_loop() {
 }
 
 inline void ConcolicDriver::run() {
-  ExploreTree.reset_cursor();
   main_exploration_loop();
   Profile.print_summary();
 }
 
 static std::monostate reset_stacks() {
   Stack.reset();
-  Frames.reset();
   SymStack.reset();
+  Frames.reset();
   SymFrames.reset();
-  initRand();
   Memory.reset();
+  SymMemory.reset();
+  initRand();
   return std::monostate{};
 }
 
diff --git a/headers/wasm/concrete_rt.hpp b/headers/wasm/concrete_rt.hpp
@@ -16,25 +16,31 @@
 struct Num {
   Num(int64_t value) : value(value) {}
   Num() : value(0) {}
-  int64_t value;
-  int32_t toInt() { return static_cast<int32_t>(value); }
+  int32_t value;
+  int32_t toInt() const { return static_cast<int32_t>(value); }
 
-  bool operator==(const Num &other) const { return value == other.value; }
+  // TODO: support different bit width operations, for now we just assume all
+  // oprands are i32
+  bool operator==(const Num &other) const { return toInt() == other.toInt(); }
   bool operator!=(const Num &other) const { return !(*this == other); }
-  Num operator+(const Num &other) const { return Num(value + other.value); }
-  Num operator-(const Num &other) const { return Num(value - other.value); }
-  Num operator*(const Num &other) const { return Num(value * other.value); }
+  Num operator+(const Num &other) const { return Num(toInt() + other.toInt()); }
+  Num operator-(const Num &other) const { return Num(toInt() - other.toInt()); }
+  Num operator*(const Num &other) const { return Num(toInt() * other.toInt()); }
   Num operator/(const Num &other) const {
-    if (other.value == 0) {
+    if (other.toInt() == 0) {
       throw std::runtime_error("Division by zero");
     }
-    return Num(value / other.value);
+    return Num(toInt() / other.toInt());
   }
-  Num operator<(const Num &other) const { return Num(value < other.value); }
-  Num operator<=(const Num &other) const { return Num(value <= other.value); }
-  Num operator>(const Num &other) const { return Num(value > other.value); }
-  Num operator>=(const Num &other) const { return Num(value >= other.value); }
-  Num operator&(const Num &other) const { return Num(value & other.value); }
+  Num operator<(const Num &other) const { return Num(toInt() < other.toInt()); }
+  Num operator<=(const Num &other) const {
+    return Num(toInt() <= other.toInt());
+  }
+  Num operator>(const Num &other) const { return Num(toInt() > other.toInt()); }
+  Num operator>=(const Num &other) const {
+    return Num(toInt() >= other.toInt());
+  }
+  Num operator&(const Num &other) const { return Num(toInt() & other.toInt()); }
 };
 
 static Num I32V(int v) { return v; }
@@ -71,8 +77,9 @@ class Stack_t {
     Profile.step(ProfileKind::POP);
 #ifdef DEBUG
     assert(count > 0 && "Stack underflow");
-    printf("[Debug] popping from stack, size of concrete stack is: %d\n",
-           count);
+    printf("[Debug] popping a value %ld from stack, size of concrete stack is: "
+           "%d\n",
+           stack_ptr[count - 1].value, count);
 #endif
     Num num = stack_ptr[count - 1];
     count--;
@@ -223,6 +230,10 @@ struct Memory_t {
         page_count(init_page_count), allocated_pages(PRE_ALLOC_PAGES) {}
 
   int32_t loadInt(int32_t base, int32_t offset) {
+#ifdef DEBUG
+    std::cout << "[Debug] loading int from memory at address: "
+              << (base + offset) << std::endl;
+#endif
     // just load a 4-byte integer from memory of the vector
     int32_t addr = base + offset;
     if (!(addr + 3 < memory.size())) {
@@ -238,8 +249,14 @@ struct Memory_t {
 
   std::monostate storeInt(int32_t base, int32_t offset, int32_t value) {
     int32_t addr = base + offset;
+#ifdef DEBUG
+    std::cout << "[Debug] storing int " << value << " to memory at address "
+              << addr << std::endl;
+#endif
     // Ensure we don't write out of bounds
-    assert(addr + 3 < memory.size());
+    if (!(addr + 3 < memory.size())) {
+      throw std::runtime_error("Invalid memory access " + std::to_string(addr));
+    }
     for (int i = 0; i < 4; ++i) {
       memory[addr + i] = static_cast<uint8_t>((value >> (8 * i)) & 0xFF);
       // Optionally, update memory[addr + i].second (SymVal) if needed
diff --git a/headers/wasm/config.hpp b/headers/wasm/config.hpp
@@ -0,0 +1,36 @@
+#ifndef CONFIG_HPP
+#define CONFIG_HPP
+
+// This file contains configuration settings for the concolic execution
+
+// If ENABLE_PROFILE defined, the compiled program will collect and print
+// profiling information
+#ifdef ENABLE_PROFILE
+const bool PROFILE_ENABLED = true;
+#else
+const bool PROFILE_ENABLED = false;
+#endif
+
+// This variable define when concolic execution will stop
+enum class ExploreMode {
+  EarlyExit, // Stop at the first error encountered
+
+  ExitByCoverage // Exit when all syntactic branches are covered
+};
+
+#ifdef EARLY_EXIT
+static const ExploreMode EXPLORE_MODE = ExploreMode::EarlyExit;
+#elif defined(BY_COVERAGE)
+static const ExploreMode EXPLORE_MODE = ExploreMode::ExitByCoverage;
+#else
+static const ExploreMode EXPLORE_MODE = ExploreMode::EarlyExit;
+#endif
+
+// This variable decides whether we enable the snapshot reuse optimization
+#ifdef NO_REUSE
+static const bool REUSE_SNAPSHOT = false;
+#else
+static const bool REUSE_SNAPSHOT = true;
+#endif
+
+#endif // CONFIG_HPP
diff --git a/headers/wasm/profile.hpp b/headers/wasm/profile.hpp
@@ -2,6 +2,7 @@
 #define PROFILE_HPP
 
 #include "utils.hpp"
+#include "config.hpp"
 #include <array>
 #include <chrono>
 #include <iomanip>
@@ -27,59 +28,57 @@ class Profile_t {
 public:
   Profile_t() : step_count(0) {}
   std::monostate step() {
-#ifdef ENABLE_PROFILE
-    step_count++;
-#endif
+    if (PROFILE_ENABLED)
+      step_count++;
     return std::monostate();
   }
   std::monostate step(ProfileKind op) {
-#ifdef ENABLE_PROFILE
-    op_count[static_cast<std::size_t>(op)]++;
-#endif
+    if (PROFILE_ENABLED)
+      op_count[static_cast<std::size_t>(op)]++;
     return std::monostate();
   }
   void print_summary() {
-#ifdef ENABLE_PROFILE
-    std::cout << "Profile Summary:" << std::endl;
-    std::cout << "Total PUSH operations: "
-              << op_count[static_cast<std::size_t>(ProfileKind::PUSH)]
-              << std::endl;
-    std::cout << "Total POP operations: "
-              << op_count[static_cast<std::size_t>(ProfileKind::POP)]
-              << std::endl;
-    std::cout << "Total PEEK operations: "
-              << op_count[static_cast<std::size_t>(ProfileKind::PEEK)]
-              << std::endl;
-    std::cout << "Total SHIFT operations: "
-              << op_count[static_cast<std::size_t>(ProfileKind::SHIFT)]
-              << std::endl;
-    std::cout << "Total SET operations: "
-              << op_count[static_cast<std::size_t>(ProfileKind::SET)]
-              << std::endl;
-    std::cout << "Total GET operations: "
-              << op_count[static_cast<std::size_t>(ProfileKind::GET)]
-              << std::endl;
-    std::cout << "Total BINARY operations: "
-              << op_count[static_cast<std::size_t>(ProfileKind::BINARY)]
-              << std::endl;
-    std::cout << "Total TREE_FILL operations: "
-              << op_count[static_cast<std::size_t>(ProfileKind::TREE_FILL)]
-              << std::endl;
-    std::cout << "Total CURSOR_MOVE operations: "
-              << op_count[static_cast<std::size_t>(ProfileKind::CURSOR_MOVE)]
-              << std::endl;
-    std::cout << "Total other instructions executed: " << step_count
-              << std::endl;
-    std::cout << "Total MEM_GROW operations: "
-              << op_count[static_cast<std::size_t>(ProfileKind::MEM_GROW)]
-              << std::endl;
-    std::cout
-        << "Total SNAPSHOT_CREATE operations: "
-        << op_count[static_cast<std::size_t>(ProfileKind::SNAPSHOT_CREATE)]
-        << std::endl;
-    std::cout << "Total time for instruction execution (s): "
-              << std::setprecision(15) << execution_time << std::endl;
-#endif
+    if (PROFILE_ENABLED) {
+      std::cout << "Profile Summary:" << std::endl;
+      std::cout << "Total PUSH operations: "
+                << op_count[static_cast<std::size_t>(ProfileKind::PUSH)]
+                << std::endl;
+      std::cout << "Total POP operations: "
+                << op_count[static_cast<std::size_t>(ProfileKind::POP)]
+                << std::endl;
+      std::cout << "Total PEEK operations: "
+                << op_count[static_cast<std::size_t>(ProfileKind::PEEK)]
+                << std::endl;
+      std::cout << "Total SHIFT operations: "
+                << op_count[static_cast<std::size_t>(ProfileKind::SHIFT)]
+                << std::endl;
+      std::cout << "Total SET operations: "
+                << op_count[static_cast<std::size_t>(ProfileKind::SET)]
+                << std::endl;
+      std::cout << "Total GET operations: "
+                << op_count[static_cast<std::size_t>(ProfileKind::GET)]
+                << std::endl;
+      std::cout << "Total BINARY operations: "
+                << op_count[static_cast<std::size_t>(ProfileKind::BINARY)]
+                << std::endl;
+      std::cout << "Total TREE_FILL operations: "
+                << op_count[static_cast<std::size_t>(ProfileKind::TREE_FILL)]
+                << std::endl;
+      std::cout << "Total CURSOR_MOVE operations: "
+                << op_count[static_cast<std::size_t>(ProfileKind::CURSOR_MOVE)]
+                << std::endl;
+      std::cout << "Total other instructions executed: " << step_count
+                << std::endl;
+      std::cout << "Total MEM_GROW operations: "
+                << op_count[static_cast<std::size_t>(ProfileKind::MEM_GROW)]
+                << std::endl;
+      std::cout
+          << "Total SNAPSHOT_CREATE operations: "
+          << op_count[static_cast<std::size_t>(ProfileKind::SNAPSHOT_CREATE)]
+          << std::endl;
+      std::cout << "Total time for instruction execution (s): "
+                << std::setprecision(15) << execution_time << std::endl;
+    }
   }
 
   // record the time spent in main instruction execution, in seconds
diff --git a/headers/wasm/symbolic_rt.hpp b/headers/wasm/symbolic_rt.hpp
diff --git a/src/main/scala/wasm/StagedConcolicMiniWasm.scala b/src/main/scala/wasm/StagedConcolicMiniWasm.scala
