Skip to content

Commit 0a4b338

Browse files
rcosta358rcosta358
authored
Merge pull request #3 from rcosta358/fix-ghost-name-resolution
Fix Ghost Name Resolution
2 parents f84a138 + 52fcd80 commit 0a4b338

8 files changed

Lines changed: 152 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: 50 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,9 @@
33
import java.util.ArrayList;
44
import java.util.HashMap;
55
import java.util.List;
6+
import java.util.Set;
67
import java.util.Stack;
8+
import java.util.function.Consumer;
79
import java.util.regex.Pattern;
810
import java.util.stream.Collectors;
911
import liquidjava.errors.ErrorEmitter;
@@ -20,6 +22,7 @@
2022
import spoon.reflect.cu.SourcePosition;
2123
import spoon.reflect.declaration.CtElement;
2224
import spoon.reflect.factory.Factory;
25+
import spoon.reflect.reference.CtTypeReference;
2326

2427
public class VCChecker {
2528
private final Context context;
@@ -47,10 +50,11 @@ public void processSubtyping(Predicate expectedType, List<GhostState> list, Stri
4750
Predicate premises = new Predicate();
4851
Predicate et = new Predicate();
4952
try {
50-
premises = premisesBeforeChange.changeStatesToRefinements(list, s, errorEmitter)
53+
List<GhostState> filtered = filterGhostStatesForVariables(list, mainVars, lrv);
54+
premises = premisesBeforeChange.changeStatesToRefinements(filtered, s, errorEmitter)
5155
.changeAliasToRefinement(context, f);
5256

53-
et = expectedType.changeStatesToRefinements(list, s, errorEmitter).changeAliasToRefinement(context, f);
57+
et = expectedType.changeStatesToRefinements(filtered, s, errorEmitter).changeAliasToRefinement(context, f);
5458
} catch (Exception e1) {
5559
printError(premises, expectedType, element, map, e1.getMessage());
5660
return;
@@ -87,9 +91,10 @@ public boolean canProcessSubtyping(Predicate type, Predicate expectedType, List<
8791
Predicate et = new Predicate();
8892
try {
8993
premises = joinPredicates(expectedType, mainVars, lrv, map).toConjunctions();
90-
premises = Predicate.createConjunction(premises, type).changeStatesToRefinements(list, s, errorEmitter)
94+
List<GhostState> filtered = filterGhostStatesForVariables(list, mainVars, lrv);
95+
premises = Predicate.createConjunction(premises, type).changeStatesToRefinements(filtered, s, errorEmitter)
9196
.changeAliasToRefinement(context, f);
92-
et = expectedType.changeStatesToRefinements(list, s, errorEmitter).changeAliasToRefinement(context, f);
97+
et = expectedType.changeStatesToRefinements(filtered, s, errorEmitter).changeAliasToRefinement(context, f);
9398
} catch (Exception e) {
9499
return false;
95100
// printError(premises, expectedType, element, map, e.getMessage());
@@ -100,6 +105,47 @@ public boolean canProcessSubtyping(Predicate type, Predicate expectedType, List<
100105
return smtChecks(premises, et, p);
101106
}
102107

108+
/**
109+
* Reduce the ghost states list to those whose declaring class (prefix) matches any of the involved variable types
110+
* or their supertypes This prevents ambiguous simple name substitutions across unrelated classes that share state
111+
* names
112+
*/
113+
private List<GhostState> filterGhostStatesForVariables(List<GhostState> list, List<RefinedVariable> mainVars,
114+
List<RefinedVariable> vars) {
115+
if (list.isEmpty())
116+
return list;
117+
118+
// Collect all relevant qualified type names from involved variables and their supertypes
119+
if (list == null || list.isEmpty())
120+
return list;
121+
122+
// Collect all relevant qualified type names (types + supertypes), keeping order and deduping
123+
Set<String> allowedPrefixes = new java.util.LinkedHashSet<>();
124+
Consumer<RefinedVariable> collect = rv -> {
125+
if (rv.getType() != null) {
126+
allowedPrefixes.add(rv.getType().getQualifiedName());
127+
}
128+
for (CtTypeReference<?> st : rv.getSuperTypes()) {
129+
if (st != null) {
130+
allowedPrefixes.add(st.getQualifiedName());
131+
}
132+
}
133+
};
134+
mainVars.forEach(collect);
135+
vars.forEach(collect);
136+
137+
if (allowedPrefixes.isEmpty())
138+
return list; // avoid over-filtering when types are unknown
139+
140+
List<GhostState> filtered = list.stream().filter(g -> {
141+
String prefix = (g.getParent() != null) ? g.getParent().getPrefix() : g.getPrefix();
142+
return allowedPrefixes.contains(prefix);
143+
}).collect(Collectors.toList());
144+
145+
// If nothing matched, keep original to avoid accidental empties
146+
return filtered.isEmpty() ? list : filtered;
147+
}
148+
103149
private VCImplication joinPredicates(Predicate expectedType, List<RefinedVariable> mainVars,
104150
List<RefinedVariable> vars, HashMap<String, PlacementInCode> map) {
105151

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

Lines changed: 33 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,34 @@ 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+
// Keep order: class, then superclass, then interfaces; avoid duplicates
216+
java.util.LinkedHashSet<String> typeNames = new java.util.LinkedHashSet<>();
217+
typeNames.add(Utils.getSimpleName(qualifiedClass));
218+
219+
CtTypeReference<?> ref = tc.getFactory().Type().createReference(qualifiedClass);
220+
if (ref != null) {
221+
CtTypeReference<?> sup = ref.getSuperclass();
222+
if (sup != null)
223+
typeNames.add(Utils.getSimpleName(sup.getQualifiedName()));
224+
for (CtTypeReference<?> itf : ref.getSuperInterfaces()) {
225+
if (itf != null)
226+
typeNames.add(Utils.getSimpleName(itf.getQualifiedName()));
227+
}
228+
}
229+
230+
List<GhostState> res = new ArrayList<>();
231+
for (String tn : typeNames) {
232+
List<GhostState> states = tc.getContext().getGhostState(tn);
233+
if (states != null)
234+
res.addAll(states);
235+
}
236+
return res;
237+
}
238+
212239
/**
213240
* Create predicate with the equalities with previous versions of the object e.g., ghostfunction1(this) ==
214241
* 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: 36 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,10 @@ 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)
97+
fd = resolveFunctionDeclFallback(name, params);
98+
9899
Sort[] s = fd.getDomain();
99100
for (int i = 0; i < s.length; i++) {
100101
Expr<?> param = params[i];
@@ -114,6 +115,37 @@ public Expr<?> makeFunctionInvocation(String name, Expr<?>[] params) throws Exce
114115
return z3.mkApp(fd, params);
115116
}
116117

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