Skip to content

Commit cab0b30

Browse files
CatarinaGamboaCatarinaGamboa
committed
refactor code in methodchecker
1 parent 3ac0f36 commit cab0b30

1 file changed

Lines changed: 146 additions & 154 deletions

File tree

‎liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/MethodsFunctionsChecker.java‎

Lines changed: 146 additions & 154 deletions
Original file line numberDiff line numberDiff line change
@@ -84,58 +84,62 @@ public void getConstructorInvocationRefinements(CtConstructorCall<?> ctConstruct
8484

8585
// ################### VISIT METHOD ##############################
8686
public <R> void getMethodRefinements(CtMethod<R> method) throws LJError {
87-
RefinedFunction f = new RefinedFunction();
88-
f.setName(method.getSimpleName().replaceAll("\\p{C}", "")); // remove any empty chars from string
89-
f.setType(method.getType());
90-
f.setRefReturn(new Predicate());
91-
f.setPlacementInCode(method);
92-
93-
CtClass<?> klass = null;
94-
if (method.getParent() instanceof CtClass) {
95-
klass = (CtClass<?>) method.getParent();
96-
f.setClass(klass.getQualifiedName());
97-
}
98-
if (method.getParent()instanceof CtInterface<?> inter) {
99-
f.setClass(inter.getQualifiedName());
100-
}
101-
String owner = f.getTargetClass();
102-
if (owner != null)
103-
f.setSignature(String.format("%s.%s", owner, method.getSignature()));
104-
else
105-
f.setSignature(method.getSignature());
106-
rtc.getContext().addFunctionToContext(f);
87+
String className = parentQualifiedName(method);
88+
String signature = (className != null) ? String.format("%s.%s", className, method.getSignature())
89+
: method.getSignature();
90+
RefinedFunction f = buildAndRegisterFunction(method, method.getSimpleName(), className, signature);
10791

108-
auxGetMethodRefinements(method, f);
10992
String prefix = method.getDeclaringType().getQualifiedName();
11093
AuxStateHandler.handleMethodState(method, f, rtc, prefix);
11194

112-
if (klass != null)
95+
if (method.getParent()instanceof CtClass<?> klass)
11396
AuxHierarchyRefinementsPassage.checkFunctionInSupertypes(klass, method, f, rtc);
11497
}
11598

11699
public <R> void getMethodRefinements(CtMethod<R> method, String prefix) throws LJError {
117100
String constructorName = "<init>";
118-
String k = Utils.getSimpleName(prefix);
101+
boolean isConstructor = Utils.getSimpleName(prefix).equals(method.getSimpleName());
102+
String functionName = isConstructor ? constructorName : String.format("%s.%s", prefix, method.getSimpleName());
103+
String signature = String.format("%s.%s", prefix, method.getSignature());
119104

120-
String functionName = String.format("%s.%s", prefix, method.getSimpleName());
121-
if (k.equals(method.getSimpleName())) { // is a constructor
122-
functionName = String.format(constructorName);
105+
RefinedFunction f = buildAndRegisterFunction(method, functionName, prefix, signature);
106+
107+
AuxStateHandler.handleMethodState(method, f, rtc, prefix);
108+
if (isConstructor && !f.hasStateChange()) {
109+
AuxStateHandler.setDefaultState(f, rtc);
123110
}
111+
}
124112

113+
/**
114+
* Creates a {@link RefinedFunction} with the shared boilerplate (sanitized name, type, empty return refinement,
115+
* placement, optional owning class and signature), registers it in the context, and processes its parameter/return
116+
* refinements.
117+
*/
118+
private RefinedFunction buildAndRegisterFunction(CtMethod<?> method, String name, String className,
119+
String signature) throws LJError {
125120
RefinedFunction f = new RefinedFunction();
126-
f.setName(functionName.replaceAll("\\p{C}", "")); // remove any empty chars from string
121+
f.setName(name.replaceAll("\\p{C}", "")); // remove any empty chars from string
127122
f.setType(method.getType());
128123
f.setRefReturn(new Predicate());
129124
f.setPlacementInCode(method);
130-
f.setClass(prefix);
131-
f.setSignature(String.format("%s.%s", prefix, method.getSignature()));
125+
if (className != null)
126+
f.setClass(className);
127+
f.setSignature(signature);
132128
rtc.getContext().addFunctionToContext(f);
133129
auxGetMethodRefinements(method, f);
130+
return f;
131+
}
134132

135-
AuxStateHandler.handleMethodState(method, f, rtc, prefix);
136-
if (functionName.equals(constructorName) && !f.hasStateChange()) {
137-
AuxStateHandler.setDefaultState(f, rtc);
138-
}
133+
/**
134+
* Qualified name of the type ({@link CtClass} or {@link CtInterface}) declaring {@code element}, or {@code null}.
135+
*/
136+
private static String parentQualifiedName(CtElement element) {
137+
CtElement parent = element.getParent();
138+
if (parent instanceof CtClass<?> c)
139+
return c.getQualifiedName();
140+
if (parent instanceof CtInterface<?> i)
141+
return i.getQualifiedName();
142+
return null;
139143
}
140144

141145
private <R> void auxGetMethodRefinements(CtMethod<R> method, RefinedFunction rf) throws LJError {
@@ -183,44 +187,47 @@ private Predicate handleFunctionRefinements(RefinedFunction f, CtElement method,
183187
public <R> void getReturnRefinements(CtReturn<R> ret) throws LJError {
184188
CtClass<?> c = ret.getParent(CtClass.class);
185189
String className = c.getSimpleName();
186-
if (ret.getReturnedExpression() != null) {
187-
// check if there are refinements
188-
if (rtc.getRefinement(ret.getReturnedExpression()) == null)
189-
ret.getReturnedExpression().putMetadata(Keys.REFINEMENT, new Predicate());
190-
CtMethod<?> method = ret.getParent(CtMethod.class);
191-
// check if method has refinements
192-
if (rtc.getRefinement(method) == null)
193-
return;
194-
if (method.getParent() instanceof CtClass) {
195-
RefinedFunction fi = rtc.getContext().getFunction(method.getSimpleName(),
196-
((CtClass<?>) method.getParent()).getQualifiedName(), method.getParameters().size());
197-
if (fi == null)
198-
return;
190+
if (ret.getReturnedExpression() == null) {
191+
return;
192+
}
199193

200-
List<Variable> lv = fi.getArguments();
201-
for (Variable v : lv) {
202-
rtc.getContext().addVarToContext(v);
203-
}
194+
// check if there are refinements
195+
if (rtc.getRefinement(ret.getReturnedExpression()) == null)
196+
ret.getReturnedExpression().putMetadata(Keys.REFINEMENT, new Predicate());
197+
CtMethod<?> method = ret.getParent(CtMethod.class);
204198

205-
// Both return and the method have metadata
206-
String thisName = String.format(Formats.THIS, className);
207-
rtc.getContext().addInstanceToContext(thisName, c.getReference(), new Predicate(), ret);
199+
// check if method has refinements
200+
if (rtc.getRefinement(method) == null || !(method.getParent() instanceof CtClass))
201+
return;
208202

209-
String returnVarName = String.format(Formats.RET, rtc.getContext().getCounter());
210-
Predicate cretRef = rtc.getRefinement(ret.getReturnedExpression())
211-
.substituteVariable(Keys.WILDCARD, returnVarName).substituteVariable(Keys.THIS, returnVarName);
212-
Predicate cexpectedType = fi.getRefReturn().substituteVariable(Keys.WILDCARD, returnVarName)
213-
.substituteVariable(Keys.THIS, returnVarName);
203+
RefinedFunction fi = rtc.getContext().getFunction(method.getSimpleName(),
204+
((CtClass<?>) method.getParent()).getQualifiedName(), method.getParameters().size());
205+
if (fi == null)
206+
return;
214207

215-
rtc.getContext().addVarToContext(returnVarName, method.getType(), cretRef, ret);
216-
rtc.checkSMT(cexpectedType, ret, fi.getMessage());
217-
rtc.getContext().newRefinementToVariableInContext(returnVarName, cexpectedType);
218-
}
208+
List<Variable> lv = fi.getArguments();
209+
for (Variable v : lv) {
210+
rtc.getContext().addVarToContext(v);
219211
}
212+
213+
// Both return and the method have metadata
214+
String thisName = String.format(Formats.THIS, className);
215+
rtc.getContext().addInstanceToContext(thisName, c.getReference(), new Predicate(), ret);
216+
217+
String returnVarName = String.format(Formats.RET, rtc.getContext().getCounter());
218+
Predicate cretRef = rtc.getRefinement(ret.getReturnedExpression())
219+
.substituteVariable(Keys.WILDCARD, returnVarName).substituteVariable(Keys.THIS, returnVarName);
220+
Predicate cexpectedType = fi.getRefReturn().substituteVariable(Keys.WILDCARD, returnVarName)
221+
.substituteVariable(Keys.THIS, returnVarName);
222+
223+
rtc.getContext().addVarToContext(returnVarName, method.getType(), cretRef, ret);
224+
rtc.checkSMT(cexpectedType, ret, fi.getMessage());
225+
rtc.getContext().newRefinementToVariableInContext(returnVarName, cexpectedType);
226+
220227
}
221228

222229
// ############################### VISIT INVOCATION
223-
// ################################3
230+
// ################################
224231

225232
public <R> void getInvocationRefinements(CtInvocation<R> invocation) throws LJError {
226233
CtExecutable<?> method = invocation.getExecutable().getDeclaration();
@@ -253,37 +260,35 @@ private void searchMethodInLibrary(CtExecutableReference<?> ctr, CtInvocation<?>
253260

254261
String name = ctr.getSimpleName(); // missing
255262
List<CtTypeReference<?>> paramTypes = ctr.getParameters();
256-
String qualifiedSignature = null;
257-
if (ctype != null) {
258-
qualifiedSignature = String.format("%s.%s", ctype, ctr.getSignature());
259-
RefinedFunction f = rtc.getContext().getFunction(qualifiedSignature, ctype, paramTypes);
260-
if (f != null) {
261-
checkInvocationRefinements(invocation, invocation.getArguments(), invocation.getTarget(),
262-
qualifiedSignature, ctype, paramTypes);
263-
return;
264-
}
265-
}
266-
String signature = ctr.getSignature();
267-
RefinedFunction f = rtc.getContext().getFunction(signature, ctype, paramTypes);
268-
if (f != null) {
269-
checkInvocationRefinements(invocation, invocation.getArguments(), invocation.getTarget(), signature, ctype,
270-
paramTypes);
263+
264+
// Try each candidate key in order; a null key (when ctype is unknown) is skipped.
265+
String qualifiedSignature = (ctype != null) ? String.format("%s.%s", ctype, ctr.getSignature()) : null;
266+
String completeName = (ctype != null) ? String.format("%s.%s", ctype, name) : null;
267+
268+
if (tryRefinements(invocation, qualifiedSignature, ctype, paramTypes)
269+
|| tryRefinements(invocation, ctr.getSignature(), ctype, paramTypes)
270+
|| tryRefinements(invocation, name, ctype, paramTypes)) {
271271
return;
272272
}
273-
f = rtc.getContext().getFunction(name, ctype, paramTypes);
274-
if (f != null) { // inside rtc.context
275-
checkInvocationRefinements(invocation, invocation.getArguments(), invocation.getTarget(), name, ctype,
276-
paramTypes);
277-
return;
273+
tryRefinements(invocation, completeName, ctype, paramTypes);
274+
}
275+
276+
/**
277+
* Look up {@code key} in the context and, if a refined function is found, check the invocation against it. Returns
278+
* whether a match was found. A {@code null} key is treated as no match.
279+
*/
280+
private boolean tryRefinements(CtInvocation<?> invocation, String key, String ctype,
281+
List<CtTypeReference<?>> paramTypes) throws LJError {
282+
if (key == null) {
283+
return false;
278284
}
279-
if (qualifiedSignature != null) {
280-
String completeName = String.format("%s.%s", ctype, name);
281-
f = rtc.getContext().getFunction(completeName, ctype, paramTypes);
282-
if (f != null) {
283-
checkInvocationRefinements(invocation, invocation.getArguments(), invocation.getTarget(), completeName,
284-
ctype, paramTypes);
285-
}
285+
RefinedFunction f = rtc.getContext().getFunction(key, ctype, paramTypes);
286+
if (f == null) {
287+
return false;
286288
}
289+
checkInvocationRefinements(invocation, invocation.getArguments(), invocation.getTarget(), key, ctype,
290+
paramTypes);
291+
return true;
287292
}
288293

289294
private Map<String, String> checkInvocationRefinements(CtElement invocation, List<CtExpression<?>> arguments,
@@ -297,15 +302,7 @@ private Map<String, String> checkInvocationRefinements(CtElement invocation, Lis
297302
return new HashMap<>();
298303
Map<String, String> map = mapInvocation(arguments, f);
299304

300-
// Stable return-value name so `_`/`return` in @StateRefinement to= matches the post-call VariableInstance.
301-
String returnViName = null;
302-
CtTypeReference<?> retType = f.getType();
303-
if (retType != null && !"void".equals(retType.toString())) {
304-
returnViName = String.format(Formats.INSTANCE, f.getName(), rtc.getContext().getCounter());
305-
invocation.putMetadata(Keys.RETURN_VAR_NAME, returnViName);
306-
if (f.allRefinementsTrue())
307-
rtc.getContext().addInstanceToContext(returnViName, retType, new Predicate(), invocation);
308-
}
305+
String returnViName = prepareReturnInstance(invocation, f);
309306

310307
if (target != null)
311308
AuxStateHandler.prepareInvocationTarget(rtc, target, invocation);
@@ -328,35 +325,59 @@ private Map<String, String> checkInvocationRefinements(CtElement invocation, Lis
328325
AuxStateHandler.checkTargetChanges(rtc, f, target, map, invocation);
329326

330327
// -- Part 2: Apply changes
331-
// applyRefinementsToArguments(element, arguments, f, map);
332-
Predicate methodRef = f.getRefReturn();
328+
applyReturnRefinement(invocation, f, map, returnViName);
329+
return map;
330+
}
333331

334-
if (methodRef != null) {
335-
boolean equalsThis = methodRef.toString().equals("_ == this"); // TODO change for better
336-
List<String> vars = methodRef.getVariableNames();
337-
for (String s : vars)
338-
if (map.containsKey(s))
339-
methodRef = methodRef.substituteVariable(s, map.get(s));
332+
/**
333+
* Computes a stable return-value instance name so {@code _}/{@code return} in a {@code @StateRefinement to=} clause
334+
* matches the post-call VariableInstance. Returns {@code null} for void methods. When the function has no
335+
* refinements to check, the (empty) instance is registered eagerly.
336+
*/
337+
private String prepareReturnInstance(CtElement invocation, RefinedFunction f) {
338+
CtTypeReference<?> retType = f.getType();
339+
if (retType == null || "void".equals(retType.toString()))
340+
return null;
341+
String returnViName = String.format(Formats.INSTANCE, f.getName(), rtc.getContext().getCounter());
342+
invocation.putMetadata(Keys.RETURN_VAR_NAME, returnViName);
343+
if (f.allRefinementsTrue())
344+
rtc.getContext().addInstanceToContext(returnViName, retType, new Predicate(), invocation);
345+
return returnViName;
346+
}
340347

341-
String varName = null;
342-
if (invocation.getMetadata(Keys.TARGET) != null) {
343-
VariableInstance vi = (VariableInstance) invocation.getMetadata(Keys.TARGET);
344-
methodRef = methodRef.substituteVariable(Keys.THIS, vi.getName());
345-
Variable v = rtc.getContext().getVariableFromInstance(vi);
346-
if (v != null)
347-
varName = v.getName();
348-
}
348+
/**
349+
* Part 2 of an invocation check: applies the function's return refinement to the context, substituting argument and
350+
* target variables and registering the resulting return-value instance.
351+
*/
352+
private void applyReturnRefinement(CtElement invocation, RefinedFunction f, Map<String, String> map,
353+
String returnViName) {
354+
Predicate methodRef = f.getRefReturn();
355+
if (methodRef == null)
356+
return;
349357

350-
String viName = returnViName != null ? returnViName
351-
: String.format(Formats.INSTANCE, f.getName(), rtc.getContext().getCounter());
352-
VariableInstance vi = (VariableInstance) rtc.getContext().addInstanceToContext(viName, f.getType(),
353-
methodRef.substituteVariable(Keys.WILDCARD, viName), invocation); // TODO REVIEW!!
354-
if (varName != null && f.hasStateChange() && equalsThis)
355-
rtc.getContext().addRefinementInstanceToVariable(varName, viName);
356-
invocation.putMetadata(Keys.TARGET, vi);
357-
invocation.putMetadata(Keys.REFINEMENT, methodRef);
358+
boolean equalsThis = methodRef.toString().equals("_ == this"); // TODO change for better
359+
List<String> vars = methodRef.getVariableNames();
360+
for (String s : vars)
361+
if (map.containsKey(s))
362+
methodRef = methodRef.substituteVariable(s, map.get(s));
363+
364+
String varName = null;
365+
if (invocation.getMetadata(Keys.TARGET) != null) {
366+
VariableInstance vi = (VariableInstance) invocation.getMetadata(Keys.TARGET);
367+
methodRef = methodRef.substituteVariable(Keys.THIS, vi.getName());
368+
Variable v = rtc.getContext().getVariableFromInstance(vi);
369+
if (v != null)
370+
varName = v.getName();
358371
}
359-
return map;
372+
373+
String viName = returnViName != null ? returnViName
374+
: String.format(Formats.INSTANCE, f.getName(), rtc.getContext().getCounter());
375+
VariableInstance vi = (VariableInstance) rtc.getContext().addInstanceToContext(viName, f.getType(),
376+
methodRef.substituteVariable(Keys.WILDCARD, viName), invocation); // TODO REVIEW!!
377+
if (varName != null && f.hasStateChange() && equalsThis)
378+
rtc.getContext().addRefinementInstanceToVariable(varName, viName);
379+
invocation.putMetadata(Keys.TARGET, vi);
380+
invocation.putMetadata(Keys.REFINEMENT, methodRef);
360381
}
361382

362383
private Map<String, String> mapInvocation(List<CtExpression<?>> arguments, RefinedFunction f) {
@@ -410,37 +431,8 @@ private void checkParameters(CtElement invocation, List<CtExpression<?>> argumen
410431
}
411432
}
412433

413-
// IN CONSTRUCTION _ NOT USED
414-
@SuppressWarnings("unused")
415-
private void applyRefinementsToArguments(CtElement element, List<CtExpression<?>> arguments, RefinedFunction f,
416-
Map<String, String> map) {
417-
Context context = rtc.getContext();
418-
List<Variable> functionParams = f.getArguments();
419-
420-
for (int i = 0; i < arguments.size(); i++) {
421-
Variable fArg = functionParams.get(i);
422-
Predicate inferredRefinement = fArg.getRefinement();
423-
424-
CtExpression<?> e = arguments.get(i);
425-
if (e instanceof CtVariableRead<?> v) {
426-
String varName = v.getVariable().getSimpleName(); // TODO CHANGE
427-
RefinedVariable rv = context.getVariableByName(varName);
428-
String instanceName = String.format(Formats.INSTANCE, varName, context.getCounter());
429-
430-
inferredRefinement = inferredRefinement.substituteVariable(fArg.getName(), instanceName);
431-
context.addInstanceToContext(instanceName, rv.getType(), inferredRefinement, element);
432-
context.addRefinementInstanceToVariable(varName, instanceName);
433-
} // TODO else's?
434-
}
435-
}
436-
437434
public void loadFunctionInfo(CtExecutable<?> method) {
438-
String className = null;
439-
if (method.getParent() instanceof CtClass) {
440-
className = ((CtClass<?>) method.getParent()).getQualifiedName();
441-
} else if (method.getParent() instanceof CtInterface<?>) {
442-
className = ((CtInterface<?>) method.getParent()).getQualifiedName();
443-
}
435+
String className = parentQualifiedName(method);
444436
if (className != null) {
445437
List<CtTypeReference<?>> paramTypes = new ArrayList<>();
446438
for (CtParameter<?> p : method.getParameters())

0 commit comments

Comments
 (0)