src/peers/gov/nasa/jpf/vm/JPF_java_lang_String.java

   1 /*
   2  * Copyright (C) 2014, United States Government, as represented by the
   3  * Administrator of the National Aeronautics and Space Administration.
   4  * All rights reserved.
   5  *
   6  * The Java Pathfinder core (jpf-core) platform is licensed under the
   7  * Apache License, Version 2.0 (the "License"); you may not use this file except
   8  * in compliance with the License. You may obtain a copy of the License at
   9  *
  10  *        http://www.apache.org/licenses/LICENSE-2.0.
  11  *
  12  * Unless required by applicable law or agreed to in writing, software
  13  * distributed under the License is distributed on an "AS IS" BASIS,
  14  * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
  15  * See the License for the specific language governing permissions and
  16  * limitations under the License.
  17  */
  18 package gov.nasa.jpf.vm;
  19
  20 import gov.nasa.jpf.annotation.MJI;
  21 import gov.nasa.jpf.vm.CharArrayFields;
  22 import gov.nasa.jpf.vm.ElementInfo;
  23 import gov.nasa.jpf.vm.Fields;
  24 import gov.nasa.jpf.vm.Heap;
  25 import gov.nasa.jpf.vm.MJIEnv;
  26 import gov.nasa.jpf.vm.NativePeer;
  27
  28 import java.io.UnsupportedEncodingException;
  29 import java.util.Locale;
  30
  31 /**
  32  * MJI NativePeer class for java.lang.String library abstraction
  33  */
  34 public class JPF_java_lang_String extends NativePeer {
  35
  36
  37   @MJI
  38   public int init___3CII__Ljava_lang_String_2 (MJIEnv env, int objRef, int valueRef, int offset, int count) {
  39     char[] value = env.getCharArrayObject(valueRef);
  40     String result = new String(value, offset, count);
  41     return env.newString(result);
  42   }
  43
  44   @MJI
  45   public int init___3III__Ljava_lang_String_2 (MJIEnv env, int objRef, int codePointsRef, int offset, int count) {
  46     int[] codePoints = env.getIntArrayObject(codePointsRef);
  47     String result = new String(codePoints, offset, count);
  48     return env.newString(result);
  49   }
  50
  51   @SuppressWarnings("deprecation")
  52   @MJI
  53   public int init___3BIII__Ljava_lang_String_2 (MJIEnv env, int objRef, int asciiRef, int hibyte, int offset, int count) {
  54     byte[] ascii = env.getByteArrayObject(asciiRef);
  55     String result = new String(ascii, hibyte, offset, count);
  56     return env.newString(result);
  57   }
  58
  59   @MJI
  60   public int init___3BIILjava_lang_String_2__Ljava_lang_String_2 (MJIEnv env, int objRef, int bytesRef, int offset, int length, int charsetNameRef) throws UnsupportedEncodingException {
  61     byte[] bytes = env.getByteArrayObject(bytesRef);
  62     String charsetName = env.getStringObject(charsetNameRef);
  63     String result = new String(bytes, offset, length, charsetName);
  64     return env.newString(result);
  65   }
  66
  67   @MJI
  68   public int init___3BII__Ljava_lang_String_2 (MJIEnv env, int objRef, int bytesRef, int offset, int length) {
  69     byte[] bytes = env.getByteArrayObject(bytesRef);
  70     String result = new String(bytes, offset, length);
  71     return env.newString(result);
  72   }
  73
  74   @MJI
  75   public int codePointAt__I__I (MJIEnv env, int objRef, int index) {
  76     String obj = env.getStringObject(objRef);
  77     return obj.codePointAt(index);
  78   }
  79
  80   @MJI
  81   public int codePointBefore__I__I (MJIEnv env, int objRef, int index) {
  82     String obj = env.getStringObject(objRef);
  83     return obj.codePointBefore(index);
  84   }
  85
  86   @MJI
  87   public int codePointCount__II__I (MJIEnv env, int objRef, int beginIndex, int endIndex) {
  88     String obj = env.getStringObject(objRef);
  89     return obj.codePointCount(beginIndex, endIndex);
  90   }
  91
  92   @MJI
  93   public int offsetByCodePoints__II__I (MJIEnv env, int objRef, int index, int codePointOffset) {
  94     String obj = env.getStringObject(objRef);
  95     return obj.offsetByCodePoints(index, codePointOffset);
  96   }
  97
  98   @MJI
  99   public void getChars__II_3CI__V (MJIEnv env, int objRef, int srcBegin, int srcEnd, int dstRef, int dstBegin) {
 100     String obj = env.getStringObject(objRef);
 101     char[] dst = env.getCharArrayObject(dstRef);
 102     obj.getChars(srcBegin, srcEnd, dst, dstBegin);
 103   }
 104
 105   @MJI
 106   public void getChars___3CI__V(MJIEnv env, int objRef, int dstRef, int dstBegin) {
 107     String obj = env.getStringObject(objRef);
 108     char[] dst = env.getCharArrayObject(dstRef);
 109     obj.getChars(0, obj.length(), dst, dstBegin);
 110   }
 111
 112   @SuppressWarnings("deprecation")
 113   @MJI
 114   public void getBytes__II_3BI__V (MJIEnv env, int objRef, int srcBegin, int srcEnd, int dstRef, int dstBegin) {
 115     String obj = env.getStringObject(objRef);
 116     byte[] dst = env.getByteArrayObject(dstRef);
 117     obj.getBytes(srcBegin, srcEnd, dst, dstBegin);
 118   }
 119
 120   @MJI
 121   public int getBytes__Ljava_lang_String_2___3B (MJIEnv env, int objRef, int charSetRef) {
 122     String string = env.getStringObject(objRef);
 123     String charset = env.getStringObject(charSetRef);
 124
 125     try {
 126       byte[] b = string.getBytes(charset);
 127       return env.newByteArray(b);
 128
 129     } catch (UnsupportedEncodingException uex) {
 130       env.throwException(uex.getClass().getName(), uex.getMessage());
 131       return MJIEnv.NULL;
 132     }
 133   }
 134
 135   @MJI
 136   public int getBytes_____3B (MJIEnv env, int objRef) {
 137     String obj = env.getStringObject(objRef);
 138     byte[] bytes = obj.getBytes();
 139     return env.newByteArray(bytes);
 140   }
 141
 142   @MJI
 143   public char charAt__I__C (MJIEnv env, int objRef, int index){
 144     char[] data = env.getStringChars(objRef);
 145     return data[index];
 146   }
 147
 148
 149   @MJI
 150   public boolean equals0___3C_3CI__Z (MJIEnv env, int clsObjRef, int charsRef1, int charsRef2, int len) {
 151
 152     if ((charsRef1 == MJIEnv.NULL) || (charsRef2 == MJIEnv.NULL)) { return false; }
 153
 154     char[] a = env.getCharArrayObject(charsRef1);
 155     char[] b = env.getCharArrayObject(charsRef2);
 156
 157     if (a.length < len || b.length < len) { return false; }
 158
 159     for (int i = 0; i < len; i++) {
 160       if (a[i] != b[i]) { return false; }
 161     }
 162
 163     return true;
 164   }
 165
 166   @MJI
 167   public boolean equals__Ljava_lang_Object_2__Z (MJIEnv env, int objRef, int argRef) {
 168     if (argRef == MJIEnv.NULL) {
 169       return false;
 170     }
 171
 172     Heap heap = env.getHeap();
 173     ElementInfo s1 = heap.get(objRef);
 174     ClassInfo ci1 = s1.getClassInfo();
 175
 176     ElementInfo s2 = heap.get(argRef);
 177     ClassInfo ci2 = s2.getClassInfo();
 178
 179     if (!ci2.isInstanceOf(ci1)) {
 180       return false;
 181     }
 182
 183     Fields f1 = heap.get(s1.getReferenceField("value")).getFields();
 184     Fields f2 = heap.get(s2.getReferenceField("value")).getFields();
 185
 186     char[] c1 = ((CharArrayFields) f1).asCharArray();
 187     char[] c2 = ((CharArrayFields) f2).asCharArray();
 188
 189     if (c1.length != c2.length) {
 190       return false;
 191     }
 192
 193     for (int i = 0; i < c1.length; i++) {
 194       if (c1[i] != c2[i]) {
 195         return false;
 196       }
 197     }
 198
 199     return true;
 200   }
 201
 202   @MJI
 203   public boolean equalsIgnoreCase__Ljava_lang_String_2__Z (MJIEnv env, int objref, int anotherString) {
 204     String thisString = env.getStringObject(objref);
 205     if (anotherString != MJIEnv.NULL) {
 206       return thisString.equalsIgnoreCase(env.getStringObject(anotherString));
 207     } else {
 208       return false;
 209     }
 210   }
 211
 212   @MJI
 213   public int compareTo__Ljava_lang_String_2__I (MJIEnv env, int objRef, int anotherStringRef) {
 214     String obj = env.getStringObject(objRef);
 215     String anotherString = env.getStringObject(anotherStringRef);
 216     return obj.compareTo(anotherString);
 217   }
 218
 219   @MJI
 220   public int MJIcompare__Ljava_lang_String_2Ljava_lang_String_2__I (MJIEnv env, int clsRef, int s1Ref, int s2Ref) {
 221     // Is there a way to reflect?
 222     String a = env.getStringObject(s1Ref);
 223     String s2 = env.getStringObject(s2Ref);
 224     int n1 = a.length();
 225     int n2 = s2.length();
 226     int min = Math.min(n1, n2);
 227     for (int i = 0; i < min; i++) {
 228       char x = a.charAt(i);
 229       char y = s2.charAt(i);
 230       if (x != y) {
 231         x = Character.toUpperCase(x);
 232         y = Character.toUpperCase(y);
 233         if (x != y) {
 234           x = Character.toLowerCase(x);
 235           y = Character.toLowerCase(y);
 236           if (x != y) { return x - y; }
 237         }
 238       }
 239     }
 240     return n1 - n2;
 241   }
 242
 243   @MJI
 244   public boolean regionMatches__ILjava_lang_String_2II__Z (MJIEnv env, int objRef, int toffset, int otherRef, int ooffset, int len) {
 245     String obj = env.getStringObject(objRef);
 246     String other = env.getStringObject(otherRef);
 247     return obj.regionMatches(toffset, other, ooffset, len);
 248
 249   }
 250
 251   @MJI
 252   public boolean regionMatches__ZILjava_lang_String_2II__Z (MJIEnv env, int objRef, boolean ignoreCase, int toffset, int otherRef, int ooffset, int len) {
 253     String obj = env.getStringObject(objRef);
 254     String other = env.getStringObject(otherRef);
 255     return obj.regionMatches(ignoreCase, toffset, other, ooffset, len);
 256
 257   }
 258
 259   @MJI
 260   public boolean startsWith__Ljava_lang_String_2I__Z (MJIEnv env, int objRef, int prefixRef, int toffset) {
 261     String thisStr = env.getStringObject(objRef);
 262     String prefix = env.getStringObject(prefixRef);
 263     return thisStr.startsWith(prefix, toffset);
 264   }
 265
 266   @MJI
 267   public boolean startsWith__Ljava_lang_String_2__Z (MJIEnv env, int objRef, int prefixRef) {
 268     String thisStr = env.getStringObject(objRef);
 269     String prefix = env.getStringObject(prefixRef);
 270     return thisStr.startsWith(prefix);
 271   }
 272
 273   @MJI
 274   public int hashCode____I (MJIEnv env, int objref) {
 275     return computeStringHashCode(env, objref);
 276   }
 277
 278   public static int computeStringHashCode(MJIEnv env, int objref) {
 279     ElementInfo ei = env.getElementInfo(objref);
 280     int h = ei.getIntField("hash");
 281
 282     if (h == 0) {
 283       int vref = env.getReferenceField(objref, "value");
 284
 285       // now get the char array data, but be aware they are stored as ints
 286       ElementInfo eiVal = env.getElementInfo(vref);
 287       char[] values = eiVal.asCharArray();
 288
 289       for (int i = 0; i < values.length; i++) {
 290         h = 31 * h + values[i];
 291       }
 292
 293       ei = ei.getModifiableInstance();
 294       ei.setIntField("hash", h);
 295     }
 296
 297     return h;
 298   }
 299
 300   @MJI
 301   public int indexOf__I__I (MJIEnv env, int objref, int c) {
 302     return indexOf__II__I(env, objref, c, 0);
 303   }
 304
 305   @MJI
 306   public int indexOf__II__I (MJIEnv env, int objref, int c, int fromIndex) {
 307     int vref = env.getReferenceField(objref, "value");
 308     ElementInfo ei = env.getElementInfo(vref);
 309     char[] values = ((CharArrayFields) ei.getFields()).asCharArray();
 310
 311     int len = values.length;
 312
 313     if (fromIndex >= len) { return -1; }
 314     if (fromIndex < 0) {
 315       fromIndex = 0;
 316     }
 317
 318     for (int i = fromIndex; i < len; i++) {
 319       if (values[i] == c) { return i; }
 320     }
 321
 322     return -1;
 323   }
 324
 325   @MJI
 326   public int lastIndexOf__I__I (MJIEnv env, int objref, int c) {
 327     return lastIndexOf__II__I(env, objref, c, Integer.MAX_VALUE);
 328   }
 329
 330   @MJI
 331   public int lastIndexOf__II__I (MJIEnv env, int objref, int c, int fromIndex) {
 332     int vref = env.getReferenceField(objref, "value");
 333     ElementInfo ei = env.getElementInfo(vref);
 334     char[] values = ((CharArrayFields) ei.getFields()).asCharArray();
 335
 336     int len = values.length;
 337
 338     if (fromIndex < 0) { return -1; }
 339     if (fromIndex > len - 1) {
 340       fromIndex = len - 1;
 341     }
 342
 343     for (int i = fromIndex; i > 0; i--) {
 344       if (values[i] == c) { return i; }
 345     }
 346
 347     return -1;
 348   }
 349
 350   @MJI
 351   public int indexOf__Ljava_lang_String_2__I (MJIEnv env, int objref, int str) {
 352     String thisStr = env.getStringObject(objref);
 353     String indexStr = env.getStringObject(str);
 354
 355     return thisStr.indexOf(indexStr);
 356   }
 357
 358   @MJI
 359   public int indexOf__Ljava_lang_String_2I__I (MJIEnv env, int objref, int str, int fromIndex) {
 360     String thisStr = env.getStringObject(objref);
 361     String indexStr = env.getStringObject(str);
 362
 363     return thisStr.indexOf(indexStr, fromIndex);
 364   }
 365
 366   @MJI
 367   public int lastIndexOf__Ljava_lang_String_2I__I (MJIEnv env, int objref, int str, int fromIndex) {
 368     String thisStr = env.getStringObject(objref);
 369     String indexStr = env.getStringObject(str);
 370
 371     return thisStr.lastIndexOf(indexStr, fromIndex);
 372   }
 373
 374   @MJI
 375   public int substring__I__Ljava_lang_String_2 (MJIEnv env, int objRef, int beginIndex) {
 376     String obj = env.getStringObject(objRef);
 377     String result = obj.substring(beginIndex);
 378     return env.newString(result);
 379
 380   }
 381
 382   @MJI
 383   public int substring__II__Ljava_lang_String_2 (MJIEnv env, int objRef, int beginIndex, int endIndex) {
 384     String obj = env.getStringObject(objRef);
 385     String result = obj.substring(beginIndex, endIndex);
 386     return env.newString(result);
 387
 388   }
 389
 390   @MJI
 391   public int concat__Ljava_lang_String_2__Ljava_lang_String_2 (MJIEnv env, int objRef, int strRef) {
 392     Heap heap = env.getHeap();
 393
 394     ElementInfo thisStr = heap.get(objRef);
 395     CharArrayFields thisFields = (CharArrayFields) heap.get(thisStr.getReferenceField("value")).getFields();
 396     char[] thisChars = thisFields.asCharArray();
 397     int thisLength = thisChars.length;
 398
 399     ElementInfo otherStr = heap.get(strRef);
 400     CharArrayFields otherFields = (CharArrayFields) heap.get(otherStr.getReferenceField("value")).getFields();
 401     char[] otherChars = otherFields.asCharArray();
 402     int otherLength = otherChars.length;
 403
 404     if (otherLength == 0) { return objRef; }
 405
 406     char resultChars[] = new char[thisLength + otherLength];
 407     System.arraycopy(thisChars, 0, resultChars, 0, thisLength);
 408     System.arraycopy(otherChars, 0, resultChars, thisLength, otherLength);
 409
 410     return env.newString(new String(resultChars));
 411   }
 412
 413   // --- the various replaces
 414
 415   @MJI
 416   public int replace__CC__Ljava_lang_String_2 (MJIEnv env, int objRef, char oldChar, char newChar) {
 417
 418     if (oldChar == newChar) { // nothing to replace
 419       return objRef;
 420     }
 421
 422     int vref = env.getReferenceField(objRef, "value");
 423     ElementInfo ei = env.getModifiableElementInfo(vref);
 424     char[] values = ((CharArrayFields) ei.getFields()).asCharArray();
 425     int len = values.length;
 426
 427     char[] newValues = null;
 428
 429     for (int i = 0, j = 0; j < len; i++, j++) {
 430       char c = values[i];
 431       if (c == oldChar) {
 432         if (newValues == null) {
 433           newValues = new char[len];
 434           if (j > 0) {
 435             System.arraycopy(values, 0, newValues, 0, j);
 436           }
 437         }
 438         newValues[j] = newChar;
 439       } else {
 440         if (newValues != null) {
 441           newValues[j] = c;
 442         }
 443       }
 444     }
 445
 446     if (newValues != null) {
 447       String s = new String(newValues);
 448       return env.newString(s);
 449
 450     } else { // oldChar not found, return the original string
 451       return objRef;
 452     }
 453   }
 454
 455   @MJI
 456   public boolean matches__Ljava_lang_String_2__Z (MJIEnv env, int objRef, int regexRef) {
 457     String s = env.getStringObject(objRef);
 458     String r = env.getStringObject(regexRef);
 459
 460     return s.matches(r);
 461   }
 462
 463   @MJI
 464   public int replaceFirst__Ljava_lang_String_2Ljava_lang_String_2__Ljava_lang_String_2 (MJIEnv env, int objRef, int regexRef, int replacementRef) {
 465     String thisStr = env.getStringObject(objRef);
 466     String regexStr = env.getStringObject(regexRef);
 467     String replacementStr = env.getStringObject(replacementRef);
 468
 469     String result = thisStr.replaceFirst(regexStr, replacementStr);
 470     return (result != thisStr) ? env.newString(result) : objRef;
 471   }
 472
 473   @MJI
 474   public int replaceAll__Ljava_lang_String_2Ljava_lang_String_2__Ljava_lang_String_2 (MJIEnv env, int objRef, int regexRef, int replacementRef) {
 475     String thisStr = env.getStringObject(objRef);
 476     String regexStr = env.getStringObject(regexRef);
 477     String replacementStr = env.getStringObject(replacementRef);
 478
 479     String result = thisStr.replaceAll(regexStr, replacementStr);
 480     return (result != thisStr) ? env.newString(result) : objRef;
 481   }
 482
 483   @MJI
 484   public int split__Ljava_lang_String_2I___3Ljava_lang_String_2 (MJIEnv env, int clsObjRef, int strRef, int limit) {
 485     String s = env.getStringObject(strRef);
 486     String obj = env.getStringObject(clsObjRef);
 487
 488     String[] result = obj.split(s, limit);
 489
 490     return env.newStringArray(result);
 491   }
 492
 493   @MJI
 494   public int split__Ljava_lang_String_2___3Ljava_lang_String_2 (MJIEnv env, int clsObjRef, int strRef) {
 495     String s = env.getStringObject(strRef);
 496     String obj = env.getStringObject(clsObjRef);
 497
 498     String[] result = obj.split(s);
 499
 500     return env.newStringArray(result);
 501   }
 502
 503   @MJI
 504   public int toLowerCase__Ljava_util_Locale_2__Ljava_lang_String_2 (MJIEnv env, int objRef, int locRef) {
 505     String s = env.getStringObject(objRef);
 506     Locale loc = JPF_java_util_Locale.getLocale(env, locRef);
 507
 508     String lower = s.toLowerCase(loc);
 509
 510     return (s == lower) ? objRef : env.newString(lower);
 511   }
 512
 513   @MJI
 514   public int toLowerCase____Ljava_lang_String_2 (MJIEnv env, int objRef) {
 515     String s = env.getStringObject(objRef);
 516     String lower = s.toLowerCase();
 517
 518     return (s == lower) ? objRef : env.newString(lower);
 519   }
 520
 521   @MJI
 522   public int toUpperCase__Ljava_util_Locale_2__Ljava_lang_String_2 (MJIEnv env, int objRef, int locRef) {
 523     String s = env.getStringObject(objRef);
 524     Locale loc = JPF_java_util_Locale.getLocale(env, locRef);
 525
 526     String upper = s.toUpperCase(loc);
 527
 528     return (s == upper) ? objRef : env.newString(upper);
 529   }
 530
 531   @MJI
 532   public int toUpperCase____Ljava_lang_String_2 (MJIEnv env, int objRef) {
 533     String s = env.getStringObject(objRef);
 534     String upper = s.toUpperCase();
 535
 536     return (s == upper) ? objRef : env.newString(upper);
 537   }
 538
 539   @MJI
 540   public int trim____Ljava_lang_String_2 (MJIEnv env, int objRef) {
 541     Heap heap = env.getHeap();
 542     ElementInfo thisStr = heap.get(objRef);
 543
 544     CharArrayFields thisFields = (CharArrayFields) heap.get(thisStr.getReferenceField("value")).getFields();
 545     char[] thisChars = thisFields.asCharArray();
 546     int thisLength = thisChars.length;
 547
 548     int start = 0;
 549     int end = thisLength;
 550
 551     while ((start < end) && (thisChars[start] <= ' ')) {
 552       start++;
 553     }
 554
 555     while ((start < end) && (thisChars[end - 1] <= ' ')) {
 556       end--;
 557     }
 558
 559     if (start == 0 && end == thisLength) {
 560       // if there was no white space, return the string itself
 561       return objRef;
 562     }
 563
 564     String result = new String(thisChars, start, end - start);
 565     return env.newString(result);
 566   }
 567
 568   @MJI
 569   public int toCharArray_____3C (MJIEnv env, int objref) {
 570     int vref = env.getReferenceField(objref, "value");
 571     char[] v = env.getCharArrayObject(vref);
 572
 573     int cref = env.newCharArray(v);
 574
 575     return cref;
 576   }
 577
 578   @MJI
 579   public int format__Ljava_lang_String_2_3Ljava_lang_Object_2__Ljava_lang_String_2 (MJIEnv env, int clsObjRef, int fmtRef, int argRef) {
 580     return env.newString(env.format(fmtRef, argRef));
 581   }
 582
 583   @MJI
 584   public int format__Ljava_util_Locale_2Ljava_lang_String_2_3Ljava_lang_Object_2__Ljava_lang_String_2 (MJIEnv env, int clsObjRef, int locRef, int fmtRef, int argRef) {
 585     Locale loc = JPF_java_util_Locale.getLocale(env, locRef);
 586     return env.newString(env.format(loc, fmtRef, argRef));
 587   }
 588
 589   @MJI
 590   public int intern____Ljava_lang_String_2 (MJIEnv env, int robj) {
 591     // <2do> Replace this with a JPF space HashSet once we have a String model
 592     Heap heap = env.getHeap();
 593
 594     String s = env.getStringObject(robj);
 595     ElementInfo ei = heap.newInternString(s, env.getThreadInfo());
 596
 597     return ei.getObjectRef();
 598   }
 599
 600   @MJI
 601   public int valueOf__I__Ljava_lang_String_2 (MJIEnv env, int clsref, int i) {
 602     String result = String.valueOf(i);
 603     return env.newString(result);
 604   }
 605
 606   @MJI
 607   public int valueOf__J__Ljava_lang_String_2 (MJIEnv env, int clsref, long l) {
 608     String result = String.valueOf(l);
 609     return env.newString(result);
 610   }
 611
 612   @MJI
 613   public int valueOf__F__Ljava_lang_String_2 (MJIEnv env, int clsref, float f) {
 614     String result = String.valueOf(f);
 615     return env.newString(result);
 616   }
 617
 618   @MJI
 619   public int valueOf__D__Ljava_lang_String_2 (MJIEnv env, int clsref, double d) {
 620     String result = String.valueOf(d);
 621     return env.newString(result);
 622   }
 623 }