From 478eb94adcc59f4bc310acd6296fe8d1f9f10fec Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Tue, 13 Oct 2026 09:40:43 +0100 Subject: [PATCH 1/2] Resolve field reads by declaring type and target object (#321, #322) A field read first looked up the field's simple name in the context. Since #327 fields live there only under their qualified name, so that lookup could only find an unrelated local with the same name: Format.JPG was read as the local JPG (#321). That branch is removed. The context variable this#C.f tracks the value of the field of the current object, but reads of the same field on another object (other.val) used it too, so facts about this.val leaked into other.val (#322). Utils gains accessesTrackedField, true for static fields and for this/super/Outer.this targets; field reads on any other target use the field's declared refinement instead, in visitCtFieldRead and in the operand and compound assignment paths of OperationsChecker. Limits.max vs this.max (the first #322 reproducer) was already fixed by the qualified names of #327 and gets a regression test. Fixes #321 Fixes #322 Co-Authored-By: Claude Opus 5.5 --- .../testSuite/CorrectFieldReadResolution.java | 65 +++++++++++++++++++ .../testSuite/ErrorFieldOfOtherClass.java | 17 +++++ .../testSuite/ErrorFieldOfOtherObject.java | 41 ++++++++++++ .../testSuite/ErrorLocalShadowsConstant.java | 26 ++++++++ .../RefinementTypeChecker.java | 15 ++--- .../general_checkers/OperationsChecker.java | 11 ++-- .../src/main/java/liquidjava/utils/Utils.java | 13 ++++ 7 files changed, 173 insertions(+), 15 deletions(-) create mode 100644 liquidjava-example/src/main/java/testSuite/CorrectFieldReadResolution.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorFieldOfOtherClass.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorFieldOfOtherObject.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorLocalShadowsConstant.java diff --git a/liquidjava-example/src/main/java/testSuite/CorrectFieldReadResolution.java b/liquidjava-example/src/main/java/testSuite/CorrectFieldReadResolution.java new file mode 100644 index 00000000..cdda210f --- /dev/null +++ b/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; + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorFieldOfOtherClass.java b/liquidjava-example/src/main/java/testSuite/ErrorFieldOfOtherClass.java new file mode 100644 index 00000000..0ea7a91c --- /dev/null +++ b/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; + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorFieldOfOtherObject.java b/liquidjava-example/src/main/java/testSuite/ErrorFieldOfOtherObject.java new file mode 100644 index 00000000..409f86fa --- /dev/null +++ b/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 + } + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorLocalShadowsConstant.java b/liquidjava-example/src/main/java/testSuite/ErrorLocalShadowsConstant.java new file mode 100644 index 00000000..d03045c2 --- /dev/null +++ b/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 + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java index 995c5927..c6e3d3d2 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java @@ -316,17 +316,10 @@ public void visitCtField(CtField f) { @Override public void visitCtFieldRead(CtFieldRead 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 (#321), and the tracked value is that of this object, not of another one (#322) + 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))); diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java index 8e387712..a20b2a9b 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java +++ b/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()); diff --git a/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java b/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java index 018287e4..79083915 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java +++ b/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; + } } From b67ff37b6796f98b1fd19e35edad43f5832983c9 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Wed, 14 Oct 2026 10:50:14 +0100 Subject: [PATCH 2/2] Drop issue numbers from code comments Co-Authored-By: Claude Opus 5.5 --- .../processor/refinement_checker/RefinementTypeChecker.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java index c6e3d3d2..ce82359c 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java @@ -317,7 +317,7 @@ public void visitCtField(CtField f) { public void visitCtFieldRead(CtFieldRead fieldRead) { String fieldName = fieldRead.getVariable().getSimpleName(); // fields live in the context under their qualified name only: a variable with the field's simple name is an - // unrelated local (#321), and the tracked value is that of this object, not of another one (#322) + // 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());