ArrayIndexOutOfBoundsException when using JPF on Scala

[liuyic00]

Hi, I'm trying to use jpf-core on Scala code.
However, I encounter a java.lang.ArrayIndexOutOfBoundsException as shown below.

java.lang.ArrayIndexOutOfBoundsException

java.lang.ArrayIndexOutOfBoundsException: Index 1536 out of bounds for length 499 at gov.nasa.jpf.jvm.ClassFile.utf8At(ClassFile.java:246) at gov.nasa.jpf.jvm.ClassFile.methodTypeDescriptorAt(ClassFile.java:325) at gov.nasa.jpf.jvm.JVMClassInfo$Initializer.setBootstrapMethod(JVMClassInfo.java:168) at gov.nasa.jpf.jvm.ClassFile.setBootstrapMethod(ClassFile.java:694) at gov.nasa.jpf.jvm.ClassFile.parseBootstrapMethodAttr(ClassFile.java:1528) at gov.nasa.jpf.jvm.JVMClassInfo$Initializer.setClassAttribute(JVMClassInfo.java:112) at gov.nasa.jpf.jvm.ClassFile.setClassAttribute(ClassFile.java:671) at gov.nasa.jpf.jvm.ClassFile.parseClassAttributes(ClassFile.java:1411) at gov.nasa.jpf.jvm.ClassFile.parse(ClassFile.java:980) at gov.nasa.jpf.jvm.JVMClassInfo$Initializer.(JVMClassInfo.java:80) at gov.nasa.jpf.jvm.JVMClassInfo.(JVMClassInfo.java:771) at gov.nasa.jpf.jvm.JVMClassFileContainer$JVMClassFileMatch.createClassInfo(JVMClassFileContainer.java:59) at gov.nasa.jpf.jvm.JVMClassFileContainer$JVMClassFileMatch.createClassInfo(JVMClassFileContainer.java:34) at gov.nasa.jpf.vm.ClassLoaderInfo.getResolvedClassInfo(ClassLoaderInfo.java:356) at gov.nasa.jpf.vm.SystemClassLoaderInfo.getResolvedClassInfo(SystemClassLoaderInfo.java:148) at gov.nasa.jpf.vm.SystemClassLoaderInfo.loadClass(SystemClassLoaderInfo.java:183) at gov.nasa.jpf.vm.ClassInfo.resolveReferencedClass(ClassInfo.java:2485) at gov.nasa.jpf.vm.ClassInfo.loadInterfaces(ClassInfo.java:2437) at gov.nasa.jpf.vm.ClassInfo.resolveClass(ClassInfo.java:2454) at gov.nasa.jpf.vm.ClassInfo.resolveAndLink(ClassInfo.java:550) at gov.nasa.jpf.jvm.JVMClassInfo.(JVMClassInfo.java:773) at gov.nasa.jpf.jvm.JVMClassFileContainer$JVMClassFileMatch.createClassInfo(JVMClassFileContainer.java:59) at gov.nasa.jpf.jvm.JVMClassFileContainer$JVMClassFileMatch.createClassInfo(JVMClassFileContainer.java:34) at gov.nasa.jpf.vm.ClassLoaderInfo.getResolvedClassInfo(ClassLoaderInfo.java:356) at gov.nasa.jpf.vm.SystemClassLoaderInfo.getResolvedClassInfo(SystemClassLoaderInfo.java:148) at gov.nasa.jpf.vm.SystemClassLoaderInfo.loadClass(SystemClassLoaderInfo.java:183) at gov.nasa.jpf.vm.ClassInfo.resolveReferencedClass(ClassInfo.java:2485) at gov.nasa.jpf.vm.ClassInfo.loadSuperClass(ClassInfo.java:2423) at gov.nasa.jpf.vm.ClassInfo.resolveClass(ClassInfo.java:2451) at gov.nasa.jpf.vm.ClassInfo.resolveAndLink(ClassInfo.java:550) at gov.nasa.jpf.jvm.JVMClassInfo.(JVMClassInfo.java:773) at gov.nasa.jpf.jvm.JVMClassFileContainer$JVMClassFileMatch.createClassInfo(JVMClassFileContainer.java:59) at gov.nasa.jpf.jvm.JVMClassFileContainer$JVMClassFileMatch.createClassInfo(JVMClassFileContainer.java:34) at gov.nasa.jpf.vm.ClassLoaderInfo.getResolvedClassInfo(ClassLoaderInfo.java:356) at gov.nasa.jpf.vm.SystemClassLoaderInfo.getResolvedClassInfo(SystemClassLoaderInfo.java:148) at gov.nasa.jpf.vm.SystemClassLoaderInfo.loadClass(SystemClassLoaderInfo.java:183) at gov.nasa.jpf.vm.ClassInfo.resolveReferencedClass(ClassInfo.java:2485) at gov.nasa.jpf.vm.bytecode.StaticFieldInstruction.initialize(StaticFieldInstruction.java:43) at gov.nasa.jpf.vm.bytecode.StaticFieldInstruction.getFieldInfo(StaticFieldInstruction.java:89) at gov.nasa.jpf.jvm.bytecode.GETSTATIC.execute(GETSTATIC.java:47) at gov.nasa.jpf.vm.ThreadInfo.executeInstruction(ThreadInfo.java:1910) at gov.nasa.jpf.vm.ThreadInfo.executeTransition(ThreadInfo.java:1861) at gov.nasa.jpf.vm.SystemState.executeNextTransition(SystemState.java:765) at gov.nasa.jpf.vm.VM.forward(VM.java:1721) at gov.nasa.jpf.search.Search.forward(Search.java:937) at gov.nasa.jpf.search.DFSearch.search(DFSearch.java:79) at gov.nasa.jpf.JPF.run(JPF.java:613) at gov.nasa.jpf.JPF.start(JPF.java:189) at java.base/jdk.internal.reflect.NativeMethodAccessorImpl.invoke0(Native Method) at java.base/jdk.internal.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:62) at java.base/jdk.internal.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43) at java.base/java.lang.reflect.Method.invoke(Method.java:566) at gov.nasa.jpf.tool.Run.call(Run.java:80) at gov.nasa.jpf.tool.RunJPF.main(RunJPF.java:116)

Here is a small example that triggers this problem with the assert. Reproduce:

git clone https://github.com/liuyic00/scala-try.git
cd scala-try && git checkout jpf-issue-1
sbt assembly
java -Xmx1024m -ea -jar <path>/<to>/RunJPF.jar TestObject.jpf

I use sbt assembly to package all the dependencies of Scala into one jar, and jpf-core from the master branch.