From c877ae8e4220b1c44a048d1fcb579a09c0dd5dd7 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Fri, 6 Feb 2026 16:33:52 +0000 Subject: [PATCH] Add Ghost Dot Syntax --- .../CorrectDotNotationIncrementOnce.java | 21 +++++++++ .../CorrectDotNotationTrafficLight.java | 27 +++++++++++ .../ErrorDotNotationIncrementOnce.java | 21 +++++++++ .../ErrorDotNotationTrafficLight.java | 28 +++++++++++ .../src/main/antlr4/rj/grammar/RJ.g4 | 8 +++- .../visitors/CreateASTVisitor.java | 47 ++++++++++++++++--- 6 files changed, 143 insertions(+), 9 deletions(-) create mode 100644 liquidjava-example/src/main/java/testSuite/CorrectDotNotationIncrementOnce.java create mode 100644 liquidjava-example/src/main/java/testSuite/CorrectDotNotationTrafficLight.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorDotNotationIncrementOnce.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorDotNotationTrafficLight.java diff --git a/liquidjava-example/src/main/java/testSuite/CorrectDotNotationIncrementOnce.java b/liquidjava-example/src/main/java/testSuite/CorrectDotNotationIncrementOnce.java new file mode 100644 index 00000000..8eb1174c --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/CorrectDotNotationIncrementOnce.java @@ -0,0 +1,21 @@ +package testSuite; + +import liquidjava.specification.Ghost; +import liquidjava.specification.StateRefinement; + +@Ghost("int n") +public class CorrectDotNotationIncrementOnce { + + // explicit this + @StateRefinement(to="this.n() == 0") + public CorrectDotNotationIncrementOnce() {} + + // implicit this + @StateRefinement(from="n() == 0", to="n() == old(this).n() + 1") + public void incrementOnce() {} + + public static void main(String[] args) { + CorrectDotNotationIncrementOnce t = new CorrectDotNotationIncrementOnce(); + t.incrementOnce(); + } +} diff --git a/liquidjava-example/src/main/java/testSuite/CorrectDotNotationTrafficLight.java b/liquidjava-example/src/main/java/testSuite/CorrectDotNotationTrafficLight.java new file mode 100644 index 00000000..aaef95fe --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/CorrectDotNotationTrafficLight.java @@ -0,0 +1,27 @@ +package testSuite; + +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@StateSet({"green", "amber", "red"}) +public class CorrectDotNotationTrafficLight { + + @StateRefinement(to="this.green()") + public CorrectDotNotationTrafficLight() {} + + @StateRefinement(from="this.green()", to="this.amber()") + public void transitionToAmber() {} + + @StateRefinement(from="red()", to="green()") + public void transitionToGreen() {} + + @StateRefinement(from="this.amber()", to="red()") + public void transitionToRed() {} + + public static void main(String[] args) { + CorrectDotNotationTrafficLight tl = new CorrectDotNotationTrafficLight(); + tl.transitionToAmber(); + tl.transitionToRed(); + tl.transitionToGreen(); + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorDotNotationIncrementOnce.java b/liquidjava-example/src/main/java/testSuite/ErrorDotNotationIncrementOnce.java new file mode 100644 index 00000000..8bf06584 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorDotNotationIncrementOnce.java @@ -0,0 +1,21 @@ +// State Refinement Error +package testSuite; + +import liquidjava.specification.Ghost; +import liquidjava.specification.StateRefinement; + +@Ghost("int n") +public class ErrorDotNotationIncrementOnce { + + @StateRefinement(to="this.n() == 0") + public ErrorDotNotationIncrementOnce() {} + + @StateRefinement(from="n() == 0", to="n() == old(this).n() + 1") + public void incrementOnce() {} + + public static void main(String[] args) { + ErrorDotNotationIncrementOnce t = new ErrorDotNotationIncrementOnce(); + t.incrementOnce(); + t.incrementOnce(); // error + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorDotNotationTrafficLight.java b/liquidjava-example/src/main/java/testSuite/ErrorDotNotationTrafficLight.java new file mode 100644 index 00000000..e40ddb30 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorDotNotationTrafficLight.java @@ -0,0 +1,28 @@ +// State Refinement Error +package testSuite; + +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@StateSet({"green", "amber", "red"}) +public class ErrorDotNotationTrafficLight { + + @StateRefinement(to="this.green()") + public ErrorDotNotationTrafficLight() {} + + @StateRefinement(from="this.green()", to="this.amber()") + public void transitionToAmber() {} + + @StateRefinement(from="red()", to="green()") + public void transitionToGreen() {} + + @StateRefinement(from="this.amber()", to="red()") + public void transitionToRed() {} + + public static void main(String[] args) { + ErrorDotNotationTrafficLight tl = new ErrorDotNotationTrafficLight(); + tl.transitionToAmber(); + tl.transitionToGreen(); // error + tl.transitionToRed(); + } +} diff --git a/liquidjava-verifier/src/main/antlr4/rj/grammar/RJ.g4 b/liquidjava-verifier/src/main/antlr4/rj/grammar/RJ.g4 index e34f40ad..d6f7f45f 100644 --- a/liquidjava-verifier/src/main/antlr4/rj/grammar/RJ.g4 +++ b/liquidjava-verifier/src/main/antlr4/rj/grammar/RJ.g4 @@ -37,13 +37,17 @@ literalExpression: '(' literalExpression ')' #litGroup | literal #lit | ID #var - | ID '.' functionCall #targetInvocation | functionCall #invocation ; functionCall: ghostCall - | aliasCall; + | aliasCall + | dotCall; + +dotCall: + OBJECT_TYPE '(' args? ')' + | ID '(' args? ')' '.' ID '(' args? ')'; ghostCall: ID '(' args? ')'; 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 1bedda99..2967a799 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 @@ -19,11 +19,13 @@ import liquidjava.rj_language.ast.UnaryExpression; import liquidjava.rj_language.ast.Var; import liquidjava.utils.Utils; +import liquidjava.utils.constants.Keys; import org.antlr.v4.runtime.tree.ParseTree; import org.apache.commons.lang3.NotImplementedException; import rj.grammar.RJParser.AliasCallContext; import rj.grammar.RJParser.ArgsContext; +import rj.grammar.RJParser.DotCallContext; import rj.grammar.RJParser.ExpBoolContext; import rj.grammar.RJParser.ExpContext; import rj.grammar.RJParser.ExpGroupContext; @@ -51,9 +53,7 @@ import rj.grammar.RJParser.ProgContext; import rj.grammar.RJParser.StartContext; import rj.grammar.RJParser.StartPredContext; -import rj.grammar.RJParser.TargetInvocationContext; import rj.grammar.RJParser.VarContext; -import spoon.reflect.cu.SourcePosition; import liquidjava.diagnostics.errors.ArgumentMismatchError; /** @@ -82,6 +82,8 @@ else if (rc instanceof OperandContext) return operandCreate(rc); else if (rc instanceof LiteralExpressionContext) return literalExpressionCreate(rc); + else if (rc instanceof DotCallContext) + return dotCallCreate((DotCallContext) rc); else if (rc instanceof FunctionCallContext) return functionCallCreate((FunctionCallContext) rc); else if (rc instanceof LiteralContext) @@ -156,9 +158,7 @@ else if (rc instanceof LitContext) return create(((LitContext) rc).literal()); else if (rc instanceof VarContext) { return new Var(((VarContext) rc).ID().getText()); - } else if (rc instanceof TargetInvocationContext) { - // TODO Finish Invocation with Target (a.len()) - return null; + } else { return create(((InvocationContext) rc).functionCall()); } @@ -171,15 +171,48 @@ private Expression functionCallCreate(FunctionCallContext rc) throws LJError { String name = Utils.qualifyName(prefix, ref); List args = getArgs(gc.args()); if (args.isEmpty()) - throw new ArgumentMismatchError("Ghost call cannot have empty arguments"); + args.add(new Var(Keys.THIS)); // implicit this: size() => this.size() + return new FunctionInvocation(name, args); - } else { + } else if (rc.aliasCall() != null) { AliasCallContext gc = rc.aliasCall(); String ref = gc.ID_UPPER().getText(); List args = getArgs(gc.args()); if (args.isEmpty()) throw new ArgumentMismatchError("Alias call cannot have empty arguments"); + return new AliasInvocation(ref, args); + } else { + return dotCallCreate(rc.dotCall()); + } + } + + private Expression dotCallCreate(DotCallContext rc) throws LJError { + if (rc.OBJECT_TYPE() != null) { + // this.func(args) + String text = rc.OBJECT_TYPE().getText(); + int dot = text.indexOf('.'); + String target = text.substring(0, dot); + String simpleName = text.substring(dot + 1); + String name = Utils.qualifyName(prefix, simpleName); + List args = getArgs(rc.args(0)); + if (!args.isEmpty() && args.get(0)instanceof Var v && v.getName().equals(Keys.THIS) + && target.equals(Keys.THIS)) + throw new SyntaxError("Cannot use both dot notation and explicit 'this' argument. Use either 'this." + + simpleName + "()' or '" + simpleName + "(this)'", text); + + args.add(0, new Var(target)); + return new FunctionInvocation(name, args); + + } else { + // targetFunc(this).func(args) + String targetFunc = rc.ID(0).getText(); + String func = rc.ID(1).getText(); + String name = Utils.qualifyName(prefix, func); + List targetArgs = getArgs(rc.args(0)); + List funcArgs = getArgs(rc.args(1)); + funcArgs.add(0, new FunctionInvocation(targetFunc, targetArgs)); + return new FunctionInvocation(name, funcArgs); } }