Decide how to deal with JVM class initialization

[brianhuffman]

The translation of JVM to crucible in the crucible-jvm package includes global state for keeping track of initialization status for each class, and many operations will conditionally call the static initializer method for a class (and its superclasses) if a class has not yet been initialized. However, we currently have no way to say anything about JVM class initialization status in saw-script.

At the moment I'm working on adding a jvm_static_field_is declaration to address #908. However, I'm running into a problem when I try to verify a method that reads from these static fields. The precondition section says that the static fields for class C should initially contain symbolic values. But then when I start symbolic simulation, the crucible-jvm class initialization status table says that class C is still uninitialized. So before the getstatic instruction is executed, it dutifully runs the static initializer method for class C, which overwrites all the static fields of C with 0. Then the method's return value is based on reading a 0 instead of the symbolic input I declared in the spec.

One could imagine having a SAW command declaring the precondition that a specific class must be initialized. However, this seems like it would be burdensome to use in some cases, because you might be forced to prove a whole collection of overrides for one method, each with a different combination of initialized classes in the preconditions. Most of the time you don't really care about the initialization status of most classes before you start, and the result and/or effects of a method call don't depend on the initialization status either. It would be nice if we could just prove a single override that would be applicable regardless of class initialization status.

[brianhuffman]

The old jss-based java verification interface provided the following setup command:

    java_requires_class : String -> JavaSetup ()

Declare that the given method can only be executed if the given
class has already been initialized.

We could probably use something similar for crucible-jvm verification.

[sauclovian-g]

Initialization is great, but it's the wrong thing to do. When symbolically executing methods from a class, you aren't intending to only cover the cases where it was just initialized. If you do, you can miss stuff. (hence the unsoundness tag)

The right thing to do is for initialization to be an override spec that establishes the class's invariants, so that the resulting state is a general one that nonetheless respects whatever invariants the initialization is supposed to establish. (Which is also in turn sometimes nonempty, so skipping initialization and assigning a purely symbolic state is also wrong.)

As noted, this is the same as #357 (which is the same issue for C++ global initialization), but it's a general problem and the same considerations also apply to initialization of class instances and other state tracking.

See also #2053.