Qualify Ghost Names

.vscode/launch.json

@@ -0,0 +1,12 @@
+{
+  "configurations": [
+    {
+      "type": "java",
+      "name": "Run LiquidJava",
+      "request": "launch",
+      "mainClass": "liquidjava.api.CommandLineLauncher",
+      "projectName": "liquidjava-verifier",
+      "args": "liquidjava-example/src/main/java/test"
+    }
+  ]
+}

liquidjava-example/src/main/java/testSuite/classes/ambiguous_state_names_correct/Door.java

@@ -0,0 +1,11 @@
+package testSuite.classes.ambiguous_state_names_correct;
+
+import liquidjava.specification.StateSet;
+import liquidjava.specification.StateRefinement;
+
+@StateSet({"open", "closed"})
+public class Door {
+
+    @StateRefinement(to = "open(this)")
+    public Door() { }
+}

liquidjava-example/src/main/java/testSuite/classes/ambiguous_state_names_correct/Pipe.java

@@ -0,0 +1,11 @@
+package testSuite.classes.ambiguous_state_names_correct;
+
+import liquidjava.specification.StateSet;
+import liquidjava.specification.StateRefinement;
+
+@StateSet({"open", "closed"})
+public class Pipe {
+
+    @StateRefinement(to = "open(this)")
+    public Pipe() { }
+}

liquidjava-example/src/main/java/testSuite/classes/ambiguous_state_names_correct/SimpleTest.java

@@ -0,0 +1,14 @@
+package testSuite.classes.ambiguous_state_names_correct;
+
+import liquidjava.specification.Refinement;
+
+public class SimpleTest {
+
+    public static void main(String[] args) {
+        Door d = new Door(); // contains 'open' and 'closed' states
+        Pipe p = new Pipe(); // unrelated type with the same state names
+        requiresOpen(d); // ok iff 'open' binds to Door.open otherwise it may bind to Pipe.open and fail
+    }
+
+    public static void requiresOpen(@Refinement("open(s)") Door s) { }
+}

liquidjava-example/src/main/java/testSuite/classes/conflicting_state_names_correct/SM1.java

@@ -0,0 +1,15 @@
+package testSuite.classes.conflicting_state_names_correct;
+
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+@StateSet({"uninitialized", "initialized"})
+public class SM1 {
+
+	@StateRefinement(to="uninitialized(this)")
+	public SM1() {}
+
+
+	@StateRefinement(from="uninitialized(this)", to="initialized(this)")
+	public void initialize() {}
+}

liquidjava-example/src/main/java/testSuite/classes/conflicting_state_names_correct/SM2.java

@@ -0,0 +1,15 @@
+package testSuite.classes.conflicting_state_names_correct;
+
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+@StateSet({"uninitialized", "initialized"})
+public class SM2 {
+
+	@StateRefinement(to="uninitialized(this)")
+	public SM2() {}
+
+
+	@StateRefinement(from="uninitialized(this)", to="initialized(this)")
+	public void initialize() {}
+}

liquidjava-example/src/main/java/testSuite/classes/conflicting_state_names_correct/SimpleTest.java

@@ -0,0 +1,11 @@
+package testSuite.classes.conflicting_state_names_correct;
+
+class SimpleTest {
+	public static void main(String[] args) {
+		// both classes contain the same state names
+		SM1 sm1 = new SM1();
+		SM2 sm2 = new SM2();
+		sm1.initialize();
+		sm2.initialize();
+	}
+}

liquidjava-verifier/src/main/java/liquidjava/processor/VCImplication.java

@@ -1,6 +1,7 @@
 package liquidjava.processor;
 
 import liquidjava.rj_language.Predicate;
+import liquidjava.utils.Utils;
 import spoon.reflect.reference.CtTypeReference;
 
 /**
@@ -29,7 +30,7 @@ public void setNext(VCImplication c) {
     public String toString() {
         if (name != null && type != null) {
             String qualType = type.getQualifiedName();
-            String simpleType = qualType.contains(".") ? qualType.substring(qualType.lastIndexOf(".") + 1) : qualType;
+            String simpleType = qualType.contains(".") ? Utils.getSimpleName(qualType) : qualType;
             return String.format("%-20s %s %s", "∀" + name + ":" + simpleType + ",", refinement.toString(),
                     next != null ? " => \n" + next.toString() : "");
         } else

liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java

@@ -335,7 +335,7 @@ public void addGhostFunction(GhostFunction gh) {
 
     public boolean hasGhost(String name) {
         for (GhostFunction g : ghosts) {
-            if (g.getName().equals(name))
+            if (g.matches(name))
                 return true;
         }
         return false;

liquidjava-verifier/src/main/java/liquidjava/processor/context/GhostFunction.java

@@ -12,40 +12,39 @@ public class GhostFunction {
     private String name;
     private List<CtTypeReference<?>> param_types;
     private CtTypeReference<?> return_type;
+    private String prefix;
 
-    private String klassName;
-
-    public GhostFunction(GhostDTO f, Factory factory, String path, String klass) {
-        name = f.getName();
-        return_type = Utils.getType(f.getReturn_type().equals(klass) ? path : f.getReturn_type(), factory);
-        param_types = new ArrayList<>();
+    public GhostFunction(GhostDTO f, Factory factory, String prefix) {
+        String klass = this.getParentClassName(prefix);
+        this.name = f.getName();
+        this.return_type = Utils.getType(f.getReturn_type().equals(klass) ? prefix : f.getReturn_type(), factory);
+        this.param_types = new ArrayList<>();
+        this.prefix = prefix;
         for (String t : f.getParam_types()) {
-            param_types.add(Utils.getType(t.equals(klass) ? path : t, factory));
+            this.param_types.add(Utils.getType(t.equals(klass) ? prefix : t, factory));
         }
     }
 
     public GhostFunction(String name, List<String> param_types, CtTypeReference<?> return_type, Factory factory,
-            String path, String klass) {
+            String prefix) {
+        String klass = this.getParentClassName(prefix);
+        String type = return_type.toString().equals(klass) ? prefix : return_type.toString();
         this.name = name;
-        this.return_type = Utils.getType(return_type.toString().equals(klass) ? path : return_type.toString(), factory);
+        this.return_type = Utils.getType(type, factory);
         this.param_types = new ArrayList<>();
+        this.prefix = prefix;
         for (int i = 0; i < param_types.size(); i++) {
             String mType = param_types.get(i).toString();
-            this.param_types.add(Utils.getType(mType.equals(klass) ? path : mType, factory));
+            this.param_types.add(Utils.getType(mType.equals(klass) ? prefix : mType, factory));
         }
-        this.klassName = klass;
     }
 
-    protected GhostFunction(String name, List<CtTypeReference<?>> list, CtTypeReference<?> return_type, String klass) {
+    protected GhostFunction(String name, List<CtTypeReference<?>> list, CtTypeReference<?> return_type, String prefix) {
         this.name = name;
         this.return_type = return_type;
         this.param_types = new ArrayList<>();
         this.param_types = list;
-        this.klassName = klass;
-    }
-
-    public String getName() {
-        return name;
+        this.prefix = prefix;
     }
 
     public CtTypeReference<?> getReturnType() {
@@ -67,7 +66,30 @@ public String toString() {
         return sb.toString();
     }
 
+    public String getName() {
+        return name;
+    }
+
+    public String getPrefix() {
+        return prefix;
+    }
+
+    public String getQualifiedName() {
+        return Utils.qualifyName(prefix, name);
+    }
+
     public String getParentClassName() {
-        return klassName;
+        return getParentClassName(prefix);
+    }
+
+    private String getParentClassName(String pref) {
+        return Utils.getSimpleName(pref);
+    }
+
+    // Match by fully qualified name, exact simple name or by comparing the simple name of the provided identifier
+    // This allows references written in a different class (different prefix) to still match
+    public boolean matches(String name) {
+        return this.getQualifiedName().equals(name) || this.name.equals(name)
+                || this.name.equals(Utils.getSimpleName(name));
     }
 }

liquidjava-verifier/src/main/java/liquidjava/processor/context/GhostParentState.java

@@ -9,9 +9,8 @@ public class GhostParentState extends GhostFunction {
 
     private ArrayList<GhostState> states;
 
-    public GhostParentState(String name, List<String> params, CtTypeReference<?> ret, Factory factory,
-            String qualifiedName, String simpleName) {
-        super(name, params, ret, factory, qualifiedName, simpleName);
+    public GhostParentState(String name, List<String> params, CtTypeReference<?> ret, Factory factory, String prefix) {
+        super(name, params, ret, factory, prefix);
         states = new ArrayList<>();
     }
 

liquidjava-verifier/src/main/java/liquidjava/processor/context/GhostState.java

@@ -9,8 +9,8 @@ public class GhostState extends GhostFunction {
     private GhostFunction parent;
     private Predicate refinement;
 
-    public GhostState(String name, List<CtTypeReference<?>> list, CtTypeReference<?> return_type, String klass) {
-        super(name, list, return_type, klass);
+    public GhostState(String name, List<CtTypeReference<?>> list, CtTypeReference<?> return_type, String prefix) {
+        super(name, list, return_type, prefix);
     }
 
     public void setGhostParent(GhostFunction parent) {

liquidjava-verifier/src/main/java/liquidjava/processor/facade/AliasDTO.java

@@ -12,6 +12,7 @@ public class AliasDTO {
     private List<String> varTypes;
     private List<String> varNames;
     private Expression expression;
+    private String ref;
 
     public AliasDTO(String name, List<CtTypeReference<?>> varTypes, List<String> varNames, Expression expression) {
         super();
@@ -26,7 +27,15 @@ public AliasDTO(String name2, List<String> varTypes2, List<String> varNames2, St
         this.name = name2;
         this.varTypes = varTypes2;
         this.varNames = varNames2;
-        this.expression = RefinementsParser.createAST(ref);
+        this.ref = ref;
+    }
+
+    // Parse the alias expression using the given the prefix to ensure ghost names are qualified consistently with
+    // where the alias is declared or used
+    public void parse(String prefix) throws ParsingException {
+        if (ref != null) {
+            this.expression = RefinementsParser.createAST(ref, prefix);
+        }
     }
 
     public String getName() {

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java

@@ -12,6 +12,7 @@
 import liquidjava.rj_language.Predicate;
 import liquidjava.rj_language.parsing.ParsingException;
 import liquidjava.rj_language.parsing.RefinementsParser;
+import liquidjava.utils.Utils;
 import spoon.reflect.declaration.CtClass;
 import spoon.reflect.declaration.CtElement;
 import spoon.reflect.declaration.CtField;
@@ -40,7 +41,7 @@ public <T> void visitCtInterface(CtInterface<T> intrface) {
 
         Optional<String> externalRefinements = getExternalRefinement(intrface);
         if (externalRefinements.isPresent()) {
-            prefix = externalRefinements.get();
+            this.prefix = externalRefinements.get();
             try {
                 getRefinementFromAnnotation(intrface);
             } catch (ParsingException e) {
@@ -89,9 +90,7 @@ protected void getGhostFunction(String value, CtElement element) {
             // RefinementParser.parseFunctionDecl(value);
             GhostDTO f = RefinementsParser.getGhostDeclaration(value);
             if (f != null && element.getParent() instanceof CtInterface<?>) {
-                String[] a = prefix.split("\\.");
-                String d = a[a.length - 1];
-                GhostFunction gh = new GhostFunction(f, factory, prefix, d);
+                GhostFunction gh = new GhostFunction(f, factory, prefix);
                 context.addGhostFunction(gh);
             }
 
@@ -104,13 +103,12 @@ protected void getGhostFunction(String value, CtElement element) {
 
     @Override
     protected Optional<GhostFunction> createStateGhost(int order, CtElement element) {
-        String[] a = prefix.split("\\.");
-        String klass = a[a.length - 1];
+        String klass = Utils.getSimpleName(prefix);
         if (klass != null) {
             CtTypeReference<?> ret = factory.Type().INTEGER_PRIMITIVE;
             List<String> params = Arrays.asList(klass);
-            GhostFunction gh = new GhostFunction(String.format("%s_state%d", klass.toLowerCase(), order), params, ret,
-                    factory, prefix, klass);
+            String name = String.format("state%d", order);
+            GhostFunction gh = new GhostFunction(name, params, ret, factory, prefix);
             return Optional.of(gh);
         }
         return Optional.empty();
@@ -123,7 +121,6 @@ protected String getQualifiedClassName(CtElement elem) {
 
     @Override
     protected String getSimpleClassName(CtElement elem) {
-        String[] a = prefix.split("\\.");
-        return a[a.length - 1];
+        return Utils.getSimpleName(prefix);
     }
 }

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java

@@ -128,7 +128,7 @@ private void createStateSet(CtNewArray<String> e, int set, CtElement element) {
                 CtLiteral<String> s = (CtLiteral<String>) ce;
                 String f = s.getValue();
                 GhostState gs = new GhostState(f, g.getParametersTypes(), factory.Type().BOOLEAN_PRIMITIVE,
-                        g.getParentClassName());
+                        g.getPrefix());
                 gs.setGhostParent(g);
                 gs.setRefinement(
                         /* new OperationPredicate(new InvocationPredicate(f, THIS), "<-->", */
@@ -194,9 +194,8 @@ protected Optional<GhostFunction> createStateGhost(int order, CtElement element)
         if (klass != null) {
             CtTypeReference<?> ret = factory.Type().INTEGER_PRIMITIVE;
             List<String> params = Arrays.asList(klass.getSimpleName());
-            GhostFunction gh = new GhostFunction(
-                    String.format("%s_state%d", klass.getSimpleName().toLowerCase(), order), params, ret, factory,
-                    klass.getQualifiedName(), klass.getSimpleName());
+            String name = String.format("state%d", order);
+            GhostFunction gh = new GhostFunction(name, params, ret, factory, klass.getQualifiedName());
             return Optional.of(gh);
         }
         return Optional.empty();
@@ -207,7 +206,7 @@ protected void getGhostFunction(String value, CtElement element) {
             GhostDTO f = RefinementsParser.getGhostDeclaration(value);
             if (f != null && element.getParent() instanceof CtClass<?>) {
                 CtClass<?> klass = (CtClass<?>) element.getParent();
-                GhostFunction gh = new GhostFunction(f, factory, klass.getQualifiedName(), klass.getSimpleName());
+                GhostFunction gh = new GhostFunction(f, factory, klass.getQualifiedName());
                 context.addGhostFunction(gh);
             }
         } catch (ParsingException e) {
@@ -233,6 +232,7 @@ protected void handleAlias(String value, CtElement element) {
                     path = ((CtInterface<?>) element).getQualifiedName();
                 }
                 if (klass != null && path != null) {
+                    a.parse(path);
                     AliasWrapper aw = new AliasWrapper(a, factory, WILD_VAR, context, klass, path);
                     context.addAlias(aw);
                 }