Use Annotation Position & Mark Parameters

This is needed to suggest parameters in method and parameter refinements

Author: rcosta358

liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java

@@ -129,7 +129,7 @@ public String getSnippet() {
 
                         // line number padding + pipe + column offset
                         String indent = " ".repeat(padding) + Colors.GREY + PIPE + Colors.RESET
-                            + " ".repeat(visualColStart - 1);
+                                + " ".repeat(visualColStart - 1);
                         String markers = accentColor + "^".repeat(Math.max(1, visualColEnd - visualColStart + 1));
                         sb.append(indent).append(markers);
 

liquidjava-verifier/src/main/java/liquidjava/processor/context/ContextHistory.java

@@ -5,6 +5,7 @@
 import java.util.Map;
 import java.util.Set;
 
+import liquidjava.utils.Utils;
 import spoon.reflect.cu.SourcePosition;
 import spoon.reflect.declaration.CtElement;
 import spoon.reflect.declaration.CtExecutable;
@@ -76,12 +77,8 @@ private String getFile(CtElement element) {
 
     public String getScopePosition(CtElement element) {
         SourcePosition pos = element.getPosition();
-        SourcePosition innerPosition = pos;
-        if (element instanceof CtExecutable<?> executable) {
-            if (executable.getBody() != null)
-                innerPosition = executable.getBody().getPosition();
-        }
-        return String.format("%d:%d-%d:%d", innerPosition.getLine(), innerPosition.getColumn() + 1, pos.getEndLine(),
+        SourcePosition annPosition = Utils.getFirstAnnotationPosition(element);
+        return String.format("%d:%d-%d:%d", annPosition.getLine(), annPosition.getColumn() + 1, pos.getEndLine(),
                 pos.getEndColumn());
     }
 

liquidjava-verifier/src/main/java/liquidjava/processor/context/RefinedVariable.java

@@ -9,10 +9,12 @@
 public abstract class RefinedVariable extends Refined {
     private final List<CtTypeReference<?>> supertypes;
     private PlacementInCode placementInCode;
+    private boolean isParameter;
 
     public RefinedVariable(String name, CtTypeReference<?> type, Predicate c) {
         super(name, type, c);
         supertypes = new ArrayList<>();
+        isParameter = false;
     }
 
     public abstract Predicate getMainRefinement();
@@ -65,4 +67,12 @@ public boolean equals(Object obj) {
             return supertypes.equals(other.supertypes);
         }
     }
+
+    public void setIsParameter(boolean b) {
+        isParameter = b;
+    }
+
+    public boolean isParameter() {
+        return isParameter;
+    }
 }

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/MethodsFunctionsChecker.java

@@ -154,6 +154,7 @@ private Predicate handleFunctionRefinements(RefinedFunction f, CtElement method,
                 c = oc.get().substituteVariable(Keys.WILDCARD, paramName);
             param.putMetadata(Keys.REFINEMENT, c);
             RefinedVariable v = rtc.getContext().addVarToContext(param.getSimpleName(), param.getType(), c, param);
+            v.setIsParameter(true);
             rtc.getMessageFromAnnotation(param).ifPresent(v::setMessage);
             if (v instanceof Variable)
                 f.addArgRefinements((Variable) v);

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

@@ -44,6 +44,16 @@ public static SourcePosition getAnnotationPosition(CtElement element, String ref
                 .map(CtElement::getPosition).orElse(element.getPosition());
     }
 
+    public static SourcePosition getFirstAnnotationPosition(CtElement element) {
+        CtElement target = element.getParent() != null ? element.getParent() : element;
+        return target.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(target.getPosition());
+    }
+
     private static boolean isLiquidJavaAnnotation(CtAnnotation<?> annotation) {
         return annotation.getAnnotationType().getQualifiedName().startsWith("liquidjava.specification");
     }