From e41291840c8fef5b07eaee74485d71f1dde749e9 Mon Sep 17 00:00:00 2001 From: AdamZsofi Date: Mon, 28 Oct 2024 11:21:04 +0100 Subject: [PATCH] xcfa-cli trace generation can be built, but not tested --- .../bme/mit/theta/xcfa/cli/ExecuteConfig.kt | 5 ++-- .../xcfa/cli/checkers/ConfigToChecker.kt | 23 +++++++++++++++++-- .../mit/theta/xcfa/cli/portfolio/bounded.kt | 3 ++- .../mit/theta/xcfa/cli/portfolio/complex23.kt | 3 ++- .../mit/theta/xcfa/cli/portfolio/complex24.kt | 3 ++- .../bme/mit/theta/xcfa/cli/portfolio/horn.kt | 3 ++- .../hu/bme/mit/theta/xcfa/cli/XcfaDslTest.kt | 6 ++--- 7 files changed, 34 insertions(+), 12 deletions(-) diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/ExecuteConfig.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/ExecuteConfig.kt index ec37a3bf42..8a58b1fdc2 100644 --- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/ExecuteConfig.kt +++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/ExecuteConfig.kt @@ -26,14 +26,12 @@ import hu.bme.mit.theta.analysis.algorithm.* import hu.bme.mit.theta.analysis.algorithm.arg.ARG import hu.bme.mit.theta.analysis.algorithm.arg.debug.ARGWebDebugger import hu.bme.mit.theta.analysis.algorithm.tracegeneration.TraceGenerationChecker -import hu.bme.mit.theta.analysis.algorithm.tracegeneration.summary.AbstractSummaryNode import hu.bme.mit.theta.analysis.algorithm.tracegeneration.summary.AbstractTraceSummary import hu.bme.mit.theta.analysis.algorithm.tracegeneration.summary.TraceGenerationResult import hu.bme.mit.theta.analysis.expl.ExplPrec import hu.bme.mit.theta.analysis.expl.ExplState import hu.bme.mit.theta.analysis.ptr.PtrPrec import hu.bme.mit.theta.analysis.ptr.PtrState -import hu.bme.mit.theta.analysis.utils.AbstractTraceSummaryVisualizer import hu.bme.mit.theta.analysis.utils.ArgVisualizer import hu.bme.mit.theta.analysis.utils.TraceVisualizer import hu.bme.mit.theta.c2xcfa.CMetaData @@ -56,6 +54,7 @@ import hu.bme.mit.theta.xcfa.analysis.coi.XcfaCoiSingleThread import hu.bme.mit.theta.xcfa.analysis.por.XcfaDporLts import hu.bme.mit.theta.xcfa.analysis.por.XcfaSporLts import hu.bme.mit.theta.xcfa.cli.checkers.getChecker +import hu.bme.mit.theta.xcfa.cli.checkers.getSafetyChecker import hu.bme.mit.theta.xcfa.cli.params.* import hu.bme.mit.theta.xcfa.cli.utils.* import hu.bme.mit.theta.xcfa.cli.witnesses.XcfaTraceConcretizer @@ -277,7 +276,7 @@ private fun safetyBackend( return result } else { val stopwatch = Stopwatch.createStarted() - val checker = getChecker(xcfa, mcm, config, parseContext, logger, uniqueLogger) as SafetyChecker<*, *, XcfaPrec<*>> + val checker = getSafetyChecker(xcfa, mcm, config, parseContext, logger, uniqueLogger) val result = exitOnError(config.debugConfig.stacktrace, config.debugConfig.debug || throwDontExit) { checker.check() diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToChecker.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToChecker.kt index 984324dc82..348a7e0f61 100644 --- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToChecker.kt +++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToChecker.kt @@ -32,9 +32,9 @@ import hu.bme.mit.theta.xcfa.cli.params.Backend import hu.bme.mit.theta.xcfa.cli.params.XcfaConfig import hu.bme.mit.theta.xcfa.model.XCFA -fun getChecker(xcfa: XCFA, mcm: MCM, config: XcfaConfig<*, *>, parseContext: ParseContext, +fun getSafetyChecker(xcfa: XCFA, mcm: MCM, config: XcfaConfig<*, *>, parseContext: ParseContext, logger: Logger, - uniqueLogger: Logger): Checker<*, XcfaPrec<*>> = + uniqueLogger: Logger): SafetyChecker<*, *, XcfaPrec<*>> = if (config.backendConfig.inProcess) { InProcessChecker(xcfa, config, parseContext, logger) } else { @@ -46,7 +46,26 @@ fun getChecker(xcfa: XCFA, mcm: MCM, config: XcfaConfig<*, *>, parseContext: Par Backend.PORTFOLIO -> getPortfolioChecker(xcfa, mcm, config, parseContext, logger, uniqueLogger) Backend.NONE -> SafetyChecker>, XcfaAction>, Trace>, XcfaAction>, XcfaPrec<*>> { _ -> SafetyResult.unknown() } Backend.CHC -> getHornChecker(xcfa, mcm, config, logger) + Backend.TRACEGEN -> throw RuntimeException("Trace generation is NOT safety analysis, can not return safety checker for trace generation") + } + } + +fun getChecker(xcfa: XCFA, mcm: MCM, config: XcfaConfig<*, *>, parseContext: ParseContext, + logger: Logger, + uniqueLogger: Logger): Checker<*, XcfaPrec<*>> = + if (config.backendConfig.inProcess) { + InProcessChecker(xcfa, config, parseContext, logger) + } else { + when (config.backendConfig.backend) { Backend.TRACEGEN -> getTracegenChecker(xcfa, mcm, config, logger) + Backend.CEGAR -> throw RuntimeException("Use getSafetyChecker method for safety analysis instead of getChecker") + Backend.BOUNDED -> throw RuntimeException("Use getSafetyChecker method for safety analysis instead of getChecker") + Backend.OC -> throw RuntimeException("Use getSafetyChecker method for safety analysis instead of getChecker") + Backend.LAZY -> TODO() + Backend.PORTFOLIO -> throw RuntimeException("Use getSafetyChecker method for portfolio safety analysis instead of getChecker") + Backend.NONE -> SafetyChecker>, XcfaAction>, Trace>, XcfaAction>, XcfaPrec<*>> { _ -> SafetyResult.unknown() } + Backend.CHC -> throw RuntimeException("Use getSafetyChecker method for safety analysis instead of getChecker") } } + diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/portfolio/bounded.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/portfolio/bounded.kt index 787774d93f..0360acc295 100644 --- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/portfolio/bounded.kt +++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/portfolio/bounded.kt @@ -16,6 +16,7 @@ package hu.bme.mit.theta.xcfa.cli.portfolio +import hu.bme.mit.theta.analysis.algorithm.SafetyResult import hu.bme.mit.theta.analysis.expr.refinement.PruneStrategy import hu.bme.mit.theta.common.logging.Logger import hu.bme.mit.theta.frontend.ParseContext @@ -40,7 +41,7 @@ fun boundedPortfolio( logger: Logger, uniqueLogger: Logger): STM { - val checker = { config: XcfaConfig<*, *> -> runConfig(config, logger, uniqueLogger, true) } + val checker = { config: XcfaConfig<*, *> -> runConfig(config, logger, uniqueLogger, true) as SafetyResult<*, *> } var baseConfig = XcfaConfig( inputConfig = InputConfig( diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/portfolio/complex23.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/portfolio/complex23.kt index c6901d3838..83f98a7915 100644 --- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/portfolio/complex23.kt +++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/portfolio/complex23.kt @@ -16,6 +16,7 @@ package hu.bme.mit.theta.xcfa.cli.portfolio +import hu.bme.mit.theta.analysis.algorithm.SafetyResult import hu.bme.mit.theta.analysis.expr.refinement.PruneStrategy import hu.bme.mit.theta.common.logging.Logger import hu.bme.mit.theta.frontend.ParseContext @@ -35,7 +36,7 @@ fun complexPortfolio23(xcfa: XCFA, mcm: MCM, logger: Logger, uniqueLogger: Logger): STM { - val checker = { config: XcfaConfig<*, *> -> runConfig(config, logger, uniqueLogger, true) } + val checker = { config: XcfaConfig<*, *> -> runConfig(config, logger, uniqueLogger, true) as SafetyResult<*, *> } var baseConfig = XcfaConfig( inputConfig = InputConfig( diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/portfolio/complex24.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/portfolio/complex24.kt index ca6f147553..2353b3c112 100644 --- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/portfolio/complex24.kt +++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/portfolio/complex24.kt @@ -16,6 +16,7 @@ package hu.bme.mit.theta.xcfa.cli.portfolio +import hu.bme.mit.theta.analysis.algorithm.SafetyResult import hu.bme.mit.theta.analysis.expr.refinement.PruneStrategy import hu.bme.mit.theta.common.logging.Logger import hu.bme.mit.theta.frontend.ParseContext @@ -39,7 +40,7 @@ fun complexPortfolio24( logger: Logger, uniqueLogger: Logger): STM { - val checker = { config: XcfaConfig<*, *> -> runConfig(config, logger, uniqueLogger, true) } + val checker = { config: XcfaConfig<*, *> -> runConfig(config, logger, uniqueLogger, true) as SafetyResult<*, *> } var baseConfig = XcfaConfig( inputConfig = InputConfig( diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/portfolio/horn.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/portfolio/horn.kt index 5a3933b59c..f5a59f931e 100644 --- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/portfolio/horn.kt +++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/portfolio/horn.kt @@ -16,6 +16,7 @@ package hu.bme.mit.theta.xcfa.cli.portfolio +import hu.bme.mit.theta.analysis.algorithm.SafetyResult import hu.bme.mit.theta.common.logging.Logger import hu.bme.mit.theta.frontend.ParseContext import hu.bme.mit.theta.frontend.transformation.ArchitectureConfig @@ -36,7 +37,7 @@ fun hornPortfolio( logger: Logger, uniqueLogger: Logger): STM { - val checker = { config: XcfaConfig<*, *> -> runConfig(config, logger, uniqueLogger, true) } + val checker = { config: XcfaConfig<*, *> -> runConfig(config, logger, uniqueLogger, true) as SafetyResult<*, *> } var baseConfig = XcfaConfig( inputConfig = InputConfig( diff --git a/subprojects/xcfa/xcfa-cli/src/test/java/hu/bme/mit/theta/xcfa/cli/XcfaDslTest.kt b/subprojects/xcfa/xcfa-cli/src/test/java/hu/bme/mit/theta/xcfa/cli/XcfaDslTest.kt index 53d5ba6130..d53d8a56c7 100644 --- a/subprojects/xcfa/xcfa-cli/src/test/java/hu/bme/mit/theta/xcfa/cli/XcfaDslTest.kt +++ b/subprojects/xcfa/xcfa-cli/src/test/java/hu/bme/mit/theta/xcfa/cli/XcfaDslTest.kt @@ -20,7 +20,7 @@ import hu.bme.mit.theta.core.type.inttype.IntExprs.Int import hu.bme.mit.theta.frontend.ParseContext import hu.bme.mit.theta.solver.SolverManager import hu.bme.mit.theta.solver.z3legacy.Z3SolverManager -import hu.bme.mit.theta.xcfa.cli.checkers.getChecker +import hu.bme.mit.theta.xcfa.cli.checkers.getSafetyChecker import hu.bme.mit.theta.xcfa.cli.params.* import hu.bme.mit.theta.xcfa.model.ParamDirection.IN import hu.bme.mit.theta.xcfa.model.ParamDirection.OUT @@ -91,14 +91,14 @@ class XcfaDslTest { backendConfig = BackendConfig(backend = Backend.CEGAR, specConfig = CegarConfig())) run { val xcfa = getSyncXcfa() - val checker = getChecker(xcfa, emptySet(), config, ParseContext(), NullLogger.getInstance(), + val checker = getSafetyChecker(xcfa, emptySet(), config, ParseContext(), NullLogger.getInstance(), NullLogger.getInstance()) val safetyResult = checker.check() Assert.assertTrue(safetyResult.isSafe) } run { val xcfa = getAsyncXcfa() - val checker = getChecker(xcfa, emptySet(), config, ParseContext(), NullLogger.getInstance(), + val checker = getSafetyChecker(xcfa, emptySet(), config, ParseContext(), NullLogger.getInstance(), NullLogger.getInstance()) val safetyResult = checker.check() Assert.assertTrue(safetyResult.isUnsafe)