From f5e6aefbceb07a3e45041ae9f5dcc9d2e9ea0340 Mon Sep 17 00:00:00 2001 From: Levente Bajczi Date: Mon, 11 Nov 2024 21:06:14 +0100 Subject: [PATCH] Added BOUNDED25 portfolio --- .../mit/theta/xcfa/cli/portfolio/bounded25.kt | 240 ++++++++++++++---- .../bme/mit/theta/xcfa/cli/portfolio/stm.kt | 40 ++- .../theta/xcfa/cli/XcfaCliPortfolioTest.kt | 27 +- 3 files changed, 233 insertions(+), 74 deletions(-) diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/portfolio/bounded25.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/portfolio/bounded25.kt index 3d532f2b9b..5b8d481b8b 100644 --- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/portfolio/bounded25.kt +++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/portfolio/bounded25.kt @@ -15,9 +15,11 @@ */ package hu.bme.mit.theta.xcfa.cli.portfolio +import hu.bme.mit.theta.analysis.algorithm.mdd.MddChecker import hu.bme.mit.theta.common.logging.Logger import hu.bme.mit.theta.frontend.ParseContext import hu.bme.mit.theta.frontend.transformation.ArchitectureConfig +import hu.bme.mit.theta.frontend.transformation.grammar.preprocess.ArithmeticTrait import hu.bme.mit.theta.graphsolver.patterns.constraints.MCM import hu.bme.mit.theta.xcfa.analysis.isInlined import hu.bme.mit.theta.xcfa.cli.params.* @@ -38,7 +40,7 @@ fun boundedPortfolio25( val checker = { config: XcfaConfig<*, *> -> runConfig(config, logger, uniqueLogger, true) } - var baseConfig = + var boundedBaseConfig = XcfaConfig( inputConfig = InputConfig( @@ -84,6 +86,29 @@ fun boundedPortfolio25( debugConfig = portfolioConfig.debugConfig, ) + val mddBaseConfig = + XcfaConfig( + inputConfig = boundedBaseConfig.inputConfig, + frontendConfig = boundedBaseConfig.frontendConfig, + backendConfig = + BackendConfig( + backend = Backend.MDD, + solverHome = portfolioConfig.backendConfig.solverHome, + timeoutMs = 0, + specConfig = + MddConfig( + solver = "Z3", + validateSolver = false, + iterationStrategy = MddChecker.IterationStrategy.GSAT, + reversed = false, + cegar = false, + initPrec = InitPrec.EMPTY, + ), + ), + outputConfig = boundedBaseConfig.outputConfig, + debugConfig = boundedBaseConfig.debugConfig, + ) + if (parseContext.multiThreading) { throw UnsupportedOperationException("Multithreading for bounded checkers not supported") } @@ -113,7 +138,7 @@ fun boundedPortfolio25( val anyError = ExceptionTrigger(label = "Anything") - fun XcfaConfig<*, BoundedConfig>.adaptConfig( + fun XcfaConfig.adaptConfig( bmcEnabled: Boolean = false, indEnabled: Boolean = false, itpEnabled: Boolean = false, @@ -122,6 +147,9 @@ fun boundedPortfolio25( itpSolver: String = "cvc5:1.0.8", timeoutMs: Long = 0, inProcess: Boolean = this.backendConfig.inProcess, + reversed: Boolean = false, + cegar: Boolean = false, + initprec: InitPrec = InitPrec.EMPTY, ): XcfaConfig<*, BoundedConfig> { return copy( backendConfig = @@ -130,6 +158,9 @@ fun boundedPortfolio25( inProcess = inProcess, specConfig = backendConfig.specConfig!!.copy( + reversed = reversed, + cegar = cegar, + initPrec = initprec, bmcConfig = backendConfig.specConfig!! .bmcConfig @@ -147,95 +178,204 @@ fun boundedPortfolio25( ) } - fun getStm(inProcess: Boolean): STM { + fun XcfaConfig.adaptConfig( + timeoutMs: Long = 0, + inProcess: Boolean = this.backendConfig.inProcess, + ): XcfaConfig<*, MddConfig> { + return copy(backendConfig = backendConfig.copy(timeoutMs = timeoutMs, inProcess = inProcess)) + } + + val canUseMathsat = !parseContext.arithmeticTraits.contains(ArithmeticTrait.FLOAT) + + fun getMddConfig(inProcess: Boolean): Node = + ConfigNode( + "MddZ3-GSAT-$inProcess", + mddBaseConfig.adaptConfig(inProcess = inProcess, timeoutMs = 180_000), + checker, + ) + + fun getBmcConfig(inProcess: Boolean): Node { val edges = LinkedHashSet() + lateinit var lastNode: ConfigNode + val configBmcZ3 = ConfigNode( "BmcZ3-$inProcess", - baseConfig.adaptConfig(inProcess = inProcess, bmcEnabled = true, timeoutMs = 30000), + boundedBaseConfig.adaptConfig(inProcess = inProcess, bmcEnabled = true, timeoutMs = 30_000), checker, ) - val configBmcMathsat = + lastNode = configBmcZ3 + if (canUseMathsat) { + val configBmcMathsat = + ConfigNode( + "BmcMathsat-$inProcess", + boundedBaseConfig.adaptConfig( + inProcess = inProcess, + bmcSolver = "mathsat:5.6.10", + bmcEnabled = true, + timeoutMs = 30_000, + ), + checker, + ) + edges.add(Edge(lastNode, configBmcMathsat, solverError)) + lastNode = configBmcMathsat + } + val configBmcCvc5 = ConfigNode( - "BmcMathsat-$inProcess", - baseConfig.adaptConfig( + "BmcCvc5-$inProcess", + boundedBaseConfig.adaptConfig( inProcess = inProcess, - bmcSolver = "mathsat:5.6.10", + bmcSolver = "cvc5:1.0.8", bmcEnabled = true, - timeoutMs = 30000, + timeoutMs = 30_000, ), checker, ) - val configIndZ3 = + edges.add(Edge(lastNode, configBmcCvc5, solverError)) + lastNode = configBmcCvc5 + + return HierarchicalNode("BMC_$inProcess", STM(configBmcZ3, edges)) + } + + fun getKindConfig(inProcess: Boolean): Node { + val edges = LinkedHashSet() + lateinit var lastNode: ConfigNode + + val configKindZ3 = ConfigNode( - "IndZ3-$inProcess", - baseConfig.adaptConfig( + "KindZ3-$inProcess", + boundedBaseConfig.adaptConfig( inProcess = inProcess, bmcEnabled = true, indEnabled = true, - timeoutMs = 300000, + timeoutMs = 300_000, ), checker, ) - val configIndMathsat = + lastNode = configKindZ3 + + val configKindCvc5 = ConfigNode( - "IndMathsat-$inProcess", - baseConfig.adaptConfig( + "KindCvc5-$inProcess", + boundedBaseConfig.adaptConfig( inProcess = inProcess, - bmcSolver = "mathsat:5.6.10", - indSolver = "mathsat:5.6.10", bmcEnabled = true, indEnabled = true, - timeoutMs = 300000, + bmcSolver = "cvc5:1.0.8", + indSolver = "cvc5:1.0.8", + timeoutMs = 300_000, ), checker, ) - val configItpCvc5 = + edges.add(Edge(lastNode, configKindCvc5, solverError)) + lastNode = configKindCvc5 + + if (canUseMathsat) { + val configKindMathsat = + ConfigNode( + "KindMathsat-$inProcess", + boundedBaseConfig.adaptConfig( + inProcess = inProcess, + bmcEnabled = true, + indEnabled = true, + bmcSolver = "mathsat:5.6.10", + indSolver = "mathsat:5.6.10", + timeoutMs = 300_000, + ), + checker, + ) + edges.add(Edge(lastNode, configKindMathsat, solverError)) + lastNode = configKindMathsat + } + + return HierarchicalNode("KIND_$inProcess", STM(configKindZ3, edges)) + } + + fun getIMCConfig(inProcess: Boolean): Node { + val edges = LinkedHashSet() + lateinit var lastNode: ConfigNode + + val configIMCZ3abstract = ConfigNode( - "ItpCvc5-$inProcess", - baseConfig.adaptConfig( + "IMCZ3-abstract-$inProcess", + boundedBaseConfig.adaptConfig( inProcess = inProcess, - itpEnabled = true, - itpSolver = "cvc5:1.0.8", - timeoutMs = 0, + bmcEnabled = true, + indEnabled = true, + cegar = true, + timeoutMs = 300_000, ), checker, ) - val configItpMathsat = + lastNode = configIMCZ3abstract + + val configRIMCZ3 = ConfigNode( - "ItpMathsat-$inProcess", - baseConfig.adaptConfig( + "RIMCZ3-$inProcess", + boundedBaseConfig.adaptConfig( inProcess = inProcess, - itpSolver = "mathsat:5.6.10", - itpEnabled = true, - timeoutMs = 0, + bmcEnabled = true, + indEnabled = true, + reversed = true, + timeoutMs = 300_000, ), checker, ) + edges.add(Edge(lastNode, configRIMCZ3, solverError)) + lastNode = configRIMCZ3 - edges.add(Edge(configBmcZ3, configBmcMathsat, solverError)) - edges.add( - Edge(configBmcZ3, configIndZ3, if (inProcess) timeoutOrNotSolvableError else anyError) - ) - edges.add( - Edge( - configBmcMathsat, - configIndMathsat, - if (inProcess) timeoutOrNotSolvableError else anyError, + val configRIMCCvc5 = + ConfigNode( + "RIMCCvc5-$inProcess", + boundedBaseConfig.adaptConfig( + inProcess = inProcess, + bmcEnabled = true, + indEnabled = true, + reversed = true, + bmcSolver = "cvc5:1.0.8", + indSolver = "cvc5:1.0.8", + timeoutMs = 300_000, + ), + checker, ) - ) + edges.add(Edge(lastNode, configRIMCCvc5, solverError)) + lastNode = configRIMCCvc5 - edges.add(Edge(configIndZ3, configIndMathsat, solverError)) - edges.add( - Edge(configIndZ3, configItpCvc5, if (inProcess) timeoutOrNotSolvableError else anyError) - ) - edges.add( - Edge(configIndMathsat, configItpCvc5, if (inProcess) timeoutOrNotSolvableError else anyError) - ) + if (canUseMathsat) { + val configRIMCMathsat = + ConfigNode( + "RIMCMathsat-$inProcess", + boundedBaseConfig.adaptConfig( + inProcess = inProcess, + bmcEnabled = true, + indEnabled = true, + reversed = true, + bmcSolver = "mathsat:5.6.10", + indSolver = "mathsat:5.6.10", + timeoutMs = 300_000, + ), + checker, + ) + edges.add(Edge(lastNode, configRIMCMathsat, solverError)) + lastNode = configRIMCMathsat + } + + return HierarchicalNode("IMC_$inProcess", STM(configIMCZ3abstract, edges)) + } + + fun getStm(inProcess: Boolean): STM { + val edges = LinkedHashSet() + + val mddConfig = getMddConfig(inProcess) + val bmcConfig = getBmcConfig(inProcess) + val indConfig = getKindConfig(inProcess) + val imcConfig = getIMCConfig(inProcess) - edges.add(Edge(configItpCvc5, configItpMathsat, anyError)) + edges.add(Edge(mddConfig, bmcConfig, if (inProcess) timeoutOrNotSolvableError else anyError)) + edges.add(Edge(bmcConfig, indConfig, if (inProcess) timeoutOrNotSolvableError else anyError)) + edges.add(Edge(indConfig, imcConfig, if (inProcess) timeoutOrNotSolvableError else anyError)) - return STM(configBmcZ3, edges) + return STM(mddConfig, edges) } logger.write(Logger.Level.RESULT, "Using bounded portfolio\n") diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/portfolio/stm.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/portfolio/stm.kt index a68572f6a2..b8b33c9c21 100644 --- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/portfolio/stm.kt +++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/portfolio/stm.kt @@ -16,6 +16,8 @@ package hu.bme.mit.theta.xcfa.cli.portfolio import hu.bme.mit.theta.analysis.algorithm.SafetyResult +import hu.bme.mit.theta.xcfa.cli.params.Backend +import hu.bme.mit.theta.xcfa.cli.params.BoundedConfig import hu.bme.mit.theta.xcfa.cli.params.XcfaConfig abstract class Node(val name: String) { @@ -28,7 +30,7 @@ abstract class Node(val name: String) { abstract fun visualize(): String } -class HierarchicalNode(name: String, private val innerSTM: STM) : Node(name) { +class HierarchicalNode(name: String, val innerSTM: STM) : Node(name) { override fun execute(): Pair = innerSTM.execute() @@ -39,6 +41,24 @@ ${innerSTM.visualize()} .trimIndent() } +fun XcfaConfig<*, *>.visualize(): String = + if (backendConfig.backend == Backend.BOUNDED) { + val specConfig = backendConfig.specConfig as BoundedConfig + """ + reversed: ${specConfig.reversed} + abstract: ${specConfig.cegar} + bmc: ${!specConfig.bmcConfig.disable} + bmcSolver: ${specConfig.bmcConfig.bmcSolver} + kind: ${!specConfig.indConfig.disable} + kindSolver: ${specConfig.indConfig.indSolver} + imc: ${!specConfig.itpConfig.disable} + imcSolver: ${specConfig.itpConfig.itpSolver} + """ + .trimIndent() + } else { + "" + } + class ConfigNode( name: String, private val config: XcfaConfig<*, *>, @@ -52,7 +72,7 @@ class ConfigNode( override fun visualize(): String = config - .toString() + .visualize() .lines() // TODO: reintroduce visualize() .map { "state ${name.replace(Regex("[:\\.-]+"), "_")}: $it" } .reduce { a, b -> "$a\n$b" } @@ -108,13 +128,15 @@ data class STM(val initNode: Node, val edges: Set) { } } - private fun visualizeNodes(): String = - edges - .map { listOf(it.source, it.target) } - .flatten() - .toSet() - .map { it.visualize() } - .reduce { a, b -> "$a\n$b" } + private fun visualizeNodes(): String { + val lastNodes = mutableSetOf() + val nodes = mutableSetOf(initNode) + while (!lastNodes.containsAll(nodes)) { + lastNodes.addAll(nodes) + nodes.addAll(nodes.flatMap { it.outEdges.map { it.target } }) + } + return nodes.map { it.visualize() }.reduce { a, b -> "$a\n$b" } + } fun visualize(): String = """ diff --git a/subprojects/xcfa/xcfa-cli/src/test/java/hu/bme/mit/theta/xcfa/cli/XcfaCliPortfolioTest.kt b/subprojects/xcfa/xcfa-cli/src/test/java/hu/bme/mit/theta/xcfa/cli/XcfaCliPortfolioTest.kt index bcd0d3c02b..a21bf274a3 100644 --- a/subprojects/xcfa/xcfa-cli/src/test/java/hu/bme/mit/theta/xcfa/cli/XcfaCliPortfolioTest.kt +++ b/subprojects/xcfa/xcfa-cli/src/test/java/hu/bme/mit/theta/xcfa/cli/XcfaCliPortfolioTest.kt @@ -18,7 +18,6 @@ package hu.bme.mit.theta.xcfa.cli import hu.bme.mit.theta.common.logging.Logger import hu.bme.mit.theta.common.logging.NullLogger import hu.bme.mit.theta.frontend.ParseContext -import hu.bme.mit.theta.frontend.transformation.grammar.preprocess.ArithmeticTrait import hu.bme.mit.theta.graphsolver.patterns.constraints.MCM import hu.bme.mit.theta.xcfa.cli.params.SpecBackendConfig import hu.bme.mit.theta.xcfa.cli.params.SpecFrontendConfig @@ -108,20 +107,18 @@ class XcfaCliPortfolioTest { uniqueLogger: Logger, ) -> STM ) { + val stm = + portfolio( + XCFA("name", setOf()), + emptySet(), + ParseContext(), + XcfaConfig(), + NullLogger.getInstance(), + NullLogger.getInstance(), + ) - for (value in ArithmeticTrait.values()) { - - val stm = - portfolio( - XCFA("name", setOf()), - emptySet(), - ParseContext(), - XcfaConfig(), - NullLogger.getInstance(), - NullLogger.getInstance(), - ) - - Assertions.assertTrue(stm.visualize().isNotEmpty()) - } + val vis = stm.visualize() + System.err.println(vis) + Assertions.assertTrue(vis.isNotEmpty()) } }