diff --git a/src/main/scala/Main.scala b/src/main/scala/Main.scala index b4ec4bc96..498c6eacb 100644 --- a/src/main/scala/Main.scala +++ b/src/main/scala/Main.scala @@ -47,7 +47,9 @@ object Main { @arg(name = "analysis-results-dot", doc = "Log analysis results in .dot form at specified path.") analysisResultsDot: Option[String], @arg(name = "threads", short = 't', doc = "Separates threads into multiple .bpl files with given output filename as prefix (requires --analyse flag)") - threadSplit: Flag + threadSplit: Flag, + @arg(name = "summarise-procedures", doc = "Generates summaries of procedures which are used in pre/post-conditions (requires --analyse flag)") + summariseProcedures: Flag ) def main(args: Array[String]): Unit = { @@ -80,7 +82,7 @@ object Main { val q = BASILConfig( loading = ILLoadingConfig(conf.inputFileName, conf.relfFileName, conf.specFileName, conf.dumpIL, conf.mainProcedureName, conf.procedureDepth), runInterpret = conf.interpret.value, - staticAnalysis = if conf.analyse.value then Some(StaticAnalysisConfig(conf.dumpIL, conf.analysisResults, conf.analysisResultsDot, conf.threadSplit.value)) else None, + staticAnalysis = if conf.analyse.value then Some(StaticAnalysisConfig(conf.dumpIL, conf.analysisResults, conf.analysisResultsDot, conf.threadSplit.value, conf.summariseProcedures.value)) else None, boogieTranslation = BoogieGeneratorConfig(if conf.lambdaStores.value then BoogieMemoryAccessMode.LambdaStoreSelect else BoogieMemoryAccessMode.SuccessiveStoreSelect, true, rely, conf.threadSplit.value), outputPrefix = conf.outFileName, diff --git a/src/main/scala/analysis/SummaryGenerator.scala b/src/main/scala/analysis/SummaryGenerator.scala index 97c7e4a8e..9d633f3a5 100644 --- a/src/main/scala/analysis/SummaryGenerator.scala +++ b/src/main/scala/analysis/SummaryGenerator.scala @@ -16,7 +16,7 @@ private trait RNATaintableAnalysis( globals: Map[BigInt, String], constProp: Map[CFGPosition, Map[Variable, FlatElement[BitVecLiteral]]], ) { - val lattice: MapLattice[ir.CFGPosition, Set[Taintable], PowersetLattice[Taintable]] = MapLattice(PowersetLattice()) + val lattice: MapLattice[CFGPosition, Set[Taintable], PowersetLattice[Taintable]] = MapLattice(PowersetLattice()) val domain: Set[CFGPosition] = Set.empty ++ program @@ -83,10 +83,11 @@ class SummaryGenerator( constProp: Map[CFGPosition, Map[Variable, FlatElement[BitVecLiteral]]], varDepsSummaries: Map[Procedure, Map[Taintable, Set[Taintable]]], ) { - val rnaResults = RNATaintableSolver(program, globals, constProp).analyze() + private val rnaResults = RNATaintableSolver(program, globals, constProp).analyze() - // TODO should the stack/link/frame pointers propagate taint? - val variables: Set[analysis.Taintable] = 0.to(28).map { n => + // registers R19 to R29 and R31 must be preserved by a procedure call, so we only need summaries for R0-R18 and R30 + // TODO support R30? the analysis currently ignores it? + val variables: Set[Taintable] = 0.to(18).map { n => Register(s"R$n", 64) }.toSet ++ specGlobals.map { g => analysis.GlobalVariable(dsl.mem, BitVecLiteral(g.address, 64), g.size, g.name) @@ -137,6 +138,7 @@ class SummaryGenerator( } } + // TODO further explanation of this would help // Use rnaResults to find stack function arguments val tainters = relevantVars.map { v => (v, Set()) @@ -144,14 +146,13 @@ class SummaryGenerator( relevantVars.contains(variable) } - tainters.toList - .flatMap { (variable, taints) => - { + tainters.toList.flatMap { + (variable, taints) => { // If our variable was tainted by memory that we know nothing about, it is sound to assume that we // know nothing about its gamma in the post state. if taints.contains(UnknownMemory()) then None - else toGamma(variable).flatMap - { varGamma => { + else toGamma(variable).flatMap { + varGamma => { if taints.isEmpty then { // If the variable is tainted by nothing, it must have been set to some constant value, meaning // its gamma is low. Note that if a variable was unchanged, it would be tainted by itself. @@ -170,7 +171,7 @@ class SummaryGenerator( } } - if equations.size > 0 then { + if equations.nonEmpty then { Some(equations.foldLeft(varGamma) { (expr, eq) => BinaryBExpr(BoolOR, expr, eq) }) diff --git a/src/main/scala/analysis/solvers/FixPointSolver.scala b/src/main/scala/analysis/solvers/FixPointSolver.scala index 710189a41..bae5f8b9d 100644 --- a/src/main/scala/analysis/solvers/FixPointSolver.scala +++ b/src/main/scala/analysis/solvers/FixPointSolver.scala @@ -249,9 +249,7 @@ trait PushDownWorklistFixpointSolver[N, T, L <: Lattice[T]] extends MapLatticeSo def process(n: N): Unit = val xn = x(n) val y = transfer(n, xn) - if (y != xn) { - for succ <- outdep(n) do propagate(y, succ) - } + for succ <- outdep(n) do propagate(y, succ) /** Worklist-based fixpoint solver. diff --git a/src/main/scala/analysis/solvers/IDESolver.scala b/src/main/scala/analysis/solvers/IDESolver.scala index d5862298e..ef1d34b54 100644 --- a/src/main/scala/analysis/solvers/IDESolver.scala +++ b/src/main/scala/analysis/solvers/IDESolver.scala @@ -164,11 +164,13 @@ abstract class IDESolver[E <: Procedure | Command, EE <: Procedure | Command, C edgesCallToEntry(call, entry)(d).foreach { (d2, e) => propagate(e(xnd), (entry, d2)) - summaries.get(IRWalk.procedure(entry)).foreach(_(d2).foreach { (d3, e2) => - edgesExitToAfterCall(entryToExit(entry), ret)(d3).foreach { (d4, e3) => - propagate(e3(e2(e(xnd))), (ret, d4)) + summaries.get(IRWalk.procedure(entry)).foreach { + _(d2).foreach { (d3, e2) => + edgesExitToAfterCall(entryToExit(entry), ret)(d3).foreach { (d4, e3) => + propagate(e3(e2(e(xnd))), (ret, d4)) + } } - }) + } } edgesCallToAfterCall(call, ret)(d).foreach { (d2, e) => diff --git a/src/main/scala/util/BASILConfig.scala b/src/main/scala/util/BASILConfig.scala index 41b7b17d6..667a25ba9 100644 --- a/src/main/scala/util/BASILConfig.scala +++ b/src/main/scala/util/BASILConfig.scala @@ -6,7 +6,12 @@ enum ProcRelyVersion: case class BoogieGeneratorConfig(memoryFunctionType: BoogieMemoryAccessMode = BoogieMemoryAccessMode.SuccessiveStoreSelect, coalesceConstantMemory: Boolean = true, procedureRely: Option[ProcRelyVersion] = None, threadSplit: Boolean = false) case class ILLoadingConfig(inputFile: String, relfFile: String, specFile: Option[String] = None, dumpIL: Option[String] = None, mainProcedureName: String = "main", procedureTrimDepth: Int = Int.MaxValue) -case class StaticAnalysisConfig(dumpILToPath: Option[String] = None, analysisResultsPath: Option[String] = None, analysisDotPath: Option[String] = None, threadSplit: Boolean = false) +case class StaticAnalysisConfig(dumpILToPath: Option[String] = None, + analysisResultsPath: Option[String] = None, + analysisDotPath: Option[String] = None, + threadSplit: Boolean = false, + summariseProcedures: Boolean = false + ) enum BoogieMemoryAccessMode: case SuccessiveStoreSelect, LambdaStoreSelect diff --git a/src/main/scala/util/RunUtils.scala b/src/main/scala/util/RunUtils.scala index b5172b84d..fc69c8df1 100644 --- a/src/main/scala/util/RunUtils.scala +++ b/src/main/scala/util/RunUtils.scala @@ -551,7 +551,7 @@ object IRTransform { } } - def generateFunctionSummaries( + def generateProcedureSummaries( ctx: IRContext, IRProgram: Program, constPropResult: Map[CFGPosition, Map[Variable, FlatElement[BitVecLiteral]]], @@ -733,19 +733,6 @@ object StaticAnalysis { //val paramResults = ParamAnalysis(IRProgram).analyze() val paramResults = Map[Procedure, Set[Variable]]() - /* - Logger.info("[!] Running Taint Analysis") - val taintResults = TaintAnalysis(IRProgram, specGlobalAddresses, constPropResult, - IRProgram.procedures.foldLeft(Map[CFGPosition, Set[analysis.Taintable]]()) { - (m, p) => m + (p -> Set(analysis.UnknownMemory())) - } - ).analyze() - - config.analysisResultsPath.foreach(s => - writeToFile(printAnalysisResults(IRProgram, taintResults), s"${s}_taint$iteration.txt") - ) - */ - StaticAnalysisContext( cfg = cfg, constPropResult = constPropResult, @@ -982,7 +969,9 @@ object RunUtils { ctx.program ) Logger.info("[!] Generating Function Summaries") - modified = modified | IRTransform.generateFunctionSummaries(ctx, ctx.program, result.constPropResult, result.varDepsSummaries) + if (config.summariseProcedures) { + IRTransform.generateFunctionSummaries(ctx, ctx.program, result.constPropResult, result.varDepsSummaries) + } if (modified) { iteration += 1 Logger.info(s"[!] Analysing again (iter $iteration)")