Add read-uninitialised locals check

src/main/scala/analysis/InterLiveVarsAnalysis.scala

@@ -17,6 +17,9 @@ import ir.{
   Return,
   Variable
 }
+import util.Logger
+
+import scala.collection.immutable.ListSet
 
 /** Micro-transfer-functions for LiveVar analysis
  *  This analysis works by inlining function calls - instead of just mapping parameters and returns, all live variables
@@ -136,6 +139,56 @@ trait LiveVarsAnalysisFunctions(inline: Boolean, addExternals: Boolean = true)
   }
 }
 
-class InterLiveVarsAnalysis(program: Program, ignoreExternals: Boolean = false)
-    extends BackwardIDESolver[Variable, TwoElement, TwoElementLattice](program),
+class InterLiveVarsAnalysis(program: Program, ignoreExternals: Boolean = false, entry: Option[Procedure] = None)
+    extends BackwardIDESolver[Variable, TwoElement, TwoElementLattice](program, entry),
       LiveVarsAnalysisFunctions(true, !ignoreExternals)
+
+def interLiveVarsAnalysis(
+  program: Program,
+  ignoreExternals: Boolean = false
+): Map[CFGPosition, Map[Variable, TwoElement]] = {
+
+  var procs = ListSet.from(program.procedures)
+  var starts = List[Procedure]()
+
+  while {
+    val entries =
+      procs.toList.filter(p => p.incomingCalls().size == 0 && p.entryBlock.isDefined && p.returnBlock.isDefined)
+    if (entries.nonEmpty) {
+      starts = entries.head :: starts
+      val done = entries.head.reachableFrom
+      procs = procs -- done
+      procs.nonEmpty
+    } else {
+      Logger.warn(s"Live vars :: no program entry candidates remaining")
+      false
+    }
+  } do {}
+
+  val reachable = starts.toSet.flatMap(_.reachableFrom)
+  if (
+    !(reachable.contains(
+      program.mainProcedure
+    )) && procs.nonEmpty && program.mainProcedure.entryBlock.isDefined && program.mainProcedure.returnBlock.isDefined
+  ) {
+    Logger.warn(
+      s"mainProcedure has predecessors but is not reachable from an entry-candidate, using it as an entry candidate."
+    )
+    val remaining = program.procedures.toSet -- program.mainProcedure.reachableFrom
+    starts = List(program.mainProcedure)
+    procs = procs -- program.mainProcedure.reachableFrom
+  } else if (!reachable.contains(program.mainProcedure)) {
+    Logger.warn(s"mainProcedure ${program.mainProcedure.name} is a stub and is not reachable from any entry point")
+  }
+
+  if (procs.nonEmpty) {
+    Logger.error(s"Code unreachable for liveness analysis: ${procs.toList}")
+  }
+
+  var r = Map[CFGPosition, Map[Variable, TwoElement]]()
+  for (p <- starts) {
+    r = r ++ InterLiveVarsAnalysis(program, ignoreExternals, Some(p)).analyze()
+  }
+  r
+
+}

src/main/scala/analysis/solvers/IDESolver.scala

@@ -245,21 +245,14 @@ abstract class IDESolver[
   }
 
   def analyze(): Map[CFGPosition, Map[D, T]] = {
-    if (
-      program.mainProcedure.blocks.nonEmpty && program.mainProcedure.returnBlock.isDefined && program.mainProcedure.entryBlock.isDefined
-    ) {
-      val phase1 = Phase1()
-      val phase2 = Phase2(phase1)
-      phase2.restructure(phase2.analyze())
-    } else {
-      Logger.warn(s"Disabling IDE solver tests due to external main procedure: ${program.mainProcedure.name}")
-      Map()
-    }
+    val phase1 = Phase1()
+    val phase2 = Phase2(phase1)
+    phase2.restructure(phase2.analyze())
   }
 }
 
-abstract class ForwardIDESolver[D, T, L <: Lattice[T]](program: Program)
-    extends IDESolver[Procedure, Return, DirectCall, Command, D, T, L](program, program.mainProcedure),
+abstract class ForwardIDESolver[D, T, L <: Lattice[T]](program: Program, entry: Option[Procedure] = None)
+    extends IDESolver[Procedure, Return, DirectCall, Command, D, T, L](program, entry.getOrElse(program.mainProcedure)),
       ForwardIDEAnalysis[D, T, L],
       IRInterproceduralForwardDependencies {
 
@@ -302,10 +295,12 @@ abstract class ForwardIDESolver[D, T, L <: Lattice[T]](program: Program)
     InterProcIRCursor.succ(exit).filter(_.isInstanceOf[Command]).map(_.asInstanceOf[Command])
 }
 
-abstract class BackwardIDESolver[D, T, L <: Lattice[T]](program: Program)
+abstract class BackwardIDESolver[D, T, L <: Lattice[T]](program: Program, entry: Option[Procedure] = None)
     extends IDESolver[Return, Procedure, Command, DirectCall, D, T, L](
-      program,
-      IRWalk.lastInProc(program.mainProcedure).getOrElse(program.mainProcedure)
+      program, {
+        val e = entry.getOrElse(program.mainProcedure)
+        IRWalk.lastInProc(e).getOrElse(e)
+      }
     ),
       BackwardIDEAnalysis[D, T, L],
       IRInterproceduralBackwardDependencies {

src/main/scala/ir/invariant/ReadUninitialised.scala

@@ -0,0 +1,74 @@
+package ir.invariant
+
+import ir.*
+import util.Logger
+
+import scala.collection.mutable
+
+class ReadUninitialised() {
+
+  var init = Set[Variable]()
+  var readUninit = List[(Command, Set[Variable])]()
+
+  final def check(a: Command) = {
+    val free = freeVarsPos(a).filter(_.isInstanceOf[LocalVar]) -- init
+    if (free.size > 0) {
+      readUninit = (a, free) :: readUninit
+    }
+  }
+
+  final def readUninitialised(b: Iterable[Statement]): Boolean = {
+    val i = readUninit.size
+    b.foreach {
+      case a: Assign => {
+        check(a)
+        init = init ++ a.assignees
+      }
+      case o => {
+        check(o)
+      }
+    }
+    i != readUninit.size
+  }
+
+  final def readUninitialised(b: Block): Boolean = {
+    val i = readUninit.size
+    readUninitialised(b.statements)
+    check(b.jump)
+    i != readUninit.size
+  }
+
+  final def getResult(): Option[String] = {
+    if (readUninit.size > 0) {
+      val msg = readUninit
+        .map { case (s, vars) =>
+          s"   ${vars.mkString(", ")} uninitialised in statement $s"
+        }
+        .mkString("\n")
+      Some(msg)
+    } else {
+      None
+    }
+  }
+
+  final def readUninitialised(p: Procedure): Boolean = {
+    init = init ++ p.formalInParam
+
+    ir.transforms.reversePostOrder(p)
+
+    val worklist = mutable.PriorityQueue[Block]()(Ordering.by(_.rpoOrder))
+    worklist.addAll(p.blocks)
+
+    while (worklist.nonEmpty) {
+      val b = worklist.dequeue()
+      readUninitialised(b)
+    }
+    getResult().map(e => Logger.error(p.name + "\n" + e)).isDefined
+  }
+
+}
+
+def readUninitialised(p: Program): Boolean = {
+  val r = p.procedures.map(ReadUninitialised().readUninitialised)
+  r.forall(x => !x)
+}

src/main/scala/ir/transforms/DynamicSingleAssignment.scala

@@ -299,7 +299,7 @@ class OnePassDSA(
     val worklist = mutable.PriorityQueue[Block]()(Ordering.by(b => b.rpoOrder))
     worklist.addAll(p.blocks)
     var seen = Set[Block]()
-    val count = mutable.Map[Variable, Int]().withDefaultValue(0)
+    val count = mutable.Map[Variable, Int]().withDefaultValue(p.ssaCount)
 
     while (worklist.nonEmpty) {
       while (worklist.nonEmpty) {

src/main/scala/ir/transforms/Inline.scala

@@ -28,11 +28,7 @@ def renameBlock(s: String): String = {
 class VarRenamer(proc: Procedure) extends CILVisitor {
 
   def doRename(v: Variable): Variable = v match {
-    case l: LocalVar if l.name.endsWith("_in") => {
-      val name = l.name.stripSuffix("_in")
-      proc.getFreshSSAVar(name, l.getType)
-    }
-    case l: LocalVar if l.index != 0 =>
+    case l: LocalVar =>
       proc.getFreshSSAVar(l.varName, l.getType)
     case _ => v
   }

src/main/scala/ir/transforms/ProcedureParameters.scala

@@ -4,7 +4,7 @@ import ir.cilvisitor.*
 import ir.{CallGraph, *}
 import specification.Specification
 import translating.PrettyPrinter
-import util.{DebugDumpIRLogger, Logger}
+import util.DebugDumpIRLogger
 
 import java.io.File
 import scala.collection.{immutable, mutable}
@@ -119,12 +119,7 @@ def liftProcedureCallAbstraction(ctx: ir.IRContext): ir.IRContext = {
   val mainHasReturn = ctx.program.mainProcedure.returnBlock.isDefined
   val mainHasEntry = ctx.program.mainProcedure.entryBlock.isDefined
 
-  val liveVars = if (mainNonEmpty && mainHasEntry && mainHasReturn) {
-    analysis.InterLiveVarsAnalysis(ctx.program).analyze()
-  } else {
-    Logger.error(s"Empty live vars $mainNonEmpty $mainHasReturn $mainHasEntry")
-    Map.empty
-  }
+  val liveVars = analysis.interLiveVarsAnalysis(ctx.program)
   transforms.applyRPO(ctx.program)
 
   val liveLab = () =>

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

@@ -1244,48 +1244,50 @@ object OffsetProp {
   // 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
     val lastUpdate = mutable.Map[Block, Int]()
     var stSequenceNo = 1
 
-    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 eval(c: BitVecLiteral)(v: BitVecLiteral | Variable | BinaryExpr): BitVecLiteral | Variable | BinaryExpr =
+      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 findOff(v: Variable, c: BitVecLiteral, fuel: Int = 1000): BitVecLiteral | Variable | BinaryExpr =
+      find(v, fuel) 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 joinState(lhs: Variable, rhs: Expr) = {
-      specJoinState(lhs, rhs) match {
-        case Some((l, r)) => {
-          if (st.contains(l) && st(l) != r) {
-            stSequenceNo += 1
+    def find(v: Variable, fuel: Int = 1000): BitVecLiteral | Variable | BinaryExpr = {
+      if (fuel == 0) {
+        var chain = List(v)
+        for (i <- 0 to 10) {
+          chain = st.get(chain.head) match {
+            case Some((Some(v: Variable), _)) => v :: chain
+            case o =>
+              chain
           }
-          st(l) = r
         }
-        case _ => ()
+        throw Exception(
+          s"Ran out of fuel recursively resolving copyprop (at $v): probable cycle. Next lookups are: $chain"
+        )
+      }
+      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, fuel - 1)
+        case Some((Some(v), Some(c))) => findOff(v, c, fuel - 1)
       }
     }
 
@@ -1302,8 +1304,11 @@ object OffsetProp {
       }
     }
 
-    def clob(v: Variable) = {
-      st(v) = (None, None)
+    def update(v: Variable, r: Value) = {
+      if (!st.get(v).exists(_ == r)) {
+        stSequenceNo += 1
+        st(v) = r
+      }
     }
 
     def transfer(s: Statement) = s match {
@@ -1316,11 +1321,11 @@ object OffsetProp {
             case (l: Variable, _) => Seq(l -> (None, None))
           }
           .foreach { case (l, r) =>
-            st(l) = r
+            update(l, r)
           }
       case a: Assign => {
         // memoryload and DirectCall
-        a.assignees.foreach(clob)
+        a.assignees.foreach(v => update(v, (None, None)))
       }
       case _: MemoryStore => ()
       case _: NOP => ()

src/main/scala/ir/transforms/SimplifyPipeline.scala

@@ -56,6 +56,7 @@ def doSimplify(ctx: IRContext, config: Option[StaticAnalysisConfig]): Unit = {
 
   transforms.OnePassDSA().applyTransform(program)
 
+  assert(ir.invariant.readUninitialised(ctx.program))
   // fixme: this used to be a plain function but now we have to supply an analysis manager!
   transforms.inlinePLTLaunchpad(ctx, AnalysisManager(ctx.program))
 
@@ -113,6 +114,7 @@ def doSimplify(ctx: IRContext, config: Option[StaticAnalysisConfig]): Unit = {
     }
   }
   Logger.info("Copyprop Start")
+  assert(ir.invariant.readUninitialised(ctx.program))
   transforms.copyPropParamFixedPoint(program, ctx.globalOffsets)
 
   transforms.fixupGuards(program)

src/main/scala/translating/GTIRBLoader.scala

@@ -386,6 +386,7 @@ class GTIRBLoader(parserMap: immutable.Map[String, List[InsnSemantics]]) {
       case "and_bits.0" => resolveBinaryOp(BVAND, function, 1, typeArgs, args, ctx.getText)
       case "eor_bits.0" => resolveBinaryOp(BVXOR, function, 1, typeArgs, args, ctx.getText)
       case "eq_bits.0" => resolveBinaryOp(EQ, function, 1, typeArgs, args, ctx.getText)
+      case "ne_bits.0" => resolveBinaryOp(NEQ, function, 1, typeArgs, args, ctx.getText)
       case "add_bits.0" => resolveBinaryOp(BVADD, function, 1, typeArgs, args, ctx.getText)
       case "sub_bits.0" => resolveBinaryOp(BVSUB, function, 1, typeArgs, args, ctx.getText)
       case "mul_bits.0" => resolveBinaryOp(BVMUL, function, 1, typeArgs, args, ctx.getText)

src/main/scala/translating/offlineLifter/InstructionBuilder.scala

@@ -82,7 +82,12 @@ trait LifterIFace[L] extends LiftState[Expr, L, BitVecLiteral] {
     smt_bvlshr(arg0, BitVecLiteral(arg1.value, arg0.size))
 
   def f_decl_bool(arg0: String): Expr = LocalVar(b.fresh_local + "_bool", BoolType)
-  def f_decl_bv(arg0: String, arg1: BigInt): Expr = LocalVar(b.fresh_local + "_bv" + arg1, BitVecType(arg1.toInt))
+  def f_decl_bv(arg0: String, arg1: BigInt): Expr = {
+    val v = LocalVar(b.fresh_local + "_bv" + arg1, BitVecType(arg1.toInt))
+    // FIXME: shouldn't need always clear
+    b.push_stmt(LocalAssign(v, BitVecLiteral(0, arg1.toInt)))
+    v
+  }
 
   def f_AtomicEnd(): Expr = LocalVar("ATOMICEND", BoolType)
   def f_AtomicStart(): Expr = LocalVar("ATOMICSTART", BoolType)