src/peers/gov/nasa/jpf/vm/JPF_java_lang_StringBuilder.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.MJIEnv;
  22 import gov.nasa.jpf.vm.NativePeer;
  23
  24 public class JPF_java_lang_StringBuilder extends NativePeer {
  25
  26   int appendString (MJIEnv env, int objref, String s) {
  27     int slen = s.length();
  28     int aref = env.getReferenceField(objref, "value");
  29     int alen = env.getArrayLength(aref);
  30     int count = env.getIntField(objref, "count");
  31     int i, j;
  32     int n = count + slen;
  33
  34     if (n < alen) {
  35       for (i=count, j=0; i<n; i++, j++) {
  36         env.setCharArrayElement(aref, i, s.charAt(j));
  37       }
  38     } else {
  39       int m = 3 * alen / 2;
  40       if (m < n) {
  41         m = n;
  42       }
  43       int arefNew = env.newCharArray(m);
  44       for (i=0; i<count; i++) {
  45         env.setCharArrayElement(arefNew, i, env.getCharArrayElement(aref, i));
  46       }
  47       for (j=0; i<n; i++, j++) {
  48         env.setCharArrayElement(arefNew, i, s.charAt(j));
  49       }
  50       env.setReferenceField(objref, "value", arefNew);
  51     }
  52
  53     env.setIntField(objref, "count", n);
  54
  55     return objref;
  56   }
  57
  58   // we skip the AbstractStringBuilder ctor here, which is a bit dangerous
  59   // This is only justified because StringBuilders are used everywhere (implicitly)
  60   @MJI
  61   public void $init____V (MJIEnv env, int objref){
  62     int aref = env.newCharArray(16);
  63     env.setReferenceField(objref, "value", aref);
  64   }
  65   @MJI
  66   public void $init__I__V (MJIEnv env, int objref, int len){
  67     int aref = env.newCharArray(len);
  68     env.setReferenceField(objref, "value", aref);
  69   }
  70   @MJI
  71   public void $init__Ljava_lang_String_2__V (MJIEnv env, int objref, int sRef){
  72     if (sRef == MJIEnv.NULL){
  73       env.throwException("java.lang.NullPointerException");
  74       return;
  75     }
  76
  77     char[] src = env.getStringChars(sRef);
  78     int aref = env.newCharArray(src.length + 16);
  79     char[] dst = env.getCharArrayObject(aref);
  80     System.arraycopy(src,0,dst,0,src.length);
  81
  82     env.setReferenceField(objref, "value", aref);
  83     env.setIntField(objref, "count", src.length);
  84   }
  85
  86
  87   @MJI
  88   public int append__Ljava_lang_String_2__Ljava_lang_StringBuilder_2 (MJIEnv env, int objref, int sref) {
  89     String s = env.getStringObject(sref);
  90
  91     if (s == null) s = "null";
  92
  93     return appendString(env, objref, s);
  94   }
  95
  96   @MJI
  97   public int append__I__Ljava_lang_StringBuilder_2 (MJIEnv env, int objref, int i) {
  98     String s = Integer.toString(i);
  99
 100     return appendString(env, objref, s);
 101   }
 102
 103   @MJI
 104   public int append__F__Ljava_lang_StringBuilder_2 (MJIEnv env, int objref, float f) {
 105     String s = Float.toString(f);
 106
 107     return appendString(env, objref, s);
 108   }
 109
 110   @MJI
 111   public int append__D__Ljava_lang_StringBuilder_2 (MJIEnv env, int objref, double d) {
 112     String s = Double.toString(d);
 113
 114     return appendString(env, objref, s);
 115   }
 116
 117   @MJI
 118   public int append__J__Ljava_lang_StringBuilder_2 (MJIEnv env, int objref, long l) {
 119     String s = Long.toString(l);
 120
 121     return appendString(env, objref, s);
 122   }
 123
 124   @MJI
 125   public int append__Z__Ljava_lang_StringBuilder_2 (MJIEnv env, int objref, boolean b) {
 126     String s = b ? "true" : "false";
 127
 128     return appendString(env, objref, s);
 129   }
 130
 131   @MJI
 132   public int append__C__Ljava_lang_StringBuilder_2 (MJIEnv env, int objref, char c) {
 133     int aref = env.getReferenceField(objref, "value");
 134     int alen = env.getArrayLength(aref);
 135     int count = env.getIntField(objref, "count");
 136     int i;
 137     int n = count +1;
 138
 139     // TODO: Fix for Groovy's model-checking
 140     // TODO: Need to allocate something if the initial array is really empty
 141     if (alen == 0) {
 142       $init____V (env, objref);
 143       aref = env.getReferenceField(objref, "value");
 144       alen = env.getArrayLength(aref);
 145     }
 146     if (n < alen) {
 147       env.setCharArrayElement(aref, count, c);
 148     } else {
 149       int m = 3 * alen / 2;
 150       int arefNew = env.newCharArray(m);
 151       for (i = 0; i < count; i++) {
 152         env.setCharArrayElement(arefNew, i, env.getCharArrayElement(aref, i));
 153       }
 154       env.setCharArrayElement(arefNew, count, c);
 155       env.setReferenceField(objref, "value", arefNew);
 156     }
 157
 158     env.setIntField(objref, "count", n);
 159
 160     return objref;
 161
 162   }
 163
 164   @MJI
 165   public int toString____Ljava_lang_String_2 (MJIEnv env, int objref) {
 166     int aref = env.getReferenceField(objref, "value");
 167     int count = env.getIntField(objref, "count");
 168
 169     char[] buf = env.getCharArrayObject(aref);
 170     String s = new String(buf, 0, count);
 171     return env.newString(s);
 172   }
 173 }