From b6f90adff7661331566b13a131d8163abf2861fd Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Tue, 5 May 2026 11:47:16 +0100 Subject: [PATCH 1/2] Fix Operator Precedence --- .../testSuite/CorrectOperatorPrecedence.java | 66 +++++++++++++++++++ .../src/main/antlr4/rj/grammar/RJ.g4 | 41 +++++------- .../parsing/RefinementsParser.java | 2 +- .../visitors/CreateASTVisitor.java | 66 +++++-------------- 4 files changed, 97 insertions(+), 78 deletions(-) create mode 100644 liquidjava-example/src/main/java/testSuite/CorrectOperatorPrecedence.java diff --git a/liquidjava-example/src/main/java/testSuite/CorrectOperatorPrecedence.java b/liquidjava-example/src/main/java/testSuite/CorrectOperatorPrecedence.java new file mode 100644 index 00000000..62de8119 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/CorrectOperatorPrecedence.java @@ -0,0 +1,66 @@ +package testSuite; + +import liquidjava.specification.Refinement; + +public class CorrectOperatorPrecedence { + + @Refinement("_ == 1 + 2 * 0") + int multiplicationBeforeAddition() { + return 1; + } + + @Refinement("_ == (1 + 2) * 0") + int groupedAdditionBeforeMultiplication() { + return 0; + } + + @Refinement("_ == 10 - 3 - 1") + int subtractionAssociatesLeft() { + return 6; + } + + @Refinement("_ == 10 - (3 - 1)") + int groupedSubtractionAssociatesRight() { + return 8; + } + + @Refinement("_ == -2 + 3") + int unaryBeforeAddition() { + return 1; + } + + @Refinement("_ == (true || false && false)") + boolean andBeforeOr() { + return true; + } + + @Refinement("_ == (!false && false)") + boolean notBeforeAnd() { + return false; + } + + @Refinement("_ == (false --> true && false)") + boolean andBeforeImplication() { + return true; + } + + @Refinement("_ == (true || true --> false)") + boolean orBeforeImplication() { + return false; + } + + @Refinement("_ == (false --> false && false)") + boolean anotherAndBeforeImplication() { + return true; + } + + @Refinement("_ == (false --> true --> false)") + boolean implicationAssociatesRight() { + return true; + } + + @Refinement("_ == (true ? false : true ? false : true)") + boolean ternaryAssociatesRight() { + return false; + } +} diff --git a/liquidjava-verifier/src/main/antlr4/rj/grammar/RJ.g4 b/liquidjava-verifier/src/main/antlr4/rj/grammar/RJ.g4 index c6b79a3c..4c4c5647 100644 --- a/liquidjava-verifier/src/main/antlr4/rj/grammar/RJ.g4 +++ b/liquidjava-verifier/src/main/antlr4/rj/grammar/RJ.g4 @@ -1,41 +1,31 @@ grammar RJ; -prog: start | ; +prog: start EOF; start: pred #startPred | alias #startAlias | ghost #startGhost ; +//----------------------- Predicates ----------------------- pred: - '(' pred ')' #predGroup - | '!' pred #predNegate - | pred LOGOP pred #predLogic - | pred '?' pred ':' pred #ite - | exp #predExp + '-' pred #opMinus + | '!' pred #opNot + | '(' pred ')' #predGroup + | literalExpression #opLiteral + | pred MULOP pred #opArith + | pred ('+'|'-') pred #opArith + | pred BOOLOP pred #expBool + | pred '&&' pred #predLogic + | pred '||' pred #predLogic + | pred '-->' pred #predLogic + | pred '?' pred ':' pred #ite ; -exp: - '(' exp ')' #expGroup - | exp BOOLOP exp #expBool - | operand #expOperand - ; - -operand: - literalExpression #opLiteral - | operand ARITHOP operand #opArith - | operand '-' operand #opSub - | '-' operand #opMinus - | '!' operand #opNot - | '(' operand ')' #opGroup - ; - - literalExpression: - '(' literalExpression ')' #litGroup - | literal #lit + literal #lit | ID #var | functionCall #invocation | enumerate #enum @@ -93,9 +83,8 @@ type: | type '[]'; -LOGOP : '&&'|'||'| '-->'; BOOLOP : '=='|'!='|'>='|'>'|'<='|'<'; -ARITHOP : '+'|'*'|'/'|'%';//|'-'; +MULOP : '*'|'/'|'%'; BOOL : 'true' | 'false'; ID_UPPER: ([A-Z][a-zA-Z0-9]*); 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 0141a64c..2475dbcd 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 @@ -71,7 +71,7 @@ private static ParseTree compile(String toParse, String errorMessage) throws Syn private static Optional getErrors(String toParse) { RJErrorListener err = new RJErrorListener(); RJParser parser = createParser(toParse, err); - parser.start(); // all consumed + parser.prog(); // all consumed if (err.getErrors() > 0) return Optional.of(err.getMessages()); return Optional.empty(); diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/CreateASTVisitor.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/CreateASTVisitor.java index 5efee64f..680c4695 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/CreateASTVisitor.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/CreateASTVisitor.java @@ -20,7 +20,6 @@ import liquidjava.rj_language.ast.UnaryExpression; import liquidjava.rj_language.ast.Var; import liquidjava.utils.Utils; -import liquidjava.utils.constants.Formats; import liquidjava.utils.constants.Keys; import org.antlr.v4.runtime.tree.ParseTree; @@ -30,29 +29,20 @@ import rj.grammar.RJParser.DotCallContext; import rj.grammar.RJParser.EnumContext; import rj.grammar.RJParser.ExpBoolContext; -import rj.grammar.RJParser.ExpContext; -import rj.grammar.RJParser.ExpGroupContext; -import rj.grammar.RJParser.ExpOperandContext; import rj.grammar.RJParser.FunctionCallContext; import rj.grammar.RJParser.GhostCallContext; import rj.grammar.RJParser.InvocationContext; import rj.grammar.RJParser.IteContext; import rj.grammar.RJParser.LitContext; -import rj.grammar.RJParser.LitGroupContext; import rj.grammar.RJParser.LiteralContext; import rj.grammar.RJParser.LiteralExpressionContext; import rj.grammar.RJParser.OpArithContext; -import rj.grammar.RJParser.OpGroupContext; import rj.grammar.RJParser.OpLiteralContext; import rj.grammar.RJParser.OpMinusContext; import rj.grammar.RJParser.OpNotContext; -import rj.grammar.RJParser.OpSubContext; -import rj.grammar.RJParser.OperandContext; import rj.grammar.RJParser.PredContext; -import rj.grammar.RJParser.PredExpContext; import rj.grammar.RJParser.PredGroupContext; import rj.grammar.RJParser.PredLogicContext; -import rj.grammar.RJParser.PredNegateContext; import rj.grammar.RJParser.ProgContext; import rj.grammar.RJParser.StartContext; import rj.grammar.RJParser.StartPredContext; @@ -79,10 +69,6 @@ else if (rc instanceof StartContext) return startCreate(rc); else if (rc instanceof PredContext) return predCreate(rc); - else if (rc instanceof ExpContext) - return expCreate(rc); - else if (rc instanceof OperandContext) - return operandCreate(rc); else if (rc instanceof LiteralExpressionContext) return literalExpressionCreate(rc); else if (rc instanceof DotCallContext) @@ -111,53 +97,31 @@ private Expression startCreate(ParseTree rc) throws LJError { private Expression predCreate(ParseTree rc) throws LJError { if (rc instanceof PredGroupContext) return new GroupExpression(create(((PredGroupContext) rc).pred())); - else if (rc instanceof PredNegateContext) - return new UnaryExpression("!", create(((PredNegateContext) rc).pred())); + else if (rc instanceof OpLiteralContext) + return create(((OpLiteralContext) rc).literalExpression()); + else if (rc instanceof OpMinusContext) + return new UnaryExpression("-", create(((OpMinusContext) rc).pred())); + else if (rc instanceof OpNotContext) + return new UnaryExpression("!", create(((OpNotContext) rc).pred())); + else if (rc instanceof OpArithContext) + return new BinaryExpression(create(((OpArithContext) rc).pred(0)), + ((OpArithContext) rc).getChild(1).getText(), create(((OpArithContext) rc).pred(1))); + else if (rc instanceof ExpBoolContext) + return new BinaryExpression(create(((ExpBoolContext) rc).pred(0)), ((ExpBoolContext) rc).BOOLOP().getText(), + create(((ExpBoolContext) rc).pred(1))); else if (rc instanceof PredLogicContext) return new BinaryExpression(create(((PredLogicContext) rc).pred(0)), - ((PredLogicContext) rc).LOGOP().getText(), create(((PredLogicContext) rc).pred(1))); - else if (rc instanceof IteContext) + ((PredLogicContext) rc).getChild(1).getText(), create(((PredLogicContext) rc).pred(1))); + if (rc instanceof IteContext) return new Ite(create(((IteContext) rc).pred(0)), create(((IteContext) rc).pred(1)), create(((IteContext) rc).pred(2))); - else - return create(((PredExpContext) rc).exp()); - } - private Expression expCreate(ParseTree rc) throws LJError { - if (rc instanceof ExpGroupContext) - return new GroupExpression(create(((ExpGroupContext) rc).exp())); - else if (rc instanceof ExpBoolContext) { - return new BinaryExpression(create(((ExpBoolContext) rc).exp(0)), ((ExpBoolContext) rc).BOOLOP().getText(), - create(((ExpBoolContext) rc).exp(1))); - } else { - ExpOperandContext eoc = (ExpOperandContext) rc; - return create(eoc.operand()); - } - } - - private Expression operandCreate(ParseTree rc) throws LJError { - if (rc instanceof OpLiteralContext) - return create(((OpLiteralContext) rc).literalExpression()); - else if (rc instanceof OpArithContext) - return new BinaryExpression(create(((OpArithContext) rc).operand(0)), - ((OpArithContext) rc).ARITHOP().getText(), create(((OpArithContext) rc).operand(1))); - else if (rc instanceof OpSubContext) - return new BinaryExpression(create(((OpSubContext) rc).operand(0)), "-", - create(((OpSubContext) rc).operand(1))); - else if (rc instanceof OpMinusContext) - return new UnaryExpression("-", create(((OpMinusContext) rc).operand())); - else if (rc instanceof OpNotContext) - return new UnaryExpression("!", create(((OpNotContext) rc).operand())); - else if (rc instanceof OpGroupContext) - return new GroupExpression(create(((OpGroupContext) rc).operand())); assert false; return null; } private Expression literalExpressionCreate(ParseTree rc) throws LJError { - if (rc instanceof LitGroupContext) - return new GroupExpression(create(((LitGroupContext) rc).literalExpression())); - else if (rc instanceof LitContext) + if (rc instanceof LitContext) return create(((LitContext) rc).literal()); else if (rc instanceof VarContext) return new Var(((VarContext) rc).ID().getText()); From f53a4177c51c981e184cba807789bd0d4e83cec5 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Tue, 5 May 2026 13:42:31 +0100 Subject: [PATCH 2/2] Add Extra Token Text --- .../src/main/java/testSuite/ErrorExtraToken.java | 12 ++++++++++++ 1 file changed, 12 insertions(+) create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorExtraToken.java diff --git a/liquidjava-example/src/main/java/testSuite/ErrorExtraToken.java b/liquidjava-example/src/main/java/testSuite/ErrorExtraToken.java new file mode 100644 index 00000000..9c594065 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorExtraToken.java @@ -0,0 +1,12 @@ +package testSuite; + +import liquidjava.specification.Refinement; + +@SuppressWarnings("unused") +public class ErrorExtraToken { + + void test() { + @Refinement("true false") // Syntax Error + int a = 1; + } +}