JSpecify nullness annotations (WIP): follow-up of PR #3470 by wadoon · Pull Request #4003 · KeYProject/key

wadoon · 2026-10-24T17:33:53Z

Related Issue

This pull request resolves #3470 (continues the goal of PR #3470 "Nullness Type System for key.core" with a workflow that avoids its speed problem).

Intended Change

Apply JSpecify nullness annotations to the whole KeY codebase, module by module, following the dependency chain and module size; within each module, package by package.

Annotated code gets JSpecify @NullMarked scopes and precise @Nullable type-use annotations (correct placement for arrays, nested types, generic bounds) so that downstream consumers — Kotlin, IDEs, and nullness checkers — see a real API contract. Behavior does not change.

Status at a Glance

Milestone	State
JSpecify annotations — all modules	✅ done (waves 1–3)
NullAway fast trials (`-DENABLE_NULLAWAY`, opt-in)	✅ 16 committed waves
EISOP gate (`-DENABLE_NULLNESS=true`)	⛔ dropped — its CI compile hung 6h on GitHub Actions; NullAway is the operating gate (see §2)
CI Tests on pre-rebase head `39412df61f`	✅ green; re-validating on rebased head `9ac56c631d`

Plan

1 · JSpecify annotations — done

key.util, key.ncore, key.ncore.calculus, key.ncore.matcher
key.core (1573 files) — 10 package clusters (waves 1–3), compile + spotless green per wave
Level 1–3 modules: infflow, testgen, wd, example, slicing, exploration, ui, isabelletranslation, proofmanagement, caching, ui.testgen
Rebased on current main (76167728c6); head 9ac56c631d — all 67 commits linear (no merges), formatting clean (spotlessCheck green on all modules)
- Conflicts resolved with main's API priority (the Add support for type Annotations #3996 KeYJavaType → TypeReference change) and the branch's JSpecify annotations re-applied (@NullMarked/@Nullable, crash-equivalent guards). Rebase-marker contamination (NullAway waves 3/4/5/11) and latent resolution bugs were repaired inside their owning commits (no standalone spotless commits).
- Locally verified: spotlessCheck + compileJava (all modules) and testClasses (key.core, key.core.infflow, key.ui). Per user directive the EISOP gate is dropped — its CI compile hung 6h on GitHub Actions (see §Status); NullAway is the operating nullness gate and CI re-validation of the rebased head is in progress.
- CI-failure fixes (the first CI run exposed branch regressions predating the rebase — the key.core commits were never CI-tested): the .key loader crashed on legal schematic inputs because branch-added guards were not crash-equivalent to main's pass-through semantics — zero-arity calls (ExpressionBuilder, main maps a missing argument list to NO_SUBTERMS), schema declarations without concrete KeYJavaType (JP2KeYConverter.visitVariableSpecification/visitNoMap, resolved at taclet instantiation), bodyless schematic methods like $allocate (SLEnvInput, the AST walkers tolerate a null root), and \datatype taclets without parse-time builder (TacletPBuilder, main deliberately stores a null builder). All restored to main semantics with scoped, javadoc'd suppressions; null-message hardening on the error-reporting path (ExceptionTools). A second regression class was found the same way: several wave commits replaced main's position-preserving new Location(nullableFile, position) with Location.UNDEFINED whenever the source had no file URI (in-memory inputs), silently destroying error positions in BuildingIssue, SyntaxErrorReporter, PreParser, PositionedString, KeyAst, JavaSourceLocations, SVInstantiationExceptionWithPosition, TextualJMLConstruct, and SLTranslationException — all restored to main semantics (MultiSyntaxErrorTest, KeYParserExceptionTest, IssueDialogMessageTest green again). A third class: the testgen drive turned main's tolerated-null Z3 version logging into a hard NullPointerException in TGMain, failing all test-case generation whenever the solver version could not be parsed — restored to main's logging behavior (amended into the testgen drive 1038f066d2). Commit 4397a036c0 regenerates the 76 pipeline expected files ("Created by" line-number drift and pure line moves only).
- A second CI run surfaced a fourth and fifth regression class, all fixed inside the key.core drive 2a303cd83a (bisect-verified to that commit): (a) the drive's Objects.requireNonNull(uic) in FinishSymbolicExecutionUntilMergePointMacro.doPostProcessing crashed on the null UserInterfaceControl that macros legitimately receive in headless runs (e.g. tests); the surrounding empty catch swallowed the NPE, the post-processing steps silently stopped, and the resulting merge-partner program counters no longer matched — restored to main's pass-through with a scoped suppression (MergeRuleTests incl. testDoManualGcdProof, LoopScopeInvRuleTests green); (b) the drive hardened proof-replay/pruning sites where main deliberately tolerates nulls (ProgVarReplaceVisitor's null-tolerant term replacement — performActionOnLoopInvariant on a null free invariant, ProofPruner.prune's possibly-null rule-app pass-through, IntermediateProofReplayer's nullable parse-tree enqueue and null join-procedure lookup) — restored to main semantics with scoped suppressions (TestGoal, TestCopyingReplayer, MT-determinism suites, caching ProofCachingSingleRunTest/TestReferenceSearcher, and the full keyext.slicing module green).

2 · NullAway fast trials — done (opt-in `-DENABLE_NULLAWAY`)

Wiring committed (Error Prone 5.1.1 + NullAway 3.3.0, JSpecify mode, 121d45465c)
16 committed waves fixing their targeted cascade layer per wave (bba4686bc1 … 0b9c490ec9); each fix deepened the analysis and surfaced new downstream findings — key.core was never fully NullAway-clean (see the parked count below)
Wave 15 was a stop-and-fix CI wave: runtime-NPE regressions from over-eager requireNonNull in proof paths restored to main semantics via honest @Nullable widenings; verified locally (ScDeterminismTest 14/14, InfFlowProfileLoadingTest 3/3, IssueDialogMessageTest 2/2)
Count-correction e006949b24: earlier counts were truncated at javac's 100-error cap; an uncapped scan shows a long key.core tail (4,024 findings / 493 files) — parked; EISOP was the conformance gate until it was dropped (see §Status)
CI job wired as non-blocking (a9cf52f32e, continue-on-error): the gate run reports 3,358 findings on the head, 3,319 of which already exist on the pre-rebase tip; blocking gating waits for the fix campaign

3 · EISOP conformance (`-DENABLE_NULLNESS=true -Werror`) — modules done

Module	Main fix	Test sources
`keyext.ui.testgen`	`cac81640f9`	✅
`key.core.example`	`cd4351dabd`	✅
`key.core.wd`	`0211349ef0`	✅
`keyext.caching`	`9231ccf268`	✅
`keyext.exploration`	`7772d6eb32`	✅
`key.core.testgen`	`1038f066d2`	✅
`keyext.slicing`	`40caa77220`	✅
`keyext.proofmanagement`	`6f8d0a4c5b`	✅
`keyext.isabelletranslation`	`0796e759b3`	✅
`key.core.infflow`	`a1a9aff15f`	✅
`key.ui`	`8d890495e0` (+ test fixes `23a73e9bf6`, format `72709e382d`)	✅

4 · Final gates — ⬜

Drive key.core NullAway findings to zero (3,358 on head — 3,319 pre-date the rebase; see §2), then flip the CI nullaway job from continue-on-error to a blocking gate
CI Tests green on the merged head (re-running on 9ac56c631d)
CI CodeQuality green on the merged head (formatting; NullAway informational)
Code cleanup + PR documentation

Type of pull request

Refactoring (behaviour should not change or only minimally change)
There are changes to the (Java) code
There are changes to the deployment/CI infrastructure (gradle, github, ...)

Ensuring quality

I made sure that introduced/changed code is well documented (javadoc and inline comments).
I have tested the feature as follows: each annotated module stays green under compileJava and spotlessCheck; NullAway runs per module before that module is marked done (the EISOP gate is dropped — see §Status).
I have checked that runtime performance has not deteriorated (annotations are compile-time only).

Additional information and contact(s)

This PR is tracked in docs/plan-jspecify-nullness.md in this branch. Work is executed in parallel by package clusters; each cluster is committed and pushed as it lands.

The contributions within this pull request are licensed under GPLv2, or (at your option) any later version, for inclusion in KeY.

Previous (verbose) description — kept for the audit trail

Plan

@NullMarked

…e cluster 1) Class-level @NullMarked + @nullable where null is possible (232 uses). Verified by compile + spotlessCheck. Follow-up of PR #3470.

@NullMarked

…core cluster 2) 196 files @NullMarked; precise @nullable placements (132 uses). Verified by compile + spotlessCheck. Follow-up of PR #3470.

@NullMarked

… cluster 3) 253 files @NullMarked; @nullable on lazily-nullable fields/params/returns. Verified by compile + spotlessCheck. Follow-up of PR #3470.

@NullMarked

…/visitor) with JSpecify (key.core cluster 4) 72 files @NullMarked. Verified by compile + spotless. Follow-up of PR #3470.

@NullMarked

…e cluster 5) 174 files @NullMarked; io/ carries the bulk (problem loaders, replayers, parser state, FileRepo streams). Verified by compile + spotless. PR #3470.

@NullMarked

…core cluster 6) 196 files @NullMarked; option/cache/feature chains annotated end-to-end. Verified by compile + spotless. PR #3470.

@NullMarked

…core cluster 7) 99 files @NullMarked, 755 @nullable across the JML/NJML/spec translation chain. Verified by compile + spotless. PR #3470.

@NullMarked

…cluster 8) 100 files @NullMarked; lazy-initialized translator state and Map.get chains annotated. Verified by compile + spotless. PR #3470.

@NullMarked

…y (cluster 9) 117 files @NullMarked; scripts package-level @NullMarked from prior commit, @nullable gap-fills added. Verified by compile + spotless. PR #3470.

@NullMarked

…luster 10) 151 files @NullMarked in ldt/nparser/parser/prover/control/axiom_abstraction/ taclettranslation/settings. Verified by compile + spotless. PR #3470.

…se 2 trial setup Prepares the opt-in NullAway fast-trial for the annotated modules (-DENABLE_NULLAWAY), keeping EISOP as final conformance gate. PR #3470.

…ins (-DENABLE_NULLAWAY) NullAway 0.14.x is an Error Prone BugChecker, not a javac Plugin, so the earlier -Xplugin route cannot work. Add net.ltgt.errorprone 5.1.1 + net.ltgt.nullaway 3.3.0 Gradle plugins (error_prone_core 2.49.0, nullaway 0.14.3 on the errorprone configuration). Off by default; with -DENABLE_NULLAWAY the NullAway check is ERROR severity with JSpecify mode and annotated-package scope de.uka.ilkd.key,org.key_project. EISOP (NullnessChecker) stays the final conformance gate. First trial: 155 findings across key.util/ncore/ncore.calculus/key.core. PR #3470.

@SuppressWarnings

…, key.ncore.calculus (Phase 2 wave 1) 55 findings cleared: Objects.requireNonNull narrowing at deref sites, honest @nullable widenings (DefaultEdge fields, PLookup.get default, ArraySort), override/param and element-nullability alignments, and @SuppressWarnings ('NullAway') bridges where NullAway cannot express the EISOP-approved contract (Location record family, type-variable array components). EISOP (the module's conformance gate) is unaffected. PR #3470.

… hot spots (Phase 2 wave 1) 68 findings cleared in Proof, Goal, Services, NamespaceSet via Objects.requireNonNull narrowing at deref sites, honest @nullable alignments and localized suppressions (intentional setGoal(null) detach contract). PR #3470.

…(Phase 2 wave 1) 17 findings cleared (ProverCore, SingleRuleApplicationInfo, DefaultProver, FormulaTagManager, TacletExecutor, BelowBinderFeature, SortComparisonFeature, SubtermGenerator) via requireNonNull narrowing and one honest @nullable return. PR #3470.

…r 2 (Phase 2 wave 2) Cleared 101 second-order findings surfaced by the first wave's honest annotations: JavaInfo (49 + ExecutionContext runtimeInstance @nullable on IExecutionContext/ctor/field per ProgramSV precedent), SpecificationRepository (25), VariableNamer (15 incl. field-init defaults + override param alignment), TypeConverter residual (6), ConstantExpressionEvaluator (5), and made ProgramElementName's NameCreationInfo ctor params @nullable so null-name creation info is an honest contract. JDK-25 flexible-constructor syntax accidentally introduced was reverted to Java-21-legal super(...) calls. PR #3470.

…r 3 (Phase 2 wave 3) Cleared the 101 gate6 findings: TypeConverter (29, getPromotedType/getSort derefs narrowed — JavaInfo.getKeYJavaType(PrimitiveType) runtime non-null), SpecificationRepository (25, getToplevelPM wraps, updateVariables rebuilt via ProgramVariableCollection no-arg ctor + public-field assignment preserving legit-null selfVar/resultVar/excVar), TermBuilder (23, master-factory @nullable overload routing), TermLabelManager (15, honest @nullable applicationTerm chain + 7 TermLabelConfiguration fields), OriginTermLabel (6), AbstractBetaFeature (1), SVInstantiations (1), RenamingTermProperty (1). Next cascade layer surfaced (101 findings: TermBuilder 49, TacletApp 14, Node 9, NoPosTacletApp 7, TermLabelManager 6, NodeInfo 4, TermFactory 4, JavaService 3, SpecificationRepository 2, ClashFreeSubst/LDT/AbstractLDT 1 each). PR #3470.

…r 4 (Phase 2 wave 4) Cleared the 101 gate7 findings: TermBuilder (49, heapLDT/namespace/operator- lookup narrows, getOriginFactory honest @nullable), TacletApp (14) + NoPos TacletApp (7) + Node (9) + NodeInfo (4) via requireNonNull narrows, honest @nullable param widenings, eager ctor init, and 2 scoped suppressions for the deferred assumes-Instantiation widening, TermLabelManager interface boundary resolved honestly (TermLabelUpdate.updateLabels + TermLabelRefactoring params -> @nullable), TermFactory boundVars @nullable (clears ClashFreeSubst too), JavaService getConverter @nullable, LDT/AbstractLDT requireNonNull. Next cascade layer surfaced (101): TacletApp 35, OneStepSimplifier 25, Taclet 10, ProgramTransformer 6, ProgramVariable 6, LocationVariable 6, KeYJavaType 4, TacletIndex/Statistics 2, misc 5. PR #3470.

@nonnull

…r 5 (Phase 2 wave 5) Cleared the 101 gate8 findings: TacletApp (35)+Taclet (10, @EnsuresNonNull executor + TacletLabelHint optional fields @nullable), OneStepSimplifier (25 field-init + thread @nullable context/protocol/ruleApp) + RuleApp trio, TacletIndex/Statistics narrows, and the override-mismatch family: honest widening of 8 superclass methods over-annotated @nonnull in the campaign (ReferencePrefix.getReferencePrefix, Type.getDefaultValue, TypeReference .getReferencePrefix/getKeYJavaType, PackageReferenceContainer .getPackageReference, StatementContainer.getStatementAt, ExpressionContainer .getExpressionAt, Expression.getKeYJavaType) + PackageReference ctor/field/ getter @nullable. Next cascade layer (101): the java.ast AST subsystem — TypeConverter 15, ContextStatementBlock 13, TypeDeclaration 11, DLEmbeddedExpression 9, ArrayDeclaration 9, JavaDeclaration 6, + ~27 files with 1-4 findings. PR #3470.

@SuppressWarnings

…r 6, java.ast subsystem (Phase 2 wave 6) Cleared the 101 gate9 findings across the AST subsystem: TypeConverter 15 + DLEmbeddedExpression 9 (requireNonNull narrows), AST composites 40 (ContextStatementBlock incl. override-param contravariance alignment, TypeDeclaration/JavaDeclaration/StatementBlock/JavaNonTerminalProgramElement/ CompilationUnit/Throws/PackageSpecification; authorized ClassType 6-getter + ProgramPrefix.getInnerMostMethodFrame widenings), arrays+literals 24 (uniform getKeYJavaType(Services) @nullable widening across 13 literal classes, ArrayDeclaration, Literal, Operator), stragglers 13. Controller surgical fixes: TypeRef/TypeReferenceImp prefix chain and ExecutionContext/ IExecutionContext methodContext widened to @nullable; moved an illegal statement-level @SuppressWarnings in ContextStatementBlock to the method. Next cascade layer (101): java.ast statement subsystem — Try 12, MethodBodyStatement 9, EnhancedFor 9, LoopStatement 8, LabeledStatement 7, MethodDeclaration 7, + 17 files 1-4 each. PR #3470.

@NullMarked

Level-3 module 3/4: class-level @NullMarked on all 19 main sources, @nullable on lazy fields (CachingExtension toggleAction/cachingPruneHandler, ReferenceSearchDialog applyButton/closeDialog/scrollPane) and honest widenings (ReferenceSearcher findPreviousProof -> @nullable ClosedBy, ReferenceSearchButton.updateState proof param) - all call sites already null-guard. Annotations + imports only, zero behavior change. Pre-existing unguarded derefs of @nullable node.lookup/getOpenGoal/ getSelectedProof flagged for EISOP phase, deliberately not fixed.

@NullMarked

Level-3 module 2/4: class-level @NullMarked on all 26 main sources (12 files from the first agent pass + 15 completed/rewrapped in the resumed pass). Honest @nullable: KeYFacade findProofLine/loadProofFile/createProofObligationContainer/ replayProof envInput, CheckerData transient lifecycle fields + ProofEntry public fields + getProofEntryByContract, Node/PathNode parent chains (root = null), ProofBundleHandler bootclasspath/topLevelProjectFile (or null), DependencyGraph allSCCs/getNodeByName, DependencyChecker data, CheckConfigDialog checkWorker. Qualified types: IPersistablePO.@nullable LoadedPOContainer, IntermediatePresentationProofFileParser.@nullable Result. Annotations + imports only, zero behavior change. Pre-existing latent unguarded derefs (ProofEntry. settingsId, poContainer.getProofOblInput, DependencyGraphBuilder line.proof etc) documented for EISOP phase.

@NullMarked

Level-3 module 1/4 (last of Level 3): class-level @NullMarked on all 40 previously-unannotated sources (2 already marked). Honest @nullable: lazy INSTANCE, solver result/preamble/translation/exception lifecycle fields, computationTime/successfulTactic, progress-dialog lazy widgets, getSolver (orElse(null)), handlerSnippets param across interface + impls, fieldSort/ nullSort from Namespace.lookup, originalSelectedNode. java.time.@nullable Duration placement (scala Duration owns the simple name). Annotations + imports only, zero behavior change. Residual unguarded derefs (lazy-field reads, Map.get flows, key.ui @nullable getter chains) documented for EISOP phase.

…ample Phase-3 infra: checkerFramework block behind -DENABLE_NULLNESS=true with -AonlyDefs scoping to each module's packages, -Xmaxerrs 10000, -Werror (same shape as key.util/key.ncore/*). Exploratory baseline: key.core.example 0 findings; keyext.ui.testgen 42 (29 init-checker artifacts + 13 real nullable flows, all pre-existing latent).

@SuppressWarnings

…=true, -Werror) Phase-3 first module: 42 findings to zero. 29 initialization-checker artifacts (methods called on 'this' while receiver under initialization in Swing/extension ctors - safe, fields set before the calls) -> 6 scoped @SuppressWarnings("nullness:method.invocation.invalid") on the constructors (CounterExampleAction, TestGenerationAction, TGInfoDialog, TestgenOptionsPanel, TestgenExtension, TGWorker). 13 real nullable flows -> explicit crash-equivalent NPE guards (this EISOP fork treats Objects.requireNonNull's param as @nonnull, so the masking idiom is rejected; explicit if (x == null) throw new NullPointerException matches key.core house style): Z3_CE_SOLVER x2, TGWorker originalProof (ctor/start/done), getInitConfig/ getEnv/getServices/getProofOblInput, TestgenExtension Arrays.asList + JToolBar.add. Zero behavior change on happy paths.

…exploration Phase-3 infra behind -DENABLE_NULLNESS=true (onlyDefs per module, -Xmaxerrs 10000, -Werror). Baseline: key.core.wd 125 findings; caching/exploration baselines pending wd (key.ui dependency chain pulls wd's compile).

…true, -Werror) Phase-3 example module: Main.java:170 deref of @nullable Profile.getDefaultStrategyFactory() -> crash-equivalent explicit NPE guard (house style; requireNonNull rejected by this EISOP fork). Note: the earlier '0 findings' baseline for example was a false negative - gradle dropped the task after ui.testgen's failure, so it was never checked; caught by CI's full compileTestJava run.

@SuppressWarnings

… -Werror) Phase-3 wd module: 125 findings in 16 files to zero. Honest @nullable first: require/ensures/modifiable + accessible/mby/represents fields (null-tolerant setters), getVisibility/posInOcc override params widened to match key.core contracts, WellDefinednessPO.createSelf @nullable. Crash-equivalent explicit NPE guards for getHeapLDT/selfKJT/getSort/replace/combine/Maps.get chains (house style; requireNonNull rejected by this EISOP fork). Ctor super() arg handling via private requireX static helpers (Java non-virtual-expr workaround). map() propagates null for the genuinely-optional term fields (accessible/mby/represents/globalDefs/axiom) - previously op.apply(null) crashed; propagation mirrors the widened getters' true nullability. 3 scoped @SuppressWarnings("nullness:method.invocation.invalid") on ctors only (WdProfile:54 super.getStandardRules, BlockWellDefinedness:74, LoopWellDefinedness:72). compileJava + compileTestJava (4 test files, onlyDefs-scoped) both green.

@SuppressWarnings

…ue, -Werror) Phase-3 caching module: 69 findings in 15 main files + 37 in 2 test files (onlyDefs ^de\.uka\.ilkd\.key\.(gui|proof) covers the test package) to zero. Honest @nullable: lazy lifecycle fields (CachingExtension mediator, referenceSearchButton). Crash-equivalent explicit NPE guards for getSelectedProof/getOpenGoal/lookup/node-chain/results (house style; requireNonNull rejected by this EISOP fork). 6 scoped ctor-only @SuppressWarnings("nullness:method.invocation.invalid"). Two lifecycle-safe structural changes: ReferenceSearchButton listener registration moved to registerListeners() (called immediately after ctor, before use) and ReferenceSearchTable setModel/getColumnModel moved to init() (same); ProofCachingSettings field initializers moved into ctor body (order preserved); ReferenceSearcher stream->explicit-loop rewrite + CopyBeforeDispose single-lookup filter (both semantics-identical); type-arguments-not.inferred resolved via loop rewrite instead of unsolvable @nullable streaming constraints. Test files fixed with same guard discipline, zero suppressions.

@SuppressWarnings

…S=true, -Werror) Phase-3 exploration module: 76 main + 30 test findings to zero (onlyDefs ^org\.key_project\.exploration covers the test package). Honest @nullable: lazy leftPanel/changeSupport lifecycle state (memoized getter), renderer value params. Crash-equivalent guards for getEnv/lookup/rule-app/parent/ branch-label chains. 9 scoped ctor-only @SuppressWarnings ("nullness:method.invocation.invalid"). Deliberate fixes: ExplorationStepsModel null-root state via EMPTY_ROOT sentinel + setRootVisible toggling (JDK sig is @nonnull, runtime supports null; all in-module root consumers updated); ExplorationRenderer graceful-degradation on GC'd WeakReference-backed nodes (a Swing renderer must never throw; previously NPE'd the tree) + tooltip null guard. Test file guard-fixed per caching precedent, all 27 assertions kept, 3/3 tests pass.

…ng + isabelletranslation + proofmanagement Phase-3 mid-tier infra behind -DENABLE_NULLNESS=true (onlyDefs per module, -Xmaxerrs 10000, -Werror). testgen onlyDefs covers both main (testgen) and test (testcase) roots; slicing test root covered by its main root; the two keyext modules have no test sources. Baselines (onlyDefs fixed to single backslash escapes - the first draft doubled them, silently matching nothing): testgen 67, slicing 179, isabelletranslation 147, proofmanagement 99.

@polynull

…true, -Werror) Phase-3 mid-tier: 67 main findings to zero (plus 22 test findings under the testcase onlyDefs branch). Notable: an EISOP BugInCF crash (inconsistent sizes in visitNewArray/lub) was masking ~20 findings in TestCaseGenerator, root-caused to a double-annotated return type (@polynull + @nullable) feeding javapoet varargs -> getSafeType rewritten to a single @polynull annotation (return null legal, crash gone). Var->explicit-type fix in TestgenFacade (List.of element annotation inference). Honest @nullable widenings (TGReporter.writeln, getServices), ~40 crash-equivalent NPE guards (Map.get/ getHeapLDT/getKeYJavaType/Z3_CE_SOLVER/modelDir), 2 scoped ctor-only suppressions (TestCaseGenerator:122, OracleGenerator:80). Test sources: guard-then-assert conversions (assertNotNull has @nonnull param in this fork; NPE guard is crash-equivalent), ProgressMonitor.Empty for null-monitor (the API documents a nullable monitor), honest @nullable test fields.

…ue, -Werror) Phase-3 mid-tier: 179 main findings to zero (47 method.invocation.invalid, 42 deref, 51 arg, 18 assignment...) plus 62 test-source findings. 4 argument.type.incompatible suppressions are deliberate-null-into-legacy-API (the loader accepts null = 'not specified'; DependencyTracker ctor self- registration is the init-artifact pattern EISOP frames under a different key; DependencyGraphTest's null node is a deliberate test datum, runtime- legal via IdentityHashMap null keys) - all scoped + javadoc'd. Guard helper restructures (getAncestor(Path,levels) range-guard replacing an unchecked parent-chain). Stream->loop/tracker-local rewrites. Tests: guard-then-assert, assertions preserved, 1 scoped suppression.

…LNESS=true, -Werror) Phase-3 mid-tier: 99 findings in 20 files to zero. Honest @nullable: Proof @nullable [] loadProofFile, findProofLine @nullable ProofEntry, settingsId() @nullable Integer, picocli-injected @nullable bundlePath/output in Main. Crash-equivalent explicit NPE guards for Map.get/unboxing/getSelectedFile/getContainerType/contract/entry.proof chains (house style; requireNonNull rejected by this EISOP fork). 5 scoped argument.type.incompatible deliberate-null sites all verified runtime-legal (CheckConfigDialog + ProofManagementExt main: null Frame = standalone dialog, JDialog accepts null owner; KeYFacade replayProof + ensureSourceLoaded: loader error-origin-only / null-progressMonitor / null classpath = empty per JavaModel; HTMLReport.print: null into ST.add = empty). 3 scoped method.invocation.invalid ctor-only. ONE class-level exception: check/Node 's self-referential generic bound (T extends Comparable<T> implements Comparable<Node<T>>) trips EISOP's type-argument fixpoint - verified both alternates fail (wildcard-in-implements is javac-illegal; Comparable<? super T> also errors); scoped to single key type.argument.type.incompatible + javadoc'd.

@KeyFor

…_NULLNESS=true, -Werror) Phase-3 mid-tier: 147 findings in 23 files to zero. Honest @nullable widenings (SledgehammerSolver rawOutput/result/computationTime, launcher shutdown resources, NumberConstantsHandler numberSymbol/services fields, IntegerOpHandler integerLDT, sort lookups) + crash-equivalent NPE guards everywhere (Map.get/parent/preamble/ poll/Matcher.group/getMessage chains; requireNonNull rewritten to guards - rejected by this EISOP fork). IsabelleRule.posInOccurrence override param widened @nullable. @KeyFor fix: getExtraSorts/getPredefinedSorts wrap keySet() in new HashSet (callers only iterate; backing maps are HashMap so no ordering guarantee changes). Lazy-getter field-flow invalidation fixes in Mediator (getFinishedSolvers returns the real array via a non-null empty-array initializer + getters; prepareDialog still assigns the real array before any outcome callback). 11 scoped suppressions with javadoc rationale: method.invocation.invalid on ctor init artifacts (8), deliberate-null argument.type.incompatible (RuleApp pio null = hierarchy-stored @nullable; Mediator actionPerformed(null) - event unused by contract; MasterHandler this-before-ctor-end with only services already assigned; ProgressPanel lazy widget getter), methodref.receiver.bound.invalid init artifact (TranslationSettings this::save).

Phase-3 big-module infra behind -DENABLE_NULLNESS=true (onlyDefs ^de\.uka\. ilkd\.key covers main + test roots, -Xmaxerrs 10000, -Werror). Baseline (real, checked): 315 main findings; test-source findings appear once main is green (fail-fast). key.ui is handled in parallel from the main worktree (separate branch, pushed after this one lands).

…true, -Werror) key.core.infflow is now NullMarked-clean under the EISOP NullnessChecker: baseline 315 findings -> 0 (compileJava + compileTestJava, -Werror). Spotless and the full module test suite (incl. the InfFlowProfileLoadingTest autopilot integration test) are green. Suppressions (all javadoc'd, scoped): 9 nullness:argument.type.incompatible (5 deliberate-null-into-legacy/Map-value sites incl. the linkStateVarsToCopies null-pair convention consumed via containsKey by InfFlowProgVarRenamer, and the macro-level canApplyTo pass-through of a null PosInOccurrence to null-tolerant base implementations), 7 nullness:override.return.invalid (getGlobalDefs x4, getMbyAtPre x2, getOrigVars), 1 nullness:override.receiver.invalid. Deliberate nulls preserved: getGlobalDefs, getMbyAtPre, getOrigVars, mapTerm mby/result/exc, ExhaustiveProofMacro cache, collectAxioms asserted-null proofConfig, linkStateVarsToCopies null pairs.

@KeyFor

…ror) Main sources of the UI module now check clean with the EISOP NullnessChecker (3.49.5-eisop1, -AonlyDefs scoped to de.uka.ilkd.key / org.key_project.util): 2303 baseline findings in 276 files driven to zero via honest @nullable widenings, crash-equivalent explicit NPE guards, and scoped, javadoc'd suppressions (368 annotation sites, no class-level blankets, 0 added Objects.requireNonNull - rejected by this EISOP fork). Wiring (key.ui/build.gradle): EISOP NullnessChecker under -DENABLE_NULLNESS=true with the -AonlyDefs scope used by the other modules, plus a forked 4g javac worker heap - the checker OOM'd at the default 512m worker heap on this module's large source set (the bump is also required by CI's CodeQuality run). Notable fixes: - KeYGuiExtensionFacade: getContextMenuItems accepts a @nullable underlyingObject (keyboard-invoked menus pass a null position; base crashed or produced extension-dependent content, now consistently empty); getExtensionInstances drops null instances exactly like the base Objects::nonNull filter. - ProofAggregateTask.getProofEnv null-env guard mirroring BasicTask; ThreadUtilities rootGroup guard hoisted before the thread walk. - FontAwesomeSolid: explicit InputStream null guard (previous failure was an OOM artifact of the undersized checker worker). - Map.keySet() @KeyFor qualifier leaks erased via target-typed collection copies, per the isabelletranslation precedent. Known debt (CodeQuality expected RED until landed): :key.ui:compileTestJava still reports 23 findings in test sources (7 test files, untouched from base); follow-up widens the main-side contracts the tests rely on.

@nonnull

…DENABLE_NULLNESS=true, -Werror) Clears the known-debt note recorded in the KEY.UI LANDED ledger entry (c1c43c5): the 23 EISOP findings in the 7 untouched test files now check clean, flipping :key.ui CodeQuality from expected-RED to green. Main-side contract widening (the honest source of four test findings): - RecentFileMenu: ctor param + field accept a @nullable MainWindow (unit tests construct the menu without a real window); the two load-action deref sites (loadProofFromBundle, loadProblem) go through a new private requireMainWindow() NPE guard - crash-equivalent with the previous implicit NPE and unreachable in production (actions only fire from a real window); the JOptionPane parent site stays raw @nullable per JDK contract. Test-side fixes (assertions preserved, no behavior change): - RecentFileMenuTest: AssertJ assertThat()/isEqualTo() on the @nullable getMostRecent() suppressed scoped to the two test methods with javadoc (external library @nonnull signatures; both values null in the files-don't-exist branch, equal non-null in the exist branch). - ChaosMonkey: the getAllActions() method-ref chain (Reference::get / Objects::nonNull / Collectors.toSet) rewritten as an explicit WeakReference<Action> loop into a HashSet (EISOP rejects the chain); nullable log args wrapped in String.valueOf(...) at 3 LOGGER sites; getToolTipText() hoisted to a local to avoid the double nullable deref. - IssueDialogMessageTest: Document.insertString receives new SimpleAttributeSet() instead of a null AttributeSet (identical for plain text). - KeyboardTacletTest / ShortUniqueFileNamesTest: Map.keySet() @KeyFor qualifier leaks erased via target-typed HashSet copies (iso precedent); observable results identical (deterministic sorted stream / seeded-shuffle ArrayList, "insertion order does not matter"). - DisposedProofTreeUpdateTest: Objects.requireNonNull (rejected by this EISOP fork) converted to requireExampleDirectory()/requireProof() NPE-guard helpers - message-bearing, crash-equivalent. - AssumesInputTest: deliberate nulls into key.core ctors (BuildingException reclamation token/position, Location fileUri) suppressed method-scoped with javadoc; assertNotNull(err.position()) + double deref replaced by an explicit guard throwing AssertionError on null. - Extension: scoped class-level @SuppressWarnings("nullness:type.argument.type.incompatible") + javadoc for the self-referential generic bound (Extension<T> implements Comparable<Extension<T>>). The checker only mis-resolves T's lower bound (@KeyForBottom vs @UnknownKeyFor above NullType) under partial/incremental compilation; full module compiles were always clean. Same documented pattern as keyext.proofmanagement check/Node, applied so every build mode (including incremental and cached CI states) stays EISOP-green. Verification: canonical --rerun-tasks :key.ui:compileJava + :key.ui:compileTestJava green, and incremental builds green (the Extension flake is silenced); :key.ui:test + :key.ui:spotlessCheck green under -DENABLE_NULLNESS=true.

46 files from the key.ui EISOP landing (c1c43c5) carried pre-existing format violations (long annotated lines never re-wrapped because the commit-time gate died at :key.ui:compileTestJava before spotlessCheck ran). This commit is the mechanical `:key.ui:spotlessApply` output only: line wrapping and import order, zero semantic change (no checker delta by construction; the module was re-gated green afterwards, incl. spotlessCheck).

@NullMarked

… key.core files CI's formatting job (top-level spotlessCheck) flagged 4 key.core files whose import blocks carried JMLtk-rebase artifacts: a redundant blank line between the javaparser and jspecify import groups (TransactionStatement, AbstractOperationPO) and unused org.jspecify.annotations.NonNull imports (JmlDocRemoval, AuxiliaryContractBuilders - @NullMarked covers the file). Mechanical spotlessApply output; spotlessCheck clean; no semantic change.

… stub dir, heap) - key.core checkerFramework block behind -DENABLE_NULLNESS with -Werror, -Xmaxerrs 10000, module-wide -AonlyDefs (de.uka.ilkd.key, org.key_project.util) - -PnullWave=<FQCN,...> scopes -AonlyDefs to per-class waves for fast iteration - shared stub dir key.util/src/main/checkerframework for all modules (drops the explicit permit-nullness-assertion-exception.astub suffix), new javaparser astubs; retire java/beans/PropertyChangeSupport.astub - 6g daemon and forked javac worker heaps: the checker OOMs at defaults on key.core's ~1600-file source set - suppress the legacy -Ajavadoc.packages option in nullness builds (-Werror rejects the unrecognized -A warning once a processor is active)

…error) Full-module EISOP NullnessChecker conformance for key.core main sources (argument/assignment/deref waves consolidated; per-class -PnullWave waves merged into the module-wide gate). Honest @nullable widenings, explicit crash-equivalent guards, and scoped javadoc'd suppressions only; no behavior change.

The nullness annotations shifted line numbers in the pipeline builder sources (cluster 4 and the EISOP drive), so the 'Created by X.java:N' comments in the generated outputs drifted; the 76 affected expected files are regenerated from the actual pipeline output. Verified the diff is purely line-number updates and pure line moves.

Mirrors the checkerFramework job with Error Prone's NullAway in JSpecify mode. Left continue-on-error until key.core is NullAway-clean: the gate run on this head reports ~3.3k findings, most of which predate the rebase (the wave campaigns deepened the analysis instead of exhausting it, cf. docs/plan-jspecify-nullness.md). Flip the flag once the findings are driven to zero.

The NullnessChecker (EISOP) build hangs during compilation and burns the whole job timeout on CI. Disable the job (reversible via if: true); the operating nullness gate is NullAway for now.

wadoon self-assigned this Oct 25, 2026

wadoon force-pushed the nullness/jspecify-annotations branch 7 times, most recently from 05a372a to 4d3d3e3 Compare November 2, 2026 01:32

wadoon force-pushed the nullness/jspecify-annotations branch from 4d3d3e3 to 39412df Compare November 2, 2026 13:14

wadoon added 21 commits November 3, 2026 00:12

docs: add plan for JSpecify nullness annotations (follow-up of PR #3470)

3255256

feat(nullness): annotate de.uka.ilkd.key.logic with JSpecify (key.cor…

9f0c9a6

…e cluster 1) Class-level @NullMarked + @nullable where null is possible (232 uses). Verified by compile + spotlessCheck. Follow-up of PR #3470.

feat(nullness): annotate de.uka.ilkd.key.java.ast with JSpecify (key.…

0bf0a3b

…core cluster 2) 196 files @NullMarked; precise @nullable placements (132 uses). Verified by compile + spotlessCheck. Follow-up of PR #3470.

feat(nullness): annotate de.uka.ilkd.key.rule with JSpecify (key.core…

f5f722d

… cluster 3) 253 files @NullMarked; @nullable on lazily-nullable fields/params/returns. Verified by compile + spotlessCheck. Follow-up of PR #3470.

feat(nullness): annotate de.uka.ilkd.key.java (loader/transformations…

d583998

…/visitor) with JSpecify (key.core cluster 4) 72 files @NullMarked. Verified by compile + spotless. Follow-up of PR #3470.

feat(nullness): annotate de.uka.ilkd.key.proof with JSpecify (key.cor…

34d0ebf

…e cluster 5) 174 files @NullMarked; io/ carries the bulk (problem loaders, replayers, parser state, FileRepo streams). Verified by compile + spotless. PR #3470.

feat(nullness): annotate de.uka.ilkd.key.strategy with JSpecify (key.…

02679d0

…core cluster 6) 196 files @NullMarked; option/cache/feature chains annotated end-to-end. Verified by compile + spotless. PR #3470.

feat(nullness): annotate de.uka.ilkd.key.speclang with JSpecify (key.…

e244e70

…core cluster 7) 99 files @NullMarked, 755 @nullable across the JML/NJML/spec translation chain. Verified by compile + spotless. PR #3470.

feat(nullness): annotate de.uka.ilkd.key.smt with JSpecify (key.core …

34ad116

…cluster 8) 100 files @NullMarked; lazy-initialized translator state and Map.get chains annotated. Verified by compile + spotless. PR #3470.

feat(nullness): annotate key.core pp/util/scripts/macros with JSpecif…

4ac6aa6

…y (cluster 9) 117 files @NullMarked; scripts package-level @NullMarked from prior commit, @nullable gap-fills added. Verified by compile + spotless. PR #3470.

feat(nullness): annotate remaining key.core packages with JSpecify (c…

19c63e7

…luster 10) 151 files @NullMarked in ldt/nparser/parser/prover/control/axiom_abstraction/ taclettranslation/settings. Verified by compile + spotless. PR #3470.

build(nullness): add NullAway 0.14.3 to version catalog; document Pha…

9ad9b21

…se 2 trial setup Prepares the opt-in NullAway fast-trial for the annotated modules (-DENABLE_NULLAWAY), keeping EISOP as final conformance gate. PR #3470.

wadoon added 26 commits November 3, 2026 00:40

ci(nullness): skip the EISOP checkerFramework gate (hangs 6h on CI)

9ac56c6

The NullnessChecker (EISOP) build hangs during compilation and burns the whole job timeout on CI. Disable the job (reversible via if: true); the operating nullness gate is NullAway for now.

wadoon force-pushed the nullness/jspecify-annotations branch from 39412df to 9ac56c6 Compare November 3, 2026 09:37

Navigation Menu

Repository navigation

JSpecify nullness annotations (WIP): follow-up of PR #3470 - #4003

JSpecify nullness annotations (WIP): follow-up of PR #3470#4003
wadoon wants to merge 67 commits into
mainfrom
nullness/jspecify-annotations

wadoon commented Oct 24, 2026 •

edited

Loading

Uh oh!

Reviewers

Uh oh!

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Conversation

wadoon commented Oct 24, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Related Issue

Intended Change

Status at a Glance

Plan

1 · JSpecify annotations — done

2 · NullAway fast trials — done (opt-in -DENABLE_NULLAWAY)

3 · EISOP conformance (-DENABLE_NULLNESS=true -Werror) — modules done

4 · Final gates — ⬜

Type of pull request

Ensuring quality

Additional information and contact(s)

Plan

Uh oh!

Reviewers

Uh oh!

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

wadoon commented Oct 24, 2026 •

edited

Loading

2 · NullAway fast trials — done (opt-in `-DENABLE_NULLAWAY`)

3 · EISOP conformance (`-DENABLE_NULLNESS=true -Werror`) — modules done