From 3bac32d660d9d8d301167baacaec93e818b99d79 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Thu, 19 Mar 2026 14:29:29 +0000 Subject: [PATCH 1/2] Fix Diagnostic Positions --- .../ExternalRefinementTypeChecker.java | 2 +- .../refinement_checker/TypeChecker.java | 18 ++++---- .../refinement_checker/VCChecker.java | 14 +++++-- .../object_checkers/AuxStateHandler.java | 3 +- .../liquidjava/rj_language/Predicate.java | 6 ++- .../src/main/java/liquidjava/utils/Utils.java | 42 +++++++++++++------ 6 files changed, 58 insertions(+), 27 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java index 20c6079f..6e5f0f0d 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java @@ -47,7 +47,7 @@ public void visitCtInterface(CtInterface intrface) { this.prefix = literal.getValue(); if (!classExists(prefix)) { String message = String.format("Could not find class '%s'", prefix); - diagnostics.add(new ExternalClassNotFoundWarning(externalRef.get().getPosition(), message, prefix)); + diagnostics.add(new ExternalClassNotFoundWarning(literal.getPosition(), message, prefix)); return; } getRefinementFromAnnotation(intrface); diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java index a91a4cb2..bdb1c912 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java @@ -70,12 +70,14 @@ public Optional getRefinementFromAnnotation(CtElement element) throws ref = Optional.of(value); } else if (an.contentEquals("liquidjava.specification.RefinementPredicate")) { - String value = getStringFromAnnotation(ann.getValue("value")); - getGhostFunction(value, element, ann.getPosition()); + CtExpression rawValue = ann.getValue("value"); + String value = getStringFromAnnotation(rawValue); + getGhostFunction(value, element, rawValue.getPosition()); } else if (an.contentEquals("liquidjava.specification.RefinementAlias")) { - String value = getStringFromAnnotation(ann.getValue("value")); - handleAlias(value, element, ann.getPosition()); + CtExpression rawValue = ann.getValue("value"); + String value = getStringFromAnnotation(rawValue); + handleAlias(value, element, rawValue.getPosition()); } } if (ref.isPresent()) { @@ -116,7 +118,7 @@ public void handleStateSetsFromAnnotation(CtElement element) throws LJError { } if (an.contentEquals("liquidjava.specification.Ghost")) { CtLiteral s = (CtLiteral) ann.getAllValues().get("value"); - createStateGhost(s.getValue(), element, ann.getPosition()); + createStateGhost(s.getValue(), element, s.getPosition()); } } } @@ -167,7 +169,8 @@ protected GhostDTO getGhostDeclaration(String value, SourcePosition position) th return RefinementsParser.parseGhostDeclaration(value); } catch (LJError e) { // add location info to error - e.setPosition(position); + if (e.getPosition() == null) + e.setPosition(position); throw e; } } @@ -259,7 +262,8 @@ protected void handleAlias(String ref, CtElement element, SourcePosition positio } } catch (LJError e) { // add location info to error - e.setPosition(position); + if (e.getPosition() == null) + e.setPosition(position); throw e; } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java index 51084672..0b212892 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java @@ -15,6 +15,7 @@ import liquidjava.smt.Counterexample; import liquidjava.smt.SMTEvaluator; import liquidjava.smt.SMTResult; +import liquidjava.utils.Utils; import liquidjava.utils.constants.Keys; import spoon.reflect.cu.SourcePosition; import spoon.reflect.declaration.CtElement; @@ -53,10 +54,15 @@ public void processSubtyping(Predicate expectedType, List list, CtEl expected = expectedType.changeStatesToRefinements(filtered, s).changeAliasToRefinement(context, f); } catch (LJError e) { // add location info to error - e.setPosition(element.getPosition()); + if (e.getPosition() == null) { + SourcePosition pos = e instanceof NotFoundError ? Utils.getFirstLJAnnotationValuePosition(element) + : Utils.getFirstLJAnnotationPosition(element); + e.setPosition(pos); + } throw e; } - SMTResult result = verifySMTSubtype(expected, premises, element.getPosition()); + SourcePosition annotationValuePos = Utils.getFirstLJAnnotationValuePosition(element); + SMTResult result = verifySMTSubtype(expected, premises, annotationValuePos); if (result.isError()) { throw new RefinementError(element.getPosition(), expectedType.simplify(), premisesBeforeChange.simplify(), map, result.getCounterexample(), customMessage); @@ -94,7 +100,9 @@ public SMTResult verifySMTSubtype(Predicate expected, Predicate found, SourcePos try { return new SMTEvaluator().verifySubtype(found, expected, context); } catch (LJError e) { - e.setPosition(position); + if (e.getPosition() == null) { + e.setPosition(position); + } throw e; } catch (Exception e) { throw new CustomError(e.getMessage(), position); diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java index 9d435dff..ef32c8b7 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java @@ -225,7 +225,8 @@ private static Predicate createStatePredicate(String value, String targetClass, c = c.changeOldMentions(nameOld, name); boolean ok = tc.checkStateSMT(new Predicate(), c.negate(), e.getPosition()); if (ok) { - tc.throwStateConflictError(e.getPosition(), p); + SourcePosition pos = Utils.getLJAnnotationPosition(e, value); + tc.throwStateConflictError(pos, p); } return c1; } diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java index c91380ee..df491b50 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java @@ -86,8 +86,10 @@ protected Expression parse(String ref, CtElement element) throws LJError { return RefinementsParser.createAST(ref, prefix); } catch (LJError e) { // add location info to error - SourcePosition pos = Utils.getLJAnnotationPosition(element, ref); - e.setPosition(pos); + if (e.getPosition() == null) { + SourcePosition pos = Utils.getLJAnnotationPosition(element, ref); + e.setPosition(pos); + } throw e; } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java b/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java index 3924aefd..7e7aa7c2 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java +++ b/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java @@ -1,5 +1,6 @@ package liquidjava.utils; +import java.util.List; import java.util.Map; import java.util.Set; import java.util.stream.Stream; @@ -22,6 +23,7 @@ public class Utils { private static final Set DEFAULT_NAMES = Set.of("old", "length", "addToIndex", "getFromIndex"); + private static final List REFINEMENT_KEYS = List.of("value", "to", "from"); public static CtTypeReference getType(String type, Factory factory) { // TODO: complete with other types @@ -54,28 +56,42 @@ public static String getFile(CtElement element) { return pos.getFile().getAbsolutePath(); } - public static SourcePosition getLJAnnotationPosition(CtElement element, String refinement) { - return element.getAnnotations().stream() - .filter(a -> isLiquidJavaAnnotation(a) && hasRefinementValue(a, "\"" + refinement + "\"")).findFirst() - .map(CtElement::getPosition).orElse(element.getPosition()); + // Get the position of the annotation with the given value + public static SourcePosition getLJAnnotationPosition(CtElement element, String value) { + String quotedValue = "\"" + value + "\""; + return getLiquidJavaAnnotations(element) + .flatMap(annotation -> getLJAnnotationValues(annotation) + .filter(expr -> quotedValue.equals(expr.toString())) + .map(expr -> expr.getPosition() != null ? expr.getPosition() : annotation.getPosition())) + .findFirst().orElse(element.getPosition()); } + // Get the position of the first LJ annotation on the element public static SourcePosition getFirstLJAnnotationPosition(CtElement element) { - return element.getAnnotations().stream().filter(Utils::isLiquidJavaAnnotation).map(CtElement::getPosition) - .min((p1, p2) -> { - if (p1.getLine() != p2.getLine()) - return Integer.compare(p1.getLine(), p2.getLine()); - return Integer.compare(p1.getColumn(), p2.getColumn()); - }).orElse(element.getPosition()); + return getLiquidJavaAnnotations(element).map(CtAnnotation::getPosition).filter(pos -> pos != null).findFirst() + .orElse(element.getPosition()); + } + + // Get the position of the first value of the first LJ annotation on the element + public static SourcePosition getFirstLJAnnotationValuePosition(CtElement element) { + return getLiquidJavaAnnotations(element) + .map(annotation -> getLJAnnotationValues(annotation).map(CtElement::getPosition) + .filter(pos -> pos != null).findFirst() + .orElse(annotation.getPosition() != null ? annotation.getPosition() : element.getPosition())) + .findFirst().orElse(element.getPosition()); + } + + private static Stream> getLiquidJavaAnnotations(CtElement element) { + return element.getAnnotations().stream().filter(Utils::isLiquidJavaAnnotation); } private static boolean isLiquidJavaAnnotation(CtAnnotation annotation) { return annotation.getAnnotationType().getQualifiedName().startsWith("liquidjava.specification"); } - private static boolean hasRefinementValue(CtAnnotation annotation, String refinement) { - Map values = annotation.getValues(); - return Stream.of("value", "to", "from").anyMatch(key -> refinement.equals(String.valueOf(values.get(key)))); + private static Stream getLJAnnotationValues(CtAnnotation annotation) { + Map values = annotation.getAllValues(); + return REFINEMENT_KEYS.stream().map(values::get).filter(CtElement.class::isInstance).map(CtElement.class::cast); } public static SourcePosition getRealPosition(CtElement element) { From 0f6cc488cfceca2b1a2afcf65569aac82a39397e Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Thu, 19 Mar 2026 14:45:11 +0000 Subject: [PATCH 2/2] Minor Change --- .../liquidjava/processor/refinement_checker/VCChecker.java | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java index 0b212892..0035be6e 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java @@ -55,8 +55,7 @@ public void processSubtyping(Predicate expectedType, List list, CtEl } catch (LJError e) { // add location info to error if (e.getPosition() == null) { - SourcePosition pos = e instanceof NotFoundError ? Utils.getFirstLJAnnotationValuePosition(element) - : Utils.getFirstLJAnnotationPosition(element); + SourcePosition pos = Utils.getFirstLJAnnotationValuePosition(element); e.setPosition(pos); } throw e;