crucible-jvm: Add permission bit for writability to each instance field and array.

[brianhuffman]

The field permission bit is asserted on every putfield instruction. The array permission bit is asserted on every astore instruction.

This PR builds on top of #733. It will be used to address GaloisInc/saw-script#900.

[robdockins]

Looks OK to me. Two questions though:

1. Why did you decide to use a separate StringMap for object field permissions instead of adding a boolean flag to the field value map?

2. It seems like objects always default to writable, which makes sense for crux-style simulation. How does SAW twiddle those bits?

[brianhuffman]

1. Why did you decide to use a separate StringMap for object field permissions instead of adding a boolean flag to the field value map?

That choice is mainly because the object fields are often updated during simulation while the permission bits never are. By keeping them separate, we can be sure that the values in the permission map will stay concrete, even in the presence of conditional updates to the value fields. I mentioned some of this in response to some comments on #733.

2. It seems like objects always default to writable, which makes sense for crux-style simulation. How does SAW twiddle those bits?

SAW sets those bits when an object is created (while executing the pre-state section of a method spec during verification) and then never changes them afterward. Fields are only set to writable if there is a jvm_modifies_field or jvm_field_is declaration in the post-state section; otherwise we interpret the spec as asserting that the field does not change, and so we set the field to read-only.