From 7d9e8de55ded7bba4db1e9bfe13947237ebbd7fb Mon Sep 17 00:00:00 2001 From: AdamZsofi Date: Thu, 12 Aug 2021 17:32:24 +0200 Subject: [PATCH] Added ARG and precision check against getting stuck in the analysis --- .../bme/mit/theta/cfa/analysis/CfaState.java | 5 ++ .../java/hu/bme/mit/theta/analysis/State.java | 2 + .../bme/mit/theta/analysis/algorithm/ARG.java | 15 +++++ .../algorithm/cegar/CegarChecker.java | 56 +++++++++++++++++++ .../mit/theta/analysis/expl/ExplState.java | 6 ++ 5 files changed, 84 insertions(+) diff --git a/subprojects/cfa/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/CfaState.java b/subprojects/cfa/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/CfaState.java index 5fb4683987..b354aaa657 100644 --- a/subprojects/cfa/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/CfaState.java +++ b/subprojects/cfa/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/CfaState.java @@ -67,6 +67,11 @@ public boolean isBottom() { return state.isBottom(); } + @Override + public boolean isTop() { + return state.isTop(); + } + @Override public Expr toExpr() { // TODO Should be loc = l and toExpr(state) diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/State.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/State.java index 4d1de9c526..3d357e618b 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/State.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/State.java @@ -27,4 +27,6 @@ public interface State { */ boolean isBottom(); + default boolean isTop() { return false; } + } diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/ARG.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/ARG.java index 16221bf33e..b50f60f710 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/ARG.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/ARG.java @@ -22,6 +22,8 @@ import java.util.Collection; import hu.bme.mit.theta.common.container.Containers; + +import java.util.Objects; import java.util.Optional; import java.util.OptionalInt; import java.util.stream.Stream; @@ -41,6 +43,19 @@ public final class ARG { private int nextId = 0; final PartialOrd partialOrd; + @Override + public boolean equals(Object o) { + if (this == o) return true; + if (o == null || getClass() != o.getClass()) return false; + ARG arg = (ARG) o; + return initialized == arg.initialized && nextId == arg.nextId && initNodes.equals(arg.initNodes) && partialOrd.equals(arg.partialOrd); + } + + @Override + public int hashCode() { + return Objects.hash(initNodes.stream().map(ArgNode::getState), initialized, nextId, partialOrd); + } + private ARG(final PartialOrd partialOrd) { initNodes = Containers.createSet(); this.partialOrd = partialOrd; 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 e6b2648400..065db19bf1 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,7 +17,13 @@ import static com.google.common.base.Preconditions.checkNotNull; +import java.util.Collection; +import java.util.LinkedHashSet; +import java.util.Objects; +import java.util.Set; import java.util.concurrent.TimeUnit; +import java.util.stream.Collectors; +import java.util.stream.Stream; import com.google.common.base.Stopwatch; @@ -25,6 +31,7 @@ import hu.bme.mit.theta.analysis.Prec; import hu.bme.mit.theta.analysis.State; import hu.bme.mit.theta.analysis.algorithm.ARG; +import hu.bme.mit.theta.analysis.algorithm.ArgNode; import hu.bme.mit.theta.analysis.algorithm.SafetyChecker; import hu.bme.mit.theta.analysis.algorithm.SafetyResult; import hu.bme.mit.theta.common.Utils; @@ -44,6 +51,10 @@ public final class CegarChecker refiner; private final Logger logger; + // controlled restart + private Set args = new LinkedHashSet<>(); + private P lastPrecision = null; + private CegarChecker(final Abstractor abstractor, final Refiner refiner, final Logger logger) { this.abstractor = checkNotNull(abstractor); this.refiner = checkNotNull(refiner); @@ -60,6 +71,28 @@ public static CegarChecker(abstractor, refiner, logger); } + private class AbstractArg { + private final Collection states; + + + private AbstractArg(final Stream> nodes){ + states = nodes.map(ArgNode::getState).collect(Collectors.toSet()); + } + + @Override + public boolean equals(Object o) { + if (this == o) return true; + if (o == null || getClass() != o.getClass()) return false; + AbstractArg that = (AbstractArg) o; + return states.equals(that.states); + } + + @Override + public int hashCode() { + return Objects.hash(states); + } + } + @Override public SafetyResult check(final P initPrec) { logger.write(Level.INFO, "Configuration: %s%n", this); @@ -81,6 +114,29 @@ public SafetyResult check(final P initPrec) { abstractorTime += stopwatch.elapsed(TimeUnit.MILLISECONDS) - abstractorStartTime; logger.write(Level.MAINSTEP, "| Checking abstraction done, result: %s%n", abstractorResult); + AbstractArg abstractArg = new AbstractArg(arg.getNodes()); + if(args.contains(abstractArg) && lastPrecision != null && lastPrecision.equals(prec)) { + System.err.println("Not solvable!"); + throw new RuntimeException("Not solvable!"); + } + args.add(abstractArg); + lastPrecision = prec; + + /*Stream> argNodeStream = arg.getNodes().filter(saArgNode -> !saArgNode.getState().isTop() && saArgNode.isSafe()); + List> collect = arg.getNodes().filter(saArgNode -> !saArgNode.getState().isTop() && saArgNode.isSafe()).collect(Collectors.toList()); + + if(argNodeStream.count() == 0) { + System.err.println("True arg"); + if(lastArgTrue && lastPrecision != null && lastPrecision.equals(prec)) { + System.err.println("Not solvable!"); + throw new RuntimeException("Not solvable!"); + } + lastArgTrue = true; + } else { + lastArgTrue = false; + } + lastPrecision = prec;*/ + if (abstractorResult.isUnsafe()) { logger.write(Level.MAINSTEP, "| Refining abstraction...%n"); final long refinerStartTime = stopwatch.elapsed(TimeUnit.MILLISECONDS); diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/expl/ExplState.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/expl/ExplState.java index 54887e6985..d14d004790 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/expl/ExplState.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/expl/ExplState.java @@ -124,6 +124,11 @@ public boolean isBottom() { return false; } + @Override + public boolean isTop() { + return val.getDecls().isEmpty(); + } + @Override public String toString() { return Utils.lispStringBuilder(ExplState.class.getSimpleName()).aligned() @@ -183,4 +188,5 @@ private static class BottomLazyHolder { private static class TopLazyHolder { static final ExplState INSTANCE = new NonBottom(ImmutableValuation.empty()); } + }