Skip to content

Commit b8d5efb

Browse files
rcosta358rcosta358
committed
Fix Ghost Name Resolution (GPT-5)
1 parent 52a32a5 commit b8d5efb

8 files changed

Lines changed: 151 additions & 24 deletions

File tree

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

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -86,7 +86,10 @@ private String getParentClassName(String pref) {
8686
return Utils.getSimpleName(pref);
8787
}
8888

89+
// Match by fully qualified name, exact simple name or by comparing the simple name of the provided identifier
90+
// This allows references written in a different class (different prefix) to still match
8991
public boolean matches(String name) {
90-
return this.name.equals(name) || this.getQualifiedName().equals(name);
92+
return this.getQualifiedName().equals(name) || this.name.equals(name)
93+
|| this.name.equals(Utils.getSimpleName(name));
9194
}
9295
}

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

Lines changed: 52 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -2,8 +2,11 @@
22

33
import java.util.ArrayList;
44
import java.util.HashMap;
5+
import java.util.HashSet;
56
import java.util.List;
7+
import java.util.Set;
68
import java.util.Stack;
9+
import java.util.function.Consumer;
710
import java.util.regex.Pattern;
811
import java.util.stream.Collectors;
912
import liquidjava.errors.ErrorEmitter;
@@ -20,6 +23,7 @@
2023
import spoon.reflect.cu.SourcePosition;
2124
import spoon.reflect.declaration.CtElement;
2225
import spoon.reflect.factory.Factory;
26+
import spoon.reflect.reference.CtTypeReference;
2327

2428
public class VCChecker {
2529
private final Context context;
@@ -47,10 +51,11 @@ public void processSubtyping(Predicate expectedType, List<GhostState> list, Stri
4751
Predicate premises = new Predicate();
4852
Predicate et = new Predicate();
4953
try {
50-
premises = premisesBeforeChange.changeStatesToRefinements(list, s, errorEmitter)
54+
List<GhostState> filtered = filterGhostStatesForVariables(list, mainVars, lrv);
55+
premises = premisesBeforeChange.changeStatesToRefinements(filtered, s, errorEmitter)
5156
.changeAliasToRefinement(context, f);
5257

53-
et = expectedType.changeStatesToRefinements(list, s, errorEmitter).changeAliasToRefinement(context, f);
58+
et = expectedType.changeStatesToRefinements(filtered, s, errorEmitter).changeAliasToRefinement(context, f);
5459
} catch (Exception e1) {
5560
printError(premises, expectedType, element, map, e1.getMessage());
5661
return;
@@ -87,9 +92,10 @@ public boolean canProcessSubtyping(Predicate type, Predicate expectedType, List<
8792
Predicate et = new Predicate();
8893
try {
8994
premises = joinPredicates(expectedType, mainVars, lrv, map).toConjunctions();
90-
premises = Predicate.createConjunction(premises, type).changeStatesToRefinements(list, s, errorEmitter)
95+
List<GhostState> filtered = filterGhostStatesForVariables(list, mainVars, lrv);
96+
premises = Predicate.createConjunction(premises, type).changeStatesToRefinements(filtered, s, errorEmitter)
9197
.changeAliasToRefinement(context, f);
92-
et = expectedType.changeStatesToRefinements(list, s, errorEmitter).changeAliasToRefinement(context, f);
98+
et = expectedType.changeStatesToRefinements(filtered, s, errorEmitter).changeAliasToRefinement(context, f);
9399
} catch (Exception e) {
94100
return false;
95101
// printError(premises, expectedType, element, map, e.getMessage());
@@ -100,6 +106,48 @@ public boolean canProcessSubtyping(Predicate type, Predicate expectedType, List<
100106
return smtChecks(premises, et, p);
101107
}
102108

109+
/**
110+
* Reduce the ghost states list to those whose declaring class (prefix) matches any of the involved variable types
111+
* or their supertypes This prevents ambiguous simple name substitutions across unrelated classes that share state
112+
* names
113+
*/
114+
private List<GhostState> filterGhostStatesForVariables(List<GhostState> list, List<RefinedVariable> mainVars,
115+
List<RefinedVariable> vars) {
116+
if (list.isEmpty()) return list;
117+
118+
// Collect all relevant qualified type names from involved variables and their supertypes
119+
Set<String> allowedPrefixes = new HashSet<>();
120+
Consumer<RefinedVariable> collect = rv -> {
121+
if (rv.getType() != null)
122+
allowedPrefixes.add(rv.getType().getQualifiedName());
123+
for (CtTypeReference<?> st : rv.getSuperTypes()) {
124+
if (st != null) allowedPrefixes.add(st.getQualifiedName());
125+
}
126+
};
127+
mainVars.forEach(collect);
128+
vars.forEach(collect);
129+
130+
// If we couldn't determine any types, return the original list
131+
if (allowedPrefixes.isEmpty()) return list;
132+
133+
// Otherwise filter the list
134+
List<GhostState> filtered = new ArrayList<>();
135+
for (GhostState g : list) {
136+
String prefix;
137+
if (g.getParent() != null) {
138+
prefix = g.getParent().getPrefix();
139+
} else {
140+
// Standalone ghosts use their own prefix
141+
prefix = g.getPrefix();
142+
}
143+
if (allowedPrefixes.contains(prefix)) {
144+
filtered.add(g);
145+
}
146+
}
147+
// Fallback to original if filtering removed everything
148+
return filtered.isEmpty() ? list : filtered;
149+
}
150+
103151
private VCImplication joinPredicates(Predicate expectedType, List<RefinedVariable> mainVars,
104152
List<RefinedVariable> vars, HashMap<String, PlacementInCode> map) {
105153

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

Lines changed: 31 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -72,7 +72,7 @@ private static void setConstructorStates(RefinedFunction f, List<CtAnnotation<?
7272
}
7373

7474
public static void setDefaultState(RefinedFunction f, TypeChecker tc) {
75-
String klass = Utils.getSimpleName(f.getTargetClass());
75+
String klass = f.getTargetClass();
7676
Predicate[] s = { Predicate.createVar(tc.THIS) };
7777
Predicate c = new Predicate();
7878
List<GhostFunction> sets = getDifferentSets(tc, klass); // ??
@@ -94,9 +94,9 @@ public static void setDefaultState(RefinedFunction f, TypeChecker tc) {
9494
f.setAllStates(los);
9595
}
9696

97-
private static List<GhostFunction> getDifferentSets(TypeChecker tc, String klass) {
97+
private static List<GhostFunction> getDifferentSets(TypeChecker tc, String klassQualified) {
9898
List<GhostFunction> sets = new ArrayList<>();
99-
List<GhostState> l = tc.getContext().getGhostState(klass);
99+
List<GhostState> l = getGhostStatesFor(klassQualified, tc);
100100
if (l != null) {
101101
for (GhostState g : l) {
102102
if (g.getParent() == null) {
@@ -196,9 +196,8 @@ private static Predicate createStatePredicate(String value, /* RefinedFunction f
196196
}
197197

198198
private static Predicate getMissingStates(String t, TypeChecker tc, Predicate p) {
199-
String simpleT = Utils.getSimpleName(t);
200-
List<GhostState> gs = p.getStateInvocations(tc.getContext().getGhostState(simpleT));
201-
List<GhostFunction> sets = getDifferentSets(tc, simpleT);
199+
List<GhostState> gs = p.getStateInvocations(getGhostStatesFor(t, tc));
200+
List<GhostFunction> sets = getDifferentSets(tc, t);
202201
for (GhostState g : gs) {
203202
if (g.getParent() == null && sets.contains(g)) {
204203
sets.remove(g);
@@ -209,6 +208,32 @@ private static Predicate getMissingStates(String t, TypeChecker tc, Predicate p)
209208
return addOldStates(p, Predicate.createVar(tc.THIS), sets, tc);
210209
}
211210

211+
/**
212+
* Collect ghost states for the given qualified class name and its immediate supertypes (superclass and interfaces).
213+
*/
214+
private static List<GhostState> getGhostStatesFor(String qualifiedClass, TypeChecker tc) {
215+
List<GhostState> res = new ArrayList<>();
216+
String simpleT = Utils.getSimpleName(qualifiedClass);
217+
List<GhostState> base = tc.getContext().getGhostState(simpleT);
218+
if (base != null)
219+
res.addAll(base);
220+
CtTypeReference<?> ref = tc.getFactory().Type().createReference(qualifiedClass);
221+
if (ref != null) {
222+
CtTypeReference<?> sup = ref.getSuperclass();
223+
if (sup != null) {
224+
List<GhostState> supStates = tc.getContext().getGhostState(Utils.getSimpleName(sup.getQualifiedName()));
225+
if (supStates != null)
226+
res.addAll(supStates);
227+
}
228+
for (CtTypeReference<?> itf : ref.getSuperInterfaces()) {
229+
List<GhostState> ifStates = tc.getContext().getGhostState(Utils.getSimpleName(itf.getQualifiedName()));
230+
if (ifStates != null)
231+
res.addAll(ifStates);
232+
}
233+
}
234+
return res;
235+
}
236+
212237
/**
213238
* Create predicate with the equalities with previous versions of the object e.g., ghostfunction1(this) ==
214239
* ghostfunction1(old(this))

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

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -185,6 +185,9 @@ public Predicate changeStatesToRefinements(List<GhostState> ghostState, String[]
185185
String name = gs.getQualifiedName();
186186
Expression exp = innerParse(gs.getRefinement().toString(), ee, gs.getPrefix());
187187
nameRefinementMap.put(name, exp);
188+
// Also allow simple name lookup to enable hierarchy matching
189+
String simple = Utils.getSimpleName(name);
190+
nameRefinementMap.putIfAbsent(simple, exp);
188191
}
189192
}
190193
Expression e = exp.substituteState(nameRefinementMap, toChange);

‎liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Expression.java‎

Lines changed: 11 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -8,6 +8,7 @@
88
import liquidjava.processor.facade.AliasDTO;
99
import liquidjava.rj_language.ast.typing.TypeInfer;
1010
import liquidjava.smt.TranslatorToZ3;
11+
import liquidjava.utils.Utils;
1112
import spoon.reflect.factory.Factory;
1213

1314
public abstract class Expression {
@@ -98,10 +99,13 @@ public Expression substituteState(Map<String, Expression> subMap, String[] toCha
9899
Expression e = clone();
99100
if (this instanceof FunctionInvocation) {
100101
FunctionInvocation fi = (FunctionInvocation) this;
101-
if (subMap.containsKey(fi.name) && fi.children.size() == 1 && fi.children.get(0) instanceof Var) { // object
102+
String key = fi.name;
103+
String simple = Utils.getSimpleName(key);
104+
boolean has = subMap.containsKey(key) || subMap.containsKey(simple);
105+
if (has && fi.children.size() == 1 && fi.children.get(0) instanceof Var) { // object
102106
// state
103107
Var v = (Var) fi.children.get(0);
104-
Expression sub = subMap.get(fi.name).clone();
108+
Expression sub = (subMap.containsKey(key) ? subMap.get(key) : subMap.get(simple)).clone();
105109
for (String s : toChange) {
106110
sub = sub.substitute(new Var(s), v);
107111
}
@@ -119,10 +123,13 @@ private void auxSubstituteState(Map<String, Expression> subMap, String[] toChang
119123
Expression exp = children.get(i);
120124
if (exp instanceof FunctionInvocation) {
121125
FunctionInvocation fi = (FunctionInvocation) exp;
122-
if (subMap.containsKey(fi.name) && fi.children.size() == 1 && fi.children.get(0) instanceof Var) { // object
126+
String key = fi.name;
127+
String simple = Utils.getSimpleName(key);
128+
boolean has = subMap.containsKey(key) || subMap.containsKey(simple);
129+
if (has && fi.children.size() == 1 && fi.children.get(0) instanceof Var) { // object
123130
// state
124131
Var v = (Var) fi.children.get(0);
125-
Expression sub = subMap.get(fi.name).clone();
132+
Expression sub = (subMap.containsKey(key) ? subMap.get(key) : subMap.get(simple)).clone();
126133
for (String s : toChange) {
127134
sub = sub.substitute(new Var(s), v);
128135
}

‎liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/FunctionInvocation.java‎

Lines changed: 13 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,7 @@
55
import java.util.List;
66
import java.util.stream.Collectors;
77
import liquidjava.smt.TranslatorToZ3;
8+
import liquidjava.utils.Utils;
89

910
public class FunctionInvocation extends Expression {
1011
String name;
@@ -50,8 +51,18 @@ public void getVariableNames(List<String> toAdd) {
5051

5152
@Override
5253
public void getStateInvocations(List<String> toAdd, List<String> all) {
53-
if (!toAdd.contains(name) && all.contains(name))
54-
toAdd.add(name);
54+
if (!toAdd.contains(name)) {
55+
// Accept either qualified or simple name
56+
if (all.contains(name)) {
57+
toAdd.add(name);
58+
} else {
59+
String simple = Utils.getSimpleName(name);
60+
boolean matchesSimple = all.stream()
61+
.anyMatch(s -> s.equals(simple) || (s.contains(".") && Utils.getSimpleName(s).equals(simple)));
62+
if (matchesSimple)
63+
toAdd.add(name);
64+
}
65+
}
5566
for (Expression e : getArgs())
5667
e.getStateInvocations(toAdd, all);
5768
}

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

Lines changed: 35 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -17,6 +17,8 @@
1717
import java.util.List;
1818
import java.util.Map;
1919
import liquidjava.processor.context.AliasWrapper;
20+
import liquidjava.utils.Utils;
21+
2022
import org.apache.commons.lang3.NotImplementedException;
2123

2224
public class TranslatorToZ3 implements AutoCloseable {
@@ -90,11 +92,9 @@ public Expr<?> makeFunctionInvocation(String name, Expr<?>[] params) throws Exce
9092
return makeStore(name, params);
9193
if (name.equals("getFromIndex"))
9294
return makeSelect(name, params);
93-
94-
if (!funcTranslation.containsKey(name))
95-
throw new NotFoundError("Function '" + name + "' not found");
96-
9795
FuncDecl<?> fd = funcTranslation.get(name);
96+
if (fd == null) fd = resolveFunctionDeclFallback(name, params);
97+
9898
Sort[] s = fd.getDomain();
9999
for (int i = 0; i < s.length; i++) {
100100
Expr<?> param = params[i];
@@ -114,6 +114,37 @@ public Expr<?> makeFunctionInvocation(String name, Expr<?>[] params) throws Exce
114114
return z3.mkApp(fd, params);
115115
}
116116

117+
/**
118+
* Fallback resolver for function declarations when an exact qualified name lookup fails. Tries to match by simple
119+
* name and number of parameters, preferring an exact qualified-name match if found among candidates; otherwise returns the first
120+
* compatible candidate and relies on later coercion via var supertypes.
121+
*/
122+
private FuncDecl<?> resolveFunctionDeclFallback(String name, Expr<?>[] params) throws Exception {
123+
String simple = Utils.getSimpleName(name);
124+
FuncDecl<?> candidate = null;
125+
for (Map.Entry<String, FuncDecl<?>> entry : funcTranslation.entrySet()) {
126+
String k = entry.getKey();
127+
String simpleK = Utils.getSimpleName(k);
128+
if (simple.equals(simpleK)) {
129+
FuncDecl<?> fTry = entry.getValue();
130+
Sort[] dom = fTry.getDomain();
131+
if (dom.length == params.length) {
132+
// Prefer exact qualified name match if available
133+
if (k.equals(name)) {
134+
candidate = fTry;
135+
break;
136+
}
137+
// Otherwise first compatible match
138+
candidate = fTry;
139+
}
140+
}
141+
}
142+
if (candidate != null) {
143+
return candidate;
144+
}
145+
throw new NotFoundError("Function '" + name + "' not found");
146+
}
147+
117148
@SuppressWarnings({ "unchecked", "rawtypes" })
118149
private Expr<?> makeSelect(String name, Expr<?>[] params) {
119150
if (params.length == 2 && params[0] instanceof ArrayExpr)

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

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -59,9 +59,8 @@ public static CtTypeReference<?> getType(String type, Factory factory) {
5959
}
6060
}
6161

62-
public static String getSimpleName(String qualifiedName) {
63-
String[] parts = qualifiedName.split("\\.");
64-
return parts[parts.length - 1];
62+
public static String getSimpleName(String name) {
63+
return name.contains(".") ? name.substring(name.lastIndexOf('.') + 1) : name;
6564
}
6665

6766
public static String qualifyName(String prefix, String name) {

0 commit comments

Comments
 (0)