Improve Error Location Precision

Author: rcosta358

liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/IllegalConstructorTransitionError.java

@@ -1,6 +1,6 @@
 package liquidjava.diagnostics.errors;
 
-import spoon.reflect.declaration.CtElement;
+import spoon.reflect.cu.SourcePosition;
 
 /**
  * Error indicating that a constructor contains a state refinement with a 'from' state, which is not allowed
@@ -9,9 +9,8 @@
  */
 public class IllegalConstructorTransitionError extends LJError {
 
-    public IllegalConstructorTransitionError(CtElement element) {
+    public IllegalConstructorTransitionError(SourcePosition position) {
         super("Illegal Constructor Transition Error",
-                "Found constructor with 'from' state: constructors should only have a 'to' state",
-                element.getPosition(), null);
+                "Found constructor with 'from' state: constructors should only have a 'to' state", position, null);
     }
 }

liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java

@@ -68,6 +68,9 @@ public VCSimplificationResult getFound() {
 
     // Filters counterexample assignments only in found VC and sorts them in the order of its binders
     private Counterexample filterCounterexample(Counterexample counterexample) {
+        if (counterexample == null)
+            return new Counterexample(List.of());
+
         List<String> binderNames = getFound().getBinders();
         Set<String> knownAssignments = getFound().getImplication().toPredicate().getExpression().getConjuncts().stream()
                 .map(Expression::toString).collect(Collectors.toSet());

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

@@ -97,12 +97,12 @@ public Optional<Predicate> getRefinementFromAnnotation(CtElement element) throws
             } else if (an.contentEquals("liquidjava.specification.RefinementPredicate")) {
                 CtExpression<String> rawValue = ann.getValue("value");
                 String value = getStringFromAnnotation(rawValue);
-                getGhostFunction(value, element, rawValue.getPosition());
+                getGhostFunction(value, element, Utils.getAnnotationValuePosition(rawValue));
 
             } else if (an.contentEquals("liquidjava.specification.RefinementAlias")) {
                 CtExpression<String> rawValue = ann.getValue("value");
                 String value = getStringFromAnnotation(rawValue);
-                handleAlias(value, element, rawValue.getPosition());
+                handleAlias(value, element, Utils.getAnnotationValuePosition(rawValue));
             }
         }
         if (ref.isPresent()) {
@@ -187,7 +187,7 @@ public void handleStateSetsFromAnnotation(CtElement element) throws LJError {
             }
             if (an.contentEquals("liquidjava.specification.Ghost")) {
                 CtLiteral<String> s = (CtLiteral<String>) ann.getAllValues().get("value");
-                createStateGhost(s.getValue(), element, s.getPosition());
+                createStateGhost(s.getValue(), element, Utils.getAnnotationValuePosition(s));
             }
         }
     }
@@ -201,7 +201,7 @@ private void createStateSet(CtNewArray<String> e, int set, CtElement element) th
                 CtLiteral<String> s = (CtLiteral<String>) ce;
                 String f = s.getValue();
                 if (Character.isUpperCase(f.charAt(0))) {
-                    throw new CustomError("State names must start with lowercase", s.getPosition());
+                    throw new CustomError("State names must start with lowercase", Utils.getAnnotationValuePosition(s));
                 }
             }
         }

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

@@ -124,12 +124,12 @@ private RefinedFunction buildAndRegisterFunction(CtMethod<?> method, String name
         f.setName(name.replaceAll("\\p{C}", "")); // remove any empty chars from string
         f.setType(method.getType());
         f.setRefReturn(new Predicate());
+        f.setPlacementInCode(method);
         if (className != null)
             f.setClass(className);
         f.setSignature(signature);
         rtc.getContext().addFunctionToContext(f);
         auxGetMethodRefinements(method, f);
-        f.setPlacementInCode(method);
         return f;
     }
 

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

@@ -240,7 +240,7 @@ private Predicate getOperationRefinements(CtBinaryOperator<?> operator, CtVariab
                 return new Predicate();
             }
             if (l.getValue() == null)
-                throw new CustomError("Null literals are not supported");
+                throw new CustomError("Null literals are not supported", l.getPosition());
 
             return new Predicate(l.getValue().toString(), element);
 

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java

@@ -39,7 +39,7 @@ public static void handleConstructorState(CtConstructor<?> c, RefinedFunction f,
                 Map<String, CtExpression> m = a.getAllValues();
                 CtLiteral<String> from = (CtLiteral<String>) m.get("from");
                 if (from != null) {
-                    throw new IllegalConstructorTransitionError(from);
+                    throw new IllegalConstructorTransitionError(Utils.getAnnotationValuePosition(from));
                 }
             }
             setConstructorStates(f, an, c);
@@ -70,7 +70,7 @@ private static void setConstructorStates(RefinedFunction f, List<CtAnnotation<?
             if (to != null) {
                 Predicate p = new Predicate(to, element);
                 if (!p.getExpression().isBooleanExpression()) {
-                    throw new InvalidRefinementError(an.getPosition(),
+                    throw new InvalidRefinementError(Utils.getLJAnnotationPosition(element, to),
                             "State refinement transition must be a boolean expression", to);
                 }
                 state.setTo(p);

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

@@ -63,22 +63,28 @@ public static SourcePosition getLJAnnotationPosition(CtElement element, String v
         String quotedValue = "\"" + value + "\"";
         return getLiquidJavaAnnotations(element).flatMap(annotation -> getLJAnnotationValues(annotation)
                 .filter(expr -> quotedValue.equals(expr.toString())).map(expr -> {
-                    SourcePosition position = expr.getPosition();
-                    return (SourcePosition) new SourcePositionImpl(position.getCompilationUnit(),
-                            position.getSourceStart() + 1, position.getSourceEnd() - 1,
-                            position.getCompilationUnit().getLineSeparatorPositions());
+                    return getAnnotationValuePosition(expr);
                 })).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)
+                .map(annotation -> getLJAnnotationValues(annotation).map(Utils::getAnnotationValuePosition)
                         .filter(pos -> pos != null).findFirst()
                         .orElse(annotation.getPosition() != null ? annotation.getPosition() : element.getPosition()))
                 .findFirst().orElse(element.getPosition());
     }
 
+    public static SourcePosition getAnnotationValuePosition(CtElement value) {
+        SourcePosition position = value.getPosition();
+        if (position == null || !position.isValidPosition())
+            return null;
+
+        return (SourcePosition) new SourcePositionImpl(position.getCompilationUnit(), position.getSourceStart() + 1,
+                position.getSourceEnd() - 1, position.getCompilationUnit().getLineSeparatorPositions());
+    }
+
     private static Stream<CtAnnotation<?>> getLiquidJavaAnnotations(CtElement element) {
         return element.getAnnotations().stream().filter(Utils::isLiquidJavaAnnotation);
     }