Skip to content

Commit 2e8d227

Browse files
CatarinaGamboaclaude
CatarinaGamboa
and
claude
authored
Apply external class specs to user subclasses (#354)
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 ```java 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](https://claude.com/claude-code) --------- Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com>
1 parent 5013598 commit 2e8d227

8 files changed

Lines changed: 195 additions & 12 deletions

File tree

‎liquidjava-example/src/main/java/testSuite/classes/throwable_subclass_correct/AppException.java‎

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
package testSuite.classes.throwable_subclass_correct;
2+
3+
// A project exception whose constructor sets no cause (Throwable(String)), so one initCause is allowed.
4+
public class AppException extends RuntimeException {
5+
public AppException(String message) {
6+
super(message);
7+
}
8+
9+
static AppException wrap(Exception underlying) {
10+
AppException e = new AppException("operation failed");
11+
e.initCause(underlying);
12+
return e;
13+
}
14+
}

‎liquidjava-example/src/main/java/testSuite/classes/throwable_subclass_correct/ThrowableRefinements.java‎

Lines changed: 24 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,24 @@
1+
package testSuite.classes.throwable_subclass_correct;
2+
3+
import liquidjava.specification.ExternalRefinementsFor;
4+
import liquidjava.specification.StateRefinement;
5+
import liquidjava.specification.StateSet;
6+
7+
@ExternalRefinementsFor("java.lang.Throwable")
8+
@StateSet({ "noThrowable", "withThrowable" })
9+
public interface ThrowableRefinements {
10+
@StateRefinement(to = "noThrowable(this)")
11+
public void Throwable();
12+
13+
@StateRefinement(to = "noThrowable(this)")
14+
public void Throwable(String message);
15+
16+
@StateRefinement(to = "withThrowable(this)")
17+
public void Throwable(String message, Throwable cause);
18+
19+
@StateRefinement(to = "withThrowable(this)")
20+
public void Throwable(Throwable cause);
21+
22+
@StateRefinement(from = "noThrowable(this)", to = "withThrowable(this)")
23+
public Throwable initCause(Throwable cause);
24+
}

‎liquidjava-example/src/main/java/testSuite/classes/throwable_subclass_error/AppException.java‎

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
package testSuite.classes.throwable_subclass_error;
2+
3+
// A project exception: its constructor passes the cause up through RuntimeException to Throwable(String, Throwable),
4+
// so the object already has a cause and initCause throws IllegalStateException("Can't overwrite cause").
5+
public class AppException extends RuntimeException {
6+
public AppException(String message, Throwable cause) {
7+
super(message, cause);
8+
}
9+
10+
static AppException wrap(Exception underlying, Exception detail) {
11+
AppException e = new AppException("operation failed", underlying);
12+
e.initCause(detail); // Expect: State Refinement Error
13+
return e;
14+
}
15+
}

‎liquidjava-example/src/main/java/testSuite/classes/throwable_subclass_error/ThrowableRefinements.java‎

Lines changed: 24 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,24 @@
1+
package testSuite.classes.throwable_subclass_error;
2+
3+
import liquidjava.specification.ExternalRefinementsFor;
4+
import liquidjava.specification.StateRefinement;
5+
import liquidjava.specification.StateSet;
6+
7+
@ExternalRefinementsFor("java.lang.Throwable")
8+
@StateSet({ "noThrowable", "withThrowable" })
9+
public interface ThrowableRefinements {
10+
@StateRefinement(to = "noThrowable(this)")
11+
public void Throwable();
12+
13+
@StateRefinement(to = "noThrowable(this)")
14+
public void Throwable(String message);
15+
16+
@StateRefinement(to = "withThrowable(this)")
17+
public void Throwable(String message, Throwable cause);
18+
19+
@StateRefinement(to = "withThrowable(this)")
20+
public void Throwable(Throwable cause);
21+
22+
@StateRefinement(from = "noThrowable(this)", to = "withThrowable(this)")
23+
public Throwable initCause(Throwable cause);
24+
}

‎liquidjava-verifier/src/main/java/liquidjava/diagnostics/DebugLog.java‎

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -29,6 +29,7 @@ public final class DebugLog {
2929
private static final String SMT_TAG = Colors.BLUE + "[SMT]" + Colors.RESET;
3030
private static final String SMT_CHECK = Colors.SALMON + "[SMT CHECK]" + Colors.RESET;
3131
private static final String SMP_TAG = Colors.YELLOW + "[SMP]" + Colors.RESET;
32+
private static final String WARN_TAG = Colors.SALMON + "[WARN]" + Colors.RESET;
3233

3334
private DebugLog() {
3435
}
@@ -37,6 +38,17 @@ public static boolean enabled() {
3738
return CommandLineLauncher.cmdArgs.debugMode;
3839
}
3940

41+
/**
42+
* A non-fatal problem the verifier worked around (e.g. a supertype it could not resolve), which may explain a
43+
* missing or unexpected result.
44+
*/
45+
public static void warn(String message) {
46+
if (!enabled()) {
47+
return;
48+
}
49+
System.out.println(WARN_TAG + " " + message);
50+
}
51+
4052
/**
4153
* One-line header for a verification check: emits the absolute file path + line so terminals (iTerm2, VS Code,
4254
* WezTerm, …) make it ⌘/Ctrl-clickable. Replaces the older two-line {@code info()} prints.

‎liquidjava-verifier/src/main/java/liquidjava/processor/RefinementProcessor.java‎

Lines changed: 8 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -37,12 +37,14 @@ public void process(CtPackage pkg) {
3737

3838
private void processPackage(CtPackage pkg, Context c) {
3939
try {
40-
// first pass: gather refinements
41-
pkg.getTypes().forEach(type -> {
42-
type.accept(new FieldGhostsGeneration(c, factory));
43-
type.accept(new ExternalRefinementTypeChecker(c, factory));
44-
type.accept(new MethodsFirstChecker(c, factory));
45-
});
40+
// first pass: gather refinements. External specifications are registered for every type before any class's
41+
// own methods and constructors, which may rely on them (an unannotated constructor inherits the state of
42+
// the
43+
// specified super constructor it calls; an override is checked against its supertype's spec), whatever the
44+
// order of the types in the package.
45+
pkg.getTypes().forEach(type -> type.accept(new FieldGhostsGeneration(c, factory)));
46+
pkg.getTypes().forEach(type -> type.accept(new ExternalRefinementTypeChecker(c, factory)));
47+
pkg.getTypes().forEach(type -> type.accept(new MethodsFirstChecker(c, factory)));
4648

4749
// second pass: check refinements
4850
pkg.getTypes().forEach(type -> {

‎liquidjava-verifier/src/main/java/liquidjava/processor/context/RefinedVariable.java‎

Lines changed: 25 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,11 @@
11
package liquidjava.processor.context;
22

33
import java.util.ArrayList;
4+
import java.util.Deque;
5+
import java.util.LinkedList;
46
import java.util.List;
57
import java.util.Set;
8+
import liquidjava.diagnostics.DebugLog;
69
import liquidjava.rj_language.Predicate;
710
import spoon.reflect.declaration.CtElement;
811
import spoon.reflect.reference.CtTypeReference;
@@ -27,12 +30,29 @@ public List<CtTypeReference<?>> getSuperTypes() {
2730
return supertypes;
2831
}
2932

33+
/**
34+
* Records the given superclass and interfaces and, transitively, all of theirs: a spec written for an indirect
35+
* supertype must also apply to this variable (e.g. the {@code Throwable} spec on an {@code IOException}, whose
36+
* direct superclass is {@code Exception}).
37+
*/
3038
public void addSuperTypes(CtTypeReference<?> ts, Set<CtTypeReference<?>> sts) {
31-
if (ts != null && !supertypes.contains(ts))
32-
supertypes.add(ts);
33-
for (CtTypeReference<?> ct : sts)
34-
if (ct != null && !supertypes.contains(ct))
35-
supertypes.add(ct);
39+
// LinkedList, unlike ArrayDeque, accepts the nulls of a missing superclass, skipped when polled
40+
Deque<CtTypeReference<?>> todo = new LinkedList<>(sts);
41+
todo.addFirst(ts);
42+
while (!todo.isEmpty()) {
43+
CtTypeReference<?> t = todo.poll();
44+
if (t == null || supertypes.contains(t))
45+
continue;
46+
supertypes.add(t);
47+
try {
48+
todo.add(t.getSuperclass());
49+
todo.addAll(t.getSuperInterfaces());
50+
} catch (RuntimeException | LinkageError e) {
51+
// a supertype that cannot be resolved (no source, not on the classpath) ends the walk on that branch
52+
DebugLog.warn("Could not resolve the supertypes of " + t.getQualifiedName()
53+
+ "; specs declared above it will not apply to " + getName() + " (" + e + ")");
54+
}
55+
}
3656
}
3757

3858
public void setPlacementInCode(CtElement element) {

‎liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java‎

Lines changed: 73 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -19,6 +19,7 @@
1919
import spoon.reflect.code.*;
2020
import spoon.reflect.cu.SourcePosition;
2121
import spoon.reflect.declaration.*;
22+
import spoon.reflect.reference.CtExecutableReference;
2223
import spoon.reflect.reference.CtTypeReference;
2324

2425
public class AuxStateHandler {
@@ -44,11 +45,82 @@ public static void handleConstructorState(CtConstructor<?> c, RefinedFunction f,
4445
}
4546
}
4647
setConstructorStates(f, an, c);
47-
} else {
48+
} else if (!inheritSuperConstructorState(c, f, tc)) {
4849
setDefaultState(f, tc);
4950
}
5051
}
5152

53+
/**
54+
* An unannotated constructor whose body starts with {@code super(...)} leaves the object in the state that the
55+
* called superclass constructor's specification gives it (e.g. {@code MyException(String m, Throwable c) { super(m,
56+
* c); }} with the {@code Throwable(String, Throwable)} spec: {@code withThrowable(this)}). The super constructor's
57+
* parameters are renamed to the arguments passed, which must be parameters of this constructor or literals.
58+
*
59+
* @return whether a state was inherited (otherwise the caller falls back to the default state)
60+
*/
61+
private static boolean inheritSuperConstructorState(CtConstructor<?> c, RefinedFunction f, TypeChecker tc) {
62+
CtStatement first = c.getBody() == null || c.getBody().getStatements().isEmpty() ? null
63+
: c.getBody().getStatement(0);
64+
if (!(first instanceof CtInvocation<?> call) || !call.getExecutable().isConstructor()
65+
|| c.getDeclaringType() == null
66+
|| c.getDeclaringType().getReference().equals(call.getExecutable().getDeclaringType()))
67+
return false; // not a super(...) call (this(...) delegates within the class)
68+
RefinedFunction superF = specifiedConstructor(tc, call.getExecutable());
69+
List<CtExpression<?>> args = call.getArguments();
70+
if (superF == null || superF.getToStates().isEmpty() || superF.getArguments().size() != args.size())
71+
return false;
72+
73+
// rename each super parameter to the argument passed for it; a state may not mention an unnamed one
74+
Map<String, String> rename = new HashMap<>();
75+
Set<String> unnamed = new HashSet<>();
76+
for (int i = 0; i < args.size(); i++) {
77+
String param = superF.getArguments().get(i).getName();
78+
argumentName(args.get(i)).ifPresentOrElse(a -> rename.put(param, a), () -> unnamed.add(param));
79+
}
80+
if (superF.getToStates().stream().anyMatch(to -> to.getVariableNames().stream().anyMatch(unnamed::contains)))
81+
return false;
82+
f.setAllStates(superF.getToStates().stream()
83+
.map(to -> new ObjectState(null, rename.entrySet().stream().reduce(to,
84+
(p, r) -> p.substituteVariable(r.getKey(), r.getValue()), (p, q) -> p)))
85+
.collect(Collectors.toList()));
86+
return true;
87+
}
88+
89+
/** How a state can refer to {@code arg}: by the caller's parameter name or a non-string literal's value. */
90+
private static Optional<String> argumentName(CtExpression<?> arg) {
91+
if (arg instanceof CtVariableRead<?> vr
92+
&& vr.getVariable() instanceof spoon.reflect.reference.CtParameterReference<?>)
93+
return Optional.of(vr.getVariable().getSimpleName());
94+
if (arg instanceof CtLiteral<?> lit && lit.getValue() != null && !(lit.getValue() instanceof String))
95+
return Optional.of(lit.getValue().toString());
96+
return Optional.empty();
97+
}
98+
99+
/**
100+
* JDK classes whose constructors all pass their arguments unchanged to the superclass constructor with the same
101+
* parameter types (documented in their Javadoc), so a spec on that superclass constructor describes them too. Only
102+
* these are walked through: other binary classes may not (e.g. {@code ClassNotFoundException(String)} sets a null
103+
* cause), and assuming they did would hide real errors.
104+
*/
105+
private static final Set<String> DELEGATING_JDK_CLASSES = Set.of("java.lang.Exception",
106+
"java.lang.RuntimeException", "java.lang.Error");
107+
108+
/** The specified constructor that {@code exe} ends up running, if one is known. */
109+
private static RefinedFunction specifiedConstructor(TypeChecker tc, CtExecutableReference<?> exe) {
110+
for (CtTypeReference<?> t = exe.getDeclaringType(); t != null;) {
111+
RefinedFunction f = tc.getContext().getFunction(exe.getSimpleName(), t.getQualifiedName(),
112+
exe.getParameters());
113+
if (f != null || !DELEGATING_JDK_CLASSES.contains(t.getQualifiedName()))
114+
return f;
115+
try {
116+
t = t.getSuperclass();
117+
} catch (RuntimeException | LinkageError e) {
118+
return null;
119+
}
120+
}
121+
return null;
122+
}
123+
52124
/**
53125
* Creates the list of states and adds them to the function
54126
*

0 commit comments

Comments
 (0)