Adding Memory Regions to IR #231
There are no files selected for viewing
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,23 @@ | ||
| #include <stdio.h> | ||
|
|
||
| // Function declarations | ||
| int addNumbers(int a, int b); | ||
|
|
||
| int callAddFromAnotherFunction(int x, int y) { | ||
| return addNumbers(x, y); | ||
| } | ||
|
|
||
| int callFromFun2(int x, int y) { | ||
| return addNumbers(x, y); | ||
| } | ||
|
|
||
| int addNumbers(int a, int b) { | ||
| return a + b; | ||
| } | ||
|
|
||
| int main() { | ||
| int resultFromMain = addNumbers(10, 5); | ||
| int resultFromOtherFunc = callAddFromAnotherFunction(20, 15); | ||
| int resultFromFun2 = callFromFun2(30, 25); | ||
| return 0; | ||
| } |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
|
There was a problem hiding this comment. What does this analysis actually do & why do we need it to be separate from the MRA? There was a problem hiding this comment. This analysis only evaluates data regions and MRA evaluates the remaining stack and heap regions. MRA uses the results of GRA to skip statements that are already evaluated to data regions There was a problem hiding this comment. Why do we need separate analyses for that then? There was a problem hiding this comment. It was to separate the eval and transfer functions. They can be merged by bringing the functions over. I will work on that |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,247 @@ | ||
| package analysis | ||
|
|
||
| import analysis.solvers.SimpleWorklistFixpointSolver | ||
| import ir.* | ||
|
|
||
| import scala.collection.mutable | ||
|
|
||
| trait GlobalRegionAnalysis(val program: Program, | ||
| val domain: Set[CFGPosition], | ||
| val constantProp: Map[CFGPosition, Map[Variable, FlatElement[BitVecLiteral]]], | ||
| val reachingDefs: Map[CFGPosition, (Map[Variable, Set[Assign]], Map[Variable, Set[Assign]])], | ||
| val mmm: MemoryModelMap, | ||
| val vsaResult: Option[Map[CFGPosition, LiftedElement[Map[Variable | MemoryRegion, Set[Value]]]]]) { | ||
|
There was a problem hiding this comment. it doesn't really make sense to have a Map inside an Option - you can just use an empty Map as the default instead of None. |
||
|
|
||
| var dataCount: Int = 0 | ||
| private def nextDataCount() = { | ||
| dataCount += 1 | ||
| s"data_$dataCount" | ||
| } | ||
|
|
||
| val regionLattice: PowersetLattice[DataRegion] = PowersetLattice() | ||
|
|
||
| val lattice: MapLattice[CFGPosition, Set[DataRegion], PowersetLattice[DataRegion]] = MapLattice(regionLattice) | ||
|
|
||
| val first: Set[CFGPosition] = Set.empty + program.mainProcedure | ||
|
|
||
| private val stackPointer = Register("R31", 64) | ||
| private val linkRegister = Register("R30", 64) | ||
| private val framePointer = Register("R29", 64) | ||
| private val mallocVariable = Register("R0", 64) | ||
|
|
||
| private val dataMap: mutable.HashMap[BigInt, DataRegion] = mutable.HashMap() | ||
|
|
||
| private def dataPoolMaster(offset: BigInt, size: BigInt): Option[DataRegion] = { | ||
| assert(size >= 0) | ||
| if (dataMap.contains(offset)) { | ||
| if (dataMap(offset).size < (size.toDouble / 8).ceil.toInt) { | ||
| dataMap(offset) = DataRegion(dataMap(offset).regionIdentifier, offset, (size.toDouble / 8).ceil.toInt) | ||
| Some(dataMap(offset)) | ||
| } else { | ||
| Some(dataMap(offset)) | ||
| } | ||
| } else { | ||
| dataMap(offset) = DataRegion(nextDataCount(), offset, (size.toDouble / 8).ceil.toInt) | ||
| Some(dataMap(offset)) | ||
| } | ||
| } | ||
|
There was a problem hiding this comment. Why does this need to return an Option when it never returns None? |
||
|
|
||
| def getDataMap: mutable.HashMap[BigInt, DataRegion] = dataMap | ||
|
|
||
| /** | ||
| * For DataRegions, the actual address used needs to be converted to the relocated address. | ||
| * This is because when regions are found, the relocated address is used and as such match | ||
| * the correct range. | ||
| * | ||
| * @param address: The starting DataRegion | ||
| * @return DataRegion: The relocated data region if any | ||
| */ | ||
| def resolveGlobalOffsetSecondLast(address: DataRegion): DataRegion = { | ||
| var tableAddress = address | ||
| // addresses may be layered as in jumptable2 example for which recursive search is required | ||
| var exitLoop = false | ||
| while (mmm.relocatedDataRegion(tableAddress.start).isDefined && mmm.relocatedDataRegion(mmm.relocatedDataRegion(tableAddress.start).get.start).isDefined && !exitLoop) { | ||
| val newAddress = mmm.relocatedDataRegion(tableAddress.start).getOrElse(tableAddress) | ||
| if (newAddress == tableAddress) { | ||
| exitLoop = true | ||
| } else { | ||
| tableAddress = newAddress | ||
| } | ||
| } | ||
| tableAddress | ||
| } | ||
|
|
||
| def tryCoerceIntoData(exp: Expr, n: Command, subAccess: BigInt, loadOp: Boolean = false): Set[DataRegion] = { | ||
|
There was a problem hiding this comment. I don't really understand how this method works, can you explain it? I don't really follow why BinaryExprs are such a special case for it? |
||
| val eval = evaluateExpression(exp, constantProp(n)) | ||
| if (eval.isDefined) { | ||
| val region = dataPoolMaster(eval.get.value, subAccess) | ||
| if (region.isDefined) { | ||
| return Set(region.get) | ||
| } | ||
| } | ||
| exp match | ||
| case literal: BitVecLiteral => tryCoerceIntoData(literal, n, subAccess) | ||
| case Extract(end, start, body) => tryCoerceIntoData(body, n, subAccess) | ||
| case Repeat(repeats, body) => tryCoerceIntoData(body, n, subAccess) | ||
| case ZeroExtend(extension, body) => tryCoerceIntoData(body, n, subAccess) | ||
| case SignExtend(extension, body) => tryCoerceIntoData(body, n, subAccess) | ||
| case UnaryExpr(op, arg) => tryCoerceIntoData(arg, n, subAccess) | ||
|
There was a problem hiding this comment. None of these are robust ways of trying to identify which data regions an expression points to. You can't just ignore these operations like this, it will give incorrect results. |
||
| case BinaryExpr(op, arg1, arg2) => | ||
| val evalArg2 = evaluateExpression(arg2, constantProp(n)) | ||
| if (evalArg2.isDefined) { | ||
| val firstArg = tryCoerceIntoData(arg1, n, subAccess, true) | ||
| var regions = Set.empty[DataRegion] | ||
| for (i <- firstArg) { | ||
| val newExpr = BinaryExpr(op, BitVecLiteral(i.start, evalArg2.get.size), evalArg2.get) | ||
| regions = regions ++ tryCoerceIntoData(newExpr, n, subAccess) | ||
| } | ||
| return regions | ||
| } | ||
| Set.empty | ||
| case MemoryLoad(mem, index, endian, size) => ??? | ||
| case UninterpretedFunction(name, params, returnType) => Set.empty | ||
| case variable: Variable => | ||
| val ctx = getUse(variable, n, reachingDefs) | ||
| var collage = Set.empty[DataRegion] | ||
| for (i <- ctx) { | ||
| if (i != n) { | ||
| var tryVisit = Set.empty[DataRegion] | ||
| if (vsaResult.isDefined) { | ||
| vsaResult.get.get(i) match | ||
| case Some(value) => value match | ||
| case Lift(el) => el.get(i.lhs) match | ||
| case Some(value) => value.map { | ||
| case addressValue: AddressValue => | ||
| // find what the region contains | ||
| vsaResult.get.get(i) match | ||
| case Some(value) => value match | ||
| case Lift(el) => el.get(addressValue.region) match | ||
| case Some(value) => value.map { | ||
| case addressValue: AddressValue => | ||
| addressValue.region match | ||
| case region: DataRegion => | ||
| tryVisit = tryVisit + region | ||
| case _ => | ||
| case literalValue: LiteralValue => | ||
| } | ||
| case None => | ||
| case LiftedBottom => | ||
| case _ => | ||
| case None => | ||
| case literalValue: LiteralValue => | ||
| } | ||
| case None => | ||
| case LiftedBottom => | ||
| case _ => | ||
| case None => | ||
| } | ||
|
There was a problem hiding this comment. This seems overly convoluted |
||
| if (tryVisit.isEmpty) { | ||
| tryVisit = localTransfer(i, Set.empty) | ||
| } | ||
| if (tryVisit.nonEmpty) { | ||
| collage = collage ++ tryVisit | ||
| } | ||
| } | ||
| } | ||
| collage.map(i => | ||
| val resolved = resolveGlobalOffsetSecondLast(i) | ||
| if !loadOp then mmm.relocatedDataRegion(i.start).getOrElse(i) else resolved) | ||
| case _ => Set.empty | ||
| } | ||
|
|
||
| def evalMemLoadToGlobal(index: Expr, size: BigInt, n: Command, loadOp: Boolean = false): Set[DataRegion] = { | ||
| val indexValue = evaluateExpression(index, constantProp(n)) | ||
| if (indexValue.isDefined) { | ||
| val indexValueBigInt = indexValue.get.value | ||
| val region = dataPoolMaster(indexValueBigInt, size) | ||
| if (region.isDefined) { | ||
| return Set(region.get) | ||
| } | ||
| } | ||
| tryCoerceIntoData(index, n, size) | ||
| } | ||
|
|
||
| // def mergeRegions(regions: Set[DataRegion]): DataRegion = { | ||
| // if (regions.size == 1) { | ||
| // return regions.head | ||
| // } | ||
| // val start = regions.minBy(_.start).start | ||
| // val end = regions.maxBy(_.end).end | ||
| // val size = end - start | ||
| // val newRegion = DataRegion(nextDataCount(), start, size) | ||
| // regions.foreach(i => dataMap(i.start) = newRegion) | ||
| // newRegion | ||
| // } | ||
|
|
||
| /** | ||
| * Check if the data region is defined. | ||
| * Finds full and partial matches | ||
| * Full matches sizes are altered to match the size of the data region | ||
| * Partial matches are not altered | ||
| * Otherwise the data region is returned | ||
| * | ||
| * @param dataRegions Set[DataRegion] | ||
| * @param n CFGPosition | ||
| * @return Set[DataRegion] | ||
| */ | ||
| def checkIfDefined(dataRegions: Set[DataRegion], n: CFGPosition): Set[DataRegion] = { | ||
| var returnSet = Set.empty[DataRegion] | ||
| for (i <- dataRegions) { | ||
| val (f, p) = mmm.findDataObjectWithSize(i.start, i.size) | ||
| val accesses = f.union(p) | ||
| if (accesses.isEmpty) { | ||
| returnSet = returnSet + i | ||
| } else { | ||
| if (accesses.size == 1) { | ||
| dataMap(i.start) = DataRegion(i.regionIdentifier, i.start, i.size.max(accesses.head.size)) | ||
| returnSet = returnSet + dataMap(i.start) | ||
| } else if (accesses.size > 1) { | ||
| val highestRegion = accesses.maxBy(_.start) | ||
| dataMap(i.start) = DataRegion(i.regionIdentifier, i.start, i.size.max(highestRegion.end - i.start)) | ||
| returnSet = returnSet + dataMap(i.start) | ||
| } | ||
| } | ||
| } | ||
| if (returnSet.size > 1) { | ||
| mmm.addMergeRegions(returnSet.asInstanceOf[Set[MemoryRegion]], nextDataCount()) | ||
| } | ||
| returnSet | ||
| } | ||
|
|
||
| /** Transfer function for state lattice elements. | ||
| */ | ||
| def localTransfer(n: CFGPosition, s: Set[DataRegion]): Set[DataRegion] = { | ||
| n match { | ||
| case cmd: Command => | ||
| cmd match { | ||
| case memAssign: MemoryAssign => | ||
| return checkIfDefined(evalMemLoadToGlobal(memAssign.index, memAssign.size, cmd), n) | ||
| case assign: Assign => | ||
| val unwrapped = unwrapExpr(assign.rhs) | ||
| if (unwrapped.isDefined) { | ||
| return checkIfDefined(evalMemLoadToGlobal(unwrapped.get.index, unwrapped.get.size, cmd, loadOp = true), n) | ||
| } else { | ||
| // this is a constant but we need to check if it is a data region | ||
| return checkIfDefined(evalMemLoadToGlobal(assign.rhs, 1, cmd), n) | ||
| } | ||
| case _ => | ||
| } | ||
| case _ => | ||
| } | ||
| Set.empty | ||
| } | ||
|
|
||
| def transfer(n: CFGPosition, s: Set[DataRegion]): Set[DataRegion] = localTransfer(n, s) | ||
| } | ||
|
|
||
| class GlobalRegionAnalysisSolver( | ||
| program: Program, | ||
| domain: Set[CFGPosition], | ||
| constantProp: Map[CFGPosition, Map[Variable, FlatElement[BitVecLiteral]]], | ||
| reachingDefs: Map[CFGPosition, (Map[Variable, Set[Assign]], Map[Variable, Set[Assign]])], | ||
| mmm: MemoryModelMap, | ||
| vsaResult: Option[Map[CFGPosition, LiftedElement[Map[Variable | MemoryRegion, Set[Value]]]]] | ||
| ) extends GlobalRegionAnalysis(program, domain, constantProp, reachingDefs, mmm, vsaResult) | ||
| with IRIntraproceduralForwardDependencies | ||
| with Analysis[Map[CFGPosition, Set[DataRegion]]] | ||
| with SimpleWorklistFixpointSolver[CFGPosition, Set[DataRegion], PowersetLattice[DataRegion]] | ||
Oops, something went wrong.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Please don't commit unnecessary files like this