From ad7ff95d0e7afadb9921bb67b903c095dc213582 Mon Sep 17 00:00:00 2001 From: RipplB Date: Sat, 12 Oct 2024 08:33:57 +0200 Subject: [PATCH] Rename Witness to Proof --- .../impact/CfaPredImpactCheckerTest.java | 45 +- .../java/hu/bme/mit/theta/cfa/cli/CfaCli.java | 217 +++--- .../mit/theta/analysis/algorithm/Checker.java | 5 +- .../{EmptyWitness.java => EmptyProof.java} | 10 +- .../algorithm/{Witness.java => Proof.java} | 3 +- .../mit/theta/analysis/algorithm/Result.java | 5 +- .../analysis/algorithm/SafetyChecker.java | 12 +- .../analysis/algorithm/SafetyResult.java | 85 +-- .../mit/theta/analysis/algorithm/arg/ARG.java | 74 +-- .../algorithm/bounded/BoundedChecker.kt | 405 ++++++------ .../analysis/algorithm/cegar/Abstractor.java | 21 +- .../algorithm/cegar/BasicArgAbstractor.java | 47 +- .../algorithm/cegar/CegarChecker.java | 50 +- .../analysis/algorithm/cegar/Refiner.java | 6 +- .../analysis/algorithm/chc/HornChecker.kt | 83 +-- .../mcm/analysis/FiniteStateChecker.kt | 91 ++- .../analysis/algorithm/mdd/MddChecker.java | 163 +++-- .../mdd/{MddWitness.java => MddProof.java} | 10 +- .../theta/analysis/utils/ArgVisualizer.java | 97 ++- ...ssVisualizer.java => ProofVisualizer.java} | 8 +- .../algorithm/mdd/MddCheckerTest.java | 159 +++-- .../theta/grammar/gson/SafetyResultAdapter.kt | 114 ++-- .../mit/theta/sts/analysis/StsExplTest.java | 85 ++- .../theta/sts/analysis/StsMddCheckerTest.java | 93 ++- .../mit/theta/sts/analysis/StsPredTest.java | 89 ++- .../java/hu/bme/mit/theta/sts/cli/StsCli.java | 187 ++++-- .../theta/xcfa/analysis/oc/XcfaOcChecker.kt | 615 +++++++++--------- .../bme/mit/theta/xcfa/cli/ExecuteConfig.kt | 588 +++++++++-------- .../cli/checkers/ConfigToBoundedChecker.kt | 63 +- .../xcfa/cli/checkers/ConfigToCegarChecker.kt | 214 +++--- .../xcfa/cli/checkers/ConfigToHornChecker.kt | 52 +- .../xcfa/cli/checkers/ConfigToOcChecker.kt | 30 +- .../xcfa/cli/checkers/InProcessChecker.kt | 250 +++---- .../mit/theta/xcfa/cli/XcfaCliProofTest.kt | 136 ++++ .../mit/theta/xcfa/cli/XcfaCliWitnessTest.kt | 130 ---- .../xsts/analysis/mdd/XstsMddChecker.java | 157 +++-- .../xsts/analysis/XstsMddCheckerTest.java | 215 +++--- .../bme/mit/theta/xsts/cli/XstsCliBounded.kt | 168 +++-- .../hu/bme/mit/theta/xsts/cli/XstsCliCegar.kt | 144 ++-- .../hu/bme/mit/theta/xsts/cli/XstsCliMdd.kt | 98 ++- .../xta/analysis/LazyXtaCheckerTest.java | 60 +- .../theta/xta/analysis/XtaAnalysisTest.java | 67 +- .../xta/analysis/XtaZoneAnalysisTest.java | 75 +-- .../java/hu/bme/mit/theta/xta/cli/XtaCli.java | 77 ++- 44 files changed, 2904 insertions(+), 2399 deletions(-) rename subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/{EmptyWitness.java => EmptyProof.java} (78%) rename subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/{Witness.java => Proof.java} (95%) rename subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/{MddWitness.java => MddProof.java} (81%) rename subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/utils/{WitnessVisualizer.java => ProofVisualizer.java} (83%) create mode 100644 subprojects/xcfa/xcfa-cli/src/test/java/hu/bme/mit/theta/xcfa/cli/XcfaCliProofTest.kt delete mode 100644 subprojects/xcfa/xcfa-cli/src/test/java/hu/bme/mit/theta/xcfa/cli/XcfaCliWitnessTest.kt diff --git a/subprojects/cfa/cfa-analysis/src/test/java/hu/bme/mit/theta/cfa/analysis/impact/CfaPredImpactCheckerTest.java b/subprojects/cfa/cfa-analysis/src/test/java/hu/bme/mit/theta/cfa/analysis/impact/CfaPredImpactCheckerTest.java index 4204a3785d..111600967f 100644 --- a/subprojects/cfa/cfa-analysis/src/test/java/hu/bme/mit/theta/cfa/analysis/impact/CfaPredImpactCheckerTest.java +++ b/subprojects/cfa/cfa-analysis/src/test/java/hu/bme/mit/theta/cfa/analysis/impact/CfaPredImpactCheckerTest.java @@ -17,60 +17,65 @@ import static org.junit.Assert.assertTrue; -import java.io.FileInputStream; -import java.io.FileNotFoundException; -import java.io.IOException; - import hu.bme.mit.theta.analysis.Trace; import hu.bme.mit.theta.analysis.algorithm.SafetyResult; -import hu.bme.mit.theta.analysis.pred.PredState; -import hu.bme.mit.theta.cfa.analysis.CfaAction; -import hu.bme.mit.theta.cfa.analysis.CfaState; -import hu.bme.mit.theta.solver.Solver; -import org.junit.Test; - import hu.bme.mit.theta.analysis.algorithm.arg.ARG; import hu.bme.mit.theta.analysis.algorithm.arg.ArgChecker; import hu.bme.mit.theta.analysis.expr.ExprAction; import hu.bme.mit.theta.analysis.expr.ExprState; +import hu.bme.mit.theta.analysis.pred.PredState; import hu.bme.mit.theta.analysis.unit.UnitPrec; import hu.bme.mit.theta.analysis.utils.ArgVisualizer; import hu.bme.mit.theta.cfa.CFA; +import hu.bme.mit.theta.cfa.analysis.CfaAction; +import hu.bme.mit.theta.cfa.analysis.CfaState; import hu.bme.mit.theta.cfa.analysis.lts.CfaLbeLts; import hu.bme.mit.theta.cfa.dsl.CfaDslManager; import hu.bme.mit.theta.common.visualization.writer.GraphvizWriter; import hu.bme.mit.theta.solver.ItpSolver; +import hu.bme.mit.theta.solver.Solver; import hu.bme.mit.theta.solver.z3legacy.Z3LegacySolverFactory; +import java.io.FileInputStream; +import java.io.FileNotFoundException; +import java.io.IOException; +import org.junit.Test; public final class CfaPredImpactCheckerTest { @Test public void test() throws FileNotFoundException, IOException { // Arrange - final CFA cfa = CfaDslManager.createCfa( - new FileInputStream("src/test/resources/counter5_true.cfa")); + final CFA cfa = + CfaDslManager.createCfa( + new FileInputStream("src/test/resources/counter5_true.cfa")); final Solver abstractionSolver = Z3LegacySolverFactory.getInstance().createSolver(); final ItpSolver refinementSolver = Z3LegacySolverFactory.getInstance().createItpSolver(); - final PredImpactChecker checker = PredImpactChecker.create( - CfaLbeLts.of(cfa.getErrorLoc().get()), cfa.getInitLoc(), - l -> l.equals(cfa.getErrorLoc().get()), abstractionSolver, refinementSolver); + final PredImpactChecker checker = + PredImpactChecker.create( + CfaLbeLts.of(cfa.getErrorLoc().get()), + cfa.getInitLoc(), + l -> l.equals(cfa.getErrorLoc().get()), + abstractionSolver, + refinementSolver); // Act - final SafetyResult, CfaAction>, Trace, CfaAction>> status = checker.check( - UnitPrec.getInstance()); + final SafetyResult< + ARG, CfaAction>, Trace, CfaAction>> + status = checker.check(UnitPrec.getInstance()); // Assert assertTrue(status.isSafe()); - final ARG arg = status.getWitness(); + final ARG arg = status.getProof(); arg.minimize(); final ArgChecker argChecker = ArgChecker.create(abstractionSolver); assertTrue(argChecker.isWellLabeled(arg)); System.out.println( - GraphvizWriter.getInstance().writeString(ArgVisualizer.getDefault().visualize(arg))); + GraphvizWriter.getInstance() + .writeString(ArgVisualizer.getDefault().visualize(arg))); } -} \ No newline at end of file +} 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 024911743e..eda6c15702 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 @@ -15,6 +15,8 @@ */ package hu.bme.mit.theta.cfa.cli; +import static com.google.common.base.Preconditions.checkNotNull; + import com.beust.jcommander.JCommander; import com.beust.jcommander.Parameter; import com.beust.jcommander.ParameterException; @@ -27,8 +29,6 @@ import hu.bme.mit.theta.analysis.algorithm.bounded.MonolithicExpr; import hu.bme.mit.theta.analysis.algorithm.cegar.CegarStatistics; import hu.bme.mit.theta.analysis.expl.ExplState; -import hu.bme.mit.theta.analysis.expr.ExprAction; -import hu.bme.mit.theta.analysis.expr.ExprState; import hu.bme.mit.theta.analysis.expr.refinement.PruneStrategy; import hu.bme.mit.theta.cfa.CFA; import hu.bme.mit.theta.cfa.analysis.CfaAction; @@ -37,14 +37,7 @@ import hu.bme.mit.theta.cfa.analysis.CfaTraceConcretizer; import hu.bme.mit.theta.cfa.analysis.config.CfaConfig; import hu.bme.mit.theta.cfa.analysis.config.CfaConfigBuilder; -import hu.bme.mit.theta.cfa.analysis.config.CfaConfigBuilder.Algorithm; -import hu.bme.mit.theta.cfa.analysis.config.CfaConfigBuilder.Domain; -import hu.bme.mit.theta.cfa.analysis.config.CfaConfigBuilder.Encoding; -import hu.bme.mit.theta.cfa.analysis.config.CfaConfigBuilder.InitPrec; -import hu.bme.mit.theta.cfa.analysis.config.CfaConfigBuilder.PrecGranularity; -import hu.bme.mit.theta.cfa.analysis.config.CfaConfigBuilder.PredSplit; -import hu.bme.mit.theta.cfa.analysis.config.CfaConfigBuilder.Refinement; -import hu.bme.mit.theta.cfa.analysis.config.CfaConfigBuilder.Search; +import hu.bme.mit.theta.cfa.analysis.config.CfaConfigBuilder.*; import hu.bme.mit.theta.cfa.analysis.utils.CfaVisualizer; import hu.bme.mit.theta.cfa.dsl.CfaDslManager; import hu.bme.mit.theta.common.CliUtils; @@ -62,28 +55,21 @@ import hu.bme.mit.theta.solver.smtlib.SmtLibSolverManager; import hu.bme.mit.theta.solver.z3legacy.Z3LegacySolverFactory; import hu.bme.mit.theta.solver.z3legacy.Z3SolverManager; - -import java.io.File; -import java.io.FileInputStream; -import java.io.FileNotFoundException; -import java.io.InputStream; -import java.io.PrintWriter; -import java.io.StringWriter; +import java.io.*; import java.nio.file.Path; import java.util.concurrent.TimeUnit; import java.util.stream.Stream; -import static com.google.common.base.Preconditions.checkNotNull; - -/** - * A command line interface for running a CEGAR configuration on a CFA. - */ +/** A command line interface for running a CEGAR configuration on a CFA. */ public class CfaCli { private static final String JAR_NAME = "theta-cfa-cli.jar"; private final String[] args; private final TableWriter writer; - @Parameter(names = {"--algorithm"}, description = "Algorithm") + + @Parameter( + names = {"--algorithm"}, + description = "Algorithm") Algorithm algorithm = Algorithm.CEGAR; @Parameter(names = "--domain", description = "Abstract domain") @@ -95,16 +81,34 @@ public class CfaCli { @Parameter(names = "--search", description = "Search strategy") Search search = Search.BFS; - @Parameter(names = "--predsplit", description = "Predicate splitting (for predicate abstraction)") + @Parameter( + names = "--predsplit", + description = "Predicate splitting (for predicate abstraction)") PredSplit predSplit = PredSplit.WHOLE; - @Parameter(names = "--solver", description = "Sets the underlying SMT solver to use for both the abstraction and the refinement process. Enter in format :, see theta-smtlib-cli.jar for more details. Enter \"Z3\" to use the legacy z3 solver.") + @Parameter( + names = "--solver", + description = + "Sets the underlying SMT solver to use for both the abstraction and the" + + " refinement process. Enter in format :, see" + + " theta-smtlib-cli.jar for more details. Enter \"Z3\" to use the legacy" + + " z3 solver.") String solver = "Z3"; - @Parameter(names = "--abstraction-solver", description = "Sets the underlying SMT solver to use for the abstraction process. Enter in format :, see theta-smtlib-cli.jar for more details. Enter \"Z3\" to use the legacy z3 solver.") + @Parameter( + names = "--abstraction-solver", + description = + "Sets the underlying SMT solver to use for the abstraction process. Enter in" + + " format :, see theta-smtlib-cli.jar for" + + " more details. Enter \"Z3\" to use the legacy z3 solver.") String abstractionSolver; - @Parameter(names = "--refinement-solver", description = "Sets the underlying SMT solver to use for the refinement process. Enter in format :, see theta-smtlib-cli.jar for more details. Enter \"Z3\" to use the legacy z3 solver.") + @Parameter( + names = "--refinement-solver", + description = + "Sets the underlying SMT solver to use for the refinement process. Enter in" + + " format :, see theta-smtlib-cli.jar for" + + " more details. Enter \"Z3\" to use the legacy z3 solver.") String refinementSolver; @Parameter(names = "--home", description = "The path of the solver registry") @@ -122,13 +126,17 @@ public class CfaCli { @Parameter(names = "--encoding", description = "Block encoding") Encoding encoding = Encoding.LBE; - @Parameter(names = "--maxenum", description = "Maximal number of explicitly enumerated successors (0: unlimited)") + @Parameter( + names = "--maxenum", + description = "Maximal number of explicitly enumerated successors (0: unlimited)") Integer maxEnum = 10; @Parameter(names = "--initprec", description = "Initial precision of abstraction") InitPrec initPrec = InitPrec.EMPTY; - @Parameter(names = "--prunestrategy", description = "Strategy for pruning the ARG after refinement") + @Parameter( + names = "--prunestrategy", + description = "Strategy for pruning the ARG after refinement") PruneStrategy pruneStrategy = PruneStrategy.LAZY; @Parameter(names = "--loglevel", description = "Detailedness of logging") @@ -140,13 +148,20 @@ public class CfaCli { @Parameter(names = "--cex", description = "Write concrete counterexample to a file") String cexfile = null; - @Parameter(names = "--header", description = "Print only a header (for benchmarks)", help = true) + @Parameter( + names = "--header", + description = "Print only a header (for benchmarks)", + help = true) boolean headerOnly = false; - @Parameter(names = "--visualize", description = "Visualize CFA to this file without running the algorithm") + @Parameter( + names = "--visualize", + description = "Visualize CFA to this file without running the algorithm") String visualize = null; - @Parameter(names = "--metrics", description = "Print metrics about the CFA without running the algorithm") + @Parameter( + names = "--metrics", + description = "Print metrics about the CFA without running the algorithm") boolean metrics = false; @Parameter(names = "--stacktrace", description = "Print full stack trace in case of exception") @@ -241,13 +256,19 @@ private void run() { final SafetyResult> status; if (algorithm == Algorithm.CEGAR) { - final CfaConfig configuration = buildConfiguration(cfa, errLoc, abstractionSolverFactory, refinementSolverFactory); + final CfaConfig configuration = + buildConfiguration( + cfa, errLoc, abstractionSolverFactory, refinementSolverFactory); status = check(configuration); - } else if (algorithm == Algorithm.BMC || algorithm == Algorithm.KINDUCTION || algorithm == Algorithm.IMC) { - final BoundedChecker checker = buildBoundedChecker(cfa, abstractionSolverFactory); + } else if (algorithm == Algorithm.BMC + || algorithm == Algorithm.KINDUCTION + || algorithm == Algorithm.IMC) { + final BoundedChecker checker = + buildBoundedChecker(cfa, abstractionSolverFactory); status = checker.check(null); } else { - throw new UnsupportedOperationException("Algorithm " + algorithm + " not supported"); + throw new UnsupportedOperationException( + "Algorithm " + algorithm + " not supported"); } sw.stop(); @@ -262,8 +283,18 @@ private void run() { } private void printHeader() { - Stream.of("Result", "TimeMs", "AlgoTimeMs", "AbsTimeMs", "RefTimeMs", "Iterations", - "ArgSize", "ArgDepth", "ArgMeanBranchFactor", "CexLen").forEach(writer::cell); + Stream.of( + "Result", + "TimeMs", + "AlgoTimeMs", + "AbsTimeMs", + "RefTimeMs", + "Iterations", + "ArgSize", + "ArgDepth", + "ArgMeanBranchFactor", + "CexLen") + .forEach(writer::cell); writer.newRow(); } @@ -277,67 +308,89 @@ private CFA loadModel() throws Exception { } } - private CfaConfig buildConfiguration(final CFA cfa, final CFA.Loc errLoc, - final SolverFactory abstractionSolverFactory, final SolverFactory refinementSolverFactory) + private CfaConfig buildConfiguration( + final CFA cfa, + final CFA.Loc errLoc, + final SolverFactory abstractionSolverFactory, + final SolverFactory refinementSolverFactory) throws Exception { try { - return new CfaConfigBuilder(domain, refinement, abstractionSolverFactory, - refinementSolverFactory) - .precGranularity(precGranularity).search(search) - .predSplit(predSplit).encoding(encoding).maxEnum(maxEnum).initPrec(initPrec) - .pruneStrategy(pruneStrategy).logger(logger).build(cfa, errLoc); + return new CfaConfigBuilder( + domain, refinement, abstractionSolverFactory, refinementSolverFactory) + .precGranularity(precGranularity) + .search(search) + .predSplit(predSplit) + .encoding(encoding) + .maxEnum(maxEnum) + .initPrec(initPrec) + .pruneStrategy(pruneStrategy) + .logger(logger) + .build(cfa, errLoc); } catch (final Exception ex) { throw new Exception("Could not create configuration: " + ex.getMessage(), ex); } } - private BoundedChecker buildBoundedChecker(final CFA cfa, final SolverFactory abstractionSolverFactory) { + private BoundedChecker buildBoundedChecker( + final CFA cfa, final SolverFactory abstractionSolverFactory) { final MonolithicExpr monolithicExpr = CfaToMonolithicExprKt.toMonolithicExpr(cfa); final BoundedChecker checker; switch (algorithm) { - case BMC -> checker = BoundedCheckerBuilderKt.buildBMC( - monolithicExpr, - abstractionSolverFactory.createSolver(), - val -> CfaToMonolithicExprKt.valToState(cfa, val), - (val1, val2) -> CfaToMonolithicExprKt.valToAction(cfa, val1, val2), - logger - ); - case KINDUCTION -> checker = BoundedCheckerBuilderKt.buildKIND( - monolithicExpr, - abstractionSolverFactory.createSolver(), - abstractionSolverFactory.createSolver(), - val -> CfaToMonolithicExprKt.valToState(cfa, val), - (val1, val2) -> CfaToMonolithicExprKt.valToAction(cfa, val1, val2), - logger - ); - case IMC -> checker = BoundedCheckerBuilderKt.buildIMC( - monolithicExpr, - abstractionSolverFactory.createSolver(), - abstractionSolverFactory.createItpSolver(), - val -> CfaToMonolithicExprKt.valToState(cfa, val), - (val1, val2) -> CfaToMonolithicExprKt.valToAction(cfa, val1, val2), - logger - ); + case BMC -> + checker = + BoundedCheckerBuilderKt.buildBMC( + monolithicExpr, + abstractionSolverFactory.createSolver(), + val -> CfaToMonolithicExprKt.valToState(cfa, val), + (val1, val2) -> + CfaToMonolithicExprKt.valToAction(cfa, val1, val2), + logger); + case KINDUCTION -> + checker = + BoundedCheckerBuilderKt.buildKIND( + monolithicExpr, + abstractionSolverFactory.createSolver(), + abstractionSolverFactory.createSolver(), + val -> CfaToMonolithicExprKt.valToState(cfa, val), + (val1, val2) -> + CfaToMonolithicExprKt.valToAction(cfa, val1, val2), + logger); + case IMC -> + checker = + BoundedCheckerBuilderKt.buildIMC( + monolithicExpr, + abstractionSolverFactory.createSolver(), + abstractionSolverFactory.createItpSolver(), + val -> CfaToMonolithicExprKt.valToState(cfa, val), + (val1, val2) -> + CfaToMonolithicExprKt.valToAction(cfa, val1, val2), + logger); default -> - throw new UnsupportedOperationException("Algorithm " + algorithm + " not supported"); + throw new UnsupportedOperationException( + "Algorithm " + algorithm + " not supported"); } return checker; } - private SafetyResult, ? extends Trace> check(CfaConfig configuration) throws Exception { + private SafetyResult, ? extends Trace> check( + CfaConfig configuration) throws Exception { try { return configuration.check(); } catch (final Exception ex) { String message = ex.getMessage() == null ? "(no message)" : ex.getMessage(); throw new Exception( - "Error while running algorithm: " + ex.getClass().getSimpleName() + " " + message, + "Error while running algorithm: " + + ex.getClass().getSimpleName() + + " " + + message, ex); } } - private void printResult(final SafetyResult> status, final long totalTimeMs) { - final CegarStatistics stats = (CegarStatistics) - status.getStats().orElse(new CegarStatistics(0, 0, 0, 0)); + private void printResult( + final SafetyResult> status, final long totalTimeMs) { + final CegarStatistics stats = + (CegarStatistics) status.getStats().orElse(new CegarStatistics(0, 0, 0, 0)); if (benchmarkMode) { writer.cell(status.isSafe()); writer.cell(totalTimeMs); @@ -345,7 +398,7 @@ private void printResult(final SafetyResult> status, fi writer.cell(stats.getAbstractorTimeMs()); writer.cell(stats.getRefinerTimeMs()); writer.cell(stats.getIterations()); - if (status.getWitness() instanceof ARG arg) { + if (status.getProof() instanceof ARG arg) { writer.cell(arg.size()); writer.cell(arg.getDepth()); writer.cell(arg.getMeanBranchingFactor()); @@ -369,7 +422,10 @@ private void printError(final Throwable ex) { writer.cell("[EX] " + ex.getClass().getSimpleName() + ": " + message); writer.newRow(); } else { - logger.write(Level.RESULT, "%s occurred, message: %s%n", ex.getClass().getSimpleName(), + logger.write( + Level.RESULT, + "%s occurred, message: %s%n", + ex.getClass().getSimpleName(), message); if (stacktrace) { final StringWriter errors = new StringWriter(); @@ -382,9 +438,10 @@ private void printError(final Throwable ex) { } private void writeCex(final SafetyResult.Unsafe status) throws FileNotFoundException { - @SuppressWarnings("unchecked") final Trace, CfaAction> trace = (Trace, CfaAction>) status.getCex(); - final Trace, CfaAction> concrTrace = CfaTraceConcretizer.concretize( - trace, Z3LegacySolverFactory.getInstance()); + @SuppressWarnings("unchecked") + final Trace, CfaAction> trace = (Trace, CfaAction>) status.getCex(); + final Trace, CfaAction> concrTrace = + CfaTraceConcretizer.concretize(trace, Z3LegacySolverFactory.getInstance()); final File file = new File(cexfile); PrintWriter printWriter = null; try { diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/Checker.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/Checker.java index e1a86bee69..afed36eab9 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/Checker.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/Checker.java @@ -15,8 +15,7 @@ */ package hu.bme.mit.theta.analysis.algorithm; -public interface Checker { - - Result check(I input); +public interface Checker { + Result check(I input); } diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/EmptyWitness.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/EmptyProof.java similarity index 78% rename from subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/EmptyWitness.java rename to subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/EmptyProof.java index 49794dd84e..1c8d976149 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/EmptyWitness.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/EmptyProof.java @@ -15,15 +15,13 @@ */ package hu.bme.mit.theta.analysis.algorithm; -public class EmptyWitness implements Witness { +public class EmptyProof implements Proof { - private final static EmptyWitness empty = new EmptyWitness(); + private static final EmptyProof empty = new EmptyProof(); - private EmptyWitness() { - } + private EmptyProof() {} - public static EmptyWitness getInstance() { + public static EmptyProof getInstance() { return empty; } - } diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/Witness.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/Proof.java similarity index 95% rename from subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/Witness.java rename to subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/Proof.java index ff6157e1e3..3668ab6315 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/Witness.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/Proof.java @@ -15,5 +15,4 @@ */ package hu.bme.mit.theta.analysis.algorithm; -public interface Witness { -} +public interface Proof {} diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/Result.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/Result.java index 0c81bf5836..438edde295 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/Result.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/Result.java @@ -17,10 +17,9 @@ import java.util.Optional; -public interface Result { +public interface Result { - W getWitness(); + Pr getProof(); Optional getStats(); - } diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/SafetyChecker.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/SafetyChecker.java index 4f13fac64c..c716c1dc24 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/SafetyChecker.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/SafetyChecker.java @@ -15,19 +15,15 @@ */ package hu.bme.mit.theta.analysis.algorithm; -import hu.bme.mit.theta.analysis.*; -import hu.bme.mit.theta.analysis.algorithm.Checker; -import hu.bme.mit.theta.analysis.algorithm.SafetyResult; -import hu.bme.mit.theta.analysis.algorithm.arg.ARG; +import hu.bme.mit.theta.analysis.Cex; @FunctionalInterface -public interface SafetyChecker extends Checker { +public interface SafetyChecker extends Checker { @Override - SafetyResult check(final I input); + SafetyResult check(final I input); - default SafetyResult check() { + default SafetyResult check() { return check(null); } - } 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 dfd812ebea..0862dc3079 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 @@ -15,30 +15,29 @@ */ package hu.bme.mit.theta.analysis.algorithm; +import static com.google.common.base.Preconditions.checkNotNull; + import hu.bme.mit.theta.analysis.Cex; import hu.bme.mit.theta.common.Utils; - import java.util.Optional; -import static com.google.common.base.Preconditions.checkNotNull; - -public abstract class SafetyResult implements Result { - private final W witness; +public abstract class SafetyResult implements Result { + private final Pr proof; private final Optional stats; - private SafetyResult(final W witness, final Optional stats) { - this.witness = checkNotNull(witness); + private SafetyResult(final Pr proof, final Optional stats) { + this.proof = checkNotNull(proof); this.stats = checkNotNull(stats); } private SafetyResult() { - this.witness = null; + this.proof = null; this.stats = Optional.empty(); } @Override - public W getWitness() { - return witness; + public Pr getProof() { + return proof; } @Override @@ -46,28 +45,30 @@ public Optional getStats() { return stats; } - public static Safe safe(final W witness) { + public static Safe safe(final Pr witness) { return new Safe<>(witness, Optional.empty()); } - public static Unsafe unsafe(final C cex, final W witness) { + public static Unsafe unsafe( + final C cex, final Pr witness) { return new Unsafe<>(cex, witness, Optional.empty()); } - public static Unknown unknown() { + public static Unknown unknown() { return new Unknown<>(); } - public static Safe safe(final W witness, final Statistics stats) { + public static Safe safe( + final Pr witness, final Statistics stats) { return new Safe<>(witness, Optional.of(stats)); } - public static Unsafe unsafe(final C cex, final W witness, - final Statistics stats) { + public static Unsafe unsafe( + final C cex, final Pr witness, final Statistics stats) { return new Unsafe<>(cex, witness, Optional.of(stats)); } - public static Unknown unknown(final Statistics stats) { + public static Unknown unknown(final Statistics stats) { return new Unknown<>(Optional.of(stats)); } @@ -75,15 +76,15 @@ public static Unknown unknown(final Sta public abstract boolean isUnsafe(); - public abstract Safe asSafe(); + public abstract Safe asSafe(); - public abstract Unsafe asUnsafe(); + public abstract Unsafe asUnsafe(); //// - public static final class Safe extends SafetyResult { - private Safe(final W witness, final Optional stats) { - super(witness, stats); + public static final class Safe extends SafetyResult { + private Safe(final Pr proof, final Optional stats) { + super(proof, stats); } @Override @@ -97,28 +98,32 @@ public boolean isUnsafe() { } @Override - public Safe asSafe() { + public Safe asSafe() { return this; } @Override - public Unsafe asUnsafe() { + public Unsafe asUnsafe() { throw new ClassCastException( - "Cannot cast " + Safe.class.getSimpleName() + " to " + Unsafe.class.getSimpleName()); + "Cannot cast " + + Safe.class.getSimpleName() + + " to " + + Unsafe.class.getSimpleName()); } @Override public String toString() { - return Utils.lispStringBuilder(SafetyResult.class.getSimpleName()).add(Safe.class.getSimpleName()) + return Utils.lispStringBuilder(SafetyResult.class.getSimpleName()) + .add(Safe.class.getSimpleName()) .toString(); } } - public static final class Unsafe extends SafetyResult { + public static final class Unsafe extends SafetyResult { private final C cex; - private Unsafe(final C cex, final W witness, final Optional stats) { - super(witness, stats); + private Unsafe(final C cex, final Pr proof, final Optional stats) { + super(proof, stats); this.cex = checkNotNull(cex); } @@ -137,24 +142,29 @@ public boolean isUnsafe() { } @Override - public Safe asSafe() { + public Safe asSafe() { throw new ClassCastException( - "Cannot cast " + Unsafe.class.getSimpleName() + " to " + Safe.class.getSimpleName()); + "Cannot cast " + + Unsafe.class.getSimpleName() + + " to " + + Safe.class.getSimpleName()); } @Override - public Unsafe asUnsafe() { + public Unsafe asUnsafe() { return this; } @Override public String toString() { - return Utils.lispStringBuilder(SafetyResult.class.getSimpleName()).add(Unsafe.class.getSimpleName()) - .add("Trace length: " + cex.length()).toString(); + return Utils.lispStringBuilder(SafetyResult.class.getSimpleName()) + .add(Unsafe.class.getSimpleName()) + .add("Trace length: " + cex.length()) + .toString(); } } - public static final class Unknown extends SafetyResult { + public static final class Unknown extends SafetyResult { public Unknown() { super(); @@ -175,12 +185,12 @@ public boolean isUnsafe() { } @Override - public Safe asSafe() { + public Safe asSafe() { return null; } @Override - public Unsafe asUnsafe() { + public Unsafe asUnsafe() { return null; } @@ -191,5 +201,4 @@ public String toString() { .toString(); } } - } diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/arg/ARG.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/arg/ARG.java index b43fb37e35..9f2b3c3ae0 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/arg/ARG.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/arg/ARG.java @@ -15,28 +15,22 @@ */ package hu.bme.mit.theta.analysis.algorithm.arg; +import static com.google.common.base.Preconditions.*; +import static java.util.stream.Collectors.toList; + import hu.bme.mit.theta.analysis.Action; import hu.bme.mit.theta.analysis.PartialOrd; import hu.bme.mit.theta.analysis.State; -import hu.bme.mit.theta.analysis.algorithm.Witness; +import hu.bme.mit.theta.analysis.algorithm.Proof; import hu.bme.mit.theta.analysis.algorithm.arg.debug.ARGWebDebugger; import hu.bme.mit.theta.common.container.Containers; - import java.util.Collection; import java.util.Optional; import java.util.OptionalInt; import java.util.stream.Stream; -import static com.google.common.base.Preconditions.checkArgument; -import static com.google.common.base.Preconditions.checkNotNull; -import static com.google.common.base.Preconditions.checkState; -import static java.util.stream.Collectors.toList; - -/** - * Represents an abstract reachability graph (ARG). See the related class - * ArgBuilder. - */ -public final class ARG implements Witness { +/** Represents an abstract reachability graph (ARG). See the related class ArgBuilder. */ +public final class ARG implements Proof { private final Collection> initNodes; public boolean initialized; // Set by ArgBuilder @@ -49,7 +43,8 @@ private ARG(final PartialOrd partialOrd) { this.initialized = false; } - public static ARG create(final PartialOrd partialOrd) { + public static ARG create( + final PartialOrd partialOrd) { return new ARG<>(partialOrd); } @@ -75,7 +70,6 @@ public Stream> getIncompleteNodes() { return getInitNodes().flatMap(ArgNode::unexcludedDescendants).filter(n -> !n.isExpanded()); } - PartialOrd getPartialOrd() { return partialOrd; } @@ -83,24 +77,19 @@ PartialOrd getPartialOrd() { //// /** - * Checks if the ARG is complete, i.e., whether it is initialized and all of - * its nodes are complete. + * Checks if the ARG is complete, i.e., whether it is initialized and all of its nodes are + * complete. */ public boolean isComplete() { return isInitialized() && getNodes().allMatch(ArgNode::isComplete); } - /** - * Checks if the ARG is safe, i.e., whether all of its nodes are safe. - */ + /** Checks if the ARG is safe, i.e., whether all of its nodes are safe. */ public boolean isSafe() { return getNodes().allMatch(ArgNode::isSafe); } - /** - * Checks if the ARG is initialized, i.e., all of its initial nodes are - * present. - */ + /** Checks if the ARG is initialized, i.e., all of its initial nodes are present. */ public boolean isInitialized() { return initialized; } @@ -115,8 +104,8 @@ public ArgNode createInitNode(final S initState, final boolean target) { return initNode; } - public ArgNode createSuccNode(final ArgNode node, final A action, final S succState, - final boolean target) { + public ArgNode createSuccNode( + final ArgNode node, final A action, final S succState, final boolean target) { checkNotNull(node); checkNotNull(action); checkNotNull(succState); @@ -133,7 +122,8 @@ private ArgNode createNode(final S state, final int depth, final boolean t return node; } - private ArgEdge createEdge(final ArgNode source, final A action, final ArgNode target) { + private ArgEdge createEdge( + final ArgNode source, final A action, final ArgNode target) { final ArgEdge edge = new ArgEdge<>(source, action, target); source.outEdges.add(edge); target.inEdge = Optional.of(edge); @@ -141,9 +131,7 @@ private ArgEdge createEdge(final ArgNode source, final A action, fin return edge; } - /** - * Removes a node along with its subtree. - */ + /** Removes a node along with its subtree. */ public void prune(final ArgNode node) { checkNotNull(node); checkArgument(node.arg == this, "Node does not belong to this ARG"); @@ -162,17 +150,13 @@ public void prune(final ArgNode node) { node.descendants().forEach(ArgNode::clearCoveredNodes); } - /** - * Prune the whole ARG, making it uninitialized. - */ + /** Prune the whole ARG, making it uninitialized. */ public void pruneAll() { initNodes.clear(); this.initialized = false; } - /** - * Marks the node for reexpanding without pruning it. - */ + /** Marks the node for reexpanding without pruning it. */ public void markForReExpansion(final ArgNode node) { node.expanded = false; } @@ -192,24 +176,19 @@ private void minimizeSubTree(final ArgNode node) { //// - /** - * Gets all counterexamples, i.e., traces leading to target nodes. - */ + /** Gets all counterexamples, i.e., traces leading to target nodes. */ public Stream> getCexs() { return getUnsafeNodes().map(ArgTrace::to); } - /** - * Gets the size of the ARG, i.e., the number of nodes. - */ + /** Gets the size of the ARG, i.e., the number of nodes. */ public long size() { return getNodes().count(); } /** - * Gets the depth of the ARG, i.e., the maximal depth of its nodes. Depth - * starts (at the initial nodes) from 0. Depth is undefined for an empty - * ARG. + * Gets the depth of the ARG, i.e., the maximal depth of its nodes. Depth starts (at the initial + * nodes) from 0. Depth is undefined for an empty ARG. */ public int getDepth() { final OptionalInt maxOpt = getNodes().mapToInt(ArgNode::getDepth).max(); @@ -217,12 +196,11 @@ public int getDepth() { return maxOpt.getAsInt(); } - /** - * Gets the mean branching factor of the expanded nodes. - */ + /** Gets the mean branching factor of the expanded nodes. */ public double getMeanBranchingFactor() { final Stream> nodesToCalculate = getNodes().filter(ArgNode::isExpanded); - final double mean = nodesToCalculate.mapToDouble(n -> n.getOutEdges().count()).average().orElse(0); + final double mean = + nodesToCalculate.mapToDouble(n -> n.getOutEdges().count()).average().orElse(0); return mean; } } 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 72b90fe53f..2c1273f87f 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 @@ -13,11 +13,10 @@ * See the License for the specific language governing permissions and * limitations under the License. */ - package hu.bme.mit.theta.analysis.algorithm.bounded import hu.bme.mit.theta.analysis.Trace -import hu.bme.mit.theta.analysis.algorithm.EmptyWitness +import hu.bme.mit.theta.analysis.algorithm.EmptyProof import hu.bme.mit.theta.analysis.algorithm.SafetyChecker import hu.bme.mit.theta.analysis.algorithm.SafetyResult import hu.bme.mit.theta.analysis.expr.ExprAction @@ -43,228 +42,246 @@ import java.util.* * @param The state type, must inherit from ExprState. * @param The action type, must inherit from StmtAction. * @param monolithicExpr The monolithic expression to be checked - * @param shouldGiveUp A function determining whether to give up checking based on a given iteration count. Use this - * to implement custom timeout or thread interruption checking subroutines. + * @param shouldGiveUp A function determining whether to give up checking based on a given iteration + * count. Use this to implement custom timeout or thread interruption checking subroutines. * @param bmcSolver The solver for bounded model checking. - * @param bmcEnabled A function determining whether bounded model checking is enabled. Cannot be disabled per-iteration. - * Use the capabilities of the lambda parameter to decide on enabledness based on external factors, - * such as available memory or time limit remaining. + * @param bmcEnabled A function determining whether bounded model checking is enabled. Cannot be + * disabled per-iteration. Use the capabilities of the lambda parameter to decide on enabledness + * based on external factors, such as available memory or time limit remaining. * @param lfPathOnly A function determining whether to consider only loop-free paths. * @param itpSolver The solver for interpolation, used in IMC. * @param imcEnabled A function determining whether IMC is enabled. Can be different per-iteration. * @param indSolver The solver for induction checking in KIND. * @param kindEnabled A function determining whether k-induction (KIND) is enabled. - * @param valToState A function mapping valuations to expression states, used to construct a counterexample. - * @param biValToAction A function mapping pairs of valuations to statements, used to construct a counterexample. + * @param valToState A function mapping valuations to expression states, used to construct a + * counterexample. + * @param biValToAction A function mapping pairs of valuations to statements, used to construct a + * counterexample. * @param logger The logger for logging. */ -class BoundedChecker @JvmOverloads constructor( - private val monolithicExpr: MonolithicExpr, - private val shouldGiveUp: (Int) -> Boolean = { false }, - private val bmcSolver: Solver? = null, - 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 indSolver: Solver? = null, - private val kindEnabled: (Int) -> Boolean = { indSolver != null }, - private val valToState: (Valuation) -> S, - private val biValToAction: (Valuation, Valuation) -> A, - private val logger: Logger, -) : SafetyChecker, UnitPrec> { - - private val vars = monolithicExpr.vars() - private val unfoldedInitExpr = PathUtils.unfold(monolithicExpr.initExpr, VarIndexingFactory.indexing(0)) - private val unfoldedPropExpr = { i: VarIndexing -> PathUtils.unfold(monolithicExpr.propExpr, i) } - private val indices = mutableListOf(monolithicExpr.initOffsetIndex) - private val exprs = mutableListOf>() - private var kindLastIterLookup = 0 - private var iteration = 0 - - init { - 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!" } - } - - override fun check(prec: UnitPrec?): SafetyResult> { - - iteration = 0 - - val isBmcEnabled = bmcEnabled() // we don't allow per-iteration setting of bmc enabledness - bmcSolver?.add(unfoldedInitExpr) - - while (!shouldGiveUp(iteration)) { - iteration++ - logger.write(Logger.Level.MAINSTEP, "Starting iteration $iteration\n") - - exprs.add(PathUtils.unfold(monolithicExpr.transExpr, indices.last())) - - indices.add(indices.last().add(monolithicExpr.transOffsetIndex)) - - if (isBmcEnabled) { - bmc()?.let { return it } - } +class BoundedChecker +@JvmOverloads +constructor( + private val monolithicExpr: MonolithicExpr, + private val shouldGiveUp: (Int) -> Boolean = { false }, + private val bmcSolver: Solver? = null, + 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 indSolver: Solver? = null, + private val kindEnabled: (Int) -> Boolean = { indSolver != null }, + private val valToState: (Valuation) -> S, + private val biValToAction: (Valuation, Valuation) -> A, + private val logger: Logger, +) : SafetyChecker, UnitPrec> { + + private val vars = monolithicExpr.vars() + private val unfoldedInitExpr = + PathUtils.unfold(monolithicExpr.initExpr, VarIndexingFactory.indexing(0)) + private val unfoldedPropExpr = { i: VarIndexing -> PathUtils.unfold(monolithicExpr.propExpr, i) } + private val indices = mutableListOf(monolithicExpr.initOffsetIndex) + private val exprs = mutableListOf>() + private var kindLastIterLookup = 0 + private var iteration = 0 + + init { + 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!" } + } + + override fun check(prec: UnitPrec?): SafetyResult> { + + iteration = 0 + + val isBmcEnabled = bmcEnabled() // we don't allow per-iteration setting of bmc enabledness + bmcSolver?.add(unfoldedInitExpr) + + while (!shouldGiveUp(iteration)) { + iteration++ + logger.write(Logger.Level.MAINSTEP, "Starting iteration $iteration\n") + + exprs.add(PathUtils.unfold(monolithicExpr.transExpr, indices.last())) + + indices.add(indices.last().add(monolithicExpr.transOffsetIndex)) + + if (isBmcEnabled) { + bmc()?.let { + return it + } + } - if (kindEnabled(iteration)) { - if (!isBmcEnabled) { - error("Bad configuration: induction check should always be preceded by a BMC/SAT check") - } - kind()?.let { return it } - kindLastIterLookup = iteration - } + if (kindEnabled(iteration)) { + if (!isBmcEnabled) { + error("Bad configuration: induction check should always be preceded by a BMC/SAT check") + } + kind()?.let { + return it + } + kindLastIterLookup = iteration + } - if (imcEnabled(iteration)) { - itp()?.let { return it } - } + if (imcEnabled(iteration)) { + itp()?.let { + return it } - return SafetyResult.unknown(BoundedStatistics(iteration)) + } } - - private fun bmc(): SafetyResult>? { - val bmcSolver = this.bmcSolver!! - logger.write(Logger.Level.MAINSTEP, "\tStarting BMC\n") - - bmcSolver.add(exprs.last()) - - if (lfPathOnly()) { // indices contains currIndex as last() - for (indexing in indices) { - if (indexing != indices.last()) { - val allVarsSame = And(vars.map { - Eq(PathUtils.unfold(it.ref, indexing), PathUtils.unfold(it.ref, indices.last())) - }) - bmcSolver.add(Not(allVarsSame)) - } - } - - if (bmcSolver.check().isUnsat) { - logger.write(Logger.Level.MAINSTEP, "Safety proven in BMC step\n") - return SafetyResult.safe(EmptyWitness.getInstance(), BoundedStatistics(iteration)) - } + return SafetyResult.unknown(BoundedStatistics(iteration)) + } + + private fun bmc(): SafetyResult>? { + val bmcSolver = this.bmcSolver!! + logger.write(Logger.Level.MAINSTEP, "\tStarting BMC\n") + + bmcSolver.add(exprs.last()) + + if (lfPathOnly()) { // indices contains currIndex as last() + for (indexing in indices) { + if (indexing != indices.last()) { + val allVarsSame = + And( + vars.map { + Eq(PathUtils.unfold(it.ref, indexing), PathUtils.unfold(it.ref, indices.last())) + } + ) + bmcSolver.add(Not(allVarsSame)) } + } - return WithPushPop(bmcSolver).use { - bmcSolver.add(Not(unfoldedPropExpr(indices.last()))) - - 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, EmptyWitness.getInstance(), BoundedStatistics(iteration)) - } else null - } + if (bmcSolver.check().isUnsat) { + logger.write(Logger.Level.MAINSTEP, "Safety proven in BMC step\n") + return SafetyResult.safe(EmptyProof.getInstance(), BoundedStatistics(iteration)) + } } - private fun kind(): SafetyResult>? { - val indSolver = this.indSolver!! + return WithPushPop(bmcSolver).use { + bmcSolver.add(Not(unfoldedPropExpr(indices.last()))) - logger.write(Logger.Level.MAINSTEP, "\tStarting k-induction\n") + 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, EmptyProof.getInstance(), BoundedStatistics(iteration)) + } else null + } + } - exprs.subList(kindLastIterLookup, exprs.size).forEach { indSolver.add(it) } - indices.subList(kindLastIterLookup, indices.size - 1).forEach { indSolver.add(unfoldedPropExpr(it)) } + private fun kind(): SafetyResult>? { + val indSolver = this.indSolver!! - return WithPushPop(indSolver).use { - indSolver.add(Not(unfoldedPropExpr(indices.last()))) + logger.write(Logger.Level.MAINSTEP, "\tStarting k-induction\n") - if (indSolver.check().isUnsat) { - logger.write(Logger.Level.MAINSTEP, "Safety proven in k-induction step\n") - SafetyResult.safe(EmptyWitness.getInstance(), BoundedStatistics(iteration)) - } else null - } + exprs.subList(kindLastIterLookup, exprs.size).forEach { indSolver.add(it) } + indices.subList(kindLastIterLookup, indices.size - 1).forEach { + indSolver.add(unfoldedPropExpr(it)) } - private fun itp(): SafetyResult>? { - val itpSolver = this.itpSolver!! - logger.write(Logger.Level.MAINSTEP, "\tStarting IMC\n") - - itpSolver.push() - - val a = itpSolver.createMarker() - val b = itpSolver.createMarker() - val pattern = itpSolver.createBinPattern(a, b) - - itpSolver.push() - - itpSolver.add(a, unfoldedInitExpr) - itpSolver.add(a, exprs[0]) - itpSolver.add(b, exprs.subList(1, exprs.size)) - - if (lfPathOnly()) { // indices contains currIndex as last() - itpSolver.push() - for (indexing in indices) { - if (indexing != indices.last()) { - val allVarsSame = And(vars.map { - Eq(PathUtils.unfold(it.ref, indexing), PathUtils.unfold(it.ref, indices.last())) - }) - itpSolver.add(a, Not(allVarsSame)) - } - } - - if (itpSolver.check().isUnsat) { - itpSolver.pop() - itpSolver.pop() - logger.write(Logger.Level.MAINSTEP, "Safety proven in IMC/BMC step\n") - return SafetyResult.safe(EmptyWitness.getInstance(), BoundedStatistics(iteration)) - } - itpSolver.pop() + return WithPushPop(indSolver).use { + indSolver.add(Not(unfoldedPropExpr(indices.last()))) + + if (indSolver.check().isUnsat) { + logger.write(Logger.Level.MAINSTEP, "Safety proven in k-induction step\n") + SafetyResult.safe(EmptyProof.getInstance(), BoundedStatistics(iteration)) + } else null + } + } + + private fun itp(): SafetyResult>? { + val itpSolver = this.itpSolver!! + logger.write(Logger.Level.MAINSTEP, "\tStarting IMC\n") + + itpSolver.push() + + val a = itpSolver.createMarker() + val b = itpSolver.createMarker() + val pattern = itpSolver.createBinPattern(a, b) + + itpSolver.push() + + itpSolver.add(a, unfoldedInitExpr) + itpSolver.add(a, exprs[0]) + itpSolver.add(b, exprs.subList(1, exprs.size)) + + if (lfPathOnly()) { // indices contains currIndex as last() + itpSolver.push() + for (indexing in indices) { + if (indexing != indices.last()) { + val allVarsSame = + And( + vars.map { + Eq(PathUtils.unfold(it.ref, indexing), PathUtils.unfold(it.ref, indices.last())) + } + ) + itpSolver.add(a, Not(allVarsSame)) } + } - itpSolver.add(b, Not(unfoldedPropExpr(indices.last()))) + if (itpSolver.check().isUnsat) { + itpSolver.pop() + itpSolver.pop() + logger.write(Logger.Level.MAINSTEP, "Safety proven in IMC/BMC step\n") + return SafetyResult.safe(EmptyProof.getInstance(), BoundedStatistics(iteration)) + } + itpSolver.pop() + } - val status = itpSolver.check() + itpSolver.add(b, Not(unfoldedPropExpr(indices.last()))) - if (status.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() - return SafetyResult.unsafe(trace, EmptyWitness.getInstance(), BoundedStatistics(iteration)) - } + val status = itpSolver.check() - var img = unfoldedInitExpr - while (itpSolver.check().isUnsat) { - val interpolant = itpSolver.getInterpolant(pattern) - val itpFormula = PathUtils.unfold(PathUtils.foldin(interpolant.eval(a), indices[1]), indices[0]) - itpSolver.pop() - - 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(EmptyWitness.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()))) - } + if (status.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() + return SafetyResult.unsafe(trace, EmptyProof.getInstance(), BoundedStatistics(iteration)) + } + var img = unfoldedInitExpr + while (itpSolver.check().isUnsat) { + val interpolant = itpSolver.getInterpolant(pattern) + val itpFormula = + PathUtils.unfold(PathUtils.foldin(interpolant.eval(a), indices[1]), indices[0]) + itpSolver.pop() + + 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 null + 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()))) } - - private fun getTrace(model: Valuation): Trace { - val stateList = LinkedList() - val actionList = LinkedList() - var lastValuation: Valuation? = null - for (i in indices) { - val valuation = PathUtils.extractValuation(model, i, vars) - stateList.add(valToState(valuation)) - if (lastValuation != null) { - actionList.add(biValToAction(lastValuation, valuation)) - } - lastValuation = valuation - } - return Trace.of(stateList, actionList) + itpSolver.pop() + itpSolver.pop() + return null + } + + private fun getTrace(model: Valuation): Trace { + val stateList = LinkedList() + val actionList = LinkedList() + var lastValuation: Valuation? = null + for (i in indices) { + val valuation = PathUtils.extractValuation(model, i, vars) + stateList.add(valToState(valuation)) + if (lastValuation != null) { + actionList.add(biValToAction(lastValuation, valuation)) + } + lastValuation = valuation } - -} \ No newline at end of file + return Trace.of(stateList, actionList) + } +} diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/Abstractor.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/Abstractor.java index a6cb49bb43..d4601d334e 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/Abstractor.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/Abstractor.java @@ -16,22 +16,17 @@ package hu.bme.mit.theta.analysis.algorithm.cegar; import hu.bme.mit.theta.analysis.Prec; -import hu.bme.mit.theta.analysis.algorithm.Witness; +import hu.bme.mit.theta.analysis.algorithm.Proof; /** - * Common interface for the abstractor component. It can create an initial witness and check a witness with - * a given precision. + * Common interface for the abstractor component. It can create an initial witness and check a + * witness with a given precision. */ -public interface Abstractor

{ +public interface Abstractor

{ - /** - * Create initial witness - */ - W createWitness(); - - /** - * Check witness with given precision - */ - AbstractorResult check(W witness, P prec); + /** Create initial witness */ + Pr createProof(); + /** Check witness with given precision */ + AbstractorResult check(Pr witness, P prec); } diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/BasicArgAbstractor.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/BasicArgAbstractor.java index 050ae32ce3..a92dbedfc2 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/BasicArgAbstractor.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/BasicArgAbstractor.java @@ -15,6 +15,9 @@ */ package hu.bme.mit.theta.analysis.algorithm.cegar; +import static com.google.common.base.Preconditions.checkNotNull; +import static com.google.common.base.Preconditions.checkState; + import hu.bme.mit.theta.analysis.Action; import hu.bme.mit.theta.analysis.Prec; import hu.bme.mit.theta.analysis.State; @@ -30,18 +33,13 @@ import hu.bme.mit.theta.common.logging.Logger; import hu.bme.mit.theta.common.logging.Logger.Level; import hu.bme.mit.theta.common.logging.NullLogger; - import java.util.Collection; import java.util.Collections; import java.util.function.Function; -import static com.google.common.base.Preconditions.checkNotNull; -import static com.google.common.base.Preconditions.checkState; - -/** - * Basic implementation for the abstractor, relying on an ArgBuilder. - */ -public class BasicArgAbstractor implements ArgAbstractor { +/** Basic implementation for the abstractor, relying on an ArgBuilder. */ +public class BasicArgAbstractor + implements ArgAbstractor { protected final ArgBuilder argBuilder; protected final Function projection; @@ -49,8 +47,12 @@ public class BasicArgAbstractor stopCriterion; protected final Logger logger; - protected BasicArgAbstractor(final ArgBuilder argBuilder, final Function projection, - final Waitlist> waitlist, final StopCriterion stopCriterion, final Logger logger) { + protected BasicArgAbstractor( + final ArgBuilder argBuilder, + final Function projection, + final Waitlist> waitlist, + final StopCriterion stopCriterion, + final Logger logger) { this.argBuilder = checkNotNull(argBuilder); this.projection = checkNotNull(projection); this.waitlist = checkNotNull(waitlist); @@ -64,7 +66,7 @@ public static Builder createWitness() { + public ARG createProof() { return argBuilder.createArg(); } @@ -82,11 +84,16 @@ public AbstractorResult check(final ARG arg, final P prec) { assert arg.isInitialized(); - logger.write(Level.INFO, "| | Starting ARG: %d nodes, %d incomplete, %d unsafe%n", arg.getNodes().count(), - arg.getIncompleteNodes().count(), arg.getUnsafeNodes().count()); + logger.write( + Level.INFO, + "| | Starting ARG: %d nodes, %d incomplete, %d unsafe%n", + arg.getNodes().count(), + arg.getIncompleteNodes().count(), + arg.getUnsafeNodes().count()); logger.write(Level.SUBSTEP, "| | Building ARG..."); - final Partition, ?> reachedSet = Partition.of(n -> projection.apply(n.getState())); + final Partition, ?> reachedSet = + Partition.of(n -> projection.apply(n.getState())); waitlist.clear(); reachedSet.addAll(arg.getNodes()); @@ -109,8 +116,12 @@ public AbstractorResult check(final ARG arg, final P prec) { } logger.write(Level.SUBSTEP, "done%n"); - logger.write(Level.INFO, "| | Finished ARG: %d nodes, %d incomplete, %d unsafe%n", arg.getNodes().count(), - arg.getIncompleteNodes().count(), arg.getUnsafeNodes().count()); + logger.write( + Level.INFO, + "| | Finished ARG: %d nodes, %d incomplete, %d unsafe%n", + arg.getNodes().count(), + arg.getIncompleteNodes().count(), + arg.getUnsafeNodes().count()); waitlist.clear(); // Optimization @@ -175,8 +186,8 @@ public Builder logger(final Logger logger) { } public BasicArgAbstractor build() { - return new BasicArgAbstractor<>(argBuilder, projection, waitlist, stopCriterion, logger); + return new BasicArgAbstractor<>( + argBuilder, projection, waitlist, stopCriterion, logger); } } - } diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/CegarChecker.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/CegarChecker.java index fa811afc42..30da9a28e5 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/CegarChecker.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/CegarChecker.java @@ -20,11 +20,11 @@ import hu.bme.mit.theta.analysis.Cex; import hu.bme.mit.theta.analysis.Prec; import hu.bme.mit.theta.analysis.State; +import hu.bme.mit.theta.analysis.algorithm.Proof; import hu.bme.mit.theta.analysis.algorithm.SafetyChecker; import hu.bme.mit.theta.analysis.algorithm.SafetyResult; -import hu.bme.mit.theta.analysis.algorithm.Witness; import hu.bme.mit.theta.analysis.runtimemonitor.MonitorCheckpoint; -import hu.bme.mit.theta.analysis.utils.WitnessVisualizer; +import hu.bme.mit.theta.analysis.utils.ProofVisualizer; import hu.bme.mit.theta.common.Utils; import hu.bme.mit.theta.common.logging.Logger; import hu.bme.mit.theta.common.logging.Logger.Level; @@ -42,38 +42,38 @@ * check counterexamples and refine them if needed. It also provides certain * statistics about its execution. */ -public final class CegarChecker implements SafetyChecker { +public final class CegarChecker implements SafetyChecker { - private final Abstractor abstractor; - private final Refiner refiner; + private final Abstractor abstractor; + private final Refiner refiner; private final Logger logger; - private final W witness; - private final WitnessVisualizer witnessVisualizer; + private final Pr proof; + private final ProofVisualizer proofVisualizer; - private CegarChecker(final Abstractor abstractor, final Refiner refiner, final Logger logger, final WitnessVisualizer witnessVisualizer) { + private CegarChecker(final Abstractor abstractor, final Refiner refiner, final Logger logger, final ProofVisualizer proofVisualizer) { this.abstractor = checkNotNull(abstractor); this.refiner = checkNotNull(refiner); this.logger = checkNotNull(logger); - witness = abstractor.createWitness(); - this.witnessVisualizer = checkNotNull(witnessVisualizer); + proof = abstractor.createProof(); + this.proofVisualizer = checkNotNull(proofVisualizer); } - public static CegarChecker create( - final Abstractor abstractor, final Refiner refiner, final WitnessVisualizer witnessVisualizer) { - return create(abstractor, refiner, NullLogger.getInstance(), witnessVisualizer); + public static CegarChecker create( + final Abstractor abstractor, final Refiner refiner, final ProofVisualizer proofVisualizer) { + return create(abstractor, refiner, NullLogger.getInstance(), proofVisualizer); } - public static CegarChecker create( - final Abstractor abstractor, final Refiner refiner, final Logger logger, final WitnessVisualizer witnessVisualizer) { - return new CegarChecker<>(abstractor, refiner, logger, witnessVisualizer); + public static CegarChecker create( + final Abstractor abstractor, final Refiner refiner, final Logger logger, final ProofVisualizer proofVisualizer) { + return new CegarChecker<>(abstractor, refiner, logger, proofVisualizer); } - public W getWitness() { - return witness; + public Pr getProof() { + return proof; } @Override - public SafetyResult check(final P initPrec) { + public SafetyResult check(final P initPrec) { logger.write(Level.INFO, "Configuration: %s%n", this); final Stopwatch stopwatch = Stopwatch.createStarted(); long abstractorTime = 0; @@ -89,12 +89,12 @@ public SafetyResult check(final P initPrec) { logger.write(Level.MAINSTEP, "Iteration %d%n", iteration); logger.write(Level.MAINSTEP, "| Checking abstraction...%n"); final long abstractorStartTime = stopwatch.elapsed(TimeUnit.MILLISECONDS); - abstractorResult = abstractor.check(witness, prec); + abstractorResult = abstractor.check(proof, prec); abstractorTime += stopwatch.elapsed(TimeUnit.MILLISECONDS) - abstractorStartTime; logger.write(Level.MAINSTEP, "| Checking abstraction done, result: %s%n", abstractorResult); if (WebDebuggerLogger.enabled()) { - String argGraph = JSONWriter.getInstance().writeString(witnessVisualizer.visualize(witness)); + String argGraph = JSONWriter.getInstance().writeString(proofVisualizer.visualize(proof)); String precString = prec.toString(); wdl.addIteration(iteration, argGraph, precString); } @@ -105,7 +105,7 @@ public SafetyResult check(final P initPrec) { P lastPrec = prec; logger.write(Level.MAINSTEP, "| Refining abstraction...%n"); final long refinerStartTime = stopwatch.elapsed(TimeUnit.MILLISECONDS); - refinerResult = refiner.refine(witness, prec); + refinerResult = refiner.refine(proof, prec); refinerTime += stopwatch.elapsed(TimeUnit.MILLISECONDS) - refinerStartTime; logger.write(Level.MAINSTEP, "Refining abstraction done, result: %s%n", refinerResult); @@ -124,16 +124,16 @@ public SafetyResult check(final P initPrec) { } while (!abstractorResult.isSafe() && !refinerResult.isUnsafe()); stopwatch.stop(); - SafetyResult cegarResult = null; + SafetyResult cegarResult = null; final CegarStatistics stats = new CegarStatistics(stopwatch.elapsed(TimeUnit.MILLISECONDS), abstractorTime, refinerTime, iteration); assert abstractorResult.isSafe() || refinerResult.isUnsafe(); if (abstractorResult.isSafe()) { - cegarResult = SafetyResult.safe(witness, stats); + cegarResult = SafetyResult.safe(proof, stats); } else if (refinerResult.isUnsafe()) { - cegarResult = SafetyResult.unsafe(refinerResult.asUnsafe().getCex(), witness, stats); + cegarResult = SafetyResult.unsafe(refinerResult.asUnsafe().getCex(), proof, stats); } assert cegarResult != null; diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/Refiner.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/Refiner.java index 6eca5d7c21..abd645f3cf 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/Refiner.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/Refiner.java @@ -19,16 +19,16 @@ import hu.bme.mit.theta.analysis.Cex; import hu.bme.mit.theta.analysis.Prec; import hu.bme.mit.theta.analysis.State; -import hu.bme.mit.theta.analysis.algorithm.Witness; +import hu.bme.mit.theta.analysis.algorithm.Proof; /** * Common interface for refiners. It takes a witness and a precision, checks if the counterexample in * the witness is feasible and if not, it refines the precision */ -public interface Refiner { +public interface Refiner { /** * Checks if the counterexample in the witness is feasible. If not, refines the precision */ - RefinerResult refine(W witness, P prec); + RefinerResult refine(Pr witness, P prec); } diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/chc/HornChecker.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/chc/HornChecker.kt index 0c083b7cd0..a52da53d51 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/chc/HornChecker.kt +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/chc/HornChecker.kt @@ -13,13 +13,12 @@ * See the License for the specific language governing permissions and * limitations under the License. */ - package hu.bme.mit.theta.analysis.algorithm.chc import hu.bme.mit.theta.analysis.Cex +import hu.bme.mit.theta.analysis.algorithm.Proof import hu.bme.mit.theta.analysis.algorithm.SafetyChecker import hu.bme.mit.theta.analysis.algorithm.SafetyResult -import hu.bme.mit.theta.analysis.algorithm.Witness import hu.bme.mit.theta.analysis.unit.UnitPrec import hu.bme.mit.theta.common.logging.Logger import hu.bme.mit.theta.core.Relation @@ -30,58 +29,62 @@ import hu.bme.mit.theta.solver.ProofNode import hu.bme.mit.theta.solver.SolverFactory import hu.bme.mit.theta.solver.SolverStatus -data class Invariant(val lookup: Map>) : Witness +data class Invariant(val lookup: Map>) : Proof data class CexTree(val proofNode: ProofNode) : Cex { - override fun length(): Int = proofNode.depth() + override fun length(): Int = proofNode.depth() } -/** - * A checker for CHC-based verification. - */ +/** A checker for CHC-based verification. */ class HornChecker( - private val relations: List, - private val hornSolverFactory: SolverFactory, - private val logger: Logger, + private val relations: List, + private val hornSolverFactory: SolverFactory, + private val logger: Logger, ) : SafetyChecker { - override fun check(prec: UnitPrec?): SafetyResult { - val solver = hornSolverFactory.createHornSolver() - logger.write(Logger.Level.MAINSTEP, "Starting encoding\n") - solver.add(relations) - logger.write(Logger.Level.DETAIL, "Relations:\n\t${ + override fun check(prec: UnitPrec?): SafetyResult { + val solver = hornSolverFactory.createHornSolver() + logger.write(Logger.Level.MAINSTEP, "Starting encoding\n") + solver.add(relations) + logger.write( + Logger.Level.DETAIL, + "Relations:\n\t${ relations.joinToString("\n\t") { it.constDecl.toString() } - }\n") - logger.write(Logger.Level.DETAIL, "Rules:\n\t${ + }\n", + ) + logger.write( + Logger.Level.DETAIL, + "Rules:\n\t${ solver.assertions.joinToString("\n\t") { it.toString().replace(Regex("[\r\n\t ]+"), " ") } - }\n") - logger.write(Logger.Level.MAINSTEP, "Added constraints to solver\n") - solver.check() - logger.write(Logger.Level.MAINSTEP, "Check() finished (result: ${solver.status})\n") - return when (solver.status) { - SolverStatus.SAT -> { - logger.write(Logger.Level.MAINSTEP, "Proof (model) found\n") - val model = solver.model.toMap() - SafetyResult.safe( - Invariant(relations.associateWith { model[it.constDecl] as? Expr ?: True() })) - } + }\n", + ) + logger.write(Logger.Level.MAINSTEP, "Added constraints to solver\n") + solver.check() + logger.write(Logger.Level.MAINSTEP, "Check() finished (result: ${solver.status})\n") + return when (solver.status) { + SolverStatus.SAT -> { + logger.write(Logger.Level.MAINSTEP, "Proof (model) found\n") + val model = solver.model.toMap() + SafetyResult.safe( + Invariant(relations.associateWith { model[it.constDecl] as? Expr ?: True() }) + ) + } - SolverStatus.UNSAT -> { - logger.write(Logger.Level.MAINSTEP, "Counterexample found\n") - val proof = solver.proof - SafetyResult.unsafe(CexTree(proof), Invariant(emptyMap())) - } + SolverStatus.UNSAT -> { + logger.write(Logger.Level.MAINSTEP, "Counterexample found\n") + val proof = solver.proof + SafetyResult.unsafe(CexTree(proof), Invariant(emptyMap())) + } - else -> { - logger.write(Logger.Level.MAINSTEP, "No solution found.\n") - SafetyResult.unknown() - } - } + else -> { + logger.write(Logger.Level.MAINSTEP, "No solution found.\n") + SafetyResult.unknown() + } } - -} \ No newline at end of file + } +} diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/analysis/FiniteStateChecker.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/analysis/FiniteStateChecker.kt index 05c02303c3..b316300d9c 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/analysis/FiniteStateChecker.kt +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/analysis/FiniteStateChecker.kt @@ -13,14 +13,13 @@ * See the License for the specific language governing permissions and * limitations under the License. */ - package hu.bme.mit.theta.analysis.algorithm.mcm.analysis import hu.bme.mit.theta.analysis.EmptyCex import hu.bme.mit.theta.analysis.InitFunc import hu.bme.mit.theta.analysis.LTS import hu.bme.mit.theta.analysis.TransFunc -import hu.bme.mit.theta.analysis.algorithm.EmptyWitness +import hu.bme.mit.theta.analysis.algorithm.EmptyProof import hu.bme.mit.theta.analysis.algorithm.SafetyChecker import hu.bme.mit.theta.analysis.algorithm.SafetyResult import hu.bme.mit.theta.analysis.algorithm.mcm.interpreter.MemoryEventProvider @@ -35,52 +34,52 @@ import hu.bme.mit.theta.graphsolver.patterns.constraints.GraphConstraint import hu.bme.mit.theta.graphsolver.solvers.GraphSolver import java.util.* -/** - * WiP checker for finite-state systems - */ +/** WiP checker for finite-state systems */ class FiniteStateChecker( - private val mcm: Collection, - private val initFunc: InitFunc, - private val actionFunc: LTS, - private val transFunc: TransFunc, - private val memoryEventProvider: MemoryEventProvider, - private val graphPatternCompiler: GraphPatternCompiler, - private val graphPatternSolver: GraphSolver -) : SafetyChecker { + private val mcm: Collection, + private val initFunc: InitFunc, + private val actionFunc: LTS, + private val transFunc: TransFunc, + private val memoryEventProvider: MemoryEventProvider, + private val graphPatternCompiler: GraphPatternCompiler, + private val graphPatternSolver: GraphSolver, +) : SafetyChecker { - override fun check(prec: ExplPrec): SafetyResult { - val eventIds = LinkedList() - val rels = LinkedList>() - val lastIds = LinkedHashMap() - val initId = nextId(eventIds) - val initStates = LinkedList(initFunc.getInitStates(prec)) - initStates.forEach { lastIds[it] = initId } - while (initStates.isNotEmpty()) { - val state = initStates.pop() - val lastId = checkNotNull(lastIds[state]) - val actions = actionFunc.getEnabledActionsFor(state) - - val nextStates = actions.map { a -> - val memEvent = memoryEventProvider[a, prec] - transFunc.getSuccStates(state, a, prec).onEach { s -> - memEvent?.also { - val id = nextId(eventIds) - rels.add(Pair(memEvent.type().label, Tuple1.of(id))) - rels.add(Pair("po", Tuple2.of(lastId, id))) - lastIds[s] = id - } - } - }.flatten() - initStates.addAll(nextStates) - } -// PartialSolver(mcm, CandidateExecutionGraph(eventIds, rels)) - return SafetyResult.unsafe(EmptyCex.getInstance(), EmptyWitness.getInstance()) + override fun check(prec: ExplPrec): SafetyResult { + val eventIds = LinkedList() + val rels = LinkedList>() + val lastIds = LinkedHashMap() + val initId = nextId(eventIds) + val initStates = LinkedList(initFunc.getInitStates(prec)) + initStates.forEach { lastIds[it] = initId } + while (initStates.isNotEmpty()) { + val state = initStates.pop() + val lastId = checkNotNull(lastIds[state]) + val actions = actionFunc.getEnabledActionsFor(state) + val nextStates = + actions + .map { a -> + val memEvent = memoryEventProvider[a, prec] + transFunc.getSuccStates(state, a, prec).onEach { s -> + memEvent?.also { + val id = nextId(eventIds) + rels.add(Pair(memEvent.type().label, Tuple1.of(id))) + rels.add(Pair("po", Tuple2.of(lastId, id))) + lastIds[s] = id + } + } + } + .flatten() + initStates.addAll(nextStates) } + // PartialSolver(mcm, CandidateExecutionGraph(eventIds, rels)) + return SafetyResult.unsafe(EmptyCex.getInstance(), EmptyProof.getInstance()) + } - private fun nextId(list: MutableList): Int { - val ret = list.size - list.add(list.size) - return ret - } -} \ No newline at end of file + private fun nextId(list: MutableList): Int { + val ret = list.size + list.add(list.size) + return ret + } +} diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/MddChecker.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/MddChecker.java index df1feb4743..cd81d5a697 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/MddChecker.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/MddChecker.java @@ -15,28 +15,28 @@ */ package hu.bme.mit.theta.analysis.algorithm.mdd; -import hu.bme.mit.delta.collections.impl.RecursiveIntObjMapViews; -import hu.bme.mit.delta.java.mdd.*; +import static hu.bme.mit.theta.core.type.booltype.SmartBoolExprs.Not; + +import hu.bme.mit.delta.java.mdd.JavaMddFactory; +import hu.bme.mit.delta.java.mdd.MddGraph; +import hu.bme.mit.delta.java.mdd.MddHandle; +import hu.bme.mit.delta.java.mdd.MddVariableOrder; import hu.bme.mit.delta.mdd.MddInterpreter; import hu.bme.mit.delta.mdd.MddVariableDescriptor; -import hu.bme.mit.theta.analysis.algorithm.SafetyResult; import hu.bme.mit.theta.analysis.algorithm.SafetyChecker; +import hu.bme.mit.theta.analysis.algorithm.SafetyResult; +import hu.bme.mit.theta.analysis.algorithm.mdd.ansd.AbstractNextStateDescriptor; +import hu.bme.mit.theta.analysis.algorithm.mdd.ansd.impl.MddNodeInitializer; +import hu.bme.mit.theta.analysis.algorithm.mdd.ansd.impl.MddNodeNextStateDescriptor; +import hu.bme.mit.theta.analysis.algorithm.mdd.expressionnode.ExprLatticeDefinition; +import hu.bme.mit.theta.analysis.algorithm.mdd.expressionnode.MddExpressionTemplate; import hu.bme.mit.theta.analysis.algorithm.mdd.fixedpoint.BfsProvider; import hu.bme.mit.theta.analysis.algorithm.mdd.fixedpoint.GeneralizedSaturationProvider; -import hu.bme.mit.theta.analysis.algorithm.mdd.ansd.AbstractNextStateDescriptor; import hu.bme.mit.theta.analysis.algorithm.mdd.fixedpoint.SimpleSaturationProvider; import hu.bme.mit.theta.analysis.algorithm.mdd.fixedpoint.StateSpaceEnumerationProvider; -import hu.bme.mit.theta.common.logging.Logger.Level; -import hu.bme.mit.theta.solver.SolverPool; -import hu.bme.mit.theta.analysis.algorithm.mdd.expressionnode.ExprLatticeDefinition; -import hu.bme.mit.theta.analysis.algorithm.mdd.expressionnode.MddExpressionTemplate; -import hu.bme.mit.theta.analysis.algorithm.mdd.ansd.impl.MddNodeInitializer; -import hu.bme.mit.theta.analysis.algorithm.mdd.ansd.impl.MddNodeNextStateDescriptor; import hu.bme.mit.theta.analysis.expr.ExprAction; -import hu.bme.mit.theta.analysis.utils.MddNodeVisualizer; import hu.bme.mit.theta.common.logging.Logger; -import hu.bme.mit.theta.common.visualization.Graph; -import hu.bme.mit.theta.common.visualization.writer.GraphvizWriter; +import hu.bme.mit.theta.common.logging.Logger.Level; import hu.bme.mit.theta.core.decl.Decl; import hu.bme.mit.theta.core.decl.VarDecl; import hu.bme.mit.theta.core.type.Expr; @@ -45,15 +45,11 @@ import hu.bme.mit.theta.core.utils.PathUtils; import hu.bme.mit.theta.core.utils.indexings.VarIndexing; import hu.bme.mit.theta.core.utils.indexings.VarIndexingFactory; -import hu.bme.mit.theta.solver.SolverFactory; - -import java.io.FileNotFoundException; +import hu.bme.mit.theta.solver.SolverPool; import java.util.List; import java.util.Set; -import static hu.bme.mit.theta.core.type.booltype.SmartBoolExprs.Not; - -public class MddChecker implements SafetyChecker { +public class MddChecker implements SafetyChecker { private final Expr initRel; private final VarIndexing initIndexing; @@ -64,16 +60,19 @@ public class MddChecker implements SafetyChecker initRel, - VarIndexing initIndexing, - A transRel, - Expr safetyProperty, - SolverPool solverPool, - Logger logger, - IterationStrategy iterationStrategy) { + private MddChecker( + Expr initRel, + VarIndexing initIndexing, + A transRel, + Expr safetyProperty, + SolverPool solverPool, + Logger logger, + IterationStrategy iterationStrategy) { this.initRel = initRel; this.initIndexing = initIndexing; this.transRel = transRel; @@ -83,40 +82,63 @@ private MddChecker(Expr initRel, this.iterationStrategy = iterationStrategy; } - public static MddChecker create(Expr initRel, - VarIndexing initIndexing, - A transRel, - Expr safetyProperty, - SolverPool solverPool, - Logger logger) { - return new MddChecker(initRel, initIndexing, transRel, safetyProperty, solverPool, logger, IterationStrategy.GSAT); + public static MddChecker create( + Expr initRel, + VarIndexing initIndexing, + A transRel, + Expr safetyProperty, + SolverPool solverPool, + Logger logger) { + return new MddChecker( + initRel, + initIndexing, + transRel, + safetyProperty, + solverPool, + logger, + IterationStrategy.GSAT); } - public static MddChecker create(Expr initRel, - VarIndexing initIndexing, - A transRel, - Expr safetyProperty, - SolverPool solverPool, - Logger logger, - IterationStrategy iterationStrategy) { - return new MddChecker(initRel, initIndexing, transRel, safetyProperty, solverPool, logger, iterationStrategy); + public static MddChecker create( + Expr initRel, + VarIndexing initIndexing, + A transRel, + Expr safetyProperty, + SolverPool solverPool, + Logger logger, + IterationStrategy iterationStrategy) { + return new MddChecker( + initRel, + initIndexing, + transRel, + safetyProperty, + solverPool, + logger, + iterationStrategy); } @Override - public SafetyResult check(Void input) { + public SafetyResult check(Void input) { - final MddGraph mddGraph = JavaMddFactory.getDefault().createMddGraph(ExprLatticeDefinition.forExpr()); + final MddGraph mddGraph = + JavaMddFactory.getDefault().createMddGraph(ExprLatticeDefinition.forExpr()); - final MddVariableOrder stateOrder = JavaMddFactory.getDefault().createMddVariableOrder(mddGraph); - final MddVariableOrder transOrder = JavaMddFactory.getDefault().createMddVariableOrder(mddGraph); + final MddVariableOrder stateOrder = + JavaMddFactory.getDefault().createMddVariableOrder(mddGraph); + final MddVariableOrder transOrder = + JavaMddFactory.getDefault().createMddVariableOrder(mddGraph); - final Set> vars = ExprUtils.getVars(List.of(initRel, transRel.toExpr(), safetyProperty)); + final Set> vars = + ExprUtils.getVars(List.of(initRel, transRel.toExpr(), safetyProperty)); for (var v : vars) { final var domainSize = v.getType() instanceof BoolType ? 2 : 0; - stateOrder.createOnTop(MddVariableDescriptor.create(v.getConstDecl(initIndexing.get(v)), domainSize)); + stateOrder.createOnTop( + MddVariableDescriptor.create(v.getConstDecl(initIndexing.get(v)), domainSize)); - transOrder.createOnTop(MddVariableDescriptor.create(v.getConstDecl(transRel.nextIndexing().get(v)), domainSize)); + transOrder.createOnTop( + MddVariableDescriptor.create( + v.getConstDecl(transRel.nextIndexing().get(v)), domainSize)); transOrder.createOnTop(MddVariableDescriptor.create(v.getConstDecl(0), domainSize)); } @@ -124,13 +146,20 @@ public SafetyResult check(Void input) { final var transSig = transOrder.getDefaultSetSignature(); final Expr initExpr = PathUtils.unfold(initRel, initIndexing); - final MddHandle initNode = stateSig.getTopVariableHandle().checkInNode(MddExpressionTemplate.of(initExpr, o -> (Decl) o, solverPool)); + final MddHandle initNode = + stateSig.getTopVariableHandle() + .checkInNode(MddExpressionTemplate.of(initExpr, o -> (Decl) o, solverPool)); logger.write(Level.INFO, "Created initial node"); - final Expr transExpr = PathUtils.unfold(transRel.toExpr(), VarIndexingFactory.indexing(0)); - final MddHandle transitionNode = transSig.getTopVariableHandle().checkInNode(MddExpressionTemplate.of(transExpr, o -> (Decl) o, solverPool)); - final AbstractNextStateDescriptor nextStates = MddNodeNextStateDescriptor.of(transitionNode); + final Expr transExpr = + PathUtils.unfold(transRel.toExpr(), VarIndexingFactory.indexing(0)); + final MddHandle transitionNode = + transSig.getTopVariableHandle() + .checkInNode( + MddExpressionTemplate.of(transExpr, o -> (Decl) o, solverPool)); + final AbstractNextStateDescriptor nextStates = + MddNodeNextStateDescriptor.of(transitionNode); logger.write(Level.INFO, "Created next-state node, starting fixed point calculation"); @@ -147,12 +176,20 @@ public SafetyResult check(Void input) { } default -> throw new IllegalStateException("Unexpected value: " + iterationStrategy); } - final MddHandle stateSpace = stateSpaceProvider.compute(MddNodeInitializer.of(initNode), nextStates, stateSig.getTopVariableHandle()); + final MddHandle stateSpace = + stateSpaceProvider.compute( + MddNodeInitializer.of(initNode), + nextStates, + stateSig.getTopVariableHandle()); logger.write(Level.INFO, "Enumerated state-space"); final Expr negatedPropExpr = PathUtils.unfold(Not(safetyProperty), initIndexing); - final MddHandle propNode = stateSig.getTopVariableHandle().checkInNode(MddExpressionTemplate.of(negatedPropExpr, o -> (Decl) o, solverPool)); + final MddHandle propNode = + stateSig.getTopVariableHandle() + .checkInNode( + MddExpressionTemplate.of( + negatedPropExpr, o -> (Decl) o, solverPool)); final MddHandle propViolating = (MddHandle) stateSpace.intersection(propNode); @@ -164,13 +201,21 @@ public SafetyResult check(Void input) { final Long stateSpaceSize = MddInterpreter.calculateNonzeroCount(stateSpace); logger.write(Level.DETAIL, "State space size: " + stateSpaceSize); - final MddAnalysisStatistics statistics = new MddAnalysisStatistics(violatingSize, stateSpaceSize, stateSpaceProvider.getHitCount(), stateSpaceProvider.getQueryCount(), stateSpaceProvider.getCacheSize()); + final MddAnalysisStatistics statistics = + new MddAnalysisStatistics( + violatingSize, + stateSpaceSize, + stateSpaceProvider.getHitCount(), + stateSpaceProvider.getQueryCount(), + stateSpaceProvider.getCacheSize()); - final SafetyResult result; + final SafetyResult result; if (violatingSize != 0) { - result = SafetyResult.unsafe(MddCex.of(propViolating), MddWitness.of(stateSpace), statistics); + result = + SafetyResult.unsafe( + MddCex.of(propViolating), MddProof.of(stateSpace), statistics); } else { - result = SafetyResult.safe(MddWitness.of(stateSpace), statistics); + result = SafetyResult.safe(MddProof.of(stateSpace), statistics); } logger.write(Level.RESULT, "%s%n", result); return result; diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/MddWitness.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/MddProof.java similarity index 81% rename from subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/MddWitness.java rename to subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/MddProof.java index 300dc6579f..805a138399 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/MddWitness.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/MddProof.java @@ -17,18 +17,18 @@ import hu.bme.mit.delta.java.mdd.MddHandle; import hu.bme.mit.delta.mdd.MddInterpreter; -import hu.bme.mit.theta.analysis.algorithm.Witness; +import hu.bme.mit.theta.analysis.algorithm.Proof; -public class MddWitness implements Witness { +public class MddProof implements Proof { private final MddHandle stateSpace; - private MddWitness(MddHandle stateSpace) { + private MddProof(MddHandle stateSpace) { this.stateSpace = stateSpace; } - public static MddWitness of(MddHandle stateSpace) { - return new MddWitness(stateSpace); + public static MddProof of(MddHandle stateSpace) { + return new MddProof(stateSpace); } public Long size() { diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/utils/ArgVisualizer.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/utils/ArgVisualizer.java index c4c82eeb74..89efd988a5 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/utils/ArgVisualizer.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/utils/ArgVisualizer.java @@ -18,25 +18,23 @@ import static hu.bme.mit.theta.common.visualization.Alignment.LEFT; import static hu.bme.mit.theta.common.visualization.Shape.RECTANGLE; -import java.awt.Color; - -import hu.bme.mit.theta.common.container.Containers; - -import java.util.Set; -import java.util.function.Function; -import java.util.stream.Collectors; - import hu.bme.mit.theta.analysis.Action; import hu.bme.mit.theta.analysis.State; import hu.bme.mit.theta.analysis.algorithm.arg.ARG; import hu.bme.mit.theta.analysis.algorithm.arg.ArgEdge; import hu.bme.mit.theta.analysis.algorithm.arg.ArgNode; +import hu.bme.mit.theta.common.container.Containers; import hu.bme.mit.theta.common.visualization.EdgeAttributes; import hu.bme.mit.theta.common.visualization.Graph; import hu.bme.mit.theta.common.visualization.LineStyle; import hu.bme.mit.theta.common.visualization.NodeAttributes; +import java.awt.*; +import java.util.Set; +import java.util.function.Function; +import java.util.stream.Collectors; -public final class ArgVisualizer implements WitnessVisualizer> { +public final class ArgVisualizer + implements ProofVisualizer> { private static final LineStyle COVER_EDGE_STYLE = LineStyle.DASHED; private static final LineStyle SUCC_EDGE_STYLE = LineStyle.NORMAL; @@ -53,8 +51,8 @@ public final class ArgVisualizer implements W private static class LazyHolderDefault { - static final ArgVisualizer INSTANCE = new ArgVisualizer<>(Object::toString, - Object::toString); + static final ArgVisualizer INSTANCE = + new ArgVisualizer<>(Object::toString, Object::toString); } private static class LazyHolderStructureOnly { @@ -62,8 +60,8 @@ private static class LazyHolderStructureOnly { static final ArgVisualizer INSTANCE = new ArgVisualizer<>(s -> "", a -> ""); } - public ArgVisualizer(final Function stateToString, - final Function actionToString) { + public ArgVisualizer( + final Function stateToString, final Function actionToString) { this.stateToString = stateToString; this.actionToString = actionToString; } @@ -87,24 +85,37 @@ public Graph visualize(final ARG arg) { final Set> traversed = Containers.createSet(); - for (final ArgNode initNode : arg.getInitNodes() - .collect(Collectors.toSet())) { + for (final ArgNode initNode : + arg.getInitNodes().collect(Collectors.toSet())) { traverse(graph, initNode, traversed); - final NodeAttributes nAttributes = NodeAttributes.builder().label("") - .fillColor(FILL_COLOR) - .lineColor(FILL_COLOR).lineStyle(SUCC_EDGE_STYLE).peripheries(1).build(); + final NodeAttributes nAttributes = + NodeAttributes.builder() + .label("") + .fillColor(FILL_COLOR) + .lineColor(FILL_COLOR) + .lineStyle(SUCC_EDGE_STYLE) + .peripheries(1) + .build(); graph.addNode(PHANTOM_INIT_ID + initNode.getId(), nAttributes); - final EdgeAttributes eAttributes = EdgeAttributes.builder().label("").color(LINE_COLOR) - .lineStyle(SUCC_EDGE_STYLE).build(); - graph.addEdge(PHANTOM_INIT_ID + initNode.getId(), NODE_ID_PREFIX + initNode.getId(), + final EdgeAttributes eAttributes = + EdgeAttributes.builder() + .label("") + .color(LINE_COLOR) + .lineStyle(SUCC_EDGE_STYLE) + .build(); + graph.addEdge( + PHANTOM_INIT_ID + initNode.getId(), + NODE_ID_PREFIX + initNode.getId(), eAttributes); } return graph; } - private void traverse(final Graph graph, final ArgNode node, - final Set> traversed) { + private void traverse( + final Graph graph, + final ArgNode node, + final Set> traversed) { if (traversed.contains(node)) { return; } else { @@ -114,21 +125,33 @@ private void traverse(final Graph graph, final ArgNode final LineStyle lineStyle = SUCC_EDGE_STYLE; final int peripheries = node.isTarget() ? 2 : 1; - final NodeAttributes nAttributes = NodeAttributes.builder() - .label(stateToString.apply(node.getState())) - .alignment(LEFT).shape(RECTANGLE).font(FONT).fillColor(FILL_COLOR).lineColor(LINE_COLOR) - .lineStyle(lineStyle).peripheries(peripheries).build(); + final NodeAttributes nAttributes = + NodeAttributes.builder() + .label(stateToString.apply(node.getState())) + .alignment(LEFT) + .shape(RECTANGLE) + .font(FONT) + .fillColor(FILL_COLOR) + .lineColor(LINE_COLOR) + .lineStyle(lineStyle) + .peripheries(peripheries) + .build(); graph.addNode(nodeId, nAttributes); - for (final ArgEdge edge : node.getOutEdges() - .collect(Collectors.toSet())) { + for (final ArgEdge edge : + node.getOutEdges().collect(Collectors.toSet())) { traverse(graph, edge.getTarget(), traversed); final String sourceId = NODE_ID_PREFIX + edge.getSource().getId(); final String targetId = NODE_ID_PREFIX + edge.getTarget().getId(); - final EdgeAttributes eAttributes = EdgeAttributes.builder() - .label(actionToString.apply(edge.getAction())) - .alignment(LEFT).font(FONT).color(LINE_COLOR).lineStyle(SUCC_EDGE_STYLE).build(); + final EdgeAttributes eAttributes = + EdgeAttributes.builder() + .label(actionToString.apply(edge.getAction())) + .alignment(LEFT) + .font(FONT) + .color(LINE_COLOR) + .lineStyle(SUCC_EDGE_STYLE) + .build(); graph.addEdge(sourceId, targetId, eAttributes); } @@ -136,10 +159,14 @@ private void traverse(final Graph graph, final ArgNode traverse(graph, node.getCoveringNode().get(), traversed); final String sourceId = NODE_ID_PREFIX + node.getId(); final String targetId = NODE_ID_PREFIX + node.getCoveringNode().get().getId(); - final EdgeAttributes eAttributes = EdgeAttributes.builder().label("").color(LINE_COLOR) - .lineStyle(COVER_EDGE_STYLE).weight(0).build(); + final EdgeAttributes eAttributes = + EdgeAttributes.builder() + .label("") + .color(LINE_COLOR) + .lineStyle(COVER_EDGE_STYLE) + .weight(0) + .build(); graph.addEdge(sourceId, targetId, eAttributes); } } - } diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/utils/WitnessVisualizer.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/utils/ProofVisualizer.java similarity index 83% rename from subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/utils/WitnessVisualizer.java rename to subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/utils/ProofVisualizer.java index bd1a9d8234..954604871d 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/utils/WitnessVisualizer.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/utils/ProofVisualizer.java @@ -13,14 +13,12 @@ * See the License for the specific language governing permissions and * limitations under the License. */ - package hu.bme.mit.theta.analysis.utils; -import hu.bme.mit.theta.analysis.algorithm.Witness; +import hu.bme.mit.theta.analysis.algorithm.Proof; import hu.bme.mit.theta.common.visualization.Graph; -public interface WitnessVisualizer { - - Graph visualize(W witness); +public interface ProofVisualizer { + Graph visualize(Pr proof); } diff --git a/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/mdd/MddCheckerTest.java b/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/mdd/MddCheckerTest.java index 070daeb91f..0f9f524354 100644 --- a/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/mdd/MddCheckerTest.java +++ b/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/mdd/MddCheckerTest.java @@ -15,6 +15,14 @@ */ package hu.bme.mit.theta.analysis.algorithm.mdd; +import static hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.*; +import static hu.bme.mit.theta.core.type.anytype.Exprs.Prime; +import static hu.bme.mit.theta.core.type.booltype.BoolExprs.And; +import static hu.bme.mit.theta.core.type.booltype.BoolExprs.Not; +import static hu.bme.mit.theta.core.type.inttype.IntExprs.Int; +import static org.junit.Assert.assertEquals; +import static org.junit.Assert.assertTrue; + import hu.bme.mit.theta.analysis.algorithm.SafetyResult; import hu.bme.mit.theta.analysis.expr.ExprAction; import hu.bme.mit.theta.common.logging.ConsoleLogger; @@ -29,31 +37,19 @@ import hu.bme.mit.theta.core.utils.indexings.VarIndexingFactory; import hu.bme.mit.theta.solver.SolverPool; import hu.bme.mit.theta.solver.z3legacy.Z3LegacySolverFactory; +import java.util.Arrays; +import java.util.Collection; import org.junit.Test; import org.junit.runner.RunWith; import org.junit.runners.Parameterized; -import java.io.IOException; -import java.util.Arrays; -import java.util.Collection; - -import static hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.*; -import static hu.bme.mit.theta.core.type.anytype.Exprs.Prime; -import static hu.bme.mit.theta.core.type.booltype.BoolExprs.And; -import static hu.bme.mit.theta.core.type.booltype.BoolExprs.Not; -import static hu.bme.mit.theta.core.type.inttype.IntExprs.Int; -import static org.junit.Assert.assertEquals; -import static org.junit.Assert.assertTrue; - @RunWith(value = Parameterized.class) - public class MddCheckerTest { private static final VarDecl X = Decls.Var("x", IntType.getInstance()); private static final VarDecl Y = Decls.Var("y", IntType.getInstance()); private static final VarDecl Z = Decls.Var("z", IntType.getInstance()); - @Parameterized.Parameter(value = 0) public Expr initExpr; @@ -71,57 +67,86 @@ public class MddCheckerTest { @Parameterized.Parameters(name = "{index}: {0}, {1}, {2}, {3}, {4}") public static Collection data() { - return Arrays.asList(new Object[][]{ - - {Eq(X.getRef(), Int(0)), // x = 0 + return Arrays.asList( + new Object[][] { + { + Eq(X.getRef(), Int(0)), // x = 0 Eq(Prime(X.getRef()), X.getRef()), // x'=x Not(Eq(X.getRef(), Int(5))), // not x = 5 true, - 1L}, - - {Eq(X.getRef(), Int(0)), + 1L + }, + { + Eq(X.getRef(), Int(0)), Eq(Prime(X.getRef()), X.getRef()), Not(Eq(X.getRef(), Int(0))), false, - 1L}, - - {Eq(X.getRef(), Int(0)), // x = 0 - And(Eq(Prime(X.getRef()), Add(X.getRef(), Int(1))), Leq(Prime(X.getRef()), Int(10))), // x' = x + 1 & x' <= 10 + 1L + }, + { + Eq(X.getRef(), Int(0)), // x = 0 + And( + Eq(Prime(X.getRef()), Add(X.getRef(), Int(1))), + Leq(Prime(X.getRef()), Int(10))), // x' = x + 1 & x' <= 10 Not(Eq(X.getRef(), Int(5))), false, - 11L}, - - {Eq(X.getRef(), Int(0)), - And(Eq(Prime(X.getRef()), Add(X.getRef(), Int(1))), Leq(Prime(X.getRef()), Int(5))), + 11L + }, + { + Eq(X.getRef(), Int(0)), + And( + Eq(Prime(X.getRef()), Add(X.getRef(), Int(1))), + Leq(Prime(X.getRef()), Int(5))), Not(Eq(X.getRef(), Int(5))), false, - 6L}, - - {Eq(X.getRef(), Int(0)), - And(Eq(Prime(X.getRef()), Add(X.getRef(), Int(1))), Leq(Prime(X.getRef()), Int(4))), + 6L + }, + { + Eq(X.getRef(), Int(0)), + And( + Eq(Prime(X.getRef()), Add(X.getRef(), Int(1))), + Leq(Prime(X.getRef()), Int(4))), Not(Eq(X.getRef(), Int(5))), true, - 5L}, - - {And(Eq(X.getRef(), Int(0)), Eq(Y.getRef(), Int(0)), Eq(Z.getRef(), Int(0))), - And(And(Eq(Prime(X.getRef()), Add(Y.getRef(), Int(1))), Eq(Prime(Y.getRef()), Add(Z.getRef(), Int(1))), Eq(Prime(Z.getRef()), Add(Z.getRef(), Int(1)))), IntExprs.Lt(Prime(Z.getRef()), Int(10))), + 5L + }, + { + And(Eq(X.getRef(), Int(0)), Eq(Y.getRef(), Int(0)), Eq(Z.getRef(), Int(0))), + And( + And( + Eq(Prime(X.getRef()), Add(Y.getRef(), Int(1))), + Eq(Prime(Y.getRef()), Add(Z.getRef(), Int(1))), + Eq(Prime(Z.getRef()), Add(Z.getRef(), Int(1)))), + IntExprs.Lt(Prime(Z.getRef()), Int(10))), Not(Eq(X.getRef(), Int(5))), false, - 10L}, - - {And(Eq(X.getRef(), Int(0)), Eq(Y.getRef(), Int(0)), Eq(Z.getRef(), Int(0))), - And(And(Eq(Prime(X.getRef()), Add(Y.getRef(), Int(1))), Eq(Prime(Y.getRef()), Add(Z.getRef(), Int(1))), Eq(Prime(Z.getRef()), Add(Z.getRef(), Int(1)))), IntExprs.Lt(Prime(Z.getRef()), Int(6))), + 10L + }, + { + And(Eq(X.getRef(), Int(0)), Eq(Y.getRef(), Int(0)), Eq(Z.getRef(), Int(0))), + And( + And( + Eq(Prime(X.getRef()), Add(Y.getRef(), Int(1))), + Eq(Prime(Y.getRef()), Add(Z.getRef(), Int(1))), + Eq(Prime(Z.getRef()), Add(Z.getRef(), Int(1)))), + IntExprs.Lt(Prime(Z.getRef()), Int(6))), Not(Eq(X.getRef(), Int(5))), false, - 6L}, - - {And(Eq(X.getRef(), Int(0)), Eq(Y.getRef(), Int(0)), Eq(Z.getRef(), Int(0))), - And(And(Eq(Prime(X.getRef()), Add(Y.getRef(), Int(1))), Eq(Prime(Y.getRef()), Add(Z.getRef(), Int(1))), Eq(Prime(Z.getRef()), Add(Z.getRef(), Int(1)))), IntExprs.Lt(Prime(Z.getRef()), Int(5))), + 6L + }, + { + And(Eq(X.getRef(), Int(0)), Eq(Y.getRef(), Int(0)), Eq(Z.getRef(), Int(0))), + And( + And( + Eq(Prime(X.getRef()), Add(Y.getRef(), Int(1))), + Eq(Prime(Y.getRef()), Add(Z.getRef(), Int(1))), + Eq(Prime(Z.getRef()), Add(Z.getRef(), Int(1)))), + IntExprs.Lt(Prime(Z.getRef()), Int(5))), Not(Eq(X.getRef(), Int(5))), true, - 5L}, - - }); + 5L + }, + }); } @Test @@ -139,23 +164,32 @@ public void testGsat() throws Exception { testWithIterationStrategy(MddChecker.IterationStrategy.GSAT); } - public void testWithIterationStrategy(MddChecker.IterationStrategy iterationStrategy) throws Exception { + public void testWithIterationStrategy(MddChecker.IterationStrategy iterationStrategy) + throws Exception { final Logger logger = new ConsoleLogger(Logger.Level.SUBSTEP); - final SafetyResult status; + final SafetyResult status; try (var solverPool = new SolverPool(Z3LegacySolverFactory.getInstance())) { - final MddChecker checker = MddChecker.create(initExpr, VarIndexingFactory.indexing(0), new ExprAction() { - @Override - public Expr toExpr() { - return tranExpr; - } - - @Override - public VarIndexing nextIndexing() { - return VarIndexingFactory.indexing(1); - } - }, propExpr, solverPool, logger, iterationStrategy); + final MddChecker checker = + MddChecker.create( + initExpr, + VarIndexingFactory.indexing(0), + new ExprAction() { + @Override + public Expr toExpr() { + return tranExpr; + } + + @Override + public VarIndexing nextIndexing() { + return VarIndexingFactory.indexing(1); + } + }, + propExpr, + solverPool, + logger, + iterationStrategy); status = checker.check(null); } @@ -164,9 +198,6 @@ public VarIndexing nextIndexing() { } else { assertTrue(status.isUnsafe()); } - assertEquals(stateSpaceSize, status.getWitness().size()); - - + assertEquals(stateSpaceSize, status.getProof().size()); } - } diff --git a/subprojects/common/grammar/src/main/java/hu/bme/mit/theta/grammar/gson/SafetyResultAdapter.kt b/subprojects/common/grammar/src/main/java/hu/bme/mit/theta/grammar/gson/SafetyResultAdapter.kt index 6829d577c0..0cd6eb5b2f 100644 --- a/subprojects/common/grammar/src/main/java/hu/bme/mit/theta/grammar/gson/SafetyResultAdapter.kt +++ b/subprojects/common/grammar/src/main/java/hu/bme/mit/theta/grammar/gson/SafetyResultAdapter.kt @@ -13,7 +13,6 @@ * See the License for the specific language governing permissions and * limitations under the License. */ - package hu.bme.mit.theta.grammar.gson import com.google.gson.Gson @@ -24,72 +23,75 @@ import com.google.gson.stream.JsonWriter import hu.bme.mit.theta.analysis.Action import hu.bme.mit.theta.analysis.State import hu.bme.mit.theta.analysis.Trace -import hu.bme.mit.theta.analysis.algorithm.arg.ARG import hu.bme.mit.theta.analysis.algorithm.SafetyResult import hu.bme.mit.theta.analysis.algorithm.Statistics +import hu.bme.mit.theta.analysis.algorithm.arg.ARG import java.lang.reflect.Type import java.util.* class SafetyResultAdapter( - val gsonSupplier: () -> Gson, - private val argTypeSupplier: () -> Type, - private val traceTypeSupplier: () -> Type, + val gsonSupplier: () -> Gson, + private val argTypeSupplier: () -> Type, + private val traceTypeSupplier: () -> Type, ) : TypeAdapter, Trace>>() { - private lateinit var gson: Gson - private lateinit var argType: Type - private lateinit var traceType: Type + private lateinit var gson: Gson + private lateinit var argType: Type + private lateinit var traceType: Type - override fun write(writer: JsonWriter, - value: SafetyResult, Trace>) { - initGson() - writer.beginObject() - writer.name("arg") - gson.toJson(gson.toJsonTree(value.witness), writer) - writer.name("stats") -// gson.toJson(gson.toJsonTree(value.stats), writer) - gson.toJson(gson.toJsonTree(Optional.empty()), writer) - if (value.isSafe) { - writer.name("safe").value(true) - } else { - val unsafe = value.asUnsafe() - writer.name("safe").value(false) - writer.name("trace") - gson.toJson(gson.toJsonTree(unsafe.cex), writer) - } - writer.endObject() + override fun write( + writer: JsonWriter, + value: SafetyResult, Trace>, + ) { + initGson() + writer.beginObject() + writer.name("arg") + gson.toJson(gson.toJsonTree(value.proof), writer) + writer.name("stats") + // gson.toJson(gson.toJsonTree(value.stats), writer) + gson.toJson(gson.toJsonTree(Optional.empty()), writer) + if (value.isSafe) { + writer.name("safe").value(true) + } else { + val unsafe = value.asUnsafe() + writer.name("safe").value(false) + writer.name("trace") + gson.toJson(gson.toJsonTree(unsafe.cex), writer) } + writer.endObject() + } - override fun read(reader: JsonReader): SafetyResult, Trace> { - initGson() - initTypes() - lateinit var arg: ARG - lateinit var stats: Optional - var safe: Boolean? = null - lateinit var trace: Trace - reader.beginObject() - while (reader.peek() != JsonToken.END_OBJECT) { - when (reader.nextName()) { - "arg" -> arg = gson.fromJson(reader, argType) - "stats" -> stats = gson.fromJson(reader, Optional::class.java) - "safe" -> safe = reader.nextBoolean() - "trace" -> trace = gson.fromJson(reader, traceType) - } - } - reader.endObject() - return if (stats.isEmpty) - if (safe == true) SafetyResult.safe(arg) else SafetyResult.unsafe(trace, arg) - else - if (safe == false) SafetyResult.safe(arg, stats.get()) else SafetyResult.unsafe(trace, - arg, stats.get()) + override fun read( + reader: JsonReader + ): SafetyResult, Trace> { + initGson() + initTypes() + lateinit var arg: ARG + lateinit var stats: Optional + var safe: Boolean? = null + lateinit var trace: Trace + reader.beginObject() + while (reader.peek() != JsonToken.END_OBJECT) { + when (reader.nextName()) { + "arg" -> arg = gson.fromJson(reader, argType) + "stats" -> stats = gson.fromJson(reader, Optional::class.java) + "safe" -> safe = reader.nextBoolean() + "trace" -> trace = gson.fromJson(reader, traceType) + } } + reader.endObject() + return if (stats.isEmpty) + if (safe == true) SafetyResult.safe(arg) else SafetyResult.unsafe(trace, arg) + else if (safe == false) SafetyResult.safe(arg, stats.get()) + else SafetyResult.unsafe(trace, arg, stats.get()) + } - private fun initGson() { - if (!this::gson.isInitialized) gson = gsonSupplier() - } + private fun initGson() { + if (!this::gson.isInitialized) gson = gsonSupplier() + } - private fun initTypes() { - if (!this::traceType.isInitialized) traceType = traceTypeSupplier() - if (!this::argType.isInitialized) argType = argTypeSupplier() - } -} \ No newline at end of file + private fun initTypes() { + if (!this::traceType.isInitialized) traceType = traceTypeSupplier() + if (!this::argType.isInitialized) argType = argTypeSupplier() + } +} diff --git a/subprojects/sts/sts-analysis/src/test/java/hu/bme/mit/theta/sts/analysis/StsExplTest.java b/subprojects/sts/sts-analysis/src/test/java/hu/bme/mit/theta/sts/analysis/StsExplTest.java index 4f2f998af5..f6609fdc97 100644 --- a/subprojects/sts/sts-analysis/src/test/java/hu/bme/mit/theta/sts/analysis/StsExplTest.java +++ b/subprojects/sts/sts-analysis/src/test/java/hu/bme/mit/theta/sts/analysis/StsExplTest.java @@ -15,18 +15,25 @@ */ package hu.bme.mit.theta.sts.analysis; +import static hu.bme.mit.theta.analysis.algorithm.arg.ArgUtils.isWellLabeled; +import static hu.bme.mit.theta.core.decl.Decls.Var; +import static hu.bme.mit.theta.core.type.anytype.Exprs.Prime; +import static hu.bme.mit.theta.core.type.booltype.BoolExprs.*; +import static hu.bme.mit.theta.core.type.inttype.IntExprs.*; +import static org.junit.Assert.assertTrue; + import hu.bme.mit.theta.analysis.Analysis; import hu.bme.mit.theta.analysis.LTS; import hu.bme.mit.theta.analysis.State; import hu.bme.mit.theta.analysis.Trace; +import hu.bme.mit.theta.analysis.algorithm.SafetyChecker; import hu.bme.mit.theta.analysis.algorithm.SafetyResult; import hu.bme.mit.theta.analysis.algorithm.arg.ARG; import hu.bme.mit.theta.analysis.algorithm.arg.ArgBuilder; import hu.bme.mit.theta.analysis.algorithm.arg.ArgNodeComparators; -import hu.bme.mit.theta.analysis.algorithm.SafetyChecker; import hu.bme.mit.theta.analysis.algorithm.cegar.ArgAbstractor; -import hu.bme.mit.theta.analysis.algorithm.cegar.BasicArgAbstractor; import hu.bme.mit.theta.analysis.algorithm.cegar.ArgCegarChecker; +import hu.bme.mit.theta.analysis.algorithm.cegar.BasicArgAbstractor; import hu.bme.mit.theta.analysis.expl.ExplAnalysis; import hu.bme.mit.theta.analysis.expl.ExplPrec; import hu.bme.mit.theta.analysis.expl.ExplState; @@ -34,12 +41,7 @@ import hu.bme.mit.theta.analysis.expr.ExprAction; import hu.bme.mit.theta.analysis.expr.ExprState; import hu.bme.mit.theta.analysis.expr.ExprStatePredicate; -import hu.bme.mit.theta.analysis.expr.refinement.ExprTraceChecker; -import hu.bme.mit.theta.analysis.expr.refinement.ExprTraceUnsatCoreChecker; -import hu.bme.mit.theta.analysis.expr.refinement.JoiningPrecRefiner; -import hu.bme.mit.theta.analysis.expr.refinement.PruneStrategy; -import hu.bme.mit.theta.analysis.expr.refinement.SingleExprTraceRefiner; -import hu.bme.mit.theta.analysis.expr.refinement.VarsRefutation; +import hu.bme.mit.theta.analysis.expr.refinement.*; import hu.bme.mit.theta.analysis.waitlist.PriorityWaitlist; import hu.bme.mit.theta.common.logging.ConsoleLogger; import hu.bme.mit.theta.common.logging.Logger; @@ -52,23 +54,9 @@ import hu.bme.mit.theta.solver.z3legacy.Z3LegacySolverFactory; import hu.bme.mit.theta.sts.STS; import hu.bme.mit.theta.sts.STS.Builder; -import org.junit.Test; - import java.util.Collections; import java.util.function.Predicate; - -import static hu.bme.mit.theta.analysis.algorithm.arg.ArgUtils.isWellLabeled; -import static hu.bme.mit.theta.core.decl.Decls.Var; -import static hu.bme.mit.theta.core.type.anytype.Exprs.Prime; -import static hu.bme.mit.theta.core.type.booltype.BoolExprs.And; -import static hu.bme.mit.theta.core.type.booltype.BoolExprs.Imply; -import static hu.bme.mit.theta.core.type.booltype.BoolExprs.Not; -import static hu.bme.mit.theta.core.type.inttype.IntExprs.Add; -import static hu.bme.mit.theta.core.type.inttype.IntExprs.Eq; -import static hu.bme.mit.theta.core.type.inttype.IntExprs.Geq; -import static hu.bme.mit.theta.core.type.inttype.IntExprs.Int; -import static hu.bme.mit.theta.core.type.inttype.IntExprs.Lt; -import static org.junit.Assert.assertTrue; +import org.junit.Test; public class StsExplTest { @@ -88,8 +76,10 @@ public void test() { builder.addInit(Eq(x, Int(0))); builder.addInit(Eq(y, Int(0))); - builder.addTrans(And(Imply(Lt(x, Int(mod)), Eq(Prime(x), Add(x, Int(1)))), - Imply(Geq(x, Int(mod)), Eq(Prime(x), Int(0))))); + builder.addTrans( + And( + Imply(Lt(x, Int(mod)), Eq(Prime(x), Add(x, Int(1)))), + Imply(Geq(x, Int(mod)), Eq(Prime(x), Int(0))))); builder.addTrans(Eq(Prime(y), Int(0))); builder.setProp(Not(Eq(x, Int(mod)))); @@ -98,40 +88,45 @@ public void test() { final Solver abstractionSolver = Z3LegacySolverFactory.getInstance().createSolver(); final UCSolver refinementSolver = Z3LegacySolverFactory.getInstance().createUCSolver(); - final Analysis analysis = ExplAnalysis.create( - abstractionSolver, sts.getInit()); - final Predicate target = new ExprStatePredicate(Not(sts.getProp()), - abstractionSolver); + final Analysis analysis = + ExplAnalysis.create(abstractionSolver, sts.getInit()); + final Predicate target = + new ExprStatePredicate(Not(sts.getProp()), abstractionSolver); final ExplPrec prec = ExplPrec.of(Collections.singleton(vy)); final LTS lts = StsLts.create(sts); - final ArgBuilder argBuilder = ArgBuilder.create(lts, - analysis, target); + final ArgBuilder argBuilder = + ArgBuilder.create(lts, analysis, target); - final ArgAbstractor abstractor = BasicArgAbstractor.builder( - argBuilder) - .waitlist(PriorityWaitlist.create(ArgNodeComparators.bfs())).logger(logger).build(); + final ArgAbstractor abstractor = + BasicArgAbstractor.builder(argBuilder) + .waitlist(PriorityWaitlist.create(ArgNodeComparators.bfs())) + .logger(logger) + .build(); - final ExprTraceChecker exprTraceChecker = ExprTraceUnsatCoreChecker.create( - sts.getInit(), - Not(sts.getProp()), refinementSolver); + final ExprTraceChecker exprTraceChecker = + ExprTraceUnsatCoreChecker.create( + sts.getInit(), Not(sts.getProp()), refinementSolver); - final SingleExprTraceRefiner refiner = SingleExprTraceRefiner - .create(exprTraceChecker, JoiningPrecRefiner.create(new VarsRefToExplPrec()), - PruneStrategy.LAZY, logger); + final SingleExprTraceRefiner refiner = + SingleExprTraceRefiner.create( + exprTraceChecker, + JoiningPrecRefiner.create(new VarsRefToExplPrec()), + PruneStrategy.LAZY, + logger); - final SafetyChecker, Trace, ExplPrec> checker = ArgCegarChecker.create( - abstractor, refiner, logger); + final SafetyChecker, Trace, ExplPrec> + checker = ArgCegarChecker.create(abstractor, refiner, logger); - final SafetyResult, Trace> safetyStatus = checker.check(prec); + final SafetyResult, Trace> safetyStatus = + checker.check(prec); - final ARG arg = safetyStatus.getWitness(); + final ARG arg = safetyStatus.getProof(); assertTrue(isWellLabeled(arg, abstractionSolver)); // System.out.println(new // GraphvizWriter().writeString(ArgVisualizer.visualize(arg))); } - } diff --git a/subprojects/sts/sts-analysis/src/test/java/hu/bme/mit/theta/sts/analysis/StsMddCheckerTest.java b/subprojects/sts/sts-analysis/src/test/java/hu/bme/mit/theta/sts/analysis/StsMddCheckerTest.java index e9f88faaad..929a01e400 100644 --- a/subprojects/sts/sts-analysis/src/test/java/hu/bme/mit/theta/sts/analysis/StsMddCheckerTest.java +++ b/subprojects/sts/sts-analysis/src/test/java/hu/bme/mit/theta/sts/analysis/StsMddCheckerTest.java @@ -15,11 +15,13 @@ */ package hu.bme.mit.theta.sts.analysis; +import static org.junit.Assert.assertTrue; + import hu.bme.mit.theta.analysis.algorithm.SafetyResult; import hu.bme.mit.theta.analysis.algorithm.mdd.MddCex; import hu.bme.mit.theta.analysis.algorithm.mdd.MddChecker; import hu.bme.mit.theta.analysis.algorithm.mdd.MddChecker.IterationStrategy; -import hu.bme.mit.theta.analysis.algorithm.mdd.MddWitness; +import hu.bme.mit.theta.analysis.algorithm.mdd.MddProof; import hu.bme.mit.theta.analysis.expr.ExprAction; import hu.bme.mit.theta.common.Utils; import hu.bme.mit.theta.common.logging.ConsoleLogger; @@ -35,16 +37,12 @@ import hu.bme.mit.theta.sts.aiger.AigerToSts; import hu.bme.mit.theta.sts.dsl.StsDslManager; import hu.bme.mit.theta.sts.dsl.StsSpec; -import org.junit.Test; -import org.junit.runner.RunWith; -import org.junit.runners.Parameterized; - import java.io.FileInputStream; -import java.io.IOException; import java.util.Arrays; import java.util.Collection; - -import static org.junit.Assert.assertTrue; +import org.junit.Test; +import org.junit.runner.RunWith; +import org.junit.runners.Parameterized; @RunWith(value = Parameterized.class) public class StsMddCheckerTest { @@ -56,35 +54,23 @@ public class StsMddCheckerTest { @Parameterized.Parameters(name = "{index}: {0}, {1}") public static Collection data() { - return Arrays.asList(new Object[][]{ - {"src/test/resources/hw1_false.aag", false}, - - {"src/test/resources/hw2_true.aag", true}, - - {"src/test/resources/boolean1.system", false}, - - {"src/test/resources/boolean2.system", false}, - - {"src/test/resources/counter.system", true}, - - {"src/test/resources/counter_bad.system", false}, - - {"src/test/resources/counter_parametric.system", true}, - - {"src/test/resources/loop.system", true}, - - {"src/test/resources/loop_bad.system", false}, - - {"src/test/resources/multipleinitial.system", false}, - - {"src/test/resources/readerswriters.system", true}, - - {"src/test/resources/simple1.system", false}, - - {"src/test/resources/simple2.system", true}, - - {"src/test/resources/simple3.system", false}, - }); + return Arrays.asList( + new Object[][] { + {"src/test/resources/hw1_false.aag", false}, + {"src/test/resources/hw2_true.aag", true}, + {"src/test/resources/boolean1.system", false}, + {"src/test/resources/boolean2.system", false}, + {"src/test/resources/counter.system", true}, + {"src/test/resources/counter_bad.system", false}, + {"src/test/resources/counter_parametric.system", true}, + {"src/test/resources/loop.system", true}, + {"src/test/resources/loop_bad.system", false}, + {"src/test/resources/multipleinitial.system", false}, + {"src/test/resources/readerswriters.system", true}, + {"src/test/resources/simple1.system", false}, + {"src/test/resources/simple2.system", true}, + {"src/test/resources/simple3.system", false}, + }); } @Test @@ -100,19 +86,27 @@ public void test() throws Exception { sts = Utils.singleElementOf(spec.getAllSts()); } - final SafetyResult status; + final SafetyResult status; try (var solverPool = new SolverPool(Z3LegacySolverFactory.getInstance())) { - final MddChecker checker = MddChecker.create(sts.getInit(), VarIndexingFactory.indexing(0), new ExprAction() { - @Override - public Expr toExpr() { - return sts.getTrans(); - } - - @Override - public VarIndexing nextIndexing() { - return VarIndexingFactory.indexing(1); - } - }, sts.getProp(), solverPool, logger, IterationStrategy.GSAT); + final MddChecker checker = + MddChecker.create( + sts.getInit(), + VarIndexingFactory.indexing(0), + new ExprAction() { + @Override + public Expr toExpr() { + return sts.getTrans(); + } + + @Override + public VarIndexing nextIndexing() { + return VarIndexingFactory.indexing(1); + } + }, + sts.getProp(), + solverPool, + logger, + IterationStrategy.GSAT); status = checker.check(null); } @@ -122,5 +116,4 @@ public VarIndexing nextIndexing() { assertTrue(status.isUnsafe()); } } - } diff --git a/subprojects/sts/sts-analysis/src/test/java/hu/bme/mit/theta/sts/analysis/StsPredTest.java b/subprojects/sts/sts-analysis/src/test/java/hu/bme/mit/theta/sts/analysis/StsPredTest.java index bed9497f54..5022d36401 100644 --- a/subprojects/sts/sts-analysis/src/test/java/hu/bme/mit/theta/sts/analysis/StsPredTest.java +++ b/subprojects/sts/sts-analysis/src/test/java/hu/bme/mit/theta/sts/analysis/StsPredTest.java @@ -18,53 +18,40 @@ import static hu.bme.mit.theta.analysis.algorithm.arg.ArgUtils.isWellLabeled; import static hu.bme.mit.theta.core.decl.Decls.Var; import static hu.bme.mit.theta.core.type.anytype.Exprs.Prime; -import static hu.bme.mit.theta.core.type.booltype.BoolExprs.And; -import static hu.bme.mit.theta.core.type.booltype.BoolExprs.Imply; -import static hu.bme.mit.theta.core.type.booltype.BoolExprs.Not; -import static hu.bme.mit.theta.core.type.inttype.IntExprs.Add; -import static hu.bme.mit.theta.core.type.inttype.IntExprs.Eq; -import static hu.bme.mit.theta.core.type.inttype.IntExprs.Geq; -import static hu.bme.mit.theta.core.type.inttype.IntExprs.Int; -import static hu.bme.mit.theta.core.type.inttype.IntExprs.Lt; +import static hu.bme.mit.theta.core.type.booltype.BoolExprs.*; +import static hu.bme.mit.theta.core.type.inttype.IntExprs.*; import static org.junit.Assert.assertTrue; -import java.util.function.Predicate; - -import hu.bme.mit.theta.analysis.Trace; -import hu.bme.mit.theta.analysis.algorithm.SafetyResult; -import hu.bme.mit.theta.analysis.expr.refinement.*; -import hu.bme.mit.theta.solver.ItpSolver; -import hu.bme.mit.theta.solver.Solver; -import org.junit.Before; -import org.junit.Test; - import hu.bme.mit.theta.analysis.Analysis; import hu.bme.mit.theta.analysis.LTS; import hu.bme.mit.theta.analysis.State; +import hu.bme.mit.theta.analysis.Trace; +import hu.bme.mit.theta.analysis.algorithm.SafetyChecker; +import hu.bme.mit.theta.analysis.algorithm.SafetyResult; import hu.bme.mit.theta.analysis.algorithm.arg.ARG; import hu.bme.mit.theta.analysis.algorithm.arg.ArgBuilder; -import hu.bme.mit.theta.analysis.algorithm.SafetyChecker; import hu.bme.mit.theta.analysis.algorithm.cegar.ArgAbstractor; -import hu.bme.mit.theta.analysis.algorithm.cegar.BasicArgAbstractor; import hu.bme.mit.theta.analysis.algorithm.cegar.ArgCegarChecker; +import hu.bme.mit.theta.analysis.algorithm.cegar.BasicArgAbstractor; import hu.bme.mit.theta.analysis.expr.ExprAction; import hu.bme.mit.theta.analysis.expr.ExprState; import hu.bme.mit.theta.analysis.expr.ExprStatePredicate; -import hu.bme.mit.theta.analysis.pred.ExprSplitters; -import hu.bme.mit.theta.analysis.pred.ItpRefToPredPrec; -import hu.bme.mit.theta.analysis.pred.PredAbstractors; -import hu.bme.mit.theta.analysis.pred.PredAnalysis; -import hu.bme.mit.theta.analysis.pred.PredPrec; -import hu.bme.mit.theta.analysis.pred.PredState; +import hu.bme.mit.theta.analysis.expr.refinement.*; +import hu.bme.mit.theta.analysis.pred.*; import hu.bme.mit.theta.common.logging.ConsoleLogger; import hu.bme.mit.theta.common.logging.Logger; import hu.bme.mit.theta.common.logging.Logger.Level; import hu.bme.mit.theta.core.decl.VarDecl; import hu.bme.mit.theta.core.type.Expr; import hu.bme.mit.theta.core.type.inttype.IntType; +import hu.bme.mit.theta.solver.ItpSolver; +import hu.bme.mit.theta.solver.Solver; import hu.bme.mit.theta.solver.z3legacy.Z3LegacySolverFactory; import hu.bme.mit.theta.sts.STS; import hu.bme.mit.theta.sts.STS.Builder; +import java.util.function.Predicate; +import org.junit.Before; +import org.junit.Test; public class StsPredTest { @@ -81,8 +68,10 @@ public void setUp() { final Builder builder = STS.builder(); builder.addInit(Eq(x, Int(0))); - builder.addTrans(And(Imply(Lt(x, Int(mod)), Eq(Prime(x), Add(x, Int(1)))), - Imply(Geq(x, Int(mod)), Eq(Prime(x), Int(0))))); + builder.addTrans( + And( + Imply(Lt(x, Int(mod)), Eq(Prime(x), Add(x, Int(1)))), + Imply(Geq(x, Int(mod)), Eq(Prime(x), Int(0))))); builder.setProp(Not(Eq(x, Int(mod)))); sts = builder.build(); @@ -91,39 +80,43 @@ public void setUp() { @Test public void testPredPrec() { - final Analysis analysis = PredAnalysis.create( - abstractionSolver, - PredAbstractors.booleanSplitAbstractor(abstractionSolver), sts.getInit()); - final Predicate target = new ExprStatePredicate(Not(sts.getProp()), - abstractionSolver); + final Analysis analysis = + PredAnalysis.create( + abstractionSolver, + PredAbstractors.booleanSplitAbstractor(abstractionSolver), + sts.getInit()); + final Predicate target = + new ExprStatePredicate(Not(sts.getProp()), abstractionSolver); final PredPrec prec = PredPrec.of(); final LTS lts = StsLts.create(sts); - final ArgBuilder argBuilder = ArgBuilder.create(lts, - analysis, target); + final ArgBuilder argBuilder = + ArgBuilder.create(lts, analysis, target); - final ArgAbstractor abstractor = BasicArgAbstractor.builder( - argBuilder).logger(logger) - .build(); + final ArgAbstractor abstractor = + BasicArgAbstractor.builder(argBuilder).logger(logger).build(); - final ExprTraceChecker exprTraceChecker = ExprTraceFwBinItpChecker.create( - sts.getInit(), - Not(sts.getProp()), refinementSolver); + final ExprTraceChecker exprTraceChecker = + ExprTraceFwBinItpChecker.create( + sts.getInit(), Not(sts.getProp()), refinementSolver); - final SingleExprTraceRefiner refiner = SingleExprTraceRefiner - .create(exprTraceChecker, + final SingleExprTraceRefiner refiner = + SingleExprTraceRefiner.create( + exprTraceChecker, JoiningPrecRefiner.create(new ItpRefToPredPrec(ExprSplitters.atoms())), - PruneStrategy.LAZY, logger); + PruneStrategy.LAZY, + logger); - final SafetyChecker, Trace, PredPrec> checker = ArgCegarChecker.create( - abstractor, refiner, logger); + final SafetyChecker, Trace, PredPrec> + checker = ArgCegarChecker.create(abstractor, refiner, logger); - final SafetyResult, Trace> safetyStatus = checker.check(prec); + final SafetyResult, Trace> safetyStatus = + checker.check(prec); System.out.println(safetyStatus); - final ARG arg = safetyStatus.getWitness(); + final ARG arg = safetyStatus.getProof(); assertTrue(isWellLabeled(arg, abstractionSolver)); // System.out.println(new 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 ddb48470eb..884bfabdae 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 @@ -52,26 +52,14 @@ import hu.bme.mit.theta.sts.analysis.StsTraceConcretizer; import hu.bme.mit.theta.sts.analysis.config.StsConfig; import hu.bme.mit.theta.sts.analysis.config.StsConfigBuilder; -import hu.bme.mit.theta.sts.analysis.config.StsConfigBuilder.Domain; -import hu.bme.mit.theta.sts.analysis.config.StsConfigBuilder.InitPrec; -import hu.bme.mit.theta.sts.analysis.config.StsConfigBuilder.PredSplit; -import hu.bme.mit.theta.sts.analysis.config.StsConfigBuilder.Refinement; -import hu.bme.mit.theta.sts.analysis.config.StsConfigBuilder.Search; +import hu.bme.mit.theta.sts.analysis.config.StsConfigBuilder.*; import hu.bme.mit.theta.sts.dsl.StsDslManager; import hu.bme.mit.theta.sts.dsl.StsSpec; - -import java.io.File; -import java.io.FileInputStream; -import java.io.FileNotFoundException; -import java.io.InputStream; -import java.io.PrintWriter; -import java.io.StringWriter; +import java.io.*; import java.util.concurrent.TimeUnit; import java.util.stream.Stream; -/** - * A command line interface for running a CEGAR configuration on an STS. - */ +/** A command line interface for running a CEGAR configuration on an STS. */ public class StsCli { private static final String JAR_NAME = "theta-sts-cli.jar"; @@ -85,41 +73,64 @@ enum Algorithm { IMC } - @Parameter(names = {"--domain"}, description = "Abstract domain") + @Parameter( + names = {"--domain"}, + description = "Abstract domain") Domain domain = Domain.PRED_CART; - @Parameter(names = {"--algorithm"}, description = "Algorithm") + @Parameter( + names = {"--algorithm"}, + description = "Algorithm") Algorithm algorithm = Algorithm.CEGAR; - @Parameter(names = {"--refinement"}, description = "Refinement strategy") + @Parameter( + names = {"--refinement"}, + description = "Refinement strategy") Refinement refinement = Refinement.SEQ_ITP; - @Parameter(names = {"--search"}, description = "Search strategy") + @Parameter( + names = {"--search"}, + description = "Search strategy") Search search = Search.BFS; - @Parameter(names = {"--predsplit"}, description = "Predicate splitting") + @Parameter( + names = {"--predsplit"}, + description = "Predicate splitting") PredSplit predSplit = PredSplit.WHOLE; - @Parameter(names = {"--model"}, description = "Path of the input STS model", required = true) + @Parameter( + names = {"--model"}, + description = "Path of the input STS model", + required = true) String model; - @Parameter(names = {"--initprec"}, description = "Initial precision") + @Parameter( + names = {"--initprec"}, + description = "Initial precision") InitPrec initPrec = InitPrec.EMPTY; - @Parameter(names = "--prunestrategy", description = "Strategy for pruning the ARG after refinement") + @Parameter( + names = "--prunestrategy", + description = "Strategy for pruning the ARG after refinement") PruneStrategy pruneStrategy = PruneStrategy.LAZY; - @Parameter(names = {"--loglevel"}, description = "Detailedness of logging") + @Parameter( + names = {"--loglevel"}, + description = "Detailedness of logging") Logger.Level logLevel = Level.SUBSTEP; - @Parameter(names = {"--benchmark"}, description = "Benchmark mode (only print metrics)") + @Parameter( + names = {"--benchmark"}, + description = "Benchmark mode (only print metrics)") Boolean benchmarkMode = false; @Parameter(names = "--cex", description = "Write concrete counterexample to a file") String cexfile = null; - @Parameter(names = { - "--header"}, description = "Print only a header (for benchmarks)", help = true) + @Parameter( + names = {"--header"}, + description = "Print only a header (for benchmarks)", + help = true) boolean headerOnly = false; @Parameter(names = "--stacktrace", description = "Print full stack trace in case of exception") @@ -169,11 +180,15 @@ private void run() { if (algorithm.equals(Algorithm.CEGAR)) { final StsConfig configuration = buildConfiguration(sts); status = check(configuration); - } else if (algorithm == Algorithm.BMC || algorithm == Algorithm.KINDUCTION || algorithm == Algorithm.IMC) { - final BoundedChecker checker = buildBoundedChecker(sts, Z3LegacySolverFactory.getInstance()); + } else if (algorithm == Algorithm.BMC + || algorithm == Algorithm.KINDUCTION + || algorithm == Algorithm.IMC) { + final BoundedChecker checker = + buildBoundedChecker(sts, Z3LegacySolverFactory.getInstance()); status = checker.check(null); } else { - throw new UnsupportedOperationException("Algorithm " + algorithm + " not supported"); + throw new UnsupportedOperationException( + "Algorithm " + algorithm + " not supported"); } sw.stop(); printResult(status, sts, sw.elapsed(TimeUnit.MILLISECONDS)); @@ -186,20 +201,35 @@ private void run() { } } - private SafetyResult, ? extends Trace> check(StsConfig configuration) throws Exception { + private SafetyResult, ? extends Trace> check( + StsConfig configuration) throws Exception { try { return configuration.check(); } catch (final Exception ex) { String message = ex.getMessage() == null ? "(no message)" : ex.getMessage(); throw new Exception( - "Error while running algorithm: " + ex.getClass().getSimpleName() + " " + message, + "Error while running algorithm: " + + ex.getClass().getSimpleName() + + " " + + message, ex); } } private void printHeader() { - Stream.of("Result", "TimeMs", "AlgoTimeMs", "AbsTimeMs", "RefTimeMs", "Iterations", - "ArgSize", "ArgDepth", "ArgMeanBranchFactor", "CexLen", "Vars", "Size") + Stream.of( + "Result", + "TimeMs", + "AlgoTimeMs", + "AbsTimeMs", + "RefTimeMs", + "Iterations", + "ArgSize", + "ArgDepth", + "ArgMeanBranchFactor", + "CexLen", + "Vars", + "Size") .forEach(writer::cell); writer.newRow(); } @@ -228,49 +258,64 @@ private STS loadModel() throws Exception { private StsConfig buildConfiguration(final STS sts) throws Exception { try { return new StsConfigBuilder(domain, refinement, Z3LegacySolverFactory.getInstance()) - .initPrec(initPrec).search(search) - .predSplit(predSplit).pruneStrategy(pruneStrategy).logger(logger).build(sts); + .initPrec(initPrec) + .search(search) + .predSplit(predSplit) + .pruneStrategy(pruneStrategy) + .logger(logger) + .build(sts); } catch (final Exception ex) { throw new Exception("Could not create configuration: " + ex.getMessage(), ex); } } - private BoundedChecker buildBoundedChecker(final STS sts, final SolverFactory abstractionSolverFactory) { + private BoundedChecker buildBoundedChecker( + final STS sts, final SolverFactory abstractionSolverFactory) { final MonolithicExpr monolithicExpr = StsToMonolithicExprKt.toMonolithicExpr(sts); final BoundedChecker checker; switch (algorithm) { - case BMC -> checker = BoundedCheckerBuilderKt.buildBMC( - monolithicExpr, - abstractionSolverFactory.createSolver(), - val -> StsToMonolithicExprKt.valToState(sts, val), - (val1, val2) -> StsToMonolithicExprKt.valToAction(sts, val1, val2), - logger - ); - case KINDUCTION -> checker = BoundedCheckerBuilderKt.buildKIND( - monolithicExpr, - abstractionSolverFactory.createSolver(), - abstractionSolverFactory.createSolver(), - val -> StsToMonolithicExprKt.valToState(sts, val), - (val1, val2) -> StsToMonolithicExprKt.valToAction(sts, val1, val2), - logger - ); - case IMC -> checker = BoundedCheckerBuilderKt.buildIMC( - monolithicExpr, - abstractionSolverFactory.createSolver(), - abstractionSolverFactory.createItpSolver(), - val -> StsToMonolithicExprKt.valToState(sts, val), - (val1, val2) -> StsToMonolithicExprKt.valToAction(sts, val1, val2), - logger - ); + case BMC -> + checker = + BoundedCheckerBuilderKt.buildBMC( + monolithicExpr, + abstractionSolverFactory.createSolver(), + val -> StsToMonolithicExprKt.valToState(sts, val), + (val1, val2) -> + StsToMonolithicExprKt.valToAction(sts, val1, val2), + logger); + case KINDUCTION -> + checker = + BoundedCheckerBuilderKt.buildKIND( + monolithicExpr, + abstractionSolverFactory.createSolver(), + abstractionSolverFactory.createSolver(), + val -> StsToMonolithicExprKt.valToState(sts, val), + (val1, val2) -> + StsToMonolithicExprKt.valToAction(sts, val1, val2), + logger); + case IMC -> + checker = + BoundedCheckerBuilderKt.buildIMC( + monolithicExpr, + abstractionSolverFactory.createSolver(), + abstractionSolverFactory.createItpSolver(), + val -> StsToMonolithicExprKt.valToState(sts, val), + (val1, val2) -> + StsToMonolithicExprKt.valToAction(sts, val1, val2), + logger); default -> - throw new UnsupportedOperationException("Algorithm " + algorithm + " not supported"); + throw new UnsupportedOperationException( + "Algorithm " + algorithm + " not supported"); } return checker; } - private void printResult(final SafetyResult> status, final STS sts, - final long totalTimeMs) { - final CegarStatistics stats = (CegarStatistics) status.getStats().orElse(new CegarStatistics(0, 0, 0, 0)); + private void printResult( + final SafetyResult> status, + final STS sts, + final long totalTimeMs) { + final CegarStatistics stats = + (CegarStatistics) status.getStats().orElse(new CegarStatistics(0, 0, 0, 0)); if (benchmarkMode) { writer.cell(status.isSafe()); writer.cell(totalTimeMs); @@ -278,7 +323,7 @@ private void printResult(final SafetyResult> status, fi writer.cell(stats.getAbstractorTimeMs()); writer.cell(stats.getRefinerTimeMs()); writer.cell(stats.getIterations()); - if (status.getWitness() instanceof ARG arg) { + if (status.getProof() instanceof ARG arg) { writer.cell(arg.size()); writer.cell(arg.getDepth()); writer.cell(arg.getMeanBranchingFactor()); @@ -304,7 +349,10 @@ private void printError(final Throwable ex) { writer.cell("[EX] " + ex.getClass().getSimpleName() + ": " + message); writer.newRow(); } else { - logger.write(Level.RESULT, "%s occurred, message: %s%n", ex.getClass().getSimpleName(), + logger.write( + Level.RESULT, + "%s occurred, message: %s%n", + ex.getClass().getSimpleName(), message); if (stacktrace) { final StringWriter errors = new StringWriter(); @@ -318,9 +366,10 @@ private void printError(final Throwable ex) { private void writeCex(final STS sts, final SafetyResult.Unsafe> status) throws FileNotFoundException { - @SuppressWarnings("unchecked") final Trace trace = (Trace) status.getCex(); - final Trace concrTrace = StsTraceConcretizer.concretize(sts, trace, - Z3LegacySolverFactory.getInstance()); + @SuppressWarnings("unchecked") + final Trace trace = (Trace) status.getCex(); + final Trace concrTrace = + StsTraceConcretizer.concretize(sts, trace, Z3LegacySolverFactory.getInstance()); final File file = new File(cexfile); PrintWriter printWriter = null; try { diff --git a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/oc/XcfaOcChecker.kt b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/oc/XcfaOcChecker.kt index 6ffa9bc1fb..72f7a2520e 100644 --- a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/oc/XcfaOcChecker.kt +++ b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/oc/XcfaOcChecker.kt @@ -13,15 +13,12 @@ * See the License for the specific language governing permissions and * limitations under the License. */ - package hu.bme.mit.theta.xcfa.analysis.oc -import hu.bme.mit.theta.analysis.EmptyCex import hu.bme.mit.theta.analysis.Trace -import hu.bme.mit.theta.analysis.algorithm.EmptyWitness +import hu.bme.mit.theta.analysis.algorithm.EmptyProof import hu.bme.mit.theta.analysis.algorithm.SafetyChecker import hu.bme.mit.theta.analysis.algorithm.SafetyResult -import hu.bme.mit.theta.analysis.algorithm.arg.ARG import hu.bme.mit.theta.analysis.algorithm.oc.EventType import hu.bme.mit.theta.analysis.algorithm.oc.OcChecker import hu.bme.mit.theta.analysis.algorithm.oc.Relation @@ -52,335 +49,363 @@ import hu.bme.mit.theta.xcfa.passes.AssumeFalseRemovalPass import hu.bme.mit.theta.xcfa.passes.AtomicReadsOneWritePass import hu.bme.mit.theta.xcfa.passes.MutexToVarPass -private val Expr<*>.vars get() = ExprUtils.getVars(this) +private val Expr<*>.vars + get() = ExprUtils.getVars(this) -class XcfaOcChecker(xcfa: XCFA, decisionProcedure: OcDecisionProcedureType, private val logger: Logger) : - SafetyChecker>, XcfaAction>, XcfaPrec> { +class XcfaOcChecker( + xcfa: XCFA, + decisionProcedure: OcDecisionProcedureType, + private val logger: Logger, +) : SafetyChecker>, XcfaAction>, XcfaPrec> { - private val ocChecker: OcChecker = decisionProcedure.checker() - private val solver = ocChecker.solver + private val ocChecker: OcChecker = decisionProcedure.checker() + private val solver = ocChecker.solver - private val xcfa: XCFA = xcfa.optimizeFurther( - listOf(AssumeFalseRemovalPass(), MutexToVarPass(), AtomicReadsOneWritePass()) + private val xcfa: XCFA = + xcfa.optimizeFurther( + listOf(AssumeFalseRemovalPass(), MutexToVarPass(), AtomicReadsOneWritePass()) ) - private var indexing = VarIndexingFactory.indexing(0) - private val localVars = mutableMapOf, MutableMap>>() - - private val threads = mutableSetOf() - private val events = mutableMapOf, MutableMap>>() - private val violations = mutableListOf() // OR! - private val branchingConditions = mutableListOf>() - private val pos = mutableListOf() - private val rfs = mutableMapOf, MutableSet>() - - override fun check( - prec: XcfaPrec?): SafetyResult>, XcfaAction>> = let { - if (xcfa.initProcedures.size > 1) error("Multiple entry points are not supported by OC checker.") + private var indexing = VarIndexingFactory.indexing(0) + private val localVars = mutableMapOf, MutableMap>>() + + private val threads = mutableSetOf() + private val events = mutableMapOf, MutableMap>>() + private val violations = mutableListOf() // OR! + private val branchingConditions = mutableListOf>() + private val pos = mutableListOf() + private val rfs = mutableMapOf, MutableSet>() + + override fun check( + prec: XcfaPrec? + ): SafetyResult>, XcfaAction>> = + let { + if (xcfa.initProcedures.size > 1) + error("Multiple entry points are not supported by OC checker.") logger.write(Logger.Level.MAINSTEP, "Adding constraints...\n") xcfa.initProcedures.forEach { processThread(Thread(it.first)) } addCrossThreadRelations() - if (!addToSolver()) return@let SafetyResult.safe>, XcfaAction>>( - EmptyWitness.getInstance()) // no violations in the model + if (!addToSolver()) + return@let SafetyResult.safe>, XcfaAction>>( + EmptyProof.getInstance() + ) // no violations in the model logger.write(Logger.Level.MAINSTEP, "Start checking...\n") val status = ocChecker.check(events, pos, rfs) when { - status?.isUnsat == true -> SafetyResult.safe(EmptyWitness.getInstance()) - status?.isSat == true -> SafetyResult.unsafe( - XcfaOcTraceExtractor(xcfa, ocChecker, threads, events, violations, pos).trace, - EmptyWitness.getInstance() + status?.isUnsat == true -> SafetyResult.safe(EmptyProof.getInstance()) + status?.isSat == true -> + SafetyResult.unsafe( + XcfaOcTraceExtractor(xcfa, ocChecker, threads, events, violations, pos).trace, + EmptyProof.getInstance(), ) - else -> SafetyResult.unknown() + else -> SafetyResult.unknown() } - }.also { logger.write(Logger.Level.MAINSTEP, "OC checker result: $it\n") } - - private fun processThread(thread: Thread): List { - threads.add(thread) - val pid = thread.pid - var last = listOf() - var guard = setOf>() - lateinit var lastWrites: MutableMap, Set> - lateinit var edge: XcfaEdge - var inEdge = false - var atomicEntered: Boolean? = null - - val newEvent: (VarDecl<*>, EventType) -> List = { d, type -> - check(!inEdge || last.size == 1) - val decl = d.threadVar(pid) - val useLastClk = inEdge || atomicEntered == true - val e = - if (useLastClk) E(decl.getNewIndexed(), type, guard, pid, edge, last.first().clkId) - else E(decl.getNewIndexed(), type, guard, pid, edge) - last.forEach { po(it, e) } - inEdge = true - if (atomicEntered == false) atomicEntered = true - when (type) { - EventType.READ -> lastWrites[decl]?.forEach { rfs.add(RelationType.RF, it, e) } - EventType.WRITE -> lastWrites[decl] = setOf(e) - } - events[decl] = (events[decl] ?: mutableMapOf()).apply { - this[pid] = (this[pid] ?: mutableListOf()).apply { add(e) } - } - listOf(e) + } + .also { logger.write(Logger.Level.MAINSTEP, "OC checker result: $it\n") } + + private fun processThread(thread: Thread): List { + threads.add(thread) + val pid = thread.pid + var last = listOf() + var guard = setOf>() + lateinit var lastWrites: MutableMap, Set> + lateinit var edge: XcfaEdge + var inEdge = false + var atomicEntered: Boolean? = null + + val newEvent: (VarDecl<*>, EventType) -> List = { d, type -> + check(!inEdge || last.size == 1) + val decl = d.threadVar(pid) + val useLastClk = inEdge || atomicEntered == true + val e = + if (useLastClk) E(decl.getNewIndexed(), type, guard, pid, edge, last.first().clkId) + else E(decl.getNewIndexed(), type, guard, pid, edge) + last.forEach { po(it, e) } + inEdge = true + if (atomicEntered == false) atomicEntered = true + when (type) { + EventType.READ -> lastWrites[decl]?.forEach { rfs.add(RelationType.RF, it, e) } + EventType.WRITE -> lastWrites[decl] = setOf(e) + } + events[decl] = + (events[decl] ?: mutableMapOf()).apply { + this[pid] = (this[pid] ?: mutableListOf()).apply { add(e) } } + listOf(e) + } - val waitList = mutableSetOf() - val toVisit = mutableSetOf(SearchItem(thread.procedure.initLoc).apply { - guards.add(thread.guard) - thread.startEvent?.let { lastEvents.add(it) } - this.lastWrites.add(thread.lastWrites) - }) - val threads = mutableListOf() - - while (toVisit.isNotEmpty()) { - val current = toVisit.first() - toVisit.remove(current) - check(current.incoming == current.loc.incomingEdges.size) - check(current.incoming == current.guards.size || current.loc.initial) - // lastEvents intentionally skipped - check(current.incoming == current.lastWrites.size || current.loc.initial) - check(current.incoming == current.threadLookups.size) - check(current.incoming == current.atomics.size) - check(current.atomics.all { it == current.atomics.first() }) // bad pattern otherwise - - if (current.loc.error) { - val errorGuard = Or(current.lastEvents.map { it.guard.toAnd() }) - violations.add(Violation(current.loc, pid, errorGuard, current.lastEvents)) - continue - } - - if (current.loc.final) { - thread.finalEvents.addAll(current.lastEvents) + val waitList = mutableSetOf() + val toVisit = + mutableSetOf( + SearchItem(thread.procedure.initLoc).apply { + guards.add(thread.guard) + thread.startEvent?.let { lastEvents.add(it) } + this.lastWrites.add(thread.lastWrites) + } + ) + val threads = mutableListOf() + + while (toVisit.isNotEmpty()) { + val current = toVisit.first() + toVisit.remove(current) + check(current.incoming == current.loc.incomingEdges.size) + check(current.incoming == current.guards.size || current.loc.initial) + // lastEvents intentionally skipped + check(current.incoming == current.lastWrites.size || current.loc.initial) + check(current.incoming == current.threadLookups.size) + check(current.incoming == current.atomics.size) + check(current.atomics.all { it == current.atomics.first() }) // bad pattern otherwise + + if (current.loc.error) { + val errorGuard = Or(current.lastEvents.map { it.guard.toAnd() }) + violations.add(Violation(current.loc, pid, errorGuard, current.lastEvents)) + continue + } + + if (current.loc.final) { + thread.finalEvents.addAll(current.lastEvents) + } + + val mergedGuard = current.guards.toOrInSet() + val assumeConsts = mutableMapOf, MutableList>>() + + for (e in current.loc.outgoingEdges) { + edge = e + inEdge = false + last = current.lastEvents + // intersection of guards of incoming edges: + guard = mergedGuard + lastWrites = current.lastWrites.merge().toMutableMap() + val threadLookup = + current.threadLookups + .merge { s1, s2 -> + s1 + s2.filter { (guard2, _) -> s1.none { (guard1, _) -> guard1 == guard2 } } } + .toMutableMap() + var firstLabel = true + atomicEntered = current.atomics.firstOrNull() + + edge.getFlatLabels().forEach { label -> + if (label.references.isNotEmpty() || label.dereferences.isNotEmpty()) { + error("References not supported by OC checker.") + } + when (label) { + is StmtLabel -> { + when (val stmt = label.stmt) { + is AssignStmt<*> -> { + val consts = mutableMapOf, ConstDecl<*>>() + stmt.expr.vars.forEach { + last = newEvent(it, EventType.READ) + consts[it] = last.first().const + } + last = newEvent(stmt.varDecl, EventType.WRITE) + last.first().assignment = Eq(last.first().const.ref, stmt.expr.withConsts(consts)) + } - val mergedGuard = current.guards.toOrInSet() - val assumeConsts = mutableMapOf, MutableList>>() - - for (e in current.loc.outgoingEdges) { - edge = e - inEdge = false - last = current.lastEvents - // intersection of guards of incoming edges: - guard = mergedGuard - lastWrites = current.lastWrites.merge().toMutableMap() - val threadLookup = current.threadLookups.merge { s1, s2 -> - s1 + s2.filter { (guard2, _) -> s1.none { (guard1, _) -> guard1 == guard2 } } - }.toMutableMap() - var firstLabel = true - atomicEntered = current.atomics.firstOrNull() - - edge.getFlatLabels().forEach { label -> - if (label.references.isNotEmpty() || label.dereferences.isNotEmpty()) { - error("References not supported by OC checker.") - } - when (label) { - is StmtLabel -> { - when (val stmt = label.stmt) { - is AssignStmt<*> -> { - val consts = mutableMapOf, ConstDecl<*>>() - stmt.expr.vars.forEach { - last = newEvent(it, EventType.READ) - consts[it] = last.first().const - } - last = newEvent(stmt.varDecl, EventType.WRITE) - last.first().assignment = Eq(last.first().const.ref, stmt.expr.withConsts(consts)) - } - - is AssumeStmt -> { - val consts = stmt.cond.vars.associateWith { it.threadVar(pid).getNewIndexed(false) } - val condWithConsts = stmt.cond.withConsts(consts) - val asAssign = consts.size == 1 && consts.keys.first().threadVar(pid) !in lastWrites - if (edge.source.outgoingEdges.size > 1 || !asAssign) { - guard = guard + condWithConsts - if (firstLabel) { - consts.forEach { (v, c) -> - assumeConsts.getOrPut(v) { mutableListOf() }.add(c) - } - } - } - stmt.cond.vars.forEach { - last = newEvent(it, EventType.READ) - } - if (edge.source.outgoingEdges.size == 1 && asAssign) { - last.first().assignment = condWithConsts - } - } - - is HavocStmt<*> -> { - last = newEvent(stmt.varDecl, EventType.WRITE) - } - - else -> error("Unsupported statement type: $stmt") - } - } - - is StartLabel -> { - // TODO StartLabel params - if (label.name in thread.startHistory) { - error("Recursive thread start not supported by OC checker.") - } - val procedure = xcfa.procedures.find { it.name == label.name } - ?: error("Procedure not found: ${label.name}") - last = newEvent(label.pidVar, EventType.WRITE) - val pidVar = label.pidVar.threadVar(pid) - if (this.threads.any { it.pidVar == pidVar }) { - error("Using a pthread_t variable in multiple threads is not supported by OC checker.") - } - val newHistory = thread.startHistory + thread.procedure.name - val newThread = Thread(procedure, guard, pidVar, last.first(), newHistory, lastWrites) - last.first().assignment = Eq(last.first().const.ref, Int(newThread.pid)) - threadLookup[pidVar] = setOf(Pair(guard, newThread)) - processThread(newThread) - } - - is JoinLabel -> { - val incomingGuard = guard - val lastEvents = mutableListOf() - val joinGuards = mutableListOf>>() - threadLookup[label.pidVar.threadVar(pid)]?.forEach { (g, thread) -> - guard = incomingGuard + g + thread.finalEvents.map { it.guard }.toOrInSet() - val joinEvent = newEvent(label.pidVar, EventType.READ).first() - thread.finalEvents.forEach { final -> po(final, joinEvent) } - lastEvents.add(joinEvent) - joinGuards.add(guard) - } ?: error("Thread started in a different thread: not supported by OC checker.") - guard = joinGuards.toOrInSet() - last = lastEvents - } - - is FenceLabel -> { - if (label.labels.size > 1 || label.labels.firstOrNull()?.contains("ATOMIC") != true) { - error("Untransformed fence label: $label") - } - if (label.isAtomicBegin) atomicEntered = false - if (label.isAtomicEnd) atomicEntered = null - } - - is NopLabel -> {} - else -> error("Unsupported label type by OC checker: $label") + is AssumeStmt -> { + val consts = + stmt.cond.vars.associateWith { it.threadVar(pid).getNewIndexed(false) } + val condWithConsts = stmt.cond.withConsts(consts) + val asAssign = + consts.size == 1 && consts.keys.first().threadVar(pid) !in lastWrites + if (edge.source.outgoingEdges.size > 1 || !asAssign) { + guard = guard + condWithConsts + if (firstLabel) { + consts.forEach { (v, c) -> + assumeConsts.getOrPut(v) { mutableListOf() }.add(c) + } } - firstLabel = false + } + stmt.cond.vars.forEach { last = newEvent(it, EventType.READ) } + if (edge.source.outgoingEdges.size == 1 && asAssign) { + last.first().assignment = condWithConsts + } } - val searchItem = waitList.find { it.loc == edge.target } - ?: SearchItem(edge.target).apply { waitList.add(this) } - searchItem.guards.add(guard) - searchItem.lastEvents.addAll(last) - searchItem.lastWrites.add(lastWrites) - searchItem.threadLookups.add(threadLookup) - searchItem.atomics.add(atomicEntered) - searchItem.incoming++ - if (searchItem.incoming == searchItem.loc.incomingEdges.size) { - waitList.remove(searchItem) - toVisit.add(searchItem) + is HavocStmt<*> -> { + last = newEvent(stmt.varDecl, EventType.WRITE) } - } - if (current.loc.outgoingEdges.size > 1) { - for (e in current.loc.outgoingEdges) { - val first = e.getFlatLabels().first() - if (first !is StmtLabel || first.stmt !is AssumeStmt) { - error("Branching with non-assume labels not supported by OC checker.") - } - } - assumeConsts.forEach { (_, set) -> - for ((i1, v1) in set.withIndex()) - for ((i2, v2) in set.withIndex()) { - if (i1 == i2) break - branchingConditions.add(Eq(v1.ref, v2.ref)) - } - } + else -> error("Unsupported statement type: $stmt") + } } - } - if (waitList.isNotEmpty()) error("Loops and dangling edges not supported by OC checker.") - return threads - } + is StartLabel -> { + // TODO StartLabel params + if (label.name in thread.startHistory) { + error("Recursive thread start not supported by OC checker.") + } + val procedure = + xcfa.procedures.find { it.name == label.name } + ?: error("Procedure not found: ${label.name}") + last = newEvent(label.pidVar, EventType.WRITE) + val pidVar = label.pidVar.threadVar(pid) + if (this.threads.any { it.pidVar == pidVar }) { + error( + "Using a pthread_t variable in multiple threads is not supported by OC checker." + ) + } + val newHistory = thread.startHistory + thread.procedure.name + val newThread = Thread(procedure, guard, pidVar, last.first(), newHistory, lastWrites) + last.first().assignment = Eq(last.first().const.ref, Int(newThread.pid)) + threadLookup[pidVar] = setOf(Pair(guard, newThread)) + processThread(newThread) + } - private fun addCrossThreadRelations() { - for ((_, map) in events) - for ((pid1, list1) in map) - for ((pid2, list2) in map) - if (pid1 != pid2) - for (e1 in list1.filter { it.type == EventType.WRITE }) - for (e2 in list2.filter { it.type == EventType.READ }) - rfs.add(RelationType.RF, e1, e2) - } + is JoinLabel -> { + val incomingGuard = guard + val lastEvents = mutableListOf() + val joinGuards = mutableListOf>>() + threadLookup[label.pidVar.threadVar(pid)]?.forEach { (g, thread) -> + guard = incomingGuard + g + thread.finalEvents.map { it.guard }.toOrInSet() + val joinEvent = newEvent(label.pidVar, EventType.READ).first() + thread.finalEvents.forEach { final -> po(final, joinEvent) } + lastEvents.add(joinEvent) + joinGuards.add(guard) + } ?: error("Thread started in a different thread: not supported by OC checker.") + guard = joinGuards.toOrInSet() + last = lastEvents + } - private fun addToSolver(): Boolean { - if (violations.isEmpty()) return false + is FenceLabel -> { + if (label.labels.size > 1 || label.labels.firstOrNull()?.contains("ATOMIC") != true) { + error("Untransformed fence label: $label") + } + if (label.isAtomicBegin) atomicEntered = false + if (label.isAtomicEnd) atomicEntered = null + } - // Value assignment - events.values.flatMap { it.values.flatten() }.filter { it.assignment != null }.forEach { event -> - if (event.guard.isEmpty()) solver.add(event.assignment) - else solver.add(Imply(event.guardExpr, event.assignment)) + is NopLabel -> {} + else -> error("Unsupported label type by OC checker: $label") + } + firstLabel = false } - // Branching conditions - branchingConditions.forEach { solver.add(it) } - - // Property violation - solver.add(Or(violations.map { it.guard })) - - // RF - rfs.forEach { (_, list) -> - list.groupBy { it.to }.forEach { (event, rels) -> - rels.forEach { rel -> - solver.add( - Imply( - rel.declRef, - And(rel.from.guardExpr, rel.to.guardExpr, Eq(rel.from.const.ref, rel.to.const.ref)) - ) - ) // RF-Val - } - solver.add(Imply(event.guardExpr, Or(rels.map { it.declRef }))) // RF-Some - } + val searchItem = + waitList.find { it.loc == edge.target } + ?: SearchItem(edge.target).apply { waitList.add(this) } + searchItem.guards.add(guard) + searchItem.lastEvents.addAll(last) + searchItem.lastWrites.add(lastWrites) + searchItem.threadLookups.add(threadLookup) + searchItem.atomics.add(atomicEntered) + searchItem.incoming++ + if (searchItem.incoming == searchItem.loc.incomingEdges.size) { + waitList.remove(searchItem) + toVisit.add(searchItem) } - - return true - } - - // Utility functions - - private fun po(from: E?, to: E) { - from ?: return - pos.add(Relation(RelationType.PO, from, to)) + } + + if (current.loc.outgoingEdges.size > 1) { + for (e in current.loc.outgoingEdges) { + val first = e.getFlatLabels().first() + if (first !is StmtLabel || first.stmt !is AssumeStmt) { + error("Branching with non-assume labels not supported by OC checker.") + } + } + assumeConsts.forEach { (_, set) -> + for ((i1, v1) in set.withIndex()) for ((i2, v2) in set.withIndex()) { + if (i1 == i2) break + branchingConditions.add(Eq(v1.ref, v2.ref)) + } + } + } } - private fun List>>.merge(merge: (Set, Set) -> Set = { a, b -> a + b }) = - reduce(mapOf()) { acc, map -> - (acc.keys + map.keys).associateWith { k -> - val set1 = acc[k] ?: setOf() - val set2 = map[k] ?: setOf() - merge(set1, set2) - } + if (waitList.isNotEmpty()) error("Loops and dangling edges not supported by OC checker.") + return threads + } + + private fun addCrossThreadRelations() { + for ((_, map) in events) for ((pid1, list1) in map) for ((pid2, list2) in map) if (pid1 != pid2) + for (e1 in list1.filter { it.type == EventType.WRITE }) for (e2 in + list2.filter { it.type == EventType.READ }) rfs.add(RelationType.RF, e1, e2) + } + + private fun addToSolver(): Boolean { + if (violations.isEmpty()) return false + + // Value assignment + events.values + .flatMap { it.values.flatten() } + .filter { it.assignment != null } + .forEach { event -> + if (event.guard.isEmpty()) solver.add(event.assignment) + else solver.add(Imply(event.guardExpr, event.assignment)) + } + + // Branching conditions + branchingConditions.forEach { solver.add(it) } + + // Property violation + solver.add(Or(violations.map { it.guard })) + + // RF + rfs.forEach { (_, list) -> + list + .groupBy { it.to } + .forEach { (event, rels) -> + rels.forEach { rel -> + solver.add( + Imply( + rel.declRef, + And(rel.from.guardExpr, rel.to.guardExpr, Eq(rel.from.const.ref, rel.to.const.ref)), + ) + ) // RF-Val + } + solver.add(Imply(event.guardExpr, Or(rels.map { it.declRef }))) // RF-Some } + } - private inline fun Collection.reduce(default: T, operation: (T, T) -> T): T = - if (isEmpty()) default else reduce(operation) + return true + } + + // Utility functions + + private fun po(from: E?, to: E) { + from ?: return + pos.add(Relation(RelationType.PO, from, to)) + } + + private fun List>>.merge( + merge: (Set, Set) -> Set = { a, b -> a + b } + ) = + reduce(mapOf()) { acc, map -> + (acc.keys + map.keys).associateWith { k -> + val set1 = acc[k] ?: setOf() + val set2 = map[k] ?: setOf() + merge(set1, set2) + } + } - private fun MutableMap, MutableSet>.add(type: RelationType, from: E, to: E) = - getOrPut(from.const.varDecl) { mutableSetOf() }.add(Relation(type, from, to)) + private inline fun Collection.reduce(default: T, operation: (T, T) -> T): T = + if (isEmpty()) default else reduce(operation) - private fun Expr.withConsts(varToConst: Map, ConstDecl<*>>): Expr { - if (this is RefExpr) { - return varToConst[decl]?.ref?.let { cast(it, type) } ?: this - } - return map { it.withConsts(varToConst) } - } + private fun MutableMap, MutableSet>.add(type: RelationType, from: E, to: E) = + getOrPut(from.const.varDecl) { mutableSetOf() }.add(Relation(type, from, to)) - private fun VarDecl.threadVar(pid: Int): VarDecl = - if (xcfa.vars.none { it.wrappedVar == this && !it.threadLocal }) { // if not global var - cast(localVars.getOrPut(this) { mutableMapOf() }.getOrPut(pid) { - Decls.Var("t$pid::$name", type) - }, type) - } else this - - private fun VarDecl.getNewIndexed(increment: Boolean = true): IndexedConstDecl { - val constDecl = getConstDecl(indexing.get(this)) - if (increment) indexing = indexing.inc(this) - return constDecl + private fun Expr.withConsts(varToConst: Map, ConstDecl<*>>): Expr { + if (this is RefExpr) { + return varToConst[decl]?.ref?.let { cast(it, type) } ?: this } + return map { it.withConsts(varToConst) } + } + + private fun VarDecl.threadVar(pid: Int): VarDecl = + if (xcfa.vars.none { it.wrappedVar == this && !it.threadLocal }) { // if not global var + cast( + localVars + .getOrPut(this) { mutableMapOf() } + .getOrPut(pid) { Decls.Var("t$pid::$name", type) }, + type, + ) + } else this + + private fun VarDecl.getNewIndexed(increment: Boolean = true): IndexedConstDecl { + val constDecl = getConstDecl(indexing.get(this)) + if (increment) indexing = indexing.inc(this) + return constDecl + } } diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/ExecuteConfig.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/ExecuteConfig.kt index 9469c2eca3..c7027914fc 100644 --- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/ExecuteConfig.kt +++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/ExecuteConfig.kt @@ -13,7 +13,6 @@ * See the License for the specific language governing permissions and * limitations under the License. */ - package hu.bme.mit.theta.xcfa.cli import com.google.common.base.Stopwatch @@ -23,7 +22,7 @@ import hu.bme.mit.theta.analysis.Action import hu.bme.mit.theta.analysis.EmptyCex import hu.bme.mit.theta.analysis.State import hu.bme.mit.theta.analysis.Trace -import hu.bme.mit.theta.analysis.algorithm.EmptyWitness +import hu.bme.mit.theta.analysis.algorithm.EmptyProof import hu.bme.mit.theta.analysis.algorithm.SafetyResult import hu.bme.mit.theta.analysis.algorithm.arg.ARG import hu.bme.mit.theta.analysis.algorithm.arg.debug.ARGWebDebugger @@ -68,318 +67,379 @@ import java.util.concurrent.TimeUnit import kotlin.random.Random fun runConfig( - config: XcfaConfig<*, *>, logger: Logger, uniqueLogger: Logger, - throwDontExit: Boolean + config: XcfaConfig<*, *>, + logger: Logger, + uniqueLogger: Logger, + throwDontExit: Boolean, ): SafetyResult<*, *> { - propagateInputOptions(config, logger, uniqueLogger) + propagateInputOptions(config, logger, uniqueLogger) - registerAllSolverManagers(config.backendConfig.solverHome, logger) + registerAllSolverManagers(config.backendConfig.solverHome, logger) - validateInputOptions(config, logger, uniqueLogger) + validateInputOptions(config, logger, uniqueLogger) - val (xcfa, mcm, parseContext) = frontend(config, logger, uniqueLogger) + val (xcfa, mcm, parseContext) = frontend(config, logger, uniqueLogger) - preVerificationLogging(xcfa, mcm, parseContext, config, logger, uniqueLogger) + preVerificationLogging(xcfa, mcm, parseContext, config, logger, uniqueLogger) - val result = backend(xcfa, mcm, parseContext, config, logger, uniqueLogger, throwDontExit) + val result = backend(xcfa, mcm, parseContext, config, logger, uniqueLogger, throwDontExit) - postVerificationLogging(result, mcm, parseContext, config, logger, uniqueLogger) + postVerificationLogging(result, mcm, parseContext, config, logger, uniqueLogger) - return result + return result } - private fun propagateInputOptions(config: XcfaConfig<*, *>, logger: Logger, uniqueLogger: Logger) { - config.inputConfig.property = determineProperty(config, logger) - LbePass.level = config.frontendConfig.lbeLevel - StaticCoiPass.enabled = config.frontendConfig.staticCoi - if (config.backendConfig.backend == Backend.CEGAR) { - val cegarConfig = config.backendConfig.specConfig - cegarConfig as CegarConfig - val random = Random(cegarConfig.porRandomSeed) - XcfaSporLts.random = random - XcfaDporLts.random = random - } - if (config.debugConfig.argToFile) { - WebDebuggerLogger.enableWebDebuggerLogger() - WebDebuggerLogger.getInstance().setTitle(config.inputConfig.input?.name) - } - - LoopUnrollPass.UNROLL_LIMIT = config.frontendConfig.loopUnroll - LoopUnrollPass.FORCE_UNROLL_LIMIT = config.frontendConfig.forceUnroll - FetchExecuteWriteback.enabled = config.frontendConfig.enableFew - ARGWebDebugger.on = config.debugConfig.argdebug + config.inputConfig.property = determineProperty(config, logger) + LbePass.level = config.frontendConfig.lbeLevel + StaticCoiPass.enabled = config.frontendConfig.staticCoi + if (config.backendConfig.backend == Backend.CEGAR) { + val cegarConfig = config.backendConfig.specConfig + cegarConfig as CegarConfig + val random = Random(cegarConfig.porRandomSeed) + XcfaSporLts.random = random + XcfaDporLts.random = random + } + if (config.debugConfig.argToFile) { + WebDebuggerLogger.enableWebDebuggerLogger() + WebDebuggerLogger.getInstance().setTitle(config.inputConfig.input?.name) + } + + LoopUnrollPass.UNROLL_LIMIT = config.frontendConfig.loopUnroll + LoopUnrollPass.FORCE_UNROLL_LIMIT = config.frontendConfig.forceUnroll + FetchExecuteWriteback.enabled = config.frontendConfig.enableFew + ARGWebDebugger.on = config.debugConfig.argdebug } private fun validateInputOptions(config: XcfaConfig<*, *>, logger: Logger, uniqueLogger: Logger) { - rule("NoCoiWhenDataRace") { - config.backendConfig.backend == Backend.CEGAR && - (config.backendConfig.specConfig as? CegarConfig)?.coi != ConeOfInfluenceMode.NO_COI && - config.inputConfig.property == ErrorDetection.DATA_RACE - } - rule("NoAaporWhenDataRace") { - (config.backendConfig.specConfig as? CegarConfig)?.porLevel?.isAbstractionAware == true && - config.inputConfig.property == ErrorDetection.DATA_RACE - } - rule("DPORWithoutDFS") { - (config.backendConfig.specConfig as? CegarConfig)?.porLevel?.isDynamic == true && - (config.backendConfig.specConfig as? CegarConfig)?.abstractorConfig?.search != Search.DFS - } - rule("SensibleLoopUnrollLimits") { - config.frontendConfig.loopUnroll != -1 && config.frontendConfig.loopUnroll < config.frontendConfig.forceUnroll - } - rule("NoPredSplitUntilFixed(https://github.com/ftsrg/theta/issues/267)") { - (config.backendConfig.specConfig as? CegarConfig)?.abstractorConfig?.domain == Domain.PRED_SPLIT - } + rule("NoCoiWhenDataRace") { + config.backendConfig.backend == Backend.CEGAR && + (config.backendConfig.specConfig as? CegarConfig)?.coi != ConeOfInfluenceMode.NO_COI && + config.inputConfig.property == ErrorDetection.DATA_RACE + } + rule("NoAaporWhenDataRace") { + (config.backendConfig.specConfig as? CegarConfig)?.porLevel?.isAbstractionAware == true && + config.inputConfig.property == ErrorDetection.DATA_RACE + } + rule("DPORWithoutDFS") { + (config.backendConfig.specConfig as? CegarConfig)?.porLevel?.isDynamic == true && + (config.backendConfig.specConfig as? CegarConfig)?.abstractorConfig?.search != Search.DFS + } + rule("SensibleLoopUnrollLimits") { + config.frontendConfig.loopUnroll != -1 && + config.frontendConfig.loopUnroll < config.frontendConfig.forceUnroll + } + rule("NoPredSplitUntilFixed(https://github.com/ftsrg/theta/issues/267)") { + (config.backendConfig.specConfig as? CegarConfig)?.abstractorConfig?.domain == Domain.PRED_SPLIT + } } -fun frontend(config: XcfaConfig<*, *>, logger: Logger, uniqueLogger: Logger): Triple { - if (config.inputConfig.xcfaWCtx != null) { - val xcfa = config.inputConfig.xcfaWCtx!!.first - ConeOfInfluence = if (config.inputConfig.xcfaWCtx!!.third.multiThreading) { - XcfaCoiMultiThread(xcfa) - } else { - XcfaCoiSingleThread(xcfa) - } - return config.inputConfig.xcfaWCtx!! - } - - val stopwatch = Stopwatch.createStarted() - - val input = config.inputConfig.input!! - logger.write(Logger.Level.INFO, "Parsing the input $input as ${config.frontendConfig.inputType}\n") - - val parseContext = ParseContext() - - if (config.frontendConfig.inputType == InputType.C) { - val cConfig = config.frontendConfig.specConfig - cConfig as CFrontendConfig - parseContext.arithmetic = cConfig.arithmetic - parseContext.architecture = cConfig.architecture - } - - val xcfa = getXcfa(config, parseContext, logger, uniqueLogger) - - val mcm = if (config.inputConfig.catFile != null) { - CatDslManager.createMCM(config.inputConfig.catFile!!) +fun frontend( + config: XcfaConfig<*, *>, + logger: Logger, + uniqueLogger: Logger, +): Triple { + if (config.inputConfig.xcfaWCtx != null) { + val xcfa = config.inputConfig.xcfaWCtx!!.first + ConeOfInfluence = + if (config.inputConfig.xcfaWCtx!!.third.multiThreading) { + XcfaCoiMultiThread(xcfa) + } else { + XcfaCoiSingleThread(xcfa) + } + return config.inputConfig.xcfaWCtx!! + } + + val stopwatch = Stopwatch.createStarted() + + val input = config.inputConfig.input!! + logger.write( + Logger.Level.INFO, + "Parsing the input $input as ${config.frontendConfig.inputType}\n", + ) + + val parseContext = ParseContext() + + if (config.frontendConfig.inputType == InputType.C) { + val cConfig = config.frontendConfig.specConfig + cConfig as CFrontendConfig + parseContext.arithmetic = cConfig.arithmetic + parseContext.architecture = cConfig.architecture + } + + val xcfa = getXcfa(config, parseContext, logger, uniqueLogger) + + val mcm = + if (config.inputConfig.catFile != null) { + CatDslManager.createMCM(config.inputConfig.catFile!!) } else { - emptySet() - } - - ConeOfInfluence = if (parseContext.multiThreading) XcfaCoiMultiThread(xcfa) else XcfaCoiSingleThread(xcfa) - - if (parseContext.multiThreading && (config.backendConfig.specConfig as? CegarConfig)?.let { it.abstractorConfig.search == Search.ERR } == true) { - val cConfig = config.backendConfig.specConfig as CegarConfig - cConfig.abstractorConfig.search = Search.DFS - uniqueLogger.write(INFO, "Multithreaded program found, using DFS instead of ERR.") + emptySet() } - logger.write( - Logger.Level.INFO, "Frontend finished: ${xcfa.name} (in ${ + ConeOfInfluence = + if (parseContext.multiThreading) XcfaCoiMultiThread(xcfa) else XcfaCoiSingleThread(xcfa) + + if ( + parseContext.multiThreading && + (config.backendConfig.specConfig as? CegarConfig)?.let { + it.abstractorConfig.search == Search.ERR + } == true + ) { + val cConfig = config.backendConfig.specConfig as CegarConfig + cConfig.abstractorConfig.search = Search.DFS + uniqueLogger.write(INFO, "Multithreaded program found, using DFS instead of ERR.") + } + + logger.write( + Logger.Level.INFO, + "Frontend finished: ${xcfa.name} (in ${ stopwatch.elapsed(TimeUnit.MILLISECONDS) - } ms)\n" - ) + } ms)\n", + ) - logger.write(RESULT, "ParsingResult Success\n") - logger.write(RESULT, - "Alias graph size: ${xcfa.pointsToGraph.size} -> ${xcfa.pointsToGraph.values.map { it.size }.toList()}\n") + logger.write(RESULT, "ParsingResult Success\n") + logger.write( + RESULT, + "Alias graph size: ${xcfa.pointsToGraph.size} -> ${xcfa.pointsToGraph.values.map { it.size }.toList()}\n", + ) - return Triple(xcfa, mcm, parseContext) + return Triple(xcfa, mcm, parseContext) } private fun backend( - xcfa: XCFA, mcm: MCM, parseContext: ParseContext, config: XcfaConfig<*, *>, - logger: Logger, - uniqueLogger: Logger, - throwDontExit: Boolean + xcfa: XCFA, + mcm: MCM, + parseContext: ParseContext, + config: XcfaConfig<*, *>, + logger: Logger, + uniqueLogger: Logger, + throwDontExit: Boolean, ): SafetyResult<*, *> = - if (config.backendConfig.backend == Backend.NONE) { - SafetyResult.unknown() + if (config.backendConfig.backend == Backend.NONE) { + SafetyResult.unknown() + } else { + if ( + xcfa.procedures.all { + it.errorLoc.isEmpty && config.inputConfig.property == ErrorDetection.ERROR_LOCATION + } + ) { + val result = SafetyResult.safe(EmptyProof.getInstance()) + logger.write(Logger.Level.INFO, "Input is trivially safe\n") + + logger.write(RESULT, result.toString() + "\n") + result } else { - if (xcfa.procedures.all { it.errorLoc.isEmpty && config.inputConfig.property == ErrorDetection.ERROR_LOCATION }) { - val result = SafetyResult.safe(EmptyWitness.getInstance()) - logger.write(Logger.Level.INFO, "Input is trivially safe\n") - - logger.write(RESULT, result.toString() + "\n") - result - } else { - val stopwatch = Stopwatch.createStarted() - - logger.write( - Logger.Level.INFO, - "Starting verification of ${if (xcfa.name == "") "UnnamedXcfa" else xcfa.name} using ${config.backendConfig.backend}\n" - ) - - val checker = getChecker(xcfa, mcm, config, parseContext, logger, uniqueLogger) - val result = exitOnError(config.debugConfig.stacktrace, config.debugConfig.debug || throwDontExit) { - checker.check() - }.let { result -> - when { - result.isSafe && LoopUnrollPass.FORCE_UNROLL_USED -> { // cannot report safe if force unroll was used - logger.write(RESULT, "Incomplete loop unroll used: safe result is unreliable.\n") - SafetyResult.unknown() - } - - else -> result - } + val stopwatch = Stopwatch.createStarted() + + logger.write( + Logger.Level.INFO, + "Starting verification of ${if (xcfa.name == "") "UnnamedXcfa" else xcfa.name} using ${config.backendConfig.backend}\n", + ) + + val checker = getChecker(xcfa, mcm, config, parseContext, logger, uniqueLogger) + val result = + exitOnError(config.debugConfig.stacktrace, config.debugConfig.debug || throwDontExit) { + checker.check() + } + .let { result -> + when { + result.isSafe && + LoopUnrollPass.FORCE_UNROLL_USED -> { // cannot report safe if force unroll was used + logger.write(RESULT, "Incomplete loop unroll used: safe result is unreliable.\n") + SafetyResult.unknown() + } + + else -> result } + } - logger.write( - Logger.Level.INFO, "Backend finished (in ${ + logger.write( + Logger.Level.INFO, + "Backend finished (in ${ stopwatch.elapsed(TimeUnit.MILLISECONDS) - } ms)\n" - ) + } ms)\n", + ) - logger.write(RESULT, result.toString() + "\n") - result - } + logger.write(RESULT, result.toString() + "\n") + result } + } private fun preVerificationLogging( - xcfa: XCFA, mcm: MCM, parseContext: ParseContext, config: XcfaConfig<*, *>, - logger: Logger, uniqueLogger: Logger + xcfa: XCFA, + mcm: MCM, + parseContext: ParseContext, + config: XcfaConfig<*, *>, + logger: Logger, + uniqueLogger: Logger, ) { - if (config.outputConfig.enableOutput) { - try { - val resultFolder = config.outputConfig.resultFolder - resultFolder.mkdirs() - - logger.write( - Logger.Level.INFO, - "Writing pre-verification artifacts to directory ${resultFolder.absolutePath}\n" - ) - - if (!config.outputConfig.chcOutputConfig.disable) { - xcfa.procedures.forEach { - try { - val chcFile = File(resultFolder, "xcfa-${it.name}.smt2") - chcFile.writeText(it.toSMT2CHC()) - } catch (e: Exception) { - logger.write(INFO, "Could not write CHC file: " + e.stackTraceToString()) - } - } - } + if (config.outputConfig.enableOutput) { + try { + val resultFolder = config.outputConfig.resultFolder + resultFolder.mkdirs() + + logger.write( + Logger.Level.INFO, + "Writing pre-verification artifacts to directory ${resultFolder.absolutePath}\n", + ) + + if (!config.outputConfig.chcOutputConfig.disable) { + xcfa.procedures.forEach { + try { + val chcFile = File(resultFolder, "xcfa-${it.name}.smt2") + chcFile.writeText(it.toSMT2CHC()) + } catch (e: Exception) { + logger.write(INFO, "Could not write CHC file: " + e.stackTraceToString()) + } + } + } - if (!config.outputConfig.xcfaOutputConfig.disable) { - val xcfaDotFile = File(resultFolder, "xcfa.dot") - xcfaDotFile.writeText(xcfa.toDot()) + if (!config.outputConfig.xcfaOutputConfig.disable) { + val xcfaDotFile = File(resultFolder, "xcfa.dot") + xcfaDotFile.writeText(xcfa.toDot()) - val xcfaJsonFile = File(resultFolder, "xcfa.json") - val uglyJson = getGson(xcfa).toJson(xcfa) - val create = GsonBuilder().setPrettyPrinting().create() - xcfaJsonFile.writeText(create.toJson(JsonParser.parseString(uglyJson))) - } + val xcfaJsonFile = File(resultFolder, "xcfa.json") + val uglyJson = getGson(xcfa).toJson(xcfa) + val create = GsonBuilder().setPrettyPrinting().create() + xcfaJsonFile.writeText(create.toJson(JsonParser.parseString(uglyJson))) + } - if (!config.outputConfig.cOutputConfig.disable) { - try { - val xcfaCFile = File(resultFolder, "xcfa.c") - xcfaCFile.writeText( - xcfa.toC( - parseContext, config.outputConfig.cOutputConfig.useArr, - config.outputConfig.cOutputConfig.useExArr, config.outputConfig.cOutputConfig.useRange - ) - ) - } catch (e: Throwable) { - logger.write(Logger.Level.VERBOSE, "Could not emit C file\n") - } - } + if (!config.outputConfig.cOutputConfig.disable) { + try { + val xcfaCFile = File(resultFolder, "xcfa.c") + xcfaCFile.writeText( + xcfa.toC( + parseContext, + config.outputConfig.cOutputConfig.useArr, + config.outputConfig.cOutputConfig.useExArr, + config.outputConfig.cOutputConfig.useRange, + ) + ) } catch (e: Throwable) { - logger.write(Logger.Level.INFO, "Could not output files: ${e.stackTraceToString()}\n") + logger.write(Logger.Level.VERBOSE, "Could not emit C file\n") } + } + } catch (e: Throwable) { + logger.write(Logger.Level.INFO, "Could not output files: ${e.stackTraceToString()}\n") } + } } private fun postVerificationLogging( - safetyResult: SafetyResult<*, *>, mcm: MCM, - parseContext: ParseContext, config: XcfaConfig<*, *>, logger: Logger, uniqueLogger: Logger + safetyResult: SafetyResult<*, *>, + mcm: MCM, + parseContext: ParseContext, + config: XcfaConfig<*, *>, + logger: Logger, + uniqueLogger: Logger, ) { - if (config.outputConfig.enableOutput) { - try { - // we only want to log the files if the current configuration is not --in-process or portfolio - if (config.backendConfig.inProcess || config.backendConfig.backend == Backend.PORTFOLIO) { - return - } - - val resultFolder = config.outputConfig.resultFolder - resultFolder.mkdirs() - - logger.write( - Logger.Level.INFO, - "Writing post-verification artifacts to directory ${resultFolder.absolutePath}\n" + if (config.outputConfig.enableOutput) { + try { + // we only want to log the files if the current configuration is not --in-process or portfolio + if (config.backendConfig.inProcess || config.backendConfig.backend == Backend.PORTFOLIO) { + return + } + + val resultFolder = config.outputConfig.resultFolder + resultFolder.mkdirs() + + logger.write( + Logger.Level.INFO, + "Writing post-verification artifacts to directory ${resultFolder.absolutePath}\n", + ) + + // TODO eliminate the need for the instanceof check + if ( + !config.outputConfig.argConfig.disable && safetyResult.proof is ARG? + ) { + val argFile = File(resultFolder, "arg-${safetyResult.isSafe}.dot") + val g: Graph = + ArgVisualizer.getDefault().visualize(safetyResult.proof as ARG?) + argFile.writeText(GraphvizWriter.getInstance().writeString(g)) + } + + if (!config.outputConfig.witnessConfig.disable) { + if ( + safetyResult.isUnsafe && + safetyResult.asUnsafe().cex != null && + !config.outputConfig.witnessConfig.svcomp + ) { + val concrTrace: Trace, XcfaAction> = + XcfaTraceConcretizer.concretize( + safetyResult.asUnsafe().cex as Trace>, XcfaAction>?, + getSolver( + config.outputConfig.witnessConfig.concretizerSolver, + config.outputConfig.witnessConfig.validateConcretizerSolver, + ), + parseContext, ) - // TODO eliminate the need for the instanceof check - if (!config.outputConfig.argConfig.disable && safetyResult.witness is ARG?) { - val argFile = File(resultFolder, "arg-${safetyResult.isSafe}.dot") - val g: Graph = ArgVisualizer.getDefault().visualize(safetyResult.witness as ARG?) - argFile.writeText(GraphvizWriter.getInstance().writeString(g)) - } - - if (!config.outputConfig.witnessConfig.disable) { - if (safetyResult.isUnsafe && safetyResult.asUnsafe().cex != null && !config.outputConfig.witnessConfig.svcomp) { - val concrTrace: Trace, XcfaAction> = XcfaTraceConcretizer.concretize( - safetyResult.asUnsafe().cex as Trace>, XcfaAction>?, - getSolver( - config.outputConfig.witnessConfig.concretizerSolver, - config.outputConfig.witnessConfig.validateConcretizerSolver - ), - parseContext - ) - - val traceFile = File(resultFolder, "trace.dot") - val traceG: Graph = TraceVisualizer.getDefault().visualize(concrTrace) - traceFile.writeText(GraphvizWriter.getInstance().writeString(traceG)) - - val sequenceFile = File(resultFolder, "trace.plantuml") - writeSequenceTrace(sequenceFile, - safetyResult.asUnsafe().cex as Trace, XcfaAction>) { (_, act) -> - act.label.getFlatLabels().map(XcfaLabel::toString) - } - - val optSequenceFile = File(resultFolder, "trace-optimized.plantuml") - writeSequenceTrace(optSequenceFile, concrTrace) { (_, act) -> - act.label.getFlatLabels().map(XcfaLabel::toString) - } - - val cSequenceFile = File(resultFolder, "trace-c.plantuml") - writeSequenceTrace(cSequenceFile, concrTrace) { (state, act) -> - val proc = state.processes[act.pid] - val loc = proc?.locs?.peek() - (loc?.metadata as? CMetaData)?.sourceText?.split("\n") ?: listOf("") - } - } - val witnessFile = File(resultFolder, "witness.graphml") - XcfaWitnessWriter().writeWitness( - safetyResult, config.inputConfig.input!!, - getSolver( - config.outputConfig.witnessConfig.concretizerSolver, - config.outputConfig.witnessConfig.validateConcretizerSolver - ), parseContext, witnessFile - ) - } - } catch (e: Throwable) { - logger.write(Logger.Level.INFO, "Could not output files: ${e.stackTraceToString()}\n") + val traceFile = File(resultFolder, "trace.dot") + val traceG: Graph = TraceVisualizer.getDefault().visualize(concrTrace) + traceFile.writeText(GraphvizWriter.getInstance().writeString(traceG)) + + val sequenceFile = File(resultFolder, "trace.plantuml") + writeSequenceTrace( + sequenceFile, + safetyResult.asUnsafe().cex as Trace, XcfaAction>, + ) { (_, act) -> + act.label.getFlatLabels().map(XcfaLabel::toString) + } + + val optSequenceFile = File(resultFolder, "trace-optimized.plantuml") + writeSequenceTrace(optSequenceFile, concrTrace) { (_, act) -> + act.label.getFlatLabels().map(XcfaLabel::toString) + } + + val cSequenceFile = File(resultFolder, "trace-c.plantuml") + writeSequenceTrace(cSequenceFile, concrTrace) { (state, act) -> + val proc = state.processes[act.pid] + val loc = proc?.locs?.peek() + (loc?.metadata as? CMetaData)?.sourceText?.split("\n") ?: listOf("") + } } + val witnessFile = File(resultFolder, "witness.graphml") + XcfaWitnessWriter() + .writeWitness( + safetyResult, + config.inputConfig.input!!, + getSolver( + config.outputConfig.witnessConfig.concretizerSolver, + config.outputConfig.witnessConfig.validateConcretizerSolver, + ), + parseContext, + witnessFile, + ) + } + } catch (e: Throwable) { + logger.write(Logger.Level.INFO, "Could not output files: ${e.stackTraceToString()}\n") } + } } -private fun writeSequenceTrace(sequenceFile: File, trace: Trace, XcfaAction>, - printer: (Pair, XcfaAction>) -> List) { - sequenceFile.writeText("@startuml\n") - var maxWidth = 0 - trace.actions.forEachIndexed { i, it -> - val stateBefore = trace.states[i] - sequenceFile.appendText("hnote over ${it.pid}\n") - val labelStrings = printer(Pair(stateBefore, it)) - if (maxWidth < (labelStrings.maxOfOrNull { it.length } ?: 0)) { - maxWidth = labelStrings.maxOfOrNull { it.length } ?: 0 - } - sequenceFile.appendText("${labelStrings.joinToString("\n")}\n") - sequenceFile.appendText("endhnote\n") +private fun writeSequenceTrace( + sequenceFile: File, + trace: Trace, XcfaAction>, + printer: (Pair, XcfaAction>) -> List, +) { + sequenceFile.writeText("@startuml\n") + var maxWidth = 0 + trace.actions.forEachIndexed { i, it -> + val stateBefore = trace.states[i] + sequenceFile.appendText("hnote over ${it.pid}\n") + val labelStrings = printer(Pair(stateBefore, it)) + if (maxWidth < (labelStrings.maxOfOrNull { it.length } ?: 0)) { + maxWidth = labelStrings.maxOfOrNull { it.length } ?: 0 } - trace.actions.map { it.pid }.distinct().reduce { acc, current -> - sequenceFile.appendText("$acc --> $current: \"${" ".repeat(maxWidth)}\"\n") - current + sequenceFile.appendText("${labelStrings.joinToString("\n")}\n") + sequenceFile.appendText("endhnote\n") + } + trace.actions + .map { it.pid } + .distinct() + .reduce { acc, current -> + sequenceFile.appendText("$acc --> $current: \"${" ".repeat(maxWidth)}\"\n") + current } - sequenceFile.appendText("@enduml\n") -} \ No newline at end of file + sequenceFile.appendText("@enduml\n") +} 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 18e0bd82ca..5825b0d922 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 @@ -13,11 +13,10 @@ * See the License for the specific language governing permissions and * limitations under the License. */ - package hu.bme.mit.theta.xcfa.cli.checkers import hu.bme.mit.theta.analysis.Trace -import hu.bme.mit.theta.analysis.algorithm.EmptyWitness +import hu.bme.mit.theta.analysis.algorithm.EmptyProof import hu.bme.mit.theta.analysis.algorithm.SafetyChecker import hu.bme.mit.theta.analysis.algorithm.bounded.BoundedChecker import hu.bme.mit.theta.analysis.ptr.PtrState @@ -30,35 +29,41 @@ import hu.bme.mit.theta.xcfa.cli.params.XcfaConfig import hu.bme.mit.theta.xcfa.cli.utils.getSolver import hu.bme.mit.theta.xcfa.model.XCFA -fun getBoundedChecker(xcfa: XCFA, mcm: MCM, - config: XcfaConfig<*, *>, - logger: Logger): SafetyChecker>, XcfaAction>, XcfaPrec<*>> { - - val boundedConfig = config.backendConfig.specConfig as BoundedConfig +fun getBoundedChecker( + xcfa: XCFA, + mcm: MCM, + config: XcfaConfig<*, *>, + logger: Logger, +): SafetyChecker>, XcfaAction>, XcfaPrec<*>> { - return BoundedChecker( - monolithicExpr = xcfa.toMonolithicExpr(), - bmcSolver = tryGetSolver(boundedConfig.bmcConfig.bmcSolver, - boundedConfig.bmcConfig.validateBMCSolver)?.createSolver(), - bmcEnabled = { !boundedConfig.bmcConfig.disable }, - lfPathOnly = { !boundedConfig.bmcConfig.nonLfPath }, - itpSolver = tryGetSolver(boundedConfig.itpConfig.itpSolver, - boundedConfig.itpConfig.validateItpSolver)?.createItpSolver(), - imcEnabled = { !boundedConfig.itpConfig.disable }, - indSolver = tryGetSolver(boundedConfig.indConfig.indSolver, - boundedConfig.indConfig.validateIndSolver)?.createSolver(), - kindEnabled = { !boundedConfig.indConfig.disable }, - valToState = { xcfa.valToState(it) }, - biValToAction = { val1, val2 -> xcfa.valToAction(val1, val2) }, - logger = logger - ) as SafetyChecker>, XcfaAction>, XcfaPrec<*>> + val boundedConfig = config.backendConfig.specConfig as BoundedConfig + return BoundedChecker( + monolithicExpr = xcfa.toMonolithicExpr(), + bmcSolver = + tryGetSolver(boundedConfig.bmcConfig.bmcSolver, boundedConfig.bmcConfig.validateBMCSolver) + ?.createSolver(), + bmcEnabled = { !boundedConfig.bmcConfig.disable }, + lfPathOnly = { !boundedConfig.bmcConfig.nonLfPath }, + itpSolver = + tryGetSolver(boundedConfig.itpConfig.itpSolver, boundedConfig.itpConfig.validateItpSolver) + ?.createItpSolver(), + imcEnabled = { !boundedConfig.itpConfig.disable }, + indSolver = + tryGetSolver(boundedConfig.indConfig.indSolver, boundedConfig.indConfig.validateIndSolver) + ?.createSolver(), + kindEnabled = { !boundedConfig.indConfig.disable }, + valToState = { xcfa.valToState(it) }, + biValToAction = { val1, val2 -> xcfa.valToAction(val1, val2) }, + logger = logger, + ) + as SafetyChecker>, XcfaAction>, XcfaPrec<*>> } private fun tryGetSolver(name: String, validate: Boolean): SolverFactory? { - try { - return getSolver(name, validate) - } catch (e: Throwable) { - return null - } -} \ No newline at end of file + try { + return getSolver(name, validate) + } catch (e: Throwable) { + return null + } +} diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToCegarChecker.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToCegarChecker.kt index f8bf86f8d2..25a81fdb2e 100644 --- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToCegarChecker.kt +++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToCegarChecker.kt @@ -13,16 +13,15 @@ * See the License for the specific language governing permissions and * limitations under the License. */ - package hu.bme.mit.theta.xcfa.cli.checkers import hu.bme.mit.theta.analysis.PartialOrd import hu.bme.mit.theta.analysis.Prec import hu.bme.mit.theta.analysis.Trace -import hu.bme.mit.theta.analysis.algorithm.arg.ArgNode import hu.bme.mit.theta.analysis.algorithm.SafetyChecker import hu.bme.mit.theta.analysis.algorithm.SafetyResult import hu.bme.mit.theta.analysis.algorithm.arg.ARG +import hu.bme.mit.theta.analysis.algorithm.arg.ArgNode import hu.bme.mit.theta.analysis.algorithm.cegar.ArgAbstractor import hu.bme.mit.theta.analysis.algorithm.cegar.ArgCegarChecker import hu.bme.mit.theta.analysis.algorithm.cegar.ArgRefiner @@ -44,109 +43,138 @@ import hu.bme.mit.theta.xcfa.cli.utils.getSolver import hu.bme.mit.theta.xcfa.model.XCFA fun getCegarChecker( - xcfa: XCFA, mcm: MCM, - config: XcfaConfig<*, *>, - logger: Logger -): SafetyChecker, XcfaAction>, Trace>, XcfaAction>, XcfaPrec<*>> { - val cegarConfig = config.backendConfig.specConfig as CegarConfig - val abstractionSolverFactory: SolverFactory = getSolver( - cegarConfig.abstractorConfig.abstractionSolver, - cegarConfig.abstractorConfig.validateAbstractionSolver + xcfa: XCFA, + mcm: MCM, + config: XcfaConfig<*, *>, + logger: Logger, +): SafetyChecker< + ARG, XcfaAction>, + Trace>, XcfaAction>, + XcfaPrec<*>, +> { + val cegarConfig = config.backendConfig.specConfig as CegarConfig + val abstractionSolverFactory: SolverFactory = + getSolver( + cegarConfig.abstractorConfig.abstractionSolver, + cegarConfig.abstractorConfig.validateAbstractionSolver, ) - val refinementSolverFactory: SolverFactory = getSolver( - cegarConfig.refinerConfig.refinementSolver, - cegarConfig.refinerConfig.validateRefinementSolver + val refinementSolverFactory: SolverFactory = + getSolver( + cegarConfig.refinerConfig.refinementSolver, + cegarConfig.refinerConfig.validateRefinementSolver, ) - val ignoredVarRegistry = mutableMapOf, MutableSet>() + val ignoredVarRegistry = mutableMapOf, MutableSet>() - val lts = cegarConfig.coi.getLts(xcfa, ignoredVarRegistry, cegarConfig.porLevel) - val waitlist = if (cegarConfig.porLevel.isDynamic) { - (cegarConfig.coi.porLts as XcfaDporLts).waitlist + val lts = cegarConfig.coi.getLts(xcfa, ignoredVarRegistry, cegarConfig.porLevel) + val waitlist = + if (cegarConfig.porLevel.isDynamic) { + (cegarConfig.coi.porLts as XcfaDporLts).waitlist } else { - PriorityWaitlist.create>, XcfaAction>>( - cegarConfig.abstractorConfig.search.getComp(xcfa) - ) + PriorityWaitlist.create>, XcfaAction>>( + cegarConfig.abstractorConfig.search.getComp(xcfa) + ) } - val abstractionSolverInstance = abstractionSolverFactory.createSolver() - val globalStatePartialOrd: PartialOrd> = cegarConfig.abstractorConfig.domain.partialOrd( - abstractionSolverInstance - ) as PartialOrd> - val corePartialOrd: PartialOrd>> = - if (xcfa.isInlined) getPartialOrder(globalStatePartialOrd) - else getStackPartialOrder(globalStatePartialOrd) - val abstractor: ArgAbstractor = cegarConfig.abstractorConfig.domain.abstractor( - xcfa, - abstractionSolverInstance, - cegarConfig.abstractorConfig.maxEnum, - waitlist, - cegarConfig.refinerConfig.refinement.stopCriterion, - logger, - lts, - config.inputConfig.property, - if (cegarConfig.porLevel.isDynamic) { - XcfaDporLts.getPartialOrder(corePartialOrd) - } else { - corePartialOrd - }, - cegarConfig.abstractorConfig.havocMemory + val abstractionSolverInstance = abstractionSolverFactory.createSolver() + val globalStatePartialOrd: PartialOrd> = + cegarConfig.abstractorConfig.domain.partialOrd(abstractionSolverInstance) + as PartialOrd> + val corePartialOrd: PartialOrd>> = + if (xcfa.isInlined) getPartialOrder(globalStatePartialOrd) + else getStackPartialOrder(globalStatePartialOrd) + val abstractor: ArgAbstractor = + cegarConfig.abstractorConfig.domain.abstractor( + xcfa, + abstractionSolverInstance, + cegarConfig.abstractorConfig.maxEnum, + waitlist, + cegarConfig.refinerConfig.refinement.stopCriterion, + logger, + lts, + config.inputConfig.property, + if (cegarConfig.porLevel.isDynamic) { + XcfaDporLts.getPartialOrder(corePartialOrd) + } else { + corePartialOrd + }, + cegarConfig.abstractorConfig.havocMemory, ) as ArgAbstractor - val ref: ExprTraceChecker = - cegarConfig.refinerConfig.refinement.refiner(refinementSolverFactory, cegarConfig.cexMonitor) - as ExprTraceChecker - val precRefiner: PrecRefiner = - cegarConfig.abstractorConfig.domain.itpPrecRefiner(cegarConfig.refinerConfig.exprSplitter.exprSplitter) - as PrecRefiner - val atomicNodePruner: NodePruner = - cegarConfig.abstractorConfig.domain.nodePruner as NodePruner - val refiner: ArgRefiner = - if (cegarConfig.refinerConfig.refinement == Refinement.MULTI_SEQ) - if (cegarConfig.porLevel == POR.AASPOR) - MultiExprTraceRefiner.create( - ref, precRefiner, cegarConfig.refinerConfig.pruneStrategy, logger, - atomicNodePruner - ) - else - MultiExprTraceRefiner.create(ref, precRefiner, cegarConfig.refinerConfig.pruneStrategy, logger) - else - if (cegarConfig.porLevel == POR.AASPOR) - XcfaSingleExprTraceRefiner.create( - ref, precRefiner, cegarConfig.refinerConfig.pruneStrategy, logger, - atomicNodePruner - ) - else - XcfaSingleExprTraceRefiner.create(ref, precRefiner, cegarConfig.refinerConfig.pruneStrategy, logger) - - val cegarChecker = if (cegarConfig.porLevel == POR.AASPOR) - ArgCegarChecker.create( - abstractor, - AasporRefiner.create(refiner, cegarConfig.refinerConfig.pruneStrategy, ignoredVarRegistry), - logger + val ref: ExprTraceChecker = + cegarConfig.refinerConfig.refinement.refiner(refinementSolverFactory, cegarConfig.cexMonitor) + as ExprTraceChecker + val precRefiner: PrecRefiner = + cegarConfig.abstractorConfig.domain.itpPrecRefiner( + cegarConfig.refinerConfig.exprSplitter.exprSplitter + ) as PrecRefiner + val atomicNodePruner: NodePruner = + cegarConfig.abstractorConfig.domain.nodePruner as NodePruner + val refiner: ArgRefiner = + if (cegarConfig.refinerConfig.refinement == Refinement.MULTI_SEQ) + if (cegarConfig.porLevel == POR.AASPOR) + MultiExprTraceRefiner.create( + ref, + precRefiner, + cegarConfig.refinerConfig.pruneStrategy, + logger, + atomicNodePruner, + ) + else + MultiExprTraceRefiner.create( + ref, + precRefiner, + cegarConfig.refinerConfig.pruneStrategy, + logger, ) + else if (cegarConfig.porLevel == POR.AASPOR) + XcfaSingleExprTraceRefiner.create( + ref, + precRefiner, + cegarConfig.refinerConfig.pruneStrategy, + logger, + atomicNodePruner, + ) else - ArgCegarChecker.create(abstractor, refiner, logger) + XcfaSingleExprTraceRefiner.create( + ref, + precRefiner, + cegarConfig.refinerConfig.pruneStrategy, + logger, + ) - // initialize monitors - MonitorCheckpoint.reset() - if (cegarConfig.cexMonitor == CexMonitorOptions.CHECK) { - val cm = CexMonitor(logger, cegarChecker.witness) - MonitorCheckpoint.register(cm, "CegarChecker.unsafeARG") - } + val cegarChecker = + if (cegarConfig.porLevel == POR.AASPOR) + ArgCegarChecker.create( + abstractor, + AasporRefiner.create(refiner, cegarConfig.refinerConfig.pruneStrategy, ignoredVarRegistry), + logger, + ) + else ArgCegarChecker.create(abstractor, refiner, logger) + + // initialize monitors + MonitorCheckpoint.reset() + if (cegarConfig.cexMonitor == CexMonitorOptions.CHECK) { + val cm = CexMonitor(logger, cegarChecker.proof) + MonitorCheckpoint.register(cm, "CegarChecker.unsafeARG") + } - return object : - SafetyChecker, XcfaAction>, Trace>, XcfaAction>, XcfaPrec<*>> { - override fun check( - prec: XcfaPrec<*>? - ): SafetyResult, XcfaAction>, Trace>, XcfaAction>> { - return cegarChecker.check( - prec - ) as SafetyResult, XcfaAction>, Trace>, XcfaAction>> - } + return object : + SafetyChecker< + ARG, XcfaAction>, + Trace>, XcfaAction>, + XcfaPrec<*>, + > { + override fun check( + prec: XcfaPrec<*>? + ): SafetyResult, XcfaAction>, Trace>, XcfaAction>> { + return cegarChecker.check(prec) + as SafetyResult, XcfaAction>, Trace>, XcfaAction>> + } - override fun check(): SafetyResult, XcfaAction>, Trace>, XcfaAction>> { - return check(cegarConfig.abstractorConfig.domain.initPrec(xcfa, cegarConfig.initPrec)) - } + override fun check(): + SafetyResult, XcfaAction>, Trace>, XcfaAction>> { + return check(cegarConfig.abstractorConfig.domain.initPrec(xcfa, cegarConfig.initPrec)) } -} \ No newline at end of file + } +} diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToHornChecker.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToHornChecker.kt index dd63b5eb48..a944126ace 100644 --- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToHornChecker.kt +++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToHornChecker.kt @@ -13,11 +13,10 @@ * See the License for the specific language governing permissions and * limitations under the License. */ - package hu.bme.mit.theta.xcfa.cli.checkers import hu.bme.mit.theta.analysis.Trace -import hu.bme.mit.theta.analysis.algorithm.EmptyWitness +import hu.bme.mit.theta.analysis.algorithm.EmptyProof import hu.bme.mit.theta.analysis.algorithm.SafetyChecker import hu.bme.mit.theta.analysis.algorithm.SafetyResult import hu.bme.mit.theta.analysis.algorithm.chc.HornChecker @@ -36,32 +35,37 @@ import hu.bme.mit.theta.xcfa.model.XCFA import hu.bme.mit.theta.xcfa2chc.toCHC import org.abego.treelayout.internal.util.Contract.checkState -fun getHornChecker(xcfa: XCFA, mcm: MCM, config: XcfaConfig<*, *>, logger: Logger): - SafetyChecker>, XcfaAction>, XcfaPrec<*>> { +fun getHornChecker( + xcfa: XCFA, + mcm: MCM, + config: XcfaConfig<*, *>, + logger: Logger, +): SafetyChecker>, XcfaAction>, XcfaPrec<*>> { - checkState(xcfa.isInlined, "Only inlined XCFAs work right now") - checkState(xcfa.initProcedures.size == 1, "Only one-procedure XCFAs work right now") + checkState(xcfa.isInlined, "Only inlined XCFAs work right now") + checkState(xcfa.initProcedures.size == 1, "Only one-procedure XCFAs work right now") - val hornConfig = config.backendConfig.specConfig as HornConfig + val hornConfig = config.backendConfig.specConfig as HornConfig - val checker = HornChecker( - relations = xcfa.initProcedures[0].first.toCHC(), - hornSolverFactory = getSolver(hornConfig.solver, hornConfig.validateSolver), - logger = logger, + val checker = + HornChecker( + relations = xcfa.initProcedures[0].first.toCHC(), + hornSolverFactory = getSolver(hornConfig.solver, hornConfig.validateSolver), + logger = logger, ) - return SafetyChecker>, XcfaAction>, XcfaPrec<*>> { - val result = checker.check(null) + return SafetyChecker>, XcfaAction>, XcfaPrec<*>> { + val result = checker.check(null) - if (result.isSafe) { - SafetyResult.safe(EmptyWitness.getInstance()) - } else if (result.isUnsafe) { - val proof = result.asUnsafe().cex - val state = XcfaState>(xcfa, mapOf(), PtrState(PredState.of(proof.proofNode.expr))) - SafetyResult.unsafe(Trace.of(listOf(state), listOf()), EmptyWitness.getInstance()) - } else { - SafetyResult.unknown() - } + if (result.isSafe) { + SafetyResult.safe(EmptyProof.getInstance()) + } else if (result.isUnsafe) { + val proof = result.asUnsafe().cex + val state = + XcfaState>(xcfa, mapOf(), PtrState(PredState.of(proof.proofNode.expr))) + SafetyResult.unsafe(Trace.of(listOf(state), listOf()), EmptyProof.getInstance()) + } else { + SafetyResult.unknown() } - -} \ No newline at end of file + } +} diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToOcChecker.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToOcChecker.kt index df14f6ee8f..d8e3fc76ff 100644 --- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToOcChecker.kt +++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToOcChecker.kt @@ -13,11 +13,10 @@ * See the License for the specific language governing permissions and * limitations under the License. */ - package hu.bme.mit.theta.xcfa.cli.checkers import hu.bme.mit.theta.analysis.Trace -import hu.bme.mit.theta.analysis.algorithm.EmptyWitness +import hu.bme.mit.theta.analysis.algorithm.EmptyProof import hu.bme.mit.theta.analysis.algorithm.SafetyChecker import hu.bme.mit.theta.analysis.algorithm.SafetyResult import hu.bme.mit.theta.analysis.ptr.PtrState @@ -31,14 +30,21 @@ import hu.bme.mit.theta.xcfa.cli.params.OcConfig import hu.bme.mit.theta.xcfa.cli.params.XcfaConfig import hu.bme.mit.theta.xcfa.model.XCFA -fun getOcChecker(xcfa: XCFA, mcm: MCM, - config: XcfaConfig<*, *>, - logger: Logger): SafetyChecker>, XcfaAction>, XcfaPrec<*>> { - val ocChecker = XcfaOcChecker(xcfa, (config.backendConfig.specConfig as OcConfig).decisionProcedure, logger) - return object : SafetyChecker>, XcfaAction>, XcfaPrec<*>> { - override fun check( - prec: XcfaPrec<*>?): SafetyResult>, XcfaAction>> = check() +fun getOcChecker( + xcfa: XCFA, + mcm: MCM, + config: XcfaConfig<*, *>, + logger: Logger, +): SafetyChecker>, XcfaAction>, XcfaPrec<*>> { + val ocChecker = + XcfaOcChecker(xcfa, (config.backendConfig.specConfig as OcConfig).decisionProcedure, logger) + return object : + SafetyChecker>, XcfaAction>, XcfaPrec<*>> { + override fun check( + prec: XcfaPrec<*>? + ): SafetyResult>, XcfaAction>> = check() - override fun check(): SafetyResult>, XcfaAction>> = ocChecker.check() - } -} \ No newline at end of file + override fun check(): SafetyResult>, XcfaAction>> = + ocChecker.check() + } +} diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/InProcessChecker.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/InProcessChecker.kt index a20d9a5aaf..193a062499 100644 --- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/InProcessChecker.kt +++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/InProcessChecker.kt @@ -13,17 +13,15 @@ * See the License for the specific language governing permissions and * limitations under the License. */ - package hu.bme.mit.theta.xcfa.cli.checkers import com.zaxxer.nuprocess.NuAbstractProcessHandler import com.zaxxer.nuprocess.NuProcess import com.zaxxer.nuprocess.NuProcessBuilder import hu.bme.mit.theta.analysis.EmptyCex -import hu.bme.mit.theta.analysis.algorithm.EmptyWitness +import hu.bme.mit.theta.analysis.algorithm.EmptyProof import hu.bme.mit.theta.analysis.algorithm.SafetyChecker import hu.bme.mit.theta.analysis.algorithm.SafetyResult -import hu.bme.mit.theta.analysis.ptr.PtrState import hu.bme.mit.theta.common.logging.Logger import hu.bme.mit.theta.frontend.ParseContext import hu.bme.mit.theta.xcfa.analysis.XcfaPrec @@ -40,47 +38,48 @@ import java.util.concurrent.TimeUnit import kotlin.io.path.createTempDirectory class InProcessChecker( - val xcfa: XCFA, - val config: XcfaConfig, - val parseContext: ParseContext, - val logger: Logger, -) : SafetyChecker> { - - override fun check( - prec: XcfaPrec<*>?): SafetyResult { - return check() - } - - override fun check(): SafetyResult { - val tempDir = createTempDirectory(config.outputConfig.resultFolder.toPath()) - - val xcfaJson = CachingFileSerializer.serialize("xcfa.json", xcfa) { getGson(xcfa).toJson(xcfa) } - val parseContextJson = CachingFileSerializer.serialize("parseContext.json", parseContext) { - getGson(xcfa).toJson(parseContext) - } - - val processConfig = config.copy( - inputConfig = config.inputConfig.copy( - input = xcfaJson, - parseCtx = parseContextJson, - ), - frontendConfig = config.frontendConfig.copy( - inputType = InputType.JSON - ), - backendConfig = config.backendConfig.copy(inProcess = false, timeoutMs = 0), - outputConfig = config.outputConfig.copy( - resultFolder = tempDir.toFile(), - cOutputConfig = COutputConfig(disable = true), - xcfaOutputConfig = XcfaOutputConfig(disable = true), - argConfig = config.outputConfig.argConfig.copy(disable = false), // we need the arg to be produced - ) - ) - - val configJson = CachingFileSerializer.serialize("config.json", processConfig) { - getGson(xcfa).toJson(processConfig) - } - - val pb = NuProcessBuilder(listOf( + val xcfa: XCFA, + val config: XcfaConfig, + val parseContext: ParseContext, + val logger: Logger, +) : SafetyChecker> { + + override fun check(prec: XcfaPrec<*>?): SafetyResult { + return check() + } + + override fun check(): SafetyResult { + val tempDir = createTempDirectory(config.outputConfig.resultFolder.toPath()) + + val xcfaJson = CachingFileSerializer.serialize("xcfa.json", xcfa) { getGson(xcfa).toJson(xcfa) } + val parseContextJson = + CachingFileSerializer.serialize("parseContext.json", parseContext) { + getGson(xcfa).toJson(parseContext) + } + + val processConfig = + config.copy( + inputConfig = config.inputConfig.copy(input = xcfaJson, parseCtx = parseContextJson), + frontendConfig = config.frontendConfig.copy(inputType = InputType.JSON), + backendConfig = config.backendConfig.copy(inProcess = false, timeoutMs = 0), + outputConfig = + config.outputConfig.copy( + resultFolder = tempDir.toFile(), + cOutputConfig = COutputConfig(disable = true), + xcfaOutputConfig = XcfaOutputConfig(disable = true), + argConfig = + config.outputConfig.argConfig.copy(disable = false), // we need the arg to be produced + ), + ) + + val configJson = + CachingFileSerializer.serialize("config.json", processConfig) { + getGson(xcfa).toJson(processConfig) + } + + val pb = + NuProcessBuilder( + listOf( ProcessHandle.current().info().command().orElse("java"), "-Xss120m", "-Xmx14210m", @@ -88,91 +87,94 @@ class InProcessChecker( File(XcfaCli::class.java.protectionDomain.codeSource.location.toURI()).absolutePath, XcfaCli::class.qualifiedName, "-c", - configJson.absolutePath - ).filterNotNull()) - val processHandler = ProcessHandler() - pb.setProcessListener(processHandler) - val process: NuProcess = pb.start() - pb.environment().putAll(System.getenv()) - - val retCode = process.waitFor(config.backendConfig.timeoutMs, TimeUnit.MILLISECONDS) - val booleanSafetyResult = - if (retCode == Int.MIN_VALUE) { - if (processHandler.safetyResult == null) { - process.destroy(true) - throw ErrorCodeException(ExitCodes.TIMEOUT.code) - } else { - logger.write(Logger.Level.RESULT, - "Config timed out but started writing result, trying to wait an additional 10%...") - val retCode = process.waitFor(config.backendConfig.timeoutMs / 10, TimeUnit.MILLISECONDS) - if (retCode != 0) { - throw ErrorCodeException(retCode) - } else { - processHandler.safetyResult - } - } - } else if (retCode != 0) { - throw ErrorCodeException(retCode) - } else { - processHandler.safetyResult - } - - tempDir.toFile().listFiles()?.forEach { - it.copyTo(config.outputConfig.resultFolder.resolve(it.name), overwrite = true) + configJson.absolutePath, + ) + .filterNotNull() + ) + val processHandler = ProcessHandler() + pb.setProcessListener(processHandler) + val process: NuProcess = pb.start() + pb.environment().putAll(System.getenv()) + + val retCode = process.waitFor(config.backendConfig.timeoutMs, TimeUnit.MILLISECONDS) + val booleanSafetyResult = + if (retCode == Int.MIN_VALUE) { + if (processHandler.safetyResult == null) { + process.destroy(true) + throw ErrorCodeException(ExitCodes.TIMEOUT.code) + } else { + logger.write( + Logger.Level.RESULT, + "Config timed out but started writing result, trying to wait an additional 10%...", + ) + val retCode = process.waitFor(config.backendConfig.timeoutMs / 10, TimeUnit.MILLISECONDS) + if (retCode != 0) { + throw ErrorCodeException(retCode) + } else { + processHandler.safetyResult + } } - tempDir.toFile().deleteRecursively() - - return booleanSafetyResult as SafetyResult + } else if (retCode != 0) { + throw ErrorCodeException(retCode) + } else { + processHandler.safetyResult + } + + tempDir.toFile().listFiles()?.forEach { + it.copyTo(config.outputConfig.resultFolder.resolve(it.name), overwrite = true) } + tempDir.toFile().deleteRecursively() - private class ProcessHandler : NuAbstractProcessHandler() { - - private val stdout = LinkedList() - private var stdoutRemainder = "" - private val stderr = LinkedList() - private var stderrRemainder = "" - var safetyResult: SafetyResult<*, *>? = null - private set - - override fun onStdout(buffer: ByteBuffer, closed: Boolean) { - if (!closed) { - val bytes = ByteArray(buffer.remaining()) - buffer[bytes] - val str = bytes.decodeToString() - - stdoutRemainder += str - if (stdoutRemainder.contains("SafetyResult Safe")) { - safetyResult = SafetyResult.safe(EmptyWitness.getInstance()) - } - if (stdoutRemainder.contains("SafetyResult Unsafe")) { - safetyResult = SafetyResult.unsafe(EmptyCex.getInstance(), EmptyWitness.getInstance()) - } - - val newLines = stdoutRemainder.split("\n") // if ends with \n, last element will be "" - newLines.subList(0, newLines.size - 1).forEach { - stdout.add(it) - println("server: $it") - } - stdoutRemainder = newLines[newLines.size - 1] - } + return booleanSafetyResult as SafetyResult + } + + private class ProcessHandler : NuAbstractProcessHandler() { + + private val stdout = LinkedList() + private var stdoutRemainder = "" + private val stderr = LinkedList() + private var stderrRemainder = "" + var safetyResult: SafetyResult<*, *>? = null + private set + + override fun onStdout(buffer: ByteBuffer, closed: Boolean) { + if (!closed) { + val bytes = ByteArray(buffer.remaining()) + buffer[bytes] + val str = bytes.decodeToString() + + stdoutRemainder += str + if (stdoutRemainder.contains("SafetyResult Safe")) { + safetyResult = SafetyResult.safe(EmptyProof.getInstance()) + } + if (stdoutRemainder.contains("SafetyResult Unsafe")) { + safetyResult = SafetyResult.unsafe(EmptyCex.getInstance(), EmptyProof.getInstance()) } - override fun onStderr(buffer: ByteBuffer, closed: Boolean) { - if (!closed) { - val bytes = ByteArray(buffer.remaining()) - buffer[bytes] - val str = bytes.decodeToString() - - stderrRemainder += str - - val newLines = stderrRemainder.split("\n") // if ends with \n, last element will be "" - newLines.subList(0, newLines.size - 1).forEach { - stderr.add(it) - err.println("server: $it") - } - stderrRemainder = newLines[newLines.size - 1] - } + val newLines = stdoutRemainder.split("\n") // if ends with \n, last element will be "" + newLines.subList(0, newLines.size - 1).forEach { + stdout.add(it) + println("server: $it") } + stdoutRemainder = newLines[newLines.size - 1] + } } -} \ No newline at end of file + override fun onStderr(buffer: ByteBuffer, closed: Boolean) { + if (!closed) { + val bytes = ByteArray(buffer.remaining()) + buffer[bytes] + val str = bytes.decodeToString() + + stderrRemainder += str + + val newLines = stderrRemainder.split("\n") // if ends with \n, last element will be "" + newLines.subList(0, newLines.size - 1).forEach { + stderr.add(it) + err.println("server: $it") + } + stderrRemainder = newLines[newLines.size - 1] + } + } + } +} diff --git a/subprojects/xcfa/xcfa-cli/src/test/java/hu/bme/mit/theta/xcfa/cli/XcfaCliProofTest.kt b/subprojects/xcfa/xcfa-cli/src/test/java/hu/bme/mit/theta/xcfa/cli/XcfaCliProofTest.kt new file mode 100644 index 0000000000..3d29c73fb0 --- /dev/null +++ b/subprojects/xcfa/xcfa-cli/src/test/java/hu/bme/mit/theta/xcfa/cli/XcfaCliProofTest.kt @@ -0,0 +1,136 @@ +/* + * 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 + +import hu.bme.mit.theta.xcfa.cli.XcfaCli.Companion.main +import java.util.stream.Stream +import kotlin.io.path.absolutePathString +import kotlin.io.path.createTempDirectory +import kotlin.io.path.exists +import org.junit.jupiter.api.Assertions +import org.junit.jupiter.params.ParameterizedTest +import org.junit.jupiter.params.provider.Arguments +import org.junit.jupiter.params.provider.MethodSource + +data class WitnessEdge( + val startlineRange: Pair?, + val endlineRange: Pair?, + val startoffsetRange: Pair?, + val endoffsetRange: Pair?, + val assumption: Regex?, +) + +class XcfaCliProofTest { + companion object { + + @JvmStatic + fun cFiles(): Stream { + return Stream.of( + Arguments.of( + "/c/litmustest/singlethread/witness_test.c", + null, + listOf( + WitnessEdge( + startlineRange = Pair(5, 5), + endlineRange = Pair(5, 5), + startoffsetRange = Pair(100, 130), + endoffsetRange = Pair(100, 130), + assumption = Regex("i *== *-1"), + ) + ), + ), + Arguments.of( + "/c/litmustest/singlethread/witness_test.c", + "--backend BOUNDED", + listOf( + WitnessEdge( + startlineRange = Pair(5, 5), + endlineRange = Pair(5, 5), + startoffsetRange = Pair(100, 130), + endoffsetRange = Pair(100, 130), + assumption = Regex("i *== *-1"), + ) + ), + ), + ) + } + } + + @ParameterizedTest + @MethodSource("cFiles") + fun testCWitness(filePath: String, extraArgs: String?, expectedWitnessEdges: List) { + val temp = createTempDirectory() + val params = + arrayOf( + "--enable-output", + "--input-type", + "C", + "--input", + javaClass.getResource(filePath)!!.path, + *(extraArgs?.split(" ")?.toTypedArray() ?: emptyArray()), + "--stacktrace", + "--output-directory", + temp.absolutePathString(), + "--debug", + ) + main(params) + Assertions.assertTrue(temp.resolve("witness.graphml").exists()) + val witnessContents = temp.resolve("witness.graphml").toFile().readText() + val edges = mutableListOf>() + val edgeMatcher = Regex("(?s)(.*)") + val data = mutableMapOf() + for (dataMatch in dataMatcher.findAll(match.value)) { + val (key, value) = dataMatch.destructured + data.put(key, value) + } + edges.add(data) + println( + "Found edge containing data: ${data.entries.map { "${it.key}: ${it.value}" }.joinToString(", ")}" + ) + } + for (expectedWitnessEdge in expectedWitnessEdges) { + Assertions.assertFalse( + edges.none { edge -> + val startline = + expectedWitnessEdge.startlineRange + ?.let { edge["startline"]?.let { v -> Pair(it, Integer.parseInt(v)) } } + ?.let { it.first.first <= it.second && it.second <= it.first.second } ?: false + val endline = + expectedWitnessEdge.endlineRange + ?.let { edge["endline"]?.let { v -> Pair(it, Integer.parseInt(v)) } } + ?.let { it.first.first <= it.second && it.second <= it.first.second } ?: false + val startoffset = + expectedWitnessEdge.startoffsetRange + ?.let { edge["startoffset"]?.let { v -> Pair(it, Integer.parseInt(v)) } } + ?.let { it.first.first <= it.second && it.second <= it.first.second } ?: false + val endoffset = + expectedWitnessEdge.endoffsetRange + ?.let { edge["endoffset"]?.let { v -> Pair(it, Integer.parseInt(v)) } } + ?.let { it.first.first <= it.second && it.second <= it.first.second } ?: false + val assumption = + expectedWitnessEdge.assumption + ?.let { edge["assumption"]?.let { v -> Pair(it, v) } } + ?.let { it.first.matches(it.second) } ?: false + startline && endline && startoffset && endoffset && assumption + }, + "Expected witness edge not found: $expectedWitnessEdge", + ) + } + temp.toFile().deleteRecursively() + } +} diff --git a/subprojects/xcfa/xcfa-cli/src/test/java/hu/bme/mit/theta/xcfa/cli/XcfaCliWitnessTest.kt b/subprojects/xcfa/xcfa-cli/src/test/java/hu/bme/mit/theta/xcfa/cli/XcfaCliWitnessTest.kt deleted file mode 100644 index bc5657f5ba..0000000000 --- a/subprojects/xcfa/xcfa-cli/src/test/java/hu/bme/mit/theta/xcfa/cli/XcfaCliWitnessTest.kt +++ /dev/null @@ -1,130 +0,0 @@ -/* - * 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 - -import hu.bme.mit.theta.xcfa.cli.XcfaCli.Companion.main -import org.junit.jupiter.api.Assertions -import org.junit.jupiter.params.ParameterizedTest -import org.junit.jupiter.params.provider.Arguments -import org.junit.jupiter.params.provider.MethodSource -import java.util.stream.Stream -import kotlin.io.path.absolutePathString -import kotlin.io.path.createTempDirectory -import kotlin.io.path.exists - -data class WitnessEdge( - val startlineRange: Pair?, - val endlineRange: Pair?, - val startoffsetRange: Pair?, - val endoffsetRange: Pair?, - val assumption: Regex?, -) - -class XcfaCliWitnessTest { - companion object { - - @JvmStatic - fun cFiles(): Stream { - return Stream.of( - Arguments.of("/c/litmustest/singlethread/witness_test.c", null, listOf( - WitnessEdge( - startlineRange = Pair(5, 5), - endlineRange = Pair(5, 5), - startoffsetRange = Pair(100, 130), - endoffsetRange = Pair(100, 130), - assumption = Regex("i *== *-1"), - ), - )), - Arguments.of("/c/litmustest/singlethread/witness_test.c", "--backend BOUNDED", listOf( - WitnessEdge( - startlineRange = Pair(5, 5), - endlineRange = Pair(5, 5), - startoffsetRange = Pair(100, 130), - endoffsetRange = Pair(100, 130), - assumption = Regex("i *== *-1"), - ), - )), - ) - } - - } - - @ParameterizedTest - @MethodSource("cFiles") - fun testCWitness(filePath: String, extraArgs: String?, expectedWitnessEdges: List) { - val temp = createTempDirectory() - val params = arrayOf( - "--enable-output", - "--input-type", "C", - "--input", javaClass.getResource(filePath)!!.path, - *(extraArgs?.split(" ")?.toTypedArray() ?: emptyArray()), - "--stacktrace", - "--output-directory", temp.absolutePathString(), - "--debug", - ) - main(params) - Assertions.assertTrue(temp.resolve("witness.graphml").exists()) - val witnessContents = temp.resolve("witness.graphml").toFile().readText() - val edges = mutableListOf>() - val edgeMatcher = Regex("(?s)(.*)") - val data = mutableMapOf() - for (dataMatch in dataMatcher.findAll(match.value)) { - val (key, value) = dataMatch.destructured - data.put(key, value) - } - edges.add(data) - println("Found edge containing data: ${data.entries.map { "${it.key}: ${it.value}" }.joinToString(", ")}") - } - for (expectedWitnessEdge in expectedWitnessEdges) { - Assertions.assertFalse( - edges.none { edge -> - val startline = expectedWitnessEdge.startlineRange?.let { - edge["startline"]?.let { v -> - Pair(it, Integer.parseInt(v)) - } - }?.let { it.first.first <= it.second && it.second <= it.first.second } ?: false - val endline = expectedWitnessEdge.endlineRange?.let { - edge["endline"]?.let { v -> - Pair(it, Integer.parseInt(v)) - } - }?.let { it.first.first <= it.second && it.second <= it.first.second } ?: false - val startoffset = expectedWitnessEdge.startoffsetRange?.let { - edge["startoffset"]?.let { v -> - Pair(it, Integer.parseInt(v)) - } - }?.let { it.first.first <= it.second && it.second <= it.first.second } ?: false - val endoffset = expectedWitnessEdge.endoffsetRange?.let { - edge["endoffset"]?.let { v -> - Pair(it, Integer.parseInt(v)) - } - }?.let { it.first.first <= it.second && it.second <= it.first.second } ?: false - val assumption = expectedWitnessEdge.assumption?.let { - edge["assumption"]?.let { v -> - Pair(it, v) - } - }?.let { it.first.matches(it.second) } ?: false - startline && endline && startoffset && endoffset && assumption - }, - "Expected witness edge not found: $expectedWitnessEdge" - ) - } - temp.toFile().deleteRecursively() - } - - -} diff --git a/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/mdd/XstsMddChecker.java b/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/mdd/XstsMddChecker.java index ae9262e03f..b8ae5f098e 100644 --- a/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/mdd/XstsMddChecker.java +++ b/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/mdd/XstsMddChecker.java @@ -15,30 +15,32 @@ */ package hu.bme.mit.theta.xsts.analysis.mdd; +import static hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.Eq; +import static hu.bme.mit.theta.core.type.booltype.BoolExprs.And; +import static hu.bme.mit.theta.core.type.booltype.SmartBoolExprs.Not; + import com.google.common.base.Preconditions; -import hu.bme.mit.delta.collections.impl.RecursiveIntObjMapViews; -import hu.bme.mit.delta.java.mdd.*; +import hu.bme.mit.delta.java.mdd.JavaMddFactory; +import hu.bme.mit.delta.java.mdd.MddGraph; +import hu.bme.mit.delta.java.mdd.MddHandle; +import hu.bme.mit.delta.java.mdd.MddVariableOrder; import hu.bme.mit.delta.mdd.MddInterpreter; import hu.bme.mit.delta.mdd.MddVariableDescriptor; -import hu.bme.mit.theta.analysis.algorithm.SafetyResult; import hu.bme.mit.theta.analysis.algorithm.SafetyChecker; +import hu.bme.mit.theta.analysis.algorithm.SafetyResult; import hu.bme.mit.theta.analysis.algorithm.mdd.MddAnalysisStatistics; import hu.bme.mit.theta.analysis.algorithm.mdd.MddCex; import hu.bme.mit.theta.analysis.algorithm.mdd.MddChecker.IterationStrategy; -import hu.bme.mit.theta.analysis.algorithm.mdd.MddWitness; -import hu.bme.mit.theta.analysis.algorithm.mdd.fixedpoint.*; +import hu.bme.mit.theta.analysis.algorithm.mdd.MddProof; import hu.bme.mit.theta.analysis.algorithm.mdd.ansd.AbstractNextStateDescriptor; +import hu.bme.mit.theta.analysis.algorithm.mdd.ansd.impl.MddNodeInitializer; +import hu.bme.mit.theta.analysis.algorithm.mdd.ansd.impl.MddNodeNextStateDescriptor; import hu.bme.mit.theta.analysis.algorithm.mdd.ansd.impl.OrNextStateDescriptor; -import hu.bme.mit.theta.common.logging.Logger; -import hu.bme.mit.theta.common.logging.Logger.Level; -import hu.bme.mit.theta.solver.SolverPool; import hu.bme.mit.theta.analysis.algorithm.mdd.expressionnode.ExprLatticeDefinition; import hu.bme.mit.theta.analysis.algorithm.mdd.expressionnode.MddExpressionTemplate; -import hu.bme.mit.theta.analysis.algorithm.mdd.ansd.impl.MddNodeInitializer; -import hu.bme.mit.theta.analysis.algorithm.mdd.ansd.impl.MddNodeNextStateDescriptor; -import hu.bme.mit.theta.analysis.utils.MddNodeVisualizer; -import hu.bme.mit.theta.common.visualization.Graph; -import hu.bme.mit.theta.common.visualization.writer.GraphvizWriter; +import hu.bme.mit.theta.analysis.algorithm.mdd.fixedpoint.*; +import hu.bme.mit.theta.common.logging.Logger; +import hu.bme.mit.theta.common.logging.Logger.Level; import hu.bme.mit.theta.core.decl.Decl; import hu.bme.mit.theta.core.stmt.NonDetStmt; import hu.bme.mit.theta.core.stmt.SequenceStmt; @@ -48,17 +50,12 @@ import hu.bme.mit.theta.core.utils.PathUtils; import hu.bme.mit.theta.core.utils.StmtUtils; import hu.bme.mit.theta.core.utils.indexings.VarIndexingFactory; +import hu.bme.mit.theta.solver.SolverPool; import hu.bme.mit.theta.xsts.XSTS; - -import java.io.FileNotFoundException; import java.util.ArrayList; import java.util.List; -import static hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.Eq; -import static hu.bme.mit.theta.core.type.booltype.BoolExprs.And; -import static hu.bme.mit.theta.core.type.booltype.SmartBoolExprs.Not; - -public class XstsMddChecker implements SafetyChecker { +public class XstsMddChecker implements SafetyChecker { private final SolverPool solverPool; private final XSTS xsts; @@ -66,7 +63,8 @@ public class XstsMddChecker implements SafetyChecker { private final Logger logger; private IterationStrategy iterationStrategy; - private XstsMddChecker(XSTS xsts, SolverPool solverPool, Logger logger, IterationStrategy iterationStrategy) { + private XstsMddChecker( + XSTS xsts, SolverPool solverPool, Logger logger, IterationStrategy iterationStrategy) { this.xsts = xsts; this.solverPool = solverPool; this.logger = logger; @@ -77,33 +75,64 @@ public static XstsMddChecker create(XSTS xsts, SolverPool solverPool, Logger log return new XstsMddChecker(xsts, solverPool, logger, IterationStrategy.GSAT); } - public static XstsMddChecker create(XSTS xsts, SolverPool solverPool, Logger logger, IterationStrategy iterationStrategy) { + public static XstsMddChecker create( + XSTS xsts, SolverPool solverPool, Logger logger, IterationStrategy iterationStrategy) { return new XstsMddChecker(xsts, solverPool, logger, iterationStrategy); } @Override - public SafetyResult check(Void input) { - - final MddGraph mddGraph = JavaMddFactory.getDefault().createMddGraph(ExprLatticeDefinition.forExpr()); - - final MddVariableOrder stateOrder = JavaMddFactory.getDefault().createMddVariableOrder(mddGraph); - final MddVariableOrder transOrder = JavaMddFactory.getDefault().createMddVariableOrder(mddGraph); - final MddVariableOrder initOrder = JavaMddFactory.getDefault().createMddVariableOrder(mddGraph); - - final NonDetStmt envTran = NonDetStmt.of(xsts.getEnv().getStmts().stream().flatMap(e -> xsts.getTran().getStmts().stream().map(t -> (Stmt) SequenceStmt.of(List.of(e, t)))).toList()); + public SafetyResult check(Void input) { + + final MddGraph mddGraph = + JavaMddFactory.getDefault().createMddGraph(ExprLatticeDefinition.forExpr()); + + final MddVariableOrder stateOrder = + JavaMddFactory.getDefault().createMddVariableOrder(mddGraph); + final MddVariableOrder transOrder = + JavaMddFactory.getDefault().createMddVariableOrder(mddGraph); + final MddVariableOrder initOrder = + JavaMddFactory.getDefault().createMddVariableOrder(mddGraph); + + final NonDetStmt envTran = + NonDetStmt.of( + xsts.getEnv().getStmts().stream() + .flatMap( + e -> + xsts.getTran().getStmts().stream() + .map( + t -> + (Stmt) + SequenceStmt.of( + List.of( + e, + t)))) + .toList()); final var envTranToExprResult = StmtUtils.toExpr(envTran, VarIndexingFactory.indexing(0)); - final var initToExprResult = StmtUtils.toExpr(xsts.getInit(), VarIndexingFactory.indexing(0)); + final var initToExprResult = + StmtUtils.toExpr(xsts.getInit(), VarIndexingFactory.indexing(0)); for (var v : xsts.getVars()) { final var domainSize = /*v.getType() instanceof BoolType ? 2 :*/ 0; stateOrder.createOnTop(MddVariableDescriptor.create(v.getConstDecl(0), domainSize)); - transOrder.createOnTop(MddVariableDescriptor.create(v.getConstDecl(envTranToExprResult.getIndexing().get(v) == 0 ? 1 : envTranToExprResult.getIndexing().get(v)), domainSize)); + transOrder.createOnTop( + MddVariableDescriptor.create( + v.getConstDecl( + envTranToExprResult.getIndexing().get(v) == 0 + ? 1 + : envTranToExprResult.getIndexing().get(v)), + domainSize)); transOrder.createOnTop(MddVariableDescriptor.create(v.getConstDecl(0), domainSize)); // TODO if indexes are identical, inject v'=v - initOrder.createOnTop(MddVariableDescriptor.create(v.getConstDecl(initToExprResult.getIndexing().get(v) == 0 ? 1 : initToExprResult.getIndexing().get(v)), domainSize)); + initOrder.createOnTop( + MddVariableDescriptor.create( + v.getConstDecl( + initToExprResult.getIndexing().get(v) == 0 + ? 1 + : initToExprResult.getIndexing().get(v)), + domainSize)); initOrder.createOnTop(MddVariableDescriptor.create(v.getConstDecl(0), domainSize)); } @@ -112,21 +141,30 @@ public SafetyResult check(Void input) { final var initSig = initOrder.getDefaultSetSignature(); final Expr initExpr = PathUtils.unfold(xsts.getInitFormula(), 0); - final MddHandle initNode = stateSig.getTopVariableHandle().checkInNode(MddExpressionTemplate.of(initExpr, o -> (Decl) o, solverPool)); + final MddHandle initNode = + stateSig.getTopVariableHandle() + .checkInNode(MddExpressionTemplate.of(initExpr, o -> (Decl) o, solverPool)); Preconditions.checkState(initToExprResult.getExprs().size() == 1); - final var initUnfold = PathUtils.unfold(initToExprResult.getExprs().stream().findFirst().get(), 0); + final var initUnfold = + PathUtils.unfold(initToExprResult.getExprs().stream().findFirst().get(), 0); final var initIdentityExprs = new ArrayList>(); for (var v : xsts.getVars()) { if (initToExprResult.getIndexing().get(v) == 0) initIdentityExprs.add(Eq(v.getConstDecl(0).getRef(), v.getConstDecl(1).getRef())); } final var initExprWithIdentity = And(initUnfold, And(initIdentityExprs)); - final MddHandle initTranNode = initSig.getTopVariableHandle().checkInNode(MddExpressionTemplate.of(initExprWithIdentity, o -> (Decl) o, solverPool)); - final AbstractNextStateDescriptor initNextState = MddNodeNextStateDescriptor.of(initTranNode); + final MddHandle initTranNode = + initSig.getTopVariableHandle() + .checkInNode( + MddExpressionTemplate.of( + initExprWithIdentity, o -> (Decl) o, solverPool)); + final AbstractNextStateDescriptor initNextState = + MddNodeNextStateDescriptor.of(initTranNode); final var rel = new LegacyRelationalProductProvider(stateSig.getVariableOrder()); - final var initResult = rel.compute(initNode, initNextState, stateSig.getTopVariableHandle()); + final var initResult = + rel.compute(initNode, initNextState, stateSig.getTopVariableHandle()); logger.write(Level.INFO, "Created initial node"); @@ -138,13 +176,21 @@ public SafetyResult check(Void input) { final var identityExprs = new ArrayList>(); for (var v : xsts.getVars()) { if (stmtToExpr.getIndexing().get(v) < envTranToExprResult.getIndexing().get(v)) - identityExprs.add(Eq(v.getConstDecl(stmtToExpr.getIndexing().get(v)).getRef(), v.getConstDecl(envTranToExprResult.getIndexing().get(v)).getRef())); + identityExprs.add( + Eq( + v.getConstDecl(stmtToExpr.getIndexing().get(v)).getRef(), + v.getConstDecl(envTranToExprResult.getIndexing().get(v)) + .getRef())); if (envTranToExprResult.getIndexing().get(v) == 0) identityExprs.add(Eq(v.getConstDecl(0).getRef(), v.getConstDecl(1).getRef())); } if (!identityExprs.isEmpty()) stmtUnfold = And(stmtUnfold, And(identityExprs)); - MddHandle transitionNode = transSig.getTopVariableHandle().checkInNode(MddExpressionTemplate.of(stmtUnfold, o -> (Decl) o, solverPool)); + MddHandle transitionNode = + transSig.getTopVariableHandle() + .checkInNode( + MddExpressionTemplate.of( + stmtUnfold, o -> (Decl) o, solverPool)); descriptors.add(MddNodeNextStateDescriptor.of(transitionNode)); } final AbstractNextStateDescriptor nextStates = OrNextStateDescriptor.create(descriptors); @@ -164,12 +210,20 @@ public SafetyResult check(Void input) { } default -> throw new IllegalStateException("Unexpected value: " + iterationStrategy); } - final MddHandle stateSpace = stateSpaceProvider.compute(MddNodeInitializer.of(initResult), nextStates, stateSig.getTopVariableHandle()); + final MddHandle stateSpace = + stateSpaceProvider.compute( + MddNodeInitializer.of(initResult), + nextStates, + stateSig.getTopVariableHandle()); logger.write(Level.INFO, "Enumerated state-space"); final Expr negatedPropExpr = PathUtils.unfold(Not(xsts.getProp()), 0); - final MddHandle propNode = stateSig.getTopVariableHandle().checkInNode(MddExpressionTemplate.of(negatedPropExpr, o -> (Decl) o, solverPool)); + final MddHandle propNode = + stateSig.getTopVariableHandle() + .checkInNode( + MddExpressionTemplate.of( + negatedPropExpr, o -> (Decl) o, solverPool)); final MddHandle propViolating = (MddHandle) stateSpace.intersection(propNode); @@ -181,16 +235,23 @@ public SafetyResult check(Void input) { final Long stateSpaceSize = MddInterpreter.calculateNonzeroCount(stateSpace); logger.write(Level.DETAIL, "State space size: " + stateSpaceSize); - final MddAnalysisStatistics statistics = new MddAnalysisStatistics(violatingSize, stateSpaceSize, stateSpaceProvider.getHitCount(), stateSpaceProvider.getQueryCount(), stateSpaceProvider.getCacheSize()); + final MddAnalysisStatistics statistics = + new MddAnalysisStatistics( + violatingSize, + stateSpaceSize, + stateSpaceProvider.getHitCount(), + stateSpaceProvider.getQueryCount(), + stateSpaceProvider.getCacheSize()); - final SafetyResult result; + final SafetyResult result; if (violatingSize != 0) { - result = SafetyResult.unsafe(MddCex.of(propViolating), MddWitness.of(stateSpace), statistics); + result = + SafetyResult.unsafe( + MddCex.of(propViolating), MddProof.of(stateSpace), statistics); } else { - result = SafetyResult.safe(MddWitness.of(stateSpace), statistics); + result = SafetyResult.safe(MddProof.of(stateSpace), statistics); } logger.write(Level.RESULT, "%s%n", result); return result; - } } diff --git a/subprojects/xsts/xsts-analysis/src/test/java/hu/bme/mit/theta/xsts/analysis/XstsMddCheckerTest.java b/subprojects/xsts/xsts-analysis/src/test/java/hu/bme/mit/theta/xsts/analysis/XstsMddCheckerTest.java index bda3053ed6..4208cdfd6a 100644 --- a/subprojects/xsts/xsts-analysis/src/test/java/hu/bme/mit/theta/xsts/analysis/XstsMddCheckerTest.java +++ b/subprojects/xsts/xsts-analysis/src/test/java/hu/bme/mit/theta/xsts/analysis/XstsMddCheckerTest.java @@ -15,10 +15,12 @@ */ package hu.bme.mit.theta.xsts.analysis; +import static org.junit.Assert.assertTrue; + import hu.bme.mit.theta.analysis.algorithm.SafetyResult; import hu.bme.mit.theta.analysis.algorithm.mdd.MddCex; import hu.bme.mit.theta.analysis.algorithm.mdd.MddChecker.IterationStrategy; -import hu.bme.mit.theta.analysis.algorithm.mdd.MddWitness; +import hu.bme.mit.theta.analysis.algorithm.mdd.MddProof; import hu.bme.mit.theta.common.logging.ConsoleLogger; import hu.bme.mit.theta.common.logging.Logger; import hu.bme.mit.theta.solver.SolverPool; @@ -26,99 +28,159 @@ import hu.bme.mit.theta.xsts.XSTS; import hu.bme.mit.theta.xsts.analysis.mdd.XstsMddChecker; import hu.bme.mit.theta.xsts.dsl.XstsDslManager; -import org.junit.Test; -import org.junit.runner.RunWith; -import org.junit.runners.Parameterized; - import java.io.FileInputStream; -import java.io.IOException; import java.io.InputStream; import java.io.SequenceInputStream; import java.util.Arrays; import java.util.Collection; -import static org.junit.Assert.assertTrue; - public class XstsMddCheckerTest { public static Collection data() { - return Arrays.asList(new Object[][]{ - -// { "src/test/resources/model/trafficlight.xsts", "src/test/resources/property/green_and_red.prop", true}, - - {"src/test/resources/model/trafficlight_v2.xsts", "src/test/resources/property/green_and_red.prop", true}, - - {"src/test/resources/model/counter5.xsts", "src/test/resources/property/x_between_0_and_5.prop", true}, - - {"src/test/resources/model/counter5.xsts", "src/test/resources/property/x_eq_5.prop", false}, - - {"src/test/resources/model/x_and_y.xsts", "src/test/resources/property/x_geq_y.prop", true}, - - {"src/test/resources/model/x_powers.xsts", "src/test/resources/property/x_even.prop", true}, - -// { "src/test/resources/model/cross_with.xsts", "src/test/resources/property/cross.prop", false}, - -// { "src/test/resources/model/cross_without.xsts", "src/test/resources/property/cross.prop", false}, - - {"src/test/resources/model/choices.xsts", "src/test/resources/property/choices.prop", false}, - -// { "src/test/resources/model/literals.xsts", "src/test/resources/property/literals.prop", true}, - -// { "src/test/resources/model/cross3.xsts", "src/test/resources/property/cross.prop", false}, - - {"src/test/resources/model/sequential.xsts", "src/test/resources/property/sequential.prop", true}, - - {"src/test/resources/model/sequential.xsts", "src/test/resources/property/sequential2.prop", false}, - - {"src/test/resources/model/on_off_statemachine.xsts", "src/test/resources/property/on_off_statemachine.prop", false}, - - {"src/test/resources/model/on_off_statemachine.xsts", "src/test/resources/property/on_off_statemachine2.prop", true}, - - {"src/test/resources/model/on_off_statemachine.xsts", "src/test/resources/property/on_off_statemachine3.prop", false}, - -// {"src/test/resources/model/counter50.xsts", "src/test/resources/property/x_eq_5.prop", false}, -// -// {"src/test/resources/model/counter50.xsts", "src/test/resources/property/x_eq_50.prop", false}, -// -// {"src/test/resources/model/counter50.xsts", "src/test/resources/property/x_eq_51.prop", true}, - - {"src/test/resources/model/count_up_down.xsts", "src/test/resources/property/count_up_down.prop", false}, - - {"src/test/resources/model/count_up_down.xsts", "src/test/resources/property/count_up_down2.prop", true}, - -// {"src/test/resources/model/bhmr2007.xsts", "src/test/resources/property/bhmr2007.prop", true}, -// -// {"src/test/resources/model/css2003.xsts", "src/test/resources/property/css2003.prop", true}, -// -// { "src/test/resources/model/array_counter.xsts", "src/test/resources/property/array_10.prop", false}, -// -// { "src/test/resources/model/array_constant.xsts", "src/test/resources/property/array_constant.prop", true}, -// -// { "src/test/resources/model/localvars.xsts", "src/test/resources/property/localvars.prop", true}, -// -// { "src/test/resources/model/localvars2.xsts", "src/test/resources/property/localvars2.prop", true}, -// -// { "src/test/resources/model/loopxy.xsts", "src/test/resources/property/loopxy.prop", true}, -// -// { "src/test/resources/model/arraywrite_sugar.xsts", "src/test/resources/property/arraywrite_sugar.prop", false}, -// -// { "src/test/resources/model/if1.xsts", "src/test/resources/property/if1.prop", true}, -// -// { "src/test/resources/model/if2.xsts", "src/test/resources/property/if2.prop", false} - }); + return Arrays.asList( + new Object[][] { + + // { "src/test/resources/model/trafficlight.xsts", + // "src/test/resources/property/green_and_red.prop", true}, + + { + "src/test/resources/model/trafficlight_v2.xsts", + "src/test/resources/property/green_and_red.prop", + true + }, + { + "src/test/resources/model/counter5.xsts", + "src/test/resources/property/x_between_0_and_5.prop", + true + }, + { + "src/test/resources/model/counter5.xsts", + "src/test/resources/property/x_eq_5.prop", + false + }, + { + "src/test/resources/model/x_and_y.xsts", + "src/test/resources/property/x_geq_y.prop", + true + }, + { + "src/test/resources/model/x_powers.xsts", + "src/test/resources/property/x_even.prop", + true + }, + + // { "src/test/resources/model/cross_with.xsts", + // "src/test/resources/property/cross.prop", false}, + + // { "src/test/resources/model/cross_without.xsts", + // "src/test/resources/property/cross.prop", false}, + + { + "src/test/resources/model/choices.xsts", + "src/test/resources/property/choices.prop", + false + }, + + // { "src/test/resources/model/literals.xsts", + // "src/test/resources/property/literals.prop", true}, + + // { "src/test/resources/model/cross3.xsts", + // "src/test/resources/property/cross.prop", false}, + + { + "src/test/resources/model/sequential.xsts", + "src/test/resources/property/sequential.prop", + true + }, + { + "src/test/resources/model/sequential.xsts", + "src/test/resources/property/sequential2.prop", + false + }, + { + "src/test/resources/model/on_off_statemachine.xsts", + "src/test/resources/property/on_off_statemachine.prop", + false + }, + { + "src/test/resources/model/on_off_statemachine.xsts", + "src/test/resources/property/on_off_statemachine2.prop", + true + }, + { + "src/test/resources/model/on_off_statemachine.xsts", + "src/test/resources/property/on_off_statemachine3.prop", + false + }, + + // {"src/test/resources/model/counter50.xsts", + // "src/test/resources/property/x_eq_5.prop", false}, + // + // {"src/test/resources/model/counter50.xsts", + // "src/test/resources/property/x_eq_50.prop", false}, + // + // {"src/test/resources/model/counter50.xsts", + // "src/test/resources/property/x_eq_51.prop", true}, + + { + "src/test/resources/model/count_up_down.xsts", + "src/test/resources/property/count_up_down.prop", + false + }, + { + "src/test/resources/model/count_up_down.xsts", + "src/test/resources/property/count_up_down2.prop", + true + }, + + // {"src/test/resources/model/bhmr2007.xsts", + // "src/test/resources/property/bhmr2007.prop", true}, + // + // {"src/test/resources/model/css2003.xsts", + // "src/test/resources/property/css2003.prop", true}, + // + // { "src/test/resources/model/array_counter.xsts", + // "src/test/resources/property/array_10.prop", false}, + // + // { "src/test/resources/model/array_constant.xsts", + // "src/test/resources/property/array_constant.prop", true}, + // + // { "src/test/resources/model/localvars.xsts", + // "src/test/resources/property/localvars.prop", true}, + // + // { "src/test/resources/model/localvars2.xsts", + // "src/test/resources/property/localvars2.prop", true}, + // + // { "src/test/resources/model/loopxy.xsts", + // "src/test/resources/property/loopxy.prop", true}, + // + // { "src/test/resources/model/arraywrite_sugar.xsts", + // "src/test/resources/property/arraywrite_sugar.prop", false}, + // + // { "src/test/resources/model/if1.xsts", + // "src/test/resources/property/if1.prop", true}, + // + // { "src/test/resources/model/if2.xsts", + // "src/test/resources/property/if2.prop", false} + }); } - public static void runTestWithIterationStrategy(String filePath, String propPath, boolean safe, IterationStrategy iterationStrategy) throws Exception { + public static void runTestWithIterationStrategy( + String filePath, String propPath, boolean safe, IterationStrategy iterationStrategy) + throws Exception { final Logger logger = new ConsoleLogger(Logger.Level.SUBSTEP); XSTS xsts; - try (InputStream inputStream = new SequenceInputStream(new FileInputStream(filePath), new FileInputStream(propPath))) { + try (InputStream inputStream = + new SequenceInputStream( + new FileInputStream(filePath), new FileInputStream(propPath))) { xsts = XstsDslManager.createXsts(inputStream); } - final SafetyResult status; + final SafetyResult status; try (var solverPool = new SolverPool(Z3LegacySolverFactory.getInstance())) { - final XstsMddChecker checker = XstsMddChecker.create(xsts, solverPool, logger, iterationStrategy); + final XstsMddChecker checker = + XstsMddChecker.create(xsts, solverPool, logger, iterationStrategy); status = checker.check(null); } @@ -128,5 +190,4 @@ public static void runTestWithIterationStrategy(String filePath, String propPath assertTrue(status.isUnsafe()); } } - } 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 b0582bf87f..7df23a5d53 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 @@ -13,7 +13,6 @@ * See the License for the specific language governing permissions and * limitations under the License. */ - package hu.bme.mit.theta.xsts.cli import com.github.ajalt.clikt.parameters.options.default @@ -21,7 +20,7 @@ import com.github.ajalt.clikt.parameters.options.option import com.github.ajalt.clikt.parameters.types.enum import com.google.common.base.Stopwatch import hu.bme.mit.theta.analysis.Trace -import hu.bme.mit.theta.analysis.algorithm.EmptyWitness +import hu.bme.mit.theta.analysis.algorithm.EmptyProof import hu.bme.mit.theta.analysis.algorithm.SafetyResult import hu.bme.mit.theta.analysis.algorithm.bounded.* import hu.bme.mit.theta.analysis.expl.ExplState @@ -40,84 +39,109 @@ import kotlin.system.exitProcess typealias S = XstsState -class XstsCliBounded : XstsCliBaseCommand( +class XstsCliBounded : + XstsCliBaseCommand( name = "BOUNDED", - help = "Bounded model checking algorithms (BMC, IMC, KINDUCTION). Use --variant to select the algorithm (by default BMC is selected)." -) { - - enum class Variant { - BMC { + help = + "Bounded model checking algorithms (BMC, IMC, KINDUCTION). Use --variant to select the algorithm (by default BMC is selected).", + ) { - override fun buildChecker( - monolithicExpr: MonolithicExpr, solverFactory: SolverFactory, - valToState: (Valuation) -> S, biValToAction: (Valuation, Valuation) -> XstsAction, - logger: Logger - ) = buildBMC(monolithicExpr, solverFactory.createSolver(), valToState, biValToAction, logger) - }, - KINDUCTION { + enum class Variant { + BMC { - override fun buildChecker( - monolithicExpr: MonolithicExpr, solverFactory: SolverFactory, - valToState: (Valuation) -> S, biValToAction: (Valuation, Valuation) -> XstsAction, - logger: Logger - ) = buildKIND( - monolithicExpr, solverFactory.createSolver(), solverFactory.createSolver(), valToState, biValToAction, - logger - ) - }, - IMC { + override fun buildChecker( + monolithicExpr: MonolithicExpr, + solverFactory: SolverFactory, + valToState: (Valuation) -> S, + biValToAction: (Valuation, Valuation) -> XstsAction, + logger: Logger, + ) = buildBMC(monolithicExpr, solverFactory.createSolver(), valToState, biValToAction, logger) + }, + KINDUCTION { - override fun buildChecker( - monolithicExpr: MonolithicExpr, solverFactory: SolverFactory, - valToState: (Valuation) -> S, biValToAction: (Valuation, Valuation) -> XstsAction, - logger: Logger - ) = buildIMC( - monolithicExpr, solverFactory.createSolver(), solverFactory.createItpSolver(), valToState, - biValToAction, logger - ) - }; + override fun buildChecker( + monolithicExpr: MonolithicExpr, + solverFactory: SolverFactory, + valToState: (Valuation) -> S, + biValToAction: (Valuation, Valuation) -> XstsAction, + logger: Logger, + ) = + buildKIND( + monolithicExpr, + solverFactory.createSolver(), + solverFactory.createSolver(), + valToState, + biValToAction, + logger, + ) + }, + IMC { - abstract fun buildChecker( - monolithicExpr: MonolithicExpr, solverFactory: SolverFactory, valToState: (Valuation) -> S, - biValToAction: (Valuation, Valuation) -> XstsAction, logger: Logger - ): BoundedChecker - } + override fun buildChecker( + monolithicExpr: MonolithicExpr, + solverFactory: SolverFactory, + valToState: (Valuation) -> S, + biValToAction: (Valuation, Valuation) -> XstsAction, + logger: Logger, + ) = + buildIMC( + monolithicExpr, + solverFactory.createSolver(), + solverFactory.createItpSolver(), + valToState, + biValToAction, + logger, + ) + }; - private val variant by option().enum().default(Variant.BMC) + abstract fun buildChecker( + monolithicExpr: MonolithicExpr, + solverFactory: SolverFactory, + valToState: (Valuation) -> S, + biValToAction: (Valuation, Valuation) -> XstsAction, + logger: Logger, + ): BoundedChecker + } - private fun printResult(status: SafetyResult>, xsts: XSTS, totalTimeMs: Long) { - if (!outputOptions.benchmarkMode) return - printCommonResult(status, xsts, totalTimeMs) - val stats = status.stats.orElse(BoundedStatistics(0)) as BoundedStatistics - listOf( - stats.iterations, - ).forEach(writer::cell) - writer.newRow() - } + private val variant by option().enum().default(Variant.BMC) - override fun run() { - try { - doRun() - } catch (e: Exception) { - printError(e) - exitProcess(1) - } - } + private fun printResult( + status: SafetyResult>, + xsts: XSTS, + totalTimeMs: Long, + ) { + if (!outputOptions.benchmarkMode) return + printCommonResult(status, xsts, totalTimeMs) + val stats = status.stats.orElse(BoundedStatistics(0)) as BoundedStatistics + listOf(stats.iterations).forEach(writer::cell) + writer.newRow() + } - private fun doRun() { - registerSolverManagers() - val solverFactory = SolverManager.resolveSolverFactory(solver) - val xsts = inputOptions.loadXsts() - val sw = Stopwatch.createStarted() - val checker = variant.buildChecker( - xsts.toMonolithicExpr(), solverFactory, xsts::valToState, - xsts::valToAction, - logger - ) - val result = checker.check() - sw.stop() - printResult(result, xsts, sw.elapsed(TimeUnit.MILLISECONDS)) - writeCex(result, xsts) + override fun run() { + try { + doRun() + } catch (e: Exception) { + printError(e) + exitProcess(1) } + } -} \ No newline at end of file + private fun doRun() { + registerSolverManagers() + val solverFactory = SolverManager.resolveSolverFactory(solver) + val xsts = inputOptions.loadXsts() + val sw = Stopwatch.createStarted() + val checker = + variant.buildChecker( + xsts.toMonolithicExpr(), + solverFactory, + xsts::valToState, + xsts::valToAction, + logger, + ) + val result = checker.check() + sw.stop() + printResult(result, xsts, sw.elapsed(TimeUnit.MILLISECONDS)) + writeCex(result, xsts) + } +} diff --git a/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliCegar.kt b/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliCegar.kt index ee455f86dc..ade34d7127 100644 --- a/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliCegar.kt +++ b/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliCegar.kt @@ -13,7 +13,6 @@ * See the License for the specific language governing permissions and * limitations under the License. */ - package hu.bme.mit.theta.xsts.cli import com.github.ajalt.clikt.parameters.options.default @@ -38,73 +37,90 @@ import hu.bme.mit.theta.xsts.analysis.config.XstsConfigBuilder.* import java.util.concurrent.TimeUnit import kotlin.system.exitProcess -class XstsCliCegar : XstsCliBaseCommand( +class XstsCliCegar : + XstsCliBaseCommand( name = "CEGAR", - help = "Model checking using the CEGAR (CounterExample Guided Abstraction Refinement) algorithm" -) { + help = "Model checking using the CEGAR (CounterExample Guided Abstraction Refinement) algorithm", + ) { - private val domain: Domain by option(help = "Abstraction domain to use").enum().default(Domain.PRED_CART) - private val refinement: Refinement by option(help = "Refinement strategy to use").enum() - .default(Refinement.SEQ_ITP) - private val search: Search by option(help = "Search strategy to use").enum().default(Search.BFS) - private val refinementSolver: String? by option(help = "Use a different solver for abstraction") - private val abstractionSolver: String? by option(help = "Use a different solver for refinement") - private val predsplit: PredSplit by option().enum().default(PredSplit.WHOLE) - private val maxenum: Int by option().int().default(0) - private val autoexpl: AutoExpl by option().enum().default(AutoExpl.NEWOPERANDS) - private val initprec: InitPrec by option().enum().default(InitPrec.EMPTY) - private val prunestrategy: PruneStrategy by option().enum().default(PruneStrategy.LAZY) - private val optimizestmts: OptimizeStmts by option().enum().default(OptimizeStmts.ON) + private val domain: Domain by + option(help = "Abstraction domain to use").enum().default(Domain.PRED_CART) + private val refinement: Refinement by + option(help = "Refinement strategy to use").enum().default(Refinement.SEQ_ITP) + private val search: Search by + option(help = "Search strategy to use").enum().default(Search.BFS) + private val refinementSolver: String? by option(help = "Use a different solver for abstraction") + private val abstractionSolver: String? by option(help = "Use a different solver for refinement") + private val predsplit: PredSplit by option().enum().default(PredSplit.WHOLE) + private val maxenum: Int by option().int().default(0) + private val autoexpl: AutoExpl by option().enum().default(AutoExpl.NEWOPERANDS) + private val initprec: InitPrec by option().enum().default(InitPrec.EMPTY) + private val prunestrategy: PruneStrategy by + option().enum().default(PruneStrategy.LAZY) + private val optimizestmts: OptimizeStmts by + option().enum().default(OptimizeStmts.ON) - private fun printResult(status: SafetyResult?, out Trace<*, *>?>, xsts: XSTS, totalTimeMs: Long) { - if (!outputOptions.benchmarkMode) return - printCommonResult(status, xsts, totalTimeMs) - val stats = status.stats.orElse(CegarStatistics(0, 0, 0, 0)) as CegarStatistics - listOf( - stats.algorithmTimeMs, - stats.abstractorTimeMs, - stats.refinerTimeMs, - stats.iterations, - status.witness!!.size(), - status.witness!!.depth, - status.witness!!.meanBranchingFactor, - ).forEach(writer::cell) - writer.newRow() - } + private fun printResult( + status: SafetyResult?, out Trace<*, *>?>, + xsts: XSTS, + totalTimeMs: Long, + ) { + if (!outputOptions.benchmarkMode) return + printCommonResult(status, xsts, totalTimeMs) + val stats = status.stats.orElse(CegarStatistics(0, 0, 0, 0)) as CegarStatistics + listOf( + stats.algorithmTimeMs, + stats.abstractorTimeMs, + stats.refinerTimeMs, + stats.iterations, + status.proof!!.size(), + status.proof!!.depth, + status.proof!!.meanBranchingFactor, + ) + .forEach(writer::cell) + writer.newRow() + } - private fun writeVisualStatus( - status: SafetyResult?, out Trace?> - ) { - if (outputOptions.visualize == null) return - val graph = if (status.isSafe) ArgVisualizer.getDefault().visualize(status.asSafe().witness) - else TraceVisualizer.getDefault().visualize(status.asUnsafe().cex) - GraphvizWriter.getInstance().writeFile(graph, outputOptions.visualize!!) - } - - override fun run() { - try { - doRun() - } catch (e: Exception) { - printError(e) - exitProcess(1) - } - } + private fun writeVisualStatus( + status: SafetyResult?, out Trace?> + ) { + if (outputOptions.visualize == null) return + val graph = + if (status.isSafe) ArgVisualizer.getDefault().visualize(status.asSafe().proof) + else TraceVisualizer.getDefault().visualize(status.asUnsafe().cex) + GraphvizWriter.getInstance().writeFile(graph, outputOptions.visualize!!) + } - private fun doRun() { - registerSolverManagers() - val abstractionSolverFactory = SolverManager.resolveSolverFactory(abstractionSolver ?: solver) - val refinementSolverFactory = SolverManager.resolveSolverFactory(refinementSolver ?: solver) - val xsts = inputOptions.loadXsts() - val config = - XstsConfigBuilder(domain, refinement, abstractionSolverFactory, refinementSolverFactory).maxEnum(maxenum) - .autoExpl(autoexpl).initPrec(initprec).pruneStrategy(prunestrategy).search(search).predSplit(predsplit) - .optimizeStmts(optimizestmts).logger(logger).build(xsts) - val sw = Stopwatch.createStarted() - val result = config.check() - sw.stop() - printResult(result, xsts, sw.elapsed(TimeUnit.MILLISECONDS)) - writeCex(result, xsts) - writeVisualStatus(result) + override fun run() { + try { + doRun() + } catch (e: Exception) { + printError(e) + exitProcess(1) } + } -} \ No newline at end of file + private fun doRun() { + registerSolverManagers() + val abstractionSolverFactory = SolverManager.resolveSolverFactory(abstractionSolver ?: solver) + val refinementSolverFactory = SolverManager.resolveSolverFactory(refinementSolver ?: solver) + val xsts = inputOptions.loadXsts() + val config = + XstsConfigBuilder(domain, refinement, abstractionSolverFactory, refinementSolverFactory) + .maxEnum(maxenum) + .autoExpl(autoexpl) + .initPrec(initprec) + .pruneStrategy(prunestrategy) + .search(search) + .predSplit(predsplit) + .optimizeStmts(optimizestmts) + .logger(logger) + .build(xsts) + val sw = Stopwatch.createStarted() + val result = config.check() + sw.stop() + printResult(result, xsts, sw.elapsed(TimeUnit.MILLISECONDS)) + writeCex(result, xsts) + writeVisualStatus(result) + } +} diff --git a/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliMdd.kt b/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliMdd.kt index cc74818770..f64094d0a8 100644 --- a/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliMdd.kt +++ b/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliMdd.kt @@ -13,80 +13,70 @@ * See the License for the specific language governing permissions and * limitations under the License. */ - package hu.bme.mit.theta.xsts.cli import com.github.ajalt.clikt.parameters.options.default import com.github.ajalt.clikt.parameters.options.option -import com.github.ajalt.clikt.parameters.options.required import com.github.ajalt.clikt.parameters.types.enum import com.google.common.base.Stopwatch -import hu.bme.mit.theta.analysis.Trace -import hu.bme.mit.theta.analysis.algorithm.EmptyWitness import hu.bme.mit.theta.analysis.algorithm.SafetyResult -import hu.bme.mit.theta.analysis.algorithm.bounded.* -import hu.bme.mit.theta.analysis.algorithm.cegar.CegarStatistics import hu.bme.mit.theta.analysis.algorithm.mdd.MddAnalysisStatistics import hu.bme.mit.theta.analysis.algorithm.mdd.MddCex import hu.bme.mit.theta.analysis.algorithm.mdd.MddChecker -import hu.bme.mit.theta.analysis.algorithm.mdd.MddWitness -import hu.bme.mit.theta.common.logging.Logger -import hu.bme.mit.theta.core.model.Valuation -import hu.bme.mit.theta.solver.SolverFactory +import hu.bme.mit.theta.analysis.algorithm.mdd.MddProof import hu.bme.mit.theta.solver.SolverManager import hu.bme.mit.theta.solver.SolverPool import hu.bme.mit.theta.xsts.XSTS -import hu.bme.mit.theta.xsts.analysis.XstsAction -import hu.bme.mit.theta.xsts.analysis.hu.bme.mit.theta.xsts.analysis.toMonolithicExpr -import hu.bme.mit.theta.xsts.analysis.hu.bme.mit.theta.xsts.analysis.valToAction -import hu.bme.mit.theta.xsts.analysis.hu.bme.mit.theta.xsts.analysis.valToState import hu.bme.mit.theta.xsts.analysis.mdd.XstsMddChecker import java.util.concurrent.TimeUnit import kotlin.system.exitProcess -class XstsCliMdd : XstsCliBaseCommand( +class XstsCliMdd : + XstsCliBaseCommand( name = "MDD", - help = "Model checking of XSTS using MDDs (Multi-value Decision Diagrams)" -) { - - private val iterationStrategy: MddChecker.IterationStrategy by option( - help = "The state space enumeration algorithm to use" - ).enum().default(MddChecker.IterationStrategy.GSAT) + help = "Model checking of XSTS using MDDs (Multi-value Decision Diagrams)", + ) { - private fun printResult(status: SafetyResult, xsts: XSTS, totalTimeMs: Long) { - if (!outputOptions.benchmarkMode) return - printCommonResult(status, xsts, totalTimeMs) - val stats = status.stats.orElse(MddAnalysisStatistics(0, 0, 0, 0, 0)) as MddAnalysisStatistics - listOf( - stats.violatingSize, - stats.stateSpaceSize, - stats.hitCount, - stats.queryCount, - stats.cacheSize, - ).forEach(writer::cell) - writer.newRow() - } + private val iterationStrategy: MddChecker.IterationStrategy by + option(help = "The state space enumeration algorithm to use") + .enum() + .default(MddChecker.IterationStrategy.GSAT) - override fun run() { - try { - doRun() - } catch (e: Exception) { - printError(e) - exitProcess(1) - } - } + private fun printResult(status: SafetyResult, xsts: XSTS, totalTimeMs: Long) { + if (!outputOptions.benchmarkMode) return + printCommonResult(status, xsts, totalTimeMs) + val stats = status.stats.orElse(MddAnalysisStatistics(0, 0, 0, 0, 0)) as MddAnalysisStatistics + listOf( + stats.violatingSize, + stats.stateSpaceSize, + stats.hitCount, + stats.queryCount, + stats.cacheSize, + ) + .forEach(writer::cell) + writer.newRow() + } - private fun doRun() { - registerSolverManagers() - val solverFactory = SolverManager.resolveSolverFactory(solver) - val xsts = inputOptions.loadXsts() - val sw = Stopwatch.createStarted() - val result = SolverPool(solverFactory).use { - val checker = XstsMddChecker.create(xsts, it, logger, iterationStrategy) - checker.check(null) - } - sw.stop() - printResult(result, xsts, sw.elapsed(TimeUnit.MILLISECONDS)) + override fun run() { + try { + doRun() + } catch (e: Exception) { + printError(e) + exitProcess(1) } + } -} \ No newline at end of file + private fun doRun() { + registerSolverManagers() + val solverFactory = SolverManager.resolveSolverFactory(solver) + val xsts = inputOptions.loadXsts() + val sw = Stopwatch.createStarted() + val result = + SolverPool(solverFactory).use { + val checker = XstsMddChecker.create(xsts, it, logger, iterationStrategy) + checker.check(null) + } + sw.stop() + printResult(result, xsts, sw.elapsed(TimeUnit.MILLISECONDS)) + } +} diff --git a/subprojects/xta/xta-analysis/src/test/java/hu/bme/mit/theta/xta/analysis/LazyXtaCheckerTest.java b/subprojects/xta/xta-analysis/src/test/java/hu/bme/mit/theta/xta/analysis/LazyXtaCheckerTest.java index be1fc4afe0..eefc740ce6 100644 --- a/subprojects/xta/xta-analysis/src/test/java/hu/bme/mit/theta/xta/analysis/LazyXtaCheckerTest.java +++ b/subprojects/xta/xta-analysis/src/test/java/hu/bme/mit/theta/xta/analysis/LazyXtaCheckerTest.java @@ -15,13 +15,17 @@ */ package hu.bme.mit.theta.xta.analysis; +import static hu.bme.mit.theta.analysis.algorithm.arg.SearchStrategy.BFS; +import static hu.bme.mit.theta.xta.analysis.lazy.ClockStrategy.LU; +import static org.junit.Assert.assertTrue; + import com.google.common.collect.ImmutableList; import com.google.common.collect.ImmutableSet; import hu.bme.mit.theta.analysis.Trace; +import hu.bme.mit.theta.analysis.algorithm.SafetyChecker; import hu.bme.mit.theta.analysis.algorithm.SafetyResult; import hu.bme.mit.theta.analysis.algorithm.arg.ARG; import hu.bme.mit.theta.analysis.algorithm.arg.ArgChecker; -import hu.bme.mit.theta.analysis.algorithm.SafetyChecker; import hu.bme.mit.theta.analysis.unit.UnitPrec; import hu.bme.mit.theta.solver.z3legacy.Z3LegacySolverFactory; import hu.bme.mit.theta.xta.XtaSystem; @@ -29,6 +33,10 @@ import hu.bme.mit.theta.xta.analysis.lazy.DataStrategy; import hu.bme.mit.theta.xta.analysis.lazy.LazyXtaCheckerFactory; import hu.bme.mit.theta.xta.dsl.XtaDslManager; +import java.io.IOException; +import java.io.InputStream; +import java.util.ArrayList; +import java.util.Collection; import org.junit.Before; import org.junit.Test; import org.junit.runner.RunWith; @@ -36,15 +44,6 @@ import org.junit.runners.Parameterized.Parameter; import org.junit.runners.Parameterized.Parameters; -import java.io.IOException; -import java.io.InputStream; -import java.util.ArrayList; -import java.util.Collection; - -import static hu.bme.mit.theta.analysis.algorithm.arg.SearchStrategy.BFS; -import static hu.bme.mit.theta.xta.analysis.lazy.ClockStrategy.LU; -import static org.junit.Assert.assertTrue; - @RunWith(Parameterized.class) public final class LazyXtaCheckerTest { @@ -55,13 +54,17 @@ public final class LazyXtaCheckerTest { private static final String MODEL_ENGINE = "/engine-classic.xta"; private static final String MODEL_BROADCAST = "/broadcast.xta"; - private static final Collection MODELS = ImmutableList.of(MODEL_CSMA, MODEL_FDDI, - MODEL_FISCHER, - MODEL_LYNCH, MODEL_ENGINE, MODEL_BROADCAST); + private static final Collection MODELS = + ImmutableList.of( + MODEL_CSMA, + MODEL_FDDI, + MODEL_FISCHER, + MODEL_LYNCH, + MODEL_ENGINE, + MODEL_BROADCAST); - private static final Collection MODELS_WITH_UNKNOWN_SOLVER_STATUS = ImmutableSet.of( - MODEL_FDDI, - MODEL_ENGINE, MODEL_BROADCAST); + private static final Collection MODELS_WITH_UNKNOWN_SOLVER_STATUS = + ImmutableSet.of(MODEL_FDDI, MODEL_ENGINE, MODEL_BROADCAST); @Parameter(0) public String filepath; @@ -72,7 +75,11 @@ public final class LazyXtaCheckerTest { @Parameter(2) public ClockStrategy clockStrategy; - private SafetyChecker, XtaAction>, ? extends Trace, XtaAction>, UnitPrec> checker; + private SafetyChecker< + ? extends ARG, XtaAction>, + ? extends Trace, XtaAction>, + UnitPrec> + checker; @Parameters(name = "model: {0}, discrete: {1}, clock: {2}") public static Collection data() { @@ -80,9 +87,9 @@ public static Collection data() { for (final String model : MODELS) { for (final DataStrategy dataStrategy : DataStrategy.values()) { for (final ClockStrategy clockStrategy : ClockStrategy.values()) { - if (!MODELS_WITH_UNKNOWN_SOLVER_STATUS.contains(model) || (clockStrategy - != LU)) { - result.add(new Object[]{model, dataStrategy, clockStrategy}); + if (!MODELS_WITH_UNKNOWN_SOLVER_STATUS.contains(model) + || (clockStrategy != LU)) { + result.add(new Object[] {model, dataStrategy, clockStrategy}); } } } @@ -100,14 +107,15 @@ public void initialize() throws IOException { @Test public void test() { // Act - final SafetyResult, XtaAction>, ? extends Trace, XtaAction>> status = checker.check( - UnitPrec.getInstance()); + final SafetyResult< + ? extends ARG, XtaAction>, + ? extends Trace, XtaAction>> + status = checker.check(UnitPrec.getInstance()); // Assert - final ArgChecker argChecker = ArgChecker.create( - Z3LegacySolverFactory.getInstance().createSolver()); - final boolean argCheckResult = argChecker.isWellLabeled(status.getWitness()); + final ArgChecker argChecker = + ArgChecker.create(Z3LegacySolverFactory.getInstance().createSolver()); + final boolean argCheckResult = argChecker.isWellLabeled(status.getProof()); assertTrue(argCheckResult); } - } diff --git a/subprojects/xta/xta-analysis/src/test/java/hu/bme/mit/theta/xta/analysis/XtaAnalysisTest.java b/subprojects/xta/xta-analysis/src/test/java/hu/bme/mit/theta/xta/analysis/XtaAnalysisTest.java index 6bbc845a97..aabfaa25e3 100644 --- a/subprojects/xta/xta-analysis/src/test/java/hu/bme/mit/theta/xta/analysis/XtaAnalysisTest.java +++ b/subprojects/xta/xta-analysis/src/test/java/hu/bme/mit/theta/xta/analysis/XtaAnalysisTest.java @@ -15,18 +15,6 @@ */ package hu.bme.mit.theta.xta.analysis; -import java.io.FileNotFoundException; -import java.io.IOException; -import java.io.InputStream; -import java.util.Arrays; -import java.util.Collection; - -import org.junit.Test; -import org.junit.runner.RunWith; -import org.junit.runners.Parameterized; -import org.junit.runners.Parameterized.Parameter; -import org.junit.runners.Parameterized.Parameters; - import hu.bme.mit.theta.analysis.Analysis; import hu.bme.mit.theta.analysis.LTS; import hu.bme.mit.theta.analysis.algorithm.arg.ARG; @@ -40,27 +28,31 @@ import hu.bme.mit.theta.common.visualization.writer.GraphvizWriter; import hu.bme.mit.theta.xta.XtaSystem; import hu.bme.mit.theta.xta.dsl.XtaDslManager; +import java.io.FileNotFoundException; +import java.io.IOException; +import java.io.InputStream; +import java.util.Arrays; +import java.util.Collection; +import org.junit.Test; +import org.junit.runner.RunWith; +import org.junit.runners.Parameterized; +import org.junit.runners.Parameterized.Parameter; +import org.junit.runners.Parameterized.Parameters; @RunWith(Parameterized.class) public final class XtaAnalysisTest { @Parameters(name = "{0}") public static Collection data() { - return Arrays.asList(new Object[][]{ - - {"/critical-2-25-50.xta"}, - - {"/csma-2.xta"}, - - {"/fddi-2.xta"}, - - {"/fischer-2-32-64.xta"}, - - {"/lynch-2-16.xta"}, - - {"/broadcast.xta"}, - - }); + return Arrays.asList( + new Object[][] { + {"/critical-2-25-50.xta"}, + {"/csma-2.xta"}, + {"/fddi-2.xta"}, + {"/fischer-2-32-64.xta"}, + {"/lynch-2-16.xta"}, + {"/broadcast.xta"}, + }); } @Parameter(0) @@ -72,22 +64,19 @@ public void test() throws FileNotFoundException, IOException { final XtaSystem system = XtaDslManager.createSystem(inputStream); final LTS, XtaAction> lts = XtaLts.create(system); - final Analysis, XtaAction, UnitPrec> analysis = XtaAnalysis.create( - system, - UnitAnalysis.getInstance()); - final ArgBuilder, XtaAction, UnitPrec> argBuilder = ArgBuilder.create( - lts, analysis, - s -> false); + final Analysis, XtaAction, UnitPrec> analysis = + XtaAnalysis.create(system, UnitAnalysis.getInstance()); + final ArgBuilder, XtaAction, UnitPrec> argBuilder = + ArgBuilder.create(lts, analysis, s -> false); - final ArgAbstractor, XtaAction, UnitPrec> abstractor = BasicArgAbstractor.builder( - argBuilder) - .projection(s -> s.getLocs()).build(); + final ArgAbstractor, XtaAction, UnitPrec> abstractor = + BasicArgAbstractor.builder(argBuilder).projection(s -> s.getLocs()).build(); - final ARG, XtaAction> arg = abstractor.createWitness(); + final ARG, XtaAction> arg = abstractor.createProof(); abstractor.check(arg, UnitPrec.getInstance()); System.out.println( - GraphvizWriter.getInstance().writeString(ArgVisualizer.getDefault().visualize(arg))); + GraphvizWriter.getInstance() + .writeString(ArgVisualizer.getDefault().visualize(arg))); } - } diff --git a/subprojects/xta/xta-analysis/src/test/java/hu/bme/mit/theta/xta/analysis/XtaZoneAnalysisTest.java b/subprojects/xta/xta-analysis/src/test/java/hu/bme/mit/theta/xta/analysis/XtaZoneAnalysisTest.java index 111e451934..1c1e6fa56e 100644 --- a/subprojects/xta/xta-analysis/src/test/java/hu/bme/mit/theta/xta/analysis/XtaZoneAnalysisTest.java +++ b/subprojects/xta/xta-analysis/src/test/java/hu/bme/mit/theta/xta/analysis/XtaZoneAnalysisTest.java @@ -15,19 +15,6 @@ */ package hu.bme.mit.theta.xta.analysis; -import java.io.FileNotFoundException; -import java.io.IOException; -import java.io.InputStream; -import java.util.Arrays; -import java.util.Collection; -import java.util.stream.Collectors; - -import org.junit.Test; -import org.junit.runner.RunWith; -import org.junit.runners.Parameterized; -import org.junit.runners.Parameterized.Parameter; -import org.junit.runners.Parameterized.Parameters; - import hu.bme.mit.theta.analysis.Analysis; import hu.bme.mit.theta.analysis.LTS; import hu.bme.mit.theta.analysis.algorithm.arg.ARG; @@ -46,25 +33,31 @@ import hu.bme.mit.theta.xta.analysis.expl.XtaExplAnalysis; import hu.bme.mit.theta.xta.analysis.zone.XtaZoneAnalysis; import hu.bme.mit.theta.xta.dsl.XtaDslManager; +import java.io.FileNotFoundException; +import java.io.IOException; +import java.io.InputStream; +import java.util.Arrays; +import java.util.Collection; +import java.util.stream.Collectors; +import org.junit.Test; +import org.junit.runner.RunWith; +import org.junit.runners.Parameterized; +import org.junit.runners.Parameterized.Parameter; +import org.junit.runners.Parameterized.Parameters; @RunWith(Parameterized.class) public final class XtaZoneAnalysisTest { @Parameters(name = "{0}") public static Collection data() { - return Arrays.asList(new Object[][]{ - - {"/csma-2.xta"}, - - {"/fddi-2.xta"}, - - {"/fischer-2-32-64.xta"}, - - {"/lynch-2-16.xta"}, - - {"/broadcast.xta"}, - - }); + return Arrays.asList( + new Object[][] { + {"/csma-2.xta"}, + {"/fddi-2.xta"}, + {"/fischer-2-32-64.xta"}, + {"/lynch-2-16.xta"}, + {"/broadcast.xta"}, + }); } @Parameter(0) @@ -76,30 +69,32 @@ public void test() throws FileNotFoundException, IOException { final XtaSystem system = XtaDslManager.createSystem(inputStream); final LTS, XtaAction> lts = XtaLts.create(system); - final Analysis explAnalysis = XtaExplAnalysis.create( - system); + final Analysis explAnalysis = + XtaExplAnalysis.create(system); final Analysis zoneAnalysis = XtaZoneAnalysis.getInstance(); - final Analysis, XtaAction, Prod2Prec> prodAnalysis = Prod2Analysis - .create(explAnalysis, zoneAnalysis); - final Analysis, XtaAction, ZonePrec> mappedAnalysis = PrecMappingAnalysis - .create(prodAnalysis, z -> Prod2Prec.of(UnitPrec.getInstance(), z)); - final Analysis>, XtaAction, ZonePrec> analysis = XtaAnalysis - .create(system, mappedAnalysis); + final Analysis, XtaAction, Prod2Prec> + prodAnalysis = Prod2Analysis.create(explAnalysis, zoneAnalysis); + final Analysis, XtaAction, ZonePrec> mappedAnalysis = + PrecMappingAnalysis.create( + prodAnalysis, z -> Prod2Prec.of(UnitPrec.getInstance(), z)); + final Analysis>, XtaAction, ZonePrec> analysis = + XtaAnalysis.create(system, mappedAnalysis); final ZonePrec prec = ZonePrec.of(system.getClockVars()); - final ArgBuilder>, XtaAction, ZonePrec> argBuilder = ArgBuilder - .create(lts, analysis, s -> false); + final ArgBuilder>, XtaAction, ZonePrec> + argBuilder = ArgBuilder.create(lts, analysis, s -> false); - final ArgAbstractor>, XtaAction, ZonePrec> abstractor = BasicArgAbstractor - .builder(argBuilder).projection(s -> s.getLocs()).build(); + final ArgAbstractor>, XtaAction, ZonePrec> + abstractor = + BasicArgAbstractor.builder(argBuilder).projection(s -> s.getLocs()).build(); - final ARG>, XtaAction> arg = abstractor.createWitness(); + final ARG>, XtaAction> arg = + abstractor.createProof(); abstractor.check(arg, prec); System.out.println(arg.getNodes().collect(Collectors.toSet())); System.out.println(arg.getNodes().count()); } - } diff --git a/subprojects/xta/xta-cli/src/main/java/hu/bme/mit/theta/xta/cli/XtaCli.java b/subprojects/xta/xta-cli/src/main/java/hu/bme/mit/theta/xta/cli/XtaCli.java index 4bf1694ff4..7f5185f6fb 100644 --- a/subprojects/xta/xta-cli/src/main/java/hu/bme/mit/theta/xta/cli/XtaCli.java +++ b/subprojects/xta/xta-cli/src/main/java/hu/bme/mit/theta/xta/cli/XtaCli.java @@ -15,12 +15,9 @@ */ package hu.bme.mit.theta.xta.cli; -import java.io.*; - import com.beust.jcommander.JCommander; import com.beust.jcommander.Parameter; import com.beust.jcommander.ParameterException; - import hu.bme.mit.theta.analysis.Action; import hu.bme.mit.theta.analysis.State; import hu.bme.mit.theta.analysis.Trace; @@ -42,6 +39,7 @@ import hu.bme.mit.theta.xta.analysis.lazy.LazyXtaCheckerFactory; import hu.bme.mit.theta.xta.analysis.lazy.LazyXtaStatistics; import hu.bme.mit.theta.xta.dsl.XtaDslManager; +import java.io.*; public final class XtaCli { @@ -49,29 +47,44 @@ public final class XtaCli { private final String[] args; private final TableWriter writer; - @Parameter(names = {"--model", "-m"}, description = "Path of the input model", required = true) + @Parameter( + names = {"--model", "-m"}, + description = "Path of the input model", + required = true) String model; - @Parameter(names = {"--discrete", - "-d"}, description = "Refinement strategy for discrete variables", required = false) + @Parameter( + names = {"--discrete", "-d"}, + description = "Refinement strategy for discrete variables", + required = false) DataStrategy dataStrategy = DataStrategy.NONE; - @Parameter(names = {"--clock", - "-c"}, description = "Refinement strategy for clock variables", required = true) + @Parameter( + names = {"--clock", "-c"}, + description = "Refinement strategy for clock variables", + required = true) ClockStrategy clockStrategy; - @Parameter(names = {"--search", "-s"}, description = "Search strategy", required = true) + @Parameter( + names = {"--search", "-s"}, + description = "Search strategy", + required = true) SearchStrategy searchStrategy; - @Parameter(names = {"--benchmark", "-b"}, description = "Benchmark mode (only print metrics)") + @Parameter( + names = {"--benchmark", "-b"}, + description = "Benchmark mode (only print metrics)") Boolean benchmarkMode = false; - @Parameter(names = {"--visualize", - "-v"}, description = "Write proof or counterexample to file in dot format") + @Parameter( + names = {"--visualize", "-v"}, + description = "Write proof or counterexample to file in dot format") String dotfile = null; - @Parameter(names = {"--header", - "-h"}, description = "Print only a header (for benchmarks)", help = true) + @Parameter( + names = {"--header", "-h"}, + description = "Print only a header (for benchmarks)", + help = true) boolean headerOnly = false; @Parameter(names = "--stacktrace", description = "Print full stack trace in case of exception") @@ -112,10 +125,12 @@ private void run() { try { final XtaSystem system = loadModel(); - final SafetyChecker checker = LazyXtaCheckerFactory.create(system, - dataStrategy, - clockStrategy, searchStrategy); - final SafetyResult, ? extends Trace> result = check(checker); + final SafetyChecker checker = + LazyXtaCheckerFactory.create( + system, dataStrategy, clockStrategy, searchStrategy); + final SafetyResult< + ? extends ARG, ? extends Trace> + result = check(checker); printResult(result); if (dotfile != null) { writeVisualStatus(result, dotfile); @@ -126,13 +141,20 @@ private void run() { } } - private SafetyResult, ? extends Trace> check(SafetyChecker checker) throws Exception { + private SafetyResult, ? extends Trace> + check(SafetyChecker checker) throws Exception { try { - return (SafetyResult, ? extends Trace>) checker.check(UnitPrec.getInstance()); + return (SafetyResult< + ? extends ARG, + ? extends Trace>) + checker.check(UnitPrec.getInstance()); } catch (final Exception ex) { String message = ex.getMessage() == null ? "(no message)" : ex.getMessage(); throw new Exception( - "Error while running algorithm: " + ex.getClass().getSimpleName() + " " + message, + "Error while running algorithm: " + + ex.getClass().getSimpleName() + + " " + + message, ex); } } @@ -147,7 +169,8 @@ private XtaSystem loadModel() throws Exception { } } - private void printResult(final SafetyResult, ? extends Trace> result) { + private void printResult( + final SafetyResult, ? extends Trace> result) { final LazyXtaStatistics stats = (LazyXtaStatistics) result.getStats().get(); if (benchmarkMode) { stats.writeData(writer); @@ -173,12 +196,16 @@ private void printError(final Throwable ex) { } } - private void writeVisualStatus(final SafetyResult, ? extends Trace> status, final String filename) + private void writeVisualStatus( + final SafetyResult< + ? extends ARG, ? extends Trace> + status, + final String filename) throws FileNotFoundException { final Graph graph = - status.isSafe() ? ArgVisualizer.getDefault().visualize(status.asSafe().getWitness()) + status.isSafe() + ? ArgVisualizer.getDefault().visualize(status.asSafe().getProof()) : TraceVisualizer.getDefault().visualize(status.asUnsafe().getCex()); GraphvizWriter.getInstance().writeFile(graph, filename); } - }