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     if (index >= 0 && index < data.length) {
 146       return data[index];
 147     }
 148     env.throwException("java.lang.StringIndexOutOfBoundsException",
 149                        "String index out of range: " + index);
 150     return '\0';
 151   }
 152
 153
 154   @MJI
 155   public boolean equals0___3C_3CI__Z (MJIEnv env, int clsObjRef, int charsRef1, int charsRef2, int len) {
 156
 157     if ((charsRef1 == MJIEnv.NULL) || (charsRef2 == MJIEnv.NULL)) { return false; }
 158
 159     char[] a = env.getCharArrayObject(charsRef1);
 160     char[] b = env.getCharArrayObject(charsRef2);
 161
 162     if (a.length < len || b.length < len) { return false; }
 163
 164     for (int i = 0; i < len; i++) {
 165       if (a[i] != b[i]) { return false; }
 166     }
 167
 168     return true;
 169   }
 170
 171   @MJI
 172   public boolean equals__Ljava_lang_Object_2__Z (MJIEnv env, int objRef, int argRef) {
 173     if (argRef == MJIEnv.NULL) {
 174       return false;
 175     }
 176
 177     Heap heap = env.getHeap();
 178     ElementInfo s1 = heap.get(objRef);
 179     ClassInfo ci1 = s1.getClassInfo();
 180
 181     ElementInfo s2 = heap.get(argRef);
 182     ClassInfo ci2 = s2.getClassInfo();
 183
 184     if (!ci2.isInstanceOf(ci1)) {
 185       return false;
 186     }
 187
 188     Fields f1 = heap.get(s1.getReferenceField("value")).getFields();
 189     Fields f2 = heap.get(s2.getReferenceField("value")).getFields();
 190
 191     char[] c1 = ((CharArrayFields) f1).asCharArray();
 192     char[] c2 = ((CharArrayFields) f2).asCharArray();
 193
 194     if (c1.length != c2.length) {
 195       return false;
 196     }
 197
 198     for (int i = 0; i < c1.length; i++) {
 199       if (c1[i] != c2[i]) {
 200         return false;
 201       }
 202     }
 203
 204     return true;
 205   }
 206
 207   @MJI
 208   public boolean equalsIgnoreCase__Ljava_lang_String_2__Z (MJIEnv env, int objref, int anotherString) {
 209     String thisString = env.getStringObject(objref);
 210     if (anotherString != MJIEnv.NULL) {
 211       return thisString.equalsIgnoreCase(env.getStringObject(anotherString));
 212     } else {
 213       return false;
 214     }
 215   }
 216
 217   @MJI
 218   public int compareTo__Ljava_lang_String_2__I (MJIEnv env, int objRef, int anotherStringRef) {
 219     String obj = env.getStringObject(objRef);
 220     String anotherString = env.getStringObject(anotherStringRef);
 221     return obj.compareTo(anotherString);
 222   }
 223
 224   @MJI
 225   public int MJIcompare__Ljava_lang_String_2Ljava_lang_String_2__I (MJIEnv env, int clsRef, int s1Ref, int s2Ref) {
 226     // Is there a way to reflect?
 227     String a = env.getStringObject(s1Ref);
 228     String s2 = env.getStringObject(s2Ref);
 229     int n1 = a.length();
 230     int n2 = s2.length();
 231     int min = Math.min(n1, n2);
 232     for (int i = 0; i < min; i++) {
 233       char x = a.charAt(i);
 234       char y = s2.charAt(i);
 235       if (x != y) {
 236         x = Character.toUpperCase(x);
 237         y = Character.toUpperCase(y);
 238         if (x != y) {
 239           x = Character.toLowerCase(x);
 240           y = Character.toLowerCase(y);
 241           if (x != y) { return x - y; }
 242         }
 243       }
 244     }
 245     return n1 - n2;
 246   }
 247
 248   @MJI
 249   public boolean regionMatches__ILjava_lang_String_2II__Z (MJIEnv env, int objRef, int toffset, int otherRef, int ooffset, int len) {
 250     String obj = env.getStringObject(objRef);
 251     String other = env.getStringObject(otherRef);
 252     return obj.regionMatches(toffset, other, ooffset, len);
 253
 254   }
 255
 256   @MJI
 257   public boolean regionMatches__ZILjava_lang_String_2II__Z (MJIEnv env, int objRef, boolean ignoreCase, int toffset, int otherRef, int ooffset, int len) {
 258     String obj = env.getStringObject(objRef);
 259     String other = env.getStringObject(otherRef);
 260     return obj.regionMatches(ignoreCase, toffset, other, ooffset, len);
 261
 262   }
 263
 264   @MJI
 265   public boolean startsWith__Ljava_lang_String_2I__Z (MJIEnv env, int objRef, int prefixRef, int toffset) {
 266     String thisStr = env.getStringObject(objRef);
 267     String prefix = env.getStringObject(prefixRef);
 268     return thisStr.startsWith(prefix, toffset);
 269   }
 270
 271   @MJI
 272   public boolean startsWith__Ljava_lang_String_2__Z (MJIEnv env, int objRef, int prefixRef) {
 273     String thisStr = env.getStringObject(objRef);
 274     String prefix = env.getStringObject(prefixRef);
 275     return thisStr.startsWith(prefix);
 276   }
 277
 278   @MJI
 279   public int hashCode____I (MJIEnv env, int objref) {
 280     return computeStringHashCode(env, objref);
 281   }
 282
 283   public static int computeStringHashCode(MJIEnv env, int objref) {
 284     ElementInfo ei = env.getElementInfo(objref);
 285     int h = ei.getIntField("hash");
 286
 287     if (h == 0) {
 288       int vref = env.getReferenceField(objref, "value");
 289
 290       // now get the char array data, but be aware they are stored as ints
 291       ElementInfo eiVal = env.getElementInfo(vref);
 292       char[] values = eiVal.asCharArray();
 293
 294       for (int i = 0; i < values.length; i++) {
 295         h = 31 * h + values[i];
 296       }
 297
 298       ei = ei.getModifiableInstance();
 299       ei.setIntField("hash", h);
 300     }
 301
 302     return h;
 303   }
 304
 305   @MJI
 306   public int indexOf__I__I (MJIEnv env, int objref, int c) {
 307     return indexOf__II__I(env, objref, c, 0);
 308   }
 309
 310   @MJI
 311   public int indexOf__II__I (MJIEnv env, int objref, int c, int fromIndex) {
 312     int vref = env.getReferenceField(objref, "value");
 313     ElementInfo ei = env.getElementInfo(vref);
 314     char[] values = ((CharArrayFields) ei.getFields()).asCharArray();
 315
 316     int len = values.length;
 317
 318     if (fromIndex >= len) { return -1; }
 319     if (fromIndex < 0) {
 320       fromIndex = 0;
 321     }
 322
 323     for (int i = fromIndex; i < len; i++) {
 324       if (values[i] == c) { return i; }
 325     }
 326
 327     return -1;
 328   }
 329
 330   @MJI
 331   public int lastIndexOf__I__I (MJIEnv env, int objref, int c) {
 332     return lastIndexOf__II__I(env, objref, c, Integer.MAX_VALUE);
 333   }
 334
 335   @MJI
 336   public int lastIndexOf__II__I (MJIEnv env, int objref, int c, int fromIndex) {
 337     int vref = env.getReferenceField(objref, "value");
 338     ElementInfo ei = env.getElementInfo(vref);
 339     char[] values = ((CharArrayFields) ei.getFields()).asCharArray();
 340
 341     int len = values.length;
 342
 343     if (fromIndex < 0) { return -1; }
 344     if (fromIndex > len - 1) {
 345       fromIndex = len - 1;
 346     }
 347
 348     for (int i = fromIndex; i > 0; i--) {
 349       if (values[i] == c) { return i; }
 350     }
 351
 352     return -1;
 353   }
 354
 355   @MJI
 356   public int indexOf__Ljava_lang_String_2__I (MJIEnv env, int objref, int str) {
 357     String thisStr = env.getStringObject(objref);
 358     String indexStr = env.getStringObject(str);
 359
 360     return thisStr.indexOf(indexStr);
 361   }
 362
 363   @MJI
 364   public int indexOf__Ljava_lang_String_2I__I (MJIEnv env, int objref, int str, int fromIndex) {
 365     String thisStr = env.getStringObject(objref);
 366     String indexStr = env.getStringObject(str);
 367
 368     return thisStr.indexOf(indexStr, fromIndex);
 369   }
 370
 371   @MJI
 372   public int lastIndexOf__Ljava_lang_String_2I__I (MJIEnv env, int objref, int str, int fromIndex) {
 373     String thisStr = env.getStringObject(objref);
 374     String indexStr = env.getStringObject(str);
 375
 376     return thisStr.lastIndexOf(indexStr, fromIndex);
 377   }
 378
 379   @MJI
 380   public int substring__I__Ljava_lang_String_2 (MJIEnv env, int objRef, int beginIndex) {
 381     String obj = env.getStringObject(objRef);
 382     String result = obj.substring(beginIndex);
 383     return env.newString(result);
 384
 385   }
 386
 387   @MJI
 388   public int substring__II__Ljava_lang_String_2 (MJIEnv env, int objRef, int beginIndex, int endIndex) {
 389     String obj = env.getStringObject(objRef);
 390     String result = obj.substring(beginIndex, endIndex);
 391     return env.newString(result);
 392
 393   }
 394
 395   @MJI
 396   public int concat__Ljava_lang_String_2__Ljava_lang_String_2 (MJIEnv env, int objRef, int strRef) {
 397     Heap heap = env.getHeap();
 398
 399     ElementInfo thisStr = heap.get(objRef);
 400     CharArrayFields thisFields = (CharArrayFields) heap.get(thisStr.getReferenceField("value")).getFields();
 401     char[] thisChars = thisFields.asCharArray();
 402     int thisLength = thisChars.length;
 403
 404     ElementInfo otherStr = heap.get(strRef);
 405     CharArrayFields otherFields = (CharArrayFields) heap.get(otherStr.getReferenceField("value")).getFields();
 406     char[] otherChars = otherFields.asCharArray();
 407     int otherLength = otherChars.length;
 408
 409     if (otherLength == 0) { return objRef; }
 410
 411     char resultChars[] = new char[thisLength + otherLength];
 412     System.arraycopy(thisChars, 0, resultChars, 0, thisLength);
 413     System.arraycopy(otherChars, 0, resultChars, thisLength, otherLength);
 414
 415     return env.newString(new String(resultChars));
 416   }
 417
 418   // --- the various replaces
 419
 420   @MJI
 421   public int replace__CC__Ljava_lang_String_2 (MJIEnv env, int objRef, char oldChar, char newChar) {
 422
 423     if (oldChar == newChar) { // nothing to replace
 424       return objRef;
 425     }
 426
 427     int vref = env.getReferenceField(objRef, "value");
 428     ElementInfo ei = env.getModifiableElementInfo(vref);
 429     char[] values = ((CharArrayFields) ei.getFields()).asCharArray();
 430     int len = values.length;
 431
 432     char[] newValues = null;
 433
 434     for (int i = 0, j = 0; j < len; i++, j++) {
 435       char c = values[i];
 436       if (c == oldChar) {
 437         if (newValues == null) {
 438           newValues = new char[len];
 439           if (j > 0) {
 440             System.arraycopy(values, 0, newValues, 0, j);
 441           }
 442         }
 443         newValues[j] = newChar;
 444       } else {
 445         if (newValues != null) {
 446           newValues[j] = c;
 447         }
 448       }
 449     }
 450
 451     if (newValues != null) {
 452       String s = new String(newValues);
 453       return env.newString(s);
 454
 455     } else { // oldChar not found, return the original string
 456       return objRef;
 457     }
 458   }
 459
 460   @MJI
 461   public boolean matches__Ljava_lang_String_2__Z (MJIEnv env, int objRef, int regexRef) {
 462     String s = env.getStringObject(objRef);
 463     String r = env.getStringObject(regexRef);
 464
 465     return s.matches(r);
 466   }
 467
 468   @MJI
 469   public int replaceFirst__Ljava_lang_String_2Ljava_lang_String_2__Ljava_lang_String_2 (MJIEnv env, int objRef, int regexRef, int replacementRef) {
 470     String thisStr = env.getStringObject(objRef);
 471     String regexStr = env.getStringObject(regexRef);
 472     String replacementStr = env.getStringObject(replacementRef);
 473
 474     String result = thisStr.replaceFirst(regexStr, replacementStr);
 475     return (result != thisStr) ? env.newString(result) : objRef;
 476   }
 477
 478   @MJI
 479   public int replaceAll__Ljava_lang_String_2Ljava_lang_String_2__Ljava_lang_String_2 (MJIEnv env, int objRef, int regexRef, int replacementRef) {
 480     String thisStr = env.getStringObject(objRef);
 481     String regexStr = env.getStringObject(regexRef);
 482     String replacementStr = env.getStringObject(replacementRef);
 483
 484     String result = thisStr.replaceAll(regexStr, replacementStr);
 485     return (result != thisStr) ? env.newString(result) : objRef;
 486   }
 487
 488   @MJI
 489   public int split__Ljava_lang_String_2I___3Ljava_lang_String_2 (MJIEnv env, int clsObjRef, int strRef, int limit) {
 490     String s = env.getStringObject(strRef);
 491     String obj = env.getStringObject(clsObjRef);
 492
 493     String[] result = obj.split(s, limit);
 494
 495     return env.newStringArray(result);
 496   }
 497
 498   @MJI
 499   public int split__Ljava_lang_String_2___3Ljava_lang_String_2 (MJIEnv env, int clsObjRef, int strRef) {
 500     String s = env.getStringObject(strRef);
 501     String obj = env.getStringObject(clsObjRef);
 502
 503     String[] result = obj.split(s);
 504
 505     return env.newStringArray(result);
 506   }
 507
 508   @MJI
 509   public int toLowerCase__Ljava_util_Locale_2__Ljava_lang_String_2 (MJIEnv env, int objRef, int locRef) {
 510     String s = env.getStringObject(objRef);
 511     Locale loc = JPF_java_util_Locale.getLocale(env, locRef);
 512
 513     String lower = s.toLowerCase(loc);
 514
 515     return (s == lower) ? objRef : env.newString(lower);
 516   }
 517
 518   @MJI
 519   public int toLowerCase____Ljava_lang_String_2 (MJIEnv env, int objRef) {
 520     String s = env.getStringObject(objRef);
 521     String lower = s.toLowerCase();
 522
 523     return (s == lower) ? objRef : env.newString(lower);
 524   }
 525
 526   @MJI
 527   public int toUpperCase__Ljava_util_Locale_2__Ljava_lang_String_2 (MJIEnv env, int objRef, int locRef) {
 528     String s = env.getStringObject(objRef);
 529     Locale loc = JPF_java_util_Locale.getLocale(env, locRef);
 530
 531     String upper = s.toUpperCase(loc);
 532
 533     return (s == upper) ? objRef : env.newString(upper);
 534   }
 535
 536   @MJI
 537   public int toUpperCase____Ljava_lang_String_2 (MJIEnv env, int objRef) {
 538     String s = env.getStringObject(objRef);
 539     String upper = s.toUpperCase();
 540
 541     return (s == upper) ? objRef : env.newString(upper);
 542   }
 543
 544   @MJI
 545   public int trim____Ljava_lang_String_2 (MJIEnv env, int objRef) {
 546     Heap heap = env.getHeap();
 547     ElementInfo thisStr = heap.get(objRef);
 548
 549     CharArrayFields thisFields = (CharArrayFields) heap.get(thisStr.getReferenceField("value")).getFields();
 550     char[] thisChars = thisFields.asCharArray();
 551     int thisLength = thisChars.length;
 552
 553     int start = 0;
 554     int end = thisLength;
 555
 556     while ((start < end) && (thisChars[start] <= ' ')) {
 557       start++;
 558     }
 559
 560     while ((start < end) && (thisChars[end - 1] <= ' ')) {
 561       end--;
 562     }
 563
 564     if (start == 0 && end == thisLength) {
 565       // if there was no white space, return the string itself
 566       return objRef;
 567     }
 568
 569     String result = new String(thisChars, start, end - start);
 570     return env.newString(result);
 571   }
 572
 573   @MJI
 574   public int toCharArray_____3C (MJIEnv env, int objref) {
 575     int vref = env.getReferenceField(objref, "value");
 576     char[] v = env.getCharArrayObject(vref);
 577
 578     int cref = env.newCharArray(v);
 579
 580     return cref;
 581   }
 582
 583   @MJI
 584   public int format__Ljava_lang_String_2_3Ljava_lang_Object_2__Ljava_lang_String_2 (MJIEnv env, int clsObjRef, int fmtRef, int argRef) {
 585     return env.newString(env.format(fmtRef, argRef));
 586   }
 587
 588   @MJI
 589   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) {
 590     Locale loc = JPF_java_util_Locale.getLocale(env, locRef);
 591     return env.newString(env.format(loc, fmtRef, argRef));
 592   }
 593
 594   @MJI
 595   public int intern____Ljava_lang_String_2 (MJIEnv env, int robj) {
 596     // <2do> Replace this with a JPF space HashSet once we have a String model
 597     Heap heap = env.getHeap();
 598
 599     String s = env.getStringObject(robj);
 600     ElementInfo ei = heap.newInternString(s, env.getThreadInfo());
 601
 602     return ei.getObjectRef();
 603   }
 604
 605   @MJI
 606   public int valueOf__I__Ljava_lang_String_2 (MJIEnv env, int clsref, int i) {
 607     String result = String.valueOf(i);
 608     return env.newString(result);
 609   }
 610
 611   @MJI
 612   public int valueOf__J__Ljava_lang_String_2 (MJIEnv env, int clsref, long l) {
 613     String result = String.valueOf(l);
 614     return env.newString(result);
 615   }
 616
 617   @MJI
 618   public int valueOf__F__Ljava_lang_String_2 (MJIEnv env, int clsref, float f) {
 619     String result = String.valueOf(f);
 620     return env.newString(result);
 621   }
 622
 623   @MJI
 624   public int valueOf__D__Ljava_lang_String_2 (MJIEnv env, int clsref, double d) {
 625     String result = String.valueOf(d);
 626     return env.newString(result);
 627   }
 628 }