Skip to content

Commit 0240947

Browse files
authored
Fix Operator Precedence (#209)
1 parent 48bf708 commit 0240947

5 files changed

Lines changed: 109 additions & 78 deletions

File tree

Lines changed: 66 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,66 @@
1+
package testSuite;
2+
3+
import liquidjava.specification.Refinement;
4+
5+
public class CorrectOperatorPrecedence {
6+
7+
@Refinement("_ == 1 + 2 * 0")
8+
int multiplicationBeforeAddition() {
9+
return 1;
10+
}
11+
12+
@Refinement("_ == (1 + 2) * 0")
13+
int groupedAdditionBeforeMultiplication() {
14+
return 0;
15+
}
16+
17+
@Refinement("_ == 10 - 3 - 1")
18+
int subtractionAssociatesLeft() {
19+
return 6;
20+
}
21+
22+
@Refinement("_ == 10 - (3 - 1)")
23+
int groupedSubtractionAssociatesRight() {
24+
return 8;
25+
}
26+
27+
@Refinement("_ == -2 + 3")
28+
int unaryBeforeAddition() {
29+
return 1;
30+
}
31+
32+
@Refinement("_ == (true || false && false)")
33+
boolean andBeforeOr() {
34+
return true;
35+
}
36+
37+
@Refinement("_ == (!false && false)")
38+
boolean notBeforeAnd() {
39+
return false;
40+
}
41+
42+
@Refinement("_ == (false --> true && false)")
43+
boolean andBeforeImplication() {
44+
return true;
45+
}
46+
47+
@Refinement("_ == (true || true --> false)")
48+
boolean orBeforeImplication() {
49+
return false;
50+
}
51+
52+
@Refinement("_ == (false --> false && false)")
53+
boolean anotherAndBeforeImplication() {
54+
return true;
55+
}
56+
57+
@Refinement("_ == (false --> true --> false)")
58+
boolean implicationAssociatesRight() {
59+
return true;
60+
}
61+
62+
@Refinement("_ == (true ? false : true ? false : true)")
63+
boolean ternaryAssociatesRight() {
64+
return false;
65+
}
66+
}
Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
package testSuite;
2+
3+
import liquidjava.specification.Refinement;
4+
5+
@SuppressWarnings("unused")
6+
public class ErrorExtraToken {
7+
8+
void test() {
9+
@Refinement("true false") // Syntax Error
10+
int a = 1;
11+
}
12+
}

liquidjava-verifier/src/main/antlr4/rj/grammar/RJ.g4

Lines changed: 15 additions & 26 deletions
Original file line numberDiff line numberDiff line change
@@ -1,41 +1,31 @@
11
grammar RJ;
22

33

4-
prog: start | ;
4+
prog: start EOF;
55
start:
66
pred #startPred
77
| alias #startAlias
88
| ghost #startGhost
99
;
1010

11+
//----------------------- Predicates -----------------------
1112

1213
pred:
13-
'(' pred ')' #predGroup
14-
| '!' pred #predNegate
15-
| pred LOGOP pred #predLogic
16-
| pred '?' pred ':' pred #ite
17-
| exp #predExp
14+
'-' pred #opMinus
15+
| '!' pred #opNot
16+
| '(' pred ')' #predGroup
17+
| literalExpression #opLiteral
18+
| pred MULOP pred #opArith
19+
| pred ('+'|'-') pred #opArith
20+
| pred BOOLOP pred #expBool
21+
| pred '&&' pred #predLogic
22+
| pred '||' pred #predLogic
23+
| <assoc=right> pred '-->' pred #predLogic
24+
| <assoc=right> pred '?' pred ':' pred #ite
1825
;
1926

20-
exp:
21-
'(' exp ')' #expGroup
22-
| exp BOOLOP exp #expBool
23-
| operand #expOperand
24-
;
25-
26-
operand:
27-
literalExpression #opLiteral
28-
| operand ARITHOP operand #opArith
29-
| operand '-' operand #opSub
30-
| '-' operand #opMinus
31-
| '!' operand #opNot
32-
| '(' operand ')' #opGroup
33-
;
34-
35-
3627
literalExpression:
37-
'(' literalExpression ')' #litGroup
38-
| literal #lit
28+
literal #lit
3929
| ID #var
4030
| functionCall #invocation
4131
| enumerate #enum
@@ -93,9 +83,8 @@ type:
9383
| type '[]';
9484

9585

96-
LOGOP : '&&'|'||'| '-->';
9786
BOOLOP : '=='|'!='|'>='|'>'|'<='|'<';
98-
ARITHOP : '+'|'*'|'/'|'%';//|'-';
87+
MULOP : '*'|'/'|'%';
9988

10089
BOOL : 'true' | 'false';
10190
ID_UPPER: ([A-Z][a-zA-Z0-9]*);

liquidjava-verifier/src/main/java/liquidjava/rj_language/parsing/RefinementsParser.java

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -71,7 +71,7 @@ private static ParseTree compile(String toParse, String errorMessage) throws Syn
7171
private static Optional<String> getErrors(String toParse) {
7272
RJErrorListener err = new RJErrorListener();
7373
RJParser parser = createParser(toParse, err);
74-
parser.start(); // all consumed
74+
parser.prog(); // all consumed
7575
if (err.getErrors() > 0)
7676
return Optional.of(err.getMessages());
7777
return Optional.empty();

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

Lines changed: 15 additions & 51 deletions
Original file line numberDiff line numberDiff line change
@@ -20,7 +20,6 @@
2020
import liquidjava.rj_language.ast.UnaryExpression;
2121
import liquidjava.rj_language.ast.Var;
2222
import liquidjava.utils.Utils;
23-
import liquidjava.utils.constants.Formats;
2423
import liquidjava.utils.constants.Keys;
2524

2625
import org.antlr.v4.runtime.tree.ParseTree;
@@ -30,29 +29,20 @@
3029
import rj.grammar.RJParser.DotCallContext;
3130
import rj.grammar.RJParser.EnumContext;
3231
import rj.grammar.RJParser.ExpBoolContext;
33-
import rj.grammar.RJParser.ExpContext;
34-
import rj.grammar.RJParser.ExpGroupContext;
35-
import rj.grammar.RJParser.ExpOperandContext;
3632
import rj.grammar.RJParser.FunctionCallContext;
3733
import rj.grammar.RJParser.GhostCallContext;
3834
import rj.grammar.RJParser.InvocationContext;
3935
import rj.grammar.RJParser.IteContext;
4036
import rj.grammar.RJParser.LitContext;
41-
import rj.grammar.RJParser.LitGroupContext;
4237
import rj.grammar.RJParser.LiteralContext;
4338
import rj.grammar.RJParser.LiteralExpressionContext;
4439
import rj.grammar.RJParser.OpArithContext;
45-
import rj.grammar.RJParser.OpGroupContext;
4640
import rj.grammar.RJParser.OpLiteralContext;
4741
import rj.grammar.RJParser.OpMinusContext;
4842
import rj.grammar.RJParser.OpNotContext;
49-
import rj.grammar.RJParser.OpSubContext;
50-
import rj.grammar.RJParser.OperandContext;
5143
import rj.grammar.RJParser.PredContext;
52-
import rj.grammar.RJParser.PredExpContext;
5344
import rj.grammar.RJParser.PredGroupContext;
5445
import rj.grammar.RJParser.PredLogicContext;
55-
import rj.grammar.RJParser.PredNegateContext;
5646
import rj.grammar.RJParser.ProgContext;
5747
import rj.grammar.RJParser.StartContext;
5848
import rj.grammar.RJParser.StartPredContext;
@@ -79,10 +69,6 @@ else if (rc instanceof StartContext)
7969
return startCreate(rc);
8070
else if (rc instanceof PredContext)
8171
return predCreate(rc);
82-
else if (rc instanceof ExpContext)
83-
return expCreate(rc);
84-
else if (rc instanceof OperandContext)
85-
return operandCreate(rc);
8672
else if (rc instanceof LiteralExpressionContext)
8773
return literalExpressionCreate(rc);
8874
else if (rc instanceof DotCallContext)
@@ -111,53 +97,31 @@ private Expression startCreate(ParseTree rc) throws LJError {
11197
private Expression predCreate(ParseTree rc) throws LJError {
11298
if (rc instanceof PredGroupContext)
11399
return new GroupExpression(create(((PredGroupContext) rc).pred()));
114-
else if (rc instanceof PredNegateContext)
115-
return new UnaryExpression("!", create(((PredNegateContext) rc).pred()));
100+
else if (rc instanceof OpLiteralContext)
101+
return create(((OpLiteralContext) rc).literalExpression());
102+
else if (rc instanceof OpMinusContext)
103+
return new UnaryExpression("-", create(((OpMinusContext) rc).pred()));
104+
else if (rc instanceof OpNotContext)
105+
return new UnaryExpression("!", create(((OpNotContext) rc).pred()));
106+
else if (rc instanceof OpArithContext)
107+
return new BinaryExpression(create(((OpArithContext) rc).pred(0)),
108+
((OpArithContext) rc).getChild(1).getText(), create(((OpArithContext) rc).pred(1)));
109+
else if (rc instanceof ExpBoolContext)
110+
return new BinaryExpression(create(((ExpBoolContext) rc).pred(0)), ((ExpBoolContext) rc).BOOLOP().getText(),
111+
create(((ExpBoolContext) rc).pred(1)));
116112
else if (rc instanceof PredLogicContext)
117113
return new BinaryExpression(create(((PredLogicContext) rc).pred(0)),
118-
((PredLogicContext) rc).LOGOP().getText(), create(((PredLogicContext) rc).pred(1)));
119-
else if (rc instanceof IteContext)
114+
((PredLogicContext) rc).getChild(1).getText(), create(((PredLogicContext) rc).pred(1)));
115+
if (rc instanceof IteContext)
120116
return new Ite(create(((IteContext) rc).pred(0)), create(((IteContext) rc).pred(1)),
121117
create(((IteContext) rc).pred(2)));
122-
else
123-
return create(((PredExpContext) rc).exp());
124-
}
125118

126-
private Expression expCreate(ParseTree rc) throws LJError {
127-
if (rc instanceof ExpGroupContext)
128-
return new GroupExpression(create(((ExpGroupContext) rc).exp()));
129-
else if (rc instanceof ExpBoolContext) {
130-
return new BinaryExpression(create(((ExpBoolContext) rc).exp(0)), ((ExpBoolContext) rc).BOOLOP().getText(),
131-
create(((ExpBoolContext) rc).exp(1)));
132-
} else {
133-
ExpOperandContext eoc = (ExpOperandContext) rc;
134-
return create(eoc.operand());
135-
}
136-
}
137-
138-
private Expression operandCreate(ParseTree rc) throws LJError {
139-
if (rc instanceof OpLiteralContext)
140-
return create(((OpLiteralContext) rc).literalExpression());
141-
else if (rc instanceof OpArithContext)
142-
return new BinaryExpression(create(((OpArithContext) rc).operand(0)),
143-
((OpArithContext) rc).ARITHOP().getText(), create(((OpArithContext) rc).operand(1)));
144-
else if (rc instanceof OpSubContext)
145-
return new BinaryExpression(create(((OpSubContext) rc).operand(0)), "-",
146-
create(((OpSubContext) rc).operand(1)));
147-
else if (rc instanceof OpMinusContext)
148-
return new UnaryExpression("-", create(((OpMinusContext) rc).operand()));
149-
else if (rc instanceof OpNotContext)
150-
return new UnaryExpression("!", create(((OpNotContext) rc).operand()));
151-
else if (rc instanceof OpGroupContext)
152-
return new GroupExpression(create(((OpGroupContext) rc).operand()));
153119
assert false;
154120
return null;
155121
}
156122

157123
private Expression literalExpressionCreate(ParseTree rc) throws LJError {
158-
if (rc instanceof LitGroupContext)
159-
return new GroupExpression(create(((LitGroupContext) rc).literalExpression()));
160-
else if (rc instanceof LitContext)
124+
if (rc instanceof LitContext)
161125
return create(((LitContext) rc).literal());
162126
else if (rc instanceof VarContext)
163127
return new Var(((VarContext) rc).ID().getText());

0 commit comments

Comments
 (0)