Reuse symbolic states

benchmarks/wasm/staged/return_poly.wat

@@ -0,0 +1,19 @@
+(module
+  (type (;0;) (func))
+  (type (;1;) (func (result i32))) 
+  ;; TODO: It seems that our parser or preprocessor has some problems; the result type of the last line doesn't take effect
+  (func (result i32)
+    block
+      i32.const 21
+      i32.const 35
+      i32.const 42
+      return
+    end
+    i32.const 100
+  )
+  (func (type 0)
+    call 0
+    ;; unreachable
+  )
+  (export "$real_main" (func 1))
+)

headers/wasm/concolic_driver.hpp

@@ -4,6 +4,7 @@
 #include "concrete_rt.hpp"
 #include "smt_solver.hpp"
 #include "symbolic_rt.hpp"
+#include "utils.hpp"
 #include <functional>
 #include <ostream>
 #include <string>
@@ -43,33 +44,33 @@ inline void ConcolicDriver::run() {
 
     auto unexplored = ExploreTree.pick_unexplored();
     if (!unexplored) {
-      std::cout << "No unexplored nodes found, exiting..." << std::endl;
+      GENSYM_INFO("No unexplored nodes found, exiting...");
       return;
     }
     auto cond = unexplored->collect_path_conds();
     auto result = solver.solve(cond);
     if (!result.has_value()) {
-      // TODO: current implementation is buggy, there could be other reachable
-      // unexplored paths
-      std::cout << "Found an unreachable path, marking it as unreachable..."
-                << std::endl;
+      GENSYM_INFO("Found an unreachable path, marking it as unreachable...");
       unexplored->fillUnreachableNode();
       continue;
     }
     auto new_env = result.value();
     SymEnv.update(std::move(new_env));
     try {
+      GENSYM_INFO("Now execute the program with symbolic environment: ");
+      GENSYM_INFO(SymEnv.to_string());
       entrypoint();
-      std::cout << "Execution finished successfully with symbolic environment:"
-                << std::endl;
-      std::cout << SymEnv.to_string() << std::endl;
+      GENSYM_INFO("Execution finished successfully with symbolic environment:");
+      GENSYM_INFO(SymEnv.to_string());
     } catch (...) {
       ExploreTree.fillFailedNode();
-      std::cout << "Caught runtime error with symbolic environment:"
-                << std::endl;
-      std::cout << SymEnv.to_string() << std::endl;
+      GENSYM_INFO("Caught runtime error with symbolic environment:");
+      GENSYM_INFO(SymEnv.to_string());
       return;
     }
+#if defined(RUN_ONCE)
+    return;
+#endif
   }
 }
 

headers/wasm/concrete_rt.hpp

@@ -72,9 +72,7 @@ class Stack_t {
 
   Num pop() {
 #ifdef DEBUG
-    if (count == 0) {
-      throw std::runtime_error("Stack underflow");
-    }
+    assert(count > 0 && "Stack underflow");
 #endif
     Num num = stack_ptr[count - 1];
     count--;
@@ -117,7 +115,7 @@ class Stack_t {
 
   void initialize() {
     // todo: remove this method
-   reset();
+    reset();
   }
 
   void reset() { count = 0; }

headers/wasm/controls.hpp

@@ -0,0 +1,5 @@
+#include <functional>
+#include <variant>
+
+using MCont_t = std::function<std::monostate(std::monostate)>;
+using Cont_t = std::function<std::monostate(MCont_t)>;

headers/wasm/smt_solver.hpp

@@ -3,6 +3,7 @@
 
 #include "concrete_rt.hpp"
 #include "symbolic_rt.hpp"
+#include "utils.hpp"
 #include "z3++.h"
 #include <array>
 #include <set>
@@ -35,8 +36,8 @@ class Solver {
       std::vector<Num> result;
       // Reference:
       // https://github.com/Z3Prover/z3/blob/master/examples/c%2B%2B/example.cpp#L59
-
-      std::cout << "Solved Z3 model" << std::endl << model << std::endl;
+      GENSYM_INFO("Solved Z3 model");
+      GENSYM_INFO(model);
       for (unsigned i = 0; i < model.size(); ++i) {
         z3::func_decl var = model[i];
         z3::expr value = model.get_const_interp(var);
@@ -48,8 +49,7 @@ class Solver {
           }
           result[id] = Num(value.get_numeral_int64());
         } else {
-          std::cout << "Find a variable that is not created by GenSym: " << name
-                    << std::endl;
+          GENSYM_INFO("Find a variable that is not created by GenSym: " + name);
         }
       }
       return result;

headers/wasm/symbolic_rt.hpp

@@ -2,7 +2,9 @@
 #define WASM_SYMBOLIC_RT_HPP
 
 #include "concrete_rt.hpp"
+#include "controls.hpp"
 #include <cassert>
+#include <cstddef>
 #include <cstdio>
 #include <fstream>
 #include <iterator>
@@ -22,6 +24,12 @@ class Symbolic {
 
 static int max_id = 0;
 
+#ifdef NO_REUSE
+static bool REUSE_MODE = false;
+#else
+static bool REUSE_MODE = true;
+#endif
+
 class Symbol : public Symbolic {
 public:
   // TODO: add type information to determine the size of bitvector
@@ -65,6 +73,10 @@ struct SymVal {
   SymVal negate() const;
 };
 
+static SymVal make_symbolic(int index) {
+  return SymVal(std::make_shared<Symbol>(index));
+}
+
 inline SymVal Concrete(Num num) {
   return SymVal(std::make_shared<SymConcrete>(num));
 }
@@ -133,6 +145,8 @@ inline SymVal SymVal::makeSymbolic() const {
   }
 }
 
+class Snapshot_t;
+
 class SymStack_t {
 public:
   void push(SymVal val) {
@@ -142,18 +156,37 @@ class SymStack_t {
 
   SymVal pop() {
     // Pop a symbolic value from the stack
+
+#ifdef DEBUG
+    printf("[Debug] poping from stack, size of symbolic stack is: %zu\n",
+           stack.size());
+#endif
     auto ret = stack.back();
     stack.pop_back();
     return ret;
   }
 
   SymVal peek() { return stack.back(); }
 
+  std::monostate shift(int32_t offset, int32_t size) {
+    auto n = stack.size();
+    for (size_t i = n - size; i < n; ++i) {
+      stack[i - offset] = stack[i];
+    }
+    stack.resize(n - offset);
+    return std::monostate();
+  }
+
   void reset() {
     // Reset the symbolic stack
     stack.clear();
   }
 
+  void reuse(Snapshot_t snapshot);
+
+  size_t size() const { return stack.size(); }
+
+private:
   std::vector<SymVal> stack;
 };
 
@@ -187,9 +220,46 @@ class SymFrames_t {
     stack.clear();
   }
 
+  void reuse(Snapshot_t snapshot);
+
   std::vector<SymVal> stack;
 };
 
+// A snapshot of the symbolic state and execution context (control)
+class Snapshot_t {
+public:
+  explicit Snapshot_t();
+
+  SymStack_t get_stack() const { return stack; }
+  SymFrames_t get_frames() const { return frames; }
+
+private:
+  SymStack_t stack;
+  SymFrames_t frames;
+};
+
+inline void SymStack_t::reuse(Snapshot_t snapshot) {
+// Reusing the symbolic stack from the snapshot
+#ifdef DEBUG
+  std::cout << "Reusing symbolic state from snapshot" << std::endl;
+  std::cout << "Old stack size = " << stack.size() << std::endl;
+  std::cout << "New stack size = " << snapshot.get_stack().stack.size()
+            << std::endl;
+#endif
+  stack = snapshot.get_stack().stack;
+}
+
+inline void SymFrames_t::reuse(Snapshot_t snapshot) {
+// Reusing the symbolic frames from the snapshot
+#ifdef DEBUG
+  std::cout << "Reusing symbolic state from snapshot" << std::endl;
+  std::cout << "Old frame size = " << stack.size() << std::endl;
+  std::cout << "New frame size = " << snapshot.get_frames().stack.size()
+            << std::endl;
+#endif
+  stack = snapshot.get_frames().stack;
+}
+
 static SymFrames_t SymFrames;
 
 struct Node;
@@ -199,7 +269,7 @@ struct NodeBox {
   std::unique_ptr<Node> node;
   NodeBox *parent;
 
-  std::monostate fillIfElseNode(SymVal cond);
+  std::monostate fillIfElseNode(SymVal cond, const Snapshot_t &snapshot);
   std::monostate fillFinishedNode();
   std::monostate fillFailedNode();
   std::monostate fillUnreachableNode();
@@ -251,8 +321,9 @@ struct IfElseNode : Node {
   SymVal cond;
   std::unique_ptr<NodeBox> true_branch;
   std::unique_ptr<NodeBox> false_branch;
+  Snapshot_t snapshot;
 
-  IfElseNode(SymVal cond, NodeBox *parent)
+  IfElseNode(SymVal cond, NodeBox *parent, Snapshot_t snapshot)
       : cond(cond), true_branch(std::make_unique<NodeBox>(parent)),
         false_branch(std::make_unique<NodeBox>(parent)) {}
 
@@ -367,13 +438,15 @@ inline NodeBox::NodeBox(NodeBox *parent)
       /* TODO: avoid allocation of unexplored node */
       parent(parent) {}
 
-inline std::monostate NodeBox::fillIfElseNode(SymVal cond) {
-  // fill the current NodeBox with an ifelse branch node it's unexplored
+inline std::monostate NodeBox::fillIfElseNode(SymVal cond,
+                                              const Snapshot_t &snapshot) {
+  // fill the current NodeBox with an ifelse branch node when it's unexplored
   if (dynamic_cast<UnExploredNode *>(node.get())) {
-    node = std::make_unique<IfElseNode>(cond, this);
+    node = std::make_unique<IfElseNode>(cond, this, snapshot);
   }
-  assert(dynamic_cast<IfElseNode *>(node.get()) != nullptr &&
-         "Current node is not an IfElseNode, cannot fill it!");
+  assert(
+      dynamic_cast<IfElseNode *>(node.get()) != nullptr &&
+      "Current node is not an Unexplored nor an IfElseNode, cannot fill it!");
   return std::monostate();
 }
 
@@ -427,6 +500,32 @@ inline std::vector<SymVal> NodeBox::collect_path_conds() {
   return result;
 }
 
+class Reuse_t {
+public:
+  Reuse_t() : reuse_flag(false) {}
+  bool is_reusing() {
+    // we are in reuse mode and the flag is set
+    return REUSE_MODE && reuse_flag;
+  }
+
+  void turn_on_reusing() { reuse_flag = true; }
+
+  void turn_off_reusing() { reuse_flag = false; }
+
+private:
+  bool reuse_flag;
+};
+
+static Reuse_t Reuse;
+
+inline Snapshot_t::Snapshot_t() : stack(SymStack), frames(SymFrames) {
+#ifdef DEBUG
+  std::cout << "Creating snapshot of size " << stack.size() << std::endl;
+#endif
+  assert(!Reuse.is_reusing() &&
+         "Creating snapshot while reusing the symbolic stack");
+}
+
 class ExploreTree_t {
 public:
   explicit ExploreTree_t()
@@ -435,14 +534,19 @@ class ExploreTree_t {
   void reset_cursor() {
     // Reset the cursor to the root of the tree
     cursor = root.get();
+    Reuse.turn_off_reusing();
+    // if root cursor is a branch node, then we can reuse the snapshot inside it
+    if (auto ite = dynamic_cast<IfElseNode *>(cursor->node.get())) {
+      Reuse.turn_on_reusing();
+    }
   }
 
   std::monostate fillFinishedNode() { return cursor->fillFinishedNode(); }
 
   std::monostate fillFailedNode() { return cursor->fillFailedNode(); }
 
-  std::monostate fillIfElseNode(SymVal cond) {
-    return cursor->fillIfElseNode(cond);
+  std::monostate fillIfElseNode(SymVal cond, const Snapshot_t &snapshot) {
+    return cursor->fillIfElseNode(cond, snapshot);
   }
 
   std::monostate moveCursor(bool branch) {
@@ -456,6 +560,24 @@ class ExploreTree_t {
     } else {
       cursor = if_else_node->false_branch.get();
     }
+
+    if (dynamic_cast<UnExploredNode *>(cursor->node.get())) {
+      // If we meet an unexplored node, resume the snapshot before and keep
+      // going
+
+#ifdef DEBUG
+      std::cout << "Resuming snapshot for unexplored node" << std::endl;
+#endif
+      if (Reuse.is_reusing()) {
+        Reuse.turn_off_reusing();
+        SymStack.reuse(if_else_node->snapshot);
+      }
+    } else if (dynamic_cast<IfElseNode *>(cursor->node.get())) {
+      // if we are moving to a branch node, we must have reused the symbolic
+      // states
+      assert((!REUSE_MODE || Reuse.is_reusing()) &&
+             "Moving to a branch node without reusing symbolic states");
+    }
     return std::monostate();
   }
 
@@ -531,9 +653,7 @@ class SymEnv_t {
     return map[symbol->get_id()];
   }
 
-  void update(std::vector<Num> new_env) {
-    map = std::move(new_env);
-  }
+  void update(std::vector<Num> new_env) { map = std::move(new_env); }
 
   std::string to_string() const {
     std::string result;
@@ -548,7 +668,7 @@ class SymEnv_t {
   }
 
 private:
-  std::vector<Num> map;    // The symbolic environment, a vector of Num
+  std::vector<Num> map; // The symbolic environment, a vector of Num
 };
 
 static SymEnv_t SymEnv;