-
Notifications
You must be signed in to change notification settings - Fork 62
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Allow reading and writing structured objects in Java analysis #158
Comments
The old Java stuff is obsolete, but we should make sure that the new crucible/jvm stuff supports the same feature. |
For crucible/jvm, issue #422 is specifically about reading and writing arrays. We'll have to think about whether it makes sense to read and write objects with named fields. |
One of the tricky things about mapping between JVM object field names and Cryptol record fields is that JVM field names are not just identified by name; the class name and type are also used to identify a field of an object. The class name of a field might be the class of the object, or else it could be a superclass. It's not obvious how users would typically want those fields to be organized. Should they be one flat record? But that doesn't work if some field names shadow the names from a superclass. We could have a record field called Basically, I'm thinking that this is not something we want to implement. The saw-script commands, as they exist now, let you define your own object-specific wrapper functions for the |
Update to follow changes in What4
This adapts cryptol-saw-core to GaloisInc/cryptol#1066. (Note: saw-core PR #158 was intended to adapt to the same cryptol PR, but missing translations for the new cryptol primitives caused the cryptol-saw-core test suite to fail. This PR fixes the test suite failure.)
Right now, arrays of scalars can be read and written from the Java heap as monolithic entities. Similarly, it would be possible in principle to specify or extract the value of an object as a SAWCore record, but that's not currently implemented.
The text was updated successfully, but these errors were encountered: