minor cleanup + add comment clarifying an issue

UQ-PAC · Jan 16, 2025 · 730a06c · 730a06c
1 parent 7def0b4
commit 730a06c
Show file tree

Hide file tree

Showing 5 changed files with 79 additions and 92 deletions.
diff --git a/src/main/scala/Main.scala b/src/main/scala/Main.scala
@@ -50,7 +50,7 @@ object Main {
     threadSplit: Flag,
     @arg(name = "summarise-procedures", doc = "Generates summaries of procedures which are used in pre/post-conditions (requires --analyse flag)")
     summariseProcedures: Flag,
-    @arg(name = "memory-regions", doc = "Performs static analysis to separate memory into discrete regions in Boogie output (requires --analyse flag) (mra|dsa)")
+    @arg(name = "memory-regions", doc = "Performs static analysis to separate memory into discrete regions in Boogie output (requires --analyse flag) (mra|dsa) (dsa is recommended over mra)")
     memoryRegions: Option[String],
     @arg(name = "no-irreducible-loops", doc = "Disable producing irreducible loops when --analyse is passed (does nothing without --analyse)")
     noIrreducibleLoops: Flag

diff --git a/src/main/scala/analysis/GlobalRegionAnalysis.scala b/src/main/scala/analysis/GlobalRegionAnalysis.scala
@@ -152,7 +152,8 @@ trait GlobalRegionAnalysis(
         checkIfDefined(regions, n)
       case assign: LocalAssign =>
         // this is a constant but we need to check if it is a data region
-        // size assumption of 1 here is ok, because it will get approximated later with strict mode
+        // TODO aefault value of 1 here causes problems as 1 is both used as a default and is also
+        //  a valid size for 1-byte accesses
         checkIfDefined(tryCoerceIntoData(assign.rhs, assign, 1, noLoad = true), n, strict = true)
       case _ =>
         Set()
@@ -162,13 +163,13 @@ trait GlobalRegionAnalysis(
 }
 
 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: Map[CFGPosition, LiftedElement[Map[Variable | MemoryRegion, Set[Value]]]]
-  ) extends GlobalRegionAnalysis(program, domain, constantProp, reachingDefs, mmm, vsaResult)
+  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: 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]]
diff --git a/src/main/scala/analysis/InterprocSteensgaardAnalysis.scala b/src/main/scala/analysis/InterprocSteensgaardAnalysis.scala
@@ -16,10 +16,10 @@ case class RegisterWrapperEqualSets(variable: Variable, ssa: FlatElement[Int])
  * expression node in the AST. It is implemented using [[analysis.solvers.UnionFindSolver]].
  */
 class InterprocSteensgaardAnalysis(
-      domain: Set[CFGPosition],
-      mmm: MemoryModelMap,
-      reachingDefs: Map[CFGPosition, (Map[Variable, FlatElement[Int]], Map[Variable, FlatElement[Int]])],
-      vsaResult: Map[CFGPosition, LiftedElement[Map[Variable | MemoryRegion, Set[Value]]]]) extends Analysis[Any] {
+  domain: Set[CFGPosition],
+  mmm: MemoryModelMap,
+  reachingDefs: Map[CFGPosition, (Map[Variable, FlatElement[Int]], Map[Variable, FlatElement[Int]])],
+) extends Analysis[Any] {
 
   val solver: UnionFindSolver[StTerm] = UnionFindSolver()
   val callSiteSummary: mutable.Map[DirectCall, Map[RegisterWrapperEqualSets, Set[RegisterWrapperEqualSets | MemoryRegion]]] = mutable.Map()
@@ -52,7 +52,7 @@ class InterprocSteensgaardAnalysis(
   def analyze(): Unit = {
     // generate the constraints by traversing the AST and solve them on-the-fly
     domain.foreach { p =>
-      visit(p, ())
+      visit(p)
     }
 
     // for every direct call in mmm.contextMapVSA the ctx is unified with the call site summary
@@ -85,65 +85,61 @@ class InterprocSteensgaardAnalysis(
    * @param arg
    *   unused for this visitor
    */
-  def visit(node: CFGPosition, arg: Unit): Unit = {
+  def visit(node: CFGPosition): Unit = {
     node match {
-      case cmd: Command =>
-        cmd match {
-          case directCall: DirectCall if directCall.target.name == "malloc" =>
-            // X = alloc P:  [[X]] = ↑[[alloc-i]]
-            val alloc = mmm.nodeToRegion(directCall).head
-            val defs = getSSADefinition(mallocVariable, directCall, reachingDefs)
-            unify(IdentifierVariable(RegisterWrapperEqualSets(mallocVariable, defs)), PointerRef(AllocVariable(alloc)))
-          case assign: LocalAssign =>
-            // TODO: unsound
-            val unwrapped = unwrapExprToVar(assign.rhs)
-            if (unwrapped.isDefined) {
-              // X1 = X2: [[X1]] = [[X2]]
-              val X1 = assign.lhs
-              val X2 = unwrapped.get
-              unify(IdentifierVariable(RegisterWrapperEqualSets(X1, getSSADefinition(X1, assign, reachingDefs))), IdentifierVariable(RegisterWrapperEqualSets(X2, getSSAUse(X2, assign, reachingDefs))))
-            } else {
-              // X1 = *X2: [[X2]] = ↑a ^ [[X1]] = a where a is a fresh term variable TODO: this rule has been adapted to match [[X1]] = ↑[[alloc_X2]]
-              val X1 = assign.lhs
-              val X2_star = mmm.nodeToRegion(node)
-              X2_star.foreach { x =>
-                unify(IdentifierVariable(RegisterWrapperEqualSets(X1, getSSADefinition(X1, assign, reachingDefs))), PointerRef(AllocVariable(x)))
-              }
-            }
-          case memoryStore: MemoryStore =>
-            // *X1 = X2: [[X1]] = ↑a ^ [[X2]] = a where a is a fresh term variable
-            val X1_star = mmm.nodeToRegion(node)
-            // TODO: This is not sound
-            val unwrapped = unwrapExprToVar(memoryStore.value)
-            if (unwrapped.isDefined) {
-              val X2 = unwrapped.get
-              val alpha = FreshVariable()
-              X1_star.foreach { x =>
-                //unify(PointerRef(AllocVariable(x)), PointerRef(alpha))
-                unify(IdentifierVariable(RegisterWrapperEqualSets(X2, getSSAUse(X2, memoryStore, reachingDefs))), PointerRef(AllocVariable(x)))
-              }
-              //unify(IdentifierVariable(RegisterWrapperEqualSets(X2, getSSAUse(X2, memoryStore, reachingDefs))), alpha)
-              //            X1_star.foreach { x =>
-              //              unify(PointerRef(AllocVariable(x)), IdentifierVariable(RegisterWrapperEqualSets(X2, getSSAUse(X2, memoryAssign, reachingDefs))))
-              //            }
-            }
-          case load: MemoryLoad =>
-            // TODO: unsound
-            val unwrapped = unwrapExprToVar(load.index)
-            if (unwrapped.isDefined) {
-              // X1 = X2: [[X1]] = [[X2]]
-              val X1 = load.lhs
-              val X2 = unwrapped.get
-              unify(IdentifierVariable(RegisterWrapperEqualSets(X1, getSSADefinition(X1, load, reachingDefs))), IdentifierVariable(RegisterWrapperEqualSets(X2, getSSAUse(X2, load, reachingDefs))))
-            } else {
-              // X1 = *X2: [[X2]] = ↑a ^ [[X1]] = a where a is a fresh term variable TODO: this rule has been adapted to match [[X1]] = ↑[[alloc_X2]]
-              val X1 = load.lhs
-              val X2_star = mmm.nodeToRegion(node)
-              X2_star.foreach { x =>
-                unify(IdentifierVariable(RegisterWrapperEqualSets(X1, getSSADefinition(X1, load, reachingDefs))), PointerRef(AllocVariable(x)))
-              }
-            }
-          case _ => // do nothing
+      case directCall: DirectCall if directCall.target.name == "malloc" =>
+        // X = alloc P:  [[X]] = ↑[[alloc-i]]
+        val alloc = mmm.nodeToRegion(directCall).head
+        val defs = getSSADefinition(mallocVariable, directCall, reachingDefs)
+        unify(IdentifierVariable(RegisterWrapperEqualSets(mallocVariable, defs)), PointerRef(AllocVariable(alloc)))
+      case assign: LocalAssign =>
+        // TODO: unsound
+        val unwrapped = unwrapExprToVar(assign.rhs)
+        if (unwrapped.isDefined) {
+          // X1 = X2: [[X1]] = [[X2]]
+          val X1 = assign.lhs
+          val X2 = unwrapped.get
+          unify(IdentifierVariable(RegisterWrapperEqualSets(X1, getSSADefinition(X1, assign, reachingDefs))), IdentifierVariable(RegisterWrapperEqualSets(X2, getSSAUse(X2, assign, reachingDefs))))
+        } else {
+          // X1 = *X2: [[X2]] = ↑a ^ [[X1]] = a where a is a fresh term variable TODO: this rule has been adapted to match [[X1]] = ↑[[alloc_X2]]
+          val X1 = assign.lhs
+          val X2_star = mmm.nodeToRegion(node)
+          X2_star.foreach { x =>
+            unify(IdentifierVariable(RegisterWrapperEqualSets(X1, getSSADefinition(X1, assign, reachingDefs))), PointerRef(AllocVariable(x)))
+          }
+        }
+      case memoryStore: MemoryStore =>
+        // *X1 = X2: [[X1]] = ↑a ^ [[X2]] = a where a is a fresh term variable
+        val X1_star = mmm.nodeToRegion(node)
+        // TODO: This is not sound
+        val unwrapped = unwrapExprToVar(memoryStore.value)
+        if (unwrapped.isDefined) {
+          val X2 = unwrapped.get
+          val alpha = FreshVariable()
+          X1_star.foreach { x =>
+            //unify(PointerRef(AllocVariable(x)), PointerRef(alpha))
+            unify(IdentifierVariable(RegisterWrapperEqualSets(X2, getSSAUse(X2, memoryStore, reachingDefs))), PointerRef(AllocVariable(x)))
+          }
+          //unify(IdentifierVariable(RegisterWrapperEqualSets(X2, getSSAUse(X2, memoryStore, reachingDefs))), alpha)
+          //            X1_star.foreach { x =>
+          //              unify(PointerRef(AllocVariable(x)), IdentifierVariable(RegisterWrapperEqualSets(X2, getSSAUse(X2, memoryAssign, reachingDefs))))
+          //            }
+        }
+      case load: MemoryLoad =>
+        // TODO: unsound
+        val unwrapped = unwrapExprToVar(load.index)
+        if (unwrapped.isDefined) {
+          // X1 = X2: [[X1]] = [[X2]]
+          val X1 = load.lhs
+          val X2 = unwrapped.get
+          unify(IdentifierVariable(RegisterWrapperEqualSets(X1, getSSADefinition(X1, load, reachingDefs))), IdentifierVariable(RegisterWrapperEqualSets(X2, getSSAUse(X2, load, reachingDefs))))
+        } else {
+          // X1 = *X2: [[X2]] = ↑a ^ [[X1]] = a where a is a fresh term variable TODO: this rule has been adapted to match [[X1]] = ↑[[alloc_X2]]
+          val X1 = load.lhs
+          val X2_star = mmm.nodeToRegion(node)
+          X2_star.foreach { x =>
+            unify(IdentifierVariable(RegisterWrapperEqualSets(X1, getSSADefinition(X1, load, reachingDefs))), PointerRef(AllocVariable(x)))
+          }
         }
       case _ => // do nothing
     }

diff --git a/src/main/scala/analysis/MemoryRegionAnalysis.scala b/src/main/scala/analysis/MemoryRegionAnalysis.scala
@@ -11,12 +11,7 @@ import scala.collection.mutable.ListBuffer
 trait MemoryRegionAnalysis(
   val program: Program,
   val domain: Set[CFGPosition],
-  val globals: Map[BigInt, String],
-  val globalOffsets: Map[BigInt, BigInt],
-  val subroutines: Map[BigInt, String],
   val constantProp: Map[CFGPosition, Map[Variable, FlatElement[BitVecLiteral]]],
-  val ANRResult: Map[CFGPosition, Set[Variable]],
-  val RNAResult: Map[CFGPosition, Set[Variable]],
   val reachingDefs: Map[CFGPosition, (Map[Variable, Set[Assign]], Map[Variable, Set[Assign]])],
   val graResult: Map[CFGPosition, Set[DataRegion]],
   val mmm: MemoryModelMap,
@@ -265,19 +260,14 @@ trait MemoryRegionAnalysis(
 }
 
 class MemoryRegionAnalysisSolver(
-    program: Program,
-    domain: Set[CFGPosition],
-    globals: Map[BigInt, String],
-    globalOffsets: Map[BigInt, BigInt],
-    subroutines: Map[BigInt, String],
-    constantProp: Map[CFGPosition, Map[Variable, FlatElement[BitVecLiteral]]],
-    ANRResult: Map[CFGPosition, Set[Variable]],
-    RNAResult: Map[CFGPosition, Set[Variable]],
-    reachingDefs: Map[CFGPosition, (Map[Variable, Set[Assign]], Map[Variable, Set[Assign]])],
-    graResult: Map[CFGPosition, Set[DataRegion]],
-    mmm: MemoryModelMap,
-    vsaResult: Map[CFGPosition, LiftedElement[Map[Variable | MemoryRegion, Set[Value]]]]
-  ) extends MemoryRegionAnalysis(program, domain, globals, globalOffsets, subroutines, constantProp, ANRResult, RNAResult, reachingDefs, graResult, mmm, vsaResult)
+  program: Program,
+  domain: Set[CFGPosition],
+  constantProp: Map[CFGPosition, Map[Variable, FlatElement[BitVecLiteral]]],
+  reachingDefs: Map[CFGPosition, (Map[Variable, Set[Assign]], Map[Variable, Set[Assign]])],
+  graResult: Map[CFGPosition, Set[DataRegion]],
+  mmm: MemoryModelMap,
+  vsaResult: Map[CFGPosition, LiftedElement[Map[Variable | MemoryRegion, Set[Value]]]]
+) extends MemoryRegionAnalysis(program, domain, constantProp, reachingDefs, graResult, mmm, vsaResult)
   with IRIntraproceduralForwardDependencies
   with Analysis[Map[CFGPosition, ((Set[StackRegion], Set[Variable]), Set[HeapRegion])]]
   with SimpleWorklistFixpointSolver[CFGPosition, ((Set[StackRegion], Set[Variable]), Set[HeapRegion]), TupleLattice[TupleLattice[PowersetLattice[StackRegion], PowersetLattice[Variable], Set[StackRegion], Set[Variable]], PowersetLattice[HeapRegion], (Set[StackRegion], Set[Variable]), Set[HeapRegion]]]
diff --git a/src/main/scala/util/RunUtils.scala b/src/main/scala/util/RunUtils.scala
@@ -408,7 +408,7 @@ object StaticAnalysis {
     val graResult = graSolver.analyze()
 
     Logger.debug("[!] Running MRA")
-    val mraSolver = MemoryRegionAnalysisSolver(IRProgram, domain.toSet, globalAddresses, globalOffsets, mergedSubroutines, interProcConstPropResult, ANRResult, RNAResult, reachingDefinitionsAnalysisResults, graResult, mmm, previousVSAResults)
+    val mraSolver = MemoryRegionAnalysisSolver(IRProgram, domain.toSet, interProcConstPropResult, reachingDefinitionsAnalysisResults, graResult, mmm, previousVSAResults)
     val mraResult = mraSolver.analyze()
 
     config.analysisDotPath.foreach { s =>
@@ -462,7 +462,7 @@ object StaticAnalysis {
     }
 
     Logger.debug("[!] Running Steensgaard")
-    val steensgaardSolver = InterprocSteensgaardAnalysis(interDomain.toSet, mmm, SSAResults, previousVSAResults)
+    val steensgaardSolver = InterprocSteensgaardAnalysis(interDomain.toSet, mmm, SSAResults)
     steensgaardSolver.analyze()
     val steensgaardResults = steensgaardSolver.pointsTo()