a bitmap to record the branch coverage

Author: butterunderflow

headers/wasm/concolic_driver.hpp

@@ -6,6 +6,7 @@
 #include "symbolic_rt.hpp"
 #include "utils.hpp"
 #include <functional>
+#include <optional>
 #include <ostream>
 #include <string>
 #include <vector>
@@ -14,10 +15,11 @@ 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) {}
+  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);
+  }
   void run();
 
 private:
@@ -92,22 +94,16 @@ static std::monostate reset_stacks() {
   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, int branchCount) {
 
   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{}); });
+  auto tree_file =
+      env_tree_file ? std::make_optional(env_tree_file) : std::nullopt;
+
+  ConcolicDriver driver = ConcolicDriver(
+      [=]() { entrypoint(std::monostate{}); }, tree_file, branchCount);
   driver.run();
 }
 

headers/wasm/symbolic_rt.hpp

@@ -291,7 +291,7 @@ struct NodeBox {
   std::unique_ptr<Node> node;
   NodeBox *parent;
 
-  std::monostate fillIfElseNode(SymVal cond, int id);
+  std::monostate fillIfElseNode(SymVal cond);
   std::monostate fillFinishedNode();
   std::monostate fillFailedNode();
   std::monostate fillUnreachableNode();
@@ -344,11 +344,10 @@ struct IfElseNode : Node {
   SymVal cond;
   std::unique_ptr<NodeBox> true_branch;
   std::unique_ptr<NodeBox> false_branch;
-  int id;
 
-  IfElseNode(SymVal cond, NodeBox *parent, int id)
+  IfElseNode(SymVal cond, NodeBox *parent)
       : cond(cond), true_branch(std::make_unique<NodeBox>(parent)),
-        false_branch(std::make_unique<NodeBox>(parent)), id(id) {}
+        false_branch(std::make_unique<NodeBox>(parent)) {}
 
   std::string to_string() override {
     std::string result = "IfElseNode {\n";
@@ -481,10 +480,10 @@ inline NodeBox::NodeBox(NodeBox *parent)
       /* TODO: avoid allocation of unexplored node */
       parent(parent) {}
 
-inline std::monostate NodeBox::fillIfElseNode(SymVal cond, int id) {
+inline std::monostate NodeBox::fillIfElseNode(SymVal cond) {
   // fill the current NodeBox with an ifelse branch node when it's unexplored
   if (this->isUnexplored()) {
-    node = std::make_unique<IfElseNode>(cond, this, id);
+    node = std::make_unique<IfElseNode>(cond, this);
   }
   assert(
       dynamic_cast<IfElseNode *>(node.get()) != nullptr &&
@@ -583,7 +582,8 @@ class ExploreTree_t {
   std::monostate fillFailedNode() { return cursor->fillFailedNode(); }
 
   std::monostate fillIfElseNode(SymVal cond, int id) {
-    return cursor->fillIfElseNode(cond, id);
+    branch_cov_map[id] = true;
+    return cursor->fillIfElseNode(cond);
   }
 
   std::monostate moveCursor(bool branch, Snapshot_t snapshot) {
@@ -637,6 +637,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;
+  bool all_branch_covered() const {
+    for (bool covered : branch_cov_map) {
+      if (!covered)
+        return false;
+    }
+    return true;
+  }
 
 private:
   NodeBox *pick_unexplored_of(NodeBox *node) {