Skip to content

Commit

Permalink
fix interpreter
Browse files Browse the repository at this point in the history
  • Loading branch information
l-kent committed Nov 16, 2023
1 parent 973b39e commit 92c800d
Show file tree
Hide file tree
Showing 2 changed files with 91 additions and 48 deletions.
137 changes: 91 additions & 46 deletions src/main/scala/ir/Interpreter.scala
View file
Original file line number Diff line number Diff line change
@@ -1,5 +1,4 @@
//package ir
/*
package ir
import analysis.BitVectorEval.*
import util.Logger

Expand All @@ -15,7 +14,7 @@ class Interpreter() {
private var nextBlock: Option[Block] = None
private val returnBlock: mutable.Stack[Block] = mutable.Stack()

def eval(exp: Expr, env: mutable.Map[Variable, BitVecLiteral]): Literal = {
def eval(exp: Expr, env: mutable.Map[Variable, BitVecLiteral]): BitVecLiteral = {
exp match {
case id: Variable =>
env.get(id) match {
Expand Down Expand Up @@ -47,16 +46,11 @@ class Interpreter() {

case r: Repeat =>
Logger.debug(s"\t$r")
val arg = eval(r.body, env)
var result = arg
for (_ <- 1 to r.repeats) {
result = smt_concat(result, arg)
}
result
??? // TODO

case bin: BinaryExpr =>
val left: BitVecLiteral = eval(bin.arg1, env).asInstanceOf[BitVecLiteral]
val right: BitVecLiteral = eval(bin.arg2, env).asInstanceOf[BitVecLiteral]
val left = eval(bin.arg1, env)
val right = eval(bin.arg2, env)
Logger.debug(
s"\tBinaryExpr(0x${left.value.toString(16)}[u${left.size}] ${bin.op} 0x${right.value.toString(16)}[u${right.size}])"
)
Expand All @@ -69,27 +63,18 @@ class Interpreter() {
case BVUREM => smt_bvurem(left, right)
case BVSHL => smt_bvshl(left, right)
case BVLSHR => smt_bvlshr(left, right)
case BVULT => smt_bvult(left, right)
case BVNAND => ???
case BVNOR => ???
case BVXOR => ???
case BVXNOR => ???
case BVNAND => smt_bvnand(left, right)
case BVNOR => smt_bvnor(left, right)
case BVXOR => smt_bvxor(left, right)
case BVXNOR => smt_bvxnor(left, right)
case BVCOMP => smt_bvcomp(left, right)
case BVSUB => smt_bvsub(left, right)
case BVSDIV => smt_bvsdiv(left, right)
case BVSREM => smt_bvsrem(left, right)
case BVSMOD => ???
case BVSMOD => smt_bvsmod(left, right)
case BVASHR => smt_bvashr(left, right)
case BVULE => smt_bvule(left, right)
case BVUGT => ???
case BVUGE => ???
case BVSLT => smt_bvslt(left, right)
case BVSLE => smt_bvsle(left, right)
case BVSGT => ???
case BVSGE => ???
case BVEQ => smt_bveq(left, right)
case BVNEQ => smt_bvneq(left, right)
case BVCONCAT => smt_concat(left, right)
case _ => ???
}

case un: UnaryExpr =>
Expand All @@ -98,8 +83,6 @@ class Interpreter() {
un.op match {
case BVNEG => smt_bvneg(arg)
case BVNOT => smt_bvnot(arg)
case IntNEG => ???
case BoolNOT => ???
}

case m: Memory =>
Expand All @@ -108,18 +91,89 @@ class Interpreter() {

case ml: MemoryLoad =>
Logger.debug(s"\t$ml")
val index: Int = eval(ml.index, env).asInstanceOf[BitVecLiteral].value.toInt
val index: Int = eval(ml.index, env).value.toInt
getMemory(index, ml.size, ml.endian, mems)

case ms: MemoryStore =>
val index: Int = eval(ms.index, env).asInstanceOf[BitVecLiteral].value.toInt
val value: BitVecLiteral = eval(ms.value, env).asInstanceOf[BitVecLiteral]
val index: Int = eval(ms.index, env).value.toInt
val value: BitVecLiteral = eval(ms.value, env)
Logger.debug(s"\tMemoryStore(mem:${ms.mem}, index:0x${index.toHexString}, value:0x${value.value
.toString(16)}[u${value.size}], size:${ms.size})")
setMemory(index, ms.size, ms.endian, value, mems)
}
}

def evalBool(exp: Expr, env: mutable.Map[Variable, BitVecLiteral]): BoolLit = {
exp match {
case n: BoolLit => n
case bin: BinaryExpr =>
bin.op match {
case b: BoolBinOp =>
val arg1 = evalBool(bin.arg1, env)
val arg2 = evalBool(bin.arg2, env)
b match {
case BoolEQ =>
if (arg1 == arg2) {
TrueLiteral
} else {
FalseLiteral
}
case BoolNEQ =>
if (arg1 != arg2) {
TrueLiteral
} else {
FalseLiteral
}
case BoolAND =>
(arg1, arg2) match {
case (TrueLiteral, TrueLiteral) => TrueLiteral
case _ => FalseLiteral
}
case BoolOR =>
(arg1, arg2) match {
case (FalseLiteral, FalseLiteral) => FalseLiteral
case _ => TrueLiteral
}
case BoolIMPLIES =>
(arg1, arg2) match {
case (TrueLiteral, FalseLiteral) => FalseLiteral
case _ => TrueLiteral
}
case BoolEQUIV =>
if (arg1 == arg2) {
TrueLiteral
} else {
FalseLiteral
}
}
case b: BVBinOp =>
val left = eval(bin.arg1, env)
val right = eval(bin.arg2, env)
b match {
case BVULT => smt_bvult(left, right)
case BVULE => smt_bvule(left, right)
case BVUGT => smt_bvugt(left, right)
case BVUGE => smt_bvuge(left, right)
case BVSLT => smt_bvslt(left, right)
case BVSLE => smt_bvsle(left, right)
case BVSGT => smt_bvsgt(left, right)
case BVSGE => smt_bvsge(left, right)
case BVEQ => smt_bveq(left, right)
case BVNEQ => smt_bvneq(left, right)
case _ => ???
}
case _ => ???
}

case un: UnaryExpr =>
un.op match {
case BoolNOT => if evalBool(un.arg, env) == TrueLiteral then FalseLiteral else TrueLiteral
case _ => ???
}

}
}

def getMemory(index: Int, size: Int, endian: Endian, env: mutable.Map[Int, BitVecLiteral]): BitVecLiteral = {
val end = index + size / 8 - 1
val memoryChunks = (index to end).map(i => env.getOrElse(i, BitVecLiteral(0, 8)))
Expand Down Expand Up @@ -179,7 +233,7 @@ class Interpreter() {
}

private def interpretBlock(b: Block): Unit = {
Logger.debug(s"Block:${nextBlock.get.label} ${nextBlock.get.address}")
Logger.debug(s"Block:${b.label} ${b.address}")
// Block.Statement
for ((statement, index) <- b.statements.zipWithIndex) {
Logger.debug(s"statement[$index]:")
Expand All @@ -195,7 +249,7 @@ class Interpreter() {
for (g <- gt.targets) {
val condition: Option[Expr] = g.statements.headOption.collect { case a: Assume => a.body }
condition match {
case Some(e) => eval(e, regs) match {
case Some(e) => evalBool(e, regs) match {
case TrueLiteral =>
nextBlock = Some(g)
break
Expand Down Expand Up @@ -235,21 +289,13 @@ class Interpreter() {
case assign: LocalAssign =>
Logger.debug(s"LocalAssign ${assign.lhs} = ${assign.rhs}")
val evalRight = eval(assign.rhs, regs)
evalRight match {
case BitVecLiteral(value, size) =>
Logger.debug(s"LocalAssign ${assign.lhs} := 0x${value.toString(16)}[u$size]\n")
regs += (assign.lhs -> BitVecLiteral(value, size))
case _ => throw new Exception("cannot register non-bitvectors")
}
Logger.debug(s"LocalAssign ${assign.lhs} := 0x${evalRight.value.toString(16)}[u${evalRight.size}]\n")
regs += (assign.lhs -> evalRight)

case assign: MemoryAssign =>
Logger.debug(s"MemoryAssign ${assign.lhs} = ${assign.rhs}")
val evalRight = eval(assign.rhs, regs)
evalRight match {
case BitVecLiteral(value, size) =>
Logger.debug(s"MemoryAssign ${assign.lhs} := 0x${value.toString(16)}[u$size]\n")
case _ => throw new Exception("cannot register non-bitvectors")
}
Logger.debug(s"MemoryAssign ${assign.lhs} := 0x${evalRight.value.toString(16)}[u$evalRight.size]\n")

case assert: Assert =>
Logger.debug(assert)
Expand Down Expand Up @@ -290,5 +336,4 @@ class Interpreter() {

regs
}
}
*/
}
2 changes: 0 additions & 2 deletions src/test/scala/ir/InterpreterTests.scala
View file
Original file line number Diff line number Diff line change
@@ -1,4 +1,3 @@
/*
package ir

import analysis.BitVectorEval.*
Expand Down Expand Up @@ -192,4 +191,3 @@ class InterpreterTests extends AnyFunSuite with BeforeAndAfter {
testInterpret("no_interference_update_y", expected)
}
}
*/

0 comments on commit 92c800d

Please sign in to comment.