give every branch node an ID

Author: butterunderflow

headers/wasm/concolic_driver.hpp

@@ -100,7 +100,7 @@ static void start_concolic_execution_with(
 }
 
 static void start_concolic_execution_with(
-    std::function<std::monostate(std::monostate)> entrypoint) {
+    std::function<std::monostate(std::monostate)> entrypoint, int branchCount) {
 
   const char *env_tree_file = std::getenv("TREE_FILE");
 

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 &&
@@ -581,8 +582,8 @@ class ExploreTree_t {
 
   std::monostate fillFailedNode() { return cursor->fillFailedNode(); }
 
-  std::monostate fillIfElseNode(SymVal cond) {
-    return cursor->fillIfElseNode(cond);
+  std::monostate fillIfElseNode(SymVal cond, int id) {
+    return cursor->fillIfElseNode(cond, id);
   }
 
   std::monostate moveCursor(bool branch, Snapshot_t snapshot) {

src/main/scala/wasm/StagedConcolicMiniWasm.scala

@@ -19,6 +19,26 @@ import gensym.wasm.symbolic.Concrete
 import gensym.wasm.symbolic.ExploreTree
 import gensym.structure.freer.Explore
 
+object Counter {
+  var currentId: Int = 0
+  private val dict = new HashMap[WIR, Int]()
+
+  def reset(): Unit = {
+    currentId = 0
+    dict.clear()
+  }
+
+  def getId(wir: WIR): Int = {
+    if (dict.contains(wir)) {
+      dict(wir)
+    } else {
+      val id = currentId
+      currentId += 1
+      dict(wir) = id
+      id
+    }
+  }
+}
 @virtualize
 trait StagedWasmEvaluator extends SAIOps {
   def module: ModuleInstance
@@ -365,7 +385,8 @@ trait StagedWasmEvaluator extends SAIOps {
           val newRestCtx = restCtx.shift(offset, funcTy.out.size)
           eval(rest, kont, mk, trail)(newRestCtx)
         })
-        ExploreTree.fillWithIfElse(symCond.s)
+        val id = Counter.getId(inst)
+        ExploreTree.fillWithIfElse(symCond.s, id)
         def thnK: Rep[Cont[Unit]] = topFun((mk: Rep[MCont[Unit]]) => {
           info("Entering the true branch of the if")
           eval(thn, restK _, mk, restK _ :: trail)(newCtx)
@@ -392,7 +413,8 @@ trait StagedWasmEvaluator extends SAIOps {
         val cond = Stack.popC(ty)
         val symCond = Stack.popS(ty)
         info(s"The br_if(${label})'s condition is ", cond.toInt)
-        ExploreTree.fillWithIfElse(symCond.s)
+        val id = Counter.getId(inst)
+        ExploreTree.fillWithIfElse(symCond.s, id)
         def thnK: Rep[Cont[Unit]] = topFun((mk: Rep[MCont[Unit]]) => {
           trail(label)(newCtx)(mk)
         })
@@ -423,7 +445,8 @@ trait StagedWasmEvaluator extends SAIOps {
             val labelSym = Stack.peekS(ty)
             val cond = (label - toStagedNum(I32V(idx))).isZero()
             val condSym = (labelSym - toStagedSymbolicNum(I32V(idx))).isZero()
-            ExploreTree.fillWithIfElse(condSym.s)
+            val id = Counter.getId(inst)
+            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)
             // TODO: store snapshot into this snapshot node
@@ -622,6 +645,7 @@ trait StagedWasmEvaluator extends SAIOps {
   }
 
   def evalTop(mkont: Rep[MCont[Unit]], main: Option[String]): Rep[Unit] = {
+    Counter.reset()
     val funBody: FuncBodyDef = main match {
       case Some(func_name) =>
         module.defs.flatMap({
@@ -912,8 +936,8 @@ trait StagedWasmEvaluator extends SAIOps {
 
   // Exploration tree, 
   object ExploreTree {
-    def fillWithIfElse(s: Rep[SymVal]): Rep[Unit] = {
-      "tree-fill-if-else".reflectCtrlWith[Unit](s)
+    def fillWithIfElse(s: Rep[SymVal], id: Int): Rep[Unit] = {
+      "tree-fill-if-else".reflectCtrlWith[Unit](s, id)
     }
 
     def fillWithFinished(): Rep[Unit] = {
@@ -1448,8 +1472,8 @@ trait StagedWasmCppGen extends CGenBase with CppSAICodeGenBase {
       emit("SymEnv.read("); shallow(sym); emit(")")
     case Node(_, "assert-true", List(cond), _) =>
       emit("GENSYM_ASSERT("); shallow(cond); emit(")")
-    case Node(_, "tree-fill-if-else", List(sym), _) =>
-      emit("ExploreTree.fillIfElseNode("); shallow(sym); emit(")")
+    case Node(_, "tree-fill-if-else", List(sym, id), _) =>
+      emit("ExploreTree.fillIfElseNode("); shallow(sym); emit(", "); emit(id.toString); emit(")")
     case Node(_, "tree-fill-finished", List(), _) =>
       emit("ExploreTree.fillFinishedNode()")
     case Node(_, "tree-move-cursor", List(b, snapshot), _) =>
@@ -1496,12 +1520,12 @@ trait StagedWasmCppGen extends CGenBase with CppSAICodeGenBase {
     emitDatastructures(stream)
     emitFunctions(stream)
     emit(src)
-    emitln("""
+    emitln(s"""
     |/*****************************************
     |End of Generated Code
     |*******************************************/
     |int main(int argc, char *argv[]) {
-    |  start_concolic_execution_with(Snippet);
+    |  start_concolic_execution_with(Snippet, ${Counter.currentId});
     |  return 0;
     |}""".stripMargin)
   }