From 0e25181c2eaacbab1b1998b46d55c11c327bd33c Mon Sep 17 00:00:00 2001
From: Mikail Khan <mikail@mikail-khan.com>
Date: Wed, 29 Nov 2023 03:48:34 -0500
Subject: [PATCH] concolic driver outline

---
 src/main/scala/wasm/ConcolicDriver.scala | 44 ++++++++++++++++++++++++
 1 file changed, 44 insertions(+)
 create mode 100644 src/main/scala/wasm/ConcolicDriver.scala

diff --git a/src/main/scala/wasm/ConcolicDriver.scala b/src/main/scala/wasm/ConcolicDriver.scala
new file mode 100644
index 00000000..59a33852
--- /dev/null
+++ b/src/main/scala/wasm/ConcolicDriver.scala
@@ -0,0 +1,44 @@
+package gensym.wasm.concolicdriver
+
+import gensym.wasm.concolicminiwasm._
+import gensym.wasm.ast._
+import gensym.wasm.symbolic._
+
+import scala.collection.immutable.Queue
+import scala.collection.mutable.{HashMap, HashSet}
+
+object ConcolicDriver {
+  def condsToEnv(conds: List[Cond]): HashMap[Int, Value] = {
+    ???
+  }
+
+  def negateCond(conds: List[Cond], i: Int): List[Cond] = {
+    ???
+  }
+
+  def checkPCToFile(pc: List[Cond]): Unit = {
+    ???
+  }
+
+  def exec(module: Module, mainFun: String, startEnv: HashMap[Int, Value]) = {
+    val worklist = Queue(startEnv)
+    // val visited = ???
+
+    def loop(worklist: Queue[HashMap[Int, Value]]): Unit = worklist match {
+      case Queue() => ()
+      case env +: rest => {
+        Evaluator.execWholeProgram(module, mainFun, env, (_endStack, _endSymStack, pathConds) => {
+          val newEnv = condsToEnv(pathConds)
+          val newWork = for (i <- 0 until pathConds.length) yield {
+            val newConds = negateCond(pathConds, i)
+            checkPCToFile(newConds)
+            condsToEnv(newConds)
+          }
+          loop(rest ++ newWork)
+        })
+      }
+    }
+
+    loop(worklist)
+  }
+}