Merge pull request #152 from UQ-PAC/stream-writers

Stream writer boogie file translation and function trimming for large binaries

src/main/scala/Main.scala

@@ -34,6 +34,10 @@ object Main {
       interpret: Flag,
       @arg(name = "dump-il", doc = "Dump the Intermediate Language to text.")
       dumpIL: Option[String],
+      @arg(name = "main-procedure-name", short = 'm', doc = "Name of the main procedure to begin analysis at.")
+      mainProcedureName: String = "main",
+      @arg(name = "procedure-call-depth", doc = "Cull procedures beyond this call depth from the main function (defaults to Int.MaxValue)")
+      procedureDepth: Int = Int.MaxValue,
       @arg(name = "help", short = 'h', doc = "Show this help message.")
       help: Flag,
       @arg(name = "analysis-results", doc = "Log analysis results in files at specified path.")
@@ -63,7 +67,7 @@ object Main {
     }
 
     val q = BASILConfig(
-      loading = ILLoadingConfig(conf.adtFileName, conf.relfFileName, conf.specFileName, conf.dumpIL),
+      loading = ILLoadingConfig(conf.adtFileName, conf.relfFileName, conf.specFileName, conf.dumpIL, conf.mainProcedureName, conf.procedureDepth),
       runInterpret = conf.interpret.value,
       staticAnalysis = if conf.analyse.value then Some(StaticAnalysisConfig(conf.dumpIL, conf.analysisResults, conf.analysisResultsDot)) else None,
       boogieTranslation = BoogieGeneratorConfig(if conf.lambdaStores.value then BoogieMemoryAccessMode.LambdaStoreSelect else BoogieMemoryAccessMode.SuccessiveStoreSelect),

src/main/scala/boogie/BExpr.scala

@@ -1,6 +1,9 @@
 package boogie
-import ir._
-import specification._
+import ir.*
+import specification.*
+import collection.mutable
+
+import java.io.Writer
 
 trait BExpr {
   def getType: BType
@@ -15,6 +18,7 @@ trait BExpr {
   def resolveSpecL: BExpr = this
   def resolveInsideOld: BExpr = this
   def loads: Set[BExpr] = Set()
+  def serialiseBoogie(w: Writer): Unit = w.append(toString)
 }
 
 trait BLiteral extends BExpr {}
@@ -59,11 +63,18 @@ case class BVExtract(end: Int, start: Int, body: BExpr) extends BExpr {
   override def resolveInsideOld: BVExtract = copy(body = body.resolveInsideOld)
   override def removeOld: BVExtract = copy(body = body.removeOld)
   override def loads: Set[BExpr] = body.loads
+
+  override def serialiseBoogie(w: Writer): Unit = {
+    body.serialiseBoogie(w)
+    w.append(s"[$end:$start]")
+  }
+
 }
 
 case class BVRepeat(repeats: Int, body: BExpr) extends BExpr {
   override def getType: BitVecBType = BitVecBType(bodySize * repeats)
 
+
   private def bodySize: Int = body.getType match {
     case bv: BitVecBType => bv.size
     case _ => throw new Exception("type mismatch, non bv expression: " + body + " in body of extract: " + this)
@@ -72,6 +83,13 @@ case class BVRepeat(repeats: Int, body: BExpr) extends BExpr {
 
   override def toString: String = s"$fnName($body)"
 
+  override def serialiseBoogie(w: Writer): Unit = {
+    w.append(fnName)
+    w.append("(")
+    body.serialiseBoogie(w)
+    w.append(")")
+  }
+
   override def functionOps: Set[FunctionOp] = {
     val thisFn = BVFunctionOp(fnName, s"repeat $repeats", List(BParam(BitVecBType(bodySize))), BParam(getType))
     body.functionOps + thisFn
@@ -100,6 +118,13 @@ case class BVZeroExtend(extension: Int, body: BExpr) extends BExpr {
 
   override def toString: String = s"$fnName($body)"
 
+  override def serialiseBoogie(w: Writer): Unit = {
+    w.append(fnName)
+    w.append("(")
+    body.serialiseBoogie(w)
+    w.append(")")
+  }
+
   override def functionOps: Set[FunctionOp] = {
     val thisFn = BVFunctionOp(fnName, s"zero_extend $extension", List(BParam(BitVecBType(bodySize))), BParam(getType))
     body.functionOps + thisFn
@@ -128,6 +153,14 @@ case class BVSignExtend(extension: Int, body: BExpr) extends BExpr {
 
   override def toString: String = s"$fnName($body)"
 
+  override def serialiseBoogie(w: Writer): Unit = {
+    w.append(fnName)
+    w.append("(")
+    body.serialiseBoogie(w)
+    w.append(")")
+  }
+
+
   override def functionOps: Set[FunctionOp] = {
     val thisFn = BVFunctionOp(fnName, s"sign_extend $extension", List(BParam(BitVecBType(bodySize))), BParam(getType))
     body.functionOps + thisFn
@@ -297,6 +330,32 @@ case class BinaryBExpr(op: BinOp, arg1: BExpr, arg2: BExpr) extends BExpr {
     case _               => throw new Exception("type mismatch")
   }
 
+  override def serialiseBoogie(w: Writer): Unit = {
+    val traversalQueue = mutable.Stack[BExpr | BinOp | String]()
+    traversalQueue.append(this)
+
+    while (traversalQueue.nonEmpty) {
+      val next = traversalQueue.pop()
+
+      def infix(b: BinaryBExpr): Unit = traversalQueue.pushAll(Seq("(", b.arg1, s" ${b.op} ", b.arg2, ")").reverse)
+      def prefix(b: BinaryBExpr): Unit = traversalQueue.pushAll(Seq(s"bv${b.op}${b.inSize}(", b.arg1, ",", b.arg2, ")").reverse)
+
+      next match
+        case b: BinaryBExpr =>
+          b.op match {
+            case bOp: BoolBinOp => infix(b)
+            case bOp: BVBinOp => bOp match {
+                case BVEQ | BVNEQ | BVCONCAT => infix(b)
+                case _ => prefix(b)
+              }
+            case bOp: IntBinOp => infix(b)
+          }
+        case b: BExpr => b.serialiseBoogie(w)
+        case b: BinOp => w.append(b.toString)
+        case s: String => w.append(s)
+    }
+  }
+
   override def toString: String = op match {
     case bOp: BoolBinOp => s"($arg1 $bOp $arg2)"
     case bOp: BVBinOp =>
@@ -309,6 +368,8 @@ case class BinaryBExpr(op: BinOp, arg1: BExpr, arg2: BExpr) extends BExpr {
     case bOp: IntBinOp => s"($arg1 $bOp $arg2)"
   }
 
+
+
   override def functionOps: Set[FunctionOp] = {
     val thisFn = op match {
       case b: BVBinOp =>

src/main/scala/boogie/BProgram.scala

@@ -1,12 +1,27 @@
 package boogie
+import java.io.{StringWriter, Writer}
 
 case class BProgram(declarations: List[BDeclaration]) {
-  override def toString: String = declarations.flatMap(x => x.toBoogie).mkString("\n")
+  override def toString: String = declarations.flatMap(x => x.toBoogie).mkString(System.lineSeparator())
+
+  def writeToString(w: Writer): Unit = {
+    declarations.foreach(x => {
+      x.writeToString(w)
+    })
+  }
 }
 
 trait BDeclaration extends HasAttributes {
   override def attributes: List[BAttribute] = List()
   def toBoogie: List[String] = List(toString)
+
+  final def writeToString(w: Writer): Unit = {
+    for (elem <- toBoogie) {
+      w.append(elem)
+      w.append(System.lineSeparator())
+    }
+  }
+
 }
 
 case class BProcedure(
@@ -27,12 +42,12 @@ case class BProcedure(
   override def compare(that: BProcedure): Int = name.compare(that.name)
   override def toBoogie: List[String] = {
     val header = s"procedure $attrString$name(${in.map(_.withType).mkString(", ")})"
+    val implHeader = s"implementation $attrString$name(${in.map(_.withType).mkString(", ")})"
     val returns = if (out.nonEmpty) {
       s" returns (${out.map(_.withType).mkString(", ")})"
     } else {
       ""
     }
-    val semicolon = if body.nonEmpty then "" else ";"
     val modifiesStr = if (modifies.nonEmpty) {
       List(s"  modifies ${modifies.toSeq.sorted.mkString(", ")};")
     } else {
@@ -49,9 +64,17 @@ case class BProcedure(
     } else {
       List()
     }
-    List(
-      header + returns + semicolon
-    ) ++ modifiesStr ++ requiresStrs ++ freeRequiresStrs ++ ensuresStrs ++ freeEnsuresStrs ++ bodyStr ++ List("")
+
+    val procDecl = s"$header$returns;"
+    val procList = List(procDecl) ++ modifiesStr ++ requiresStrs ++ freeRequiresStrs ++ ensuresStrs ++ freeEnsuresStrs
+    val implDecl = s"$implHeader$returns"
+    val implList = if (body.nonEmpty) {
+      List("", implDecl) ++ bodyStr
+    } else {
+      List()
+    }
+
+    procList ++ implList ++ List("")
   }
   override def toString: String = toBoogie.mkString("\n")
   def functionOps: Set[FunctionOp] =
@@ -72,12 +95,21 @@ case class BFunction(name: String, in: List[BVar], out: BVar, body: Option[BExpr
     with Ordered[BFunction] {
   override def compare(that: BFunction): Int = name.compare(that.name)
   override def toBoogie: List[String] = {
+    val s = new StringWriter()
+
     val inString = in.map(_.withType).mkString(", ")
     val declString = s"function $attrString$name($inString) returns (${out.withType})"
-    body match {
-      case Some(b) => List(declString + " {", "  " + b.toString, "}", "")
-      case None    => List(declString + ";")
+    s.append(declString)
+
+    val decl = body match {
+      case Some(b) =>
+        s.append(" {" + System.lineSeparator() + "  ")
+        b.serialiseBoogie(s)
+        s.append(System.lineSeparator())
+        s.append("}" + System.lineSeparator())
+      case None    => s.append(";")
     }
+    List(s.toString)
   }
   override def toString: String = toBoogie.mkString("\n")
   def functionOps: Set[FunctionOp] = body match {

src/main/scala/ir/Expr.scala

@@ -146,6 +146,7 @@ sealed trait IntUnOp(op: String) extends UnOp {
 
 case object IntNEG extends IntUnOp("-")
 
+
 sealed trait BVUnOp(op: String) extends UnOp {
   override def toString: String = op
 }

src/main/scala/ir/IRType.scala

@@ -22,3 +22,12 @@ case class BitVecType(size: Int) extends IRType("bv" + size) {
 case class MapType(param: IRType, result: IRType) extends IRType(s"[$param]$result") {
   override def toBoogie: BType = MapBType(param.toBoogie, result.toBoogie)
 }
+
+def coerceToBool(e: Expr): Expr = {
+  e.getType match {
+    case BitVecType(s) => BinaryExpr(BVNEQ, e, BitVecLiteral(0, s))
+    case IntType => BinaryExpr(IntNEQ, e, IntLiteral(0))
+    case BoolType => e
+    case MapType(_, _) => ???
+  }
+}

src/main/scala/ir/Interpreter.scala

@@ -170,7 +170,7 @@ class Interpreter() {
           case BoolNOT => if evalBool(un.arg, env) == TrueLiteral then FalseLiteral else TrueLiteral
           case _ => ???
         }
-
+      case _ => ???
     }
   }
 

src/main/scala/ir/Program.scala

@@ -8,25 +8,39 @@ import analysis.BitVectorEval
 class Program(var procedures: ArrayBuffer[Procedure], var mainProcedure: Procedure, var initialMemory: ArrayBuffer[MemorySection], var readOnlyMemory: ArrayBuffer[MemorySection]) {
 
   // This shouldn't be run before indirect calls are resolved
-  def stripUnreachableFunctions(): Unit = {
-    val functionToChildren = procedures.map(f => f.name -> f.calls.map(_.name)).toMap
 
-    var next = mainProcedure.name
-    var reachableNames: Set[String] = Set(next)
-    var toVisit: List[String] = List()
+
+  def stripUnreachableFunctions(depth: Int = Int.MaxValue): Unit = {
+    val procedureCalleeNames = procedures.map(f => f.name -> f.calls.map(_.name)).toMap
+
+    var toVisit: mutable.LinkedHashSet[(Int, String)] = mutable.LinkedHashSet((0, mainProcedure.name))
     var reachableFound = true
-    while (reachableFound) {
-      val children = functionToChildren(next) -- reachableNames -- toVisit - next
-      reachableNames = reachableNames ++ children
-      toVisit = toVisit ++ children
-      if (toVisit.isEmpty) {
-        reachableFound = false
-      } else {
-        next = toVisit.head
-        toVisit = toVisit.tail
+    val reachableNames = mutable.HashMap[String, Int]()
+    while (toVisit.nonEmpty) {
+      val next = toVisit.head
+      toVisit.remove(next)
+
+      if (next._1 <= depth) {
+
+        def addName(depth: Int, name: String): Unit = {
+          val oldDepth = reachableNames.getOrElse(name, Integer.MAX_VALUE)
+          reachableNames.put(next._2, if depth < oldDepth then depth else oldDepth)
+        }
+        addName(next._1, next._2)
+
+        val callees = procedureCalleeNames(next._2)
+
+        toVisit.addAll(callees.diff(reachableNames.keySet).map(c => (next._1 + 1, c)))
+        callees.foreach(c => addName(next._1 + 1, c))
       }
     }
-    procedures = procedures.filter(f => reachableNames.contains(f.name))
+    procedures = procedures.filter(f => reachableNames.keySet.contains(f.name))
+
+    for (elem <- procedures.filter(c => c.calls.exists(s => !procedures.contains(s)))) {
+      // last layer is analysed only as specifications so we remove the body for anything that calls
+      // a function we have removed
+      elem.blocks.clear()
+    }
   }
 
   def setModifies(specModifies: Map[String, List[String]]): Unit = {

src/main/scala/translating/BAPToIR.scala

@@ -2,7 +2,7 @@ package translating
 
 import bap.*
 import boogie.UnaryBExpr
-import ir.{UnaryExpr, *}
+import ir.{UnaryExpr, BinaryExpr, *}
 import specification.*
 
 import scala.collection.mutable
@@ -147,10 +147,27 @@ class BAPToIR(var program: BAPProgram, mainAddress: Int) {
     * Converts a BAPExpr condition that returns a bitvector of size 1 to an Expr condition that returns a Boolean
     *
     * If negative is true then the negation of the condition is returned
+    *
+    * If the BAPExpr uses a comparator that returns a Boolean then no further conversion is performed except negation,
+    * if necessary.
     * */
   private def convertConditionBool(expr: BAPExpr, negative: Boolean): Expr = {
-    val op = if negative then BVEQ else BVNEQ
-    BinaryExpr(op, expr.toIR, BitVecLiteral(0, expr.size))
+    val e = expr.toIR
+    e.getType match {
+      case BitVecType(s) =>
+        if (negative) {
+          BinaryExpr(BVEQ, e, BitVecLiteral(0, s))
+        } else {
+          BinaryExpr(BVNEQ, e, BitVecLiteral(0, s))
+        }
+      case BoolType =>
+        if (negative) {
+          UnaryExpr(BoolNOT, e)
+        } else {
+          e
+        }
+      case _ => ???
+    }
   }
 
   private def newBlockCondition(block: Block, target: Block, condition: Expr): Block = {