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 index 06260c732c..8ac9d3a5a7 100644 --- 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 @@ -25,24 +25,25 @@ 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. + * 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() { - } + private ArgCegarChecker() {} - public static CegarChecker, Trace> create( - final ArgAbstractor abstractor, final ArgRefiner refiner) { + 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) { + 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 index 2683a2fd0f..afb07b11c7 100644 --- 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 @@ -25,5 +25,5 @@ * 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> { -} +public interface ArgRefiner + extends Refiner, Trace> {} 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 30da9a28e5..dac497e043 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 @@ -15,11 +15,11 @@ */ package hu.bme.mit.theta.analysis.algorithm.cegar; +import static com.google.common.base.Preconditions.checkNotNull; + 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.algorithm.Proof; import hu.bme.mit.theta.analysis.algorithm.SafetyChecker; import hu.bme.mit.theta.analysis.algorithm.SafetyResult; @@ -31,26 +31,27 @@ 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; - import java.util.concurrent.TimeUnit; -import static com.google.common.base.Preconditions.checkNotNull; - /** - * 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. + * 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 CegarChecker implements SafetyChecker { +public final class CegarChecker

+ implements SafetyChecker { private final Abstractor abstractor; - private final Refiner refiner; + private final Refiner refiner; private final Logger logger; private final Pr proof; private final ProofVisualizer proofVisualizer; - private CegarChecker(final Abstractor abstractor, final Refiner refiner, final Logger logger, final ProofVisualizer proofVisualizer) { + private CegarChecker( + final Abstractor abstractor, + final Refiner refiner, + final Logger logger, + final ProofVisualizer proofVisualizer) { this.abstractor = checkNotNull(abstractor); this.refiner = checkNotNull(refiner); this.logger = checkNotNull(logger); @@ -58,13 +59,18 @@ private CegarChecker(final Abstractor abstractor, final Refiner CegarChecker create( - final Abstractor abstractor, final Refiner refiner, final ProofVisualizer proofVisualizer) { + public static

CegarChecker create( + final Abstractor abstractor, + final Refiner refiner, + final ProofVisualizer proofVisualizer) { return create(abstractor, refiner, NullLogger.getInstance(), proofVisualizer); } - public static CegarChecker create( - final Abstractor abstractor, final Refiner refiner, final Logger logger, final ProofVisualizer proofVisualizer) { + public static

CegarChecker create( + final Abstractor abstractor, + final Refiner refiner, + final Logger logger, + final ProofVisualizer proofVisualizer) { return new CegarChecker<>(abstractor, refiner, logger, proofVisualizer); } @@ -78,7 +84,7 @@ public SafetyResult check(final P initPrec) { final Stopwatch stopwatch = Stopwatch.createStarted(); long abstractorTime = 0; long refinerTime = 0; - RefinerResult refinerResult = null; + RefinerResult refinerResult = null; AbstractorResult abstractorResult; P prec = initPrec; int iteration = 0; @@ -91,10 +97,12 @@ public SafetyResult check(final P initPrec) { final long abstractorStartTime = stopwatch.elapsed(TimeUnit.MILLISECONDS); abstractorResult = abstractor.check(proof, prec); abstractorTime += stopwatch.elapsed(TimeUnit.MILLISECONDS) - abstractorStartTime; - logger.write(Level.MAINSTEP, "| Checking abstraction done, result: %s%n", abstractorResult); + logger.write( + Level.MAINSTEP, "| Checking abstraction done, result: %s%n", abstractorResult); if (WebDebuggerLogger.enabled()) { - String argGraph = JSONWriter.getInstance().writeString(proofVisualizer.visualize(proof)); + String argGraph = + JSONWriter.getInstance().writeString(proofVisualizer.visualize(proof)); String precString = prec.toString(); wdl.addIteration(iteration, argGraph, precString); } @@ -107,26 +115,35 @@ public SafetyResult check(final P initPrec) { final long refinerStartTime = stopwatch.elapsed(TimeUnit.MILLISECONDS); refinerResult = refiner.refine(proof, prec); refinerTime += stopwatch.elapsed(TimeUnit.MILLISECONDS) - refinerStartTime; - logger.write(Level.MAINSTEP, "Refining abstraction done, result: %s%n", refinerResult); + logger.write( + Level.MAINSTEP, "Refining abstraction done, result: %s%n", refinerResult); if (refinerResult.isSpurious()) { prec = refinerResult.asSpurious().getRefinedPrec(); } if (lastPrec.equals(prec)) { - logger.write(Level.MAINSTEP, "! Precision did NOT change in this iteration" + System.lineSeparator()); + logger.write( + Level.MAINSTEP, + "! Precision did NOT change in this iteration" + + System.lineSeparator()); } else { - logger.write(Level.MAINSTEP, "! Precision DID change in this iteration" + System.lineSeparator()); + logger.write( + Level.MAINSTEP, + "! Precision DID change in this iteration" + System.lineSeparator()); } - } } while (!abstractorResult.isSafe() && !refinerResult.isUnsafe()); stopwatch.stop(); SafetyResult cegarResult = null; - final CegarStatistics stats = new CegarStatistics(stopwatch.elapsed(TimeUnit.MILLISECONDS), abstractorTime, - refinerTime, iteration); + final CegarStatistics stats = + new CegarStatistics( + stopwatch.elapsed(TimeUnit.MILLISECONDS), + abstractorTime, + refinerTime, + iteration); assert abstractorResult.isSafe() || refinerResult.isUnsafe(); @@ -144,6 +161,9 @@ public SafetyResult check(final P initPrec) { @Override public String toString() { - return Utils.lispStringBuilder(getClass().getSimpleName()).add(abstractor).add(refiner).toString(); + return Utils.lispStringBuilder(getClass().getSimpleName()) + .add(abstractor) + .add(refiner) + .toString(); } } 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 abd645f3cf..819bd3c403 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 @@ -15,20 +15,16 @@ */ 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.Proof; /** - * Common interface for refiners. It takes a witness and a precision, checks if the counterexample in - * the witness is feasible and if not, it refines the precision + * Common interface for refiners. It takes a witness and a precision, checks if the counterexample + * in the witness is feasible and if not, it refines the precision */ -public interface Refiner { +public interface Refiner

{ - /** - * Checks if the counterexample in the witness is feasible. If not, refines the precision - */ - RefinerResult refine(Pr witness, P prec); + /** Checks if the counterexample in the witness is feasible. If not, refines the precision */ + RefinerResult refine(Pr 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 a4be30781e..63011b7d08 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,26 @@ */ package hu.bme.mit.theta.analysis.algorithm.cegar; -import hu.bme.mit.theta.analysis.Action; +import static com.google.common.base.Preconditions.checkNotNull; + 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.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

{ - protected RefinerResult() { - } + protected RefinerResult() {} /** * Create a new spurious result. * * @param refinedPrec Refined precision */ - public static Spurious spurious( - final P refinedPrec) { + public static

Spurious spurious(final P refinedPrec) { return new Spurious<>(refinedPrec); } @@ -47,8 +43,7 @@ public static * * @param cex Feasible counterexample */ - public static Unsafe unsafe( - final C cex) { + public static

Unsafe unsafe(final C cex) { return new Unsafe<>(cex); } @@ -56,15 +51,12 @@ public static public abstract boolean isUnsafe(); - public abstract Spurious 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 { + /** Represents the spurious result with a refined precision. */ + public static final class Spurious

extends RefinerResult { private final P refinedPrec; @@ -87,14 +79,16 @@ 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 " + "Cannot cast " + + Spurious.class.getSimpleName() + + " to " + Unsafe.class.getSimpleName()); } @@ -106,11 +100,8 @@ public String toString() { } } - /** - * Represents the unsafe result with a feasible counterexample. - */ - public static final class Unsafe extends - RefinerResult { + /** Represents the unsafe result with a feasible counterexample. */ + public static final class Unsafe

extends RefinerResult { private final C cex; @@ -133,14 +124,16 @@ public boolean isUnsafe() { } @Override - public Spurious asSpurious() { + public Spurious asSpurious() { throw new ClassCastException( - "Cannot cast " + Unsafe.class.getSimpleName() + " to " + "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 f1f7430241..69b184e8b6 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 @@ -24,13 +24,13 @@ import hu.bme.mit.theta.analysis.expr.ExprAction; import hu.bme.mit.theta.analysis.expr.ExprState; import hu.bme.mit.theta.core.decl.VarDecl; - import java.util.HashSet; import java.util.Map; import java.util.Set; import java.util.stream.Collectors; -public final class AasporRefiner implements ArgRefiner { +public final class AasporRefiner + implements ArgRefiner { private final ArgRefiner refiner; @@ -38,38 +38,51 @@ public final class AasporRefiner, Set> ignoredVarRegistry; - private AasporRefiner(final ArgRefiner refiner, - final PruneStrategy pruneStrategy, - final Map, Set> ignoredVarRegistry) { + private AasporRefiner( + final ArgRefiner refiner, + final PruneStrategy pruneStrategy, + final Map, Set> ignoredVarRegistry) { this.refiner = refiner; this.pruneStrategy = pruneStrategy; this.ignoredVarRegistry = ignoredVarRegistry; } - public static AasporRefiner create( - final ArgRefiner refiner, final PruneStrategy pruneStrategy, - final Map, Set> ignoredVarRegistry) { + public static + AasporRefiner create( + 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(); final Set> newlyAddedVars = new HashSet<>(newPrec.getUsedVars()); newlyAddedVars.removeAll(prec.getUsedVars()); - newlyAddedVars.forEach(newVar -> { - if (ignoredVarRegistry.containsKey(newVar)) { - Set> nodesToReExpand = ignoredVarRegistry.get(newVar).stream().flatMap(stateToPrune -> - arg.getNodes().filter(node -> node.getState().equals(stateToPrune)) // TODO one state can be in one ARG node? - ).collect(Collectors.toSet()); - nodesToReExpand.forEach(arg::markForReExpansion); - ignoredVarRegistry.remove(newVar); - } - }); + newlyAddedVars.forEach( + newVar -> { + if (ignoredVarRegistry.containsKey(newVar)) { + Set> nodesToReExpand = + ignoredVarRegistry.get(newVar).stream() + .flatMap( + stateToPrune -> + arg.getNodes() + .filter( + node -> + node.getState() + .equals( + stateToPrune)) // TODO one state can be in one ARG node? + ) + .collect(Collectors.toSet()); + nodesToReExpand.forEach(arg::markForReExpansion); + ignoredVarRegistry.remove(newVar); + } + }); return result; } 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 b2cee796d0..71b8799468 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 @@ -15,6 +15,8 @@ */ package hu.bme.mit.theta.analysis.expr.refinement; +import static com.google.common.base.Preconditions.checkNotNull; + import hu.bme.mit.theta.analysis.Prec; import hu.bme.mit.theta.analysis.Trace; import hu.bme.mit.theta.analysis.algorithm.arg.ARG; @@ -26,14 +28,11 @@ import hu.bme.mit.theta.analysis.expr.ExprState; import hu.bme.mit.theta.common.logging.Logger; import hu.bme.mit.theta.common.logging.Logger.Level; - import java.util.ArrayList; import java.util.List; -import java.util.stream.Collectors; -import static com.google.common.base.Preconditions.checkNotNull; - -public final class MultiExprTraceRefiner +public final class MultiExprTraceRefiner< + S extends ExprState, A extends ExprAction, P extends Prec, R extends Refutation> implements ArgRefiner { private final ExprTraceChecker exprTraceChecker; @@ -42,9 +41,11 @@ public final class MultiExprTraceRefiner nodePruner; private final Logger logger; - private MultiExprTraceRefiner(final ExprTraceChecker exprTraceChecker, - final PrecRefiner precRefiner, - final PruneStrategy pruneStrategy, final Logger logger) { + private MultiExprTraceRefiner( + final ExprTraceChecker exprTraceChecker, + final PrecRefiner precRefiner, + final PruneStrategy pruneStrategy, + final Logger logger) { this.exprTraceChecker = checkNotNull(exprTraceChecker); this.precRefiner = checkNotNull(precRefiner); this.pruneStrategy = checkNotNull(pruneStrategy); @@ -52,10 +53,12 @@ private MultiExprTraceRefiner(final ExprTraceChecker exprTraceChecker, this.logger = checkNotNull(logger); } - private MultiExprTraceRefiner(final ExprTraceChecker exprTraceChecker, - final PrecRefiner precRefiner, - final PruneStrategy pruneStrategy, final Logger logger, - final NodePruner nodePruner) { + private MultiExprTraceRefiner( + final ExprTraceChecker exprTraceChecker, + final PrecRefiner precRefiner, + final PruneStrategy pruneStrategy, + final Logger logger, + final NodePruner nodePruner) { this.exprTraceChecker = checkNotNull(exprTraceChecker); this.precRefiner = checkNotNull(precRefiner); this.pruneStrategy = checkNotNull(pruneStrategy); @@ -63,20 +66,28 @@ private MultiExprTraceRefiner(final ExprTraceChecker exprTraceChecker, this.logger = checkNotNull(logger); } - public static MultiExprTraceRefiner create( - final ExprTraceChecker exprTraceChecker, final PrecRefiner precRefiner, - final PruneStrategy pruneStrategy, final Logger logger) { + public static + MultiExprTraceRefiner create( + final ExprTraceChecker exprTraceChecker, + final PrecRefiner precRefiner, + final PruneStrategy pruneStrategy, + final Logger logger) { return new MultiExprTraceRefiner<>(exprTraceChecker, precRefiner, pruneStrategy, logger); } - public static MultiExprTraceRefiner create( - final ExprTraceChecker exprTraceChecker, final PrecRefiner precRefiner, - final PruneStrategy pruneStrategy, final Logger logger, final NodePruner nodePruner) { - return new MultiExprTraceRefiner<>(exprTraceChecker, precRefiner, pruneStrategy, logger, nodePruner); + public static + MultiExprTraceRefiner create( + final ExprTraceChecker exprTraceChecker, + final PrecRefiner precRefiner, + final PruneStrategy pruneStrategy, + final Logger logger, + final NodePruner nodePruner) { + return new MultiExprTraceRefiner<>( + exprTraceChecker, precRefiner, pruneStrategy, logger, nodePruner); } @Override - public RefinerResult> 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"; @@ -100,13 +111,18 @@ public RefinerResult> refine(final ARG arg, final P p if (cexStatuses.stream().anyMatch(ExprTraceStatus::isFeasible)) { logger.write(Level.SUBSTEP, "done, result: found feasible%n"); - return RefinerResult.unsafe(traces.get( - cexStatuses.indexOf(cexStatuses.stream().filter(ExprTraceStatus::isFeasible).findFirst().get()))); + return RefinerResult.unsafe( + traces.get( + cexStatuses.indexOf( + cexStatuses.stream() + .filter(ExprTraceStatus::isFeasible) + .findFirst() + .get()))); } else { assert cexStatuses.size() == cexs.size(); logger.write(Level.SUBSTEP, "done, result: all infeasible%n"); - final List refutations = cexStatuses.stream().map(s -> s.asInfeasible().getRefutation()) - .toList(); + final List refutations = + cexStatuses.stream().map(s -> s.asInfeasible().getRefutation()).toList(); assert refutations.size() == cexs.size(); final List> nodesToPrune = new ArrayList<>(traces.size()); @@ -130,7 +146,8 @@ public RefinerResult> refine(final ARG arg, final P p P refinedPrec = prec; for (int i = 0; i < refutations.size(); ++i) { if (!skip.get(i)) { - refinedPrec = precRefiner.refine(refinedPrec, traces.get(i), refutations.get(i)); + refinedPrec = + precRefiner.refine(refinedPrec, traces.get(i), refutations.get(i)); } } @@ -153,7 +170,5 @@ public RefinerResult> refine(final ARG arg, final P p logger.write(Level.SUBSTEP, "done%n"); return RefinerResult.spurious(refinedPrec); } - } - -} \ No newline at end of file +} 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 126f4212f4..04befdbfcb 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 @@ -15,6 +15,8 @@ */ package hu.bme.mit.theta.analysis.expr.refinement; +import static com.google.common.base.Preconditions.checkNotNull; + import hu.bme.mit.theta.analysis.Prec; import hu.bme.mit.theta.analysis.Trace; import hu.bme.mit.theta.analysis.algorithm.arg.ARG; @@ -27,16 +29,14 @@ 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 java.util.Optional; -import static com.google.common.base.Preconditions.checkNotNull; - /** - * A Refiner implementation that can refine a single trace (of ExprStates and - * ExprActions) using an ExprTraceChecker and a PrecRefiner. + * A Refiner implementation that can refine a single trace (of ExprStates and ExprActions) using an + * ExprTraceChecker and a PrecRefiner. */ -public class SingleExprTraceRefiner +public class SingleExprTraceRefiner< + S extends ExprState, A extends ExprAction, P extends Prec, R extends Refutation> implements ArgRefiner { protected final ExprTraceChecker exprTraceChecker; protected final PrecRefiner precRefiner; @@ -44,9 +44,11 @@ public class SingleExprTraceRefiner nodePruner; protected final Logger logger; - protected SingleExprTraceRefiner(final ExprTraceChecker exprTraceChecker, - final PrecRefiner precRefiner, - final PruneStrategy pruneStrategy, final Logger logger) { + protected SingleExprTraceRefiner( + final ExprTraceChecker exprTraceChecker, + final PrecRefiner precRefiner, + final PruneStrategy pruneStrategy, + final Logger logger) { this.exprTraceChecker = checkNotNull(exprTraceChecker); this.precRefiner = checkNotNull(precRefiner); this.pruneStrategy = checkNotNull(pruneStrategy); @@ -54,10 +56,12 @@ protected SingleExprTraceRefiner(final ExprTraceChecker exprTraceChecker, this.logger = checkNotNull(logger); } - protected SingleExprTraceRefiner(final ExprTraceChecker exprTraceChecker, - final PrecRefiner precRefiner, - final PruneStrategy pruneStrategy, final Logger logger, - final NodePruner nodePruner) { + protected SingleExprTraceRefiner( + final ExprTraceChecker exprTraceChecker, + final PrecRefiner precRefiner, + final PruneStrategy pruneStrategy, + final Logger logger, + final NodePruner nodePruner) { this.exprTraceChecker = checkNotNull(exprTraceChecker); this.precRefiner = checkNotNull(precRefiner); this.pruneStrategy = checkNotNull(pruneStrategy); @@ -65,20 +69,28 @@ protected SingleExprTraceRefiner(final ExprTraceChecker exprTraceChecker, this.logger = checkNotNull(logger); } - public static SingleExprTraceRefiner create( - final ExprTraceChecker exprTraceChecker, final PrecRefiner precRefiner, - final PruneStrategy pruneStrategy, final Logger logger) { + public static + SingleExprTraceRefiner create( + final ExprTraceChecker exprTraceChecker, + final PrecRefiner precRefiner, + final PruneStrategy pruneStrategy, + final Logger logger) { return new SingleExprTraceRefiner<>(exprTraceChecker, precRefiner, pruneStrategy, logger); } - public static SingleExprTraceRefiner create( - final ExprTraceChecker exprTraceChecker, final PrecRefiner precRefiner, - final PruneStrategy pruneStrategy, final Logger logger, final NodePruner nodePruner) { - return new SingleExprTraceRefiner<>(exprTraceChecker, precRefiner, pruneStrategy, logger, nodePruner); + public static + SingleExprTraceRefiner create( + final ExprTraceChecker exprTraceChecker, + final PrecRefiner precRefiner, + final PruneStrategy pruneStrategy, + final Logger logger, + final NodePruner nodePruner) { + return new SingleExprTraceRefiner<>( + exprTraceChecker, precRefiner, pruneStrategy, logger, nodePruner); } @Override - public RefinerResult> 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"; @@ -127,7 +139,9 @@ public RefinerResult> refine(final ARG arg, final P p @Override public String toString() { - return Utils.lispStringBuilder(getClass().getSimpleName()).add(exprTraceChecker).add(precRefiner).toString(); + return Utils.lispStringBuilder(getClass().getSimpleName()) + .add(exprTraceChecker) + .add(precRefiner) + .toString(); } - } 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 93410e0641..4ca545dd9b 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 @@ -29,143 +29,168 @@ import hu.bme.mit.theta.analysis.ptr.patch import hu.bme.mit.theta.common.logging.Logger import java.util.* - class XcfaSingleExprTraceRefiner : - SingleExprTraceRefiner { - - private constructor( - exprTraceChecker: ExprTraceChecker, - precRefiner: PrecRefiner, - pruneStrategy: PruneStrategy, - logger: Logger - ) : super(exprTraceChecker, precRefiner, pruneStrategy, logger) - - private constructor( - exprTraceChecker: ExprTraceChecker, - precRefiner: PrecRefiner, - pruneStrategy: PruneStrategy, - logger: Logger, - nodePruner: NodePruner - ) : super(exprTraceChecker, precRefiner, pruneStrategy, logger, nodePruner) - - private fun findPoppedState(trace: Trace): Pair>? { - trace.states.forEachIndexed { i, s -> - val state = s as XcfaState - state.processes.entries.find { (_, processState) -> processState.popped != null } - ?.let { (pid, processState) -> - val stackBeforePop = LinkedList(processState.locs) - stackBeforePop.push(processState.popped) - val processesBeforePop = state.processes.toMutableMap() - processesBeforePop[pid] = processState.copy(locs = stackBeforePop) - val stateBeforePop = state.copy(processes = processesBeforePop) - return Pair(i, stateBeforePop) - } + SingleExprTraceRefiner { + + private constructor( + exprTraceChecker: ExprTraceChecker, + precRefiner: PrecRefiner, + pruneStrategy: PruneStrategy, + logger: Logger, + ) : super(exprTraceChecker, precRefiner, pruneStrategy, logger) + + private constructor( + exprTraceChecker: ExprTraceChecker, + precRefiner: PrecRefiner, + pruneStrategy: PruneStrategy, + logger: Logger, + nodePruner: NodePruner, + ) : super(exprTraceChecker, precRefiner, pruneStrategy, logger, nodePruner) + + private fun findPoppedState(trace: Trace): Pair>? { + trace.states.forEachIndexed { i, s -> + val state = s as XcfaState + state.processes.entries + .find { (_, processState) -> processState.popped != null } + ?.let { (pid, processState) -> + val stackBeforePop = LinkedList(processState.locs) + stackBeforePop.push(processState.popped) + val processesBeforePop = state.processes.toMutableMap() + processesBeforePop[pid] = processState.copy(locs = stackBeforePop) + val stateBeforePop = state.copy(processes = processesBeforePop) + return Pair(i, stateBeforePop) } - return null } - - fun refineTemp(arg: ARG, prec: P?): RefinerResult> { - Preconditions.checkNotNull(arg) - Preconditions.checkNotNull(prec) - assert(!arg.isSafe) { "ARG must be unsafe" } - val optionalNewCex = arg.cexs.findFirst() - val cexToConcretize = optionalNewCex.get() - val rawTrace = cexToConcretize.toTrace() - val (_, states, actions) = rawTrace.actions.foldIndexed( - Triple(Pair(emptyMap(), 0), listOf(rawTrace.getState(0)), - listOf())) { i: Int, (wTripleCnt: Pair, states: List, actions: List): Triple, List, List>, a: A -> - val (wTriple, cnt) = wTripleCnt - val newA = (a as XcfaAction).withLastWrites(wTriple, cnt) - val newState = (rawTrace.getState(i + 1) as XcfaState>).let { - it.withState(PtrState(it.sGlobal.innerState.patch(newA.nextWriteTriples()))) - } - Triple(Pair(newA.nextWriteTriples(), newA.cnts.values.maxOrNull() ?: newA.inCnt), states + (newState as S), - actions + (newA as A)) + return null + } + + fun refineTemp(arg: ARG, prec: P?): RefinerResult> { + Preconditions.checkNotNull(arg) + Preconditions.checkNotNull(prec) + assert(!arg.isSafe) { "ARG must be unsafe" } + val optionalNewCex = arg.cexs.findFirst() + val cexToConcretize = optionalNewCex.get() + val rawTrace = cexToConcretize.toTrace() + val (_, states, actions) = + rawTrace.actions.foldIndexed( + Triple(Pair(emptyMap(), 0), listOf(rawTrace.getState(0)), listOf()) + ) { + i: Int, + (wTripleCnt: Pair, states: List, actions: List): Triple< + Pair, + List, + List, + >, + a: A -> + val (wTriple, cnt) = wTripleCnt + val newA = (a as XcfaAction).withLastWrites(wTriple, cnt) + val newState = + (rawTrace.getState(i + 1) as XcfaState>).let { + it.withState(PtrState(it.sGlobal.innerState.patch(newA.nextWriteTriples()))) + } + Triple( + Pair(newA.nextWriteTriples(), newA.cnts.values.maxOrNull() ?: newA.inCnt), + states + (newState as S), + actions + (newA as A), + ) + } + val traceToConcretize = Trace.of(states, actions) + + logger.write(Logger.Level.INFO, "| | Trace length: %d%n", traceToConcretize.length()) + logger.write(Logger.Level.DETAIL, "| | Trace: %s%n", traceToConcretize) + logger.write(Logger.Level.SUBSTEP, "| | Checking trace...") + val cexStatus = exprTraceChecker.check(traceToConcretize) + logger.write(Logger.Level.SUBSTEP, "done, result: %s%n", cexStatus) + assert(cexStatus.isFeasible() || cexStatus.isInfeasible()) { "Unknown CEX status" } + return if (cexStatus.isFeasible()) { + RefinerResult.unsafe(traceToConcretize) + } else { + val refutation = cexStatus.asInfeasible().refutation + logger.write(Logger.Level.DETAIL, "| | | Refutation: %s%n", refutation) + val refinedPrec = precRefiner.refine(prec, traceToConcretize, refutation) + val pruneIndex = refutation.getPruneIndex() + assert(0 <= pruneIndex) { "Pruning index must be non-negative" } + assert(pruneIndex <= cexToConcretize.length()) { "Pruning index larger than cex length" } + when (pruneStrategy) { + PruneStrategy.LAZY -> { + logger.write(Logger.Level.SUBSTEP, "| | Pruning from index %d...", pruneIndex) + val nodeToPrune = cexToConcretize.node(pruneIndex) + nodePruner.prune(arg, nodeToPrune) } - val traceToConcretize = Trace.of(states, actions) - - logger.write(Logger.Level.INFO, "| | Trace length: %d%n", traceToConcretize.length()) - logger.write(Logger.Level.DETAIL, "| | Trace: %s%n", traceToConcretize) - logger.write(Logger.Level.SUBSTEP, "| | Checking trace...") - val cexStatus = exprTraceChecker.check(traceToConcretize) - logger.write(Logger.Level.SUBSTEP, "done, result: %s%n", cexStatus) - assert(cexStatus.isFeasible() || cexStatus.isInfeasible()) { "Unknown CEX status" } - return if (cexStatus.isFeasible()) { - RefinerResult.unsafe(traceToConcretize) - } else { - val refutation = cexStatus.asInfeasible().refutation - logger.write(Logger.Level.DETAIL, "| | | Refutation: %s%n", refutation) - val refinedPrec = precRefiner.refine(prec, traceToConcretize, refutation) - val pruneIndex = refutation.getPruneIndex() - assert(0 <= pruneIndex) { "Pruning index must be non-negative" } - assert(pruneIndex <= cexToConcretize.length()) { "Pruning index larger than cex length" } - when (pruneStrategy) { - PruneStrategy.LAZY -> { - logger.write(Logger.Level.SUBSTEP, "| | Pruning from index %d...", pruneIndex) - val nodeToPrune = cexToConcretize.node(pruneIndex) - nodePruner.prune(arg, nodeToPrune) - } - - PruneStrategy.FULL -> { - logger.write(Logger.Level.SUBSTEP, "| | Pruning whole ARG", pruneIndex) - arg.pruneAll() - } - - else -> throw java.lang.UnsupportedOperationException("Unsupported pruning strategy") - } - logger.write(Logger.Level.SUBSTEP, "done%n") - RefinerResult.spurious(refinedPrec) + + PruneStrategy.FULL -> { + logger.write(Logger.Level.SUBSTEP, "| | Pruning whole ARG", pruneIndex) + arg.pruneAll() } - } - override fun refine(arg: ARG, prec: P?): RefinerResult> { - Preconditions.checkNotNull(arg) - Preconditions.checkNotNull

(prec) - assert(!arg.isSafe) { "ARG must be unsafe" } - - val optionalNewCex = arg.cexs.findFirst() - val cexToConcretize = optionalNewCex.get() - val traceToConcretize = cexToConcretize.toTrace() - - val refinerResult = refineTemp(arg, prec) //super.refine(arg, prec) - val checkForPop = !(traceToConcretize.states.first() as XcfaState<*>).xcfa!!.isInlined - - return if (checkForPop && refinerResult.isUnsafe) findPoppedState(traceToConcretize)?.let { (i, state) -> - when (pruneStrategy) { - PruneStrategy.LAZY -> { - logger.write(Logger.Level.SUBSTEP, "| | Pruning from index %d...", i) - val nodeToPrune = cexToConcretize.node(i) - nodePruner.prune(arg, nodeToPrune) - } - - PruneStrategy.FULL -> { - logger.write(Logger.Level.SUBSTEP, "| | Pruning whole ARG", i) - arg.pruneAll() - } - - else -> throw UnsupportedOperationException("Unsupported pruning strategy") - } - - val refinedPrec = (prec as XcfaPrec

).copy() - refinedPrec.noPop.add(state) - RefinerResult.spurious(refinedPrec as P?) - } ?: refinerResult else refinerResult + else -> throw java.lang.UnsupportedOperationException("Unsupported pruning strategy") + } + logger.write(Logger.Level.SUBSTEP, "done%n") + RefinerResult.spurious(refinedPrec) } - - companion object { - - fun create( - exprTraceChecker: ExprTraceChecker, precRefiner: PrecRefiner, - pruneStrategy: PruneStrategy, logger: Logger - ): XcfaSingleExprTraceRefiner { - return XcfaSingleExprTraceRefiner(exprTraceChecker, precRefiner, pruneStrategy, logger) + } + + override fun refine(arg: ARG, prec: P?): RefinerResult> { + Preconditions.checkNotNull(arg) + Preconditions.checkNotNull

(prec) + assert(!arg.isSafe) { "ARG must be unsafe" } + + val optionalNewCex = arg.cexs.findFirst() + val cexToConcretize = optionalNewCex.get() + val traceToConcretize = cexToConcretize.toTrace() + + val refinerResult = refineTemp(arg, prec) // super.refine(arg, prec) + val checkForPop = !(traceToConcretize.states.first() as XcfaState<*>).xcfa!!.isInlined + + return if (checkForPop && refinerResult.isUnsafe) + findPoppedState(traceToConcretize)?.let { (i, state) -> + when (pruneStrategy) { + PruneStrategy.LAZY -> { + logger.write(Logger.Level.SUBSTEP, "| | Pruning from index %d...", i) + val nodeToPrune = cexToConcretize.node(i) + nodePruner.prune(arg, nodeToPrune) + } + + PruneStrategy.FULL -> { + logger.write(Logger.Level.SUBSTEP, "| | Pruning whole ARG", i) + arg.pruneAll() + } + + else -> throw UnsupportedOperationException("Unsupported pruning strategy") } - fun create( - exprTraceChecker: ExprTraceChecker, precRefiner: PrecRefiner, - pruneStrategy: PruneStrategy, logger: Logger, nodePruner: NodePruner - ): XcfaSingleExprTraceRefiner { - return XcfaSingleExprTraceRefiner(exprTraceChecker, precRefiner, pruneStrategy, logger, nodePruner) - } + val refinedPrec = (prec as XcfaPrec

).copy() + refinedPrec.noPop.add(state) + RefinerResult.spurious(refinedPrec as P?) + } ?: refinerResult + else refinerResult + } + + companion object { + + fun create( + exprTraceChecker: ExprTraceChecker, + precRefiner: PrecRefiner, + pruneStrategy: PruneStrategy, + logger: Logger, + ): XcfaSingleExprTraceRefiner { + return XcfaSingleExprTraceRefiner(exprTraceChecker, precRefiner, pruneStrategy, logger) + } + + fun create( + exprTraceChecker: ExprTraceChecker, + precRefiner: PrecRefiner, + pruneStrategy: PruneStrategy, + logger: Logger, + nodePruner: NodePruner, + ): XcfaSingleExprTraceRefiner { + return XcfaSingleExprTraceRefiner( + exprTraceChecker, + precRefiner, + pruneStrategy, + logger, + nodePruner, + ) } + } }