Concolic driver

.github/workflows/scala.yml

@@ -9,7 +9,7 @@ on:
 jobs:
   build:
 
-    runs-on: ubuntu-20.04
+    runs-on: ubuntu-22.04
     defaults:
       run:
         working-directory: ./
@@ -27,7 +27,7 @@ jobs:
     - name: Set up dependencies
       run: |
         sudo apt-get update
-        sudo DEBIAN_FRONTEND=noninteractive apt-get install -y git g++ cmake bison flex libboost-all-dev python
+        sudo DEBIAN_FRONTEND=noninteractive apt-get install -y git g++ cmake bison flex libboost-all-dev 2to3 python-is-python3
         sudo DEBIAN_FRONTEND=noninteractive apt-get install -y perl minisat curl gnupg2 locales clang-11 wget
     - name: Generate test files (LLVM IR)
       run: |
@@ -77,3 +77,4 @@ jobs:
         sbt 'testOnly gensym.wasm.TestEval'
         sbt 'testOnly gensym.wasm.TestScriptRun'
         sbt 'testOnly gensym.wasm.TestConcolic'
+        sbt 'testOnly gensym.wasm.TestDriver'

benchmarks/wasm/branch-strip-buggy.wat

@@ -0,0 +1,46 @@
+(module
+  (type (;0;) (func (param i32 i32) (result i32)))
+  (type (;1;) (func (param i32)))
+  (func (;0;) (type 0) (param i32 i32) (result i32)
+    local.get 0
+    i32.const 0
+    i32.le_s
+    if (result i32)  ;; label = @1
+      i32.const 1
+    else
+      local.get 1
+      i32.const 0
+      i32.le_s
+    end
+    if (result i32)  ;; label = @1
+      i32.const -1
+    else
+      local.get 0
+      local.get 0
+      i32.mul
+      local.get 1
+      local.get 1
+      i32.mul
+      i32.add
+      i32.const 25
+      i32.eq
+      if (result i32)  ;; label = @2
+        i32.const 1
+      else
+        i32.const 0
+        call 2
+      end
+    end
+  )
+  (export "f" (func 0))
+  (func $real_main
+    ;; TODO: is there a better way to put symbolic values on the stack?
+    i32.const 0
+    i32.symbolic
+    i32.const 1
+    i32.symbolic
+    call 0
+  )
+  (import "console" "assert" (func (type 1)))
+  (export "real_main" (func 1))
+)

benchmarks/wasm/branch-strip.wat

@@ -4,11 +4,14 @@
     local.get 0
     i32.const 0
     i32.le_s
-    local.get 1
-    i32.const 0
-    i32.le_s
-    i32.or
-    if (result i32) ;; label = @1
+    if (result i32)  ;; label = @1
+      i32.const 1
+    else
+      local.get 1
+      i32.const 0
+      i32.le_s
+    end
+    if (result i32)  ;; label = @1
       i32.const -1
     else
       local.get 0
@@ -20,7 +23,7 @@
       i32.add
       i32.const 25
       i32.eq
-      if (result i32) ;; label = @2
+      if (result i32)  ;; label = @2
         i32.const 1
       else
         i32.const 0

benchmarks/wasm/branch-strip1.wat

@@ -0,0 +1,41 @@
+(module
+  (type (;0;) (func (param i32 i32) (result i32)))
+  (func (;0;) (type 0) (param i32 i32) (result i32)
+    local.get 0
+    i32.const 0
+    i32.le_s
+    local.get 1
+    i32.const 0
+    i32.le_s
+    i32.or
+    if (result i32) ;; label = @1
+      i32.const -1
+    else
+      local.get 0
+      local.get 0
+      i32.mul
+      local.get 1
+      local.get 1
+      i32.mul
+      i32.add
+      i32.const 25
+      i32.eq
+      if (result i32) ;; label = @2
+        i32.const 1
+      else
+        i32.const 0
+      end
+    end
+  )
+  (export "f" (func 0))
+  (func $real_main
+    ;; TODO: is there a better way to put symbolic values on the stack?
+    i32.const 0
+    i32.symbolic
+    i32.const 1
+    i32.symbolic
+    call 0
+  )
+
+  (export "real_main" (func 1))
+)

benchmarks/wasm/branch.wat

@@ -2,9 +2,10 @@
   (func $f (param $x i32) (param $y i32) (result i32)
     ;; if (x <= 0 || y <= 0)
     (if (result i32)
-      (i32.or
+      (if (result i32)
         (i32.le_s (local.get $x) (i32.const 0))
-        (i32.le_s (local.get $y) (i32.const 0))
+        (then (i32.const 1))
+        (else (i32.le_s (local.get $y) (i32.const 0)))
       )
       (then (i32.const -1)) ;; return -1
       (else

benchmarks/wasm/branch1.wat

@@ -0,0 +1,29 @@
+(module
+  (func $f (param $x i32) (param $y i32) (result i32)
+    ;; if (x <= 0 || y <= 0)
+    (if (result i32)
+      (i32.or
+        (i32.le_s (local.get $x) (i32.const 0))
+        (i32.le_s (local.get $y) (i32.const 0))
+      )
+      (then (i32.const -1)) ;; return -1
+      (else
+        ;; if (x * x + y * y == 25)
+        (if (result i32)
+          (i32.eq
+            (i32.add
+              (i32.mul (local.get $x) (local.get $x))
+              (i32.mul (local.get $y) (local.get $y))
+            )
+            (i32.const 25)
+          )
+          (then (i32.const 1)) ;; return 1
+          (else (i32.const 0)) ;; return 0
+        )
+      )
+    )
+  )
+
+  ;; Optionally export the function
+  (export "f" (func $f))
+)

src/main/scala/wasm/ConcolicDriver.scala

@@ -9,9 +9,10 @@ import scala.collection.immutable.Queue
 import scala.collection.mutable.{HashMap, HashSet}
 
 import z3.scala._
+import scala.tools.nsc.doc.model.Val
 
 object ConcolicDriver {
-  def condsToEnv(conds: List[Cond])(implicit z3Ctx: Z3Context): HashMap[Int, Value] = {
+  def condsToEnv(conds: List[Cond])(implicit z3Ctx: Z3Context): Option[HashMap[Int, Value]] = {
     val intSort = z3Ctx.mkIntSort()
     val boolSort = z3Ctx.mkBoolSort()
 
@@ -24,16 +25,57 @@ object ConcolicDriver {
           case Add(_) => z3Ctx.mkAdd(symVToZ3(lhs), symVToZ3(rhs)) // does numtype matter?
           case Sub(_) => z3Ctx.mkSub(symVToZ3(lhs), symVToZ3(rhs))
           case Mul(_) => z3Ctx.mkMul(symVToZ3(lhs), symVToZ3(rhs))
-          case _      => ???
+          case Or(_)  => 
+            var result = z3Ctx.mkBVOr(
+              z3Ctx.mkInt2BV(32, symVToZ3(lhs)), 
+              z3Ctx.mkInt2BV(32, symVToZ3(rhs))
+            )
+            z3Ctx.mkBV2Int(result, false)
+          case _      => throw new NotImplementedError(s"Unsupported binary operation: $op")
         }
       case SymUnary(op, v) =>
         op match {
           case _ => ???
         }
       case SymIte(cond, thenV, elseV) => z3Ctx.mkITE(condToZ3(cond), symVToZ3(thenV), symVToZ3(elseV))
-      case Concrete(v)                => ???
-      case _                          => ???
+      case Concrete(v) => 
+        v match {
+          // todo: replace with bitvector
+          case I32V(i) => z3Ctx.mkInt(i, intSort)
+          case I64V(i) => z3Ctx.mkNumeral(i.toString(), intSort)
+          // TODO: Float
+          case _       => ???
+        }
+      case RelCond(op, lhs, rhs) => 
+        val res = op match {
+          case GeS(_) => z3Ctx.mkGE(symVToZ3(lhs), symVToZ3(rhs))
+          case GtS(_) => z3Ctx.mkGT(symVToZ3(lhs), symVToZ3(rhs))
+          case LtS(_) => z3Ctx.mkLT(symVToZ3(lhs), symVToZ3(rhs))
+          case LeS(_) => z3Ctx.mkLE(symVToZ3(lhs), symVToZ3(rhs))
+          case GtU(_) => z3Ctx.mkGT(symVToZ3(lhs), symVToZ3(rhs))
+          case GeU(_) => z3Ctx.mkGE(symVToZ3(lhs), symVToZ3(rhs))
+          case LtU(_) => z3Ctx.mkLT(symVToZ3(lhs), symVToZ3(rhs))
+          case LeU(_) => z3Ctx.mkLE(symVToZ3(lhs), symVToZ3(rhs))
+          case Eq(_)  => z3Ctx.mkEq(symVToZ3(lhs), symVToZ3(rhs))
+          case Ne(_)  => z3Ctx.mkNot(z3Ctx.mkEq(symVToZ3(lhs), symVToZ3(rhs)))
+          case Ge(_)  => z3Ctx.mkGE(symVToZ3(lhs), symVToZ3(rhs))
+          case Gt(_)  => z3Ctx.mkGT(symVToZ3(lhs), symVToZ3(rhs))
+          case Le(_)  => z3Ctx.mkLE(symVToZ3(lhs), symVToZ3(rhs))
+          case Lt(_)  => z3Ctx.mkLT(symVToZ3(lhs), symVToZ3(rhs))
+        }
+        // convert resutl to int
+        z3Ctx.mkITE(res, z3Ctx.mkInt(1, intSort), z3Ctx.mkInt(0, intSort))
+      case _                          => throw new NotImplementedError(s"Unsupported SymVal: $symV")
+    }
+
+    def getIndexOfSym(sym: String): Int = {
+      val pattern = ".*_(\\d+)$".r
+      sym match {
+        case pattern(index) => index.toInt
+        case _              => throw new IllegalArgumentException(s"Invalid symbol format: $sym")
+      }
     }
+
     def condToZ3(cond: Cond): Z3AST = cond match {
       case CondEqz(v) => z3Ctx.mkEq(symVToZ3(v), z3Ctx.mkInt(0, intSort))
       case Not(cond)  => z3Ctx.mkNot(condToZ3(cond))
@@ -49,74 +91,93 @@ object ConcolicDriver {
     }
 
     // solve for all vars
+    println(s"solving constraints: ${solver.toString()}")
     solver.check() match {
       case Some(true) => {
         val model = solver.getModel()
         val vars = model.getConsts
-        val env = HashMap()
+        val env = HashMap[Int, Value]()
         for (v <- vars) {
           val name = v.getName
           val ast = z3Ctx.mkConst(name, intSort)
           val value = model.eval(ast)
+          println(s"name: $name")
+          println(s"value: $value")
+          // TODO: support other types of symbolic values(currently only i32)
           val intValue = if (value.isDefined && value.get.getSort.isIntSort) {
-            I32V(value.toString.toInt)
+            val negPattern = """\(\-\s*(\d+)\)""".r
+            val plainPattern = """(-?\d+)""".r
+            val num = value.get.toString match {
+              case negPattern(digits) => -digits.toInt
+              case plainPattern(number)  => number.toInt
+              case _ => throw new IllegalArgumentException("Invalid format")
+            }
+            I32V(num)
           } else {
             ???
           }
-          // env += (name.toString -> intValue)
-          ???
+          env += (getIndexOfSym(name.toString) -> intValue)
         }
-        ???
-        // env
+        println(s"solved env: $env")
+        Some(env)
       }
-      case _ => ???
+      case _ => None
     }
   }
 
   def negateCond(conds: List[Cond], i: Int): List[Cond] = {
-    ???
+    conds(i).negated :: conds.drop(i + 1)
   }
 
   def checkPCToFile(pc: List[Cond]): Unit = {
+    // TODO: what this function for?
     ???
   }
 
   def exec(module: Module, mainFun: String, startEnv: HashMap[Int, Value])(implicit z3Ctx: Z3Context) = {
     val worklist = Queue(startEnv)
-    // val visited = ??? // how to avoid re-execution
-
+    val unreachables = HashSet[ExploreTree]()
+    val visited = HashSet[ExploreTree]()
+    // the root node of exploration tree
+    val root = new ExploreTree()
     def loop(worklist: Queue[HashMap[Int, Value]]): Unit = worklist match {
       case Queue() => ()
       case env +: rest => {
         val moduleInst = ModuleInstance(module)
         Evaluator(moduleInst).execWholeProgram(
           Some(mainFun),
           env,
-          (_endStack, _endSymStack, pathConds) => {
-            println(s"env: $env")
-            val newEnv = condsToEnv(pathConds)
-            val newWork = for (i <- 0 until pathConds.length) yield {
-              val newConds = negateCond(pathConds, i)
-              checkPCToFile(newConds)
-              condsToEnv(newConds)
+          root,
+          (_endStack, _endSymStack, tree) => {
+            tree.fillWithFinished()
+            val unexploredTrees = root.unexploredTrees()
+            // if a node is already visited or marked as unreachable, don't try to explore it
+            val addedNewWork = unexploredTrees.filterNot(unreachables.contains)
+                                              .filterNot(visited.contains)
+                                              .flatMap { tree =>
+              val conds = tree.collectConds()
+              val newEnv = condsToEnv(conds)
+              // if the path conditions to reach this node are unsatisfiable, mark it as unreachable.
+              if (newEnv.isEmpty) unreachables.add(tree)
+              newEnv
+            }
+            for (tree <- unexploredTrees) {
+              visited.add(tree)
             }
-            loop(rest ++ newWork)
+            loop(rest ++ addedNewWork)
           }
         )
       }
     }
 
     loop(worklist)
+    println(s"unreachable trees number: ${unreachables.size}")
+    println(s"number of normal explored paths: ${root.finishedTrees().size}")
+    val failedTrees = root.failedTrees()
+    println(s"number of failed explored paths: ${failedTrees.size}")
+    for (tree <- failedTrees) {
+      println(s"find a failed endpoint: ${tree}")
+    }
+    println(s"exploration tree: ${root.toString}")
   }
 }
-
-object DriverSimpleTest {
-  def fileTestDriver(file: String, mainFun: String, startEnv: HashMap[Int, Value]) = {
-    import gensym.wasm.concolicminiwasm._
-    import collection.mutable.ArrayBuffer
-    val module = Parser.parseFile(file)
-    ConcolicDriver.exec(module, mainFun, startEnv)(new Z3Context())
-  }
-
-  def main(args: Array[String]) = {}
-}