From 827946c84dfae96ca106dacdd61b504cec58e1d5 Mon Sep 17 00:00:00 2001 From: Alistair Michael Date: Tue, 14 Jan 2025 16:40:50 +1000 Subject: [PATCH] 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 --- .../ir/transforms/ProcedureParameters.scala | 25 ++++---- src/main/scala/ir/transforms/Simp.scala | 58 +++++++++++++++++++ src/main/scala/translating/IRToBoogie.scala | 1 - src/main/scala/util/RunUtils.scala | 10 +++- 4 files changed, 81 insertions(+), 13 deletions(-) diff --git a/src/main/scala/ir/transforms/ProcedureParameters.scala b/src/main/scala/ir/transforms/ProcedureParameters.scala index bb76765ed..a6e4db2e2 100644 --- a/src/main/scala/ir/transforms/ProcedureParameters.scala +++ b/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 _ => () } diff --git a/src/main/scala/ir/transforms/Simp.scala b/src/main/scala/ir/transforms/Simp.scala index 62deadab7..4daa3f8e3 100644 --- a/src/main/scala/ir/transforms/Simp.scala +++ b/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 { diff --git a/src/main/scala/translating/IRToBoogie.scala b/src/main/scala/translating/IRToBoogie.scala index 45bd28f06..e0b2215e9 100644 --- a/src/main/scala/translating/IRToBoogie.scala +++ b/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(), diff --git a/src/main/scala/util/RunUtils.scala b/src/main/scala/util/RunUtils.scala index 7f3a1b950..c49d3084f 100644 --- a/src/main/scala/util/RunUtils.scala +++ b/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))