Skip to content

Commit ec170de

Browse files
rcosta358rcosta358
authored
Fix Diagnostic Positions (#185)
1 parent 2eb9510 commit ec170de

6 files changed

Lines changed: 57 additions & 27 deletions

File tree

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -47,7 +47,7 @@ public <T> void visitCtInterface(CtInterface<T> intrface) {
4747
this.prefix = literal.getValue();
4848
if (!classExists(prefix)) {
4949
String message = String.format("Could not find class '%s'", prefix);
50-
diagnostics.add(new ExternalClassNotFoundWarning(externalRef.get().getPosition(), message, prefix));
50+
diagnostics.add(new ExternalClassNotFoundWarning(literal.getPosition(), message, prefix));
5151
return;
5252
}
5353
getRefinementFromAnnotation(intrface);

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

Lines changed: 11 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -70,12 +70,14 @@ public Optional<Predicate> getRefinementFromAnnotation(CtElement element) throws
7070
ref = Optional.of(value);
7171

7272
} else if (an.contentEquals("liquidjava.specification.RefinementPredicate")) {
73-
String value = getStringFromAnnotation(ann.getValue("value"));
74-
getGhostFunction(value, element, ann.getPosition());
73+
CtExpression<String> rawValue = ann.getValue("value");
74+
String value = getStringFromAnnotation(rawValue);
75+
getGhostFunction(value, element, rawValue.getPosition());
7576

7677
} else if (an.contentEquals("liquidjava.specification.RefinementAlias")) {
77-
String value = getStringFromAnnotation(ann.getValue("value"));
78-
handleAlias(value, element, ann.getPosition());
78+
CtExpression<String> rawValue = ann.getValue("value");
79+
String value = getStringFromAnnotation(rawValue);
80+
handleAlias(value, element, rawValue.getPosition());
7981
}
8082
}
8183
if (ref.isPresent()) {
@@ -116,7 +118,7 @@ public void handleStateSetsFromAnnotation(CtElement element) throws LJError {
116118
}
117119
if (an.contentEquals("liquidjava.specification.Ghost")) {
118120
CtLiteral<String> s = (CtLiteral<String>) ann.getAllValues().get("value");
119-
createStateGhost(s.getValue(), element, ann.getPosition());
121+
createStateGhost(s.getValue(), element, s.getPosition());
120122
}
121123
}
122124
}
@@ -167,7 +169,8 @@ protected GhostDTO getGhostDeclaration(String value, SourcePosition position) th
167169
return RefinementsParser.parseGhostDeclaration(value);
168170
} catch (LJError e) {
169171
// add location info to error
170-
e.setPosition(position);
172+
if (e.getPosition() == null)
173+
e.setPosition(position);
171174
throw e;
172175
}
173176
}
@@ -259,7 +262,8 @@ protected void handleAlias(String ref, CtElement element, SourcePosition positio
259262
}
260263
} catch (LJError e) {
261264
// add location info to error
262-
e.setPosition(position);
265+
if (e.getPosition() == null)
266+
e.setPosition(position);
263267
throw e;
264268
}
265269
}

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

Lines changed: 10 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -20,6 +20,7 @@
2020
import liquidjava.smt.Counterexample;
2121
import liquidjava.smt.SMTEvaluator;
2222
import liquidjava.smt.SMTResult;
23+
import liquidjava.utils.Utils;
2324
import liquidjava.utils.constants.Keys;
2425
import spoon.reflect.cu.SourcePosition;
2526
import spoon.reflect.declaration.CtElement;
@@ -58,10 +59,14 @@ public void processSubtyping(Predicate expectedType, List<GhostState> list, CtEl
5859
expected = expectedType.changeStatesToRefinements(filtered, s).changeAliasToRefinement(context, f);
5960
} catch (LJError e) {
6061
// add location info to error
61-
e.setPosition(element.getPosition());
62+
if (e.getPosition() == null) {
63+
SourcePosition pos = Utils.getFirstLJAnnotationValuePosition(element);
64+
e.setPosition(pos);
65+
}
6266
throw e;
6367
}
64-
SMTResult result = verifySMTSubtype(expected, premises, element.getPosition());
68+
SourcePosition annotationValuePos = Utils.getFirstLJAnnotationValuePosition(element);
69+
SMTResult result = verifySMTSubtype(expected, premises, annotationValuePos);
6570
if (result.isError()) {
6671
throw new RefinementError(element.getPosition(), expectedType.simplify(context),
6772
premisesBeforeChange.simplify(context), map, result.getCounterexample(), customMessage);
@@ -99,7 +104,9 @@ public SMTResult verifySMTSubtype(Predicate expected, Predicate found, SourcePos
99104
try {
100105
return new SMTEvaluator().verifySubtype(found, expected, context);
101106
} catch (LJError e) {
102-
e.setPosition(position);
107+
if (e.getPosition() == null) {
108+
e.setPosition(position);
109+
}
103110
throw e;
104111
} catch (Exception e) {
105112
throw new CustomError(e.getMessage(), position);

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

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -225,7 +225,8 @@ private static Predicate createStatePredicate(String value, String targetClass,
225225
c = c.changeOldMentions(nameOld, name);
226226
boolean ok = tc.checkStateSMT(new Predicate(), c.negate(), e.getPosition());
227227
if (ok) {
228-
tc.throwStateConflictError(e.getPosition(), p);
228+
SourcePosition pos = Utils.getLJAnnotationPosition(e, value);
229+
tc.throwStateConflictError(pos, p);
229230
}
230231
return c1;
231232
}

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

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -86,8 +86,10 @@ protected Expression parse(String ref, CtElement element) throws LJError {
8686
return RefinementsParser.createAST(ref, prefix);
8787
} catch (LJError e) {
8888
// add location info to error
89-
SourcePosition pos = Utils.getLJAnnotationPosition(element, ref);
90-
e.setPosition(pos);
89+
if (e.getPosition() == null) {
90+
SourcePosition pos = Utils.getLJAnnotationPosition(element, ref);
91+
e.setPosition(pos);
92+
}
9193
throw e;
9294
}
9395
}

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

Lines changed: 29 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,6 @@
11
package liquidjava.utils;
22

3+
import java.util.List;
34
import java.util.Map;
45
import java.util.Set;
56
import java.util.stream.Stream;
@@ -22,6 +23,7 @@
2223
public class Utils {
2324

2425
private static final Set<String> DEFAULT_NAMES = Set.of("old", "length", "addToIndex", "getFromIndex");
26+
private static final List<String> REFINEMENT_KEYS = List.of("value", "to", "from");
2527

2628
public static CtTypeReference<?> getType(String type, Factory factory) {
2729
// TODO: complete with other types
@@ -54,28 +56,42 @@ public static String getFile(CtElement element) {
5456
return pos.getFile().getAbsolutePath();
5557
}
5658

57-
public static SourcePosition getLJAnnotationPosition(CtElement element, String refinement) {
58-
return element.getAnnotations().stream()
59-
.filter(a -> isLiquidJavaAnnotation(a) && hasRefinementValue(a, "\"" + refinement + "\"")).findFirst()
60-
.map(CtElement::getPosition).orElse(element.getPosition());
59+
// Get the position of the annotation with the given value
60+
public static SourcePosition getLJAnnotationPosition(CtElement element, String value) {
61+
String quotedValue = "\"" + value + "\"";
62+
return getLiquidJavaAnnotations(element)
63+
.flatMap(annotation -> getLJAnnotationValues(annotation)
64+
.filter(expr -> quotedValue.equals(expr.toString()))
65+
.map(expr -> expr.getPosition() != null ? expr.getPosition() : annotation.getPosition()))
66+
.findFirst().orElse(element.getPosition());
6167
}
6268

69+
// Get the position of the first LJ annotation on the element
6370
public static SourcePosition getFirstLJAnnotationPosition(CtElement element) {
64-
return element.getAnnotations().stream().filter(Utils::isLiquidJavaAnnotation).map(CtElement::getPosition)
65-
.min((p1, p2) -> {
66-
if (p1.getLine() != p2.getLine())
67-
return Integer.compare(p1.getLine(), p2.getLine());
68-
return Integer.compare(p1.getColumn(), p2.getColumn());
69-
}).orElse(element.getPosition());
71+
return getLiquidJavaAnnotations(element).map(CtAnnotation::getPosition).filter(pos -> pos != null).findFirst()
72+
.orElse(element.getPosition());
73+
}
74+
75+
// Get the position of the first value of the first LJ annotation on the element
76+
public static SourcePosition getFirstLJAnnotationValuePosition(CtElement element) {
77+
return getLiquidJavaAnnotations(element)
78+
.map(annotation -> getLJAnnotationValues(annotation).map(CtElement::getPosition)
79+
.filter(pos -> pos != null).findFirst()
80+
.orElse(annotation.getPosition() != null ? annotation.getPosition() : element.getPosition()))
81+
.findFirst().orElse(element.getPosition());
82+
}
83+
84+
private static Stream<CtAnnotation<?>> getLiquidJavaAnnotations(CtElement element) {
85+
return element.getAnnotations().stream().filter(Utils::isLiquidJavaAnnotation);
7086
}
7187

7288
private static boolean isLiquidJavaAnnotation(CtAnnotation<?> annotation) {
7389
return annotation.getAnnotationType().getQualifiedName().startsWith("liquidjava.specification");
7490
}
7591

76-
private static boolean hasRefinementValue(CtAnnotation<?> annotation, String refinement) {
77-
Map<String, ?> values = annotation.getValues();
78-
return Stream.of("value", "to", "from").anyMatch(key -> refinement.equals(String.valueOf(values.get(key))));
92+
private static Stream<CtElement> getLJAnnotationValues(CtAnnotation<?> annotation) {
93+
Map<String, ?> values = annotation.getAllValues();
94+
return REFINEMENT_KEYS.stream().map(values::get).filter(CtElement.class::isInstance).map(CtElement.class::cast);
7995
}
8096

8197
public static SourcePosition getRealPosition(CtElement element) {

0 commit comments

Comments
 (0)