started lifted VSA but some issues marked with TODO

src/main/scala/analysis/Analysis.scala

@@ -364,7 +364,7 @@ trait MemoryRegionAnalysisMisc:
             */
             s ++ Set((n, result))
           case localAssign: LocalAssign =>
-            var m = s
+            val m = s
             unwrapExpr(localAssign.rhs).foreach {
               case memoryLoad: MemoryLoad =>
                 val result = eval(memoryLoad.index, s, n)
@@ -417,9 +417,8 @@ abstract class LiftedMemoryRegionAnalysis[P <: ProgramCfg](
   val globals: Map[BigInt, String],
   val globalOffsets: Map[BigInt, BigInt],
   val subroutines: Map[BigInt, String],
-  val constantProp: Map[CfgNode, Map[Variable, ConstantPropagationLattice.Element]]
-
-  , stateAfterNode: Boolean)
+  val constantProp: Map[CfgNode, Map[Variable, ConstantPropagationLattice.Element]],
+  stateAfterNode: Boolean)
   extends FlowSensitiveAnalysis(stateAfterNode)
     with MapLatticeSolver[CfgNode]
     with MemoryRegionAnalysisMisc {
@@ -471,13 +470,13 @@ trait LiftedMemoryRegionAnalysisMisc extends MemoryRegionAnalysisMisc {
  * Intraprocedural value analysis that uses [[tip.solvers.WorklistFixpointSolverWithReachability]],
  * with all function entries as start nodes.
  */
-abstract class IntraprocValueAnalysisWorklistSolverWithReachability[L](
-  cfg: ProgramCfg,
-  globals: Map[BigInt, String],
-  globalOffsets: Map[BigInt, BigInt],
-  subroutines: Map[BigInt, String],
-  constantProp: Map[CfgNode, Map[Variable, ConstantPropagationLattice.Element]]
-  )
+abstract class IntraprocMemoryRegionAnalysisWorklistSolverWithReachability[L](
+    cfg: ProgramCfg,
+    globals: Map[BigInt, String],
+    globalOffsets: Map[BigInt, BigInt],
+    subroutines: Map[BigInt, String],
+    constantProp: Map[CfgNode, Map[Variable, ConstantPropagationLattice.Element]]
+    )
   extends LiftedMemoryRegionAnalysis(
     cfg,
     globals,
@@ -497,7 +496,7 @@ object MemoryRegionAnalysis:
       globalOffsets: Map[BigInt, BigInt],
       subroutines: Map[BigInt, String],
       constantProp: Map[CfgNode, Map[Variable, ConstantPropagationLattice.Element]]
-  ) extends IntraprocValueAnalysisWorklistSolverWithReachability(
+  ) extends IntraprocMemoryRegionAnalysisWorklistSolverWithReachability(
         cfg,
         globals,
         globalOffsets,

src/main/scala/analysis/UtilMethods.scala

@@ -25,6 +25,7 @@ def evaluateExpression(exp: Expr, n: CfgNode, constantPropResult: Map[Variable,
             case BVSUB => BitVectorEval.smt_bvsub(l, r)
             case BVASHR => BitVectorEval.smt_bvashr(l, r)
             case BVCOMP => BitVectorEval.smt_bvcomp(l, r)
+            case BVCONCAT => BitVectorEval.smt_concat(l, r)
             case _ => throw new RuntimeException("Binary operation support not implemented: " + binOp.op)
           }
         case _ => exp

src/main/scala/analysis/VSA.scala

@@ -27,7 +27,7 @@ case class LiteralValue(expr: BitVecLiteral) extends Value {
 
 type VSALatticeElem = MapLattice[Variable | MemoryRegion, PowersetLattice[Value]]
 
-trait MemoryRegionValueSetAnalysis:
+trait ValueSetAnalysisMisc:
 
   val cfg: ProgramCfg
   val globals: Map[BigInt, String]
@@ -43,7 +43,7 @@ trait MemoryRegionValueSetAnalysis:
 
   /** The lattice of abstract states.
     */
-  val lattice: MapLattice[CfgNode, VSALatticeElem] = MapLattice(powersetLattice)
+  val stateLattice: MapLattice[CfgNode, VSALatticeElem] = MapLattice(powersetLattice)
 
   val domain: Set[CfgNode] = cfg.nodes.toSet
 
@@ -100,7 +100,7 @@ trait MemoryRegionValueSetAnalysis:
 
   /** Default implementation of eval.
     */
-  def eval(cmd: Command, s: lattice.sublattice.Element, n: CfgNode): lattice.sublattice.Element = {
+  def eval(cmd: Command, s: stateLattice.Element, n: CfgNode): stateLattice.Element = {
     Logger.debug(s"eval: $cmd")
     Logger.debug(s"state: $s")
     Logger.debug(s"node: $n")
@@ -114,17 +114,17 @@ trait MemoryRegionValueSetAnalysis:
                 // this is an exception to the rule and only applies to data regions
                 evaluateExpression(memoryLoad.index, n, constantProp(n)) match
                   case bitVecLiteral: BitVecLiteral =>
-                    val m = s + (r -> Set(getValueType(bitVecLiteral)))
-                    m + (localAssign.lhs -> m(r))
+                    s//TODO: val m = s + Set((n, Map(r -> Set(getValueType(bitVecLiteral)))))
+                    //m + (n, localAssign.lhs -> m(r))
                   case _ =>
-                    s + (localAssign.lhs -> s(r))
+                    s//TODO: s + (localAssign.lhs -> s(r))
               case None =>
                 Logger.warn("could not find region for " + localAssign)
                 s
           case e: Expr => {
             val evaled = evaluateExpression(e, n, constantProp(n))
             evaled match
-              case bv: BitVecLiteral => s + (localAssign.lhs -> Set(getValueType(bv)))
+              case bv: BitVecLiteral => s//TODO: s + (localAssign.lhs -> Set(getValueType(bv)))
               case _ =>
                 Logger.warn("could not evaluate expression" + e)
                 s
@@ -137,9 +137,9 @@ trait MemoryRegionValueSetAnalysis:
               case Some(r: MemoryRegion) =>
                 evaluateExpression(memAssign.rhs.value, n, constantProp(n)) match
                   case bitVecLiteral: BitVecLiteral =>
-                    return s + (r -> Set(getValueType(bitVecLiteral)))
+                    return s//TODO: return s + (r -> Set(getValueType(bitVecLiteral)))
                   case variable: Variable => // constant prop returned BOT OR TOP. Merge regions because RHS could be a memory loaded address
-                    return s + (r -> s(variable))
+                    return s//TODO: return s + (r -> s(variable))
 
                   case _ => Logger.warn("Too Complex or Wrapped i.e. Extract(Variable)") // do nothing
                 s
@@ -154,7 +154,7 @@ trait MemoryRegionValueSetAnalysis:
 
   /** Transfer function for state lattice elements.
     */
-  def localTransfer(n: CfgNode, s: lattice.sublattice.Element): lattice.sublattice.Element =
+  def localTransfer(n: CfgNode, s: stateLattice.Element): stateLattice.Element =
     n match {
       case entry: CfgFunctionEntryNode =>
         mmm.pushContext(entry.data.name)
@@ -167,25 +167,85 @@ trait MemoryRegionValueSetAnalysis:
       case _ => s // ignore other kinds of nodes
     }
 
-/** Base class for memory region analysis (non-lifted) lattice.
-  */
-abstract class ValueSetAnalysis(
-    val cfg: ProgramCfg,
+///** Base class for memory region analysis (non-lifted) lattice.
+//  */
+//abstract class ValueSetAnalysis(
+//    val cfg: ProgramCfg,
+//    val globals: Map[BigInt, String],
+//    val externalFunctions: Map[BigInt, String],
+//    val globalOffsets: Map[BigInt, BigInt],
+//    val subroutines: Map[BigInt, String],
+//    val mmm: MemoryModelMap,
+//    val constantProp: Map[CfgNode, Map[Variable, ConstantPropagationLattice.Element]]
+//) extends FlowSensitiveAnalysis(true)
+//    with MemoryRegionValueSetAnalysis {
+//
+//  /** Transfer function for state lattice elements. (Same as `localTransfer` for simple value analysis.)
+//    */
+//  def transfer(n: CfgNode, s: lattice.sublattice.Element): lattice.sublattice.Element = localTransfer(n, s)
+//
+//}
+
+/**
+ * Base class for value analysis with lifted lattice, where the extra bottom element represents "unreachable".
+ */
+abstract class LiftedValueSetAnalysis[P <: ProgramCfg] (
+    val cfg: P,
     val globals: Map[BigInt, String],
     val externalFunctions: Map[BigInt, String],
     val globalOffsets: Map[BigInt, BigInt],
     val subroutines: Map[BigInt, String],
     val mmm: MemoryModelMap,
-    val constantProp: Map[CfgNode, Map[Variable, ConstantPropagationLattice.Element]]
-) extends FlowSensitiveAnalysis(true)
-    with MemoryRegionValueSetAnalysis {
+    val constantProp: Map[CfgNode, Map[Variable, ConstantPropagationLattice.Element]],
+    stateAfterNode: Boolean)
+  extends FlowSensitiveAnalysis(stateAfterNode)
+    with MapLatticeSolver[CfgNode]
+    with ValueSetAnalysisMisc {
 
-  /** Transfer function for state lattice elements. (Same as `localTransfer` for simple value analysis.)
-    */
-  def transfer(n: CfgNode, s: lattice.sublattice.Element): lattice.sublattice.Element = localTransfer(n, s)
+  /**
+   * Lifted state lattice, with new bottom element representing "unreachable".
+   */
+  val liftedstatelattice: LiftLattice[stateLattice.type] = new LiftLattice(stateLattice)
+
+  /**
+   * The analysis lattice.
+   */
+  val lattice: MapLattice[CfgNode, liftedstatelattice.type] = new MapLattice(liftedstatelattice)
+
+  override val domain: Set[CfgNode] = cfg.nodes.toSet
+
+  /**
+   * The worklist is initialized with all function entry nodes.
+   */
+  val first: Set[CfgNode] = cfg.funEntries.toSet[CfgNode]
+
+  /**
+   * Overrides `funsub` from [[tip.solvers.MapLatticeSolver]], treating function entry nodes as reachable.
+   */
+  override def funsub(n: CfgNode, x: lattice.Element, intra: Boolean): liftedstatelattice.Element = {
+    import liftedstatelattice._
+    n match {
+      // function entry nodes are always reachable (if intra-procedural analysis)
+      case _: CfgFunctionEntryNode => lift(stateLattice.bottom)
+      // all other nodes are processed with join+transfer
+      case _ => super.funsub(n, x, intra = true)
+    }
+  }
+}
+
+/**
+ * Functionality for basic analyses with lifted state lattice.
+ */
+trait LiftedValueSetAnalysisMisc extends ValueSetAnalysisMisc {
 
+  /**
+   * Transfer function for state lattice elements.
+   * (Same as `localTransfer` for basic analyses with lifted state lattice.)
+   */
+  def transferUnlifted(n: CfgNode, s: stateLattice.Element): stateLattice.Element = localTransfer(n, s)
 }
 
+
 abstract class IntraprocValueSetAnalysisWorklistSolver[L <: VSALatticeElem](
     cfg: ProgramCfg,
     globals: Map[BigInt, String],
@@ -195,8 +255,16 @@ abstract class IntraprocValueSetAnalysisWorklistSolver[L <: VSALatticeElem](
     mmm: MemoryModelMap,
     constantProp: Map[CfgNode, Map[Variable, ConstantPropagationLattice.Element]],
     val powersetLattice: L
-) extends ValueSetAnalysis(cfg, globals, externalFunctions, globalOffsets, subroutines, mmm, constantProp)
-    with SimpleWorklistFixpointSolver[CfgNode]
+) extends LiftedValueSetAnalysis(
+    cfg,
+    globals,
+    externalFunctions,
+    globalOffsets, subroutines,
+    mmm,
+    constantProp,
+    true)
+    with LiftedValueSetAnalysisMisc
+    with WorklistFixpointSolverWithReachability[CfgNode]
     with ForwardDependencies
 
 object ValueSetAnalysis:

src/main/scala/util/RunUtils.scala

@@ -173,7 +173,10 @@ object RunUtils {
     Logger.info("[!] Running VSA")
     val vsaSolver =
       ValueSetAnalysis.WorklistSolver(cfg, globalAddresses, externalAddresses, globalOffsets, subroutines, mmm, constPropResult)
-    val vsaResult: Map[CfgNode, Map[Variable | MemoryRegion, Set[Value]]]  = vsaSolver.analyze(false)
+      // TODO: replace ? with the right type
+    val vsaResult: Map[CfgNode, Map[Variable | MemoryRegion, Set[Value]]]  = vsaSolver.unliftedAnalyze(true).asInstanceOf[Map[CfgNode, ?]]].map {
+      case (k, v) => k -> v.values.flatten.toSet
+    }
     Output.output(
       OtherOutput(OutputKindE.cfg),
       cfg.toDot(Output.labeler(vsaResult, vsaSolver.stateAfterNode), Output.dotIder),