Skip to content

Commit

Permalink
Refactor JPF_java_lang_String to fix invalid casting of value field
Browse files Browse the repository at this point in the history 
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.
  • Loading branch information
@gayanW
gayanW committed Jul 31, 2018
1 parent 22e5990 commit 1ccefdf
Showing 1 changed file with 22 additions and 164 deletions.
186 changes: 22 additions & 164 deletions src/peers/gov/nasa/jpf/vm/JPF_java_lang_String.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -141,8 +141,8 @@ public int getBytes_____3B (MJIEnv env, int objRef) {

@MJI
public char charAt__I__C (MJIEnv env, int objRef, int index){
char[] data = env.getStringChars(objRef);
return data[index];
String str = env.getStringObject(objRef);
return str.charAt(index);
}


Expand All @@ -169,34 +169,10 @@ public boolean equals__Ljava_lang_Object_2__Z (MJIEnv env, int objRef, int argRe
return false;
}

Heap heap = env.getHeap();
ElementInfo s1 = heap.get(objRef);
ClassInfo ci1 = s1.getClassInfo();

ElementInfo s2 = heap.get(argRef);
ClassInfo ci2 = s2.getClassInfo();

if (!ci2.isInstanceOf(ci1)) {
return false;
}

Fields f1 = heap.get(s1.getReferenceField("value")).getFields();
Fields f2 = heap.get(s2.getReferenceField("value")).getFields();

char[] c1 = ((CharArrayFields) f1).asCharArray();
char[] c2 = ((CharArrayFields) f2).asCharArray();

if (c1.length != c2.length) {
return false;
}
String s1 = env.getStringObject(objRef);
String s2 = env.getStringObject(objRef);

for (int i = 0; i < c1.length; i++) {
if (c1[i] != c2[i]) {
return false;
}
}

return true;
return s1.equals(s2);
}

@MJI
Expand Down Expand Up @@ -272,25 +248,8 @@ public boolean startsWith__Ljava_lang_String_2__Z (MJIEnv env, int objRef, int p

@MJI
public int hashCode____I (MJIEnv env, int objref) {
ElementInfo ei = env.getElementInfo(objref);
int h = ei.getIntField("hash");

if (h == 0) {
int vref = env.getReferenceField(objref, "value");

// now get the char array data, but be aware they are stored as ints
ElementInfo eiVal = env.getElementInfo(vref);
char[] values = eiVal.asCharArray();

for (int i = 0; i < values.length; i++) {
h = 31 * h + values[i];
}

ei = ei.getModifiableInstance();
ei.setIntField("hash", h);
}

return h;
String str = env.getStringObject(objref);
return str.hashCode();
}

@MJI
Expand All @@ -300,22 +259,8 @@ public int indexOf__I__I (MJIEnv env, int objref, int c) {

@MJI
public int indexOf__II__I (MJIEnv env, int objref, int c, int fromIndex) {
int vref = env.getReferenceField(objref, "value");
ElementInfo ei = env.getElementInfo(vref);
char[] values = ((CharArrayFields) ei.getFields()).asCharArray();

int len = values.length;

if (fromIndex >= len) { return -1; }
if (fromIndex < 0) {
fromIndex = 0;
}

for (int i = fromIndex; i < len; i++) {
if (values[i] == c) { return i; }
}

return -1;
String str = env.getStringObject(objref);
return str.indexOf(c, fromIndex);
}

@MJI
Expand All @@ -325,22 +270,8 @@ public int lastIndexOf__I__I (MJIEnv env, int objref, int c) {

@MJI
public int lastIndexOf__II__I (MJIEnv env, int objref, int c, int fromIndex) {
int vref = env.getReferenceField(objref, "value");
ElementInfo ei = env.getElementInfo(vref);
char[] values = ((CharArrayFields) ei.getFields()).asCharArray();

int len = values.length;

if (fromIndex < 0) { return -1; }
if (fromIndex > len - 1) {
fromIndex = len - 1;
}

for (int i = fromIndex; i > 0; i--) {
if (values[i] == c) { return i; }
}

return -1;
String str = env.getStringObject(objref);
return str.lastIndexOf(c, fromIndex);
}

@MJI
Expand Down Expand Up @@ -385,67 +316,20 @@ public int substring__II__Ljava_lang_String_2 (MJIEnv env, int objRef, int begin

@MJI
public int concat__Ljava_lang_String_2__Ljava_lang_String_2 (MJIEnv env, int objRef, int strRef) {
Heap heap = env.getHeap();

ElementInfo thisStr = heap.get(objRef);
CharArrayFields thisFields = (CharArrayFields) heap.get(thisStr.getReferenceField("value")).getFields();
char[] thisChars = thisFields.asCharArray();
int thisLength = thisChars.length;

ElementInfo otherStr = heap.get(strRef);
CharArrayFields otherFields = (CharArrayFields) heap.get(otherStr.getReferenceField("value")).getFields();
char[] otherChars = otherFields.asCharArray();
int otherLength = otherChars.length;

if (otherLength == 0) { return objRef; }

char resultChars[] = new char[thisLength + otherLength];
System.arraycopy(thisChars, 0, resultChars, 0, thisLength);
System.arraycopy(otherChars, 0, resultChars, thisLength, otherLength);
String thisStr = env.getStringObject(objRef);
String otherStr = env.getStringObject(objRef);

return env.newString(new String(resultChars));
String result = thisStr.concat(otherStr);
return env.newString(result);
}

// --- the various replaces

@MJI
public int replace__CC__Ljava_lang_String_2 (MJIEnv env, int objRef, char oldChar, char newChar) {

if (oldChar == newChar) { // nothing to replace
return objRef;
}

int vref = env.getReferenceField(objRef, "value");
ElementInfo ei = env.getModifiableElementInfo(vref);
char[] values = ((CharArrayFields) ei.getFields()).asCharArray();
int len = values.length;

char[] newValues = null;

for (int i = 0, j = 0; j < len; i++, j++) {
char c = values[i];
if (c == oldChar) {
if (newValues == null) {
newValues = new char[len];
if (j > 0) {
System.arraycopy(values, 0, newValues, 0, j);
}
}
newValues[j] = newChar;
} else {
if (newValues != null) {
newValues[j] = c;
}
}
}

if (newValues != null) {
String s = new String(newValues);
return env.newString(s);

} else { // oldChar not found, return the original string
return objRef;
}
String thisStr = env.getStringObject(objRef);
String result = thisStr.replace(oldChar, newChar);
return env.newString(result);
}

@MJI
Expand Down Expand Up @@ -534,41 +418,15 @@ public int toUpperCase____Ljava_lang_String_2 (MJIEnv env, int objRef) {

@MJI
public int trim____Ljava_lang_String_2 (MJIEnv env, int objRef) {
Heap heap = env.getHeap();
ElementInfo thisStr = heap.get(objRef);

CharArrayFields thisFields = (CharArrayFields) heap.get(thisStr.getReferenceField("value")).getFields();
char[] thisChars = thisFields.asCharArray();
int thisLength = thisChars.length;

int start = 0;
int end = thisLength;

while ((start < end) && (thisChars[start] <= ' ')) {
start++;
}

while ((start < end) && (thisChars[end - 1] <= ' ')) {
end--;
}

if (start == 0 && end == thisLength) {
// if there was no white space, return the string itself
return objRef;
}

String result = new String(thisChars, start, end - start);
String str = env.getStringObject(objRef);
String result = str.trim();
return env.newString(result);
}

@MJI
public int toCharArray_____3C (MJIEnv env, int objref) {
int vref = env.getReferenceField(objref, "value");
char[] v = env.getCharArrayObject(vref);

int cref = env.newCharArray(v);

return cref;
String str = env.getStringObject(objref);
return env.newCharArray(str.toCharArray()) ;
}

@MJI
Expand Down

0 comments on commit 1ccefdf

Please sign in to comment.