Add extern attribute and captureState attribute to pass binary locations to boogie for better debugging

src/main/scala/bap/BAPStatement.scala

@@ -32,7 +32,7 @@ trait BAPAssign(lhs: BAPVariable, rhs: BAPExpr, line: String, instruction: Strin
 
 /** Memory store
   */
-case class BAPMemAssign(lhs: BAPMemory, rhs: BAPStore, line: String, instruction: String)
+case class BAPMemAssign(lhs: BAPMemory, rhs: BAPStore, line: String, instruction: String, address: Option[Int] = None)
     extends BAPAssign(lhs, rhs, line, instruction)
 
 /*
@@ -47,5 +47,5 @@ case object BAPMemAssign {
 }
  */
 
-case class BAPLocalAssign(lhs: BAPVar, rhs: BAPExpr, line: String, instruction: String)
+case class BAPLocalAssign(lhs: BAPVar, rhs: BAPExpr, line: String, instruction: String, address: Option[Int] = None)
     extends BAPAssign(lhs, rhs, line, instruction)

src/main/scala/boogie/BAttribute.scala

@@ -0,0 +1,16 @@
+package boogie
+
+trait HasAttributes {
+  def attributes: List[BAttribute]
+
+  val attrString: String = if attributes.nonEmpty then {
+    attributes.mkString(" ") + " "
+  } else {
+    ""
+  }
+}
+
+case class BAttribute(name: String, value: Option[String] = None) {
+  private val valueStr = if value.nonEmpty then s" ${value.get}" else ""
+  override def toString: String = s"{:$name$valueStr}"
+}

src/main/scala/boogie/BCmd.scala

@@ -17,23 +17,25 @@ case class BBlock(label: String, body: List[BCmd]) extends BCmdOrBlock {
   override def globals: Set[BVar] = body.flatMap(c => c.globals).toSet
 }
 
-sealed trait BCmd extends BCmdOrBlock {
+sealed trait BCmd() extends BCmdOrBlock with HasAttributes {
+  override def attributes: List[BAttribute] = List()
   def comment: Option[String]
+
   override def toBoogie: List[String] = {
     val commentOut = comment.map(" //" + _).getOrElse("")
     List(toString + commentOut)
   }
 }
 
-case class BAssert(body: BExpr, comment: Option[String] = None) extends BCmd {
-  override def toString: String = s"assert $body;"
+case class BAssert(body: BExpr, comment: Option[String] = None, override val attributes: List[BAttribute] = List.empty) extends BCmd {
+  override def toString: String = s"assert $attrString$body;"
   override def functionOps: Set[FunctionOp] = body.functionOps
   override def locals: Set[BVar] = body.locals
   override def globals: Set[BVar] = body.globals
 }
 
-case class BAssume(body: BExpr, comment: Option[String] = None) extends BCmd {
-  override def toString: String = s"assume $body;"
+case class BAssume(body: BExpr, comment: Option[String] = None, override val attributes: List[BAttribute] = List.empty) extends BCmd {
+  override def toString: String = s"assume $attrString$body;"
   override def functionOps: Set[FunctionOp] = body.functionOps
   override def locals: Set[BVar] = body.locals
   override def globals: Set[BVar] = body.globals
@@ -42,9 +44,9 @@ case class BAssume(body: BExpr, comment: Option[String] = None) extends BCmd {
 case class BProcedureCall(name: String, lhss: Seq[BVar], params: Seq[BExpr], comment: Option[String] = None) extends BCmd {
   override def toString: String = {
     if (lhss.isEmpty) {
-      s"call $name();"
+      s"call $attrString$name();"
     } else {
-      s"call ${lhss.mkString(", ")} := $name(${params.mkString(", ")});"
+      s"call $attrString${lhss.mkString(", ")} := $name(${params.mkString(", ")});"
     }
   }
   override def functionOps: Set[FunctionOp] = params.flatMap(p => p.functionOps).toSet

src/main/scala/boogie/BExpr.scala

@@ -443,7 +443,10 @@ case class MapUpdate(map: BExpr, index: BExpr, value: BExpr) extends BExpr {
 
 sealed trait FunctionOp
 
-case class BVFunctionOp(name: String, bvbuiltin: String, in: List[BVar], out: BVar) extends FunctionOp
+case class BVFunctionOp(name: String, bvbuiltin: String, in: List[BVar], out: BVar) extends FunctionOp {
+  def attribute: BAttribute = BAttribute("bvbuiltin", Some(s"\"$bvbuiltin\""))
+}
+
 case class MemoryLoadOp(addressSize: Int, valueSize: Int, endian: Endian, bits: Int) extends FunctionOp {
   val accesses: Int = bits / valueSize
 

src/main/scala/boogie/BProgram.scala

@@ -4,7 +4,8 @@ case class BProgram(declarations: List[BDeclaration]) {
   override def toString: String = declarations.flatMap(x => x.toBoogie).mkString("\n")
 }
 
-trait BDeclaration {
+trait BDeclaration extends HasAttributes {
+  override def attributes: List[BAttribute] = List()
   def toBoogie: List[String] = List(toString)
 }
 
@@ -19,12 +20,13 @@ case class BProcedure(
     freeEnsures: List[BExpr],
     freeRequires: List[BExpr],
     modifies: Set[BVar],
-    body: List[BCmdOrBlock]
-) extends BDeclaration
+    body: List[BCmdOrBlock],
+    override val attributes: List[BAttribute]
+) extends BDeclaration()
     with Ordered[BProcedure] {
   override def compare(that: BProcedure): Int = name.compare(that.name)
   override def toBoogie: List[String] = {
-    val header = s"procedure $name(${in.map(_.withType).mkString(", ")})"
+    val header = s"procedure $attrString$name(${in.map(_.withType).mkString(", ")})"
     val returns = if (out.nonEmpty) {
       s" returns (${out.map(_.withType).mkString(", ")})"
     } else {
@@ -41,7 +43,7 @@ case class BProcedure(
     val freeRequiresStrs = freeRequires.map(r => s"  free requires $r;")
     val freeEnsuresStrs = freeEnsures.map(e => s"  free ensures $e;")
     val locals = body.flatMap(l => l.locals).distinct.sorted
-    val localDefs = locals.map(l => "  " + BVarDecl(l).toString)
+    val localDefs = locals.map(l => "  " + BVarDecl(l, List.empty).toString)
     val bodyStr = if (body.nonEmpty) {
       List("{") ++ localDefs ++ body.flatMap(x => x.toBoogie).map(s => "  " + s) ++ List("}")
     } else {
@@ -60,22 +62,19 @@ case class BProcedure(
   def globals: Set[BVar] = body.flatMap(c => c.globals).toSet ++ modifies
 }
 
-case class BAxiom(body: BExpr) extends BDeclaration {
-  override def toString: String = s"axiom $body;"
+case class BAxiom(body: BExpr, override val attributes: List[BAttribute]) extends BDeclaration() {
+  override def toString: String = s"axiom $attrString$body;"
 }
 
-case class BFunction(name: String, bvbuiltin: String, in: List[BVar], out: BVar, body: Option[BExpr])
-    extends BDeclaration
+case class BFunction(name: String, in: List[BVar], out: BVar, body: Option[BExpr],
+                     override val attributes: List[BAttribute])
+    extends BDeclaration()
     with Ordered[BFunction] {
+
   override def compare(that: BFunction): Int = name.compare(that.name)
   override def toBoogie: List[String] = {
-    val bvbuiltinString = if (bvbuiltin.isEmpty) {
-      ""
-    } else {
-      s" {:bvbuiltin \"$bvbuiltin\"}"
-    }
     val inString = in.map(_.withType).mkString(", ")
-    val declString = s"function$bvbuiltinString $name($inString) returns (${out.withType})"
+    val declString = s"function $attrString$name($inString) returns (${out.withType})"
     body match {
       case Some(b) => List(declString + " {", "  " + b.toString, "}", "")
       case None    => List(declString + ";")
@@ -88,16 +87,16 @@ case class BFunction(name: String, bvbuiltin: String, in: List[BVar], out: BVar,
   }
 }
 
-case class BVarDecl(variable: BVar) extends BDeclaration with Ordered[BVarDecl] {
+case class BVarDecl(variable: BVar, override val attributes: List[BAttribute]) extends BDeclaration() with Ordered[BVarDecl] {
   def compare(that: BVarDecl): Int = variable.compare(that.variable)
   override def toString: String = if (variable.scope == Scope.Const) {
-    s"const $variable: ${variable.getType};"
+    s"const $attrString$variable: ${variable.getType};"
   } else {
-    s"var $variable: ${variable.getType};"
+    s"var $attrString$variable: ${variable.getType};"
   }
 }
 
-case class BConstAxiomPair(const: BVarDecl, axiom: BAxiom) extends BDeclaration with Ordered[BConstAxiomPair] {
+case class BConstAxiomPair(const: BVarDecl, axiom: BAxiom) extends BDeclaration() with Ordered[BConstAxiomPair] {
   override def compare(that: BConstAxiomPair): Int = const.compare(that.const)
   override def toString: String = const.toString + "\n" + axiom.toString
 }

src/main/scala/ir/Statement.scala

@@ -1,6 +1,8 @@
 package ir
 
-trait Command
+trait Command {
+  def label: Option[String]
+}
 
 trait Statement extends Command {
   def modifies: Set[Global] = Set()
@@ -10,7 +12,7 @@ trait Statement extends Command {
   )
 }
 
-class LocalAssign(var lhs: Variable, var rhs: Expr) extends Statement {
+class LocalAssign(var lhs: Variable, var rhs: Expr, override 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)
@@ -20,31 +22,48 @@ class LocalAssign(var lhs: Variable, var rhs: Expr) extends Statement {
   override def acceptVisit(visitor: Visitor): Statement = visitor.visitLocalAssign(this)
 }
 
-class MemoryAssign(var lhs: Memory, var rhs: MemoryStore) extends Statement {
+object LocalAssign:
+  def unapply(l: LocalAssign): Option[(Variable, Expr, Option[String])] = Some(l.lhs, l.rhs, l.label)
+
+class MemoryAssign(var lhs: Memory, var rhs: MemoryStore, override 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"
   override def acceptVisit(visitor: Visitor): Statement = visitor.visitMemoryAssign(this)
 }
 
+object MemoryAssign:
+  def unapply(m: MemoryAssign): Option[(Memory, MemoryStore, Option[String])] = Some(m.lhs, m.rhs, m.label)
+
 case object NOP extends Statement {
+  override def label: Option[String] = None
   override def toString: String = "<NOP>"
   override def acceptVisit(visitor: Visitor): Statement = this
 }
 
-class Assert(var body: Expr, var comment: Option[String]) extends Statement {
+class Assume(var body: Expr, var comment: Option[String], override val label: Option[String] = None) extends Statement {
+  override def toString: String = s"assume $body" + comment.map(" //" + _)
+  override def acceptVisit(visitor: Visitor): Statement = visitor.visitAssume(this)
+}
+
+object Assume:
+  def unapply(a: Assume): Option[(Expr, Option[String], Option[String])] = Some(a.body, a.comment, a.label)
+
+class Assert(var body: Expr, var comment: Option[String], override val label: Option[String] = None) extends Statement {
   override def toString: String = s"assert $body" + comment.map(" //" + _)
   override def acceptVisit(visitor: Visitor): Statement = visitor.visitAssert(this)
 }
 
+object Assert:
+  def unapply(a: Assert): Option[(Expr, Option[String], Option[String])] = Some(a.body, a.comment, a.label)
+
 trait Jump extends Command {
   def modifies: Set[Global] = Set()
   //def locals: Set[Variable] = Set()
   def calls: Set[Procedure] = Set()
   def acceptVisit(visitor: Visitor): Jump = throw new Exception("visitor " + visitor + " unimplemented for: " + this)
 }
-
-class GoTo(var target: Block, var condition: Option[Expr]) extends Jump {
+class GoTo(var target: Block, var condition: Option[Expr], override val label: Option[String] = None) extends Jump {
   /* override def locals: Set[Variable] = condition match {
     case Some(c) => c.locals
     case None => Set()
@@ -54,7 +73,10 @@ class GoTo(var target: Block, var condition: Option[Expr]) extends Jump {
   override def acceptVisit(visitor: Visitor): Jump = visitor.visitGoTo(this)
 }
 
-class DirectCall(var target: Procedure, var condition: Option[Expr], var returnTarget: Option[Block]) extends Jump {
+object GoTo:
+  def unapply(g: GoTo): Option[(Block, Option[Expr], Option[String])] = Some(g.target, g.condition, g.label)
+
+class DirectCall(var target: Procedure, var condition: Option[Expr], var returnTarget: Option[Block], override val label: Option[String] = None) extends Jump {
   /* override def locals: Set[Variable] = condition match {
     case Some(c) => c.locals
     case None => Set()
@@ -64,11 +86,18 @@ class DirectCall(var target: Procedure, var condition: Option[Expr], var returnT
   override def acceptVisit(visitor: Visitor): Jump = visitor.visitDirectCall(this)
 }
 
-class IndirectCall(var target: Variable, var condition: Option[Expr], var returnTarget: Option[Block]) extends Jump {
+object DirectCall:
+  def unapply(i: DirectCall): Option[(Procedure, Option[Expr], Option[Block], Option[String])] = Some(i.target, i.condition, i.returnTarget, i.label)
+
+class IndirectCall(var target: Variable, var condition: Option[Expr], var returnTarget: Option[Block],
+                   override val label: Option[String] = None) extends Jump {
   /* override def locals: Set[Variable] = condition match {
     case Some(c) => c.locals + target
     case None => Set(target)
   } */
   override def toString: String = s"IndirectCall($target, $condition, ${returnTarget.map(_.label)})"
   override def acceptVisit(visitor: Visitor): Jump = visitor.visitIndirectCall(this)
 }
+
+object IndirectCall:
+  def unapply(i: IndirectCall): Option[(Variable, Option[Expr], Option[Block], Option[String])] = Some(i.target, i.condition, i.returnTarget, i.label)

src/main/scala/ir/Visitor.scala

@@ -21,6 +21,11 @@ abstract class Visitor {
     node
   }
 
+  def visitAssume(node: Assume): Statement = {
+    node.body = visitExpr(node.body)
+    node
+  }
+
   def visitAssert(node: Assert): Statement = {
     node.body = visitExpr(node.body)
     node
@@ -197,6 +202,11 @@ abstract class ReadOnlyVisitor extends Visitor {
     node
   }
 
+  override def visitAssume(node: Assume): Statement = {
+    visitExpr(node.body)
+    node
+  }
+
   override def visitAssert(node: Assert): Statement = {
     visitExpr(node.body)
     node

src/main/scala/specification/Specification.scala

@@ -23,7 +23,7 @@ case class SpecGlobal(name: String, override val size: Int, arraySize: Option[In
   override val toAddrVar: BVar = BVariable("$" + s"${name}_addr", BitVecBType(64), Scope.Const)
   override val toOldVar: BVar = BVariable(s"${name}_old", BitVecBType(size), Scope.Local)
   override val toOldGamma: BVar = BVariable(s"Gamma_${name}_old", BoolBType, Scope.Local)
-  val toAxiom: BAxiom = BAxiom(BinaryBExpr(BoolEQ, toAddrVar, BitVecBLiteral(address, 64)))
+  val toAxiom: BAxiom = BAxiom(BinaryBExpr(BoolEQ, toAddrVar, BitVecBLiteral(address, 64)), List.empty)
   override def resolveSpec: BMemoryLoad = BMemoryLoad(
     BMapVar("mem", MapBType(BitVecBType(64), BitVecBType(8)), Scope.Global),
     toAddrVar,

src/main/scala/translating/BAPLoader.scala

@@ -231,13 +231,15 @@ object BAPLoader {
   def visitImmDef(ctx: ImmDefContext): BAPLocalAssign = {
     val line = visitQuoteString(ctx.tid.name)
     val insn = parseFromAttrs(ctx.attrs, "insn").getOrElse("")
-    BAPLocalAssign(visitImmVar(ctx.lhs), visitExp(ctx.rhs), line, insn)
+    val addr = parseFromAttrs(ctx.attrs, "address").map(x => Integer.parseInt(x.stripPrefix("0x"), 16));
+    BAPLocalAssign(visitImmVar(ctx.lhs), visitExp(ctx.rhs), line, insn, addr)
   }
 
   def visitMemDef(ctx: MemDefContext): BAPMemAssign = {
     val line = visitQuoteString(ctx.tid.name)
     val insn = parseFromAttrs(ctx.attrs, "insn").getOrElse("")
-    BAPMemAssign(visitMemVar(ctx.lhs), visitStore(ctx.rhs), line, insn)
+    val addr = parseFromAttrs(ctx.attrs, "address").map(x => Integer.parseInt(x.stripPrefix("0x"), 16));
+    BAPMemAssign(visitMemVar(ctx.lhs), visitStore(ctx.rhs), line, insn, addr)
   }
 
   def visitQuoteString(ctx: QuoteStringContext): String = ctx.getText.stripPrefix("\"").stripSuffix("\"")

src/main/scala/translating/BAPToIR.scala

@@ -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)
-    case b: BAPLocalAssign => LocalAssign(b.lhs.toIR, b.rhs.toIR)
+    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)
   }
 
@@ -70,12 +70,13 @@ class BAPToIR(var program: BAPProgram, mainAddress: Int) {
       DirectCall(
         nameToProcedure(b.target),
         coerceToBool(b.condition),
-        b.returnTarget.map { (t: String) => labelToBlock(t) }
+        b.returnTarget.map { (t: String) => labelToBlock(t) },
+        Some(b.line)
       )
     case b: BAPIndirectCall =>
-      IndirectCall(b.target.toIR, coerceToBool(b.condition), b.returnTarget.map { (t: String) => labelToBlock(t) })
+      IndirectCall(b.target.toIR, coerceToBool(b.condition), b.returnTarget.map { (t: String) => labelToBlock(t) }, Some(b.line))
     case b: BAPGoTo =>
-      GoTo(labelToBlock(b.target), coerceToBool(b.condition))
+      GoTo(labelToBlock(b.target), coerceToBool(b.condition), Some(b.line))
     case _ =>
       throw new Exception("unsupported jump: " + j)
   }