Memory Region and VSA bug fixes

src/main/scala/analysis/BitVectorEval.scala

@@ -338,4 +338,30 @@ object BitVectorEval {
       smt_zero_extend(i, s)
     }
   }
+
+  def bitVec_min(s: BitVecLiteral, t: BitVecLiteral): BitVecLiteral = {
+    if (smt_bvslt(s, t) == TrueLiteral) s else t
+  }
+
+  def bitVec_min(s: List[BitVecLiteral]): BitVecLiteral = {
+    s.reduce(bitVec_min)
+  }
+
+  def bitVec_max(s: BitVecLiteral, t: BitVecLiteral): BitVecLiteral = {
+    if (smt_bvslt(s, t) == TrueLiteral) t else s
+  }
+
+  def bitVec_max(s: List[BitVecLiteral]): BitVecLiteral = {
+    s.reduce(bitVec_max)
+  }
+
+  @tailrec
+  def bitVec_gcd(a: BitVecLiteral, b: BitVecLiteral): BitVecLiteral = {
+    if (b.value == 0) a else bitVec_gcd(b, smt_bvsmod(a, b))
+  }
+
+  def bitVec_interval(lb: BitVecLiteral, ub: BitVecLiteral, step: BitVecLiteral): Set[BitVecLiteral] = {
+    require(smt_bvule(lb, ub) == TrueLiteral, "Lower bound must be less than or equal to upper bound")
+    (lb.value to ub.value by step.value).map(BitVecLiteral(_, lb.size)).toSet
+  }
 }

src/main/scala/analysis/GlobalRegionAnalysis.scala

@@ -66,10 +66,11 @@ trait GlobalRegionAnalysis(val program: Program,
     tableAddress
   }
 
-  def tryCoerceIntoData(exp: Expr, n: Command, subAccess: BigInt, loadOp: Boolean = false): Set[DataRegion] = {
+  def tryCoerceIntoData(exp: Expr, n: Command, subAccess: BigInt): Set[DataRegion] = {
     val eval = evaluateExpression(exp, constantProp(n))
     if (eval.isDefined) {
-      Set(dataPoolMaster(eval.get.value, subAccess))
+      val index = eval.get.value
+      Set(dataPoolMaster(index, subAccess))
     } else {
       exp match {
         case literal: BitVecLiteral => tryCoerceIntoData(literal, n, subAccess)
@@ -81,7 +82,7 @@ trait GlobalRegionAnalysis(val program: Program,
         case BinaryExpr(op, arg1, arg2) =>
           val evalArg2 = evaluateExpression(arg2, constantProp(n))
           if (evalArg2.isDefined) {
-            tryCoerceIntoData(arg1, n, subAccess, true) flatMap { i =>
+            tryCoerceIntoData(arg1, n, subAccess) flatMap { i =>
               val newExpr = BinaryExpr(op, BitVecLiteral(i.start, evalArg2.get.size), evalArg2.get)
               tryCoerceIntoData(newExpr, n, subAccess)
             }
@@ -91,52 +92,20 @@ trait GlobalRegionAnalysis(val program: Program,
         case _: MemoryLoad => ???
         case _: UninterpretedFunction => Set.empty
         case variable: Variable =>
-          val ctx = getUse(variable, n, reachingDefs)
-          val collage = ctx.flatMap { i =>
-            if (i != n) {
-              val regions: Set[DataRegion] = vsaResult.get(i) match {
-                case Some(Lift(el)) =>
-                  el.getOrElse(i.lhs, Set()).flatMap {
-                    case AddressValue(region) =>
-                      el.getOrElse(region, Set()).flatMap {
-                        case AddressValue(dataRegion: DataRegion) => Some(dataRegion)
-                        case _ => None
-                      }
-                    case _ => Set()
-                  }
+          val collage: Set[DataRegion] = vsaResult.get(n) match {
+            case Some(Lift(el)) =>
+              el.getOrElse(variable, Set()).flatMap {
+                case AddressValue(dataRegion2: DataRegion) => Some(dataRegion2)
                 case _ => Set()
               }
-              if (regions.isEmpty) {
-                localTransfer(i, Set())
-              } else {
-                regions
-              }
-            } else {
-              Set()
-            }
-          }
-          collage.map { i =>
-            if (!loadOp) {
-              mmm.relocatedDataRegion(i.start).getOrElse(i)
-            } else {
-              resolveGlobalOffsetSecondLast(i)
-            }
+            case _ => Set()
           }
+          return collage
         case _ => Set()
       }
     }
   }
 
-  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
-      Set(dataPoolMaster(indexValueBigInt, size))
-    } else {
-      tryCoerceIntoData(index, n, size)
-    }
-  }
-
   /**
    * Check if the data region is defined.
    * Finds full and partial matches
@@ -149,35 +118,48 @@ trait GlobalRegionAnalysis(val program: Program,
    * @return Set[DataRegion]
    */
   def checkIfDefined(dataRegions: Set[DataRegion], n: CFGPosition): Set[DataRegion] = {
-    dataRegions.map { i =>
+    var converted: Set[DataRegion] = Set.empty
+    dataRegions.foreach { i =>
       val (f, p) = mmm.findDataObjectWithSize(i.start, i.size)
       val accesses = f.union(p)
       if (accesses.isEmpty) {
         i
       } else if (accesses.size == 1) {
-        dataMap(i.start) = DataRegion(i.regionIdentifier, i.start, i.size.max(accesses.head.size))
-        dataMap(i.start)
+        if (f.contains(accesses.head)) {
+          // full access
+          dataMap(i.start) = DataRegion(i.regionIdentifier, i.start, i.size.max(accesses.head.size))
+          converted = converted ++ Set(dataMap(i.start))
+        } else {
+          // partial access (we cannot determine the size)
+          dataMap(i.start) = DataRegion(i.regionIdentifier, i.start, i.size)
+          converted = converted ++ Set(dataMap(i.start))
+        }
       } else {
-        val highestRegion = accesses.maxBy(_.start)
-        dataMap(i.start) = DataRegion(i.regionIdentifier, i.start, i.size.max(highestRegion.end - i.start))
-        dataMap(i.start)
+  //        val highestRegion = accesses.maxBy(_.start)
+  //        dataMap(i.start) = DataRegion(i.regionIdentifier, i.start, i.size.max(highestRegion.end - i.start))
+  //        dataMap(i.start)
+        dataMap.remove(i.start)
+        accesses.foreach(a => dataMap(a.start) = dataPoolMaster(a.start, a.size))
+        converted = converted ++ accesses.collect({ case a => dataMap(a.start) })
       }
     }
+    converted
   }
 
   /** Transfer function for state lattice elements.
    */
   def localTransfer(n: CFGPosition, s: Set[DataRegion]): Set[DataRegion] = {
     n match {
       case memAssign: MemoryAssign =>
-        checkIfDefined(evalMemLoadToGlobal(memAssign.index, memAssign.size, memAssign), n)
+        return checkIfDefined(tryCoerceIntoData(memAssign.index, memAssign, memAssign.size), n)
       case assign: Assign =>
         val unwrapped = unwrapExpr(assign.rhs)
         if (unwrapped.isDefined) {
-          checkIfDefined(evalMemLoadToGlobal(unwrapped.get.index, unwrapped.get.size, assign, loadOp = true), n)
+          val regions: Set[DataRegion] = tryCoerceIntoData(unwrapped.get.index, assign, unwrapped.get.size)
+          return checkIfDefined(regions, n)
         } else {
           // this is a constant but we need to check if it is a data region
-          checkIfDefined(evalMemLoadToGlobal(assign.rhs, 1, assign), n)
+          return checkIfDefined(tryCoerceIntoData(assign.rhs, assign, 1), n)
         }
       case _ =>
         Set()

src/main/scala/analysis/Lattice.scala

@@ -2,31 +2,32 @@ package analysis
 
 import ir._
 import analysis.BitVectorEval
+import math.pow
 import util.Logger
 
 /** Basic lattice
-  */
+ */
 trait Lattice[T]:
 
   type Element = T
   /** The bottom element of this lattice.
-    */
+   */
   val bottom: T
 
   /** The top element of this lattice. Default: not implemented.
-    */
+   */
   def top: T = ???
 
   /** The least upper bound of `x` and `y`.
-    */
+   */
   def lub(x: T, y: T): T
 
   /** Returns true whenever `x` <= `y`.
-    */
+   */
   def leq(x: T, y: T): Boolean = lub(x, y) == y // rarely used, but easy to implement :-)
 
 /** The powerset lattice of a set of elements of type `A` with subset ordering.
-  */
+ */
 class PowersetLattice[A] extends Lattice[Set[A]] {
   val bottom: Set[A] = Set.empty
   def lub(x: Set[A], y: Set[A]): Set[A] = x.union(y)
@@ -104,8 +105,8 @@ 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.
-  */
+ * other element. No additional ordering is defined.
+ */
 class FlatLattice[X] extends Lattice[FlatElement[X]] {
 
   val bottom: FlatElement[X] = Bottom
@@ -140,18 +141,17 @@ class TupleLattice[L1 <: Lattice[T1], L2 <: Lattice[T2], T1, T2](val lattice1: L
   override def top: (T1, T2) = (lattice1.top, lattice2.top)
 }
 
-
 /** A lattice of maps from a set of elements of type `A` to a lattice with element `L'. Bottom is the default value.
-  */
+ */
 class MapLattice[A, T, +L <: Lattice[T]](val sublattice: L) extends Lattice[Map[A, T]] {
   val bottom: Map[A, T] = Map().withDefaultValue(sublattice.bottom)
   def lub(x: Map[A, T], y: Map[A, T]): Map[A, T] =
     x.keys.foldLeft(y)((m, a) => m + (a -> sublattice.lub(x(a), y(a)))).withDefaultValue(sublattice.bottom)
 }
 
 /** Constant propagation lattice.
-  *
-  */
+ *
+ */
 class ConstantPropagationLattice extends FlatLattice[BitVecLiteral] {
   private def apply(op: (BitVecLiteral, BitVecLiteral) => BitVecLiteral, a: FlatElement[BitVecLiteral], b: FlatElement[BitVecLiteral]): FlatElement[BitVecLiteral] = try {
     (a, b) match

src/main/scala/analysis/MemoryModelMap.scala

@@ -18,7 +18,7 @@ case class RangeKey(start: BigInt, end: BigInt) extends Ordered[RangeKey]:
   override def toString: String = s"Range[$start, $end] (size: $size)"
 
 // Custom data structure for storing range-to-object mappings
-class MemoryModelMap(val globalOffsets: Map[BigInt, BigInt]) {
+class MemoryModelMap(val globalOffsets: Map[BigInt, BigInt], val externalFunctions: Map[BigInt, String], val globalAddresses: Map[BigInt, String], val globalSizes: Map[String, Int]) {
   private val contextStack = mutable.Stack.empty[String]
   private val sharedContextStack = mutable.Stack.empty[List[StackRegion]]
   private val localStacks = mutable.Map[String, List[StackRegion]]().withDefaultValue(List.empty)
@@ -118,7 +118,7 @@ class MemoryModelMap(val globalOffsets: Map[BigInt, BigInt]) {
   // size of pointer is 8 bytes
   private val SIZE_OF_POINTER = 8
 
-  def preLoadGlobals(externalFunctions: Map[BigInt, String], globalAddresses: Map[BigInt, String], globalSizes: Map[String, Int]): Unit = {
+  def preLoadGlobals(): Unit = {
     val relocRegions = globalOffsets.keys.map(offset => DataRegion(nextRelocCount(), offset, SIZE_OF_POINTER))
 
     // map externalFunctions name, value to DataRegion(name, value) and then sort by value
@@ -136,6 +136,10 @@ class MemoryModelMap(val globalOffsets: Map[BigInt, BigInt]) {
     relocatedAddressesMap = globalOffsets.map { (offset, offset2) =>
       (offset, findDataObject(offset2).get)
     }
+
+    relocatedAddressesMap.foreach((offset, region) => {
+      relfContent(region) = relfContent.getOrElse(region, mutable.Set()) += region.regionIdentifier
+    })
   }
 
   def relocatedDataRegion(value: BigInt): Option[DataRegion] = {
@@ -285,10 +289,10 @@ class MemoryModelMap(val globalOffsets: Map[BigInt, BigInt]) {
           case _: DataRegion => "  "
       }
       Logger.debug(s"$spacing$range -> $region")
-      if content.contains(region) then
-        if content.contains(region) then
-          for value <- content(region) do
-            Logger.debug(s"$spacing    $value")
+      region match
+        case region1: DataRegion if relfContent.contains(region1) => for value <- relfContent(region1) do
+          Logger.debug(s"$spacing    $value")
+        case _ =>
     }
     Logger.debug("Stack:")
     for name <- localStacks.keys do
@@ -364,14 +368,24 @@ class MemoryModelMap(val globalOffsets: Map[BigInt, BigInt]) {
     heapCalls(directCall)
   }
 
+  def getHeapRegions: Set[HeapRegion] = {
+    heapMap.values.toSet
+  }
+
   def getStack(allocationSite: CFGPosition): Set[StackRegion] = {
     stackAllocationSites.getOrElse(allocationSite, Set.empty).map(returnRegion)
   }
 
+  def getLocalStacks: mutable.Map[String, List[StackRegion]] = localStacks
+
   def getData(cfgPosition: CFGPosition): Set[DataRegion] = {
     cfgPositionToDataRegion.getOrElse(cfgPosition, Set.empty).map(returnRegion)
   }
 
+  def getDataRegions: Set[DataRegion] = {
+    dataMap.values.toSet
+  }
+
   def nodeToRegion(n: CFGPosition): Set[MemoryRegion] = {
     n match {
       case directCall: DirectCall =>
@@ -380,6 +394,14 @@ class MemoryModelMap(val globalOffsets: Map[BigInt, BigInt]) {
         getStack(n) ++ getData(n)
     }
   }
+
+  def getOffset(region: MemoryRegion): BigInt = {
+    region match {
+      case s: StackRegion => s.start
+      case d: DataRegion => d.start
+      case h: HeapRegion => h.start
+    }
+  }
 }
 
 trait MemoryRegion {

src/main/scala/analysis/MemoryRegionAnalysis.scala

@@ -103,7 +103,7 @@ trait MemoryRegionAnalysis(val program: Program,
       case variable: Variable if !spList.contains(variable) =>
         evaluateExpression(binExpr.arg2, constantProp(n)) match {
           case Some(b: BitVecLiteral) =>
-            val ctx = getUse(variable, n, reachingDefs)
+            val ctx = getUse(variable, n, reachingDefs).filter(assign => unwrapExpr(assign.rhs).isEmpty)
             for {
               i <- ctx
               stackRegion <- eval(i.rhs, Set.empty, i, subAccess)