Skip to content

Refactor Refinements Parser #167

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
rcosta358 merged 7 commits into from
Mar 5, 2026
+40 −62
Merged

Refactor Refinements Parser #167

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
7 commits
Select commit Hold shift + click to select a range
99ebc66
Improve Syntax Errors
rcosta358 Feb 28, 2026
b048323
Requested Changes
rcosta358 Mar 1, 2026
418bec8
Use Annotation Position Directly for Syntax Errors
rcosta358 Mar 1, 2026
81a741d
Use Annotation Position in Invalid Refinement Errors
rcosta358 Mar 1, 2026
b06676c
Update Error Messages
rcosta358 Mar 1, 2026
45cf93e
Minor Change
rcosta358 Mar 1, 2026
0318082
Improve Parser
rcosta358 Mar 2, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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);
Expand Down Expand Up @@ -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) {
Expand Down
89 changes: 37 additions & 52 deletions liquidjava-verifier/src/main/java/liquidjava/rj_language/parsing/RefinementsParser.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand All @@ -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;
}
}
9 changes: 1 addition & 8 deletions liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/AliasVisitor.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
*
Expand Down Expand Up @@ -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);
Copy link
Collaborator

@CatarinaGamboa CatarinaGamboa Mar 5, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

should we worry about nulls here?

Copy link
Collaborator Author

@rcosta358 rcosta358 Mar 5, 2026 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I don't think so, because this method is only called after a match with AliasContext, so both pred.start and getInputStream() are non-null.

}

private List<Pair<String, String>> getArgsDecl(ArgDeclIDContext argDeclID) {
Expand Down