Keep the meaning of enum and static constants compared in conditions

[CatarinaGamboa]

What was wrong

Comparing an enum constant or a static constant of another class directly in an if (if (format == Format.JPG)) crashed the verifier with an NPE (elemRef is null). OperationsChecker.getOperationRefinements always looks a field read up as this#X; such constants are not in context under that name, and inside an if there was no fallback.

What changed

• OperationsChecker.getOperationRefinements: when the this#X lookup finds nothing for a field read, use the value from the field read's own refinement via the existing valueFromRefinement helper: an enum declared in the sources becomes Format.JPG, a static final literal becomes its value, and anything else becomes an unconstrained fresh value (sound, but carries no information).
• RefinementTypeChecker.visitCtFieldRead: getDeclaringType().isEnum() is now getDeclaringType().getDeclaration() instanceof CtEnum, so only enums declared in the analysed sources are translated to SMT. A JDK enum constant (DayOfWeek.MONDAY) used to give a false "Variable 'DayOfWeek.MONDAY' could not be found" error (e.g. boolean b = d == DayOfWeek.MONDAY;); now it carries no information.

Tests

testSuite/CorrectEnumConstantInCondition.java and testSuite/ErrorEnumConstantInCondition.java, one violation per method in the error file. Both crash with the NPE on main.

• Positive: then- and else-branches, !=, constant on the left, && and ||, else-if chains (the final else is known to be GIF), a user static final (alone and in arithmetic), a JDK static final, a JDK enum, and a non-final static field.
• Negative: wrong then-branch, else-branch, !=, ||, else-if chain, null || constant, two different constants (Format.JPG == Format.PNG, so the else-branch is checked), a wrong static final value, arithmetic, and the else-branch of a JDK enum comparison (still checked).

mvn test: 345/345 on main, 347/347 on this branch.

Review

An adversarial review ran 40 small programs on main and on this branch:

• No program that main accepted is now rejected, and no new crashes. Of the 9 programs that crashed on main, 8 (enum constants in if, else-if chains, constant on both sides, enum from another package, a field compared to a constant, JDK enum) now verify or report the expected error. The ninth is the local-name clash described under follow-ups. One false error on main is gone (JDK enum in a boolean local).
• Held up: non-final static fields are not treated as known constants. Arithmetic (n + Limits.max > 15), ternaries, !, &&/||, return, boolean locals, a parameter named like the constant, and a static (final or not) field of the current class all behave the same as other comparisons.
• The discriminator (elemRef == null && elemVar instanceof CtFieldRead) only changes field reads that used to crash in an if. Outside an if, the old path created an instance of this#X from the same refinement, so the result is equivalent. The only difference is that it no longer adds a stray this#X to the context. Keying on static-ness instead would not fix the name-clash problems below, because they come from visitCtFieldRead.
• Added: the test shapes listed above (else-if, arithmetic, null ||, two constants).

Known limitations / follow-ups (pre-existing on main, not changed here)

• A field read can resolve to a local with the same name (visitCtFieldRead, first branch: _ == fieldName when the location does not match). With Format JPG = Format.PNG; as a local, Format.JPG means the local, and onlyPng(Format.JPG)-style violations are accepted. On main this already happens outside an if (Format g = Format.JPG; onlyPng(g); is accepted). Inside an if, main crashed and this branch accepts. Candidate fix: only use the context variable when its location matches the target, and otherwise fall through. That removes 5 lines, keeps all 347 tests green, and fixes the 3 cases. It is left out because it changes field reads in general, not just in conditions.
• Name clash with a field of the current class: any field read X.f resolves to this#f when the current class has a field f (both in visitCtFieldRead and in the this#X lookup here). So Format.JPG is read as this.JPG when the class has a field named JPG, other.val is read as this.val, and a field shadowed by a nested Limits.max loses its refinement. All of these are accepted unsoundly, on main as well.
• Field initial values are assumed in every method (int mode = 0; with void set() { mode = 3; }, then if (n == mode) proves n == 0). This holds for instance fields and non-final statics.
• static final int X = compute(); gives a false "Variable '#compute_1' could not be found" error.
• Uppercase static final int MAX: "Invalid ghost declaration" (static final field plus a refinement gives a spurious "Invalid ghost declaration" #307). Open PR Exclude Static Final Constants from Instance Field Ghosts #313 does not conflict with this branch (they touch different files). With both merged, if (n == Limits.MAX) verifies the correct case and reports the wrong one. The tests use a lowercase max until static final field plus a refinement gives a spurious "Invalid ghost declaration" #307 is fixed.

Fixes #302

🤖 Generated with Claude Code

[CatarinaGamboa]

Follow-ups from the review, filed as separate bugs: #321 (a local with a constant's name shadows the constant; with this PR that clash inside an if becomes an accepted violation instead of a crash) and #322 (a field of another class/object read as this class's field of the same name; pre-existing).

🤖 Generated with Claude Code