add prop for base+offset

Author: ailrst

src/main/scala/ir/transforms/Simp.scala

@@ -553,16 +553,8 @@ def copypropTransform(
   // SimplifyLogger.info(s"${p.name} ExprComplexity ${ExprComplexity()(p)}")
   // val result = solver.solveProc(p, true).withDefaultValue(dom.bot)
 
-  MinCopyProp.transform(p)
+  OffsetProp.transform(p)
 
-  val result = CopyProp.DSACopyProp(p, procFrames, funcEntries, constRead)
-  val solve = t.checkPoint("Solve CopyProp")
-
-  if (result.nonEmpty) {
-    val vis = Simplify(CopyProp.toResult(result))
-    visit_proc(vis, p)
-  }
-  // visit_proc(CopyProp.BlockyProp(), p)
   val gvis = GuardVisitor()
   visit_proc(gvis, p)
 
@@ -1015,6 +1007,139 @@ object getProcFrame {
 
 }
 
+object OffsetProp {
+
+  /*
+   * Copyprop for any expression of fitting into the structure
+   *    bvadd(variable, constant)
+   *
+   * This is sufficient to propagate branch conditions through.
+   */
+
+  // None, None -> Top
+  // Some(v), None -> v
+  // Some(v), Some(Lit) -> v + Lit
+  // None, Some(Lit) -> Lit
+  type Value = (Option[Variable], Option[BitVecLiteral])
+
+  def joinValue(l: Value, r: Value) = {
+    (l, r) match {
+      case ((None, None), _) => (None, None)
+      case (_, (None, None)) => (None, None)
+      case (l, r) if l != r => (None, None)
+      case (l, r) => l
+    }
+  }
+
+  class CopyProp() {
+    val st = mutable.Map[Variable, Value]()
+    var giveUp = false
+
+    def findOff(v: Variable, c: BitVecLiteral): BitVecLiteral | Variable | BinaryExpr = find(v) match {
+      case lc: BitVecLiteral => ir.eval.BitVectorEval.smt_bvadd(lc, c)
+      case lv: Variable => BinaryExpr(BVADD, lv, c)
+      case BinaryExpr(BVADD, l: Variable, r: BitVecLiteral) =>
+        BinaryExpr(BVADD, l, ir.eval.BitVectorEval.smt_bvadd(r, c))
+      case _ => throw Exception("Unexpected expression structure created by find() at some point")
+    }
+
+    def find(v: Variable): BitVecLiteral | Variable | BinaryExpr = {
+      st.get(v) match {
+        case None => v
+        case Some((None, None)) => v
+        case Some((None, Some(c))) => c
+        case Some((Some(v), None)) => find(v)
+        case Some((Some(v), Some(c))) => findOff(v, c)
+      }
+    }
+
+    def joinState(lhs: Variable, rhs: Expr) = {
+      specJoinState(lhs, rhs) match {
+        case Some((l, r)) => st(l) = r
+        case _ => ()
+      }
+    }
+
+    def specJoinState(lhs: Variable, rhs: Expr): Option[(Variable, Value)] = {
+      rhs match {
+        case e @ BinaryExpr(BVADD, l: Variable, r: BitVecLiteral) if (!st.contains(lhs)) =>
+          Some(lhs -> (Some(l), Some(r)))
+        case e @ BinaryExpr(BVADD, l: Variable, r: BitVecLiteral) if findOff(l, r) == find(lhs) => None
+        case v: Variable if (!st.contains(lhs)) => Some(lhs -> (Some(v), None))
+        case v: BitVecLiteral if (!st.contains(lhs)) => Some(lhs -> (None, Some(v)))
+        case v: Variable if (find(lhs) == find(v)) => None
+        case c: BitVecLiteral if (find(lhs) != c) => Some(lhs -> (None, None))
+        case _ => Some(lhs -> (None, None))
+      }
+    }
+
+    def clob(v: Variable) = {
+      st(v) = (None, None)
+    }
+
+    def transfer(s: Statement) = s match {
+      case LocalAssign(l: Variable, r: Variable, _) => joinState(l, r)
+      case LocalAssign(l: Variable, r: Literal, _) => joinState(l, r)
+      case LocalAssign(l: Variable, r @ BinaryExpr(BVADD, _: Variable, _: BitVecLiteral), _) => joinState(l, r)
+      case LocalAssign(l: Variable, _, _) => clob(l)
+      // case s: SimulAssign => s.assignments.flatMap {
+      //   case (l: Variable, r: Variable) => specJoinState(l, r).toSeq
+      //   case (l: Variable, r) => Seq(l -> None)
+      // }.foreach {
+      //   case (l, r) => st(l) = r
+      // }
+      case a: Assign => {
+        // memoryload and DirectCall
+        a.assignees.foreach(clob)
+      }
+      case _: MemoryStore => ()
+      case _: NOP => ()
+      case _: Assert => ()
+      case _: Assume => ()
+      case i: IndirectCall => giveUp = true
+    }
+
+    def analyse(p: Procedure): Map[Variable, Expr] = {
+      reversePostOrder(p)
+      val worklist = mutable.PriorityQueue[Block]()(Ordering.by(_.rpoOrder))
+      worklist.addAll(p.blocks)
+      while (worklist.nonEmpty && !giveUp) {
+        val b = worklist.dequeue()
+        b.statements.foreach(transfer)
+      }
+
+      val res: Map[Variable, Variable | Literal | BinaryExpr] =
+        if giveUp then Map()
+        else
+          st.collect {
+            case (v, (Some(v2), None)) => v -> find(v2)
+            case (v, (None, Some(c))) => v -> c
+            case (v, (Some(v2), Some(c))) => v -> findOff(v2, c)
+          }.toMap
+
+      res
+    }
+
+  }
+
+  def transform(p: Procedure) = {
+    val solver = CopyProp()
+    val res = solver.analyse(p)
+
+    class SubstExprs(subst: Map[Variable, Expr]) extends CILVisitor {
+      override def vexpr(e: Expr) = {
+        Substitute(subst.get)(e) match {
+          case Some(n) => ChangeTo(n)
+          case _ => SkipChildren()
+        }
+      }
+    }
+    if (res.nonEmpty) {
+      visit_proc(SubstExprs(res), p)
+    }
+  }
+}
+
 object MinCopyProp {
 
   // None -> Top
@@ -1101,7 +1226,6 @@ object MinCopyProp {
 
       res
     }
-
   }
 
   def transform(p: Procedure) = {