Merge branch 'main' into null-support

rcosta358 · rcosta358 · commit e959ce6fe01d · 2026-02-12T14:49:26.000Z
diff --git a/liquidjava-example/src/main/java/testSuite/CorrectDotNotationIncrementOnce.java 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
@@ -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
@@ -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/ErrorDotNotationMultiple.java b/liquidjava-example/src/main/java/testSuite/ErrorDotNotationMultiple.java
@@ -0,0 +1,18 @@
+// Syntax Error
+package testSuite;
+
+import liquidjava.specification.Ghost;
+import liquidjava.specification.Refinement;
+import liquidjava.specification.StateRefinement;
+
+@Ghost("int size")
+public class ErrorDotNotationMultiple {
+
+    @StateRefinement(to="size() == 0")
+    public ErrorDotNotationMultiple() {}
+
+    void test() {
+        @Refinement("_ == this.not.size()")
+        int x = 0;
+    }
+}
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorDotNotationTrafficLight.java 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-example/src/main/java/testSuite/ErrorSyntaxRefinement.java b/liquidjava-example/src/main/java/testSuite/ErrorSyntaxRefinement.java
@@ -4,7 +4,7 @@
 import liquidjava.specification.Refinement;
 
 @SuppressWarnings("unused")
-public class ErrorSyntax1 {
+public class ErrorSyntaxRefinement {
     public static void main(String[] args) {
         @Refinement("_ < 100 +")
         int value = 90 + 4;
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorSyntaxStateRefinement.java b/liquidjava-example/src/main/java/testSuite/ErrorSyntaxStateRefinement.java
@@ -0,0 +1,10 @@
+// Syntax Error
+package testSuite;
+
+import liquidjava.specification.StateRefinement;
+
+public class ErrorSyntaxStateRefinement {
+    
+    @StateRefinement(from="$", to="#")
+    void test() {}
+}
diff --git 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/diagnostics/errors/StateConflictError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateConflictError.java
@@ -17,7 +17,7 @@ public StateConflictError(SourcePosition position, Expression state, Translation
         super("State Conflict Error",
                 "Found multiple disjoint states in state transition: state transition can only go to one state of each state set",
                 position, translationTable);
-        this.state = state.toSimplifiedString();
+        this.state = state.toString();
     }
 
     public String getState() {
diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java
@@ -16,10 +16,11 @@ public class StateRefinementError extends LJError {
 
     public StateRefinementError(SourcePosition position, Expression expected, Expression found,
             TranslationTable translationTable, String customMessage) {
-        super("State Refinement Error", String.format("Expected state %s but found %s", expected.toSimplifiedString(),
-                found.toSimplifiedString()), position, translationTable, customMessage);
-        this.expected = expected.toSimplifiedString();
-        this.found = found.toSimplifiedString();
+        super("State Refinement Error",
+                String.format("Expected state %s but found %s", expected.toString(), found.toString()), position,
+                translationTable, customMessage);
+        this.expected = expected.toString();
+        this.found = found.toString();
     }
 
     public String getExpected() {
diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java
@@ -3,6 +3,7 @@
 import java.lang.annotation.Annotation;
 import java.util.Collections;
 import java.util.List;
+import java.util.Map;
 import java.util.Optional;
 
 import liquidjava.diagnostics.errors.*;
@@ -89,11 +90,13 @@ public Optional<Predicate> getRefinementFromAnnotation(CtElement element) throws
         return constr;
     }
 
+    @SuppressWarnings({ "rawtypes" })
     public Optional<String> getMessageFromAnnotation(CtElement element) {
         for (CtAnnotation<? extends Annotation> ann : element.getAnnotations()) {
             String an = ann.getActualAnnotation().annotationType().getCanonicalName();
             if (an.contentEquals("liquidjava.specification.Refinement")) {
-                String msg = getStringFromAnnotation(ann.getValue("msg"));
+                Map<String, CtExpression> values = ann.getAllValues();
+                String msg = getStringFromAnnotation((values.get("msg")));
                 if (msg != null && !msg.isEmpty()) {
                     return Optional.of(msg);
                 }
@@ -248,7 +251,7 @@ protected void handleAlias(String ref, CtElement element) throws LJError {
             }
         } catch (LJError e) {
             // add location info to error
-            SourcePosition pos = Utils.getRefinementAnnotationPosition(element, ref);
+            SourcePosition pos = Utils.getAnnotationPosition(element, ref);
             e.setPosition(pos);
             throw e;
         }
diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/MethodsFunctionsChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/MethodsFunctionsChecker.java
@@ -296,7 +296,7 @@ private Map<String, String> checkInvocationRefinements(CtElement invocation, Lis
         Predicate methodRef = f.getRefReturn();
 
         if (methodRef != null) {
-            boolean equalsThis = methodRef.toString().equals("(_ == this)"); // TODO change for better
+            boolean equalsThis = methodRef.toString().equals("_ == this"); // TODO change for better
             List<String> vars = methodRef.getVariableNames();
             for (String s : vars)
                 if (map.containsKey(s))
diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java
@@ -85,7 +85,7 @@ protected Expression parse(String ref, CtElement element) throws LJError {
             return RefinementsParser.createAST(ref, prefix);
         } catch (LJError e) {
             // add location info to error
-            SourcePosition pos = Utils.getRefinementAnnotationPosition(element, ref);
+            SourcePosition pos = Utils.getAnnotationPosition(element, ref);
             e.setPosition(pos);
             throw e;
         }
diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/AliasInvocation.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/AliasInvocation.java
@@ -34,12 +34,6 @@ public String toString() {
         return name + "(" + getArgs().stream().map(Expression::toString).collect(Collectors.joining(", ")) + ")";
     }
 
-    @Override
-    public String toSimplifiedString() {
-        return name + "(" + getArgs().stream().map(Expression::toSimplifiedString).collect(Collectors.joining(", "))
-                + ")";
-    }
-
     @Override
     public void getVariableNames(List<String> toAdd) {
         for (Expression e : getArgs())
diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/BinaryExpression.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/BinaryExpression.java
@@ -50,11 +50,6 @@ public String toString() {
         return getFirstOperand().toString() + " " + op + " " + getSecondOperand().toString();
     }
 
-    @Override
-    public String toSimplifiedString() {
-        return getFirstOperand().toSimplifiedString() + " " + op + " " + getSecondOperand().toSimplifiedString();
-    }
-
     @Override
     public void getVariableNames(List<String> toAdd) {
         getFirstOperand().getVariableNames(toAdd);
diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Expression.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Expression.java
@@ -36,17 +36,6 @@ public abstract class Expression {
 
     public abstract String toString();
 
-    /**
-     * Returns a simplified string representation of this expression with unqualified names (e.g.,
-     * com.example.State.open => open Default implementation delegates to toString() Subclasses that contain qualified
-     * names should override this method
-     *
-     * @return simplified string representation
-     */
-    public String toSimplifiedString() {
-        return toString();
-    }
-
     List<Expression> children = new ArrayList<>();
 
     public void addChild(Expression e) {
diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/FunctionInvocation.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/FunctionInvocation.java
@@ -37,14 +37,8 @@ public <T> T accept(ExpressionVisitor<T> visitor) throws LJError {
 
     @Override
     public String toString() {
-        return name + "(" + getArgs().stream().map(Expression::toString).collect(Collectors.joining(",")) + ")";
-    }
-
-    @Override
-    public String toSimplifiedString() {
-        String simpleName = Utils.getSimpleName(name);
-        return simpleName + "("
-                + getArgs().stream().map(Expression::toSimplifiedString).collect(Collectors.joining(",")) + ")";
+        return Utils.getSimpleName(name) + "("
+                + getArgs().stream().map(Expression::toString).collect(Collectors.joining(",")) + ")";
     }
 
     @Override
diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/GroupExpression.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/GroupExpression.java
@@ -21,12 +21,7 @@ public <T> T accept(ExpressionVisitor<T> visitor) throws LJError {
     }
 
     public String toString() {
-        return "(" + getExpression().toString() + ")";
-    }
-
-    @Override
-    public String toSimplifiedString() {
-        return getExpression().toSimplifiedString();
+        return getExpression().toString();
     }
 
     @Override
diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Ite.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Ite.java
@@ -32,13 +32,7 @@ public <T> T accept(ExpressionVisitor<T> visitor) throws LJError {
 
     @Override
     public String toString() {
-        return getCondition().toString() + "?" + getThen().toString() + ":" + getElse().toString();
-    }
-
-    @Override
-    public String toSimplifiedString() {
-        return getCondition().toSimplifiedString() + "?" + getThen().toSimplifiedString() + ":"
-                + getElse().toSimplifiedString();
+        return getCondition().toString() + " ? " + getThen().toString() + " : " + getElse().toString();
     }
 
     @Override
diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/UnaryExpression.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/UnaryExpression.java
@@ -32,11 +32,6 @@ public String toString() {
         return op + getExpression().toString();
     }
 
-    @Override
-    public String toSimplifiedString() {
-        return op + getExpression().toSimplifiedString();
-    }
-
     @Override
     public void getVariableNames(List<String> toAdd) {
         getExpression().getVariableNames(toAdd);
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
diff --git a/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java b/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java

Original file line number	Diff line number	Diff line change
`@@ -17,7 +17,7 @@ public StateConflictError(SourcePosition position, Expression state, Translation`
`17`	`17`	`super("State Conflict Error",`
`18`	`18`	`"Found multiple disjoint states in state transition: state transition can only go to one state of each state set",`
`19`	`19`	`position, translationTable);`
`20`		`- this.state = state.toSimplifiedString();`
	`20`	`+ this.state = state.toString();`
`21`	`21`	`}`
`22`	`22`
`23`	`23`	`public String getState() {`