diff --git a/.github/actions/setup-openjml/action.yml b/.github/actions/setup-openjml/action.yml index 2ee679f..fa54897 100644 --- a/.github/actions/setup-openjml/action.yml +++ b/.github/actions/setup-openjml/action.yml @@ -7,9 +7,9 @@ description: > Installs a pinned, checksum-verified OpenJML release (Ubuntu x64 build) into $RUNNER_TEMP/openjml and exposes the location as the OPENJML_HOME environment variable. The unzipped distribution (~1 GB, zip ~490 MB) is cached keyed on - version + checksum + fixup revision. Known-broken bundled JDK specification - files are deleted on install (see the fixup step below); because the deletion - happens before the cache is saved, cache hits already contain the fixed tree. + version + checksum + fixup revision. The bundled jdk/release is repaired on + install if needed (see the fixup step below); because the repair happens before + the cache is saved, cache hits already contain the fixed tree. inputs: version: @@ -27,9 +27,12 @@ runs: uses: actions/cache@55cc8345863c7cc4c66a329aec7e433d2d1c52a9 # v6 with: path: ${{ runner.temp }}/openjml - # spec-fixups-v2: bump this suffix whenever the fixup step below changes, + # spec-fixups-v3: bump this suffix whenever the fixup step below changes, # otherwise cached installs keep the previous fixup state. - key: openjml-ubuntu-x64-${{ inputs.version }}-${{ inputs.sha256 }}-spec-fixups-v2 + # v3 deletes no bundled spec any more: OpenJML 21.0.29 ships the RAC fixes for + # ArrayDeque.jml (dropped in v3, OpenJML/OpenJML#1012) and AtomicLong.jml (dropped in v2, + # OpenJML/Specs#29); the RAC suite passes against both bundled files (285/285). + key: openjml-ubuntu-x64-${{ inputs.version }}-${{ inputs.sha256 }}-spec-fixups-v3 - name: Download pinned OpenJML (checksum-verified) if: steps.cache.outputs.cache-hit != 'true' @@ -44,27 +47,7 @@ runs: rm "$RUNNER_TEMP/openjml.zip" chmod +x "$RUNNER_TEMP/openjml/openjml" "$RUNNER_TEMP/openjml/openjml-java" - - name: Delete known-broken bundled JDK specs (fixups v2) - if: steps.cache.outputs.cache-hit != 'true' - shell: bash - # The file ships broken in OpenJML 21.0.27 to 21.0.29 and breaks the RAC layer; deleting a - # bundled spec degrades the affected JDK class to default (empty) contracts, which - # is exactly what this repo needs — StreamBuffer's own contracts are the ones being - # checked. `rm` without -f: if an upgrade removes/fixes the file upstream, this - # step fails loudly and the fixup (plus the cache-key suffix) must be revisited. - # - ArrayDeque.jml: references the undeclared model variable `containsNull`; - # `openjml --rac` fails with "cannot find symbol: containsNull". - # Still open upstream (comment on OpenJML/OpenJML#806, closed issue). - # Dropped in v2: concurrent/atomic/AtomicLong.jml, whose RAC-generated checks read the - # private field AtomicLong.value across the module boundary (IllegalAccessError in every - # test touching the statistics counters). The upstream fix (OpenJML/Specs#29 + - # OpenJML/OpenJML#982) shipped in 21.0.29 -- its contracts are `//-RAC@` there -- and the - # suite passes against the bundled file (285/285, measured 2026-10-20). - run: | - set -euo pipefail - rm "$RUNNER_TEMP/openjml/specs/java/util/ArrayDeque.jml" - - - name: Repair the bundled JDK release file (fixups v2) + - name: Repair the bundled JDK release file (fixups v3) if: steps.cache.outputs.cache-hit != 'true' shell: bash # OpenJML 21.0.27's and 21.0.28's bundled jdk/release omit the JAVA_VERSION key (21.0.29 has diff --git a/CHANGELOG.md b/CHANGELOG.md index 25c1767..a357cd6 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -17,6 +17,11 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0 - Cancellable pipeline start-gate via a `startgate` GitHub Environment with configurable wait timer. ### Changed +- Formal verification: the last bundled-spec workaround is gone. OpenJML 21.0.29 also ships the RAC fix + for `ArrayDeque.jml` (OpenJML/OpenJML#1012), so the setup action no longer deletes any bundled spec + (fixups v3); RAC 285/285 against the unmodified 21.0.29 distribution. The class-invariant blocker is + narrowed down: RAC miscompiles an unqualified call from an inner-class method to an outer instance + method (`writeSingleByte(b)` in `SBOutputStream`), see TODO.md. - Build tooling: spotbugs-maven-plugin 4.10.4.1 -> 4.10.5.0 (SpotBugs 4.10.5, the first release that reads JSpecify; nothing to report here), in step with the sibling repositories. - Build and test tooling bumped in step with the sibling repositories: Spotless 3.10.4 and Checker @@ -28,7 +33,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0 Lincheck and jcstress runs depend on it. - Formal verification: OpenJML 21.0.29 (from 21.0.28). ESC 14/14 (1.7 s locally: SMT commands are now pipelined) and RAC 285/285 unchanged. The `AtomicLong.jml` workaround is gone -- the upstream fix - (OpenJML/Specs#29) shipped in 21.0.29 -- while `ArrayDeque.jml` is still deleted at install. Class + (OpenJML/Specs#29) shipped in 21.0.29 -- while `ArrayDeque.jml` was still deleted at install. Class invariants still break RAC (now `NoSuchMethodError` on the inner stream classes), so they stay out. - Build tooling: `anthropics/claude-code-action` v1.0.255 (from v1.0.252) and Gradle 9.8.2 in the shared `verify-signing-key-gradle` job, in step with the sibling repositories. diff --git a/CLAUDE.md b/CLAUDE.md index c003a7c..ec116e2 100644 --- a/CLAUDE.md +++ b/CLAUDE.md @@ -118,10 +118,13 @@ mvn -P jml-rac -Dopenjml.home= -Dopenjml.jdk.java=/jdk/bin/jav invariant inside the constructor of a non-static inner class and reads the field on the wrong class → `NoSuchFieldError` at runtime (14-line reproducer: private field + invariant + inner class). On this class every test fails (258/285). An earlier 21.0.27 compile crash - ("no enclosing instance") was not reproduced. **21.0.29 changed the symptom, not the defect:** + ("no enclosing instance") was not reproduced. **21.0.29 fixed that case but not this class:** the 14-line reproducer runs clean there, but the four candidate invariants on this class still - break RAC -- `NoSuchMethodError` on `StreamBuffer$SBOutputStream.JML$INV$$()` (RAC calls the - outer class's invariant check on the inner class), 106 errors (measured 2026-10-20). Re-test on upgrades. + break RAC -- `NoSuchMethodError` on `StreamBuffer$SBOutputStream.JML$INV$$()`, 106 errors + (measured 2026-10-20). Cause (narrowed down 2026-10-21): an inner-class method calling an outer + instance method *without a qualifier* (`writeSingleByte(b)`); RAC checks the callee's receiver + invariant on `this` (the inner object) instead of `StreamBuffer.this`. `Outer.this.m()` runs clean. + Reproducer in TODO.md. Re-test on upgrades. - `//@ nullable_by_default` at the class head is load-bearing for RAC: without it JML's non-null-by-default inserts an implicit non-null precondition on every reference parameter, so the null-argument tests hit `JmlAssertionError.Precondition` instead of the specified NPE. @@ -139,12 +142,13 @@ mvn -P jml-rac -Dopenjml.home= -Dopenjml.jdk.java=/jdk/bin/jav The setup action also patches `jdk/release` to add the `JAVA_VERSION` key surefire needs to fork that JVM (missing in 21.0.27/21.0.28, present again in 21.0.29; the guarded step is a no-op there and stays as a regression guard). -- One bundled OpenJML JDK spec is known-broken and deleted at install time by - `.github/actions/setup-openjml` (`ArrayDeque.jml`: undeclared `containsNull`, still in 21.0.29). - The second one, `atomic/AtomicLong.jml` (RAC read the private field `value` → - `IllegalAccessError`), was fixed upstream by [OpenJML/Specs#29](https://github.com/OpenJML/Specs/pull/29) - + [OpenJML/OpenJML#982](https://github.com/OpenJML/OpenJML/pull/982), released in 21.0.29; its - `rm` is gone, and the suite passes against the bundled file (285/285). +- No bundled OpenJML JDK spec is deleted at install any more (fixups v3). Up to 21.0.28 two were + broken under RAC and deleted by `.github/actions/setup-openjml`: `ArrayDeque.jml` (undeclared + `containsNull`, fixed via [OpenJML/OpenJML#1012](https://github.com/OpenJML/OpenJML/issues/1012)) + and `atomic/AtomicLong.jml` (RAC read the private field `value` → `IllegalAccessError`, fixed by + [OpenJML/Specs#29](https://github.com/OpenJML/Specs/pull/29) + + [OpenJML/OpenJML#982](https://github.com/OpenJML/OpenJML/pull/982)). Both fixes are in 21.0.29; + the suite passes against the unmodified distribution (285/285). - RAC classes are class-file 65 and live only under `target/rac-classes` — they never enter the shipped jar, so the Java 8 bytecode floor is unaffected. diff --git a/TODO.md b/TODO.md index 58399f0..2d0ade8 100644 --- a/TODO.md +++ b/TODO.md @@ -34,8 +34,8 @@ annotated, so everything below is genuinely still open. reporting upstream (its native peer already implements the methods the stub model never declared). Possible extension: a second harness for the array-read / `waitForAtLeast` blocking paths (jcstress already covers those; JPF would make them exhaustive too). - - **OpenJML bundled-spec defects** (21.0.28 shipped all of them, built from Specs `1a91cb6`; - the pinned 21.0.29 carries the AtomicLong fix and still ships the ArrayDeque one). All three share one cause: a model field declared + - **OpenJML bundled-spec defects — all fixed in 21.0.29, no workaround left (fixups v3)** + (21.0.28 shipped all of them, built from Specs `1a91cb6`). All three share one cause: a model field declared only behind `-RAC` in `java/lang/Iterable.jml` (`values`, `containsNull`) or a private `java.base` field (`value`) used in a clause RAC compiles. - `atomic/Atomic{Long,Integer,Boolean}.jml` (`value` → `IllegalAccessError` at runtime): @@ -47,13 +47,13 @@ annotated, so everything below is genuinely still open. (fixups v2); RAC 285/285 against the bundled 21.0.29 file. - `java/util/ArrayDeque.jml:30` (`containsNull` → RAC compile error) and `java/util/Collections.jml:116-117` (`singletonList`, `values` → RAC compile error): - **open.** Both are the original errors of the closed + **fixed upstream, released in 21.0.29** (`//-RAC@`, Specs `43ab561`). Both are the original errors of the closed [OpenJML/OpenJML#806](https://github.com/OpenJML/OpenJML/issues/806) ("repaired" there in 2024 — true for ESC/check, never for RAC; neither file changed in that window). **Reported** with a sweep over all bundled specs (9 files fail `--rac`) and a proposed fix in [OpenJML/OpenJML#1012](https://github.com/OpenJML/OpenJML/issues/1012) (2026-10-07). - Fix + red/green testspecs cases prepared locally, offered as PRs. Once released: drop the - `ArrayDeque.jml` `rm`. + **Done 2026-10-21:** the `ArrayDeque.jml` `rm` is gone (fixups v3); RAC compile and 285/285 + against the unmodified 21.0.29 distribution. - Missing `JAVA_VERSION` key in the bundled `jdk/release`: missing in 21.0.28 (reported in #1012), **present again in 21.0.29**; the guarded repair step is a no-op there and stays as a guard. - **Invariants + non-static inner classes break RAC — confirmed OpenJML bug, reported in @@ -62,9 +62,27 @@ annotated, so everything below is genuinely still open. **21.0.29: the minimal reproducer below runs clean, the defect on this class does not go away** -- with the four candidate invariants RAC throws `NoSuchMethodError` on `StreamBuffer$SBOutputStream.JML$INV$$()` (the outer invariant check called on the inner - class), 106 errors (measured 2026-10-20). A reproducer for - #1012 therefore needs an inner class whose methods run while the outer invariant is checked. - Minimal reproducer: + class), 106 errors (measured 2026-10-20). + **Narrowed down 2026-10-21 (21.0.29):** the trigger is an inner-class method calling an outer + instance method *without a qualifier* -- exactly the delegation `SBOutputStream.write(int)` → + `writeSingleByte(b)` (and `writeFromArray`, `closeAll`, `readSingleByte`, `availableClamped`). + RAC checks the callee's receiver invariant on `this` (the inner object) instead of + `StreamBuffer.this`: + ```java + public class InvA { + private long x = 1; + //@ private invariant 0 <= x; + void inc() { x++; } + class Inner { void go() { inc(); } } + public static void main(String... a) { new InvA().new Inner().go(); } + } + ``` + → `NoSuchMethodError: 'boolean InvA$Inner.JML$INV$$107()'`. Same with a `private` outer method. + Clean: `InvA.this.inc()`, `other.inc()` on another reference, outer → inner calls, + `synchronized (InvA.this) { x++; }` inside the inner class. To report on + [OpenJML/OpenJML#1012](https://github.com/OpenJML/OpenJML/issues/1012). Possible downstream + workaround to try: qualify the delegating calls as `StreamBuffer.this.writeSingleByte(b)`. + The 21.0.27/21.0.28 reproducer (fixed in 21.0.29): ```java public class Outer { private long x = 1; diff --git a/src/main/jml/net/ladenthin/streambuffer/StreamBuffer.jml b/src/main/jml/net/ladenthin/streambuffer/StreamBuffer.jml index f6ba247..e6306dd 100644 --- a/src/main/jml/net/ladenthin/streambuffer/StreamBuffer.jml +++ b/src/main/jml/net/ladenthin/streambuffer/StreamBuffer.jml @@ -89,8 +89,9 @@ public class StreamBuffer implements Closeable { // 258/285 tests fail. Minimal reproducer: private field + invariant + inner class (see // TODO.md). An earlier 21.0.27 compile crash ("no enclosing instance") was not reproduced. // 21.0.29: the minimal reproducer passes, but these four invariants on this class still break - // RAC with NoSuchMethodError on SBOutputStream.JML$INV$$() (106 errors) -- the same - // defect with a different symptom. + // RAC with NoSuchMethodError on SBOutputStream.JML$INV$$() (106 errors): the inner streams + // call outer instance methods without a qualifier (writeSingleByte(b)), and RAC checks the + // callee's invariant on the inner object instead of StreamBuffer.this (see TODO.md). // The candidate invariants // (0 <= availableBytes, 0 <= positionAtCurrentBufferEntry, 1 <= maxAllocationSize, // 0 <= maxObservedBytes) would have been RAC-only value anyway — the ESC layer proves