More type changes

UQ-PAC · Nov 30, 2023 · b68020d · b68020d
1 parent b296a50
commit b68020d
Show file tree

Hide file tree

Showing 3 changed files with 11 additions and 10 deletions.
diff --git 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
@@ -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
@@ -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"))