Fix Refinement Declaration Positions

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
+    }
+}

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);
     }
 

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

@@ -92,7 +92,6 @@ public Optional<Predicate> 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<String> rawValue = ann.getValue("value");
@@ -340,8 +339,7 @@ Optional<CtAnnotation<?>> getExternalRefinement(CtInterface<?> intrface) {
     public void checkVariableRefinements(Predicate refinementFound, String simpleName, CtTypeReference<?> type,
             CtElement usage, CtElement variable) throws LJError {
         Optional<Predicate> 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)) {

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 + "\"";

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";

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<LJError> 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);
+    }
+}