a new exploring strategy: exit when all branches are covered

Author: butterunderflow

headers/wasm/concolic_driver.hpp

@@ -11,14 +11,25 @@
 #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;
 
 public:
   ConcolicDriver(std::function<void()> entrypoint,
                  std::optional<std::string> tree_file, int branchCount)
       : entrypoint(entrypoint), tree_file(tree_file) {
-    ExploreTree.branch_cov_map.assign(branchCount, false);
+    ExploreTree.true_branch_cov_map.assign(branchCount, false);
+    ExploreTree.false_branch_cov_map.assign(branchCount, false);
   }
   void run();
 
@@ -76,7 +87,15 @@ inline void ConcolicDriver::run() {
       ExploreTree.fillFailedNode();
       GENSYM_INFO("Caught runtime error with symbolic environment:");
       GENSYM_INFO(SymEnv.to_string());
-      return;
+      switch (EXPLORE_MODE) {
+      case ExploreMode::EarlyExit:
+        return;
+      case ExploreMode::ExitByCoverage:
+        if (ExploreTree.all_branch_covered()) {
+          GENSYM_INFO("All branches covered, exiting...");
+          return;
+        }
+      }
     }
 #if defined(RUN_ONCE)
     return;

headers/wasm/symbolic_rt.hpp

@@ -291,7 +291,7 @@ struct NodeBox {
   std::unique_ptr<Node> node;
   NodeBox *parent;
 
-  std::monostate fillIfElseNode(SymVal cond);
+  std::monostate fillIfElseNode(SymVal cond, int id);
   std::monostate fillFinishedNode();
   std::monostate fillFailedNode();
   std::monostate fillUnreachableNode();
@@ -344,10 +344,11 @@ struct IfElseNode : Node {
   SymVal cond;
   std::unique_ptr<NodeBox> true_branch;
   std::unique_ptr<NodeBox> false_branch;
+  int id;
 
-  IfElseNode(SymVal cond, NodeBox *parent)
+  IfElseNode(SymVal cond, NodeBox *parent, int id)
       : cond(cond), true_branch(std::make_unique<NodeBox>(parent)),
-        false_branch(std::make_unique<NodeBox>(parent)) {}
+        false_branch(std::make_unique<NodeBox>(parent)), id(id) {}
 
   std::string to_string() override {
     std::string result = "IfElseNode {\n";
@@ -480,10 +481,10 @@ inline NodeBox::NodeBox(NodeBox *parent)
       /* TODO: avoid allocation of unexplored node */
       parent(parent) {}
 
-inline std::monostate NodeBox::fillIfElseNode(SymVal cond) {
+inline std::monostate NodeBox::fillIfElseNode(SymVal cond, int id) {
   // fill the current NodeBox with an ifelse branch node when it's unexplored
   if (this->isUnexplored()) {
-    node = std::make_unique<IfElseNode>(cond, this);
+    node = std::make_unique<IfElseNode>(cond, this, id);
   }
   assert(
       dynamic_cast<IfElseNode *>(node.get()) != nullptr &&
@@ -582,8 +583,7 @@ class ExploreTree_t {
   std::monostate fillFailedNode() { return cursor->fillFailedNode(); }
 
   std::monostate fillIfElseNode(SymVal cond, int id) {
-    branch_cov_map[id] = true;
-    return cursor->fillIfElseNode(cond);
+    return cursor->fillIfElseNode(cond, id);
   }
 
   std::monostate moveCursor(bool branch, Snapshot_t snapshot) {
@@ -593,9 +593,11 @@ class ExploreTree_t {
         if_else_node != nullptr &&
         "Can't move cursor when the branch node is not initialized correctly!");
     if (branch) {
+      true_branch_cov_map[if_else_node->id] = true;
       if_else_node->false_branch->fillSnapshotNode(snapshot);
       cursor = if_else_node->true_branch.get();
     } else {
+      false_branch_cov_map[if_else_node->id] = true;
       if_else_node->true_branch->fillSnapshotNode(snapshot);
       cursor = if_else_node->false_branch.get();
     }
@@ -637,9 +639,14 @@ class ExploreTree_t {
     // For now, we just iterate through the tree and return the first unexplored
     return pick_unexplored_of(root.get());
   }
-  std::vector<bool> branch_cov_map;
+  std::vector<bool> true_branch_cov_map;
+  std::vector<bool> false_branch_cov_map;
   bool all_branch_covered() const {
-    for (bool covered : branch_cov_map) {
+    for (bool covered : true_branch_cov_map) {
+      if (!covered)
+        return false;
+    }
+    for (bool covered : false_branch_cov_map) {
       if (!covered)
         return false;
     }

src/main/scala/wasm/StagedConcolicMiniWasm.scala

@@ -21,22 +21,30 @@ import gensym.structure.freer.Explore
 
 object Counter {
   var currentId: Int = 0
-  private val dict = new HashMap[WIR, Int]()
+
+  // WIR is the branch's corresponding ast, while the Int stands for the nth
+  // branch of the AST(a WIR may contain multiple branches, e.g., br_table)
+  private val dict = new HashMap[(WIR, Int), Int]()
 
   def reset(): Unit = {
     currentId = 0
     dict.clear()
   }
 
-  def getId(wir: WIR): Int = {
-    if (dict.contains(wir)) {
-      dict(wir)
+  def getId(wir: WIR, nth: Int = 0): Int = {
+    if (dict.contains((wir, nth))) {
+      dict((wir, nth))
     } else {
       val id = currentId
       currentId += 1
-      dict(wir) = id
+      dict((wir, nth)) = id
       id
     }
+
+  }
+
+  def getId(wir: WIR): Int = {
+    getId(wir, 0)
   }
 }
 @virtualize
@@ -445,7 +453,7 @@ trait StagedWasmEvaluator extends SAIOps {
             val labelSym = Stack.peekS(ty)
             val cond = (label - toStagedNum(I32V(idx))).isZero()
             val condSym = (labelSym - toStagedSymbolicNum(I32V(idx))).isZero()
-            val id = Counter.getId(inst)
+            val id = Counter.getId(inst, idx)
             ExploreTree.fillWithIfElse(condSym.s, id)
             // When moving the cursor to a branch, we mark another branch as
             // snapshotNode (this is done by moveCursor's runtime implementation)

src/test/scala/genwasym/TestStagedConcolicEval.scala

@@ -9,12 +9,14 @@ import gensym.wasm.parser._
 import gensym.wasm.stagedconcolicminiwasm._
 
 class TestStagedConcolicEval extends FunSuite {
-  def testFileConcolicCpp(filename: String, main: Option[String] = None) = {
+  def testFileConcolicCpp(filename: String,
+                          main: Option[String] = None,
+                          exitByCoverage: Boolean = false) = {
     val moduleInst = ModuleInstance(Parser.parseFile(filename))
     val cppFile = s"$filename.cpp"
     val exe = s"$cppFile.exe"
     val exploreTreeFile = s"$filename.tree.dot"
-    WasmToCppCompiler.compileToExe(moduleInst, main, cppFile, exe, true)
+    WasmToCppCompiler.compileToExe(moduleInst, main, cppFile, exe, true, if (exitByCoverage) "BY_COVERAGE" else "EARLY_EXIT")
 
     import sys.process._
     val result = Process(s"./$exe", None, "TREE_FILE" -> exploreTreeFile).!!
@@ -52,6 +54,14 @@ class TestStagedConcolicEval extends FunSuite {
     testFileConcolicCpp("./benchmarks/wasm/staged/brtable_concolic.wat")
   }
 
+  test("bug-finding-cov-concolic") {
+    testFileConcolicCpp("./benchmarks/wasm/branch-strip-buggy.wat", Some("real_main"), exitByCoverage=true)
+  }
+
+  test("brtable-bug-finding-cov-concolic") {
+    testFileConcolicCpp("./benchmarks/wasm/staged/brtable_concolic.wat", exitByCoverage=true)
+  }
+
   test("return-poly - concrete") {
     testFileConcreteCpp("./benchmarks/wasm/staged/return_poly.wat", Some("$real_main"), expect=Some(List(42)))
   }