Non-deterministic GoTos for indirect call resolution

src/main/scala/analysis/Cfg.scala

@@ -304,6 +304,8 @@ case class CfgCallReturnNode(
   */
 trait CfgCommandNode extends CfgNodeWithData[Command] {
   override def copyNode(): CfgCommandNode
+  val block: Block
+  val parent: CfgFunctionEntryNode
 }
 
 /** CFG's representation of a single statement.
@@ -315,8 +317,8 @@ case class CfgStatementNode(
     override val succIntra: mutable.Set[CfgEdge] = mutable.Set[CfgEdge](),
     override val succInter: mutable.Set[CfgEdge] = mutable.Set[CfgEdge](),
     data: Statement,
-    block: Block,
-    parent: CfgFunctionEntryNode
+    override val block: Block,
+    override val parent: CfgFunctionEntryNode
 ) extends CfgCommandNode:
   override def toString: String = s"[Stmt] $data"
 
@@ -332,12 +334,13 @@ case class CfgJumpNode(
     override val succIntra: mutable.Set[CfgEdge] = mutable.Set[CfgEdge](),
     override val succInter: mutable.Set[CfgEdge] = mutable.Set[CfgEdge](),
     data: Jump,
-    block: Block
+    override val block: Block,
+    override val parent: CfgFunctionEntryNode
 ) extends CfgCommandNode:
   override def toString: String = s"[Jmp] $data"
 
   /** Copy this node, but give unique ID and reset edges */
-  override def copyNode(): CfgJumpNode = CfgJumpNode(data = this.data, block = this.block)
+  override def copyNode(): CfgJumpNode = CfgJumpNode(data = this.data, block = this.block, parent = this.parent)
 
 /** A general purpose node which in terms of the IR has no functionality, but can have purpose in the CFG. As example,
   * this is used as a "block" start node for the case that a block contains no statements, but has a `GoTo` as its jump.
@@ -350,13 +353,14 @@ case class CfgGhostNode(
     override val predInter: mutable.Set[CfgEdge] = mutable.Set[CfgEdge](),
     override val succIntra: mutable.Set[CfgEdge] = mutable.Set[CfgEdge](),
     override val succInter: mutable.Set[CfgEdge] = mutable.Set[CfgEdge](),
-    block: Block
+    override val block: Block,
+    override val parent: CfgFunctionEntryNode
 ) extends CfgCommandNode:
   override val data: Statement = NOP
   override def toString: String = s"[NOP]"
 
   /** Copy this node, but give unique ID and reset edges */
-  override def copyNode(): CfgGhostNode = CfgGhostNode(block = this.block)
+  override def copyNode(): CfgGhostNode = CfgGhostNode(block = this.block, parent = this.parent)
 
 /** A control-flow graph. Nodes provide the ability to walk it as both an intra and inter procedural CFG.
   */
@@ -738,7 +742,7 @@ class ProgramCfgFactory:
         */
       def visitJumps(jmps: ArrayBuffer[Jump], prevNode: CfgNode, cond: Expr, solitary: Boolean): Unit = {
 
-        val jmpNode: CfgJumpNode = CfgJumpNode(data = jmps.head, block = block)
+        val jmpNode: CfgJumpNode = CfgJumpNode(data = jmps.head, block = block, parent = funcEntryNode)
         var precNode: CfgNode = prevNode
 
         if (solitary) {
@@ -753,7 +757,7 @@ class ProgramCfgFactory:
           jmps.head match {
             case jmp: GoTo =>
               // `GoTo`s are just edges, so introduce a fake `start of block` that can be jmp'd to
-              val ghostNode = CfgGhostNode(block = block)
+              val ghostNode = CfgGhostNode(block = block, parent = funcEntryNode)
               cfg.addEdge(prevNode, ghostNode, cond)
               precNode = ghostNode
               visitedBlocks += (block -> ghostNode)
@@ -798,12 +802,20 @@ class ProgramCfgFactory:
                 visitBlock(targetBlock, precNode, targetCond)
               }
             }
-
+          case n: NonDetGoTo =>
+            for (targetBlock <- n.targets) {
+              if (visitedBlocks.contains(targetBlock)) {
+                val targetBlockEntry: CfgCommandNode = visitedBlocks(targetBlock)
+                cfg.addEdge(precNode, targetBlockEntry)
+              } else {
+                visitBlock(targetBlock, precNode, TrueLiteral)
+              }
+            }
           case dCall: DirectCall =>
             val targetProc: Procedure = dCall.target
 
             // Branch to this call
-            val calls = jmps.filter(_.isInstanceOf[DirectCall]).map(x => CfgJumpNode(data = x, block = block))
+            val calls = jmps.filter(_.isInstanceOf[DirectCall]).map(x => CfgJumpNode(data = x, block = block, parent = funcEntryNode))
 
             calls.foreach(node => {
               cfg.addEdge(precNode, node, node.data.asInstanceOf[DirectCall].condition.getOrElse(TrueLiteral))

src/main/scala/analysis/VSA.scala

@@ -10,14 +10,18 @@ import scala.collection.immutable
 import util.Logger
 
 /** ValueSets are PowerSet of possible values */
-trait Value
-trait AddressValue(val expr: Expr, val name: String) extends Value
+trait Value {
+  val expr: BitVecLiteral
+}
+trait AddressValue extends Value {
+  val name: String
+}
 
-case class GlobalAddress(val e: Expr, val n: String) extends AddressValue(e, n) {
+case class GlobalAddress(override val expr: BitVecLiteral, override val name: String) extends AddressValue {
   override def toString: String = "GlobalAddress(" + expr + ", " + name + ")"
 }
 
-case class LocalAddress(val e: Expr, val n: String) extends AddressValue(e, n) {
+case class LocalAddress(override val expr: BitVecLiteral, override val name: String) extends AddressValue {
   override def toString: String = "LocalAddress(" + expr + ", " + name + ")"
 }
 

src/main/scala/boogie/BCmd.scala

@@ -106,8 +106,8 @@ case class IfCmd(guard: BExpr, thenCmds: List[BCmd], comment: Option[String] = N
   override def globals: Set[BVar] = guard.globals ++ thenCmds.flatMap(c => c.globals).toSet
 }
 
-case class GoToCmd(destination: String, comment: Option[String] = None) extends BCmd {
-  override def toString: String = s"goto $destination;"
+case class GoToCmd(destinations: Seq[String], comment: Option[String] = None) extends BCmd {
+  override def toString: String = s"goto ${destinations.mkString(", ")};"
 }
 
 case object ReturnCmd extends BCmd {

src/main/scala/ir/Program.scala

@@ -149,6 +149,7 @@ class Procedure(
           case g: GoTo => visitBlock(g.target)
           case d: DirectCall => d.returnTarget.foreach(visitBlock)
           case i: IndirectCall => i.returnTarget.foreach(visitBlock)
+          case n: NonDetGoTo => n.targets.foreach(visitBlock)
         }
       }
     }

src/main/scala/ir/Statement.scala

@@ -32,11 +32,16 @@ case object NOP extends Statement {
   override def acceptVisit(visitor: Visitor): Statement = this
 }
 
-class Assert(var body: Expr, var comment: Option[String]) extends Statement {
+class Assert(var body: Expr, var comment: Option[String] = None) extends Statement {
   override def toString: String = s"assert $body" + comment.map(" //" + _)
   override def acceptVisit(visitor: Visitor): Statement = visitor.visitAssert(this)
 }
 
+class Assume(var body: Expr, var comment: Option[String] = None) extends Statement {
+  override def toString: String = s"assume $body" + comment.map(" //" + _)
+  override def acceptVisit(visitor: Visitor): Statement = visitor.visitAssume(this)
+}
+
 trait Jump extends Command {
   def modifies: Set[Global] = Set()
   //def locals: Set[Variable] = Set()
@@ -54,6 +59,11 @@ class GoTo(var target: Block, var condition: Option[Expr]) extends Jump {
   override def acceptVisit(visitor: Visitor): Jump = visitor.visitGoTo(this)
 }
 
+class NonDetGoTo(var targets: Seq[Block]) extends Jump {
+  override def toString: String = s"NonDetGoTo(${targets.map(_.label).mkString(", ")})"
+  override def acceptVisit(visitor: Visitor): Jump = visitor.visitNonDetGoTo(this)
+}
+
 class DirectCall(var target: Procedure, var condition: Option[Expr], var returnTarget: Option[Block]) extends Jump {
   /* override def locals: Set[Variable] = condition match {
     case Some(c) => c.locals

src/main/scala/ir/Visitor.scala

@@ -26,13 +26,22 @@ abstract class Visitor {
     node
   }
 
+  def visitAssume(node: Assume): Statement = {
+    node.body = visitExpr(node.body)
+    node
+  }
+
   def visitJump(node: Jump): Jump = node.acceptVisit(this)
 
   def visitGoTo(node: GoTo): Jump = {
     node.condition = node.condition.map(visitExpr)
     node
   }
 
+  def visitNonDetGoTo(node: NonDetGoTo): Jump = {
+    node
+  }
+
   def visitDirectCall(node: DirectCall): Jump = {
     node.condition = node.condition.map(visitExpr)
     node
@@ -202,6 +211,11 @@ abstract class ReadOnlyVisitor extends Visitor {
     node
   }
 
+  override def visitAssume(node: Assume): Statement = {
+    visitExpr(node.body)
+    node
+  }
+
   override def visitGoTo(node: GoTo): Jump = {
     node.condition.map(visitExpr)
     node

src/main/scala/translating/IRToBoogie.scala

@@ -385,7 +385,7 @@ class IRToBoogie(var program: Program, var spec: Specification) {
     case d: DirectCall =>
       val call = List(ProcedureCall(d.target.name, List(), List(), List()))
       val returnTarget = d.returnTarget match {
-        case Some(r) => List(GoToCmd(r.label))
+        case Some(r) => List(GoToCmd(Seq(r.label)))
         case None    => List(Comment("no return target"), BAssume(FalseBLiteral))
       }
       d.condition match {
@@ -403,7 +403,7 @@ class IRToBoogie(var program: Program, var spec: Specification) {
       } else {
         val unresolved: List[BCmd] = List(Comment(s"UNRESOLVED: call ${i.target.name}"), BAssume(FalseBLiteral))
         i.returnTarget match {
-          case Some(r) => unresolved :+ GoToCmd(r.label)
+          case Some(r) => unresolved :+ GoToCmd(Seq(r.label))
           case None    => unresolved ++ List(Comment("no return target"), BAssume(FalseBLiteral))
         }
       }
@@ -420,10 +420,12 @@ class IRToBoogie(var program: Program, var spec: Specification) {
         case Some(c) =>
           val guard = c.toBoogie
           val guardGamma = c.toGamma
-          List(BAssert(guardGamma), IfCmd(guard, List(GoToCmd(g.target.label))))
+          List(BAssert(guardGamma), IfCmd(guard, List(GoToCmd(Seq(g.target.label)))))
         case None =>
-          List(GoToCmd(g.target.label))
+          List(GoToCmd(Seq(g.target.label)))
       }
+    case n: NonDetGoTo =>
+      List(GoToCmd(n.targets.map(_.label)))
   }
 
   def translate(s: Statement): List[BCmd] = s match {
@@ -476,6 +478,9 @@ class IRToBoogie(var program: Program, var spec: Specification) {
     case a: Assert =>
       val body = a.body.toBoogie
       List(BAssert(body, a.comment))
+    case a: Assume =>
+      val body = a.body.toBoogie
+      List(BAssume(body, a.comment))
   }
 
   def coerceProcedureCall(target: Procedure): List[BCmd] = {

src/main/scala/util/RunUtils.scala

@@ -92,7 +92,6 @@ object RunUtils {
     }
 
     if (performAnalysis) {
-      iterations += 1;
       IRProgram = analyse(IRProgram, externalFunctions, globals, globalOffsets)
       if (dumpIL) {
         dump_file(serialiseIL(IRProgram), "after-analysis.il")
@@ -207,18 +206,12 @@ object RunUtils {
       }
     }
 
-    def extractExprFromValue(v: Value): Expr = v match {
-      case literalValue: LiteralValue          => literalValue.expr
-      case localAddress: LocalAddress   => localAddress.expr
-      case globalAddress: GlobalAddress => globalAddress.expr
-      case _                            => throw new Exception("Expected a Value with an Expr")
-    }
-
     def process(n: CfgNode): Unit = n match {
-      case commandNode: CfgCommandNode =>
-        commandNode.data match
-          /*
-          We do not want to insert the VSA results into the IR like this
+      /*
+      case c: CfgStatementNode =>
+        c.data match
+
+        //We do not want to insert the VSA results into the IR like this
           case localAssign: LocalAssign =>
             localAssign.rhs match
               case _: MemoryLoad =>
@@ -240,57 +233,43 @@ object RunUtils {
                    */
                 }
               case _ =>
-          */
+      */
+      case c: CfgJumpNode =>
+        val block = c.block
+        c.data match
           case indirectCall: IndirectCall =>
-            if (!commandNode.block.jumps.contains(indirectCall)) {
+            if (!block.jumps.contains(indirectCall)) {
               // We only replace the calls with DirectCalls in the IR, and don't replace the CommandNode.data
               // Hence if we have already processed this CFG node there will be no corresponding IndirectCall in the IR
               // to replace.
               // We want to replace all possible indirect calls based on this CFG, before regenerating it from the IR
               return
             }
             val valueSet: Map[Variable, Set[Value]] = valueSets(n)
-            val functionNames = resolveAddresses(valueSet(indirectCall.target))
-            if (functionNames.size == 1) {
+            val targetNames = resolveAddresses(valueSet(indirectCall.target)).map(_.name).toList.sorted
+            val targets = targetNames.map(name => IRProgram.procedures.filter(_.name.equals(name)).head)
+            if (targets.size == 1) {
               modified = true
-              val block = commandNode.block
-              block.jumps = block.jumps.filter(!_.equals(indirectCall))
-              block.jumps += DirectCall(
-                IRProgram.procedures.filter(_.name.equals(functionNames.head.name)).head,
-                indirectCall.condition,
-                indirectCall.returnTarget
-              )
-            } else if (functionNames.size > 1) {
+              val newCall = DirectCall(targets.head, indirectCall.condition, indirectCall.returnTarget)
+              block.jumps.remove(block.jumps.indexOf(indirectCall))
+              block.jumps.append(newCall)
+            } else if (targets.size > 1) {
               modified = true
-              functionNames.foreach(addressValue =>
-                val block = commandNode.block
-                block.jumps = block.jumps.filter(!_.equals(indirectCall))
-                if (indirectCall.condition.isDefined) {
-                  block.jumps += DirectCall(
-                    IRProgram.procedures.filter(_.name.equals(addressValue.name)).head,
-                    Option(
-                      BinaryExpr(
-                        BVAND,
-                        indirectCall.condition.get,
-                        BinaryExpr(BVEQ, indirectCall.target, addressValue.expr)
-                      )
-                    ),
-                    indirectCall.returnTarget
-                  )
-                } else {
-                  block.jumps += DirectCall(
-                    IRProgram.procedures.filter(_.name.equals(addressValue.name)).head,
-                    Option(BinaryExpr(BVEQ, indirectCall.target, addressValue.expr)),
-                    indirectCall.returnTarget
-                  )
-                }
-              )
-            } else {
-              // must be a call to R30
-              if (!indirectCall.target.equals(exitRegister)) {
-                throw new Exception(
-                  s"Indirect call ${indirectCall} has no possible targets. Value set: ${valueSet(indirectCall.target)}"
-                )
+              val procedure = c.parent.data
+              indirectCall.condition match {
+                // it doesn't seem like calls can actually have conditions in the ARM64 instruction set
+                case Some(_) => throw Exception("indirect call has a condition")
+                case None =>
+                  val newBlocks = for (t <- targets) yield {
+                    val assume = Assume(BinaryExpr(BVEQ, indirectCall.target, BitVecLiteral(t.address.get, 64)))
+                    val newLabel: String = block.label + t.name
+                    val directCall = DirectCall(t, None, indirectCall.returnTarget)
+                    Block(newLabel, None, ArrayBuffer(assume), ArrayBuffer(directCall))
+                  }
+                  procedure.blocks.addAll(newBlocks)
+                  block.jumps.remove(block.jumps.indexOf(indirectCall))
+                  val newCall = NonDetGoTo(newBlocks)
+                  block.jumps.append(newCall)
               }
             }
           case _ =>