Merge pull request #114 from UQ-PAC/yousif-memory-region-analysis

Adding lifted lattice solver

src/main/scala/analysis/Analysis.scala

@@ -124,13 +124,13 @@ trait MemoryRegionAnalysis(val cfg: ProgramCfg,
   }
 
   /**
-    * Controls the pool of stack regions. Each pool is unique to a function.
-    * If the offset has already been defined in the context of the function, then the same region is returned.
-    *
-    * @param expr   : the offset
-    * @param parent : the function entry node
-    * @return the stack region corresponding to the offset
-    */
+   * Controls the pool of stack regions. Each pool is unique to a function.
+   * If the offset has already been defined in the context of the function, then the same region is returned.
+   *
+   * @param expr   : the offset
+   * @param parent : the function entry node
+   * @return the stack region corresponding to the offset
+   */
   def poolMaster(expr: BitVecLiteral, parent: CfgFunctionEntryNode): StackRegion = {
     val stackPool = stackMap.getOrElseUpdate(parent, mutable.HashMap())
     if (stackPool.contains(expr)) {
@@ -161,17 +161,18 @@ trait MemoryRegionAnalysis(val cfg: ProgramCfg,
     buffers
   }
 
-  /** The lattice of abstract values.
-    */
-  val powersetLattice: PowersetLattice[MemoryRegion] = PowersetLattice()
+  val regionLattice: PowersetLattice[MemoryRegion] = PowersetLattice()
 
-  /** The lattice of abstract states.
+  /**
+    * Lifted memory region lattice, with new bottom element representing "unreachable".
     */
-  val lattice: MapLattice[CfgNode, Set[MemoryRegion], PowersetLattice[MemoryRegion]] = MapLattice(powersetLattice)
+  val liftedLattice: LiftLattice[Set[MemoryRegion], PowersetLattice[MemoryRegion]] = LiftLattice(regionLattice)
+
+  val lattice: MapLattice[CfgNode, LiftedElement[Set[MemoryRegion]], LiftLattice[Set[MemoryRegion], PowersetLattice[MemoryRegion]]] = MapLattice(liftedLattice)
 
   val domain: Set[CfgNode] = cfg.nodes.toSet
 
-  val first: Set[CfgNode] = domain.collect { case n: CfgFunctionEntryNode if n.predIntra.isEmpty => n }
+  val first: Set[CfgNode] = cfg.funEntries.toSet
 
   private val stackPointer = Register("R31", BitVecType(64))
   private val linkRegister = Register("R30", BitVecType(64))
@@ -232,22 +233,23 @@ trait MemoryRegionAnalysis(val cfg: ProgramCfg,
                 env // we cannot evaluate this to a concrete value, we need VSA for this
             }
         }
+      // we cannot evaluate this to a concrete value, we need VSA for this
       case _ =>
         Logger.debug(s"type: ${exp.getClass} $exp\n")
         throw new Exception("Unknown type")
     }
   }
 
   /** Transfer function for state lattice elements.
-    */
+   */
   def localTransfer(n: CfgNode, s: Set[MemoryRegion]): Set[MemoryRegion] = n match {
     case cmd: CfgCommandNode =>
       cmd.data match {
         case directCall: DirectCall =>
           if (directCall.target.name == "malloc") {
             evaluateExpression(mallocVariable, constantProp(n)) match {
               case Some(b: BitVecLiteral) =>
-                lattice.sublattice.lub(s, Set(HeapRegion(nextMallocCount())))
+                regionLattice.lub(s, Set(HeapRegion(nextMallocCount(), b)))
               case None => s
             }
           } else {
@@ -258,46 +260,13 @@ trait MemoryRegionAnalysis(val cfg: ProgramCfg,
             return s
           }
           val result = eval(memAssign.rhs.index, s, cmd)
-          /*
-          don't modify the IR in the middle of the analysis like this, also this produces a lot of incorrect results
-          result.collectFirst({
-            case StackRegion(name, _, _, _) =>
-              memAssign.rhs = MemoryStore(
-                Memory(name,
-                  memAssign.rhs.mem.addressSize,
-                  memAssign.rhs.mem.valueSize),
-                memAssign.rhs.index,
-                memAssign.rhs.value, memAssign.rhs.endian,
-                memAssign.rhs.size
-              )
-            case DataRegion(name, _, _, _) =>
-              memAssign.rhs = MemoryStore(
-                Memory(name, memAssign.rhs.mem.addressSize, memAssign.rhs.mem.valueSize),
-                memAssign.rhs.index,
-                memAssign.rhs.value,
-                memAssign.rhs.endian,
-                memAssign.rhs.size
-              )
-            case _ =>
-          })
-          */
-          lattice.sublattice.lub(s, result)
+          regionLattice.lub(s, result)
         case localAssign: LocalAssign =>
           var m = s
           unwrapExpr(localAssign.rhs).foreach {
             case memoryLoad: MemoryLoad =>
               val result = eval(memoryLoad.index, s, cmd)
-              /*
-              don't modify the IR in the middle of the analysis like this, this also produces incorrect results
-              result.collectFirst({
-                case StackRegion(name, _, _, _) =>
-                  memoryLoad.mem = Memory(name, memoryLoad.mem.addressSize, memoryLoad.mem.valueSize)
-                case DataRegion(name, _, _, _) =>
-                  memoryLoad.mem = Memory(name, memoryLoad.mem.addressSize, memoryLoad.mem.valueSize)
-                case _ =>
-              })
-              */
-              m = lattice.sublattice.lub(m, result)
+              m = regionLattice.lub(m, result)
             case _ => m
           }
           m
@@ -306,10 +275,7 @@ trait MemoryRegionAnalysis(val cfg: ProgramCfg,
     case _ => s // ignore other kinds of nodes
   }
 
-  /** Transfer function for state lattice elements. (Same as `localTransfer` for simple value analysis.)
-    */
-  def transfer(n: CfgNode, s: Set[MemoryRegion]): Set[MemoryRegion] = localTransfer(n, s)
-
+  def transferUnlifted(n: CfgNode, s: Set[MemoryRegion]): Set[MemoryRegion] = localTransfer(n, s)
 }
 
 class MemoryRegionAnalysisSolver(
@@ -320,4 +286,15 @@ class MemoryRegionAnalysisSolver(
     constantProp: Map[CfgNode, Map[Variable, FlatElement[BitVecLiteral]]]
 ) extends MemoryRegionAnalysis(cfg, globals, globalOffsets, subroutines, constantProp)
     with IntraproceduralForwardDependencies
-    with SimpleMonotonicSolver[CfgNode, Set[MemoryRegion], PowersetLattice[MemoryRegion]]
+    with Analysis[Map[CfgNode, LiftedElement[Set[MemoryRegion]]]]
+    with WorklistFixpointSolverWithReachability[CfgNode, Set[MemoryRegion], PowersetLattice[MemoryRegion]] {
+
+  override def funsub(n: CfgNode, x: Map[CfgNode, LiftedElement[Set[MemoryRegion]]]): LiftedElement[Set[MemoryRegion]] = {
+    n match {
+      // function entry nodes are always reachable as this is intraprocedural
+      case _: CfgFunctionEntryNode => liftedLattice.lift(regionLattice.bottom)
+      // all other nodes are processed with join+transfer
+      case _ => super.funsub(n, x)
+    }
+  }
+}

src/main/scala/analysis/Cfg.scala

@@ -203,6 +203,7 @@ class ProgramCfg:
 
   var startNode: CfgFunctionEntryNode = _
   var nodes: mutable.Set[CfgNode] = mutable.Set()
+  var funEntries: mutable.Set[CfgFunctionEntryNode] = mutable.Set()
 
   /** Inline edges are for connecting an intraprocedural cfg with a copy of another procedure's intraprocedural cfg
     * which is placed inside this one. They are considered interprocedural edges, and will not be followed if the caller
@@ -414,6 +415,7 @@ class ProgramCfgFactory:
     val funcExitNode: CfgFunctionExitNode = CfgFunctionExitNode(proc)
     cfg.nodes += funcEntryNode
     cfg.nodes += funcExitNode
+    cfg.funEntries += funcEntryNode
 
     procToCfg += (proc -> (funcEntryNode, funcExitNode))
     callToNodes += (funcEntryNode -> mutable.Set())

src/main/scala/analysis/Lattice.scala

@@ -32,6 +32,45 @@ class PowersetLattice[A] extends Lattice[Set[A]] {
   def lub(x: Set[A], y: Set[A]): Set[A] = x.union(y)
 }
 
+trait LiftedElement[+T]
+case class Lift[T](el: T) extends LiftedElement[T] {
+  override def toString = s"Lift($el)"
+}
+case object LiftedBottom extends LiftedElement[Nothing] {
+  override def toString = "LiftBot"
+}
+/**
+ * The lift lattice for `sublattice`.
+ * Supports implicit lifting and unlifting.
+ */
+class LiftLattice[T, +L <: Lattice[T]](val sublattice: L) extends Lattice[LiftedElement[T]] {
+
+  val bottom: LiftedElement[T] = LiftedBottom
+
+  def lub(x: LiftedElement[T], y: LiftedElement[T]): LiftedElement[T] =
+    (x, y) match {
+      case (LiftedBottom, t) => t
+      case (t, LiftedBottom) => t
+      case (Lift(a), Lift(b)) => Lift(sublattice.lub(a, b))
+    }
+
+  /**
+   * Lift elements of the sublattice to this lattice.
+   * Note that this method is declared as implicit, so the conversion can be done automatically.
+   */
+  def lift(x: T): LiftedElement[T] = Lift(x)
+
+  /**
+   * Un-lift elements of this lattice to the sublattice.
+   * Throws an IllegalArgumentException if trying to unlift the bottom element
+   * Note that this method is declared as implicit, so the conversion can be done automatically.
+   */
+  def unlift(x: LiftedElement[T]): T = x match {
+    case Lift(s) => s
+    case LiftedBottom => throw new IllegalArgumentException("Cannot unlift bottom")
+  }
+}
+
 trait FlatElement[+T]
 case class FlatEl[T](el: T) extends FlatElement[T]
 case object Top extends FlatElement[Nothing]

src/main/scala/analysis/MemoryModelMap.scala

@@ -44,27 +44,29 @@ class MemoryModelMap {
     }
   }
 
-  def convertMemoryRegions(memoryRegions: Map[CfgNode, Set[MemoryRegion]], externalFunctions: Map[BigInt, String]): Unit = {
+  def convertMemoryRegions(memoryRegions: Map[CfgNode, LiftedElement[Set[MemoryRegion]]], externalFunctions: Map[BigInt, String]): Unit = {
     // map externalFunctions name, value to DataRegion(name, value) and then sort by value
     val externalFunctionRgns = externalFunctions.map((offset, name) => DataRegion(name, BitVecLiteral(offset, 64)))
 
     // get all function exit node
     val exitNodes = memoryRegions.keys.collect { case e: CfgFunctionExitNode => e }
     exitNodes.foreach(exitNode =>
-      val node = memoryRegions(exitNode)
+      memoryRegions(exitNode) match {
+        case Lift(node) =>
+          // for each function exit node we get the memory region and add it to the mapping
+          val stackRgns = node.collect { case r: StackRegion => r }.toList.sortBy(_.start.value)
+          val dataRgns = node.collect { case r: DataRegion => r }
 
-      // for each function exit node we get the memory region and add it to the mapping
-      val stackRgns = node.collect { case r: StackRegion => r }.toList.sortBy(_.start.value)
-      val dataRgns = node.collect { case r: DataRegion => r }
+          // add externalFunctionRgn to dataRgns and sort by value
+          val allDataRgns = (dataRgns ++ externalFunctionRgns).toList.sortBy(_.start.value)
 
-      // add externalFunctionRgn to dataRgns and sort by value
-      val allDataRgns = (dataRgns ++ externalFunctionRgns).toList.sortBy(_.start.value)
+          allStacks(exitNode.data.name) = stackRgns
 
-      allStacks(exitNode.data.name) = stackRgns
-
-      for (dataRgn <- allDataRgns) {
-        add(dataRgn.start.value, dataRgn)
-      }
+          for (dataRgn <- allDataRgns) {
+            add(dataRgn.start.value, dataRgn)
+          }
+        case LiftedBottom =>
+    }
     )
   }
 
@@ -123,8 +125,8 @@ class StackRegion(override val regionIdentifier: String, val start: BitVecLitera
   }
 }
 
-class HeapRegion(override val regionIdentifier: String) extends MemoryRegion {
-  override def toString: String = s"Heap($regionIdentifier)"
+class HeapRegion(override val regionIdentifier: String, val size: BitVecLiteral) extends MemoryRegion {
+  override def toString: String = s"Heap($regionIdentifier, $size)"
   override def hashCode(): Int = regionIdentifier.hashCode()
   override def equals(obj: Any): Boolean = obj match {
     case h: HeapRegion => h.regionIdentifier == regionIdentifier

src/main/scala/analysis/UtilMethods.scala

@@ -25,6 +25,7 @@ def evaluateExpression(exp: Expr, constantPropResult: Map[Variable, FlatElement[
             case BVSUB => Some(BitVectorEval.smt_bvsub(l, r))
             case BVASHR => Some(BitVectorEval.smt_bvashr(l, r))
             case BVCOMP => Some(BitVectorEval.smt_bvcomp(l, r))
+            case BVCONCAT => Some(BitVectorEval.smt_concat(l, r))
             case _ => throw new RuntimeException("Binary operation support not implemented: " + binOp.op)
           }
         case _ => None

src/main/scala/analysis/VSA.scala

@@ -41,7 +41,9 @@ trait ValueSetAnalysis(cfg: ProgramCfg,
 
   val mapLattice: MapLattice[Variable | MemoryRegion, Set[Value], PowersetLattice[Value]] = MapLattice(powersetLattice)
 
-  val lattice: MapLattice[CfgNode, Map[Variable | MemoryRegion, Set[Value]], mapLattice.type] = MapLattice(mapLattice)
+  val liftedLattice: LiftLattice[Map[Variable | MemoryRegion, Set[Value]], mapLattice.type] = LiftLattice(mapLattice)
+
+  val lattice: MapLattice[CfgNode, LiftedElement[Map[Variable | MemoryRegion, Set[Value]]], LiftLattice[Map[Variable | MemoryRegion, Set[Value]], mapLattice.type]] = MapLattice(liftedLattice)
 
   val domain: Set[CfgNode] = cfg.nodes.toSet
 
@@ -102,6 +104,7 @@ trait ValueSetAnalysis(cfg: ProgramCfg,
     Logger.debug(s"eval: $cmd")
     Logger.debug(s"state: $s")
     Logger.debug(s"node: $n")
+    var m = s
     cmd match
       case localAssign: LocalAssign =>
         localAssign.rhs match
@@ -111,19 +114,23 @@ trait ValueSetAnalysis(cfg: ProgramCfg,
                 // this is an exception to the rule and only applies to data regions
                 evaluateExpression(memoryLoad.index, constantProp(n)) match
                   case Some(bitVecLiteral: BitVecLiteral) =>
-                    val m = s + (r -> Set(getValueType(bitVecLiteral)))
-                    m + (localAssign.lhs -> m(r))
+                    m = m + (r -> Set(getValueType(bitVecLiteral)))
+                    m = m + (localAssign.lhs -> m(r))
+                    m
                   case None =>
-                    s + (localAssign.lhs -> s(r))
+                    m = m + (localAssign.lhs -> m(r))
+                    m
               case None =>
                 Logger.warn("could not find region for " + localAssign)
-                s
+                m
           case e: Expr =>
             evaluateExpression(e, constantProp(n)) match {
-              case Some(bv: BitVecLiteral) => s + (localAssign.lhs -> Set(getValueType(bv)))
+              case Some(bv: BitVecLiteral) =>
+                m = m + (localAssign.lhs -> Set(getValueType(bv)))
+                m
               case None =>
                 Logger.warn("could not evaluate expression" + e)
-                s
+                m
             }
       case memAssign: MemoryAssign =>
         memAssign.rhs.index match
@@ -134,27 +141,29 @@ trait ValueSetAnalysis(cfg: ProgramCfg,
                 val storeValue = memAssign.rhs.value
                 evaluateExpression(storeValue, constantProp(n)) match
                   case Some(bitVecLiteral: BitVecLiteral) =>
-                    s + (r -> Set(getValueType(bitVecLiteral)))
-                  /*
-                // TODO constant prop returned BOT OR TOP. Merge regions because RHS could be a memory loaded address
-                case variable: Variable =>
-                  s + (r -> s(variable))
-                  */
+                    m = m + (r -> Set(getValueType(bitVecLiteral)))
+                    m
+                    /*
+                  // TODO constant prop returned BOT OR TOP. Merge regions because RHS could be a memory loaded address
+                  case variable: Variable =>
+                    s + (r -> s(variable))
+                    */
                   case None =>
                     storeValue.match {
                       case v: Variable =>
-                        s + (r -> s(v))
+                        m = m + (r -> m(v))
+                        m
                       case _ =>
                         Logger.warn(s"Too Complex: $storeValue") // do nothing
-                        s
+                        m
                     }
               case None =>
                 Logger.warn("could not find region for " + memAssign)
-                s
+                m
           case _ =>
-            s
+            m
       case _ =>
-        s
+        m
   }
 
   /** Transfer function for state lattice elements.
@@ -173,7 +182,7 @@ trait ValueSetAnalysis(cfg: ProgramCfg,
 
   /** Transfer function for state lattice elements. (Same as `localTransfer` for simple value analysis.)
     */
-  def transfer(n: CfgNode, s: Map[Variable | MemoryRegion, Set[Value]]): Map[Variable | MemoryRegion, Set[Value]] = localTransfer(n, s)
+  def transferUnlifted(n: CfgNode, s: Map[Variable | MemoryRegion, Set[Value]]): Map[Variable | MemoryRegion, Set[Value]] = localTransfer(n, s)
 }
 
 class ValueSetAnalysisSolver(
@@ -186,4 +195,15 @@ class ValueSetAnalysisSolver(
     constantProp: Map[CfgNode, Map[Variable, FlatElement[BitVecLiteral]]],
 ) extends ValueSetAnalysis(cfg, globals, externalFunctions, globalOffsets, subroutines, mmm, constantProp)
     with InterproceduralForwardDependencies
-    with SimpleMonotonicSolver[CfgNode, Map[Variable | MemoryRegion, Set[Value]], MapLattice[Variable | MemoryRegion, Set[Value], PowersetLattice[Value]]]
+    with Analysis[Map[CfgNode, LiftedElement[Map[Variable | MemoryRegion, Set[Value]]]]]
+    with WorklistFixpointSolverWithReachability[CfgNode, Map[Variable | MemoryRegion, Set[Value]], MapLattice[Variable | MemoryRegion, Set[Value], PowersetLattice[Value]]] {
+
+  override def funsub(n: CfgNode, x: Map[CfgNode, LiftedElement[Map[Variable | MemoryRegion, Set[Value]]]]): LiftedElement[Map[Variable | MemoryRegion, Set[Value]]] = {
+    n match {
+      // function entry nodes are always reachable as this is intraprocedural
+      case _: CfgFunctionEntryNode => liftedLattice.lift(mapLattice.bottom)
+      // all other nodes are processed with join+transfer
+      case _ => super.funsub(n, x)
+    }
+  }
+}