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