Fix collisions between same-named fields

liquidjava-example/src/main/java/testSuite/CorrectCombinedNestedFields.java

@@ -0,0 +1,33 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+public class CorrectCombinedNestedFields {
+    @Refinement("_ < 0")
+    int port = -1;
+
+    private final Job job = new Job();
+
+    static class Marker {
+        int value;
+    }
+
+    @Refinement("_ < 0")
+    public int getOuterPort() {
+        return port;
+    }
+
+    @Refinement("_ >= 0")
+    public int getJobPort() {
+        return job.port;
+    }
+
+    public void send() {
+        job.port = 5;
+    }
+
+    static class Job {
+        @Refinement("_ >= 0")
+        int port;
+    }
+}

liquidjava-example/src/main/java/testSuite/CorrectDistinctClassFields.java

@@ -0,0 +1,16 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+public class CorrectDistinctClassFields {
+    @Refinement("_ < 0") int port = -1;
+    private final Job job = new Job();
+
+    public void send() {
+        job.port = 5;
+    }
+
+    static class Job {
+        @Refinement("_ >= 0") int port;
+    }
+}

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java

@@ -15,6 +15,7 @@
 import liquidjava.rj_language.Predicate;
 import liquidjava.rj_language.ast.Enum;
 import liquidjava.utils.StaticConstants;
+import liquidjava.utils.Utils;
 import liquidjava.utils.constants.Formats;
 import liquidjava.utils.constants.Keys;
 import liquidjava.utils.constants.Types;
@@ -220,7 +221,7 @@ private <T, A extends T> void visitAssignment(CtAssignment<T, A> assignment) thr
         } else if (ex instanceof CtFieldWrite<?> fw) {
             CtFieldReference<?> cr = fw.getVariable();
             CtField<?> f = fw.getVariable().getDeclaration();
-            String updatedVarName = String.format(Formats.THIS, cr.getSimpleName());
+            String updatedVarName = Utils.qualifyFieldName(cr);
             checkAssignment(updatedVarName, cr.getType(), ex, assignment.getAssignment(), assignment, f);
 
             // corresponding ghost function update
@@ -261,7 +262,7 @@ public <T> void visitCtLiteral(CtLiteral<T> lit) {
     public <T> void visitCtField(CtField<T> f) {
         super.visitCtField(f);
         Optional<Predicate> c = getRefinementFromAnnotation(f);
-        String name = String.format(Formats.THIS, f.getSimpleName());
+        String name = Utils.qualifyFieldName(f.getReference());
         Predicate ret = new Predicate();
         if (c.isPresent()) {
             ret = c.get().substituteVariable(Keys.WILDCARD, name).substituteVariable(f.getSimpleName(), name);
@@ -291,8 +292,8 @@ public <T> void visitCtFieldRead(CtFieldRead<T> fieldRead) {
                         Predicate.createEquals(Predicate.createVar(Keys.WILDCARD), Predicate.createVar(fieldName)));
             }
 
-        } else if (context.hasVariable(String.format(Formats.THIS, fieldName))) {
-            String thisName = String.format(Formats.THIS, fieldName);
+        } else if (context.hasVariable(Utils.qualifyFieldName(fieldRead.getVariable()))) {
+            String thisName = Utils.qualifyFieldName(fieldRead.getVariable());
             fieldRead.putMetadata(Keys.REFINEMENT,
                     Predicate.createEquals(Predicate.createVar(Keys.WILDCARD), Predicate.createVar(thisName)));
 

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java

@@ -10,13 +10,15 @@
 import liquidjava.processor.context.Variable;
 import liquidjava.processor.context.VariableInstance;
 import liquidjava.processor.refinement_checker.TypeChecker;
+import liquidjava.utils.Utils;
 import liquidjava.utils.constants.Formats;
 import liquidjava.utils.constants.Keys;
 import liquidjava.utils.constants.Ops;
 import liquidjava.utils.constants.Types;
 import liquidjava.rj_language.Predicate;
 import liquidjava.rj_language.ast.BinaryExpression;
 import liquidjava.rj_language.ast.Expression;
+import liquidjava.rj_language.ast.UnaryExpression;
 import org.apache.commons.lang3.NotImplementedException;
 import spoon.reflect.code.BinaryOperatorKind;
 import spoon.reflect.code.CtAssignment;
@@ -121,12 +123,19 @@ public Predicate getOperatorAssignmentRefinement(String assignedName, CtOperator
     @SuppressWarnings({ "unchecked" })
     public <T> void getUnaryOpRefinements(CtUnaryOperator<T> operator) throws LJError {
         CtExpression<T> ex = (CtExpression<T>) operator.getOperand();
+        if (operator.getKind() == UnaryOperatorKind.NEG && ex instanceof CtLiteral<?> literal
+                && literal.getValue() instanceof Number) {
+            Predicate operand = Predicate.createLit(literal.getValue().toString(), ex.getType().getQualifiedName());
+            Predicate value = new Predicate(new UnaryExpression("-", operand.getExpression()));
+            operator.putMetadata(Keys.REFINEMENT, Predicate.createEquals(Predicate.createVar(Keys.WILDCARD), value));
+            return;
+        }
         String name = Formats.FRESH;
         Predicate all;
         if (ex instanceof CtVariableWrite<T> w) {
             name = w.getVariable().getSimpleName();
-            if (w instanceof CtFieldWrite<?>)
-                name = String.format(Formats.THIS, name);
+            if (w instanceof CtFieldWrite<?> fieldWrite)
+                name = Utils.qualifyFieldName(fieldWrite.getVariable());
             all = getRefinementUnaryVariableWrite(ex, operator, w, name);
             rtc.checkVariableRefinements(all, name, w.getType(), operator, w.getVariable().getDeclaration());
             return;
@@ -203,8 +212,8 @@ private Predicate getOperationRefinements(CtBinaryOperator<?> operator, CtVariab
 
         if (element instanceof CtVariableRead<?> elemVar) {
             String elemName = elemVar.getVariable().getSimpleName();
-            if (elemVar instanceof CtFieldRead)
-                elemName = String.format(Formats.THIS, elemName);
+            if (elemVar instanceof CtFieldRead<?> fieldRead)
+                elemName = Utils.qualifyFieldName(fieldRead.getVariable());
             Predicate elemRef = rtc.getContext().getVariableRefinements(elemName);
 
             String returnName = elemName;
@@ -336,8 +345,8 @@ private Predicate getCurrentVariableValue(String name) {
     private Predicate getOperatorAssignmentRefinement(CtExpression<?> element) throws LJError {
         if (element instanceof CtVariableRead<?> variableRead) {
             String name = variableRead.getVariable().getSimpleName();
-            if (variableRead instanceof CtFieldRead<?>)
-                name = String.format(Formats.THIS, name);
+            if (variableRead instanceof CtFieldRead<?> fieldRead)
+                name = Utils.qualifyFieldName(fieldRead.getVariable());
             return getCurrentVariableValue(name);
         } else if (element instanceof CtBinaryOperator<?> binaryOperator) {
             Predicate left = getOperatorAssignmentRefinement(binaryOperator.getLeftHandOperand());

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java

@@ -180,13 +180,13 @@ private static ObjectState getStates(CtAnnotation<? extends Annotation> ctAnnota
 
         // has from
         if (from != null) {
-            state.setFrom(createStatePredicate(from, f.getTargetClass(), tc, e, false, prefix));
+            state.setFrom(createStatePredicate(new Predicate(from, e, prefix), from, f.getTargetClass(), tc, e, false));
             state.setFromPosition(Utils.getLJAnnotationPosition(e, from));
         }
 
         // has to
         if (to != null) {
-            state.setTo(createStatePredicate(to, f.getTargetClass(), tc, e, true, prefix));
+            state.setTo(createStatePredicate(new Predicate(to, e, prefix), to, f.getTargetClass(), tc, e, true));
             state.setToPosition(Utils.getLJAnnotationPosition(e, to));
         }
 
@@ -209,10 +209,9 @@ private static ObjectState getStates(CtAnnotation<? extends Annotation> ctAnnota
      * 
      * @return the created predicate
      */
-    private static Predicate createStatePredicate(String value, String targetClass, TypeChecker tc, CtElement e,
-            boolean isTo, String prefix) throws LJError {
+    private static Predicate createStatePredicate(Predicate p, String value, String targetClass, TypeChecker tc,
+            CtElement e, boolean isTo) throws LJError {
         SourcePosition position = Utils.getLJAnnotationPosition(e, value);
-        Predicate p = new Predicate(value, e, prefix);
         if (!p.getExpression().isBooleanExpression()) {
             throw new InvalidRefinementError(position, "State refinement transition must be a boolean expression",
                     value);
@@ -392,7 +391,7 @@ public static void checkTargetChanges(TypeChecker tc, RefinedFunction f, CtExpre
      */
     public static void updateGhostField(CtFieldWrite<?> fw, TypeChecker tc) throws LJError {
         CtField<?> field = fw.getVariable().getDeclaration();
-        String updatedVarName = String.format(Formats.THIS, fw.getVariable().getSimpleName());
+        String updatedVarName = Utils.qualifyFieldName(fw.getVariable());
         String targetClass = field.getDeclaringType().getQualifiedName();
 
         // state transition annotation construction
@@ -421,8 +420,12 @@ public static void updateGhostField(CtFieldWrite<?> fw, TypeChecker tc) throws L
 
         ObjectState stateChange = new ObjectState();
         String prefix = field.getDeclaringType().getQualifiedName();
-        Predicate fromPredicate = createStatePredicate(stateChangeRefinementFrom, targetClass, tc, fw, false, prefix);
-        Predicate toPredicate = createStatePredicate(stateChangeRefinementTo, targetClass, tc, fw, true, prefix);
+        Predicate fromPredicate = createStatePredicate(new Predicate(), stateChangeRefinementFrom, targetClass, tc, fw,
+                false);
+        Predicate toPredicate = Predicate.createEquals(Predicate
+                .createInvocation(Utils.qualifyName(prefix, field.getSimpleName()), Predicate.createVar(Keys.THIS)),
+                Predicate.createVar(updatedVarName));
+        toPredicate = createStatePredicate(toPredicate, stateChangeRefinementTo, targetClass, tc, fw, true);
         stateChange.setFrom(fromPredicate);
         stateChange.setTo(toPredicate);
 
@@ -604,7 +607,7 @@ public static String prepareInvocationTarget(TypeChecker tc, CtElement target2,
             // means invocation is in a form of `t.method(args)`
             String name = v.getVariable().getSimpleName();
             if (target2 instanceof CtFieldRead<?> fieldRead && fieldRead.getTarget() instanceof CtThisAccess<?>) {
-                String fieldName = String.format(Formats.THIS, name);
+                String fieldName = Utils.qualifyFieldName(fieldRead.getVariable());
                 if (tc.getContext().hasVariable(fieldName))
                     name = fieldName;
             }

liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java

@@ -19,6 +19,7 @@
 import spoon.reflect.declaration.CtElement;
 import spoon.reflect.declaration.CtMethod;
 import spoon.reflect.factory.Factory;
+import spoon.reflect.reference.CtFieldReference;
 import spoon.reflect.reference.CtTypeReference;
 import spoon.support.reflect.cu.position.SourcePositionImpl;
 
@@ -50,6 +51,10 @@ public static String qualifyName(String prefix, String name) {
         return String.format("%s.%s", prefix, name);
     }
 
+    public static String qualifyFieldName(CtFieldReference<?> field) {
+        return "this#" + field.getDeclaringType().getQualifiedName() + "." + field.getSimpleName();
+    }
+
     public static String getFile(CtElement element) {
         SourcePosition pos = element.getPosition();
         if (pos == null || pos.getFile() == null)