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"))