Merge pull request #120 from ftsrg/cfachecks

Check CFA variables and locations for unique names

build.gradle.kts

@@ -10,7 +10,7 @@ buildscript {
 
 allprojects {
     group = "hu.bme.mit.inf.theta"
-    version = "2.16.0"
+    version = "2.17.0"
 
     apply(from = rootDir.resolve("gradle/shared-with-buildSrc/mirrors.gradle.kts"))
 }

subprojects/cfa/cfa/src/main/java/hu/bme/mit/theta/cfa/CFA.java

@@ -53,6 +53,11 @@ private CFA(final Builder builder) {
 		locs = ImmutableSet.copyOf(builder.locs);
 		edges = ImmutableList.copyOf(builder.edges);
 		vars = edges.stream().flatMap(e -> StmtUtils.getVars(e.getStmt()).stream()).collect(toImmutableSet());
+		Set<String> varNames = Containers.createSet();
+		for (var v : vars) {
+			checkArgument(!varNames.contains(v.getName()), "Variable with name '" + v.getName() + "' already exists in the CFA.");
+			varNames.add(v.getName());
+		}
 	}
 
 	public Loc getInitLoc() {
@@ -174,10 +179,15 @@ public static final class Builder {
 		private final Collection<Loc> locs;
 		private final Collection<Edge> edges;
 
+		private final Set<String> locNames;
+
 		private boolean built;
 
+		private static int UNNAMED_LOC_LABEL = 0;
+
 		private Builder() {
 			locs = Containers.createSet();
+			locNames = Containers.createSet();
 			edges = new LinkedList<>();
 			built = false;
 		}
@@ -223,11 +233,17 @@ public void setErrorLoc(final Loc errorLoc) {
 
 		public Loc createLoc(final String name) {
 			checkNotBuilt();
+			checkArgument(!locNames.contains(name), "Location with name '" + name + "' already exists in the CFA.");
 			final Loc loc = new Loc(name);
 			locs.add(loc);
+			locNames.add(name);
 			return loc;
 		}
 
+		public Loc createLoc() {
+			return createLoc("__" + UNNAMED_LOC_LABEL++);
+		}
+
 		public Edge createEdge(final Loc source, final Loc target, final Stmt stmt) {
 			checkNotBuilt();
 			checkArgument(locs.contains(source), "Invalid source.");

subprojects/cfa/cfa/src/main/java/hu/bme/mit/theta/cfa/dsl/CfaEdgeDefinition.java

@@ -63,7 +63,7 @@ public List<Edge> instantiate(final CFA.Builder cfa, final Env env) {
 		final List<Loc> locs = new ArrayList<>(stmts.size() + 1);
 		locs.add(sourceLoc);
 		for (int i = 0; i < stmts.size() - 1; ++i) {
-			locs.add(cfa.createLoc(""));
+			locs.add(cfa.createLoc());
 		}
 		locs.add(targetLoc);
 

subprojects/cfa/cfa/src/test/java/hu/bme/mit/theta/cfa/CfaTest.java

@@ -0,0 +1,33 @@
+package hu.bme.mit.theta.cfa;
+
+import hu.bme.mit.theta.core.decl.Decls;
+import hu.bme.mit.theta.core.decl.VarDecl;
+import hu.bme.mit.theta.core.stmt.Stmts;
+import hu.bme.mit.theta.core.type.inttype.IntExprs;
+import hu.bme.mit.theta.core.type.inttype.IntType;
+import org.junit.Test;
+
+public class CfaTest {
+
+    @Test(expected = IllegalArgumentException.class)
+    public void testDuplicateLocationName() {
+        CFA.Builder builder = CFA.builder();
+        builder.createLoc("A");
+        builder.createLoc("B");
+        builder.createLoc("A");
+    }
+
+    @Test(expected = IllegalArgumentException.class)
+    public void testDuplicateVarName() {
+        CFA.Builder builder = CFA.builder();
+        VarDecl<IntType> v1 = Decls.Var("x", IntExprs.Int());
+        VarDecl<IntType> v2 = Decls.Var("x", IntExprs.Int());
+        CFA.Loc init = builder.createLoc();
+        CFA.Loc loc1 = builder.createLoc();
+        CFA.Loc loc2 = builder.createLoc();
+        builder.createEdge(init, loc1, Stmts.Havoc(v1));
+        builder.createEdge(init, loc2, Stmts.Havoc(v2));
+        builder.setInitLoc(init);
+        builder.build();
+    }
+}