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

Der Absturz wird in OperationsChecker.getBinaryOpRefinements (Zeile 77) ausgelöst, erreicht von RefinementTypeChecker.visitCtBinaryOperator (Zeile 383). Beginne damit zu lesen, wie diese Methode den Typ des Operators verwendet, und führe dann die minimale Repro-Klasse aus, während org.example.missing nicht im Classpath liegt. Fertig ist es, wenn Correct! Passed Verification. mit der Compilerwarnung und ohne NullPointerException gemeldet wird.

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).