Skip to content

Commit 3f07c62

Browse files
rcosta358rcosta358
committed
Fix AuxStateHandler
1 parent bf0c2ef commit 3f07c62

File tree

4 files changed

+61
-38
lines changed

4 files changed

+61
-38
lines changed

‎liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java‎

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -33,7 +33,10 @@ public static void main(String[] args) {
3333

3434
/**
3535
* Launch the LiquidJava verifier on the given file or directory paths
36-
* @param paths Array of paths to be verified
36+
*
37+
* @param paths
38+
* Array of paths to be verified
39+
*
3740
* @return ErrorEmitter containing any errors found during verification
3841
*/
3942
public static ErrorEmitter launch(String... paths) {

‎liquidjava-verifier/src/main/java/liquidjava/errors/ErrorHandler.java‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -181,7 +181,7 @@ public static void printCostumeError(CtElement element, String msg, ErrorEmitter
181181
sb.append(element + "\n\n");
182182
sb.append("Location: " + element.getPosition() + "\n");
183183
sb.append("______________________________________________________\n");
184-
184+
185185
errorl.addError(s, sb.toString(), element.getPosition(), 1);
186186
}
187187

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

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -119,7 +119,8 @@ private void createStateSet(CtNewArray<String> e, int set, CtElement element) {
119119
CtLiteral<String> s = (CtLiteral<String>) ce;
120120
String f = s.getValue();
121121
if (Character.isUpperCase(f.charAt(0))) {
122-
ErrorHandler.printCostumeError(s, "State name must start with lowercase in '" + f + "'", errorEmitter);
122+
ErrorHandler.printCostumeError(s, "State name must start with lowercase in '" + f + "'",
123+
errorEmitter);
123124
}
124125
}
125126
}

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

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

7474
public static void setDefaultState(RefinedFunction f, TypeChecker tc) {
75-
String[] path = f.getTargetClass().split("\\.");
76-
String klass = path[path.length - 1];
77-
75+
String klass = f.getTargetClass();
7876
Predicate[] s = { Predicate.createVar(tc.THIS) };
7977
Predicate c = new Predicate();
8078
List<GhostFunction> sets = getDifferentSets(tc, klass); // ??
8179
for (GhostFunction sg : sets) {
8280
if (sg.getReturnType().toString().equals("int")) {
83-
Predicate p = Predicate.createEquals(Predicate.createInvocation(sg.getName(), s),
81+
Predicate p = Predicate.createEquals(Predicate.createInvocation(sg.getQualifiedName(), s),
8482
Predicate.createLit("0", Utils.INT));
8583
c = Predicate.createConjunction(c, p);
86-
} else if (sg.getReturnType().toString().equals("boolean")) {
87-
Predicate p = Predicate.createEquals(Predicate.createInvocation(sg.getName(), s),
88-
Predicate.createLit("false", Utils.BOOLEAN));
89-
c = Predicate.createConjunction(c, p);
9084
} else {
9185
// TODO: Implement other stuff
92-
throw new RuntimeException("Ghost Functions not implemented for other types than int/boolean -> implement in"
86+
throw new RuntimeException("Ghost Functions not implemented for other types than int -> implement in"
9387
+ " AuxStateHandler defaultState");
9488
}
9589
}
@@ -100,9 +94,9 @@ public static void setDefaultState(RefinedFunction f, TypeChecker tc) {
10094
f.setAllStates(los);
10195
}
10296

103-
private static List<GhostFunction> getDifferentSets(TypeChecker tc, String klass) {
97+
private static List<GhostFunction> getDifferentSets(TypeChecker tc, String klassQualified) {
10498
List<GhostFunction> sets = new ArrayList<>();
105-
List<GhostState> l = tc.getContext().getGhostState(klass);
99+
List<GhostState> l = getGhostStatesFor(klassQualified, tc);
106100
if (l != null) {
107101
for (GhostState g : l) {
108102
if (g.getParent() == null) {
@@ -124,11 +118,11 @@ private static List<GhostFunction> getDifferentSets(TypeChecker tc, String klass
124118
*
125119
* @throws ParsingException
126120
*/
127-
public static void handleMethodState(CtMethod<?> method, RefinedFunction f, TypeChecker tc)
121+
public static void handleMethodState(CtMethod<?> method, RefinedFunction f, TypeChecker tc, String prefix)
128122
throws ParsingException {
129123
List<CtAnnotation<? extends Annotation>> an = getStateAnnotation(method);
130124
if (!an.isEmpty()) {
131-
setFunctionStates(f, an, tc, method);
125+
setFunctionStates(f, an, tc, method, prefix);
132126
}
133127
// f.setState(an, context.getGhosts(), method);
134128

@@ -145,33 +139,31 @@ public static void handleMethodState(CtMethod<?> method, RefinedFunction f, Type
145139
* @throws ParsingException
146140
*/
147141
private static void setFunctionStates(RefinedFunction f, List<CtAnnotation<? extends Annotation>> anns,
148-
TypeChecker tc, CtElement element) throws ParsingException {
142+
TypeChecker tc, CtElement element, String prefix) throws ParsingException {
149143
List<ObjectState> l = new ArrayList<>();
150144
for (CtAnnotation<? extends Annotation> an : anns) {
151-
l.add(getStates(an, f, tc, element));
145+
l.add(getStates(an, f, tc, element, prefix));
152146
}
153147
f.setAllStates(l);
154148
}
155149

156150
@SuppressWarnings({ "rawtypes" })
157151
private static ObjectState getStates(CtAnnotation<? extends Annotation> ctAnnotation, RefinedFunction f,
158-
TypeChecker tc, CtElement e) throws ParsingException {
152+
TypeChecker tc, CtElement e, String prefix) throws ParsingException {
159153
Map<String, CtExpression> m = ctAnnotation.getAllValues();
160154
String from = TypeCheckingUtils.getStringFromAnnotation(m.get("from"));
161155
String to = TypeCheckingUtils.getStringFromAnnotation(m.get("to"));
162156
ObjectState state = new ObjectState();
163-
if (from != null) // has From
164-
{
165-
state.setFrom(createStatePredicate(from, f.getTargetClass(), tc, e, false));
157+
if (from != null) { // has From
158+
state.setFrom(createStatePredicate(from, f.getTargetClass(), tc, e, false, prefix));
166159
}
167-
if (to != null) // has To
168-
{
169-
state.setTo(createStatePredicate(to, f.getTargetClass(), tc, e, true));
160+
if (to != null) { // has To
161+
state.setTo(createStatePredicate(to, f.getTargetClass(), tc, e, true, prefix));
170162
}
171163

172164
if (from != null && to == null) // has From but not To -> the state remains the same
173165
{
174-
state.setTo(createStatePredicate(from, f.getTargetClass(), tc, e, true));
166+
state.setTo(createStatePredicate(from, f.getTargetClass(), tc, e, true, prefix));
175167
}
176168
if (from == null && to != null) // has To but not From -> enters with true and exists with a specific state
177169
{
@@ -181,8 +173,8 @@ private static ObjectState getStates(CtAnnotation<? extends Annotation> ctAnnota
181173
}
182174

183175
private static Predicate createStatePredicate(String value, /* RefinedFunction f */ String targetClass,
184-
TypeChecker tc, CtElement e, boolean isTo) throws ParsingException {
185-
Predicate p = new Predicate(value, e, tc.getErrorEmitter());
176+
TypeChecker tc, CtElement e, boolean isTo, String prefix) throws ParsingException {
177+
Predicate p = new Predicate(value, e, tc.getErrorEmitter(), prefix);
186178
String t = targetClass; // f.getTargetClass();
187179
CtTypeReference<?> r = tc.getFactory().Type().createReference(t);
188180

@@ -204,10 +196,8 @@ private static Predicate createStatePredicate(String value, /* RefinedFunction f
204196
}
205197

206198
private static Predicate getMissingStates(String t, TypeChecker tc, Predicate p) {
207-
String[] temp = t.split("\\.");
208-
String simpleT = temp[temp.length - 1];
209-
List<GhostState> gs = p.getStateInvocations(tc.getContext().getGhostState(simpleT));
210-
List<GhostFunction> sets = getDifferentSets(tc, simpleT);
199+
List<GhostState> gs = p.getStateInvocations(getGhostStatesFor(t, tc));
200+
List<GhostFunction> sets = getDifferentSets(tc, t);
211201
for (GhostState g : gs) {
212202
if (g.getParent() == null && sets.contains(g)) {
213203
sets.remove(g);
@@ -218,6 +208,34 @@ private static Predicate getMissingStates(String t, TypeChecker tc, Predicate p)
218208
return addOldStates(p, Predicate.createVar(tc.THIS), sets, tc);
219209
}
220210

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+
221239
/**
222240
* Create predicate with the equalities with previous versions of the object e.g., ghostfunction1(this) ==
223241
* ghostfunction1(old(this))
@@ -233,8 +251,8 @@ private static Predicate addOldStates(Predicate p, Predicate th, List<GhostFunct
233251
Predicate c = p;
234252
for (GhostFunction gf : sets) {
235253
Predicate eq = Predicate.createEquals( // gf.name == old(gf.name(this))
236-
Predicate.createInvocation(gf.getName(), th),
237-
Predicate.createInvocation(gf.getName(), Predicate.createInvocation(Utils.OLD, th)));
254+
Predicate.createInvocation(gf.getQualifiedName(), th),
255+
Predicate.createInvocation(gf.getQualifiedName(), Predicate.createInvocation(Utils.OLD, th)));
238256
c = Predicate.createConjunction(c, eq);
239257
}
240258
return c;
@@ -334,7 +352,6 @@ public static void updateGhostField(CtFieldWrite<?> fw, TypeChecker tc) {
334352
}
335353

336354
VariableInstance vi = invocation_callee.get();
337-
338355
String instanceName = vi.getName();
339356
Predicate prevState = vi.getRefinement().substituteVariable(tc.WILD_VAR, instanceName)
340357
.substituteVariable(parentTargetName, instanceName);
@@ -344,8 +361,10 @@ public static void updateGhostField(CtFieldWrite<?> fw, TypeChecker tc) {
344361

345362
ObjectState stateChange = new ObjectState();
346363
try {
347-
Predicate fromPredicate = createStatePredicate(stateChangeRefinementFrom, targetClass, tc, fw, false);
348-
Predicate toPredicate = createStatePredicate(stateChangeRefinementTo, targetClass, tc, fw, true);
364+
String prefix = field.getDeclaringType().getQualifiedName();
365+
Predicate fromPredicate = createStatePredicate(stateChangeRefinementFrom, targetClass, tc, fw, false,
366+
prefix);
367+
Predicate toPredicate = createStatePredicate(stateChangeRefinementTo, targetClass, tc, fw, true, prefix);
349368
stateChange.setFrom(fromPredicate);
350369
stateChange.setTo(toPredicate);
351370
} catch (ParsingException e) {
@@ -612,4 +631,4 @@ private static List<CtAnnotation<? extends Annotation>> getStateAnnotation(CtEle
612631
// }
613632
// return l;
614633
}
615-
}
634+
}

0 commit comments

Comments
 (0)