JVM overrides that don't specify final values can lead to unsoundness

[brianhuffman]

Currently we can prove an override for a JVM method with crucible_jvm_verify that specifies no final value for a field of an allocated object. The verification will still succeed if the method modifies such a field, but then executing the override will leave that field unmodified. This can lead to unsoundness.

To fix the problem, we should perform an invalidation pass and invalidate any allocated fields that do not have final values specified, as was implemented for LLVM in #549.

[brianhuffman]

The plan is to have an explicit declaration to say that a location could be modified in an unspecified way, much like the java_modifies declaration in the old java verification system. If there is no final value specified, and also no jvm_modifies declaration, then the default should be that the value is asserted to stay the same.

[brianhuffman]

My latest thoughts about jvm_modifies: It seems like we would need more than one variant of this declaration. We would need jvm_modifies_field for instance fields, jvm_modifies_elem for array elements, and jvm_modifies_static_field for static fields of classes. (Basically we would need a separate command for each kind of points-to declaration we have.)

A simpler API would be to just add a new JVMValue constructor denoting an "unspecified" value, and then just use that with the already-existing JVM points-to commands. I think this would make the user-facing API both simpler and easier to understand.

To summarize, we want to just add one new saw-script primitive jvm_unspecified : JVMValue, and then we can start putting declarations like these in our setup blocks:

jvm_field_is ref "val" jvm_unspecified
jvm_elem_is ref 3 jvm_unspecified
jvm_static_field_is "C.fname" jvm_unspecified

Even if we do decide to offer 3 varieties of jvm_modifies declarations, it's probably best to implement them all in the way described above.

[atomb]

I think I remember talking about this in person, but not what conclusion we came to: how is jvm_unspecified in this proposal different from the result of jvm_fresh_var?

[brianhuffman]

They are different. In the post-state section, a declaration of a field or array element as jvm_unspecified means that when the override is executed, that field or array element will be reset to an uninitialized state, so that any subsequent reads will simply fail.

On the other hand, if you want to have a value that can be subsequently read, but just with an unconstrained value, that's when you would use jvm_fresh_var in the post-state section.

By the way, I have some of this implemented already in the bh-jvm branch, and I actually decided to do the three new points-to variants instead of adding jvm_unspecified as a new JVMValue constructor. For dumb reasons related to abstractions in the saw/crucible code, I can't add a new constructor only to the JVMValue type without also touching a lot of LLVM-related code; adding new kinds of points-to declarations was much more straightforward.

[brianhuffman]

Fixed in #1290.