Skip to content

Commit

Permalink
Resolving type issues
Browse files Browse the repository at this point in the history
  • Loading branch information
@yousifpatti
yousifpatti committed Nov 29, 2023
1 parent b04ec03 commit 4ecdc7d
Show file tree
Hide file tree
Showing 5 changed files with 69 additions and 130 deletions.
154 changes: 47 additions & 107 deletions src/main/scala/analysis/Analysis.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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)) {
Expand Down Expand Up @@ -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

Expand Down Expand Up @@ -232,23 +232,23 @@ 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")
}
}

/** Transfer function for state lattice elements.
*/
*/
def localTransfer(n: CfgNode, s: Set[MemoryRegion]): Set[MemoryRegion] = n match {
case cmd: CfgCommandNode =>
cmd.data match {
case directCall: DirectCall =>
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 {
Expand All @@ -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.
Expand All @@ -317,93 +312,38 @@ 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],
globalOffsets: Map[BigInt, BigInt],
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
// )
with WorklistFixpointSolverWithReachability[CfgNode, Set[MemoryRegion], PowersetLattice[MemoryRegion]]
14 changes: 7 additions & 7 deletions src/main/scala/analysis/Lattice.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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"
Expand All @@ -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

Expand Down Expand Up @@ -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.
*/
Expand Down
4 changes: 2 additions & 2 deletions src/main/scala/analysis/MemoryModelMap.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
23 changes: 11 additions & 12 deletions src/main/scala/analysis/solvers/FixPointSolver.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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))
}
}
}
Expand Down Expand Up @@ -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
}

Expand All @@ -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]
}
Expand Down
4 changes: 2 additions & 2 deletions src/main/scala/util/RunUtils.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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"))
Expand All @@ -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"))
Expand Down

0 comments on commit 4ecdc7d

Please sign in to comment.