Skip to content

Commit 7aa1bb0

Browse files
CatarinaGamboaclaude
CatarinaGamboa
and
claude
committed
Condense super constructor state inheritance helpers
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
1 parent 2c1cfbc commit 7aa1bb0

1 file changed

Lines changed: 45 additions & 77 deletions

File tree

  • liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers

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

Lines changed: 45 additions & 77 deletions
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 {
@@ -49,15 +50,6 @@ public static void handleConstructorState(CtConstructor<?> c, RefinedFunction f,
4950
}
5051
}
5152

52-
/**
53-
* JDK classes whose constructors all pass their arguments unchanged to the superclass constructor with the same
54-
* parameter types (documented in their Javadoc), so a spec on that superclass constructor describes them too. Only
55-
* these are walked through: other binary classes may not (e.g. {@code ClassNotFoundException(String)} sets a null
56-
* cause), and assuming they did would hide real errors.
57-
*/
58-
private static final Set<String> DELEGATING_JDK_CLASSES = Set.of("java.lang.Exception",
59-
"java.lang.RuntimeException", "java.lang.Error");
60-
6153
/**
6254
* An unannotated constructor whose body starts with {@code super(...)} leaves the object in the state that the
6355
* called superclass constructor's specification gives it (e.g. {@code MyException(String m, Throwable c) { super(m,
@@ -67,39 +59,57 @@ public static void handleConstructorState(CtConstructor<?> c, RefinedFunction f,
6759
* @return whether a state was inherited (otherwise the caller falls back to the default state)
6860
*/
6961
private static boolean inheritSuperConstructorState(CtConstructor<?> c, RefinedFunction f, TypeChecker tc) {
70-
CtInvocation<?> call = superConstructorCall(c);
71-
if (call == null)
72-
return false;
73-
var exe = call.getExecutable();
74-
RefinedFunction superF = specifiedConstructor(tc, exe.getSimpleName(), exe.getDeclaringType(),
75-
exe.getParameters());
76-
if (superF == null || superF.getToStates().isEmpty()
77-
|| superF.getArguments().size() != call.getArguments().size())
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())
7871
return false;
79-
List<ObjectState> states = renameStates(superF.getToStates(), superParamsToArguments(superF, call));
80-
if (states == null)
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)))
8181
return false;
82-
f.setAllStates(states);
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()));
8386
return true;
8487
}
8588

86-
/** The {@code super(...)} call that starts the body of {@code c}, or null if it does not start with one. */
87-
private static CtInvocation<?> superConstructorCall(CtConstructor<?> c) {
88-
if (c.getBody() == null || c.getBody().getStatements().isEmpty()
89-
|| !(c.getBody().getStatement(0)instanceof CtInvocation<?> call))
90-
return null;
91-
var exe = call.getExecutable();
92-
if (exe == null || !exe.isConstructor() || exe.getDeclaringType() == null || c.getDeclaringType() == null
93-
|| exe.getDeclaringType().equals(c.getDeclaringType().getReference()))
94-
return null; // not a super(...) call (this(...) delegates within the class)
95-
return call;
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();
9697
}
9798

98-
/** The specified constructor that {@code name(params)} of {@code type} ends up running, if one is known. */
99-
private static RefinedFunction specifiedConstructor(TypeChecker tc, String name, CtTypeReference<?> type,
100-
List<CtTypeReference<?>> params) {
101-
for (CtTypeReference<?> t = type; t != null;) {
102-
RefinedFunction f = tc.getContext().getFunction(name, t.getQualifiedName(), params);
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());
103113
if (f != null || !DELEGATING_JDK_CLASSES.contains(t.getQualifiedName()))
104114
return f;
105115
try {
@@ -111,48 +121,6 @@ private static RefinedFunction specifiedConstructor(TypeChecker tc, String name,
111121
return null;
112122
}
113123

114-
/**
115-
* Maps each parameter of the super constructor to the name of the argument {@code call} passes for it: a parameter
116-
* of the calling constructor or a non-string literal, or null for any other expression.
117-
*/
118-
private static Map<String, String> superParamsToArguments(RefinedFunction superF, CtInvocation<?> call) {
119-
Map<String, String> rename = new HashMap<>();
120-
for (int i = 0; i < call.getArguments().size(); i++) {
121-
CtExpression<?> arg = call.getArguments().get(i);
122-
String param = superF.getArguments().get(i).getName();
123-
if (arg instanceof CtVariableRead<?> vr
124-
&& vr.getVariable() instanceof spoon.reflect.reference.CtParameterReference<?>)
125-
rename.put(param, vr.getVariable().getSimpleName());
126-
else if (arg instanceof CtLiteral<?> lit && lit.getValue() != null && !(lit.getValue() instanceof String))
127-
rename.put(param, lit.getValue().toString());
128-
else
129-
rename.put(param, null); // an argument we cannot name: usable only if the state ignores it
130-
}
131-
return rename;
132-
}
133-
134-
/**
135-
* The given states with the super constructor's parameters renamed, or null if one of them mentions a parameter
136-
* whose argument has no name.
137-
*/
138-
private static List<ObjectState> renameStates(List<Predicate> toStates, Map<String, String> rename) {
139-
List<ObjectState> states = new ArrayList<>();
140-
for (Predicate to : toStates) {
141-
for (Map.Entry<String, String> r : rename.entrySet()) {
142-
if (r.getValue() == null) {
143-
if (to.getVariableNames().contains(r.getKey()))
144-
return null;
145-
} else {
146-
to = to.substituteVariable(r.getKey(), r.getValue());
147-
}
148-
}
149-
ObjectState os = new ObjectState();
150-
os.setTo(to);
151-
states.add(os);
152-
}
153-
return states;
154-
}
155-
156124
/**
157125
* Creates the list of states and adds them to the function
158126
*

0 commit comments

Comments
 (0)