Robust/src/ClassLibrary/SSJava/String.java

   1 import Object;
   2 import String;
   3 import StringBuffer;
   4 import System;
   5
   6 @LATTICE("V<C, V<O")
   7 @METHODDEFAULT("O<V,V<C,C<IN,THISLOC=O,C*")
   8 public class String {
   9
  10   @LOC("V") char value[];
  11   @LOC("C") int count;
  12   @LOC("O") int offset;
  13   @LOC("V") private int cachedHashcode;
  14
  15   private String() {
  16   }
  17
  18   public String(byte str[]) {
  19     char charstr[]=new char[str.length];
  20     for(int i=0; i<str.length; i++)
  21       charstr[i]=(char)str[i];
  22     this.value=charstr;
  23     this.count=str.length;
  24     this.offset=0;
  25   }
  26
  27   public String(char str[], int offset, int length) {
  28     if (length>(str.length-offset))
  29       length=str.length-offset;
  30     char charstr[]=new char[length];
  31     for(int i=0; i<length; i++)
  32       charstr[i]=str[i+offset];
  33     this.value=charstr;
  34     this.count=length;
  35     this.offset=0;
  36   }
  37
  38
  39   public String(byte str[], String encoding) {
  40     int length = this.count;
  41     if (length>(str.length))
  42       length=str.length;
  43     char charstr[]=new char[length];
  44     for(int i=0; i<length; i++)
  45       charstr[i]=(char)str[i];
  46     this.value=charstr;
  47     this.count=length;
  48     this.offset=0;
  49   }
  50
  51   public String(@LOC("IN") String str) {
  52     this.value=str.value;
  53     this.count=str.count;
  54     this.offset=str.offset;
  55   }
  56
  57   public String(StringBuffer strbuf) {
  58     value=new char[strbuf.length()];
  59     count=strbuf.length();
  60     offset=0;
  61     for(int i=0; i<count; i++)
  62       value[i]=strbuf.value[i];
  63   }
  64
  65   public String(@LOC("IN") char c) {
  66     @LOC("V") char[] str = new char[1];
  67     str[0] = c;
  68     String(str);
  69   }
  70
  71   public String(@LOC("IN") char str[]) {
  72     @LOC("V") char charstr[]=new char[str.length];
  73     for(@LOC("C") int i=0; i<str.length; i++)
  74       charstr[i]=str[i];
  75     this.value=charstr;
  76     charstr=null;
  77     this.count=str.length;
  78     this.offset=0;
  79   }
  80
  81   public String(String str) {
  82     this.value=str.value;
  83     this.count=str.count;
  84     this.offset=str.offset;
  85   }
  86
  87   @LATTICE("O<V,V<C,C<IN,THISLOC=IN,C*")
  88   @RETURNLOC("O")
  89   public String concat(@LOC("IN") String str) {
  90     @LOC("O") String newstr=new String(); // create new one, it has OUT location
  91     @LOC("C") int newCount=this.count+str.count;
  92
  93     @LOC("V") char charstr[]=new char[newCount];
  94
  95     // here, for loop introduces indirect flow from [C] to [V]
  96     for(@LOC("C") int i=0; i<count; i++) {
  97       // value flows from GLB(THISLOC,C,THISLOC.V)=(THISLOC,TOP) to [V]
  98       charstr[i]=value[i+offset];
  99     }
 100     for(@LOC("C") int i=0; i<str.count; i++) {
 101       charstr[i+count]=str.value[i+str.offset];
 102     }
 103
 104     newstr.value=charstr;
 105     charstr=null;
 106     // LOC(newstr.value)=[O,V]
 107     // LOC(charstr)=[V]
 108     // [O,V] < [V]
 109
 110     return newstr;
 111   }
 112
 113   @RETURNLOC("O")
 114   public boolean equals(@LOC("IN") Object o) {
 115     if (o.getType()!=getType()) // values are coming from [IN] and [THISLOC]
 116       return false;
 117     @LOC("V") String s=(String)o;
 118     o=null;
 119     if (s.count!=count)
 120       return false;
 121     for(@LOC("C") int i=0; i<count; i++) {
 122       if (s.value[i+s.offset]!=value[i+offset])
 123         return false;
 124     }
 125     return true;
 126   }
 127
 128   public void getChars(char dst[], int dstBegin) {
 129     getChars(0, count, dst, dstBegin);
 130   }
 131
 132   public void getChars(int srcBegin, int srcEnd, char dst[], int dstBegin) {
 133     if((srcBegin < 0) || (srcEnd > count) || (srcBegin > srcEnd)) {
 134       // FIXME
 135       System.printString("Index error: "+srcBegin+" "+srcEnd+" "+count+"\n"+this);
 136       System.exit(-1);
 137     }
 138     int len = srcEnd - srcBegin;
 139     int j = dstBegin;
 140     for(int i=srcBegin; i<srcEnd; i++)
 141       dst[j++]=value[i+offset];
 142     return;
 143   }
 144
 145   public int indexOf(String str, int fromIndex) {
 146     if (fromIndex<0)
 147       fromIndex=0;
 148     for(int i=fromIndex; i<=(count-str.count); i++)
 149       if (regionMatches(i, str, 0, str.count))
 150         return i;
 151     return -1;
 152   }
 153
 154   public boolean regionMatches(int toffset, String other, int ooffset, int len) {
 155     if (toffset<0 || ooffset <0 || (toffset+len)>count || (ooffset+len)>other.count)
 156       return false;
 157     for(int i=0; i<len; i++)
 158       if (other.value[i+other.offset+ooffset]!=
 159           this.value[i+this.offset+toffset])
 160         return false;
 161     return true;
 162   }
 163
 164   @RETURNLOC("O")
 165   public static String valueOf(@LOC("IN") Object o) {
 166     if (o==null)
 167       return "null";
 168     else
 169       return o.toString();
 170   }
 171
 172   public static String valueOf(boolean b) {
 173     if (b)
 174       return new String("true");
 175     else
 176       return new String("false");
 177   }
 178
 179   public static String valueOf(char c) {
 180     char ar[]=new char[1];
 181     ar[0]=c;
 182     return new String(ar);
 183   }
 184
 185   public static String valueOf(int x) {
 186     int length=0;
 187     int tmp;
 188     if (x<0)
 189       tmp=-x;
 190     else
 191       tmp=x;
 192     do {
 193       tmp=tmp/10;
 194       length=length+1;
 195     } while(tmp!=0);
 196
 197     char chararray[];
 198     if (x<0)
 199       chararray=new char[length+1];
 200     else
 201       chararray=new char[length];
 202     int voffset;
 203     if (x<0) {
 204       chararray[0]='-';
 205       voffset=1;
 206       x=-x;
 207     } else
 208       voffset=0;
 209
 210     do {
 211       chararray[--length+voffset]=(char)(x%10+'0');
 212       x=x/10;
 213     } while (length!=0);
 214     return new String(chararray);
 215   }
 216
 217   public static String valueOf(double val) {
 218     char[] chararray=new char[20];
 219     String s=new String();
 220     s.offset=0;
 221     s.count=convertdoubletochar(val, chararray);
 222     s.value=chararray;
 223     return s;
 224   }
 225
 226   public static native int convertdoubletochar(double val, char [] chararray);
 227
 228
 229   public static String valueOf(long x) {
 230     int length=0;
 231     long tmp;
 232     if (x<0)
 233       tmp=-x;
 234     else
 235       tmp=x;
 236     do {
 237       tmp=tmp/10;
 238       length=length+1;
 239     } while(tmp!=0);
 240
 241     char chararray[];
 242     if (x<0)
 243       chararray=new char[length+1];
 244     else
 245       chararray=new char[length];
 246     int voffset;
 247     if (x<0) {
 248       chararray[0]='-';
 249       voffset=1;
 250       x=-x;
 251     } else
 252       voffset=0;
 253
 254     do {
 255       chararray[--length+voffset]=(char)(x%10+'0');
 256       x=x/10;
 257     } while (length!=0);
 258     return new String(chararray);
 259   }
 260
 261   @LATTICE("O<V,V<C,C<IN,THISLOC=IN,C*")
 262   @RETURNLOC("O")
 263   public byte[] getBytes() {
 264     @LOC("V") byte str[]=new byte[count];
 265     for(@LOC("C") int i=0; i<count; i++)
 266       str[i]=(byte)value[i+offset];
 267     return str;
 268   }
 269
 270
 271
 272   @RETURNLOC("IN")
 273   public int length() {
 274     return count;
 275   }
 276
 277   @RETURNLOC("O")
 278   public char charAt(@LOC("IN") int index){
 279     return value[index];
 280   }
 281
 282     //public static native int convertdoubletochar(double val, char [] chararray);
 283
 284 }