From 49133e3d92a540fbfec801ac0f81e4343b1d9583 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Mon, 5 Oct 2026 15:03:32 +0100 Subject: [PATCH] Highlight predicates in refinement declaration diagnostics Co-authored-by: Codex --- .../ErrorRefinementDeclarationPositions.java | 32 ++++++++ .../processor/context/PlacementInCode.java | 5 +- .../refinement_checker/TypeChecker.java | 4 +- .../src/main/java/liquidjava/utils/Utils.java | 9 +++ .../java/liquidjava/utils/constants/Keys.java | 1 - .../api/tests/TestDeclarationPositions.java | 80 +++++++++++++++++++ 6 files changed, 124 insertions(+), 7 deletions(-) create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorRefinementDeclarationPositions.java create mode 100644 liquidjava-verifier/src/test/java/liquidjava/api/tests/TestDeclarationPositions.java diff --git a/liquidjava-example/src/main/java/testSuite/ErrorRefinementDeclarationPositions.java b/liquidjava-example/src/main/java/testSuite/ErrorRefinementDeclarationPositions.java new file mode 100644 index 00000000..7c3c66a2 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorRefinementDeclarationPositions.java @@ -0,0 +1,32 @@ +package testSuite; + +import liquidjava.specification.Refinement; +import liquidjava.specification.StateRefinement; + +public class ErrorRefinementDeclarationPositions { + @Refinement("_ > 10") + private int field = 11; + + @StateRefinement(from = "true", to = "true") + @Refinement(value = "_ > 20", msg = "result must exceed twenty") + int result() { + return 0; // Expect: Refinement Error + } + + void parameter(@Refinement("_ > 30") int value) { + } + + void check() { + parameter(0); // Expect: Refinement Error + } + + void local() { + @Refinement("_ > 40") + int local = 41; + local = 0; // Expect: Refinement Error + } + + void field() { + field = 0; // Expect: Refinement Error + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/context/PlacementInCode.java b/liquidjava-verifier/src/main/java/liquidjava/processor/context/PlacementInCode.java index 3310289f..77eddd35 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/PlacementInCode.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/PlacementInCode.java @@ -2,7 +2,7 @@ import java.lang.annotation.Annotation; -import liquidjava.utils.constants.Keys; +import liquidjava.utils.Utils; import spoon.reflect.code.CtComment; import spoon.reflect.cu.SourcePosition; import spoon.reflect.declaration.CtAnnotation; @@ -46,8 +46,7 @@ public static PlacementInCode createPlacement(CtElement elem) { } } String elemText = elemCopy.toString(); - SourcePosition annotationPosition = elem.getMetadata(Keys.REFINEMENT_POSITION)instanceof SourcePosition p ? p - : elem.getPosition(); + SourcePosition annotationPosition = Utils.getRefinementPosition(elem); return new PlacementInCode(elemText, elem.getPosition(), annotationPosition); } 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 7ab7e0bc..176e3379 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 @@ -92,7 +92,6 @@ public Optional getRefinementFromAnnotation(CtElement element) throws if (an.contentEquals("liquidjava.specification.Refinement")) { String value = getStringFromAnnotation(ann.getValue("value")); ref = Optional.of(value); - element.putMetadata(Keys.REFINEMENT_POSITION, Utils.getLJAnnotationPosition(element, value)); } else if (an.contentEquals("liquidjava.specification.RefinementPredicate")) { CtExpression rawValue = ann.getValue("value"); @@ -340,8 +339,7 @@ Optional> getExternalRefinement(CtInterface intrface) { public void checkVariableRefinements(Predicate refinementFound, String simpleName, CtTypeReference type, CtElement usage, CtElement variable) throws LJError { Optional expectedType = getRefinementFromAnnotation(variable); - SourcePosition declarationPosition = variable.getMetadata(Keys.REFINEMENT_POSITION)instanceof SourcePosition p - ? p : variable.getPosition(); + SourcePosition declarationPosition = Utils.getRefinementPosition(variable); Predicate cEt; RefinedVariable mainRV = null; if (context.hasVariable(simpleName)) { diff --git a/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java b/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java index 38f6b2ef..4dbd1a43 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java +++ b/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java @@ -2,6 +2,7 @@ import java.util.List; import java.util.Map; +import java.util.Objects; import java.util.Scanner; import java.util.Set; import java.util.stream.Stream; @@ -58,6 +59,14 @@ public static String getFile(CtElement element) { return pos.getFile().getAbsolutePath(); } + public static SourcePosition getRefinementPosition(CtElement element) { + return getLiquidJavaAnnotations(element) + .filter(annotation -> annotation.getAnnotationType().getQualifiedName() + .equals("liquidjava.specification.Refinement")) + .map(annotation -> getAnnotationValuePosition(annotation.getValue("value"))).filter(Objects::nonNull) + .findFirst().orElse(null); + } + // Get the position of the annotation with the given value public static SourcePosition getLJAnnotationPosition(CtElement element, String value) { String quotedValue = "\"" + value + "\""; diff --git a/liquidjava-verifier/src/main/java/liquidjava/utils/constants/Keys.java b/liquidjava-verifier/src/main/java/liquidjava/utils/constants/Keys.java index a7b9bb89..0f6cd964 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/utils/constants/Keys.java +++ b/liquidjava-verifier/src/main/java/liquidjava/utils/constants/Keys.java @@ -2,7 +2,6 @@ public final class Keys { public static final String REFINEMENT = "refinement"; - public static final String REFINEMENT_POSITION = "refinement_position"; public static final String REFINEMENT_SAT_CHECK = "refinement_sat_check"; public static final String TARGET = "target"; public static final String RETURN_VAR_NAME = "return_var_name"; diff --git a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestDeclarationPositions.java b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestDeclarationPositions.java new file mode 100644 index 00000000..aa53c632 --- /dev/null +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestDeclarationPositions.java @@ -0,0 +1,80 @@ +package liquidjava.api.tests; + +import static org.junit.jupiter.api.Assertions.*; + +import java.io.IOException; +import java.nio.file.Files; +import java.nio.file.Path; +import java.util.Comparator; +import java.util.List; + +import org.junit.jupiter.api.Test; + +import liquidjava.api.CommandLineLauncher; +import liquidjava.diagnostics.Diagnostics; +import liquidjava.diagnostics.errors.LJError; +import spoon.reflect.cu.SourcePosition; + +class TestDeclarationPositions { + @Test + void smtUnknownPointsToReturnPredicate() throws IOException { + assertDeclarations("ErrorSMTUnknown.java", "SMT Unknown Error", "_ > 2.0"); + } + + @Test + void refinementErrorPointsToReturnPredicate() throws IOException { + assertDeclarations("ErrorIdentity.java", "Refinement Error", "_ > 0"); + } + + @Test + void smtUnknownPointsToStatePredicate() throws IOException { + assertDeclarations("ErrorSMTUnknownState.java", "SMT Unknown Error", "amount(this) < limit"); + } + + @Test + void stateErrorPointsToStatePredicate() throws IOException { + assertDeclarations("ErrorUnconstrainedStateRefinement.java", "State Refinement Error", "ready(this)"); + } + + @Test + void declarationsCoverReturnsParametersLocalsAndFields() throws IOException { + assertDeclarations("ErrorRefinementDeclarationPositions.java", "Refinement Error", "_ > 20", "_ > 30", "_ > 40", + "_ > 10"); + } + + private static void assertDeclarations(String file, String title, String... predicates) throws IOException { + Path path = Path.of("../liquidjava-example/src/main/java/testSuite/", file).toRealPath(); + String source = Files.readString(path); + CommandLineLauncher.launch(path.toString()); + List errors = Diagnostics.getInstance().getErrors().stream() + .sorted(Comparator.comparingInt(error -> error.getPosition().getSourceStart())).toList(); + + assertEquals(predicates.length, errors.size()); + for (int i = 0; i < predicates.length; i++) { + LJError error = errors.get(i); + assertEquals(title, error.getTitle()); + assertPredicatePosition(error.getDeclarationPosition(), path, source, predicates[i]); + assertPredicateUnderline(error, predicates[i]); + } + } + + private static void assertPredicatePosition(SourcePosition position, Path file, String source, String predicate) + throws IOException { + assertNotNull(position, "Missing refinement declaration position"); + int start = source.indexOf("\"" + predicate + "\"") + 1; + assertTrue(start > 0, "Predicate not found in fixture: " + predicate); + assertEquals(start, position.getSourceStart()); + assertEquals(start + predicate.length() - 1, position.getSourceEnd()); + assertEquals(file, position.getFile().toPath().toRealPath()); + } + + private static void assertPredicateUnderline(LJError error, String predicate) { + String output = error.toString().replaceAll("\u001B\\[[;\\d]*m", ""); + String heading = "--> Refinement declared here:\n"; + assertTrue(output.contains(heading), "Missing refinement declaration snippet"); + String snippet = output.substring(output.indexOf(heading) + heading.length()); + String indent = " ".repeat(error.getDeclarationPosition().getColumn() - 1); + String underline = "^".repeat(predicate.length()); + assertTrue(snippet.contains(indent + underline + "\n"), snippet); + } +}