JVM methods that write to static fields not mentioned in the spec can be unsound

[brianhuffman]

This is an issue that is closely related to #900. While that issue is about fields of allocated objects that don't have a final value specified, this one is instead about static fields, which are more like globals. If executing a method causes a specific static field to be written to, but the spec doesn't mention that particular static field at all, then using the resuling override in other proofs can be unsound.

Issue #900 can be addressed by doing an invalidation pass after applying the override: For every allocated object mentioned in the spec, each instance field that does not have a final value specified can be invalidated by resetting it to an uninitialized state.

However, for static fields, we can't do the same thing (or at least, we don't want to). If we apply an override for a method, we don't want to invalidate every static field for every class that wasn't mentioned in the spec, because this would destroy the usefulness of compositional proof. When we execute an override, it should leave all unmentioned static fields exactly as they were. But during verification, we also need to make sure that the method doesn't actually modify any unmentioned static fields.

One approach might be to add a proof obligation for each static field, asserting that the contents before and after are unchanged. But this wouldn't scale very well, because the number of static fields in existence might be very large, consisting of all fields from all classes that the translator knows about.

Probably what we need to do is to add an explicit write permission bit to static fields in the crucible-jvm memory model. Every putstatic instruction should check this bit and assert that it is true. When performing a verification, we can then set the permissions so that the only writable static fields are the ones explicitly mentioned in the spec. This way we can ensure that symbolic execution will never modify any parts of global state that we don't know about.