Impact: verification stops with an internal error: 3 of the 53 real-world files below.
Description
!x.m() where x's class is not on the classpath: OperationsChecker.getUnaryOpRefinements adds the operand to the context, and Context.addInstanceVariable calls getSuperclass() on its type, which is null.
Minimal reproducer (org.example.missing is not on the classpath)
import org.example.missing.Settings;
public class Repro {
static void start(Settings settings) {
if (!settings.enabled()) {
return;
}
}
}Expected
Correct! Passed Verification. (with the "Java compilation encountered issues" warning).
Actual
Exception in thread "main" java.lang.RuntimeException:
Error while checking CtMethodImpl
on start(Settings settings) {
at Repro.java:4
with
Error while checking CtBlockImpl
on {
at Repro.java:4
with
Error while checking CtIfImpl
on if (!settings.enabled()) {
at Repro.java:5
with Cannot invoke "spoon.reflect.reference.CtTypeReference.getSuperclass()" because "type" 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.getSuperclass()" because "type" is null
at liquidjava.processor.context.Context.addInstanceVariable(Context.java:267)
at liquidjava.processor.context.Context.addInstanceToContext(Context.java:164)
at liquidjava.processor.refinement_checker.general_checkers.OperationsChecker.getUnaryOpRefinements(OperationsChecker.java:179)
Reproduced on main at dcfc4eb (liquidjava-verifier 0.0.35).
Real-world files that hit it
if (!appProperties.simulator().enabled()) { — skyleedevzero86/carebridge-platform (file)if (!Game.isInNoGUIMode()) { — gurkenlabs/litiengine (file)(!context.isExportedEquipment(identifiable) || extensions.isEmpty()) { — stvzhou/powsybl-core (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.