Hacktoberfest 2026: die Issues, die Maintainer für den Oktober markiert haben – offen und einsteigerfreundlich. Hacktoberfest-Issues durchsuchen

External specs do not reach user subclasses: a typestate call on a subclass receiver crashes with a sort mismatch

Geschlossen
  • Stimmt etwas nicht?
#353 0 Kommentare 0 Reaktionen 0 zugewiesene Personen Auf GitHub ansehen

Maintainer antworten meist innerhalb von 1 Tag

Ein zugehöriger Pull Request wurde bereits gemerged.

  • #354 von @CatarinaGamboa — gemerged

Bewertung

Schwierigkeit
4/5
Geschätzter Aufwand
3-5 Tage
Anfängerfreundlichkeit
35/100
Issue-Typ
Bug
Klarheit
Klar beschrieben
Aktivitätsstatus
Aktiv
Tech-Stack
java
Bereich
compilers

Rechercherichtung

Start from RefinedVariable (how it records superclass/interface relations) and RefinementProcessor (its first pass processes types one by one), the two components named in the Causes section. Reproduce with the Repro/AppException example on main to see the sort mismatch, then trace where the state function argument sort is chosen for a subclass receiver. Done looks like the subclass case reporting State Refinement Error: found withThrowable(e) but expected noThrowable(e) instead of crashing — but note open PR #354 is already addressing this, so coordinate before starting.

Vom Indexierungsmodell aus dem Issue-Text verfasst.

Beschreibung

bug

An external spec written for a class (@ExternalRefinementsFor("java.lang.Throwable")) does not reach user subclasses. A typestate call on a subclass receiver makes the verifier crash instead of reporting the violation.

Example

Spec (abridged from the Barista Throwable spec):

@ExternalRefinementsFor("java.lang.Throwable")
@StateSet({"noThrowable", "withThrowable"})
public interface ThrowableRefinements {
    @StateRefinement(to = "noThrowable(this)") void Throwable(String message);
    @StateRefinement(to = "withThrowable(this)") void Throwable(String message, Throwable cause);
    @StateRefinement(from = "noThrowable(this)", to = "withThrowable(this)") Throwable initCause(Throwable cause);
}

Client code (a real bug shape: initCause on an exception whose cause was already set throws IllegalStateException: Can't overwrite cause):

public class Repro {
    static class AppException extends RuntimeException {
        AppException(String message, Throwable cause) { super(message, cause); }
    }
    static AppException wrap(Exception underlying, Exception detail) {
        AppException e = new AppException("operation failed", underlying);
        e.initCause(detail); // throws at runtime
        return e;
    }
}

On main (be47cb68):

Error: Sort mismatch at argument #1 for function (declare-fun java.lang.Throwable.state1 (java.lang.Throwable) Int) supplied sort is Repro$AppException

The same code with Throwable e = new Throwable("operation failed", underlying); is reported as intended:

State Refinement Error: found withThrowable(e) but expected noThrowable(e)

Causes

  1. RefinedVariable records only the direct superclass and the direct interfaces, so AppException is never related to Throwable (two levels up), and the state function's argument sort does not match.
  2. A user constructor that delegates to super(...) gets the default state rather than the state the super constructor's spec gives.
  3. RefinementProcessor runs the first pass type by type, so a user class can be processed before the external spec it depends on is registered.

Found while building exercises from real Java bugs (e.g. the "Can't overwrite cause" bugs in Apache projects), where a custom exception subclass is the usual shape.

Vorherrschende Sprache
Java
Sterne
67
Forks
36
Ø Merge
2 T. 4 Std.
Gemergte PRs (30 T.)
28

Entwicklungsumgebung

Erste Schritte

  1. Lesen Sie das ganze Issue und danach den Beitragsleitfaden des Projekts.
  2. Schreiben Sie ins Issue, dass Sie es übernehmen — das erspart doppelte Arbeit.
  3. Forken Sie das Repository und arbeiten Sie in einem Branch.
  4. Öffnen Sie einen Pull Request, der die Issue-Nummer nennt.

Mehr aus liquid-java/liquidjava

Alle Issues in liquid-java/liquidjava

Ähnliche Issues

Weitere Issues zu Java

Neue Issues direkt in Ihr Postfach

Eine kurze Übersicht über anfängerfreundliche GitHub-Issues.