From bdcba97a26ec6dead8d45e1cae024806a98f21fd Mon Sep 17 00:00:00 2001 From: Klevis Imeri Date: Mon, 27 Jan 2025 21:30:07 +0100 Subject: [PATCH 1/6] Optimized IMC Solver and added popAll() to Solvers --- .../java/hu/bme/mit/theta/cfa/cli/CfaCli.java | 1 + .../algorithm/bounded/BoundedChecker.kt | 62 +++++++++---------- .../bounded/BoundedCheckerBuilder.kt | 4 ++ .../solver/javasmt/JavaSMTItpSolver.java | 10 +++ .../theta/solver/javasmt/JavaSMTSolver.java | 9 +++ .../impl/generic/GenericHornSolver.java | 5 ++ .../solver/smtlib/solver/SmtLibItpSolver.java | 10 +++ .../solver/smtlib/solver/SmtLibSolver.java | 10 +++ .../theta/solver/z3legacy/Z3ItpSolver.java | 12 +++- .../mit/theta/solver/z3legacy/Z3Solver.java | 10 +++ .../bme/mit/theta/solver/z3/Z3ItpSolver.java | 10 +++ .../hu/bme/mit/theta/solver/z3/Z3Solver.java | 10 +++ .../hu/bme/mit/theta/solver/SolverBase.java | 3 + .../bme/mit/theta/solver/impl/NullSolver.java | 7 ++- .../validator/ItpSolverValidatorWrapper.java | 5 ++ .../validator/SolverValidatorWrapper.java | 5 ++ .../validator/UCSolverValidatorWrapper.java | 5 ++ .../hu/bme/mit/theta/solver/SolverStub.java | 5 ++ .../java/hu/bme/mit/theta/sts/cli/StsCli.java | 1 + .../bme/mit/theta/xsts/cli/XstsCliBounded.kt | 1 + 20 files changed, 151 insertions(+), 34 deletions(-) diff --git a/subprojects/cfa/cfa-cli/src/main/java/hu/bme/mit/theta/cfa/cli/CfaCli.java b/subprojects/cfa/cfa-cli/src/main/java/hu/bme/mit/theta/cfa/cli/CfaCli.java index 2438e93338..75be1081d4 100644 --- a/subprojects/cfa/cfa-cli/src/main/java/hu/bme/mit/theta/cfa/cli/CfaCli.java +++ b/subprojects/cfa/cfa-cli/src/main/java/hu/bme/mit/theta/cfa/cli/CfaCli.java @@ -361,6 +361,7 @@ private CFA loadModel() throws Exception { monolithicExpr, abstractionSolverFactory.createSolver(), abstractionSolverFactory.createItpSolver(), + abstractionSolverFactory.createSolver(), val -> CfaToMonolithicExprKt.valToState(cfa, val), (val1, val2) -> CfaToMonolithicExprKt.valToAction(cfa, val1, val2), 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 160c414f39..80e80c3a86 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 @@ -68,7 +68,8 @@ constructor( private val bmcEnabled: () -> Boolean = { bmcSolver != null }, private val lfPathOnly: () -> Boolean = { true }, private val itpSolver: ItpSolver? = null, - private val imcEnabled: (Int) -> Boolean = { itpSolver != null }, + private val imcFpSolver: Solver? = null, + private val imcEnabled: (Int) -> Boolean = { itpSolver != null && imcFpSolver != null}, private val indSolver: Solver? = null, private val kindEnabled: (Int) -> Boolean = { indSolver != null }, private val valToState: (Valuation) -> S, @@ -189,20 +190,24 @@ constructor( private fun itp(): SafetyResult>? { val itpSolver = this.itpSolver!! + val imcFpSolver = this.imcFpSolver!! logger.write(Logger.Level.MAINSTEP, "\tStarting IMC\n") - itpSolver.push() + itpSolver.push(); val a = itpSolver.createMarker() val b = itpSolver.createMarker() val pattern = itpSolver.createBinPattern(a, b) - itpSolver.push() + itpSolver.push(); - itpSolver.add(a, unfoldedInitExpr) itpSolver.add(a, exprs[0]) itpSolver.add(b, exprs.subList(1, exprs.size)) + itpSolver.push(); + + itpSolver.add(a, unfoldedInitExpr) + if (lfPathOnly()) { // indices contains currIndex as last() itpSolver.push() for (indexing in indices) { @@ -218,23 +223,22 @@ constructor( } if (itpSolver.check().isUnsat) { - itpSolver.pop() - itpSolver.pop() + itpSolver.popAll(); logger.write(Logger.Level.MAINSTEP, "Safety proven in IMC/BMC step\n") return SafetyResult.safe(EmptyProof.getInstance(), BoundedStatistics(iteration)) } itpSolver.pop() } + itpSolver.pop() itpSolver.add(b, Not(unfoldedPropExpr(indices.last()))) + itpSolver.push() + itpSolver.add(a, unfoldedInitExpr) - val status = itpSolver.check() - - if (status.isSat) { + if (itpSolver.check().isSat) { val trace = getTrace(itpSolver.model) logger.write(Logger.Level.MAINSTEP, "CeX found in IMC/BMC step (length ${trace.length()})\n") - itpSolver.pop() - itpSolver.pop() + itpSolver.popAll() return SafetyResult.unsafe(trace, EmptyProof.getInstance(), BoundedStatistics(iteration)) } @@ -243,30 +247,24 @@ constructor( val interpolant = itpSolver.getInterpolant(pattern) val itpFormula = PathUtils.unfold(PathUtils.foldin(interpolant.eval(a), indices[1]), indices[0]) - itpSolver.pop() + + imcFpSolver.add(itpFormula) + imcFpSolver.add(Not(img)) + if (imcFpSolver.check().isUnsat) { + logger.write(Logger.Level.MAINSTEP, "Safety proven in IMC step\n") + itpSolver.popAll() + return SafetyResult.safe(EmptyProof.getInstance(), BoundedStatistics(iteration)) + } + imcFpSolver.popAll() - itpSolver.push() - itpSolver.add(a, itpFormula) - itpSolver.add(a, Not(img)) - val itpStatus = itpSolver.check() - if (itpStatus.isUnsat) { - logger.write(Logger.Level.MAINSTEP, "Safety proven in IMC step\n") - itpSolver.pop() - itpSolver.pop() - return SafetyResult.safe(EmptyProof.getInstance(), BoundedStatistics(iteration)) - } - itpSolver.pop() img = Or(img, itpFormula) - - itpSolver.push() - itpSolver.add(a, itpFormula) - itpSolver.add(a, exprs[0]) - itpSolver.add(b, exprs.subList(1, exprs.size)) - itpSolver.add(b, Not(unfoldedPropExpr(indices.last()))) + + itpSolver.pop(); + itpSolver.add(a, itpFormula) + itpSolver.push(); } - - itpSolver.pop() - itpSolver.pop() + + itpSolver.popAll() return null } diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/BoundedCheckerBuilder.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/BoundedCheckerBuilder.kt index 461dc22e37..456047a207 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/BoundedCheckerBuilder.kt +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/BoundedCheckerBuilder.kt @@ -40,6 +40,7 @@ fun buildBMC( bmcEnabled, lfPathOnly, null, + null, { false }, null, { false }, @@ -69,6 +70,7 @@ fun buildKIND( bmcEnabled, lfPathOnly, null, + null, { false }, indSolver, kindEnabled, @@ -83,6 +85,7 @@ fun buildIMC( monolithicExpr: MonolithicExpr, bmcSolver: Solver, itpSolver: ItpSolver, + imcFpSolver: Solver, valToState: (Valuation) -> S, biValToAction: (Valuation, Valuation) -> A, logger: Logger, @@ -98,6 +101,7 @@ fun buildIMC( bmcEnabled, lfPathOnly, itpSolver, + imcFpSolver, imcEnabled, null, { false }, diff --git a/subprojects/solver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTItpSolver.java b/subprojects/solver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTItpSolver.java index fade4d1266..3ced7f6dc5 100644 --- a/subprojects/solver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTItpSolver.java +++ b/subprojects/solver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTItpSolver.java @@ -57,6 +57,8 @@ final class JavaSMTItpSolver implements ItpSolver, Solver { private final JavaSMTTermTransformer termTransformer; private final SolverContext context; + + private int expCnt = 0; public JavaSMTItpSolver( final JavaSMTSymbolTable symbolTable, @@ -193,6 +195,7 @@ public SolverStatus check() { @Override public void push() { + expCnt++; markers.push(); termMap.push(); for (final JavaSMTItpMarker marker : markers) { @@ -206,6 +209,7 @@ public void push() { @Override public void pop(final int n) { + expCnt-=n; markers.pop(n); termMap.pop(n); for (final JavaSMTItpMarker marker : markers) { @@ -217,9 +221,15 @@ public void pop(final int n) { .collect(Collectors.toMap(Tuple2::get1, Tuple2::get2)); } + @Override + public void popAll() { + pop(expCnt); + } + @Override public void reset() { solver.reset(); + expCnt = 0; combinedTermMap = Map.of(); } diff --git a/subprojects/solver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTSolver.java b/subprojects/solver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTSolver.java index 032aeb7e51..697d1c36e2 100644 --- a/subprojects/solver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTSolver.java +++ b/subprojects/solver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTSolver.java @@ -69,6 +69,8 @@ final class JavaSMTSolver implements UCSolver, Solver { private final Map> assumptions; private SolverStatus status; + private int expCnt = 0; + public JavaSMTSolver( final JavaSMTSymbolTable symbolTable, final JavaSMTTransformationManager transformationManager, @@ -154,6 +156,7 @@ public SolverStatus check() { @Override public void push() { + expCnt++; assertions.push(); try { solver.push(); @@ -164,12 +167,18 @@ public void push() { @Override public void pop(final int n) { + expCnt-=n; assertions.pop(n); for (int i = 0; i < n; i++) { solver.pop(); } clearState(); } + + @Override + public void popAll() { + pop(expCnt); + } @Override public void reset() { diff --git a/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/generic/GenericHornSolver.java b/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/generic/GenericHornSolver.java index a4b43ec7aa..fe52673ad4 100644 --- a/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/generic/GenericHornSolver.java +++ b/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/generic/GenericHornSolver.java @@ -154,6 +154,11 @@ public void pop(int n) { throw new UnsupportedOperationException("Pop is not supported."); } + @Override + public void popAll() { + throw new UnsupportedOperationException("PopAll is not supported."); + } + @Override public Collection> getUnsatCore() { throw new UnsupportedOperationException("This solver cannot return unsat cores"); diff --git a/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/solver/SmtLibItpSolver.java b/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/solver/SmtLibItpSolver.java index 5cc6d9f4ef..f657d3fcc8 100644 --- a/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/solver/SmtLibItpSolver.java +++ b/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/solver/SmtLibItpSolver.java @@ -61,6 +61,8 @@ public abstract class SmtLibItpSolver implements ItpS private Valuation model; private SolverStatus status; + private int expCnt = 0; + public SmtLibItpSolver( final SmtLibSymbolTable symbolTable, final SmtLibTransformationManager transformationManager, @@ -172,6 +174,7 @@ public SolverStatus check() { @Override public void push() { + expCnt++; markers.push(); for (final var marker : markers) { marker.push(); @@ -184,6 +187,7 @@ public void push() { @Override public void pop(final int n) { + expCnt -= n; markers.pop(n); for (final var marker : markers) { marker.pop(n); @@ -195,8 +199,14 @@ public void pop(final int n) { clearState(); } + @Override + public void popAll() { + pop(expCnt); + } + @Override public void reset() { + expCnt = 0; issueGeneralCommand("(reset)"); clearState(); init(); diff --git a/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/solver/SmtLibSolver.java b/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/solver/SmtLibSolver.java index d4fba45d1f..8256a24f06 100644 --- a/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/solver/SmtLibSolver.java +++ b/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/solver/SmtLibSolver.java @@ -72,6 +72,8 @@ public class SmtLibSolver implements UCSolver, Solver { protected Collection> unsatCore; protected SolverStatus status; + private int expCnt = 0; + public SmtLibSolver( final SmtLibSymbolTable symbolTable, final SmtLibTransformationManager transformationManager, @@ -219,6 +221,7 @@ public SolverStatus check() { @Override public void push() { + expCnt++; assertions.push(); declarationStack.push(); typeStack.push(); @@ -227,15 +230,22 @@ public void push() { @Override public void pop(int n) { + expCnt -= n; assertions.pop(n); declarationStack.pop(n); typeStack.pop(n); issueGeneralCommand("(pop 1)"); clearState(); } + + @Override + public void popAll() { + pop(expCnt); + } @Override public void reset() { + expCnt = 0; issueGeneralCommand("(reset)"); clearState(); init(); diff --git a/subprojects/solver/solver-z3-legacy/src/main/java/hu/bme/mit/theta/solver/z3legacy/Z3ItpSolver.java b/subprojects/solver/solver-z3-legacy/src/main/java/hu/bme/mit/theta/solver/z3legacy/Z3ItpSolver.java index b13fa21281..6c73d9081e 100644 --- a/subprojects/solver/solver-z3-legacy/src/main/java/hu/bme/mit/theta/solver/z3legacy/Z3ItpSolver.java +++ b/subprojects/solver/solver-z3-legacy/src/main/java/hu/bme/mit/theta/solver/z3legacy/Z3ItpSolver.java @@ -48,7 +48,9 @@ final class Z3ItpSolver implements ItpSolver, Solver { private final Z3Solver solver; private final Stack markers; - + + private int expCnt = 0; + public Z3ItpSolver( final Z3SymbolTable symbolTable, final Z3TransformationManager transformationManager, @@ -172,6 +174,7 @@ public SolverStatus check() { @Override public void push() { + expCnt++; markers.push(); for (final Z3ItpMarker marker : markers) { marker.push(); @@ -181,6 +184,7 @@ public void push() { @Override public void pop(final int n) { + expCnt -= n; markers.pop(n); for (final Z3ItpMarker marker : markers) { marker.pop(n); @@ -188,8 +192,14 @@ public void pop(final int n) { solver.pop(n); } + @Override + public void popAll() { + pop(expCnt); + } + @Override public void reset() { + expCnt = 0; solver.reset(); } diff --git a/subprojects/solver/solver-z3-legacy/src/main/java/hu/bme/mit/theta/solver/z3legacy/Z3Solver.java b/subprojects/solver/solver-z3-legacy/src/main/java/hu/bme/mit/theta/solver/z3legacy/Z3Solver.java index 49e5dc4ab9..87dc92d851 100644 --- a/subprojects/solver/solver-z3-legacy/src/main/java/hu/bme/mit/theta/solver/z3legacy/Z3Solver.java +++ b/subprojects/solver/solver-z3-legacy/src/main/java/hu/bme/mit/theta/solver/z3legacy/Z3Solver.java @@ -59,6 +59,8 @@ final class Z3Solver implements UCSolver, Solver { private Collection> unsatCore; private SolverStatus status; + private int expCnt = 0; + public Z3Solver( final Z3SymbolTable symbolTable, final Z3TransformationManager transformationManager, @@ -128,19 +130,27 @@ private SolverStatus transformStatus(final Status z3Status) { @Override public void push() { + expCnt++; assertions.push(); z3Solver.push(); } @Override public void pop(final int n) { + expCnt -= n; assertions.pop(n); z3Solver.pop(n); clearState(); } + @Override + public void popAll() { + pop(expCnt); + } + @Override public void reset() { + expCnt = 0; z3Solver.reset(); assertions.clear(); assumptions.clear(); diff --git a/subprojects/solver/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3ItpSolver.java b/subprojects/solver/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3ItpSolver.java index 349fd5dfa9..96558aa6c5 100644 --- a/subprojects/solver/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3ItpSolver.java +++ b/subprojects/solver/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3ItpSolver.java @@ -74,6 +74,8 @@ final class Z3ItpSolver implements ItpSolver, Solver { private final SmtLibTransformationManager smtLibTransformationManager; private final SmtLibTermTransformer smtLibTermTransformer; + private int expCnt = 0; + public Z3ItpSolver( final Z3SymbolTable symbolTable, final Z3TransformationManager transformationManager, @@ -231,6 +233,7 @@ public SolverStatus check() { @Override public void push() { + expCnt++; markers.push(); for (final Z3ItpMarker marker : markers) { marker.push(); @@ -241,6 +244,7 @@ public void push() { @Override public void pop(final int n) { + expCnt += n; markers.pop(n); for (final Z3ItpMarker marker : markers) { marker.pop(n); @@ -249,8 +253,14 @@ public void pop(final int n) { solver.pop(n); } + @Override + public void popAll() { + pop(expCnt); + } + @Override public void reset() { + expCnt = 0; solver.reset(); } diff --git a/subprojects/solver/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3Solver.java b/subprojects/solver/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3Solver.java index 6fbf4fac56..8591b138b5 100644 --- a/subprojects/solver/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3Solver.java +++ b/subprojects/solver/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3Solver.java @@ -69,6 +69,8 @@ class Z3Solver implements UCSolver, Solver { protected Collection> unsatCore; protected SolverStatus status; + private int expCnt = 0; + public Z3Solver( final Z3SymbolTable symbolTable, final Z3TransformationManager transformationManager, @@ -138,19 +140,27 @@ private SolverStatus transformStatus(final Status z3Status) { @Override public void push() { + expCnt++; assertions.push(); z3Solver.push(); } @Override public void pop(final int n) { + expCnt -= n; assertions.pop(n); z3Solver.pop(n); clearState(); } + @Override + public void popAll() { + pop(expCnt); + } + @Override public void reset() { + expCnt = 0; z3Solver.reset(); assertions.clear(); assumptions.clear(); diff --git a/subprojects/solver/solver/src/main/java/hu/bme/mit/theta/solver/SolverBase.java b/subprojects/solver/solver/src/main/java/hu/bme/mit/theta/solver/SolverBase.java index f7a0b6dc55..bff145624b 100644 --- a/subprojects/solver/solver/src/main/java/hu/bme/mit/theta/solver/SolverBase.java +++ b/subprojects/solver/solver/src/main/java/hu/bme/mit/theta/solver/SolverBase.java @@ -48,6 +48,9 @@ default void pop() { pop(1); } + /** Remove all expressions added. */ + void popAll(); + /** Reset the solver state. */ void reset(); diff --git a/subprojects/solver/solver/src/main/java/hu/bme/mit/theta/solver/impl/NullSolver.java b/subprojects/solver/solver/src/main/java/hu/bme/mit/theta/solver/impl/NullSolver.java index 805974bc7d..48cdc4dad2 100644 --- a/subprojects/solver/solver/src/main/java/hu/bme/mit/theta/solver/impl/NullSolver.java +++ b/subprojects/solver/solver/src/main/java/hu/bme/mit/theta/solver/impl/NullSolver.java @@ -54,7 +54,12 @@ public void push() { public void pop(final int n) { throw new UnsupportedOperationException(); } - + + @Override + public void popAll() { + throw new UnsupportedOperationException(); + } + @Override public void reset() { throw new UnsupportedOperationException(); diff --git a/subprojects/solver/solver/src/main/java/hu/bme/mit/theta/solver/validator/ItpSolverValidatorWrapper.java b/subprojects/solver/solver/src/main/java/hu/bme/mit/theta/solver/validator/ItpSolverValidatorWrapper.java index 10298f693c..28a6557a31 100644 --- a/subprojects/solver/solver/src/main/java/hu/bme/mit/theta/solver/validator/ItpSolverValidatorWrapper.java +++ b/subprojects/solver/solver/src/main/java/hu/bme/mit/theta/solver/validator/ItpSolverValidatorWrapper.java @@ -86,6 +86,11 @@ public void pop(int n) { solver.pop(); } + @Override + public void popAll() { + solver.pop(); + } + @Override public void reset() { solver.reset(); diff --git a/subprojects/solver/solver/src/main/java/hu/bme/mit/theta/solver/validator/SolverValidatorWrapper.java b/subprojects/solver/solver/src/main/java/hu/bme/mit/theta/solver/validator/SolverValidatorWrapper.java index 682f6b6b84..8480c3959d 100644 --- a/subprojects/solver/solver/src/main/java/hu/bme/mit/theta/solver/validator/SolverValidatorWrapper.java +++ b/subprojects/solver/solver/src/main/java/hu/bme/mit/theta/solver/validator/SolverValidatorWrapper.java @@ -62,6 +62,11 @@ public void pop(int n) { solver.pop(); } + @Override + public void popAll() { + solver.pop(); + } + @Override public void reset() { solver.reset(); diff --git a/subprojects/solver/solver/src/main/java/hu/bme/mit/theta/solver/validator/UCSolverValidatorWrapper.java b/subprojects/solver/solver/src/main/java/hu/bme/mit/theta/solver/validator/UCSolverValidatorWrapper.java index 7fb63cd158..e86eb2ba41 100644 --- a/subprojects/solver/solver/src/main/java/hu/bme/mit/theta/solver/validator/UCSolverValidatorWrapper.java +++ b/subprojects/solver/solver/src/main/java/hu/bme/mit/theta/solver/validator/UCSolverValidatorWrapper.java @@ -57,6 +57,11 @@ public void pop(int n) { solver.pop(); } + @Override + public void popAll() { + solver.pop(); + } + @Override public void reset() { solver.reset(); diff --git a/subprojects/solver/solver/src/test/java/hu/bme/mit/theta/solver/SolverStub.java b/subprojects/solver/solver/src/test/java/hu/bme/mit/theta/solver/SolverStub.java index 059afa235e..447073244c 100644 --- a/subprojects/solver/solver/src/test/java/hu/bme/mit/theta/solver/SolverStub.java +++ b/subprojects/solver/solver/src/test/java/hu/bme/mit/theta/solver/SolverStub.java @@ -48,6 +48,11 @@ public void pop(final int n) { nPush -= n; } + @Override + public void popAll() { + pop(nPush); + } + @Override public void reset() { // Stub diff --git a/subprojects/sts/sts-cli/src/main/java/hu/bme/mit/theta/sts/cli/StsCli.java b/subprojects/sts/sts-cli/src/main/java/hu/bme/mit/theta/sts/cli/StsCli.java index 90c898bc99..5a13dc8909 100644 --- a/subprojects/sts/sts-cli/src/main/java/hu/bme/mit/theta/sts/cli/StsCli.java +++ b/subprojects/sts/sts-cli/src/main/java/hu/bme/mit/theta/sts/cli/StsCli.java @@ -299,6 +299,7 @@ private STS loadModel() throws Exception { monolithicExpr, abstractionSolverFactory.createSolver(), abstractionSolverFactory.createItpSolver(), + abstractionSolverFactory.createSolver(), val -> StsToMonolithicExprKt.valToState(sts, val), (val1, val2) -> StsToMonolithicExprKt.valToAction(sts, val1, val2), diff --git a/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliBounded.kt b/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliBounded.kt index b6ee960a00..34ba3eeae3 100644 --- a/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliBounded.kt +++ b/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliBounded.kt @@ -88,6 +88,7 @@ class XstsCliBounded : monolithicExpr, solverFactory.createSolver(), solverFactory.createItpSolver(), + solverFactory.createSolver(), valToState, biValToAction, logger, From 2bc392101bc4bf0b8ced898e0f18b9e69a767362 Mon Sep 17 00:00:00 2001 From: Klevis Imeri Date: Mon, 27 Jan 2025 22:41:56 +0100 Subject: [PATCH 2/6] Fixed itp loop faling BoundedTest --- .../mit/theta/analysis/algorithm/bounded/BoundedChecker.kt | 3 ++- .../java/hu/bme/mit/theta/analysis/algorithm/BoundedTest.kt | 4 ++++ 2 files changed, 6 insertions(+), 1 deletion(-) 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 80e80c3a86..cf6d9be115 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 @@ -248,6 +248,7 @@ constructor( val itpFormula = PathUtils.unfold(PathUtils.foldin(interpolant.eval(a), indices[1]), indices[0]) + imcFpSolver.push() imcFpSolver.add(itpFormula) imcFpSolver.add(Not(img)) if (imcFpSolver.check().isUnsat) { @@ -260,8 +261,8 @@ constructor( img = Or(img, itpFormula) itpSolver.pop(); + itpSolver.push(); itpSolver.add(a, itpFormula) - itpSolver.push(); } itpSolver.popAll() diff --git a/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/BoundedTest.kt b/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/BoundedTest.kt index 4820edd81a..1f3fd4a179 100644 --- a/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/BoundedTest.kt +++ b/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/BoundedTest.kt @@ -69,11 +69,13 @@ class BoundedTest { val solver = Z3LegacySolverFactory.getInstance().createSolver() val itpSolver = Z3LegacySolverFactory.getInstance().createItpSolver() val indSolver = Z3LegacySolverFactory.getInstance().createSolver() + val fpSolver = Z3LegacySolverFactory.getInstance().createSolver() val checker: BoundedChecker<*, *> = BoundedChecker( monolithicExpr = unsafeMonolithicExpr!!, bmcSolver = solver, itpSolver = itpSolver, + imcFpSolver = fpSolver, indSolver = indSolver, valToState = valToState, biValToAction = biValToAction, @@ -88,11 +90,13 @@ class BoundedTest { val solver = Z3LegacySolverFactory.getInstance().createSolver() val itpSolver = Z3LegacySolverFactory.getInstance().createItpSolver() val indSolver = Z3LegacySolverFactory.getInstance().createSolver() + val fpSolver = Z3LegacySolverFactory.getInstance().createSolver() val checker: BoundedChecker<*, *> = BoundedChecker( monolithicExpr = safeMonolithicExpr!!, bmcSolver = solver, itpSolver = itpSolver, + imcFpSolver = fpSolver, indSolver = indSolver, valToState = valToState, biValToAction = biValToAction, From 9a8aca4feae518ac65a32838acad6c1d9daf8071 Mon Sep 17 00:00:00 2001 From: Klevis Imeri Date: Tue, 28 Jan 2025 00:32:52 +0100 Subject: [PATCH 3/6] Updated XCFA Bounded Config for new BoundedChecker interface --- .../bme/mit/theta/analysis/algorithm/bounded/BoundedChecker.kt | 1 + .../bme/mit/theta/xcfa/cli/checkers/ConfigToBoundedChecker.kt | 3 +++ 2 files changed, 4 insertions(+) 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 cf6d9be115..f4360af0f2 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 @@ -253,6 +253,7 @@ constructor( imcFpSolver.add(Not(img)) if (imcFpSolver.check().isUnsat) { logger.write(Logger.Level.MAINSTEP, "Safety proven in IMC step\n") + imcFpSolver.popAll() itpSolver.popAll() return SafetyResult.safe(EmptyProof.getInstance(), BoundedStatistics(iteration)) } 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 a0b6f37165..80152e0539 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 @@ -61,6 +61,9 @@ fun getBoundedChecker( itpSolver = tryGetSolver(boundedConfig.itpConfig.itpSolver, boundedConfig.itpConfig.validateItpSolver) ?.createItpSolver(), + imcFpSolver = + tryGetSolver(boundedConfig.itpConfig.itpSolver, boundedConfig.itpConfig.validateItpSolver) + ?.createSolver(), imcEnabled = { !boundedConfig.itpConfig.disable }, indSolver = tryGetSolver(boundedConfig.indConfig.indSolver, boundedConfig.indConfig.validateIndSolver) From 83db5d033b595d3718e3be8bf8bf9e55df26fae6 Mon Sep 17 00:00:00 2001 From: Klevis Imeri Date: Tue, 28 Jan 2025 01:44:58 +0100 Subject: [PATCH 4/6] Fixed indenting issues and added checking for itpSolver & imcFpSolver --- .../algorithm/bounded/BoundedChecker.kt | 53 ++++++++++--------- .../bounded/BoundedCheckerBuilder.kt | 8 +-- .../theta/analysis/algorithm/BoundedTest.kt | 8 +-- .../solver/javasmt/JavaSMTItpSolver.java | 18 +++---- .../theta/solver/javasmt/JavaSMTSolver.java | 16 +++--- .../bme/mit/theta/solver/z3/Z3ItpSolver.java | 16 +++--- .../hu/bme/mit/theta/solver/z3/Z3Solver.java | 16 +++--- .../hu/bme/mit/theta/solver/SolverBase.java | 2 +- .../bme/mit/theta/solver/impl/NullSolver.java | 10 ++-- .../validator/ItpSolverValidatorWrapper.java | 8 +-- .../validator/SolverValidatorWrapper.java | 8 +-- .../validator/UCSolverValidatorWrapper.java | 8 +-- .../hu/bme/mit/theta/solver/SolverStub.java | 8 +-- .../cli/checkers/ConfigToBoundedChecker.kt | 2 +- 14 files changed, 91 insertions(+), 90 deletions(-) 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 f4360af0f2..8af9a4dbc1 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 @@ -68,7 +68,7 @@ constructor( private val bmcEnabled: () -> Boolean = { bmcSolver != null }, private val lfPathOnly: () -> Boolean = { true }, private val itpSolver: ItpSolver? = null, - private val imcFpSolver: Solver? = null, + private val imcFpSolver: Solver? = null, private val imcEnabled: (Int) -> Boolean = { itpSolver != null && imcFpSolver != null}, private val indSolver: Solver? = null, private val kindEnabled: (Int) -> Boolean = { indSolver != null }, @@ -90,6 +90,7 @@ constructor( check(bmcSolver != itpSolver || bmcSolver == null) { "Use distinct solvers for BMC and IMC!" } check(bmcSolver != indSolver || bmcSolver == null) { "Use distinct solvers for BMC and KInd!" } check(itpSolver != indSolver || itpSolver == null) { "Use distinct solvers for IMC and KInd!" } + check((itpSolver == null) == (imcFpSolver == null)) { "Both itpSolver and imcFpSolver must be either null or non-null!" } } override fun check(prec: UnitPrec?): SafetyResult> { @@ -190,7 +191,7 @@ constructor( private fun itp(): SafetyResult>? { val itpSolver = this.itpSolver!! - val imcFpSolver = this.imcFpSolver!! + val imcFpSolver = this.imcFpSolver!! logger.write(Logger.Level.MAINSTEP, "\tStarting IMC\n") itpSolver.push(); @@ -204,9 +205,9 @@ constructor( itpSolver.add(a, exprs[0]) itpSolver.add(b, exprs.subList(1, exprs.size)) - itpSolver.push(); + itpSolver.push(); - itpSolver.add(a, unfoldedInitExpr) + itpSolver.add(a, unfoldedInitExpr) if (lfPathOnly()) { // indices contains currIndex as last() itpSolver.push() @@ -223,22 +224,22 @@ constructor( } if (itpSolver.check().isUnsat) { - itpSolver.popAll(); + itpSolver.popAll(); logger.write(Logger.Level.MAINSTEP, "Safety proven in IMC/BMC step\n") return SafetyResult.safe(EmptyProof.getInstance(), BoundedStatistics(iteration)) } itpSolver.pop() } - itpSolver.pop() + itpSolver.pop() itpSolver.add(b, Not(unfoldedPropExpr(indices.last()))) - itpSolver.push() - itpSolver.add(a, unfoldedInitExpr) + itpSolver.push() + itpSolver.add(a, unfoldedInitExpr) if (itpSolver.check().isSat) { val trace = getTrace(itpSolver.model) logger.write(Logger.Level.MAINSTEP, "CeX found in IMC/BMC step (length ${trace.length()})\n") - itpSolver.popAll() + itpSolver.popAll() return SafetyResult.unsafe(trace, EmptyProof.getInstance(), BoundedStatistics(iteration)) } @@ -247,26 +248,26 @@ constructor( val interpolant = itpSolver.getInterpolant(pattern) val itpFormula = PathUtils.unfold(PathUtils.foldin(interpolant.eval(a), indices[1]), indices[0]) - - imcFpSolver.push() - imcFpSolver.add(itpFormula) - imcFpSolver.add(Not(img)) - if (imcFpSolver.check().isUnsat) { - logger.write(Logger.Level.MAINSTEP, "Safety proven in IMC step\n") - imcFpSolver.popAll() - itpSolver.popAll() - return SafetyResult.safe(EmptyProof.getInstance(), BoundedStatistics(iteration)) - } - imcFpSolver.popAll() + + imcFpSolver.push() + imcFpSolver.add(itpFormula) + imcFpSolver.add(Not(img)) + if (imcFpSolver.check().isUnsat) { + logger.write(Logger.Level.MAINSTEP, "Safety proven in IMC step\n") + imcFpSolver.popAll() + itpSolver.popAll() + return SafetyResult.safe(EmptyProof.getInstance(), BoundedStatistics(iteration)) + } + imcFpSolver.popAll() img = Or(img, itpFormula) - - itpSolver.pop(); - itpSolver.push(); - itpSolver.add(a, itpFormula) + + itpSolver.pop(); + itpSolver.push(); + itpSolver.add(a, itpFormula) } - - itpSolver.popAll() + + itpSolver.popAll() return null } diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/BoundedCheckerBuilder.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/BoundedCheckerBuilder.kt index 456047a207..c6083682aa 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/BoundedCheckerBuilder.kt +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/BoundedCheckerBuilder.kt @@ -40,7 +40,7 @@ fun buildBMC( bmcEnabled, lfPathOnly, null, - null, + null, { false }, null, { false }, @@ -70,7 +70,7 @@ fun buildKIND( bmcEnabled, lfPathOnly, null, - null, + null, { false }, indSolver, kindEnabled, @@ -85,7 +85,7 @@ fun buildIMC( monolithicExpr: MonolithicExpr, bmcSolver: Solver, itpSolver: ItpSolver, - imcFpSolver: Solver, + imcFpSolver: Solver, valToState: (Valuation) -> S, biValToAction: (Valuation, Valuation) -> A, logger: Logger, @@ -101,7 +101,7 @@ fun buildIMC( bmcEnabled, lfPathOnly, itpSolver, - imcFpSolver, + imcFpSolver, imcEnabled, null, { false }, diff --git a/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/BoundedTest.kt b/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/BoundedTest.kt index 1f3fd4a179..ea4e37f936 100644 --- a/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/BoundedTest.kt +++ b/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/BoundedTest.kt @@ -69,13 +69,13 @@ class BoundedTest { val solver = Z3LegacySolverFactory.getInstance().createSolver() val itpSolver = Z3LegacySolverFactory.getInstance().createItpSolver() val indSolver = Z3LegacySolverFactory.getInstance().createSolver() - val fpSolver = Z3LegacySolverFactory.getInstance().createSolver() + val fpSolver = Z3LegacySolverFactory.getInstance().createSolver() val checker: BoundedChecker<*, *> = BoundedChecker( monolithicExpr = unsafeMonolithicExpr!!, bmcSolver = solver, itpSolver = itpSolver, - imcFpSolver = fpSolver, + imcFpSolver = fpSolver, indSolver = indSolver, valToState = valToState, biValToAction = biValToAction, @@ -90,13 +90,13 @@ class BoundedTest { val solver = Z3LegacySolverFactory.getInstance().createSolver() val itpSolver = Z3LegacySolverFactory.getInstance().createItpSolver() val indSolver = Z3LegacySolverFactory.getInstance().createSolver() - val fpSolver = Z3LegacySolverFactory.getInstance().createSolver() + val fpSolver = Z3LegacySolverFactory.getInstance().createSolver() val checker: BoundedChecker<*, *> = BoundedChecker( monolithicExpr = safeMonolithicExpr!!, bmcSolver = solver, itpSolver = itpSolver, - imcFpSolver = fpSolver, + imcFpSolver = fpSolver, indSolver = indSolver, valToState = valToState, biValToAction = biValToAction, diff --git a/subprojects/solver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTItpSolver.java b/subprojects/solver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTItpSolver.java index 3ced7f6dc5..cf9e567e4e 100644 --- a/subprojects/solver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTItpSolver.java +++ b/subprojects/solver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTItpSolver.java @@ -57,8 +57,8 @@ final class JavaSMTItpSolver implements ItpSolver, Solver { private final JavaSMTTermTransformer termTransformer; private final SolverContext context; - - private int expCnt = 0; + + private int expCnt = 0; public JavaSMTItpSolver( final JavaSMTSymbolTable symbolTable, @@ -195,7 +195,7 @@ public SolverStatus check() { @Override public void push() { - expCnt++; + expCnt++; markers.push(); termMap.push(); for (final JavaSMTItpMarker marker : markers) { @@ -209,7 +209,7 @@ public void push() { @Override public void pop(final int n) { - expCnt-=n; + expCnt-=n; markers.pop(n); termMap.pop(n); for (final JavaSMTItpMarker marker : markers) { @@ -221,15 +221,15 @@ public void pop(final int n) { .collect(Collectors.toMap(Tuple2::get1, Tuple2::get2)); } - @Override - public void popAll() { - pop(expCnt); - } + @Override + public void popAll() { + pop(expCnt); + } @Override public void reset() { solver.reset(); - expCnt = 0; + expCnt = 0; combinedTermMap = Map.of(); } diff --git a/subprojects/solver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTSolver.java b/subprojects/solver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTSolver.java index 697d1c36e2..5f86b2b07e 100644 --- a/subprojects/solver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTSolver.java +++ b/subprojects/solver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTSolver.java @@ -69,7 +69,7 @@ final class JavaSMTSolver implements UCSolver, Solver { private final Map> assumptions; private SolverStatus status; - private int expCnt = 0; + private int expCnt = 0; public JavaSMTSolver( final JavaSMTSymbolTable symbolTable, @@ -156,7 +156,7 @@ public SolverStatus check() { @Override public void push() { - expCnt++; + expCnt++; assertions.push(); try { solver.push(); @@ -167,18 +167,18 @@ public void push() { @Override public void pop(final int n) { - expCnt-=n; + expCnt-=n; assertions.pop(n); for (int i = 0; i < n; i++) { solver.pop(); } clearState(); } - - @Override - public void popAll() { - pop(expCnt); - } + + @Override + public void popAll() { + pop(expCnt); + } @Override public void reset() { diff --git a/subprojects/solver/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3ItpSolver.java b/subprojects/solver/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3ItpSolver.java index 96558aa6c5..759bc332e7 100644 --- a/subprojects/solver/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3ItpSolver.java +++ b/subprojects/solver/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3ItpSolver.java @@ -74,7 +74,7 @@ final class Z3ItpSolver implements ItpSolver, Solver { private final SmtLibTransformationManager smtLibTransformationManager; private final SmtLibTermTransformer smtLibTermTransformer; - private int expCnt = 0; + private int expCnt = 0; public Z3ItpSolver( final Z3SymbolTable symbolTable, @@ -233,7 +233,7 @@ public SolverStatus check() { @Override public void push() { - expCnt++; + expCnt++; markers.push(); for (final Z3ItpMarker marker : markers) { marker.push(); @@ -244,7 +244,7 @@ public void push() { @Override public void pop(final int n) { - expCnt += n; + expCnt += n; markers.pop(n); for (final Z3ItpMarker marker : markers) { marker.pop(n); @@ -253,14 +253,14 @@ public void pop(final int n) { solver.pop(n); } - @Override - public void popAll() { - pop(expCnt); - } + @Override + public void popAll() { + pop(expCnt); + } @Override public void reset() { - expCnt = 0; + expCnt = 0; solver.reset(); } diff --git a/subprojects/solver/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3Solver.java b/subprojects/solver/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3Solver.java index 8591b138b5..95bf9867de 100644 --- a/subprojects/solver/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3Solver.java +++ b/subprojects/solver/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3Solver.java @@ -69,7 +69,7 @@ class Z3Solver implements UCSolver, Solver { protected Collection> unsatCore; protected SolverStatus status; - private int expCnt = 0; + private int expCnt = 0; public Z3Solver( final Z3SymbolTable symbolTable, @@ -140,27 +140,27 @@ private SolverStatus transformStatus(final Status z3Status) { @Override public void push() { - expCnt++; + expCnt++; assertions.push(); z3Solver.push(); } @Override public void pop(final int n) { - expCnt -= n; + expCnt -= n; assertions.pop(n); z3Solver.pop(n); clearState(); } - @Override - public void popAll() { - pop(expCnt); - } + @Override + public void popAll() { + pop(expCnt); + } @Override public void reset() { - expCnt = 0; + expCnt = 0; z3Solver.reset(); assertions.clear(); assumptions.clear(); diff --git a/subprojects/solver/solver/src/main/java/hu/bme/mit/theta/solver/SolverBase.java b/subprojects/solver/solver/src/main/java/hu/bme/mit/theta/solver/SolverBase.java index bff145624b..3414d5091d 100644 --- a/subprojects/solver/solver/src/main/java/hu/bme/mit/theta/solver/SolverBase.java +++ b/subprojects/solver/solver/src/main/java/hu/bme/mit/theta/solver/SolverBase.java @@ -49,7 +49,7 @@ default void pop() { } /** Remove all expressions added. */ - void popAll(); + void popAll(); /** Reset the solver state. */ void reset(); diff --git a/subprojects/solver/solver/src/main/java/hu/bme/mit/theta/solver/impl/NullSolver.java b/subprojects/solver/solver/src/main/java/hu/bme/mit/theta/solver/impl/NullSolver.java index 48cdc4dad2..f19a1493b8 100644 --- a/subprojects/solver/solver/src/main/java/hu/bme/mit/theta/solver/impl/NullSolver.java +++ b/subprojects/solver/solver/src/main/java/hu/bme/mit/theta/solver/impl/NullSolver.java @@ -54,12 +54,12 @@ public void push() { public void pop(final int n) { throw new UnsupportedOperationException(); } - - @Override - public void popAll() { + + @Override + public void popAll() { throw new UnsupportedOperationException(); - } - + } + @Override public void reset() { throw new UnsupportedOperationException(); diff --git a/subprojects/solver/solver/src/main/java/hu/bme/mit/theta/solver/validator/ItpSolverValidatorWrapper.java b/subprojects/solver/solver/src/main/java/hu/bme/mit/theta/solver/validator/ItpSolverValidatorWrapper.java index 28a6557a31..50c5c1d5d1 100644 --- a/subprojects/solver/solver/src/main/java/hu/bme/mit/theta/solver/validator/ItpSolverValidatorWrapper.java +++ b/subprojects/solver/solver/src/main/java/hu/bme/mit/theta/solver/validator/ItpSolverValidatorWrapper.java @@ -86,10 +86,10 @@ public void pop(int n) { solver.pop(); } - @Override - public void popAll() { - solver.pop(); - } + @Override + public void popAll() { + solver.pop(); + } @Override public void reset() { diff --git a/subprojects/solver/solver/src/main/java/hu/bme/mit/theta/solver/validator/SolverValidatorWrapper.java b/subprojects/solver/solver/src/main/java/hu/bme/mit/theta/solver/validator/SolverValidatorWrapper.java index 8480c3959d..48f1d54567 100644 --- a/subprojects/solver/solver/src/main/java/hu/bme/mit/theta/solver/validator/SolverValidatorWrapper.java +++ b/subprojects/solver/solver/src/main/java/hu/bme/mit/theta/solver/validator/SolverValidatorWrapper.java @@ -62,10 +62,10 @@ public void pop(int n) { solver.pop(); } - @Override - public void popAll() { - solver.pop(); - } + @Override + public void popAll() { + solver.pop(); + } @Override public void reset() { diff --git a/subprojects/solver/solver/src/main/java/hu/bme/mit/theta/solver/validator/UCSolverValidatorWrapper.java b/subprojects/solver/solver/src/main/java/hu/bme/mit/theta/solver/validator/UCSolverValidatorWrapper.java index e86eb2ba41..e45d4c0199 100644 --- a/subprojects/solver/solver/src/main/java/hu/bme/mit/theta/solver/validator/UCSolverValidatorWrapper.java +++ b/subprojects/solver/solver/src/main/java/hu/bme/mit/theta/solver/validator/UCSolverValidatorWrapper.java @@ -57,10 +57,10 @@ public void pop(int n) { solver.pop(); } - @Override - public void popAll() { - solver.pop(); - } + @Override + public void popAll() { + solver.pop(); + } @Override public void reset() { diff --git a/subprojects/solver/solver/src/test/java/hu/bme/mit/theta/solver/SolverStub.java b/subprojects/solver/solver/src/test/java/hu/bme/mit/theta/solver/SolverStub.java index 447073244c..4e364fa434 100644 --- a/subprojects/solver/solver/src/test/java/hu/bme/mit/theta/solver/SolverStub.java +++ b/subprojects/solver/solver/src/test/java/hu/bme/mit/theta/solver/SolverStub.java @@ -48,10 +48,10 @@ public void pop(final int n) { nPush -= n; } - @Override - public void popAll() { - pop(nPush); - } + @Override + public void popAll() { + pop(nPush); + } @Override public void reset() { 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 80152e0539..10f6162a58 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 @@ -61,7 +61,7 @@ fun getBoundedChecker( itpSolver = tryGetSolver(boundedConfig.itpConfig.itpSolver, boundedConfig.itpConfig.validateItpSolver) ?.createItpSolver(), - imcFpSolver = + imcFpSolver = tryGetSolver(boundedConfig.itpConfig.itpSolver, boundedConfig.itpConfig.validateItpSolver) ?.createSolver(), imcEnabled = { !boundedConfig.itpConfig.disable }, From ad4e437a0aed1be2909c4ed12f7c45c40711c290 Mon Sep 17 00:00:00 2001 From: Klevis Imeri Date: Wed, 29 Jan 2025 23:43:56 +0100 Subject: [PATCH 5/6] style: apply spotless code formatting --- .../algorithm/bounded/BoundedChecker.kt | 18 +++++++++-------- .../theta/analysis/algorithm/BoundedTest.kt | 4 ++-- .../solver/javasmt/JavaSMTItpSolver.java | 8 ++++---- .../theta/solver/javasmt/JavaSMTSolver.java | 4 ++-- .../solver/smtlib/solver/SmtLibSolver.java | 2 +- .../theta/solver/z3legacy/Z3ItpSolver.java | 20 +++++++++---------- .../mit/theta/solver/z3legacy/Z3Solver.java | 16 +++++++-------- .../cli/checkers/ConfigToBoundedChecker.kt | 2 +- 8 files changed, 38 insertions(+), 36 deletions(-) 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 8af9a4dbc1..727f08a1b3 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 @@ -69,7 +69,7 @@ constructor( private val lfPathOnly: () -> Boolean = { true }, private val itpSolver: ItpSolver? = null, private val imcFpSolver: Solver? = null, - private val imcEnabled: (Int) -> Boolean = { itpSolver != null && imcFpSolver != null}, + private val imcEnabled: (Int) -> Boolean = { itpSolver != null && imcFpSolver != null }, private val indSolver: Solver? = null, private val kindEnabled: (Int) -> Boolean = { indSolver != null }, private val valToState: (Valuation) -> S, @@ -90,7 +90,9 @@ constructor( check(bmcSolver != itpSolver || bmcSolver == null) { "Use distinct solvers for BMC and IMC!" } check(bmcSolver != indSolver || bmcSolver == null) { "Use distinct solvers for BMC and KInd!" } check(itpSolver != indSolver || itpSolver == null) { "Use distinct solvers for IMC and KInd!" } - check((itpSolver == null) == (imcFpSolver == null)) { "Both itpSolver and imcFpSolver must be either null or non-null!" } + check((itpSolver == null) == (imcFpSolver == null)) { + "Both itpSolver and imcFpSolver must be either null or non-null!" + } } override fun check(prec: UnitPrec?): SafetyResult> { @@ -194,18 +196,18 @@ constructor( val imcFpSolver = this.imcFpSolver!! logger.write(Logger.Level.MAINSTEP, "\tStarting IMC\n") - itpSolver.push(); + itpSolver.push() val a = itpSolver.createMarker() val b = itpSolver.createMarker() val pattern = itpSolver.createBinPattern(a, b) - itpSolver.push(); + itpSolver.push() itpSolver.add(a, exprs[0]) itpSolver.add(b, exprs.subList(1, exprs.size)) - itpSolver.push(); + itpSolver.push() itpSolver.add(a, unfoldedInitExpr) @@ -224,7 +226,7 @@ constructor( } if (itpSolver.check().isUnsat) { - itpSolver.popAll(); + itpSolver.popAll() logger.write(Logger.Level.MAINSTEP, "Safety proven in IMC/BMC step\n") return SafetyResult.safe(EmptyProof.getInstance(), BoundedStatistics(iteration)) } @@ -262,8 +264,8 @@ constructor( img = Or(img, itpFormula) - itpSolver.pop(); - itpSolver.push(); + itpSolver.pop() + itpSolver.push() itpSolver.add(a, itpFormula) } diff --git a/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/BoundedTest.kt b/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/BoundedTest.kt index ea4e37f936..0634269e1c 100644 --- a/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/BoundedTest.kt +++ b/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/BoundedTest.kt @@ -69,7 +69,7 @@ class BoundedTest { val solver = Z3LegacySolverFactory.getInstance().createSolver() val itpSolver = Z3LegacySolverFactory.getInstance().createItpSolver() val indSolver = Z3LegacySolverFactory.getInstance().createSolver() - val fpSolver = Z3LegacySolverFactory.getInstance().createSolver() + val fpSolver = Z3LegacySolverFactory.getInstance().createSolver() val checker: BoundedChecker<*, *> = BoundedChecker( monolithicExpr = unsafeMonolithicExpr!!, @@ -90,7 +90,7 @@ class BoundedTest { val solver = Z3LegacySolverFactory.getInstance().createSolver() val itpSolver = Z3LegacySolverFactory.getInstance().createItpSolver() val indSolver = Z3LegacySolverFactory.getInstance().createSolver() - val fpSolver = Z3LegacySolverFactory.getInstance().createSolver() + val fpSolver = Z3LegacySolverFactory.getInstance().createSolver() val checker: BoundedChecker<*, *> = BoundedChecker( monolithicExpr = safeMonolithicExpr!!, diff --git a/subprojects/solver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTItpSolver.java b/subprojects/solver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTItpSolver.java index cf9e567e4e..e79e3e6043 100644 --- a/subprojects/solver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTItpSolver.java +++ b/subprojects/solver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTItpSolver.java @@ -57,8 +57,8 @@ final class JavaSMTItpSolver implements ItpSolver, Solver { private final JavaSMTTermTransformer termTransformer; private final SolverContext context; - - private int expCnt = 0; + + private int expCnt = 0; public JavaSMTItpSolver( final JavaSMTSymbolTable symbolTable, @@ -209,7 +209,7 @@ public void push() { @Override public void pop(final int n) { - expCnt-=n; + expCnt -= n; markers.pop(n); termMap.pop(n); for (final JavaSMTItpMarker marker : markers) { @@ -221,7 +221,7 @@ public void pop(final int n) { .collect(Collectors.toMap(Tuple2::get1, Tuple2::get2)); } - @Override + @Override public void popAll() { pop(expCnt); } diff --git a/subprojects/solver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTSolver.java b/subprojects/solver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTSolver.java index 5f86b2b07e..e403c30310 100644 --- a/subprojects/solver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTSolver.java +++ b/subprojects/solver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTSolver.java @@ -167,7 +167,7 @@ public void push() { @Override public void pop(final int n) { - expCnt-=n; + expCnt -= n; assertions.pop(n); for (int i = 0; i < n; i++) { solver.pop(); @@ -175,7 +175,7 @@ public void pop(final int n) { clearState(); } - @Override + @Override public void popAll() { pop(expCnt); } diff --git a/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/solver/SmtLibSolver.java b/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/solver/SmtLibSolver.java index 8256a24f06..98797800ed 100644 --- a/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/solver/SmtLibSolver.java +++ b/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/solver/SmtLibSolver.java @@ -237,7 +237,7 @@ public void pop(int n) { issueGeneralCommand("(pop 1)"); clearState(); } - + @Override public void popAll() { pop(expCnt); diff --git a/subprojects/solver/solver-z3-legacy/src/main/java/hu/bme/mit/theta/solver/z3legacy/Z3ItpSolver.java b/subprojects/solver/solver-z3-legacy/src/main/java/hu/bme/mit/theta/solver/z3legacy/Z3ItpSolver.java index 6c73d9081e..bab40caa7a 100644 --- a/subprojects/solver/solver-z3-legacy/src/main/java/hu/bme/mit/theta/solver/z3legacy/Z3ItpSolver.java +++ b/subprojects/solver/solver-z3-legacy/src/main/java/hu/bme/mit/theta/solver/z3legacy/Z3ItpSolver.java @@ -48,9 +48,9 @@ final class Z3ItpSolver implements ItpSolver, Solver { private final Z3Solver solver; private final Stack markers; - - private int expCnt = 0; - + + private int expCnt = 0; + public Z3ItpSolver( final Z3SymbolTable symbolTable, final Z3TransformationManager transformationManager, @@ -174,7 +174,7 @@ public SolverStatus check() { @Override public void push() { - expCnt++; + expCnt++; markers.push(); for (final Z3ItpMarker marker : markers) { marker.push(); @@ -184,7 +184,7 @@ public void push() { @Override public void pop(final int n) { - expCnt -= n; + expCnt -= n; markers.pop(n); for (final Z3ItpMarker marker : markers) { marker.pop(n); @@ -192,14 +192,14 @@ public void pop(final int n) { solver.pop(n); } - @Override - public void popAll() { - pop(expCnt); - } + @Override + public void popAll() { + pop(expCnt); + } @Override public void reset() { - expCnt = 0; + expCnt = 0; solver.reset(); } diff --git a/subprojects/solver/solver-z3-legacy/src/main/java/hu/bme/mit/theta/solver/z3legacy/Z3Solver.java b/subprojects/solver/solver-z3-legacy/src/main/java/hu/bme/mit/theta/solver/z3legacy/Z3Solver.java index 87dc92d851..b1dc795649 100644 --- a/subprojects/solver/solver-z3-legacy/src/main/java/hu/bme/mit/theta/solver/z3legacy/Z3Solver.java +++ b/subprojects/solver/solver-z3-legacy/src/main/java/hu/bme/mit/theta/solver/z3legacy/Z3Solver.java @@ -59,7 +59,7 @@ final class Z3Solver implements UCSolver, Solver { private Collection> unsatCore; private SolverStatus status; - private int expCnt = 0; + private int expCnt = 0; public Z3Solver( final Z3SymbolTable symbolTable, @@ -130,27 +130,27 @@ private SolverStatus transformStatus(final Status z3Status) { @Override public void push() { - expCnt++; + expCnt++; assertions.push(); z3Solver.push(); } @Override public void pop(final int n) { - expCnt -= n; + expCnt -= n; assertions.pop(n); z3Solver.pop(n); clearState(); } - @Override - public void popAll() { - pop(expCnt); - } + @Override + public void popAll() { + pop(expCnt); + } @Override public void reset() { - expCnt = 0; + expCnt = 0; z3Solver.reset(); assertions.clear(); assumptions.clear(); 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 10f6162a58..b427868ea0 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 @@ -63,7 +63,7 @@ fun getBoundedChecker( ?.createItpSolver(), imcFpSolver = tryGetSolver(boundedConfig.itpConfig.itpSolver, boundedConfig.itpConfig.validateItpSolver) - ?.createSolver(), + ?.createSolver(), imcEnabled = { !boundedConfig.itpConfig.disable }, indSolver = tryGetSolver(boundedConfig.indConfig.indSolver, boundedConfig.indConfig.validateIndSolver) From a1f2d76ee37d39883450a6a906f61bb65f982164 Mon Sep 17 00:00:00 2001 From: Klevis Imeri Date: Tue, 18 Feb 2025 14:50:33 +0100 Subject: [PATCH 6/6] Small bug fix --- .../src/main/java/hu/bme/mit/theta/solver/z3/Z3ItpSolver.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/subprojects/solver/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3ItpSolver.java b/subprojects/solver/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3ItpSolver.java index 759bc332e7..1c2ee0083b 100644 --- a/subprojects/solver/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3ItpSolver.java +++ b/subprojects/solver/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3ItpSolver.java @@ -244,7 +244,7 @@ public void push() { @Override public void pop(final int n) { - expCnt += n; + expCnt -= n; markers.pop(n); for (final Z3ItpMarker marker : markers) { marker.pop(n);