Skip to content

Commit 3bac32d

Browse files
rcosta358rcosta358
committed
Fix Diagnostic Positions
1 parent f8d3f3e commit 3bac32d

File tree

6 files changed

+58
-27
lines changed

6 files changed

+58
-27
lines changed

‎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: 11 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -15,6 +15,7 @@
1515
import liquidjava.smt.Counterexample;
1616
import liquidjava.smt.SMTEvaluator;
1717
import liquidjava.smt.SMTResult;
18+
import liquidjava.utils.Utils;
1819
import liquidjava.utils.constants.Keys;
1920
import spoon.reflect.cu.SourcePosition;
2021
import spoon.reflect.declaration.CtElement;
@@ -53,10 +54,15 @@ public void processSubtyping(Predicate expectedType, List<GhostState> list, CtEl
5354
expected = expectedType.changeStatesToRefinements(filtered, s).changeAliasToRefinement(context, f);
5455
} catch (LJError e) {
5556
// add location info to error
56-
e.setPosition(element.getPosition());
57+
if (e.getPosition() == null) {
58+
SourcePosition pos = e instanceof NotFoundError ? Utils.getFirstLJAnnotationValuePosition(element)
59+
: Utils.getFirstLJAnnotationPosition(element);
60+
e.setPosition(pos);
61+
}
5762
throw e;
5863
}
59-
SMTResult result = verifySMTSubtype(expected, premises, element.getPosition());
64+
SourcePosition annotationValuePos = Utils.getFirstLJAnnotationValuePosition(element);
65+
SMTResult result = verifySMTSubtype(expected, premises, annotationValuePos);
6066
if (result.isError()) {
6167
throw new RefinementError(element.getPosition(), expectedType.simplify(), premisesBeforeChange.simplify(),
6268
map, result.getCounterexample(), customMessage);
@@ -94,7 +100,9 @@ public SMTResult verifySMTSubtype(Predicate expected, Predicate found, SourcePos
94100
try {
95101
return new SMTEvaluator().verifySubtype(found, expected, context);
96102
} catch (LJError e) {
97-
e.setPosition(position);
103+
if (e.getPosition() == null) {
104+
e.setPosition(position);
105+
}
98106
throw e;
99107
} catch (Exception e) {
100108
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)