Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
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
Original file line number Diff line number Diff line change
@@ -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;
}
}
12 changes: 12 additions & 0 deletions liquidjava-example/src/main/java/testSuite/ErrorExtraToken.java
Original file line number Diff line number Diff line change
@@ -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;
}
}
41 changes: 15 additions & 26 deletions liquidjava-verifier/src/main/antlr4/rj/grammar/RJ.g4
Original file line number Diff line number Diff line change
@@ -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
| <assoc=right> pred '-->' pred #predLogic
Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

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

ok didnt know you could use <assoc=right>

| <assoc=right> 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
Expand Down Expand Up @@ -93,9 +83,8 @@ type:
| type '[]';


LOGOP : '&&'|'||'| '-->';
BOOLOP : '=='|'!='|'>='|'>'|'<='|'<';
ARITHOP : '+'|'*'|'/'|'%';//|'-';
MULOP : '*'|'/'|'%';

BOOL : 'true' | 'false';
ID_UPPER: ([A-Z][a-zA-Z0-9]*);
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -71,7 +71,7 @@ private static ParseTree compile(String toParse, String errorMessage) throws Syn
private static Optional<String> 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();
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand All @@ -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;
Expand All @@ -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)
Expand Down Expand Up @@ -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());
Expand Down
Loading