Resolve field reads by declaring type and target object

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

@@ -0,0 +1,65 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+// #321, #322: field reads resolve to the field of the class and object they name
+public class CorrectFieldReadResolution {
+    enum Codec {
+        JPG, PNG
+    }
+
+    static final int LIMIT = 10;
+
+    @Refinement("val > 0")
+    int val;
+
+    int max = 5;
+
+    public CorrectFieldReadResolution(@Refinement("_ > 0") int v) {
+        val = v;
+    }
+
+    static void onlyPng(@Refinement("_ == Codec.PNG") Codec f) {}
+
+    void otherClass() {
+        @Refinement("_ == 10")
+        int k = Limits.max;
+        @Refinement("_ == 5")
+        int m = max;
+        @Refinement("_ == 5")
+        int t = this.max;
+    }
+
+    void otherObject(CorrectFieldReadResolution other) {
+        val = 7;
+        @Refinement("_ > 0")
+        int k = other.val;
+        @Refinement("_ > 7")
+        int s = val + other.val;
+        if (other.val == 3) {
+            @Refinement("_ == 7")
+            int t = val;
+        }
+        @Refinement("_ == 7")
+        int u = this.val;
+    }
+
+    static void sameNamedLocals() {
+        Codec JPG = Codec.JPG;
+        Codec PNG = Codec.PNG;
+        onlyPng(PNG);
+        onlyPng(Codec.PNG);
+        Codec g = Codec.PNG;
+        onlyPng(g);
+
+        int LIMIT = 3;
+        @Refinement("_ == 10")
+        int k = CorrectFieldReadResolution.LIMIT;
+        @Refinement("_ == 3")
+        int l = LIMIT;
+    }
+
+    static class Limits {
+        static final int max = 10;
+    }
+}

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

@@ -0,0 +1,17 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+// #322: Limits.max must not be read as this class's own field max
+public class ErrorFieldOfOtherClass {
+    int max = 5;
+
+    void check() {
+        @Refinement("_ == 5")
+        int k = Limits.max; // Expect: Refinement Error
+    }
+
+    static class Limits {
+        static final int max = 10;
+    }
+}

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

@@ -0,0 +1,41 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+// #322: other.val is a different object's field, not this.val
+public class ErrorFieldOfOtherObject {
+    @Refinement("val > 0")
+    int val;
+
+    public ErrorFieldOfOtherObject(@Refinement("_ > 0") int v) {
+        val = v;
+    }
+
+    void read(ErrorFieldOfOtherObject other) {
+        val = 7;
+        @Refinement("_ == 7")
+        int k = other.val; // Expect: Refinement Error
+    }
+
+    void sum(ErrorFieldOfOtherObject other) {
+        val = 7;
+        @Refinement("_ == 14")
+        int k = val + other.val; // Expect: Refinement Error
+    }
+
+    void compound(ErrorFieldOfOtherObject other) {
+        val = 7;
+        int j = 0;
+        j += other.val;
+        @Refinement("_ == 7")
+        int k = j; // Expect: Refinement Error
+    }
+
+    void condition(ErrorFieldOfOtherObject other) {
+        val = 7;
+        if (other.val == 3) {
+            @Refinement("_ == 3")
+            int k = val; // Expect: Refinement Error
+        }
+    }
+}

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

@@ -0,0 +1,26 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+// #321: a local named like a constant must not stand for the constant
+public class ErrorLocalShadowsConstant {
+    enum Encoding {
+        JPG, PNG
+    }
+
+    static final int LIMIT = 10;
+
+    static void onlyPng(@Refinement("_ == Encoding.PNG") Encoding f) {}
+
+    public static void main(String[] args) {
+        Encoding JPG = Encoding.PNG;
+        Encoding g = Encoding.JPG;
+        onlyPng(g); // Expect: Refinement Error
+    }
+
+    static void staticConstant() {
+        int LIMIT = 3;
+        @Refinement("_ == 3")
+        int k = ErrorLocalShadowsConstant.LIMIT; // Expect: Refinement Error
+    }
+}

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

@@ -316,17 +316,10 @@ public <T> void visitCtField(CtField<T> f) {
     @Override
     public <T> void visitCtFieldRead(CtFieldRead<T> fieldRead) {
         String fieldName = fieldRead.getVariable().getSimpleName();
-        if (context.hasVariable(fieldName)) {
-            RefinedVariable rv = context.getVariableByName(fieldName);
-            if (rv instanceof Variable && ((Variable) rv).getLocation().isPresent()
-                    && ((Variable) rv).getLocation().get().equals(fieldRead.getTarget().toString())) {
-                fieldRead.putMetadata(Keys.REFINEMENT, context.getVariableRefinements(fieldName));
-            } else {
-                fieldRead.putMetadata(Keys.REFINEMENT,
-                        Predicate.createEquals(Predicate.createVar(Keys.WILDCARD), Predicate.createVar(fieldName)));
-            }
-
-        } else if (context.hasVariable(Utils.qualifyFieldName(fieldRead.getVariable()))) {
+        // fields live in the context under their qualified name only: a variable with the field's simple name is an
+        // unrelated local, the tracked value is that of this object, not of another one
+        if (Utils.accessesTrackedField(fieldRead)
+                && 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

@@ -222,9 +222,10 @@ private Predicate getOperationRefinements(CtBinaryOperator<?> operator, CtVariab
                 elemName = Utils.qualifyFieldName(fieldRead.getVariable());
             Predicate elemRef = rtc.getContext().getVariableRefinements(elemName);
 
-            // Not a field of this class (e.g. an enum constant or a static constant): use the value given by the
-            // field read refinement (e.g. Format.JPG), or an unconstrained fresh value when there is none
-            if (elemRef == null && elemVar instanceof CtFieldRead)
+            // Not a field of this class or of this object (e.g. an enum constant, a static constant or other.f): use
+            // the value given by the field read refinement (e.g. Format.JPG), or an unconstrained fresh value
+            if (elemVar instanceof CtFieldRead<?> fieldRead
+                    && (elemRef == null || !Utils.accessesTrackedField(fieldRead)))
                 return valueFromRefinement(elemVar, rtc.getRefinement(elemVar));
 
             String returnName = elemName;
@@ -361,7 +362,9 @@ private Predicate getCurrentVariableValue(String name) {
      * Converts a operator assignment into an arithmetic predicate operand
      */
     private Predicate getOperatorAssignmentRefinement(CtExpression<?> element) throws LJError {
-        if (element instanceof CtVariableRead<?> variableRead) {
+        if (element instanceof CtFieldRead<?> fieldRead && !Utils.accessesTrackedField(fieldRead)) {
+            return valueFromRefinement(element, rtc.getRefinement(element)); // a field of another object
+        } else if (element instanceof CtVariableRead<?> variableRead) {
             String name = variableRead.getVariable().getSimpleName();
             if (variableRead instanceof CtFieldRead<?> fieldRead)
                 name = Utils.qualifyFieldName(fieldRead.getVariable());

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

@@ -9,9 +9,12 @@
 
 import liquidjava.utils.constants.Types;
 import spoon.reflect.code.CtBlock;
+import spoon.reflect.code.CtFieldAccess;
 import spoon.reflect.code.CtFor;
 import spoon.reflect.code.CtForEach;
 import spoon.reflect.code.CtIf;
+import spoon.reflect.code.CtSuperAccess;
+import spoon.reflect.code.CtThisAccess;
 import spoon.reflect.code.CtTry;
 import spoon.reflect.code.CtWhile;
 import spoon.reflect.cu.SourcePosition;
@@ -144,4 +147,14 @@ public static String getExpressionFromPosition(SourcePosition position) {
         }
         return null;
     }
+
+    /**
+     * Whether the context variable {@link #qualifyFieldName} names the field accessed here: a static field, or a field
+     * of the current object ({@code f}, {@code this.f}, {@code super.f}, {@code Outer.this.f}). A field of another
+     * object ({@code other.f}) has its own value, which is not tracked in the context.
+     */
+    public static boolean accessesTrackedField(CtFieldAccess<?> access) {
+        return access.getVariable().isStatic() || access.getTarget() == null
+                || access.getTarget() instanceof CtThisAccess<?> || access.getTarget() instanceof CtSuperAccess<?>;
+    }
 }