Improve Syntax Errors

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/refinement_checker/ExternalRefinementTypeChecker.java

@@ -15,6 +15,7 @@
 import liquidjava.rj_language.parsing.RefinementsParser;
 import liquidjava.utils.Utils;
 import spoon.reflect.code.CtLiteral;
+import spoon.reflect.cu.SourcePosition;
 import spoon.reflect.declaration.CtAnnotation;
 import spoon.reflect.declaration.CtClass;
 import spoon.reflect.declaration.CtElement;
@@ -93,8 +94,8 @@ public <R> void visitCtMethod(CtMethod<R> method) {
         super.visitCtMethod(method);
     }
 
-    protected void getGhostFunction(String value, CtElement element) throws LJError {
-        GhostDTO f = RefinementsParser.getGhostDeclaration(value);
+    protected void getGhostFunction(String value, CtElement element, SourcePosition position) throws LJError {
+        GhostDTO f = getGhostDeclaration(value, position);
         if (element.getParent() instanceof CtInterface<?>) {
             GhostFunction gh = new GhostFunction(f, factory, prefix);
             context.addGhostFunction(gh);

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

@@ -66,25 +66,24 @@ public Optional<Predicate> getRefinementFromAnnotation(CtElement element) throws
         for (CtAnnotation<? extends Annotation> ann : element.getAnnotations()) {
             String an = ann.getActualAnnotation().annotationType().getCanonicalName();
             if (an.contentEquals("liquidjava.specification.Refinement")) {
-                String st = getStringFromAnnotation(ann.getValue("value"));
-                ref = Optional.of(st);
+                String value = getStringFromAnnotation(ann.getValue("value"));
+                ref = Optional.of(value);
 
             } else if (an.contentEquals("liquidjava.specification.RefinementPredicate")) {
-                String st = getStringFromAnnotation(ann.getValue("value"));
-                getGhostFunction(st, element);
+                String value = getStringFromAnnotation(ann.getValue("value"));
+                getGhostFunction(value, element, ann.getPosition());
 
             } else if (an.contentEquals("liquidjava.specification.RefinementAlias")) {
-                String st = getStringFromAnnotation(ann.getValue("value"));
-                handleAlias(st, element);
+                String value = getStringFromAnnotation(ann.getValue("value"));
+                handleAlias(value, element, ann.getPosition());
             }
         }
         if (ref.isPresent()) {
             Predicate p = new Predicate(ref.get(), element);
-
-            // check if refinement is valid
             if (!p.getExpression().isBooleanExpression()) {
-                throw new InvalidRefinementError(element.getPosition(),
-                        "Refinement predicate must be a boolean expression", ref.get());
+                SourcePosition position = Utils.getAnnotationPosition(element, ref.get());
+                throw new InvalidRefinementError(position, "Refinement predicate must be a boolean expression",
+                        ref.get());
             }
             constr = Optional.of(p);
         }
@@ -117,7 +116,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(), ann, element);
+                createStateGhost(s.getValue(), element, ann.getPosition());
             }
         }
     }
@@ -163,13 +162,22 @@ private void createStateSet(CtNewArray<String> e, int set, CtElement element) th
         }
     }
 
-    private void createStateGhost(String string, CtAnnotation<? extends Annotation> ann, CtElement element)
-            throws LJError {
-        GhostDTO gd = RefinementsParser.getGhostDeclaration(string);
+    protected GhostDTO getGhostDeclaration(String value, SourcePosition position) throws LJError {
+        try {
+            return RefinementsParser.getGhostDeclaration(value);
+        } catch (LJError e) {
+            // add location info to error
+            e.setPosition(position);
+            throw e;
+        }
+    }
+
+    private void createStateGhost(String string, CtElement element, SourcePosition position) throws LJError {
+        GhostDTO gd = getGhostDeclaration(string, position);
         if (!gd.paramTypes().isEmpty()) {
             throw new CustomError(
                     "Ghost States have the class as parameter " + "by default, no other parameters are allowed",
-                    ann.getPosition());
+                    position);
         }
         // Set class as parameter of Ghost
         String qn = getQualifiedClassName(element);
@@ -220,15 +228,15 @@ protected Optional<GhostFunction> createStateGhost(int order, CtElement element)
         return Optional.empty();
     }
 
-    protected void getGhostFunction(String value, CtElement element) throws LJError {
-        GhostDTO f = RefinementsParser.getGhostDeclaration(value);
+    protected void getGhostFunction(String value, CtElement element, SourcePosition position) throws LJError {
+        GhostDTO f = getGhostDeclaration(value, position);
         if (element.getParent()instanceof CtClass<?> klass) {
             GhostFunction gh = new GhostFunction(f, factory, klass.getQualifiedName());
             context.addGhostFunction(gh);
         }
     }
 
-    protected void handleAlias(String ref, CtElement element) throws LJError {
+    protected void handleAlias(String ref, CtElement element, SourcePosition position) throws LJError {
         try {
             AliasDTO a = RefinementsParser.getAliasDeclaration(ref);
             String klass = null;
@@ -242,18 +250,16 @@ protected void handleAlias(String ref, CtElement element) throws LJError {
             }
             if (klass != null && path != null) {
                 a.parse(path);
-                // refinement alias must return a boolean expression
                 if (a.getExpression() != null && !a.getExpression().isBooleanExpression()) {
-                    throw new InvalidRefinementError(element.getPosition(),
-                            "Refinement alias must return a boolean expression", ref);
+                    throw new InvalidRefinementError(position, "Refinement alias must return a boolean expression",
+                            ref);
                 }
                 AliasWrapper aw = new AliasWrapper(a, factory, klass, path);
                 context.addAlias(aw);
             }
         } catch (LJError e) {
             // add location info to error
-            SourcePosition pos = Utils.getAnnotationPosition(element, ref);
-            e.setPosition(pos);
+            e.setPosition(position);
             throw e;
         }
     }

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

@@ -16,6 +16,7 @@
 import liquidjava.utils.constants.Keys;
 import liquidjava.utils.constants.Types;
 import spoon.reflect.code.*;
+import spoon.reflect.cu.SourcePosition;
 import spoon.reflect.declaration.*;
 import spoon.reflect.reference.CtTypeReference;
 
@@ -69,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(element.getPosition(),
+                    throw new InvalidRefinementError(an.getPosition(),
                             "State refinement transition must be a boolean expression", to);
                 }
                 state.setTo(p);
@@ -208,8 +209,9 @@ private static Predicate createStatePredicate(String value, String targetClass,
             boolean isTo, String prefix) throws LJError {
         Predicate p = new Predicate(value, e, prefix);
         if (!p.getExpression().isBooleanExpression()) {
-            throw new InvalidRefinementError(e.getPosition(),
-                    "State refinement transition must be a boolean expression", value);
+            SourcePosition position = Utils.getAnnotationPosition(e, value);
+            throw new InvalidRefinementError(position, "State refinement transition must be a boolean expression",
+                    value);
         }
         CtTypeReference<?> r = tc.getFactory().Type().createReference(targetClass);
         String nameOld = String.format(Formats.INSTANCE, Keys.THIS, tc.getContext().getCounter());

liquidjava-verifier/src/main/java/liquidjava/rj_language/parsing/RefinementsParser.java

@@ -35,16 +35,12 @@ public static GhostDTO getGhostDeclaration(String s) throws LJError {
         ParseTree rc = compile(s);
         GhostDTO g = GhostVisitor.getGhostDecl(rc);
         if (g == null)
-            throw new SyntaxError("Ghost declarations should be in format <type> <name> (<parameters>)", s);
+            throw new SyntaxError("Invalid ghost declaration, expected e.g. @Ghost(\"int size\")", s);
         return g;
     }
 
     public static AliasDTO getAliasDeclaration(String s) throws LJError {
-        Optional<String> os = getErrors(s);
-        if (os.isPresent())
-            throw new SyntaxError(os.get(), s);
-        CodePointCharStream input;
-        input = CharStreams.fromString(s);
+        CodePointCharStream input = CharStreams.fromString(s);
         RJErrorListener err = new RJErrorListener();
         RJLexer lexer = new RJLexer(input);
         lexer.removeErrorListeners();
@@ -60,14 +56,15 @@ public static AliasDTO getAliasDeclaration(String s) throws LJError {
         AliasVisitor av = new AliasVisitor(input);
         AliasDTO alias = av.getAlias(rc);
         if (alias == null)
-            throw new SyntaxError("Alias definitions should be in format <name>(<parameters>) { <definition> }", s);
+            throw new SyntaxError(
+                    "Invalid alias definition, expected e.g. @RefinementAlias(\"Positive(int v) { v >= 0 }\")", s);
         return alias;
     }
 
     private static ParseTree compile(String toParse) throws LJError {
         Optional<String> s = getErrors(toParse);
         if (s.isPresent())
-            throw new SyntaxError(s.get(), toParse);
+            throw new SyntaxError("Invalid refinement expression, expected a logical predicate", toParse);
 
         CodePointCharStream input = CharStreams.fromString(toParse);
         RJErrorListener err = new RJErrorListener();

liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/GhostVisitor.java

@@ -19,9 +19,7 @@ public static GhostDTO getGhostDecl(ParseTree rc) {
             List<String> ls = args.stream().map(Pair::first).collect(Collectors.toList());
             return new GhostDTO(name, ls, type);
         } else if (rc.getChildCount() > 0) {
-            int i = rc.getChildCount();
-            if (i > 0)
-                return getGhostDecl(rc.getChild(0));
+            return getGhostDecl(rc.getChild(0));
         }
         return null;
     }