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

Le plantage est levé dans OperationsChecker.getBinaryOpRefinements (ligne 77), atteint depuis RefinementTypeChecker.visitCtBinaryOperator (ligne 383). Commence par lire comment cette méthode utilise le type de l'opérateur, puis exécute la classe minimale Repro avec org.example.missing absent du classpath. C'est terminé lorsqu'elle affiche Correct! Passed Verification. avec l'avertissement de compilation et sans 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).