diff --git a/src/main/scala/util/PerformanceTimer.scala b/src/main/scala/util/PerformanceTimer.scala index 2c7511cec..ca3951166 100644 --- a/src/main/scala/util/PerformanceTimer.scala +++ b/src/main/scala/util/PerformanceTimer.scala @@ -18,7 +18,7 @@ case class PerformanceTimer(timerName: String = "") { val delta = elapsed() lastCheckpoint = System.currentTimeMillis() checkpoints.append((name, s"${file.value}:${line.value}", 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/test/scala/DataStructureAnalysisTest.scala b/src/test/scala/DataStructureAnalysisTest.scala index 04ca1dd8c..1dfbea366 100644 --- a/src/test/scala/DataStructureAnalysisTest.scala +++ b/src/test/scala/DataStructureAnalysisTest.scala @@ -3,7 +3,7 @@ import ir.* import org.scalatest.funsuite.AnyFunSuite import ir.dsl.* import specification.{Specification, SpecGlobal} -import util.{BASILConfig, BASILResult, BoogieGeneratorConfig, ILLoadingConfig, IRContext, RunUtils, StaticAnalysisConfig, StaticAnalysisContext, writeToFile} +import util.{BASILConfig, BASILResult, BoogieGeneratorConfig, ILLoadingConfig, IRContext, RunUtils, StaticAnalysisConfig, StaticAnalysisContext, writeToFile, Logger, LogLevel} /** * This is the test suite for testing DSA functionality @@ -20,6 +20,7 @@ import util.{BASILConfig, BASILResult, BoogieGeneratorConfig, ILLoadingConfig, I class DataStructureAnalysisTest extends AnyFunSuite { def runAnalysis(program: Program): StaticAnalysisContext = { + Logger.setLevel(LogLevel.WARN) cilvisitor.visit_prog(transforms.ReplaceReturns(), program) transforms.addReturnBlocks(program) cilvisitor.visit_prog(transforms.ConvertSingleReturn(), program) diff --git a/src/test/scala/IndirectCallTests.scala b/src/test/scala/IndirectCallTests.scala index 02d0e614b..1d78be00a 100644 --- a/src/test/scala/IndirectCallTests.scala +++ b/src/test/scala/IndirectCallTests.scala @@ -1,6 +1,6 @@ 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, LogLevel, Logger, PerformanceTimer, RunUtils, StaticAnalysisConfig, MemoryRegionsMode} import scala.collection.mutable.ArrayBuffer import test_util.BASILTest @@ -43,7 +43,9 @@ class IndirectCallTests extends AnyFunSuite, BASILTest { val testSuffix = if conf.useBAPFrontend then ":BAP" else ":GTIRB" Logger.debug(s"$name/$variation$testSuffix") - val basilResult = runBASIL(inputPath, RELFPath, Some(specPath), BPLPath, Some(StaticAnalysisConfig())) + val basilResult = runBASIL(inputPath, RELFPath, Some(specPath), BPLPath, Some(StaticAnalysisConfig( + memoryRegions = MemoryRegionsMode.MRA, + ))) Logger.debug(s"$name/$variation$testSuffix DONE") val boogieResult = runBoogie(directoryPath, BPLPath, conf.boogieFlags) @@ -416,4 +418,4 @@ class IndirectCallTests extends AnyFunSuite, BASILTest { runTest("switch2", "clang", GTIRBConfig, resolvedCalls) } -} \ No newline at end of file +} diff --git a/src/test/scala/PointsToTest.scala b/src/test/scala/PointsToTest.scala index 045a2fea2..29bee79e8 100644 --- a/src/test/scala/PointsToTest.scala +++ b/src/test/scala/PointsToTest.scala @@ -3,7 +3,7 @@ import ir.Endian.LittleEndian import org.scalatest.* import org.scalatest.funsuite.* import specification.* -import util.{RunUtils, StaticAnalysisConfig, StaticAnalysis, StaticAnalysisContext, IRContext} +import util.{RunUtils, StaticAnalysisConfig, StaticAnalysis, StaticAnalysisContext, IRContext, MemoryRegionsMode} import java.io.IOException import java.nio.file.* @@ -20,7 +20,9 @@ class PointsToTest extends AnyFunSuite with OneInstancePerTest { globalOffsets: Map[BigInt, BigInt] = Map.empty): StaticAnalysisContext = { val ctx = IRContext(List.empty, externalFunctions, globals, funcEntries, globalOffsets, Specification(Set(), Set(), Map(), List(), List(), List(), Set()), program) - StaticAnalysis.analyse(ctx, StaticAnalysisConfig(), 1) + StaticAnalysis.analyse(ctx, StaticAnalysisConfig( + memoryRegions = MemoryRegionsMode.MRA, + ), 1) } /** diff --git a/src/test/scala/SystemTests.scala b/src/test/scala/SystemTests.scala index 45004391d..17f2af366 100644 --- a/src/test/scala/SystemTests.scala +++ b/src/test/scala/SystemTests.scala @@ -223,6 +223,16 @@ class DSAMemoryRegionSystemTestsGTIRB extends SystemTests { runTests("incorrect", TestConfig(staticAnalysisConfig = Some(StaticAnalysisConfig(memoryRegions = MemoryRegionsMode.DSA)), useBAPFrontend = false, expectVerify = false)) } +class MRAMemoryRegionSystemTestsBAP extends SystemTests { + runTests("correct", TestConfig(staticAnalysisConfig = Some(StaticAnalysisConfig(memoryRegions = MemoryRegionsMode.MRA)), useBAPFrontend = true, expectVerify = true)) + runTests("incorrect", TestConfig(staticAnalysisConfig = Some(StaticAnalysisConfig(memoryRegions = MemoryRegionsMode.MRA)), useBAPFrontend = true, expectVerify = false)) +} + +class MRAMemoryRegionSystemTestsGTIRB extends SystemTests { + runTests("correct", TestConfig(staticAnalysisConfig = Some(StaticAnalysisConfig(memoryRegions = MemoryRegionsMode.MRA)), useBAPFrontend = false, expectVerify = true)) + runTests("incorrect", TestConfig(staticAnalysisConfig = Some(StaticAnalysisConfig(memoryRegions = MemoryRegionsMode.MRA)), useBAPFrontend = false, expectVerify = false)) +} + class MemoryRegionTestsDSA extends SystemTests { // stack_pointer currently times out because Boogie is bad at handling abstract map accesses runTests("memory_regions", TestConfig(staticAnalysisConfig = Some(StaticAnalysisConfig(memoryRegions = MemoryRegionsMode.DSA)), useBAPFrontend = true, expectVerify = true)) @@ -245,4 +255,4 @@ class ProcedureSummaryTests extends SystemTests { class UnimplementedTests extends SystemTests { runTests("unimplemented", TestConfig(useBAPFrontend = false, expectVerify = true)) runTests("unimplemented", TestConfig(useBAPFrontend = true, expectVerify = false)) -} \ No newline at end of file +} diff --git a/src/test/scala/TimeStaticAnalysis.scala b/src/test/scala/TimeStaticAnalysis.scala index faf0f8242..f4ddb4c60 100644 --- a/src/test/scala/TimeStaticAnalysis.scala +++ b/src/test/scala/TimeStaticAnalysis.scala @@ -13,7 +13,7 @@ import ExecutionContext.Implicits.global import ir.cilvisitor.* import scala.sys.process.* -val ANALYSE_TIMEOUT: Duration = 60000.millis +val ANALYSE_TIMEOUT: Duration = 240000.millis class TimeStaticAnalysis extends AnyFunSuite { @@ -115,7 +115,7 @@ class TimeStaticAnalysis extends AnyFunSuite { } } // give up after \timeout_thresh consecutive timeouts - val timeout_thresh = 3 + val timeout_thresh = 1 var timeouts = 0 val result: List[(String, ProgStats, List[(String, String, Long)])] = sorted .map(v => { diff --git a/src/test/scala/ir/InterpreterTests.scala b/src/test/scala/ir/InterpreterTests.scala index 92f728ee8..5060cc17c 100644 --- a/src/test/scala/ir/InterpreterTests.scala +++ b/src/test/scala/ir/InterpreterTests.scala @@ -12,7 +12,6 @@ import util.ILLoadingConfig class InterpreterTests extends AnyFunSuite with BeforeAndAfter { var i: Interpreter = Interpreter() - Logger.setLevel(LogLevel.DEBUG) def getProgram(name: String): (Program, Set[SpecGlobal]) = { diff --git a/src/test/scala/test_util/BASILTest.scala b/src/test/scala/test_util/BASILTest.scala index b9003ade4..22c6dc75c 100644 --- a/src/test/scala/test_util/BASILTest.scala +++ b/src/test/scala/test_util/BASILTest.scala @@ -2,7 +2,7 @@ package test_util import org.scalatest.funsuite.AnyFunSuite import ir.{Block, Procedure, Program} -import util.{BASILConfig, BASILResult, BoogieGeneratorConfig, ILLoadingConfig, Logger, RunUtils, StaticAnalysisConfig} +import util.{BASILConfig, BASILResult, BoogieGeneratorConfig, ILLoadingConfig, Logger, RunUtils, StaticAnalysisConfig, LogLevel} import scala.sys.process.* import scala.io.Source @@ -18,6 +18,7 @@ case class TestConfig(boogieFlags: Seq[String] = Seq("/timeLimit:10", "/useArray trait BASILTest { def runBASIL(inputPath: String, RELFPath: String, specPath: Option[String], BPLPath: String, staticAnalysisConf: Option[StaticAnalysisConfig]): BASILResult = { + Logger.setLevel(LogLevel.WARN) val specFile = if (specPath.isDefined && File(specPath.get).exists) { specPath } else {