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) {