fix: cap byte[] allocations at MAX_ARRAY_LENGTH (Integer.MAX_VALUE - 8)

.github/actions/setup-openjml/action.yml

@@ -57,6 +57,7 @@ runs:
       #   - concurrent/atomic/AtomicLong.jml: RAC-generated checks read the private field
       #     AtomicLong.value across the module boundary; every test touching the
       #     statistics counters then dies with java.lang.IllegalAccessError.
+      #     Upstream fix: OpenJML/Specs#29 (+ test OpenJML/OpenJML#982); drop this rm once released.
       run: |
         set -euo pipefail
         rm "$RUNNER_TEMP/openjml/specs/java/util/ArrayDeque.jml"

CHANGELOG.md

@@ -28,6 +28,13 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 - CI `publish.yml`: `softprops/action-gh-release` bumped from v2 to v3.
 - CI `publish.yml`: `org.codehaus.mojo:exec-maven-plugin` bumped to 3.6.3.
 - Release Process prompt template moved from `CHANGELOG.md` to `docs/RELEASE.md`.
+- `maxAllocationSize` defaults to `Integer.MAX_VALUE - 8` (was `Integer.MAX_VALUE`);
+  `setMaxAllocationSize` clamps larger values to it.
+
+### Fixed
+- `trim()` with more than 2 GB buffered no longer allocates `new byte[Integer.MAX_VALUE]`, which the
+  JVM always rejects ("Requested array size exceeds VM limit"). Allocations are capped at
+  `Integer.MAX_VALUE - 8`, the JDK's `SOFT_MAX_ARRAY_LENGTH`.
 
 ## [1.2.0] - 2026-05-11
 

CLAUDE.md

@@ -114,8 +114,11 @@ mvn -P jml-rac -Dopenjml.home=<openjml> -Dopenjml.jdk.java=<openjml>/jdk/bin/jav
   at the ceiling-division boundary). Everything else is proven overflow-free under safe math.
 - The exception-message builder `newInvalidOffsetOrLengthToWriteException` carries an ASSUMED
   (unproven) contract — string concatenation defeats the SMT encoding. Do not inline it back.
-- NO class invariants in the `.jml`: OpenJML 21.0.27's RAC crashes on invariants combined with
-  non-static inner classes ("no enclosing instance" AssertionError). Re-test on upgrades.
+- NO class invariants in the `.jml`: adding instance invariants to this class made OpenJML 21.0.27's
+  RAC abort with a catastrophic javac `Lower` AssertionError ("no enclosing instance"). This was
+  NOT minimally reproducible (invariant + inner classes alone compiles fine — see TODO.md), so it
+  may be an artifact of a specific spec construct rather than a clean OpenJML bug; invariants stay
+  omitted defensively. 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.
@@ -134,7 +137,9 @@ mvn -P jml-rac -Dopenjml.home=<openjml> -Dopenjml.jdk.java=<openjml>/jdk/bin/jav
   fork that JVM.
 - Two bundled OpenJML JDK specs are known-broken and deleted at install time by
   `.github/actions/setup-openjml` (`ArrayDeque.jml`: undeclared `containsNull`;
-  `atomic/AtomicLong.jml`: RAC reads the private field `value` → `IllegalAccessError`).
+  `atomic/AtomicLong.jml`: RAC reads the private field `value` → `IllegalAccessError`;
+  upstream fix [OpenJML/Specs#29](https://github.com/OpenJML/Specs/pull/29) + test
+  [OpenJML/OpenJML#982](https://github.com/OpenJML/OpenJML/pull/982), both open).
 - 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.
 

TODO.md

@@ -34,12 +34,36 @@ 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).
-  - **Report the three OpenJML defects upstream** (all reproduced on 21.0.27, all documented in
-    the spec-file header / setup-openjml action): bundled `ArrayDeque.jml` references undeclared
-    `containsNull`; bundled `atomic/AtomicLong.jml` makes RAC emit an access to the private field
-    `AtomicLong.value` (`IllegalAccessError` at test runtime); RAC crashes with a javac `Lower`
-    AssertionError ("no enclosing instance") when a class with non-static inner classes declares
-    any instance invariant.
+  - **Report the OpenJML bundled-spec defects upstream** (both reproduced on 21.0.27 with a
+    minimal standalone class — the reproducers live in this session's notes, re-create before
+    filing):
+    - `java/util/ArrayDeque.jml:30` has an ungated `//@ instance public invariant !containsNull;`,
+      but `containsNull` is declared only in `java/lang/Iterable.jml` behind a `-RAC` key (and
+      carries the maintainers' own `// FIXME - get rid of this`). So under `openjml --rac` the
+      symbol is undeclared and RAC-compiling any ArrayDeque-using class fails with
+      "cannot find symbol: containsNull". ESC is unaffected (it keeps the `-RAC`-gated
+      declaration). Confirmed with a 4-line class.
+    - `java/util/concurrent/atomic/AtomicLong.jml` keeps `value`-referencing clauses that are not
+      `-RAC`-gated (e.g. line 16 `ensures value == v`), so RAC emits a direct read of the private
+      `java.base` field `AtomicLong.value`; running the instrumented class on a stock modular JVM
+      throws `IllegalAccessError` (compile succeeds, run fails). Confirmed with a 5-line class.
+      Also fails on OpenJML's own bundled JVM and via `openjml-java` (re-checked 2026-09-29).
+      The maintainers already `-RAC`-gate most `value` clauses → incomplete-guard defect.
+      Same defect in `AtomicInteger.jml` / `AtomicBoolean.jml`.
+      **Reported (2026-09-30), awaiting maintainer review:**
+      [OpenJML/Specs#29](https://github.com/OpenJML/Specs/pull/29) (fix for all three, base
+      `master-21`) + [OpenJML/OpenJML#982](https://github.com/OpenJML/OpenJML/pull/982)
+      (testspecs, base `master-21`). Verified locally: streambuffer RAC suite green WITH the
+      fixed `AtomicLong.jml` (285/285), red with the original (258/285 `IllegalAccessError`).
+      Once an OpenJML release ships it: drop the `rm` in `.github/actions/setup-openjml`.
+  - **NOT a confirmed OpenJML bug (do not report yet):** during this work RAC once aborted with a
+    catastrophic javac `Lower` AssertionError ("no enclosing instance of type
+    StreamBuffer.SBInputStream") when the `.jml` declared instance invariants on the class with the
+    non-static inner stream classes. That crash was real but could NOT be reproduced minimally
+    (invariant + inner class, invariant + inner class extending InputStream, and invariant +
+    eager inner-class-instance fields all compiled cleanly). Until a minimal reproducer exists it
+    is unclear whether it is an OpenJML defect or an artifact of some specific spec construct;
+    the invariants stay omitted defensively regardless. Isolate before filing.
   - **Deeper ESC — instance-method / trim() functional correctness (parked, revisit).** Today
     ESC proves the 14 static helpers; the instance methods and trim() are RAC-only. A full
     functional proof (e.g. a ghost model sequence for the deque with the invariant

src/main/java/net/ladenthin/streambuffer/StreamBuffer.java

@@ -133,9 +133,18 @@ public class StreamBuffer implements Closeable {
     private final AtomicLong totalBytesRead = new AtomicLong();
 
     /**
-     * Maximum size of a single byte array during consolidation. Default {@link Integer#MAX_VALUE}.
+     * Largest {@code byte[]} length this class allocates: {@code Integer.MAX_VALUE - 8}.
+     * Same value as {@code jdk.internal.util.ArraysSupport.SOFT_MAX_ARRAY_LENGTH}, mirrored
+     * because that class is JDK-internal (not exported, absent on Java 8).
+     * Reason: VMs reserve array header words; HotSpot rejects {@code Integer.MAX_VALUE} and
+     * {@code Integer.MAX_VALUE - 1} with "Requested array size exceeds VM limit", on any heap size.
      */
-    private volatile long maxAllocationSize = Integer.MAX_VALUE;
+    static final int MAX_ARRAY_LENGTH = Integer.MAX_VALUE - 8;
+
+    /**
+     * Maximum size of a single byte array during consolidation. Default {@link #MAX_ARRAY_LENGTH}.
+     */
+    private volatile long maxAllocationSize = MAX_ARRAY_LENGTH;
 
     /**
      * Flag set to true while trim is rearranging internal buffers.
@@ -258,7 +267,8 @@ public long getMaxAllocationSize() {
     /**
      * Set the maximum size of a single byte array allocated during {@link #trim()}.
      * When trim consolidates the buffer, it splits data into chunks respecting
-     * this limit. Default is {@link Integer#MAX_VALUE}.
+     * this limit. Default is {@link #MAX_ARRAY_LENGTH} ({@code Integer.MAX_VALUE - 8});
+     * larger values are clamped to it.
      *
      * @param maxSize maximum allocation size in bytes. Must be positive.
      * @throws IllegalArgumentException if maxSize is not positive.
@@ -267,7 +277,7 @@ public void setMaxAllocationSize(final long maxSize) {
         if (maxSize <= 0) {
             throw new IllegalArgumentException("maxAllocationSize must be positive but was " + maxSize);
         }
-        this.maxAllocationSize = maxSize;
+        this.maxAllocationSize = Math.min(maxSize, MAX_ARRAY_LENGTH);
     }
 
     /**
@@ -652,7 +662,7 @@ boolean shouldTrim() {
      *
      * If availableBytes ever exceeds Integer.MAX_VALUE (e.g., 5GB+ of buffered data):
      * 1. This method returns Integer.MAX_VALUE (~2.1GB)
-     * 2. The trim() loop reads Integer.MAX_VALUE bytes in one iteration
+     * 2. The trim() loop reads at most maxAllocationSize (&#x2264; MAX_ARRAY_LENGTH) bytes per iteration
      * 3. Loop condition (available > 0) allows continuation
      * 4. Next iteration calls available() again, reads remaining bytes
      * 5. Process repeats until all availableBytes are consolidated

src/main/jml/net/ladenthin/streambuffer/StreamBuffer.jml

@@ -83,10 +83,13 @@ public class StreamBuffer implements Closeable {
 
     // ---------------------------------------------------------------------------------------
     // NO class invariants — deliberate, and load-bearing for the RAC layer:
-    // `openjml --rac` (21.0.27) crashes with "no enclosing instance of type
-    // StreamBuffer.SBInputStream in scope" (javac Lower AssertionError, exit 4) as soon as
-    // this class declares any instance invariant, because the generated invariant checks
-    // interact badly with the non-static inner stream classes. The candidate invariants
+    // adding instance invariants to THIS class made `openjml --rac` (21.0.27) abort with
+    // "no enclosing instance of type StreamBuffer.SBInputStream in scope" (javac Lower
+    // AssertionError, exit 4) — the generated invariant checks interact badly with the
+    // non-static inner stream classes. NB: this was not reproducible in isolation (a bare
+    // invariant + inner class compiles fine), so it may be an artifact of a specific spec
+    // construct rather than a clean OpenJML bug (see TODO.md); the invariants stay omitted
+    // defensively either way. The candidate invariants
     // (0 <= availableBytes, 0 <= positionAtCurrentBufferEntry, 1 <= maxAllocationSize,
     // 0 <= maxObservedBytes) would have been RAC-only value anyway — the ESC layer proves
     // static methods, which never see instance state. Their content is still enforced

src/test/java/net/ladenthin/streambuffer/StreamBufferTest.java

@@ -2642,7 +2642,7 @@
         @Test
         public void clampToMaxInt_valueAboveMaxInt_returnsMaxInt() {
             // arrange
             StreamBuffer sb = new StreamBuffer();
             // act
             // assert
             assertThat(StreamBuffer.clampToMaxInt((long) Integer.MAX_VALUE + 1), is(Integer.MAX_VALUE));
@@ -2652,7 +2652,7 @@
         @Test
         public void clampToMaxInt_valueEqualToMaxInt_returnsMaxInt() {
             // arrange
             StreamBuffer sb = new StreamBuffer();
             // act
             // assert
             assertThat(StreamBuffer.clampToMaxInt((long) Integer.MAX_VALUE), is(Integer.MAX_VALUE));
@@ -2678,7 +2678,7 @@
             // original: current - decrement = 9 - 4 = 5
             // mutant:   current + decrement = 9 + 4 = 13  → mutation killed
             // arrange
             StreamBuffer sb = new StreamBuffer();
             // act
             // assert
             assertThat(StreamBuffer.decrementAvailableBytesBudget(9L, 4L), is(5L));
@@ -3219,17 +3219,67 @@
     @DisplayName("maxAllocationSize: getter, setter, trim behavior")
     class MaxAllocationSizeTests {
 
-        @DisplayName("maxAllocationSize(): default value — is integer max value")
+        static Stream<Arguments> aboveMaxArrayLength() {
+            return Stream.of(
+                    Arguments.of((long) StreamBuffer.MAX_ARRAY_LENGTH + 1), // boundary
+                    Arguments.of((long) Integer.MAX_VALUE - 1), // HotSpot VM limit
+                    Arguments.of((long) Integer.MAX_VALUE), // old default
+                    Arguments.of(Long.MAX_VALUE));
+        }
+
+        static Stream<Arguments> atOrBelowMaxArrayLength() {
+            return Stream.of(
+                    Arguments.of((long) StreamBuffer.MAX_ARRAY_LENGTH), // boundary
+                    Arguments.of((long) StreamBuffer.MAX_ARRAY_LENGTH - 1),
+                    Arguments.of(1L));
+        }
+
+        @DisplayName("MAX_ARRAY_LENGTH: equals JDK SOFT_MAX_ARRAY_LENGTH (Integer.MAX_VALUE - 8)")
+        @Test
+        public void maxArrayLength_value_isIntegerMaxValueMinusEight() {
+            // assert
+            assertThat(StreamBuffer.MAX_ARRAY_LENGTH, is(Integer.MAX_VALUE - 8));
+        }
+
+        @DisplayName("maxAllocationSize(): default value — is MAX_ARRAY_LENGTH")
         @Test
-        public void maxAllocationSize_defaultValue_isIntegerMaxValue() {
+        public void maxAllocationSize_defaultValue_isMaxArrayLength() {
             // arrange
             StreamBuffer sb = new StreamBuffer();
 
             // act
             long maxSize = sb.getMaxAllocationSize();
 
             // assert
-            assertThat(maxSize, is((long) Integer.MAX_VALUE));
+            assertThat(maxSize, is((long) StreamBuffer.MAX_ARRAY_LENGTH));
+        }
+
+        @DisplayName("setMaxAllocationSize(): above MAX_ARRAY_LENGTH — clamped to MAX_ARRAY_LENGTH")
+        @ParameterizedTest
+        @MethodSource("aboveMaxArrayLength")
+        public void setMaxAllocationSize_aboveMaxArrayLength_clamped(final long maxSize) {
+            // arrange
+            StreamBuffer sb = new StreamBuffer();
+
+            // act
+            sb.setMaxAllocationSize(maxSize);
+
+            // assert
+            assertThat(sb.getMaxAllocationSize(), is((long) StreamBuffer.MAX_ARRAY_LENGTH));
+        }
+
+        @DisplayName("setMaxAllocationSize(): at / below MAX_ARRAY_LENGTH — kept as set")
+        @ParameterizedTest
+        @MethodSource("atOrBelowMaxArrayLength")
+        public void setMaxAllocationSize_atOrBelowMaxArrayLength_kept(final long maxSize) {
+            // arrange
+            StreamBuffer sb = new StreamBuffer();
+
+            // act
+            sb.setMaxAllocationSize(maxSize);
+
+            // assert
+            assertThat(sb.getMaxAllocationSize(), is(maxSize));
         }
 
         @DisplayName("maxAllocationSize(): set and get — returns set value")
@@ -3563,7 +3613,7 @@
         @Test
         public void decrementAvailableBytesBudget_subtracts_notAdds() {
             // arrange
             final StreamBuffer sb = new StreamBuffer();
 
             // act — Verify arithmetic: 100 - 30 = 70, NOT 100 + 30 = 130 (kills MathMutator on - operator)
             final long result = StreamBuffer.decrementAvailableBytesBudget(100L, 30L);
@@ -3751,7 +3801,7 @@
         @Test
         public void shouldSkipTrimDueToEdgeCase_boundsComparison() {
             // arrange
             final StreamBuffer sb = new StreamBuffer();
 
             // act & assert
             // Test >= boundary: when resultingChunks >= currentBufferSize, should skip
@@ -3777,7 +3827,7 @@
         @Test
         public void shouldSkipTrimDueToInvalidMaxBufferElements_boundsComparison() {
             // arrange
             final StreamBuffer sb = new StreamBuffer();
 
             // act & assert
             // Test <= boundary: when maxBufferElements <= 0, should skip
@@ -4028,7 +4078,7 @@
         @Test
         public void shouldCheckEdgeCase_boundaryMaxAllocSize_lessThan() {
             // arrange
             final StreamBuffer sb = new StreamBuffer();
 
             // act - maxAllocSize == availableBytes means NOT <
             // 100 > 0 (true) && 100 < 100 (false) = false
@@ -4267,7 +4317,7 @@
             assertThrows(NullPointerException.class, () -> sb.addTrimEndSignal(null));
         }
 
         /**
          * CRITICAL TEST: Exception during trim start signal release doesn't deadlock stream
          *
          * REQUIREMENT: If releaseTrimStartSignals() throws an exception (line 442),
@@ -4952,7 +5002,7 @@
         @Test
         public void isAvailableBytesPositive_one_returnsTrue() {
             // arrange
             final StreamBuffer sb = new StreamBuffer();
 
             // act
             final boolean result = StreamBuffer.isAvailableBytesPositive(1);
@@ -4965,7 +5015,7 @@
         @Test
         public void isAvailableBytesPositive_negative_returnsFalse() {
             // arrange
             final StreamBuffer sb = new StreamBuffer();
 
             // act
             final boolean result = StreamBuffer.isAvailableBytesPositive(-100);
@@ -5004,7 +5054,7 @@
         @Test
         public void isMaxAllocSizeLessThanAvailable_greaterThan_returnsFalse() {
             // arrange
             final StreamBuffer sb = new StreamBuffer();
 
             // act - when maxAllocSize > availableBytes
             final boolean result = StreamBuffer.isMaxAllocSizeLessThanAvailable(100, 50);
@@ -5017,7 +5067,7 @@
         @Test
         public void shouldUpdateMaxObservedBytes_equal_returnsFalse() {
             // arrange
             final StreamBuffer sb = new StreamBuffer();
 
             // act - when availableBytes == currentMax
             final boolean result = StreamBuffer.shouldUpdateMaxObservedBytes(100, 100);
@@ -5374,7 +5424,7 @@
         @DisplayName("shouldCheckEdgeCase(): with max alloc size greater — returns false")
         @Test
         public void shouldCheckEdgeCase_withMaxAllocSizeGreater_returnsFalse() {
             StreamBuffer sb = new StreamBuffer();
             // maxAllocSize < availableBytes is false
             assertThat(StreamBuffer.shouldCheckEdgeCase(50, 100), is(false));
         }
@@ -5773,7 +5823,7 @@
         }
     }
 
     /**
      * CORRECTNESS TESTS: Configuration changes don't affect running trim operations
      *
      * Requirement: When trim is already executing, changes to configuration parameters
@@ -5791,7 +5841,7 @@
      * - New configuration takes effect only in subsequent trim operations
      */
 
     /**
      * ROBUSTNESS TESTS: Edge cases and stress scenarios for trim operation
      *
      * Tests verify trim handles: