Skip to content

Introduce optimistic default - #1386

Open
aosen-xiong wants to merge 24 commits into
eisop:masterfrom
aosen-xiong:optimistic-default
Open

aosen-xiong wants to merge 24 commits into
eisop:masterfrom
aosen-xiong:optimistic-default

Conversation

@aosen-xiong

@aosen-xiong aosen-xiong commented Sep 4, 2025

Copy link
Copy Markdown
Collaborator

Fixes #1359.

Adds -AuseOptimisticDefaultsForUncheckedCode, which takes source and/or bytecode like
-AuseConservativeDefaultsForUncheckedCode and, 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).

@wmdietl wmdietl left a comment

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@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.

Comment thread framework/src/main/java/org/checkerframework/framework/source/SourceChecker.java Outdated
Comment thread docs/CHANGELOG.md Outdated
@wmdietl wmdietl assigned aosen-xiong and unassigned wmdietl Mar 22, 2026
@aosen-xiong aosen-xiong removed their assignment May 25, 2026
@aosen-xiong
aosen-xiong marked this pull request as draft August 1, 2026 08:30
aosen-xiong and others added 5 commits August 29, 2026 22:45
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>

Copilot AI left a comment

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

🔵 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 QualifierDefaults to maintain and apply separate conservative vs. optimistic unchecked default sets (with caching and mode selection).
  • Add SourceChecker option parsing/validation for -AuseOptimisticDefaultsForUncheckedCode and 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: ",
aosen-xiong and others added 6 commits September 11, 2026 23:54
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>
@aosen-xiong
aosen-xiong marked this pull request as ready for review September 12, 2026 04:27
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Introduce optimistic default

3 participants