concolic driver

Author: butterunderflow

headers/wasm.hpp

@@ -3,5 +3,6 @@
 
 #include "wasm/concrete_rt.hpp"
 #include "wasm/symbolic_rt.hpp"
-
+#include "wasm/concolic_driver.hpp"
+#include "wasm/utils.hpp"
 #endif

headers/wasm/concolic_driver.hpp

@@ -0,0 +1,98 @@
+#ifndef CONCOLIC_DRIVER_HPP
+#define CONCOLIC_DRIVER_HPP
+
+#include "smt_solver.hpp"
+#include "symbolic_rt.hpp"
+#include <functional>
+#include <ostream>
+#include <string>
+
+class ConcolicDriver {
+  friend class ManagedConcolicCleanup;
+
+public:
+  ConcolicDriver(std::function<void()> entrypoint, std::string tree_file)
+      : entrypoint(entrypoint), tree_file(tree_file) {}
+  ConcolicDriver(std::function<void()> entrypoint)
+      : entrypoint(entrypoint), tree_file(std::nullopt) {}
+  void run();
+
+private:
+  Solver solver;
+  std::function<void()> entrypoint;
+  std::optional<std::string> tree_file;
+};
+
+class ManagedConcolicCleanup {
+  const ConcolicDriver &driver;
+
+public:
+  ManagedConcolicCleanup(const ConcolicDriver &driver) : driver(driver) {}
+  ~ManagedConcolicCleanup() {
+    if (driver.tree_file.has_value())
+      ExploreTree.dump_graphviz(driver.tree_file.value());
+  }
+};
+
+inline void ConcolicDriver::run() {
+  ManagedConcolicCleanup cleanup{*this};
+  while (true) {
+    auto cond = ExploreTree.get_unexplored_conditions();
+    ExploreTree.reset_cursor();
+
+    if (!cond.has_value()) {
+      std::cout << "No unexplored conditions found, exiting..." << std::endl;
+      return;
+    }
+    auto new_env = solver.solve(cond.value());
+    if (!new_env.has_value()) {
+      std::cout << "All unexplored paths are unreachable, exiting..."
+                << std::endl;
+      return;
+    }
+    SymEnv.update(std::move(new_env.value()));
+    try {
+      entrypoint();
+      std::cout << "Execution finished successfully with symbolic environment:"
+                << std::endl;
+      std::cout << SymEnv.to_string() << std::endl;
+    } catch (...) {
+      ExploreTree.fillFailedNode();
+      std::cout << "Caught runtime error with symbolic environment:"
+                << std::endl;
+      std::cout << SymEnv.to_string() << std::endl;
+      return;
+    }
+  }
+}
+
+static std::monostate reset_stacks() {
+  Stack.reset();
+  Frames.reset();
+  SymStack.reset();
+  SymFrames.reset();
+  initRand();
+  Memory = Memory_t(1);
+  return std::monostate{};
+}
+
+static void start_concolic_execution_with(
+    std::function<std::monostate(std::monostate)> entrypoint,
+    std::string tree_file) {
+  ConcolicDriver driver([=]() { entrypoint(std::monostate{}); }, tree_file);
+  driver.run();
+}
+
+static void start_concolic_execution_with(
+    std::function<std::monostate(std::monostate)> entrypoint) {
+
+  const char *env_tree_file = std::getenv("TREE_FILE");
+
+  ConcolicDriver driver =
+      env_tree_file ? ConcolicDriver([=]() { entrypoint(std::monostate{}); },
+                                     env_tree_file)
+                    : ConcolicDriver([=]() { entrypoint(std::monostate{}); });
+  driver.run();
+}
+
+#endif // CONCOLIC_DRIVER_HPP

headers/wasm/concrete_rt.hpp

@@ -52,8 +52,6 @@ static Num I32V(int v) { return v; }
 
 static Num I64V(int64_t v) { return v; }
 
-using Slice = std::vector<Num>;
-
 const int STACK_SIZE = 1024 * 64;
 
 class Stack_t {
@@ -118,9 +116,12 @@ class Stack_t {
   }
 
   void initialize() {
-    // do nothing for now
+    // todo: remove this method
+   reset();
   }
 
+  void reset() { count = 0; }
+
 private:
   int32_t count;
   Num *stack_ptr;
@@ -151,6 +152,8 @@ class Frames_t {
     count += size;
   }
 
+  void reset() { count = 0; }
+
 private:
   int32_t count;
   Num *stack_ptr;

headers/wasm/smt_solver.hpp

@@ -0,0 +1,28 @@
+#ifndef SMT_SOLVER_HPP
+#define SMT_SOLVER_HPP
+
+#include "concrete_rt.hpp"
+#include "symbolic_rt.hpp"
+#include <array>
+#include <vector>
+
+class Solver {
+public:
+  Solver() : count(0) {
+    envs[0] = {Num(0), Num(0)};
+    envs[1] = {Num(1), Num(2)};
+  }
+  std::optional<std::vector<Num>> solve(const std::vector<SymVal> &conditions) {
+    // here is just a placeholder implementation to simulate solving result
+    if (count >= envs.size()) {
+      return std::nullopt; // No more environments to return
+    }
+    return envs[count++ % envs.size()];
+  }
+
+private:
+  std::array<std::vector<Num>, 5> envs;
+  int count;
+};
+
+#endif // SMT_SOLVER_HPP