Skip to content

Apply external class specs to user subclasses - #354

Open
CatarinaGamboa wants to merge 3 commits into
mainfrom
fix/16-subclass-receivers
Open

CatarinaGamboa wants to merge 3 commits into
mainfrom
fix/16-subclass-receivers

Conversation

@CatarinaGamboa

Copy link
Copy Markdown
Collaborator

Fixes #353.

Problem

An external spec (@ExternalRefinementsFor("java.lang.Throwable")) did not reach user subclasses: calling initCause on a custom RuntimeException subclass crashed with Sort mismatch at argument #1 for function java.lang.Throwable.state1 … supplied sort is AppException.

Example

class AppException extends RuntimeException {
    AppException(String message, Throwable cause) { super(message, cause); }
}
AppException e = new AppException("operation failed", underlying);
e.initCause(detail); // now: State Refinement Error, found withThrowable(e) but expected noThrowable(e)

With super(message) instead, the same initCause passes.

Change

  • RefinedVariable.addSuperTypes walks superclasses and interfaces transitively.
  • AuxStateHandler: a constructor whose first statement is super(...) inherits the to-state of the super constructor's spec, with the super arguments renamed to this constructor's parameters (or literals). If a to-state uses an argument that cannot be named, it falls back to the default state as before. The spec lookup walks up only through Exception, RuntimeException and Error, whose constructors delegate unchanged to Throwable; other JDK subclasses are not assumed to (e.g. ClassNotFoundException(String) sets a null cause).
  • RefinementProcessor: the first pass is split so all external specs are registered before any user class is checked; before, the result depended on the order of types in the package.

Tests

  • testSuite/classes/throwable_subclass_error: subclass built with super(message, cause), then initCause, gives a State Refinement Error.
  • testSuite/classes/throwable_subclass_correct: subclass built with super(message), then initCause, passes.
  • mvn test passes.

🤖 Generated with Claude Code

Fixes #353. A typestate call on a subclass of a specified class (e.g. a
custom RuntimeException calling initCause) crashed with a Z3 sort mismatch.

- RefinedVariable records supertypes transitively, so a subclass is related
  to the specified class however far up it is.
- A constructor whose first statement is super(...) takes the state the super
  constructor's spec gives, with the super arguments renamed to this
  constructor's parameters. The lookup walks through Exception,
  RuntimeException and Error only, whose constructors delegate to Throwable's
  unchanged; other JDK classes may not (ClassNotFoundException(String) sets a
  null cause), so they are not assumed to.
- RefinementProcessor registers all external specs before checking user
  classes, so the order of types in the package no longer matters.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
return null;
}

private static boolean inheritSuperConstructorState(CtConstructor<?> c, RefinedFunction f, TypeChecker tc) {

Copy link
Copy Markdown
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

this is a huge method can we maybe split it? and maybe add some documentation - at least 1 line what is doing

Copy link
Copy Markdown
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Split in 2c1cfbc: inheritSuperConstructorState is now about 15 lines and calls superConstructorCall (find the leading super(...)), specifiedConstructor (find the spec, walking through the delegating JDK classes), superParamsToArguments (map super params to the argument names) and renameStates (substitute them into the to-states). Each one has a Javadoc line. The method's own Javadoc had also ended up above the DELEGATING_JDK_CLASSES constant. I moved it back onto the method.

@CatarinaGamboa CatarinaGamboa added the enhancement New feature or request label Oct 7, 2026
- Log unresolvable supertypes in debug mode (new DebugLog.warn)
- Walk supertypes in a single loop
- Split inheritSuperConstructorState into documented helpers and fix
  its misplaced Javadoc

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
* The given states with the super constructor's parameters renamed, or null if one of them mentions a parameter
* whose argument has no name.
*/
private static List<ObjectState> renameStates(List<Predicate> toStates, Map<String, String> rename) {

Copy link
Copy Markdown
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

these are a lot of new functions in here, do we need them all? could we make them more concise? you can use more of a functional style if they end up more concise

Copy link
Copy Markdown
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Cut down in 7aa1bb0: there are now 3 functions instead of 5, and the code is about 30 lines shorter.

  • superConstructorCall is inlined into inheritSuperConstructorState as a pattern-matching guard.
  • superParamsToArguments and renameStates are merged into the main method. It builds a rename map and an unnamed set, rejects the inheritance if a state mentions an unnamed parameter (anyMatch), then maps each to-state through the substitutions with a reduce.
  • argumentName is small, returns an Optional, and says how a single argument can be named.
  • specifiedConstructor takes the CtExecutableReference directly instead of its three parts.

I kept argumentName and specifiedConstructor separate: the first is the per-argument rule and the second is the JDK delegation walk, and inlining them would make the main method harder to read.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

enhancement New feature or request

Projects

None yet

Development

Successfully merging this pull request may close these issues.

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

1 participant