Refactor String related classes and methods to comply with JEP 254 #133
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
String#value field should be set as a byte[] instead of char[], when constructing ElementInfo(s) for String references in gov.nasa.jpf.vm.GenericHeap.
This deprecates ElementInfo.getStringChars. Because String#value field should now return a byte array instead of a char array. ElementInfo.getStringBytes should be used instead.
Most methods in JPF_java_lang_String fail as the `value` field have changed from char[] to a byte[] since JEP 254. Instead of retrieving the value field, and performing operations on that value field to return a result (which is now complex as the value field now being a byte[] and and having a coder which specifies the different encoding), we turn JPF String object into a VM String object using MJIEnv.getStringObject and then delegates the method call to that VM object.
…sString String#value field can only be cast to ByteArrayFields as the value field of String is a byte[] instead of char[]
Current implementations of JPF_java_lang_StringBuffer, and JPF_java_lang_StringBuilder is highly obsolete as the value field now being a byte[] instead of char[], and having a coder which specifies the encoding. Also we are not able to use StringUTF16, StringLatin1 helper classes to help us with encoding and decoding since they are being package-private. Neither StringBuffer nor StringBuilder have any native methods. So it should be safe to remove these two.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This fixes the issues #127 and #132 which is about CastException that is being thrown due to String#value field returning a char array and sometimes a byte array. String data is always stored as byte[] array in the heap, hence it should always return a byte array. So the problem is with the way how JPF's heap implementation create String elements.
This sets
String#valuefield as a byte[] instead of char[], when constructing ElementInfo(s) for String references in gov.nasa.jpf.vm.GenericHeap.Deprecates ElementInfo.getStringChars and introduces the replacement method ElementInfo.getStringBytes
Fixes the occurrences where value field is being cast to a CharArrayFields
Delete JPF_java_lang_StringBuffer and JPF_java_lang_StringBuilder