Skip to content

Commit 3562af1

Browse files
rcosta358rcosta358
authored
Add Ghost Dot Syntax (#142)
1 parent e7933ea commit 3562af1

7 files changed

Lines changed: 170 additions & 9 deletions

File tree

‎liquidjava-example/src/main/java/testSuite/CorrectDotNotationIncrementOnce.java‎

Lines changed: 21 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,21 @@
1+
package testSuite;
2+
3+
import liquidjava.specification.Ghost;
4+
import liquidjava.specification.StateRefinement;
5+
6+
@Ghost("int n")
7+
public class CorrectDotNotationIncrementOnce {
8+
9+
// explicit this
10+
@StateRefinement(to="this.n() == 0")
11+
public CorrectDotNotationIncrementOnce() {}
12+
13+
// implicit this
14+
@StateRefinement(from="n() == 0", to="n() == old(this).n() + 1")
15+
public void incrementOnce() {}
16+
17+
public static void main(String[] args) {
18+
CorrectDotNotationIncrementOnce t = new CorrectDotNotationIncrementOnce();
19+
t.incrementOnce();
20+
}
21+
}

‎liquidjava-example/src/main/java/testSuite/CorrectDotNotationTrafficLight.java‎

Lines changed: 27 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,27 @@
1+
package testSuite;
2+
3+
import liquidjava.specification.StateRefinement;
4+
import liquidjava.specification.StateSet;
5+
6+
@StateSet({"green", "amber", "red"})
7+
public class CorrectDotNotationTrafficLight {
8+
9+
@StateRefinement(to="this.green()")
10+
public CorrectDotNotationTrafficLight() {}
11+
12+
@StateRefinement(from="this.green()", to="this.amber()")
13+
public void transitionToAmber() {}
14+
15+
@StateRefinement(from="red()", to="green()")
16+
public void transitionToGreen() {}
17+
18+
@StateRefinement(from="this.amber()", to="red()")
19+
public void transitionToRed() {}
20+
21+
public static void main(String[] args) {
22+
CorrectDotNotationTrafficLight tl = new CorrectDotNotationTrafficLight();
23+
tl.transitionToAmber();
24+
tl.transitionToRed();
25+
tl.transitionToGreen();
26+
}
27+
}

‎liquidjava-example/src/main/java/testSuite/ErrorDotNotationIncrementOnce.java‎

Lines changed: 21 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,21 @@
1+
// State Refinement Error
2+
package testSuite;
3+
4+
import liquidjava.specification.Ghost;
5+
import liquidjava.specification.StateRefinement;
6+
7+
@Ghost("int n")
8+
public class ErrorDotNotationIncrementOnce {
9+
10+
@StateRefinement(to="this.n() == 0")
11+
public ErrorDotNotationIncrementOnce() {}
12+
13+
@StateRefinement(from="n() == 0", to="n() == old(this).n() + 1")
14+
public void incrementOnce() {}
15+
16+
public static void main(String[] args) {
17+
ErrorDotNotationIncrementOnce t = new ErrorDotNotationIncrementOnce();
18+
t.incrementOnce();
19+
t.incrementOnce(); // error
20+
}
21+
}

‎liquidjava-example/src/main/java/testSuite/ErrorDotNotationMultiple.java‎

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
// Syntax Error
2+
package testSuite;
3+
4+
import liquidjava.specification.Ghost;
5+
import liquidjava.specification.Refinement;
6+
import liquidjava.specification.StateRefinement;
7+
8+
@Ghost("int size")
9+
public class ErrorDotNotationMultiple {
10+
11+
@StateRefinement(to="size() == 0")
12+
public ErrorDotNotationMultiple() {}
13+
14+
void test() {
15+
@Refinement("_ == this.not.size()")
16+
int x = 0;
17+
}
18+
}

‎liquidjava-example/src/main/java/testSuite/ErrorDotNotationTrafficLight.java‎

Lines changed: 28 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,28 @@
1+
// State Refinement Error
2+
package testSuite;
3+
4+
import liquidjava.specification.StateRefinement;
5+
import liquidjava.specification.StateSet;
6+
7+
@StateSet({"green", "amber", "red"})
8+
public class ErrorDotNotationTrafficLight {
9+
10+
@StateRefinement(to="this.green()")
11+
public ErrorDotNotationTrafficLight() {}
12+
13+
@StateRefinement(from="this.green()", to="this.amber()")
14+
public void transitionToAmber() {}
15+
16+
@StateRefinement(from="red()", to="green()")
17+
public void transitionToGreen() {}
18+
19+
@StateRefinement(from="this.amber()", to="red()")
20+
public void transitionToRed() {}
21+
22+
public static void main(String[] args) {
23+
ErrorDotNotationTrafficLight tl = new ErrorDotNotationTrafficLight();
24+
tl.transitionToAmber();
25+
tl.transitionToGreen(); // error
26+
tl.transitionToRed();
27+
}
28+
}

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

Lines changed: 6 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -37,13 +37,17 @@ literalExpression:
3737
'(' literalExpression ')' #litGroup
3838
| literal #lit
3939
| ID #var
40-
| ID '.' functionCall #targetInvocation
4140
| functionCall #invocation
4241
;
4342

4443
functionCall:
4544
ghostCall
46-
| aliasCall;
45+
| aliasCall
46+
| dotCall;
47+
48+
dotCall:
49+
OBJECT_TYPE '(' args? ')'
50+
| ID '(' args? ')' '.' ID '(' args? ')';
4751

4852
ghostCall:
4953
ID '(' args? ')';

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

Lines changed: 49 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -19,11 +19,13 @@
1919
import liquidjava.rj_language.ast.UnaryExpression;
2020
import liquidjava.rj_language.ast.Var;
2121
import liquidjava.utils.Utils;
22+
import liquidjava.utils.constants.Keys;
2223

2324
import org.antlr.v4.runtime.tree.ParseTree;
2425
import org.apache.commons.lang3.NotImplementedException;
2526
import rj.grammar.RJParser.AliasCallContext;
2627
import rj.grammar.RJParser.ArgsContext;
28+
import rj.grammar.RJParser.DotCallContext;
2729
import rj.grammar.RJParser.ExpBoolContext;
2830
import rj.grammar.RJParser.ExpContext;
2931
import rj.grammar.RJParser.ExpGroupContext;
@@ -51,9 +53,7 @@
5153
import rj.grammar.RJParser.ProgContext;
5254
import rj.grammar.RJParser.StartContext;
5355
import rj.grammar.RJParser.StartPredContext;
54-
import rj.grammar.RJParser.TargetInvocationContext;
5556
import rj.grammar.RJParser.VarContext;
56-
import spoon.reflect.cu.SourcePosition;
5757
import liquidjava.diagnostics.errors.ArgumentMismatchError;
5858

5959
/**
@@ -82,6 +82,8 @@ else if (rc instanceof OperandContext)
8282
return operandCreate(rc);
8383
else if (rc instanceof LiteralExpressionContext)
8484
return literalExpressionCreate(rc);
85+
else if (rc instanceof DotCallContext)
86+
return dotCallCreate((DotCallContext) rc);
8587
else if (rc instanceof FunctionCallContext)
8688
return functionCallCreate((FunctionCallContext) rc);
8789
else if (rc instanceof LiteralContext)
@@ -156,9 +158,7 @@ else if (rc instanceof LitContext)
156158
return create(((LitContext) rc).literal());
157159
else if (rc instanceof VarContext) {
158160
return new Var(((VarContext) rc).ID().getText());
159-
} else if (rc instanceof TargetInvocationContext) {
160-
// TODO Finish Invocation with Target (a.len())
161-
return null;
161+
162162
} else {
163163
return create(((InvocationContext) rc).functionCall());
164164
}
@@ -171,15 +171,57 @@ private Expression functionCallCreate(FunctionCallContext rc) throws LJError {
171171
String name = Utils.qualifyName(prefix, ref);
172172
List<Expression> args = getArgs(gc.args());
173173
if (args.isEmpty())
174-
throw new ArgumentMismatchError("Ghost call cannot have empty arguments");
174+
args.add(new Var(Keys.THIS)); // implicit this: size() => this.size()
175+
175176
return new FunctionInvocation(name, args);
176-
} else {
177+
} else if (rc.aliasCall() != null) {
177178
AliasCallContext gc = rc.aliasCall();
178179
String ref = gc.ID_UPPER().getText();
179180
List<Expression> args = getArgs(gc.args());
180181
if (args.isEmpty())
181182
throw new ArgumentMismatchError("Alias call cannot have empty arguments");
183+
182184
return new AliasInvocation(ref, args);
185+
} else {
186+
return dotCallCreate(rc.dotCall());
187+
}
188+
}
189+
190+
/**
191+
* Handles both cases of dot calls: this.func(args) and targetFunc(this).func(args) Converts them to func(this,
192+
* args) and func(targetFunc(this), args) respectively
193+
*/
194+
private Expression dotCallCreate(DotCallContext rc) throws LJError {
195+
if (rc.OBJECT_TYPE() != null) {
196+
String text = rc.OBJECT_TYPE().getText();
197+
198+
// check if there are multiple fields (e.g. this.a.b)
199+
if (text.chars().filter(ch -> ch == '.').count() > 1)
200+
throw new SyntaxError("Multiple dot notation is not allowed", text);
201+
202+
// this.func(args) => func(this, args)
203+
int dot = text.indexOf('.');
204+
String target = text.substring(0, dot);
205+
String simpleName = text.substring(dot + 1);
206+
String name = Utils.qualifyName(prefix, simpleName);
207+
List<Expression> args = getArgs(rc.args(0));
208+
if (!args.isEmpty() && args.get(0)instanceof Var v && v.getName().equals(Keys.THIS)
209+
&& target.equals(Keys.THIS))
210+
throw new SyntaxError("Cannot use both dot notation and explicit 'this' argument. Use either 'this."
211+
+ simpleName + "()' or '" + simpleName + "(this)'", text);
212+
213+
args.add(0, new Var(target));
214+
return new FunctionInvocation(name, args);
215+
216+
} else {
217+
// targetFunc(this).func(args) => func(targetFunc(this), args)
218+
String targetFunc = rc.ID(0).getText();
219+
String func = rc.ID(1).getText();
220+
String name = Utils.qualifyName(prefix, func);
221+
List<Expression> targetArgs = getArgs(rc.args(0));
222+
List<Expression> funcArgs = getArgs(rc.args(1));
223+
funcArgs.add(0, new FunctionInvocation(targetFunc, targetArgs));
224+
return new FunctionInvocation(name, funcArgs);
183225
}
184226
}
185227

0 commit comments

Comments
 (0)