filled some concolicminiwasm gaps

benchmarks/wasm/build_wat_c.sh

@@ -9,7 +9,7 @@ sudo docker run --rm \
     --volume "$(pwd):/home/wasp/tmp" \
     -w "/home/wasp/tmp" \
     ghcr.io/wasp-platform/wasp:latest \
-    clang --target=wasm32 --no-standard-libraries -Wl,--export-all -Wl,--no-entry -o "$2.temp" $1
+    clang --target=wasm32 -O0 --no-standard-libraries -Wl,--export-all -Wl,--no-entry -o "$2.temp" $1
 
 # clang-15 --target=wasm32 --no-standard-libraries -Wl,--export-all -Wl,--no-entry -o $2.temp $1
 

benchmarks/wasm/test.wat

@@ -148,4 +148,4 @@
   (export "__heap_base" (global 4))
   (export "__memory_base" (global 5))
   (export "__table_base" (global 6))
-  (data (;0;) (i32.const 1024) "a\00b\00"))
+  (data (;0;) (i32.const 1024) "a\00b\00"))

benchmarks/wasm/test_loop.c

@@ -0,0 +1,15 @@
+int sym_int(char* name) { return (int) name; }
+void assert(int expr) {}
+
+int main() {
+  int a = sym_int("a");
+  int b = sym_int("b");
+  int n = 0;
+
+  while (a < b) {
+    a++;
+    n++;
+  }
+
+  return n;
+}

build.sbt

@@ -13,7 +13,7 @@ libraryDependencies += "org.typelevel" %% "cats-free" % "1.6.0"
 libraryDependencies += "com.github.mpilquist" %% "simulacrum" % "0.15.0"
 libraryDependencies += "org.scala-lang.modules" %% "scala-parser-combinators" % "1.0.6"
 libraryDependencies += "org.scalaz" %% "scalaz-core" % "7.2.27"
-libraryDependencies += "org.antlr" % "antlr4-runtime" % "4.12.0"
+libraryDependencies += "org.antlr" % "antlr4-runtime" % "4.13.0"
 libraryDependencies += "org.atnos" %% "eff" % "5.7.0"
 
 Compile / unmanagedJars += {

src/main/scala/wasm/AST.scala

@@ -145,7 +145,7 @@ case class Copysign(ty: NumType) extends BinOp
 abstract class TestOp 
 case class Eqz(ty: NumType) extends TestOp
 
-abstract class RelOp 
+abstract class RelOp
 case class Eq(ty: NumType)  extends RelOp
 case class Ne(ty: NumType)  extends RelOp
 case class LtS(ty: NumType) extends RelOp

src/main/scala/wasm/ConcolicMemory.scala

@@ -1,9 +1,16 @@
 package gensym.wasm.concolicmemory
 
 import gensym.wasm.symbolic._
+import gensym.wasm.ast._
 
 import scala.collection.mutable.HashMap
 
+object ConcolicMemory {
+  def apply(): ConcolicMemory = {
+    ConcolicMemory(Map(), None, HashMap())
+  }
+}
+
 case class ConcolicMemory(map: Map[Int, (Byte, SymVal)], parent: Option[ConcolicMemory], chunktable: HashMap[Int, Int]) {
   def storeByte(addr: Int, value: (Byte, SymVal)): ConcolicMemory = {
     ConcolicMemory(map + (addr -> value), parent, chunktable)
@@ -17,7 +24,7 @@ case class ConcolicMemory(map: Map[Int, (Byte, SymVal)], parent: Option[Concolic
 
     aux(this) match {
       case Some(value) => value
-      case None => ??? // wasp returns (0, 0)
+      case None => (0, Concrete(I32V(0))) // wasp returns (0, 0)
     }
   }
 
@@ -42,4 +49,28 @@ case class ConcolicMemory(map: Map[Int, (Byte, SymVal)], parent: Option[Concolic
     }
     case None => false
   }
+
+  def storeInt(addr: Int, value: (Int, SymVal)): Unit = {
+    val (int, symval) = value
+    val bytes = intToBytes(int)
+    val newMem = storeBytes(addr, bytes, symval)
+  }
+
+  def loadInt(addr: Int): (Int, SymVal) = {
+    val (bytes, symval) = loadBytes(addr, 4)
+    val int = bytesToInt(bytes)
+    (int, symval)
+  }
+
+  def bytesToInt(bytes: List[Byte]): Int = {
+    bytes.zipWithIndex.foldLeft(0) { case (acc, (byte, i)) =>
+      acc | (byte.toInt << (i * 8))
+    }
+  }
+
+  def intToBytes(int: Int): List[Byte] = {
+    for (i <- (0 until 4).toList) yield {
+      ((int >> (i * 8)) & 0xff).toByte
+    }
+  }
 }

src/main/scala/wasm/ConcolicMiniWasm.scala

@@ -2,7 +2,9 @@ package gensym.wasm.concolicminiwasm
 
 import gensym.wasm.ast._
 import gensym.wasm.source._
-import gensym.wasm.memory._
+// import gensym.wasm.memory._
+import gensym.wasm.concolicmemory._
+import gensym.wasm.symbolic._
 import gensym.wasm.parser._
 
 import scala.util.Random
@@ -12,7 +14,7 @@ import scala.collection.mutable.{ArrayBuffer, HashMap}
 case class ModuleInstance(
   types: List[FuncType],
   funcs: List[FuncBodyDef],
-  memory: List[RTMemory] = List(RTMemory()),
+  memory: List[ConcolicMemory] = List(ConcolicMemory()),
   globals: ArrayBuffer[(RTGlobal, SymVal)] = ArrayBuffer[(RTGlobal, SymVal)]()
 )
 
@@ -43,7 +45,15 @@ object Primitives {
       case (I64V(v1), I64V(v2)) => I64V(v1 >>> v2)
       case _ => throw new Exception("Invalid types")
     }
-    case _ => ???
+    case And(_) => (lhs, rhs) match {
+      case (I32V(v1), I32V(v2)) => I32V(v1 & v2)
+      case (I64V(v1), I64V(v2)) => I64V(v1 & v2)
+      case _ => throw new Exception("Invalid types")
+    }
+    case _ => {
+      println(s"unimplemented binop: $op")
+      ???
+    }
   }
   def evalUnaryOp(op: UnaryOp, value: Value) = op match {
     case Clz(_) => value match {
@@ -138,9 +148,17 @@ object Primitives {
     }
   }
 
+  def evalSymRelOp(op: RelOp, lhs: SymVal, rhs: SymVal): SymVal = (lhs, rhs) match {
+    case (Concrete(lhs), Concrete(rhs)) => Concrete(evalRelOp(op, lhs, rhs))
+    case _ => SymIte(RelCond(op, lhs, rhs), Concrete(I32V(1)), Concrete(I32V(0)))
+  }
+
   def memOutOfBound(frame: Frame, memoryIndex: Int, offset: Int, size: Int) = {
-    val memory = frame.module.memory(memoryIndex)
-    offset + size > memory.size
+    // TODO
+    false
+    // val memory = frame.module.memory(memoryIndex)
+    // offset + size > memory.size
+    // offset + size > memory.size
   }
 
   def randomOfTy(ty: ValueType): Value = ty match {
@@ -153,17 +171,6 @@ object Primitives {
 
 case class Frame(module: ModuleInstance, locals: ArrayBuffer[Value], symLocals: ArrayBuffer[SymVal])
 
-abstract class SymVal
-case class SymV(name: String) extends SymVal
-case class SymBinary(op: BinOp, lhs: SymVal, rhs: SymVal) extends SymVal
-case class SymUnary(op: UnaryOp, v: SymVal) extends SymVal
-case class SymIte(cond: Cond, thn: SymVal, els: SymVal) extends SymVal
-case class Concrete(v: Value) extends SymVal
-
-abstract class Cond
-case class CondEqz(v: SymVal) extends Cond
-case class Not(cond: Cond) extends Cond
-
 object Evaluator {
   import Primitives._
 
@@ -176,9 +183,13 @@ object Evaluator {
            frame: Frame, ret: RetCont, trail: List[Cont])(implicit pathConds: List[Cond]): Unit = {
     if (insts.isEmpty) return ret(concStack, symStack, pathConds)
 
+    println(s"pathConds: $pathConds")
+
     val inst = insts.head
     val rest = insts.tail
 
+    println(s"inst: $inst, concStack: $concStack")
+
     inst match {
       case PushSym(name, v) =>
         eval(rest, v :: concStack, SymV(name) :: symStack, frame, ret, trail)
@@ -220,19 +231,24 @@ object Evaluator {
         val oldConc = frame.module.globals(i)._1
         frame.module.globals(i) = (oldConc.copy(value = value), symVal)
         eval(rest, newStack, newSymStack, frame, ret, trail)
+      // I think these are essentially dummies in WASP
+      // to more accurately replace them, we should probably
+      // add a dummy memory size field to ConcolicMemory
       case MemorySize =>
-        val cv = I32V(frame.module.memory.head.size)
-        val sv = Concrete(cv)
-        eval(rest, cv::concStack, sv::symStack, frame, ret, trail)
+        eval(rest, I32V(100) :: concStack, Concrete(I32V(100)) :: symStack, frame, ret, trail)
+        // val cv = I32V(frame.module.memory.head.size)
+        // val sv = Concrete(cv)
+        // eval(rest, cv::concStack, sv::symStack, frame, ret, trail)
       case MemoryGrow =>
-        val I32V(delta)::newStack = concStack
-        val mem = frame.module.memory.head
-        val oldSize = mem.size
-        val cv = mem.grow(delta) match {
-          case Some(e) => I32V(-1)
-          case _ => I32V(-1)
-        }
-        eval(rest, cv :: newStack, Concrete(cv) :: symStack.tail, frame, ret, trail)
+        eval(rest, I32V(100) :: concStack, Concrete(I32V(100)) :: symStack, frame, ret, trail)
+        // val I32V(delta)::newStack = concStack
+        // val mem = frame.module.memory.head
+        // val oldSize = mem.size
+        // val cv = mem.grow(delta) match {
+        //   case Some(e) => I32V(-1)
+        //   case _ => I32V(-1)
+        // }
+        // eval(rest, cv :: newStack, Concrete(cv) :: symStack.tail, frame, ret, trail)
       // WASP doesn't implement these
       case MemoryFill => ???
         // val I32V(value) :: I32V(offset) :: I32V(size) :: newStack = concStack
@@ -257,23 +273,28 @@ object Evaluator {
         val v :: newStack = concStack
         val sv :: newSymStack = symStack
         eval(rest, evalUnaryOp(op, v)::newStack, SymUnary(op, sv)::newSymStack, frame, ret, trail)
-      case Compare(op) => ???
-        // val v2 :: v1 :: newStack = concStack
-        // eval(rest, evalRelOp(op, v1, v2)::newStack, frame, ret, trail)
+      case Compare(op) =>
+        val v2 :: v1 :: newStack = concStack
+        val sv2 :: sv1 :: newSymStack = symStack
+        eval(rest, evalRelOp(op, v1, v2)::newStack, evalSymRelOp(op, sv1, sv2)::newSymStack, frame, ret, trail)
       case Test(op) =>
         val v :: newStack = concStack
         val sv :: newSymStack = symStack
         val test = evalTestOp(op, v)
         val symTest = evalSymTestOp(op, sv)
         eval(rest, test::newStack, symTest::newSymStack, frame, ret, trail)
-      case Store(StoreOp(align, offset, ty, None)) => ???
-        // val I32V(v)::I32V(addr)::newStack = concStack
-        // frame.module.memory(0).storeInt(addr + offset, v)
-        // eval(rest, newStack, frame, ret, trail)
-      case Load(LoadOp(align, offset, ty, None, None)) => ???
-        // val I32V(addr)::newStack = concStack
-        // val value = frame.module.memory(0).loadInt(addr + offset)
-        // eval(rest, I32V(value)::newStack, frame, ret, trail)
+      case Store(StoreOp(align, offset, ty, None)) =>
+        val I32V(v)::I32V(addr)::newStack = concStack
+        val sv :: sa :: newSymStack = symStack
+        // need to concretize sa and then checkAccess
+        frame.module.memory(0).storeInt(addr + offset, (v, sv))
+        eval(rest, newStack, symStack.drop(2), frame, ret, trail)
+      case Load(LoadOp(align, offset, ty, None, None)) =>
+        val I32V(addr)::newStack = concStack
+        val sa :: newSymStack = symStack
+        // need to concretize sv and then checkAccess
+        val (value, sv) = frame.module.memory(0).loadInt(addr + offset)
+        eval(rest, I32V(value)::newStack, sv::newSymStack, frame, ret, trail)
       case Nop =>
         eval(rest, concStack, symStack, frame, ret, trail)
       case Unreachable => throw new RuntimeException("Unreachable")
@@ -311,6 +332,7 @@ object Evaluator {
       case Return => ret(concStack, symStack, pathConds)
       case Call(f) =>
         val FuncBodyDef(ty, _, locals, body) = frame.module.funcs(f)
+        println(s"call $f: locals: ${locals}")
         val args = concStack.take(ty.inps.size).reverse
         val symArgs = symStack.take(ty.inps.size).reverse
         val newStack = concStack.drop(ty.inps.size)
@@ -338,23 +360,39 @@ object Evaluator {
     (cv, sv)
   }
 
-  def execWholeProgram(module: Module, mainFun: String) = {
+  private def printRetCont(concStack: List[Value], symStack: List[SymVal], pathConds: List[Cond]) = {
+    println(s"retCont: $concStack")
+    println(s"symStack: $symStack")
+    println(s"pathCnds: $pathConds")
+  }
+
+  def execWholeProgram(
+    module: Module, mainFun: String, symEnv: HashMap[Int, Value] = HashMap(), k: RetCont = printRetCont
+  ) = {
     import collection.mutable.ArrayBuffer
-    val module = Parser.parseFile("./benchmarks/wasm/test.wat")
+    // val module = Parser.parseFile("./benchmarks/wasm/test.wat")
     // println(module)
 
-    val instrs = module.definitions.find({
-      case FuncDef(Some(mainFun), FuncBodyDef(_, _, _, _)) => true
-      case _ => false
-    }).map({
-      case FuncDef(_, FuncBodyDef(_, _, _, body)) => body
-    }).get
-    .toList
+    // val instrs = module.definitions.find({
+    //   case FuncDef(Some(fname), FuncBodyDef(_, _, _, _)) if fname == mainFun => true
+    //   case _ => false
+    // }).map({
+    //   case FuncDef(_, FuncBodyDef(_, _, _, body)) => body
+    // }).get
+    // .toList
+
+    this.symEnv.clear()
+    this.symEnv ++= symEnv
 
     val types = List()
-    val funcs = module.definitions.collect({
-      case FuncDef(_, fndef@FuncBodyDef(_, _, _, _)) => fndef
-    }).toList
+    val funcDefs = module.definitions.collect({ case f@FuncDef(_, _) => f })
+    val funcs = funcDefs.map({ case FuncDef(_, body@FuncBodyDef(_, _, _, _)) => body })
+
+    val funcId = funcDefs.indexWhere({
+      case FuncDef(name, _) => name == Some(mainFun)
+    })
+
+    val instrs = List(Call(funcId))
 
     val moduleInst = ModuleInstance(types, funcs)
 
@@ -374,15 +412,11 @@ object Evaluator {
     }
 
     Evaluator.eval(
-      Const(I32V(2)) :: PushSym("x", I32V(8)) :: instrs, 
+      instrs, 
       List(), 
       List(), 
       Frame(moduleInst, ArrayBuffer(I32V(0)), ArrayBuffer(Concrete(I32V(0)))),
-      (newStack, newSymStack, pathCnds) => {
-        println(s"retCont: $newStack")
-        println(s"symStack: $newSymStack")
-        println(s"pathCnds: $pathCnds")
-      },
+      k,
       List((newStack, _, _) => println(s"trail: $newStack"))
     )(List())
   }

src/main/scala/wasm/Symbolic.scala

@@ -11,6 +11,7 @@ case class Concrete(v: Value) extends SymVal
 abstract class Cond extends SymVal
 case class CondEqz(v: SymVal) extends Cond
 case class Not(cond: Cond) extends Cond
+case class RelCond(op: RelOp, lhs: SymVal, rhs: SymVal) extends Cond
 
 case class InitMem(min: Int, max: Option[Int]) extends SymVal
 case class MemConcat(lhs: SymVal, rhs: SymVal) extends SymVal

src/main/scala/wasm/tests/TestConcolicWasm.scala

@@ -15,10 +15,12 @@ object ConcolicWasmTest {
   }
 
   def main(args: Array[String]) = {
-    fileTestConcolicEval("./benchmarks/wasm/test.wat", "$real_main")
-    fileTestConcolicEval(
-      "./benchmarks/wasm/Collections-C/_build/for-wasp/normal/array/array_test_add.wat",
-      "$__original_main"
-    )
+    fileTestConcolicEval("./benchmarks/wasm/test.wat", "$main")
+    // fileTestConcolicEval("./benchmarks/wasm/unit/loop.wat", "$main")
+    fileTestConcolicEval("./benchmarks/wasm/unit/br.wat", "$main")
+    // fileTestConcolicEval(
+    //   "./benchmarks/wasm/Collections-C/_build/for-wasp/normal/array/array_test_add.wat",
+    //   "$__original_main"
+    // )
   }
 }