Verifier crashes on an array read whose element type cannot be resolved (classes not on the classpath) #425

Impact: verification stops with an internal error on an array read whose element type cannot be resolved: 8 of the 74 real-world files below (6 projects).

Description

Reading an element of an array whose element type comes from a class that is not on the classpath (cookies[i] with Cookie[] cookies): RefinementTypeChecker.visitCtArrayRead (RefinementTypeChecker.java:272) adds the element with a null type, and Context.addVarToContext calls getSuperclass() on it (Context.java:193). The same null type in Context as #396 (there from a lambda parameter) and #389, reached from a different construct. An element of unknown type could be added without supertypes.

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

import com.example.missing.Cookie;

public class Repro {
    void createAll(Cookie[] cookies) {
        for (int i = 0; i < cookies.length; i++) {
            cookies[i].create();
        }
    }
}

Expected

Correct! Passed Verification. (with the usual "Java compilation encountered issues" warning).

Actual

Exception in thread "main" java.lang.RuntimeException: 
Error while checking CtMethodImpl
  on createAll(Cookie[] cookies) { 
  at /tmp/claude-1000/-home-cvgamboa-git/4a721752-8c76-4314-99f8-baeafc8d523a/scratchpad/issues/arrread/Repro.java:4
  with 
Error while checking CtBlockImpl
  on { 
  at /tmp/claude-1000/-home-cvgamboa-git/4a721752-8c76-4314-99f8-baeafc8d523a/scratchpad/issues/arrread/Repro.java:4
  with 
Error while checking CtForImpl
  on for (int i = 0; i < cookies.length; i++) { 
  at /tmp/claude-1000/-home-cvgamboa-git/4a721752-8c76-4314-99f8-baeafc8d523a/scratchpad/issues/arrread/Repro.java:5
...
Caused by: java.lang.NullPointerException: Cannot invoke "spoon.reflect.reference.CtTypeReference.getSuperclass()" because "type" is null
	at liquidjava.processor.context.Context.addVarToContext(Context.java:193)
	at liquidjava.processor.refinement_checker.RefinementTypeChecker.visitCtArrayRead(RefinementTypeChecker.java:272)

Reproduced on main at 0d489e1 (liquidjava-verifier 0.0.36).

Real-world files that hit it

• arr[i].instanceCreate(): codelerity/netbeans-releases (file)
• statementContexts[0]: apache/derby (file)
• svnProperties[0]: scm-manager/svnkit (file)
• this.errorHandlers[j]: storset/vtk.test (file)
• perfEntityMetricBases[i]: OpenNMS/opennms (file), before and after its fix
• this.getConfig().createConnection()[0]: wso2/product-integrator-mi (file), before and after its fix

Context

Found while running LiquidJava on the original repository files of 53 real-world typestate and refinement bugs (74 files with the fixed versions), each verified on its own as in #396. Related: #388, #389, #390, #396.