Skip to content

Commit

Permalink
formatting
Browse files Browse the repository at this point in the history
  • Loading branch information
@csanadtelbisz
csanadtelbisz committed Oct 18, 2024
1 parent d873017 commit 9b013e7
Show file tree
Hide file tree
Showing 2 changed files with 55 additions and 67 deletions.
4 changes: 3 additions & 1 deletion subprojects/solver/solver/src/main/java/hu/bme/mit/theta/solver/SolverBase.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -84,5 +84,7 @@ default void pop() {
*
* @return Statistics
*/
default ImmutableMap<String, String> getStatistics() { return ImmutableMap.of(); }
default ImmutableMap<String, String> getStatistics() {
return ImmutableMap.of();
}
}
118 changes: 52 additions & 66 deletions subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/ExecuteConfig.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -68,8 +68,7 @@ import java.util.concurrent.TimeUnit
import kotlin.random.Random

fun runConfig(
config: XcfaConfig<*, *>, logger: Logger, uniqueLogger: Logger,
throwDontExit: Boolean
config: XcfaConfig<*, *>, logger: Logger, uniqueLogger: Logger, throwDontExit: Boolean
): SafetyResult<*, *> {
propagateInputOptions(config, logger, uniqueLogger)

Expand Down Expand Up @@ -113,17 +112,13 @@ private fun propagateInputOptions(config: XcfaConfig<*, *>, logger: Logger, uniq

private fun validateInputOptions(config: XcfaConfig<*, *>, logger: Logger, uniqueLogger: Logger) {
rule("NoCoiWhenDataRace") {
config.backendConfig.backend == Backend.CEGAR &&
(config.backendConfig.specConfig as? CegarConfig)?.coi != ConeOfInfluenceMode.NO_COI &&
config.inputConfig.property == ErrorDetection.DATA_RACE
config.backendConfig.backend == Backend.CEGAR && (config.backendConfig.specConfig as? CegarConfig)?.coi != ConeOfInfluenceMode.NO_COI && config.inputConfig.property == ErrorDetection.DATA_RACE
}
rule("NoAaporWhenDataRace") {
(config.backendConfig.specConfig as? CegarConfig)?.porLevel?.isAbstractionAware == true &&
config.inputConfig.property == ErrorDetection.DATA_RACE
(config.backendConfig.specConfig as? CegarConfig)?.porLevel?.isAbstractionAware == true && config.inputConfig.property == ErrorDetection.DATA_RACE
}
rule("DPORWithoutDFS") {
(config.backendConfig.specConfig as? CegarConfig)?.porLevel?.isDynamic == true &&
(config.backendConfig.specConfig as? CegarConfig)?.abstractorConfig?.search != Search.DFS
(config.backendConfig.specConfig as? CegarConfig)?.porLevel?.isDynamic == true && (config.backendConfig.specConfig as? CegarConfig)?.abstractorConfig?.search != Search.DFS
}
rule("SensibleLoopUnrollLimits") {
config.frontendConfig.loopUnroll != -1 && config.frontendConfig.loopUnroll < config.frontendConfig.forceUnroll
Expand Down Expand Up @@ -181,74 +176,70 @@ fun frontend(config: XcfaConfig<*, *>, logger: Logger, uniqueLogger: Logger): Tr
)

logger.write(RESULT, "ParsingResult Success\n")
logger.write(RESULT,
logger.write(
RESULT,
"Alias graph size: ${xcfa.pointsToGraph.size} -> ${xcfa.pointsToGraph.values.map { it.size }.toList()}\n"
)

return Triple(xcfa, mcm, parseContext)
}

private fun backend(
xcfa: XCFA, mcm: MCM, parseContext: ParseContext, config: XcfaConfig<*, *>,
logger: Logger,
uniqueLogger: Logger,
xcfa: XCFA, mcm: MCM, parseContext: ParseContext, config: XcfaConfig<*, *>, logger: Logger, uniqueLogger: Logger,
throwDontExit: Boolean
): SafetyResult<*, *> =
if (config.backendConfig.backend == Backend.NONE) {
SafetyResult.unknown<EmptyWitness, EmptyCex>()
): SafetyResult<*, *> = if (config.backendConfig.backend == Backend.NONE) {
SafetyResult.unknown<EmptyWitness, EmptyCex>()
} else {
if (xcfa.procedures.all { it.errorLoc.isEmpty && config.inputConfig.property == ErrorDetection.ERROR_LOCATION }) {
val result = SafetyResult.safe<EmptyWitness, EmptyCex>(EmptyWitness.getInstance())
logger.write(Logger.Level.INFO, "Input is trivially safe\n")

logger.write(RESULT, result.toString() + "\n")
result
} else {
if (xcfa.procedures.all { it.errorLoc.isEmpty && config.inputConfig.property == ErrorDetection.ERROR_LOCATION }) {
val result = SafetyResult.safe<EmptyWitness, EmptyCex>(EmptyWitness.getInstance())
logger.write(Logger.Level.INFO, "Input is trivially safe\n")

logger.write(RESULT, result.toString() + "\n")
result
} else {
val stopwatch = Stopwatch.createStarted()

logger.write(
Logger.Level.INFO,
"Starting verification of ${if (xcfa.name == "") "UnnamedXcfa" else xcfa.name} using ${config.backendConfig.backend}\n"
)

val checker = getChecker(xcfa, mcm, config, parseContext, logger, uniqueLogger)
val result = exitOnError(config.debugConfig.stacktrace, config.debugConfig.debug || throwDontExit) {
checker.check()
}.let { result ->
when {
result.isSafe && LoopUnrollPass.FORCE_UNROLL_USED -> { // cannot report safe if force unroll was used
logger.write(RESULT, "Incomplete loop unroll used: safe result is unreliable.\n")
if (config.outputConfig.acceptUnreliableSafe) result // for comparison with BMC tools
else SafetyResult.unknown<EmptyWitness, EmptyCex>()
}

else -> result
val stopwatch = Stopwatch.createStarted()

logger.write(
Logger.Level.INFO,
"Starting verification of ${if (xcfa.name == "") "UnnamedXcfa" else xcfa.name} using ${config.backendConfig.backend}\n"
)

val checker = getChecker(xcfa, mcm, config, parseContext, logger, uniqueLogger)
val result = exitOnError(config.debugConfig.stacktrace, config.debugConfig.debug || throwDontExit) {
checker.check()
}.let { result ->
when {
result.isSafe && LoopUnrollPass.FORCE_UNROLL_USED -> { // cannot report safe if force unroll was used
logger.write(RESULT, "Incomplete loop unroll used: safe result is unreliable.\n")
if (config.outputConfig.acceptUnreliableSafe) result // for comparison with BMC tools
else SafetyResult.unknown<EmptyWitness, EmptyCex>()
}

else -> result
}
}

logger.write(
Logger.Level.INFO, "Backend finished (in ${
stopwatch.elapsed(TimeUnit.MILLISECONDS)
} ms)\n"
)
logger.write(
Logger.Level.INFO, "Backend finished (in ${
stopwatch.elapsed(TimeUnit.MILLISECONDS)
} ms)\n"
)

logger.write(RESULT, result.toString() + "\n")
result
}
logger.write(RESULT, result.toString() + "\n")
result
}
}

private fun preVerificationLogging(
xcfa: XCFA, mcm: MCM, parseContext: ParseContext, config: XcfaConfig<*, *>,
logger: Logger, uniqueLogger: Logger
xcfa: XCFA, mcm: MCM, parseContext: ParseContext, config: XcfaConfig<*, *>, logger: Logger, uniqueLogger: Logger
) {
if (config.outputConfig.enableOutput) {
try {
val resultFolder = config.outputConfig.resultFolder
resultFolder.mkdirs()

logger.write(
Logger.Level.INFO,
"Writing pre-verification artifacts to directory ${resultFolder.absolutePath}\n"
Logger.Level.INFO, "Writing pre-verification artifacts to directory ${resultFolder.absolutePath}\n"
)

if (!config.outputConfig.chcOutputConfig.disable) {
Expand Down Expand Up @@ -292,8 +283,8 @@ private fun preVerificationLogging(
}

private fun postVerificationLogging(
safetyResult: SafetyResult<*, *>, mcm: MCM,
parseContext: ParseContext, config: XcfaConfig<*, *>, logger: Logger, uniqueLogger: Logger
safetyResult: SafetyResult<*, *>, mcm: MCM, parseContext: ParseContext, config: XcfaConfig<*, *>, logger: Logger,
uniqueLogger: Logger
) {
if (config.outputConfig.enableOutput) {
try {
Expand All @@ -306,8 +297,7 @@ private fun postVerificationLogging(
resultFolder.mkdirs()

logger.write(
Logger.Level.INFO,
"Writing post-verification artifacts to directory ${resultFolder.absolutePath}\n"
Logger.Level.INFO, "Writing post-verification artifacts to directory ${resultFolder.absolutePath}\n"
)

// TODO eliminate the need for the instanceof check
Expand All @@ -320,12 +310,10 @@ private fun postVerificationLogging(
if (!config.outputConfig.witnessConfig.disable) {
if (safetyResult.isUnsafe && safetyResult.asUnsafe().cex != null && !config.outputConfig.witnessConfig.svcomp) {
val concrTrace: Trace<XcfaState<ExplState>, XcfaAction> = XcfaTraceConcretizer.concretize(
safetyResult.asUnsafe().cex as Trace<XcfaState<PtrState<*>>, XcfaAction>?,
getSolver(
safetyResult.asUnsafe().cex as Trace<XcfaState<PtrState<*>>, XcfaAction>?, getSolver(
config.outputConfig.witnessConfig.concretizerSolver,
config.outputConfig.witnessConfig.validateConcretizerSolver
),
parseContext
), parseContext
)

val traceFile = File(resultFolder, "trace.dot")
Expand All @@ -334,8 +322,7 @@ private fun postVerificationLogging(

val sequenceFile = File(resultFolder, "trace.plantuml")
writeSequenceTrace(
sequenceFile,
safetyResult.asUnsafe().cex as Trace<XcfaState<ExplState>, XcfaAction>
sequenceFile, safetyResult.asUnsafe().cex as Trace<XcfaState<ExplState>, XcfaAction>
) { (_, act) ->
act.label.getFlatLabels().map(XcfaLabel::toString)
}
Expand All @@ -354,8 +341,7 @@ private fun postVerificationLogging(
}
val witnessFile = File(resultFolder, "witness.graphml")
XcfaWitnessWriter().writeWitness(
safetyResult, config.inputConfig.input!!,
getSolver(
safetyResult, config.inputConfig.input!!, getSolver(
config.outputConfig.witnessConfig.concretizerSolver,
config.outputConfig.witnessConfig.validateConcretizerSolver
), parseContext, witnessFile
Expand Down

0 comments on commit 9b013e7

Please sign in to comment.