Merged algorithmselection

ftsrg · Aug 25, 2021 · f4a8407 · f4a8407
2 parents 619034e + 7d9e8de
commit f4a8407
Show file tree

Hide file tree

Showing 14 changed files with 1,179 additions and 1 deletion.
diff --git a/settings.gradle.kts b/settings.gradle.kts
@@ -20,6 +20,7 @@ include(
         "xcfa/xcfa-analysis",
         "xcfa/xcfa-cli",
         "xcfa/cat",
+        "xcfa/algorithmselection",
 
         "xta/xta",
         "xta/xta-analysis",

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
@@ -67,6 +67,11 @@ public boolean isBottom() {
 		return state.isBottom();
 	}
 
+	@Override
+	public boolean isTop() {
+		return state.isTop();
+	}
+
 	@Override
 	public Expr<BoolType> 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
@@ -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
@@ -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<S extends State, A extends Action> {
 	private int nextId = 0;
 	final PartialOrd<S> 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<S> partialOrd) {
 		initNodes = Containers.createSet();
 		this.partialOrd = partialOrd;

diff --git a/...common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/CegarChecker.java b/...common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/CegarChecker.java
@@ -20,14 +20,21 @@
 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;
 import hu.bme.mit.theta.common.logging.Logger;
 import hu.bme.mit.theta.common.logging.Logger.Level;
 import hu.bme.mit.theta.common.logging.NullLogger;
 
+import java.util.Collection;
+import java.util.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 static com.google.common.base.Preconditions.checkNotNull;
 
@@ -43,6 +50,10 @@ public final class CegarChecker<S extends State, A extends Action, P extends Pre
 	private final Refiner<S, A, P> refiner;
 	private final Logger logger;
 
+	// controlled restart
+	private Set<AbstractArg> args = new LinkedHashSet<>();
+	private P lastPrecision = null;
+
 	private CegarChecker(final Abstractor<S, A, P> abstractor, final Refiner<S, A, P> refiner, final Logger logger) {
 		this.abstractor = checkNotNull(abstractor);
 		this.refiner = checkNotNull(refiner);
@@ -59,6 +70,28 @@ public static <S extends State, A extends Action, P extends Prec> CegarChecker<S
 		return new CegarChecker<>(abstractor, refiner, logger);
 	}
 
+	private class AbstractArg {
+		private final Collection<State> states;
+
+
+		private AbstractArg(final Stream<ArgNode<S, A>> 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<S, A> check(final P initPrec) {
 		logger.write(Level.INFO, "Configuration: %s%n", this);
@@ -80,6 +113,29 @@ public SafetyResult<S, A> 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<ArgNode<S, A>> argNodeStream = arg.getNodes().filter(saArgNode -> !saArgNode.getState().isTop() && saArgNode.isSafe());
+			List<ArgNode<S, A>> 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
@@ -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());
 	}
+
 }
diff --git a/subprojects/common/c-frontend/build.gradle.kts b/subprojects/common/c-frontend/build.gradle.kts
@@ -4,4 +4,5 @@ plugins {
 }
 dependencies {
     compile(project(":theta-core"))
+    compile(project(":theta-algorithmselection"))
 }
diff --git a/...n/java/hu/bme/mit/theta/frontend/transformation/grammar/expression/ExpressionVisitor.java b/...n/java/hu/bme/mit/theta/frontend/transformation/grammar/expression/ExpressionVisitor.java
@@ -33,6 +33,7 @@
 import hu.bme.mit.theta.frontend.transformation.model.types.complex.compound.CArray;
 import hu.bme.mit.theta.frontend.transformation.model.types.complex.compound.CPointer;
 import hu.bme.mit.theta.frontend.transformation.model.types.complex.real.CReal;
+import hu.bme.mit.theta.xcfa.algorithmselection.MaxEnumAnalyzer;
 import org.kframework.mpfr.BigFloat;
 import org.kframework.mpfr.BinaryMathContext;
 
@@ -245,6 +246,7 @@ public Expr<?> visitRelationalExpression(CParser.RelationalExpressionContext ctx
 					default:
 						throw new IllegalStateException("Unexpected value: " + ctx.signs.get(i).getText());
 				}
+				MaxEnumAnalyzer.instance.consume(guard);
 				CComplexType signedInt = CComplexType.getSignedInt();
 				expr = Ite(guard, signedInt.getUnitValue(), signedInt.getNullValue());
 				FrontendMetadata.create(expr, "cType", signedInt);
@@ -536,7 +538,7 @@ public Expr<?> visitPrimaryExpressionConstant(CParser.PrimaryExpressionConstantC
 
 			BigFloat bigFloat;
 			if (text.startsWith("0x")) {
-				throw new UnsupportedOperationException("Hexadeximal FP constants are not yet supported!");
+				throw new UnsupportedOperationException("Hexadecimal FP constants are not yet supported!");
 			} else if (text.startsWith("0b")) {
 				throw new UnsupportedOperationException("Binary FP constants are not yet supported!");
 			} else {

diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/bvtype/BvType.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/bvtype/BvType.java
@@ -58,6 +58,11 @@ public int getSize() {
         return size;
     }
 
+    public Boolean getSigned() {
+        checkState(signed!=null);
+        return signed;
+    }
+
     @Override
     public EqExpr<BvType> Eq(Expr<BvType> leftOp, Expr<BvType> rightOp) {
         return BvEqExpr.of(leftOp, rightOp);

diff --git a/subprojects/xcfa/algorithmselection/README.md b/subprojects/xcfa/algorithmselection/README.md
@@ -0,0 +1,3 @@
+## Overview
+
+Cat language
diff --git a/subprojects/xcfa/algorithmselection/build.gradle.kts b/subprojects/xcfa/algorithmselection/build.gradle.kts
@@ -0,0 +1,9 @@
+plugins {
+    id("java-common")
+    id("antlr-grammar")
+}
+
+dependencies {
+    compile(project(":theta-common"))
+    compile(project(":theta-core"))
+}
-Original file line number
+Diff line change
@@ Expand Up / @@ -27,4 +27,6 @@ public interface State { @@
     	 */
     	boolean isBottom();
+    	default boolean isTop() { return false; }
     }