Added LiftedLattice to VSA

UQ-PAC · Dec 5, 2023 · 0c68b3f · 0c68b3f
1 parent 270eca2
commit 0c68b3f
Show file tree

Hide file tree

Showing 3 changed files with 42 additions and 72 deletions.
diff --git a/src/main/scala/analysis/MemoryModelMap.scala b/src/main/scala/analysis/MemoryModelMap.scala
@@ -67,8 +67,6 @@ class MemoryModelMap {
           }
         case LiftedBottom =>
     }
-
-
     )
   }
 

diff --git a/src/main/scala/analysis/VSA.scala b/src/main/scala/analysis/VSA.scala
@@ -41,7 +41,9 @@ trait ValueSetAnalysis(cfg: ProgramCfg,
 
   val mapLattice: MapLattice[Variable | MemoryRegion, Set[Value], PowersetLattice[Value]] = MapLattice(powersetLattice)
 
-  val lattice: MapLattice[CfgNode, Map[Variable | MemoryRegion, Set[Value]], mapLattice.type] = MapLattice(mapLattice)
+  val liftedLattice: LiftLattice[Map[Variable | MemoryRegion, Set[Value]], mapLattice.type] = LiftLattice(mapLattice)
+
+  val lattice: MapLattice[CfgNode, LiftedElement[Map[Variable | MemoryRegion, Set[Value]]], LiftLattice[Map[Variable | MemoryRegion, Set[Value]], mapLattice.type]] = MapLattice(liftedLattice)
 
   val domain: Set[CfgNode] = cfg.nodes.toSet
 
@@ -180,7 +182,7 @@ trait ValueSetAnalysis(cfg: ProgramCfg,
 
   /** Transfer function for state lattice elements. (Same as `localTransfer` for simple value analysis.)
     */
-  def transfer(n: CfgNode, s: Map[Variable | MemoryRegion, Set[Value]]): Map[Variable | MemoryRegion, Set[Value]] = localTransfer(n, s)
+  def transferUnlifted(n: CfgNode, s: Map[Variable | MemoryRegion, Set[Value]]): Map[Variable | MemoryRegion, Set[Value]] = localTransfer(n, s)
 }
 
 class ValueSetAnalysisSolver(
@@ -193,49 +195,15 @@ class ValueSetAnalysisSolver(
     constantProp: Map[CfgNode, Map[Variable, FlatElement[BitVecLiteral]]],
 ) extends ValueSetAnalysis(cfg, globals, externalFunctions, globalOffsets, subroutines, mmm, constantProp)
     with InterproceduralForwardDependencies
-    with SimpleMonotonicSolver[CfgNode, Map[Variable | MemoryRegion, Set[Value]], MapLattice[Variable | MemoryRegion, Set[Value], PowersetLattice[Value]]]
-
-
-//abstract class IntraprocValueSetAnalysisWorklistSolver[L <: VSALatticeElem](
-//    cfg: ProgramCfg,
-//    globals: Map[BigInt, String],
-//    externalFunctions: Map[BigInt, String],
-//    globalOffsets: Map[BigInt, BigInt],
-//    subroutines: Map[BigInt, String],
-//    mmm: MemoryModelMap,
-//    constantProp: Map[CfgNode, Map[Variable, ConstantPropagationLattice.Element]],
-//    val powersetLattice: L
-//) extends LiftedValueSetAnalysis(
-//    cfg,
-//    globals,
-//    externalFunctions,
-//    globalOffsets, subroutines,
-//    mmm,
-//    constantProp,
-//    true)
-//    with LiftedValueSetAnalysisMisc
-//    with WorklistFixpointSolverWithReachability[CfgNode]
-//    with ForwardDependencies
-//
-//object ValueSetAnalysis:
-//
-//  /** Interprocedural analysis that uses the worklist solver.
-//    */
-//  class WorklistSolver(
-//      cfg: ProgramCfg,
-//      globals: Map[BigInt, String],
-//      externalFunctions: Map[BigInt, String],
-//      globalOffsets: Map[BigInt, BigInt],
-//      subroutines: Map[BigInt, String],
-//      mmm: MemoryModelMap,
-//      constantProp: Map[CfgNode, Map[Variable, ConstantPropagationLattice.Element]]
-//  ) extends InterprocValueSetAnalysisWorklistSolver(
-//        cfg,
-//        globals,
-//        externalFunctions,
-//        globalOffsets,
-//        subroutines,
-//        mmm,
-//        constantProp,
-//        MapLattice[Variable | MemoryRegion, PowersetLattice[Value]](PowersetLattice[Value])
-//      )
+    with Analysis[Map[CfgNode, LiftedElement[Map[Variable | MemoryRegion, Set[Value]]]]]
+    with WorklistFixpointSolverWithReachability[CfgNode, Map[Variable | MemoryRegion, Set[Value]], MapLattice[Variable | MemoryRegion, Set[Value], PowersetLattice[Value]]] {
+
+  override def funsub(n: CfgNode, x: Map[CfgNode, LiftedElement[Map[Variable | MemoryRegion, Set[Value]]]]): LiftedElement[Map[Variable | MemoryRegion, Set[Value]]] = {
+    n match {
+      // function entry nodes are always reachable as this is intraprocedural
+      case _: CfgFunctionEntryNode => liftedLattice.lift(mapLattice.bottom)
+      // all other nodes are processed with join+transfer
+      case _ => super.funsub(n, x)
+    }
+  }
+}
diff --git a/src/main/scala/util/RunUtils.scala b/src/main/scala/util/RunUtils.scala
@@ -166,7 +166,7 @@ object RunUtils {
 
     Logger.info("[!] Running VSA")
     val vsaSolver = ValueSetAnalysisSolver(cfg, globalAddresses, externalAddresses, globalOffsets, subroutines, mmm, constPropResult)
-    val vsaResult: Map[CfgNode, Map[Variable | MemoryRegion, Set[Value]]] = vsaSolver.analyze().asInstanceOf[Map[CfgNode, Map[Variable | MemoryRegion, Set[Value]]]]
+    val vsaResult: Map[CfgNode, LiftedElement[Map[Variable | MemoryRegion, Set[Value]]]] = vsaSolver.analyze()
 
     config.analysisDotPath.foreach(s => writeToFile(cfg.toDot(Output.labeler(vsaResult, true), Output.dotIder), s"${s}_vsa$iteration.dot"))
     config.analysisResultsPath.foreach(s => writeToFile(printAnalysisResults(cfg, vsaResult, iteration), s"${s}_vsa$iteration.txt"))
@@ -267,7 +267,7 @@ object RunUtils {
 
   def resolveCFG(
       cfg: ProgramCfg,
-      valueSets: Map[CfgNode, Map[Variable | MemoryRegion, Set[Value]]],
+      valueSets: Map[CfgNode, LiftedElement[Map[Variable | MemoryRegion, Set[Value]]]],
       IRProgram: Program
   ): (Program, Boolean) = {
     var modified: Boolean = false
@@ -323,27 +323,31 @@ object RunUtils {
               // We want to replace all possible indirect calls based on this CFG, before regenerating it from the IR
               return
             }
-            val valueSet = valueSets(n)
-            val targetNames = resolveAddresses(valueSet(indirectCall.target)).map(_.name).toList.sorted
-            val targets = targetNames.map(name => IRProgram.procedures.filter(_.name.equals(name)).head)
-            if (targets.size == 1) {
-              modified = true
-              val newCall = DirectCall(targets.head, indirectCall.returnTarget, indirectCall.label)
-              block.jump = newCall
-            } else if (targets.size > 1) {
-              modified = true
-              val procedure = c.parent.data
-              val newBlocks = ArrayBuffer[Block]()
-              for (t <- targets) {
-                val assume = Assume(BinaryExpr(BVEQ, indirectCall.target, BitVecLiteral(t.address.get, 64)))
-                val newLabel: String = block.label + t.name
-                val directCall = DirectCall(t, indirectCall.returnTarget)
-                newBlocks.append(Block(newLabel, None, ArrayBuffer(assume), directCall))
+            valueSets(n) match {
+              case Lift(valueSet) =>
+                val targetNames = resolveAddresses(valueSet(indirectCall.target)).map(_.name).toList.sorted
+                val targets = targetNames.map(name => IRProgram.procedures.filter(_.name.equals(name)).head)
+
+                if (targets.size == 1) {
+                  modified = true
+                  val newCall = DirectCall(targets.head, indirectCall.returnTarget, indirectCall.label)
+                  block.jump = newCall
+                } else if (targets.size > 1) {
+                  modified = true
+                  val procedure = c.parent.data
+                  val newBlocks = ArrayBuffer[Block]()
+                  for (t <- targets) {
+                    val assume = Assume(BinaryExpr(BVEQ, indirectCall.target, BitVecLiteral(t.address.get, 64)))
+                    val newLabel: String = block.label + t.name
+                    val directCall = DirectCall(t, indirectCall.returnTarget)
+                    newBlocks.append(Block(newLabel, None, ArrayBuffer(assume), directCall))
+                  }
+                  procedure.blocks.addAll(newBlocks)
+                  val newCall = GoTo(newBlocks, indirectCall.label)
+                  block.jump = newCall
+                }
+              case LiftedBottom =>
               }
-              procedure.blocks.addAll(newBlocks)
-              val newCall = GoTo(newBlocks, indirectCall.label)
-              block.jump = newCall
-            }
           case _ =>
       case _ =>
     }
-Original file line number
+Diff line change
@@ Expand Up / @@ -67,8 +67,6 @@ class MemoryModelMap { @@
               }
             case LiftedBottom =>
         }
         )
       }
@@ Expand Down @@