Add the @SideEffectsOnly annotation - #7952
Draft
mernst wants to merge 5 commits into
Draft
Conversation
Declare @SideEffectsOnly in checker-qual and register it as an inherited annotation, so that it can be released and the annotated JDK can use it. No checker consumes it yet. The Lock Checker deliberately ignores it: the annotation constrains which expressions a method modifies, but promises nothing about locks.
Contributor
📝 WalkthroughWalkthroughThis change adds the runtime-retained Possibly related PRs
Suggested reviewers: 🚥 Pre-merge checks | ✅ 3✅ Passed checks (3 passed)
✨ Finishing Touches🧪 Generate unit tests (beta)
Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out. Comment |
…artial into side-effects-only-2-5
mernst
marked this pull request as draft
August 9, 2026 23:59
![coderabbitai[bot]](https://avatars.githubusercontent.com/in/347564?s=60&v=4){kind=small}
Contributor
There was a problem hiding this comment.
Actionable comments posted: 4
🤖 Prompt for all review comments with AI agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
Inline comments:
In `@checker/tests/lock/SideEffectsOnlyLock.java`:
- Around line 13-20: Add framework-level test coverage for inherited
`@SideEffectsOnly` by declaring the annotation on a superclass or interface method
and overriding that method in a subclass or implementation. Verify the Lock
Checker recognizes the inherited annotation, targeting the registration logic in
AnnotatedTypeFactory rather than adding another direct-annotation-only case.
In `@docs/manual/advanced-features.tex`:
- Around line 1130-1133: Update the `@SideEffectsOnly` example near computeValue()
so someOtherVariable1 and someOtherVariable2 resolve to stable, modifiable Java
expressions by declaring them in the example or reusing names already declared
there. Keep the annotation and method intent unchanged, and ensure the snippet
is valid as written.
In `@docs/manual/called-methods-checker.tex`:
- Around line 222-234: Update the Called Methods Checker documentation around
the annotation alternatives to clarify that `@SideEffectsOnly` may write to
expressions listed in its value, so it preserves the Called Methods fact only
when those expressions exclude the tracked expression; revise the warning and
corresponding fix guidance without treating every `@SideEffectsOnly` method as
side-effect-free.
In `@docs/manual/purity-checker.tex`:
- Around line 30-32: Update the override-related documentation in
purity-checker.tex to reflect that SideEffectsOnly is inherited: remove
statements requiring overriding methods to repeat purity annotations and any
claim that annotation inheritance is future work. Keep the surrounding purity
semantics unchanged.
🪄 Autofix
Fix all unresolved CodeRabbit comments on this PR:
- Push a commit to this branch (recommended)
- Create a new PR with the fixes
ℹ️ Review info
⚙️ Run configuration
Configuration used: Path: .coderabbit.yaml
Review profile: ASSERTIVE
Plan: Pro Plus
Run ID: 9b553dac-3b46-414b-9888-0cd0fd5f9adb
📒 Files selected for processing (11)
checker-qual/src/main/java/org/checkerframework/dataflow/qual/SideEffectsOnly.javachecker/src/main/java/org/checkerframework/checker/lock/LockAnnotatedTypeFactory.javachecker/tests/lock/SideEffectsOnlyLock.javadocs/CHANGELOG.mddocs/manual/advanced-features.texdocs/manual/called-methods-checker.texdocs/manual/introduction.texdocs/manual/nullness-checker.texdocs/manual/purity-checker.texdocs/manual/troubleshooting.texframework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java
Comment on lines
+13
to
+20
| @SideEffectsOnly("this") | ||
| void callsUnannotatedMethod() { | ||
| unannotated(); | ||
| } | ||
|
|
||
| @SideEffectsOnly("this") | ||
| synchronized void synchronizedMethod() { | ||
| field = null; |
Contributor
There was a problem hiding this comment.
📐 Maintainability & Code Quality | 🔵 Trivial | ⚡ Quick win
Add coverage for inherited @SideEffectsOnly.
This test covers direct annotations only. Because the Lock Checker intentionally ignores @SideEffectsOnly, it cannot detect a regression in the registration at framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java Lines [808]-[815]. Add a framework-level test with a superclass or interface declaration and an overriding method.
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@checker/tests/lock/SideEffectsOnlyLock.java` around lines 13 - 20, Add
framework-level test coverage for inherited `@SideEffectsOnly` by declaring the
annotation on a superclass or interface method and overriding that method in a
subclass or implementation. Verify the Lock Checker recognizes the inherited
annotation, targeting the registration logic in AnnotatedTypeFactory rather than
adding another direct-annotation-only case.
Comment on lines
+1130
to
+1133
| \begin{Verbatim} | ||
| @SideEffectsOnly({"someOtherVariable1", "someOtherVariable2"}) | ||
| int computeValue() { ... } | ||
| \end{Verbatim} |
Contributor
There was a problem hiding this comment.
🎯 Functional Correctness | 🟡 Minor | ⚡ Quick win
🧩 Analysis chain
🏁 Script executed:
#!/bin/bash
set -euo pipefail
# Locate and inspect the referenced manual sections around `@SideEffectsOnly`.
file="docs/manual/advanced-features.tex"
if [ -f "$file" ]; then
wc -l "$file"
sed -n '1020,1155p' "$file" | cat -n
else
echo "missing $file"
fd -i 'advanced-features.tex|advanced-features.md|side-effects' .
fi
# Search for `@SideEffectsOnly` usage and declarations in docs/code.
printf '\n--- SideEffectsOnly occurrences ---\n'
rg -n "`@SideEffectsOnly`|SideEffectsOnly" -S .Repository: typetools/checker-framework
Length of output: 10448
🏁 Script executed:
#!/bin/bash
set -euo pipefail
# Inspect the annotation contract and implementations/processing relevant to `@SideEffectsOnly`.
printf '%s\n' '--- annot qual ---'
sed -n '1,120p' checker-qual/src/main/java/org/checkerframework/dataflow/qual/SideEffectsOnly.java | cat -n
printf '%s\n' '--- relevant implementation references ---'
rg -n "SideEffectsOnly|side effect|sideEffect|SideEffectsOnly.value|findAnnotatedElement|ExpressionTree" \
checker-qual/src/main/java/jakarta/platform/framework \
framework/src/main/java \
checker/src/main/java/org/checkerframework/checker/nullness \
-S | head -n 220
printf '%s\n' '--- manual side-effects-only sections ---'
sed -n '1,130p' docs/manual/purity-checker.tex | cat -n
sed -n '1560,1595p' docs/manual/introduction.tex | cat -nRepository: typetools/checker-framework
Length of output: 38773
Make the @SideEffectsOnly example valid as written.
The listed expressions must denote stable Java expressions that the method can modify. someOtherVariable1 and someOtherVariable2 are unresolved in this context, so the example should declare these fields/parameters or use previously declared names.
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@docs/manual/advanced-features.tex` around lines 1130 - 1133, Update the
`@SideEffectsOnly` example near computeValue() so someOtherVariable1 and
someOtherVariable2 resolve to stable, modifiable Java expressions by declaring
them in the example or reusing names already declared there. Keep the annotation
and method intent unchanged, and ensure the snippet is valid as written.
Comment on lines
+222
to
+234
| \refqualclass{dataflow/qual}{SideEffectFree}, | ||
| \refqualclass{dataflow/qual}{SideEffectsOnly}, or | ||
| \refqualclass{dataflow/qual}{Pure}), | ||
| then the Called Methods Checker issues an error because | ||
| it cannot make any assumptions about the call to \<m()>, and therefore assumes | ||
| the worst: that all information it knows about in-scope variables (including | ||
| that \<close()> was called on \<sock>) is stale and must be discarded. | ||
| There are two possible fixes: | ||
|
|
||
| \begin{itemize} | ||
| \item add a \<@SideEffectFree> or \<@Pure> annotation to \<m()>, if \<m()> is | ||
| \item add a \refqualclass{dataflow/qual}{SideEffectFree}, | ||
| \refqualclass{dataflow/qual}{SideEffectsOnly}, or | ||
| \refqualclass{dataflow/qual}{Pure} annotation to \<m()>, if \<m()> is |
Contributor
There was a problem hiding this comment.
🗄️ Data Integrity & Integration | 🟠 Major | ⚡ Quick win
🧩 Analysis chain
🏁 Script executed:
#!/bin/bash
set -euo pipefail
echo "== files =="
git ls-files | rg 'called-methods|Called Methods|side effects|SideEffectsOnly|SideEffectFree|Pure' || true
echo
echo "== target file section =="
if [ -f docs/manual/called-methods-checker.tex ]; then
nl -ba docs/manual/called-methods-checker.tex | sed -n '200,255p'
fi
echo
echo "== references to SideEffectsOnly in target if present =="
rg -n "SideEffectsOnly|SideEffectFree|Pure|value list|specified expressions|listed" docs/manual/called-methods-checker.tex || true
echo
echo "== all SideEffectsOnly mentions in repo =="
rg -n "`@SideEffectsOnly`|SideEffectsOnly|SideEffectFree|Pure" . --glob '!build/**' --glob '!dist/**' | head -200Repository: typetools/checker-framework
Length of output: 1031
🏁 Script executed:
#!/bin/bash
set -euo pipefail
echo "== target file outline/section =="
python3 - <<'PY'
from pathlib import Path
p = Path('docs/manual/called-methods-checker.tex')
lines = p.read_text().splitlines()
for i in range(199, 260):
print(f"{i+1:5d}: {lines[i]}")
PY
echo
echo "== relevant SideEffectsOnly annotation source =="
python3 - <<'PY'
from pathlib import Path
for name in ['checker-qual/src/main/java/org/checkerframework/dataflow/qual/SideEffectsOnly.java',
'checker-qual/src/main/java/org/checkerframework/dataflow/qual/SideEffectFree.java',
'checker-qual/src/main/java/org/checkerframework/dataflow/qual/Pure.java']:
p = Path(name)
print(f"\n--- {name} ---")
for i, line in enumerate(p.read_text().splitlines(), 1):
if i <= 220:
print(f"{i:4d}: {line}")
echo "== all SideEffectsOnly references in docs (avoid nl/egrep if unavailable) =="
python3 - <<'PY'
from pathlib import Path
import subprocess
res = subprocess.run(['rg', '-n', 'SideEffectsOnly|SideEffectFree|Pure|specified expressions|listed expressions|expression'], 'docs/manual', text=True, capture_output=True)
print(res.stdout)
PYRepository: typetools/checker-framework
Length of output: 3646
🏁 Script executed:
#!/bin/bash
set -euo pipefail
python3 - <<'PY'
from pathlib import Path
for name in ['checker-qual/src/main/java/org/checkerframework/dataflow/qual/SideEffectsOnly.java',
'checker-qual/src/main/java/org/checkerframework/dataflow/qual/SideEffectFree.java',
'checker-qual/src/main/java/org/checkerframework/dataflow/qual/Pure.java']:
p = Path(name)
print(f"\n--- {name} ---")
for i, line in enumerate(p.read_text().splitlines(), 1):
if i <= 260:
print(f"{i:4d}: {line}")
PY
python3 - <<'PY'
import subprocess
res = subprocess.run(['rg', '-n', 'SideEffectsOnly|SideEffectFree|Pure|specified expressions|listed expressions|expression'].append('docs/manual'), text=True, capture_output=True)
print(res.stdout)
PY
echo
echo "== SideEffectsOnly tests/docs =="
rg -n "SideEffectsOnly|`@SideEffectsOnly`" checker checker-qual tests docs/framework-checker.tex | head -200 || trueRepository: typetools/checker-framework
Length of output: 8661
🏁 Script executed:
#!/bin/bash
set -euo pipefail
python3 - <<'PY'
import subprocess
res = subprocess.run(['rg', '-n', 'SideEffectsOnly|`@SideEffectsOnly`|specified expressions|listed expressions', 'checker', 'checker-qual', 'docs'], text=True, capture_output=True)
print(res.stdout)
PYRepository: typetools/checker-framework
Length of output: 4888
Do not treat every @SideEffectsOnly method as side-effect-free.
@SideEffectsOnly permits writes to the expressions in its value list. Update the warning and fix to say that @SideEffectsOnly preserves the Called Methods fact only when the listed expressions exclude the tracked expression.
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@docs/manual/called-methods-checker.tex` around lines 222 - 234, Update the
Called Methods Checker documentation around the annotation alternatives to
clarify that `@SideEffectsOnly` may write to expressions listed in its value, so
it preserves the Called Methods fact only when those expressions exclude the
tracked expression; revise the warning and corresponding fix guidance without
treating every `@SideEffectsOnly` method as side-effect-free.
Comment on lines
+30
to
+32
| \item[\refqualclass{dataflow/qual}{SideEffectsOnly}] | ||
| indicates that the method has limited externally-visible side effects. | ||
|
|
Contributor
There was a problem hiding this comment.
🎯 Functional Correctness | 🟡 Minor | ⚡ Quick win
Update the override documentation for inherited @SideEffectsOnly.
framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java registers SideEffectsOnly as an inherited annotation. However, docs/manual/purity-checker.tex Lines 70-72 and 112-113 still say overriding methods must repeat purity annotations and that inheritance is future work. Remove that contradiction before release.
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@docs/manual/purity-checker.tex` around lines 30 - 32, Update the
override-related documentation in purity-checker.tex to reflect that
SideEffectsOnly is inherited: remove statements requiring overriding methods to
repeat purity annotations and any claim that annotation inheritance is future
work. Keep the surrounding purity semantics unchanged.
This was referenced Aug 10, 2026
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
1 participant
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.
Declare @SideEffectsOnly in checker-qual and register it as an inherited annotation, so that it can be released and the annotated JDK can use it. No checker consumes it yet.
The Lock Checker deliberately ignores it: the annotation constrains which expressions a method modifies, but promises nothing about locks.