Improve Parser

Author: rcosta358

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

@@ -164,7 +164,7 @@ private void createStateSet(CtNewArray<String> 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) {

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 <type, name, list<type,name>>
-     * 
-     * @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<String> 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<String> 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;
     }
 }

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

@@ -5,20 +5,13 @@
 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;
 import rj.grammar.RJParser.ArgDeclIDContext;
 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<Pair<String, String>> getArgsDecl(ArgDeclIDContext argDeclID) {