diff --git a/src/main/scala/analysis/VariableDependencyAnalysis.scala b/src/main/scala/analysis/VariableDependencyAnalysis.scala index 1b8258ad5..ed1ed1eaf 100644 --- a/src/main/scala/analysis/VariableDependencyAnalysis.scala +++ b/src/main/scala/analysis/VariableDependencyAnalysis.scala @@ -118,7 +118,7 @@ class VariableDependencyAnalysis( var varDepsSummariesTransposed = Map[Procedure, Map[Taintable, Set[Taintable]]]() scc.flatten.filter(_.blocks.nonEmpty).foreach { procedure => { - Logger.info("Generating variable dependencies for " + procedure) + Logger.debug("Generating variable dependencies for " + procedure) val varDepResults = ProcVariableDependencyAnalysis(program, varDepVariables, globals, constProp, varDepsSummariesTransposed, procedure).analyze() val varDepMap = varDepResults.getOrElse(IRWalk.lastInProc(procedure).getOrElse(procedure), Map()) varDepsSummaries += procedure -> varDepMap diff --git a/src/main/scala/ir/transforms/IndirectCallResolution.scala b/src/main/scala/ir/transforms/IndirectCallResolution.scala index 4345dcaa1..8f1ae8e3b 100644 --- a/src/main/scala/ir/transforms/IndirectCallResolution.scala +++ b/src/main/scala/ir/transforms/IndirectCallResolution.scala @@ -104,7 +104,7 @@ def resolveIndirectCallsUsingPointsTo( targetNames.map(name => IRProgram.procedures.find(_.name == name).getOrElse(addFakeProcedure(name))) if (targets.size > 1) { - Logger.info(s"Resolved indirect call $indirectCall") + Logger.debug(s"Resolved indirect call $indirectCall") } if (targets.size == 1) { diff --git a/src/main/scala/util/PerformanceTimer.scala b/src/main/scala/util/PerformanceTimer.scala index a0be917f3..a79b1d3b7 100644 --- a/src/main/scala/util/PerformanceTimer.scala +++ b/src/main/scala/util/PerformanceTimer.scala @@ -12,7 +12,7 @@ case class PerformanceTimer(timerName: String = "") { val delta = elapsed() lastCheckpoint = System.currentTimeMillis() checkpoints.put(name, delta) - Logger.info(s"PerformanceTimer $timerName [$name]: ${delta}ms") + Logger.debug(s"PerformanceTimer $timerName [$name]: ${delta}ms") delta } private def elapsed() : Long = { diff --git a/src/main/scala/util/RunUtils.scala b/src/main/scala/util/RunUtils.scala index 0cfc93677..0d08a5f4e 100644 --- a/src/main/scala/util/RunUtils.scala +++ b/src/main/scala/util/RunUtils.scala @@ -185,7 +185,7 @@ object IRTransform { /** Initial cleanup before analysis. */ def doCleanup(ctx: IRContext): IRContext = { - Logger.info("[!] Removing external function calls") + Logger.debug("[!] Removing external function calls") // Remove external function references (e.g. @printf) val externalNames = ctx.externalFunctions.map(e => e.name) val externalNamesLibRemoved = mutable.Set[String]() @@ -215,10 +215,10 @@ object IRTransform { def prepareForTranslation(config: ILLoadingConfig, ctx: IRContext): Unit = { ctx.program.determineRelevantMemory(ctx.globalOffsets) - Logger.info("[!] Stripping unreachable") + Logger.debug("[!] Stripping unreachable") val before = ctx.program.procedures.size transforms.stripUnreachableFunctions(ctx.program, config.procedureTrimDepth) - Logger.info( + Logger.debug( s"[!] Removed ${before - ctx.program.procedures.size} functions (${ctx.program.procedures.size} remaining)" ) @@ -283,24 +283,24 @@ object StaticAnalysis { .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: ") - Logger.info(globalOffsets) - Logger.info("External: ") - Logger.info(externalAddresses) - Logger.info("Subroutine Addresses:") - Logger.info(subroutines) + Logger.debug("Globals:") + Logger.debug(globalAddresses) + Logger.debug("Global Offsets: ") + Logger.debug(globalOffsets) + Logger.debug("External: ") + Logger.debug(externalAddresses) + Logger.debug("Subroutine Addresses:") + Logger.debug(subroutines) // reducible loops val detector = LoopDetector(IRProgram) val foundLoops = detector.identify_loops() - foundLoops.foreach(l => Logger.info(s"Loop found: ${l.name}")) + foundLoops.foreach(l => Logger.debug(s"Loop found: ${l.name}")) val transformer = LoopTransform(foundLoops) val newLoops = transformer.llvm_transform() - newLoops.foreach(l => Logger.info(s"Loop found: ${l.name}")) + newLoops.foreach(l => Logger.debug(s"Loop found: ${l.name}")) config.analysisDotPath.foreach { s => writeToFile(dotBlockGraph(IRProgram, IRProgram.map(b => b -> b.toString).toMap), s"${s}_graph-after-reduce-$iteration.dot") @@ -309,21 +309,19 @@ object StaticAnalysis { val mergedSubroutines = subroutines ++ externalAddresses - val domain = computeDomain(IntraProcIRCursor, IRProgram.procedures) - - Logger.info("[!] Running ANR") + Logger.debug("[!] Running ANR") val ANRSolver = ANRAnalysisSolver(IRProgram) val ANRResult = ANRSolver.analyze() - Logger.info("[!] Running RNA") + Logger.debug("[!] Running RNA") val RNASolver = RNAAnalysisSolver(IRProgram) val RNAResult = RNASolver.analyze() - Logger.info("[!] Running Constant Propagation") + Logger.debug("[!] Running Constant Propagation") val constPropSolver = ConstantPropagationSolver(IRProgram) val constPropResult: Map[CFGPosition, Map[Variable, FlatElement[BitVecLiteral]]] = constPropSolver.analyze() - Logger.info("[!] Variable dependency summaries") + Logger.debug("[!] Variable dependency summaries") val scc = stronglyConnectedComponents(CallGraph, List(IRProgram.mainProcedure)) val specGlobalAddresses = ctx.specification.globals.map(s => s.address -> s.name).toMap val varDepsSummaries = VariableDependencyAnalysis(IRProgram, ctx.specification.globals, specGlobalAddresses, constPropResult, scc).analyze() @@ -351,7 +349,7 @@ object StaticAnalysis { }) - Logger.info("[!] Running RegToMemAnalysisSolver") + Logger.debug("[!] Running RegToMemAnalysisSolver") val regionAccessesAnalysisSolver = RegionAccessesAnalysisSolver(IRProgram, constPropResult, reachingDefinitionsAnalysisResults) val regionAccessesAnalysisResults = regionAccessesAnalysisSolver.analyze() @@ -364,11 +362,11 @@ object StaticAnalysis { ) }) - Logger.info("[!] Running Constant Propagation with SSA") + Logger.debug("[!] Running Constant Propagation with SSA") val constPropSolverWithSSA = ConstantPropagationSolverWithSSA(IRProgram, reachingDefinitionsAnalysisResults) val constPropResultWithSSA = constPropSolverWithSSA.analyze() - Logger.info("[!] Running MRA") + Logger.debug("[!] Running MRA") val mraSolver = MemoryRegionAnalysisSolver(IRProgram, globalAddresses, globalOffsets, mergedSubroutines, constPropResult, ANRResult, RNAResult, regionAccessesAnalysisResults, reachingDefinitionsAnalysisResults) val mraResult = mraSolver.analyze() @@ -390,12 +388,12 @@ object StaticAnalysis { ) }) - Logger.info("[!] Running MMM") + Logger.debug("[!] Running MMM") val mmm = MemoryModelMap() mmm.convertMemoryRegions(mraResult, mergedSubroutines, globalOffsets, mraSolver.procedureToSharedRegions) mmm.logRegions() - Logger.info("[!] Running Steensgaard") + Logger.debug("[!] Running Steensgaard") val steensgaardSolver = InterprocSteensgaardAnalysis(IRProgram, constPropResultWithSSA, regionAccessesAnalysisResults, mmm, reachingDefinitionsAnalysisResults, globalOffsets) steensgaardSolver.analyze() val steensgaardResults = steensgaardSolver.pointsTo() @@ -403,7 +401,7 @@ object StaticAnalysis { mmm.logRegions(memoryRegionContents) // turn fake procedures into diamonds - Logger.info("[!] Running VSA") + Logger.debug("[!] Running VSA") val vsaSolver = ValueSetAnalysisSolver(IRProgram, globalAddresses, externalAddresses, globalOffsets, subroutines, mmm, constPropResult) val vsaResult: Map[CFGPosition, LiftedElement[Map[Variable | MemoryRegion, Set[Value]]]] = vsaSolver.analyze() @@ -412,10 +410,10 @@ object StaticAnalysis { var interLiveVarsResults: Map[CFGPosition, Map[Variable, TwoElement]] = Map.empty if (IRProgram.mainProcedure.blocks.nonEmpty && IRProgram.mainProcedure.returnBlock.isDefined && IRProgram.mainProcedure.entryBlock.isDefined) { - Logger.info("[!] Running Interprocedural Live Variables Analysis") + Logger.debug("[!] Running Interprocedural Live Variables Analysis") interLiveVarsResults = InterLiveVarsAnalysis(IRProgram).analyze() - Logger.info("[!] Running Parameter Analysis") + Logger.debug("[!] Running Parameter Analysis") paramResults = ParamAnalysis(IRProgram).analyze() } else { @@ -489,7 +487,7 @@ object RunUtils { } def writeOutput(result: BASILResult): Unit = { - Logger.info("[!] Writing file...") + Logger.debug("[!] Writing file...") for (boogie <- result.boogie) { val wr = BufferedWriter(FileWriter(boogie.filename)) boogie.writeToString(wr) @@ -498,7 +496,7 @@ object RunUtils { } def loadAndTranslate(q: BASILConfig): BASILResult = { - Logger.info("[!] Loading Program") + Logger.debug("[!] Loading Program") val ctx = IRLoading.load(q.loading) IRTransform.doCleanup(ctx) @@ -514,7 +512,7 @@ object RunUtils { IRTransform.prepareForTranslation(q.loading, ctx) - Logger.info("[!] Translating to Boogie") + Logger.debug("[!] Translating to Boogie") val boogiePrograms = if (q.boogieTranslation.threadSplit && ctx.program.threads.nonEmpty) { val outPrograms = ArrayBuffer[BProgram]() @@ -540,23 +538,23 @@ object RunUtils { var modified: Boolean = true val analysisResult = mutable.ArrayBuffer[StaticAnalysisContext]() while (modified) { - Logger.info("[!] Running Static Analysis") + Logger.debug("[!] Running Static Analysis") val result = StaticAnalysis.analyse(ctx, config, iteration) analysisResult.append(result) - Logger.info("[!] Replacing Indirect Calls") + Logger.debug("[!] Replacing Indirect Calls") modified = transforms.resolveIndirectCallsUsingPointsTo( result.steensgaardResults, result.memoryRegionContents, result.reachingDefs, ctx.program ) - Logger.info("[!] Generating Procedure Summaries") + Logger.debug("[!] Generating Procedure Summaries") if (config.summariseProcedures) { IRTransform.generateProcedureSummaries(ctx, ctx.program, result.constPropResult, result.varDepsSummaries) } if (modified) { iteration += 1 - Logger.info(s"[!] Analysing again (iter $iteration)") + Logger.debug(s"[!] Analysing again (iter $iteration)") } } @@ -567,7 +565,7 @@ object RunUtils { } assert(invariant.singleCallBlockEnd(ctx.program)) - Logger.info(s"[!] Finished indirect call resolution after $iteration iterations") + Logger.debug(s"[!] Finished indirect call resolution after $iteration iterations") analysisResult.last } } diff --git a/src/test/scala/IndirectCallTests.scala b/src/test/scala/IndirectCallTests.scala index c9ffc95a5..f3042be67 100644 --- a/src/test/scala/IndirectCallTests.scala +++ b/src/test/scala/IndirectCallTests.scala @@ -1,7 +1,7 @@ -import ir.{Block, Procedure, Program, GoTo, DirectCall, Command, Statement} +import ir.{Block, Command, DirectCall, GoTo, Procedure, Program, Statement} import org.scalatest.funsuite.* +import util.{BASILConfig, BASILResult, BoogieGeneratorConfig, ILLoadingConfig, LogLevel, Logger, PerformanceTimer, RunUtils, StaticAnalysisConfig} -import util.{BASILConfig, BASILResult, BoogieGeneratorConfig, ILLoadingConfig, Logger, PerformanceTimer, RunUtils, StaticAnalysisConfig} import scala.collection.mutable.ArrayBuffer import test_util.BASILTest import test_util.TestConfig @@ -40,10 +40,11 @@ class IndirectCallTests extends BASILTest { val specPath = directoryPath + name + ".spec" val RELFPath = variationPath + ".relf" val resultPath = if conf.useBAPFrontend then variationPath + "_bap_result.txt" else variationPath + "_gtirb_result.txt" + val testSuffix = if conf.useBAPFrontend then ":BAP" else ":GTIRB" - Logger.info(BPLPath) + Logger.debug(s"$name/$variation$testSuffix") val basilResult = runBASIL(inputPath, RELFPath, Some(specPath), BPLPath, Some(StaticAnalysisConfig())) - Logger.info(BPLPath + " done") + Logger.debug(s"$name/$variation$testSuffix DONE") val boogieResult = runBoogie(directoryPath, BPLPath, conf.boogieFlags) val (boogieFailureMsg, _, _) = checkVerify(boogieResult, resultPath, conf.expectVerify) diff --git a/src/test/scala/IrreducibleLoop.scala b/src/test/scala/IrreducibleLoop.scala index 7c66001a4..adddf6064 100644 --- a/src/test/scala/IrreducibleLoop.scala +++ b/src/test/scala/IrreducibleLoop.scala @@ -32,7 +32,7 @@ class IrreducibleLoop extends AnyFunSuite { val variationPath = path + "/" + name val ADTPath = variationPath + ".adt" val RELFPath = variationPath + ".relf" - Logger.info(variationPath) + Logger.debug(variationPath) val program: Program = load(ILLoadingConfig(ADTPath, RELFPath)) @@ -41,14 +41,14 @@ class IrreducibleLoop extends AnyFunSuite { writeToFile(dotBlockGraph(program, program.filter(_.isInstanceOf[Block]).map(b => b -> b.toString).toMap), s"${variationPath}_blockgraph-before-reduce.dot") - foundLoops.foreach(l => Logger.info(s"found loops${System.lineSeparator()}$l")) + foundLoops.foreach(l => Logger.debug(s"found loops${System.lineSeparator()}$l")) val loops_to_transform = detector.irreducible_loops() assert(loops_to_transform.forall(foundLoops.contains)) val transformer = LoopTransform(foundLoops) val newLoops = transformer.llvm_transform() - newLoops.foreach(l => Logger.info(s"newloops${System.lineSeparator()}$l")) + newLoops.foreach(l => Logger.debug(s"newloops${System.lineSeparator()}$l")) val newDetect = LoopDetector(program) @@ -58,7 +58,7 @@ class IrreducibleLoop extends AnyFunSuite { assert(foundLoops2.count(_.reducible) > foundLoops.count(_.reducible)) assert(newDetect.irreducible_loops().isEmpty) - foundLoops2.foreach(l => Logger.info(s"updated found loops${System.lineSeparator()}$l")) + foundLoops2.foreach(l => Logger.debug(s"updated found loops${System.lineSeparator()}$l")) } test("irreducible 1") { @@ -79,7 +79,7 @@ class IrreducibleLoop extends AnyFunSuite { val boogieResult = Seq("boogie", "/useArrayAxioms", outPath).!! - Logger.info("Boogie result: " + boogieResult) + Logger.debug("Boogie result: " + boogieResult) assert(boogieResult.contains("Irreducible flow graphs are unsupported.")) } @@ -93,7 +93,7 @@ class IrreducibleLoop extends AnyFunSuite { val boogieResult = Seq("boogie", "/smoke", "/useArrayAxioms", outPath).!! - Logger.info("Boogie result: " + boogieResult) + Logger.debug("Boogie result: " + boogieResult) assert(boogieResult.contains("Boogie program verifier finished with 2 verified, 0 errors")) assert(!boogieResult.contains("found unreachable code")) diff --git a/src/test/scala/LiveVarsAnalysisTests.scala b/src/test/scala/LiveVarsAnalysisTests.scala index e70460a77..f2f360a7c 100644 --- a/src/test/scala/LiveVarsAnalysisTests.scala +++ b/src/test/scala/LiveVarsAnalysisTests.scala @@ -7,7 +7,6 @@ import test_util.BASILTest import util.{BASILResult, StaticAnalysisConfig} class LiveVarsAnalysisTests extends BASILTest { - Logger.setLevel(LogLevel.ERROR) private val correctPath = "./src/test/correct/" def runExample(name: String): BASILResult = { diff --git a/src/test/scala/SystemTests.scala b/src/test/scala/SystemTests.scala index fd696138d..3296ab803 100644 --- a/src/test/scala/SystemTests.scala +++ b/src/test/scala/SystemTests.scala @@ -1,4 +1,4 @@ -import util.{Logger, PerformanceTimer, StaticAnalysisConfig} +import util.{LogLevel, Logger, PerformanceTimer, StaticAnalysisConfig} import Numeric.Implicits.* import java.io.{BufferedWriter, File, FileWriter} @@ -135,11 +135,11 @@ trait SystemTests extends BASILTest { val testSuffix = if conf.useBAPFrontend then ":BAP" else ":GTIRB" val expectedOutPath = if conf.useBAPFrontend then variationPath + ".expected" else variationPath + "_gtirb.expected" - Logger.info(BPLPath) + Logger.info(s"$name/$variation$testSuffix") val timer = PerformanceTimer(s"test $name/$variation$testSuffix") runBASIL(inputPath, RELFPath, Some(specPath), BPLPath, conf.staticAnalysisConfig) val translateTime = timer.checkPoint("translate-boogie") - Logger.info(BPLPath + " done") + Logger.info(s"$name/$variation$testSuffix DONE") val boogieResult = runBoogie(directoryPath, BPLPath, conf.boogieFlags) val verifyTime = timer.checkPoint("verify") diff --git a/src/test/scala/test_util/BASILTest.scala b/src/test/scala/test_util/BASILTest.scala index 020c1dec2..79b1ec2e2 100644 --- a/src/test/scala/test_util/BASILTest.scala +++ b/src/test/scala/test_util/BASILTest.scala @@ -40,7 +40,7 @@ trait BASILTest extends AnyFunSuite { def runBoogie(directoryPath: String, bplPath: String, boogieFlags: Seq[String]): String = { val extraSpec = List.from(File(directoryPath).listFiles()).map(_.toString).filter(_.endsWith(".bpl")).filterNot(_.endsWith(bplPath)) val boogieCmd = Seq("boogie", "/printVerifiedProceduresCount:0") ++ boogieFlags ++ Seq(bplPath) ++ extraSpec - Logger.info(s"Verifying... ${boogieCmd.mkString(" ")}") + Logger.debug(s"Verifying... ${boogieCmd.mkString(" ")}") val boogieResult = boogieCmd.!! boogieResult }