diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java index 1c548648..d1a743dc 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java +++ b/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); diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java index 154e94d0..052c6754 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java +++ b/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 void visitCtMethod(CtMethod 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); 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 ac2abb2d..86a18875 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 @@ -66,25 +66,24 @@ public Optional getRefinementFromAnnotation(CtElement element) throws for (CtAnnotation 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 s = (CtLiteral) ann.getAllValues().get("value"); - createStateGhost(s.getValue(), ann, element); + createStateGhost(s.getValue(), element, ann.getPosition()); } } } @@ -163,13 +162,22 @@ private void createStateSet(CtNewArray e, int set, CtElement element) th } } - private void createStateGhost(String string, CtAnnotation 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 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; } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java index 31d54313..61e2592c 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java +++ b/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 r = tc.getFactory().Type().createReference(targetClass); String nameOld = String.format(Formats.INSTANCE, Keys.THIS, tc.getContext().getCounter()); diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/parsing/RefinementsParser.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/parsing/RefinementsParser.java index 2fd8e89f..61f6bde1 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/parsing/RefinementsParser.java +++ b/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 ()", 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 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 () { }", 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 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(); diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/GhostVisitor.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/GhostVisitor.java index 6409740d..667cd210 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/GhostVisitor.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/GhostVisitor.java @@ -19,9 +19,7 @@ public static GhostDTO getGhostDecl(ParseTree rc) { List 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; }