From 24db94fc5fcfd6a85d42556c2bfab2980c96d4ab Mon Sep 17 00:00:00 2001 From: AdamZsofi Date: Wed, 24 Jul 2024 10:54:30 +0200 Subject: [PATCH 1/6] added bounded portfolio --- .../MddExpressionRepresentation.java | 2 +- .../xcfa/cli/checkers/ConfigToPortfolio.kt | 2 + .../mit/theta/xcfa/cli/portfolio/bounded.kt | 199 ++++++++++++++++++ 3 files changed, 202 insertions(+), 1 deletion(-) create mode 100644 subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/portfolio/bounded.kt diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/expressionnode/MddExpressionRepresentation.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/expressionnode/MddExpressionRepresentation.java index 74415db439..9816236b4d 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/expressionnode/MddExpressionRepresentation.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/expressionnode/MddExpressionRepresentation.java @@ -409,7 +409,7 @@ public QueryResult queryEdge() { return QueryResult.failed(); } - // TODO összevonni queryChilddal + // TODO osszevonni queryChilddal public MddNode moveDown(int assignment) { if (queryEdge(assignment)) { popNegatedAssignments(); diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToPortfolio.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToPortfolio.kt index d7331c2946..4c545780ca 100644 --- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToPortfolio.kt +++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToPortfolio.kt @@ -31,6 +31,7 @@ import hu.bme.mit.theta.xcfa.analysis.XcfaState import hu.bme.mit.theta.xcfa.cli.params.PortfolioConfig import hu.bme.mit.theta.xcfa.cli.params.XcfaConfig import hu.bme.mit.theta.xcfa.cli.portfolio.STM +import hu.bme.mit.theta.xcfa.cli.portfolio.boundedPortfolio import hu.bme.mit.theta.xcfa.cli.portfolio.complexPortfolio23 import hu.bme.mit.theta.xcfa.cli.portfolio.complexPortfolio24 import hu.bme.mit.theta.xcfa.model.XCFA @@ -54,6 +55,7 @@ fun getPortfolioChecker(xcfa: XCFA, mcm: MCM, config: XcfaConfig<*, *>, "COMPLEX24" -> complexPortfolio24(xcfa, mcm, parseContext, config, logger, uniqueLogger) "COMPLEX23" -> complexPortfolio23(xcfa, mcm, parseContext, config, logger, uniqueLogger) + "BOUNDED" -> boundedPortfolio(xcfa, mcm, parseContext, config, logger, uniqueLogger) else -> { if (File(portfolioName).exists()) { val kotlinEngine: ScriptEngine = ScriptEngineManager().getEngineByExtension("kts") 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 new file mode 100644 index 0000000000..787774d93f --- /dev/null +++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/portfolio/bounded.kt @@ -0,0 +1,199 @@ +/* + * Copyright 2024 Budapest University of Technology and Economics + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ + +package hu.bme.mit.theta.xcfa.cli.portfolio + +import hu.bme.mit.theta.analysis.expr.refinement.PruneStrategy +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.solver.Solver +import hu.bme.mit.theta.xcfa.analysis.ErrorDetection +import hu.bme.mit.theta.xcfa.analysis.isInlined +import hu.bme.mit.theta.xcfa.cli.params.* +import hu.bme.mit.theta.xcfa.cli.runConfig +import hu.bme.mit.theta.xcfa.model.XCFA +import hu.bme.mit.theta.xcfa.passes.LbePass +import hu.bme.mit.theta.xcfa.passes.LoopUnrollPass +import java.nio.file.Paths + +fun boundedPortfolio( + xcfa: XCFA, + mcm: MCM, + parseContext: ParseContext, + portfolioConfig: XcfaConfig<*, *>, + logger: Logger, + uniqueLogger: Logger): STM { + + val checker = { config: XcfaConfig<*, *> -> runConfig(config, logger, uniqueLogger, true) } + + var baseConfig = XcfaConfig( + inputConfig = InputConfig( + input = null, + xcfaWCtx = Triple(xcfa, mcm, parseContext), + propertyFile = null, + property = portfolioConfig.inputConfig.property), + frontendConfig = FrontendConfig( + lbeLevel = LbePass.level, + loopUnroll = LoopUnrollPass.UNROLL_LIMIT, + inputType = InputType.C, + specConfig = CFrontendConfig(arithmetic = ArchitectureConfig.ArithmeticType.efficient)), + backendConfig = BackendConfig( + backend = Backend.BOUNDED, + solverHome = portfolioConfig.backendConfig.solverHome, + timeoutMs = 0, + specConfig = BoundedConfig( + bmcConfig = BMCConfig(true), + maxBound = 0, + indConfig = InductionConfig(true), + itpConfig = InterpolationConfig(true) + )), + outputConfig = OutputConfig( + versionInfo = false, + resultFolder = Paths.get("./").toFile(), // cwd + cOutputConfig = COutputConfig(disable = true), + witnessConfig = WitnessConfig(disable = false, concretizerSolver = "Z3", validateConcretizerSolver = false), + argConfig = ArgConfig(disable = true), + enableOutput = portfolioConfig.outputConfig.enableOutput, + ), + debugConfig = portfolioConfig.debugConfig + ) + + if (parseContext.multiThreading) { + throw UnsupportedOperationException("Multithreading for bounded checkers not supported") + } + + if (!xcfa.isInlined) { + throw UnsupportedOperationException("Recursive XCFA for bounded checkers not supported") + } + + val timeoutOrNotSolvableError = ExceptionTrigger( + fallthroughExceptions = setOf( + ErrorCodeException(ExitCodes.SOLVER_ERROR.code), + ErrorCodeException(ExitCodes.SERVER_ERROR.code), + ), + label = "TimeoutOrNotSolvableError" + ) + + val timeoutOrSolverError = ExceptionTrigger( + fallthroughExceptions = setOf( + ErrorCodeException(ExitCodes.SERVER_ERROR.code), + ), + label = "TimeoutOrSolverError" + ) + + val solverError = ExceptionTrigger( + ErrorCodeException(ExitCodes.SOLVER_ERROR.code), + label = "SolverError" + ) + + val anyError = ExceptionTrigger(label = "Anything") + + fun XcfaConfig<*, BoundedConfig>.adaptConfig( + bmcEnabled: Boolean = false, + indEnabled: Boolean = false, + itpEnabled: Boolean = false, + bmcSolver: String = "Z3", + indSolver: String = "Z3", + itpSolver: String = "cvc5:1.0.8", + timeoutMs: Long = 0, + inProcess: Boolean = this.backendConfig.inProcess + ): XcfaConfig<*, BoundedConfig> { + return copy(backendConfig = backendConfig.copy( + timeoutMs = timeoutMs, + inProcess = inProcess, + specConfig = backendConfig.specConfig!!.copy( + bmcConfig = backendConfig.specConfig!!.bmcConfig.copy(disable = !bmcEnabled, bmcSolver = bmcSolver), + indConfig = backendConfig.specConfig!!.indConfig.copy(disable = !indEnabled, indSolver = indSolver), + itpConfig = backendConfig.specConfig!!.itpConfig.copy(disable = !itpEnabled, itpSolver = itpSolver), + ) + )) + } + + fun getStm(inProcess: Boolean): STM { + val edges = LinkedHashSet() + val configBmcZ3 = ConfigNode("BmcZ3-$inProcess", + baseConfig.adaptConfig( + inProcess = inProcess, + bmcEnabled = true, + timeoutMs = 30000 + ), checker) + val configBmcMathsat = ConfigNode("BmcMathsat-$inProcess", + baseConfig.adaptConfig( + inProcess = inProcess, + bmcSolver = "mathsat:5.6.10", + bmcEnabled = true, + timeoutMs = 30000 + ), checker) + val configIndZ3 = ConfigNode("IndZ3-$inProcess", + baseConfig.adaptConfig( + inProcess = inProcess, + bmcEnabled = true, + indEnabled = true, + timeoutMs = 300000 + ), checker) + val configIndMathsat = ConfigNode("IndMathsat-$inProcess", + baseConfig.adaptConfig( + inProcess = inProcess, + bmcSolver = "mathsat:5.6.10", + indSolver = "mathsat:5.6.10", + bmcEnabled = true, + indEnabled = true, + timeoutMs = 300000 + ), checker) + val configItpCvc5 = ConfigNode("ItpCvc5-$inProcess", + baseConfig.adaptConfig( + inProcess = inProcess, + itpEnabled = true, + itpSolver = "cvc5:1.0.8", + timeoutMs = 0 + ), checker) + val configItpMathsat = ConfigNode("ItpMathsat-$inProcess", + baseConfig.adaptConfig( + inProcess = inProcess, + itpSolver = "mathsat:5.6.10", + itpEnabled = true, + timeoutMs = 0 + ), checker) + + 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)) + + 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)) + + edges.add(Edge(configItpCvc5, configItpMathsat, anyError)) + + return STM(configBmcZ3, edges) + } + + logger.write(Logger.Level.RESULT, "Using bounded portfolio\n") + + val inProcess = HierarchicalNode("InProcess", getStm(true)) + val notInProcess = HierarchicalNode("NotInprocess", getStm(false)) + + val fallbackEdge = Edge(inProcess, notInProcess, ExceptionTrigger(label = "Anything")) + + return if (portfolioConfig.debugConfig.debug) getStm(false) else STM(inProcess, setOf(fallbackEdge)) +} \ No newline at end of file From 1c787e60ecb292a7a7f8549a3c87b098654f7e51 Mon Sep 17 00:00:00 2001 From: "ThetaBotMaintainer[bot]" <139346997+ThetaBotMaintainer[bot]@users.noreply.github.com> Date: Wed, 24 Jul 2024 08:57:41 +0000 Subject: [PATCH 2/6] Version bump --- build.gradle.kts | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/build.gradle.kts b/build.gradle.kts index 6d975998c8..235741e9d6 100644 --- a/build.gradle.kts +++ b/build.gradle.kts @@ -28,7 +28,7 @@ buildscript { allprojects { group = "hu.bme.mit.theta" - version = "6.1.0" + version = "6.2.0" apply(from = rootDir.resolve("gradle/shared-with-buildSrc/mirrors.gradle.kts")) } From 30f27013cb0d6de98bddfac4f0b3d511720ec8f2 Mon Sep 17 00:00:00 2001 From: AdamZsofi Date: Wed, 24 Jul 2024 11:04:12 +0200 Subject: [PATCH 3/6] added bounded portfolio test --- .../hu/bme/mit/theta/xcfa/cli/XcfaCliVerifyTest.kt | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/subprojects/xcfa/xcfa-cli/src/test/java/hu/bme/mit/theta/xcfa/cli/XcfaCliVerifyTest.kt b/subprojects/xcfa/xcfa-cli/src/test/java/hu/bme/mit/theta/xcfa/cli/XcfaCliVerifyTest.kt index 335211363e..88a4a345e6 100644 --- a/subprojects/xcfa/xcfa-cli/src/test/java/hu/bme/mit/theta/xcfa/cli/XcfaCliVerifyTest.kt +++ b/subprojects/xcfa/xcfa-cli/src/test/java/hu/bme/mit/theta/xcfa/cli/XcfaCliVerifyTest.kt @@ -254,6 +254,20 @@ class XcfaCliVerifyTest { main(params) } + @ParameterizedTest + @MethodSource("singleThreadedCFiles") + fun testCVerifyBoundedPortfolio(filePath: String, extraArgs: String?) { + val params = arrayOf( + "--backend", "PORTFOLIO", + "--portfolio", "BOUNDED", + "--input-type", "C", + "--input", javaClass.getResource(filePath)!!.path, + "--stacktrace", + "--debug" + ) + main(params) + } + @ParameterizedTest @MethodSource("cFilesShortInt") fun testCVerifyCHC(filePath: String, extraArgs: String?) { From 57ef146ba8661c360367fefe20b72a4e3940698f Mon Sep 17 00:00:00 2001 From: AdamZsofi Date: Wed, 24 Jul 2024 11:26:15 +0200 Subject: [PATCH 4/6] handling not installed solvers gracefully --- .../cli/checkers/ConfigToBoundedChecker.kt | 23 ++++++++++++++----- 1 file changed, 17 insertions(+), 6 deletions(-) diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToBoundedChecker.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToBoundedChecker.kt index 729db2bbed..8ec6d16b95 100644 --- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToBoundedChecker.kt +++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToBoundedChecker.kt @@ -34,6 +34,9 @@ import hu.bme.mit.theta.core.type.inttype.IntExprs.Neq import hu.bme.mit.theta.core.utils.StmtUtils import hu.bme.mit.theta.core.utils.indexings.VarIndexingFactory import hu.bme.mit.theta.graphsolver.patterns.constraints.MCM +import hu.bme.mit.theta.solver.SolverFactory +import hu.bme.mit.theta.solver.smtlib.solver.installer.SmtLibSolverInstaller +import hu.bme.mit.theta.solver.smtlib.solver.installer.SmtLibSolverInstallerException import hu.bme.mit.theta.xcfa.analysis.XcfaAction import hu.bme.mit.theta.xcfa.analysis.XcfaPrec import hu.bme.mit.theta.xcfa.analysis.XcfaState @@ -57,15 +60,15 @@ fun getBoundedChecker(xcfa: XCFA, mcm: MCM, return BoundedChecker( monolithicExpr = getMonolithicExpr(xcfa), - bmcSolver = getSolver(boundedConfig.bmcConfig.bmcSolver, - boundedConfig.bmcConfig.validateBMCSolver).createSolver(), + bmcSolver = tryGetSolver(boundedConfig.bmcConfig.bmcSolver, + boundedConfig.bmcConfig.validateBMCSolver)?.createSolver(), bmcEnabled = { !boundedConfig.bmcConfig.disable }, lfPathOnly = { !boundedConfig.bmcConfig.nonLfPath }, - itpSolver = getSolver(boundedConfig.itpConfig.itpSolver, - boundedConfig.itpConfig.validateItpSolver).createItpSolver(), + itpSolver = tryGetSolver(boundedConfig.itpConfig.itpSolver, + boundedConfig.itpConfig.validateItpSolver)?.createItpSolver(), imcEnabled = { !boundedConfig.itpConfig.disable }, - indSolver = getSolver(boundedConfig.indConfig.indSolver, - boundedConfig.indConfig.validateIndSolver).createSolver(), + indSolver = tryGetSolver(boundedConfig.indConfig.indSolver, + boundedConfig.indConfig.validateIndSolver)?.createSolver(), kindEnabled = { !boundedConfig.indConfig.disable }, valToState = { valToState(xcfa, it) }, biValToAction = { val1, val2 -> valToAction(xcfa, val1, val2) }, @@ -74,6 +77,14 @@ fun getBoundedChecker(xcfa: XCFA, mcm: MCM, } +private fun tryGetSolver(name : String, validate : Boolean) : SolverFactory? { + try { + return getSolver(name, validate) + } catch (e : SmtLibSolverInstallerException) { + return null + } +} + private fun getMonolithicExpr(xcfa: XCFA): MonolithicExpr { Preconditions.checkArgument(xcfa.initProcedures.size == 1) val proc = xcfa.initProcedures.stream().findFirst().orElse(null).first From 0a07c830be0bfd86acd6856afb24e0e252e13f38 Mon Sep 17 00:00:00 2001 From: "ThetaBotMaintainer[bot]" <139346997+ThetaBotMaintainer[bot]@users.noreply.github.com> Date: Wed, 24 Jul 2024 09:29:37 +0000 Subject: [PATCH 5/6] Reformatted code --- .../bme/mit/theta/xcfa/cli/checkers/ConfigToBoundedChecker.kt | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToBoundedChecker.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToBoundedChecker.kt index 8ec6d16b95..b642f5c840 100644 --- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToBoundedChecker.kt +++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToBoundedChecker.kt @@ -77,10 +77,10 @@ fun getBoundedChecker(xcfa: XCFA, mcm: MCM, } -private fun tryGetSolver(name : String, validate : Boolean) : SolverFactory? { +private fun tryGetSolver(name: String, validate: Boolean): SolverFactory? { try { return getSolver(name, validate) - } catch (e : SmtLibSolverInstallerException) { + } catch (e: SmtLibSolverInstallerException) { return null } } From a10bd4822ae30846391405fb1ebc52001c757940 Mon Sep 17 00:00:00 2001 From: AdamZsofi Date: Wed, 24 Jul 2024 11:47:43 +0200 Subject: [PATCH 6/6] catch any throwable when instantiating solvers --- .../bme/mit/theta/xcfa/cli/checkers/ConfigToBoundedChecker.kt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToBoundedChecker.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToBoundedChecker.kt index b642f5c840..52194fa0aa 100644 --- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToBoundedChecker.kt +++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToBoundedChecker.kt @@ -80,7 +80,7 @@ fun getBoundedChecker(xcfa: XCFA, mcm: MCM, private fun tryGetSolver(name: String, validate: Boolean): SolverFactory? { try { return getSolver(name, validate) - } catch (e: SmtLibSolverInstallerException) { + } catch (e: Throwable) { return null } }