SSA based constant prop for steensgaard

src/main/scala/analysis/Analysis.scala

@@ -102,6 +102,91 @@ class ConstantPropagationSolver(cfg: ProgramCfg) extends ConstantPropagation(cfg
     with IntraproceduralForwardDependencies
     with Analysis[Map[CfgNode, Map[Variable, FlatElement[BitVecLiteral]]]]
 
+/** Base class for value analysis with simple (non-lifted) lattice.
+ */
+trait ConstantPropagationWithSSA(val cfg: ProgramCfg) {
+  /** The lattice of abstract states.
+   */
+
+  val valuelattice: ConstantPropagationLatticeWithSSA = ConstantPropagationLatticeWithSSA()
+
+  val statelattice: MapLattice[RegisterVariableWrapper, Set[BitVecLiteral], ConstantPropagationLatticeWithSSA] = MapLattice(valuelattice)
+
+  /** Default implementation of eval.
+   */
+  def eval(exp: Expr, env: Map[RegisterVariableWrapper, Set[BitVecLiteral]]): Set[BitVecLiteral] =
+    import valuelattice._
+    exp match
+      case id: Variable => env(RegisterVariableWrapper(id))
+      case n: BitVecLiteral => bv(n)
+      case ze: ZeroExtend => zero_extend(ze.extension, eval(ze.body, env))
+      case se: SignExtend => sign_extend(se.extension, eval(se.body, env))
+      case e: Extract => extract(e.end, e.start, eval(e.body, env))
+      case bin: BinaryExpr =>
+        val left = eval(bin.arg1, env)
+        val right = eval(bin.arg2, env)
+        bin.op match
+          case BVADD => bvadd(left, right)
+          case BVSUB => bvsub(left, right)
+          case BVMUL => bvmul(left, right)
+          case BVUDIV => bvudiv(left, right)
+          case BVSDIV => bvsdiv(left, right)
+          case BVSREM => bvsrem(left, right)
+          case BVUREM => bvurem(left, right)
+          case BVSMOD => bvsmod(left, right)
+          case BVAND => bvand(left, right)
+          case BVOR => bvor(left, right)
+          case BVXOR => bvxor(left, right)
+          case BVNAND => bvnand(left, right)
+          case BVNOR => bvnor(left, right)
+          case BVXNOR => bvxnor(left, right)
+          case BVSHL => bvshl(left, right)
+          case BVLSHR => bvlshr(left, right)
+          case BVASHR => bvashr(left, right)
+          case BVCOMP => bvcomp(left, right)
+          case BVCONCAT => concat(left, right)
+
+      case un: UnaryExpr =>
+        val arg = eval(un.arg, env)
+
+        un.op match
+          case BVNOT => bvnot(arg)
+          case BVNEG => bvneg(arg)
+
+      case _ => Set.empty
+
+  /** Transfer function for state lattice elements.
+   */
+  def localTransfer(n: CfgNode, s: Map[RegisterVariableWrapper, Set[BitVecLiteral]]): Map[RegisterVariableWrapper, Set[BitVecLiteral]] =
+    n match
+      case r: CfgCommandNode =>
+        r.data match
+          // assignments
+          case la: LocalAssign =>
+            if (s.contains(RegisterVariableWrapper(la.lhs))) {
+                s + (RegisterVariableWrapper(la.lhs) -> s(RegisterVariableWrapper(la.lhs)).union(eval(la.rhs, s)))
+            } else {
+              s + (RegisterVariableWrapper(la.lhs) -> eval(la.rhs, s))
+            }
+          // all others: like no-ops
+          case _ => s
+      case _ => s
+
+  /** The analysis lattice.
+   */
+  val lattice: MapLattice[CfgNode, Map[RegisterVariableWrapper, Set[BitVecLiteral]], MapLattice[RegisterVariableWrapper, Set[BitVecLiteral], ConstantPropagationLatticeWithSSA]] = MapLattice(statelattice)
+
+  val domain: Set[CfgNode] = cfg.nodes.toSet
+
+  /** Transfer function for state lattice elements. (Same as `localTransfer` for simple value analysis.)
+   */
+  def transfer(n: CfgNode, s: Map[RegisterVariableWrapper, Set[BitVecLiteral]]): Map[RegisterVariableWrapper, Set[BitVecLiteral]] = localTransfer(n, s)
+}
+
+class ConstantPropagationSolverWithSSA(cfg: ProgramCfg) extends ConstantPropagationWithSSA(cfg)
+  with SimplePushDownWorklistFixpointSolver[CfgNode, Map[RegisterVariableWrapper, Set[BitVecLiteral]], MapLattice[RegisterVariableWrapper, Set[BitVecLiteral], ConstantPropagationLatticeWithSSA]]
+  with InterproceduralForwardDependencies
+  with Analysis[Map[CfgNode, Map[RegisterVariableWrapper, Set[BitVecLiteral]]]]
 
 trait MemoryRegionAnalysis(val cfg: ProgramCfg,
                            val globals: Map[BigInt, String],

src/main/scala/analysis/ContextTransfer.scala

@@ -66,6 +66,7 @@ class ContextTransfer(
               }
             }
           }
+          case _ => {}
         }
       }
       case _ => // do nothing

src/main/scala/analysis/Lattice.scala

@@ -151,4 +151,73 @@ class ConstantPropagationLattice extends FlatLattice[BitVecLiteral] {
   def extract(high: Int, low: Int, a: FlatElement[BitVecLiteral]): FlatElement[BitVecLiteral] =
     apply(BitVectorEval.boogie_extract(high, low, _: BitVecLiteral), a)
   def concat(a: FlatElement[BitVecLiteral], b: FlatElement[BitVecLiteral]): FlatElement[BitVecLiteral] = apply(BitVectorEval.smt_concat, a, b)
+}
+
+/** Constant propagation lattice.
+ *
+ */
+class ConstantPropagationLatticeWithSSA extends PowersetLattice[BitVecLiteral] {
+  private def apply(op: (BitVecLiteral, BitVecLiteral) => BitVecLiteral, a: Set[BitVecLiteral], b: Set[BitVecLiteral]): Set[BitVecLiteral] =
+    val res = for {
+      x <- a
+      y <- b
+    } yield op(x, y)
+    res
+
+  private def apply(op: BitVecLiteral => BitVecLiteral, a: Set[BitVecLiteral]): Set[BitVecLiteral] =
+    val res = for {
+      x <- a
+    } yield op(x)
+    res
+
+  def bv(a: BitVecLiteral): Set[BitVecLiteral] = Set(a)
+
+  def bvadd(a: Set[BitVecLiteral], b: Set[BitVecLiteral]): Set[BitVecLiteral] = apply(BitVectorEval.smt_bvadd, a, b)
+
+  def bvsub(a: Set[BitVecLiteral], b: Set[BitVecLiteral]): Set[BitVecLiteral] = apply(BitVectorEval.smt_bvsub, a, b)
+
+  def bvmul(a: Set[BitVecLiteral], b: Set[BitVecLiteral]): Set[BitVecLiteral] = apply(BitVectorEval.smt_bvmul, a, b)
+
+  def bvudiv(a: Set[BitVecLiteral], b: Set[BitVecLiteral]): Set[BitVecLiteral] = apply(BitVectorEval.smt_bvudiv, a, b)
+
+  def bvsdiv(a: Set[BitVecLiteral], b: Set[BitVecLiteral]): Set[BitVecLiteral] = apply(BitVectorEval.smt_bvsdiv, a, b)
+
+  def bvsrem(a: Set[BitVecLiteral], b: Set[BitVecLiteral]): Set[BitVecLiteral] = apply(BitVectorEval.smt_bvsrem, a, b)
+
+  def bvurem(a: Set[BitVecLiteral], b: Set[BitVecLiteral]): Set[BitVecLiteral] = apply(BitVectorEval.smt_bvurem, a, b)
+
+  def bvsmod(a: Set[BitVecLiteral], b: Set[BitVecLiteral]): Set[BitVecLiteral] = apply(BitVectorEval.smt_bvsmod, a, b)
+
+  def bvand(a: Set[BitVecLiteral], b: Set[BitVecLiteral]): Set[BitVecLiteral] = apply(BitVectorEval.smt_bvand, a, b)
+
+  def bvor(a: Set[BitVecLiteral], b: Set[BitVecLiteral]): Set[BitVecLiteral] = apply(BitVectorEval.smt_bvor, a, b)
+
+  def bvxor(a: Set[BitVecLiteral], b: Set[BitVecLiteral]): Set[BitVecLiteral] = apply(BitVectorEval.smt_bvxor, a, b)
+
+  def bvnand(a: Set[BitVecLiteral], b: Set[BitVecLiteral]): Set[BitVecLiteral] = apply(BitVectorEval.smt_bvnand, a, b)
+
+  def bvnor(a: Set[BitVecLiteral], b: Set[BitVecLiteral]): Set[BitVecLiteral] = apply(BitVectorEval.smt_bvnor, a, b)
+
+  def bvxnor(a: Set[BitVecLiteral], b: Set[BitVecLiteral]): Set[BitVecLiteral] = apply(BitVectorEval.smt_bvxnor, a, b)
+
+  def bvnot(a: Set[BitVecLiteral]): Set[BitVecLiteral] = apply(BitVectorEval.smt_bvnot, a)
+
+  def bvneg(a: Set[BitVecLiteral]): Set[BitVecLiteral] = apply(BitVectorEval.smt_bvneg, a)
+
+  def bvshl(a: Set[BitVecLiteral], b: Set[BitVecLiteral]): Set[BitVecLiteral] = apply(BitVectorEval.smt_bvshl, a, b)
+
+  def bvlshr(a: Set[BitVecLiteral], b: Set[BitVecLiteral]): Set[BitVecLiteral] = apply(BitVectorEval.smt_bvlshr, a, b)
+
+  def bvashr(a: Set[BitVecLiteral], b: Set[BitVecLiteral]): Set[BitVecLiteral] = apply(BitVectorEval.smt_bvashr, a, b)
+
+  def bvcomp(a: Set[BitVecLiteral], b: Set[BitVecLiteral]): Set[BitVecLiteral] = apply(BitVectorEval.smt_bvcomp, a, b)
+
+  def zero_extend(width: Int, a: Set[BitVecLiteral]): Set[BitVecLiteral] = apply(BitVectorEval.smt_zero_extend(width, _: BitVecLiteral), a)
+
+  def sign_extend(width: Int, a: Set[BitVecLiteral]): Set[BitVecLiteral] = apply(BitVectorEval.smt_sign_extend(width, _: BitVecLiteral), a)
+
+  def extract(high: Int, low: Int, a: Set[BitVecLiteral]): Set[BitVecLiteral] =
+    apply(BitVectorEval.boogie_extract(high, low, _: BitVecLiteral), a)
+
+  def concat(a: Set[BitVecLiteral], b: Set[BitVecLiteral]): Set[BitVecLiteral] = apply(BitVectorEval.smt_concat, a, b)
 }