From 292dd94b789382e9ff453b7275c105dee04ade91 Mon Sep 17 00:00:00 2001 From: RipplB Date: Thu, 18 Jul 2024 13:17:15 +0200 Subject: [PATCH] Generalize abstractor, refiner, cegarchecker, visualizer These classes/interfaces depended on ARG and Trace before, which heavily limits reusability. They are now generalized over Witness and Cex. To ease the switch, the old entry points are replicated in "Arg..." classes, so a lot of these changes are just renames. --- build.gradle.kts | 2 +- .../cfa/analysis/config/CfaConfigBuilder.java | 433 ++++++++++--- .../analysis/algorithm/cegar/Abstractor.java | 22 +- .../algorithm/cegar/ArgAbstractor.java | 28 + .../algorithm/cegar/ArgCegarChecker.java | 48 ++ .../analysis/algorithm/cegar/ArgRefiner.java | 29 + ...bstractor.java => BasicArgAbstractor.java} | 12 +- .../algorithm/cegar/CegarChecker.java | 59 +- .../analysis/algorithm/cegar/Refiner.java | 18 +- .../algorithm/cegar/RefinerResult.java | 44 +- .../expr/refinement/AasporRefiner.java | 15 +- .../refinement/MultiExprTraceRefiner.java | 16 +- .../refinement/SingleExprTraceRefiner.java | 6 +- .../theta/analysis/utils/ArgVisualizer.java | 7 +- .../analysis/utils/WitnessVisualizer.java | 26 + .../multi/config/StmtMultiConfigBuilder.kt | 350 ++++++++--- .../sts/analysis/config/StsConfigBuilder.java | 196 +++--- .../mit/theta/sts/analysis/StsExplTest.java | 10 +- .../mit/theta/sts/analysis/StsPredTest.java | 10 +- .../mit/theta/xcfa/analysis/XcfaAbstractor.kt | 137 ---- .../mit/theta/xcfa/analysis/XcfaAnalysis.kt | 496 +++++++++------ .../theta/xcfa/analysis/XcfaArgAbstractor.kt | 143 +++++ .../analysis/XcfaSingeExprTraceRefiner.kt | 4 +- .../xcfa/analysis/XcfaExplAnalysisTest.kt | 549 ++++++++-------- .../xcfa/analysis/XcfaPredAnalysisTest.kt | 563 +++++++++-------- .../xcfa/cli/checkers/ConfigToCegarChecker.kt | 63 +- .../mit/theta/xcfa/cli/params/ParamValues.kt | 592 ++++++++++-------- .../analysis/config/XstsConfigBuilder.java | 256 +++++--- .../theta/xta/analysis/XtaAnalysisTest.java | 8 +- .../xta/analysis/XtaZoneAnalysisTest.java | 8 +- 30 files changed, 2536 insertions(+), 1614 deletions(-) create mode 100644 subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/ArgAbstractor.java create mode 100644 subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/ArgCegarChecker.java create mode 100644 subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/ArgRefiner.java rename subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/{BasicAbstractor.java => BasicArgAbstractor.java} (91%) create mode 100644 subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/utils/WitnessVisualizer.java delete mode 100644 subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaAbstractor.kt create mode 100644 subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaArgAbstractor.kt diff --git a/build.gradle.kts b/build.gradle.kts index b76fd9f7ff..06036a38d7 100644 --- a/build.gradle.kts +++ b/build.gradle.kts @@ -29,7 +29,7 @@ buildscript { allprojects { group = "hu.bme.mit.theta" - version = "6.6.3" + version = "6.6.4" apply(from = rootDir.resolve("gradle/shared-with-buildSrc/mirrors.gradle.kts")) } diff --git a/subprojects/cfa/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/config/CfaConfigBuilder.java b/subprojects/cfa/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/config/CfaConfigBuilder.java index 7427f38b20..37c30260ea 100644 --- a/subprojects/cfa/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/config/CfaConfigBuilder.java +++ b/subprojects/cfa/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/config/CfaConfigBuilder.java @@ -15,16 +15,19 @@ */ package hu.bme.mit.theta.cfa.analysis.config; +import static com.google.common.base.Preconditions.checkState; +import static hu.bme.mit.theta.core.type.booltype.BoolExprs.True; + import hu.bme.mit.theta.analysis.*; +import hu.bme.mit.theta.analysis.algorithm.SafetyChecker; 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.arg.ArgNodeComparators.ArgNodeComparator; -import hu.bme.mit.theta.analysis.algorithm.SafetyChecker; -import hu.bme.mit.theta.analysis.algorithm.cegar.Abstractor; -import hu.bme.mit.theta.analysis.algorithm.cegar.BasicAbstractor; -import hu.bme.mit.theta.analysis.algorithm.cegar.CegarChecker; -import hu.bme.mit.theta.analysis.algorithm.cegar.Refiner; +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; +import hu.bme.mit.theta.analysis.algorithm.cegar.BasicArgAbstractor; import hu.bme.mit.theta.analysis.algorithm.cegar.abstractor.StopCriterion; import hu.bme.mit.theta.analysis.algorithm.cegar.abstractor.StopCriterions; import hu.bme.mit.theta.analysis.expl.*; @@ -52,14 +55,10 @@ import hu.bme.mit.theta.common.logging.NullLogger; import hu.bme.mit.theta.solver.Solver; import hu.bme.mit.theta.solver.SolverFactory; - import java.util.Set; import java.util.function.Function; import java.util.function.Predicate; -import static com.google.common.base.Preconditions.checkState; -import static hu.bme.mit.theta.core.type.booltype.BoolExprs.True; - public class CfaConfigBuilder { private final SolverFactory abstractionSolverFactory; @@ -75,16 +74,19 @@ public class CfaConfigBuilder { private InitPrec initPrec = InitPrec.EMPTY; private PruneStrategy pruneStrategy = PruneStrategy.LAZY; - public CfaConfigBuilder(final Domain domain, final Refinement refinement, - final SolverFactory solverFactory) { + public CfaConfigBuilder( + final Domain domain, final Refinement refinement, final SolverFactory solverFactory) { this.domain = domain; this.refinement = refinement; this.abstractionSolverFactory = solverFactory; this.refinementSolverFactory = solverFactory; } - public CfaConfigBuilder(final Domain domain, final Refinement refinement, - final SolverFactory abstractionSolverFactory, final SolverFactory refinementSolverFactory) { + public CfaConfigBuilder( + final Domain domain, + final Refinement refinement, + final SolverFactory abstractionSolverFactory, + final SolverFactory refinementSolverFactory) { this.domain = domain; this.refinement = refinement; this.abstractionSolverFactory = abstractionSolverFactory; @@ -131,12 +133,13 @@ public CfaConfigBuilder pruneStrategy(final PruneStrategy pruneStrategy) { return this; } - public CfaConfig build(final CFA cfa, - final CFA.Loc errLoc) { + public CfaConfig build( + final CFA cfa, final CFA.Loc errLoc) { if (domain == Domain.EXPL) { return (new ExplStrategy(cfa)).buildConfig(errLoc); } - if (domain == Domain.PRED_BOOL || domain == Domain.PRED_CART + if (domain == Domain.PRED_BOOL + || domain == Domain.PRED_CART || domain == Domain.PRED_SPLIT) { return (new PredStrategy(cfa)).buildConfig(errLoc); } @@ -166,18 +169,53 @@ public enum Domain { public enum Refinement { FW_BIN_ITP { @Override - public Refiner, CfaAction, CfaPrec

> getRefiner(BuilderStrategy builderStrategy) { - return SingleExprTraceRefiner.create(ExprTraceFwBinItpChecker.create(True(), True(), builderStrategy.getRefinementSolverFactory().createItpSolver()), builderStrategy.getPrecGranularity().createRefiner(builderStrategy.getItpRefToPrec()), builderStrategy.getPruneStrategy(), builderStrategy.getLogger()); + public + ArgRefiner, CfaAction, CfaPrec

> getRefiner( + BuilderStrategy builderStrategy) { + return SingleExprTraceRefiner.create( + ExprTraceFwBinItpChecker.create( + True(), + True(), + builderStrategy.getRefinementSolverFactory().createItpSolver()), + builderStrategy + .getPrecGranularity() + .createRefiner(builderStrategy.getItpRefToPrec()), + builderStrategy.getPruneStrategy(), + builderStrategy.getLogger()); } - }, BW_BIN_ITP { + }, + BW_BIN_ITP { @Override - public Refiner, CfaAction, CfaPrec

> getRefiner(BuilderStrategy builderStrategy) { - return SingleExprTraceRefiner.create(ExprTraceBwBinItpChecker.create(True(), True(), builderStrategy.getRefinementSolverFactory().createItpSolver()), builderStrategy.getPrecGranularity().createRefiner(builderStrategy.getItpRefToPrec()), builderStrategy.getPruneStrategy(), builderStrategy.getLogger()); + public + ArgRefiner, CfaAction, CfaPrec

> getRefiner( + BuilderStrategy builderStrategy) { + return SingleExprTraceRefiner.create( + ExprTraceBwBinItpChecker.create( + True(), + True(), + builderStrategy.getRefinementSolverFactory().createItpSolver()), + builderStrategy + .getPrecGranularity() + .createRefiner(builderStrategy.getItpRefToPrec()), + builderStrategy.getPruneStrategy(), + builderStrategy.getLogger()); } - }, SEQ_ITP { + }, + SEQ_ITP { @Override - public Refiner, CfaAction, CfaPrec

> getRefiner(BuilderStrategy builderStrategy) { - return SingleExprTraceRefiner.create(ExprTraceSeqItpChecker.create(True(), True(), builderStrategy.getRefinementSolverFactory().createItpSolver()), builderStrategy.getPrecGranularity().createRefiner(builderStrategy.getItpRefToPrec()), builderStrategy.getPruneStrategy(), builderStrategy.getLogger()); + public + ArgRefiner, CfaAction, CfaPrec

> getRefiner( + BuilderStrategy builderStrategy) { + return SingleExprTraceRefiner.create( + ExprTraceSeqItpChecker.create( + True(), + True(), + builderStrategy.getRefinementSolverFactory().createItpSolver()), + builderStrategy + .getPrecGranularity() + .createRefiner(builderStrategy.getItpRefToPrec()), + builderStrategy.getPruneStrategy(), + builderStrategy.getLogger()); } }, MULTI_SEQ { @@ -187,60 +225,229 @@ public StopCriterion getStopCriterion() { } @Override - public Refiner, CfaAction, CfaPrec

> getRefiner(BuilderStrategy builderStrategy) { - return MultiExprTraceRefiner.create(ExprTraceSeqItpChecker.create(True(), True(), builderStrategy.getRefinementSolverFactory().createItpSolver()), builderStrategy.getPrecGranularity().createRefiner(builderStrategy.getItpRefToPrec()), builderStrategy.getPruneStrategy(), builderStrategy.getLogger()); + public + ArgRefiner, CfaAction, CfaPrec

> getRefiner( + BuilderStrategy builderStrategy) { + return MultiExprTraceRefiner.create( + ExprTraceSeqItpChecker.create( + True(), + True(), + builderStrategy.getRefinementSolverFactory().createItpSolver()), + builderStrategy + .getPrecGranularity() + .createRefiner(builderStrategy.getItpRefToPrec()), + builderStrategy.getPruneStrategy(), + builderStrategy.getLogger()); } }, UNSAT_CORE { @Override - public Refiner, CfaAction, CfaPrec

> getRefiner(BuilderStrategy builderStrategy) { - return SingleExprTraceRefiner.create(ExprTraceUnsatCoreChecker.create(True(), True(), builderStrategy.getRefinementSolverFactory().createUCSolver()), builderStrategy.getPrecGranularity().createRefiner(builderStrategy.getVarsRefToPrec()), builderStrategy.getPruneStrategy(), builderStrategy.getLogger()); + public + ArgRefiner, CfaAction, CfaPrec

> getRefiner( + BuilderStrategy builderStrategy) { + return SingleExprTraceRefiner.create( + ExprTraceUnsatCoreChecker.create( + True(), + True(), + builderStrategy.getRefinementSolverFactory().createUCSolver()), + builderStrategy + .getPrecGranularity() + .createRefiner(builderStrategy.getVarsRefToPrec()), + builderStrategy.getPruneStrategy(), + builderStrategy.getLogger()); } - }, UCB { + }, + UCB { @Override - public Refiner, CfaAction, CfaPrec

> getRefiner(BuilderStrategy builderStrategy) { - return SingleExprTraceRefiner.create(ExprTraceUCBChecker.create(True(), True(), builderStrategy.getRefinementSolverFactory().createUCSolver()), builderStrategy.getPrecGranularity().createRefiner(builderStrategy.getItpRefToPrec()), builderStrategy.getPruneStrategy(), builderStrategy.getLogger()); + public + ArgRefiner, CfaAction, CfaPrec

> getRefiner( + BuilderStrategy builderStrategy) { + return SingleExprTraceRefiner.create( + ExprTraceUCBChecker.create( + True(), + True(), + builderStrategy.getRefinementSolverFactory().createUCSolver()), + builderStrategy + .getPrecGranularity() + .createRefiner(builderStrategy.getItpRefToPrec()), + builderStrategy.getPruneStrategy(), + builderStrategy.getLogger()); } }, NWT_WP { @Override - public Refiner, CfaAction, CfaPrec

> getRefiner(BuilderStrategy builderStrategy) { - return SingleExprTraceRefiner.create(ExprTraceNewtonChecker.create(True(), True(), builderStrategy.getRefinementSolverFactory().createUCSolver()).withoutIT().withSP().withoutLV(), builderStrategy.getPrecGranularity().createRefiner(builderStrategy.getItpRefToPrec()), builderStrategy.getPruneStrategy(), builderStrategy.getLogger()); + public + ArgRefiner, CfaAction, CfaPrec

> getRefiner( + BuilderStrategy builderStrategy) { + return SingleExprTraceRefiner.create( + ExprTraceNewtonChecker.create( + True(), + True(), + builderStrategy + .getRefinementSolverFactory() + .createUCSolver()) + .withoutIT() + .withSP() + .withoutLV(), + builderStrategy + .getPrecGranularity() + .createRefiner(builderStrategy.getItpRefToPrec()), + builderStrategy.getPruneStrategy(), + builderStrategy.getLogger()); } - }, NWT_SP { + }, + NWT_SP { @Override - public Refiner, CfaAction, CfaPrec

> getRefiner(BuilderStrategy builderStrategy) { - return SingleExprTraceRefiner.create(ExprTraceNewtonChecker.create(True(), True(), builderStrategy.getRefinementSolverFactory().createUCSolver()).withoutIT().withWP().withoutLV(), builderStrategy.getPrecGranularity().createRefiner(builderStrategy.getItpRefToPrec()), builderStrategy.getPruneStrategy(), builderStrategy.getLogger()); + public + ArgRefiner, CfaAction, CfaPrec

> getRefiner( + BuilderStrategy builderStrategy) { + return SingleExprTraceRefiner.create( + ExprTraceNewtonChecker.create( + True(), + True(), + builderStrategy + .getRefinementSolverFactory() + .createUCSolver()) + .withoutIT() + .withWP() + .withoutLV(), + builderStrategy + .getPrecGranularity() + .createRefiner(builderStrategy.getItpRefToPrec()), + builderStrategy.getPruneStrategy(), + builderStrategy.getLogger()); } - }, NWT_WP_LV { + }, + NWT_WP_LV { @Override - public Refiner, CfaAction, CfaPrec

> getRefiner(BuilderStrategy builderStrategy) { - return SingleExprTraceRefiner.create(ExprTraceNewtonChecker.create(True(), True(), builderStrategy.getRefinementSolverFactory().createUCSolver()).withoutIT().withWP().withLV(), builderStrategy.getPrecGranularity().createRefiner(builderStrategy.getItpRefToPrec()), builderStrategy.getPruneStrategy(), builderStrategy.getLogger()); + public + ArgRefiner, CfaAction, CfaPrec

> getRefiner( + BuilderStrategy builderStrategy) { + return SingleExprTraceRefiner.create( + ExprTraceNewtonChecker.create( + True(), + True(), + builderStrategy + .getRefinementSolverFactory() + .createUCSolver()) + .withoutIT() + .withWP() + .withLV(), + builderStrategy + .getPrecGranularity() + .createRefiner(builderStrategy.getItpRefToPrec()), + builderStrategy.getPruneStrategy(), + builderStrategy.getLogger()); } - }, NWT_SP_LV { + }, + NWT_SP_LV { @Override - public Refiner, CfaAction, CfaPrec

> getRefiner(BuilderStrategy builderStrategy) { - return SingleExprTraceRefiner.create(ExprTraceNewtonChecker.create(True(), True(), builderStrategy.getRefinementSolverFactory().createUCSolver()).withoutIT().withSP().withLV(), builderStrategy.getPrecGranularity().createRefiner(builderStrategy.getItpRefToPrec()), builderStrategy.getPruneStrategy(), builderStrategy.getLogger()); + public + ArgRefiner, CfaAction, CfaPrec

> getRefiner( + BuilderStrategy builderStrategy) { + return SingleExprTraceRefiner.create( + ExprTraceNewtonChecker.create( + True(), + True(), + builderStrategy + .getRefinementSolverFactory() + .createUCSolver()) + .withoutIT() + .withSP() + .withLV(), + builderStrategy + .getPrecGranularity() + .createRefiner(builderStrategy.getItpRefToPrec()), + builderStrategy.getPruneStrategy(), + builderStrategy.getLogger()); } - }, NWT_IT_WP { + }, + NWT_IT_WP { @Override - public Refiner, CfaAction, CfaPrec

> getRefiner(BuilderStrategy builderStrategy) { - return SingleExprTraceRefiner.create(ExprTraceNewtonChecker.create(True(), True(), builderStrategy.getRefinementSolverFactory().createUCSolver()).withIT().withWP().withoutLV(), builderStrategy.getPrecGranularity().createRefiner(builderStrategy.getItpRefToPrec()), builderStrategy.getPruneStrategy(), builderStrategy.getLogger()); + public + ArgRefiner, CfaAction, CfaPrec

> getRefiner( + BuilderStrategy builderStrategy) { + return SingleExprTraceRefiner.create( + ExprTraceNewtonChecker.create( + True(), + True(), + builderStrategy + .getRefinementSolverFactory() + .createUCSolver()) + .withIT() + .withWP() + .withoutLV(), + builderStrategy + .getPrecGranularity() + .createRefiner(builderStrategy.getItpRefToPrec()), + builderStrategy.getPruneStrategy(), + builderStrategy.getLogger()); } - }, NWT_IT_SP { + }, + NWT_IT_SP { @Override - public Refiner, CfaAction, CfaPrec

> getRefiner(BuilderStrategy builderStrategy) { - return SingleExprTraceRefiner.create(ExprTraceNewtonChecker.create(True(), True(), builderStrategy.getRefinementSolverFactory().createUCSolver()).withIT().withSP().withoutLV(), builderStrategy.getPrecGranularity().createRefiner(builderStrategy.getItpRefToPrec()), builderStrategy.getPruneStrategy(), builderStrategy.getLogger()); + public + ArgRefiner, CfaAction, CfaPrec

> getRefiner( + BuilderStrategy builderStrategy) { + return SingleExprTraceRefiner.create( + ExprTraceNewtonChecker.create( + True(), + True(), + builderStrategy + .getRefinementSolverFactory() + .createUCSolver()) + .withIT() + .withSP() + .withoutLV(), + builderStrategy + .getPrecGranularity() + .createRefiner(builderStrategy.getItpRefToPrec()), + builderStrategy.getPruneStrategy(), + builderStrategy.getLogger()); } - }, NWT_IT_WP_LV { + }, + NWT_IT_WP_LV { @Override - public Refiner, CfaAction, CfaPrec

> getRefiner(BuilderStrategy builderStrategy) { - return SingleExprTraceRefiner.create(ExprTraceNewtonChecker.create(True(), True(), builderStrategy.getRefinementSolverFactory().createUCSolver()).withIT().withWP().withLV(), builderStrategy.getPrecGranularity().createRefiner(builderStrategy.getItpRefToPrec()), builderStrategy.getPruneStrategy(), builderStrategy.getLogger()); + public + ArgRefiner, CfaAction, CfaPrec

> getRefiner( + BuilderStrategy builderStrategy) { + return SingleExprTraceRefiner.create( + ExprTraceNewtonChecker.create( + True(), + True(), + builderStrategy + .getRefinementSolverFactory() + .createUCSolver()) + .withIT() + .withWP() + .withLV(), + builderStrategy + .getPrecGranularity() + .createRefiner(builderStrategy.getItpRefToPrec()), + builderStrategy.getPruneStrategy(), + builderStrategy.getLogger()); } - }, NWT_IT_SP_LV { + }, + NWT_IT_SP_LV { @Override - public Refiner, CfaAction, CfaPrec

> getRefiner(BuilderStrategy builderStrategy) { - return SingleExprTraceRefiner.create(ExprTraceNewtonChecker.create(True(), True(), builderStrategy.getRefinementSolverFactory().createUCSolver()).withIT().withSP().withLV(), builderStrategy.getPrecGranularity().createRefiner(builderStrategy.getItpRefToPrec()), builderStrategy.getPruneStrategy(), builderStrategy.getLogger()); + public + ArgRefiner, CfaAction, CfaPrec

> getRefiner( + BuilderStrategy builderStrategy) { + return SingleExprTraceRefiner.create( + ExprTraceNewtonChecker.create( + True(), + True(), + builderStrategy + .getRefinementSolverFactory() + .createUCSolver()) + .withIT() + .withSP() + .withLV(), + builderStrategy + .getPrecGranularity() + .createRefiner(builderStrategy.getItpRefToPrec()), + builderStrategy.getPruneStrategy(), + builderStrategy.getLogger()); } }; @@ -248,24 +455,25 @@ public StopCriterion getStopCriterion() { return StopCriterions.firstCex(); } - public abstract Refiner, CfaAction, CfaPrec

> getRefiner(BuilderStrategy builderStrategy); - + public abstract + ArgRefiner, CfaAction, CfaPrec

> getRefiner( + BuilderStrategy builderStrategy); } public enum Search { BFS { @Override public ArgNodeComparator getComp(final CFA cfa, final CFA.Loc errLoc) { - return ArgNodeComparators.combine(ArgNodeComparators.targetFirst(), - ArgNodeComparators.bfs()); + return ArgNodeComparators.combine( + ArgNodeComparators.targetFirst(), ArgNodeComparators.bfs()); } }, DFS { @Override public ArgNodeComparator getComp(final CFA cfa, final CFA.Loc errLoc) { - return ArgNodeComparators.combine(ArgNodeComparators.targetFirst(), - ArgNodeComparators.dfs()); + return ArgNodeComparators.combine( + ArgNodeComparators.targetFirst(), ArgNodeComparators.dfs()); } }, @@ -277,7 +485,6 @@ public ArgNodeComparator getComp(final CFA cfa, final CFA.Loc errLoc) { }; public abstract ArgNodeComparator getComp(CFA cfa, CFA.Loc errLoc); - } public enum PredSplit { @@ -302,8 +509,9 @@ public

CfaPrec

createPrec(final P innerPrec) { } @Override - public PrecRefiner, A, CfaPrec

, R> createRefiner( - final RefutationToPrec refToPrec) { + public + PrecRefiner, A, CfaPrec

, R> createRefiner( + final RefutationToPrec refToPrec) { return GlobalCfaPrecRefiner.create(refToPrec); } @@ -320,8 +528,9 @@ public

CfaPrec

createPrec(final P innerPrec) { } @Override - public PrecRefiner, A, CfaPrec

, R> createRefiner( - final RefutationToPrec refToPrec) { + public + PrecRefiner, A, CfaPrec

, R> createRefiner( + final RefutationToPrec refToPrec) { return LocalCfaPrecRefiner.create(refToPrec); } @@ -333,8 +542,10 @@ public CfaPrec assumePrecs(CFA cfa) { public abstract

CfaPrec

createPrec(P innerPrec); - public abstract PrecRefiner, A, CfaPrec

, R> createRefiner( - RefutationToPrec refToPrec); + public abstract < + S extends ExprState, A extends Action, P extends Prec, R extends Refutation> + PrecRefiner, A, CfaPrec

, R> createRefiner( + RefutationToPrec refToPrec); public abstract CfaPrec assumePrecs(CFA cfa); } @@ -358,19 +569,37 @@ public CfaLts getLts(CFA.Loc errorLoc) { } public enum InitPrec { - EMPTY, ALLVARS, ALLASSUMES + EMPTY, + ALLVARS, + ALLASSUMES } public abstract class BuilderStrategy { - protected static final String UNSUPPORTED_CONFIG_VALUE = "Builder strategy %s does not support configuration value %s as %s"; + protected static final String UNSUPPORTED_CONFIG_VALUE = + "Builder strategy %s does not support configuration value %s as %s"; protected final CFA cfa; @SuppressWarnings("java:S1699") protected BuilderStrategy(CFA cfa) { - checkState(getSupportedDomains().contains(domain), UNSUPPORTED_CONFIG_VALUE, getClass().getSimpleName(), domain, "domain"); - checkState(getSupportedRefinements().contains(refinement), UNSUPPORTED_CONFIG_VALUE, getClass().getSimpleName(), refinement, "refinement"); - checkState(getSupportedInitPrecs().contains(initPrec), UNSUPPORTED_CONFIG_VALUE, getClass().getSimpleName(), initPrec, "initial precision"); + checkState( + getSupportedDomains().contains(domain), + UNSUPPORTED_CONFIG_VALUE, + getClass().getSimpleName(), + domain, + "domain"); + checkState( + getSupportedRefinements().contains(refinement), + UNSUPPORTED_CONFIG_VALUE, + getClass().getSimpleName(), + refinement, + "refinement"); + checkState( + getSupportedInitPrecs().contains(initPrec), + UNSUPPORTED_CONFIG_VALUE, + getClass().getSimpleName(), + initPrec, + "initial precision"); this.cfa = cfa; } @@ -389,7 +618,10 @@ public CfaAnalysis getAnalysis() { public abstract RefutationToPrec getItpRefToPrec(); public RefutationToPrec getVarsRefToPrec() { - throw new UnsupportedOperationException(String.format("Builder strategy %s can not provide Vars refutation to precision", getClass().getSimpleName())); + throw new UnsupportedOperationException( + String.format( + "Builder strategy %s can not provide Vars refutation to precision", + getClass().getSimpleName())); } protected SolverFactory getRefinementSolverFactory() { @@ -421,22 +653,30 @@ public CfaLts getLts() { public CfaConfig, CfaAction, CfaPrec

> buildConfig(CFA.Loc errLoc) { final Predicate> target = new CfaErrorlocPredicate<>(errLoc); final Analysis, CfaAction, CfaPrec

> analysis = getAnalysis(); - final ArgBuilder, CfaAction, CfaPrec

> argBuilder = ArgBuilder.create( - getLts(errLoc), analysis, target, - true); - final Abstractor, CfaAction, CfaPrec

> abstractor = BasicAbstractor.builder( - argBuilder) - .waitlist(PriorityWaitlist.create(search.getComp(cfa, errLoc))) - .stopCriterion(refinement.getStopCriterion()) - .logger(logger).build(); - final Refiner, CfaAction, CfaPrec

> refiner = refinement.getRefiner(this); - final SafetyChecker, CfaAction>, Trace, CfaAction>, CfaPrec

> checker = CegarChecker.create( - abstractor, refiner, - logger); + final ArgBuilder, CfaAction, CfaPrec

> argBuilder = + ArgBuilder.create(getLts(errLoc), analysis, target, true); + final ArgAbstractor, CfaAction, CfaPrec

> abstractor = + BasicArgAbstractor.builder(argBuilder) + .waitlist(PriorityWaitlist.create(search.getComp(cfa, errLoc))) + .stopCriterion(refinement.getStopCriterion()) + .logger(logger) + .build(); + final ArgRefiner, CfaAction, CfaPrec

> refiner = + refinement.getRefiner(this); + final SafetyChecker< + ARG, CfaAction>, Trace, CfaAction>, CfaPrec

> + checker = ArgCegarChecker.create(abstractor, refiner, logger); return CfaConfig.create(checker, createInitPrec()); } - public MultiAnalysisSide, S, CfaState, CfaAction, CfaPrec

, CfaPrec> getMultiSide() { + public MultiAnalysisSide< + CfaState, + S, + CfaState, + CfaAction, + CfaPrec

, + CfaPrec> + getMultiSide() { return new MultiAnalysisSide<>( getAnalysis(), CfaControlInitFuncKt.cfaControlInitFunc(cfa.getInitLoc()), @@ -470,7 +710,8 @@ public Set getSupportedInitPrecs() { @Override public Analysis getDataAnalysis() { - return ExplStmtAnalysis.create(abstractionSolverFactory.createSolver(), True(), maxEnum); + return ExplStmtAnalysis.create( + abstractionSolverFactory.createSolver(), True(), maxEnum); } @Override @@ -489,7 +730,12 @@ public CfaPrec createInitPrec() { case EMPTY -> precGranularity.createPrec(ExplPrec.empty()); case ALLVARS -> precGranularity.createPrec(ExplPrec.of(cfa.getVars())); default -> - throw new UnsupportedOperationException(String.format(UNSUPPORTED_CONFIG_VALUE, getClass().getSimpleName(), initPrec, "initial precision")); + throw new UnsupportedOperationException( + String.format( + UNSUPPORTED_CONFIG_VALUE, + getClass().getSimpleName(), + initPrec, + "initial precision")); }; } } @@ -520,8 +766,7 @@ public Set getSupportedRefinements() { Refinement.NWT_IT_SP, Refinement.NWT_IT_WP, Refinement.NWT_IT_SP_LV, - Refinement.NWT_IT_WP_LV - ); + Refinement.NWT_IT_WP_LV); } @Override @@ -546,9 +791,13 @@ public CfaPrec createInitPrec() { case EMPTY -> precGranularity.createPrec(PredPrec.of()); case ALLASSUMES -> precGranularity.assumePrecs(cfa); default -> - throw new UnsupportedOperationException(String.format(UNSUPPORTED_CONFIG_VALUE, getClass().getSimpleName(), initPrec, "initial precision")); + throw new UnsupportedOperationException( + String.format( + UNSUPPORTED_CONFIG_VALUE, + getClass().getSimpleName(), + initPrec, + "initial precision")); }; } } - } 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 a7eb473efd..a6cb49bb43 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 @@ -15,31 +15,23 @@ */ package hu.bme.mit.theta.analysis.algorithm.cegar; -import hu.bme.mit.theta.analysis.Action; import hu.bme.mit.theta.analysis.Prec; -import hu.bme.mit.theta.analysis.State; -import hu.bme.mit.theta.analysis.algorithm.arg.ARG; +import hu.bme.mit.theta.analysis.algorithm.Witness; /** - * Common interface for the abstractor component. It can create an initial ARG and check an ARG with + * 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 ARG. - * - * @return + * Create initial witness */ - ARG createArg(); + W createWitness(); /** - * Check ARG with given precision. - * - * @param arg - * @param prec - * @return + * Check witness with given precision */ - AbstractorResult check(ARG arg, P prec); + AbstractorResult check(W witness, P prec); } diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/ArgAbstractor.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/ArgAbstractor.java new file mode 100644 index 0000000000..67890b8a3a --- /dev/null +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/ArgAbstractor.java @@ -0,0 +1,28 @@ +/* + * 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.analysis.algorithm.cegar; + +import hu.bme.mit.theta.analysis.Action; +import hu.bme.mit.theta.analysis.Prec; +import hu.bme.mit.theta.analysis.State; +import hu.bme.mit.theta.analysis.algorithm.arg.ARG; + +/** + * Common interface for the abstractor component. It can create an initial ARG and check an ARG with + * a given precision. + */ +public interface ArgAbstractor + extends Abstractor> {} diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/ArgCegarChecker.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/ArgCegarChecker.java new file mode 100644 index 0000000000..06260c732c --- /dev/null +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/ArgCegarChecker.java @@ -0,0 +1,48 @@ +/* + * 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.analysis.algorithm.cegar; + +import hu.bme.mit.theta.analysis.Action; +import hu.bme.mit.theta.analysis.Prec; +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.utils.ArgVisualizer; +import hu.bme.mit.theta.common.logging.Logger; +import hu.bme.mit.theta.common.logging.NullLogger; + +/** + * Counterexample-Guided Abstraction Refinement (CEGAR) loop implementation, + * that uses an Abstractor to explore the abstract state space and a Refiner to + * check counterexamples and refine them if needed. It also provides certain + * statistics about its execution. + */ +public final class ArgCegarChecker { + + private ArgCegarChecker() { + } + + public static CegarChecker, Trace> create( + final ArgAbstractor abstractor, final ArgRefiner refiner) { + return create(abstractor, refiner, NullLogger.getInstance()); + } + + public static CegarChecker, Trace> create( + final ArgAbstractor abstractor, final ArgRefiner refiner, final Logger logger) { + return CegarChecker.create(abstractor, refiner, logger, ArgVisualizer.getDefault()); + } + +} diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/ArgRefiner.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/ArgRefiner.java new file mode 100644 index 0000000000..2683a2fd0f --- /dev/null +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/ArgRefiner.java @@ -0,0 +1,29 @@ +/* + * 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.analysis.algorithm.cegar; + +import hu.bme.mit.theta.analysis.Action; +import hu.bme.mit.theta.analysis.Prec; +import hu.bme.mit.theta.analysis.State; +import hu.bme.mit.theta.analysis.Trace; +import hu.bme.mit.theta.analysis.algorithm.arg.ARG; + +/** + * Common interface for refiners. It takes an ARG and a precision, checks if the counterexample in + * the ARG is feasible and if not, it refines the precision and may also prune the ARG. + */ +public interface ArgRefiner extends Refiner, Trace> { +} diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/BasicAbstractor.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/BasicArgAbstractor.java similarity index 91% rename from subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/BasicAbstractor.java rename to subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/BasicArgAbstractor.java index 42eb1487e1..050ae32ce3 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/BasicAbstractor.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/BasicArgAbstractor.java @@ -41,7 +41,7 @@ /** * Basic implementation for the abstractor, relying on an ArgBuilder. */ -public class BasicAbstractor implements Abstractor { +public class BasicArgAbstractor implements ArgAbstractor { protected final ArgBuilder argBuilder; protected final Function projection; @@ -49,8 +49,8 @@ public class BasicAbstractor protected final StopCriterion stopCriterion; protected final Logger logger; - protected BasicAbstractor(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 +64,7 @@ public static Builder createArg() { + public ARG createWitness() { return argBuilder.createArg(); } @@ -174,8 +174,8 @@ public Builder logger(final Logger logger) { return this; } - public BasicAbstractor build() { - return new BasicAbstractor<>(argBuilder, projection, waitlist, stopCriterion, logger); + public BasicArgAbstractor build() { + 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 af69cd7121..fa811afc42 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 @@ -17,19 +17,18 @@ import com.google.common.base.Stopwatch; import hu.bme.mit.theta.analysis.Action; +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.Trace; -import hu.bme.mit.theta.analysis.algorithm.SafetyResult; -import hu.bme.mit.theta.analysis.algorithm.arg.ARG; 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.ArgVisualizer; +import hu.bme.mit.theta.analysis.utils.WitnessVisualizer; import hu.bme.mit.theta.common.Utils; 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 hu.bme.mit.theta.common.visualization.writer.JSONWriter; import hu.bme.mit.theta.common.visualization.writer.WebDebuggerLogger; @@ -43,42 +42,44 @@ * check counterexamples and refine them if needed. It also provides certain * statistics about its execution. */ -public final class CegarChecker implements SafetyChecker, Trace, P> { +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 ARG arg; // TODO I don't think putting the ARG up here from check below causes any issues, but keep it in mind, that it might + private final W witness; + private final WitnessVisualizer witnessVisualizer; - private CegarChecker(final Abstractor abstractor, final Refiner refiner, final Logger logger) { + private CegarChecker(final Abstractor abstractor, final Refiner refiner, final Logger logger, final WitnessVisualizer witnessVisualizer) { this.abstractor = checkNotNull(abstractor); this.refiner = checkNotNull(refiner); this.logger = checkNotNull(logger); - arg = abstractor.createArg(); + witness = abstractor.createWitness(); + this.witnessVisualizer = checkNotNull(witnessVisualizer); } - public static CegarChecker create( - final Abstractor abstractor, final Refiner refiner) { - return new CegarChecker<>(abstractor, refiner, NullLogger.getInstance()); + 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 Logger logger) { - return new CegarChecker<>(abstractor, refiner, logger); + public static CegarChecker create( + final Abstractor abstractor, final Refiner refiner, final Logger logger, final WitnessVisualizer witnessVisualizer) { + return new CegarChecker<>(abstractor, refiner, logger, witnessVisualizer); } - public ARG getArg() { - return arg; + public W getWitness() { + return witness; } @Override - public SafetyResult, Trace> 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; long refinerTime = 0; - RefinerResult refinerResult = null; - AbstractorResult abstractorResult = null; + RefinerResult refinerResult = null; + AbstractorResult abstractorResult; P prec = initPrec; int iteration = 0; WebDebuggerLogger wdl = WebDebuggerLogger.getInstance(); @@ -88,12 +89,12 @@ public SafetyResult, Trace> 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(arg, prec); + abstractorResult = abstractor.check(witness, 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(ArgVisualizer.getDefault().visualize(arg)); + String argGraph = JSONWriter.getInstance().writeString(witnessVisualizer.visualize(witness)); String precString = prec.toString(); wdl.addIteration(iteration, argGraph, precString); } @@ -104,7 +105,7 @@ public SafetyResult, Trace> check(final P initPrec) { P lastPrec = prec; logger.write(Level.MAINSTEP, "| Refining abstraction...%n"); final long refinerStartTime = stopwatch.elapsed(TimeUnit.MILLISECONDS); - refinerResult = refiner.refine(arg, prec); + refinerResult = refiner.refine(witness, prec); refinerTime += stopwatch.elapsed(TimeUnit.MILLISECONDS) - refinerStartTime; logger.write(Level.MAINSTEP, "Refining abstraction done, result: %s%n", refinerResult); @@ -123,16 +124,16 @@ public SafetyResult, Trace> check(final P initPrec) { } while (!abstractorResult.isSafe() && !refinerResult.isUnsafe()); stopwatch.stop(); - SafetyResult, Trace> cegarResult = null; + SafetyResult cegarResult = null; final CegarStatistics stats = new CegarStatistics(stopwatch.elapsed(TimeUnit.MILLISECONDS), abstractorTime, refinerTime, iteration); - assert abstractorResult.isSafe() || (refinerResult != null && refinerResult.isUnsafe()); + assert abstractorResult.isSafe() || refinerResult.isUnsafe(); if (abstractorResult.isSafe()) { - cegarResult = SafetyResult.safe(arg, stats); + cegarResult = SafetyResult.safe(witness, stats); } else if (refinerResult.isUnsafe()) { - cegarResult = SafetyResult.unsafe(refinerResult.asUnsafe().getCex(), arg, stats); + cegarResult = SafetyResult.unsafe(refinerResult.asUnsafe().getCex(), witness, 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 0bbfe07f1d..6eca5d7c21 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 @@ -16,23 +16,19 @@ package hu.bme.mit.theta.analysis.algorithm.cegar; import hu.bme.mit.theta.analysis.Action; +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.arg.ARG; +import hu.bme.mit.theta.analysis.algorithm.Witness; /** - * Common interface for refiners. It takes an ARG and a precision, checks if the counterexample in - * the ARG is feasible and if not, it refines the precision and may also prune the ARG. + * 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 ARG is feasible. If not, refines the precision and prunes - * the ARG. - * - * @param arg - * @param prec - * @return + * Checks if the counterexample in the witness is feasible. If not, refines the precision */ - RefinerResult refine(ARG arg, P prec); + RefinerResult refine(W witness, P prec); } diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/RefinerResult.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/RefinerResult.java index bbce8b5451..a4be30781e 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/RefinerResult.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/RefinerResult.java @@ -15,30 +15,29 @@ */ package hu.bme.mit.theta.analysis.algorithm.cegar; -import static com.google.common.base.Preconditions.checkNotNull; - import hu.bme.mit.theta.analysis.Action; +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.Trace; import hu.bme.mit.theta.common.Utils; +import static com.google.common.base.Preconditions.checkNotNull; + /** * Represents the result of the Refiner class that can be either spurious or unsafe. In the former * case it also contains the refined precision and in the latter case the feasible counterexample. */ -public abstract class RefinerResult { +public abstract class RefinerResult { - private RefinerResult() { + protected RefinerResult() { } /** * Create a new spurious result. * * @param refinedPrec Refined precision - * @return */ - public static Spurious spurious( + public static Spurious spurious( final P refinedPrec) { return new Spurious<>(refinedPrec); } @@ -47,10 +46,9 @@ public static Spurious Unsafe unsafe( - final Trace cex) { + public static Unsafe unsafe( + final C cex) { return new Unsafe<>(cex); } @@ -58,15 +56,15 @@ public static Unsafe asSpurious(); + public abstract Spurious asSpurious(); - public abstract Unsafe asUnsafe(); + public abstract Unsafe asUnsafe(); /** * Represents the spurious result with a refined precision. */ - public static final class Spurious - extends RefinerResult { + public static final class Spurious + extends RefinerResult { private final P refinedPrec; @@ -89,12 +87,12 @@ public boolean isUnsafe() { } @Override - public Spurious asSpurious() { + public Spurious asSpurious() { return this; } @Override - public Unsafe asUnsafe() { + public Unsafe asUnsafe() { throw new ClassCastException( "Cannot cast " + Spurious.class.getSimpleName() + " to " + Unsafe.class.getSimpleName()); @@ -111,16 +109,16 @@ public String toString() { /** * Represents the unsafe result with a feasible counterexample. */ - public static final class Unsafe extends - RefinerResult { + public static final class Unsafe extends + RefinerResult { - private final Trace cex; + private final C cex; - private Unsafe(final Trace cex) { + private Unsafe(final C cex) { this.cex = checkNotNull(cex); } - public Trace getCex() { + public C getCex() { return cex; } @@ -135,14 +133,14 @@ public boolean isUnsafe() { } @Override - public Spurious asSpurious() { + public Spurious asSpurious() { throw new ClassCastException( "Cannot cast " + Unsafe.class.getSimpleName() + " to " + Spurious.class.getSimpleName()); } @Override - public Unsafe asUnsafe() { + public Unsafe asUnsafe() { return this; } diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/expr/refinement/AasporRefiner.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/expr/refinement/AasporRefiner.java index 8f2f499547..f1f7430241 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/expr/refinement/AasporRefiner.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/expr/refinement/AasporRefiner.java @@ -16,9 +16,10 @@ package hu.bme.mit.theta.analysis.expr.refinement; import hu.bme.mit.theta.analysis.Prec; +import hu.bme.mit.theta.analysis.Trace; 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.Refiner; +import hu.bme.mit.theta.analysis.algorithm.cegar.ArgRefiner; import hu.bme.mit.theta.analysis.algorithm.cegar.RefinerResult; import hu.bme.mit.theta.analysis.expr.ExprAction; import hu.bme.mit.theta.analysis.expr.ExprState; @@ -29,15 +30,15 @@ import java.util.Set; import java.util.stream.Collectors; -public final class AasporRefiner implements Refiner { +public final class AasporRefiner implements ArgRefiner { - private final Refiner refiner; + private final ArgRefiner refiner; private final PruneStrategy pruneStrategy; private final Map, Set> ignoredVarRegistry; - private AasporRefiner(final Refiner refiner, + private AasporRefiner(final ArgRefiner refiner, final PruneStrategy pruneStrategy, final Map, Set> ignoredVarRegistry) { this.refiner = refiner; @@ -46,14 +47,14 @@ private AasporRefiner(final Refiner refiner, } public static AasporRefiner create( - final Refiner refiner, final PruneStrategy pruneStrategy, + final ArgRefiner refiner, final PruneStrategy pruneStrategy, final Map, Set> ignoredVarRegistry) { return new AasporRefiner<>(refiner, pruneStrategy, ignoredVarRegistry); } @Override - public RefinerResult refine(final ARG arg, final P prec) { - final RefinerResult result = refiner.refine(arg, prec); + public RefinerResult> refine(final ARG arg, final P prec) { + final RefinerResult> result = refiner.refine(arg, prec); if (result.isUnsafe() || pruneStrategy != PruneStrategy.LAZY) return result; final P newPrec = result.asSpurious().getRefinedPrec(); diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/expr/refinement/MultiExprTraceRefiner.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/expr/refinement/MultiExprTraceRefiner.java index 72c516adef..b2cee796d0 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/expr/refinement/MultiExprTraceRefiner.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/expr/refinement/MultiExprTraceRefiner.java @@ -20,7 +20,7 @@ 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.arg.ArgTrace; -import hu.bme.mit.theta.analysis.algorithm.cegar.Refiner; +import hu.bme.mit.theta.analysis.algorithm.cegar.ArgRefiner; import hu.bme.mit.theta.analysis.algorithm.cegar.RefinerResult; import hu.bme.mit.theta.analysis.expr.ExprAction; import hu.bme.mit.theta.analysis.expr.ExprState; @@ -34,7 +34,7 @@ import static com.google.common.base.Preconditions.checkNotNull; public final class MultiExprTraceRefiner - implements Refiner { + implements ArgRefiner { private final ExprTraceChecker exprTraceChecker; private final PrecRefiner precRefiner; @@ -76,17 +76,17 @@ public static refine(final ARG arg, final P prec) { + public RefinerResult> refine(final ARG arg, final P prec) { checkNotNull(arg); checkNotNull(prec); assert !arg.isSafe() : "ARG must be unsafe"; - final List> cexs = arg.getCexs().collect(Collectors.toList()); - final List> traces = arg.getCexs().map(ArgTrace::toTrace).collect(Collectors.toList()); + final List> cexs = arg.getCexs().toList(); + final List> traces = arg.getCexs().map(ArgTrace::toTrace).toList(); assert traces.size() == cexs.size(); logger.write(Level.INFO, "| | Number of traces: %d%n", traces.size()); - assert traces.size() > 0 : "No counterexample in ARG"; + assert !traces.isEmpty() : "No counterexample in ARG"; logger.write(Level.SUBSTEP, "| | Checking traces..."); final List> cexStatuses = new ArrayList<>(traces.size()); @@ -106,7 +106,7 @@ public RefinerResult refine(final ARG arg, final P prec) { assert cexStatuses.size() == cexs.size(); logger.write(Level.SUBSTEP, "done, result: all infeasible%n"); final List refutations = cexStatuses.stream().map(s -> s.asInfeasible().getRefutation()) - .collect(Collectors.toList()); + .toList(); assert refutations.size() == cexs.size(); final List> nodesToPrune = new ArrayList<>(traces.size()); @@ -120,7 +120,7 @@ public RefinerResult refine(final ARG arg, final P prec) { for (int i = 0; i < nodesToPrune.size(); ++i) { final ArgNode node = nodesToPrune.get(i); - if (node.properAncestors().anyMatch(a -> nodesToPrune.contains(a))) { + if (node.properAncestors().anyMatch(nodesToPrune::contains)) { skip.set(i, true); } } diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/expr/refinement/SingleExprTraceRefiner.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/expr/refinement/SingleExprTraceRefiner.java index ac06cf2a87..126f4212f4 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/expr/refinement/SingleExprTraceRefiner.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/expr/refinement/SingleExprTraceRefiner.java @@ -20,7 +20,7 @@ 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.arg.ArgTrace; -import hu.bme.mit.theta.analysis.algorithm.cegar.Refiner; +import hu.bme.mit.theta.analysis.algorithm.cegar.ArgRefiner; import hu.bme.mit.theta.analysis.algorithm.cegar.RefinerResult; import hu.bme.mit.theta.analysis.expr.ExprAction; import hu.bme.mit.theta.analysis.expr.ExprState; @@ -37,7 +37,7 @@ * ExprActions) using an ExprTraceChecker and a PrecRefiner. */ public class SingleExprTraceRefiner - implements Refiner { + implements ArgRefiner { protected final ExprTraceChecker exprTraceChecker; protected final PrecRefiner precRefiner; protected final PruneStrategy pruneStrategy; @@ -78,7 +78,7 @@ public static refine(final ARG arg, final P prec) { + public RefinerResult> refine(final ARG arg, final P prec) { checkNotNull(arg); checkNotNull(prec); assert !arg.isSafe() : "ARG must be unsafe"; 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 9992e5a3e7..c4c82eeb74 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 @@ -36,7 +36,7 @@ import hu.bme.mit.theta.common.visualization.LineStyle; import hu.bme.mit.theta.common.visualization.NodeAttributes; -public final class ArgVisualizer { +public final class ArgVisualizer implements WitnessVisualizer> { private static final LineStyle COVER_EDGE_STYLE = LineStyle.DASHED; private static final LineStyle SUCC_EDGE_STYLE = LineStyle.NORMAL; @@ -53,8 +53,8 @@ public final class ArgVisualizer { private static class LazyHolderDefault { - static final ArgVisualizer INSTANCE = new ArgVisualizer<>(s -> s.toString(), - a -> a.toString()); + static final ArgVisualizer INSTANCE = new ArgVisualizer<>(Object::toString, + Object::toString); } private static class LazyHolderStructureOnly { @@ -81,6 +81,7 @@ public static ArgVisualizer getStructureOnly() { return LazyHolderStructureOnly.INSTANCE; } + @Override public Graph visualize(final ARG arg) { final Graph graph = new Graph(ARG_ID, ARG_LABEL); 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/WitnessVisualizer.java new file mode 100644 index 0000000000..bd1a9d8234 --- /dev/null +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/utils/WitnessVisualizer.java @@ -0,0 +1,26 @@ +/* + * 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.analysis.utils; + +import hu.bme.mit.theta.analysis.algorithm.Witness; +import hu.bme.mit.theta.common.visualization.Graph; + +public interface WitnessVisualizer { + + Graph visualize(W witness); + +} diff --git a/subprojects/common/analysis/src/main/kotlin/hu/bme/mit/theta/analysis/multi/config/StmtMultiConfigBuilder.kt b/subprojects/common/analysis/src/main/kotlin/hu/bme/mit/theta/analysis/multi/config/StmtMultiConfigBuilder.kt index 2e7f57a91a..e0d8173455 100644 --- a/subprojects/common/analysis/src/main/kotlin/hu/bme/mit/theta/analysis/multi/config/StmtMultiConfigBuilder.kt +++ b/subprojects/common/analysis/src/main/kotlin/hu/bme/mit/theta/analysis/multi/config/StmtMultiConfigBuilder.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.multi.config import hu.bme.mit.theta.analysis.Prec import hu.bme.mit.theta.analysis.algorithm.arg.ArgBuilder -import hu.bme.mit.theta.analysis.algorithm.cegar.BasicAbstractor -import hu.bme.mit.theta.analysis.algorithm.cegar.CegarChecker +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.ExprState import hu.bme.mit.theta.analysis.expr.StmtAction import hu.bme.mit.theta.analysis.expr.refinement.* @@ -39,117 +38,264 @@ import hu.bme.mit.theta.solver.SolverFactory import hu.bme.mit.theta.solver.UCSolver import java.util.function.Predicate -sealed class StmtMultiConfigBuilder( - private val product: MultiBuilderResultPOJO, ExprMultiState, StmtMultiAction, StmtMultiLts>, - val prop: Expr, - val target: Predicate>, - private val lRefToPrec: RefutationToPrec, - private val rRefToPrec: RefutationToPrec, - private val dRefToPrec: RefutationToPrec, - private val lInitPrec: LPrec, - private val rInitPrec: RPrec, - private val dInitPrec: DataPrec, - val solverFactory: SolverFactory, - val logger: Logger, - val pruneStrategy: PruneStrategy = PruneStrategy.FULL +sealed class StmtMultiConfigBuilder< + LState : ExprState, + RState : ExprState, + DataState : ExprState, + LControl : ExprState, + RControl : ExprState, + LAction : StmtAction, + RAction : StmtAction, + R : Refutation, + LPrec : Prec, + RPrec : Prec, + DataPrec : Prec, + LControlPrec : Prec, + RControlPrec : Prec, +>( + private val product: + MultiBuilderResultPOJO< + LState, + RState, + DataState, + LControl, + RControl, + LAction, + RAction, + LPrec, + RPrec, + DataPrec, + LControlPrec, + RControlPrec, + ExprMultiState, + ExprMultiState, + StmtMultiAction, + StmtMultiLts, + >, + val prop: Expr, + val target: Predicate>, + private val lRefToPrec: RefutationToPrec, + private val rRefToPrec: RefutationToPrec, + private val dRefToPrec: RefutationToPrec, + private val lInitPrec: LPrec, + private val rInitPrec: RPrec, + private val dInitPrec: DataPrec, + val solverFactory: SolverFactory, + val logger: Logger, + val pruneStrategy: PruneStrategy = PruneStrategy.FULL, ) { - abstract fun getTraceChecker(): ExprTraceChecker + abstract fun getTraceChecker(): ExprTraceChecker - fun build(): MultiConfig, StmtMultiAction> { - val argBuilder = ArgBuilder.create(product.lts, product.side.analysis, target) - val abstractor = BasicAbstractor.builder(argBuilder).build() - val traceChecker = getTraceChecker() - val precRefiner = - JoiningPrecRefiner.create, StmtMultiAction, MultiPrec, R>( - RefToMultiPrec(lRefToPrec, rRefToPrec, dRefToPrec) - ) - val refiner = SingleExprTraceRefiner.create(traceChecker, precRefiner, pruneStrategy, logger) - return MultiConfig(CegarChecker.create(abstractor, refiner), MultiPrec(lInitPrec, rInitPrec, dInitPrec)) - } + fun build(): + MultiConfig< + DataState, + LControl, + RControl, + LAction, + RAction, + LPrec, + RPrec, + DataPrec, + ExprMultiState, + StmtMultiAction, + > { + val argBuilder = ArgBuilder.create(product.lts, product.side.analysis, target) + val abstractor = BasicArgAbstractor.builder(argBuilder).build() + val traceChecker = getTraceChecker() + val precRefiner = + JoiningPrecRefiner.create< + ExprMultiState, + StmtMultiAction, + MultiPrec, + R, + >( + RefToMultiPrec(lRefToPrec, rRefToPrec, dRefToPrec) + ) + val refiner = SingleExprTraceRefiner.create(traceChecker, precRefiner, pruneStrategy, logger) + return MultiConfig( + ArgCegarChecker.create(abstractor, refiner), + MultiPrec(lInitPrec, rInitPrec, dInitPrec), + ) + } - class ItpStmtMultiConfigBuilder( - product: MultiBuilderResultPOJO, ExprMultiState, StmtMultiAction, StmtMultiLts>, - prop: Expr, - target: Predicate>, - lRefToPrec: RefutationToPrec, - rRefToPrec: RefutationToPrec, - dRefToPrec: RefutationToPrec, - lInitPrec: LPrec, - rInitPrec: RPrec, - dInitPrec: DataPrec, - solverFactory: SolverFactory, - logger: Logger, - pruneStrategy: PruneStrategy = PruneStrategy.FULL, - private val traceCheckerType: TraceCheckerType = TraceCheckerType.SEQ_ITP - ) : StmtMultiConfigBuilder( - product, - prop, - target, - lRefToPrec, - rRefToPrec, - dRefToPrec, - lInitPrec, - rInitPrec, - dInitPrec, - solverFactory, - logger, - pruneStrategy + class ItpStmtMultiConfigBuilder< + LState : ExprState, + RState : ExprState, + DataState : ExprState, + LControl : ExprState, + RControl : ExprState, + LAction : StmtAction, + RAction : StmtAction, + LPrec : Prec, + RPrec : Prec, + DataPrec : Prec, + LControlPrec : Prec, + RControlPrec : Prec, + >( + product: + MultiBuilderResultPOJO< + LState, + RState, + DataState, + LControl, + RControl, + LAction, + RAction, + LPrec, + RPrec, + DataPrec, + LControlPrec, + RControlPrec, + ExprMultiState, + ExprMultiState, + StmtMultiAction, + StmtMultiLts, + >, + prop: Expr, + target: Predicate>, + lRefToPrec: RefutationToPrec, + rRefToPrec: RefutationToPrec, + dRefToPrec: RefutationToPrec, + lInitPrec: LPrec, + rInitPrec: RPrec, + dInitPrec: DataPrec, + solverFactory: SolverFactory, + logger: Logger, + pruneStrategy: PruneStrategy = PruneStrategy.FULL, + private val traceCheckerType: TraceCheckerType = TraceCheckerType.SEQ_ITP, + ) : + StmtMultiConfigBuilder< + LState, + RState, + DataState, + LControl, + RControl, + LAction, + RAction, + ItpRefutation, + LPrec, + RPrec, + DataPrec, + LControlPrec, + RControlPrec, + >( + product, + prop, + target, + lRefToPrec, + rRefToPrec, + dRefToPrec, + lInitPrec, + rInitPrec, + dInitPrec, + solverFactory, + logger, + pruneStrategy, ) { - enum class TraceCheckerType( - val generator: (init: Expr, target: Expr, solver: ItpSolver) -> ExprTraceChecker - ) { - - SEQ_ITP(ExprTraceSeqItpChecker::create), FW_BIN(ExprTraceFwBinItpChecker::create), BW_BIN( - ExprTraceBwBinItpChecker::create - ) - } + enum class TraceCheckerType( + val generator: + (init: Expr, target: Expr, solver: ItpSolver) -> ExprTraceChecker< + ItpRefutation + > + ) { - override fun getTraceChecker(): ExprTraceChecker = traceCheckerType.generator( - BoolExprs.True(), prop, solverFactory.createItpSolver() - ) + SEQ_ITP(ExprTraceSeqItpChecker::create), + FW_BIN(ExprTraceFwBinItpChecker::create), + BW_BIN(ExprTraceBwBinItpChecker::create), } - class VarsStmtMultiConfigBuilder( - product: MultiBuilderResultPOJO, ExprMultiState, StmtMultiAction, StmtMultiLts>, - prop: Expr, - target: Predicate>, - lRefToPrec: RefutationToPrec, - rRefToPrec: RefutationToPrec, - dRefToPrec: RefutationToPrec, - lInitPrec: LPrec, - rInitPrec: RPrec, - dInitPrec: DataPrec, - solverFactory: SolverFactory, - logger: Logger, - pruneStrategy: PruneStrategy = PruneStrategy.FULL, - private val traceCheckerType: TraceCheckerType = TraceCheckerType.UNSAT_CORE - ) : StmtMultiConfigBuilder( - product, - prop, - target, - lRefToPrec, - rRefToPrec, - dRefToPrec, - lInitPrec, - rInitPrec, - dInitPrec, - solverFactory, - logger, - pruneStrategy - ) { + override fun getTraceChecker(): ExprTraceChecker = + traceCheckerType.generator(BoolExprs.True(), prop, solverFactory.createItpSolver()) + } - enum class TraceCheckerType( - val generator: (init: Expr, target: Expr, solver: UCSolver) -> ExprTraceChecker - ) { + class VarsStmtMultiConfigBuilder< + LState : ExprState, + RState : ExprState, + DataState : ExprState, + LControl : ExprState, + RControl : ExprState, + LAction : StmtAction, + RAction : StmtAction, + LPrec : Prec, + RPrec : Prec, + DataPrec : Prec, + LControlPrec : Prec, + RControlPrec : Prec, + >( + product: + MultiBuilderResultPOJO< + LState, + RState, + DataState, + LControl, + RControl, + LAction, + RAction, + LPrec, + RPrec, + DataPrec, + LControlPrec, + RControlPrec, + ExprMultiState, + ExprMultiState, + StmtMultiAction, + StmtMultiLts, + >, + prop: Expr, + target: Predicate>, + lRefToPrec: RefutationToPrec, + rRefToPrec: RefutationToPrec, + dRefToPrec: RefutationToPrec, + lInitPrec: LPrec, + rInitPrec: RPrec, + dInitPrec: DataPrec, + solverFactory: SolverFactory, + logger: Logger, + pruneStrategy: PruneStrategy = PruneStrategy.FULL, + private val traceCheckerType: TraceCheckerType = TraceCheckerType.UNSAT_CORE, + ) : + StmtMultiConfigBuilder< + LState, + RState, + DataState, + LControl, + RControl, + LAction, + RAction, + VarsRefutation, + LPrec, + RPrec, + DataPrec, + LControlPrec, + RControlPrec, + >( + product, + prop, + target, + lRefToPrec, + rRefToPrec, + dRefToPrec, + lInitPrec, + rInitPrec, + dInitPrec, + solverFactory, + logger, + pruneStrategy, + ) { - UNSAT_CORE(ExprTraceUnsatCoreChecker::create) - } + enum class TraceCheckerType( + val generator: + (init: Expr, target: Expr, solver: UCSolver) -> ExprTraceChecker< + VarsRefutation + > + ) { - override fun getTraceChecker(): ExprTraceChecker = traceCheckerType.generator( - BoolExprs.True(), prop, solverFactory.createUCSolver() - ) + UNSAT_CORE(ExprTraceUnsatCoreChecker::create) } + override fun getTraceChecker(): ExprTraceChecker = + traceCheckerType.generator(BoolExprs.True(), prop, solverFactory.createUCSolver()) + } } diff --git a/subprojects/sts/sts-analysis/src/main/java/hu/bme/mit/theta/sts/analysis/config/StsConfigBuilder.java b/subprojects/sts/sts-analysis/src/main/java/hu/bme/mit/theta/sts/analysis/config/StsConfigBuilder.java index 397a4a4ef8..7e946253e9 100644 --- a/subprojects/sts/sts-analysis/src/main/java/hu/bme/mit/theta/sts/analysis/config/StsConfigBuilder.java +++ b/subprojects/sts/sts-analysis/src/main/java/hu/bme/mit/theta/sts/analysis/config/StsConfigBuilder.java @@ -15,16 +15,18 @@ */ package hu.bme.mit.theta.sts.analysis.config; +import static hu.bme.mit.theta.core.type.booltype.BoolExprs.Not; + import hu.bme.mit.theta.analysis.*; +import hu.bme.mit.theta.analysis.algorithm.SafetyChecker; 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.arg.ArgNodeComparators.ArgNodeComparator; -import hu.bme.mit.theta.analysis.algorithm.SafetyChecker; -import hu.bme.mit.theta.analysis.algorithm.cegar.Abstractor; -import hu.bme.mit.theta.analysis.algorithm.cegar.BasicAbstractor; -import hu.bme.mit.theta.analysis.algorithm.cegar.CegarChecker; -import hu.bme.mit.theta.analysis.algorithm.cegar.Refiner; +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; +import hu.bme.mit.theta.analysis.algorithm.cegar.BasicArgAbstractor; import hu.bme.mit.theta.analysis.algorithm.cegar.abstractor.StopCriterions; import hu.bme.mit.theta.analysis.expl.ExplAnalysis; import hu.bme.mit.theta.analysis.expl.ExplPrec; @@ -66,19 +68,23 @@ import hu.bme.mit.theta.sts.analysis.initprec.StsEmptyInitPrec; import hu.bme.mit.theta.sts.analysis.initprec.StsInitPrec; import hu.bme.mit.theta.sts.analysis.initprec.StsPropInitPrec; - import java.util.function.Predicate; -import static hu.bme.mit.theta.core.type.booltype.BoolExprs.Not; - public final class StsConfigBuilder { public enum Domain { - EXPL, PRED_BOOL, PRED_CART, PRED_SPLIT + EXPL, + PRED_BOOL, + PRED_CART, + PRED_SPLIT } public enum Refinement { - FW_BIN_ITP, BW_BIN_ITP, SEQ_ITP, MULTI_SEQ, UNSAT_CORE + FW_BIN_ITP, + BW_BIN_ITP, + SEQ_ITP, + MULTI_SEQ, + UNSAT_CORE } public enum Search { @@ -91,7 +97,6 @@ public enum Search { private Search(final ArgNodeComparator comparator) { this.comparator = comparator; } - } public enum PredSplit { @@ -109,14 +114,14 @@ private PredSplit(final ExprSplitter splitter) { } public enum InitPrec { - EMPTY(new StsEmptyInitPrec()), PROP(new StsPropInitPrec()); + EMPTY(new StsEmptyInitPrec()), + PROP(new StsPropInitPrec()); public final StsInitPrec builder; private InitPrec(final StsInitPrec builder) { this.builder = builder; } - } private Logger logger = NullLogger.getInstance(); @@ -128,8 +133,8 @@ private InitPrec(final StsInitPrec builder) { private InitPrec initPrec = InitPrec.EMPTY; private PruneStrategy pruneStrategy = PruneStrategy.LAZY; - public StsConfigBuilder(final Domain domain, final Refinement refinement, - final SolverFactory solverFactory) { + public StsConfigBuilder( + final Domain domain, final Refinement refinement, final SolverFactory solverFactory) { this.domain = domain; this.refinement = refinement; this.solverFactory = solverFactory; @@ -168,63 +173,80 @@ public StsConfigBuilder pruneStrategy(final PruneStrategy pruneStrategy) { if (domain == Domain.EXPL) { final Solver analysisSolver = solverFactory.createSolver(); final Predicate target = new ExplStatePredicate(negProp, analysisSolver); - final Analysis analysis = ExplAnalysis.create( - analysisSolver, init); - final ArgBuilder argBuilder = ArgBuilder.create(lts, - analysis, target, - true); - final Abstractor abstractor = BasicAbstractor.builder( - argBuilder) - .waitlist(PriorityWaitlist.create(search.comparator)) - .stopCriterion(refinement == Refinement.MULTI_SEQ ? StopCriterions.fullExploration() - : StopCriterions.firstCex()) - .logger(logger).build(); - - Refiner refiner = null; + final Analysis analysis = + ExplAnalysis.create(analysisSolver, init); + final ArgBuilder argBuilder = + ArgBuilder.create(lts, analysis, target, true); + final ArgAbstractor abstractor = + BasicArgAbstractor.builder(argBuilder) + .waitlist(PriorityWaitlist.create(search.comparator)) + .stopCriterion( + refinement == Refinement.MULTI_SEQ + ? StopCriterions.fullExploration() + : StopCriterions.firstCex()) + .logger(logger) + .build(); + + ArgRefiner refiner = null; switch (refinement) { case FW_BIN_ITP: - refiner = SingleExprTraceRefiner.create( - ExprTraceFwBinItpChecker.create(init, negProp, - solverFactory.createItpSolver()), - JoiningPrecRefiner.create(new ItpRefToExplPrec()), pruneStrategy, logger); + refiner = + SingleExprTraceRefiner.create( + ExprTraceFwBinItpChecker.create( + init, negProp, solverFactory.createItpSolver()), + JoiningPrecRefiner.create(new ItpRefToExplPrec()), + pruneStrategy, + logger); break; case BW_BIN_ITP: - refiner = SingleExprTraceRefiner.create( - ExprTraceBwBinItpChecker.create(init, negProp, - solverFactory.createItpSolver()), - JoiningPrecRefiner.create(new ItpRefToExplPrec()), pruneStrategy, logger); + refiner = + SingleExprTraceRefiner.create( + ExprTraceBwBinItpChecker.create( + init, negProp, solverFactory.createItpSolver()), + JoiningPrecRefiner.create(new ItpRefToExplPrec()), + pruneStrategy, + logger); break; case SEQ_ITP: - refiner = SingleExprTraceRefiner.create( - ExprTraceSeqItpChecker.create(init, negProp, - solverFactory.createItpSolver()), - JoiningPrecRefiner.create(new ItpRefToExplPrec()), pruneStrategy, logger); + refiner = + SingleExprTraceRefiner.create( + ExprTraceSeqItpChecker.create( + init, negProp, solverFactory.createItpSolver()), + JoiningPrecRefiner.create(new ItpRefToExplPrec()), + pruneStrategy, + logger); break; case MULTI_SEQ: - refiner = MultiExprTraceRefiner.create( - ExprTraceSeqItpChecker.create(init, negProp, - solverFactory.createItpSolver()), - JoiningPrecRefiner.create(new ItpRefToExplPrec()), pruneStrategy, logger); + refiner = + MultiExprTraceRefiner.create( + ExprTraceSeqItpChecker.create( + init, negProp, solverFactory.createItpSolver()), + JoiningPrecRefiner.create(new ItpRefToExplPrec()), + pruneStrategy, + logger); break; case UNSAT_CORE: - refiner = SingleExprTraceRefiner.create( - ExprTraceUnsatCoreChecker.create(init, negProp, - solverFactory.createUCSolver()), - JoiningPrecRefiner.create(new VarsRefToExplPrec()), pruneStrategy, logger); + refiner = + SingleExprTraceRefiner.create( + ExprTraceUnsatCoreChecker.create( + init, negProp, solverFactory.createUCSolver()), + JoiningPrecRefiner.create(new VarsRefToExplPrec()), + pruneStrategy, + logger); break; default: throw new UnsupportedOperationException( domain + " domain does not support " + refinement + " refinement."); } - final SafetyChecker, Trace, ExplPrec> checker = CegarChecker.create( - abstractor, refiner, - logger); + final SafetyChecker, Trace, ExplPrec> + checker = ArgCegarChecker.create(abstractor, refiner, logger); final ExplPrec prec = initPrec.builder.createExpl(sts); return StsConfig.create(checker, prec); - } else if (domain == Domain.PRED_BOOL || domain == Domain.PRED_CART + } else if (domain == Domain.PRED_BOOL + || domain == Domain.PRED_CART || domain == Domain.PRED_SPLIT) { final Solver analysisSolver = solverFactory.createSolver(); PredAbstractor predAbstractor = null; @@ -242,55 +264,65 @@ public StsConfigBuilder pruneStrategy(final PruneStrategy pruneStrategy) { throw new UnsupportedOperationException(domain + " domain is not supported."); } final Predicate target = new ExprStatePredicate(negProp, analysisSolver); - final Analysis analysis = PredAnalysis.create( - analysisSolver, predAbstractor, - init); - final ArgBuilder argBuilder = ArgBuilder.create(lts, - analysis, target, - true); - final Abstractor abstractor = BasicAbstractor.builder( - argBuilder) - .waitlist(PriorityWaitlist.create(search.comparator)) - .stopCriterion(refinement == Refinement.MULTI_SEQ ? StopCriterions.fullExploration() - : StopCriterions.firstCex()) - .logger(logger).build(); + final Analysis analysis = + PredAnalysis.create(analysisSolver, predAbstractor, init); + final ArgBuilder argBuilder = + ArgBuilder.create(lts, analysis, target, true); + final ArgAbstractor abstractor = + BasicArgAbstractor.builder(argBuilder) + .waitlist(PriorityWaitlist.create(search.comparator)) + .stopCriterion( + refinement == Refinement.MULTI_SEQ + ? StopCriterions.fullExploration() + : StopCriterions.firstCex()) + .logger(logger) + .build(); ExprTraceChecker exprTraceChecker = null; switch (refinement) { case FW_BIN_ITP: - exprTraceChecker = ExprTraceFwBinItpChecker.create(init, negProp, - solverFactory.createItpSolver()); + exprTraceChecker = + ExprTraceFwBinItpChecker.create( + init, negProp, solverFactory.createItpSolver()); break; case BW_BIN_ITP: - exprTraceChecker = ExprTraceBwBinItpChecker.create(init, negProp, - solverFactory.createItpSolver()); + exprTraceChecker = + ExprTraceBwBinItpChecker.create( + init, negProp, solverFactory.createItpSolver()); break; case SEQ_ITP: - exprTraceChecker = ExprTraceSeqItpChecker.create(init, negProp, - solverFactory.createItpSolver()); + exprTraceChecker = + ExprTraceSeqItpChecker.create( + init, negProp, solverFactory.createItpSolver()); break; case MULTI_SEQ: - exprTraceChecker = ExprTraceSeqItpChecker.create(init, negProp, - solverFactory.createItpSolver()); + exprTraceChecker = + ExprTraceSeqItpChecker.create( + init, negProp, solverFactory.createItpSolver()); break; default: throw new UnsupportedOperationException( domain + " domain does not support " + refinement + " refinement."); } - Refiner refiner; + ArgRefiner refiner; if (refinement == Refinement.MULTI_SEQ) { - refiner = MultiExprTraceRefiner.create(exprTraceChecker, - JoiningPrecRefiner.create(new ItpRefToPredPrec(predSplit.splitter)), - pruneStrategy, logger); + refiner = + MultiExprTraceRefiner.create( + exprTraceChecker, + JoiningPrecRefiner.create(new ItpRefToPredPrec(predSplit.splitter)), + pruneStrategy, + logger); } else { - refiner = SingleExprTraceRefiner.create(exprTraceChecker, - JoiningPrecRefiner.create(new ItpRefToPredPrec(predSplit.splitter)), - pruneStrategy, logger); + refiner = + SingleExprTraceRefiner.create( + exprTraceChecker, + JoiningPrecRefiner.create(new ItpRefToPredPrec(predSplit.splitter)), + pruneStrategy, + logger); } - final SafetyChecker, Trace, PredPrec> checker = CegarChecker.create( - abstractor, refiner, - logger); + final SafetyChecker, Trace, PredPrec> + checker = ArgCegarChecker.create(abstractor, refiner, logger); final PredPrec prec = initPrec.builder.createPred(sts); return StsConfig.create(checker, prec); 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 db171f2718..4f2f998af5 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 @@ -24,9 +24,9 @@ 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.Abstractor; -import hu.bme.mit.theta.analysis.algorithm.cegar.BasicAbstractor; -import hu.bme.mit.theta.analysis.algorithm.cegar.CegarChecker; +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.expl.ExplAnalysis; import hu.bme.mit.theta.analysis.expl.ExplPrec; import hu.bme.mit.theta.analysis.expl.ExplState; @@ -110,7 +110,7 @@ public void test() { final ArgBuilder argBuilder = ArgBuilder.create(lts, analysis, target); - final Abstractor abstractor = BasicAbstractor.builder( + final ArgAbstractor abstractor = BasicArgAbstractor.builder( argBuilder) .waitlist(PriorityWaitlist.create(ArgNodeComparators.bfs())).logger(logger).build(); @@ -122,7 +122,7 @@ public void test() { .create(exprTraceChecker, JoiningPrecRefiner.create(new VarsRefToExplPrec()), PruneStrategy.LAZY, logger); - final SafetyChecker, Trace, ExplPrec> checker = CegarChecker.create( + final SafetyChecker, Trace, ExplPrec> checker = ArgCegarChecker.create( abstractor, refiner, logger); final SafetyResult, Trace> safetyStatus = checker.check(prec); 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 5eea722540..bed9497f54 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 @@ -44,9 +44,9 @@ 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.Abstractor; -import hu.bme.mit.theta.analysis.algorithm.cegar.BasicAbstractor; -import hu.bme.mit.theta.analysis.algorithm.cegar.CegarChecker; +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.expr.ExprAction; import hu.bme.mit.theta.analysis.expr.ExprState; import hu.bme.mit.theta.analysis.expr.ExprStatePredicate; @@ -104,7 +104,7 @@ public void testPredPrec() { final ArgBuilder argBuilder = ArgBuilder.create(lts, analysis, target); - final Abstractor abstractor = BasicAbstractor.builder( + final ArgAbstractor abstractor = BasicArgAbstractor.builder( argBuilder).logger(logger) .build(); @@ -117,7 +117,7 @@ public void testPredPrec() { JoiningPrecRefiner.create(new ItpRefToPredPrec(ExprSplitters.atoms())), PruneStrategy.LAZY, logger); - final SafetyChecker, Trace, PredPrec> checker = CegarChecker.create( + final SafetyChecker, Trace, PredPrec> checker = ArgCegarChecker.create( abstractor, refiner, logger); final SafetyResult, Trace> safetyStatus = checker.check(prec); diff --git a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaAbstractor.kt b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaAbstractor.kt deleted file mode 100644 index d17f15fda1..0000000000 --- a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaAbstractor.kt +++ /dev/null @@ -1,137 +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.analysis - -import com.google.common.base.Preconditions -import hu.bme.mit.theta.analysis.Action -import hu.bme.mit.theta.analysis.Prec -import hu.bme.mit.theta.analysis.State -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.ArgNode -import hu.bme.mit.theta.analysis.algorithm.cegar.AbstractorResult -import hu.bme.mit.theta.analysis.algorithm.cegar.BasicAbstractor -import hu.bme.mit.theta.analysis.algorithm.cegar.abstractor.StopCriterion -import hu.bme.mit.theta.analysis.reachedset.Partition -import hu.bme.mit.theta.analysis.waitlist.Waitlist -import hu.bme.mit.theta.common.logging.Logger -import java.util.function.Function - -class XcfaAbstractor( - argBuilder: ArgBuilder, - projection: Function?, - waitlist: Waitlist>, - stopCriterion: StopCriterion, - logger: Logger, -) : BasicAbstractor(argBuilder, projection, waitlist, stopCriterion, logger) { - - override fun check(arg: ARG, prec: P): AbstractorResult { - logger.write(Logger.Level.DETAIL, "| | Precision: %s%n", prec) - - if (!arg.isInitialized) { - logger.write(Logger.Level.SUBSTEP, "| | (Re)initializing ARG...") - argBuilder.init(arg, prec) - logger.write(Logger.Level.SUBSTEP, "done%n") - } - - assert(arg.isInitialized) - - logger.write( - Logger.Level.INFO, "| | Starting ARG: %d nodes, %d incomplete, %d unsafe%n", arg.nodes.count(), - arg.incompleteNodes.count(), arg.unsafeNodes.count() - ) - logger.write(Logger.Level.SUBSTEP, "| | Building ARG...") - - val reachedSet: Partition, *> = Partition.of { n: ArgNode -> - projection.apply(n.state) - } - waitlist.clear() - - reachedSet.addAll(arg.nodes) - waitlist.addAll(arg.incompleteNodes) - - if (!stopCriterion.canStop(arg)) { - while (!waitlist.isEmpty) { - val node = waitlist.remove() - var newNodes: Collection>? = emptyList() - if ((node.state as XcfaState<*>).xcfa!!.isInlined) { - close(node, reachedSet[node]) - } else { - val expandProcedureCall = (node.state as XcfaState<*>) in (prec as XcfaPrec

).noPop - closePop(node, reachedSet[node], !expandProcedureCall) - } - if (!node.isSubsumed && !node.isTarget) { - newNodes = argBuilder.expand(node, prec) - reachedSet.addAll(newNodes) - waitlist.addAll(newNodes) - } - if (stopCriterion.canStop(arg, newNodes)) break - } - } - - logger.write(Logger.Level.SUBSTEP, "done%n") - logger.write( - Logger.Level.INFO, "| | Finished ARG: %d nodes, %d incomplete, %d unsafe%n", arg.nodes.count(), - arg.incompleteNodes.count(), arg.unsafeNodes.count() - ) - - waitlist.clear() // Optimization - - return if (arg.isSafe) { - Preconditions.checkState(arg.isComplete, "Returning incomplete ARG as safe") - AbstractorResult.safe() - } else { - AbstractorResult.unsafe() - } - } - - fun closePop(node: ArgNode, candidates: Collection>, popCovered: Boolean) { - if (!node.isLeaf) { - return - } - for (candidate in candidates) { - if (candidate.mayCover(node)) { - var onlyStackCovers = false - (node.state as XcfaState<*>).processes.forEach { (pid: Int, proc: XcfaProcessState) -> - if (proc != (candidate.state as XcfaState<*>).processes[pid]) { - if (popCovered) proc.popped = proc.locs.pop() - onlyStackCovers = true - } - } - if (!onlyStackCovers) { - node.cover(candidate) - } - return - } - } - } - - companion object { - - fun builder( - argBuilder: ArgBuilder): BasicAbstractor.Builder { - return Builder(argBuilder) - } - } - - class Builder(argBuilder: ArgBuilder) - : BasicAbstractor.Builder(argBuilder) { - - override fun build(): BasicAbstractor { - return XcfaAbstractor(argBuilder, projection, waitlist, stopCriterion, logger) - } - } -} diff --git a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaAnalysis.kt b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaAnalysis.kt index 64bd2e3d62..f923d0e6f0 100644 --- a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaAnalysis.kt +++ b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaAnalysis.kt @@ -13,13 +13,12 @@ * See the License for the specific language governing permissions and * limitations under the License. */ - package hu.bme.mit.theta.xcfa.analysis import hu.bme.mit.theta.analysis.* import hu.bme.mit.theta.analysis.algorithm.arg.ArgBuilder import hu.bme.mit.theta.analysis.algorithm.arg.ArgNode -import hu.bme.mit.theta.analysis.algorithm.cegar.Abstractor +import hu.bme.mit.theta.analysis.algorithm.cegar.ArgAbstractor import hu.bme.mit.theta.analysis.algorithm.cegar.abstractor.StopCriterion import hu.bme.mit.theta.analysis.expl.ExplInitFunc import hu.bme.mit.theta.analysis.expl.ExplPrec @@ -54,251 +53,364 @@ import java.util.* import java.util.function.Predicate open class XcfaAnalysis( - private val corePartialOrd: PartialOrd>>, - private val coreInitFunc: InitFunc>, XcfaPrec

>, - private var coreTransFunc: TransFunc>, XcfaAction, XcfaPrec

>, + private val corePartialOrd: PartialOrd>>, + private val coreInitFunc: InitFunc>, XcfaPrec

>, + private var coreTransFunc: TransFunc>, XcfaAction, XcfaPrec

>, ) : Analysis>, XcfaAction, XcfaPrec

> { - init { - ConeOfInfluence.coreTransFunc = transFunc as TransFunc>, XcfaAction, XcfaPrec> - coreTransFunc = ConeOfInfluence.transFunc as TransFunc>, XcfaAction, XcfaPrec

> - } + init { + ConeOfInfluence.coreTransFunc = + transFunc as TransFunc>, XcfaAction, XcfaPrec> + coreTransFunc = + ConeOfInfluence.transFunc as TransFunc>, XcfaAction, XcfaPrec

> + } + + override fun getPartialOrd(): PartialOrd>> = corePartialOrd + + override fun getInitFunc(): InitFunc>, XcfaPrec

> = coreInitFunc - override fun getPartialOrd(): PartialOrd>> = corePartialOrd - override fun getInitFunc(): InitFunc>, XcfaPrec

> = coreInitFunc - override fun getTransFunc(): TransFunc>, XcfaAction, XcfaPrec

> = coreTransFunc + override fun getTransFunc(): TransFunc>, XcfaAction, XcfaPrec

> = + coreTransFunc } /// Common private var tempCnt: Int = 0 -fun getCoreXcfaLts() = LTS>, XcfaAction> { s -> - s.processes.map { proc -> + +fun getCoreXcfaLts() = + LTS>, XcfaAction> { s -> + s.processes + .map { proc -> if (proc.value.locs.peek().final) { - listOf(XcfaAction(proc.key, - XcfaEdge(proc.value.locs.peek(), proc.value.locs.peek(), SequenceLabel(listOf( + listOf( + XcfaAction( + proc.key, + XcfaEdge( + proc.value.locs.peek(), + proc.value.locs.peek(), + SequenceLabel( + listOf( proc.value.paramStmts.peek().second, ReturnLabel(proc.value.returnStmts.peek()), - ))), nextCnt = s.sGlobal.nextCnt)) + ) + ), + ), + nextCnt = s.sGlobal.nextCnt, + ) + ) } else if (!proc.value.paramsInitialized) { - listOf(XcfaAction(proc.key, XcfaEdge(proc.value.locs.peek(), proc.value.locs.peek(), - proc.value.paramStmts.peek().first), nextCnt = s.sGlobal.nextCnt)) + listOf( + XcfaAction( + proc.key, + XcfaEdge( + proc.value.locs.peek(), + proc.value.locs.peek(), + proc.value.paramStmts.peek().first, + ), + nextCnt = s.sGlobal.nextCnt, + ) + ) } else { - proc.value.locs.peek().outgoingEdges.map { edge -> - val newLabel = edge.label.changeVars(proc.value.varLookup.peek()) - val flatLabels = newLabel.getFlatLabels() - if (flatLabels.any { it is InvokeLabel || it is StartLabel }) { - val newNewLabel = SequenceLabel(flatLabels.map { label -> - if (label is InvokeLabel) { - val procedure = s.xcfa?.procedures?.find { proc -> proc.name == label.name } - ?: error("No such method ${label.name}.") - val lookup: MutableMap, VarDecl<*>> = LinkedHashMap() - SequenceLabel(listOf(procedure.params.withIndex() - .filter { it.value.second != ParamDirection.OUT }.map { iVal -> - val originalVar = iVal.value.first - val tempVar = Var("tmp${tempCnt++}_" + originalVar.name, - originalVar.type) - lookup[originalVar] = tempVar + proc.value.locs.peek().outgoingEdges.map { edge -> + val newLabel = edge.label.changeVars(proc.value.varLookup.peek()) + val flatLabels = newLabel.getFlatLabels() + if (flatLabels.any { it is InvokeLabel || it is StartLabel }) { + val newNewLabel = + SequenceLabel( + flatLabels.map { label -> + if (label is InvokeLabel) { + val procedure = + s.xcfa?.procedures?.find { proc -> proc.name == label.name } + ?: error("No such method ${label.name}.") + val lookup: MutableMap, VarDecl<*>> = LinkedHashMap() + SequenceLabel( + listOf( + procedure.params + .withIndex() + .filter { it.value.second != ParamDirection.OUT } + .map { iVal -> + val originalVar = iVal.value.first + val tempVar = + Var("tmp${tempCnt++}_" + originalVar.name, originalVar.type) + lookup[originalVar] = tempVar + StmtLabel( + Stmts.Assign( + TypeUtils.cast(tempVar, tempVar.type), + TypeUtils.cast(label.params[iVal.index], tempVar.type), + ), + metadata = label.metadata, + ) + }, + listOf(label.copy(tempLookup = lookup)), + ) + .flatten() + ) + } else if (label is StartLabel) { + val procedure = + s.xcfa?.procedures?.find { proc -> proc.name == label.name } + ?: error("No such method ${label.name}.") + val lookup: MutableMap, VarDecl<*>> = LinkedHashMap() + SequenceLabel( + listOf( + procedure.params + .withIndex() + .filter { it.value.second != ParamDirection.OUT } + .mapNotNull { iVal -> + val originalVar = iVal.value.first + val tempVar = + Var("tmp${tempCnt++}_" + originalVar.name, originalVar.type) + lookup[originalVar] = tempVar + val trial = + Try.attempt { StmtLabel( - Stmts.Assign( - TypeUtils.cast(tempVar, tempVar.type), - TypeUtils.cast(label.params[iVal.index], tempVar.type)), - metadata = label.metadata) - }, listOf(label.copy(tempLookup = lookup))).flatten()) - } else if (label is StartLabel) { - val procedure = s.xcfa?.procedures?.find { proc -> proc.name == label.name } - ?: error("No such method ${label.name}.") - val lookup: MutableMap, VarDecl<*>> = LinkedHashMap() - SequenceLabel(listOf(procedure.params.withIndex() - .filter { it.value.second != ParamDirection.OUT }.mapNotNull { iVal -> - val originalVar = iVal.value.first - val tempVar = Var("tmp${tempCnt++}_" + originalVar.name, - originalVar.type) - lookup[originalVar] = tempVar - val trial = Try.attempt { - StmtLabel( - Stmts.Assign( - TypeUtils.cast(tempVar, tempVar.type), - TypeUtils.cast(label.params[iVal.index], tempVar.type)), - metadata = label.metadata) - } - if (trial.isSuccess) { - trial.asSuccess().value - } else { - null - } - }, listOf(label.copy(tempLookup = lookup))).flatten()) - } else label - }) - XcfaAction(proc.key, edge.withLabel(newNewLabel), nextCnt = s.sGlobal.nextCnt) - } else - XcfaAction(proc.key, edge.withLabel(newLabel), nextCnt = s.sGlobal.nextCnt) - } + Stmts.Assign( + TypeUtils.cast(tempVar, tempVar.type), + TypeUtils.cast(label.params[iVal.index], tempVar.type), + ), + metadata = label.metadata, + ) + } + if (trial.isSuccess) { + trial.asSuccess().value + } else { + null + } + }, + listOf(label.copy(tempLookup = lookup)), + ) + .flatten() + ) + } else label + } + ) + XcfaAction(proc.key, edge.withLabel(newNewLabel), nextCnt = s.sGlobal.nextCnt) + } else XcfaAction(proc.key, edge.withLabel(newLabel), nextCnt = s.sGlobal.nextCnt) + } } - }.flatten().toSet() -} + } + .flatten() + .toSet() + } fun getXcfaLts(): LTS>, XcfaAction> { - val lts = getCoreXcfaLts() - return LTS>, XcfaAction> { s -> - lts.getEnabledActionsFor(s).filter { !s.apply(it).first.bottom }.toSet() - } + val lts = getCoreXcfaLts() + return LTS>, XcfaAction> { s -> + lts.getEnabledActionsFor(s).filter { !s.apply(it).first.bottom }.toSet() + } } enum class ErrorDetection { - ERROR_LOCATION, - DATA_RACE, - OVERFLOW, - NO_ERROR + ERROR_LOCATION, + DATA_RACE, + OVERFLOW, + NO_ERROR, } fun getXcfaErrorPredicate( - errorDetection: ErrorDetection): Predicate>> = when (errorDetection) { + errorDetection: ErrorDetection +): Predicate>> = + when (errorDetection) { ErrorDetection.ERROR_LOCATION -> - Predicate>> { s -> s.processes.any { it.value.locs.peek().error } } + Predicate>> { s -> + s.processes.any { it.value.locs.peek().error } + } ErrorDetection.DATA_RACE -> { - Predicate>> { s -> - val xcfa = s.xcfa!! - for (process1 in s.processes) - for (process2 in s.processes) - if (process1.key != process2.key) - for (edge1 in process1.value.locs.peek().outgoingEdges) - for (edge2 in process2.value.locs.peek().outgoingEdges) { - val mutexes1 = s.mutexes.filterValues { it == process1.key }.keys - val mutexes2 = s.mutexes.filterValues { it == process2.key }.keys - val globalVars1 = edge1.getGlobalVarsWithNeededMutexes(xcfa, mutexes1) - val globalVars2 = edge2.getGlobalVarsWithNeededMutexes(xcfa, mutexes2) - for (v1 in globalVars1) - for (v2 in globalVars2) - if (v1.varDecl == v2.varDecl) - if (v1.access.isWritten || v2.access.isWritten) - if ((v1.mutexes intersect v2.mutexes).isEmpty()) - return@Predicate true - } - false - } + Predicate>> { s -> + val xcfa = s.xcfa!! + for (process1 in s.processes) for (process2 in s.processes) if ( + process1.key != process2.key + ) + for (edge1 in process1.value.locs.peek().outgoingEdges) for (edge2 in + process2.value.locs.peek().outgoingEdges) { + val mutexes1 = s.mutexes.filterValues { it == process1.key }.keys + val mutexes2 = s.mutexes.filterValues { it == process2.key }.keys + val globalVars1 = edge1.getGlobalVarsWithNeededMutexes(xcfa, mutexes1) + val globalVars2 = edge2.getGlobalVarsWithNeededMutexes(xcfa, mutexes2) + for (v1 in globalVars1) for (v2 in globalVars2) if (v1.varDecl == v2.varDecl) + if (v1.access.isWritten || v2.access.isWritten) + if ((v1.mutexes intersect v2.mutexes).isEmpty()) return@Predicate true + } + false + } } - ErrorDetection.NO_ERROR, ErrorDetection.OVERFLOW -> Predicate>> { false } -} + ErrorDetection.NO_ERROR, + ErrorDetection.OVERFLOW -> Predicate>> { false } + } fun getPartialOrder(partialOrd: PartialOrd>) = - PartialOrd>> { s1, s2 -> - s1.processes == s2.processes && s1.bottom == s2.bottom && s1.mutexes == s2.mutexes && partialOrd.isLeq( - s1.sGlobal, s2.sGlobal) - } + PartialOrd>> { s1, s2 -> + s1.processes == s2.processes && + s1.bottom == s2.bottom && + s1.mutexes == s2.mutexes && + partialOrd.isLeq(s1.sGlobal, s2.sGlobal) + } -private fun stackIsLeq(s1: XcfaState>, - s2: XcfaState>) = s2.processes.keys.all { pid -> +private fun stackIsLeq(s1: XcfaState>, s2: XcfaState>) = + s2.processes.keys.all { pid -> s1.processes[pid]?.let { ps1 -> - val ps2 = s2.processes.getValue(pid) - ps1.locs.peek() == ps2.locs.peek() && ps1.paramsInitialized && ps2.paramsInitialized + val ps2 = s2.processes.getValue(pid) + ps1.locs.peek() == ps2.locs.peek() && ps1.paramsInitialized && ps2.paramsInitialized } ?: false -} + } fun getStackPartialOrder(partialOrd: PartialOrd>) = - PartialOrd>> { s1, s2 -> - s1.processes.size == s2.processes.size && stackIsLeq(s1, - s2) && s1.bottom == s2.bottom && s1.mutexes == s2.mutexes - && partialOrd.isLeq(s1.withGeneralizedVars(), s2.withGeneralizedVars()) - } + PartialOrd>> { s1, s2 -> + s1.processes.size == s2.processes.size && + stackIsLeq(s1, s2) && + s1.bottom == s2.bottom && + s1.mutexes == s2.mutexes && + partialOrd.isLeq(s1.withGeneralizedVars(), s2.withGeneralizedVars()) + } private fun >, P : XcfaPrec> getXcfaArgBuilder( - analysis: Analysis, - lts: LTS>, XcfaAction>, - errorDetection: ErrorDetection) - : ArgBuilder = - ArgBuilder.create( - lts, - analysis, - getXcfaErrorPredicate(errorDetection) - ) + analysis: Analysis, + lts: LTS>, XcfaAction>, + errorDetection: ErrorDetection, +): ArgBuilder = + ArgBuilder.create(lts, analysis, getXcfaErrorPredicate(errorDetection)) fun >, P : XcfaPrec> getXcfaAbstractor( - analysis: Analysis, - waitlist: Waitlist<*>, - stopCriterion: StopCriterion<*, *>, - logger: Logger, - lts: LTS>, XcfaAction>, - errorDetection: ErrorDetection -): Abstractor>, XcfaAction, out XcfaPrec> = - XcfaAbstractor.builder(getXcfaArgBuilder(analysis, lts, errorDetection)) - .waitlist(waitlist as Waitlist>) // TODO: can we do this nicely? - .stopCriterion(stopCriterion as StopCriterion).logger(logger) - .projection { - if (it.xcfa!!.isInlined) it.processes - else it.processes.map { (_, p) -> p.locs.peek() } - } - .build() // TODO: can we do this nicely? + analysis: Analysis, + waitlist: Waitlist<*>, + stopCriterion: StopCriterion<*, *>, + logger: Logger, + lts: LTS>, XcfaAction>, + errorDetection: ErrorDetection, +): ArgAbstractor>, XcfaAction, out XcfaPrec> = + XcfaArgAbstractor.builder(getXcfaArgBuilder(analysis, lts, errorDetection)) + .waitlist(waitlist as Waitlist>) // TODO: can we do this nicely? + .stopCriterion(stopCriterion as StopCriterion) + .logger(logger) + .projection { + if (it.xcfa!!.isInlined) it.processes else it.processes.map { (_, p) -> p.locs.peek() } + } + .build() // TODO: can we do this nicely? /// EXPL -private fun getExplXcfaInitFunc(xcfa: XCFA, - solver: Solver): (XcfaPrec>) -> List>> { - val processInitState = xcfa.initProcedures.mapIndexed { i, it -> +private fun getExplXcfaInitFunc( + xcfa: XCFA, + solver: Solver, +): (XcfaPrec>) -> List>> { + val processInitState = + xcfa.initProcedures + .mapIndexed { i, it -> val initLocStack: LinkedList = LinkedList() initLocStack.add(it.first.initLoc) - Pair(i, XcfaProcessState(initLocStack, prefix = "T$i", - varLookup = LinkedList(listOf(createLookup(it.first, "T$i", ""))))) - }.toMap() - return { p -> - ExplInitFunc.create(solver, True()).getPtrInitFunc().getInitStates(p.p) - .map { XcfaState(xcfa, processInitState, it) } + Pair( + i, + XcfaProcessState( + initLocStack, + prefix = "T$i", + varLookup = LinkedList(listOf(createLookup(it.first, "T$i", ""))), + ), + ) + } + .toMap() + return { p -> + ExplInitFunc.create(solver, True()).getPtrInitFunc().getInitStates(p.p).map { + XcfaState(xcfa, processInitState, it) } + } } -private fun getExplXcfaTransFunc(solver: Solver, maxEnum: Int, isHavoc: Boolean): - (XcfaState>, XcfaAction, XcfaPrec>) -> List>> { - val explTransFunc = (ExplStmtTransFunc.create(solver, - maxEnum) as TransFunc).getPtrTransFunc(isHavoc) - return { s, a, p -> - val (newSt, newAct) = s.apply(a) - explTransFunc.getSuccStates(newSt.sGlobal, newAct, p.p.addVars( - listOf(s.processes.map { it.value.varLookup }.flatten(), - listOf(getTempLookup(a.label))).flatten())).map { newSt.withState(it) } - } +private fun getExplXcfaTransFunc( + solver: Solver, + maxEnum: Int, + isHavoc: Boolean, +): (XcfaState>, XcfaAction, XcfaPrec>) -> List< + XcfaState> + > { + val explTransFunc = + (ExplStmtTransFunc.create(solver, maxEnum) as TransFunc) + .getPtrTransFunc(isHavoc) + return { s, a, p -> + val (newSt, newAct) = s.apply(a) + explTransFunc + .getSuccStates( + newSt.sGlobal, + newAct, + p.p.addVars( + listOf(s.processes.map { it.value.varLookup }.flatten(), listOf(getTempLookup(a.label))) + .flatten() + ), + ) + .map { newSt.withState(it) } + } } -class ExplXcfaAnalysis(xcfa: XCFA, solver: Solver, maxEnum: Int, - partialOrd: PartialOrd>>, isHavoc: Boolean) : - XcfaAnalysis>( - corePartialOrd = partialOrd, - coreInitFunc = getExplXcfaInitFunc(xcfa, solver), - coreTransFunc = getExplXcfaTransFunc(solver, maxEnum, isHavoc) - ) +class ExplXcfaAnalysis( + xcfa: XCFA, + solver: Solver, + maxEnum: Int, + partialOrd: PartialOrd>>, + isHavoc: Boolean, +) : + XcfaAnalysis>( + corePartialOrd = partialOrd, + coreInitFunc = getExplXcfaInitFunc(xcfa, solver), + coreTransFunc = getExplXcfaTransFunc(solver, maxEnum, isHavoc), + ) /// PRED -private fun getPredXcfaInitFunc(xcfa: XCFA, - predAbstractor: PredAbstractor): (XcfaPrec>) -> List>> { - val processInitState = xcfa.initProcedures.mapIndexed { i, it -> +private fun getPredXcfaInitFunc( + xcfa: XCFA, + predAbstractor: PredAbstractor, +): (XcfaPrec>) -> List>> { + val processInitState = + xcfa.initProcedures + .mapIndexed { i, it -> val initLocStack: LinkedList = LinkedList() initLocStack.add(it.first.initLoc) - Pair(i, XcfaProcessState(initLocStack, prefix = "T$i", - varLookup = LinkedList(listOf(createLookup(it.first, "T$i", ""))))) - }.toMap() - return { p -> - PredInitFunc.create(predAbstractor, True()).getPtrInitFunc().getInitStates(p.p) - .map { XcfaState(xcfa, processInitState, it) } + Pair( + i, + XcfaProcessState( + initLocStack, + prefix = "T$i", + varLookup = LinkedList(listOf(createLookup(it.first, "T$i", ""))), + ), + ) + } + .toMap() + return { p -> + PredInitFunc.create(predAbstractor, True()).getPtrInitFunc().getInitStates(p.p).map { + XcfaState(xcfa, processInitState, it) } + } } -private fun getPredXcfaTransFunc(predAbstractor: PredAbstractors.PredAbstractor, isHavoc: Boolean): - (XcfaState>, XcfaAction, XcfaPrec>) -> List>> { - val predTransFunc = (PredTransFunc.create( - predAbstractor) as TransFunc).getPtrTransFunc(isHavoc) - return { s, a, p -> - val (newSt, newAct) = s.apply(a) - predTransFunc.getSuccStates(newSt.sGlobal, newAct, p.p.addVars( - s.processes.map { it.value.foldVarLookup() + getTempLookup(a.label) } - )).map { newSt.withState(it) } - } +private fun getPredXcfaTransFunc( + predAbstractor: PredAbstractors.PredAbstractor, + isHavoc: Boolean, +): (XcfaState>, XcfaAction, XcfaPrec>) -> List< + XcfaState> + > { + val predTransFunc = + (PredTransFunc.create(predAbstractor) as TransFunc) + .getPtrTransFunc(isHavoc) + return { s, a, p -> + val (newSt, newAct) = s.apply(a) + predTransFunc + .getSuccStates( + newSt.sGlobal, + newAct, + p.p.addVars(s.processes.map { it.value.foldVarLookup() + getTempLookup(a.label) }), + ) + .map { newSt.withState(it) } + } } -class PredXcfaAnalysis(xcfa: XCFA, solver: Solver, predAbstractor: PredAbstractor, - partialOrd: PartialOrd>>, isHavoc: Boolean) : - XcfaAnalysis>( - corePartialOrd = partialOrd, - coreInitFunc = getPredXcfaInitFunc(xcfa, predAbstractor), - coreTransFunc = getPredXcfaTransFunc(predAbstractor, isHavoc) - ) +class PredXcfaAnalysis( + xcfa: XCFA, + solver: Solver, + predAbstractor: PredAbstractor, + partialOrd: PartialOrd>>, + isHavoc: Boolean, +) : + XcfaAnalysis>( + corePartialOrd = partialOrd, + coreInitFunc = getPredXcfaInitFunc(xcfa, predAbstractor), + coreTransFunc = getPredXcfaTransFunc(predAbstractor, isHavoc), + ) diff --git a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaArgAbstractor.kt b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaArgAbstractor.kt new file mode 100644 index 0000000000..bc2d2b816c --- /dev/null +++ b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaArgAbstractor.kt @@ -0,0 +1,143 @@ +/* + * 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.analysis + +import com.google.common.base.Preconditions +import hu.bme.mit.theta.analysis.Action +import hu.bme.mit.theta.analysis.Prec +import hu.bme.mit.theta.analysis.State +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.ArgNode +import hu.bme.mit.theta.analysis.algorithm.cegar.AbstractorResult +import hu.bme.mit.theta.analysis.algorithm.cegar.BasicArgAbstractor +import hu.bme.mit.theta.analysis.algorithm.cegar.abstractor.StopCriterion +import hu.bme.mit.theta.analysis.reachedset.Partition +import hu.bme.mit.theta.analysis.waitlist.Waitlist +import hu.bme.mit.theta.common.logging.Logger +import java.util.function.Function + +class XcfaArgAbstractor( + argBuilder: ArgBuilder, + projection: Function?, + waitlist: Waitlist>, + stopCriterion: StopCriterion, + logger: Logger, +) : BasicArgAbstractor(argBuilder, projection, waitlist, stopCriterion, logger) { + + override fun check(arg: ARG, prec: P): AbstractorResult { + logger.write(Logger.Level.DETAIL, "| | Precision: %s%n", prec) + + if (!arg.isInitialized) { + logger.write(Logger.Level.SUBSTEP, "| | (Re)initializing ARG...") + argBuilder.init(arg, prec) + logger.write(Logger.Level.SUBSTEP, "done%n") + } + + assert(arg.isInitialized) + + logger.write( + Logger.Level.INFO, + "| | Starting ARG: %d nodes, %d incomplete, %d unsafe%n", + arg.nodes.count(), + arg.incompleteNodes.count(), + arg.unsafeNodes.count(), + ) + logger.write(Logger.Level.SUBSTEP, "| | Building ARG...") + + val reachedSet: Partition, *> = + Partition.of { n: ArgNode -> projection.apply(n.state) } + waitlist.clear() + + reachedSet.addAll(arg.nodes) + waitlist.addAll(arg.incompleteNodes) + + if (!stopCriterion.canStop(arg)) { + while (!waitlist.isEmpty) { + val node = waitlist.remove() + var newNodes: Collection>? = emptyList() + if ((node.state as XcfaState<*>).xcfa!!.isInlined) { + close(node, reachedSet[node]) + } else { + val expandProcedureCall = (node.state as XcfaState<*>) in (prec as XcfaPrec

).noPop + closePop(node, reachedSet[node], !expandProcedureCall) + } + if (!node.isSubsumed && !node.isTarget) { + newNodes = argBuilder.expand(node, prec) + reachedSet.addAll(newNodes) + waitlist.addAll(newNodes) + } + if (stopCriterion.canStop(arg, newNodes)) break + } + } + + logger.write(Logger.Level.SUBSTEP, "done%n") + logger.write( + Logger.Level.INFO, + "| | Finished ARG: %d nodes, %d incomplete, %d unsafe%n", + arg.nodes.count(), + arg.incompleteNodes.count(), + arg.unsafeNodes.count(), + ) + + waitlist.clear() // Optimization + + return if (arg.isSafe) { + Preconditions.checkState(arg.isComplete, "Returning incomplete ARG as safe") + AbstractorResult.safe() + } else { + AbstractorResult.unsafe() + } + } + + fun closePop(node: ArgNode, candidates: Collection>, popCovered: Boolean) { + if (!node.isLeaf) { + return + } + for (candidate in candidates) { + if (candidate.mayCover(node)) { + var onlyStackCovers = false + (node.state as XcfaState<*>).processes.forEach { (pid: Int, proc: XcfaProcessState) -> + if (proc != (candidate.state as XcfaState<*>).processes[pid]) { + if (popCovered) proc.popped = proc.locs.pop() + onlyStackCovers = true + } + } + if (!onlyStackCovers) { + node.cover(candidate) + } + return + } + } + } + + companion object { + + fun builder( + argBuilder: ArgBuilder + ): BasicArgAbstractor.Builder { + return Builder(argBuilder) + } + } + + class Builder(argBuilder: ArgBuilder) : + BasicArgAbstractor.Builder(argBuilder) { + + override fun build(): BasicArgAbstractor { + return XcfaArgAbstractor(argBuilder, projection, waitlist, stopCriterion, logger) + } + } +} diff --git a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaSingeExprTraceRefiner.kt b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaSingeExprTraceRefiner.kt index ad0a385e5d..93410e0641 100644 --- a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaSingeExprTraceRefiner.kt +++ b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaSingeExprTraceRefiner.kt @@ -64,7 +64,7 @@ class XcfaSingleExprTraceRefiner, prec: P?): RefinerResult { + fun refineTemp(arg: ARG, prec: P?): RefinerResult> { Preconditions.checkNotNull(arg) Preconditions.checkNotNull(prec) assert(!arg.isSafe) { "ARG must be unsafe" } @@ -118,7 +118,7 @@ class XcfaSingleExprTraceRefiner, prec: P?): RefinerResult { + override fun refine(arg: ARG, prec: P?): RefinerResult> { Preconditions.checkNotNull(arg) Preconditions.checkNotNull

(prec) assert(!arg.isSafe) { "ARG must be unsafe" } diff --git a/subprojects/xcfa/xcfa-analysis/src/test/java/hu/bme/mit/theta/xcfa/analysis/XcfaExplAnalysisTest.kt b/subprojects/xcfa/xcfa-analysis/src/test/java/hu/bme/mit/theta/xcfa/analysis/XcfaExplAnalysisTest.kt index b4aa758303..a04508f9cf 100644 --- a/subprojects/xcfa/xcfa-analysis/src/test/java/hu/bme/mit/theta/xcfa/analysis/XcfaExplAnalysisTest.kt +++ b/subprojects/xcfa/xcfa-analysis/src/test/java/hu/bme/mit/theta/xcfa/analysis/XcfaExplAnalysisTest.kt @@ -13,14 +13,13 @@ * See the License for the specific language governing permissions and * limitations under the License. */ - package hu.bme.mit.theta.xcfa.analysis -import hu.bme.mit.theta.analysis.algorithm.arg.ArgNodeComparators import hu.bme.mit.theta.analysis.algorithm.SafetyResult -import hu.bme.mit.theta.analysis.algorithm.cegar.Abstractor -import hu.bme.mit.theta.analysis.algorithm.cegar.CegarChecker -import hu.bme.mit.theta.analysis.algorithm.cegar.Refiner +import hu.bme.mit.theta.analysis.algorithm.arg.ArgNodeComparators +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 import hu.bme.mit.theta.analysis.algorithm.cegar.abstractor.StopCriterions import hu.bme.mit.theta.analysis.expl.* import hu.bme.mit.theta.analysis.expr.refinement.* @@ -39,255 +38,309 @@ import hu.bme.mit.theta.solver.z3legacy.Z3LegacySolverFactory import hu.bme.mit.theta.xcfa.analysis.coi.ConeOfInfluence import hu.bme.mit.theta.xcfa.analysis.coi.XcfaCoiMultiThread import hu.bme.mit.theta.xcfa.analysis.por.* +import java.util.* +import kotlin.random.Random import org.junit.jupiter.api.Assertions import org.junit.jupiter.params.ParameterizedTest import org.junit.jupiter.params.provider.MethodSource -import java.util.* -import kotlin.random.Random - class XcfaExplAnalysisTest { + companion object { - companion object { - - private val seed = 1001 - - @JvmStatic - fun data(): Collection> { - return listOf( - arrayOf("/00assignment.c", SafetyResult<*, *>::isUnsafe), - arrayOf("/01function.c", SafetyResult<*, *>::isUnsafe), - arrayOf("/02functionparam.c", SafetyResult<*, *>::isSafe), - arrayOf("/03nondetfunction.c", SafetyResult<*, *>::isUnsafe), - arrayOf("/04multithread.c", SafetyResult<*, *>::isUnsafe), - ) - } - } - - @ParameterizedTest - @MethodSource("data") - fun testNoporExpl(filepath: String, verdict: (SafetyResult<*, *>) -> Boolean) { - println("Testing NOPOR on $filepath...") - val stream = javaClass.getResourceAsStream(filepath) - val xcfa = getXcfaFromC(stream!!, ParseContext(), false, false, NullLogger.getInstance()).first - ConeOfInfluence = XcfaCoiMultiThread(xcfa) - - val analysis = ExplXcfaAnalysis( - xcfa, - Z3LegacySolverFactory.getInstance().createSolver(), - 1, - getPartialOrder(ExplOrd.getInstance().getPtrPartialOrd()), false - ) - - val lts = getXcfaLts() - - val abstractor = getXcfaAbstractor(analysis, - PriorityWaitlist.create( - ArgNodeComparators.combine(ArgNodeComparators.targetFirst(), ArgNodeComparators.bfs())), - StopCriterions.firstCex>, XcfaAction>(), - ConsoleLogger(Logger.Level.DETAIL), - lts, - ErrorDetection.ERROR_LOCATION) as Abstractor>, XcfaAction, XcfaPrec>> - - val precRefiner = XcfaPrecRefiner>, ExplPrec, ItpRefutation>( - ItpRefToPtrPrec(ItpRefToExplPrec())) - - val refiner = - XcfaSingleExprTraceRefiner.create( - ExprTraceBwBinItpChecker.create(BoolExprs.True(), BoolExprs.True(), - Z3LegacySolverFactory.getInstance().createItpSolver()), - precRefiner, PruneStrategy.FULL, - NullLogger.getInstance()) as Refiner>, XcfaAction, XcfaPrec>> - - val cegarChecker = - CegarChecker.create(abstractor, refiner) - - val safetyResult = cegarChecker.check(XcfaPrec(PtrPrec(ExplPrec.empty(), emptySet()))) - - - - Assertions.assertTrue(verdict(safetyResult)) - } - - @ParameterizedTest - @MethodSource("data") - fun testSporExpl(filepath: String, verdict: (SafetyResult<*, *>) -> Boolean) { - println("Testing SPOR on $filepath...") - val stream = javaClass.getResourceAsStream(filepath) - val xcfa = getXcfaFromC(stream!!, ParseContext(), false, false, NullLogger.getInstance()).first - ConeOfInfluence = XcfaCoiMultiThread(xcfa) - - val analysis = ExplXcfaAnalysis( - xcfa, - Z3LegacySolverFactory.getInstance().createSolver(), - 1, - getPartialOrder(ExplOrd.getInstance().getPtrPartialOrd()), false - ) - - val lts = XcfaSporLts(xcfa) - - val abstractor = getXcfaAbstractor(analysis, - PriorityWaitlist.create( - ArgNodeComparators.combine(ArgNodeComparators.targetFirst(), ArgNodeComparators.bfs())), - StopCriterions.firstCex>, XcfaAction>(), - ConsoleLogger(Logger.Level.DETAIL), - lts, - ErrorDetection.ERROR_LOCATION) as Abstractor>, XcfaAction, XcfaPrec>> - - val precRefiner = XcfaPrecRefiner>, ExplPrec, ItpRefutation>( - ItpRefToPtrPrec(ItpRefToExplPrec())) - - val refiner = - XcfaSingleExprTraceRefiner.create( - ExprTraceBwBinItpChecker.create(BoolExprs.True(), BoolExprs.True(), - Z3LegacySolverFactory.getInstance().createItpSolver()), - precRefiner, PruneStrategy.FULL, - NullLogger.getInstance()) as Refiner>, XcfaAction, XcfaPrec>> - - val cegarChecker = - CegarChecker.create(abstractor, refiner) - - val safetyResult = cegarChecker.check(XcfaPrec(PtrPrec(ExplPrec.empty(), emptySet()))) - - - - Assertions.assertTrue(verdict(safetyResult)) - } - - @ParameterizedTest - @MethodSource("data") - fun testDporExpl(filepath: String, verdict: (SafetyResult<*, *>) -> Boolean) { - XcfaDporLts.random = Random(seed) - println("Testing DPOR on $filepath...") - val stream = javaClass.getResourceAsStream(filepath) - val xcfa = getXcfaFromC(stream!!, ParseContext(), false, false, NullLogger.getInstance()).first - ConeOfInfluence = XcfaCoiMultiThread(xcfa) - - val analysis = ExplXcfaAnalysis( - xcfa, - Z3LegacySolverFactory.getInstance().createSolver(), - 1, - XcfaDporLts.getPartialOrder(getPartialOrder(ExplOrd.getInstance().getPtrPartialOrd())), false - ) - - val lts = XcfaDporLts(xcfa) - - val abstractor = getXcfaAbstractor(analysis, - lts.waitlist, - StopCriterions.firstCex>, XcfaAction>(), - ConsoleLogger(Logger.Level.DETAIL), - lts, - ErrorDetection.ERROR_LOCATION) as Abstractor>, XcfaAction, XcfaPrec>> - - val precRefiner = XcfaPrecRefiner>, ExplPrec, ItpRefutation>( - ItpRefToPtrPrec(ItpRefToExplPrec())) - - val refiner = - XcfaSingleExprTraceRefiner.create( - ExprTraceBwBinItpChecker.create(BoolExprs.True(), BoolExprs.True(), - Z3LegacySolverFactory.getInstance().createItpSolver()), - precRefiner, PruneStrategy.FULL, - ConsoleLogger( - Logger.Level.DETAIL)) as Refiner>, XcfaAction, XcfaPrec>> - - val cegarChecker = - CegarChecker.create(abstractor, refiner) - - val safetyResult = cegarChecker.check(XcfaPrec(PtrPrec(ExplPrec.empty(), emptySet()))) - - - - Assertions.assertTrue(verdict(safetyResult)) - } - - @ParameterizedTest - @MethodSource("data") - fun testAasporExpl(filepath: String, verdict: (SafetyResult<*, *>) -> Boolean) { - println("Testing AASPOR on $filepath...") - val stream = javaClass.getResourceAsStream(filepath) - val xcfa = getXcfaFromC(stream!!, ParseContext(), false, false, NullLogger.getInstance()).first - ConeOfInfluence = XcfaCoiMultiThread(xcfa) - - val analysis = ExplXcfaAnalysis( - xcfa, - Z3LegacySolverFactory.getInstance().createSolver(), - 1, - getPartialOrder(ExplOrd.getInstance().getPtrPartialOrd()), false - ) - - val lts = XcfaAasporLts(xcfa, mutableMapOf()) - - val abstractor = getXcfaAbstractor(analysis, - PriorityWaitlist.create( - ArgNodeComparators.combine(ArgNodeComparators.targetFirst(), ArgNodeComparators.bfs())), - StopCriterions.firstCex>, XcfaAction>(), - ConsoleLogger(Logger.Level.DETAIL), - lts, - ErrorDetection.ERROR_LOCATION) as Abstractor>, XcfaAction, XcfaPrec>> - - val precRefiner = XcfaPrecRefiner, ExplPrec, ItpRefutation>( - ItpRefToPtrPrec(ItpRefToExplPrec())) - val atomicNodePruner = AtomicNodePruner>, XcfaAction>() - - val refiner = - XcfaSingleExprTraceRefiner.create( - ExprTraceBwBinItpChecker.create(BoolExprs.True(), BoolExprs.True(), - Z3LegacySolverFactory.getInstance().createItpSolver()), - precRefiner, PruneStrategy.FULL, NullLogger.getInstance(), - atomicNodePruner) as Refiner>, XcfaAction, XcfaPrec>> - - val cegarChecker = - CegarChecker.create(abstractor, AasporRefiner.create(refiner, PruneStrategy.FULL, mutableMapOf())) - - val safetyResult = cegarChecker.check(XcfaPrec(PtrPrec(ExplPrec.empty(), emptySet()))) - - - - Assertions.assertTrue(verdict(safetyResult)) - } - - @ParameterizedTest - @MethodSource("data") - fun testAadporExpl(filepath: String, verdict: (SafetyResult<*, *>) -> Boolean) { - XcfaDporLts.random = Random(seed) - println("Testing AADPOR on $filepath...") - val stream = javaClass.getResourceAsStream(filepath) - val xcfa = getXcfaFromC(stream!!, ParseContext(), false, false, NullLogger.getInstance()).first - ConeOfInfluence = XcfaCoiMultiThread(xcfa) - - val analysis = ExplXcfaAnalysis( - xcfa, - Z3LegacySolverFactory.getInstance().createSolver(), - 1, - XcfaDporLts.getPartialOrder(getPartialOrder(ExplOrd.getInstance().getPtrPartialOrd())), false - ) - - val lts = XcfaAadporLts(xcfa) - - val abstractor = getXcfaAbstractor(analysis, - lts.waitlist, - StopCriterions.firstCex>, XcfaAction>(), - ConsoleLogger(Logger.Level.DETAIL), - lts, - ErrorDetection.ERROR_LOCATION) as Abstractor>, XcfaAction, XcfaPrec>> - - val precRefiner = XcfaPrecRefiner(ItpRefToPtrPrec(ItpRefToExplPrec())) - - val refiner = - XcfaSingleExprTraceRefiner.create( - ExprTraceBwBinItpChecker.create(BoolExprs.True(), BoolExprs.True(), - Z3LegacySolverFactory.getInstance().createItpSolver()), - precRefiner, PruneStrategy.FULL, - NullLogger.getInstance()) as Refiner>, XcfaAction, XcfaPrec>> - - val cegarChecker = - CegarChecker.create(abstractor, refiner) - - val safetyResult = cegarChecker.check(XcfaPrec(PtrPrec(ExplPrec.empty(), emptySet()))) - - + private val seed = 1001 - Assertions.assertTrue(verdict(safetyResult)) + @JvmStatic + fun data(): Collection> { + return listOf( + arrayOf("/00assignment.c", SafetyResult<*, *>::isUnsafe), + arrayOf("/01function.c", SafetyResult<*, *>::isUnsafe), + arrayOf("/02functionparam.c", SafetyResult<*, *>::isSafe), + arrayOf("/03nondetfunction.c", SafetyResult<*, *>::isUnsafe), + arrayOf("/04multithread.c", SafetyResult<*, *>::isUnsafe), + ) } -} \ No newline at end of file + } + + @ParameterizedTest + @MethodSource("data") + fun testNoporExpl(filepath: String, verdict: (SafetyResult<*, *>) -> Boolean) { + println("Testing NOPOR on $filepath...") + val stream = javaClass.getResourceAsStream(filepath) + val xcfa = getXcfaFromC(stream!!, ParseContext(), false, false, NullLogger.getInstance()).first + ConeOfInfluence = XcfaCoiMultiThread(xcfa) + + val analysis = + ExplXcfaAnalysis( + xcfa, + Z3LegacySolverFactory.getInstance().createSolver(), + 1, + getPartialOrder(ExplOrd.getInstance().getPtrPartialOrd()), + false, + ) + + val lts = getXcfaLts() + + val abstractor = + getXcfaAbstractor( + analysis, + PriorityWaitlist.create( + ArgNodeComparators.combine(ArgNodeComparators.targetFirst(), ArgNodeComparators.bfs()) + ), + StopCriterions.firstCex>, XcfaAction>(), + ConsoleLogger(Logger.Level.DETAIL), + lts, + ErrorDetection.ERROR_LOCATION, + ) + as ArgAbstractor>, XcfaAction, XcfaPrec>> + + val precRefiner = + XcfaPrecRefiner>, ExplPrec, ItpRefutation>( + ItpRefToPtrPrec(ItpRefToExplPrec()) + ) + + val refiner = + XcfaSingleExprTraceRefiner.create( + ExprTraceBwBinItpChecker.create( + BoolExprs.True(), + BoolExprs.True(), + Z3LegacySolverFactory.getInstance().createItpSolver(), + ), + precRefiner, + PruneStrategy.FULL, + NullLogger.getInstance(), + ) as ArgRefiner>, XcfaAction, XcfaPrec>> + + val cegarChecker = ArgCegarChecker.create(abstractor, refiner) + + val safetyResult = cegarChecker.check(XcfaPrec(PtrPrec(ExplPrec.empty(), emptySet()))) + + Assertions.assertTrue(verdict(safetyResult)) + } + + @ParameterizedTest + @MethodSource("data") + fun testSporExpl(filepath: String, verdict: (SafetyResult<*, *>) -> Boolean) { + println("Testing SPOR on $filepath...") + val stream = javaClass.getResourceAsStream(filepath) + val xcfa = getXcfaFromC(stream!!, ParseContext(), false, false, NullLogger.getInstance()).first + ConeOfInfluence = XcfaCoiMultiThread(xcfa) + + val analysis = + ExplXcfaAnalysis( + xcfa, + Z3LegacySolverFactory.getInstance().createSolver(), + 1, + getPartialOrder(ExplOrd.getInstance().getPtrPartialOrd()), + false, + ) + + val lts = XcfaSporLts(xcfa) + + val abstractor = + getXcfaAbstractor( + analysis, + PriorityWaitlist.create( + ArgNodeComparators.combine(ArgNodeComparators.targetFirst(), ArgNodeComparators.bfs()) + ), + StopCriterions.firstCex>, XcfaAction>(), + ConsoleLogger(Logger.Level.DETAIL), + lts, + ErrorDetection.ERROR_LOCATION, + ) + as ArgAbstractor>, XcfaAction, XcfaPrec>> + + val precRefiner = + XcfaPrecRefiner>, ExplPrec, ItpRefutation>( + ItpRefToPtrPrec(ItpRefToExplPrec()) + ) + + val refiner = + XcfaSingleExprTraceRefiner.create( + ExprTraceBwBinItpChecker.create( + BoolExprs.True(), + BoolExprs.True(), + Z3LegacySolverFactory.getInstance().createItpSolver(), + ), + precRefiner, + PruneStrategy.FULL, + NullLogger.getInstance(), + ) as ArgRefiner>, XcfaAction, XcfaPrec>> + + val cegarChecker = ArgCegarChecker.create(abstractor, refiner) + + val safetyResult = cegarChecker.check(XcfaPrec(PtrPrec(ExplPrec.empty(), emptySet()))) + + Assertions.assertTrue(verdict(safetyResult)) + } + + @ParameterizedTest + @MethodSource("data") + fun testDporExpl(filepath: String, verdict: (SafetyResult<*, *>) -> Boolean) { + XcfaDporLts.random = Random(seed) + println("Testing DPOR on $filepath...") + val stream = javaClass.getResourceAsStream(filepath) + val xcfa = getXcfaFromC(stream!!, ParseContext(), false, false, NullLogger.getInstance()).first + ConeOfInfluence = XcfaCoiMultiThread(xcfa) + + val analysis = + ExplXcfaAnalysis( + xcfa, + Z3LegacySolverFactory.getInstance().createSolver(), + 1, + XcfaDporLts.getPartialOrder(getPartialOrder(ExplOrd.getInstance().getPtrPartialOrd())), + false, + ) + + val lts = XcfaDporLts(xcfa) + + val abstractor = + getXcfaAbstractor( + analysis, + lts.waitlist, + StopCriterions.firstCex>, XcfaAction>(), + ConsoleLogger(Logger.Level.DETAIL), + lts, + ErrorDetection.ERROR_LOCATION, + ) + as ArgAbstractor>, XcfaAction, XcfaPrec>> + + val precRefiner = + XcfaPrecRefiner>, ExplPrec, ItpRefutation>( + ItpRefToPtrPrec(ItpRefToExplPrec()) + ) + + val refiner = + XcfaSingleExprTraceRefiner.create( + ExprTraceBwBinItpChecker.create( + BoolExprs.True(), + BoolExprs.True(), + Z3LegacySolverFactory.getInstance().createItpSolver(), + ), + precRefiner, + PruneStrategy.FULL, + ConsoleLogger(Logger.Level.DETAIL), + ) as ArgRefiner>, XcfaAction, XcfaPrec>> + + val cegarChecker = ArgCegarChecker.create(abstractor, refiner) + + val safetyResult = cegarChecker.check(XcfaPrec(PtrPrec(ExplPrec.empty(), emptySet()))) + + Assertions.assertTrue(verdict(safetyResult)) + } + + @ParameterizedTest + @MethodSource("data") + fun testAasporExpl(filepath: String, verdict: (SafetyResult<*, *>) -> Boolean) { + println("Testing AASPOR on $filepath...") + val stream = javaClass.getResourceAsStream(filepath) + val xcfa = getXcfaFromC(stream!!, ParseContext(), false, false, NullLogger.getInstance()).first + ConeOfInfluence = XcfaCoiMultiThread(xcfa) + + val analysis = + ExplXcfaAnalysis( + xcfa, + Z3LegacySolverFactory.getInstance().createSolver(), + 1, + getPartialOrder(ExplOrd.getInstance().getPtrPartialOrd()), + false, + ) + + val lts = XcfaAasporLts(xcfa, mutableMapOf()) + + val abstractor = + getXcfaAbstractor( + analysis, + PriorityWaitlist.create( + ArgNodeComparators.combine(ArgNodeComparators.targetFirst(), ArgNodeComparators.bfs()) + ), + StopCriterions.firstCex>, XcfaAction>(), + ConsoleLogger(Logger.Level.DETAIL), + lts, + ErrorDetection.ERROR_LOCATION, + ) + as ArgAbstractor>, XcfaAction, XcfaPrec>> + + val precRefiner = + XcfaPrecRefiner, ExplPrec, ItpRefutation>( + ItpRefToPtrPrec(ItpRefToExplPrec()) + ) + val atomicNodePruner = AtomicNodePruner>, XcfaAction>() + + val refiner = + XcfaSingleExprTraceRefiner.create( + ExprTraceBwBinItpChecker.create( + BoolExprs.True(), + BoolExprs.True(), + Z3LegacySolverFactory.getInstance().createItpSolver(), + ), + precRefiner, + PruneStrategy.FULL, + NullLogger.getInstance(), + atomicNodePruner, + ) as ArgRefiner>, XcfaAction, XcfaPrec>> + + val cegarChecker = + ArgCegarChecker.create( + abstractor, + AasporRefiner.create(refiner, PruneStrategy.FULL, mutableMapOf()), + ) + + val safetyResult = cegarChecker.check(XcfaPrec(PtrPrec(ExplPrec.empty(), emptySet()))) + + Assertions.assertTrue(verdict(safetyResult)) + } + + @ParameterizedTest + @MethodSource("data") + fun testAadporExpl(filepath: String, verdict: (SafetyResult<*, *>) -> Boolean) { + XcfaDporLts.random = Random(seed) + println("Testing AADPOR on $filepath...") + val stream = javaClass.getResourceAsStream(filepath) + val xcfa = getXcfaFromC(stream!!, ParseContext(), false, false, NullLogger.getInstance()).first + ConeOfInfluence = XcfaCoiMultiThread(xcfa) + + val analysis = + ExplXcfaAnalysis( + xcfa, + Z3LegacySolverFactory.getInstance().createSolver(), + 1, + XcfaDporLts.getPartialOrder(getPartialOrder(ExplOrd.getInstance().getPtrPartialOrd())), + false, + ) + + val lts = XcfaAadporLts(xcfa) + + val abstractor = + getXcfaAbstractor( + analysis, + lts.waitlist, + StopCriterions.firstCex>, XcfaAction>(), + ConsoleLogger(Logger.Level.DETAIL), + lts, + ErrorDetection.ERROR_LOCATION, + ) + as ArgAbstractor>, XcfaAction, XcfaPrec>> + + val precRefiner = + XcfaPrecRefiner(ItpRefToPtrPrec(ItpRefToExplPrec())) + + val refiner = + XcfaSingleExprTraceRefiner.create( + ExprTraceBwBinItpChecker.create( + BoolExprs.True(), + BoolExprs.True(), + Z3LegacySolverFactory.getInstance().createItpSolver(), + ), + precRefiner, + PruneStrategy.FULL, + NullLogger.getInstance(), + ) as ArgRefiner>, XcfaAction, XcfaPrec>> + + val cegarChecker = ArgCegarChecker.create(abstractor, refiner) + + val safetyResult = cegarChecker.check(XcfaPrec(PtrPrec(ExplPrec.empty(), emptySet()))) + + Assertions.assertTrue(verdict(safetyResult)) + } +} diff --git a/subprojects/xcfa/xcfa-analysis/src/test/java/hu/bme/mit/theta/xcfa/analysis/XcfaPredAnalysisTest.kt b/subprojects/xcfa/xcfa-analysis/src/test/java/hu/bme/mit/theta/xcfa/analysis/XcfaPredAnalysisTest.kt index e398b5ed07..a10e82f096 100644 --- a/subprojects/xcfa/xcfa-analysis/src/test/java/hu/bme/mit/theta/xcfa/analysis/XcfaPredAnalysisTest.kt +++ b/subprojects/xcfa/xcfa-analysis/src/test/java/hu/bme/mit/theta/xcfa/analysis/XcfaPredAnalysisTest.kt @@ -13,14 +13,13 @@ * See the License for the specific language governing permissions and * limitations under the License. */ - package hu.bme.mit.theta.xcfa.analysis -import hu.bme.mit.theta.analysis.algorithm.arg.ArgNodeComparators import hu.bme.mit.theta.analysis.algorithm.SafetyResult -import hu.bme.mit.theta.analysis.algorithm.cegar.Abstractor -import hu.bme.mit.theta.analysis.algorithm.cegar.CegarChecker -import hu.bme.mit.theta.analysis.algorithm.cegar.Refiner +import hu.bme.mit.theta.analysis.algorithm.arg.ArgNodeComparators +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 import hu.bme.mit.theta.analysis.algorithm.cegar.abstractor.StopCriterions import hu.bme.mit.theta.analysis.expr.refinement.* import hu.bme.mit.theta.analysis.pred.* @@ -39,262 +38,316 @@ import hu.bme.mit.theta.solver.z3legacy.Z3LegacySolverFactory import hu.bme.mit.theta.xcfa.analysis.coi.ConeOfInfluence import hu.bme.mit.theta.xcfa.analysis.coi.XcfaCoiMultiThread import hu.bme.mit.theta.xcfa.analysis.por.* +import java.util.* +import kotlin.random.Random import org.junit.jupiter.api.Assertions import org.junit.jupiter.params.ParameterizedTest import org.junit.jupiter.params.provider.MethodSource -import java.util.* -import kotlin.random.Random - class XcfaPredAnalysisTest { + companion object { - companion object { - - private val seed = 1001; - - @JvmStatic - fun data(): Collection> { - return listOf( - arrayOf("/00assignment.c", SafetyResult<*, *>::isUnsafe), - arrayOf("/01function.c", SafetyResult<*, *>::isUnsafe), - arrayOf("/02functionparam.c", SafetyResult<*, *>::isSafe), - arrayOf("/03nondetfunction.c", SafetyResult<*, *>::isUnsafe), - arrayOf("/04multithread.c", SafetyResult<*, *>::isUnsafe), - ) - } - } - - @ParameterizedTest - @MethodSource("data") - fun testNoporPred(filepath: String, verdict: (SafetyResult<*, *>) -> Boolean) { - println("Testing NOPOR on $filepath...") - val stream = javaClass.getResourceAsStream(filepath) - val xcfa = getXcfaFromC(stream!!, ParseContext(), false, false, NullLogger.getInstance()).first - ConeOfInfluence = XcfaCoiMultiThread(xcfa) - - val solver = Z3LegacySolverFactory.getInstance().createSolver() - val analysis = PredXcfaAnalysis( - xcfa, - solver, - PredAbstractors.cartesianAbstractor(solver), - getPartialOrder(PredOrd.create(solver).getPtrPartialOrd()), - false - ) - - val lts = getXcfaLts() - - val abstractor = getXcfaAbstractor(analysis, - PriorityWaitlist.create( - ArgNodeComparators.combine(ArgNodeComparators.targetFirst(), ArgNodeComparators.bfs())), - StopCriterions.firstCex>, XcfaAction>(), - ConsoleLogger(Logger.Level.DETAIL), - lts, - ErrorDetection.ERROR_LOCATION) as Abstractor>, XcfaAction, XcfaPrec>> - - val precRefiner = XcfaPrecRefiner>, PredPrec, ItpRefutation>( - ItpRefToPtrPrec(ItpRefToPredPrec(ExprSplitters.whole()))) - - val refiner = - XcfaSingleExprTraceRefiner.create( - ExprTraceBwBinItpChecker.create(BoolExprs.True(), BoolExprs.True(), - Z3LegacySolverFactory.getInstance().createItpSolver()), - precRefiner, PruneStrategy.FULL, - NullLogger.getInstance()) as Refiner>, XcfaAction, XcfaPrec>> - - val cegarChecker = - CegarChecker.create(abstractor, refiner) - - val safetyResult = cegarChecker.check(XcfaPrec(PtrPrec(PredPrec.of(), emptySet()))) - - - - Assertions.assertTrue(verdict(safetyResult)) - } - - @ParameterizedTest - @MethodSource("data") - fun testSporPred(filepath: String, verdict: (SafetyResult<*, *>) -> Boolean) { - println("Testing SPOR on $filepath...") - val stream = javaClass.getResourceAsStream(filepath) - val xcfa = getXcfaFromC(stream!!, ParseContext(), false, false, NullLogger.getInstance()).first - ConeOfInfluence = XcfaCoiMultiThread(xcfa) - - val solver = Z3LegacySolverFactory.getInstance().createSolver() - val analysis = PredXcfaAnalysis( - xcfa, - solver, - PredAbstractors.cartesianAbstractor(solver), - getPartialOrder(PredOrd.create(solver).getPtrPartialOrd()), false - ) - - val lts = XcfaSporLts(xcfa) - - val abstractor = getXcfaAbstractor(analysis, - PriorityWaitlist.create( - ArgNodeComparators.combine(ArgNodeComparators.targetFirst(), ArgNodeComparators.bfs())), - StopCriterions.firstCex>, XcfaAction>(), - ConsoleLogger(Logger.Level.DETAIL), - lts, - ErrorDetection.ERROR_LOCATION) as Abstractor>, XcfaAction, XcfaPrec>> - - val precRefiner = XcfaPrecRefiner>, PredPrec, ItpRefutation>( - ItpRefToPtrPrec(ItpRefToPredPrec(ExprSplitters.whole()))) - - val refiner = - XcfaSingleExprTraceRefiner.create( - ExprTraceBwBinItpChecker.create(BoolExprs.True(), BoolExprs.True(), - Z3LegacySolverFactory.getInstance().createItpSolver()), - precRefiner, PruneStrategy.FULL, - NullLogger.getInstance()) as Refiner>, XcfaAction, XcfaPrec>> - - val cegarChecker = - CegarChecker.create(abstractor, refiner) - - val safetyResult = cegarChecker.check(XcfaPrec(PtrPrec(PredPrec.of(), emptySet()))) - - - - Assertions.assertTrue(verdict(safetyResult)) - } - - @ParameterizedTest - @MethodSource("data") - fun testDporPred(filepath: String, verdict: (SafetyResult<*, *>) -> Boolean) { - XcfaDporLts.random = Random(seed) - println("Testing DPOR on $filepath...") - val stream = javaClass.getResourceAsStream(filepath) - val xcfa = getXcfaFromC(stream!!, ParseContext(), false, false, NullLogger.getInstance()).first - ConeOfInfluence = XcfaCoiMultiThread(xcfa) - - val solver = Z3LegacySolverFactory.getInstance().createSolver() - val analysis = PredXcfaAnalysis( - xcfa, - solver, - PredAbstractors.cartesianAbstractor(solver), - XcfaDporLts.getPartialOrder(getPartialOrder(PredOrd.create(solver).getPtrPartialOrd())), false - ) - - val lts = XcfaDporLts(xcfa) - - val abstractor = getXcfaAbstractor(analysis, - lts.waitlist, - StopCriterions.firstCex>, XcfaAction>(), - ConsoleLogger(Logger.Level.DETAIL), - lts, - ErrorDetection.ERROR_LOCATION) as Abstractor>, XcfaAction, XcfaPrec>> - - val precRefiner = XcfaPrecRefiner>, PredPrec, ItpRefutation>( - ItpRefToPtrPrec(ItpRefToPredPrec(ExprSplitters.whole()))) - - val refiner = - XcfaSingleExprTraceRefiner.create( - ExprTraceBwBinItpChecker.create(BoolExprs.True(), BoolExprs.True(), - Z3LegacySolverFactory.getInstance().createItpSolver()), - precRefiner, PruneStrategy.FULL, - ConsoleLogger( - Logger.Level.DETAIL)) as Refiner>, XcfaAction, XcfaPrec>> - - val cegarChecker = - CegarChecker.create(abstractor, refiner) - - val safetyResult = cegarChecker.check(XcfaPrec(PtrPrec(PredPrec.of(), emptySet()))) - - - - Assertions.assertTrue(verdict(safetyResult)) - } - - @ParameterizedTest - @MethodSource("data") - fun testAasporPred(filepath: String, verdict: (SafetyResult<*, *>) -> Boolean) { - println("Testing AASPOR on $filepath...") - val stream = javaClass.getResourceAsStream(filepath) - val xcfa = getXcfaFromC(stream!!, ParseContext(), false, false, NullLogger.getInstance()).first - ConeOfInfluence = XcfaCoiMultiThread(xcfa) - - val solver = Z3LegacySolverFactory.getInstance().createSolver() - val analysis = PredXcfaAnalysis( - xcfa, - solver, - PredAbstractors.cartesianAbstractor(solver), - getPartialOrder(PredOrd.create(solver).getPtrPartialOrd()), false - ) - - val lts = XcfaAasporLts(xcfa, mutableMapOf()) - - val abstractor = getXcfaAbstractor(analysis, - PriorityWaitlist.create( - ArgNodeComparators.combine(ArgNodeComparators.targetFirst(), ArgNodeComparators.bfs())), - StopCriterions.firstCex>, XcfaAction>(), - ConsoleLogger(Logger.Level.DETAIL), - lts, - ErrorDetection.ERROR_LOCATION) as Abstractor>, XcfaAction, XcfaPrec>> - - val precRefiner = XcfaPrecRefiner, PredPrec, ItpRefutation>( - ItpRefToPtrPrec(ItpRefToPredPrec(ExprSplitters.whole()))) - val atomicNodePruner = AtomicNodePruner>, XcfaAction>() - - val refiner = - XcfaSingleExprTraceRefiner.create( - ExprTraceBwBinItpChecker.create(BoolExprs.True(), BoolExprs.True(), - Z3LegacySolverFactory.getInstance().createItpSolver()), - precRefiner, PruneStrategy.FULL, NullLogger.getInstance(), - atomicNodePruner) as Refiner>, XcfaAction, XcfaPrec>> - - val cegarChecker = - CegarChecker.create(abstractor, AasporRefiner.create(refiner, PruneStrategy.FULL, mutableMapOf())) - - val safetyResult = cegarChecker.check(XcfaPrec(PtrPrec(PredPrec.of(), emptySet()))) - - - - Assertions.assertTrue(verdict(safetyResult)) - } - - @ParameterizedTest - @MethodSource("data") - fun testAadporPred(filepath: String, verdict: (SafetyResult<*, *>) -> Boolean) { - XcfaDporLts.random = Random(seed) - println("Testing AADPOR on $filepath...") - val stream = javaClass.getResourceAsStream(filepath) - val xcfa = getXcfaFromC(stream!!, ParseContext(), false, false, NullLogger.getInstance()).first - ConeOfInfluence = XcfaCoiMultiThread(xcfa) - - val solver = Z3LegacySolverFactory.getInstance().createSolver() - val analysis = PredXcfaAnalysis( - xcfa, - solver, - PredAbstractors.cartesianAbstractor(solver), - XcfaDporLts.getPartialOrder(getPartialOrder(PredOrd.create(solver).getPtrPartialOrd())), false - ) - - val lts = XcfaAadporLts(xcfa) - - val abstractor = getXcfaAbstractor(analysis, - lts.waitlist, - StopCriterions.firstCex>, XcfaAction>(), - ConsoleLogger(Logger.Level.DETAIL), - lts, - ErrorDetection.ERROR_LOCATION) as Abstractor>, XcfaAction, XcfaPrec>> - - val precRefiner = XcfaPrecRefiner( - ItpRefToPtrPrec(ItpRefToPredPrec(ExprSplitters.whole()))) - - val refiner = - XcfaSingleExprTraceRefiner.create( - ExprTraceBwBinItpChecker.create(BoolExprs.True(), BoolExprs.True(), - Z3LegacySolverFactory.getInstance().createItpSolver()), - precRefiner, PruneStrategy.FULL, - NullLogger.getInstance()) as Refiner>, XcfaAction, XcfaPrec>> - - val cegarChecker = - CegarChecker.create(abstractor, refiner) - - val safetyResult = cegarChecker.check(XcfaPrec(PtrPrec(PredPrec.of(), emptySet()))) - - + private val seed = 1001 - Assertions.assertTrue(verdict(safetyResult)) + @JvmStatic + fun data(): Collection> { + return listOf( + arrayOf("/00assignment.c", SafetyResult<*, *>::isUnsafe), + arrayOf("/01function.c", SafetyResult<*, *>::isUnsafe), + arrayOf("/02functionparam.c", SafetyResult<*, *>::isSafe), + arrayOf("/03nondetfunction.c", SafetyResult<*, *>::isUnsafe), + arrayOf("/04multithread.c", SafetyResult<*, *>::isUnsafe), + ) } -} \ No newline at end of file + } + + @ParameterizedTest + @MethodSource("data") + fun testNoporPred(filepath: String, verdict: (SafetyResult<*, *>) -> Boolean) { + println("Testing NOPOR on $filepath...") + val stream = javaClass.getResourceAsStream(filepath) + val xcfa = getXcfaFromC(stream!!, ParseContext(), false, false, NullLogger.getInstance()).first + ConeOfInfluence = XcfaCoiMultiThread(xcfa) + + val solver = Z3LegacySolverFactory.getInstance().createSolver() + val analysis = + PredXcfaAnalysis( + xcfa, + solver, + PredAbstractors.cartesianAbstractor(solver), + getPartialOrder(PredOrd.create(solver).getPtrPartialOrd()), + false, + ) + + val lts = getXcfaLts() + + val abstractor = + getXcfaAbstractor( + analysis, + PriorityWaitlist.create( + ArgNodeComparators.combine(ArgNodeComparators.targetFirst(), ArgNodeComparators.bfs()) + ), + StopCriterions.firstCex>, XcfaAction>(), + ConsoleLogger(Logger.Level.DETAIL), + lts, + ErrorDetection.ERROR_LOCATION, + ) + as ArgAbstractor>, XcfaAction, XcfaPrec>> + + val precRefiner = + XcfaPrecRefiner>, PredPrec, ItpRefutation>( + ItpRefToPtrPrec(ItpRefToPredPrec(ExprSplitters.whole())) + ) + + val refiner = + XcfaSingleExprTraceRefiner.create( + ExprTraceBwBinItpChecker.create( + BoolExprs.True(), + BoolExprs.True(), + Z3LegacySolverFactory.getInstance().createItpSolver(), + ), + precRefiner, + PruneStrategy.FULL, + NullLogger.getInstance(), + ) as ArgRefiner>, XcfaAction, XcfaPrec>> + + val cegarChecker = ArgCegarChecker.create(abstractor, refiner) + + val safetyResult = cegarChecker.check(XcfaPrec(PtrPrec(PredPrec.of(), emptySet()))) + + Assertions.assertTrue(verdict(safetyResult)) + } + + @ParameterizedTest + @MethodSource("data") + fun testSporPred(filepath: String, verdict: (SafetyResult<*, *>) -> Boolean) { + println("Testing SPOR on $filepath...") + val stream = javaClass.getResourceAsStream(filepath) + val xcfa = getXcfaFromC(stream!!, ParseContext(), false, false, NullLogger.getInstance()).first + ConeOfInfluence = XcfaCoiMultiThread(xcfa) + + val solver = Z3LegacySolverFactory.getInstance().createSolver() + val analysis = + PredXcfaAnalysis( + xcfa, + solver, + PredAbstractors.cartesianAbstractor(solver), + getPartialOrder(PredOrd.create(solver).getPtrPartialOrd()), + false, + ) + + val lts = XcfaSporLts(xcfa) + + val abstractor = + getXcfaAbstractor( + analysis, + PriorityWaitlist.create( + ArgNodeComparators.combine(ArgNodeComparators.targetFirst(), ArgNodeComparators.bfs()) + ), + StopCriterions.firstCex>, XcfaAction>(), + ConsoleLogger(Logger.Level.DETAIL), + lts, + ErrorDetection.ERROR_LOCATION, + ) + as ArgAbstractor>, XcfaAction, XcfaPrec>> + + val precRefiner = + XcfaPrecRefiner>, PredPrec, ItpRefutation>( + ItpRefToPtrPrec(ItpRefToPredPrec(ExprSplitters.whole())) + ) + + val refiner = + XcfaSingleExprTraceRefiner.create( + ExprTraceBwBinItpChecker.create( + BoolExprs.True(), + BoolExprs.True(), + Z3LegacySolverFactory.getInstance().createItpSolver(), + ), + precRefiner, + PruneStrategy.FULL, + NullLogger.getInstance(), + ) as ArgRefiner>, XcfaAction, XcfaPrec>> + + val cegarChecker = ArgCegarChecker.create(abstractor, refiner) + + val safetyResult = cegarChecker.check(XcfaPrec(PtrPrec(PredPrec.of(), emptySet()))) + + Assertions.assertTrue(verdict(safetyResult)) + } + + @ParameterizedTest + @MethodSource("data") + fun testDporPred(filepath: String, verdict: (SafetyResult<*, *>) -> Boolean) { + XcfaDporLts.random = Random(seed) + println("Testing DPOR on $filepath...") + val stream = javaClass.getResourceAsStream(filepath) + val xcfa = getXcfaFromC(stream!!, ParseContext(), false, false, NullLogger.getInstance()).first + ConeOfInfluence = XcfaCoiMultiThread(xcfa) + + val solver = Z3LegacySolverFactory.getInstance().createSolver() + val analysis = + PredXcfaAnalysis( + xcfa, + solver, + PredAbstractors.cartesianAbstractor(solver), + XcfaDporLts.getPartialOrder(getPartialOrder(PredOrd.create(solver).getPtrPartialOrd())), + false, + ) + + val lts = XcfaDporLts(xcfa) + + val abstractor = + getXcfaAbstractor( + analysis, + lts.waitlist, + StopCriterions.firstCex>, XcfaAction>(), + ConsoleLogger(Logger.Level.DETAIL), + lts, + ErrorDetection.ERROR_LOCATION, + ) + as ArgAbstractor>, XcfaAction, XcfaPrec>> + + val precRefiner = + XcfaPrecRefiner>, PredPrec, ItpRefutation>( + ItpRefToPtrPrec(ItpRefToPredPrec(ExprSplitters.whole())) + ) + + val refiner = + XcfaSingleExprTraceRefiner.create( + ExprTraceBwBinItpChecker.create( + BoolExprs.True(), + BoolExprs.True(), + Z3LegacySolverFactory.getInstance().createItpSolver(), + ), + precRefiner, + PruneStrategy.FULL, + ConsoleLogger(Logger.Level.DETAIL), + ) as ArgRefiner>, XcfaAction, XcfaPrec>> + + val cegarChecker = ArgCegarChecker.create(abstractor, refiner) + + val safetyResult = cegarChecker.check(XcfaPrec(PtrPrec(PredPrec.of(), emptySet()))) + + Assertions.assertTrue(verdict(safetyResult)) + } + + @ParameterizedTest + @MethodSource("data") + fun testAasporPred(filepath: String, verdict: (SafetyResult<*, *>) -> Boolean) { + println("Testing AASPOR on $filepath...") + val stream = javaClass.getResourceAsStream(filepath) + val xcfa = getXcfaFromC(stream!!, ParseContext(), false, false, NullLogger.getInstance()).first + ConeOfInfluence = XcfaCoiMultiThread(xcfa) + + val solver = Z3LegacySolverFactory.getInstance().createSolver() + val analysis = + PredXcfaAnalysis( + xcfa, + solver, + PredAbstractors.cartesianAbstractor(solver), + getPartialOrder(PredOrd.create(solver).getPtrPartialOrd()), + false, + ) + + val lts = XcfaAasporLts(xcfa, mutableMapOf()) + + val abstractor = + getXcfaAbstractor( + analysis, + PriorityWaitlist.create( + ArgNodeComparators.combine(ArgNodeComparators.targetFirst(), ArgNodeComparators.bfs()) + ), + StopCriterions.firstCex>, XcfaAction>(), + ConsoleLogger(Logger.Level.DETAIL), + lts, + ErrorDetection.ERROR_LOCATION, + ) + as ArgAbstractor>, XcfaAction, XcfaPrec>> + + val precRefiner = + XcfaPrecRefiner, PredPrec, ItpRefutation>( + ItpRefToPtrPrec(ItpRefToPredPrec(ExprSplitters.whole())) + ) + val atomicNodePruner = AtomicNodePruner>, XcfaAction>() + + val refiner = + XcfaSingleExprTraceRefiner.create( + ExprTraceBwBinItpChecker.create( + BoolExprs.True(), + BoolExprs.True(), + Z3LegacySolverFactory.getInstance().createItpSolver(), + ), + precRefiner, + PruneStrategy.FULL, + NullLogger.getInstance(), + atomicNodePruner, + ) as ArgRefiner>, XcfaAction, XcfaPrec>> + + val cegarChecker = + ArgCegarChecker.create( + abstractor, + AasporRefiner.create(refiner, PruneStrategy.FULL, mutableMapOf()), + ) + + val safetyResult = cegarChecker.check(XcfaPrec(PtrPrec(PredPrec.of(), emptySet()))) + + Assertions.assertTrue(verdict(safetyResult)) + } + + @ParameterizedTest + @MethodSource("data") + fun testAadporPred(filepath: String, verdict: (SafetyResult<*, *>) -> Boolean) { + XcfaDporLts.random = Random(seed) + println("Testing AADPOR on $filepath...") + val stream = javaClass.getResourceAsStream(filepath) + val xcfa = getXcfaFromC(stream!!, ParseContext(), false, false, NullLogger.getInstance()).first + ConeOfInfluence = XcfaCoiMultiThread(xcfa) + + val solver = Z3LegacySolverFactory.getInstance().createSolver() + val analysis = + PredXcfaAnalysis( + xcfa, + solver, + PredAbstractors.cartesianAbstractor(solver), + XcfaDporLts.getPartialOrder(getPartialOrder(PredOrd.create(solver).getPtrPartialOrd())), + false, + ) + + val lts = XcfaAadporLts(xcfa) + + val abstractor = + getXcfaAbstractor( + analysis, + lts.waitlist, + StopCriterions.firstCex>, XcfaAction>(), + ConsoleLogger(Logger.Level.DETAIL), + lts, + ErrorDetection.ERROR_LOCATION, + ) + as ArgAbstractor>, XcfaAction, XcfaPrec>> + + val precRefiner = + XcfaPrecRefiner( + ItpRefToPtrPrec(ItpRefToPredPrec(ExprSplitters.whole())) + ) + + val refiner = + XcfaSingleExprTraceRefiner.create( + ExprTraceBwBinItpChecker.create( + BoolExprs.True(), + BoolExprs.True(), + Z3LegacySolverFactory.getInstance().createItpSolver(), + ), + precRefiner, + PruneStrategy.FULL, + NullLogger.getInstance(), + ) as ArgRefiner>, XcfaAction, XcfaPrec>> + + val cegarChecker = ArgCegarChecker.create(abstractor, refiner) + + val safetyResult = cegarChecker.check(XcfaPrec(PtrPrec(PredPrec.of(), emptySet()))) + + Assertions.assertTrue(verdict(safetyResult)) + } +} 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 8c39486021..f8bf86f8d2 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 @@ -23,9 +23,9 @@ 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.cegar.Abstractor -import hu.bme.mit.theta.analysis.algorithm.cegar.CegarChecker -import hu.bme.mit.theta.analysis.algorithm.cegar.Refiner +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 import hu.bme.mit.theta.analysis.expr.ExprAction import hu.bme.mit.theta.analysis.expr.ExprState import hu.bme.mit.theta.analysis.expr.refinement.* @@ -43,14 +43,20 @@ import hu.bme.mit.theta.xcfa.cli.params.* import hu.bme.mit.theta.xcfa.cli.utils.getSolver import hu.bme.mit.theta.xcfa.model.XCFA -fun getCegarChecker(xcfa: XCFA, mcm: MCM, +fun getCegarChecker( + xcfa: XCFA, mcm: MCM, config: XcfaConfig<*, *>, - logger: Logger): SafetyChecker, XcfaAction>, Trace>, XcfaAction>, XcfaPrec<*>> { + logger: Logger +): SafetyChecker, 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 abstractionSolverFactory: SolverFactory = getSolver( + cegarConfig.abstractorConfig.abstractionSolver, + cegarConfig.abstractorConfig.validateAbstractionSolver + ) + val refinementSolverFactory: SolverFactory = getSolver( + cegarConfig.refinerConfig.refinementSolver, + cegarConfig.refinerConfig.validateRefinementSolver + ) val ignoredVarRegistry = mutableMapOf, MutableSet>() @@ -59,16 +65,18 @@ fun getCegarChecker(xcfa: XCFA, mcm: MCM, (cegarConfig.coi.porLts as XcfaDporLts).waitlist } else { PriorityWaitlist.create>, XcfaAction>>( - cegarConfig.abstractorConfig.search.getComp(xcfa)) + cegarConfig.abstractorConfig.search.getComp(xcfa) + ) } val abstractionSolverInstance = abstractionSolverFactory.createSolver() val globalStatePartialOrd: PartialOrd> = cegarConfig.abstractorConfig.domain.partialOrd( - abstractionSolverInstance) as PartialOrd> + abstractionSolverInstance + ) as PartialOrd> val corePartialOrd: PartialOrd>> = if (xcfa.isInlined) getPartialOrder(globalStatePartialOrd) else getStackPartialOrder(globalStatePartialOrd) - val abstractor: Abstractor = cegarConfig.abstractorConfig.domain.abstractor( + val abstractor: ArgAbstractor = cegarConfig.abstractorConfig.domain.abstractor( xcfa, abstractionSolverInstance, cegarConfig.abstractorConfig.maxEnum, @@ -83,7 +91,7 @@ fun getCegarChecker(xcfa: XCFA, mcm: MCM, corePartialOrd }, cegarConfig.abstractorConfig.havocMemory - ) as Abstractor + ) as ArgAbstractor val ref: ExprTraceChecker = cegarConfig.refinerConfig.refinement.refiner(refinementSolverFactory, cegarConfig.cexMonitor) @@ -91,43 +99,50 @@ fun getCegarChecker(xcfa: XCFA, mcm: MCM, val precRefiner: PrecRefiner = cegarConfig.abstractorConfig.domain.itpPrecRefiner(cegarConfig.refinerConfig.exprSplitter.exprSplitter) as PrecRefiner - val atomicNodePruner: NodePruner = cegarConfig.abstractorConfig.domain.nodePruner as NodePruner - val refiner: Refiner = + 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) + 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) + 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) - CegarChecker.create( + ArgCegarChecker.create( abstractor, AasporRefiner.create(refiner, cegarConfig.refinerConfig.pruneStrategy, ignoredVarRegistry), logger ) else - CegarChecker.create(abstractor, refiner, logger) + ArgCegarChecker.create(abstractor, refiner, logger) // initialize monitors MonitorCheckpoint.reset() if (cegarConfig.cexMonitor == CexMonitorOptions.CHECK) { - val cm = CexMonitor(logger, cegarChecker.arg) + val cm = CexMonitor(logger, cegarChecker.witness) MonitorCheckpoint.register(cm, "CegarChecker.unsafeARG") } return object : SafetyChecker, XcfaAction>, Trace>, XcfaAction>, XcfaPrec<*>> { override fun check( - prec: XcfaPrec<*>?): SafetyResult, XcfaAction>, Trace>, XcfaAction>> { + prec: XcfaPrec<*>? + ): SafetyResult, XcfaAction>, Trace>, XcfaAction>> { return cegarChecker.check( - prec) as SafetyResult, XcfaAction>, Trace>, XcfaAction>> + prec + ) as SafetyResult, XcfaAction>, Trace>, XcfaAction>> } override fun check(): SafetyResult, XcfaAction>, Trace>, XcfaAction>> { diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/params/ParamValues.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/params/ParamValues.kt index ac5b3d3236..8f1695855c 100644 --- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/params/ParamValues.kt +++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/params/ParamValues.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.params import com.google.gson.reflect.TypeToken @@ -23,7 +22,7 @@ import hu.bme.mit.theta.analysis.Prec import hu.bme.mit.theta.analysis.algorithm.arg.ArgNode import hu.bme.mit.theta.analysis.algorithm.arg.ArgNodeComparators import hu.bme.mit.theta.analysis.algorithm.arg.ArgNodeComparators.ArgNodeComparator -import hu.bme.mit.theta.analysis.algorithm.cegar.Abstractor +import hu.bme.mit.theta.analysis.algorithm.cegar.ArgAbstractor import hu.bme.mit.theta.analysis.algorithm.cegar.abstractor.StopCriterion import hu.bme.mit.theta.analysis.algorithm.cegar.abstractor.StopCriterions import hu.bme.mit.theta.analysis.expl.ExplPrec @@ -55,309 +54,386 @@ import hu.bme.mit.theta.xcfa.model.XCFA import java.lang.reflect.Type enum class InputType { - C, - LLVM, - JSON, - DSL, - CHC, - LITMUS, + C, + LLVM, + JSON, + DSL, + CHC, + LITMUS, } enum class Backend { - CEGAR, - BOUNDED, - CHC, - OC, - LAZY, - PORTFOLIO, - NONE, + CEGAR, + BOUNDED, + CHC, + OC, + LAZY, + PORTFOLIO, + NONE, } enum class POR( - val getLts: (XCFA, MutableMap, MutableSet>) -> LTS>, XcfaAction>, - val isDynamic: Boolean, - val isAbstractionAware: Boolean + val getLts: + (XCFA, MutableMap, MutableSet>) -> LTS< + XcfaState>, + XcfaAction, + >, + val isDynamic: Boolean, + val isAbstractionAware: Boolean, ) { - NOPOR({ _, _ -> getXcfaLts() }, false, false), - SPOR({ xcfa, _ -> XcfaSporLts(xcfa) }, false, false), - AASPOR({ xcfa, registry -> XcfaAasporLts(xcfa, registry) }, false, true), - DPOR({ xcfa, _ -> XcfaDporLts(xcfa) }, true, false), - AADPOR({ xcfa, _ -> XcfaAadporLts(xcfa) }, true, true) + NOPOR({ _, _ -> getXcfaLts() }, false, false), + SPOR({ xcfa, _ -> XcfaSporLts(xcfa) }, false, false), + AASPOR({ xcfa, registry -> XcfaAasporLts(xcfa, registry) }, false, true), + DPOR({ xcfa, _ -> XcfaDporLts(xcfa) }, true, false), + AADPOR({ xcfa, _ -> XcfaAadporLts(xcfa) }, true, true), } enum class Strategy { - DIRECT, - SERVER, - SERVER_DEBUG, - PORTFOLIO + DIRECT, + SERVER, + SERVER_DEBUG, + PORTFOLIO, } // TODO partial orders nicely enum class Domain( - val abstractor: ( - xcfa: XCFA, - solver: Solver, - maxEnum: Int, - waitlist: Waitlist>, XcfaAction>>, - stopCriterion: StopCriterion>, XcfaAction>, - logger: Logger, - lts: LTS>, XcfaAction>, - errorDetectionType: ErrorDetection, - partialOrd: PartialOrd>>, - isHavoc: Boolean - ) -> Abstractor, - val itpPrecRefiner: (exprSplitter: ExprSplitter) -> PrecRefiner, - val initPrec: (XCFA, InitPrec) -> XcfaPrec>, - val partialOrd: (Solver) -> PartialOrd>, - val nodePruner: NodePruner, - val stateType: Type + val abstractor: + ( + xcfa: XCFA, + solver: Solver, + maxEnum: Int, + waitlist: Waitlist>, XcfaAction>>, + stopCriterion: StopCriterion>, XcfaAction>, + logger: Logger, + lts: LTS>, XcfaAction>, + errorDetectionType: ErrorDetection, + partialOrd: PartialOrd>>, + isHavoc: Boolean, + ) -> ArgAbstractor, + val itpPrecRefiner: + (exprSplitter: ExprSplitter) -> PrecRefiner< + out ExprState, + out ExprAction, + out Prec, + out Refutation, + >, + val initPrec: (XCFA, InitPrec) -> XcfaPrec>, + val partialOrd: (Solver) -> PartialOrd>, + val nodePruner: NodePruner, + val stateType: Type, ) { - EXPL( - abstractor = { a, b, c, d, e, f, g, h, i, j -> - getXcfaAbstractor(ExplXcfaAnalysis(a, b, c, i as PartialOrd>>, j), d, - e, f, g, h) - }, - itpPrecRefiner = { - XcfaPrecRefiner, ExplPrec, ItpRefutation>(ItpRefToPtrPrec(ItpRefToExplPrec())) - }, - initPrec = { x, ip -> ip.explPrec(x) }, - partialOrd = { PartialOrd { s1, s2 -> s1.isLeq(s2) }.getPtrPartialOrd() }, - nodePruner = AtomicNodePruner>, XcfaAction>(), - stateType = TypeToken.get(ExplState::class.java).type - ), - PRED_BOOL( - abstractor = { a, b, c, d, e, f, g, h, i, j -> - getXcfaAbstractor(PredXcfaAnalysis(a, b, PredAbstractors.booleanAbstractor(b), - i as PartialOrd>>, j), d, e, f, g, h) - }, - itpPrecRefiner = { a -> - XcfaPrecRefiner, PredPrec, ItpRefutation>(ItpRefToPtrPrec(ItpRefToPredPrec(a))) - }, - initPrec = { x, ip -> ip.predPrec(x) }, - partialOrd = { solver -> PredOrd.create(solver).getPtrPartialOrd() }, - nodePruner = AtomicNodePruner>, XcfaAction>(), - stateType = TypeToken.get(PredState::class.java).type - ), - PRED_CART( - abstractor = { a, b, c, d, e, f, g, h, i, j -> - getXcfaAbstractor(PredXcfaAnalysis(a, b, PredAbstractors.cartesianAbstractor(b), - i as PartialOrd>>, j), d, e, f, g, h) - }, - itpPrecRefiner = { a -> - XcfaPrecRefiner, PredPrec, ItpRefutation>(ItpRefToPtrPrec(ItpRefToPredPrec(a))) - }, - initPrec = { x, ip -> ip.predPrec(x) }, - partialOrd = { solver -> PredOrd.create(solver).getPtrPartialOrd() }, - nodePruner = AtomicNodePruner>, XcfaAction>(), - stateType = TypeToken.get(PredState::class.java).type - ), - PRED_SPLIT( - abstractor = { a, b, c, d, e, f, g, h, i, j -> - getXcfaAbstractor(PredXcfaAnalysis(a, b, PredAbstractors.booleanSplitAbstractor(b), - i as PartialOrd>>, j), d, e, f, g, h) - }, - itpPrecRefiner = { a -> - XcfaPrecRefiner, PredPrec, ItpRefutation>(ItpRefToPtrPrec(ItpRefToPredPrec(a))) - }, - initPrec = { x, ip -> ip.predPrec(x) }, - partialOrd = { solver -> PredOrd.create(solver).getPtrPartialOrd() }, - nodePruner = AtomicNodePruner>, XcfaAction>(), - stateType = TypeToken.get(PredState::class.java).type - ), + EXPL( + abstractor = { a, b, c, d, e, f, g, h, i, j -> + getXcfaAbstractor( + ExplXcfaAnalysis(a, b, c, i as PartialOrd>>, j), + d, + e, + f, + g, + h, + ) + }, + itpPrecRefiner = { + XcfaPrecRefiner, ExplPrec, ItpRefutation>( + ItpRefToPtrPrec(ItpRefToExplPrec()) + ) + }, + initPrec = { x, ip -> ip.explPrec(x) }, + partialOrd = { PartialOrd { s1, s2 -> s1.isLeq(s2) }.getPtrPartialOrd() }, + nodePruner = AtomicNodePruner>, XcfaAction>(), + stateType = TypeToken.get(ExplState::class.java).type, + ), + PRED_BOOL( + abstractor = { a, b, c, d, e, f, g, h, i, j -> + getXcfaAbstractor( + PredXcfaAnalysis( + a, + b, + PredAbstractors.booleanAbstractor(b), + i as PartialOrd>>, + j, + ), + d, + e, + f, + g, + h, + ) + }, + itpPrecRefiner = { a -> + XcfaPrecRefiner, PredPrec, ItpRefutation>( + ItpRefToPtrPrec(ItpRefToPredPrec(a)) + ) + }, + initPrec = { x, ip -> ip.predPrec(x) }, + partialOrd = { solver -> PredOrd.create(solver).getPtrPartialOrd() }, + nodePruner = AtomicNodePruner>, XcfaAction>(), + stateType = TypeToken.get(PredState::class.java).type, + ), + PRED_CART( + abstractor = { a, b, c, d, e, f, g, h, i, j -> + getXcfaAbstractor( + PredXcfaAnalysis( + a, + b, + PredAbstractors.cartesianAbstractor(b), + i as PartialOrd>>, + j, + ), + d, + e, + f, + g, + h, + ) + }, + itpPrecRefiner = { a -> + XcfaPrecRefiner, PredPrec, ItpRefutation>( + ItpRefToPtrPrec(ItpRefToPredPrec(a)) + ) + }, + initPrec = { x, ip -> ip.predPrec(x) }, + partialOrd = { solver -> PredOrd.create(solver).getPtrPartialOrd() }, + nodePruner = AtomicNodePruner>, XcfaAction>(), + stateType = TypeToken.get(PredState::class.java).type, + ), + PRED_SPLIT( + abstractor = { a, b, c, d, e, f, g, h, i, j -> + getXcfaAbstractor( + PredXcfaAnalysis( + a, + b, + PredAbstractors.booleanSplitAbstractor(b), + i as PartialOrd>>, + j, + ), + d, + e, + f, + g, + h, + ) + }, + itpPrecRefiner = { a -> + XcfaPrecRefiner, PredPrec, ItpRefutation>( + ItpRefToPtrPrec(ItpRefToPredPrec(a)) + ) + }, + initPrec = { x, ip -> ip.predPrec(x) }, + partialOrd = { solver -> PredOrd.create(solver).getPtrPartialOrd() }, + nodePruner = AtomicNodePruner>, XcfaAction>(), + stateType = TypeToken.get(PredState::class.java).type, + ), } enum class Refinement( - val refiner: (solverFactory: SolverFactory, monitorOption: CexMonitorOptions) -> ExprTraceChecker, - val stopCriterion: StopCriterion>, XcfaAction>, + val refiner: + (solverFactory: SolverFactory, monitorOption: CexMonitorOptions) -> ExprTraceChecker< + out Refutation + >, + val stopCriterion: StopCriterion>, XcfaAction>, ) { - FW_BIN_ITP( - refiner = { s, _ -> - ExprTraceFwBinItpChecker.create(BoolExprs.True(), BoolExprs.True(), s.createItpSolver()) - }, - stopCriterion = StopCriterions.firstCex(), - ), - BW_BIN_ITP( - refiner = { s, _ -> - ExprTraceBwBinItpChecker.create(BoolExprs.True(), BoolExprs.True(), s.createItpSolver()) - }, - stopCriterion = StopCriterions.firstCex() - ), - SEQ_ITP( - refiner = { s, _ -> - ExprTraceSeqItpChecker.create(BoolExprs.True(), BoolExprs.True(), s.createItpSolver()) - }, - stopCriterion = StopCriterions.firstCex() - ), - MULTI_SEQ( - refiner = { s, m -> - if (m == CexMonitorOptions.CHECK) error("CexMonitor is not implemented for MULTI_SEQ") - ExprTraceSeqItpChecker.create(BoolExprs.True(), BoolExprs.True(), s.createItpSolver()) - }, - stopCriterion = StopCriterions.fullExploration() - ), - UNSAT_CORE( - refiner = { s, _ -> - ExprTraceUnsatCoreChecker.create(BoolExprs.True(), BoolExprs.True(), s.createUCSolver()) - }, - stopCriterion = StopCriterions.firstCex() - ), - UCB( - refiner = { s, _ -> - ExprTraceUCBChecker.create(BoolExprs.True(), BoolExprs.True(), s.createUCSolver()) - }, - stopCriterion = StopCriterions.firstCex() - ), - - NWT_SP( - refiner = { s, _ -> - ExprTraceNewtonChecker.create(BoolExprs.True(), BoolExprs.True(), s.createUCSolver()) - .withoutIT().withSP().withoutLV() - }, - stopCriterion = StopCriterions.firstCex() - ), - NWT_WP( - refiner = { s, _ -> - ExprTraceNewtonChecker.create(BoolExprs.True(), BoolExprs.True(), s.createUCSolver()) - .withoutIT().withWP().withoutLV() - }, - stopCriterion = StopCriterions.firstCex() - ), - NWT_SP_LV( - refiner = { s, _ -> - ExprTraceNewtonChecker.create(BoolExprs.True(), BoolExprs.True(), s.createUCSolver()) - .withoutIT().withSP().withLV() - }, - stopCriterion = StopCriterions.firstCex() - ), - NWT_WP_LV( - refiner = { s, _ -> - ExprTraceNewtonChecker.create(BoolExprs.True(), BoolExprs.True(), s.createUCSolver()) - .withoutIT().withWP().withLV() - }, - stopCriterion = StopCriterions.firstCex() - ), - NWT_IT_WP( - refiner = { s, _ -> - ExprTraceNewtonChecker.create(BoolExprs.True(), BoolExprs.True(), s.createUCSolver()) - .withIT().withWP().withoutLV() - }, - stopCriterion = StopCriterions.firstCex() - ), - NWT_IT_SP( - refiner = { s, _ -> - ExprTraceNewtonChecker.create(BoolExprs.True(), BoolExprs.True(), s.createUCSolver()) - .withIT().withSP().withoutLV() - }, - stopCriterion = StopCriterions.firstCex() - ), - NWT_IT_WP_LV( - refiner = { s, _ -> - ExprTraceNewtonChecker.create(BoolExprs.True(), BoolExprs.True(), s.createUCSolver()) - .withIT().withWP().withLV() - }, - stopCriterion = StopCriterions.firstCex() - ), - NWT_IT_SP_LV( - refiner = { s, _ -> - ExprTraceNewtonChecker.create(BoolExprs.True(), BoolExprs.True(), s.createUCSolver()) - .withIT().withSP().withLV() - }, - stopCriterion = StopCriterions.firstCex() - ) + FW_BIN_ITP( + refiner = { s, _ -> + ExprTraceFwBinItpChecker.create(BoolExprs.True(), BoolExprs.True(), s.createItpSolver()) + }, + stopCriterion = StopCriterions.firstCex(), + ), + BW_BIN_ITP( + refiner = { s, _ -> + ExprTraceBwBinItpChecker.create(BoolExprs.True(), BoolExprs.True(), s.createItpSolver()) + }, + stopCriterion = StopCriterions.firstCex(), + ), + SEQ_ITP( + refiner = { s, _ -> + ExprTraceSeqItpChecker.create(BoolExprs.True(), BoolExprs.True(), s.createItpSolver()) + }, + stopCriterion = StopCriterions.firstCex(), + ), + MULTI_SEQ( + refiner = { s, m -> + if (m == CexMonitorOptions.CHECK) error("CexMonitor is not implemented for MULTI_SEQ") + ExprTraceSeqItpChecker.create(BoolExprs.True(), BoolExprs.True(), s.createItpSolver()) + }, + stopCriterion = StopCriterions.fullExploration(), + ), + UNSAT_CORE( + refiner = { s, _ -> + ExprTraceUnsatCoreChecker.create(BoolExprs.True(), BoolExprs.True(), s.createUCSolver()) + }, + stopCriterion = StopCriterions.firstCex(), + ), + UCB( + refiner = { s, _ -> + ExprTraceUCBChecker.create(BoolExprs.True(), BoolExprs.True(), s.createUCSolver()) + }, + stopCriterion = StopCriterions.firstCex(), + ), + NWT_SP( + refiner = { s, _ -> + ExprTraceNewtonChecker.create(BoolExprs.True(), BoolExprs.True(), s.createUCSolver()) + .withoutIT() + .withSP() + .withoutLV() + }, + stopCriterion = StopCriterions.firstCex(), + ), + NWT_WP( + refiner = { s, _ -> + ExprTraceNewtonChecker.create(BoolExprs.True(), BoolExprs.True(), s.createUCSolver()) + .withoutIT() + .withWP() + .withoutLV() + }, + stopCriterion = StopCriterions.firstCex(), + ), + NWT_SP_LV( + refiner = { s, _ -> + ExprTraceNewtonChecker.create(BoolExprs.True(), BoolExprs.True(), s.createUCSolver()) + .withoutIT() + .withSP() + .withLV() + }, + stopCriterion = StopCriterions.firstCex(), + ), + NWT_WP_LV( + refiner = { s, _ -> + ExprTraceNewtonChecker.create(BoolExprs.True(), BoolExprs.True(), s.createUCSolver()) + .withoutIT() + .withWP() + .withLV() + }, + stopCriterion = StopCriterions.firstCex(), + ), + NWT_IT_WP( + refiner = { s, _ -> + ExprTraceNewtonChecker.create(BoolExprs.True(), BoolExprs.True(), s.createUCSolver()) + .withIT() + .withWP() + .withoutLV() + }, + stopCriterion = StopCriterions.firstCex(), + ), + NWT_IT_SP( + refiner = { s, _ -> + ExprTraceNewtonChecker.create(BoolExprs.True(), BoolExprs.True(), s.createUCSolver()) + .withIT() + .withSP() + .withoutLV() + }, + stopCriterion = StopCriterions.firstCex(), + ), + NWT_IT_WP_LV( + refiner = { s, _ -> + ExprTraceNewtonChecker.create(BoolExprs.True(), BoolExprs.True(), s.createUCSolver()) + .withIT() + .withWP() + .withLV() + }, + stopCriterion = StopCriterions.firstCex(), + ), + NWT_IT_SP_LV( + refiner = { s, _ -> + ExprTraceNewtonChecker.create(BoolExprs.True(), BoolExprs.True(), s.createUCSolver()) + .withIT() + .withSP() + .withLV() + }, + stopCriterion = StopCriterions.firstCex(), + ), } - enum class ExprSplitterOptions(val exprSplitter: ExprSplitter) { - WHOLE(ExprSplitters.whole()), - CONJUNCTS(ExprSplitters.conjuncts()), - ATOMS(ExprSplitters.atoms()); + WHOLE(ExprSplitters.whole()), + CONJUNCTS(ExprSplitters.conjuncts()), + ATOMS(ExprSplitters.atoms()), } enum class Search { - BFS { + BFS { - override fun getComp(cfa: XCFA): ArgNodeComparator { - return ArgNodeComparators.combine(ArgNodeComparators.targetFirst(), - ArgNodeComparators.bfs()) - } - }, - DFS { + override fun getComp(cfa: XCFA): ArgNodeComparator { + return ArgNodeComparators.combine(ArgNodeComparators.targetFirst(), ArgNodeComparators.bfs()) + } + }, + DFS { - override fun getComp(cfa: XCFA): ArgNodeComparator { - return ArgNodeComparators.combine(ArgNodeComparators.targetFirst(), - ArgNodeComparators.dfs()) - } - }, - ERR { + override fun getComp(cfa: XCFA): ArgNodeComparator { + return ArgNodeComparators.combine(ArgNodeComparators.targetFirst(), ArgNodeComparators.dfs()) + } + }, + ERR { - override fun getComp(cfa: XCFA): ArgNodeComparator { - return XcfaDistToErrComparator(cfa) - } - }; + override fun getComp(cfa: XCFA): ArgNodeComparator { + return XcfaDistToErrComparator(cfa) + } + }; - abstract fun getComp(cfa: XCFA): ArgNodeComparator + abstract fun getComp(cfa: XCFA): ArgNodeComparator } enum class InitPrec( - val explPrec: (xcfa: XCFA) -> XcfaPrec>, - val predPrec: (xcfa: XCFA) -> XcfaPrec>, + val explPrec: (xcfa: XCFA) -> XcfaPrec>, + val predPrec: (xcfa: XCFA) -> XcfaPrec>, ) { - EMPTY( - explPrec = { XcfaPrec(PtrPrec(ExplPrec.empty(), emptySet())) }, - predPrec = { XcfaPrec(PtrPrec(PredPrec.of(), emptySet())) } - ), - ALLVARS( - explPrec = { xcfa -> XcfaPrec(PtrPrec(ExplPrec.of(xcfa.collectVars()), emptySet())) }, - predPrec = { error("ALLVARS is not interpreted for the predicate domain.") } - ), - ALLGLOBALS( - explPrec = { xcfa -> XcfaPrec(PtrPrec(ExplPrec.of(xcfa.vars.map { it.wrappedVar }), emptySet())) }, - predPrec = { error("ALLGLOBALS is not interpreted for the predicate domain.") } - ), - ALLASSUMES( - explPrec = { xcfa -> - XcfaPrec( - PtrPrec(ExplPrec.of(xcfa.collectAssumes().flatMap(ExprUtils::getVars)), emptySet())) - }, - predPrec = { xcfa -> XcfaPrec(PtrPrec(PredPrec.of(xcfa.collectAssumes()), emptySet())) }, - ), - + EMPTY( + explPrec = { XcfaPrec(PtrPrec(ExplPrec.empty(), emptySet())) }, + predPrec = { XcfaPrec(PtrPrec(PredPrec.of(), emptySet())) }, + ), + ALLVARS( + explPrec = { xcfa -> XcfaPrec(PtrPrec(ExplPrec.of(xcfa.collectVars()), emptySet())) }, + predPrec = { error("ALLVARS is not interpreted for the predicate domain.") }, + ), + ALLGLOBALS( + explPrec = { xcfa -> + XcfaPrec(PtrPrec(ExplPrec.of(xcfa.vars.map { it.wrappedVar }), emptySet())) + }, + predPrec = { error("ALLGLOBALS is not interpreted for the predicate domain.") }, + ), + ALLASSUMES( + explPrec = { xcfa -> + XcfaPrec(PtrPrec(ExplPrec.of(xcfa.collectAssumes().flatMap(ExprUtils::getVars)), emptySet())) + }, + predPrec = { xcfa -> XcfaPrec(PtrPrec(PredPrec.of(xcfa.collectAssumes()), emptySet())) }, + ), } enum class ConeOfInfluenceMode( - val getLts: (XCFA, MutableMap, MutableSet>, POR) -> LTS>, XcfaAction> + val getLts: + (XCFA, MutableMap, MutableSet>, POR) -> LTS< + XcfaState>, + XcfaAction, + > ) { - NO_COI({ xcfa, ivr, por -> - por.getLts(xcfa, ivr).also { NO_COI.porLts = it } - }), - COI({ xcfa, ivr, por -> - ConeOfInfluence.coreLts = por.getLts(xcfa, ivr).also { COI.porLts = it } - ConeOfInfluence.lts - }), - POR_COI({ xcfa, ivr, por -> - ConeOfInfluence.coreLts = getXcfaLts() - if (por.isAbstractionAware) XcfaAasporCoiLts(xcfa, ivr, ConeOfInfluence.lts) - else XcfaSporCoiLts(xcfa, ConeOfInfluence.lts) - }), - POR_COI_POR({ xcfa, ivr, por -> - ConeOfInfluence.coreLts = por.getLts(xcfa, ivr).also { POR_COI_POR.porLts = it } - if (por.isAbstractionAware) XcfaAasporCoiLts(xcfa, ivr, ConeOfInfluence.lts) - else XcfaSporCoiLts(xcfa, ConeOfInfluence.lts) - }) - ; + NO_COI({ xcfa, ivr, por -> por.getLts(xcfa, ivr).also { NO_COI.porLts = it } }), + COI({ xcfa, ivr, por -> + ConeOfInfluence.coreLts = por.getLts(xcfa, ivr).also { COI.porLts = it } + ConeOfInfluence.lts + }), + POR_COI({ xcfa, ivr, por -> + ConeOfInfluence.coreLts = getXcfaLts() + if (por.isAbstractionAware) XcfaAasporCoiLts(xcfa, ivr, ConeOfInfluence.lts) + else XcfaSporCoiLts(xcfa, ConeOfInfluence.lts) + }), + POR_COI_POR({ xcfa, ivr, por -> + ConeOfInfluence.coreLts = por.getLts(xcfa, ivr).also { POR_COI_POR.porLts = it } + if (por.isAbstractionAware) XcfaAasporCoiLts(xcfa, ivr, ConeOfInfluence.lts) + else XcfaSporCoiLts(xcfa, ConeOfInfluence.lts) + }); - var porLts: LTS>, XcfaAction>? = null + var porLts: LTS>, XcfaAction>? = null } // TODO CexMonitor: disable for multi_seq // TODO add new monitor to xsts cli enum class CexMonitorOptions { - CHECK, - DISABLE + CHECK, + DISABLE, } diff --git a/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/config/XstsConfigBuilder.java b/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/config/XstsConfigBuilder.java index 35b38b2a27..016d828fcb 100644 --- a/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/config/XstsConfigBuilder.java +++ b/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/config/XstsConfigBuilder.java @@ -13,18 +13,20 @@ * See the License for the specific language governing permissions and * limitations under the License. */ - package hu.bme.mit.theta.xsts.analysis.config; +import static com.google.common.base.Preconditions.checkState; +import static hu.bme.mit.theta.core.type.booltype.BoolExprs.Not; + import hu.bme.mit.theta.analysis.*; +import hu.bme.mit.theta.analysis.algorithm.SafetyChecker; 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.Abstractor; -import hu.bme.mit.theta.analysis.algorithm.cegar.BasicAbstractor; -import hu.bme.mit.theta.analysis.algorithm.cegar.CegarChecker; -import hu.bme.mit.theta.analysis.algorithm.cegar.Refiner; +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; +import hu.bme.mit.theta.analysis.algorithm.cegar.BasicArgAbstractor; import hu.bme.mit.theta.analysis.algorithm.cegar.abstractor.StopCriterion; import hu.bme.mit.theta.analysis.algorithm.cegar.abstractor.StopCriterions; import hu.bme.mit.theta.analysis.expl.*; @@ -60,16 +62,12 @@ import hu.bme.mit.theta.xsts.analysis.initprec.*; import hu.bme.mit.theta.xsts.analysis.util.XstsCombineExtractUtilsKt; import hu.bme.mit.theta.xsts.analysis.util.XstsControlInitFuncKt; - import java.util.HashSet; import java.util.List; import java.util.Set; import java.util.function.Function; import java.util.function.Predicate; -import static com.google.common.base.Preconditions.checkState; -import static hu.bme.mit.theta.core.type.booltype.BoolExprs.Not; - public class XstsConfigBuilder { //////////// CEGAR configuration //////////// @@ -94,20 +92,26 @@ public enum Domain { public enum Refinement { FW_BIN_ITP { @Override - public ExprTraceChecker getItpExprTraceChecker(Expr init, Expr target, ItpSolver solver) { + public ExprTraceChecker getItpExprTraceChecker( + Expr init, Expr target, ItpSolver solver) { return ExprTraceFwBinItpChecker.create(init, target, solver); } - }, BW_BIN_ITP { + }, + BW_BIN_ITP { @Override - public ExprTraceChecker getItpExprTraceChecker(Expr init, Expr target, ItpSolver solver) { + public ExprTraceChecker getItpExprTraceChecker( + Expr init, Expr target, ItpSolver solver) { return ExprTraceBwBinItpChecker.create(init, target, solver); } - }, SEQ_ITP { + }, + SEQ_ITP { @Override - public ExprTraceChecker getItpExprTraceChecker(Expr init, Expr target, ItpSolver solver) { + public ExprTraceChecker getItpExprTraceChecker( + Expr init, Expr target, ItpSolver solver) { return ExprTraceSeqItpChecker.create(init, target, solver); } - }, UNSAT_CORE, + }, + UNSAT_CORE, MULTI_SEQ { @Override public StopCriterion getStopCriterion() { @@ -115,19 +119,20 @@ public StopCriterion getStopCriterion() { } @Override - public ExprTraceChecker getItpExprTraceChecker(Expr init, Expr target, ItpSolver solver) { + public ExprTraceChecker getItpExprTraceChecker( + Expr init, Expr target, ItpSolver solver) { return ExprTraceSeqItpChecker.create(init, target, solver); } @Override - public Refiner, XstsAction, P> - createRefiner( - ExprTraceChecker traceChecker, - RefutationToPrec refToPrec, - PruneStrategy pruneStrategy, - Logger logger - ) { - return MultiExprTraceRefiner.create(traceChecker, JoiningPrecRefiner.create(refToPrec), pruneStrategy, logger); + public + ArgRefiner, XstsAction, P> createRefiner( + ExprTraceChecker traceChecker, + RefutationToPrec refToPrec, + PruneStrategy pruneStrategy, + Logger logger) { + return MultiExprTraceRefiner.create( + traceChecker, JoiningPrecRefiner.create(refToPrec), pruneStrategy, logger); } }; @@ -136,23 +141,22 @@ public StopCriterion getStopCriterion() { } public ExprTraceChecker getItpExprTraceChecker( - final Expr init, - final Expr target, - final ItpSolver solver - ) { - throw new UnsupportedOperationException(String.format("%s domain can't provide trace checker of ItpRefutation", this.getClass().getSimpleName())); + final Expr init, final Expr target, final ItpSolver solver) { + throw new UnsupportedOperationException( + String.format( + "%s domain can't provide trace checker of ItpRefutation", + this.getClass().getSimpleName())); + } + + public + ArgRefiner, XstsAction, P> createRefiner( + ExprTraceChecker traceChecker, + RefutationToPrec refToPrec, + PruneStrategy pruneStrategy, + Logger logger) { + return SingleExprTraceRefiner.create( + traceChecker, JoiningPrecRefiner.create(refToPrec), pruneStrategy, logger); } - - public Refiner, XstsAction, P> - createRefiner( - ExprTraceChecker traceChecker, - RefutationToPrec refToPrec, - PruneStrategy pruneStrategy, - Logger logger - ) { - return SingleExprTraceRefiner.create(traceChecker, JoiningPrecRefiner.create(refToPrec), pruneStrategy, logger); - } - } public enum Search { @@ -165,7 +169,6 @@ public enum Search { Search(final ArgNodeComparators.ArgNodeComparator comparator) { this.comparator = comparator; } - } public enum PredSplit { @@ -196,7 +199,6 @@ public enum InitPrec { InitPrec(final XstsInitPrec builder) { this.builder = builder; } - } public enum AutoExpl { @@ -214,7 +216,8 @@ public enum AutoExpl { } public enum OptimizeStmts { - ON, OFF + ON, + OFF } private Logger logger = NullLogger.getInstance(); @@ -230,8 +233,11 @@ public enum OptimizeStmts { private OptimizeStmts optimizeStmts = OptimizeStmts.ON; private AutoExpl autoExpl = AutoExpl.NEWOPERANDS; - public XstsConfigBuilder(final Domain domain, final Refinement refinement, - final SolverFactory abstractionSolverFactory, final SolverFactory refinementSolverFactory) { + public XstsConfigBuilder( + final Domain domain, + final Refinement refinement, + final SolverFactory abstractionSolverFactory, + final SolverFactory refinementSolverFactory) { this.domain = domain; this.refinement = refinement; this.abstractionSolverFactory = abstractionSolverFactory; @@ -282,12 +288,15 @@ public XstsConfigBuilder autoExpl(final AutoExpl autoExpl) { if (domain == Domain.EXPL) { return (new ExplStrategy(xsts)).buildConfig(); } - if (domain == Domain.PRED_BOOL || domain == Domain.PRED_CART + if (domain == Domain.PRED_BOOL + || domain == Domain.PRED_CART || domain == Domain.PRED_SPLIT) { return (new PredStrategy(xsts)).buildConfig(); } - if (domain == Domain.EXPL_PRED_BOOL || domain == Domain.EXPL_PRED_CART - || domain == Domain.EXPL_PRED_SPLIT || domain == Domain.EXPL_PRED_COMBINED) { + if (domain == Domain.EXPL_PRED_BOOL + || domain == Domain.EXPL_PRED_CART + || domain == Domain.EXPL_PRED_SPLIT + || domain == Domain.EXPL_PRED_COMBINED) { return (new ProdStrategy(xsts)).buildConfig(); } throw new UnsupportedOperationException(domain + " domain is not supported."); @@ -295,15 +304,26 @@ public XstsConfigBuilder autoExpl(final AutoExpl autoExpl) { public abstract class BuilderStrategy { - protected static final String UNSUPPORTED_CONFIG_VALUE = "Builder strategy %s does not support configuration value %s as %s"; + protected static final String UNSUPPORTED_CONFIG_VALUE = + "Builder strategy %s does not support configuration value %s as %s"; protected final XSTS xsts; protected final Solver abstractionSolver; protected final Expr negProp; @SuppressWarnings("java:S1699") protected BuilderStrategy(XSTS xsts) { - checkState(getSupportedDomains().contains(domain), UNSUPPORTED_CONFIG_VALUE, getClass().getSimpleName(), domain, "domain"); - checkState(getSupportedRefinements().contains(refinement), UNSUPPORTED_CONFIG_VALUE, getClass().getSimpleName(), refinement, "refinement"); + checkState( + getSupportedDomains().contains(domain), + UNSUPPORTED_CONFIG_VALUE, + getClass().getSimpleName(), + domain, + "domain"); + checkState( + getSupportedRefinements().contains(refinement), + UNSUPPORTED_CONFIG_VALUE, + getClass().getSimpleName(), + refinement, + "refinement"); this.xsts = xsts; abstractionSolver = abstractionSolverFactory.createSolver(); negProp = Not(xsts.getProp()); @@ -336,7 +356,7 @@ public XstsAnalysis getAnalysis() { public abstract RefutationToPrec getItpRefToPrec(); - public Refiner, XstsAction, P> getRefiner() { + public ArgRefiner, XstsAction, P> getRefiner() { return refinement.createRefiner( refinement.getItpExprTraceChecker( xsts.getInitFormula(), @@ -353,22 +373,22 @@ XstsConfig, XstsAction, P> buildConfig() { final LTS, XstsAction> lts = getLts(); final Predicate> target = getPredicate(); final Analysis, XstsAction, P> analysis = getAnalysis(); - final ArgBuilder, XstsAction, P> argBuilder = ArgBuilder.create( - lts, analysis, target, - true); - final Abstractor, XstsAction, P> abstractor = BasicAbstractor.builder( - argBuilder) - .waitlist(PriorityWaitlist.create(search.comparator)) - .stopCriterion(refinement.getStopCriterion()) - .logger(logger).build(); - final Refiner, XstsAction, P> refiner = getRefiner(); - final SafetyChecker, XstsAction>, Trace, XstsAction>, P> checker = CegarChecker.create( - abstractor, refiner, - logger); + final ArgBuilder, XstsAction, P> argBuilder = + ArgBuilder.create(lts, analysis, target, true); + final ArgAbstractor, XstsAction, P> abstractor = + BasicArgAbstractor.builder(argBuilder) + .waitlist(PriorityWaitlist.create(search.comparator)) + .stopCriterion(refinement.getStopCriterion()) + .logger(logger) + .build(); + final ArgRefiner, XstsAction, P> refiner = getRefiner(); + final SafetyChecker, XstsAction>, Trace, XstsAction>, P> + checker = ArgCegarChecker.create(abstractor, refiner, logger); return XstsConfig.create(checker, getInitPrec()); } - public MultiAnalysisSide, S, XstsState, XstsAction, P, UnitPrec> getMultiSide() { + public MultiAnalysisSide, S, XstsState, XstsAction, P, UnitPrec> + getMultiSide() { return new MultiAnalysisSide<>( getAnalysis(), XstsControlInitFuncKt.xstsControlInitFunc(), @@ -377,7 +397,6 @@ public MultiAnalysisSide, S, XstsState, XstsAction, P, U XstsCombineExtractUtilsKt::xstsExtractDataState, XstsCombineExtractUtilsKt::xstsExtractControlPrec); } - } public class ExplStrategy extends BuilderStrategy { @@ -394,8 +413,12 @@ Set getSupportedRefinements() { public ExplStrategy(XSTS xsts) { super(xsts); - checkState(domain == Domain.EXPL, - UNSUPPORTED_CONFIG_VALUE, this.getClass().getSimpleName(), domain, "domain"); + checkState( + domain == Domain.EXPL, + UNSUPPORTED_CONFIG_VALUE, + this.getClass().getSimpleName(), + domain, + "domain"); } @Override @@ -419,12 +442,16 @@ public RefutationToPrec getItpRefToPrec() { } @Override - public Refiner, XstsAction, ExplPrec> getRefiner() { + public ArgRefiner, XstsAction, ExplPrec> getRefiner() { if (refinement == Refinement.UNSAT_CORE) { return SingleExprTraceRefiner.create( - ExprTraceUnsatCoreChecker.create(xsts.getInitFormula(), negProp, + ExprTraceUnsatCoreChecker.create( + xsts.getInitFormula(), + negProp, refinementSolverFactory.createUCSolver()), - JoiningPrecRefiner.create(new VarsRefToExplPrec()), pruneStrategy, logger); + JoiningPrecRefiner.create(new VarsRefToExplPrec()), + pruneStrategy, + logger); } return super.getRefiner(); } @@ -433,7 +460,6 @@ public Refiner, XstsAction, ExplPrec> getRefiner() { public ExplPrec getInitPrec() { return initPrec.builder.createExpl(xsts); } - } public class PredStrategy extends BuilderStrategy { @@ -444,13 +470,24 @@ Set getSupportedDomains() { @Override Set getSupportedRefinements() { - return new HashSet<>(List.of(Refinement.FW_BIN_ITP, Refinement.BW_BIN_ITP, Refinement.SEQ_ITP, Refinement.MULTI_SEQ)); + return new HashSet<>( + List.of( + Refinement.FW_BIN_ITP, + Refinement.BW_BIN_ITP, + Refinement.SEQ_ITP, + Refinement.MULTI_SEQ)); } public PredStrategy(XSTS xsts) { super(xsts); - checkState(domain == Domain.PRED_BOOL || domain == Domain.PRED_SPLIT || domain == Domain.PRED_CART, - UNSUPPORTED_CONFIG_VALUE, this.getClass().getSimpleName(), domain, "domain"); + checkState( + domain == Domain.PRED_BOOL + || domain == Domain.PRED_SPLIT + || domain == Domain.PRED_CART, + UNSUPPORTED_CONFIG_VALUE, + this.getClass().getSimpleName(), + domain, + "domain"); } @Override @@ -482,55 +519,80 @@ public PredPrec getInitPrec() { } } - public class ProdStrategy extends BuilderStrategy, Prod2Prec> { + public class ProdStrategy + extends BuilderStrategy< + Prod2State, Prod2Prec> { @Override Set getSupportedDomains() { - return new HashSet<>(List.of(Domain.EXPL_PRED_BOOL, Domain.EXPL_PRED_CART, Domain.EXPL_PRED_SPLIT, Domain.EXPL_PRED_COMBINED)); + return new HashSet<>( + List.of( + Domain.EXPL_PRED_BOOL, + Domain.EXPL_PRED_CART, + Domain.EXPL_PRED_SPLIT, + Domain.EXPL_PRED_COMBINED)); } @Override Set getSupportedRefinements() { - return new HashSet<>(List.of(Refinement.FW_BIN_ITP, Refinement.BW_BIN_ITP, Refinement.SEQ_ITP, Refinement.MULTI_SEQ)); + return new HashSet<>( + List.of( + Refinement.FW_BIN_ITP, + Refinement.BW_BIN_ITP, + Refinement.SEQ_ITP, + Refinement.MULTI_SEQ)); } public ProdStrategy(XSTS xsts) { super(xsts); - checkState(domain == Domain.EXPL_PRED_BOOL || domain == Domain.EXPL_PRED_SPLIT - || domain == Domain.EXPL_PRED_CART || domain == Domain.EXPL_PRED_COMBINED, - UNSUPPORTED_CONFIG_VALUE, this.getClass().getSimpleName(), domain, "domain"); - checkState(refinement != Refinement.UNSAT_CORE, UNSUPPORTED_CONFIG_VALUE, getClass().getSimpleName(), refinement, "refinement"); + checkState( + domain == Domain.EXPL_PRED_BOOL + || domain == Domain.EXPL_PRED_SPLIT + || domain == Domain.EXPL_PRED_CART + || domain == Domain.EXPL_PRED_COMBINED, + UNSUPPORTED_CONFIG_VALUE, + this.getClass().getSimpleName(), + domain, + "domain"); + checkState( + refinement != Refinement.UNSAT_CORE, + UNSUPPORTED_CONFIG_VALUE, + getClass().getSimpleName(), + refinement, + "refinement"); } @Override StmtOptimizer> getLtsOptimizer() { - return Prod2ExplPredStmtOptimizer.create( - ExplStmtOptimizer.getInstance() - ); + return Prod2ExplPredStmtOptimizer.create(ExplStmtOptimizer.getInstance()); } @Override public Predicate>> getPredicate() { - return new XstsStatePredicate<>( - new ExprStatePredicate(negProp, abstractionSolver)); + return new XstsStatePredicate<>(new ExprStatePredicate(negProp, abstractionSolver)); } @Override - public Analysis, StmtAction, Prod2Prec> getDataAnalysis() { - if (domain == Domain.EXPL_PRED_BOOL || domain == Domain.EXPL_PRED_CART + public Analysis, StmtAction, Prod2Prec> + getDataAnalysis() { + if (domain == Domain.EXPL_PRED_BOOL + || domain == Domain.EXPL_PRED_CART || domain == Domain.EXPL_PRED_SPLIT) { - final PredAbstractors.PredAbstractor predAbstractor = domain.predAbstractorFunction.apply(abstractionSolver); + final PredAbstractors.PredAbstractor predAbstractor = + domain.predAbstractorFunction.apply(abstractionSolver); return Prod2Analysis.create( ExplStmtAnalysis.create(abstractionSolver, xsts.getInitFormula(), maxEnum), - PredAnalysis.create(abstractionSolver, predAbstractor, xsts.getInitFormula()), + PredAnalysis.create( + abstractionSolver, predAbstractor, xsts.getInitFormula()), Prod2ExplPredPreStrengtheningOperator.create(), Prod2ExplPredStrengtheningOperator.create(abstractionSolver)); } else { - final Prod2ExplPredAbstractors.Prod2ExplPredAbstractor prodAbstractor = Prod2ExplPredAbstractors.booleanAbstractor( - abstractionSolver); + final Prod2ExplPredAbstractors.Prod2ExplPredAbstractor prodAbstractor = + Prod2ExplPredAbstractors.booleanAbstractor(abstractionSolver); return Prod2ExplPredAnalysis.create( ExplAnalysis.create(abstractionSolver, xsts.getInitFormula()), - PredAnalysis.create(abstractionSolver, + PredAnalysis.create( + abstractionSolver, PredAbstractors.booleanAbstractor(abstractionSolver), xsts.getInitFormula()), Prod2ExplPredStrengtheningOperator.create(abstractionSolver), @@ -548,7 +610,5 @@ public RefutationToPrec, ItpRefutation> getItpRefT public Prod2Prec getInitPrec() { return initPrec.builder.createProd2ExplPred(xsts); } - } - -} \ No newline at end of file +} 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 592abd7ad5..6bbc845a97 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 @@ -31,8 +31,8 @@ import hu.bme.mit.theta.analysis.LTS; 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.cegar.Abstractor; -import hu.bme.mit.theta.analysis.algorithm.cegar.BasicAbstractor; +import hu.bme.mit.theta.analysis.algorithm.cegar.ArgAbstractor; +import hu.bme.mit.theta.analysis.algorithm.cegar.BasicArgAbstractor; import hu.bme.mit.theta.analysis.unit.UnitAnalysis; import hu.bme.mit.theta.analysis.unit.UnitPrec; import hu.bme.mit.theta.analysis.unit.UnitState; @@ -79,11 +79,11 @@ public void test() throws FileNotFoundException, IOException { lts, analysis, s -> false); - final Abstractor, XtaAction, UnitPrec> abstractor = BasicAbstractor.builder( + final ArgAbstractor, XtaAction, UnitPrec> abstractor = BasicArgAbstractor.builder( argBuilder) .projection(s -> s.getLocs()).build(); - final ARG, XtaAction> arg = abstractor.createArg(); + final ARG, XtaAction> arg = abstractor.createWitness(); abstractor.check(arg, UnitPrec.getInstance()); System.out.println( 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 437049b128..111e451934 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 @@ -32,8 +32,8 @@ import hu.bme.mit.theta.analysis.LTS; 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.cegar.Abstractor; -import hu.bme.mit.theta.analysis.algorithm.cegar.BasicAbstractor; +import hu.bme.mit.theta.analysis.algorithm.cegar.ArgAbstractor; +import hu.bme.mit.theta.analysis.algorithm.cegar.BasicArgAbstractor; import hu.bme.mit.theta.analysis.expl.ExplState; import hu.bme.mit.theta.analysis.impl.PrecMappingAnalysis; import hu.bme.mit.theta.analysis.prod2.Prod2Analysis; @@ -91,10 +91,10 @@ public void test() throws FileNotFoundException, IOException { final ArgBuilder>, XtaAction, ZonePrec> argBuilder = ArgBuilder .create(lts, analysis, s -> false); - final Abstractor>, XtaAction, ZonePrec> abstractor = BasicAbstractor + final ArgAbstractor>, XtaAction, ZonePrec> abstractor = BasicArgAbstractor .builder(argBuilder).projection(s -> s.getLocs()).build(); - final ARG>, XtaAction> arg = abstractor.createArg(); + final ARG>, XtaAction> arg = abstractor.createWitness(); abstractor.check(arg, prec); System.out.println(arg.getNodes().collect(Collectors.toSet()));