RAC: spurious ClassCastException from a callee's signals clause at the call site, and a stack trace per call for skipped Arrays.equalArrays clauses (from streambuffer) #1050

[Assisted by Claude Code.] A follow-up to #1012, again from running streambuffer's JUnit suite under RAC. I'm still not a JML/OpenJML expert and most of the analysis was done with Claude Code. Both findings reproduce identically with the 21.0.28 release (Ubuntu build) and with dev-21 built from source at 529ac454da (Specs dc9f6be, the newest dev-21 on 2026-10-17), so as far as I can tell they are not fixed yet. I may have misread the causes or proposed the wrong fixes, so please treat everything here as a starting point and verify it in your own Claude session — the section For a Claude Code session at the end has everything an agent needs. If they turn out to be real, it would be great if they could make it into the next release.

Neither finding produces a wrong verdict — every contract in streambuffer holds — but the first prints a spurious "undefined" report and the second floods the output.

1. Call-site check of a callee's signals (E e) P casts the exception to E without instanceof → spurious ClassCastException

A method may throw two exception types, and a signals clause constrains only one of them. If a call site passes an argument for which the predicate folds to false (here the long literal 1L) and the callee throws the other allowed exception, the RAC code at the call site reports a ClassCastException. As far as I understand JML, signals (E e) P only applies when the exception is an E, so nothing should be reported.

public class SignalsRepro {
  /*@ public behavior
    @   requires true;
    @   signals_only IllegalArgumentException, InterruptedException;
    @   signals (IllegalArgumentException e) x <= 0;
    @*/
  public static void m(long x) throws InterruptedException {
    if (x <= 0) throw new IllegalArgumentException();
    throw new InterruptedException();
  }
  public static void caller() throws InterruptedException { m(1L); }
  public static void main(String[] a) {
    try { m(1L); } catch (InterruptedException e) { System.out.println("direct ok"); }
    try { caller(); } catch (InterruptedException e) { System.out.println("via caller ok"); }
  }
}

$ openjml --rac -d out SignalsRepro.java      # compiles, exit 0
$ openjml-java -cp out SignalsRepro            # same with -Dorg.jmlspecs.openjml.rac=exception, exit 0
JML undefined exceptional postcondition - exception thrown
java.lang.ClassCastException: class java.lang.InterruptedException cannot be cast to class java.lang.IllegalArgumentException (java.lang.InterruptedException and java.lang.IllegalArgumentException are in module java.base of loader 'bootstrap')
	at SignalsRepro.main(SignalsRepro.java:5)
direct ok
JML undefined exceptional postcondition - exception thrown
java.lang.ClassCastException: class java.lang.InterruptedException cannot be cast to class java.lang.IllegalArgumentException (java.lang.InterruptedException and java.lang.IllegalArgumentException are in module java.base of loader 'bootstrap')
	at SignalsRepro.caller(SignalsRepro.java:5)
	at SignalsRepro.main(SignalsRepro.java:14)
via caller ok

What I checked around it (same on 21.0.28 and dev-21):

• With m(1) (an int literal) or a non-constant argument, nothing is reported.
• Without the signals clause, or with signals (Exception e) true;, nothing is reported.
• A real violation (throwing IllegalArgumentException for x == 1) is reported correctly as JML signals condition is false and is thrown under rac=exception — no CCE there.
• --code-math=java --spec-math=java makes no difference. The callee-side check is fine; it is only the call-site code.

Where I think it comes from — JmlAssertionAdder.applyHelper, signals branch (21.0.28 lines 12311–12353, dev-21 12566–12608, same text). The cast (E) exception is declared when the unconverted clause expression is not false (21.0.28 l. 12322 / 12326; dev-21 l. 12577 / 12581). The instanceof E guard is only built when the converted expression e is not a false literal (21.0.28 l. 12341, dev-21 l. 12596). With x := 1L, e becomes false, the guard becomes true, and the cast runs unconditionally. javap agrees: with m(1L) there is a checkcast IllegalArgumentException followed by iconst_0 and no instanceof; with m(1) there is instanceof/ifeq before the cast.

A possible fix, untested, which you may well do differently: build the type test whenever the variable was declared, i.e. drop !treeutils.isFalseLit(e) from the condition in line 12341 (dev-21 12596).

Two smaller observations: the report is only printed even with -Dorg.jmlspecs.openjml.rac=exception (the catch (RuntimeException) calls Utils.reportException) — probably intended for "undefined"; and the line in the stack (SignalsRepro.java:5) is the clause, not the call.

In streambuffer this appears once per run of StreamBufferTest$ThreadInterruptionDuringReadTests, because waitForAnyData() is return waitForAtLeast(1L); and waitForAtLeast has exactly the spec above. The tests stay green.

2. A skipped clause with an uncompiled model method prints a full stack trace on every execution (System.arraycopy / byte[].clone() → Arrays.equalArrays)

Each execution of System.arraycopy on byte[] and each byte[].clone() prints a NoSuchMethodError with its full stack trace plus Skipping a specification clause because it contains an uncompiled model method. It repeats on every call, not once per clause:

public class ArraycopyRepro {
  public static void main(String[] a) {
    int n = a.length > 0 ? Integer.parseInt(a[0]) : 1000;
    byte[] src = new byte[16];
    byte[] dst = new byte[16];
    for (int i = 0; i < n; i++) {
      System.arraycopy(src, 0, dst, 0, src.length);
    }
    System.out.println("arraycopy done: " + n);
  }
}

$ openjml --rac -d out ArraycopyRepro.java
$ openjml-java -cp out ArraycopyRepro 1
java.lang.NoSuchMethodError: 'boolean java.util.Arrays.equalArrays(byte[], org.jmlspecs.lang.internal.bigint, byte[], org.jmlspecs.lang.internal.bigint, org.jmlspecs.lang.internal.bigint)'
	at ArraycopyRepro.main(ArraycopyRepro.java:11)
Skipping a specification clause because it contains an uncompiled model method: 'boolean java.util.Arrays.equalArrays
arraycopy done: 1
$ openjml-java -cp out ArraycopyRepro 1000 | grep -c 'Skipping a specification clause'
1000

1000 iterations give 355,021 bytes (3,001 lines); the same loop with src.clone() gives NoSuchMethodError: 'boolean java.util.Arrays.equalArrays(byte[], byte[])' 1000 times. --code-math=java --spec-math=java changes nothing. Under a test framework the stack is deeper, about 10 KB per call: one streambuffer stress test (2 million single-byte writes, with a buffer consolidation that calls arraycopy per chunk) ran for 7,344 s under RAC and wrote the message 2,003,546 times (about 21 GB of log) before it was stopped — with every contract holding. streambuffer now scales its stress loops down under RAC, so the minimal reproducer above is the better test case.

The clauses involved (unchanged on Specs dev-21):

• java/lang/System.jml:268 (byte[] case of arraycopy): ensures java.util.Arrays.equalArrays(da,destPos,sa,srcPos,length_); → java/util/Arrays.jml:968, a model method without a body. The other element types (lines 202–257) have the same shape.
• java/lang/Object.jml:168 (byte[] case of clone): ensures java.util.Arrays.equalArrays((byte[])\result,(byte[])this); → Arrays.jml:984. The other element types use an executable \forall there.
• Same pattern with new IOException(cause): java/io/IOException.jml:21 → Throwable.standardThrowable(Throwable).

Where the repetition seems to come from. JmlAssertionAdder wraps each clause in catch (NoSuchMethodError) { Utils.reportNoSuchMethod(e, null) }, and Utils.reportNoSuchMethod (runtime/Utils.java:296–304) always calls printStackTrace without remembering what it already reported. Compiling with -quiet generates an empty catch block and silences it completely (a real violation is still thrown) — a workaround for us, but it also hides every other skipped-clause note.

Possible improvements, you will know better: report each skipped clause (or each missing model method) only once per run and print the stack only at a higher verbosity; and/or make the two byte[] clauses executable (a \forall like the other clone cases) or //-RAC@, in the style of Specs 43ab561. Related: the location passed to reportNoSuchMethod is always null (// FIXME - really need to propagate the location of the call), so the line in the stack is the end of the file, not the call.

For a Claude Code session

Everything needed to reproduce both findings, from scratch, on Linux (Ubuntu 24.04 was used):

1. Minimal reproducers — save the two classes above as SignalsRepro.java and ArraycopyRepro.java, then with an OpenJML 21.0.28 release or a dev-21 build:

   openjml --rac -d out SignalsRepro.java && <openjml>/jdk/bin/java -cp out:<openjml>/jmlruntime.jar SignalsRepro
   openjml --rac -d out ArraycopyRepro.java && <openjml>/jdk/bin/java -cp out:<openjml>/jmlruntime.jar ArraycopyRepro 1000 | grep -c 'Skipping a specification clause'
   

   Expected today: two ClassCastException reports for (1) and 1000 for (2). Expected after a fix: no report for (1), and at most one per clause for (2). Counter-checks for (1): change m(1L) to m(1) (no report), drop the signals clause (no report), throw IllegalArgumentException for x == 1 (a correct JML signals condition is false).
2. In streambuffer — commit 98000f5 (JDK 21 + Maven 3.9):

   git clone https://github.com/bernardladenthin/streambuffer.git && cd streambuffer && git checkout 98000f5
   mvn -q dependency:build-classpath -Dmdep.outputFile=target/compile-classpath.txt -DincludeScope=compile
   mkdir -p target/rac-classes
   <openjml>/openjml --rac --rac-show-source=line --code-math=java --spec-math=java \
     --class-path "$(cat target/compile-classpath.txt)" --specs-path src/main/jml \
     -d target/rac-classes src/main/java/net/ladenthin/streambuffer/StreamBuffer.java
   mvn -P jml-rac -Dopenjml.home=<openjml> -Dopenjml.jdk.java=<openjml>/jdk/bin/java \
     -Dtest='StreamBufferTest$ThreadInterruptionDuringReadTests' test
   

   Look for JML undefined exceptional postcondition in the output (finding 1). For finding 2, run the whole suite and count Skipping a specification clause. On the 21.0.28 release the RAC compile needs the three workarounds from RAC: 9 bundled specs don't compile under --rac, inner-class invariants, and related findings (from streambuffer) #1012 that .github/actions/setup-openjml applies (delete specs/java/util/ArrayDeque.jml and specs/java/util/concurrent/atomic/AtomicLong.jml, add JAVA_VERSION to jdk/release); on dev-21 none were needed.
3. Source locations — JmlAssertionAdder.java applyHelper (21.0.28 l. 12311–12353, dev-21 l. 12566–12608) for (1); runtime/Utils.java l. 296–304, specs/java/lang/System.jml:268, specs/java/lang/Object.jml:168, specs/java/util/Arrays.jml:968/984 for (2).

The dev-21 build followed .github/workflows/build.yml; make release stopped only at the VS Code extension step (npm: not found), the OpenJML distribution itself was complete.

Thanks again for OpenJML and for the quick turnaround on #1012!