Java frontend needs to be lazier converting methods

[smowton]

At present the Java frontend walks the classpath looking for any type reference and converting any method defined on such a type. When the standard library JAR is available this results in far too much getting loaded, due to obscure references that most programs don't use-- for example, loading all of java.lang.System due to some trivial reference in a deserialization routine. To improve on this I am currently working on a simple lazy loading scheme, where all methods are initially stubbed, and then each is converted only when we find a call that may reach it (including through virtual dispatch). For example the following program currently runs out of memory when the standard library is available to parse:

import java.util.ArrayList;

public class al {

  public static void main(int args) {

    ArrayList<Integer> a = new ArrayList<Integer>();
    a.add(args);
    int i = a.get(0);

  }

}

With these changes the dependencies for simple construct, add and get should hopefully be much smaller.

Note that the types are still loaded eagerly, for simplicity-- only method bodies are populated on demand.

[kroening]

Yes, indeed! Please keep me up-to-date.

[smowton]

cristina-david@04a0ca5 and cristina-david@a9fe0bf provide a rough sketch of what we could do without much effort. They shrink the memory requirement for the basic program above to 1.2GB, which is of course still not good, but at least it's loadable (in around 2 seconds). I'll put pull request against master together once I'm happy it's reliable.

It still can't be fed into CBMC however because it does lots of unwinding and unrolling down paths that build exception error messages in the standard library. They could perhaps be blacklisted to make including rt.jar more practical.

[smowton]

This is extended a little further in my branch november_sprint_based_on_test_gen to restrict virtual function dispatch to only those types that are either parameters to, or are created within, the functions reachable from the analysis entry point.

[smowton]

Committed to master in #407