Fix Alias Qualified Name

Author: rcosta358

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

@@ -28,9 +28,9 @@ public GhostFunction(GhostDTO f, Factory factory, String prefix) {
     public GhostFunction(String name, List<String> param_types, CtTypeReference<?> return_type, Factory factory,
             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) ? prefix : 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++) {

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, null); // is the parent class needed here?
+        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/TypeChecker.java

@@ -232,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);
                 }

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java

@@ -154,12 +154,10 @@ private static ObjectState getStates(CtAnnotation<? extends Annotation> ctAnnota
         String from = TypeCheckingUtils.getStringFromAnnotation(m.get("from"));
         String to = TypeCheckingUtils.getStringFromAnnotation(m.get("to"));
         ObjectState state = new ObjectState();
-        if (from != null) // has From
-        {
+        if (from != null) { // has From
             state.setFrom(createStatePredicate(from, f.getTargetClass(), tc, e, false, prefix));
         }
-        if (to != null) // has To
-        {
+        if (to != null) { // has To
             state.setTo(createStatePredicate(to, f.getTargetClass(), tc, e, true, prefix));
         }
 

liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java

@@ -25,10 +25,8 @@
 import liquidjava.rj_language.parsing.RefinementsParser;
 import liquidjava.utils.Utils;
 import spoon.reflect.declaration.CtElement;
-import spoon.reflect.declaration.CtInterface;
 import spoon.reflect.declaration.CtType;
 import spoon.reflect.factory.Factory;
-import spoon.reflect.reference.CtTypeReference;
 
 /**
  * Acts as a wrapper for Expression AST
@@ -38,7 +36,7 @@
 public class Predicate {
 
     protected Expression exp;
-    protected String parentClass;
+    protected String prefix;
 
     /** Create a predicate with the expression true */
     public Predicate() {
@@ -69,7 +67,7 @@ public Predicate(String ref, CtElement element, ErrorEmitter e) throws ParsingEx
      * @throws ParsingException
      */
     public Predicate(String ref, CtElement element, ErrorEmitter e, String prefix) throws ParsingException {
-        this.parentClass = prefix;
+        this.prefix = prefix;
         exp = parse(ref, element, e);
         if (e.foundError()) {
             return;
@@ -86,16 +84,16 @@ public Predicate(Expression e) {
 
     protected Expression parse(String ref, CtElement element, ErrorEmitter e) throws ParsingException {
         try {
-            return RefinementsParser.createAST(ref, parentClass);
+            return RefinementsParser.createAST(ref, prefix);
         } catch (ParsingException e1) {
             ErrorHandler.printSyntaxError(e1.getMessage(), ref, element, e);
             throw e1;
         }
     }
 
-    protected Expression innerParse(String ref, ErrorEmitter e, String parentClass) {
+    protected Expression innerParse(String ref, ErrorEmitter e, String prefix) {
         try {
-            return RefinementsParser.createAST(ref, parentClass);
+            return RefinementsParser.createAST(ref, prefix);
         } catch (ParsingException e1) {
             ErrorHandler.printSyntaxError(e1.getMessage(), ref, e);
         }

liquidjava-verifier/src/main/java/liquidjava/rj_language/parsing/RefinementsParser.java

@@ -17,9 +17,9 @@
 
 public class RefinementsParser {
 
-    public static Expression createAST(String toParse, String parentClass) throws ParsingException {
+    public static Expression createAST(String toParse, String prefix) throws ParsingException {
         ParseTree pt = compile(toParse);
-        CreateASTVisitor visitor = new CreateASTVisitor(parentClass);
+        CreateASTVisitor visitor = new CreateASTVisitor(prefix);
         return visitor.create(pt);
     }
 

liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/CreateASTVisitor.java

@@ -57,10 +57,10 @@
  */
 public class CreateASTVisitor {
 
-    String parentClass;
+    String prefix;
 
-    public CreateASTVisitor(String parentClass) {
-        this.parentClass = parentClass;
+    public CreateASTVisitor(String prefix) {
+        this.prefix = prefix;
     }
 
     public Expression create(ParseTree rc) {
@@ -162,7 +162,7 @@ private Expression functionCallCreate(FunctionCallContext rc) {
         if (rc.ghostCall() != null) {
             GhostCallContext gc = rc.ghostCall();
             List<Expression> le = getArgs(gc.args());
-            String name = Utils.qualifyName(parentClass, gc.ID().getText());
+            String name = Utils.qualifyName(prefix, gc.ID().getText());
             return new FunctionInvocation(name, le);
         } else {
             AliasCallContext gc = rc.aliasCall();