131b7691ae5f505b7ffef6ba7a385d30e63944ae
[IRC.git] / 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 }