Allow use of plain field names with jvm_field_is

[brianhuffman]

Currently when writing jvm specs, jvm_field_is declarations must be used with a fully-qualified field name that includes the class name. Here's an example setup block from ecdsa-crucible.saw:

  do {
    this <- jvm_alloc_object "com.galois.ecc.P384ECC64";
    ph <- jvm_alloc_array 12 java_int;
    jvm_field_is this "com/galois/ecc/ECCProvider.h" ph;
    ...

In order to determine the right fully-qualified name for field h, the user has to basically perform a full field resolution procedure: No field h is declared in class P384ECC64, so check the superclass NIST64. There's no field h in NIST64 either, so check its superclass ECCProvider. Finally, we find that ECCProvider does declare a field h, so that's the qualified name we use.

Instead of making the user do this, saw should do it automatically. The user should be able to write jvm_field_is this "h" ph. Then saw should look up the class of the this reference, and resolve the field name h by checking the superclasses in order until a match is found.

Even so, we probably want to continue to allow users to optionally specify fully-qualified field names that include a classname. This is occasionally necessary in the case where a subclass declares a field that shadows a similarly-named field in a superclass; in such cases the unqualified name would always default to the field of the subclass.