Adding lifted lattice solver

src/main/scala/analysis/Analysis.scala

@@ -253,7 +253,7 @@ trait MemoryRegionAnalysisMisc:
 
   /** The lattice of abstract states.
     */
-  val lattice: MapLattice[CfgNode, PowersetLattice[MemoryRegion]] = MapLattice(powersetLattice)
+  val stateLattice: MapLattice[CfgNode, PowersetLattice[MemoryRegion]] = MapLattice(powersetLattice)
 
   val domain: Set[CfgNode] = cfg.nodes.toSet
 
@@ -267,7 +267,7 @@ trait MemoryRegionAnalysisMisc:
 
   /** Default implementation of eval.
     */
-  def eval(exp: Expr, env: lattice.sublattice.Element, n: CfgNode): lattice.sublattice.Element = {
+  def eval(exp: Expr, env: stateLattice.sublattice.Element, n: CfgNode): stateLattice.sublattice.Element = {
     Logger.debug(s"evaluating $exp")
     Logger.debug(s"env: $env")
     Logger.debug(s"n: $n")
@@ -325,13 +325,13 @@ trait MemoryRegionAnalysisMisc:
 
   /** Transfer function for state lattice elements.
     */
-  def localTransfer(n: CfgNode, s: lattice.sublattice.Element): lattice.sublattice.Element =
+  def localTransfer(n: CfgNode, s: stateLattice.sublattice.Element): stateLattice.sublattice.Element =
     n match {
       case cmd: CfgCommandNode =>
         cmd.data match {
           case directCall: DirectCall =>
             if (directCall.target.name == "malloc") {
-              return lattice.sublattice.lub(
+              return stateLattice.sublattice.lub(
                 s,
                 Set(HeapRegion(getNextMallocCount(), evaluateExpression(mallocVariable, n, constantProp(n)), None))
               )
@@ -365,7 +365,7 @@ trait MemoryRegionAnalysisMisc:
               case _ =>
             })
             */
-            lattice.sublattice.lub(s, result)
+            stateLattice.sublattice.lub(s, result)
           case localAssign: LocalAssign =>
             var m = s
             unwrapExpr(localAssign.rhs).foreach {
@@ -381,7 +381,7 @@ trait MemoryRegionAnalysisMisc:
                   case _ =>
                 })
                 */
-                m = lattice.sublattice.lub(m, result)
+                m = stateLattice.sublattice.lub(m, result)
               case _ => m
             }
             m
@@ -403,7 +403,51 @@ abstract class MemoryRegionAnalysis(
 
   /** 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: stateLattice.sublattice.Element): stateLattice.sublattice.Element = localTransfer(n, s)
+
+/**
+ * Base class for memory region analysis with lifted lattice, where the extra bottom element represents "unreachable".
+ */
+abstract class LiftedMemoryRegionAnalysis[P <: ProgramCfg](
+    val cfg: ProgramCfg,
+    val globals: Map[BigInt, String],
+    val globalOffsets: Map[BigInt, BigInt],
+    val subroutines: Map[BigInt, String],
+    val constantProp: Map[CfgNode, Map[Variable, ConstantPropagationLattice.Element]]
+) extends FlowSensitiveAnalysis(false)
+    with MapLatticeSolver[CfgNode]
+    with MemoryRegionAnalysisMisc {
+
+  /**
+   * Lifted state lattice, with new bottom element representing "unreachable".
+   */
+  val liftedstatelattice: LiftLattice[stateLattice.type] = new LiftLattice(stateLattice)
+
+  /**
+   * The analysis lattice.
+   */
+  val lattice: MapLattice[CfgNode, liftedstatelattice.type] = new MapLattice(liftedstatelattice)
+
+  val domain: Set[CfgNode] = cfg.nodes.toSet
+
+  /**
+   * The worklist is initialized with all function entry nodes.
+   */
+  val first: Set[CfgNode] = cfg.funEntries.toSet[CfgNode]
+
+  /**
+   * Overrides `funsub` from [[tip.solvers.MapLatticeSolver]], treating function entry nodes as reachable.
+   */
+  override def funsub(n: CfgNode, x: lattice.Element, intra: Boolean): liftedstatelattice.Element = {
+    import liftedstatelattice._
+    n match {
+      // function entry nodes are always reachable (if intra-procedural analysis)
+      case _: CfgFunctionEntryNode => lift(stateLattice.bottom)
+      // all other nodes are processed with join+transfer
+      case _ => super.funsub(n, x, intra)
+    }
+  }
+}
 
 abstract class IntraprocMemoryRegionAnalysisWorklistSolver[L <: PowersetLattice[MemoryRegion]](
     cfg: ProgramCfg,
@@ -412,7 +456,7 @@ abstract class IntraprocMemoryRegionAnalysisWorklistSolver[L <: PowersetLattice[
     subroutines: Map[BigInt, String],
     constantProp: Map[CfgNode, Map[Variable, ConstantPropagationLattice.Element]],
     val powersetLattice: L
-) extends MemoryRegionAnalysis(cfg, globals, globalOffsets, subroutines, constantProp)
+) extends LiftedMemoryRegionAnalysis(cfg, globals, globalOffsets, subroutines, constantProp)
     with SimpleMonotonicSolver[CfgNode]
     with ForwardDependencies
 

src/main/scala/analysis/Cfg.scala

@@ -366,6 +366,7 @@ class ProgramCfg:
 
   var edges: mutable.Set[CfgEdge] = mutable.Set[CfgEdge]()
   var nodes: mutable.Set[CfgNode] = mutable.Set[CfgNode]()
+  var funEntries: mutable.Set[CfgFunctionEntryNode] = mutable.Set[CfgFunctionEntryNode]()
 
   /** 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
@@ -481,6 +482,11 @@ class ProgramCfg:
   def addNode(node: CfgNode): Unit =
     nodes += node
 
+  /** Add a function entry node to the CFG.
+    */
+  def addFunEntryNode(node: CfgFunctionEntryNode): Unit =
+    funEntries += node
+
   /** Returns a Graphviz dot representation of the CFG. Each node is labeled using the given function labeler.
     */
   def toDot(labeler: CfgNode => String, idGen: (CfgNode, Int) => String): String = {
@@ -630,6 +636,7 @@ class ProgramCfgFactory:
     val funcExitNode: CfgFunctionExitNode = CfgFunctionExitNode(data = proc)
     cfg.addNode(funcEntryNode)
     cfg.addNode(funcExitNode)
+    cfg.addFunEntryNode(funcEntryNode)
 
     procToCfg += (proc -> (funcEntryNode, funcExitNode))
     callToNodes += (funcEntryNode -> mutable.Set[CfgCommandNode]())

src/main/scala/analysis/Lattice.scala

@@ -1,9 +1,11 @@
 package analysis
 
-import ir._
+import ir.*
 import analysis.BitVectorEval
 import util.Logger
 
+import scala.language.implicitConversions
+
 /** Basic lattice
   */
 trait Lattice:
@@ -79,6 +81,48 @@ class PowersetLattice[A] extends Lattice {
   def lub(x: Element, y: Element): Element = x.union(y)
 }
 
+/**
+ * The lift lattice for `sublattice`.
+ * Supports implicit lifting and unlifting.
+ */
+class LiftLattice[+L <: Lattice](val sublattice: L) extends Lattice {
+
+  type Element = Lifted
+
+  sealed trait Lifted
+
+  case object Bottom extends Lifted {
+    override def toString = "LiftBot"
+  }
+
+  case class Lift(n: sublattice.Element) extends Lifted
+
+  val bottom: Element = Bottom
+
+  def lub(x: Element, y: Element): Element =
+    (x, y) match {
+      case (Bottom, t) => t
+      case (t, Bottom) => 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.
+   */
+  implicit def lift(x: sublattice.Element): Element = 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.
+   */
+  implicit def unlift(x: Element): sublattice.Element = x match {
+    case Lift(s) => s
+    case Bottom => throw new IllegalArgumentException("Cannot unlift bottom")
+  }
+}
+
 /** The flat lattice made of element of `X`. Top is greater than every other element, and Bottom is less than every
   * other element. No additional ordering is defined.
   */

src/main/scala/analysis/solvers/FixPointSolver.scala

@@ -49,6 +49,28 @@ trait MapLatticeSolver[N] extends LatticeSolver with Dependencies[N]:
     val states = indep(n, intra).map(o(_))
     states.foldLeft(lattice.sublattice.bottom)((acc, pred) => lattice.sublattice.lub(acc, pred))
 
+/**
+ * Base trait for solvers for map lattices with lifted co-domains.
+ * @tparam N type of the elements in the map domain.
+ */
+trait MapLiftLatticeSolver[N] extends MapLatticeSolver[N] with Dependencies[N] {
+
+  val lattice: MapLattice[N, LiftLattice[Lattice]]
+
+  /**
+   * The transfer function for the sub-sub-lattice.
+   */
+  def transferUnlifted(n: N, s: lattice.sublattice.sublattice.Element): lattice.sublattice.sublattice.Element
+
+  def transfer(n: N, s: lattice.sublattice.Element): lattice.sublattice.Element = {
+    import lattice.sublattice._
+    s match {
+      case Bottom => Bottom // unreachable as input implied unreachable at output
+      case Lift(a) => lift(transferUnlifted(n, a))
+    }
+  }
+}
+
 /** An abstract worklist algorithm.
   *
   * @tparam N

src/main/scala/analysis/solvers/MonotonicSolver.scala

@@ -13,7 +13,7 @@ import scala.collection.mutable
   * TODO: investigate how to visit all reachable nodes at least once, then remove loopEscape. TODO: in longer term, add
   * a worklist to avoid processing nodes twice.
   */
-trait SimpleMonotonicSolver[N] extends MapLatticeSolver[N] with ListSetWorklist[N] with Dependencies[N]:
+trait SimpleMonotonicSolver[N] extends MapLiftLatticeSolver[N] with ListSetWorklist[N] with Dependencies[N]:
   /** The current lattice element.
     */
   var x: lattice.Element = _