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..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 @@ -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, 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))); 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; + } }