Merge pull request #144 from UQ-PAC/lattice-types

Analysis Cleanup and Explicit Types

src/main/scala/analysis/Dependencies.scala

@@ -10,25 +10,22 @@ trait Dependencies[N]:
     * @return
     *   the elements that depend on the given element
     */
-  def outdep(n: N, intra: Boolean): Set[N]
+  def outdep(n: N): Set[N]
 
   /** Incoming dependencies. Used when computing the join from predecessors.
     * @param n
     *   an element from the worklist
     * @return
     *   the elements that the given element depends on
     */
-  def indep(n: N, intra: Boolean): Set[N]
+  def indep(n: N): Set[N]
 
-/** Dependency methods for forward analyses.
-  */
-trait ForwardDependencies extends Dependencies[CfgNode]:
-
-  /* TODO: add functionality here for distinguishing between Intra / Inter */
-
-  // Also add support for getting edges / conditions here?
-  def outdep(n: CfgNode, intra: Boolean = true): Set[CfgNode] =
-    if intra then n.succ(intra).toSet else n.succ(intra).toSet.union(n.succ(!intra).toSet)
+trait InterproceduralForwardDependencies extends Dependencies[CfgNode] {
+  def outdep(n: CfgNode): Set[CfgNode] = n.succInter.toSet
+  def indep(n: CfgNode): Set[CfgNode] = n.predInter.toSet
+}
 
-  def indep(n: CfgNode, intra: Boolean = true): Set[CfgNode] =
-    if intra then n.pred(intra).toSet else n.pred(intra).toSet.union(n.pred(!intra).toSet)
+trait IntraproceduralForwardDependencies extends Dependencies[CfgNode] {
+  def outdep(n: CfgNode): Set[CfgNode] = n.succIntra.toSet
+  def indep(n: CfgNode): Set[CfgNode] = n.predIntra.toSet
+}

src/main/scala/analysis/MemoryModelMap.scala

@@ -108,3 +108,36 @@ class MemoryModelMap {
     s"Stack: ${rangeMap.stackMap}\n Heap: ${rangeMap.heapMap}\n Data: ${rangeMap.dataMap}\n"
 
 }
+
+trait MemoryRegion {
+  val regionIdentifier: String
+  var extent: Option[RangeKey] = None
+}
+
+class StackRegion(override val regionIdentifier: String, val start: BitVecLiteral) extends MemoryRegion {
+  override def toString: String = s"Stack($regionIdentifier, $start)"
+  override def hashCode(): Int = regionIdentifier.hashCode() * start.hashCode()
+  override def equals(obj: Any): Boolean = obj match {
+    case s: StackRegion => s.start == start && s.regionIdentifier == regionIdentifier
+    case _ => false
+  }
+}
+
+class HeapRegion(override val regionIdentifier: String) extends MemoryRegion {
+  override def toString: String = s"Heap($regionIdentifier)"
+  override def hashCode(): Int = regionIdentifier.hashCode()
+  override def equals(obj: Any): Boolean = obj match {
+    case h: HeapRegion => h.regionIdentifier == regionIdentifier
+    case _ => false
+  }
+}
+
+class DataRegion(override val regionIdentifier: String, val start: BitVecLiteral) extends MemoryRegion {
+  override def toString: String = s"Data($regionIdentifier, $start)"
+  override def hashCode(): Int = regionIdentifier.hashCode() * start.hashCode()
+  override def equals(obj: Any): Boolean = obj match {
+    case d: DataRegion => d.start == start && d.regionIdentifier == regionIdentifier
+    case _ => false
+  }
+}
+

src/main/scala/analysis/SteensgaardAnalysis.scala

@@ -1,7 +1,7 @@
 package analysis
 
 import analysis.solvers.{Cons, Term, UnionFindSolver, Var}
-import ir.{Block, DirectCall, Expr, LocalAssign, MemoryAssign, Procedure, Program, Variable}
+import ir.{Block, DirectCall, Expr, LocalAssign, MemoryAssign, Procedure, Program, Variable, BitVecLiteral}
 import util.Logger
 
 import java.io.{File, PrintWriter}
@@ -10,21 +10,21 @@ import scala.collection.mutable.ArrayBuffer
 /** Steensgaard-style pointer analysis. The analysis associates an [[StTerm]] with each variable declaration and
   * expression node in the AST. It is implemented using [[tip.solvers.UnionFindSolver]].
   */
-class SteensgaardAnalysis(program: Program, constantPropResult: Map[CfgNode, Map[Variable, ConstantPropagationLattice.Element]]) extends Analysis[Any] {
+class SteensgaardAnalysis(program: Program, constantPropResult: Map[CfgNode, Map[Variable, FlatElement[BitVecLiteral]]]) extends Analysis[Any] {
 
   val solver: UnionFindSolver[StTerm] = UnionFindSolver()
 
   val stringArr: ArrayBuffer[String] = ArrayBuffer()
 
   var mallocCallTarget: Option[Block] = None
 
-  val constantPropResult2: Map[CfgNode, Map[Variable, ConstantPropagationLattice.Element]] = constantPropResult
+  val constantPropResult2: Map[CfgNode, Map[Variable, FlatElement[BitVecLiteral]]] = constantPropResult
 
   constantPropResult2.values.foreach(v => Logger.info(s"$v"))
 
   /** @inheritdoc
     */
-  def analyze(intra: Boolean): Unit =
+  def analyze(): Unit =
   // generate the constraints by traversing the AST and solve them on-the-fly
     visit(program, ())
 
@@ -219,3 +219,15 @@ case class PointerRef(of: Term[StTerm]) extends StTerm with Cons[StTerm] {
 
   override def toString: String = s"$of"
 }
+
+/** Counter for producing fresh IDs.
+  */
+object Fresh {
+
+  var n = 0
+
+  def next(): Int = {
+    n += 1
+    n
+  }
+}

src/main/scala/analysis/UtilMethods.scala

@@ -11,7 +11,7 @@ import util.Logger
   * @return:
   *   The evaluated expression (e.g. 0x69632)
   */
-def evaluateExpression(exp: Expr, constantPropResult: Map[Variable, ConstantPropagationLattice.FlatElement]): Option[BitVecLiteral] = {
+def evaluateExpression(exp: Expr, constantPropResult: Map[Variable, FlatElement[BitVecLiteral]]): Option[BitVecLiteral] = {
   Logger.debug(s"evaluateExpression: $exp")
   exp match {
     case binOp: BinaryExpr =>
@@ -41,9 +41,9 @@ def evaluateExpression(exp: Expr, constantPropResult: Map[Variable, ConstantProp
       }
     case variable: Variable =>
       constantPropResult(variable) match {
-        case ConstantPropagationLattice.FlatElement.FlatEl(value) => Some(value.asInstanceOf[BitVecLiteral])
-        case ConstantPropagationLattice.FlatElement.Top           => None
-        case ConstantPropagationLattice.FlatElement.Bot           => None
+        case FlatEl(value) => Some(value)
+        case Top           => None
+        case Bottom           => None
       }
     case b: BitVecLiteral => Some(b)
     case _ => //throw new RuntimeException("ERROR: CASE NOT HANDLED: " + exp + "\n")

src/main/scala/analysis/VSA.scala

@@ -29,28 +29,24 @@ case class LiteralValue(expr: BitVecLiteral) extends Value {
   override def toString: String = "Literal(" + expr + ")"
 }
 
-type VSALatticeElem = MapLattice[Variable | MemoryRegion, PowersetLattice[Value]]
+trait ValueSetAnalysis(cfg: ProgramCfg,
+                        globals: Map[BigInt, String],
+                        externalFunctions: Map[BigInt, String],
+                        globalOffsets: Map[BigInt, BigInt],
+                        subroutines: Map[BigInt, String],
+                        mmm: MemoryModelMap,
+                        constantProp: Map[CfgNode, Map[Variable, FlatElement[BitVecLiteral]]]) {
 
-trait MemoryRegionValueSetAnalysis:
+  val powersetLattice: PowersetLattice[Value] = PowersetLattice()
 
-  val cfg: ProgramCfg
-  val globals: Map[BigInt, String]
-  val externalFunctions: Map[BigInt, String]
-  val globalOffsets: Map[BigInt, BigInt]
-  val subroutines: Map[BigInt, String]
-  val mmm: MemoryModelMap
-  val constantProp: Map[CfgNode, Map[Variable, ConstantPropagationLattice.Element]]
+  val mapLattice: MapLattice[Variable | MemoryRegion, Set[Value], PowersetLattice[Value]] = MapLattice(powersetLattice)
 
-  /** The lattice of abstract values.
-    */
-  val powersetLattice: VSALatticeElem
-
-  /** The lattice of abstract states.
-    */
-  val lattice: MapLattice[CfgNode, VSALatticeElem] = MapLattice(powersetLattice)
+  val lattice: MapLattice[CfgNode, Map[Variable | MemoryRegion, Set[Value]], mapLattice.type] = MapLattice(mapLattice)
 
   val domain: Set[CfgNode] = cfg.nodes.toSet
 
+  val first: Set[CfgNode] = Set(cfg.startNode)
+
   private val stackPointer = Register("R31", BitVecType(64))
   private val linkRegister = Register("R30", BitVecType(64))
   private val framePointer = Register("R29", BitVecType(64))
@@ -102,7 +98,7 @@ trait MemoryRegionValueSetAnalysis:
 
   /** Default implementation of eval.
     */
-  def eval(cmd: Command, s: lattice.sublattice.Element, n: CfgNode): lattice.sublattice.Element = {
+  def eval(cmd: Command, s: Map[Variable | MemoryRegion, Set[Value]], n: CfgNode): Map[Variable | MemoryRegion, Set[Value]] = {
     Logger.debug(s"eval: $cmd")
     Logger.debug(s"state: $s")
     Logger.debug(s"node: $n")
@@ -139,11 +135,11 @@ trait MemoryRegionValueSetAnalysis:
                 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))
-                    */
+                  /*
+                // 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 =>
@@ -163,70 +159,31 @@ trait MemoryRegionValueSetAnalysis:
 
   /** Transfer function for state lattice elements.
     */
-  def localTransfer(n: CfgNode, s: lattice.sublattice.Element): lattice.sublattice.Element =
-    n match {
-      case entry: CfgFunctionEntryNode =>
-        mmm.pushContext(entry.data.name)
-        s
-      case _: CfgFunctionExitNode =>
-        mmm.popContext()
-        s
-      case cmd: CfgCommandNode =>
-        eval(cmd.data, s, n)
-      case _ => s // ignore other kinds of nodes
-    }
-
-/** Base class for memory region analysis (non-lifted) lattice.
-  */
-abstract class ValueSetAnalysis(
-    val cfg: ProgramCfg,
-    val globals: Map[BigInt, String],
-    val externalFunctions: Map[BigInt, String],
-    val globalOffsets: Map[BigInt, BigInt],
-    val subroutines: Map[BigInt, String],
-    val mmm: MemoryModelMap,
-    val constantProp: Map[CfgNode, Map[Variable, ConstantPropagationLattice.Element]]
-) extends FlowSensitiveAnalysis(true)
-    with MemoryRegionValueSetAnalysis {
+  def localTransfer(n: CfgNode, s: Map[Variable | MemoryRegion, Set[Value]]): Map[Variable | MemoryRegion, Set[Value]] = n match {
+    case entry: CfgFunctionEntryNode =>
+      mmm.pushContext(entry.data.name)
+      s
+    case _: CfgFunctionExitNode =>
+      mmm.popContext()
+      s
+    case cmd: CfgCommandNode =>
+      eval(cmd.data, s, n)
+    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: lattice.sublattice.Element): lattice.sublattice.Element = localTransfer(n, s)
-
+  def transfer(n: CfgNode, s: Map[Variable | MemoryRegion, Set[Value]]): Map[Variable | MemoryRegion, Set[Value]] = localTransfer(n, s)
 }
 
-abstract class IntraprocValueSetAnalysisWorklistSolver[L <: VSALatticeElem](
+class ValueSetAnalysisSolver(
     cfg: ProgramCfg,
     globals: Map[BigInt, String],
     externalFunctions: Map[BigInt, String],
     globalOffsets: Map[BigInt, BigInt],
     subroutines: Map[BigInt, String],
     mmm: MemoryModelMap,
-    constantProp: Map[CfgNode, Map[Variable, ConstantPropagationLattice.Element]],
-    val powersetLattice: L
+    constantProp: Map[CfgNode, Map[Variable, FlatElement[BitVecLiteral]]],
 ) extends ValueSetAnalysis(cfg, globals, externalFunctions, globalOffsets, subroutines, mmm, constantProp)
-    with SimpleMonotonicSolver[CfgNode]
-    with ForwardDependencies
-
-object ValueSetAnalysis:
-
-  /** Intraprocedural analysis that uses the worklist solver.
-    */
-  class WorklistSolver(
-      cfg: ProgramCfg,
-      globals: Map[BigInt, String],
-      externalFunctions: Map[BigInt, String],
-      globalOffsets: Map[BigInt, BigInt],
-      subroutines: Map[BigInt, String],
-      mmm: MemoryModelMap,
-      constantProp: Map[CfgNode, Map[Variable, ConstantPropagationLattice.Element]]
-  ) extends IntraprocValueSetAnalysisWorklistSolver(
-        cfg,
-        globals,
-        externalFunctions,
-        globalOffsets,
-        subroutines,
-        mmm,
-        constantProp,
-        MapLattice[Variable | MemoryRegion, PowersetLattice[Value]](PowersetLattice[Value])
-      )
+    with InterproceduralForwardDependencies
+    with SimpleMonotonicSolver[CfgNode, Map[Variable | MemoryRegion, Set[Value]], MapLattice[Variable | MemoryRegion, Set[Value], PowersetLattice[Value]]]