Skip to content

Commit

Permalink
use BAP Tid for state instead of binary address
Browse files Browse the repository at this point in the history
  • Loading branch information
ailrst committed Oct 30, 2023
1 parent a60c354 commit 85de3c7
Show file tree
Hide file tree
Showing 3 changed files with 7 additions and 7 deletions.
4 changes: 2 additions & 2 deletions src/main/scala/ir/Statement.scala
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,7 @@ trait Statement extends Command {
)
}

case class LocalAssign(var lhs: Variable, var rhs: Expr, val address: Option[Int] = None) extends Statement {
case class LocalAssign(var lhs: Variable, var rhs: Expr, val label: Option[String] = None) extends Statement {
//override def locals: Set[Variable] = rhs.locals + lhs
override def modifies: Set[Global] = lhs match {
case r: Register => Set(r)
Expand All @@ -20,7 +20,7 @@ case class LocalAssign(var lhs: Variable, var rhs: Expr, val address: Option[Int
override def acceptVisit(visitor: Visitor): Statement = visitor.visitLocalAssign(this)
}

case class MemoryAssign(var lhs: Memory, var rhs: MemoryStore, val address: Option[Int] = None) extends Statement {
case class MemoryAssign(var lhs: Memory, var rhs: MemoryStore, val label: Option[String] = None) extends Statement {
override def modifies: Set[Global] = Set(lhs)
//override def locals: Set[Variable] = rhs.locals
override def toString: String = s"$lhs := $rhs"
Expand Down
4 changes: 2 additions & 2 deletions src/main/scala/translating/BAPToIR.scala
Original file line number Diff line number Diff line change
Expand Up @@ -60,8 +60,8 @@ class BAPToIR(var program: BAPProgram, mainAddress: Int) {
}

private def translate(s: BAPStatement) = s match {
case b: BAPMemAssign => MemoryAssign(b.lhs.toIR, b.rhs.toIR, b.address)
case b: BAPLocalAssign => LocalAssign(b.lhs.toIR, b.rhs.toIR, b.address)
case b: BAPMemAssign => MemoryAssign(b.lhs.toIR, b.rhs.toIR, Some(b.line))
case b: BAPLocalAssign => LocalAssign(b.lhs.toIR, b.rhs.toIR, Some(b.line))
case _ => throw new Exception("unsupported statement: " + s)
}

Expand Down
6 changes: 3 additions & 3 deletions src/main/scala/translating/IRToBoogie.scala
Original file line number Diff line number Diff line change
Expand Up @@ -319,7 +319,7 @@ class IRToBoogie(var program: Program, var spec: Specification) {

def translateBlock(b: Block): BBlock = {
val cmds = (b.address match {
case Some(addr) => List(getCaptureStateStatement(s"addr:0x${addr.toHexString}"))
case Some(addr) => List(getCaptureStateStatement(s"addr:${b.label}"))
case _ => List.empty
}) ++ (b.statements.flatMap(s => translate(s)) ++ b.jumps.flatMap(j => translate(j)))

Expand Down Expand Up @@ -379,8 +379,8 @@ class IRToBoogie(var program: Program, var spec: Specification) {
val rhsGamma = m.rhs.toGamma
val store = AssignCmd(List(lhs, lhsGamma), List(rhs, rhsGamma))
val stateSplit = s match {
case MemoryAssign (_,_, Some(addr)) => List(getCaptureStateStatement(s"addr:0x${addr.toHexString}"))
case LocalAssign(_,_, Some(addr)) => List(getCaptureStateStatement(s"addr:0x${addr.toHexString}"))
case MemoryAssign (_,_, Some(label)) => List(getCaptureStateStatement(s"${label}"))
case LocalAssign(_,_, Some(label)) => List(getCaptureStateStatement(s"${label}"))
case _ => List.empty
}
if (lhs == stack) {
Expand Down

0 comments on commit 85de3c7

Please sign in to comment.