From ff59cff346a737d7958d831e26d01e59d1e5f7e3 Mon Sep 17 00:00:00 2001 From: Mikail Khan Date: Wed, 29 Nov 2023 03:48:17 -0500 Subject: [PATCH] filled some concolicminiwasm gaps --- benchmarks/wasm/build_wat_c.sh | 2 +- benchmarks/wasm/test.wat | 2 +- benchmarks/wasm/test_loop.c | 15 ++ build.sbt | 2 +- src/main/scala/wasm/AST.scala | 2 +- src/main/scala/wasm/ConcolicMemory.scala | 33 +++- src/main/scala/wasm/ConcolicMiniWasm.scala | 146 +++++++++++------- src/main/scala/wasm/Symbolic.scala | 1 + .../scala/wasm/tests/TestConcolicWasm.scala | 12 +- 9 files changed, 149 insertions(+), 66 deletions(-) create mode 100644 benchmarks/wasm/test_loop.c diff --git a/benchmarks/wasm/build_wat_c.sh b/benchmarks/wasm/build_wat_c.sh index f50d5446..e56d7841 100755 --- a/benchmarks/wasm/build_wat_c.sh +++ b/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 diff --git a/benchmarks/wasm/test.wat b/benchmarks/wasm/test.wat index 3b7dc7e6..d34feec4 100644 --- a/benchmarks/wasm/test.wat +++ b/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")) \ No newline at end of file + (data (;0;) (i32.const 1024) "a\00b\00")) diff --git a/benchmarks/wasm/test_loop.c b/benchmarks/wasm/test_loop.c new file mode 100644 index 00000000..f236f0af --- /dev/null +++ b/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; +} diff --git a/build.sbt b/build.sbt index c1620c25..1609624a 100644 --- a/build.sbt +++ b/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 += { diff --git a/src/main/scala/wasm/AST.scala b/src/main/scala/wasm/AST.scala index b7f058cc..ac6ee72c 100644 --- a/src/main/scala/wasm/AST.scala +++ b/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 diff --git a/src/main/scala/wasm/ConcolicMemory.scala b/src/main/scala/wasm/ConcolicMemory.scala index 16e2b6bc..f6e29c4c 100644 --- a/src/main/scala/wasm/ConcolicMemory.scala +++ b/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 + } + } } diff --git a/src/main/scala/wasm/ConcolicMiniWasm.scala b/src/main/scala/wasm/ConcolicMiniWasm.scala index 26d32383..4482d414 100644 --- a/src/main/scala/wasm/ConcolicMiniWasm.scala +++ b/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()) } diff --git a/src/main/scala/wasm/Symbolic.scala b/src/main/scala/wasm/Symbolic.scala index 7c1c5cb6..00bfd707 100644 --- a/src/main/scala/wasm/Symbolic.scala +++ b/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 diff --git a/src/main/scala/wasm/tests/TestConcolicWasm.scala b/src/main/scala/wasm/tests/TestConcolicWasm.scala index b81c3ef0..4fe6d376 100644 --- a/src/main/scala/wasm/tests/TestConcolicWasm.scala +++ b/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" + // ) } }