Introduce optimistic default - #1386
aosen-xiong wants to merge 24 commits into
Conversation
wmdietl
left a comment
There was a problem hiding this comment.
@aosen-xiong @thisisalexandercook We had discussed this PR in the past. Let's go through this and related PRs next week and decide which direction to go.
The branch was 310 commits behind, and master reworked the code it changes. Carry the optimistic defaults forward onto master's design: - eisop#1331 removed QualifierDefaults.isElementAnnotatedForThisChecker. The new applyOptimisticDefaults calls BaseTypeChecker.isElementAnnotatedForThisCheckerOrUpstreamChecker instead, as applyConservativeDefaults now does, and shares its cache. - applyDefaultsElement now applies a memoized, precedence-ordered default list from fusedDefaultsFor rather than looping per call. Its boolean parameter becomes a three-valued DefaultsMode, with a third empty-scope slot and a third identity cache; invalidateFusedDefaults clears all six. - applyOptimisticDefaults mirrors applyConservativeDefaults, including the fast path on the two flags and the isParsingAnnotationFile guard. Without the guard it reaches the checker before the visitor is installed and throws a NullPointerException; without the fast path it costs a stub-file and bytecode test on every defaulted type. - master's bytecode test is atypeFactory.isFromByteCode, not the three-part isElementFromByteCode/declarationFromElement/isFromStubFile check. Keep the existing method names. Renaming addUncheckedCodeDefault and addUncheckedStandardDefaults would break downstream checkers, and was why this branch disabled the JSpecify reference checker in CI; the optimistic variants are added beside them instead, and that CI script is restored. Fix the bytecode branch of applyOptimisticDefaults, which tested the source flag. Regenerate the four expected outputs in checker/jtreg/nullness/onlyannotatedfor: the added @compile directive shifts every line number by one. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…icting flags Optimistic defaults put bottom qualifiers where the conservative ones put top. A qualifier can restrict where it may be written with @TargetLocations -- @KeyForBottom and @FBCBottom are not permitted on a RETURN or FIELD -- and defaulting one there made BaseTypeValidator report type.invalid.annotations.on.location on code the user never wrote. Five of the nine expected errors in AnnotatedForWithUseOptimisticDefault.out were that noise. Skip a qualifier/location pair the qualifier prohibits; the hierarchy's other defaults still apply there. The expected output drops to three errors, which match what the test's own comments say case 4 should produce. Defaulting a kind of code both optimistically and conservatively is always a mistake, and previously the conservative defaults silently won. Reject it in SourceChecker.initChecker, where the other option validation lives. An assert would not do: assertions are disabled in a normal javac run. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
There was a problem hiding this comment.
🔵 Needs a closer look
It changes core defaulting semantics and option parsing in the framework, which warrants final human review despite only minor review comments.
Pull request overview
Introduces an “optimistic” unchecked-code defaulting mode in the Checker Framework, enabling users to treat unannotated source/bytecode as more permissive (reducing false positives) while still emitting warnings, controlled via a new -AuseOptimisticDefaultsForUncheckedCode option.
Changes:
- Extend
QualifierDefaultsto maintain and apply separate conservative vs. optimistic unchecked default sets (with caching and mode selection). - Add
SourceCheckeroption parsing/validation for-AuseOptimisticDefaultsForUncheckedCodeand reject conflicting conservative+optimistic settings per kind (source/bytecode). - Document the new option and add jtreg tests covering bytecode defaults, bounds, and option-validation behavior.
File summaries
| File | Description |
|---|---|
| framework/src/test/java/org/checkerframework/framework/testchecker/nontopdefault/StubBoundAnnotatedTypeFactory.java | Updates test checker to use the renamed conservative unchecked-default registration API. |
| framework/src/main/java/org/checkerframework/framework/util/defaults/QualifierDefaults.java | Core implementation: adds optimistic unchecked defaults, mode selection, cache updates, and location-permission filtering. |
| framework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.java | Updates documentation to reflect that both conservative and optimistic unchecked defaults are added. |
| framework/src/main/java/org/checkerframework/framework/source/SourceChecker.java | Adds the new option, parsing/validation, and conflict detection with conservative defaults. |
| docs/manual/warnings.tex | Documents combining -AonlyAnnotatedFor with optimistic defaults. |
| docs/manual/introduction.tex | Adds user-facing documentation for -AuseOptimisticDefaultsForUncheckedCode. |
| docs/manual/annotating-libraries.tex | Documents optimistic defaults as an (unsound) alternative for libraries. |
| docs/manual/advanced-features.tex | Explains optimistic bytecode default behavior and its unsoundness. |
| docs/CHANGELOG.md | Records the new command-line option and its semantics. |
| checker/tests/nulless-conservative-defaults/annotatedfornullness/FieldWriteUnsound.java | Updates reference to renamed conservative defaults constant. |
| checker/jtreg/nullness/optimisticdefaultslib/Lib.java | New jtreg library used to exercise unchecked bytecode behavior. |
| checker/jtreg/nullness/optimisticdefaults/OptimisticDefaults.java | New jtreg test for optimistic defaults, bounds, and option validation. |
| checker/jtreg/nullness/optimisticdefaults/NoDefaults.out | Expected diagnostics baseline without optimistic defaults. |
| checker/jtreg/nullness/optimisticdefaults/InvalidOptimisticOption.out | Expected diagnostics for invalid optimistic option values. |
| checker/jtreg/nullness/optimisticdefaults/ConservativeDefaults.out | Expected diagnostics demonstrating conservative-default behavior differences. |
| checker/jtreg/nullness/optimisticdefaults/ConflictingOptimisticOption.out | Expected diagnostics for contradictory optimistic option values. |
| checker/jtreg/nullness/optimisticdefaults/ConflictingDefaultModes.out | Expected diagnostics for optimistic+conservative mode conflicts. |
| checker/jtreg/nullness/onlyannotatedfor/OptimisticDefaultOptions.java | New jtreg test driver for interactions with -AonlyAnnotatedFor and conservative bytecode defaults. |
| checker/jtreg/nullness/onlyannotatedfor/AnnotatedForWithUseOptimisticDefaultOnlyAnnotatedFor.out | Expected diagnostics for optimistic defaults + -AonlyAnnotatedFor. |
| checker/jtreg/nullness/onlyannotatedfor/AnnotatedForWithUseOptimisticDefault.out | Expected diagnostics for optimistic defaults without suppression. |
| checker/jtreg/nullness/onlyannotatedfor/AnnotatedForWithUseOnlyAnnotatedFor.out | Adjusted expected diagnostics line numbers due to test changes. |
| checker/jtreg/nullness/onlyannotatedfor/AnnotatedForWithUseNoFlag.out | Adjusted expected diagnostics line numbers due to test changes. |
| checker/jtreg/nullness/onlyannotatedfor/AnnotatedForWithUseConservativeDefault.out | Adjusted expected diagnostics line numbers due to test changes. |
| checker/jtreg/nullness/onlyannotatedfor/AnnotatedForWithUse.java | Adds optimistic-default compilation scenario and updates in-file expectations/comments accordingly. |
Review details
- Files reviewed: 24/24 changed files
- Comments generated: 2
- Review effort level: Lite
💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.
| @@ -263,8 +323,12 @@ public String toString() { | |||
| StringsPlume.joinLines(checkedCodeDefaults), | |||
| "Unchecked code defaults: ", | |||
Resolve the `docs/CHANGELOG.md` conflict by keeping both the optimistic default entry and master's new user-visible entries. Master added a fifth `@compile` directive to `checker/jtreg/nullness/onlyannotatedfor/AnnotatedForWithUse.java` while this branch added one of its own, so every line of that test shifted by one relative to both sides' reference files. Renumber all six `AnnotatedForWithUse*.out` files accordingly. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
`useOptimisticDefaultsForUncheckedCode` was listed before `useConservativeDefaultsForUncheckedCode` in `@SupportedOptions`, but its comment describes it in terms of the conservative option, so the reader met the reference before the thing it refers to. Move the option, and the `useOptimisticDefault` and `checkOptimisticAndConservativeDefaults` methods, after their conservative counterparts. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…aults `toString` labeled `uncheckedCodeDefaults` as "Unchecked code defaults" while printing a separate "Optimistic unchecked code defaults" set right below it, so a debugging dump did not say which of the two sets it was showing. Label it "Conservative unchecked code defaults". Also state the forms the option actually takes in the Javadoc of `addOptimisticUncheckedStandardDefaults`: it requires a value, so naming it bare suggested a spelling that `SourceChecker` rejects. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Splitting the unchecked-code defaults into a conservative and an optimistic set renamed public members that downstream checkers call: `STANDARD_UNCHECKED_DEFAULTS_TOP`/`_BOTTOM` and `addUncheckedCodeDefault`/`addUncheckedCodeDefaults`. Record them, and the new optimistic counterparts, under "Implementation details". Add eisop#1359, which this option closes, to the release's closed issues. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
DefaultsMode named both which unchecked default set to fold in and the absence of one, so every method taking a mode had to reject CHECKED: four copies of the same BugInCF guard, plus a `case CHECKED` in defaultsFor that no caller could reach. Model the axis as the two unchecked modes alone and pass null for checked code. That removes the four guards and the dead branch, collapses the three-case dispatch in addStandardDefaultsAtLocations to one addUncheckedCodeDefault call, and lets buildFusedDefaults call defaultsFor instead of repeating its mapping as a nested ternary -- the two spellings disagreed on what CHECKED meant. Both switches in fusedDefaultsFor now throw on an unhandled mode rather than falling back to the checked-code cache, which would have returned another mode's memoized defaults. Also rename uncheckedCodeDefaults to conservativeUncheckedCodeDefaults, to match optimisticUncheckedCodeDefaults and the toString label. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
The manual introduced the optimistic defaults without saying what defaulting a field to bottom does to writes: `u.field = x` is rejected unless x is itself bottom. That is the mirror of the conservative field default, which accepts every write and reports every read. Say so next to the option, and point at the existing TODO that a real fix needs separate defaulting for field reads and writes. Also lowercase "optimistic" mid-sentence. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Fixes #1359.
Adds
-AuseOptimisticDefaultsForUncheckedCode, which takessourceand/orbytecodelike-AuseConservativeDefaultsForUncheckedCodeand, like it, applies only outside the scope of an@AnnotatedFor. It defaults method parameters and upper bounds to top, and method returns, fields,and lower bounds to bottom, so a classfile's
String concatenate(String p1, String p2)is read as@Bottom String concatenate(@Top String p1, @Top String p2).