Qualify Ghost Names (#52)

Author: rcosta358

.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));
     }
 }