Added reducible regions

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

Hide file tree

Showing 3 changed files with 89 additions and 3 deletions.
diff --git a/src/main/scala/analysis/Analysis.scala b/src/main/scala/analysis/Analysis.scala
@@ -164,7 +164,6 @@ trait ConstantPropagationWithSSA(val cfg: ProgramCfg) {
           // assignments
           case la: LocalAssign =>
             if (s.contains(RegisterVariableWrapper(la.lhs))) {
-                println("Contains")
                 s + (RegisterVariableWrapper(la.lhs) -> s(RegisterVariableWrapper(la.lhs)).union(eval(la.rhs, s)))
             } else {
               s + (RegisterVariableWrapper(la.lhs) -> eval(la.rhs, s))
@@ -302,6 +301,44 @@ trait MemoryRegionAnalysis(val cfg: ProgramCfg,
   val registerToRegions: mutable.Map[RegisterVariableWrapper, mutable.Set[MemoryRegion]] = mutable.Map()
   val procedureToSharedRegions: mutable.Map[Procedure, mutable.Set[MemoryRegion]] = mutable.Map()
 
+  def reducibleToRegion(binExpr: BinaryExpr, n: CfgCommandNode): Set[MemoryRegion] = {
+    var reducedRegions = Set.empty[MemoryRegion]
+    binExpr.arg1 match {
+      case variable: Variable =>
+        val reg = RegisterVariableWrapper(variable)
+        val ctx = RegToResult(n)
+        if (ctx.contains(reg)) {
+          ctx(reg) match {
+            case FlatEl(al) =>
+              val regions = eval(al, Set.empty, n)
+              evaluateExpression(binExpr.arg2, constantProp(n)) match {
+                case Some(b: BitVecLiteral) =>
+                  regions.foreach {
+                    case stackRegion: StackRegion =>
+                      val nextOffset = BinaryExpr(op = BVADD, arg1 = stackRegion.start, arg2 = b)
+                      evaluateExpression(nextOffset, constantProp(n)) match {
+                        case Some(b2: BitVecLiteral) =>
+                          reducedRegions = reducedRegions + poolMaster(b2, n.parent.data)
+                        case None =>
+                      }
+                    case dataRegion: DataRegion =>
+                      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)
+                        case None =>
+                      }
+                    case _ =>
+                  }
+                case None =>
+              }
+          }
+        }
+      case _ =>
+    }
+    reducedRegions
+  }
+
   def eval(exp: Expr, env: Set[MemoryRegion], n: CfgCommandNode): Set[MemoryRegion] = {
     Logger.debug(s"evaluating $exp")
     Logger.debug(s"env: $env")
@@ -313,6 +350,8 @@ trait MemoryRegionAnalysis(val cfg: ProgramCfg,
             case Some(b: BitVecLiteral) => Set(poolMaster(b, n.parent.data))
             case None => env
           }
+        } else if (reducibleToRegion(binOp, n).nonEmpty) {
+          reducibleToRegion(binOp, n)
         } else {
           evaluateExpression(binOp, constantProp(n)) match {
             case Some(b: BitVecLiteral) => eval(b, env, n)

diff --git a/src/main/scala/analysis/InterprocSteensgaardAnalysis.scala b/src/main/scala/analysis/InterprocSteensgaardAnalysis.scala
@@ -59,6 +59,44 @@ class InterprocSteensgaardAnalysis(
     s"stack_$stackCount"
   }
 
+  def reducibleToRegion(binExpr: BinaryExpr, n: CfgCommandNode): Set[MemoryRegion] = {
+    var reducedRegions = Set.empty[MemoryRegion]
+    binExpr.arg1 match {
+      case variable: Variable =>
+        val reg = RegisterVariableWrapper(variable)
+        val ctx = RegToResult(n)
+        if (ctx.contains(reg)) {
+          ctx(reg) match {
+            case FlatEl(al) =>
+              val regions = exprToRegion(al, n)
+              evaluateExpressionWithSSA(binExpr.arg2, constantProp(n)).foreach (
+                b =>
+                  regions.foreach {
+                    case stackRegion: StackRegion =>
+                      val nextOffset = BinaryExpr(op = BVADD, arg1 = stackRegion.start, arg2 = b)
+                      evaluateExpressionWithSSA(nextOffset, constantProp(n)).foreach (
+                        b2 => reducedRegions = reducedRegions ++ exprToRegion(BinaryExpr(op = BVADD, arg1 = Register("R31", BitVecType(64)), arg2 = b2), n)
+                      )
+                    case dataRegion: DataRegion =>
+                      val nextOffset = BinaryExpr(op = BVADD, arg1 = dataRegion.start, arg2 = b)
+                      evaluateExpressionWithSSA(nextOffset, constantProp(n)).foreach(
+                        b2 => reducedRegions = reducedRegions ++ exprToRegion(b2, n)
+                      )
+                    case _ =>
+                  }
+              )
+          }
+        }
+        evaluateExpressionWithSSA(binExpr, constantProp(n)).foreach (
+          b =>
+            val region = mmm.findDataObject(b.value)
+            reducedRegions = reducedRegions ++ region
+        )
+      case _ =>
+    }
+    reducedRegions
+  }
+
   def exprToRegion(expr: Expr, n: CfgCommandNode): Set[MemoryRegion] = {
     var res = Set[MemoryRegion]()
     mmm.popContext()
@@ -73,6 +111,9 @@ class InterprocSteensgaardAnalysis(
             }
         }
         res
+      case binaryExpr: BinaryExpr =>
+        res = res ++ reducibleToRegion(binaryExpr, n)
+        res
       case _ =>
         evaluateExpressionWithSSA(expr, constantProp(n)).foreach {
           case b: BitVecLiteral =>
@@ -82,14 +123,17 @@ class InterprocSteensgaardAnalysis(
               res = res + region.get
             }
         }
-        if (res.isEmpty && expr.isInstanceOf[Variable]) {
+        if (res.isEmpty && expr.isInstanceOf[Variable]) { // may be passed as param
           val ctx = RegToResult(n)
           if (ctx.contains(RegisterVariableWrapper(expr.asInstanceOf[Variable]))) {
             ctx(RegisterVariableWrapper(expr.asInstanceOf[Variable])) match {
               case FlatEl(al) =>
                 al match
                   case load: MemoryLoad => // treat as a region
                     res = res ++ exprToRegion(load.index, n)
+                  case binaryExpr: BinaryExpr =>
+                    res = res ++ reducibleToRegion(binaryExpr, n)
+                    res = res ++ exprToRegion(al, n)
                   case _ => // also treat as a region (for now) even if just Base + Offset without memLoad
                     res = res ++ exprToRegion(al, n)
             }
@@ -221,7 +265,7 @@ class InterprocSteensgaardAnalysis(
               x =>
                 unify(exprToStTerm(x), PointerRef(alpha))
                 x.content.addAll(X2)
-                x.content.addAll(possibleRegions)
+                x.content.addAll(possibleRegions.filter(r => r != x))
             )
             X2.foreach(
               x => unify(alpha, exprToStTerm(x))

diff --git a/src/main/scala/analysis/UtilMethods.scala b/src/main/scala/analysis/UtilMethods.scala
@@ -85,6 +85,9 @@ def evaluateExpressionWithSSA(exp: Expr, constantPropResult: Map[RegisterVariabl
             case BVASHR => apply(BitVectorEval.smt_bvashr, lhs, rhs)
             case BVCOMP => apply(BitVectorEval.smt_bvcomp, lhs, rhs)
             case BVCONCAT => apply(BitVectorEval.smt_concat, lhs, rhs)
+            case BVLSHR => apply(BitVectorEval.smt_bvlshr, lhs, rhs)
+            case BVSHL => apply(BitVectorEval.smt_bvshl, lhs, rhs)
+            case BVOR => apply(BitVectorEval.smt_bvor, lhs, rhs)
             case _ => throw new RuntimeException("Binary operation support not implemented: " + binOp.op)
           }
       }