diff --git a/src/main/scala/Main.scala b/src/main/scala/Main.scala index 312476029..3fb3f0139 100644 --- a/src/main/scala/Main.scala +++ b/src/main/scala/Main.scala @@ -8,7 +8,7 @@ import util.RunUtils import scala.collection.mutable.{ArrayBuffer, Set} import scala.collection.{immutable, mutable} import scala.language.postfixOps -import scala.sys.process._ +import scala.sys.process.* import util.* import mainargs.{main, arg, ParserForClass, Flag} @@ -35,7 +35,11 @@ object Main { @arg(name = "dump-il", doc = "Dump the Intermediate Language to text.") dumpIL: Option[String], @arg(name = "help", short = 'h', doc = "Show this help message.") - help: Flag + help: Flag, + @arg(name = "analysis-results", doc = "Log analysis results in files at specified path.") + analysisResults: Option[String], + @arg(name = "analysis-results-dot", doc = "Log analysis results in .dot form at specified path.") + analysisResultsDot: Option[String] ) def main(args: Array[String]): Unit = { @@ -61,12 +65,12 @@ object Main { val q = BASILConfig( loading = ILLoadingConfig(conf.adtFileName, conf.relfFileName, conf.specFileName, conf.dumpIL), runInterpret = conf.interpret.value, - staticAnalysis = if (conf.analyse.value) then Some(StaticAnalysisConfig(conf.dumpIL)) else None, - boogieTranslation = BoogieGeneratorConfig(if (conf.lambdaStores.value) then BoogieMemoryAccessMode.LambdaStoreSelect else BoogieMemoryAccessMode.SuccessiveStoreSelect), - outputPrefix = conf.outFileName + staticAnalysis = if conf.analyse.value then Some(StaticAnalysisConfig(conf.dumpIL, conf.analysisResults, conf.analysisResultsDot)) else None, + boogieTranslation = BoogieGeneratorConfig(if conf.lambdaStores.value then BoogieMemoryAccessMode.LambdaStoreSelect else BoogieMemoryAccessMode.SuccessiveStoreSelect), + outputPrefix = conf.outFileName, ) - RunUtils.run(q); + RunUtils.run(q) } } diff --git a/src/main/scala/cfg_visualiser/Output.scala b/src/main/scala/cfg_visualiser/Output.scala index 23d5c2d0d..e75b3ef29 100644 --- a/src/main/scala/cfg_visualiser/Output.scala +++ b/src/main/scala/cfg_visualiser/Output.scala @@ -7,71 +7,6 @@ import analysis._ */ object Output { - /** Generate an output to a file. - * @param file - * the output file - * @param kind - * output kind (determines the file name suffix) - * @param outFolder - * the output directory - */ - def output(kind: OutputKind, content: String, fileName: String): Unit = { - val extension = kind match { - case OtherOutput(OutputKindE.`cfg`) => "_cfg.dot" - case OtherOutput(OutputKindE.`icfg`) => "_icfg.dot" -// case DataFlowOutput(k) => -// s"_$k.dot" - case _ => ??? - } - val outFile = new File(s"$fileName.dot") - val pw = new PrintWriter(outFile, "UTF-8") - pw.write(content) - pw.close() - } - - /** Escapes special characters in the given string. Special characters are all Unicode chars except 0x20-0x7e but - * including \, ", {, and }. - */ - def escape(s: String): String = { - if (s == null) - return null - val b = new StringBuilder() - for (i <- 0 until s.length) { - val c = s.charAt(i) - c match { - case '"' => - b.append("\\\"") - case '\\' => - b.append("\\\\") - case '\b' => - b.append("\\b") - case '\t' => - b.append("\\t") - case '\n' => - b.append("\\n") - case '\r' => - b.append("\\r") - case '\f' => - b.append("\\f") - case '<' => - b.append("\\<") - case '>' => - b.append("\\>") - case '{' => - b.append("\\{") - case '}' => - b.append("\\}") - case _ => - if (c >= 0x20 && c <= 0x7e) - b.append(c) - else { - b.append("\\%04X".format(c.toInt)) - } - } - } - b.toString() - } - /** Helper function for producing string output for a control-flow graph node after an analysis. * @param res * map from control-flow graph nodes to strings, as produced by the analysis @@ -99,18 +34,4 @@ object Output { case callRet: CfgCallReturnNode => s"callreturn_$uniqueId" case _ => ??? } -} - -/** Different kinds of output (determine output file names). - */ -object OutputKindE extends Enumeration { - val cfg, icfg = Value -} - -sealed trait OutputKind - -/** Other output kinds (for other processing phases than the actual analysis). - */ -case class OtherOutput(kind: OutputKindE.Value) extends OutputKind { - override def toString: String = kind.toString -} +} \ No newline at end of file diff --git a/src/main/scala/translating/SpecificationLoader.scala b/src/main/scala/translating/SpecificationLoader.scala index 9fe6d26cc..968bad056 100644 --- a/src/main/scala/translating/SpecificationLoader.scala +++ b/src/main/scala/translating/SpecificationLoader.scala @@ -361,7 +361,7 @@ case class SpecificationLoader(symbols: Set[SpecGlobal], program: Program) { val params: Map[String, Parameter] = irProc match { case None => Map() case Some(p) => - p.in.map { (p: Parameter) => p.name -> p }.toMap ++ p.out.map { (p: Parameter) => p.name -> p }.toMap + p.in.map(p => p.name -> p).toMap ++ p.out.map(p => p.name -> p).toMap } val requires = ctx.requires.asScala.collect { case r: ParsedRequiresContext => diff --git a/src/main/scala/util/BASILConfig.scala b/src/main/scala/util/BASILConfig.scala index 7b80888a1..ac0e3d5f7 100644 --- a/src/main/scala/util/BASILConfig.scala +++ b/src/main/scala/util/BASILConfig.scala @@ -2,15 +2,14 @@ package util case class ILLoadingConfig(adtFile: String, relfFile: String, specFile: Option[String], dumpIL: Option[String]) case class BoogieGeneratorConfig(memoryFunctionType: BoogieMemoryAccessMode = BoogieMemoryAccessMode.SuccessiveStoreSelect) -case class StaticAnalysisConfig(dumpILToPath: Option[String] = None) +case class StaticAnalysisConfig(dumpILToPath: Option[String] = None, analysisResultsPath: Option[String] = None, analysisDotPath: Option[String] = None) enum BoogieMemoryAccessMode: case SuccessiveStoreSelect, LambdaStoreSelect -case class BASILConfig( - loading: ILLoadingConfig, - runInterpret: Boolean = false, - staticAnalysis: Option[StaticAnalysisConfig] = None, - boogieTranslation: BoogieGeneratorConfig = BoogieGeneratorConfig(), - outputPrefix: String - ) +case class BASILConfig(loading: ILLoadingConfig, + runInterpret: Boolean = false, + staticAnalysis: Option[StaticAnalysisConfig] = None, + boogieTranslation: BoogieGeneratorConfig = BoogieGeneratorConfig(), + outputPrefix: String, + ) diff --git a/src/main/scala/util/RunUtils.scala b/src/main/scala/util/RunUtils.scala index c2c6744c3..6d66df638 100644 --- a/src/main/scala/util/RunUtils.scala +++ b/src/main/scala/util/RunUtils.scala @@ -8,7 +8,7 @@ import java.io.{BufferedWriter, FileWriter, IOException} import scala.jdk.CollectionConverters.* import analysis.solvers.* import analysis.* -import cfg_visualiser.{OtherOutput, Output, OutputKindE} +import cfg_visualiser.Output import bap.* import ir.* import boogie.* @@ -24,8 +24,6 @@ import scala.collection.mutable object RunUtils { var memoryRegionAnalysisResults: Map[CfgNode, Set[MemoryRegion]] = Map() - var iterations = 0 - // ids reserved by boogie val reserved: Set[String] = Set("free") @@ -93,16 +91,16 @@ object RunUtils { IRProgram = renamer.visitProgram(IRProgram) q.loading.dumpIL match { - case Some(s) => writeToFile(serialiseIL(IRProgram), s + "-before-analysis.il") + case Some(s: String) => writeToFile(serialiseIL(IRProgram), s"$s-before-analysis.il") case _ => } q.staticAnalysis match { case Some(analysisConfig) => - IRProgram = analyse(IRProgram, externalFunctions, globals, globalOffsets) + IRProgram = analyse(IRProgram, externalFunctions, globals, globalOffsets, analysisConfig, 1) analysisConfig.dumpILToPath match { - case Some(s) => writeToFile(serialiseIL(IRProgram), s + "-after-analysis.il") + case Some(s: String) => writeToFile(serialiseIL(IRProgram), s"$s-after-analysis.il") case _ => } case None => @@ -131,15 +129,16 @@ object RunUtils { IRProgram: Program, externalFunctions: Set[ExternalFunction], globals: Set[SpecGlobal], - globalOffsets: Map[BigInt, BigInt] + globalOffsets: Map[BigInt, BigInt], + config: StaticAnalysisConfig, + iteration: Int ): Program = { - iterations += 1 val subroutines = IRProgram.procedures .filter(p => p.address.isDefined) - .map { (p: Procedure) => BigInt(p.address.get) -> p.name } + .map(p => BigInt(p.address.get) -> p.name) .toMap - val globalAddresses = globals.map { (s: SpecGlobal) => s.address -> s.name }.toMap - val externalAddresses = externalFunctions.map { (e: ExternalFunction) => e.offset -> e.name }.toMap + val globalAddresses = globals.map(s => s.address -> s.name).toMap + val externalAddresses = externalFunctions.map(e => e.offset -> e.name).toMap Logger.info("Globals:") Logger.info(globalAddresses) Logger.info("Global Offsets: ") @@ -156,25 +155,29 @@ object RunUtils { Logger.info("[!] Running Constant Propagation") val constPropSolver = ConstantPropagationAnalysis.WorklistSolver(cfg) val constPropResult: Map[CfgNode, Map[Variable, ConstantPropagationLattice.Element]] = constPropSolver.analyze(true) - /* - Output.output( - OtherOutput(OutputKindE.cfg), - cfg.toDot(Output.labeler(constPropResult, constPropSolver.stateAfterNode), Output.dotIder), - "cpa" - ) - */ - writeToFile(printAnalysisResults(cfg, constPropResult), "cpa") + + config.analysisDotPath match { + case Some(s) => writeToFile(cfg.toDot(Output.labeler(constPropResult, constPropSolver.stateAfterNode), Output.dotIder), s"${s}_constprop$iteration.dot") + case None => + } + config.analysisResultsPath match { + case Some(s) => writeToFile(printAnalysisResults(cfg, constPropResult, iteration), s"${s}_constprop$iteration.txt") + case None => + } Logger.info("[!] Running MRA") val mraSolver = MemoryRegionAnalysis.WorklistSolver(cfg, globalAddresses, globalOffsets, mergedSubroutines, constPropResult) val mraResult: Map[CfgNode, Set[MemoryRegion]] = mraSolver.analyze(true) memoryRegionAnalysisResults = mraResult - /* Output.output( - OtherOutput(OutputKindE.cfg), - cfg.toDot(Output.labeler(mraResult, mraSolver.stateAfterNode), Output.dotIder), - "mra" - )*/ - writeToFile(printAnalysisResults(cfg, mraResult), "mra") + + config.analysisDotPath match { + case Some(s) => writeToFile(cfg.toDot(Output.labeler(mraResult, mraSolver.stateAfterNode), Output.dotIder), s"${s}_mra$iteration.dot") + case None => + } + config.analysisResultsPath match { + case Some(s) => writeToFile(printAnalysisResults(cfg, mraResult, iteration), s"${s}_mra$iteration.txt") + case None => + } Logger.info("[!] Running MMM") val mmm = MemoryModelMap() @@ -184,35 +187,39 @@ object RunUtils { val vsaSolver = ValueSetAnalysis.WorklistSolver(cfg, globalAddresses, externalAddresses, globalOffsets, subroutines, mmm, constPropResult) val vsaResult: Map[CfgNode, Map[Variable | MemoryRegion, Set[Value]]] = vsaSolver.analyze(false) - /* - Output.output( - OtherOutput(OutputKindE.cfg), - cfg.toDot(Output.labeler(vsaResult, vsaSolver.stateAfterNode), Output.dotIder), - "vsa" - ) - */ - writeToFile(printAnalysisResults(cfg, vsaResult), "vsa") + + config.analysisDotPath match { + case Some(s) => writeToFile(cfg.toDot(Output.labeler(vsaResult, vsaSolver.stateAfterNode), Output.dotIder), s"${s}_vsa$iteration.dot") + case None => + } + config.analysisResultsPath match { + case Some(s) => writeToFile(printAnalysisResults(cfg, vsaResult, iteration), s"${s}_vsa$iteration.txt") + case None => + } Logger.info("[!] Resolving CFG") val (newIR, modified): (Program, Boolean) = resolveCFG(cfg, vsaResult, IRProgram) - /* if (modified) { - Logger.info(s"[!] Analysing again (iter $iterations)") - return analyse(newIR, externalFunctions, globals, globalOffsets) + Logger.info(s"[!] Analysing again (iter $iteration)") + return analyse(newIR, externalFunctions, globals, globalOffsets, config, iteration + 1) } - */ - val newCFG = ProgramCfgFactory().fromIR(newIR) - Output.output(OtherOutput(OutputKindE.cfg), newCFG.toDot(x => x.toString, Output.dotIder), "resolvedCFG") - Logger.info(s"[!] Finished indirect call resolution after $iterations iterations") + config.analysisDotPath match { + case Some(s) => + val newCFG = ProgramCfgFactory().fromIR(newIR) + writeToFile(newCFG.toDot(x => x.toString, Output.dotIder), s"${s}_resolvedCFG.dot") + case None => + } + + Logger.info(s"[!] Finished indirect call resolution after $iteration iterations") newIR } - def printAnalysisResults(cfg: ProgramCfg, result: Map[CfgNode, _]): String = { + def printAnalysisResults(cfg: ProgramCfg, result: Map[CfgNode, _], iteration: Int): String = { val functionEntries = cfg.nodes.collect { case n: CfgFunctionEntryNode => n }.toSeq.sortBy(_.data.name) val s = StringBuilder() - + s.append(System.lineSeparator()) for (f <- functionEntries) { val stack: mutable.Stack[CfgNode] = mutable.Stack() val visited: mutable.Set[CfgNode] = mutable.Set() @@ -406,8 +413,8 @@ object RunUtils { (IRProgram, modified) } - def writeToFile(content: String, name: String): Unit = { - val outFile = File(name) + def writeToFile(content: String, fileName: String): Unit = { + val outFile = File(fileName) val pw = PrintWriter(outFile, "UTF-8") pw.write(content) pw.close()