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

A falha é lançada em OperationsChecker.getBinaryOpRefinements (linha 77), alcançada a partir de RefinementTypeChecker.visitCtBinaryOperator (linha 383). Comece lendo como esse método usa o tipo do operador e, em seguida, execute a classe mínima Repro com org.example.missing ausente do classpath. Está concluído quando ela informa Correct! Passed Verification. com o aviso de compilação e sem 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).