Error "Java method is too long"

[xavierleroy]

ocamljava fails with "Error: Cannot compile goto_table_4081 (Java method is too long: 94429 bytes)"

The function in question is generated by Menhir into Coq, then extracted into OCaml, so I really have no way to make this function shorter.

I believe JVM methods are not limited to 65535 bytes in code length; only exception handlers are. See http://docs.oracle.com/javase/specs/jvms/se7/html/jvms-4.html#jvms-4.7.3 code_length is a 32-bit integer. It's only the _pc fields of exception_table entries that are 16 bits. ("A historical mistake in the design" as the spec calls it.) In the Java standard library, you'll find several static class initialization methods that are > 64K in code length.

Would it be possible for ocamljava to emit this error only if there is an exception handler that overflows the first 64K of JVM code? This would fix my problem nicely, since the big function in question has no exception handlers, like all functions generated by Coq extraction.

[xclerc]

Well, section 4.9.1 of the same document mentions the following constraint:

_The value of the codelength item must be less than 65536

It still stands for Java 1.8, but the restriction is then mentioned in section 4.7.3:

http://docs.oracle.com/javase/specs/jvms/se8/html/jvms-4.html#jvms-4.7.3

However, the fact that some methods from the standard library have a greater length is interesting. I am wondering whether loading classes from the boot class path may allow to overcome the constraint - pure speculation though.

A temporary workaround may be to compile the file(s) with -inline 0, thus avoiding any kind of inlining. However, there is little hope to go from 94429 to 65535 by just banning inlining.

In the longer term, the code generator of ocamljava (or the underlying Barista library) may provide a way to split into several methods. It is of course not obvious, has one has to pass live variables back an forth between the original method and auxiliary one(s).

[xavierleroy]

When I wrote "you'll find static class initialization methods greater than 64k in code", that was my experience a while ago when I was working on class file transformers. The typical example was some of the Unicode classes that had big tables character code -> flags. This may no longer be true. Indeed, looking at the sources of OpenJDK, the check method code size < 64K is hardwired in the class loader and has no exception, save turning off bytecode verification altogether.

Concerning inlining, I doubt it will help given that the OCaml function in question calls no other function. (It's just a table encoded as a pattern-matching.)

So, the problem remains, but it blocks the use of ocamljava as a "second-source" alternative to ocamlopt for building CompCert.