Add File to GhostState

Author: rcosta358

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

@@ -14,9 +14,7 @@ public class ContextHistory {
     private static ContextHistory instance;
 
     private Map<String, Map<String, Set<RefinedVariable>>> fileScopeVars; // file -> (scope -> variables in scope)
-    private Map<String, Set<GhostState>> ghosts; // file -> ghosts
-
-    // globals
+    private Set<GhostState> ghosts;
     private Set<AliasWrapper> aliases;
     private Set<RefinedVariable> instanceVars;
     private Set<RefinedVariable> globalVars;
@@ -25,7 +23,7 @@ private ContextHistory() {
         fileScopeVars = new HashMap<>();
         instanceVars = new HashSet<>();
         globalVars = new HashSet<>();
-        ghosts = new HashMap<>();
+        ghosts = new HashSet<>();
         aliases = new HashSet<>();
     }
 
@@ -44,7 +42,7 @@ public void clearHistory() {
     }
 
     public void saveContext(CtElement element, Context context) {
-        String file = getFile(element);
+        String file = Utils.getFile(element);
         if (file == null)
             return;
 
@@ -56,26 +54,11 @@ public void saveContext(CtElement element, Context context) {
         // add other elements in context (except ghosts)
         instanceVars.addAll(context.getCtxInstanceVars());
         globalVars.addAll(context.getCtxGlobalVars());
+        ghosts.addAll(context.getGhostStates());
         aliases.addAll(context.getAliases());
     }
 
-    public void saveGhost(CtElement element, GhostState ghost) {
-        String file = getFile(element);
-        if (file == null)
-            return;
-        ghosts.putIfAbsent(file, new HashSet<>());
-        ghosts.get(file).add(ghost);
-    }
-
-    private String getFile(CtElement element) {
-        SourcePosition pos = element.getPosition();
-        if (pos == null || pos.getFile() == null)
-            return null;
-
-        return pos.getFile().getAbsolutePath();
-    }
-
-    public String getScopePosition(CtElement element) {
+    private String getScopePosition(CtElement element) {
         CtElement startElement = element instanceof CtParameter<?> ? element.getParent() : element;
         SourcePosition annPosition = Utils.getFirstLJAnnotationPosition(startElement);
         SourcePosition pos = element.getPosition();
@@ -95,7 +78,7 @@ public Set<RefinedVariable> getGlobalVars() {
         return globalVars;
     }
 
-    public Map<String, Set<GhostState>> getGhosts() {
+    public Set<GhostState> getGhosts() {
         return ghosts;
     }
 

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

@@ -8,9 +8,12 @@ public class GhostState extends GhostFunction {
 
     private GhostFunction parent;
     private Predicate refinement;
+    private final String file;
 
-    public GhostState(String name, List<CtTypeReference<?>> list, CtTypeReference<?> returnType, String prefix) {
+    public GhostState(String name, List<CtTypeReference<?>> list, CtTypeReference<?> returnType, String prefix,
+            String file) {
         super(name, list, returnType, prefix);
+        this.file = file;
     }
 
     public void setGhostParent(GhostFunction parent) {
@@ -28,4 +31,8 @@ public GhostFunction getParent() {
     public Predicate getRefinement() {
         return refinement;
     }
+
+    public String getFile() {
+        return file;
+    }
 }

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

@@ -8,12 +8,10 @@
 import liquidjava.diagnostics.warnings.ExternalClassNotFoundWarning;
 import liquidjava.diagnostics.warnings.ExternalMethodNotFoundWarning;
 import liquidjava.processor.context.Context;
-import liquidjava.processor.context.ContextHistory;
 import liquidjava.processor.context.GhostFunction;
 import liquidjava.processor.facade.GhostDTO;
 import liquidjava.processor.refinement_checker.general_checkers.MethodsFunctionsChecker;
 import liquidjava.rj_language.Predicate;
-import liquidjava.rj_language.parsing.RefinementsParser;
 import liquidjava.utils.Utils;
 import spoon.reflect.code.CtLiteral;
 import spoon.reflect.cu.SourcePosition;
@@ -31,7 +29,6 @@
 public class ExternalRefinementTypeChecker extends TypeChecker {
     private String prefix;
     private final Diagnostics diagnostics = Diagnostics.getInstance();
-    private final ContextHistory contextHistory = ContextHistory.getInstance();
 
     public ExternalRefinementTypeChecker(Context context, Factory factory) {
         super(context, factory);

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

@@ -154,12 +154,11 @@ private void createStateSet(CtNewArray<String> e, int set, CtElement element) th
                 CtLiteral<String> s = (CtLiteral<String>) ce;
                 String f = s.getValue();
                 GhostState gs = new GhostState(f, g.getParametersTypes(), factory.Type().BOOLEAN_PRIMITIVE,
-                        g.getPrefix());
+                        g.getPrefix(), Utils.getFile(element));
                 gs.setGhostParent(g);
                 gs.setRefinement(Predicate.createEquals(ip, Predicate.createLit(Integer.toString(order), Types.INT)));
                 // open(THIS) -> state1(THIS) == 1
                 context.addToGhostClass(g.getParentClassName(), gs);
-                contextHistory.saveGhost(element, gs);
             }
             order++;
         }
@@ -192,9 +191,8 @@ private void createStateGhost(String string, CtElement element, SourcePosition p
         List<CtTypeReference<?>> param = Collections.singletonList(factory.Type().createReference(qn));
 
         CtTypeReference<?> r = factory.Type().createReference(gd.returnType());
-        GhostState gs = new GhostState(gd.name(), param, r, qn);
+        GhostState gs = new GhostState(gd.name(), param, r, qn, Utils.getFile(element));
         context.addToGhostClass(sn, gs);
-        contextHistory.saveGhost(element, gs);
     }
 
     protected String getQualifiedClassName(CtElement element) {

liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java

@@ -38,6 +38,14 @@ public static String qualifyName(String prefix, String name) {
         return String.format("%s.%s", prefix, name);
     }
 
+    public static String getFile(CtElement element) {
+        SourcePosition pos = element.getPosition();
+        if (pos == null || pos.getFile() == null)
+            return null;
+
+        return pos.getFile().getAbsolutePath();
+    }
+
     public static SourcePosition getLJAnnotationPosition(CtElement element, String refinement) {
         return element.getAnnotations().stream()
                 .filter(a -> isLiquidJavaAnnotation(a) && hasRefinementValue(a, "\"" + refinement + "\"")).findFirst()