Skip to content

Commit 70b33e9

Browse files
ahuoguoahuoguo
committed
test branch.c for concolic miniwasm
1 parent 3e5715d commit 70b33e9

File tree

5 files changed

+132
-28
lines changed

5 files changed

+132
-28
lines changed

‎benchmarks/wasm/branch-strip.wat‎

Lines changed: 41 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,41 @@
1+
(module
2+
(type (;0;) (func (param i32 i32) (result i32)))
3+
(func (;0;) (type 0) (param i32 i32) (result i32)
4+
local.get 0
5+
i32.const 0
6+
i32.le_s
7+
local.get 1
8+
i32.const 0
9+
i32.le_s
10+
i32.or
11+
if (result i32) ;; label = @1
12+
i32.const -1
13+
else
14+
local.get 0
15+
local.get 0
16+
i32.mul
17+
local.get 1
18+
local.get 1
19+
i32.mul
20+
i32.add
21+
i32.const 25
22+
i32.eq
23+
if (result i32) ;; label = @2
24+
i32.const 1
25+
else
26+
i32.const 0
27+
end
28+
end
29+
)
30+
(export "f" (func 0))
31+
(func $real_main
32+
;; TODO: is there a better way to put symbolic values on the stack?
33+
i32.const 0
34+
i32.symbolic
35+
i32.const 1
36+
i32.symbolic
37+
call 0
38+
)
39+
40+
(export "real_main" (func 1))
41+
)

‎benchmarks/wasm/branch.wat‎

Lines changed: 29 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,29 @@
1+
(module
2+
(func $f (param $x i32) (param $y i32) (result i32)
3+
;; if (x <= 0 || y <= 0)
4+
(if (result i32)
5+
(i32.or
6+
(i32.le_s (local.get $x) (i32.const 0))
7+
(i32.le_s (local.get $y) (i32.const 0))
8+
)
9+
(then (i32.const -1)) ;; return -1
10+
(else
11+
;; if (x * x + y * y == 25)
12+
(if (result i32)
13+
(i32.eq
14+
(i32.add
15+
(i32.mul (local.get $x) (local.get $x))
16+
(i32.mul (local.get $y) (local.get $y))
17+
)
18+
(i32.const 25)
19+
)
20+
(then (i32.const 1)) ;; return 1
21+
(else (i32.const 0)) ;; return 0
22+
)
23+
)
24+
)
25+
)
26+
27+
;; Optionally export the function
28+
(export "f" (func $f))
29+
)

‎src/main/scala/wasm/ConcolicMiniWasm.scala‎

Lines changed: 28 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -70,6 +70,12 @@ object Primitives {
7070
case (I64V(v1), I64V(v2)) => I64V(v1 & v2)
7171
case _ => throw new Exception("Invalid types")
7272
}
73+
case Or(_) =>
74+
(lhs, rhs) match {
75+
case (I32V(v1), I32V(v2)) => I32V(v1 | v2)
76+
case (I64V(v1), I64V(v2)) => I64V(v1 | v2)
77+
case _ => throw new Exception("Invalid types")
78+
}
7379
case _ => {
7480
println(s"unimplemented binop: $op")
7581
???
@@ -180,13 +186,18 @@ object Primitives {
180186
case Concrete(v) => Concrete(evalTestOp(op, v))
181187
case _ =>
182188
op match {
183-
case Eqz(_) => SymIte(CondEqz(sv), Concrete(I32V(1)), Concrete(I32V(0)))
189+
case Eqz(ty) => RelCond(Eq(ty), sv, Concrete(zero(ty)))
184190
}
185191
}
186192

187193
def evalSymRelOp(op: RelOp, lhs: SymVal, rhs: SymVal): SymVal = (lhs, rhs) match {
188194
case (Concrete(lhs), Concrete(rhs)) => Concrete(evalRelOp(op, lhs, rhs))
189-
case _ => SymIte(RelCond(op, lhs, rhs), Concrete(I32V(1)), Concrete(I32V(0)))
195+
case _ =>
196+
RelCond(
197+
op,
198+
lhs,
199+
rhs
200+
) // TODO: it was SymIte(RelCond(op, lhs, rhs), Concrete(I32V(1)), Concrete(I32V(0))) before, but why??
190201
}
191202

192203
def memOutOfBound(frame: Frame, memoryIndex: Int, offset: Int, size: Int) = {
@@ -365,10 +376,10 @@ case class Evaluator(module: ModuleInstance) {
365376
case If(ty, thn, els) =>
366377
val scnd :: newSymStack = symStack
367378
val I32V(cond) :: newStack = concStack
368-
val inner = if (cond == 0) thn else els
379+
val inner = if (cond != 0) thn else els
369380
val newPathConds = scnd match {
370381
case Concrete(_) => pathConds
371-
case _ => if (cond == 0) CondEqz(scnd) :: pathConds else Not(CondEqz(scnd)) :: pathConds
382+
case _ => if (cond != 0) CondEqz(scnd) :: pathConds else Not(CondEqz(scnd)) :: pathConds
372383
}
373384
val k: Cont = (retStack, retSymStack, newPathConds) =>
374385
eval(rest, retStack ++ newStack, retSymStack ++ newSymStack, frame, ret, trail)(newPathConds)
@@ -380,7 +391,7 @@ case class Evaluator(module: ModuleInstance) {
380391
val I32V(cond) :: newStack = concStack
381392
val newPathConds = scnd match {
382393
case Concrete(_) => pathConds
383-
case _ => if (cond == 0) CondEqz(scnd) :: pathConds else Not(CondEqz(scnd)) :: pathConds
394+
case _ => if (cond != 0) CondEqz(scnd) :: pathConds else Not(CondEqz(scnd)) :: pathConds
384395
}
385396
if (cond == 0) eval(rest, newStack, newSymStack, frame, ret, trail)(newPathConds)
386397
else trail(label)(newStack, newSymStack, newPathConds)
@@ -497,22 +508,19 @@ case class Evaluator(module: ModuleInstance) {
497508
})
498509

499510
print(s"instrs: $instrs")
500-
501511
// val instrs = List(Call(funcId))
502512

503-
// TODO: what are we tryign to do with globals here
504-
// does global values allow general expressions?
505-
// val globals = module.definitions.collect({ case g@Global(_, _) => g })
513+
val globals = module.defs.collect({ case g @ Global(_, _) => g })
506514

507-
// for (global <- globals) {
508-
// global.f match {
509-
// case GlobalValue(ty, e) => {
510-
// val (cv, sv) = evalExpr(e)
511-
// moduleInst.globals.append((RTGlobal(ty, cv), sv))
512-
// }
513-
// case _ => ???
514-
// }
515-
// }
515+
for (global <- globals) {
516+
global.f match {
517+
case GlobalValue(ty, e) => {
518+
val (cv, sv) = evalExpr(e)
519+
module.globals.append((RTGlobal(ty, cv), sv))
520+
}
521+
case _ => ???
522+
}
523+
}
516524

517525
val locals = extractLocals(module, main)
518526

@@ -542,7 +550,7 @@ case class Evaluator(module: ModuleInstance) {
542550
System.err.println(s"Entering function $main")
543551
module.funcs(fid) match {
544552
case FuncDef(_, FuncBodyDef(_, _, locals, _)) => locals
545-
case _ => throw new Exception("Entry function has no concrete body")
553+
case _ => throw new Exception("Entry function has no concrete body")
546554
}
547555
case _ => List()
548556
})
@@ -552,7 +560,7 @@ case class Evaluator(module: ModuleInstance) {
552560
System.err.println(s"Entering unnamed function $id")
553561
module.funcs(id) match {
554562
case FuncDef(_, FuncBodyDef(_, _, locals, body)) => locals
555-
case _ => throw new Exception("Entry function has no concrete body")
563+
case _ => throw new Exception("Entry function has no concrete body")
556564
}
557565
case _ => List()
558566
})

‎src/main/scala/wasm/Symbolic.scala‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -9,6 +9,7 @@ case class SymUnary(op: UnaryOp, v: SymVal) extends SymVal
99
case class SymIte(cond: Cond, thn: SymVal, els: SymVal) extends SymVal
1010
case class Concrete(v: Value) extends SymVal
1111

12+
// The following should be encoded to boolean in SMT
1213
abstract class Cond extends SymVal
1314
case class CondEqz(v: SymVal) extends Cond
1415
case class Not(cond: Cond) extends Cond
@@ -20,6 +21,6 @@ case class MemExtract(mem: SymVal, offset: Int, size: Int) extends SymVal
2021
abstract class SymVal {
2122
def toZ3AST(implicit ctx: Z3Context): Z3AST = this match {
2223
case SymV(name) => ctx.mkConst(ctx.mkStringSymbol(name), ctx.mkIntSort())
23-
case _ => ???
24+
case _ => ???
2425
}
2526
}

‎src/test/scala/genwasym/TestConcolic.scala‎

Lines changed: 32 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -5,20 +5,45 @@ import gensym.wasm.source._
55
import gensym.wasm.parser._
66
import gensym.wasm.memory._
77
import gensym.wasm.symbolic._
8+
import gensym.wasm.concolicminiwasm._
89

910
import org.scalatest.FunSuite
1011
class TestConcolic extends FunSuite {
1112

12-
// TODO: actually test this
13-
def fileTestConcolicEval() = {
14-
import gensym.wasm.concolicminiwasm._
15-
val module = Parser.parseFile("./benchmarks/wasm/pow.wat")
13+
def fileTestConcolicEval(filename: String, mainFnName: Option[String]) = {
14+
val module = Parser.parseFile(filename)
1615
val moduleInst = ModuleInstance(module)
17-
Evaluator(moduleInst).execWholeProgram(Some("real_main"))
16+
Evaluator(moduleInst).execWholeProgram(mainFnName)
1817
}
1918

20-
test("fileTestConcolicEval") {
21-
fileTestConcolicEval()
19+
// TODO: is there a way to test this in a more automatic way?
20+
// we currently eyeball the path conditions
21+
test("pow") {
22+
fileTestConcolicEval("./benchmarks/wasm/pow.wat", Some("real_main"))
23+
}
24+
25+
test("branch") {
26+
fileTestConcolicEval("./benchmarks/wasm/branch-strip.wat", Some("real_main"))
27+
}
28+
29+
}
30+
31+
class TestDriver extends FunSuite {
32+
import gensym.wasm.concolicdriver._
33+
import scala.collection.mutable.{HashMap, HashSet}
34+
import z3.scala._
35+
36+
def fileTestDriver(file: String, mainFun: String, startEnv: HashMap[Int, Value]) = {
37+
import collection.mutable.ArrayBuffer
38+
val module = Parser.parseFile(file)
39+
ConcolicDriver.exec(module, mainFun, startEnv)(new Z3Context())
40+
}
41+
42+
// def main(args: Array[String]) = {}
43+
44+
// TODO: fix this
45+
test("driver") {
46+
fileTestDriver("./benchmarks/wasm/branch-strip.wat", "real_main", new HashMap[Int, Value]())
2247
}
2348

2449
}

0 commit comments

Comments
 (0)