JVM class file parsing issue with BigInteger

[atomb]

Consider the following SAWScript file that is a starting point toward specifying a function from the Java BigInteger class:

enable_experimental;

let bigint_add_setup n = do {
    x <- jvm_alloc_object "java.math.BigInteger";
    y <- jvm_alloc_object "java.math.BigInteger";
    jvm_execute_func [x, y];
    z <- jvm_alloc_object "java.math.BigInteger";
    jvm_return z;
};

let main : TopLevel () = do {
    bi <- java_load_class "java.math.BigInteger";
    let name = "add(Ljava/math/BigInteger;)Ljava/math/BigInteger;";
    crucible_jvm_verify bi name [] false (bigint_add_setup 8) z3;
    print "Done.";
};

When running this under with commit fa72caf, I get the following error:

[22:47:52.803] Loading file "/Users/atomb/galois/saw-script/examples/java/java-bigint/bug.saw"
[22:47:53.059] Index 98 is not a method reference.
CallStack (from HasCallStack):
  error, called at src/Language/JVM/Parser.hs:387:12 in jvm-parser-0.3.0.0-inplace:Language.JVM.Parser

This is with saw -j /Library/Java/JavaVirtualMachines/adoptopenjdk-8.jdk/Contents/Home/jre/lib/rt.jar with the Homebrew package adoptopenjdk8 installed.

[brianhuffman]

I just installed adoptopenjdk8 and I can reproduce the problem with its version of rt.jar. But with the one I usually use with saw (/Library/Java/JavaVirtualMachines/jdk1.8.0_172.jdk/Contents/Home/jre/lib/rt.jar, which I believe is from Oracle java) the bytecode parses just fine and the example just gives a verification error.

[brianhuffman]

The function where this error message comes from is poolMethodRef from the jvm-parser package:
https://github.com/GaloisInc/jvm-parser/blob/5368a84117dc28e0002003e8d8a491dd8756b421/src/Language/JVM/Parser.hs#L380-L387

(In case the preview doesn't work, basically what this function does is look up a ConstantPoolInfo value from the constant pool, expecting a MethodRef, and raising an error otherwise.) I augmented the error message to actually show the ConstantPoolInfo that it found in case it's not a MethodRef, and here's what it says:

Index 98 is not a method reference. InterfaceMethodRef 371 372

So perhaps we can just add a case to this function to accept InterfaceMethodRef just like it accepts MethodRef? I'll try it and see what happens.

[brianhuffman]

Well, I tried exactly that, and now the example gets exactly as far as it does with the Oracle rt.jar. I guess I'll make a PR with the patch. I'm still a bit unsure why it works (or why we were able to go so long without noticing it before). Maybe it would be enlightening to unzip the rt.jar file and run javap on the class files inside to see what those constant pool entries actually refer to.

[brianhuffman]

Ok, I found the specific class file that was causing the problem: By putting a print statement on loadClassFromJar, I determined that the error occurs while parsing class java/net/SocketPermission. Here is what looks like the relevant parts of the constant pool:

   #98 = InterfaceMethodref #371.#372     // sun/security/util/RegisteredDomain.from:(Ljava/lang/String;)Ljava/util/Optional;
  #371 = Class              #482          // sun/security/util/RegisteredDomain
  #372 = NameAndType        #483:#484     // from:(Ljava/lang/String;)Ljava/util/Optional;
  #482 = Utf8               sun/security/util/RegisteredDomain
  #483 = Utf8               from
  #484 = Utf8               (Ljava/lang/String;)Ljava/util/Optional;

Disassembly shows that the match method makes a call to this methodref:

  private boolean match(java.lang.String, java.lang.String);
    descriptor: (Ljava/lang/String;Ljava/lang/String;)Z
    flags: ACC_PRIVATE
    Code:
      stack=3, locals=5, args_size=3
         0: aload_1
[...]
        57: invokestatic  #98                 // InterfaceMethod sun/security/util/RegisteredDomain.from:(Ljava/lang/String;)Ljava/util/Optional;

There's another invokestatic instruction to the same from method a few instructions later. As far as I can tell, these two calls are the only examples of invokestatic in that class that call an InterfaceMethod as opposed to an ordinary Method. Is invokestatic supposed to be used with interface methods? I'll need to look at the JVM spec to see what it says about that.

[brianhuffman]

Ah, there it is in the JVM spec: https://docs.oracle.com/javase/specs/jvms/se8/html/jvms-6.html#jvms-6.5.invokestatic

Here's what it has to say about invokestatic:

The unsigned indexbyte1 and indexbyte2 are used to construct an index into the run-time constant pool of the current class (§2.6), where the value of the index is (indexbyte1 << 8) | indexbyte2. The run-time constant pool item at that index must be a symbolic reference to a method or an interface method (§5.1), which gives the name and descriptor (§4.3.3) of the method as well as a symbolic reference to the class or interface in which the method is to be found.
(emphasis mine)

So it looks like it's indeed a bug in the jvm-parser code, which currently does not allow interface methods to be used with invokestatic. So that explains why the patch I mentioned above is necessary. I'll put this explanation in the commit log.

[brianhuffman]

According to a careful reading of the JVM spec, apparently invokevirtual requires a regular method, invokeinterface requires an interface method, and invokespecial and invokestatic can take either a regular or interface method. So the jvm-parser package gets both invokespecial and invokestatic wrong in this respect. I'll make the patch fix both of them.