MMM global regions values adjusted

UQ-PAC · Feb 6, 2024 · fbe0bce · fbe0bce
1 parent a95bb6d
commit fbe0bce
Show file tree

Hide file tree

Showing 4 changed files with 50 additions and 8 deletions.
diff --git a/src/main/scala/analysis/Analysis.scala b/src/main/scala/analysis/Analysis.scala
@@ -250,7 +250,17 @@ trait MemoryRegionAnalysis(val cfg: ProgramCfg,
   }
 
   def resolveGlobalOffset(address: BitVecLiteral): DataRegion = {
-    val tableAddress = globalOffsets.getOrElse(address.value, address.value)
+    var tableAddress = globalOffsets.getOrElse(address.value, address.value)
+    // addresses may be layered as in jumptable2 example for recursive search required
+    var exitLoop = false
+    while (globalOffsets.contains(tableAddress) && !exitLoop) {
+      val newAddress = globalOffsets.getOrElse(tableAddress, tableAddress)
+      if (newAddress == tableAddress) {
+        exitLoop = true
+      } else {
+        tableAddress = newAddress
+      }
+    }
     var name = "@ERROR"
     if (globals.contains(tableAddress)) {
       name = globals(tableAddress)
@@ -310,7 +320,12 @@ trait MemoryRegionAnalysis(val cfg: ProgramCfg,
         if (ctx.contains(reg)) {
           ctx(reg) match {
             case FlatEl(al) =>
-              val regions = eval(al, Set.empty, n)
+              val regions = al match {
+                case memoryLoad: MemoryLoad =>
+                    eval(memoryLoad.index, Set.empty, n)
+                case _ =>
+                    eval(al, Set.empty, n)
+              }
               evaluateExpression(binExpr.arg2, constantProp(n)) match {
                 case Some(b: BitVecLiteral) =>
                   regions.foreach {
@@ -325,7 +340,7 @@ trait MemoryRegionAnalysis(val cfg: ProgramCfg,
                       val nextOffset = BinaryExpr(op = BVADD, arg1 = dataRegion.start, arg2 = b)
                       evaluateExpression(nextOffset, constantProp(n)) match {
                         case Some(b2: BitVecLiteral) =>
-                          reducedRegions = reducedRegions + poolMaster(b2, n.parent.data)
+                          reducedRegions = reducedRegions + resolveGlobalOffset(b2)
                         case None =>
                       }
                     case _ =>
@@ -334,6 +349,11 @@ trait MemoryRegionAnalysis(val cfg: ProgramCfg,
               }
           }
         }
+        evaluateExpression(binExpr, constantProp(n)) match {
+            case Some(b: BitVecLiteral) =>
+                reducedRegions = reducedRegions + resolveGlobalOffset(b)
+            case None =>
+        }
       case _ =>
     }
     reducedRegions

diff --git a/src/main/scala/analysis/InterprocSteensgaardAnalysis.scala b/src/main/scala/analysis/InterprocSteensgaardAnalysis.scala
@@ -68,7 +68,12 @@ class InterprocSteensgaardAnalysis(
         if (ctx.contains(reg)) {
           ctx(reg) match {
             case FlatEl(al) =>
-              val regions = exprToRegion(al, n)
+              val regions = al match {
+                case loadL: MemoryLoad =>
+                  exprToRegion(loadL.index, n)
+                case _ =>
+                  exprToRegion(al, n)
+              }
               evaluateExpressionWithSSA(binExpr.arg2, constantProp(n)).foreach (
                 b =>
                   regions.foreach {

diff --git a/src/main/scala/analysis/MemoryModelMap.scala b/src/main/scala/analysis/MemoryModelMap.scala
@@ -49,9 +49,26 @@ class MemoryModelMap {
     }
   }
 
-  def convertMemoryRegions(memoryRegions: Map[CfgNode, LiftedElement[Set[MemoryRegion]]], externalFunctions: Map[BigInt, String], procedureToSharedRegions: mutable.Map[Procedure, mutable.Set[MemoryRegion]]): Unit = {
+  def resolveInverseGlobalOffset(name: String, address: BitVecLiteral, globalOffsets: Map[BigInt, BigInt]): DataRegion = {
+    val inverseGlobalOffsets = globalOffsets.map(_.swap)
+    var tableAddress = inverseGlobalOffsets.getOrElse(address.value, address.value)
+    // addresses may be layered as in jumptable2 example for recursive search required
+    var exitLoop = false
+    while (inverseGlobalOffsets.contains(tableAddress) && !exitLoop) {
+      val newAddress = inverseGlobalOffsets.getOrElse(tableAddress, tableAddress)
+      if (newAddress == tableAddress) {
+        exitLoop = true
+      } else {
+        tableAddress = newAddress
+      }
+    }
+
+    DataRegion(name, BitVecLiteral(tableAddress, 64))
+  }
+
+  def convertMemoryRegions(memoryRegions: Map[CfgNode, LiftedElement[Set[MemoryRegion]]], externalFunctions: Map[BigInt, String], globalOffsets: Map[BigInt, BigInt], procedureToSharedRegions: mutable.Map[Procedure, mutable.Set[MemoryRegion]]): Unit = {
     // map externalFunctions name, value to DataRegion(name, value) and then sort by value
-    val externalFunctionRgns = externalFunctions.map((offset, name) => DataRegion(name, BitVecLiteral(offset, 64)))
+    val externalFunctionRgns = externalFunctions.map((offset, name) => resolveInverseGlobalOffset(name, BitVecLiteral(offset, 64), globalOffsets))
 
     // we should collect all data regions otherwise the ordering might be wrong
     var dataRgns: Set[DataRegion] = Set.empty

diff --git a/src/main/scala/util/RunUtils.scala b/src/main/scala/util/RunUtils.scala
@@ -219,7 +219,7 @@ object RunUtils {
 
     Logger.info("[!] Running MMM")
     val mmm = MemoryModelMap()
-    mmm.convertMemoryRegions(mraResult, mergedSubroutines, mraSolver.procedureToSharedRegions)
+    mmm.convertMemoryRegions(mraResult, mergedSubroutines, globalOffsets, mraSolver.procedureToSharedRegions)
 
     Logger.info("[!] Running Steensgaard")
     val steensgaardSolver = InterprocSteensgaardAnalysis(cfg, constPropResultWithSSA, RegToResult, mmm)
@@ -248,7 +248,7 @@ object RunUtils {
     }
     Logger.info(s"[!] Finished indirect call resolution after $iteration iterations")
 
-    mmm.printRegionsContent(true)
+    mmm.printRegionsContent(false)
 
     newIR
   }