From ebae61580de4625bcd5eac35dab7627c4cfb7060 Mon Sep 17 00:00:00 2001 From: AdamZsofi Date: Sat, 29 Nov 2025 14:27:30 +0100 Subject: [PATCH] missing bmc bound added to checker --- .../analysis/algorithm/SafetyResult.java | 11 +++- .../algorithm/bounded/BoundedChecker.kt | 61 +++++++++---------- .../formalisms/FormalismPipelineChecker.kt | 7 ++- .../cli/checkers/ConfigToBoundedChecker.kt | 1 + 4 files changed, 46 insertions(+), 34 deletions(-) diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/SafetyResult.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/SafetyResult.java index 61981ac181..f55c86937c 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/SafetyResult.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/SafetyResult.java @@ -26,7 +26,7 @@ public abstract class SafetyResult implements R private final Optional stats; private SafetyResult(final Pr proof, final Optional stats) { - this.proof = checkNotNull(proof); + this.proof = proof; this.stats = checkNotNull(stats); } @@ -72,6 +72,11 @@ public static Unknown unknown(final Sta return new Unknown<>(Optional.ofNullable(stats)); } + public static Unknown unknown( + final Pr proof, final Statistics stats) { + return new Unknown<>(proof, Optional.ofNullable(stats)); + } + public abstract boolean isSafe(); public abstract boolean isUnsafe(); @@ -174,6 +179,10 @@ public Unknown(final Optional stats) { super(null, stats); } + public Unknown(final Pr proof, final Optional stats) { + super(proof, stats); + } + @Override public boolean isSafe() { return false; diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/BoundedChecker.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/BoundedChecker.kt index 29b17a15d3..01a9d54703 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/BoundedChecker.kt +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/BoundedChecker.kt @@ -29,7 +29,6 @@ import hu.bme.mit.theta.core.type.Expr import hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.Eq import hu.bme.mit.theta.core.type.booltype.BoolExprs.True import hu.bme.mit.theta.core.type.booltype.BoolType -import hu.bme.mit.theta.core.type.booltype.SmartBoolExprs import hu.bme.mit.theta.core.type.booltype.SmartBoolExprs.* import hu.bme.mit.theta.core.utils.ExprUtils import hu.bme.mit.theta.core.utils.PathUtils @@ -136,7 +135,7 @@ constructor( } } } - return SafetyResult.unknown(BoundedStatistics(iteration)) + return SafetyResult.unknown(PredState.of(extractProof()), BoundedStatistics(iteration)) } private fun bmc(): SafetyResult>? { @@ -153,7 +152,11 @@ constructor( Logger.Level.MAINSTEP, "CeX found in the initial state (length ${trace.length()})\n", ) - return SafetyResult.unsafe(trace, PredState.of(), BoundedStatistics(iteration)) + return SafetyResult.unsafe( + trace, + PredState.of(extractProof()), + BoundedStatistics(iteration), + ) } } } @@ -177,19 +180,7 @@ constructor( if (bmcSolver.check().isUnsat) { logger.write(Logger.Level.MAINSTEP, "Safety proven in BMC step\n") - val proof = - if (needProof) { - // we enumerate all states explored by previous iteration of BMC - val expr = - And( - exprs.subList(0, exprs.size - 1) + - // loopfree.subList(0, loopfree.size - 1) + - unfoldedInitExpr - ) - extractModel(expr, indices.subList(0, indices.size - 1)) - } else { - True() - } + val proof = extractProof() return SafetyResult.safe(PredState.of(proof), BoundedStatistics(iteration)) } } @@ -200,7 +191,7 @@ constructor( if (bmcSolver.check().isSat) { val trace = getTrace(bmcSolver.model) logger.write(Logger.Level.MAINSTEP, "CeX found in BMC step (length ${trace.length()})\n") - SafetyResult.unsafe(trace, PredState.of(), BoundedStatistics(iteration)) + SafetyResult.unsafe(trace, PredState.of(extractProof()), BoundedStatistics(iteration)) } else null } } @@ -266,7 +257,11 @@ constructor( Logger.Level.MAINSTEP, "CeX found in the initial state (length ${trace.length()})\n", ) - return SafetyResult.unsafe(trace, PredState.of(), BoundedStatistics(iteration)) + return SafetyResult.unsafe( + trace, + PredState.of(extractProof()), + BoundedStatistics(iteration), + ) } } } @@ -297,19 +292,7 @@ constructor( itpSolver.pop() itpSolver.pop() logger.write(Logger.Level.MAINSTEP, "Safety proven in IMC/BMC step\n") - val proof = - if (needProof) { - // we enumerate all states explored by previous iteration of BMC - val expr = - SmartBoolExprs.And( - exprs.subList(0, exprs.size - 1) + - // loopfree.subList(0, loopfree.size - 1) + - unfoldedInitExpr - ) - extractModel(expr, indices.subList(0, indices.size - 1)) - } else { - True() - } + val proof = extractProof() return SafetyResult.safe(PredState.of(proof), BoundedStatistics(iteration)) } itpSolver.pop() @@ -324,7 +307,7 @@ constructor( logger.write(Logger.Level.MAINSTEP, "CeX found in IMC/BMC step (length ${trace.length()})\n") itpSolver.pop() itpSolver.pop() - return SafetyResult.unsafe(trace, PredState.of(), BoundedStatistics(iteration)) + return SafetyResult.unsafe(trace, PredState.of(extractProof()), BoundedStatistics(iteration)) } var img = unfoldedInitExpr @@ -362,6 +345,20 @@ constructor( return null } + private fun extractProof(): Expr? = + if (needProof) { + // we enumerate all states explored by previous iteration of BMC + val expr = + And( + exprs.subList(0, exprs.size - 1) + + // loopfree.subList(0, loopfree.size - 1) + + unfoldedInitExpr + ) + extractModel(expr, indices.subList(0, indices.size - 1)) + } else { + True() + } + private fun getTrace(model: Valuation): Trace { val stateList = LinkedList() val actionList = LinkedList() diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/pipeline/formalisms/FormalismPipelineChecker.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/pipeline/formalisms/FormalismPipelineChecker.kt index 7b8cc45bf0..436d37bd53 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/pipeline/formalisms/FormalismPipelineChecker.kt +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/pipeline/formalisms/FormalismPipelineChecker.kt @@ -58,11 +58,16 @@ open class FormalismPipelineChecker< val result = pipeline.check(input) return if (result.isSafe) SafetyResult.safe(modelAdapter.proofToModelProof(result.proof), result.stats.orElse(null)) - else + else if (result.isUnsafe) SafetyResult.unsafe( modelAdapter.traceToModelTrace(result.asUnsafe().cex), modelAdapter.proofToModelProof(result.proof), result.stats.orElse(null), ) + else + SafetyResult.unknown( + result.proof?.let { modelAdapter.proofToModelProof(it) }, + result.stats.orElse(null), + ) } } 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 e975773096..682d3e0187 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 @@ -53,6 +53,7 @@ fun getBoundedChecker( val baseChecker = { monolithicExpr: MonolithicExpr -> BoundedChecker( + shouldGiveUp = { if (boundedConfig.maxBound == 0) false else it > boundedConfig.maxBound }, monolithicExpr = monolithicExpr, bmcSolver = tryGetSolver(boundedConfig.bmcConfig.bmcSolver, boundedConfig.bmcConfig.validateBMCSolver)