From 9edd773393f5e181e280d2cc39c057287867a62f Mon Sep 17 00:00:00 2001
From: am <a.michael1@uq.edu.au>
Date: Tue, 16 Sep 2025 18:48:48 +1000
Subject: [PATCH 01/20] read-uninit

---
 .../transforms/DynamicSingleAssignment.scala  |  2 +-
 src/main/scala/ir/transforms/Inline.scala     | 10 ++---
 .../scala/ir/transforms/ReplaceReturn.scala   |  1 +
 src/main/scala/ir/transforms/Simp.scala       | 40 ++++++++++++++++---
 .../ir/transforms/SimplifyPipeline.scala      |  6 +--
 src/main/scala/util/RunUtils.scala            |  6 +++
 6 files changed, 49 insertions(+), 16 deletions(-)

diff --git a/src/main/scala/ir/transforms/DynamicSingleAssignment.scala b/src/main/scala/ir/transforms/DynamicSingleAssignment.scala
index a205b97c3..d03ea258e 100644
--- a/src/main/scala/ir/transforms/DynamicSingleAssignment.scala
+++ b/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) {
diff --git a/src/main/scala/ir/transforms/Inline.scala b/src/main/scala/ir/transforms/Inline.scala
index 3cb11c327..b07671f70 100644
--- a/src/main/scala/ir/transforms/Inline.scala
+++ b/src/main/scala/ir/transforms/Inline.scala
@@ -28,11 +28,11 @@ 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 if l.name.endsWith("_in") => {
+    //  val name = l.name.stripSuffix("_in")
+    //  proc.getFreshSSAVar(name, l.getType)
+    //}
+    case l: LocalVar =>
       proc.getFreshSSAVar(l.varName, l.getType)
     case _ => v
   }
diff --git a/src/main/scala/ir/transforms/ReplaceReturn.scala b/src/main/scala/ir/transforms/ReplaceReturn.scala
index 5b1aafd09..ff2883c13 100644
--- a/src/main/scala/ir/transforms/ReplaceReturn.scala
+++ b/src/main/scala/ir/transforms/ReplaceReturn.scala
@@ -92,6 +92,7 @@ def addReturnBlocks(p: Program, toAll: Boolean = false): Unit = {
     val returningBlocks = p.blocks.filter(_.jump.isInstanceOf[Return]).toList
     val containsReturn = returningBlocks.nonEmpty
 
+
     if (
       returningBlocks.size == 1 && !p.entryBlock.contains(returningBlocks.head)
       && returningBlocks.forall(_.statements.isEmpty)
diff --git a/src/main/scala/ir/transforms/Simp.scala b/src/main/scala/ir/transforms/Simp.scala
index df0cfbee2..807a190da 100644
--- a/src/main/scala/ir/transforms/Simp.scala
+++ b/src/main/scala/ir/transforms/Simp.scala
@@ -1267,16 +1267,40 @@ object OffsetProp {
       case _ => throw Exception("Unexpected expression structure created by find() at some point")
     }
 
-    def find(v: Variable): BitVecLiteral | Variable | BinaryExpr = {
+    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")
+    }
+
+    final def find(v: Variable, ret: BitVecLiteral | Variable | BinaryExpr =>  BitVecLiteral | Variable | BinaryExpr = x => x, fuel: Int = 5000): 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 => 
+              println(o)
+              chain
+          }
+        }
+        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)
-        case Some((Some(v), Some(c))) => findOff(v, c)
+        case Some((None, None)) => ret(v)
+        case Some((None, Some(c))) => ret(c)
+        //case Some((Some(c), None)) if c == v => ret(c)
+        case Some((Some(v), None)) => find(v, ret, fuel - 1)
+        //case Some((Some(v2), Some(c))) if v2 == v => eval(c)(v2)
+        case Some((Some(v), Some(c))) => find(v, eval(c), fuel - 1)
       }
     }
 
+    def findOff(v: BitVecLiteral, e: Variable) : BitVecLiteral | Variable | BinaryExpr = find(e, eval(v))
+
     def joinState(lhs: Variable, rhs: Expr) = {
       specJoinState(lhs, rhs) match {
         case Some((l, r)) => {
@@ -1303,6 +1327,9 @@ object OffsetProp {
     }
 
     def clob(v: Variable) = {
+      if (!st.get(v).contains((None, None))) {
+        stSequenceNo += 1
+      }
       st(v) = (None, None)
     }
 
@@ -1316,6 +1343,9 @@ object OffsetProp {
             case (l: Variable, _) => Seq(l -> (None, None))
           }
           .foreach { case (l, r) =>
+            if (!st.get(l).contains(r))  {
+              stSequenceNo += 1
+            }
             st(l) = r
           }
       case a: Assign => {
diff --git a/src/main/scala/ir/transforms/SimplifyPipeline.scala b/src/main/scala/ir/transforms/SimplifyPipeline.scala
index 0a23d884b..a6dd3275b 100644
--- a/src/main/scala/ir/transforms/SimplifyPipeline.scala
+++ b/src/main/scala/ir/transforms/SimplifyPipeline.scala
@@ -74,12 +74,8 @@ def doSimplify(ctx: IRContext, config: Option[StaticAnalysisConfig]): Unit = {
       )
     }
   }
-  config.foreach {
-    _.dumpILToPath.foreach { s =>
-      DebugDumpIRLogger.writeToFile(File(s"${s}_il-after-dsa.il"), pp_prog(program))
-    }
-  }
 
+  DebugDumpIRLogger.writeToFile(File(s"il-after-dsa.il"), pp_prog(program))
   if (ir.eval.SimplifyValidation.validate) {
     Logger.info("DSA no uninitialised")
     assert(invariant.allVariablesAssignedIndex(program))
diff --git a/src/main/scala/util/RunUtils.scala b/src/main/scala/util/RunUtils.scala
index c5963b251..0a2bd18be 100644
--- a/src/main/scala/util/RunUtils.scala
+++ b/src/main/scala/util/RunUtils.scala
@@ -67,6 +67,7 @@ object RunUtils {
     else doCleanupWithoutSimplify(ctx, analysisManager)
 
     assert(ir.invariant.programDiamondForm(ctx.program))
+    assert(ir.invariant.readUninitialised(ctx.program))
 
     transforms.inlinePLTLaunchpad(ctx, analysisManager)
 
@@ -84,6 +85,7 @@ object RunUtils {
     if (q.loading.parameterForm && !q.simplify) {
       ir.transforms.clearParams(ctx.program)
       ctx = ir.transforms.liftProcedureCallAbstraction(ctx)
+    assert(ir.invariant.readUninitialised(ctx.program))
       if (conf.assertCalleeSaved) {
         transforms.CalleePreservedParam.transform(ctx.program)
       }
@@ -106,17 +108,21 @@ object RunUtils {
     }
     q.loading.dumpIL.foreach(s => DebugDumpIRLogger.writeToFile(File(s"$s-after-analysis.il"), pp_prog(ctx.program)))
 
+
     assert(ir.invariant.programDiamondForm(ctx.program))
     ir.eval.SimplifyValidation.validate = conf.validateSimp
     if (conf.simplify) {
 
       ir.transforms.clearParams(ctx.program)
 
+      assert(ir.invariant.readUninitialised(ctx.program))
       ir.transforms.liftIndirectCall(ctx.program)
       transforms.liftSVCompNonDetEarlyIR(ctx.program)
+      assert(ir.invariant.readUninitialised(ctx.program))
 
       DebugDumpIRLogger.writeToFile(File("il-after-indirectcalllift.il"), pp_prog(ctx.program))
       ctx = ir.transforms.liftProcedureCallAbstraction(ctx)
+      assert(ir.invariant.readUninitialised(ctx.program))
       DebugDumpIRLogger.writeToFile(File("il-after-proccalls.il"), pp_prog(ctx.program))
 
       if (conf.assertCalleeSaved) {

From ec5c964664be4f03fc4b9388c92082196e902b63 Mon Sep 17 00:00:00 2001
From: am <a.michael1@uq.edu.au>
Date: Wed, 17 Sep 2025 11:51:50 +1000
Subject: [PATCH 02/20] read-uninit check, run liveness on all procedures

---
 .../analysis/InterLiveVarsAnalysis.scala      | 30 +++++++++++++++++--
 .../scala/analysis/solvers/IDESolver.scala    | 18 +++++------
 .../ir/transforms/ProcedureParameters.scala   |  2 +-
 src/main/scala/translating/GTIRBLoader.scala  |  1 +
 src/main/scala/util/RunUtils.scala            |  1 +
 5 files changed, 38 insertions(+), 14 deletions(-)

diff --git a/src/main/scala/analysis/InterLiveVarsAnalysis.scala b/src/main/scala/analysis/InterLiveVarsAnalysis.scala
index d1c794c76..f74204766 100644
--- a/src/main/scala/analysis/InterLiveVarsAnalysis.scala
+++ b/src/main/scala/analysis/InterLiveVarsAnalysis.scala
@@ -2,6 +2,7 @@ package analysis
 
 import analysis.solvers.BackwardIDESolver
 import ir.{
+  LocalVar,
   Assert,
   Assume,
   CFGPosition,
@@ -136,6 +137,31 @@ 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) = {
+
+    val entries = program.procedures.filter(p => p.incomingCalls().size == 0 && p.entryBlock.isDefined && p.returnBlock.isDefined && p.blocks.nonEmpty)
+
+    var procedures = program.procedures.toSet
+    var segments = List[Procedure]()
+
+    val reachableEntry = program.mainProcedure.preOrderIterator.collect {
+        case p: Procedure => p
+      }
+
+    procedures = procedures -- reachableEntry
+
+    var r = Map[CFGPosition, Map[Variable, TwoElement]]()
+    for (p <- entries) {
+      r = r ++ InterLiveVarsAnalysis(program, ignoreExternals, Some(p)).analyze()
+    }
+    r
+
+
+}
+
diff --git a/src/main/scala/analysis/solvers/IDESolver.scala b/src/main/scala/analysis/solvers/IDESolver.scala
index a711da891..2cb0f54bf 100644
--- a/src/main/scala/analysis/solvers/IDESolver.scala
+++ b/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()
-    }
   }
 }
 
-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,13 @@ 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)
+      {
+        val e = entry.getOrElse(program.mainProcedure) 
+        IRWalk.lastInProc(e).getOrElse(e)
+      }
     ),
       BackwardIDEAnalysis[D, T, L],
       IRInterproceduralBackwardDependencies {
diff --git a/src/main/scala/ir/transforms/ProcedureParameters.scala b/src/main/scala/ir/transforms/ProcedureParameters.scala
index a4c7453f1..13346ba8a 100644
--- a/src/main/scala/ir/transforms/ProcedureParameters.scala
+++ b/src/main/scala/ir/transforms/ProcedureParameters.scala
@@ -120,7 +120,7 @@ def liftProcedureCallAbstraction(ctx: ir.IRContext): ir.IRContext = {
   val mainHasEntry = ctx.program.mainProcedure.entryBlock.isDefined
 
   val liveVars = if (mainNonEmpty && mainHasEntry && mainHasReturn) {
-    analysis.InterLiveVarsAnalysis(ctx.program).analyze()
+    analysis.interLiveVarsAnalysis(ctx.program)
   } else {
     Logger.error(s"Empty live vars $mainNonEmpty $mainHasReturn $mainHasEntry")
     Map.empty
diff --git a/src/main/scala/translating/GTIRBLoader.scala b/src/main/scala/translating/GTIRBLoader.scala
index 7026ed5be..d8f9a2fa2 100644
--- a/src/main/scala/translating/GTIRBLoader.scala
+++ b/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)
diff --git a/src/main/scala/util/RunUtils.scala b/src/main/scala/util/RunUtils.scala
index 0a2bd18be..249424a4f 100644
--- a/src/main/scala/util/RunUtils.scala
+++ b/src/main/scala/util/RunUtils.scala
@@ -122,6 +122,7 @@ object RunUtils {
 
       DebugDumpIRLogger.writeToFile(File("il-after-indirectcalllift.il"), pp_prog(ctx.program))
       ctx = ir.transforms.liftProcedureCallAbstraction(ctx)
+      DebugDumpIRLogger.writeToFile(File("il-after-param.il"), pp_prog(ctx.program))
       assert(ir.invariant.readUninitialised(ctx.program))
       DebugDumpIRLogger.writeToFile(File("il-after-proccalls.il"), pp_prog(ctx.program))
 

From 71099c9604d9bd57ecd55bd6ee377c44bf104cec Mon Sep 17 00:00:00 2001
From: am <a.michael1@uq.edu.au>
Date: Wed, 17 Sep 2025 12:06:02 +1000
Subject: [PATCH 03/20] format

---
 .../analysis/InterLiveVarsAnalysis.scala      | 32 ++++++++---------
 .../scala/analysis/solvers/IDESolver.scala    | 11 +++---
 src/main/scala/ir/transforms/Inline.scala     |  4 +--
 .../scala/ir/transforms/ReplaceReturn.scala   |  1 -
 src/main/scala/ir/transforms/Simp.scala       | 35 +++++++++++--------
 src/main/scala/util/RunUtils.scala            |  3 +-
 6 files changed, 44 insertions(+), 42 deletions(-)

diff --git a/src/main/scala/analysis/InterLiveVarsAnalysis.scala b/src/main/scala/analysis/InterLiveVarsAnalysis.scala
index f74204766..464b69583 100644
--- a/src/main/scala/analysis/InterLiveVarsAnalysis.scala
+++ b/src/main/scala/analysis/InterLiveVarsAnalysis.scala
@@ -2,7 +2,6 @@ package analysis
 
 import analysis.solvers.BackwardIDESolver
 import ir.{
-  LocalVar,
   Assert,
   Assume,
   CFGPosition,
@@ -11,6 +10,7 @@ import ir.{
   GlobalVar,
   IndirectCall,
   LocalAssign,
+  LocalVar,
   MemoryLoad,
   MemoryStore,
   Procedure,
@@ -137,31 +137,29 @@ trait LiveVarsAnalysisFunctions(inline: Boolean, addExternals: Boolean = true)
   }
 }
 
-
-
 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) = {
 
-    val entries = program.procedures.filter(p => p.incomingCalls().size == 0 && p.entryBlock.isDefined && p.returnBlock.isDefined && p.blocks.nonEmpty)
-
-    var procedures = program.procedures.toSet
-    var segments = List[Procedure]()
+  val entries = program.procedures.filter(p =>
+    p.incomingCalls().size == 0 && p.entryBlock.isDefined && p.returnBlock.isDefined && p.blocks.nonEmpty
+  )
 
-    val reachableEntry = program.mainProcedure.preOrderIterator.collect {
-        case p: Procedure => p
-      }
+  var procedures = program.procedures.toSet
+  var segments = List[Procedure]()
 
-    procedures = procedures -- reachableEntry
+  val reachableEntry = program.mainProcedure.preOrderIterator.collect { case p: Procedure =>
+    p
+  }
 
-    var r = Map[CFGPosition, Map[Variable, TwoElement]]()
-    for (p <- entries) {
-      r = r ++ InterLiveVarsAnalysis(program, ignoreExternals, Some(p)).analyze()
-    }
-    r
+  procedures = procedures -- reachableEntry
 
+  var r = Map[CFGPosition, Map[Variable, TwoElement]]()
+  for (p <- entries) {
+    r = r ++ InterLiveVarsAnalysis(program, ignoreExternals, Some(p)).analyze()
+  }
+  r
 
 }
-
diff --git a/src/main/scala/analysis/solvers/IDESolver.scala b/src/main/scala/analysis/solvers/IDESolver.scala
index 2cb0f54bf..104fa90bf 100644
--- a/src/main/scala/analysis/solvers/IDESolver.scala
+++ b/src/main/scala/analysis/solvers/IDESolver.scala
@@ -245,9 +245,9 @@ abstract class IDESolver[
   }
 
   def analyze(): Map[CFGPosition, Map[D, T]] = {
-      val phase1 = Phase1()
-      val phase2 = Phase2(phase1)
-      phase2.restructure(phase2.analyze())
+    val phase1 = Phase1()
+    val phase2 = Phase2(phase1)
+    phase2.restructure(phase2.analyze())
   }
 }
 
@@ -297,9 +297,8 @@ abstract class ForwardIDESolver[D, T, L <: Lattice[T]](program: Program, entry:
 
 abstract class BackwardIDESolver[D, T, L <: Lattice[T]](program: Program, entry: Option[Procedure] = None)
     extends IDESolver[Return, Procedure, Command, DirectCall, D, T, L](
-      program,
-      {
-        val e = entry.getOrElse(program.mainProcedure) 
+      program, {
+        val e = entry.getOrElse(program.mainProcedure)
         IRWalk.lastInProc(e).getOrElse(e)
       }
     ),
diff --git a/src/main/scala/ir/transforms/Inline.scala b/src/main/scala/ir/transforms/Inline.scala
index b07671f70..699211032 100644
--- a/src/main/scala/ir/transforms/Inline.scala
+++ b/src/main/scala/ir/transforms/Inline.scala
@@ -28,10 +28,10 @@ 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") => {
+    // case l: LocalVar if l.name.endsWith("_in") => {
     //  val name = l.name.stripSuffix("_in")
     //  proc.getFreshSSAVar(name, l.getType)
-    //}
+    // }
     case l: LocalVar =>
       proc.getFreshSSAVar(l.varName, l.getType)
     case _ => v
diff --git a/src/main/scala/ir/transforms/ReplaceReturn.scala b/src/main/scala/ir/transforms/ReplaceReturn.scala
index ff2883c13..5b1aafd09 100644
--- a/src/main/scala/ir/transforms/ReplaceReturn.scala
+++ b/src/main/scala/ir/transforms/ReplaceReturn.scala
@@ -92,7 +92,6 @@ def addReturnBlocks(p: Program, toAll: Boolean = false): Unit = {
     val returningBlocks = p.blocks.filter(_.jump.isInstanceOf[Return]).toList
     val containsReturn = returningBlocks.nonEmpty
 
-
     if (
       returningBlocks.size == 1 && !p.entryBlock.contains(returningBlocks.head)
       && returningBlocks.forall(_.statements.isEmpty)
diff --git a/src/main/scala/ir/transforms/Simp.scala b/src/main/scala/ir/transforms/Simp.scala
index 807a190da..811d07cde 100644
--- a/src/main/scala/ir/transforms/Simp.scala
+++ b/src/main/scala/ir/transforms/Simp.scala
@@ -1267,39 +1267,46 @@ object OffsetProp {
       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 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")
+      }
 
-    final def find(v: Variable, ret: BitVecLiteral | Variable | BinaryExpr =>  BitVecLiteral | Variable | BinaryExpr = x => x, fuel: Int = 5000): BitVecLiteral | Variable | BinaryExpr = {
+    final def find(
+      v: Variable,
+      ret: BitVecLiteral | Variable | BinaryExpr => BitVecLiteral | Variable | BinaryExpr = x => x,
+      fuel: Int = 5000
+    ): 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 => 
+            case o =>
               println(o)
               chain
           }
         }
-        throw Exception(s"Ran out of fuel recursively resolving copyprop (at $v): probable cycle. Next lookups are: $chain")
+        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)) => ret(v)
         case Some((None, Some(c))) => ret(c)
-        //case Some((Some(c), None)) if c == v => ret(c)
+        // case Some((Some(c), None)) if c == v => ret(c)
         case Some((Some(v), None)) => find(v, ret, fuel - 1)
-        //case Some((Some(v2), Some(c))) if v2 == v => eval(c)(v2)
+        // case Some((Some(v2), Some(c))) if v2 == v => eval(c)(v2)
         case Some((Some(v), Some(c))) => find(v, eval(c), fuel - 1)
       }
     }
 
-    def findOff(v: BitVecLiteral, e: Variable) : BitVecLiteral | Variable | BinaryExpr = find(e, eval(v))
+    def findOff(v: BitVecLiteral, e: Variable): BitVecLiteral | Variable | BinaryExpr = find(e, eval(v))
 
     def joinState(lhs: Variable, rhs: Expr) = {
       specJoinState(lhs, rhs) match {
@@ -1343,7 +1350,7 @@ object OffsetProp {
             case (l: Variable, _) => Seq(l -> (None, None))
           }
           .foreach { case (l, r) =>
-            if (!st.get(l).contains(r))  {
+            if (!st.get(l).contains(r)) {
               stSequenceNo += 1
             }
             st(l) = r
diff --git a/src/main/scala/util/RunUtils.scala b/src/main/scala/util/RunUtils.scala
index 249424a4f..a625c6fe4 100644
--- a/src/main/scala/util/RunUtils.scala
+++ b/src/main/scala/util/RunUtils.scala
@@ -85,7 +85,7 @@ object RunUtils {
     if (q.loading.parameterForm && !q.simplify) {
       ir.transforms.clearParams(ctx.program)
       ctx = ir.transforms.liftProcedureCallAbstraction(ctx)
-    assert(ir.invariant.readUninitialised(ctx.program))
+      assert(ir.invariant.readUninitialised(ctx.program))
       if (conf.assertCalleeSaved) {
         transforms.CalleePreservedParam.transform(ctx.program)
       }
@@ -108,7 +108,6 @@ object RunUtils {
     }
     q.loading.dumpIL.foreach(s => DebugDumpIRLogger.writeToFile(File(s"$s-after-analysis.il"), pp_prog(ctx.program)))
 
-
     assert(ir.invariant.programDiamondForm(ctx.program))
     ir.eval.SimplifyValidation.validate = conf.validateSimp
     if (conf.simplify) {

From d1c7cb24485d3a1f9b4fa8fbf2c1d6837d7ea9ab Mon Sep 17 00:00:00 2001
From: am <a.michael1@uq.edu.au>
Date: Wed, 17 Sep 2025 12:14:43 +1000
Subject: [PATCH 04/20] cleanup

---
 src/main/scala/analysis/InterLiveVarsAnalysis.scala    |  9 ---------
 .../scala/ir/transforms/DynamicSingleAssignment.scala  |  2 +-
 src/main/scala/ir/transforms/Inline.scala              | 10 +++++-----
 src/main/scala/ir/transforms/Simp.scala                |  2 --
 src/main/scala/ir/transforms/SimplifyPipeline.scala    |  6 +++++-
 src/main/scala/util/RunUtils.scala                     |  9 +++++----
 6 files changed, 16 insertions(+), 22 deletions(-)

diff --git a/src/main/scala/analysis/InterLiveVarsAnalysis.scala b/src/main/scala/analysis/InterLiveVarsAnalysis.scala
index 464b69583..fb5fb92d2 100644
--- a/src/main/scala/analysis/InterLiveVarsAnalysis.scala
+++ b/src/main/scala/analysis/InterLiveVarsAnalysis.scala
@@ -147,15 +147,6 @@ def interLiveVarsAnalysis(program: Program, ignoreExternals: Boolean = false) =
     p.incomingCalls().size == 0 && p.entryBlock.isDefined && p.returnBlock.isDefined && p.blocks.nonEmpty
   )
 
-  var procedures = program.procedures.toSet
-  var segments = List[Procedure]()
-
-  val reachableEntry = program.mainProcedure.preOrderIterator.collect { case p: Procedure =>
-    p
-  }
-
-  procedures = procedures -- reachableEntry
-
   var r = Map[CFGPosition, Map[Variable, TwoElement]]()
   for (p <- entries) {
     r = r ++ InterLiveVarsAnalysis(program, ignoreExternals, Some(p)).analyze()
diff --git a/src/main/scala/ir/transforms/DynamicSingleAssignment.scala b/src/main/scala/ir/transforms/DynamicSingleAssignment.scala
index d03ea258e..a205b97c3 100644
--- a/src/main/scala/ir/transforms/DynamicSingleAssignment.scala
+++ b/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(p.ssaCount)
+    val count = mutable.Map[Variable, Int]().withDefaultValue(0)
 
     while (worklist.nonEmpty) {
       while (worklist.nonEmpty) {
diff --git a/src/main/scala/ir/transforms/Inline.scala b/src/main/scala/ir/transforms/Inline.scala
index 699211032..3cb11c327 100644
--- a/src/main/scala/ir/transforms/Inline.scala
+++ b/src/main/scala/ir/transforms/Inline.scala
@@ -28,11 +28,11 @@ 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 =>
+    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 =>
       proc.getFreshSSAVar(l.varName, l.getType)
     case _ => v
   }
diff --git a/src/main/scala/ir/transforms/Simp.scala b/src/main/scala/ir/transforms/Simp.scala
index 811d07cde..9ca6c06ac 100644
--- a/src/main/scala/ir/transforms/Simp.scala
+++ b/src/main/scala/ir/transforms/Simp.scala
@@ -1299,9 +1299,7 @@ object OffsetProp {
         case None => v
         case Some((None, None)) => ret(v)
         case Some((None, Some(c))) => ret(c)
-        // case Some((Some(c), None)) if c == v => ret(c)
         case Some((Some(v), None)) => find(v, ret, fuel - 1)
-        // case Some((Some(v2), Some(c))) if v2 == v => eval(c)(v2)
         case Some((Some(v), Some(c))) => find(v, eval(c), fuel - 1)
       }
     }
diff --git a/src/main/scala/ir/transforms/SimplifyPipeline.scala b/src/main/scala/ir/transforms/SimplifyPipeline.scala
index a6dd3275b..0a23d884b 100644
--- a/src/main/scala/ir/transforms/SimplifyPipeline.scala
+++ b/src/main/scala/ir/transforms/SimplifyPipeline.scala
@@ -74,8 +74,12 @@ def doSimplify(ctx: IRContext, config: Option[StaticAnalysisConfig]): Unit = {
       )
     }
   }
+  config.foreach {
+    _.dumpILToPath.foreach { s =>
+      DebugDumpIRLogger.writeToFile(File(s"${s}_il-after-dsa.il"), pp_prog(program))
+    }
+  }
 
-  DebugDumpIRLogger.writeToFile(File(s"il-after-dsa.il"), pp_prog(program))
   if (ir.eval.SimplifyValidation.validate) {
     Logger.info("DSA no uninitialised")
     assert(invariant.allVariablesAssignedIndex(program))
diff --git a/src/main/scala/util/RunUtils.scala b/src/main/scala/util/RunUtils.scala
index a625c6fe4..10d1d16da 100644
--- a/src/main/scala/util/RunUtils.scala
+++ b/src/main/scala/util/RunUtils.scala
@@ -56,22 +56,23 @@ object RunUtils {
     var ctx = q.context.getOrElse(IRLoading.load(q.loading))
     postLoad(ctx) // allows extracting information from the original loaded program
 
-    assert(ir.invariant.checkTypeCorrect(ctx.program))
+    assert(invariant.checkTypeCorrect(ctx.program))
     assert(invariant.singleCallBlockEnd(ctx.program))
     assert(invariant.cfgCorrect(ctx.program))
     assert(invariant.blocksUniqueToEachProcedure(ctx.program))
+    assert(invariant.readUninitialised(ctx.program))
 
     val analysisManager = AnalysisManager(ctx.program)
 
     if conf.simplify then doCleanupWithSimplify(ctx, analysisManager)
     else doCleanupWithoutSimplify(ctx, analysisManager)
 
-    assert(ir.invariant.programDiamondForm(ctx.program))
-    assert(ir.invariant.readUninitialised(ctx.program))
+    assert(invariant.programDiamondForm(ctx.program))
+    assert(invariant.readUninitialised(ctx.program))
 
     transforms.inlinePLTLaunchpad(ctx, analysisManager)
 
-    assert(ir.invariant.programDiamondForm(ctx.program))
+    assert(invariant.programDiamondForm(ctx.program))
 
     if q.loading.trimEarly then
       getStripUnreachableFunctionsTransform(q.loading.procedureTrimDepth)(ctx, analysisManager)

From e144aa186311775f22766c7aa5cb554f46eaeef9 Mon Sep 17 00:00:00 2001
From: am <a.michael1@uq.edu.au>
Date: Wed, 17 Sep 2025 12:17:59 +1000
Subject: [PATCH 05/20] add invariant

---
 .../ir/invariant/ReadUninitialised.scala      | 55 +++++++++++++++++++
 1 file changed, 55 insertions(+)
 create mode 100644 src/main/scala/ir/invariant/ReadUninitialised.scala

diff --git a/src/main/scala/ir/invariant/ReadUninitialised.scala b/src/main/scala/ir/invariant/ReadUninitialised.scala
new file mode 100644
index 000000000..79577cf93
--- /dev/null
+++ b/src/main/scala/ir/invariant/ReadUninitialised.scala
@@ -0,0 +1,55 @@
+package ir.invariant
+
+import ir.*
+import util.Logger
+
+import scala.collection.mutable
+
+def readUninitialised(p: Procedure): Boolean = {
+  ir.transforms.reversePostOrder(p)
+
+  val worklist = mutable.PriorityQueue[Block]()(Ordering.by(_.rpoOrder))
+  worklist.addAll(p.blocks)
+
+  var init = Set[Variable]() ++ p.formalInParam
+  var readUninit = List[(Command, Set[Variable])]()
+
+  def check(a: Command) = {
+    val free = freeVarsPos(a).filter(_.isInstanceOf[LocalVar]) -- init
+    if (free.size > 0) {
+      readUninit = (a, free) :: readUninit
+    }
+  }
+
+  while (worklist.nonEmpty) {
+    val b = worklist.dequeue()
+    b.statements.foreach {
+      case a: Assign => {
+        check(a)
+        init = init ++ a.assignees
+      }
+      case o => {
+        check(o)
+      }
+    }
+    check(b.jump)
+  }
+
+  if (readUninit.size > 0) {
+    Logger.error(p.name)
+    val msg = readUninit
+      .map { case (s, vars) =>
+        s"   ${vars.mkString(", ")} uninitialised in statement $s"
+      }
+      .mkString("\n")
+    Logger.error(msg)
+    true
+  } else {
+    false
+  }
+}
+
+def readUninitialised(p: Program): Boolean = {
+  val r = p.procedures.map(readUninitialised)
+  r.forall(x => !x)
+}

From 0a2907342ad0dd55134f6eb9cbfbb75037293a60 Mon Sep 17 00:00:00 2001
From: am <a.michael1@uq.edu.au>
Date: Wed, 17 Sep 2025 13:52:42 +1000
Subject: [PATCH 06/20] ensure r30 set when used

---
 src/main/scala/analysis/InterLiveVarsAnalysis.scala | 1 -
 src/main/scala/ir/transforms/Simp.scala             | 1 +
 src/test/scala/MemoryTransformTests.scala           | 1 +
 3 files changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/main/scala/analysis/InterLiveVarsAnalysis.scala b/src/main/scala/analysis/InterLiveVarsAnalysis.scala
index fb5fb92d2..a67460da0 100644
--- a/src/main/scala/analysis/InterLiveVarsAnalysis.scala
+++ b/src/main/scala/analysis/InterLiveVarsAnalysis.scala
@@ -10,7 +10,6 @@ import ir.{
   GlobalVar,
   IndirectCall,
   LocalAssign,
-  LocalVar,
   MemoryLoad,
   MemoryStore,
   Procedure,
diff --git a/src/main/scala/ir/transforms/Simp.scala b/src/main/scala/ir/transforms/Simp.scala
index 9ca6c06ac..77ad4f29f 100644
--- a/src/main/scala/ir/transforms/Simp.scala
+++ b/src/main/scala/ir/transforms/Simp.scala
@@ -2079,6 +2079,7 @@ def getDoCleanupTransform(doSimplify: Boolean): Transform = TransformBatch(
     assert(invariant.cfgCorrect(ctx.program))
     assert(invariant.blocksUniqueToEachProcedure(ctx.program))
     assert(invariant.procEntryNoIncoming(ctx.program))
+    assert(invariant.readUninitialised(ctx.program))
   }
 )
 
diff --git a/src/test/scala/MemoryTransformTests.scala b/src/test/scala/MemoryTransformTests.scala
index 63c08b2d8..9658f8621 100644
--- a/src/test/scala/MemoryTransformTests.scala
+++ b/src/test/scala/MemoryTransformTests.scala
@@ -224,6 +224,7 @@ class MemoryTransformTests extends AnyFunSuite with CaptureOutput {
     )
 
     val context = programToContext(program, globals)
+    translating.PrettyPrinter.pp_prog(context.program)
     val results = runTest(context)
 
     val loads = results.ir.program.collect { case la: MemoryLoad => la }

From d2fc2ccc2df62bdb3524c01b6a42eb5278c35579 Mon Sep 17 00:00:00 2001
From: am <a.michael1@uq.edu.au>
Date: Wed, 17 Sep 2025 15:01:15 +1000
Subject: [PATCH 07/20] fix inlining

---
 src/main/scala/ir/transforms/DynamicSingleAssignment.scala | 2 +-
 src/main/scala/ir/transforms/Inline.scala                  | 6 +-----
 2 files changed, 2 insertions(+), 6 deletions(-)

diff --git a/src/main/scala/ir/transforms/DynamicSingleAssignment.scala b/src/main/scala/ir/transforms/DynamicSingleAssignment.scala
index a205b97c3..d03ea258e 100644
--- a/src/main/scala/ir/transforms/DynamicSingleAssignment.scala
+++ b/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) {
diff --git a/src/main/scala/ir/transforms/Inline.scala b/src/main/scala/ir/transforms/Inline.scala
index 3cb11c327..9421ec601 100644
--- a/src/main/scala/ir/transforms/Inline.scala
+++ b/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
   }

From c1a513198c4e0102a89f2be2b0ce3b9bde3c40bc Mon Sep 17 00:00:00 2001
From: am <a.michael1@uq.edu.au>
Date: Wed, 17 Sep 2025 15:27:55 +1000
Subject: [PATCH 08/20] fix-simp

---
 .../ir/invariant/ReadUninitialised.scala      |  5 ++++-
 .../ir/transforms/ProcedureParameters.scala   |  2 +-
 src/main/scala/ir/transforms/Simp.scala       | 22 +++----------------
 src/test/scala/MemoryTransformTests.scala     |  1 -
 4 files changed, 8 insertions(+), 22 deletions(-)

diff --git a/src/main/scala/ir/invariant/ReadUninitialised.scala b/src/main/scala/ir/invariant/ReadUninitialised.scala
index 79577cf93..d69005e40 100644
--- a/src/main/scala/ir/invariant/ReadUninitialised.scala
+++ b/src/main/scala/ir/invariant/ReadUninitialised.scala
@@ -50,6 +50,9 @@ def readUninitialised(p: Procedure): Boolean = {
 }
 
 def readUninitialised(p: Program): Boolean = {
-  val r = p.procedures.map(readUninitialised)
+  var reach = p.mainProcedure.collect { case p: Procedure =>
+    p
+  }
+  val r = reach.map(readUninitialised)
   r.forall(x => !x)
 }
diff --git a/src/main/scala/ir/transforms/ProcedureParameters.scala b/src/main/scala/ir/transforms/ProcedureParameters.scala
index 13346ba8a..a4c7453f1 100644
--- a/src/main/scala/ir/transforms/ProcedureParameters.scala
+++ b/src/main/scala/ir/transforms/ProcedureParameters.scala
@@ -120,7 +120,7 @@ def liftProcedureCallAbstraction(ctx: ir.IRContext): ir.IRContext = {
   val mainHasEntry = ctx.program.mainProcedure.entryBlock.isDefined
 
   val liveVars = if (mainNonEmpty && mainHasEntry && mainHasReturn) {
-    analysis.interLiveVarsAnalysis(ctx.program)
+    analysis.InterLiveVarsAnalysis(ctx.program).analyze()
   } else {
     Logger.error(s"Empty live vars $mainNonEmpty $mainHasReturn $mainHasEntry")
     Map.empty
diff --git a/src/main/scala/ir/transforms/Simp.scala b/src/main/scala/ir/transforms/Simp.scala
index 77ad4f29f..ab8494974 100644
--- a/src/main/scala/ir/transforms/Simp.scala
+++ b/src/main/scala/ir/transforms/Simp.scala
@@ -1259,14 +1259,6 @@ object OffsetProp {
     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)
@@ -1287,7 +1279,6 @@ object OffsetProp {
           chain = st.get(chain.head) match {
             case Some((Some(v: Variable), _)) => v :: chain
             case o =>
-              println(o)
               chain
           }
         }
@@ -1299,12 +1290,12 @@ object OffsetProp {
         case None => v
         case Some((None, None)) => ret(v)
         case Some((None, Some(c))) => ret(c)
-        case Some((Some(v), None)) => find(v, ret, fuel - 1)
-        case Some((Some(v), Some(c))) => find(v, eval(c), fuel - 1)
+        case Some((Some(v), None)) => ret(find(v, x => x, fuel - 1))
+        case Some((Some(v), Some(c))) => ret(find(v, eval(c), fuel - 1))
       }
     }
 
-    def findOff(v: BitVecLiteral, e: Variable): BitVecLiteral | Variable | BinaryExpr = find(e, eval(v))
+    def findOff(e: Variable, v: BitVecLiteral): BitVecLiteral | Variable | BinaryExpr = eval(v)(find(e))
 
     def joinState(lhs: Variable, rhs: Expr) = {
       specJoinState(lhs, rhs) match {
@@ -1332,9 +1323,6 @@ object OffsetProp {
     }
 
     def clob(v: Variable) = {
-      if (!st.get(v).contains((None, None))) {
-        stSequenceNo += 1
-      }
       st(v) = (None, None)
     }
 
@@ -1348,9 +1336,6 @@ object OffsetProp {
             case (l: Variable, _) => Seq(l -> (None, None))
           }
           .foreach { case (l, r) =>
-            if (!st.get(l).contains(r)) {
-              stSequenceNo += 1
-            }
             st(l) = r
           }
       case a: Assign => {
@@ -2079,7 +2064,6 @@ def getDoCleanupTransform(doSimplify: Boolean): Transform = TransformBatch(
     assert(invariant.cfgCorrect(ctx.program))
     assert(invariant.blocksUniqueToEachProcedure(ctx.program))
     assert(invariant.procEntryNoIncoming(ctx.program))
-    assert(invariant.readUninitialised(ctx.program))
   }
 )
 
diff --git a/src/test/scala/MemoryTransformTests.scala b/src/test/scala/MemoryTransformTests.scala
index 9658f8621..63c08b2d8 100644
--- a/src/test/scala/MemoryTransformTests.scala
+++ b/src/test/scala/MemoryTransformTests.scala
@@ -224,7 +224,6 @@ class MemoryTransformTests extends AnyFunSuite with CaptureOutput {
     )
 
     val context = programToContext(program, globals)
-    translating.PrettyPrinter.pp_prog(context.program)
     val results = runTest(context)
 
     val loads = results.ir.program.collect { case la: MemoryLoad => la }

From cfda25d558152819eb49bf0d92fd641cfaaa82a8 Mon Sep 17 00:00:00 2001
From: am <a.michael1@uq.edu.au>
Date: Wed, 17 Sep 2025 17:57:13 +1000
Subject: [PATCH 09/20] identify stack collapses

---
 src/main/scala/analysis/InterLiveVarsAnalysis.scala | 2 ++
 src/test/scala/IntervalDSATest.scala                | 6 +++++-
 2 files changed, 7 insertions(+), 1 deletion(-)

diff --git a/src/main/scala/analysis/InterLiveVarsAnalysis.scala b/src/main/scala/analysis/InterLiveVarsAnalysis.scala
index a67460da0..d6079fd4d 100644
--- a/src/main/scala/analysis/InterLiveVarsAnalysis.scala
+++ b/src/main/scala/analysis/InterLiveVarsAnalysis.scala
@@ -146,6 +146,8 @@ def interLiveVarsAnalysis(program: Program, ignoreExternals: Boolean = false) =
     p.incomingCalls().size == 0 && p.entryBlock.isDefined && p.returnBlock.isDefined && p.blocks.nonEmpty
   )
 
+  assert(entries.toSet.flatMap(_.reachableFrom).contains(program.mainProcedure))
+
   var r = Map[CFGPosition, Map[Variable, TwoElement]]()
   for (p <- entries) {
     r = r ++ InterLiveVarsAnalysis(program, ignoreExternals, Some(p)).analyze()
diff --git a/src/test/scala/IntervalDSATest.scala b/src/test/scala/IntervalDSATest.scala
index 2d723037b..f7e2f4766 100644
--- a/src/test/scala/IntervalDSATest.scala
+++ b/src/test/scala/IntervalDSATest.scala
@@ -620,7 +620,11 @@ class IntervalDSATest extends AnyFunSuite with test_util.CaptureOutput {
       "direct_request",
       "forward_request",
       "tunnel_add",
-      "magic_auth_detect"
+      "magic_auth_detect",
+      "hlist_subcmp_all",
+      "headers_recv",
+      "scanner_hook",
+      "config_open"
     )
     val globalCollapsed = Set("to_base64", "printmem", "gl_des_ecb_crypt", "from_base64", "des_key_schedule", "scanmem")
     val locals = res.dsa.get.local

From 73c1f5cff0d920ca39cea5bdd5335d238a94ff55 Mon Sep 17 00:00:00 2001
From: am <a.michael1@uq.edu.au>
Date: Thu, 18 Sep 2025 11:11:40 +1000
Subject: [PATCH 10/20] ensure not re-analysing liveness

---
 .../scala/analysis/InterLiveVarsAnalysis.scala  | 17 +++++++++++------
 .../scala/ir/invariant/ReadUninitialised.scala  |  5 +----
 .../ir/transforms/ProcedureParameters.scala     |  2 +-
 src/test/scala/IntervalDSATest.scala            |  3 +++
 4 files changed, 16 insertions(+), 11 deletions(-)

diff --git a/src/main/scala/analysis/InterLiveVarsAnalysis.scala b/src/main/scala/analysis/InterLiveVarsAnalysis.scala
index d6079fd4d..92de89cd1 100644
--- a/src/main/scala/analysis/InterLiveVarsAnalysis.scala
+++ b/src/main/scala/analysis/InterLiveVarsAnalysis.scala
@@ -1,6 +1,7 @@
 package analysis
 
 import analysis.solvers.BackwardIDESolver
+import scala.collection.immutable.ListSet
 import ir.{
   Assert,
   Assume,
@@ -140,16 +141,20 @@ class InterLiveVarsAnalysis(program: Program, ignoreExternals: Boolean = false,
     extends BackwardIDESolver[Variable, TwoElement, TwoElementLattice](program, entry),
       LiveVarsAnalysisFunctions(true, !ignoreExternals)
 
-def interLiveVarsAnalysis(program: Program, ignoreExternals: Boolean = false) = {
+def interLiveVarsAnalysis(program: Program, ignoreExternals: Boolean = false) : Map[CFGPosition, Map[Variable, TwoElement]] = {
 
-  val entries = program.procedures.filter(p =>
-    p.incomingCalls().size == 0 && p.entryBlock.isDefined && p.returnBlock.isDefined && p.blocks.nonEmpty
-  )
+  var procs = ListSet.from(program.procedures)
+  var starts = List[Procedure]()
 
-  assert(entries.toSet.flatMap(_.reachableFrom).contains(program.mainProcedure))
+  while (procs.nonEmpty) {
+    val entries = procs.toList.filter(p => p.incomingCalls().size == 0 && p.entryBlock.isDefined && p.returnBlock.isDefined && p.blocks.nonEmpty)
+    starts = entries.head :: starts
+    val done = entries.head.reachableFrom
+    procs = procs -- done
+  }
 
   var r = Map[CFGPosition, Map[Variable, TwoElement]]()
-  for (p <- entries) {
+  for (p <- starts) {
     r = r ++ InterLiveVarsAnalysis(program, ignoreExternals, Some(p)).analyze()
   }
   r
diff --git a/src/main/scala/ir/invariant/ReadUninitialised.scala b/src/main/scala/ir/invariant/ReadUninitialised.scala
index d69005e40..79577cf93 100644
--- a/src/main/scala/ir/invariant/ReadUninitialised.scala
+++ b/src/main/scala/ir/invariant/ReadUninitialised.scala
@@ -50,9 +50,6 @@ def readUninitialised(p: Procedure): Boolean = {
 }
 
 def readUninitialised(p: Program): Boolean = {
-  var reach = p.mainProcedure.collect { case p: Procedure =>
-    p
-  }
-  val r = reach.map(readUninitialised)
+  val r = p.procedures.map(readUninitialised)
   r.forall(x => !x)
 }
diff --git a/src/main/scala/ir/transforms/ProcedureParameters.scala b/src/main/scala/ir/transforms/ProcedureParameters.scala
index a4c7453f1..13346ba8a 100644
--- a/src/main/scala/ir/transforms/ProcedureParameters.scala
+++ b/src/main/scala/ir/transforms/ProcedureParameters.scala
@@ -120,7 +120,7 @@ def liftProcedureCallAbstraction(ctx: ir.IRContext): ir.IRContext = {
   val mainHasEntry = ctx.program.mainProcedure.entryBlock.isDefined
 
   val liveVars = if (mainNonEmpty && mainHasEntry && mainHasReturn) {
-    analysis.InterLiveVarsAnalysis(ctx.program).analyze()
+    analysis.interLiveVarsAnalysis(ctx.program)
   } else {
     Logger.error(s"Empty live vars $mainNonEmpty $mainHasReturn $mainHasEntry")
     Map.empty
diff --git a/src/test/scala/IntervalDSATest.scala b/src/test/scala/IntervalDSATest.scala
index f7e2f4766..09e874222 100644
--- a/src/test/scala/IntervalDSATest.scala
+++ b/src/test/scala/IntervalDSATest.scala
@@ -630,6 +630,9 @@ class IntervalDSATest extends AnyFunSuite with test_util.CaptureOutput {
     val locals = res.dsa.get.local
     assert(locals.values.forall(_.glIntervals.size == 1))
 
+
+    println(locals.values.filter(g => stackCollapsed.contains(g.proc.procName)).map(_.proc.procName).toSet)
+
     assert(
       locals.values.filterNot(g => stackCollapsed.contains(g.proc.procName)).forall(IntervalDSA.checksStackMaintained)
     )

From b9ce4bf05a2f812bf429ce81bb648c1e2c4da6b0 Mon Sep 17 00:00:00 2001
From: am <a.michael1@uq.edu.au>
Date: Wed, 10 Sep 2025 16:59:25 +1000
Subject: [PATCH 11/20] fix flow sensitivity of offsetprop clobber

---
 src/main/scala/ir/transforms/Simp.scala | 32 ++++++-------------------
 1 file changed, 7 insertions(+), 25 deletions(-)

diff --git a/src/main/scala/ir/transforms/Simp.scala b/src/main/scala/ir/transforms/Simp.scala
index ab8494974..831f7bd8a 100644
--- a/src/main/scala/ir/transforms/Simp.scala
+++ b/src/main/scala/ir/transforms/Simp.scala
@@ -1244,15 +1244,6 @@ 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
@@ -1297,18 +1288,6 @@ object OffsetProp {
 
     def findOff(e: Variable, v: BitVecLiteral): BitVecLiteral | Variable | BinaryExpr = eval(v)(find(e))
 
-    def joinState(lhs: Variable, rhs: Expr) = {
-      specJoinState(lhs, rhs) match {
-        case Some((l, r)) => {
-          if (st.contains(l) && st(l) != r) {
-            stSequenceNo += 1
-          }
-          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)) =>
@@ -1322,8 +1301,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 {
@@ -1336,11 +1318,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 => ()

From 1e95df083998f2b5a2b3da86e376298600542ebb Mon Sep 17 00:00:00 2001
From: am <a.michael1@uq.edu.au>
Date: Thu, 18 Sep 2025 12:17:21 +1000
Subject: [PATCH 12/20] print

---
 src/test/scala/IntervalDSATest.scala | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/test/scala/IntervalDSATest.scala b/src/test/scala/IntervalDSATest.scala
index 09e874222..095b2dca2 100644
--- a/src/test/scala/IntervalDSATest.scala
+++ b/src/test/scala/IntervalDSATest.scala
@@ -631,7 +631,7 @@ class IntervalDSATest extends AnyFunSuite with test_util.CaptureOutput {
     assert(locals.values.forall(_.glIntervals.size == 1))
 
 
-    println(locals.values.filter(g => stackCollapsed.contains(g.proc.procName)).map(_.proc.procName).toSet)
+    println(locals.values.filterNot(IntervalDSA.checksStackMaintained).map(_.proc.procName).toSet)
 
     assert(
       locals.values.filterNot(g => stackCollapsed.contains(g.proc.procName)).forall(IntervalDSA.checksStackMaintained)

From 00fc9c3a7d9ddc9d7308d1523b89fc1408c7d2e8 Mon Sep 17 00:00:00 2001
From: am <a.michael1@uq.edu.au>
Date: Thu, 18 Sep 2025 12:22:53 +1000
Subject: [PATCH 13/20] fmt

---
 src/main/scala/analysis/InterLiveVarsAnalysis.scala | 12 +++++++++---
 src/main/scala/util/RunUtils.scala                  |  1 +
 src/test/scala/IntervalDSATest.scala                |  1 -
 3 files changed, 10 insertions(+), 4 deletions(-)

diff --git a/src/main/scala/analysis/InterLiveVarsAnalysis.scala b/src/main/scala/analysis/InterLiveVarsAnalysis.scala
index 92de89cd1..a6d2b7628 100644
--- a/src/main/scala/analysis/InterLiveVarsAnalysis.scala
+++ b/src/main/scala/analysis/InterLiveVarsAnalysis.scala
@@ -1,7 +1,6 @@
 package analysis
 
 import analysis.solvers.BackwardIDESolver
-import scala.collection.immutable.ListSet
 import ir.{
   Assert,
   Assume,
@@ -19,6 +18,8 @@ import ir.{
   Variable
 }
 
+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
  *  (registers) are propagated to and from callee functions. The result of which variables are alive at each point in
@@ -141,13 +142,18 @@ class InterLiveVarsAnalysis(program: Program, ignoreExternals: Boolean = false,
     extends BackwardIDESolver[Variable, TwoElement, TwoElementLattice](program, entry),
       LiveVarsAnalysisFunctions(true, !ignoreExternals)
 
-def interLiveVarsAnalysis(program: Program, ignoreExternals: Boolean = false) : Map[CFGPosition, Map[Variable, TwoElement]] = {
+def interLiveVarsAnalysis(
+  program: Program,
+  ignoreExternals: Boolean = false
+): Map[CFGPosition, Map[Variable, TwoElement]] = {
 
   var procs = ListSet.from(program.procedures)
   var starts = List[Procedure]()
 
   while (procs.nonEmpty) {
-    val entries = procs.toList.filter(p => p.incomingCalls().size == 0 && p.entryBlock.isDefined && p.returnBlock.isDefined && p.blocks.nonEmpty)
+    val entries = procs.toList.filter(p =>
+      p.incomingCalls().size == 0 && p.entryBlock.isDefined && p.returnBlock.isDefined && p.blocks.nonEmpty
+    )
     starts = entries.head :: starts
     val done = entries.head.reachableFrom
     procs = procs -- done
diff --git a/src/main/scala/util/RunUtils.scala b/src/main/scala/util/RunUtils.scala
index 10d1d16da..994e905b4 100644
--- a/src/main/scala/util/RunUtils.scala
+++ b/src/main/scala/util/RunUtils.scala
@@ -154,6 +154,7 @@ object RunUtils {
         val memTransferTimer = PerformanceTimer("Mem Transfer Timer", INFO)
         visit_prog(MemoryTransform(dsaResults.topDown, dsaResults.globals), ctx.program)
         memTransferTimer.checkPoint("Performed Memory Transform")
+        invariant.readUninitialised(ctx.program)
     }
 
     if q.summariseProcedures then
diff --git a/src/test/scala/IntervalDSATest.scala b/src/test/scala/IntervalDSATest.scala
index 095b2dca2..534821f15 100644
--- a/src/test/scala/IntervalDSATest.scala
+++ b/src/test/scala/IntervalDSATest.scala
@@ -630,7 +630,6 @@ class IntervalDSATest extends AnyFunSuite with test_util.CaptureOutput {
     val locals = res.dsa.get.local
     assert(locals.values.forall(_.glIntervals.size == 1))
 
-
     println(locals.values.filterNot(IntervalDSA.checksStackMaintained).map(_.proc.procName).toSet)
 
     assert(

From 0c8eaab55be777e247286e3e0060823a4d52abc4 Mon Sep 17 00:00:00 2001
From: am <a.michael1@uq.edu.au>
Date: Thu, 18 Sep 2025 13:24:00 +1000
Subject: [PATCH 14/20] run liveness even when main is external

---
 .../analysis/InterLiveVarsAnalysis.scala      | 38 ++++++++++++++++---
 .../ir/transforms/ProcedureParameters.scala   |  9 +----
 2 files changed, 34 insertions(+), 13 deletions(-)

diff --git a/src/main/scala/analysis/InterLiveVarsAnalysis.scala b/src/main/scala/analysis/InterLiveVarsAnalysis.scala
index a6d2b7628..d1c4a8552 100644
--- a/src/main/scala/analysis/InterLiveVarsAnalysis.scala
+++ b/src/main/scala/analysis/InterLiveVarsAnalysis.scala
@@ -17,6 +17,7 @@ import ir.{
   Return,
   Variable
 }
+import util.Logger
 
 import scala.collection.immutable.ListSet
 
@@ -150,13 +151,38 @@ def interLiveVarsAnalysis(
   var procs = ListSet.from(program.procedures)
   var starts = List[Procedure]()
 
-  while (procs.nonEmpty) {
-    val entries = procs.toList.filter(p =>
-      p.incomingCalls().size == 0 && p.entryBlock.isDefined && p.returnBlock.isDefined && p.blocks.nonEmpty
+  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."
     )
-    starts = entries.head :: starts
-    val done = entries.head.reachableFrom
-    procs = procs -- done
+    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]]()
diff --git a/src/main/scala/ir/transforms/ProcedureParameters.scala b/src/main/scala/ir/transforms/ProcedureParameters.scala
index 13346ba8a..a0b582832 100644
--- a/src/main/scala/ir/transforms/ProcedureParameters.scala
+++ b/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)
-  } else {
-    Logger.error(s"Empty live vars $mainNonEmpty $mainHasReturn $mainHasEntry")
-    Map.empty
-  }
+  val liveVars = analysis.interLiveVarsAnalysis(ctx.program)
   transforms.applyRPO(ctx.program)
 
   val liveLab = () =>

From ab3260f90cd671b9243af9c6453fe8d931cd1bd7 Mon Sep 17 00:00:00 2001
From: am <a.michael1@uq.edu.au>
Date: Thu, 18 Sep 2025 18:30:11 +1000
Subject: [PATCH 15/20] check read-uninit in frontend

---
 .../ir/invariant/ReadUninitialised.scala      | 63 ++++++++++++-------
 src/main/scala/ir/transforms/Simp.scala       | 25 ++++----
 .../offlineLifter/OfflineLifter.scala         |  8 ++-
 src/main/scala/util/RunUtils.scala            |  1 +
 src/test/scala/IntervalDSATest.scala          |  6 +-
 5 files changed, 64 insertions(+), 39 deletions(-)

diff --git a/src/main/scala/ir/invariant/ReadUninitialised.scala b/src/main/scala/ir/invariant/ReadUninitialised.scala
index 79577cf93..a301de2b6 100644
--- a/src/main/scala/ir/invariant/ReadUninitialised.scala
+++ b/src/main/scala/ir/invariant/ReadUninitialised.scala
@@ -5,25 +5,21 @@ import util.Logger
 
 import scala.collection.mutable
 
-def readUninitialised(p: Procedure): Boolean = {
-  ir.transforms.reversePostOrder(p)
+class ReadUninitialised() {
 
-  val worklist = mutable.PriorityQueue[Block]()(Ordering.by(_.rpoOrder))
-  worklist.addAll(p.blocks)
-
-  var init = Set[Variable]() ++ p.formalInParam
+  var init = Set[Variable]()
   var readUninit = List[(Command, Set[Variable])]()
 
-  def check(a: Command) = {
+  final def check(a: Command) = {
     val free = freeVarsPos(a).filter(_.isInstanceOf[LocalVar]) -- init
     if (free.size > 0) {
       readUninit = (a, free) :: readUninit
     }
   }
 
-  while (worklist.nonEmpty) {
-    val b = worklist.dequeue()
-    b.statements.foreach {
+  final def readUninitialised(b: Iterable[Statement]): Boolean = {
+    val i = readUninit.size
+    b.foreach {
       case a: Assign => {
         check(a)
         init = init ++ a.assignees
@@ -32,24 +28,47 @@ def readUninitialised(p: Procedure): Boolean = {
         check(o)
       }
     }
+    i != readUninit.size
+  }
+
+  final def readUninitialised(b: Block): Boolean = {
+    val i = readUninit.size
+    readUninitialised(b.statements)
     check(b.jump)
+    i != readUninit.size
   }
 
-  if (readUninit.size > 0) {
-    Logger.error(p.name)
-    val msg = readUninit
-      .map { case (s, vars) =>
-        s"   ${vars.mkString(", ")} uninitialised in statement $s"
-      }
-      .mkString("\n")
-    Logger.error(msg)
-    true
-  } else {
-    false
+  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)
+  val r = p.procedures.map(ReadUninitialised().readUninitialised)
   r.forall(x => !x)
 }
diff --git a/src/main/scala/ir/transforms/Simp.scala b/src/main/scala/ir/transforms/Simp.scala
index 831f7bd8a..58d507726 100644
--- a/src/main/scala/ir/transforms/Simp.scala
+++ b/src/main/scala/ir/transforms/Simp.scala
@@ -1259,11 +1259,16 @@ object OffsetProp {
         case _ => throw Exception("Unexpected expression structure created by find() at some point")
       }
 
-    final def find(
-      v: Variable,
-      ret: BitVecLiteral | Variable | BinaryExpr => BitVecLiteral | Variable | BinaryExpr = x => x,
-      fuel: Int = 5000
-    ): BitVecLiteral | Variable | BinaryExpr = {
+    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 find(v: Variable, fuel: Int = 1000): BitVecLiteral | Variable | BinaryExpr = {
       if (fuel == 0) {
         var chain = List(v)
         for (i <- 0 to 10) {
@@ -1279,15 +1284,13 @@ object OffsetProp {
       }
       st.get(v) match {
         case None => v
-        case Some((None, None)) => ret(v)
-        case Some((None, Some(c))) => ret(c)
-        case Some((Some(v), None)) => ret(find(v, x => x, fuel - 1))
-        case Some((Some(v), Some(c))) => ret(find(v, eval(c), fuel - 1))
+        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)
       }
     }
 
-    def findOff(e: Variable, v: BitVecLiteral): BitVecLiteral | Variable | BinaryExpr = eval(v)(find(e))
-
     def specJoinState(lhs: Variable, rhs: Expr): Option[(Variable, Value)] = {
       rhs match {
         case e @ BinaryExpr(BVADD, l: Variable, r: BitVecLiteral) if (!st.contains(lhs)) =>
diff --git a/src/main/scala/translating/offlineLifter/OfflineLifter.scala b/src/main/scala/translating/offlineLifter/OfflineLifter.scala
index 96964dbbb..6cf1e1e99 100644
--- a/src/main/scala/translating/offlineLifter/OfflineLifter.scala
+++ b/src/main/scala/translating/offlineLifter/OfflineLifter.scala
@@ -116,6 +116,7 @@ class StmtListLifter extends LifterIFace[Int] {
 object Lifter {
 
   def liftBlockBytes(ops: Iterable[Int], initialSp: BigInt): Seq[Seq[Statement]] = {
+
     var sp = initialSp
     ops.toSeq.map { op =>
       val ins = if (op == 0xd503201f.toInt) {
@@ -124,10 +125,15 @@ object Lifter {
         Seq(Assert(FalseLiteral, Some(s"aarch64_system_exceptions_debug_breakpoint (0x$op)")))
       } else {
         try {
+          val checker = ir.invariant.ReadUninitialised()
           val lift = StmtListLifter()
           lift.builder.pcValue = sp
           f_A64_decoder[Expr, Int, BitVecLiteral](lift, BitVecLiteral(BigInt(op), 32), BitVecLiteral(sp, 64))
-          lift.extract.toSeq
+          val stmts = lift.extract.toSeq
+          checker.readUninitialised(stmts)
+          val r = checker.getResult()
+          if (r.isDefined) throw Exception(r.get + "\n" + stmts.mkString("\n"))
+          stmts
         } catch {
           case e => {
             val o = "%x".format(op)
diff --git a/src/main/scala/util/RunUtils.scala b/src/main/scala/util/RunUtils.scala
index 994e905b4..ea9433e87 100644
--- a/src/main/scala/util/RunUtils.scala
+++ b/src/main/scala/util/RunUtils.scala
@@ -54,6 +54,7 @@ object RunUtils {
     Logger.info("[!] Loading Program")
     val q = conf
     var ctx = q.context.getOrElse(IRLoading.load(q.loading))
+    assert(invariant.readUninitialised(ctx.program))
     postLoad(ctx) // allows extracting information from the original loaded program
 
     assert(invariant.checkTypeCorrect(ctx.program))
diff --git a/src/test/scala/IntervalDSATest.scala b/src/test/scala/IntervalDSATest.scala
index 534821f15..5c86c6565 100644
--- a/src/test/scala/IntervalDSATest.scala
+++ b/src/test/scala/IntervalDSATest.scala
@@ -620,11 +620,7 @@ class IntervalDSATest extends AnyFunSuite with test_util.CaptureOutput {
       "direct_request",
       "forward_request",
       "tunnel_add",
-      "magic_auth_detect",
-      "hlist_subcmp_all",
-      "headers_recv",
-      "scanner_hook",
-      "config_open"
+      "magic_auth_detect"
     )
     val globalCollapsed = Set("to_base64", "printmem", "gl_des_ecb_crypt", "from_base64", "des_key_schedule", "scanmem")
     val locals = res.dsa.get.local

From 0fb38b6897b86452ae4a1dfdaae244ed36047745 Mon Sep 17 00:00:00 2001
From: am <a.michael1@uq.edu.au>
Date: Fri, 19 Sep 2025 12:15:45 +1000
Subject: [PATCH 16/20] zero init variables in offline lifter to handle cases
 like 0x8b031041

---
 .../translating/offlineLifter/InstructionBuilder.scala     | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/src/main/scala/translating/offlineLifter/InstructionBuilder.scala b/src/main/scala/translating/offlineLifter/InstructionBuilder.scala
index 540a61f6b..0393fa376 100644
--- a/src/main/scala/translating/offlineLifter/InstructionBuilder.scala
+++ b/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)

From a6c881ffaade24f7d352727d821ce157528d0d01 Mon Sep 17 00:00:00 2001
From: am <a.michael1@uq.edu.au>
Date: Fri, 19 Sep 2025 15:26:24 +1000
Subject: [PATCH 17/20] read-uninit check during simplify

---
 src/main/scala/ir/transforms/SimplifyPipeline.scala | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/main/scala/ir/transforms/SimplifyPipeline.scala b/src/main/scala/ir/transforms/SimplifyPipeline.scala
index 0a23d884b..b22abefa1 100644
--- a/src/main/scala/ir/transforms/SimplifyPipeline.scala
+++ b/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)

From d41cae218ca004f42e148db65f70a36731d50909 Mon Sep 17 00:00:00 2001
From: am <a.michael1@uq.edu.au>
Date: Wed, 24 Sep 2025 12:18:23 +1000
Subject: [PATCH 18/20] fix memory transform prog literal

---
 src/test/scala/MemoryTransformTests.scala | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/test/scala/MemoryTransformTests.scala b/src/test/scala/MemoryTransformTests.scala
index 63c08b2d8..3f40fd7d9 100644
--- a/src/test/scala/MemoryTransformTests.scala
+++ b/src/test/scala/MemoryTransformTests.scala
@@ -214,7 +214,7 @@ class MemoryTransformTests extends AnyFunSuite with CaptureOutput {
           MemoryStore(mem, xAddress, R31, LittleEndian, 64, Some("01")),
           MemoryLoad(R0, mem, xAddress, LittleEndian, 64, Some("02")),
           MemoryStore(mem, zAddress, R0, LittleEndian, 64, Some("03")),
-          goto("k")
+          goto("k", "dummy")
         ),
         block("h", goto("k")),
         block("k", ret),

From 4336eafe55c39d41cd058149639b11b7c32a25dd Mon Sep 17 00:00:00 2001
From: am <a.michael1@uq.edu.au>
Date: Wed, 24 Sep 2025 16:03:23 +1000
Subject: [PATCH 19/20] restore

---
 src/test/scala/IntervalDSATest.scala | 2 --
 1 file changed, 2 deletions(-)

diff --git a/src/test/scala/IntervalDSATest.scala b/src/test/scala/IntervalDSATest.scala
index 5c86c6565..2d723037b 100644
--- a/src/test/scala/IntervalDSATest.scala
+++ b/src/test/scala/IntervalDSATest.scala
@@ -626,8 +626,6 @@ class IntervalDSATest extends AnyFunSuite with test_util.CaptureOutput {
     val locals = res.dsa.get.local
     assert(locals.values.forall(_.glIntervals.size == 1))
 
-    println(locals.values.filterNot(IntervalDSA.checksStackMaintained).map(_.proc.procName).toSet)
-
     assert(
       locals.values.filterNot(g => stackCollapsed.contains(g.proc.procName)).forall(IntervalDSA.checksStackMaintained)
     )

From 90ebef753708851b8dc224d3acb7f85b1d2772e2 Mon Sep 17 00:00:00 2001
From: rina <k@rina.fyi>
Date: Mon, 5 Jan 2026 14:06:50 +1000
Subject: [PATCH 20/20] fix merge & fmt

---
 src/main/scala/ir/transforms/Simp.scala | 5 +----
 1 file changed, 1 insertion(+), 4 deletions(-)

diff --git a/src/main/scala/ir/transforms/Simp.scala b/src/main/scala/ir/transforms/Simp.scala
index 8f82531b6..8b28781e9 100644
--- a/src/main/scala/ir/transforms/Simp.scala
+++ b/src/main/scala/ir/transforms/Simp.scala
@@ -1258,7 +1258,6 @@ object OffsetProp {
         case _ => throw Exception("Unexpected expression structure created by find() at some point")
       }
 
-
     def find(v: Variable, fuel: Int = 1000): BitVecLiteral | Variable | BinaryExpr = {
       if (fuel == 0) {
         var chain = List(v)
@@ -1278,12 +1277,10 @@ object OffsetProp {
         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))) => 
-        (v, c, fuel - 1)
+        case Some((Some(v), Some(c))) => findOff(v, c, fuel - 1)
       }
     }
 
-
     def specJoinState(lhs: Variable, rhs: Expr): Option[(Variable, Value)] = {
       rhs match {
         case e @ BinaryExpr(BVADD, l: Variable, r: BitVecLiteral) if (!st.contains(lhs)) =>