From 63d59091d01638f80aa8ab48269ae2a38a2cbb4d Mon Sep 17 00:00:00 2001 From: yousifpatti Date: Tue, 24 Oct 2023 17:18:22 +1000 Subject: [PATCH] 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()