From 4ecdc7d43749cdb81013e7cb17628f2cd6337602 Mon Sep 17 00:00:00 2001 From: yousifpatti Date: Wed, 29 Nov 2023 17:12:10 +1000 Subject: [PATCH] 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"))