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)