From 99ebc668f09c010a0ea883ecd5cd016b547b5aae Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Sat, 28 Feb 2026 21:23:21 +0000 Subject: [PATCH 1/7] Improve Syntax Errors --- .../ExternalRefinementTypeChecker.java | 5 +- .../refinement_checker/TypeChecker.java | 47 ++++++++++--------- .../parsing/RefinementsParser.java | 7 ++- 3 files changed, 31 insertions(+), 28 deletions(-) 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 052c6754..18e82855 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,7 +15,6 @@ 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; @@ -94,8 +93,8 @@ public void visitCtMethod(CtMethod method) { super.visitCtMethod(method); } - protected void getGhostFunction(String value, CtElement element, SourcePosition position) throws LJError { - GhostDTO f = getGhostDeclaration(value, position); + protected void getGhostFunction(String value, CtElement element) throws LJError { + GhostDTO f = getGhostDeclaration(value, element); 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 86a18875..fae39d29 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,24 +66,25 @@ public Optional getRefinementFromAnnotation(CtElement element) throws for (CtAnnotation ann : element.getAnnotations()) { String an = ann.getActualAnnotation().annotationType().getCanonicalName(); if (an.contentEquals("liquidjava.specification.Refinement")) { - String value = getStringFromAnnotation(ann.getValue("value")); - ref = Optional.of(value); + String st = getStringFromAnnotation(ann.getValue("value")); + ref = Optional.of(st); } else if (an.contentEquals("liquidjava.specification.RefinementPredicate")) { - String value = getStringFromAnnotation(ann.getValue("value")); - getGhostFunction(value, element, ann.getPosition()); + String st = getStringFromAnnotation(ann.getValue("value")); + getGhostFunction(st, element); } else if (an.contentEquals("liquidjava.specification.RefinementAlias")) { - String value = getStringFromAnnotation(ann.getValue("value")); - handleAlias(value, element, ann.getPosition()); + String st = getStringFromAnnotation(ann.getValue("value")); + handleAlias(st, element); } } if (ref.isPresent()) { Predicate p = new Predicate(ref.get(), element); + + // check if refinement is valid if (!p.getExpression().isBooleanExpression()) { - SourcePosition position = Utils.getAnnotationPosition(element, ref.get()); - throw new InvalidRefinementError(position, "Refinement predicate must be a boolean expression", - ref.get()); + throw new InvalidRefinementError(element.getPosition(), + "Refinement predicate must be a boolean expression", ref.get()); } constr = Optional.of(p); } @@ -116,7 +117,7 @@ public void handleStateSetsFromAnnotation(CtElement element) throws LJError { } if (an.contentEquals("liquidjava.specification.Ghost")) { CtLiteral s = (CtLiteral) ann.getAllValues().get("value"); - createStateGhost(s.getValue(), element, ann.getPosition()); + createStateGhost(s.getValue(), ann, element); } } } @@ -162,22 +163,24 @@ private void createStateSet(CtNewArray e, int set, CtElement element) th } } - protected GhostDTO getGhostDeclaration(String value, SourcePosition position) throws LJError { + protected GhostDTO getGhostDeclaration(String value, CtElement element) throws LJError { try { return RefinementsParser.getGhostDeclaration(value); } catch (LJError e) { // add location info to error - e.setPosition(position); + SourcePosition annPosition = Utils.getAnnotationPosition(element, value); + e.setPosition(annPosition); throw e; } } - private void createStateGhost(String string, CtElement element, SourcePosition position) throws LJError { - GhostDTO gd = getGhostDeclaration(string, position); + private void createStateGhost(String string, CtAnnotation ann, CtElement element) + throws LJError { + GhostDTO gd = getGhostDeclaration(string, ann); if (!gd.paramTypes().isEmpty()) { throw new CustomError( "Ghost States have the class as parameter " + "by default, no other parameters are allowed", - position); + ann.getPosition()); } // Set class as parameter of Ghost String qn = getQualifiedClassName(element); @@ -228,15 +231,15 @@ protected Optional createStateGhost(int order, CtElement element) return Optional.empty(); } - protected void getGhostFunction(String value, CtElement element, SourcePosition position) throws LJError { - GhostDTO f = getGhostDeclaration(value, position); + protected void getGhostFunction(String value, CtElement element) throws LJError { + GhostDTO f = getGhostDeclaration(value, element); if (element.getParent()instanceof CtClass klass) { GhostFunction gh = new GhostFunction(f, factory, klass.getQualifiedName()); context.addGhostFunction(gh); } } - protected void handleAlias(String ref, CtElement element, SourcePosition position) throws LJError { + protected void handleAlias(String ref, CtElement element) throws LJError { try { AliasDTO a = RefinementsParser.getAliasDeclaration(ref); String klass = null; @@ -250,16 +253,18 @@ protected void handleAlias(String ref, CtElement element, SourcePosition positio } 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(position, "Refinement alias must return a boolean expression", - ref); + throw new InvalidRefinementError(element.getPosition(), + "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 - e.setPosition(position); + SourcePosition pos = Utils.getAnnotationPosition(element, ref); + e.setPosition(pos); throw e; } } 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 61f6bde1..e7a4712c 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,7 +35,7 @@ public static GhostDTO getGhostDeclaration(String s) throws LJError { ParseTree rc = compile(s); GhostDTO g = GhostVisitor.getGhostDecl(rc); if (g == null) - throw new SyntaxError("Invalid ghost declaration, expected e.g. @Ghost(\"int size\")", s); + throw new SyntaxError("Invalid ghost declaration, e.g. \"int size\"", s); return g; } @@ -56,15 +56,14 @@ public static AliasDTO getAliasDeclaration(String s) throws LJError { AliasVisitor av = new AliasVisitor(input); AliasDTO alias = av.getAlias(rc); if (alias == null) - throw new SyntaxError( - "Invalid alias definition, expected e.g. @RefinementAlias(\"Positive(int v) { v >= 0 }\")", s); + throw new SyntaxError("Invalid alias definition, e.g. \"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("Invalid refinement expression, expected a logical predicate", toParse); + throw new SyntaxError("Invalid refinement expression, e.g. \"v > 0\"", toParse); CodePointCharStream input = CharStreams.fromString(toParse); RJErrorListener err = new RJErrorListener(); From b0483230ea4187b432663ee81ac86aeace4c7103 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Sun, 1 Mar 2026 11:40:31 +0000 Subject: [PATCH 2/7] Requested Changes --- .../liquidjava/rj_language/parsing/RefinementsParser.java | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) 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 e7a4712c..062db5da 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,7 +35,7 @@ public static GhostDTO getGhostDeclaration(String s) throws LJError { ParseTree rc = compile(s); GhostDTO g = GhostVisitor.getGhostDecl(rc); if (g == null) - throw new SyntaxError("Invalid ghost declaration, e.g. \"int size\"", s); + throw new SyntaxError("Invalid ghost declaration, e.g. @Ghost(\"int size\")", s); return g; } @@ -56,14 +56,14 @@ public static AliasDTO getAliasDeclaration(String s) throws LJError { AliasVisitor av = new AliasVisitor(input); AliasDTO alias = av.getAlias(rc); if (alias == null) - throw new SyntaxError("Invalid alias definition, e.g. \"Positive(int v) { v >= 0 }\"", s); + throw new SyntaxError("Invalid alias definition, 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("Invalid refinement expression, e.g. \"v > 0\"", toParse); + throw new SyntaxError("Invalid refinement expression, expected a logical predicate", toParse); CodePointCharStream input = CharStreams.fromString(toParse); RJErrorListener err = new RJErrorListener(); From 418bec8ea99732749d7abae2272c05ec1f8c8719 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Sun, 1 Mar 2026 11:57:20 +0000 Subject: [PATCH 3/7] Use Annotation Position Directly for Syntax Errors --- .../ExternalRefinementTypeChecker.java | 5 ++- .../refinement_checker/TypeChecker.java | 38 ++++++++----------- 2 files changed, 19 insertions(+), 24 deletions(-) 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 18e82855..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 = getGhostDeclaration(value, element); + 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 fae39d29..15eb57a8 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,22 +66,20 @@ 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()); @@ -117,7 +115,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,24 +161,22 @@ private void createStateSet(CtNewArray e, int set, CtElement element) th } } - protected GhostDTO getGhostDeclaration(String value, CtElement element) throws LJError { + protected GhostDTO getGhostDeclaration(String value, SourcePosition position) throws LJError { try { return RefinementsParser.getGhostDeclaration(value); } catch (LJError e) { // add location info to error - SourcePosition annPosition = Utils.getAnnotationPosition(element, value); - e.setPosition(annPosition); + e.setPosition(position); throw e; } } - private void createStateGhost(String string, CtAnnotation ann, CtElement element) - throws LJError { - GhostDTO gd = getGhostDeclaration(string, ann); + 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); @@ -231,15 +227,15 @@ protected Optional createStateGhost(int order, CtElement element) return Optional.empty(); } - protected void getGhostFunction(String value, CtElement element) throws LJError { - GhostDTO f = getGhostDeclaration(value, element); + 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; @@ -253,7 +249,6 @@ 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); @@ -263,8 +258,7 @@ protected void handleAlias(String ref, CtElement element) throws LJError { } } catch (LJError e) { // add location info to error - SourcePosition pos = Utils.getAnnotationPosition(element, ref); - e.setPosition(pos); + e.setPosition(position); throw e; } } From 81a741dfd6873153ae460e6d54318ff2f91c05e6 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Sun, 1 Mar 2026 12:02:27 +0000 Subject: [PATCH 4/7] Use Annotation Position in Invalid Refinement Errors --- .../liquidjava/processor/refinement_checker/TypeChecker.java | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) 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 15eb57a8..efa26f0b 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 @@ -81,7 +81,8 @@ public Optional getRefinementFromAnnotation(CtElement element) throws if (ref.isPresent()) { Predicate p = new Predicate(ref.get(), element); if (!p.getExpression().isBooleanExpression()) { - throw new InvalidRefinementError(element.getPosition(), + SourcePosition position = Utils.getAnnotationPosition(element, ref.get()); + throw new InvalidRefinementError(position, "Refinement predicate must be a boolean expression", ref.get()); } constr = Optional.of(p); @@ -250,7 +251,7 @@ protected void handleAlias(String ref, CtElement element, SourcePosition positio if (klass != null && path != null) { a.parse(path); if (a.getExpression() != null && !a.getExpression().isBooleanExpression()) { - throw new InvalidRefinementError(element.getPosition(), + throw new InvalidRefinementError(position, "Refinement alias must return a boolean expression", ref); } AliasWrapper aw = new AliasWrapper(a, factory, klass, path); From b06676cef21fb87fbabc9279001ce87de553cd36 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Sun, 1 Mar 2026 14:02:36 +0000 Subject: [PATCH 5/7] Update Error Messages --- .../liquidjava/rj_language/parsing/RefinementsParser.java | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) 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 062db5da..711f7d16 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,7 +35,7 @@ public static GhostDTO getGhostDeclaration(String s) throws LJError { ParseTree rc = compile(s); GhostDTO g = GhostVisitor.getGhostDecl(rc); if (g == null) - throw new SyntaxError("Invalid ghost declaration, e.g. @Ghost(\"int size\")", s); + throw new SyntaxError("Invalid ghost declaration, expected e.g. @Ghost(\"int size\")", s); return g; } @@ -56,7 +56,7 @@ public static AliasDTO getAliasDeclaration(String s) throws LJError { AliasVisitor av = new AliasVisitor(input); AliasDTO alias = av.getAlias(rc); if (alias == null) - throw new SyntaxError("Invalid alias definition, e.g. @RefinementAlias(\"Positive(int v) { v >= 0 }\")", s); + throw new SyntaxError("Invalid alias definition, expected e.g. @RefinementAlias(\"Positive(int v) { v >= 0 }\")", s); return alias; } From 45cf93e5c406622f7e5b980d16386ffe932b4af9 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Sun, 1 Mar 2026 14:08:10 +0000 Subject: [PATCH 6/7] Minor Change --- .../processor/refinement_checker/TypeChecker.java | 8 ++++---- .../liquidjava/rj_language/parsing/RefinementsParser.java | 3 ++- 2 files changed, 6 insertions(+), 5 deletions(-) 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 efa26f0b..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 @@ -82,8 +82,8 @@ public Optional getRefinementFromAnnotation(CtElement element) throws Predicate p = new Predicate(ref.get(), element); if (!p.getExpression().isBooleanExpression()) { SourcePosition position = Utils.getAnnotationPosition(element, ref.get()); - throw new InvalidRefinementError(position, - "Refinement predicate must be a boolean expression", ref.get()); + throw new InvalidRefinementError(position, "Refinement predicate must be a boolean expression", + ref.get()); } constr = Optional.of(p); } @@ -251,8 +251,8 @@ protected void handleAlias(String ref, CtElement element, SourcePosition positio if (klass != null && path != null) { a.parse(path); if (a.getExpression() != null && !a.getExpression().isBooleanExpression()) { - throw new InvalidRefinementError(position, - "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); 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 711f7d16..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 @@ -56,7 +56,8 @@ public static AliasDTO getAliasDeclaration(String s) throws LJError { AliasVisitor av = new AliasVisitor(input); AliasDTO alias = av.getAlias(rc); if (alias == null) - throw new SyntaxError("Invalid alias definition, expected e.g. @RefinementAlias(\"Positive(int v) { v >= 0 }\")", s); + throw new SyntaxError( + "Invalid alias definition, expected e.g. @RefinementAlias(\"Positive(int v) { v >= 0 }\")", s); return alias; } From 03180829247cf95b7332663556d442d3de3deab4 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Mon, 2 Mar 2026 13:38:21 +0000 Subject: [PATCH 7/7] Improve Parser --- .../refinement_checker/TypeChecker.java | 4 +- .../parsing/RefinementsParser.java | 89 ++++++++----------- .../rj_language/visitors/AliasVisitor.java | 9 +- 3 files changed, 40 insertions(+), 62 deletions(-) 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 86a18875..d26cd25b 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 @@ -164,7 +164,7 @@ private void createStateSet(CtNewArray e, int set, CtElement element) th protected GhostDTO getGhostDeclaration(String value, SourcePosition position) throws LJError { try { - return RefinementsParser.getGhostDeclaration(value); + return RefinementsParser.parseGhostDeclaration(value); } catch (LJError e) { // add location info to error e.setPosition(position); @@ -238,7 +238,7 @@ protected void getGhostFunction(String value, CtElement element, SourcePosition protected void handleAlias(String ref, CtElement element, SourcePosition position) throws LJError { try { - AliasDTO a = RefinementsParser.getAliasDeclaration(ref); + AliasDTO a = RefinementsParser.parseAliasDefinition(ref); String klass = null; String path = null; if (element instanceof CtClass) { 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 61f6bde1..0141a64c 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 @@ -2,7 +2,6 @@ import java.util.Optional; -import liquidjava.diagnostics.errors.LJError; import liquidjava.diagnostics.errors.SyntaxError; import liquidjava.processor.facade.AliasDTO; import liquidjava.processor.facade.GhostDTO; @@ -13,99 +12,85 @@ import org.antlr.v4.runtime.CharStreams; import org.antlr.v4.runtime.CodePointCharStream; import org.antlr.v4.runtime.CommonTokenStream; -import org.antlr.v4.runtime.RuleContext; import org.antlr.v4.runtime.tree.ParseTree; import rj.grammar.RJLexer; import rj.grammar.RJParser; public class RefinementsParser { - public static Expression createAST(String toParse, String prefix) throws LJError { - ParseTree pt = compile(toParse); + /** + * Parses a refinement expression from a string + */ + public static Expression createAST(String toParse, String prefix) throws SyntaxError { + ParseTree pt = compile(toParse, "Invalid refinement expression, expected a logical predicate"); CreateASTVisitor visitor = new CreateASTVisitor(prefix); return visitor.create(pt); } /** - * The triple information of the ghost declaration in the order > - * - * @param s + * Parses the ghost declaration from the given string */ - public static GhostDTO getGhostDeclaration(String s) throws LJError { - ParseTree rc = compile(s); + public static GhostDTO parseGhostDeclaration(String toParse) throws SyntaxError { + String errorMessage = "Invalid ghost declaration, expected e.g. @Ghost(\"int size\")"; + ParseTree rc = compile(toParse, errorMessage); GhostDTO g = GhostVisitor.getGhostDecl(rc); if (g == null) - throw new SyntaxError("Invalid ghost declaration, expected e.g. @Ghost(\"int size\")", s); + throw new SyntaxError(errorMessage, toParse); return g; } - public static AliasDTO getAliasDeclaration(String s) throws LJError { - CodePointCharStream input = CharStreams.fromString(s); - RJErrorListener err = new RJErrorListener(); - RJLexer lexer = new RJLexer(input); - lexer.removeErrorListeners(); - lexer.addErrorListener(err); - - CommonTokenStream tokens = new CommonTokenStream(lexer); - RJParser parser = new RJParser(tokens); - parser.setBuildParseTree(true); - parser.removeErrorListeners(); - parser.addErrorListener(err); - - RuleContext rc = parser.prog(); - AliasVisitor av = new AliasVisitor(input); + /** + * Parses the alias declaration from the given string, throwing a SyntaxError if it is not valid + */ + public static AliasDTO parseAliasDefinition(String toParse) throws SyntaxError { + String errorMessage = "Invalid alias definition, expected e.g. @RefinementAlias(\"Positive(int v) { v >= 0 }\")"; + ParseTree rc = compile(toParse, errorMessage); + AliasVisitor av = new AliasVisitor(); AliasDTO alias = av.getAlias(rc); if (alias == null) - throw new SyntaxError( - "Invalid alias definition, expected e.g. @RefinementAlias(\"Positive(int v) { v >= 0 }\")", s); + throw new SyntaxError(errorMessage, toParse); return alias; } - private static ParseTree compile(String toParse) throws LJError { + /** + * Compiles the given string into a parse tree + */ + private static ParseTree compile(String toParse, String errorMessage) throws SyntaxError { Optional s = getErrors(toParse); if (s.isPresent()) - throw new SyntaxError("Invalid refinement expression, expected a logical predicate", toParse); + throw new SyntaxError(errorMessage, toParse); - CodePointCharStream input = CharStreams.fromString(toParse); RJErrorListener err = new RJErrorListener(); - - RJLexer lexer = new RJLexer(input); - lexer.removeErrorListeners(); - lexer.addErrorListener(err); - - CommonTokenStream tokens = new CommonTokenStream(lexer); - - RJParser parser = new RJParser(tokens); - parser.setBuildParseTree(true); - parser.removeErrorListeners(); - parser.addErrorListener(err); + RJParser parser = createParser(toParse, err); return parser.prog(); } /** - * First passage to check if there are syntax errors - * - * @param toParse - * - * @return + * Checks if the given string can be parsed without syntax errors, returning the error messages if any */ private static Optional getErrors(String toParse) { - CodePointCharStream input = CharStreams.fromString(toParse); RJErrorListener err = new RJErrorListener(); + RJParser parser = createParser(toParse, err); + parser.start(); // all consumed + if (err.getErrors() > 0) + return Optional.of(err.getMessages()); + return Optional.empty(); + } + /** + * Creates a parser for the given input string and error listener + */ + private static RJParser createParser(String toParse, RJErrorListener err) { + CodePointCharStream input = CharStreams.fromString(toParse); RJLexer lexer = new RJLexer(input); lexer.removeErrorListeners(); lexer.addErrorListener(err); CommonTokenStream tokens = new CommonTokenStream(lexer); - RJParser parser = new RJParser(tokens); parser.setBuildParseTree(true); parser.removeErrorListeners(); parser.addErrorListener(err); - parser.start(); // all consumed - if (err.getErrors() > 0) - return Optional.of(err.getMessages()); - return Optional.empty(); + return parser; } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/AliasVisitor.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/AliasVisitor.java index 4237fc4b..0fd6ae15 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/AliasVisitor.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/AliasVisitor.java @@ -5,7 +5,6 @@ import java.util.stream.Collectors; import liquidjava.processor.facade.AliasDTO; import liquidjava.utils.Pair; -import org.antlr.v4.runtime.CodePointCharStream; import org.antlr.v4.runtime.misc.Interval; import org.antlr.v4.runtime.tree.ParseTree; import rj.grammar.RJParser.AliasContext; @@ -13,12 +12,6 @@ import rj.grammar.RJParser.PredContext; public class AliasVisitor { - CodePointCharStream input; - - public AliasVisitor(CodePointCharStream input) { - this.input = input; - } - /** * Gets information about the alias * @@ -56,7 +49,7 @@ private String getText(PredContext pred) { int a = pred.start.getStartIndex(); int b = pred.stop.getStopIndex(); Interval interval = new Interval(a, b); - return input.getText(interval); + return pred.start.getInputStream().getText(interval); } private List> getArgsDecl(ArgDeclIDContext argDeclID) {