From d2b6ce1108a06f56621f3fa91ac0fe30806af7ad Mon Sep 17 00:00:00 2001
From: yousifpatti <yousifpatti@gmail.com>
Date: Tue, 17 Oct 2023 17:21:40 +1000
Subject: [PATCH 01/29] Adding lifted lattice solver

---
 src/main/scala/analysis/Analysis.scala        | 60 ++++++++++++++++---
 src/main/scala/analysis/Cfg.scala             |  7 +++
 src/main/scala/analysis/Lattice.scala         | 46 +++++++++++++-
 .../analysis/solvers/FixPointSolver.scala     | 22 +++++++
 .../analysis/solvers/MonotonicSolver.scala    |  2 +-
 5 files changed, 127 insertions(+), 10 deletions(-)

diff --git a/src/main/scala/analysis/Analysis.scala b/src/main/scala/analysis/Analysis.scala
index 621689b93..f46505d71 100644
--- a/src/main/scala/analysis/Analysis.scala
+++ b/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
 
diff --git a/src/main/scala/analysis/Cfg.scala b/src/main/scala/analysis/Cfg.scala
index f56ec239a..14d1cac20 100644
--- a/src/main/scala/analysis/Cfg.scala
+++ b/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]())
diff --git a/src/main/scala/analysis/Lattice.scala b/src/main/scala/analysis/Lattice.scala
index ad2182f70..3d0d7cc7e 100644
--- a/src/main/scala/analysis/Lattice.scala
+++ b/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.
   */
diff --git a/src/main/scala/analysis/solvers/FixPointSolver.scala b/src/main/scala/analysis/solvers/FixPointSolver.scala
index 064a3c619..ff5f844f5 100644
--- a/src/main/scala/analysis/solvers/FixPointSolver.scala
+++ b/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
diff --git a/src/main/scala/analysis/solvers/MonotonicSolver.scala b/src/main/scala/analysis/solvers/MonotonicSolver.scala
index 1c8f5aaeb..7f19a71b8 100644
--- a/src/main/scala/analysis/solvers/MonotonicSolver.scala
+++ b/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 = _

From 63d59091d01638f80aa8ab48269ae2a38a2cbb4d Mon Sep 17 00:00:00 2001
From: yousifpatti <yousifpatti@gmail.com>
Date: Tue, 24 Oct 2023 17:18:22 +1000
Subject: [PATCH 02/29] Lifted works but needs unlifting results

---
 src/main/scala/analysis/Analysis.scala        | 106 +++++++++++-------
 src/main/scala/analysis/Lattice.scala         |   4 +-
 src/main/scala/analysis/VSA.scala             |   2 +-
 .../analysis/solvers/FixPointSolver.scala     |  19 ++++
 src/main/scala/util/RunUtils.scala            |  23 ++--
 5 files changed, 101 insertions(+), 53 deletions(-)

diff --git a/src/main/scala/analysis/Analysis.scala b/src/main/scala/analysis/Analysis.scala
index f46505d71..2cd8f3c15 100644
--- a/src/main/scala/analysis/Analysis.scala
+++ b/src/main/scala/analysis/Analysis.scala
@@ -247,13 +247,11 @@ trait MemoryRegionAnalysisMisc:
   val subroutines: Map[BigInt, String]
   val constantProp: Map[CfgNode, Map[Variable, ConstantPropagationLattice.Element]]
 
-  /** The lattice of abstract values.
-    */
-  val powersetLattice: PowersetLattice[MemoryRegion]
+  val regionLattice: PowersetLattice[MemoryRegion] = PowersetLattice[MemoryRegion]
 
   /** The lattice of abstract states.
     */
-  val stateLattice: MapLattice[CfgNode, PowersetLattice[MemoryRegion]] = MapLattice(powersetLattice)
+  val stateLattice: MapLattice[CfgNode, regionLattice.type] = MapLattice(regionLattice)
 
   val domain: Set[CfgNode] = cfg.nodes.toSet
 
@@ -267,7 +265,8 @@ trait MemoryRegionAnalysisMisc:
 
   /** Default implementation of eval.
     */
-  def eval(exp: Expr, env: stateLattice.sublattice.Element, n: CfgNode): stateLattice.sublattice.Element = {
+  def eval(exp: Expr, env: stateLattice.Element, n: CfgNode): regionLattice.Element = {
+    import regionLattice._
     Logger.debug(s"evaluating $exp")
     Logger.debug(s"env: $env")
     Logger.debug(s"n: $n")
@@ -279,7 +278,7 @@ trait MemoryRegionAnalysisMisc:
         } else {
           val evaluation: Expr = evaluateExpression(binOp, n, constantProp(n))
           if (evaluation.equals(binOp)) {
-            return env
+            return Set()
           }
           eval(evaluation, env, n)
         }
@@ -306,9 +305,9 @@ trait MemoryRegionAnalysisMisc:
       case variable: Variable =>
         variable match {
           case _: LocalVar =>
-            return env
+            return Set()
           case reg: Register if reg == stackPointer =>
-            return env
+            return Set()
           case _ =>
         }
 
@@ -316,7 +315,7 @@ trait MemoryRegionAnalysisMisc:
         evaluation match
           case bitVecLiteral: BitVecLiteral =>
             eval(bitVecLiteral, env, n)
-          case _ => env // we cannot evaluate this to a concrete value, we need VSA for this
+          case _ => Set() // 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")
@@ -325,16 +324,14 @@ trait MemoryRegionAnalysisMisc:
 
   /** Transfer function for state lattice elements.
     */
-  def localTransfer(n: CfgNode, s: stateLattice.sublattice.Element): stateLattice.sublattice.Element =
+  def localTransfer(n: CfgNode, s: stateLattice.Element): stateLattice.Element =
     n match {
       case cmd: CfgCommandNode =>
         cmd.data match {
           case directCall: DirectCall =>
             if (directCall.target.name == "malloc") {
-              return stateLattice.sublattice.lub(
-                s,
-                Set(HeapRegion(getNextMallocCount(), evaluateExpression(mallocVariable, n, constantProp(n)), None))
-              )
+              return s ++ Set((n, Set(HeapRegion(getNextMallocCount(), evaluateExpression(mallocVariable, n, constantProp(n)), None))))
+
             }
             s
           case memAssign: MemoryAssign =>
@@ -365,7 +362,7 @@ trait MemoryRegionAnalysisMisc:
               case _ =>
             })
             */
-            stateLattice.sublattice.lub(s, result)
+            s ++ Set((n, result))
           case localAssign: LocalAssign =>
             var m = s
             unwrapExpr(localAssign.rhs).foreach {
@@ -381,7 +378,7 @@ trait MemoryRegionAnalysisMisc:
                   case _ =>
                 })
                 */
-                m = stateLattice.sublattice.lub(m, result)
+                m ++ Set((n, result))
               case _ => m
             }
             m
@@ -403,18 +400,27 @@ abstract class MemoryRegionAnalysis(
 
   /** Transfer function for state lattice elements. (Same as `localTransfer` for simple value analysis.)
     */
-  def transfer(n: CfgNode, s: stateLattice.sublattice.Element): stateLattice.sublattice.Element = localTransfer(n, s)
+  def transfer(n: CfgNode, s: stateLattice.Element): stateLattice.Element = localTransfer(n, s)
+
+
+trait IntraprocMemoryRegionAnalysisMisc[N] extends MemoryRegionAnalysisMisc {
+  val liftedstatelattice: LiftLattice[stateLattice.type]
+  val cfg: ProgramCfg
+  val lattice: MapLattice[N, liftedstatelattice.type]
+}
 
 /**
- * Base class for memory region analysis with lifted lattice, where the extra bottom element represents "unreachable".
+ * Base class for value 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)
+  val cfg: P,
+  val globals: Map[BigInt, String],
+  val globalOffsets: Map[BigInt, BigInt],
+  val subroutines: Map[BigInt, String],
+  val constantProp: Map[CfgNode, Map[Variable, ConstantPropagationLattice.Element]]
+
+  , stateAfterNode: Boolean)
+  extends FlowSensitiveAnalysis(stateAfterNode)
     with MapLatticeSolver[CfgNode]
     with MemoryRegionAnalysisMisc {
 
@@ -428,7 +434,7 @@ abstract class LiftedMemoryRegionAnalysis[P <: ProgramCfg](
    */
   val lattice: MapLattice[CfgNode, liftedstatelattice.type] = new MapLattice(liftedstatelattice)
 
-  val domain: Set[CfgNode] = cfg.nodes.toSet
+  override val domain: Set[CfgNode] = cfg.nodes.toSet
 
   /**
    * The worklist is initialized with all function entry nodes.
@@ -444,21 +450,44 @@ abstract class LiftedMemoryRegionAnalysis[P <: ProgramCfg](
       // 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)
+      case _ => super.funsub(n, x, intra = true)
     }
   }
 }
 
-abstract class IntraprocMemoryRegionAnalysisWorklistSolver[L <: PowersetLattice[MemoryRegion]](
-    cfg: ProgramCfg,
-    globals: Map[BigInt, String],
-    globalOffsets: Map[BigInt, BigInt],
-    subroutines: Map[BigInt, String],
-    constantProp: Map[CfgNode, Map[Variable, ConstantPropagationLattice.Element]],
-    val powersetLattice: L
-) extends LiftedMemoryRegionAnalysis(cfg, globals, globalOffsets, subroutines, constantProp)
-    with SimpleMonotonicSolver[CfgNode]
-    with ForwardDependencies
+/**
+ * Functionality for basic analyses with lifted state lattice.
+ */
+trait LiftedMemoryRegionAnalysisMisc extends MemoryRegionAnalysisMisc {
+
+  /**
+   * Transfer function for state lattice elements.
+   * (Same as `localTransfer` for basic analyses with lifted state lattice.)
+   */
+  def transferUnlifted(n: CfgNode, s: stateLattice.Element): stateLattice.Element = localTransfer(n, s)
+}
+
+/**
+ * Intraprocedural value analysis that uses [[tip.solvers.WorklistFixpointSolverWithReachability]],
+ * with all function entries as start nodes.
+ */
+abstract class IntraprocValueAnalysisWorklistSolverWithReachability[L](
+  cfg: ProgramCfg,
+  globals: Map[BigInt, String],
+  globalOffsets: Map[BigInt, BigInt],
+  subroutines: Map[BigInt, String],
+  constantProp: Map[CfgNode, Map[Variable, ConstantPropagationLattice.Element]]
+  )
+  extends LiftedMemoryRegionAnalysis(
+    cfg,
+    globals,
+    globalOffsets,
+    subroutines,
+    constantProp,
+    true)
+  with LiftedMemoryRegionAnalysisMisc
+  with WorklistFixpointSolverWithReachability[CfgNode]
+  with ForwardDependencies
 
 object MemoryRegionAnalysis:
 
@@ -468,11 +497,10 @@ object MemoryRegionAnalysis:
       globalOffsets: Map[BigInt, BigInt],
       subroutines: Map[BigInt, String],
       constantProp: Map[CfgNode, Map[Variable, ConstantPropagationLattice.Element]]
-  ) extends IntraprocMemoryRegionAnalysisWorklistSolver(
+  ) extends IntraprocValueAnalysisWorklistSolverWithReachability(
         cfg,
         globals,
         globalOffsets,
         subroutines,
-        constantProp,
-        PowersetLattice[MemoryRegion]
+        constantProp
       )
diff --git a/src/main/scala/analysis/Lattice.scala b/src/main/scala/analysis/Lattice.scala
index 3d0d7cc7e..7a6dafce8 100644
--- a/src/main/scala/analysis/Lattice.scala
+++ b/src/main/scala/analysis/Lattice.scala
@@ -110,14 +110,14 @@ class LiftLattice[+L <: Lattice](val sublattice: L) extends Lattice {
    * 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)
+  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 {
+  def unlift(x: Element): sublattice.Element = x match {
     case Lift(s) => s
     case Bottom => throw new IllegalArgumentException("Cannot unlift bottom")
   }
diff --git a/src/main/scala/analysis/VSA.scala b/src/main/scala/analysis/VSA.scala
index dfae2a804..14b7919a4 100644
--- a/src/main/scala/analysis/VSA.scala
+++ b/src/main/scala/analysis/VSA.scala
@@ -196,7 +196,7 @@ abstract class IntraprocValueSetAnalysisWorklistSolver[L <: VSALatticeElem](
     constantProp: Map[CfgNode, Map[Variable, ConstantPropagationLattice.Element]],
     val powersetLattice: L
 ) extends ValueSetAnalysis(cfg, globals, externalFunctions, globalOffsets, subroutines, mmm, constantProp)
-    with SimpleMonotonicSolver[CfgNode]
+    with SimpleWorklistFixpointSolver[CfgNode]
     with ForwardDependencies
 
 object ValueSetAnalysis:
diff --git a/src/main/scala/analysis/solvers/FixPointSolver.scala b/src/main/scala/analysis/solvers/FixPointSolver.scala
index ff5f844f5..969f149f9 100644
--- a/src/main/scala/analysis/solvers/FixPointSolver.scala
+++ b/src/main/scala/analysis/solvers/FixPointSolver.scala
@@ -159,6 +159,25 @@ trait SimpleWorklistFixpointSolver[N] extends WorklistFixpointSolver[N]:
     run(domain, intra)
     x
 
+/**
+ * The worklist-based fixpoint solver with reachability.
+ *
+ * This solver works for map lattices with lifted co-domains, where the extra bottom element typically represents "unreachable".
+ */
+trait WorklistFixpointSolverWithReachability[N] extends WorklistFixpointSolver[N] with MapLiftLatticeSolver[N] {
+
+  /**
+   * The start locations, used as the initial contents of the worklist.
+   */
+  val first: Set[N]
+
+  def analyze(intra: Boolean): lattice.Element = {
+    x = lattice.bottom
+    run(first, intra)
+    x
+  }
+}
+
 /** A pushDown worklist-based fixpoint solvers. Pushes the results of the analysis one node down. This is used to have
   * the results of the pred node in the current node. ie. NODE 1: R0 = 69551bv64 RESULT LATTICE = {} NODE 2: R0 =
   * MemLoad[R0 + 54bv64] RESULT LATTICE = {R0 = 69551bv64} NODE 3: R1 = 0bv64 RESULT LATTICE = {R0 = TOP} ...
diff --git a/src/main/scala/util/RunUtils.scala b/src/main/scala/util/RunUtils.scala
index d49363889..82fb5cc6c 100644
--- a/src/main/scala/util/RunUtils.scala
+++ b/src/main/scala/util/RunUtils.scala
@@ -5,19 +5,18 @@ import scala.collection.mutable.ArrayBuffer
 import scala.collection.mutable.Set as MutableSet
 import java.io.{File, PrintWriter}
 import java.io.{BufferedWriter, FileWriter, IOException}
-import scala.jdk.CollectionConverters._
-import analysis.solvers._
-
-import analysis._
+import scala.jdk.CollectionConverters.*
+import analysis.solvers.*
+import analysis.*
 import cfg_visualiser.{OtherOutput, Output, OutputKindE}
-import bap._
-import ir._
-import boogie._
-import specification._
-import Parsers._
+import bap.*
+import ir.*
+import boogie.*
+import specification.*
+import Parsers.*
 import org.antlr.v4.runtime.tree.ParseTreeWalker
 import org.antlr.v4.runtime.{CharStreams, CommonTokenStream}
-import translating._
+import translating.*
 import util.Logger
 
 object RunUtils {
@@ -152,13 +151,15 @@ object RunUtils {
 
     Logger.info("[!] Running MRA")
     val mraSolver = MemoryRegionAnalysis.WorklistSolver(cfg, globalAddresses, globalOffsets, mergedSubroutines, constPropResult)
-    val mraResult: Map[CfgNode, Set[MemoryRegion]] = mraSolver.analyze(true)
+    val mraResult: Map[CfgNode, Set[MemoryRegion]] = mraSolver.analyze(true).asInstanceOf[Map[CfgNode, Set[MemoryRegion]]]
     memoryRegionAnalysisResults = mraResult
     Output.output(
       OtherOutput(OutputKindE.cfg),
       cfg.toDot(Output.labeler(mraResult, mraSolver.stateAfterNode), Output.dotIder),
       "mra"
     )
+    println(mraResult.keys)
+    println(mraResult.values)
 
     Logger.info("[!] Running MMM")
     val mmm = MemoryModelMap()

From 3f8fd3a85e8758accae6b5b239289466d60d6538 Mon Sep 17 00:00:00 2001
From: yousifpatti <yousifpatti@gmail.com>
Date: Tue, 31 Oct 2023 14:39:47 +1000
Subject: [PATCH 03/29] Added unlifted analyze

---
 .../scala/analysis/solvers/FixPointSolver.scala   | 15 +++++++++++++++
 src/main/scala/util/RunUtils.scala                |  5 ++++-
 2 files changed, 19 insertions(+), 1 deletion(-)

diff --git a/src/main/scala/analysis/solvers/FixPointSolver.scala b/src/main/scala/analysis/solvers/FixPointSolver.scala
index 969f149f9..835badc4a 100644
--- a/src/main/scala/analysis/solvers/FixPointSolver.scala
+++ b/src/main/scala/analysis/solvers/FixPointSolver.scala
@@ -176,6 +176,21 @@ trait WorklistFixpointSolverWithReachability[N] extends WorklistFixpointSolver[N
     run(first, intra)
     x
   }
+
+  /**
+   * The transfer function for the sub-sub-lattice. Unlifts the resulting MapLattice[N, LiftLattice[Lattice.sublattice]]
+   * to MapLattice[N, Lattice.sublattice.sublattice].
+   *
+   * @param intra
+   * @return the sub-sub-lattice
+   */
+  def unliftedAnalyze(intra: Boolean): lattice.sublattice.sublattice.Element = {
+    val res: lattice.Element = analyze(intra)
+    // Convert liftedResult to unlifted
+    res.map {
+      case (key, value) => (key, lattice.sublattice.unlift(value))
+    }.asInstanceOf[lattice.sublattice.sublattice.Element]
+  }
 }
 
 /** A pushDown worklist-based fixpoint solvers. Pushes the results of the analysis one node down. This is used to have
diff --git a/src/main/scala/util/RunUtils.scala b/src/main/scala/util/RunUtils.scala
index c5c9e6980..9e9e7a283 100644
--- a/src/main/scala/util/RunUtils.scala
+++ b/src/main/scala/util/RunUtils.scala
@@ -153,13 +153,16 @@ object RunUtils {
 
     Logger.info("[!] Running MRA")
     val mraSolver = MemoryRegionAnalysis.WorklistSolver(cfg, globalAddresses, globalOffsets, mergedSubroutines, constPropResult)
-    val mraResult: Map[CfgNode, Set[MemoryRegion]] = mraSolver.analyze(true).asInstanceOf[Map[CfgNode, Set[MemoryRegion]]]
+    val mraResult: Map[CfgNode, Set[MemoryRegion]] = mraSolver.unliftedAnalyze(true).asInstanceOf[Map[CfgNode, Map[CfgNode, Set[MemoryRegion]]]].map {
+      case (k, v) => k -> v.values.flatten.toSet
+    }
     memoryRegionAnalysisResults = mraResult
     Output.output(
       OtherOutput(OutputKindE.cfg),
       cfg.toDot(Output.labeler(mraResult, mraSolver.stateAfterNode), Output.dotIder),
       "mra"
     )
+    println(mraResult)
     println(mraResult.keys)
     println(mraResult.values)
 

From f8dc3e63bb647933249b5faa4abc6019a633c6f9 Mon Sep 17 00:00:00 2001
From: yousifpatti <yousifpatti@gmail.com>
Date: Tue, 31 Oct 2023 17:16:16 +1000
Subject: [PATCH 04/29] started lifted VSA but some issues marked with TODO

---
 src/main/scala/analysis/Analysis.scala    |  23 +++--
 src/main/scala/analysis/UtilMethods.scala |   1 +
 src/main/scala/analysis/VSA.scala         | 112 +++++++++++++++++-----
 src/main/scala/util/RunUtils.scala        |   5 +-
 4 files changed, 106 insertions(+), 35 deletions(-)

diff --git a/src/main/scala/analysis/Analysis.scala b/src/main/scala/analysis/Analysis.scala
index 2cd8f3c15..5dadbf4b4 100644
--- a/src/main/scala/analysis/Analysis.scala
+++ b/src/main/scala/analysis/Analysis.scala
@@ -364,7 +364,7 @@ trait MemoryRegionAnalysisMisc:
             */
             s ++ Set((n, result))
           case localAssign: LocalAssign =>
-            var m = s
+            val m = s
             unwrapExpr(localAssign.rhs).foreach {
               case memoryLoad: MemoryLoad =>
                 val result = eval(memoryLoad.index, s, n)
@@ -417,9 +417,8 @@ abstract class LiftedMemoryRegionAnalysis[P <: ProgramCfg](
   val globals: Map[BigInt, String],
   val globalOffsets: Map[BigInt, BigInt],
   val subroutines: Map[BigInt, String],
-  val constantProp: Map[CfgNode, Map[Variable, ConstantPropagationLattice.Element]]
-
-  , stateAfterNode: Boolean)
+  val constantProp: Map[CfgNode, Map[Variable, ConstantPropagationLattice.Element]],
+  stateAfterNode: Boolean)
   extends FlowSensitiveAnalysis(stateAfterNode)
     with MapLatticeSolver[CfgNode]
     with MemoryRegionAnalysisMisc {
@@ -471,13 +470,13 @@ trait LiftedMemoryRegionAnalysisMisc extends MemoryRegionAnalysisMisc {
  * Intraprocedural value analysis that uses [[tip.solvers.WorklistFixpointSolverWithReachability]],
  * with all function entries as start nodes.
  */
-abstract class IntraprocValueAnalysisWorklistSolverWithReachability[L](
-  cfg: ProgramCfg,
-  globals: Map[BigInt, String],
-  globalOffsets: Map[BigInt, BigInt],
-  subroutines: Map[BigInt, String],
-  constantProp: Map[CfgNode, Map[Variable, ConstantPropagationLattice.Element]]
-  )
+abstract class IntraprocMemoryRegionAnalysisWorklistSolverWithReachability[L](
+    cfg: ProgramCfg,
+    globals: Map[BigInt, String],
+    globalOffsets: Map[BigInt, BigInt],
+    subroutines: Map[BigInt, String],
+    constantProp: Map[CfgNode, Map[Variable, ConstantPropagationLattice.Element]]
+    )
   extends LiftedMemoryRegionAnalysis(
     cfg,
     globals,
@@ -497,7 +496,7 @@ object MemoryRegionAnalysis:
       globalOffsets: Map[BigInt, BigInt],
       subroutines: Map[BigInt, String],
       constantProp: Map[CfgNode, Map[Variable, ConstantPropagationLattice.Element]]
-  ) extends IntraprocValueAnalysisWorklistSolverWithReachability(
+  ) extends IntraprocMemoryRegionAnalysisWorklistSolverWithReachability(
         cfg,
         globals,
         globalOffsets,
diff --git a/src/main/scala/analysis/UtilMethods.scala b/src/main/scala/analysis/UtilMethods.scala
index 3b76466c0..7ac6283d8 100644
--- a/src/main/scala/analysis/UtilMethods.scala
+++ b/src/main/scala/analysis/UtilMethods.scala
@@ -25,6 +25,7 @@ def evaluateExpression(exp: Expr, n: CfgNode, constantPropResult: Map[Variable,
             case BVSUB => BitVectorEval.smt_bvsub(l, r)
             case BVASHR => BitVectorEval.smt_bvashr(l, r)
             case BVCOMP => BitVectorEval.smt_bvcomp(l, r)
+            case BVCONCAT => BitVectorEval.smt_concat(l, r)
             case _ => throw new RuntimeException("Binary operation support not implemented: " + binOp.op)
           }
         case _ => exp
diff --git a/src/main/scala/analysis/VSA.scala b/src/main/scala/analysis/VSA.scala
index 14b7919a4..2c0bb5430 100644
--- a/src/main/scala/analysis/VSA.scala
+++ b/src/main/scala/analysis/VSA.scala
@@ -27,7 +27,7 @@ case class LiteralValue(expr: BitVecLiteral) extends Value {
 
 type VSALatticeElem = MapLattice[Variable | MemoryRegion, PowersetLattice[Value]]
 
-trait MemoryRegionValueSetAnalysis:
+trait ValueSetAnalysisMisc:
 
   val cfg: ProgramCfg
   val globals: Map[BigInt, String]
@@ -43,7 +43,7 @@ trait MemoryRegionValueSetAnalysis:
 
   /** The lattice of abstract states.
     */
-  val lattice: MapLattice[CfgNode, VSALatticeElem] = MapLattice(powersetLattice)
+  val stateLattice: MapLattice[CfgNode, VSALatticeElem] = MapLattice(powersetLattice)
 
   val domain: Set[CfgNode] = cfg.nodes.toSet
 
@@ -100,7 +100,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: stateLattice.Element, n: CfgNode): stateLattice.Element = {
     Logger.debug(s"eval: $cmd")
     Logger.debug(s"state: $s")
     Logger.debug(s"node: $n")
@@ -114,17 +114,17 @@ trait MemoryRegionValueSetAnalysis:
                 // this is an exception to the rule and only applies to data regions
                 evaluateExpression(memoryLoad.index, n, constantProp(n)) match
                   case bitVecLiteral: BitVecLiteral =>
-                    val m = s + (r -> Set(getValueType(bitVecLiteral)))
-                    m + (localAssign.lhs -> m(r))
+                    s//TODO: val m = s + Set((n, Map(r -> Set(getValueType(bitVecLiteral)))))
+                    //m + (n, localAssign.lhs -> m(r))
                   case _ =>
-                    s + (localAssign.lhs -> s(r))
+                    s//TODO: s + (localAssign.lhs -> s(r))
               case None =>
                 Logger.warn("could not find region for " + localAssign)
                 s
           case e: Expr => {
             val evaled = evaluateExpression(e, n, constantProp(n))
             evaled match
-              case bv: BitVecLiteral => s + (localAssign.lhs -> Set(getValueType(bv)))
+              case bv: BitVecLiteral => s//TODO: s + (localAssign.lhs -> Set(getValueType(bv)))
               case _ =>
                 Logger.warn("could not evaluate expression" + e)
                 s
@@ -137,9 +137,9 @@ trait MemoryRegionValueSetAnalysis:
               case Some(r: MemoryRegion) =>
                 evaluateExpression(memAssign.rhs.value, n, constantProp(n)) match
                   case bitVecLiteral: BitVecLiteral =>
-                    return s + (r -> Set(getValueType(bitVecLiteral)))
+                    return s//TODO: return s + (r -> Set(getValueType(bitVecLiteral)))
                   case variable: Variable => // constant prop returned BOT OR TOP. Merge regions because RHS could be a memory loaded address
-                    return s + (r -> s(variable))
+                    return s//TODO: return s + (r -> s(variable))
 
                   case _ => Logger.warn("Too Complex or Wrapped i.e. Extract(Variable)") // do nothing
                 s
@@ -154,7 +154,7 @@ trait MemoryRegionValueSetAnalysis:
 
   /** Transfer function for state lattice elements.
     */
-  def localTransfer(n: CfgNode, s: lattice.sublattice.Element): lattice.sublattice.Element =
+  def localTransfer(n: CfgNode, s: stateLattice.Element): stateLattice.Element =
     n match {
       case entry: CfgFunctionEntryNode =>
         mmm.pushContext(entry.data.name)
@@ -167,25 +167,85 @@ trait MemoryRegionValueSetAnalysis:
       case _ => s // ignore other kinds of nodes
     }
 
-/** Base class for memory region analysis (non-lifted) lattice.
-  */
-abstract class ValueSetAnalysis(
-    val cfg: ProgramCfg,
+///** 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 {
+//
+//  /** 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)
+//
+//}
+
+/**
+ * Base class for value analysis with lifted lattice, where the extra bottom element represents "unreachable".
+ */
+abstract class LiftedValueSetAnalysis[P <: ProgramCfg] (
+    val cfg: P,
     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 {
+    val constantProp: Map[CfgNode, Map[Variable, ConstantPropagationLattice.Element]],
+    stateAfterNode: Boolean)
+  extends FlowSensitiveAnalysis(stateAfterNode)
+    with MapLatticeSolver[CfgNode]
+    with ValueSetAnalysisMisc {
 
-  /** 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)
+  /**
+   * 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)
+
+  override 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 = true)
+    }
+  }
+}
+
+/**
+ * Functionality for basic analyses with lifted state lattice.
+ */
+trait LiftedValueSetAnalysisMisc extends ValueSetAnalysisMisc {
 
+  /**
+   * Transfer function for state lattice elements.
+   * (Same as `localTransfer` for basic analyses with lifted state lattice.)
+   */
+  def transferUnlifted(n: CfgNode, s: stateLattice.Element): stateLattice.Element = localTransfer(n, s)
 }
 
+
 abstract class IntraprocValueSetAnalysisWorklistSolver[L <: VSALatticeElem](
     cfg: ProgramCfg,
     globals: Map[BigInt, String],
@@ -195,8 +255,16 @@ abstract class IntraprocValueSetAnalysisWorklistSolver[L <: VSALatticeElem](
     mmm: MemoryModelMap,
     constantProp: Map[CfgNode, Map[Variable, ConstantPropagationLattice.Element]],
     val powersetLattice: L
-) extends ValueSetAnalysis(cfg, globals, externalFunctions, globalOffsets, subroutines, mmm, constantProp)
-    with SimpleWorklistFixpointSolver[CfgNode]
+) extends LiftedValueSetAnalysis(
+    cfg,
+    globals,
+    externalFunctions,
+    globalOffsets, subroutines,
+    mmm,
+    constantProp,
+    true)
+    with LiftedValueSetAnalysisMisc
+    with WorklistFixpointSolverWithReachability[CfgNode]
     with ForwardDependencies
 
 object ValueSetAnalysis:
diff --git a/src/main/scala/util/RunUtils.scala b/src/main/scala/util/RunUtils.scala
index 9e9e7a283..abecc1cbb 100644
--- a/src/main/scala/util/RunUtils.scala
+++ b/src/main/scala/util/RunUtils.scala
@@ -173,7 +173,10 @@ object RunUtils {
     Logger.info("[!] Running VSA")
     val vsaSolver =
       ValueSetAnalysis.WorklistSolver(cfg, globalAddresses, externalAddresses, globalOffsets, subroutines, mmm, constPropResult)
-    val vsaResult: Map[CfgNode, Map[Variable | MemoryRegion, Set[Value]]]  = vsaSolver.analyze(false)
+      // TODO: replace ? with the right type
+    val vsaResult: Map[CfgNode, Map[Variable | MemoryRegion, Set[Value]]]  = vsaSolver.unliftedAnalyze(true).asInstanceOf[Map[CfgNode, ?]]].map {
+      case (k, v) => k -> v.values.flatten.toSet
+    }
     Output.output(
       OtherOutput(OutputKindE.cfg),
       cfg.toDot(Output.labeler(vsaResult, vsaSolver.stateAfterNode), Output.dotIder),

From 7d06c0883608d1c35741265fb27c9fd7d9365c0d Mon Sep 17 00:00:00 2001
From: yousifpatti <yousifpatti@gmail.com>
Date: Tue, 7 Nov 2023 15:16:06 +1000
Subject: [PATCH 05/29] Lifted VSA

---
 src/main/scala/analysis/Analysis.scala |  2 +-
 src/main/scala/analysis/VSA.scala      | 21 +++++++++++----------
 src/main/scala/util/RunUtils.scala     |  8 +++-----
 3 files changed, 15 insertions(+), 16 deletions(-)

diff --git a/src/main/scala/analysis/Analysis.scala b/src/main/scala/analysis/Analysis.scala
index f568ab005..d05f0f399 100644
--- a/src/main/scala/analysis/Analysis.scala
+++ b/src/main/scala/analysis/Analysis.scala
@@ -321,7 +321,7 @@ trait MemoryRegionAnalysisMisc:
             if (directCall.target.name == "malloc") {
               evaluateExpression(mallocVariable, constantProp(n)) match {
                 case Some(b: BitVecLiteral) =>
-                  s ++ Set((s, Set(HeapRegion(nextMallocCount(), b))))
+                  s ++ Set((n, Set(HeapRegion(nextMallocCount(), b))))
                 case None => s
               }
             } else {
diff --git a/src/main/scala/analysis/VSA.scala b/src/main/scala/analysis/VSA.scala
index 73d789d44..89edc6d72 100644
--- a/src/main/scala/analysis/VSA.scala
+++ b/src/main/scala/analysis/VSA.scala
@@ -115,16 +115,17 @@ trait ValueSetAnalysisMisc:
                 // 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))
+                    val m = s + (n -> (s.getOrElse(n, Map.empty) + (r -> Set(getValueType(bitVecLiteral)))))
+                    m + (n -> (m.getOrElse(n, Map.empty) + (localAssign.lhs -> m(n)(r))))
                   case None =>
-                    s + (localAssign.lhs -> s(r))
+                    s + (n -> (s.getOrElse(n, Map.empty) + (localAssign.lhs -> s(n)(r))))
               case None =>
                 Logger.warn("could not find region for " + localAssign)
                 s
           case e: Expr =>
             evaluateExpression(e, constantProp(n)) match {
-              case Some(bv: BitVecLiteral) => s + (localAssign.lhs -> Set(getValueType(bv)))
+              case Some(bv: BitVecLiteral) =>
+                s + (n -> (s.getOrElse(n, Map.empty) + (localAssign.lhs -> Set(getValueType(bv)))))
               case None =>
                 Logger.warn("could not evaluate expression" + e)
                 s
@@ -138,7 +139,7 @@ trait ValueSetAnalysisMisc:
                 val storeValue = memAssign.rhs.value
                 evaluateExpression(storeValue, constantProp(n)) match
                   case Some(bitVecLiteral: BitVecLiteral) =>
-                    s + (r -> Set(getValueType(bitVecLiteral)))
+                    s + (n -> (s.getOrElse(n, Map.empty) + (r -> Set(getValueType(bitVecLiteral)))))
                     /*
                   // TODO constant prop returned BOT OR TOP. Merge regions because RHS could be a memory loaded address
                   case variable: Variable =>
@@ -147,7 +148,7 @@ trait ValueSetAnalysisMisc:
                   case None =>
                     storeValue.match {
                       case v: Variable =>
-                        s + (r -> s(v))
+                        s + (n -> (s.getOrElse(n, Map.empty) + (r -> s(n)(v))))
                       case _ =>
                         Logger.warn(s"Too Complex: $storeValue") // do nothing
                         s
@@ -218,7 +219,7 @@ abstract class LiftedValueSetAnalysis[P <: ProgramCfg] (
       // 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 = true)
+      case _ => super.funsub(n, x, intra = false)
     }
   }
 }
@@ -235,7 +236,7 @@ trait LiftedValueSetAnalysisMisc extends ValueSetAnalysisMisc {
   def transferUnlifted(n: CfgNode, s: stateLattice.Element): stateLattice.Element = localTransfer(n, s)
 }
 
-abstract class IntraprocValueSetAnalysisWorklistSolver[L <: VSALatticeElem](
+abstract class InterprocValueSetAnalysisWorklistSolver[L <: VSALatticeElem](
     cfg: ProgramCfg,
     globals: Map[BigInt, String],
     externalFunctions: Map[BigInt, String],
@@ -258,7 +259,7 @@ abstract class IntraprocValueSetAnalysisWorklistSolver[L <: VSALatticeElem](
 
 object ValueSetAnalysis:
 
-  /** Intraprocedural analysis that uses the worklist solver.
+  /** Interprocedural analysis that uses the worklist solver.
     */
   class WorklistSolver(
       cfg: ProgramCfg,
@@ -268,7 +269,7 @@ object ValueSetAnalysis:
       subroutines: Map[BigInt, String],
       mmm: MemoryModelMap,
       constantProp: Map[CfgNode, Map[Variable, ConstantPropagationLattice.Element]]
-  ) extends IntraprocValueSetAnalysisWorklistSolver(
+  ) extends InterprocValueSetAnalysisWorklistSolver(
         cfg,
         globals,
         externalFunctions,
diff --git a/src/main/scala/util/RunUtils.scala b/src/main/scala/util/RunUtils.scala
index a3ed41367..a30ca0775 100644
--- a/src/main/scala/util/RunUtils.scala
+++ b/src/main/scala/util/RunUtils.scala
@@ -167,11 +167,9 @@ object RunUtils {
     Logger.info("[!] Running VSA")
     val vsaSolver =
       ValueSetAnalysis.WorklistSolver(cfg, globalAddresses, externalAddresses, globalOffsets, subroutines, mmm, constPropResult)
-    // TODO: replace ? with the right type
-    val vsaResult: Map[CfgNode, Map[Variable | MemoryRegion, Set[Value]]] = vsaSolver.unliftedAnalyze(true).asInstanceOf[Map[CfgNode, ?]]
-    ].map {
-      case (k, v) => k -> v.values.flatten.toSet
-    }
+
+    val vsaResult: Map[CfgNode, Map[Variable | MemoryRegion, Set[Value]]] = vsaSolver.unliftedAnalyze(true).asInstanceOf[Map[CfgNode, Map[Variable | MemoryRegion, Set[Value]]]]
+
     config.analysisDotPath.foreach(s => writeToFile(cfg.toDot(Output.labeler(vsaResult, vsaSolver.stateAfterNode), Output.dotIder), s"${s}_vsa$iteration.dot"))
     config.analysisResultsPath.foreach(s => writeToFile(printAnalysisResults(cfg, vsaResult, iteration), s"${s}_vsa$iteration.txt"))
 

From 552d6374f3c878b3f99d4b5c6b0081585338e778 Mon Sep 17 00:00:00 2001
From: yousifpatti <yousifpatti@gmail.com>
Date: Tue, 14 Nov 2023 15:02:53 +1000
Subject: [PATCH 06/29] VSA lifted lattice

---
 src/main/scala/analysis/Lattice.scala                | 4 +++-
 src/main/scala/analysis/solvers/FixPointSolver.scala | 4 +---
 src/main/scala/util/RunUtils.scala                   | 6 ++----
 3 files changed, 6 insertions(+), 8 deletions(-)

diff --git a/src/main/scala/analysis/Lattice.scala b/src/main/scala/analysis/Lattice.scala
index 7a6dafce8..1fc3422ed 100644
--- a/src/main/scala/analysis/Lattice.scala
+++ b/src/main/scala/analysis/Lattice.scala
@@ -95,7 +95,9 @@ class LiftLattice[+L <: Lattice](val sublattice: L) extends Lattice {
     override def toString = "LiftBot"
   }
 
-  case class Lift(n: sublattice.Element) extends Lifted
+  case class Lift(n: sublattice.Element) extends Lifted {
+    override def toString = s"Lift($n)"
+  }
 
   val bottom: Element = Bottom
 
diff --git a/src/main/scala/analysis/solvers/FixPointSolver.scala b/src/main/scala/analysis/solvers/FixPointSolver.scala
index 4ef276892..d80cd9946 100644
--- a/src/main/scala/analysis/solvers/FixPointSolver.scala
+++ b/src/main/scala/analysis/solvers/FixPointSolver.scala
@@ -187,9 +187,7 @@ trait WorklistFixpointSolverWithReachability[N] extends WorklistFixpointSolver[N
   def unliftedAnalyze(intra: Boolean): lattice.sublattice.sublattice.Element = {
     val res: lattice.Element = analyze(intra)
     // Convert liftedResult to unlifted
-    res.map {
-      case (key, value) => (key, lattice.sublattice.unlift(value))
-    }.asInstanceOf[lattice.sublattice.sublattice.Element]
+    res.foldLeft(lattice.sublattice.sublattice.bottom)((acc, pred) => lattice.sublattice.sublattice.lub(acc, lattice.sublattice.unlift(pred._2)))
   }
 }
 
diff --git a/src/main/scala/util/RunUtils.scala b/src/main/scala/util/RunUtils.scala
index a30ca0775..c60023bf1 100644
--- a/src/main/scala/util/RunUtils.scala
+++ b/src/main/scala/util/RunUtils.scala
@@ -152,9 +152,7 @@ object RunUtils {
 
     Logger.info("[!] Running MRA")
     val mraSolver = MemoryRegionAnalysis.WorklistSolver(cfg, globalAddresses, globalOffsets, mergedSubroutines, constPropResult)
-    val mraResult: Map[CfgNode, Set[MemoryRegion]] = mraSolver.unliftedAnalyze(true).asInstanceOf[Map[CfgNode, Map[CfgNode, Set[MemoryRegion]]]].map {
-      case (k, v) => k -> v.values.flatten.toSet
-    }
+    val mraResult: Map[CfgNode, Set[MemoryRegion]] = mraSolver.unliftedAnalyze(true).asInstanceOf[Map[CfgNode, Set[MemoryRegion]]]
     memoryRegionAnalysisResults = mraResult
 
     config.analysisDotPath.foreach(s => writeToFile(cfg.toDot(Output.labeler(mraResult, mraSolver.stateAfterNode), Output.dotIder), s"${s}_mra$iteration.dot"))
@@ -168,7 +166,7 @@ object RunUtils {
     val vsaSolver =
       ValueSetAnalysis.WorklistSolver(cfg, globalAddresses, externalAddresses, globalOffsets, subroutines, mmm, constPropResult)
 
-    val vsaResult: Map[CfgNode, Map[Variable | MemoryRegion, Set[Value]]] = vsaSolver.unliftedAnalyze(true).asInstanceOf[Map[CfgNode, Map[Variable | MemoryRegion, Set[Value]]]]
+    val vsaResult: Map[CfgNode, Map[Variable | MemoryRegion, Set[Value]]] = vsaSolver.unliftedAnalyze(false).asInstanceOf[Map[CfgNode, Map[Variable | MemoryRegion, Set[Value]]]]
 
     config.analysisDotPath.foreach(s => writeToFile(cfg.toDot(Output.labeler(vsaResult, vsaSolver.stateAfterNode), Output.dotIder), s"${s}_vsa$iteration.dot"))
     config.analysisResultsPath.foreach(s => writeToFile(printAnalysisResults(cfg, vsaResult, iteration), s"${s}_vsa$iteration.txt"))

From e869ef01eb56645a1bbf7ce68842f96d78e84dd4 Mon Sep 17 00:00:00 2001
From: yousifpatti <yousifpatti@gmail.com>
Date: Thu, 16 Nov 2023 15:18:09 +1000
Subject: [PATCH 07/29] Fixing local transfer returns

---
 src/main/scala/analysis/Analysis.scala        | 23 +++++++-------
 src/main/scala/analysis/VSA.scala             | 30 +++++++++++--------
 .../analysis/solvers/FixPointSolver.scala     |  1 +
 3 files changed, 29 insertions(+), 25 deletions(-)

diff --git a/src/main/scala/analysis/Analysis.scala b/src/main/scala/analysis/Analysis.scala
index d05f0f399..2b56b6220 100644
--- a/src/main/scala/analysis/Analysis.scala
+++ b/src/main/scala/analysis/Analysis.scala
@@ -316,18 +316,21 @@ trait MemoryRegionAnalysisMisc:
   def localTransfer(n: CfgNode, s: stateLattice.Element): stateLattice.Element =
     n match {
       case cmd: CfgCommandNode =>
+        var m = s
         cmd.data match {
           case directCall: DirectCall =>
             if (directCall.target.name == "malloc") {
               evaluateExpression(mallocVariable, constantProp(n)) match {
                 case Some(b: BitVecLiteral) =>
-                  s ++ Set((n, Set(HeapRegion(nextMallocCount(), b))))
-                case None => s
+                  m = m ++ Set((n, Set(HeapRegion(nextMallocCount(), b))))
+                  m
+                case None => m
               }
             } else {
-              s
+              m
             }
           case memAssign: MemoryAssign =>
+            var m = s
             if (ignoreRegions.contains(memAssign.rhs.value)) {
               return s
             }
@@ -355,9 +358,10 @@ trait MemoryRegionAnalysisMisc:
               case _ =>
             })
             */
-            s ++ Set((n, result))
+            m = m ++ Set((n, result))
+            m
           case localAssign: LocalAssign =>
-            val m = s
+            var m = s
             unwrapExpr(localAssign.rhs).foreach {
               case memoryLoad: MemoryLoad =>
                 val result = eval(memoryLoad.index, s, cmd)
@@ -371,7 +375,7 @@ trait MemoryRegionAnalysisMisc:
                   case _ =>
                 })
                 */
-                m ++ Set((n, result))
+                m = m ++ Set((n, result))
               case _ => m
             }
             m
@@ -395,13 +399,6 @@ abstract class MemoryRegionAnalysis(
     */
   def transfer(n: CfgNode, s: stateLattice.Element): stateLattice.Element = localTransfer(n, s)
 
-
-trait IntraprocMemoryRegionAnalysisMisc[N] extends MemoryRegionAnalysisMisc {
-  val liftedstatelattice: LiftLattice[stateLattice.type]
-  val cfg: ProgramCfg
-  val lattice: MapLattice[N, liftedstatelattice.type]
-}
-
 /**
  * Base class for value analysis with lifted lattice, where the extra bottom element represents "unreachable".
  */
diff --git a/src/main/scala/analysis/VSA.scala b/src/main/scala/analysis/VSA.scala
index 89edc6d72..27fc427f2 100644
--- a/src/main/scala/analysis/VSA.scala
+++ b/src/main/scala/analysis/VSA.scala
@@ -106,6 +106,7 @@ trait ValueSetAnalysisMisc:
     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
@@ -115,20 +116,23 @@ trait ValueSetAnalysisMisc:
                 // 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 + (n -> (s.getOrElse(n, Map.empty) + (r -> Set(getValueType(bitVecLiteral)))))
-                    m + (n -> (m.getOrElse(n, Map.empty) + (localAssign.lhs -> m(n)(r))))
+                    m = m + (n -> (s.getOrElse(n, Map.empty) + (r -> Set(getValueType(bitVecLiteral)))))
+                    m = m + (n -> (m.getOrElse(n, Map.empty) + (localAssign.lhs -> m(n)(r))))
+                    m
                   case None =>
-                    s + (n -> (s.getOrElse(n, Map.empty) + (localAssign.lhs -> s(n)(r))))
+                    m = m + (n -> (m.getOrElse(n, Map.empty) + (localAssign.lhs -> m(n)(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 + (n -> (s.getOrElse(n, Map.empty) + (localAssign.lhs -> Set(getValueType(bv)))))
+                m = m + (n -> (m.getOrElse(n, Map.empty) + (localAssign.lhs -> Set(getValueType(bv)))))
+                m
               case None =>
                 Logger.warn("could not evaluate expression" + e)
-                s
+                m
             }
       case memAssign: MemoryAssign =>
         memAssign.rhs.index match
@@ -139,7 +143,8 @@ trait ValueSetAnalysisMisc:
                 val storeValue = memAssign.rhs.value
                 evaluateExpression(storeValue, constantProp(n)) match
                   case Some(bitVecLiteral: BitVecLiteral) =>
-                    s + (n -> (s.getOrElse(n, Map.empty) + (r -> Set(getValueType(bitVecLiteral)))))
+                    m = m + (n -> (m.getOrElse(n, Map.empty) + (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 =>
@@ -148,18 +153,19 @@ trait ValueSetAnalysisMisc:
                   case None =>
                     storeValue.match {
                       case v: Variable =>
-                        s + (n -> (s.getOrElse(n, Map.empty) + (r -> s(n)(v))))
+                        m = m + (n -> (m.getOrElse(n, Map.empty) + (r -> m(n)(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.
diff --git a/src/main/scala/analysis/solvers/FixPointSolver.scala b/src/main/scala/analysis/solvers/FixPointSolver.scala
index d80cd9946..1a8aca845 100644
--- a/src/main/scala/analysis/solvers/FixPointSolver.scala
+++ b/src/main/scala/analysis/solvers/FixPointSolver.scala
@@ -62,6 +62,7 @@ trait MapLiftLatticeSolver[N] extends MapLatticeSolver[N] with Dependencies[N] {
    */
   def transferUnlifted(n: N, s: lattice.sublattice.sublattice.Element): lattice.sublattice.sublattice.Element
 
+  @Override
   def transfer(n: N, s: lattice.sublattice.Element): lattice.sublattice.Element = {
     import lattice.sublattice._
     s match {

From cf9f077974de9e400e2ae63154287ebd9b993ba9 Mon Sep 17 00:00:00 2001
From: yousifpatti <yousifpatti@gmail.com>
Date: Tue, 21 Nov 2023 10:05:52 +1000
Subject: [PATCH 08/29] Minor format issue

---
 src/main/scala/analysis/solvers/FixPointSolver.scala | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/src/main/scala/analysis/solvers/FixPointSolver.scala b/src/main/scala/analysis/solvers/FixPointSolver.scala
index c78bd24ea..4ced829fe 100644
--- a/src/main/scala/analysis/solvers/FixPointSolver.scala
+++ b/src/main/scala/analysis/solvers/FixPointSolver.scala
@@ -63,8 +63,7 @@ trait MapLiftLatticeSolver[N] extends MapLatticeSolver[N] with Dependencies[N] {
    */
   def transferUnlifted(n: N, s: lattice.sublattice.sublattice.Element): lattice.sublattice.sublattice.Element
 
-  @Override
-  def transfer(n: N, s: lattice.sublattice.Element): lattice.sublattice.Element = {
+  override 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

From abe8f304dc4eb8159b83495b78b5903170d316b8 Mon Sep 17 00:00:00 2001
From: yousifpatti <yousifpatti@gmail.com>
Date: Tue, 21 Nov 2023 14:56:11 +1000
Subject: [PATCH 09/29] Fixed MRA join issue with liftedLattice

---
 src/main/scala/analysis/Analysis.scala        | 55 ++++---------------
 .../analysis/solvers/FixPointSolver.scala     |  6 +-
 2 files changed, 17 insertions(+), 44 deletions(-)

diff --git a/src/main/scala/analysis/Analysis.scala b/src/main/scala/analysis/Analysis.scala
index 2b56b6220..dab77a086 100644
--- a/src/main/scala/analysis/Analysis.scala
+++ b/src/main/scala/analysis/Analysis.scala
@@ -241,7 +241,7 @@ trait MemoryRegionAnalysisMisc:
 
   /** The lattice of abstract states.
     */
-  val stateLattice: MapLattice[CfgNode, regionLattice.type] = MapLattice(regionLattice)
+  val stateLattice: regionLattice.type = regionLattice
 
   val domain: Set[CfgNode] = cfg.nodes.toSet
 
@@ -322,7 +322,7 @@ trait MemoryRegionAnalysisMisc:
             if (directCall.target.name == "malloc") {
               evaluateExpression(mallocVariable, constantProp(n)) match {
                 case Some(b: BitVecLiteral) =>
-                  m = m ++ Set((n, Set(HeapRegion(nextMallocCount(), b))))
+                  m = m ++ Set(HeapRegion(nextMallocCount(), b))
                   m
                 case None => m
               }
@@ -335,47 +335,14 @@ trait MemoryRegionAnalysisMisc:
               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 _ =>
-            })
-            */
-            m = m ++ Set((n, result))
+            m = m ++ result
             m
           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 = m ++ Set((n, result))
+                m = m ++ result
               case _ => m
             }
             m
@@ -435,12 +402,14 @@ abstract class LiftedMemoryRegionAnalysis[P <: ProgramCfg](
    */
   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 = true)
-    }
+      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 _ =>
+          val joinedStates = indep(n, intra).map(x(_)).foldLeft(liftedstatelattice.bottom)((acc, pred) => liftedstatelattice.lub(acc, pred))
+          lift(localTransfer(n, unlift(joinedStates)))
+      }
   }
 }
 
diff --git a/src/main/scala/analysis/solvers/FixPointSolver.scala b/src/main/scala/analysis/solvers/FixPointSolver.scala
index 4ced829fe..3c09713e1 100644
--- a/src/main/scala/analysis/solvers/FixPointSolver.scala
+++ b/src/main/scala/analysis/solvers/FixPointSolver.scala
@@ -213,9 +213,13 @@ trait WorklistFixpointSolverWithReachability[N] extends WorklistFixpointSolver[N
    * @return the sub-sub-lattice
    */
   def unliftedAnalyze(intra: Boolean): lattice.sublattice.sublattice.Element = {
+    import lattice.sublattice._
     val res: lattice.Element = analyze(intra)
     // Convert liftedResult to unlifted
-    res.foldLeft(lattice.sublattice.sublattice.bottom)((acc, pred) => lattice.sublattice.sublattice.lub(acc, lattice.sublattice.unlift(pred._2)))
+    res.map((n, lift) => (n, lift match {
+      case Bottom => lattice.sublattice.sublattice.bottom
+      case Lift(a) => a
+    })).asInstanceOf[lattice.sublattice.sublattice.Element]
   }
 }
 

From 6f6f642c7d25288253f1cb1f0fce890f42f9ec8f Mon Sep 17 00:00:00 2001
From: yousifpatti <yousifpatti@gmail.com>
Date: Tue, 21 Nov 2023 15:18:37 +1000
Subject: [PATCH 10/29] Fixed a bug in pretty printer

---
 src/main/scala/util/RunUtils.scala | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/main/scala/util/RunUtils.scala b/src/main/scala/util/RunUtils.scala
index b203dfb34..756330205 100644
--- a/src/main/scala/util/RunUtils.scala
+++ b/src/main/scala/util/RunUtils.scala
@@ -246,7 +246,7 @@ object RunUtils {
     def printNode(node: CfgNode): Unit = {
       s.append(node)
       s.append(" :: ")
-      s.append(result(node))
+      s.append(if result.contains(node) then result(node) else "Unreachable")
       s.append(System.lineSeparator())
     }
 

From 681dc19d05d3c670e7a2ee899b3328f20447bcab Mon Sep 17 00:00:00 2001
From: yousifpatti <yousifpatti@gmail.com>
Date: Tue, 21 Nov 2023 16:41:53 +1000
Subject: [PATCH 11/29] VSA lattice change

---
 src/main/scala/analysis/VSA.scala | 28 +++++++++++++++-------------
 1 file changed, 15 insertions(+), 13 deletions(-)

diff --git a/src/main/scala/analysis/VSA.scala b/src/main/scala/analysis/VSA.scala
index 27fc427f2..6978604c8 100644
--- a/src/main/scala/analysis/VSA.scala
+++ b/src/main/scala/analysis/VSA.scala
@@ -47,7 +47,7 @@ trait ValueSetAnalysisMisc:
 
   /** The lattice of abstract states.
     */
-  val stateLattice: MapLattice[CfgNode, VSALatticeElem] = MapLattice(powersetLattice)
+  val stateLattice: VSALatticeElem = powersetLattice
 
   val domain: Set[CfgNode] = cfg.nodes.toSet
 
@@ -116,11 +116,11 @@ trait ValueSetAnalysisMisc:
                 // this is an exception to the rule and only applies to data regions
                 evaluateExpression(memoryLoad.index, constantProp(n)) match
                   case Some(bitVecLiteral: BitVecLiteral) =>
-                    m = m + (n -> (s.getOrElse(n, Map.empty) + (r -> Set(getValueType(bitVecLiteral)))))
-                    m = m + (n -> (m.getOrElse(n, Map.empty) + (localAssign.lhs -> m(n)(r))))
+                    m = m + (r -> Set(getValueType(bitVecLiteral)))
+                    m = m + (localAssign.lhs -> m(r))
                     m
                   case None =>
-                    m = m + (n -> (m.getOrElse(n, Map.empty) + (localAssign.lhs -> m(n)(r))))
+                    m = m + (localAssign.lhs -> m(r))
                     m
               case None =>
                 Logger.warn("could not find region for " + localAssign)
@@ -128,7 +128,7 @@ trait ValueSetAnalysisMisc:
           case e: Expr =>
             evaluateExpression(e, constantProp(n)) match {
               case Some(bv: BitVecLiteral) =>
-                m = m + (n -> (m.getOrElse(n, Map.empty) + (localAssign.lhs -> Set(getValueType(bv)))))
+                m = m + (localAssign.lhs -> Set(getValueType(bv)))
                 m
               case None =>
                 Logger.warn("could not evaluate expression" + e)
@@ -143,7 +143,7 @@ trait ValueSetAnalysisMisc:
                 val storeValue = memAssign.rhs.value
                 evaluateExpression(storeValue, constantProp(n)) match
                   case Some(bitVecLiteral: BitVecLiteral) =>
-                    m = m + (n -> (m.getOrElse(n, Map.empty) + (r -> Set(getValueType(bitVecLiteral)))))
+                    m = m + (r -> Set(getValueType(bitVecLiteral)))
                     m
                     /*
                   // TODO constant prop returned BOT OR TOP. Merge regions because RHS could be a memory loaded address
@@ -153,7 +153,7 @@ trait ValueSetAnalysisMisc:
                   case None =>
                     storeValue.match {
                       case v: Variable =>
-                        m = m + (n -> (m.getOrElse(n, Map.empty) + (r -> m(n)(v))))
+                        m = m + (r -> m(v))
                         m
                       case _ =>
                         Logger.warn(s"Too Complex: $storeValue") // do nothing
@@ -221,12 +221,14 @@ abstract class LiftedValueSetAnalysis[P <: ProgramCfg] (
    */
   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 = false)
-    }
+      n match {
+        // function entry nodes are always reachable (if intra-procedural analysis)
+        case entryNode: CfgFunctionEntryNode =>
+          if entryNode.data.name.equals("main") then return lift(stateLattice.bottom)
+        // all other nodes are processed with join+transfer
+        case _ => return super.funsub(n, x, intra)
+      }
+    super.funsub(n, x, intra)
   }
 }
 

From 6cbbd275fc74d130f26b584019131ecf7f1718ce Mon Sep 17 00:00:00 2001
From: yousifpatti <yousifpatti@gmail.com>
Date: Tue, 17 Oct 2023 17:21:40 +1000
Subject: [PATCH 12/29] Adding lifted lattice solver

---
 src/main/scala/analysis/Analysis.scala        | 54 +++++++++++++++++--
 src/main/scala/analysis/Cfg.scala             |  2 +
 src/main/scala/analysis/Lattice.scala         | 37 +++++++++++++
 .../analysis/solvers/FixPointSolver.scala     | 22 ++++++++
 4 files changed, 110 insertions(+), 5 deletions(-)

diff --git a/src/main/scala/analysis/Analysis.scala b/src/main/scala/analysis/Analysis.scala
index 0349082aa..dec07114d 100644
--- a/src/main/scala/analysis/Analysis.scala
+++ b/src/main/scala/analysis/Analysis.scala
@@ -167,7 +167,7 @@ trait MemoryRegionAnalysis(val cfg: ProgramCfg,
 
   /** The lattice of abstract states.
     */
-  val lattice: MapLattice[CfgNode, Set[MemoryRegion], PowersetLattice[MemoryRegion]] = MapLattice(powersetLattice)
+  val stateLattice: MapLattice[CfgNode, Set[MemoryRegion], PowersetLattice[MemoryRegion]] = MapLattice(powersetLattice)
 
   val domain: Set[CfgNode] = cfg.nodes.toSet
 
@@ -247,7 +247,7 @@ trait MemoryRegionAnalysis(val cfg: ProgramCfg,
           if (directCall.target.name == "malloc") {
             evaluateExpression(mallocVariable, constantProp(n)) match {
               case Some(b: BitVecLiteral) =>
-                lattice.sublattice.lub(s, Set(HeapRegion(nextMallocCount())))
+                lattice.sublattice.lub(s, Set(HeapRegion(nextMallocCount(), b)))
               case None => s
             }
           } else {
@@ -281,7 +281,7 @@ trait MemoryRegionAnalysis(val cfg: ProgramCfg,
             case _ =>
           })
           */
-          lattice.sublattice.lub(s, result)
+          stateLattice.sublattice.lub(s, result)
         case localAssign: LocalAssign =>
           var m = s
           unwrapExpr(localAssign.rhs).foreach {
@@ -297,7 +297,7 @@ trait MemoryRegionAnalysis(val cfg: ProgramCfg,
                 case _ =>
               })
               */
-              m = lattice.sublattice.lub(m, result)
+              m = stateLattice.sublattice.lub(m, result)
             case _ => m
           }
           m
@@ -310,6 +310,50 @@ trait MemoryRegionAnalysis(val cfg: ProgramCfg,
     */
   def transfer(n: CfgNode, s: Set[MemoryRegion]): Set[MemoryRegion] = 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, FlatElement[BitVecLiteral]]]
+) 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)
+    }
+  }
+}
+
 }
 
 class MemoryRegionAnalysisSolver(
@@ -318,6 +362,6 @@ class MemoryRegionAnalysisSolver(
     globalOffsets: Map[BigInt, BigInt],
     subroutines: Map[BigInt, String],
     constantProp: Map[CfgNode, Map[Variable, FlatElement[BitVecLiteral]]]
-) extends MemoryRegionAnalysis(cfg, globals, globalOffsets, subroutines, constantProp)
+) extends LiftedMemoryRegionAnalysis(cfg, globals, globalOffsets, subroutines, constantProp)
     with IntraproceduralForwardDependencies
     with SimpleMonotonicSolver[CfgNode, Set[MemoryRegion], PowersetLattice[MemoryRegion]]
\ No newline at end of file
diff --git a/src/main/scala/analysis/Cfg.scala b/src/main/scala/analysis/Cfg.scala
index dfaa113dd..b5a49f98c 100644
--- a/src/main/scala/analysis/Cfg.scala
+++ b/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())
diff --git a/src/main/scala/analysis/Lattice.scala b/src/main/scala/analysis/Lattice.scala
index e2379815c..93e6f6d9f 100644
--- a/src/main/scala/analysis/Lattice.scala
+++ b/src/main/scala/analysis/Lattice.scala
@@ -37,6 +37,43 @@ case class FlatEl[T](el: T) extends FlatElement[T]
 case object Top extends FlatElement[Nothing]
 case object Bottom extends FlatElement[Nothing]
 
+trait LiftedElement[+T]
+case class Lift[T](el: T) extends LiftedElement[T]
+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")
+  }
+}
+
 /** 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.
   */
diff --git a/src/main/scala/analysis/solvers/FixPointSolver.scala b/src/main/scala/analysis/solvers/FixPointSolver.scala
index f86f1f260..971c7b23d 100644
--- a/src/main/scala/analysis/solvers/FixPointSolver.scala
+++ b/src/main/scala/analysis/solvers/FixPointSolver.scala
@@ -48,6 +48,28 @@ trait MapLatticeSolver[N, T, L <: Lattice[T]] extends LatticeSolver[Map[N, T]] w
     val states = indep(n).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

From 13947447e6efd67369f741c7d19dce2cc8bc15ea Mon Sep 17 00:00:00 2001
From: yousifpatti <yousifpatti@gmail.com>
Date: Tue, 24 Oct 2023 17:18:22 +1000
Subject: [PATCH 13/29] Lifted works but needs unlifting results

---
 src/main/scala/analysis/Analysis.scala        | 70 +++++++++++++++++--
 src/main/scala/analysis/VSA.scala             | 37 ++++++++++
 .../analysis/solvers/FixPointSolver.scala     | 19 +++++
 3 files changed, 121 insertions(+), 5 deletions(-)

diff --git a/src/main/scala/analysis/Analysis.scala b/src/main/scala/analysis/Analysis.scala
index dec07114d..a7d207b42 100644
--- a/src/main/scala/analysis/Analysis.scala
+++ b/src/main/scala/analysis/Analysis.scala
@@ -163,7 +163,7 @@ trait MemoryRegionAnalysis(val cfg: ProgramCfg,
 
   /** The lattice of abstract values.
     */
-  val powersetLattice: PowersetLattice[MemoryRegion] = PowersetLattice()
+  val regionLattice: PowersetLattice[MemoryRegion] = PowersetLattice()
 
   /** The lattice of abstract states.
     */
@@ -232,6 +232,7 @@ 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")
@@ -310,11 +311,17 @@ trait MemoryRegionAnalysis(val cfg: ProgramCfg,
     */
   def transfer(n: CfgNode, s: Set[MemoryRegion]): Set[MemoryRegion] = localTransfer(n, s)
 
+trait IntraprocMemoryRegionAnalysisMisc[N] extends MemoryRegionAnalysisMisc {
+  val liftedstatelattice: LiftLattice[stateLattice.type]
+  val cfg: ProgramCfg
+  val lattice: MapLattice[N, liftedstatelattice.type]
+}
+
 /**
  * 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 cfg: P,
     val globals: Map[BigInt, String],
     val globalOffsets: Map[BigInt, BigInt],
     val subroutines: Map[BigInt, String],
@@ -333,7 +340,7 @@ abstract class LiftedMemoryRegionAnalysis[P <: ProgramCfg](
    */
   val lattice: MapLattice[CfgNode, liftedstatelattice.type] = new MapLattice(liftedstatelattice)
 
-  val domain: Set[CfgNode] = cfg.nodes.toSet
+  override val domain: Set[CfgNode] = cfg.nodes.toSet
 
   /**
    * The worklist is initialized with all function entry nodes.
@@ -349,7 +356,7 @@ abstract class LiftedMemoryRegionAnalysis[P <: ProgramCfg](
       // 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)
+      case _ => super.funsub(n, x, intra = true)
     }
   }
 }
@@ -364,4 +371,57 @@ class MemoryRegionAnalysisSolver(
     constantProp: Map[CfgNode, Map[Variable, FlatElement[BitVecLiteral]]]
 ) extends LiftedMemoryRegionAnalysis(cfg, globals, globalOffsets, subroutines, constantProp)
     with IntraproceduralForwardDependencies
-    with SimpleMonotonicSolver[CfgNode, Set[MemoryRegion], PowersetLattice[MemoryRegion]]
\ No newline at end of file
+    with SimpleMonotonicSolver[CfgNode, Set[MemoryRegion], PowersetLattice[MemoryRegion]]
+
+
+
+
+///**
+// * Functionality for basic analyses with lifted state lattice.
+// */
+//trait LiftedMemoryRegionAnalysisMisc extends MemoryRegionAnalysisMisc {
+//
+//  /**
+//   * Transfer function for state lattice elements.
+//   * (Same as `localTransfer` for basic analyses with lifted state lattice.)
+//   */
+//  def transferUnlifted(n: CfgNode, s: stateLattice.Element): stateLattice.Element = localTransfer(n, s)
+//}
+//
+///**
+// * Intraprocedural value analysis that uses [[tip.solvers.WorklistFixpointSolverWithReachability]],
+// * with all function entries as start nodes.
+// */
+//abstract class IntraprocValueAnalysisWorklistSolverWithReachability[L](
+//  cfg: ProgramCfg,
+//  globals: Map[BigInt, String],
+//  globalOffsets: Map[BigInt, BigInt],
+//  subroutines: Map[BigInt, String],
+//  constantProp: Map[CfgNode, Map[Variable, ConstantPropagationLattice.Element]]
+//  )
+//  extends LiftedMemoryRegionAnalysis(
+//    cfg,
+//    globals,
+//    globalOffsets,
+//    subroutines,
+//    constantProp,
+//    true)
+//  with LiftedMemoryRegionAnalysisMisc
+//  with WorklistFixpointSolverWithReachability[CfgNode]
+//  with ForwardDependencies
+//
+//object MemoryRegionAnalysis:
+//
+//  class WorklistSolver(
+//      cfg: ProgramCfg,
+//      globals: Map[BigInt, String],
+//      globalOffsets: Map[BigInt, BigInt],
+//      subroutines: Map[BigInt, String],
+//      constantProp: Map[CfgNode, Map[Variable, ConstantPropagationLattice.Element]]
+//  ) extends IntraprocValueAnalysisWorklistSolverWithReachability(
+//        cfg,
+//        globals,
+//        globalOffsets,
+//        subroutines,
+//        constantProp
+//      )
\ No newline at end of file
diff --git a/src/main/scala/analysis/VSA.scala b/src/main/scala/analysis/VSA.scala
index 4a8f3342d..fdf24a32b 100644
--- a/src/main/scala/analysis/VSA.scala
+++ b/src/main/scala/analysis/VSA.scala
@@ -187,3 +187,40 @@ class ValueSetAnalysisSolver(
 ) 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]]]
+
+
+//abstract class IntraprocValueSetAnalysisWorklistSolver[L <: VSALatticeElem](
+//    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
+//) extends ValueSetAnalysis(cfg, globals, externalFunctions, globalOffsets, subroutines, mmm, constantProp)
+//    with SimpleWorklistFixpointSolver[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])
+//      )
\ No newline at end of file
diff --git a/src/main/scala/analysis/solvers/FixPointSolver.scala b/src/main/scala/analysis/solvers/FixPointSolver.scala
index 971c7b23d..ed4d69ca1 100644
--- a/src/main/scala/analysis/solvers/FixPointSolver.scala
+++ b/src/main/scala/analysis/solvers/FixPointSolver.scala
@@ -185,6 +185,25 @@ trait SimpleWorklistFixpointSolver[N, T, L <: Lattice[T]] extends WorklistFixpoi
     run(domain)
     x
 
+/**
+ * The worklist-based fixpoint solver with reachability.
+ *
+ * This solver works for map lattices with lifted co-domains, where the extra bottom element typically represents "unreachable".
+ */
+trait WorklistFixpointSolverWithReachability[N] extends WorklistFixpointSolver[N] with MapLiftLatticeSolver[N] {
+
+  /**
+   * The start locations, used as the initial contents of the worklist.
+   */
+  val first: Set[N]
+
+  def analyze(intra: Boolean): lattice.Element = {
+    x = lattice.bottom
+    run(first, intra)
+    x
+  }
+}
+
 /** A pushDown worklist-based fixpoint solvers. Pushes the results of the analysis one node down. This is used to have
   * the results of the pred node in the current node. ie. NODE 1: R0 = 69551bv64 RESULT LATTICE = {} NODE 2: R0 =
   * MemLoad[R0 + 54bv64] RESULT LATTICE = {R0 = 69551bv64} NODE 3: R1 = 0bv64 RESULT LATTICE = {R0 = TOP} ...

From 45262e471fc2856913e9bcb784f6e7f79dd913e0 Mon Sep 17 00:00:00 2001
From: yousifpatti <yousifpatti@gmail.com>
Date: Tue, 31 Oct 2023 14:39:47 +1000
Subject: [PATCH 14/29] Added unlifted analyze

---
 .../scala/analysis/solvers/FixPointSolver.scala   | 15 +++++++++++++++
 src/main/scala/util/RunUtils.scala                |  2 +-
 2 files changed, 16 insertions(+), 1 deletion(-)

diff --git a/src/main/scala/analysis/solvers/FixPointSolver.scala b/src/main/scala/analysis/solvers/FixPointSolver.scala
index ed4d69ca1..b3a20441e 100644
--- a/src/main/scala/analysis/solvers/FixPointSolver.scala
+++ b/src/main/scala/analysis/solvers/FixPointSolver.scala
@@ -202,6 +202,21 @@ trait WorklistFixpointSolverWithReachability[N] extends WorklistFixpointSolver[N
     run(first, intra)
     x
   }
+
+  /**
+   * The transfer function for the sub-sub-lattice. Unlifts the resulting MapLattice[N, LiftLattice[Lattice.sublattice]]
+   * to MapLattice[N, Lattice.sublattice.sublattice].
+   *
+   * @param intra
+   * @return the sub-sub-lattice
+   */
+  def unliftedAnalyze(intra: Boolean): lattice.sublattice.sublattice.Element = {
+    val res: lattice.Element = analyze(intra)
+    // Convert liftedResult to unlifted
+    res.map {
+      case (key, value) => (key, lattice.sublattice.unlift(value))
+    }.asInstanceOf[lattice.sublattice.sublattice.Element]
+  }
 }
 
 /** A pushDown worklist-based fixpoint solvers. Pushes the results of the analysis one node down. This is used to have
diff --git a/src/main/scala/util/RunUtils.scala b/src/main/scala/util/RunUtils.scala
index 3dbc4d07c..c4161babc 100644
--- a/src/main/scala/util/RunUtils.scala
+++ b/src/main/scala/util/RunUtils.scala
@@ -154,7 +154,7 @@ object RunUtils {
 
     Logger.info("[!] Running MRA")
     val mraSolver = MemoryRegionAnalysisSolver(cfg, globalAddresses, globalOffsets, mergedSubroutines, constPropResult)
-    val mraResult = mraSolver.analyze()
+    val mraResult = mraSolver.unliftedAnalyze()
     memoryRegionAnalysisResults = mraResult
 
     config.analysisDotPath.foreach(s => writeToFile(cfg.toDot(Output.labeler(mraResult, true), Output.dotIder), s"${s}_mra$iteration.dot"))

From c55f2713f1939a5bd5024e053e6ec9bed4b71154 Mon Sep 17 00:00:00 2001
From: yousifpatti <yousifpatti@gmail.com>
Date: Tue, 31 Oct 2023 17:16:16 +1000
Subject: [PATCH 15/29] started lifted VSA but some issues marked with TODO

---
 src/main/scala/analysis/Analysis.scala    | 27 +++++++++++++++++------
 src/main/scala/analysis/UtilMethods.scala |  1 +
 src/main/scala/analysis/VSA.scala         | 12 ++++++++--
 src/main/scala/util/RunUtils.scala        |  6 ++++-
 4 files changed, 36 insertions(+), 10 deletions(-)

diff --git a/src/main/scala/analysis/Analysis.scala b/src/main/scala/analysis/Analysis.scala
index a7d207b42..2e46ef24f 100644
--- a/src/main/scala/analysis/Analysis.scala
+++ b/src/main/scala/analysis/Analysis.scala
@@ -374,6 +374,19 @@ class MemoryRegionAnalysisSolver(
     with SimpleMonotonicSolver[CfgNode, Set[MemoryRegion], PowersetLattice[MemoryRegion]]
 
 
+  class WorklistSolver(
+      cfg: ProgramCfg,
+      globals: Map[BigInt, String],
+      globalOffsets: Map[BigInt, BigInt],
+      subroutines: Map[BigInt, String],
+      constantProp: Map[CfgNode, Map[Variable, ConstantPropagationLattice.Element]]
+  ) extends IntraprocMemoryRegionAnalysisWorklistSolverWithReachability(
+        cfg,
+        globals,
+        globalOffsets,
+        subroutines,
+        constantProp
+      )
 
 
 ///**
@@ -392,13 +405,13 @@ class MemoryRegionAnalysisSolver(
 // * Intraprocedural value analysis that uses [[tip.solvers.WorklistFixpointSolverWithReachability]],
 // * with all function entries as start nodes.
 // */
-//abstract class IntraprocValueAnalysisWorklistSolverWithReachability[L](
-//  cfg: ProgramCfg,
-//  globals: Map[BigInt, String],
-//  globalOffsets: Map[BigInt, BigInt],
-//  subroutines: Map[BigInt, String],
-//  constantProp: Map[CfgNode, Map[Variable, ConstantPropagationLattice.Element]]
-//  )
+//abstract class IntraprocMemoryRegionAnalysisWorklistSolverWithReachability[L](
+//    cfg: ProgramCfg,
+//    globals: Map[BigInt, String],
+//    globalOffsets: Map[BigInt, BigInt],
+//    subroutines: Map[BigInt, String],
+//    constantProp: Map[CfgNode, Map[Variable, ConstantPropagationLattice.Element]]
+//    )
 //  extends LiftedMemoryRegionAnalysis(
 //    cfg,
 //    globals,
diff --git a/src/main/scala/analysis/UtilMethods.scala b/src/main/scala/analysis/UtilMethods.scala
index 7a4f44137..402076ee5 100644
--- a/src/main/scala/analysis/UtilMethods.scala
+++ b/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
diff --git a/src/main/scala/analysis/VSA.scala b/src/main/scala/analysis/VSA.scala
index fdf24a32b..34bddbbe6 100644
--- a/src/main/scala/analysis/VSA.scala
+++ b/src/main/scala/analysis/VSA.scala
@@ -198,8 +198,16 @@ class ValueSetAnalysisSolver(
 //    mmm: MemoryModelMap,
 //    constantProp: Map[CfgNode, Map[Variable, ConstantPropagationLattice.Element]],
 //    val powersetLattice: L
-//) extends ValueSetAnalysis(cfg, globals, externalFunctions, globalOffsets, subroutines, mmm, constantProp)
-//    with SimpleWorklistFixpointSolver[CfgNode]
+//) extends LiftedValueSetAnalysis(
+//    cfg,
+//    globals,
+//    externalFunctions,
+//    globalOffsets, subroutines,
+//    mmm,
+//    constantProp,
+//    true)
+//    with LiftedValueSetAnalysisMisc
+//    with WorklistFixpointSolverWithReachability[CfgNode]
 //    with ForwardDependencies
 //
 //object ValueSetAnalysis:
diff --git a/src/main/scala/util/RunUtils.scala b/src/main/scala/util/RunUtils.scala
index c4161babc..3586423c3 100644
--- a/src/main/scala/util/RunUtils.scala
+++ b/src/main/scala/util/RunUtils.scala
@@ -166,7 +166,11 @@ object RunUtils {
 
     Logger.info("[!] Running VSA")
     val vsaSolver = ValueSetAnalysisSolver(cfg, globalAddresses, externalAddresses, globalOffsets, subroutines, mmm, constPropResult)
-    val vsaResult = vsaSolver.analyze()
+    // TODO: replace ? with the right type
+    val vsaResult = vsaSolver.unliftedAnalyze(true).asInstanceOf[Map[CfgNode, ?]]
+    ].map {
+      case (k, v) => k -> v.values.flatten.toSet
+    }
 
     config.analysisDotPath.foreach(s => writeToFile(cfg.toDot(Output.labeler(vsaResult, true), Output.dotIder), s"${s}_vsa$iteration.dot"))
     config.analysisResultsPath.foreach(s => writeToFile(printAnalysisResults(cfg, vsaResult, iteration), s"${s}_vsa$iteration.txt"))

From 855cfdd4ef2472d10a2771b18ab42709a45b71af Mon Sep 17 00:00:00 2001
From: yousifpatti <yousifpatti@gmail.com>
Date: Tue, 7 Nov 2023 15:16:06 +1000
Subject: [PATCH 16/29] Lifted VSA

---
 src/main/scala/analysis/VSA.scala  | 4 ++--
 src/main/scala/util/RunUtils.scala | 6 +-----
 2 files changed, 3 insertions(+), 7 deletions(-)

diff --git a/src/main/scala/analysis/VSA.scala b/src/main/scala/analysis/VSA.scala
index 34bddbbe6..34916e826 100644
--- a/src/main/scala/analysis/VSA.scala
+++ b/src/main/scala/analysis/VSA.scala
@@ -212,7 +212,7 @@ class ValueSetAnalysisSolver(
 //
 //object ValueSetAnalysis:
 //
-//  /** Intraprocedural analysis that uses the worklist solver.
+//  /** Interprocedural analysis that uses the worklist solver.
 //    */
 //  class WorklistSolver(
 //      cfg: ProgramCfg,
@@ -222,7 +222,7 @@ class ValueSetAnalysisSolver(
 //      subroutines: Map[BigInt, String],
 //      mmm: MemoryModelMap,
 //      constantProp: Map[CfgNode, Map[Variable, ConstantPropagationLattice.Element]]
-//  ) extends IntraprocValueSetAnalysisWorklistSolver(
+//  ) extends InterprocValueSetAnalysisWorklistSolver(
 //        cfg,
 //        globals,
 //        externalFunctions,
diff --git a/src/main/scala/util/RunUtils.scala b/src/main/scala/util/RunUtils.scala
index 3586423c3..4959f8e45 100644
--- a/src/main/scala/util/RunUtils.scala
+++ b/src/main/scala/util/RunUtils.scala
@@ -166,11 +166,7 @@ object RunUtils {
 
     Logger.info("[!] Running VSA")
     val vsaSolver = ValueSetAnalysisSolver(cfg, globalAddresses, externalAddresses, globalOffsets, subroutines, mmm, constPropResult)
-    // TODO: replace ? with the right type
-    val vsaResult = vsaSolver.unliftedAnalyze(true).asInstanceOf[Map[CfgNode, ?]]
-    ].map {
-      case (k, v) => k -> v.values.flatten.toSet
-    }
+    val vsaResult: Map[CfgNode, Map[Variable | MemoryRegion, Set[Value]]] = vsaSolver.unliftedAnalyze(true).asInstanceOf[Map[CfgNode, Map[Variable | MemoryRegion, Set[Value]]]]
 
     config.analysisDotPath.foreach(s => writeToFile(cfg.toDot(Output.labeler(vsaResult, true), Output.dotIder), s"${s}_vsa$iteration.dot"))
     config.analysisResultsPath.foreach(s => writeToFile(printAnalysisResults(cfg, vsaResult, iteration), s"${s}_vsa$iteration.txt"))

From a97c7ea051288505eed4503a6b6c86c4c0149230 Mon Sep 17 00:00:00 2001
From: yousifpatti <yousifpatti@gmail.com>
Date: Tue, 14 Nov 2023 15:02:53 +1000
Subject: [PATCH 17/29] VSA lifted lattice

---
 src/main/scala/analysis/Lattice.scala                | 4 +++-
 src/main/scala/analysis/solvers/FixPointSolver.scala | 4 +---
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/main/scala/analysis/Lattice.scala b/src/main/scala/analysis/Lattice.scala
index 93e6f6d9f..027dcd98d 100644
--- a/src/main/scala/analysis/Lattice.scala
+++ b/src/main/scala/analysis/Lattice.scala
@@ -38,7 +38,9 @@ case object Top extends FlatElement[Nothing]
 case object Bottom extends FlatElement[Nothing]
 
 trait LiftedElement[+T]
-case class Lift[T](el: T) extends LiftedElement[T]
+case class Lift[T](el: T) extends LiftedElement[T] {
+  override def toString = s"Lift($n)"
+}
 case object LiftedBottom extends LiftedElement[Nothing] {
   override def toString = "LiftBot"
 }
diff --git a/src/main/scala/analysis/solvers/FixPointSolver.scala b/src/main/scala/analysis/solvers/FixPointSolver.scala
index b3a20441e..e46389271 100644
--- a/src/main/scala/analysis/solvers/FixPointSolver.scala
+++ b/src/main/scala/analysis/solvers/FixPointSolver.scala
@@ -213,9 +213,7 @@ trait WorklistFixpointSolverWithReachability[N] extends WorklistFixpointSolver[N
   def unliftedAnalyze(intra: Boolean): lattice.sublattice.sublattice.Element = {
     val res: lattice.Element = analyze(intra)
     // Convert liftedResult to unlifted
-    res.map {
-      case (key, value) => (key, lattice.sublattice.unlift(value))
-    }.asInstanceOf[lattice.sublattice.sublattice.Element]
+    res.foldLeft(lattice.sublattice.sublattice.bottom)((acc, pred) => lattice.sublattice.sublattice.lub(acc, lattice.sublattice.unlift(pred._2)))
   }
 }
 

From 84f85e62c773f3736b57f379775101da32e8abcc Mon Sep 17 00:00:00 2001
From: yousifpatti <yousifpatti@gmail.com>
Date: Thu, 16 Nov 2023 15:18:09 +1000
Subject: [PATCH 18/29] Fixing local transfer returns

---
 src/main/scala/analysis/VSA.scala             | 41 +++++++++++--------
 .../analysis/solvers/FixPointSolver.scala     |  1 +
 2 files changed, 25 insertions(+), 17 deletions(-)

diff --git a/src/main/scala/analysis/VSA.scala b/src/main/scala/analysis/VSA.scala
index 34916e826..84703b72c 100644
--- a/src/main/scala/analysis/VSA.scala
+++ b/src/main/scala/analysis/VSA.scala
@@ -102,6 +102,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 +112,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 + (n -> (s.getOrElse(n, Map.empty) + (r -> Set(getValueType(bitVecLiteral)))))
+                    m = m + (n -> (m.getOrElse(n, Map.empty) + (localAssign.lhs -> m(n)(r))))
+                    m
                   case None =>
-                    s + (localAssign.lhs -> s(r))
+                    m = m + (n -> (m.getOrElse(n, Map.empty) + (localAssign.lhs -> m(n)(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 + (n -> (m.getOrElse(n, Map.empty) + (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 +139,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 + (n -> (m.getOrElse(n, Map.empty) + (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 + (n -> (m.getOrElse(n, Map.empty) + (r -> m(n)(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.
diff --git a/src/main/scala/analysis/solvers/FixPointSolver.scala b/src/main/scala/analysis/solvers/FixPointSolver.scala
index e46389271..3545ccd72 100644
--- a/src/main/scala/analysis/solvers/FixPointSolver.scala
+++ b/src/main/scala/analysis/solvers/FixPointSolver.scala
@@ -61,6 +61,7 @@ trait MapLiftLatticeSolver[N] extends MapLatticeSolver[N] with Dependencies[N] {
    */
   def transferUnlifted(n: N, s: lattice.sublattice.sublattice.Element): lattice.sublattice.sublattice.Element
 
+  @Override
   def transfer(n: N, s: lattice.sublattice.Element): lattice.sublattice.Element = {
     import lattice.sublattice._
     s match {

From 60e76a5010cb2e74614fa2d38706fe3e70d5be91 Mon Sep 17 00:00:00 2001
From: yousifpatti <yousifpatti@gmail.com>
Date: Tue, 21 Nov 2023 10:05:52 +1000
Subject: [PATCH 19/29] Minor format issue

---
 src/main/scala/analysis/solvers/FixPointSolver.scala | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/src/main/scala/analysis/solvers/FixPointSolver.scala b/src/main/scala/analysis/solvers/FixPointSolver.scala
index 3545ccd72..9416a9a1b 100644
--- a/src/main/scala/analysis/solvers/FixPointSolver.scala
+++ b/src/main/scala/analysis/solvers/FixPointSolver.scala
@@ -61,8 +61,7 @@ trait MapLiftLatticeSolver[N] extends MapLatticeSolver[N] with Dependencies[N] {
    */
   def transferUnlifted(n: N, s: lattice.sublattice.sublattice.Element): lattice.sublattice.sublattice.Element
 
-  @Override
-  def transfer(n: N, s: lattice.sublattice.Element): lattice.sublattice.Element = {
+  override 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

From de6e54bc62287c7f5f635f4c255d0c2b9a4ae1a0 Mon Sep 17 00:00:00 2001
From: yousifpatti <yousifpatti@gmail.com>
Date: Tue, 21 Nov 2023 14:56:11 +1000
Subject: [PATCH 20/29] Fixed MRA join issue with liftedLattice

---
 src/main/scala/analysis/Analysis.scala        | 47 ++++---------------
 .../analysis/solvers/FixPointSolver.scala     |  6 ++-
 2 files changed, 13 insertions(+), 40 deletions(-)

diff --git a/src/main/scala/analysis/Analysis.scala b/src/main/scala/analysis/Analysis.scala
index 2e46ef24f..cba122b23 100644
--- a/src/main/scala/analysis/Analysis.scala
+++ b/src/main/scala/analysis/Analysis.scala
@@ -259,45 +259,12 @@ 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 _ =>
-          })
-          */
           stateLattice.sublattice.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 = stateLattice.sublattice.lub(m, result)
             case _ => m
           }
@@ -352,12 +319,14 @@ abstract class LiftedMemoryRegionAnalysis[P <: ProgramCfg](
    */
   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 = true)
-    }
+      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 _ =>
+          val joinedStates = indep(n, intra).map(x(_)).foldLeft(liftedstatelattice.bottom)((acc, pred) => liftedstatelattice.lub(acc, pred))
+          lift(localTransfer(n, unlift(joinedStates)))
+      }
   }
 }
 
diff --git a/src/main/scala/analysis/solvers/FixPointSolver.scala b/src/main/scala/analysis/solvers/FixPointSolver.scala
index 9416a9a1b..a308bad6c 100644
--- a/src/main/scala/analysis/solvers/FixPointSolver.scala
+++ b/src/main/scala/analysis/solvers/FixPointSolver.scala
@@ -211,9 +211,13 @@ trait WorklistFixpointSolverWithReachability[N] extends WorklistFixpointSolver[N
    * @return the sub-sub-lattice
    */
   def unliftedAnalyze(intra: Boolean): lattice.sublattice.sublattice.Element = {
+    import lattice.sublattice._
     val res: lattice.Element = analyze(intra)
     // Convert liftedResult to unlifted
-    res.foldLeft(lattice.sublattice.sublattice.bottom)((acc, pred) => lattice.sublattice.sublattice.lub(acc, lattice.sublattice.unlift(pred._2)))
+    res.map((n, lift) => (n, lift match {
+      case Bottom => lattice.sublattice.sublattice.bottom
+      case Lift(a) => a
+    })).asInstanceOf[lattice.sublattice.sublattice.Element]
   }
 }
 

From 5bc0d76ed37ddd87ad542671f6e793e89fbda927 Mon Sep 17 00:00:00 2001
From: yousifpatti <yousifpatti@gmail.com>
Date: Tue, 21 Nov 2023 15:18:37 +1000
Subject: [PATCH 21/29] Fixed a bug in pretty printer

---
 src/main/scala/util/RunUtils.scala | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/main/scala/util/RunUtils.scala b/src/main/scala/util/RunUtils.scala
index 4959f8e45..96174dc7c 100644
--- a/src/main/scala/util/RunUtils.scala
+++ b/src/main/scala/util/RunUtils.scala
@@ -245,7 +245,7 @@ object RunUtils {
     def printNode(node: CfgNode): Unit = {
       s.append(node)
       s.append(" :: ")
-      s.append(result(node))
+      s.append(if result.contains(node) then result(node) else "Unreachable")
       s.append(System.lineSeparator())
     }
 

From b04ec034a42f0ad2cd56cf474b9e1c6a9e11f80d Mon Sep 17 00:00:00 2001
From: yousifpatti <yousifpatti@gmail.com>
Date: Tue, 21 Nov 2023 16:41:53 +1000
Subject: [PATCH 22/29] VSA lattice change

---
 src/main/scala/analysis/VSA.scala | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/src/main/scala/analysis/VSA.scala b/src/main/scala/analysis/VSA.scala
index 84703b72c..d2cf1169d 100644
--- a/src/main/scala/analysis/VSA.scala
+++ b/src/main/scala/analysis/VSA.scala
@@ -112,11 +112,11 @@ 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) =>
-                    m = m + (n -> (s.getOrElse(n, Map.empty) + (r -> Set(getValueType(bitVecLiteral)))))
-                    m = m + (n -> (m.getOrElse(n, Map.empty) + (localAssign.lhs -> m(n)(r))))
+                    m = m + (r -> Set(getValueType(bitVecLiteral)))
+                    m = m + (localAssign.lhs -> m(r))
                     m
                   case None =>
-                    m = m + (n -> (m.getOrElse(n, Map.empty) + (localAssign.lhs -> m(n)(r))))
+                    m = m + (localAssign.lhs -> m(r))
                     m
               case None =>
                 Logger.warn("could not find region for " + localAssign)
@@ -124,7 +124,7 @@ trait ValueSetAnalysis(cfg: ProgramCfg,
           case e: Expr =>
             evaluateExpression(e, constantProp(n)) match {
               case Some(bv: BitVecLiteral) =>
-                m = m + (n -> (m.getOrElse(n, Map.empty) + (localAssign.lhs -> Set(getValueType(bv)))))
+                m = m + (localAssign.lhs -> Set(getValueType(bv)))
                 m
               case None =>
                 Logger.warn("could not evaluate expression" + e)
@@ -139,7 +139,7 @@ trait ValueSetAnalysis(cfg: ProgramCfg,
                 val storeValue = memAssign.rhs.value
                 evaluateExpression(storeValue, constantProp(n)) match
                   case Some(bitVecLiteral: BitVecLiteral) =>
-                    m = m + (n -> (m.getOrElse(n, Map.empty) + (r -> Set(getValueType(bitVecLiteral)))))
+                    m = m + (r -> Set(getValueType(bitVecLiteral)))
                     m
                     /*
                   // TODO constant prop returned BOT OR TOP. Merge regions because RHS could be a memory loaded address
@@ -149,7 +149,7 @@ trait ValueSetAnalysis(cfg: ProgramCfg,
                   case None =>
                     storeValue.match {
                       case v: Variable =>
-                        m = m + (n -> (m.getOrElse(n, Map.empty) + (r -> m(n)(v))))
+                        m = m + (r -> m(v))
                         m
                       case _ =>
                         Logger.warn(s"Too Complex: $storeValue") // do nothing

From 4ecdc7d43749cdb81013e7cb17628f2cd6337602 Mon Sep 17 00:00:00 2001
From: yousifpatti <yousifpatti@gmail.com>
Date: Wed, 29 Nov 2023 17:12:10 +1000
Subject: [PATCH 23/29] Resolving type issues

---
 src/main/scala/analysis/Analysis.scala        | 154 ++++++------------
 src/main/scala/analysis/Lattice.scala         |  14 +-
 src/main/scala/analysis/MemoryModelMap.scala  |   4 +-
 .../analysis/solvers/FixPointSolver.scala     |  23 ++-
 src/main/scala/util/RunUtils.scala            |   4 +-
 5 files changed, 69 insertions(+), 130 deletions(-)

diff --git a/src/main/scala/analysis/Analysis.scala b/src/main/scala/analysis/Analysis.scala
index cba122b23..8a55b4120 100644
--- a/src/main/scala/analysis/Analysis.scala
+++ b/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)) {
@@ -162,12 +162,12 @@ trait MemoryRegionAnalysis(val cfg: ProgramCfg,
   }
 
   /** The lattice of abstract values.
-    */
+   */
   val regionLattice: PowersetLattice[MemoryRegion] = PowersetLattice()
 
   /** The lattice of abstract states.
-    */
-  val stateLattice: MapLattice[CfgNode, Set[MemoryRegion], PowersetLattice[MemoryRegion]] = MapLattice(powersetLattice)
+   */
+  val stateLattice: MapLattice[CfgNode, Set[MemoryRegion], PowersetLattice[MemoryRegion]] = MapLattice(regionLattice)
 
   val domain: Set[CfgNode] = cfg.nodes.toSet
 
@@ -232,7 +232,7 @@ 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
+      // 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")
@@ -240,7 +240,7 @@ trait MemoryRegionAnalysis(val cfg: ProgramCfg,
   }
 
   /** Transfer function for state lattice elements.
-    */
+   */
   def localTransfer(n: CfgNode, s: Set[MemoryRegion]): Set[MemoryRegion] = n match {
     case cmd: CfgCommandNode =>
       cmd.data match {
@@ -248,7 +248,7 @@ trait MemoryRegionAnalysis(val cfg: ProgramCfg,
           if (directCall.target.name == "malloc") {
             evaluateExpression(mallocVariable, constantProp(n)) match {
               case Some(b: BitVecLiteral) =>
-                lattice.sublattice.lub(s, Set(HeapRegion(nextMallocCount(), b)))
+                stateLattice.sublattice.lub(s, Set(HeapRegion(nextMallocCount(), b)))
               case None => s
             }
           } else {
@@ -275,39 +275,34 @@ trait MemoryRegionAnalysis(val cfg: ProgramCfg,
   }
 
   /** 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)
-
-trait IntraprocMemoryRegionAnalysisMisc[N] extends MemoryRegionAnalysisMisc {
-  val liftedstatelattice: LiftLattice[stateLattice.type]
-  val cfg: ProgramCfg
-  val lattice: MapLattice[N, liftedstatelattice.type]
 }
 
 /**
  * Base class for memory region analysis with lifted lattice, where the extra bottom element represents "unreachable".
  */
-abstract class LiftedMemoryRegionAnalysis[P <: ProgramCfg](
-    val cfg: P,
-    val globals: Map[BigInt, String],
-    val globalOffsets: Map[BigInt, BigInt],
-    val subroutines: Map[BigInt, String],
-    val constantProp: Map[CfgNode, Map[Variable, FlatElement[BitVecLiteral]]]
-) extends FlowSensitiveAnalysis(false)
-    with MapLatticeSolver[CfgNode]
-    with MemoryRegionAnalysisMisc {
+abstract class LiftedMemoryRegionAnalysis(
+                                  val cfg: ProgramCfg,
+                                  val globals: Map[BigInt, String],
+                                  val globalOffsets: Map[BigInt, BigInt],
+                                  val subroutines: Map[BigInt, String],
+                                  val constantProp: Map[CfgNode, Map[Variable, FlatElement[BitVecLiteral]]]
+                                ) extends IntraproceduralForwardDependencies
+  with MapLiftLatticeSolver[CfgNode, Set[MemoryRegion], PowersetLattice[MemoryRegion]]
+  with MemoryRegionAnalysis(cfg, globals, globalOffsets, subroutines, constantProp) {
 
   /**
    * Lifted state lattice, with new bottom element representing "unreachable".
    */
-  val liftedstatelattice: LiftLattice[stateLattice.type] = new LiftLattice(stateLattice)
+  val liftedstatelattice = LiftLattice(stateLattice)
 
   /**
    * The analysis lattice.
    */
-  val lattice: MapLattice[CfgNode, liftedstatelattice.type] = new MapLattice(liftedstatelattice)
+  val lattice = MapLattice(liftedstatelattice) // TODO: TYPING ISSUE
 
-  override val domain: Set[CfgNode] = cfg.nodes.toSet
+  val domain: Set[CfgNode] = cfg.nodes.toSet
 
   /**
    * The worklist is initialized with all function entry nodes.
@@ -317,21 +312,31 @@ abstract class LiftedMemoryRegionAnalysis[P <: ProgramCfg](
   /**
    * Overrides `funsub` from [[tip.solvers.MapLatticeSolver]], treating function entry nodes as reachable.
    */
-  override def funsub(n: CfgNode, x: lattice.Element, intra: Boolean): liftedstatelattice.Element = {
+  override def funsub(n: CfgNode, x: Map[CfgNode, Set[MemoryRegion]]): LiftedElement[Map[analysis.CfgNode, Set[analysis.MemoryRegion]]] = {
     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 _ =>
-          val joinedStates = indep(n, intra).map(x(_)).foldLeft(liftedstatelattice.bottom)((acc, pred) => liftedstatelattice.lub(acc, pred))
-          lift(localTransfer(n, unlift(joinedStates)))
-      }
+    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 _ => lift(stateLattice.bottom) //super.funsub(n, x) TODO: TYPING ISSUE
+    }
   }
 }
 
+/**
+ * Functionality for basic analyses with lifted state lattice.
+ */
+trait LiftedValueAnalysisMisc extends MemoryRegionAnalysis {
+
+  /**
+   * Transfer function for state lattice elements.
+   * (Same as `localTransfer` for basic analyses with lifted state lattice.)
+   */
+  def transferUnlifted(n: CfgNode, s: Set[MemoryRegion]): Set[MemoryRegion] = localTransfer(n, s)
 }
 
+
+
 class MemoryRegionAnalysisSolver(
     cfg: ProgramCfg,
     globals: Map[BigInt, String],
@@ -339,71 +344,6 @@ class MemoryRegionAnalysisSolver(
     subroutines: Map[BigInt, String],
     constantProp: Map[CfgNode, Map[Variable, FlatElement[BitVecLiteral]]]
 ) extends LiftedMemoryRegionAnalysis(cfg, globals, globalOffsets, subroutines, constantProp)
+    with LiftedValueAnalysisMisc
     with IntraproceduralForwardDependencies
-    with SimpleMonotonicSolver[CfgNode, Set[MemoryRegion], PowersetLattice[MemoryRegion]]
-
-
-  class WorklistSolver(
-      cfg: ProgramCfg,
-      globals: Map[BigInt, String],
-      globalOffsets: Map[BigInt, BigInt],
-      subroutines: Map[BigInt, String],
-      constantProp: Map[CfgNode, Map[Variable, ConstantPropagationLattice.Element]]
-  ) extends IntraprocMemoryRegionAnalysisWorklistSolverWithReachability(
-        cfg,
-        globals,
-        globalOffsets,
-        subroutines,
-        constantProp
-      )
-
-
-///**
-// * Functionality for basic analyses with lifted state lattice.
-// */
-//trait LiftedMemoryRegionAnalysisMisc extends MemoryRegionAnalysisMisc {
-//
-//  /**
-//   * Transfer function for state lattice elements.
-//   * (Same as `localTransfer` for basic analyses with lifted state lattice.)
-//   */
-//  def transferUnlifted(n: CfgNode, s: stateLattice.Element): stateLattice.Element = localTransfer(n, s)
-//}
-//
-///**
-// * Intraprocedural value analysis that uses [[tip.solvers.WorklistFixpointSolverWithReachability]],
-// * with all function entries as start nodes.
-// */
-//abstract class IntraprocMemoryRegionAnalysisWorklistSolverWithReachability[L](
-//    cfg: ProgramCfg,
-//    globals: Map[BigInt, String],
-//    globalOffsets: Map[BigInt, BigInt],
-//    subroutines: Map[BigInt, String],
-//    constantProp: Map[CfgNode, Map[Variable, ConstantPropagationLattice.Element]]
-//    )
-//  extends LiftedMemoryRegionAnalysis(
-//    cfg,
-//    globals,
-//    globalOffsets,
-//    subroutines,
-//    constantProp,
-//    true)
-//  with LiftedMemoryRegionAnalysisMisc
-//  with WorklistFixpointSolverWithReachability[CfgNode]
-//  with ForwardDependencies
-//
-//object MemoryRegionAnalysis:
-//
-//  class WorklistSolver(
-//      cfg: ProgramCfg,
-//      globals: Map[BigInt, String],
-//      globalOffsets: Map[BigInt, BigInt],
-//      subroutines: Map[BigInt, String],
-//      constantProp: Map[CfgNode, Map[Variable, ConstantPropagationLattice.Element]]
-//  ) extends IntraprocValueAnalysisWorklistSolverWithReachability(
-//        cfg,
-//        globals,
-//        globalOffsets,
-//        subroutines,
-//        constantProp
-//      )
\ No newline at end of file
+    with WorklistFixpointSolverWithReachability[CfgNode, Set[MemoryRegion], PowersetLattice[MemoryRegion]]
\ No newline at end of file
diff --git a/src/main/scala/analysis/Lattice.scala b/src/main/scala/analysis/Lattice.scala
index 027dcd98d..d12bc7ba8 100644
--- a/src/main/scala/analysis/Lattice.scala
+++ b/src/main/scala/analysis/Lattice.scala
@@ -32,14 +32,9 @@ class PowersetLattice[A] extends Lattice[Set[A]] {
   def lub(x: Set[A], y: Set[A]): Set[A] = x.union(y)
 }
 
-trait FlatElement[+T]
-case class FlatEl[T](el: T) extends FlatElement[T]
-case object Top extends FlatElement[Nothing]
-case object Bottom extends FlatElement[Nothing]
-
 trait LiftedElement[+T]
 case class Lift[T](el: T) extends LiftedElement[T] {
-  override def toString = s"Lift($n)"
+  override def toString = s"Lift($el)"
 }
 case object LiftedBottom extends LiftedElement[Nothing] {
   override def toString = "LiftBot"
@@ -48,7 +43,7 @@ case object LiftedBottom extends LiftedElement[Nothing] {
  * The lift lattice for `sublattice`.
  * Supports implicit lifting and unlifting.
  */
-class LiftLattice[T, +L <: Lattice[T]](val sublattice: L) extends Lattice[LiftedElement[T]] {
+class LiftLattice[N, T, +L <: Lattice[T]](val sublattice: L) extends Lattice[LiftedElement[T]] {
 
   val bottom: LiftedElement[T] = LiftedBottom
 
@@ -76,6 +71,11 @@ class LiftLattice[T, +L <: Lattice[T]](val sublattice: L) extends Lattice[Lifted
   }
 }
 
+trait FlatElement[+T]
+case class FlatEl[T](el: T) extends FlatElement[T]
+case object Top extends FlatElement[Nothing]
+case object Bottom extends FlatElement[Nothing]
+
 /** 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.
   */
diff --git a/src/main/scala/analysis/MemoryModelMap.scala b/src/main/scala/analysis/MemoryModelMap.scala
index 87456b54d..1591725f6 100644
--- a/src/main/scala/analysis/MemoryModelMap.scala
+++ b/src/main/scala/analysis/MemoryModelMap.scala
@@ -123,8 +123,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
diff --git a/src/main/scala/analysis/solvers/FixPointSolver.scala b/src/main/scala/analysis/solvers/FixPointSolver.scala
index a308bad6c..9c8eba1c4 100644
--- a/src/main/scala/analysis/solvers/FixPointSolver.scala
+++ b/src/main/scala/analysis/solvers/FixPointSolver.scala
@@ -52,20 +52,19 @@ trait MapLatticeSolver[N, T, L <: Lattice[T]] extends LatticeSolver[Map[N, T]] w
  * 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]]
+trait MapLiftLatticeSolver[N, T, L <: Lattice[T]] extends MapLatticeSolver[N, T, L] with Dependencies[N] {
+  val lattice: MapLattice[N, LiftedElement[T], LiftLattice[N, T, L]]
 
   /**
    * The transfer function for the sub-sub-lattice.
    */
-  def transferUnlifted(n: N, s: lattice.sublattice.sublattice.Element): lattice.sublattice.sublattice.Element
+  def transferUnlifted(n: N, s: T): T
 
-  override def transfer(n: N, s: lattice.sublattice.Element): lattice.sublattice.Element = {
+  override def transfer(n: N, s: T): LiftedElement[T] = {
     import lattice.sublattice._
     s match {
-      case Bottom => Bottom // unreachable as input implied unreachable at output
-      case Lift(a) => lift(transferUnlifted(n, a))
+      case LiftedBottom => LiftedBottom // unreachable as input implied unreachable at output
+      case l: Lift[T] => lift(transferUnlifted(n, l.el))
     }
   }
 }
@@ -190,16 +189,16 @@ trait SimpleWorklistFixpointSolver[N, T, L <: Lattice[T]] extends WorklistFixpoi
  *
  * This solver works for map lattices with lifted co-domains, where the extra bottom element typically represents "unreachable".
  */
-trait WorklistFixpointSolverWithReachability[N] extends WorklistFixpointSolver[N] with MapLiftLatticeSolver[N] {
+trait WorklistFixpointSolverWithReachability[N, T, L <: Lattice[T]] extends WorklistFixpointSolver[N, T, L] with MapLiftLatticeSolver[N, T, L] {
 
   /**
    * The start locations, used as the initial contents of the worklist.
    */
   val first: Set[N]
 
-  def analyze(intra: Boolean): lattice.Element = {
+  def analyze(): Map[N, T] = {
     x = lattice.bottom
-    run(first, intra)
+    run(first)
     x
   }
 
@@ -212,10 +211,10 @@ trait WorklistFixpointSolverWithReachability[N] extends WorklistFixpointSolver[N
    */
   def unliftedAnalyze(intra: Boolean): lattice.sublattice.sublattice.Element = {
     import lattice.sublattice._
-    val res: lattice.Element = analyze(intra)
+    val res: lattice.Element = analyze()
     // Convert liftedResult to unlifted
     res.map((n, lift) => (n, lift match {
-      case Bottom => lattice.sublattice.sublattice.bottom
+      case LiftedBottom => lattice.sublattice.sublattice.bottom
       case Lift(a) => a
     })).asInstanceOf[lattice.sublattice.sublattice.Element]
   }
diff --git a/src/main/scala/util/RunUtils.scala b/src/main/scala/util/RunUtils.scala
index 96174dc7c..ef01dbbc4 100644
--- a/src/main/scala/util/RunUtils.scala
+++ b/src/main/scala/util/RunUtils.scala
@@ -154,7 +154,7 @@ object RunUtils {
 
     Logger.info("[!] Running MRA")
     val mraSolver = MemoryRegionAnalysisSolver(cfg, globalAddresses, globalOffsets, mergedSubroutines, constPropResult)
-    val mraResult = mraSolver.unliftedAnalyze()
+    val mraResult = mraSolver.analyze()
     memoryRegionAnalysisResults = mraResult
 
     config.analysisDotPath.foreach(s => writeToFile(cfg.toDot(Output.labeler(mraResult, true), Output.dotIder), s"${s}_mra$iteration.dot"))
@@ -166,7 +166,7 @@ object RunUtils {
 
     Logger.info("[!] Running VSA")
     val vsaSolver = ValueSetAnalysisSolver(cfg, globalAddresses, externalAddresses, globalOffsets, subroutines, mmm, constPropResult)
-    val vsaResult: Map[CfgNode, Map[Variable | MemoryRegion, Set[Value]]] = vsaSolver.unliftedAnalyze(true).asInstanceOf[Map[CfgNode, Map[Variable | MemoryRegion, Set[Value]]]]
+    val vsaResult: Map[CfgNode, Map[Variable | MemoryRegion, Set[Value]]] = vsaSolver.analyze().asInstanceOf[Map[CfgNode, Map[Variable | MemoryRegion, Set[Value]]]]
 
     config.analysisDotPath.foreach(s => writeToFile(cfg.toDot(Output.labeler(vsaResult, true), Output.dotIder), s"${s}_vsa$iteration.dot"))
     config.analysisResultsPath.foreach(s => writeToFile(printAnalysisResults(cfg, vsaResult, iteration), s"${s}_vsa$iteration.txt"))

From 9fe43c1e2f42afacb52b9c6d496426e23f4a4bcf Mon Sep 17 00:00:00 2001
From: yousifpatti <yousifpatti@gmail.com>
Date: Thu, 30 Nov 2023 11:19:47 +1000
Subject: [PATCH 24/29] fixing lattice type stage 1

---
 src/main/scala/analysis/Analysis.scala | 24 ++++++++++++------------
 1 file changed, 12 insertions(+), 12 deletions(-)

diff --git a/src/main/scala/analysis/Analysis.scala b/src/main/scala/analysis/Analysis.scala
index 8a55b4120..912039f4a 100644
--- a/src/main/scala/analysis/Analysis.scala
+++ b/src/main/scala/analysis/Analysis.scala
@@ -283,42 +283,42 @@ trait MemoryRegionAnalysis(val cfg: ProgramCfg,
  * Base class for memory region analysis with lifted lattice, where the extra bottom element represents "unreachable".
  */
 abstract class LiftedMemoryRegionAnalysis(
-                                  val cfg: ProgramCfg,
-                                  val globals: Map[BigInt, String],
-                                  val globalOffsets: Map[BigInt, BigInt],
-                                  val subroutines: Map[BigInt, String],
-                                  val constantProp: Map[CfgNode, Map[Variable, FlatElement[BitVecLiteral]]]
-                                ) extends IntraproceduralForwardDependencies
+            val cfg: ProgramCfg,
+            val globals: Map[BigInt, String],
+            val globalOffsets: Map[BigInt, BigInt],
+            val subroutines: Map[BigInt, String],
+            val constantProp: Map[CfgNode, Map[Variable, FlatElement[BitVecLiteral]]]
+          ) extends IntraproceduralForwardDependencies
   with MapLiftLatticeSolver[CfgNode, Set[MemoryRegion], PowersetLattice[MemoryRegion]]
   with MemoryRegionAnalysis(cfg, globals, globalOffsets, subroutines, constantProp) {
 
   /**
    * Lifted state lattice, with new bottom element representing "unreachable".
    */
-  val liftedstatelattice = LiftLattice(stateLattice)
+  val liftedstatelattice: LiftLattice[CfgNode, Map[CfgNode, Set[MemoryRegion]], MapLattice[CfgNode, Set[MemoryRegion], PowersetLattice[MemoryRegion]]] = LiftLattice(stateLattice)
 
   /**
    * The analysis lattice.
    */
-  val lattice = MapLattice(liftedstatelattice) // TODO: TYPING ISSUE
+  override val lattice: MapLattice[CfgNode, LiftedElement[Map[CfgNode, Set[MemoryRegion]]], liftedstatelattice.type] = MapLattice(liftedstatelattice) // TODO: TYPING ISSUE
 
-  val domain: Set[CfgNode] = cfg.nodes.toSet
+  override val domain: Set[CfgNode] = cfg.nodes.toSet
 
   /**
    * The worklist is initialized with all function entry nodes.
    */
-  val first: Set[CfgNode] = cfg.funEntries.toSet[CfgNode]
+  override 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: Map[CfgNode, Set[MemoryRegion]]): LiftedElement[Map[analysis.CfgNode, Set[analysis.MemoryRegion]]] = {
+  override def funsub(n: CfgNode, x: Map[CfgNode, Set[MemoryRegion]]): LiftedElement[Map[CfgNode, Set[MemoryRegion]]] = {
     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 _ => lift(stateLattice.bottom) //super.funsub(n, x) TODO: TYPING ISSUE
+      case _ => lift(super.funsub(n, x))
     }
   }
 }

From b296a509269e52f4aa032ecd40f591306b77df00 Mon Sep 17 00:00:00 2001
From: yousifpatti <yousifpatti@gmail.com>
Date: Thu, 30 Nov 2023 13:18:47 +1000
Subject: [PATCH 25/29] Small changes

---
 src/main/scala/analysis/Analysis.scala               | 5 ++---
 src/main/scala/analysis/solvers/FixPointSolver.scala | 2 +-
 2 files changed, 3 insertions(+), 4 deletions(-)

diff --git a/src/main/scala/analysis/Analysis.scala b/src/main/scala/analysis/Analysis.scala
index 912039f4a..2f6247380 100644
--- a/src/main/scala/analysis/Analysis.scala
+++ b/src/main/scala/analysis/Analysis.scala
@@ -289,7 +289,6 @@ abstract class LiftedMemoryRegionAnalysis(
             val subroutines: Map[BigInt, String],
             val constantProp: Map[CfgNode, Map[Variable, FlatElement[BitVecLiteral]]]
           ) extends IntraproceduralForwardDependencies
-  with MapLiftLatticeSolver[CfgNode, Set[MemoryRegion], PowersetLattice[MemoryRegion]]
   with MemoryRegionAnalysis(cfg, globals, globalOffsets, subroutines, constantProp) {
 
   /**
@@ -318,7 +317,7 @@ abstract class LiftedMemoryRegionAnalysis(
       // function entry nodes are always reachable (if intra-procedural analysis)
       case _: CfgFunctionEntryNode => lift(stateLattice.bottom)
       // all other nodes are processed with join+transfer
-      case _ => lift(super.funsub(n, x))
+      case _ => lift(Map(n -> super.funsub(n, x)))
     }
   }
 }
@@ -346,4 +345,4 @@ class MemoryRegionAnalysisSolver(
 ) extends LiftedMemoryRegionAnalysis(cfg, globals, globalOffsets, subroutines, constantProp)
     with LiftedValueAnalysisMisc
     with IntraproceduralForwardDependencies
-    with WorklistFixpointSolverWithReachability[CfgNode, Set[MemoryRegion], PowersetLattice[MemoryRegion]]
\ No newline at end of file
+    with WorklistFixpointSolverWithReachability[CfgNode, LiftedElement[Map[CfgNode, Set[MemoryRegion]]], LiftLattice[CfgNode, Map[CfgNode, Set[MemoryRegion]], MapLattice[CfgNode, Set[MemoryRegion], PowersetLattice[MemoryRegion]]]]
\ No newline at end of file
diff --git a/src/main/scala/analysis/solvers/FixPointSolver.scala b/src/main/scala/analysis/solvers/FixPointSolver.scala
index 9c8eba1c4..a566d18d0 100644
--- a/src/main/scala/analysis/solvers/FixPointSolver.scala
+++ b/src/main/scala/analysis/solvers/FixPointSolver.scala
@@ -52,7 +52,7 @@ trait MapLatticeSolver[N, T, L <: Lattice[T]] extends LatticeSolver[Map[N, T]] w
  * Base trait for solvers for map lattices with lifted co-domains.
  * @tparam N type of the elements in the map domain.
  */
-trait MapLiftLatticeSolver[N, T, L <: Lattice[T]] extends MapLatticeSolver[N, T, L] with Dependencies[N] {
+trait MapLiftLatticeSolver[N, T, L <: Lattice[T]] extends MapLatticeSolver[N, LiftedElement[T], LiftLattice[N, T, L]] with Dependencies[N] {
   val lattice: MapLattice[N, LiftedElement[T], LiftLattice[N, T, L]]
 
   /**

From b68020d3286ce0e9599fe8e6b0148ed326b697b3 Mon Sep 17 00:00:00 2001
From: yousifpatti <yousifpatti@gmail.com>
Date: Thu, 30 Nov 2023 13:57:37 +1000
Subject: [PATCH 26/29] More type changes

---
 src/main/scala/analysis/Analysis.scala            | 15 ++++++++-------
 .../scala/analysis/solvers/FixPointSolver.scala   |  4 ++--
 src/main/scala/util/RunUtils.scala                |  2 +-
 3 files changed, 11 insertions(+), 10 deletions(-)

diff --git a/src/main/scala/analysis/Analysis.scala b/src/main/scala/analysis/Analysis.scala
index 2f6247380..830a0b256 100644
--- a/src/main/scala/analysis/Analysis.scala
+++ b/src/main/scala/analysis/Analysis.scala
@@ -283,12 +283,13 @@ trait MemoryRegionAnalysis(val cfg: ProgramCfg,
  * Base class for memory region analysis with lifted lattice, where the extra bottom element represents "unreachable".
  */
 abstract class LiftedMemoryRegionAnalysis(
-            val cfg: ProgramCfg,
-            val globals: Map[BigInt, String],
-            val globalOffsets: Map[BigInt, BigInt],
-            val subroutines: Map[BigInt, String],
-            val constantProp: Map[CfgNode, Map[Variable, FlatElement[BitVecLiteral]]]
+            override val cfg: ProgramCfg,
+            override val globals: Map[BigInt, String],
+            override val globalOffsets: Map[BigInt, BigInt],
+            override val subroutines: Map[BigInt, String],
+            override val constantProp: Map[CfgNode, Map[Variable, FlatElement[BitVecLiteral]]]
           ) extends IntraproceduralForwardDependencies
+  with MapLatticeSolver[CfgNode, LiftedElement[Map[CfgNode, Set[MemoryRegion]]], LiftLattice[CfgNode, Map[CfgNode, Set[MemoryRegion]], MapLattice[CfgNode, Set[MemoryRegion], PowersetLattice[MemoryRegion]]]]
   with MemoryRegionAnalysis(cfg, globals, globalOffsets, subroutines, constantProp) {
 
   /**
@@ -311,13 +312,13 @@ abstract class LiftedMemoryRegionAnalysis(
   /**
    * Overrides `funsub` from [[tip.solvers.MapLatticeSolver]], treating function entry nodes as reachable.
    */
-  override def funsub(n: CfgNode, x: Map[CfgNode, Set[MemoryRegion]]): LiftedElement[Map[CfgNode, Set[MemoryRegion]]] = {
+  override def funsub(n: CfgNode, x: Map[CfgNode, LiftedElement[Map[CfgNode, Set[MemoryRegion]]]]): LiftedElement[Map[CfgNode, Set[MemoryRegion]]] = {
     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 _ => lift(Map(n -> super.funsub(n, x)))
+      case _ => super.funsub(n, x)
     }
   }
 }
diff --git a/src/main/scala/analysis/solvers/FixPointSolver.scala b/src/main/scala/analysis/solvers/FixPointSolver.scala
index a566d18d0..516f4a5c6 100644
--- a/src/main/scala/analysis/solvers/FixPointSolver.scala
+++ b/src/main/scala/analysis/solvers/FixPointSolver.scala
@@ -52,7 +52,7 @@ trait MapLatticeSolver[N, T, L <: Lattice[T]] extends LatticeSolver[Map[N, T]] w
  * Base trait for solvers for map lattices with lifted co-domains.
  * @tparam N type of the elements in the map domain.
  */
-trait MapLiftLatticeSolver[N, T, L <: Lattice[T]] extends MapLatticeSolver[N, LiftedElement[T], LiftLattice[N, T, L]] with Dependencies[N] {
+trait MapLiftLatticeSolver[N, T, L <: Lattice[T]] extends MapLatticeSolver[N, T, L] with Dependencies[N] {
   val lattice: MapLattice[N, LiftedElement[T], LiftLattice[N, T, L]]
 
   /**
@@ -209,7 +209,7 @@ trait WorklistFixpointSolverWithReachability[N, T, L <: Lattice[T]] extends Work
    * @param intra
    * @return the sub-sub-lattice
    */
-  def unliftedAnalyze(intra: Boolean): lattice.sublattice.sublattice.Element = {
+  def unliftedAnalyze(): lattice.sublattice.sublattice.Element = {
     import lattice.sublattice._
     val res: lattice.Element = analyze()
     // Convert liftedResult to unlifted
diff --git a/src/main/scala/util/RunUtils.scala b/src/main/scala/util/RunUtils.scala
index ef01dbbc4..8cddf48ff 100644
--- a/src/main/scala/util/RunUtils.scala
+++ b/src/main/scala/util/RunUtils.scala
@@ -154,7 +154,7 @@ object RunUtils {
 
     Logger.info("[!] Running MRA")
     val mraSolver = MemoryRegionAnalysisSolver(cfg, globalAddresses, globalOffsets, mergedSubroutines, constPropResult)
-    val mraResult = mraSolver.analyze()
+    val mraResult = mraSolver.unliftedAnalyze()
     memoryRegionAnalysisResults = mraResult
 
     config.analysisDotPath.foreach(s => writeToFile(cfg.toDot(Output.labeler(mraResult, true), Output.dotIder), s"${s}_mra$iteration.dot"))

From 8a4dd71f5b1570525577cba14ee55a4518cd8b17 Mon Sep 17 00:00:00 2001
From: yousifpatti <yousifpatti@gmail.com>
Date: Thu, 30 Nov 2023 14:04:07 +1000
Subject: [PATCH 27/29] Bug fix

---
 src/main/scala/analysis/solvers/FixPointSolver.scala | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/main/scala/analysis/solvers/FixPointSolver.scala b/src/main/scala/analysis/solvers/FixPointSolver.scala
index 516f4a5c6..72e904742 100644
--- a/src/main/scala/analysis/solvers/FixPointSolver.scala
+++ b/src/main/scala/analysis/solvers/FixPointSolver.scala
@@ -52,7 +52,7 @@ trait MapLatticeSolver[N, T, L <: Lattice[T]] extends LatticeSolver[Map[N, T]] w
  * Base trait for solvers for map lattices with lifted co-domains.
  * @tparam N type of the elements in the map domain.
  */
-trait MapLiftLatticeSolver[N, T, L <: Lattice[T]] extends MapLatticeSolver[N, T, L] with Dependencies[N] {
+trait MapLiftLatticeSolver[N, T, L <: Lattice[T]] extends MapLatticeSolver[N, LiftedElement[T], LiftLattice[N, T, L]] with Dependencies[N] {
   val lattice: MapLattice[N, LiftedElement[T], LiftLattice[N, T, L]]
 
   /**

From 270eca26b990dcdb9a3c0a3749a32a98b3101ac2 Mon Sep 17 00:00:00 2001
From: l-kent <l.kent@uq.edu.au>
Date: Fri, 1 Dec 2023 09:37:09 +1000
Subject: [PATCH 28/29] fix types with lifted lattice

---
 src/main/scala/analysis/Analysis.scala        | 95 +++++--------------
 src/main/scala/analysis/Lattice.scala         |  2 +-
 src/main/scala/analysis/MemoryModelMap.scala  | 26 ++---
 .../analysis/solvers/FixPointSolver.scala     | 32 ++-----
 src/main/scala/util/RunUtils.scala            |  6 +-
 .../scala/MemoryRegionAnalysisMiscTest.scala  |  6 +-
 6 files changed, 52 insertions(+), 115 deletions(-)

diff --git a/src/main/scala/analysis/Analysis.scala b/src/main/scala/analysis/Analysis.scala
index 830a0b256..fe275c0cd 100644
--- a/src/main/scala/analysis/Analysis.scala
+++ b/src/main/scala/analysis/Analysis.scala
@@ -161,17 +161,18 @@ trait MemoryRegionAnalysis(val cfg: ProgramCfg,
     buffers
   }
 
-  /** The lattice of abstract values.
-   */
   val regionLattice: PowersetLattice[MemoryRegion] = PowersetLattice()
 
-  /** The lattice of abstract states.
-   */
-  val stateLattice: MapLattice[CfgNode, Set[MemoryRegion], PowersetLattice[MemoryRegion]] = MapLattice(regionLattice)
+  /**
+    * Lifted memory region lattice, with new bottom element representing "unreachable".
+    */
+  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))
@@ -248,7 +249,7 @@ trait MemoryRegionAnalysis(val cfg: ProgramCfg,
           if (directCall.target.name == "malloc") {
             evaluateExpression(mallocVariable, constantProp(n)) match {
               case Some(b: BitVecLiteral) =>
-                stateLattice.sublattice.lub(s, Set(HeapRegion(nextMallocCount(), b)))
+                regionLattice.lub(s, Set(HeapRegion(nextMallocCount(), b)))
               case None => s
             }
           } else {
@@ -259,13 +260,13 @@ trait MemoryRegionAnalysis(val cfg: ProgramCfg,
             return s
           }
           val result = eval(memAssign.rhs.index, s, cmd)
-          stateLattice.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)
-              m = stateLattice.sublattice.lub(m, result)
+              m = regionLattice.lub(m, result)
             case _ => m
           }
           m
@@ -274,76 +275,26 @@ 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)
-}
-
-/**
- * Base class for memory region analysis with lifted lattice, where the extra bottom element represents "unreachable".
- */
-abstract class LiftedMemoryRegionAnalysis(
-            override val cfg: ProgramCfg,
-            override val globals: Map[BigInt, String],
-            override val globalOffsets: Map[BigInt, BigInt],
-            override val subroutines: Map[BigInt, String],
-            override val constantProp: Map[CfgNode, Map[Variable, FlatElement[BitVecLiteral]]]
-          ) extends IntraproceduralForwardDependencies
-  with MapLatticeSolver[CfgNode, LiftedElement[Map[CfgNode, Set[MemoryRegion]]], LiftLattice[CfgNode, Map[CfgNode, Set[MemoryRegion]], MapLattice[CfgNode, Set[MemoryRegion], PowersetLattice[MemoryRegion]]]]
-  with MemoryRegionAnalysis(cfg, globals, globalOffsets, subroutines, constantProp) {
-
-  /**
-   * Lifted state lattice, with new bottom element representing "unreachable".
-   */
-  val liftedstatelattice: LiftLattice[CfgNode, Map[CfgNode, Set[MemoryRegion]], MapLattice[CfgNode, Set[MemoryRegion], PowersetLattice[MemoryRegion]]] = LiftLattice(stateLattice)
-
-  /**
-   * The analysis lattice.
-   */
-  override val lattice: MapLattice[CfgNode, LiftedElement[Map[CfgNode, Set[MemoryRegion]]], liftedstatelattice.type] = MapLattice(liftedstatelattice) // TODO: TYPING ISSUE
-
-  override val domain: Set[CfgNode] = cfg.nodes.toSet
-
-  /**
-   * The worklist is initialized with all function entry nodes.
-   */
-  override 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: Map[CfgNode, LiftedElement[Map[CfgNode, Set[MemoryRegion]]]]): LiftedElement[Map[CfgNode, Set[MemoryRegion]]] = {
-    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)
-    }
-  }
-}
-
-/**
- * Functionality for basic analyses with lifted state lattice.
- */
-trait LiftedValueAnalysisMisc extends MemoryRegionAnalysis {
-
-  /**
-   * Transfer function for state lattice elements.
-   * (Same as `localTransfer` for basic analyses with lifted state lattice.)
-   */
   def transferUnlifted(n: CfgNode, s: Set[MemoryRegion]): Set[MemoryRegion] = localTransfer(n, s)
 }
 
-
-
 class MemoryRegionAnalysisSolver(
     cfg: ProgramCfg,
     globals: Map[BigInt, String],
     globalOffsets: Map[BigInt, BigInt],
     subroutines: Map[BigInt, String],
     constantProp: Map[CfgNode, Map[Variable, FlatElement[BitVecLiteral]]]
-) extends LiftedMemoryRegionAnalysis(cfg, globals, globalOffsets, subroutines, constantProp)
-    with LiftedValueAnalysisMisc
+) extends MemoryRegionAnalysis(cfg, globals, globalOffsets, subroutines, constantProp)
     with IntraproceduralForwardDependencies
-    with WorklistFixpointSolverWithReachability[CfgNode, LiftedElement[Map[CfgNode, Set[MemoryRegion]]], LiftLattice[CfgNode, Map[CfgNode, Set[MemoryRegion]], MapLattice[CfgNode, Set[MemoryRegion], PowersetLattice[MemoryRegion]]]]
\ No newline at end of file
+    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)
+    }
+  }
+}
\ No newline at end of file
diff --git a/src/main/scala/analysis/Lattice.scala b/src/main/scala/analysis/Lattice.scala
index d12bc7ba8..6f9cb5f41 100644
--- a/src/main/scala/analysis/Lattice.scala
+++ b/src/main/scala/analysis/Lattice.scala
@@ -43,7 +43,7 @@ case object LiftedBottom extends LiftedElement[Nothing] {
  * The lift lattice for `sublattice`.
  * Supports implicit lifting and unlifting.
  */
-class LiftLattice[N, T, +L <: Lattice[T]](val sublattice: L) extends Lattice[LiftedElement[T]] {
+class LiftLattice[T, +L <: Lattice[T]](val sublattice: L) extends Lattice[LiftedElement[T]] {
 
   val bottom: LiftedElement[T] = LiftedBottom
 
diff --git a/src/main/scala/analysis/MemoryModelMap.scala b/src/main/scala/analysis/MemoryModelMap.scala
index 1591725f6..7e4b5039d 100644
--- a/src/main/scala/analysis/MemoryModelMap.scala
+++ b/src/main/scala/analysis/MemoryModelMap.scala
@@ -44,27 +44,31 @@ 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
+
+          for (dataRgn <- allDataRgns) {
+            add(dataRgn.start.value, dataRgn)
+          }
+        case LiftedBottom =>
+    }
 
-      allStacks(exitNode.data.name) = stackRgns
 
-      for (dataRgn <- allDataRgns) {
-        add(dataRgn.start.value, dataRgn)
-      }
     )
   }
 
diff --git a/src/main/scala/analysis/solvers/FixPointSolver.scala b/src/main/scala/analysis/solvers/FixPointSolver.scala
index 72e904742..aa4e52d5c 100644
--- a/src/main/scala/analysis/solvers/FixPointSolver.scala
+++ b/src/main/scala/analysis/solvers/FixPointSolver.scala
@@ -52,19 +52,19 @@ trait MapLatticeSolver[N, T, L <: Lattice[T]] extends LatticeSolver[Map[N, T]] w
  * Base trait for solvers for map lattices with lifted co-domains.
  * @tparam N type of the elements in the map domain.
  */
-trait MapLiftLatticeSolver[N, T, L <: Lattice[T]] extends MapLatticeSolver[N, LiftedElement[T], LiftLattice[N, T, L]] with Dependencies[N] {
-  val lattice: MapLattice[N, LiftedElement[T], LiftLattice[N, T, L]]
+trait MapLiftLatticeSolver[N, T, L <: Lattice[T]] extends MapLatticeSolver[N, LiftedElement[T], LiftLattice[T, L]] with Dependencies[N] {
+
+  val lattice: MapLattice[N, LiftedElement[T], LiftLattice[T, L]]
 
   /**
    * The transfer function for the sub-sub-lattice.
    */
   def transferUnlifted(n: N, s: T): T
 
-  override def transfer(n: N, s: T): LiftedElement[T] = {
-    import lattice.sublattice._
+  override def transfer(n: N, s: LiftedElement[T]): LiftedElement[T] = {
     s match {
       case LiftedBottom => LiftedBottom // unreachable as input implied unreachable at output
-      case l: Lift[T] => lift(transferUnlifted(n, l.el))
+      case Lift(a) => lattice.sublattice.lift(transferUnlifted(n, a))
     }
   }
 }
@@ -189,35 +189,18 @@ trait SimpleWorklistFixpointSolver[N, T, L <: Lattice[T]] extends WorklistFixpoi
  *
  * This solver works for map lattices with lifted co-domains, where the extra bottom element typically represents "unreachable".
  */
-trait WorklistFixpointSolverWithReachability[N, T, L <: Lattice[T]] extends WorklistFixpointSolver[N, T, L] with MapLiftLatticeSolver[N, T, L] {
+trait WorklistFixpointSolverWithReachability[N, T, L <: Lattice[T]] extends WorklistFixpointSolver[N, LiftedElement[T], LiftLattice[T, L]] with MapLiftLatticeSolver[N, T, L] {
 
   /**
    * The start locations, used as the initial contents of the worklist.
    */
   val first: Set[N]
 
-  def analyze(): Map[N, T] = {
+  def analyze(): Map[N, LiftedElement[T]] = {
     x = lattice.bottom
     run(first)
     x
   }
-
-  /**
-   * The transfer function for the sub-sub-lattice. Unlifts the resulting MapLattice[N, LiftLattice[Lattice.sublattice]]
-   * to MapLattice[N, Lattice.sublattice.sublattice].
-   *
-   * @param intra
-   * @return the sub-sub-lattice
-   */
-  def unliftedAnalyze(): lattice.sublattice.sublattice.Element = {
-    import lattice.sublattice._
-    val res: lattice.Element = analyze()
-    // Convert liftedResult to unlifted
-    res.map((n, lift) => (n, lift match {
-      case LiftedBottom => lattice.sublattice.sublattice.bottom
-      case Lift(a) => a
-    })).asInstanceOf[lattice.sublattice.sublattice.Element]
-  }
 }
 
 /** A pushDown worklist-based fixpoint solvers. Pushes the results of the analysis one node down. This is used to have
@@ -248,7 +231,6 @@ trait PushDownWorklistFixpointSolver[N, T, L <: Lattice[T]] extends MapLatticeSo
   }
 
   def process(n: N): Unit =
-    //val y = funsub(n, x, intra)
     val xn = x(n)
     val y = transfer(n, xn)
 
diff --git a/src/main/scala/util/RunUtils.scala b/src/main/scala/util/RunUtils.scala
index 8cddf48ff..3df433fa4 100644
--- a/src/main/scala/util/RunUtils.scala
+++ b/src/main/scala/util/RunUtils.scala
@@ -22,7 +22,7 @@ import util.Logger
 import scala.collection.mutable
 
 object RunUtils {
-  var memoryRegionAnalysisResults: Map[CfgNode, Set[MemoryRegion]] = Map()
+  var memoryRegionAnalysisResults: Map[CfgNode, LiftedElement[Set[MemoryRegion]]] = Map()
 
   // ids reserved by boogie
   val reserved: Set[String] = Set("free")
@@ -154,7 +154,7 @@ object RunUtils {
 
     Logger.info("[!] Running MRA")
     val mraSolver = MemoryRegionAnalysisSolver(cfg, globalAddresses, globalOffsets, mergedSubroutines, constPropResult)
-    val mraResult = mraSolver.unliftedAnalyze()
+    val mraResult = mraSolver.analyze()
     memoryRegionAnalysisResults = mraResult
 
     config.analysisDotPath.foreach(s => writeToFile(cfg.toDot(Output.labeler(mraResult, true), Output.dotIder), s"${s}_mra$iteration.dot"))
@@ -245,7 +245,7 @@ object RunUtils {
     def printNode(node: CfgNode): Unit = {
       s.append(node)
       s.append(" :: ")
-      s.append(if result.contains(node) then result(node) else "Unreachable")
+      s.append(result(node))
       s.append(System.lineSeparator())
     }
 
diff --git a/src/test/scala/MemoryRegionAnalysisMiscTest.scala b/src/test/scala/MemoryRegionAnalysisMiscTest.scala
index 93cad362e..a25061293 100644
--- a/src/test/scala/MemoryRegionAnalysisMiscTest.scala
+++ b/src/test/scala/MemoryRegionAnalysisMiscTest.scala
@@ -1,9 +1,9 @@
-import analysis.{CfgNode, MemoryRegion}
+import analysis.{CfgNode, LiftedElement, MemoryRegion}
 import org.scalatest.Inside.inside
 import org.scalatest.*
 import org.scalatest.funsuite.*
 import util.RunUtils
-import util.{BASILConfig, ILLoadingConfig, BoogieGeneratorConfig, StaticAnalysisConfig, BoogieMemoryAccessMode}
+import util.{BASILConfig, BoogieGeneratorConfig, BoogieMemoryAccessMode, ILLoadingConfig, StaticAnalysisConfig}
 
 import java.io.{File, OutputStream, PrintStream, PrintWriter}
 class MemoryRegionAnalysisMiscTest extends AnyFunSuite with OneInstancePerTest {
@@ -15,7 +15,7 @@ class MemoryRegionAnalysisMiscTest extends AnyFunSuite with OneInstancePerTest {
   def runMain(name: String, dump: Boolean = false): Unit = {
     var expected = ""
     var actual = ""
-    var output: Map[CfgNode, Set[MemoryRegion]] = Map()
+    var output: Map[CfgNode, LiftedElement[Set[MemoryRegion]]] = Map()
     RunUtils.loadAndTranslate(
       BASILConfig(
         loading = ILLoadingConfig(

From 0c68b3fdeceb39859b18cd8199bf3e470364a0e2 Mon Sep 17 00:00:00 2001
From: yousifpatti <yousifpatti@gmail.com>
Date: Tue, 5 Dec 2023 12:06:58 +1000
Subject: [PATCH 29/29] Added LiftedLattice to VSA

---
 src/main/scala/analysis/MemoryModelMap.scala |  2 -
 src/main/scala/analysis/VSA.scala            | 64 +++++---------------
 src/main/scala/util/RunUtils.scala           | 48 ++++++++-------
 3 files changed, 42 insertions(+), 72 deletions(-)

diff --git a/src/main/scala/analysis/MemoryModelMap.scala b/src/main/scala/analysis/MemoryModelMap.scala
index 7e4b5039d..a33b7b6af 100644
--- a/src/main/scala/analysis/MemoryModelMap.scala
+++ b/src/main/scala/analysis/MemoryModelMap.scala
@@ -67,8 +67,6 @@ class MemoryModelMap {
           }
         case LiftedBottom =>
     }
-
-
     )
   }
 
diff --git a/src/main/scala/analysis/VSA.scala b/src/main/scala/analysis/VSA.scala
index d2cf1169d..a09a1c5f3 100644
--- a/src/main/scala/analysis/VSA.scala
+++ b/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
 
@@ -180,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(
@@ -193,49 +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]]]
-
-
-//abstract class IntraprocValueSetAnalysisWorklistSolver[L <: VSALatticeElem](
-//    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
-//) extends LiftedValueSetAnalysis(
-//    cfg,
-//    globals,
-//    externalFunctions,
-//    globalOffsets, subroutines,
-//    mmm,
-//    constantProp,
-//    true)
-//    with LiftedValueSetAnalysisMisc
-//    with WorklistFixpointSolverWithReachability[CfgNode]
-//    with ForwardDependencies
-//
-//object ValueSetAnalysis:
-//
-//  /** Interprocedural 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 InterprocValueSetAnalysisWorklistSolver(
-//        cfg,
-//        globals,
-//        externalFunctions,
-//        globalOffsets,
-//        subroutines,
-//        mmm,
-//        constantProp,
-//        MapLattice[Variable | MemoryRegion, PowersetLattice[Value]](PowersetLattice[Value])
-//      )
\ No newline at end of file
+    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)
+    }
+  }
+}
\ No newline at end of file
diff --git a/src/main/scala/util/RunUtils.scala b/src/main/scala/util/RunUtils.scala
index 3df433fa4..dd4173871 100644
--- a/src/main/scala/util/RunUtils.scala
+++ b/src/main/scala/util/RunUtils.scala
@@ -166,7 +166,7 @@ object RunUtils {
 
     Logger.info("[!] Running VSA")
     val vsaSolver = ValueSetAnalysisSolver(cfg, globalAddresses, externalAddresses, globalOffsets, subroutines, mmm, constPropResult)
-    val vsaResult: Map[CfgNode, Map[Variable | MemoryRegion, Set[Value]]] = vsaSolver.analyze().asInstanceOf[Map[CfgNode, Map[Variable | MemoryRegion, Set[Value]]]]
+    val vsaResult: Map[CfgNode, LiftedElement[Map[Variable | MemoryRegion, Set[Value]]]] = vsaSolver.analyze()
 
     config.analysisDotPath.foreach(s => writeToFile(cfg.toDot(Output.labeler(vsaResult, true), Output.dotIder), s"${s}_vsa$iteration.dot"))
     config.analysisResultsPath.foreach(s => writeToFile(printAnalysisResults(cfg, vsaResult, iteration), s"${s}_vsa$iteration.txt"))
@@ -267,7 +267,7 @@ object RunUtils {
 
   def resolveCFG(
       cfg: ProgramCfg,
-      valueSets: Map[CfgNode, Map[Variable | MemoryRegion, Set[Value]]],
+      valueSets: Map[CfgNode, LiftedElement[Map[Variable | MemoryRegion, Set[Value]]]],
       IRProgram: Program
   ): (Program, Boolean) = {
     var modified: Boolean = false
@@ -323,27 +323,31 @@ object RunUtils {
               // We want to replace all possible indirect calls based on this CFG, before regenerating it from the IR
               return
             }
-            val valueSet = valueSets(n)
-            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 newCall = DirectCall(targets.head, indirectCall.returnTarget, indirectCall.label)
-              block.jump = newCall
-            } else if (targets.size > 1) {
-              modified = true
-              val procedure = c.parent.data
-              val newBlocks = ArrayBuffer[Block]()
-              for (t <- targets) {
-                val assume = Assume(BinaryExpr(BVEQ, indirectCall.target, BitVecLiteral(t.address.get, 64)))
-                val newLabel: String = block.label + t.name
-                val directCall = DirectCall(t, indirectCall.returnTarget)
-                newBlocks.append(Block(newLabel, None, ArrayBuffer(assume), directCall))
+            valueSets(n) match {
+              case Lift(valueSet) =>
+                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 newCall = DirectCall(targets.head, indirectCall.returnTarget, indirectCall.label)
+                  block.jump = newCall
+                } else if (targets.size > 1) {
+                  modified = true
+                  val procedure = c.parent.data
+                  val newBlocks = ArrayBuffer[Block]()
+                  for (t <- targets) {
+                    val assume = Assume(BinaryExpr(BVEQ, indirectCall.target, BitVecLiteral(t.address.get, 64)))
+                    val newLabel: String = block.label + t.name
+                    val directCall = DirectCall(t, indirectCall.returnTarget)
+                    newBlocks.append(Block(newLabel, None, ArrayBuffer(assume), directCall))
+                  }
+                  procedure.blocks.addAll(newBlocks)
+                  val newCall = GoTo(newBlocks, indirectCall.label)
+                  block.jump = newCall
+                }
+              case LiftedBottom =>
               }
-              procedure.blocks.addAll(newBlocks)
-              val newCall = GoTo(newBlocks, indirectCall.label)
-              block.jump = newCall
-            }
           case _ =>
       case _ =>
     }