Exclude Static Final Constants from Instance Field Ghosts - #313
Merged
Merged
Conversation
CatarinaGamboa
added a commit
that referenced
this pull request
Oct 2, 2026
…319) ## 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" (#307). Open PR #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 #307 is fixed. Fixes #302 🤖 Generated with [Claude Code](https://claude.com/claude-code) --------- Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Closes #307. Excludes static final int constants from generated instance field ghosts, preventing incorrect “Invalid ghost declaration” errors.