xcfa-cli trace generation can be built, but not tested

ftsrg · Oct 28, 2024 · e412918 · e412918
1 parent 5520360
commit e412918
Show file tree

Hide file tree

Showing 7 changed files with 34 additions and 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
@@ -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/...rojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToChecker.kt b/...rojects/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<ARG<XcfaState<PtrState<*>>, XcfaAction>, Trace<XcfaState<PtrState<*>>, 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<ARG<XcfaState<PtrState<*>>, XcfaAction>, Trace<XcfaState<PtrState<*>>, 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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)