Save Ghosts By File

Author: rcosta358

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

@@ -13,16 +13,18 @@ public class ContextHistory {
     private static ContextHistory instance;
 
     private Map<String, Map<String, Set<RefinedVariable>>> vars; // file -> (scope -> variables in scope)
+    private Map<String, Set<GhostState>> ghosts; // file -> ghosts
+
+    // globals
+    private Set<AliasWrapper> aliases;
     private Set<RefinedVariable> instanceVars;
     private Set<RefinedVariable> globalVars;
-    private Set<GhostState> ghosts;
-    private Set<AliasWrapper> aliases;
 
     private ContextHistory() {
         vars = new HashMap<>();
         instanceVars = new HashSet<>();
         globalVars = new HashSet<>();
-        ghosts = new HashSet<>();
+        ghosts = new HashMap<>();
         aliases = new HashSet<>();
     }
 
@@ -41,23 +43,37 @@ public void clearHistory() {
     }
 
     public void saveContext(CtElement element, Context context) {
-        SourcePosition pos = element.getPosition();
-        if (pos == null || pos.getFile() == null)
+        String file = getFile(element);
+        if (file == null)
             return;
 
-        // add variables in scope for this position
-        String file = pos.getFile().getAbsolutePath();
+        // add variables in scope
         String scope = getScopePosition(element);
         vars.putIfAbsent(file, new HashMap<>());
         vars.get(file).put(scope, new HashSet<>(context.getCtxVars()));
 
-        // add other elements in 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) {
         SourcePosition pos = element.getPosition();
         SourcePosition innerPosition = pos;
@@ -81,7 +97,7 @@ public Set<RefinedVariable> getGlobalVars() {
         return globalVars;
     }
 
-    public Set<GhostState> getGhosts() {
+    public Map<String, Set<GhostState>> getGhosts() {
         return ghosts;
     }
 

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

@@ -8,6 +8,7 @@
 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;
@@ -27,8 +28,9 @@
 import spoon.reflect.reference.CtTypeReference;
 
 public class ExternalRefinementTypeChecker extends TypeChecker {
-    String prefix;
-    Diagnostics diagnostics = Diagnostics.getInstance();
+    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

@@ -9,6 +9,7 @@
 import liquidjava.diagnostics.errors.*;
 import liquidjava.processor.context.AliasWrapper;
 import liquidjava.processor.context.Context;
+import liquidjava.processor.context.ContextHistory;
 import liquidjava.processor.context.GhostFunction;
 import liquidjava.processor.context.GhostState;
 import liquidjava.processor.context.RefinedVariable;
@@ -40,6 +41,7 @@ public abstract class TypeChecker extends CtScanner {
     protected final Context context;
     protected final Factory factory;
     protected final VCChecker vcChecker;
+    private final ContextHistory contextHistory = ContextHistory.getInstance();
 
     public TypeChecker(Context context, Factory factory) {
         this.context = context;
@@ -158,6 +160,7 @@ private void createStateSet(CtNewArray<String> e, int set, CtElement element) th
                 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++;
         }
@@ -183,6 +186,7 @@ private void createStateGhost(String string, CtAnnotation<? extends Annotation>
         CtTypeReference<?> r = factory.Type().createReference(gd.returnType());
         GhostState gs = new GhostState(gd.name(), param, r, qn);
         context.addToGhostClass(sn, gs);
+        contextHistory.saveGhost(element, gs);
     }
 
     protected String getQualifiedClassName(CtElement element) {