Skip to content

Commit 553c53c

Browse files
CatarinaGamboaclaude
CatarinaGamboa
and
claude
committed
Apply external class specs to user subclasses
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>
1 parent be47cb6 commit 553c53c

7 files changed

Lines changed: 190 additions & 11 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/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: 28 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,8 @@
11
package liquidjava.processor.context;
22

3+
import java.util.ArrayDeque;
34
import java.util.ArrayList;
5+
import java.util.Deque;
46
import java.util.List;
57
import java.util.Set;
68
import liquidjava.rj_language.Predicate;
@@ -27,12 +29,34 @@ public List<CtTypeReference<?>> getSuperTypes() {
2729
return supertypes;
2830
}
2931

32+
/**
33+
* Records the given superclass and interfaces and, transitively, all of theirs: a spec written for an indirect
34+
* supertype must also apply to this variable (e.g. the {@code Throwable} spec on an {@code IOException}, whose
35+
* direct superclass is {@code Exception}).
36+
*/
3037
public void addSuperTypes(CtTypeReference<?> ts, Set<CtTypeReference<?>> sts) {
31-
if (ts != null && !supertypes.contains(ts))
32-
supertypes.add(ts);
38+
Deque<CtTypeReference<?>> todo = new ArrayDeque<>();
39+
if (ts != null)
40+
todo.add(ts);
3341
for (CtTypeReference<?> ct : sts)
34-
if (ct != null && !supertypes.contains(ct))
35-
supertypes.add(ct);
42+
if (ct != null)
43+
todo.add(ct);
44+
while (!todo.isEmpty()) {
45+
CtTypeReference<?> t = todo.poll();
46+
if (supertypes.contains(t))
47+
continue;
48+
supertypes.add(t);
49+
try {
50+
CtTypeReference<?> sup = t.getSuperclass();
51+
if (sup != null)
52+
todo.add(sup);
53+
for (CtTypeReference<?> i : t.getSuperInterfaces())
54+
if (i != null)
55+
todo.add(i);
56+
} catch (RuntimeException | LinkageError ignored) {
57+
// a supertype that cannot be resolved (no source, not on the classpath) ends the walk on that branch
58+
}
59+
}
3660
}
3761

3862
public void setPlacementInCode(CtElement element) {

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

Lines changed: 77 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -44,11 +44,87 @@ public static void handleConstructorState(CtConstructor<?> c, RefinedFunction f,
4444
}
4545
}
4646
setConstructorStates(f, an, c);
47-
} else {
47+
} else if (!inheritSuperConstructorState(c, f, tc)) {
4848
setDefaultState(f, tc);
4949
}
5050
}
5151

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

0 commit comments

Comments
 (0)