Multiedge CFA - name collision in generated locations

[ghost]

If you define an edge with multiple stmts, the CFA is split in CfaEdgeDefinition.java, but the intermediate generated locations all have a name of empty string. This can collide later as something asserts that location names are unique. I've found the bug using this project, but maybe the error is not here.

I have a test that fails without this patch, but runs fine when applied:

diff --git a/subprojects/cfa/src/main/java/hu/bme/mit/theta/cfa/dsl/CfaEdgeDefinition.java b/subprojects/cfa/src/main/java/hu/bme/mit/theta/cfa/dsl/CfaEdgeDefinition.java
index e1551039a..cff703735 100644
--- a/subprojects/cfa/src/main/java/hu/bme/mit/theta/cfa/dsl/CfaEdgeDefinition.java
+++ b/subprojects/cfa/src/main/java/hu/bme/mit/theta/cfa/dsl/CfaEdgeDefinition.java
@@ -49,6 +49,8 @@ final class CfaEdgeDefinition {

        ////

+       private static int counter = 0;
+
        public List<Edge> instantiate(final CFA.Builder cfa, final Env env) {
                final CfaLocationSymbol sourceSymbol = (CfaLocationSymbol) scope.resolve(source).get();
                final CfaLocationSymbol targetSymbol = (CfaLocationSymbol) scope.resolve(target).get();
@@ -63,7 +65,7 @@ final class CfaEdgeDefinition {
                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("Lgen" + ++counter));
                }
                locs.add(targetLoc);

Do you know anything in this lib that asserts location name uniqueness? @mondokm If not, I'll move the discussion to the theta :)

[mondokm]

Yes, CfaProductState.equals asserts location name uniqueness. This bug can cause the abstractor to believe an unvisited state has already been visited, missing a possible counterexample. I believe this discussion should be moved to theta as this means there is currently no way of distinguishing between two locations of the same name.

[ghost]

Location instances and CFA Locations (as an abstract entity) have a one-to-one mapping, thus loc.getName().equals(other.loc.getName()) could be changed loc == other.loc or loc.equals(other.loc) and it will work.

[ghost]

See for example:

https://github.com/ftsrg/theta/blob/master/subprojects/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/CfaState.java#L96

[mondokm]

Ok