Code Refactoring (GPT-5)

Author: rcosta358

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

@@ -2,7 +2,6 @@
 
 import java.util.ArrayList;
 import java.util.HashMap;
-import java.util.HashSet;
 import java.util.List;
 import java.util.Set;
 import java.util.Stack;
@@ -113,38 +112,37 @@ public boolean canProcessSubtyping(Predicate type, Predicate expectedType, List<
      */
     private List<GhostState> filterGhostStatesForVariables(List<GhostState> list, List<RefinedVariable> mainVars,
             List<RefinedVariable> vars) {
-        if (list.isEmpty()) return list;
+        if (list.isEmpty())
+            return list;
 
         // Collect all relevant qualified type names from involved variables and their supertypes
-        Set<String> allowedPrefixes = new HashSet<>();
+        if (list == null || list.isEmpty())
+            return list;
+
+        // Collect all relevant qualified type names (types + supertypes), keeping order and deduping
+        Set<String> allowedPrefixes = new java.util.LinkedHashSet<>();
         Consumer<RefinedVariable> collect = rv -> {
-            if (rv.getType() != null)
+            if (rv.getType() != null) {
                 allowedPrefixes.add(rv.getType().getQualifiedName());
+            }
             for (CtTypeReference<?> st : rv.getSuperTypes()) {
-                if (st != null) allowedPrefixes.add(st.getQualifiedName());
+                if (st != null) {
+                    allowedPrefixes.add(st.getQualifiedName());
+                }
             }
         };
         mainVars.forEach(collect);
         vars.forEach(collect);
 
-        // If we couldn't determine any types, return the original list
-        if (allowedPrefixes.isEmpty()) return list;
-
-        // Otherwise filter the list
-        List<GhostState> filtered = new ArrayList<>();
-        for (GhostState g : list) {
-            String prefix;
-            if (g.getParent() != null) {
-                prefix = g.getParent().getPrefix();
-            } else {
-                // Standalone ghosts use their own prefix
-                prefix = g.getPrefix();
-            }
-            if (allowedPrefixes.contains(prefix)) {
-                filtered.add(g);
-            }
-        }
-        // Fallback to original if filtering removed everything
+        if (allowedPrefixes.isEmpty())
+            return list; // avoid over-filtering when types are unknown
+
+        List<GhostState> filtered = list.stream().filter(g -> {
+            String prefix = (g.getParent() != null) ? g.getParent().getPrefix() : g.getPrefix();
+            return allowedPrefixes.contains(prefix);
+        }).collect(Collectors.toList());
+
+        // If nothing matched, keep original to avoid accidental empties
         return filtered.isEmpty() ? list : filtered;
     }
 

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

@@ -212,25 +212,27 @@ private static Predicate getMissingStates(String t, TypeChecker tc, Predicate p)
      * Collect ghost states for the given qualified class name and its immediate supertypes (superclass and interfaces).
      */
     private static List<GhostState> getGhostStatesFor(String qualifiedClass, TypeChecker tc) {
-        List<GhostState> res = new ArrayList<>();
-        String simpleT = Utils.getSimpleName(qualifiedClass);
-        List<GhostState> base = tc.getContext().getGhostState(simpleT);
-        if (base != null)
-            res.addAll(base);
+        // Keep order: class, then superclass, then interfaces; avoid duplicates
+        java.util.LinkedHashSet<String> typeNames = new java.util.LinkedHashSet<>();
+        typeNames.add(Utils.getSimpleName(qualifiedClass));
+
         CtTypeReference<?> ref = tc.getFactory().Type().createReference(qualifiedClass);
         if (ref != null) {
             CtTypeReference<?> sup = ref.getSuperclass();
-            if (sup != null) {
-                List<GhostState> supStates = tc.getContext().getGhostState(Utils.getSimpleName(sup.getQualifiedName()));
-                if (supStates != null)
-                    res.addAll(supStates);
-            }
+            if (sup != null)
+                typeNames.add(Utils.getSimpleName(sup.getQualifiedName()));
             for (CtTypeReference<?> itf : ref.getSuperInterfaces()) {
-                List<GhostState> ifStates = tc.getContext().getGhostState(Utils.getSimpleName(itf.getQualifiedName()));
-                if (ifStates != null)
-                    res.addAll(ifStates);
+                if (itf != null)
+                    typeNames.add(Utils.getSimpleName(itf.getQualifiedName()));
             }
         }
+
+        List<GhostState> res = new ArrayList<>();
+        for (String tn : typeNames) {
+            List<GhostState> states = tc.getContext().getGhostState(tn);
+            if (states != null)
+                res.addAll(states);
+        }
         return res;
     }
 

liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java

@@ -93,8 +93,9 @@ public Expr<?> makeFunctionInvocation(String name, Expr<?>[] params) throws Exce
         if (name.equals("getFromIndex"))
             return makeSelect(name, params);
         FuncDecl<?> fd = funcTranslation.get(name);
-        if (fd == null) fd = resolveFunctionDeclFallback(name, params);
-        
+        if (fd == null)
+            fd = resolveFunctionDeclFallback(name, params);
+
         Sort[] s = fd.getDomain();
         for (int i = 0; i < s.length; i++) {
             Expr<?> param = params[i];
@@ -116,8 +117,8 @@ public Expr<?> makeFunctionInvocation(String name, Expr<?>[] params) throws Exce
 
     /**
      * Fallback resolver for function declarations when an exact qualified name lookup fails. Tries to match by simple
-     * name and number of parameters, preferring an exact qualified-name match if found among candidates; otherwise returns the first
-     * compatible candidate and relies on later coercion via var supertypes.
+     * name and number of parameters, preferring an exact qualified-name match if found among candidates; otherwise
+     * returns the first compatible candidate and relies on later coercion via var supertypes.
      */
     private FuncDecl<?> resolveFunctionDeclFallback(String name, Expr<?>[] params) throws Exception {
         String simple = Utils.getSimpleName(name);