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

El fallo se lanza en OperationsChecker.getBinaryOpRefinements (línea 77), al que se llega desde RefinementTypeChecker.visitCtBinaryOperator (línea 383). Empieza leyendo cómo ese método usa el tipo del operador y luego ejecuta la clase mínima Repro con org.example.missing ausente del classpath. Está terminado cuando informa Correct! Passed Verification. con la advertencia de compilación y sin 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).