Impact: verification stops with an internal error: 5 of the 53 real-world files below.
Description
Reading a field whose declaring type is unknown (an enum constant in a case label, a field generated by Lombok such as log, an array's .length on a value of an unresolved type): CtFieldReference.getDeclaringType() is null and Utils.qualifyFieldName calls getQualifiedName() on it.
Minimal reproducer (org.example.missing is not on the classpath)
import org.example.missing.Mode;
public class Repro {
static int weight(Mode mode) {
switch (mode) {
case STATEFUL:
return 2;
default:
return 1;
}
}
}Expected
Correct! Passed Verification. (with the "Java compilation encountered issues" warning).
Actual
Exception in thread "main" java.lang.RuntimeException:
Error while checking CtMethodImpl
on weight(Mode mode) {
at Repro.java:4
with
Error while checking CtBlockImpl
on {
at Repro.java:4
with
Error while checking CtSwitchImpl
on switch (mode) {
at Repro.java:5
with
Error while checking CtCaseImpl
on case STATEFUL:
at Repro.java:6
with
Error while checking CtFieldReadImpl
on STATEFUL:
at Repro.java:6
with Cannot invoke "spoon.reflect.reference.CtTypeReference.getQualifiedName()" because the return value of "spoon.reflect.reference.CtFieldReference.getDeclaringType()" is null
at liquidjava.processor.refinement_checker.TypeChecker.scan(TypeChecker.java:80)
at spoon.reflect.visitor.CtScanner.scan(CtScanner.java:189)
at spoon.reflect.visitor.CtScanner.scan(CtScanner.java:154)
at spoon.reflect.visitor.CtScanner.visitCtClass(CtScanner.java:363)
at liquidjava.processor.refinement_checker.RefinementTypeChecker.visitCtClass(RefinementTypeChecker.java:97)
at spoon.support.reflect.declaration.CtClassImpl.accept(CtClassImpl.java:63)
at liquidjava.processor.RefinementProcessor.lambda$processPackage$3(RefinementProcessor.java:51)
at java.base/java.lang.Iterable.forEach(Iterable.java:75)
at liquidjava.processor.RefinementProcessor.processPackage(RefinementProcessor.java:50)
at liquidjava.processor.RefinementProcessor.process(RefinementProcessor.java:35)
at liquidjava.processor.RefinementProcessor.process(RefinementProcessor.java:15)
at spoon.support.visitor.ProcessingVisitor.scan(ProcessingVisitor.java:72)
at spoon.support.QueueProcessingManager.process(QueueProcessingManager.java:118)
at spoon.support.QueueProcessingManager.process(QueueProcessingManager.java:132)
at liquidjava.api.CommandLineLauncher.launch(CommandLineLauncher.java:92)
at liquidjava.api.CommandLineLauncher.main(CommandLineLauncher.java:41)
...
Caused by: java.lang.NullPointerException: Cannot invoke "spoon.reflect.reference.CtTypeReference.getQualifiedName()" because the return value of "spoon.reflect.reference.CtFieldReference.getDeclaringType()" is null
at liquidjava.utils.Utils.qualifyFieldName(Utils.java:56)
at liquidjava.processor.refinement_checker.RefinementTypeChecker.visitCtFieldRead(RefinementTypeChecker.java:325)
at liquidjava.processor.refinement_checker.TypeChecker.scan(TypeChecker.java:69)
Reproduced on main at dcfc4eb (liquidjava-verifier 0.0.35).
Real-world files that hit it
log.error("get host name error:{}", e.getMessage()); — apache/ozhera (file)UNKNOWN_CASING; — apache/derby (file)(p.define().length > 0 || p.include().length > 0 || p.cinclude().length > 0 || — larael/javacpp (file)STATEFUL: — stratwine/openejb (file)(config.httpAdminPassword.length() < MIN_ADMIN_PASSWORD_LENGTH) { — spazio17/muralis (file)
Context
Found while running LiquidJava on the original repository files of 53 real-world typestate and refinement bugs (the same files as our study exercises, before simplification). Each file is verified on its own, as a user would on one file of a project, so the project's other classes and its dependencies are not on the classpath. On main this crash and the two related ones (#388 binary operator, #389 unary operator, #390 field read) stop verification in 33 of the 53 files.