Verifier crashes on a comparison or other binary operator whose operand types cannot be resolved (classes not on the classpath)

崩溃在 OperationsChecker.getBinaryOpRefinements（第 77 行）中抛出，由 RefinementTypeChecker.visitCtBinaryOperator（第 383 行）调用到达。先阅读该方法如何使用运算符的类型，然后在 classpath 中不包含 org.example.missing 的情况下运行最小的 Repro 类。当它报告 Correct! Passed Verification. 且伴随编译警告、没有 NullPointerException 时，即完成。

Impact: verification stops with an internal error on any file that compares, adds or otherwise combines values of a type LiquidJava cannot resolve: 25 of the 53 real-world files below.

Description

When an operand's type comes from a class that is not on the classpath (a class of the same project, or of a dependency), Spoon gives the binary operator no type, and OperationsChecker.getBinaryOpRefinements calls getQualifiedName() on it. Same null type as #344 (a var local), but a different cause: here the types are simply not available, which is the usual case when one file of a project is verified. A binary operator with an unknown type could be treated as having no refinement instead of stopping verification.

Minimal reproducer (org.example.missing is not on the classpath)

import org.example.missing.Item;

public class Repro {
    static boolean same(Item a, Item b) {
        if (a.id() == b.id()) {
            return true;
        }
        return false;
    }
}

Expected

Correct! Passed Verification. (with the usual "Java compilation encountered issues" warning): the comparison carries no refinement.

Actual

Exception in thread "main" java.lang.RuntimeException: 
Error while checking CtMethodImpl
  on same(Item a, Item b) { 
  at Repro.java:4
  with 
Error while checking CtBlockImpl
  on { 
  at Repro.java:4
  with 
Error while checking CtIfImpl
  on if (a.id() == b.id()) { 
  at Repro.java:5
  with Cannot invoke "spoon.reflect.reference.CtTypeReference.getQualifiedName()" because the return value of "spoon.reflect.code.CtBinaryOperator.getType()" 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.code.CtBinaryOperator.getType()" is null
	at liquidjava.processor.refinement_checker.general_checkers.OperationsChecker.getBinaryOpRefinements(OperationsChecker.java:77)
	at liquidjava.processor.refinement_checker.RefinementTypeChecker.visitCtBinaryOperator(RefinementTypeChecker.java:383)
	at liquidjava.processor.refinement_checker.RefinementTypeChecker.getExpressionRefinements(RefinementTypeChecker.java:729)

Reproduced on main at dcfc4eb2 (liquidjava-verifier 0.0.35).

Real-world files that hit it (the construct where verification stops)

• if (itemParser != null) { — pacsbrasil/dcm4che2 (file)
• if (p.getValue() == id) { — hashsploit/clank (file)
• if (!someHandlerDefined || Interrupts.isInterruptsDisabled()) { — EmulatorArchive/jpcsp (file)
• StringUtils.leftPad(this.mdfe.getInfo().getIdentificacao().getCodigoUF().getCodigoIbge(), — wmixvideo/nfe (file)
• if (itemParser != null) { — fenyuzhe/protoss-toolkit (file)
• if (Build.VERSION.SDK_INT >= 33) { — Dathaze20/Music-Player-Tagger (file)
• "Configuration is not an SQL config:" — wso2/product-integrator-mi (file)
• if (model == null) { — eclipse-pde/eclipse.pde (file)
• if (factory == null) — cytoscape/cytoscape-impl (file)
• i < embedding.length(); i++ ) { — darrenfoong/depnn (file)
• if (timeoutDiagnostics != null) { — 0Lilhate/stand-test-framework (file)
• if (admissionsRouter == null) { — Hellblazer/Delos (file)
• if (exInterceptor != null) { — JIA-JA/111502-case (file)
• if (theFolder == null) { — codelerity/netbeans-releases (file)
• if (commandInstance instanceof Module) return (Module) commandInstance; — elect86/scijava-common (file)
• persona.getContextDefinition() == null — open-metadata/OpenMetadata (file)
• if (mapping != null) { — sabineheider/eclipselink.runtime (file)
• svnOperationFactory == null; — scm-manager/svnkit (file)
• Version.getFrameworkTitle() — storset/vtk.test (file)
• if (table == null) — tejeswarp/tungsten-replicator (file)
• if (serializers == null) { — valdecimartins/satellite-spacewalkproject-spacewalk (file)
• Environment.getExternalStorageDirectory().getPath() + "/secrets"; — rogerta/secrets-for-android (file)
• if (m_serviceInstance != null) { — OpenNMS/opennms (file)
• (in.readableBytes() > 0) { — credentials/irma_assurer (file)
• m.mes.getString("Generator.53") — gil612/Softwaretechnik_2019 (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. Related: #389, #390, and #344 (the same null type from a var local).