basic exit call identification

in the main procedure, add return statements after all
calls functions which exit on all paths, this
gives the ide solver a return point to attach
summaries to

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

@@ -7,6 +7,7 @@ import collection.immutable.SortedMap
 import specification.Specification
 import analysis.{TwoElement, TwoElementTop, TwoElementBottom}
 import ir.CallGraph
+import util.Logger
 
 case class FunSig(inArgs: List[Register], outArgs: List[Register])
 
@@ -30,14 +31,18 @@ def fnsigToBinding(f: FunSig) = (
 
 def liftProcedureCallAbstraction(ctx: util.IRContext): util.IRContext = {
 
-  val liveVars =
-    if (
-      ctx.program.mainProcedure.blocks.nonEmpty && ctx.program.mainProcedure.returnBlock.isDefined && ctx.program.mainProcedure.entryBlock.isDefined
-    ) {
-      analysis.InterLiveVarsAnalysis(ctx.program).analyze()
-    } else {
-      Map.empty
-    }
+  val mainNonEmpty = ctx.program.mainProcedure.blocks.nonEmpty
+  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
+  }
+
+  transforms.applyRPO(ctx.program)
 
   val params = inOutParams(ctx.program, liveVars)
 
@@ -337,8 +342,8 @@ class SetActualParams(
       //   }
       // }
       case d: DirectCall => {
-        d.actualParams = SortedMap.from(d.target.inParamDefaultBinding)
-        d.outParams = SortedMap.from(d.target.outParamDefaultBinding)
+        d.actualParams = SortedMap.from(inBinding(d.target))
+        d.outParams = SortedMap.from(outBinding(d.target))
       }
       case _ => ()
     }

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

@@ -878,7 +878,65 @@ class Substitute(val res: Variable => Option[Expr], val recurse: Boolean = true,
       None
     }
   }
+}
+
+enum PathExit:
+  case Maybe
+  case Return
+  case NoReturn
+  case Bot
+
+class ProcExitsDomain(is_nonreturning: String => Boolean) extends AbstractDomain[PathExit] {
+  /* backwards analysis to identify non-returning function */
+
+  override def transfer(s: PathExit, b: Command) = {
+    b match {
+      case d: DirectCall if is_nonreturning(d.target.name) => PathExit.NoReturn
+      case r: Return                                       => PathExit.Maybe
+      case _                                               => s
+    }
+  }
+  override def top = PathExit.Maybe
+  def bot = PathExit.Bot
+  def join(l: PathExit, r: PathExit, pos: Block) = (l, r) match {
+    case (PathExit.Return, PathExit.Return)     => PathExit.Return
+    case (PathExit.NoReturn, PathExit.NoReturn) => PathExit.NoReturn
+    case (PathExit.Return, PathExit.NoReturn)   => PathExit.Maybe
+    case (PathExit.NoReturn, PathExit.Return)   => PathExit.Maybe
+    case (PathExit.Maybe, x)                    => PathExit.Maybe
+    case (x, PathExit.Maybe)                    => PathExit.Maybe
+    case (PathExit.Bot, x)                      => x
+    case (x, PathExit.Bot)                      => x
+  }
+}
+
+case class ProcReturnInfo(returning: Set[Procedure], nonreturning: Set[Procedure])
 
+def findNonReturningFunctionsSaturating(p: Program) = {
+  var returning = Set[String]()
+  var old_nonreturning = Set[String]()
+
+  val exit = p.procedures.find(p => p.procName == "exit").map(_.name)
+  var nonreturning = exit.toSet ++ Set("exit")
+
+  while (nonreturning != old_nonreturning) {
+    old_nonreturning = nonreturning
+
+    for (p <- p.procedures.filterNot(p => nonreturning.contains(p.name) || returning.contains(p.name))) {
+      val solver = worklistSolver(ProcExitsDomain(s => nonreturning.contains(s)))
+      val (beforeBlocks, afterBlocks) = solver.solveProc(p, true)
+      p.entryBlock.flatMap(beforeBlocks.get) match {
+        case Some(PathExit.NoReturn) => nonreturning = nonreturning + p.name
+        case Some(PathExit.Return)   => returning = returning + p.name
+        case _                       => ()
+      }
+    }
+  }
+
+  ProcReturnInfo(
+    returning.flatMap(pn => p.procedures.find(_.name == pn).toSet),
+    nonreturning.flatMap(pn => p.procedures.find(_.name == pn).toSet)
+  )
 }
 
 class Simplify(val res: Variable => Option[Expr], val initialBlock: Block = null) extends CILVisitor {

src/main/scala/translating/IRToBoogie.scala

@@ -757,7 +757,6 @@ class IRToBoogie(
 
         val inv = BinaryBExpr(BoolOR, Rc, Gf)
         val conseq = BinaryBExpr(BoolIMPLIES, Rc, Rf)
-
         val procInv = BProcedure(
           targetName + "$InlineInv",
           List(),

src/main/scala/util/RunUtils.scala

@@ -205,6 +205,13 @@ object IRTransform {
       }
     }
 
+    transforms.applyRPO(ctx.program)
+    val nonReturning = transforms.findNonReturningFunctionsSaturating(ctx.program)
+    ctx.program.mainProcedure.foreach(s => s match {
+      case d : DirectCall if nonReturning.nonreturning.contains(d.target) => d.parent.replaceJump(Return())
+      case _ => ()
+    })
+
     cilvisitor.visit_prog(transforms.ReplaceReturns(), ctx.program)
     transforms.addReturnBlocks(ctx.program)
     cilvisitor.visit_prog(transforms.ConvertSingleReturn(), ctx.program)
@@ -550,7 +557,6 @@ object RunUtils {
 
     DebugDumpIRLogger.writeToFile(File("blockgraph-before-dsa.dot"), dotBlockGraph(ctx.program.mainProcedure))
 
-    Logger.info(s"RPO ${timer.checkPoint("RPO")} ms ")
     Logger.info("[!] Simplify :: DynamicSingleAssignment")
     DebugDumpIRLogger.writeToFile(File("il-before-dsa.il"), serialiseIL(ctx.program))
 
@@ -587,7 +593,7 @@ object RunUtils {
     // assert(ctx.program.procedures.forall(transforms.rdDSAProperty))
 
     assert(invariant.blockUniqueLabels(ctx.program))
-    Logger.info(s"CopyProp ${timer.checkPoint("CopyProp")} ms ")
+    Logger.info(s"CopyProp ${timer.checkPoint("Simplify")} ms ")
     DebugDumpIRLogger.writeToFile(File("il-after-copyprop.il"), pp_prog(ctx.program))