flow insensitive copyprop and single pass dsa

src/main/scala/analysis/IntraLiveVarsAnalysis.scala

@@ -11,16 +11,15 @@ abstract class LivenessAnalysis(program: Program) extends Analysis[Any]:
     n match {
       case p: Procedure => s
       case b: Block => s
-      case Assign(variable, expr, _) => (s - variable) ++ expr.variables
-      case MemoryAssign(_, index, value, _, _, _) => s ++ index.variables ++ value.variables
-      case Assume(expr, _, _, _) => s ++ expr.variables
-      case Assert(expr, _, _) => s ++ expr.variables
-      case IndirectCall(variable, _) => s + variable
-      case c: DirectCall => s -- c.outParams.map(_._2) ++ c.actualParams.flatMap(_._2.variables)
+      case a : Assign => (s - a.lhs) ++ a.rhs.variables
+      case m: MemoryAssign => s ++ m.index.variables ++ m.value.variables
+      case a : Assume => s ++ a.body.variables
+      case a : Assert => s ++ a.body.variables
+      case i : IndirectCall => s + i.target
+      case c: DirectCall => (s -- c.outParams.map(_._2)) ++ c.actualParams.flatMap(_._2.variables)
       case g: GoTo => s
       case r: Return => s ++ r.outParams.flatMap(_._2.variables)
       case r: Unreachable => s
-      case _ => ???
     }
   }
 

src/main/scala/boogie/BExpr.scala

@@ -359,7 +359,7 @@ case class BinaryBExpr(op: BinOp, arg1: BExpr, arg2: BExpr) extends BExpr {
           } else {
             throw new Exception(s"bitvector size mismatch: $arg1, $arg2")
           }
-        case BVULT | BVULE | BVUGT | BVUGE | BVSLT | BVSLE | BVSGT | BVSGE =>
+        case BVULT | BVULE | BVUGT | BVUGE | BVSLT | BVSLE | BVSGT | BVSGE | BVSADDO =>
           if (bv1.size == bv2.size) {
             BoolBType
           } else {

src/main/scala/cfg_visualiser/DotTools.scala

@@ -57,7 +57,7 @@ class DotNode(val id: String, val label: String) extends DotElement {
   override def toString: String = toDotString
 
   def toDotString: String =
-    s"\"$id\"" + "[label=\"" + wrap(label, 100) + "\", shape=\"box\", fontname=\"Mono\"]"
+    s"\"$id\"" + "[label=\"" + wrap(label, 100) + "\", shape=\"box\", fontname=\"Mono\", fontsize=\"5\"]"
 
 }
 
@@ -140,5 +140,6 @@ class DotGraph(val title: String, val nodes: Iterable[DotNode], val edges: Itera
 
   override def toString: String = toDotString
 
-  def toDotString: String = "digraph " + title + " {\n" + (nodes ++ edges).foldLeft("")((str, elm) => str + elm.toDotString + "\n") + "}"
+  val graph = "graph [ fontsize=18 ];" 
+  def toDotString: String = "digraph " + title + " {\n" + graph + "\n" + (nodes ++ edges).foldLeft("")((str, elm) => str + elm.toDotString + "\n") + "}"
 }

src/main/scala/ir/Expr.scala

@@ -21,6 +21,8 @@ sealed trait Expr {
   def gammas: Set[Expr] = Set()
   def variables: Set[Variable] = Set()
   def acceptVisit(visitor: Visitor): Expr = throw new Exception("visitor " + visitor + " unimplemented for: " + this)
+
+  lazy val variablesCached = variables
 }
 
 
@@ -195,7 +197,7 @@ case class BinaryExpr(op: BinOp, arg1: Expr, arg2: Expr) extends Expr {
           } else {
             throw new Exception("bitvector size mismatch")
           }
-        case BVULT | BVULE | BVUGT | BVUGE | BVSLT | BVSLE | BVSGT | BVSGE =>
+        case BVULT | BVULE | BVUGT | BVUGE | BVSLT | BVSLE | BVSGT | BVSGE | BVSADDO =>
           if (bv1.size == bv2.size) {
             BoolType
           } else {
@@ -210,7 +212,7 @@ case class BinaryExpr(op: BinOp, arg1: Expr, arg2: Expr) extends Expr {
         case IntEQ | IntNEQ | IntLT | IntLE | IntGT | IntGE => BoolType
       }
     case _ =>
-      throw new Exception("type mismatch, operator " + op + " type doesn't match args: (" + arg1 + ", " + arg2 + ")")
+      throw new Exception("type mismatch, operator " + op.getClass.getSimpleName + s" type doesn't match args: (" + arg1 + ", " + arg2 + ")")
   }
 
   private def inSize = arg1.getType match {
@@ -255,6 +257,7 @@ sealed trait BVBinOp(op: String) extends BinOp {
   def opName = op
 }
 
+case object BVSADDO extends BVBinOp("saddo")
 case object BVAND extends BVBinOp("and")
 case object BVOR extends BVBinOp("or")
 case object BVADD extends BVBinOp("add")

src/main/scala/ir/IRCursor.scala

@@ -289,7 +289,7 @@ def toDot[T <: CFGPosition](
 
   def nodeText(node: CFGPosition): String = {
     var text = node match {
-      case s: Block => f"[Block] ${s.label}"
+      case s: Block => f"[Block] (prec ${s.rpoOrder}) ${s.label}"
       case s        => s.toString
     }
     if (labels.contains(node)) {

src/main/scala/ir/Statement.scala

@@ -156,7 +156,7 @@ class DirectCall(val target: Procedure,
     case None => Set()
   } */
   def calls: Set[Procedure] = Set(target)
-  override def toString: String = s"${labelStr}${outParams.mkString(",")} := DirectCall(${target.name})(${actualParams.mkString(",")})"
+  override def toString: String = s"${labelStr}${outParams.map(_._2.name).mkString(",")} := DirectCall(${target.name})(${actualParams.map(_._2).mkString(",")})"
   override def acceptVisit(visitor: Visitor): Statement = visitor.visitDirectCall(this)
 
   override def linkParent(p: Block): Unit = {

src/main/scala/ir/cilvisitor/CILVisitor.scala

@@ -80,18 +80,46 @@ class CILVisitorImpl(val v: CILVisitor) {
   }
 
 
-  def visit_expr(n: Expr): Expr = {
+
+   def visit_expr(n: Expr): Expr = {
     def continue(n: Expr): Expr = n match {
-      case n: Literal                           => n
-      case MemoryLoad(mem, index, endian, size) => MemoryLoad(visit_mem(mem), visit_expr(index), endian, size)
-      case Extract(end, start, arg)             => Extract(end, start, visit_expr(arg))
-      case Repeat(repeats, arg)                 => Repeat(repeats, visit_expr(arg))
-      case ZeroExtend(bits, arg)                => ZeroExtend(bits, visit_expr(arg))
-      case SignExtend(bits, arg)                => SignExtend(bits, visit_expr(arg))
-      case BinaryExpr(op, arg, arg2)            => BinaryExpr(op, visit_expr(arg), visit_expr(arg2))
-      case UnaryExpr(op, arg)                   => UnaryExpr(op, visit_expr(arg))
-      case v: Variable                          => visit_rvar(v)
-      case UninterpretedFunction(n, params, rt) => UninterpretedFunction(n, params.map(visit_expr), rt)
+      case n: Literal => n
+      case MemoryLoad(mem, index, endian, size) => {
+        val nmem = visit_mem(mem)
+        val nind = visit_expr(index)
+        if ((nmem ne mem) || (nind ne index)) MemoryLoad(visit_mem(mem), visit_expr(index), endian, size) else n
+      }
+      case Extract(end, start, arg) => {
+        val narg = visit_expr(arg)
+        if (narg ne arg) Extract(end, start, narg) else n
+      }
+      case Repeat(repeats, arg) => {
+        val narg = visit_expr(arg)
+        if (narg ne arg) Repeat(repeats, arg) else n
+      }
+      case ZeroExtend(bits, arg) => {
+        val narg = visit_expr(arg)
+        if (narg ne arg) ZeroExtend(bits, narg) else n
+      }
+      case SignExtend(bits, arg) => {
+        val narg = visit_expr(arg)
+        if (narg ne arg) SignExtend(bits, narg) else n
+      }
+      case BinaryExpr(op, arg, arg2) => {
+        val narg1 = visit_expr(arg)
+        val narg2 = visit_expr(arg2)
+        if ((narg1 ne arg) || (narg2 ne arg2)) BinaryExpr(op, narg1, narg2) else n
+      }
+      case UnaryExpr(op, arg) => {
+        val narg = visit_expr(arg)
+        if (narg ne arg) UnaryExpr(op, narg) else n
+      }
+      case v: Variable => visit_rvar(v)
+      case UninterpretedFunction(name, params, rt) => {
+        val nparams = params.map(visit_expr)
+        val updated = (params.zip(nparams).map((a, b) => a ne b)).contains(true)
+        if (updated) UninterpretedFunction(name, nparams, rt) else n
+      } 
     }
     doVisit(v, v.vexpr(n), n, continue)
   }

src/main/scala/ir/eval/ExprEval.scala

@@ -147,6 +147,84 @@ trait Loader[S, E] {
   }
 }
 
+def fastPartialEvalExpr(exp: Expr): Expr = {
+  /*
+   * Ignore substitutions and parital eval
+   */
+  exp match {
+    case f: UninterpretedFunction => f
+    case unOp: UnaryExpr => {
+        unOp.arg match {
+          case l: Literal => evalUnOp(unOp.op, l)
+          case o          => UnaryExpr(unOp.op, o) 
+        }
+      }
+    case binOp: BinaryExpr =>
+        val lhs = binOp.arg1
+        val rhs = binOp.arg2
+        binOp.getType match {
+        case m: MapType => binOp
+        case b: BitVecType => {
+          (binOp.op, lhs, rhs) match {
+            case (o: BVBinOp, l: BitVecLiteral, r: BitVecLiteral) => evalBVBinExpr(o, l, r)
+            case _                                                => BinaryExpr(binOp.op, lhs, rhs)
+          }
+        }
+        case BoolType => {
+          def bool2lit(b: Boolean) = if b then TrueLiteral else FalseLiteral
+          (binOp.op, lhs, rhs) match {
+            case (o: BVBinOp, l: BitVecLiteral, r: BitVecLiteral) => bool2lit(evalBVLogBinExpr(o, l, r))
+            case (o: IntBinOp, l: IntLiteral, r: IntLiteral)      => bool2lit(evalIntLogBinExpr(o, l.value, r.value))
+            case (o: BoolBinOp, l: BoolLit, r: BoolLit)           => bool2lit(evalBoolLogBinExpr(o, l.value, r.value))
+            case _                                                => BinaryExpr(binOp.op, lhs, rhs)
+          }
+        }
+        case IntType => {
+          (binOp.op, lhs, rhs) match {
+            case (o: IntBinOp, l: IntLiteral, r: IntLiteral) => IntLiteral(evalIntBinExpr(o, l.value, r.value))
+            case _                                           => BinaryExpr(binOp.op, lhs, rhs)
+          }
+        }
+      }
+    case extend: ZeroExtend =>
+      val body = extend.body
+      (body match {
+        case b: BitVecLiteral => BitVectorEval.smt_zero_extend(extend.extension, b)
+        case o                => extend.copy(body = o)
+      })
+    case extend: SignExtend =>
+      val body = extend.body
+      body match {
+        case b: BitVecLiteral => BitVectorEval.smt_sign_extend(extend.extension, b)
+        case o                => extend.copy(body = o)
+      }
+    case e: Extract =>
+      val body = e.body
+      body match {
+        case b: BitVecLiteral => BitVectorEval.boogie_extract(e.end, e.start, b)
+        case o                => e.copy(body = o)
+      }
+    case r: Repeat =>
+      val body = r.body
+      body match {
+        case b: BitVecLiteral => {
+          assert(r.repeats > 0)
+          if (r.repeats == 1) b
+          else {
+            (2 to r.repeats).foldLeft(b)((acc, r) => BitVectorEval.smt_concat(acc, b))
+          }
+        }
+        case o => r.copy(body = o)
+      }
+    case variable: Variable => variable
+    case ml: MemoryLoad => 
+      val addr = ml.index
+      ml.copy(index= addr)
+    case b: Literal =>  b
+  }
+}
+
+
 def statePartialEvalExpr[S](l: Loader[S, InterpreterError])(exp: Expr): State[S, Expr, InterpreterError] = {
   val eval = statePartialEvalExpr(l)
   val ns = exp match {