@@ -9,9 +9,10 @@ import scala.collection.immutable.Queue
99import scala .collection .mutable .{HashMap , HashSet }
1010
1111import z3 .scala ._
12+ import scala .tools .nsc .doc .model .Val
1213
1314object ConcolicDriver {
14- def condsToEnv (conds : List [Cond ])(implicit z3Ctx : Z3Context ): HashMap [Int , Value ] = {
15+ def condsToEnv (conds : List [Cond ])(implicit z3Ctx : Z3Context ): Option [ HashMap [Int , Value ] ] = {
1516 val intSort = z3Ctx.mkIntSort()
1617 val boolSort = z3Ctx.mkBoolSort()
1718
@@ -24,16 +25,57 @@ object ConcolicDriver {
2425 case Add (_) => z3Ctx.mkAdd(symVToZ3(lhs), symVToZ3(rhs)) // does numtype matter?
2526 case Sub (_) => z3Ctx.mkSub(symVToZ3(lhs), symVToZ3(rhs))
2627 case Mul (_) => z3Ctx.mkMul(symVToZ3(lhs), symVToZ3(rhs))
27- case _ => ???
28+ case Or (_) =>
29+ var result = z3Ctx.mkBVOr(
30+ z3Ctx.mkInt2BV(32 , symVToZ3(lhs)),
31+ z3Ctx.mkInt2BV(32 , symVToZ3(rhs))
32+ )
33+ z3Ctx.mkBV2Int(result, false )
34+ case _ => throw new NotImplementedError (s " Unsupported binary operation: $op" )
2835 }
2936 case SymUnary (op, v) =>
3037 op match {
3138 case _ => ???
3239 }
3340 case SymIte (cond, thenV, elseV) => z3Ctx.mkITE(condToZ3(cond), symVToZ3(thenV), symVToZ3(elseV))
34- case Concrete (v) => ???
35- case _ => ???
41+ case Concrete (v) =>
42+ v match {
43+ // todo: replace with bitvector
44+ case I32V (i) => z3Ctx.mkInt(i, intSort)
45+ case I64V (i) => z3Ctx.mkNumeral(i.toString(), intSort)
46+ // TODO: Float
47+ case _ => ???
48+ }
49+ case RelCond (op, lhs, rhs) =>
50+ val res = op match {
51+ case GeS (_) => z3Ctx.mkGE(symVToZ3(lhs), symVToZ3(rhs))
52+ case GtS (_) => z3Ctx.mkGT(symVToZ3(lhs), symVToZ3(rhs))
53+ case LtS (_) => z3Ctx.mkLT(symVToZ3(lhs), symVToZ3(rhs))
54+ case LeS (_) => z3Ctx.mkLE(symVToZ3(lhs), symVToZ3(rhs))
55+ case GtU (_) => z3Ctx.mkGT(symVToZ3(lhs), symVToZ3(rhs))
56+ case GeU (_) => z3Ctx.mkGE(symVToZ3(lhs), symVToZ3(rhs))
57+ case LtU (_) => z3Ctx.mkLT(symVToZ3(lhs), symVToZ3(rhs))
58+ case LeU (_) => z3Ctx.mkLE(symVToZ3(lhs), symVToZ3(rhs))
59+ case Eq (_) => z3Ctx.mkEq(symVToZ3(lhs), symVToZ3(rhs))
60+ case Ne (_) => z3Ctx.mkNot(z3Ctx.mkEq(symVToZ3(lhs), symVToZ3(rhs)))
61+ case Ge (_) => z3Ctx.mkGE(symVToZ3(lhs), symVToZ3(rhs))
62+ case Gt (_) => z3Ctx.mkGT(symVToZ3(lhs), symVToZ3(rhs))
63+ case Le (_) => z3Ctx.mkLE(symVToZ3(lhs), symVToZ3(rhs))
64+ case Lt (_) => z3Ctx.mkLT(symVToZ3(lhs), symVToZ3(rhs))
65+ }
66+ // convert resutl to int
67+ z3Ctx.mkITE(res, z3Ctx.mkInt(1 , intSort), z3Ctx.mkInt(0 , intSort))
68+ case _ => throw new NotImplementedError (s " Unsupported SymVal: $symV" )
69+ }
70+
71+ def getIndexOfSym (sym : String ): Int = {
72+ val pattern = " .*_(\\ d+)$"
73+ sym match {
74+ case pattern(index) => index.toInt
75+ case _ => throw new IllegalArgumentException (s " Invalid symbol format: $sym" )
76+ }
3677 }
78+
3779 def condToZ3 (cond : Cond ): Z3AST = cond match {
3880 case CondEqz (v) => z3Ctx.mkEq(symVToZ3(v), z3Ctx.mkInt(0 , intSort))
3981 case Not (cond) => z3Ctx.mkNot(condToZ3(cond))
@@ -49,74 +91,93 @@ object ConcolicDriver {
4991 }
5092
5193 // solve for all vars
94+ println(s " solving constraints: ${solver.toString()}" )
5295 solver.check() match {
5396 case Some (true ) => {
5497 val model = solver.getModel()
5598 val vars = model.getConsts
56- val env = HashMap ()
99+ val env = HashMap [ Int , Value ] ()
57100 for (v <- vars) {
58101 val name = v.getName
59102 val ast = z3Ctx.mkConst(name, intSort)
60103 val value = model.eval(ast)
104+ println(s " name: $name" )
105+ println(s " value: $value" )
106+ // TODO: support other types of symbolic values(currently only i32)
61107 val intValue = if (value.isDefined && value.get.getSort.isIntSort) {
62- I32V (value.toString.toInt)
108+ val negPattern = """ \(\-\s*(\d+)\)"""
109+ val plainPattern = """ (-?\d+)"""
110+ val num = value.get.toString match {
111+ case negPattern(digits) => - digits.toInt
112+ case plainPattern(number) => number.toInt
113+ case _ => throw new IllegalArgumentException (" Invalid format"
114+ }
115+ I32V (num)
63116 } else {
64117 ???
65118 }
66- // env += (name.toString -> intValue)
67- ???
119+ env += (getIndexOfSym(name.toString) -> intValue)
68120 }
69- ???
70- // env
121+ println( s " solved env: $env " )
122+ Some ( env)
71123 }
72- case _ => ???
124+ case _ => None
73125 }
74126 }
75127
76128 def negateCond (conds : List [Cond ], i : Int ): List [Cond ] = {
77- ???
129+ conds(i).negated :: conds.drop(i + 1 )
78130 }
79131
80132 def checkPCToFile (pc : List [Cond ]): Unit = {
133+ // TODO: what this function for?
81134 ???
82135 }
83136
84137 def exec (module : Module , mainFun : String , startEnv : HashMap [Int , Value ])(implicit z3Ctx : Z3Context ) = {
85138 val worklist = Queue (startEnv)
86- // val visited = ??? // how to avoid re-execution
87-
139+ val unreachables = HashSet [ExploreTree ]()
140+ val visited = HashSet [ExploreTree ]()
141+ // the root node of exploration tree
142+ val root = new ExploreTree ()
88143 def loop (worklist : Queue [HashMap [Int , Value ]]): Unit = worklist match {
89144 case Queue () => ()
90145 case env +: rest => {
91146 val moduleInst = ModuleInstance (module)
92147 Evaluator (moduleInst).execWholeProgram(
93148 Some (mainFun),
94149 env,
95- (_endStack, _endSymStack, pathConds) => {
96- println(s " env: $env" )
97- val newEnv = condsToEnv(pathConds)
98- val newWork = for (i <- 0 until pathConds.length) yield {
99- val newConds = negateCond(pathConds, i)
100- checkPCToFile(newConds)
101- condsToEnv(newConds)
150+ root,
151+ (_endStack, _endSymStack, tree) => {
152+ tree.fillWithFinished()
153+ val unexploredTrees = root.unexploredTrees()
154+ // if a node is already visited or marked as unreachable, don't try to explore it
155+ val addedNewWork = unexploredTrees.filterNot(unreachables.contains)
156+ .filterNot(visited.contains)
157+ .flatMap { tree =>
158+ val conds = tree.collectConds()
159+ val newEnv = condsToEnv(conds)
160+ // if the path conditions to reach this node are unsatisfiable, mark it as unreachable.
161+ if (newEnv.isEmpty) unreachables.add(tree)
162+ newEnv
163+ }
164+ for (tree <- unexploredTrees) {
165+ visited.add(tree)
102166 }
103- loop(rest ++ newWork )
167+ loop(rest ++ addedNewWork )
104168 }
105169 )
106170 }
107171 }
108172
109173 loop(worklist)
174+ println(s " unreachable trees number: ${unreachables.size}" )
175+ println(s " number of normal explored paths: ${root.finishedTrees().size}" )
176+ val failedTrees = root.failedTrees()
177+ println(s " number of failed explored paths: ${failedTrees.size}" )
178+ for (tree <- failedTrees) {
179+ println(s " find a failed endpoint: ${tree}" )
180+ }
181+ println(s " exploration tree: ${root.toString}" )
110182 }
111183}
112-
113- object DriverSimpleTest {
114- def fileTestDriver (file : String , mainFun : String , startEnv : HashMap [Int , Value ]) = {
115- import gensym .wasm .concolicminiwasm ._
116- import collection .mutable .ArrayBuffer
117- val module = Parser .parseFile(file)
118- ConcolicDriver .exec(module, mainFun, startEnv)(new Z3Context ())
119- }
120-
121- def main (args : Array [String ]) = {}
122- }
0 commit comments