Finalizing the beta version of the implementation for Groovy extension in JPF: JPF...
[jpf-core.git] / src / main / gov / nasa / jpf / vm / Types.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.JPFException;
21
22 import java.lang.reflect.Method;
23 import java.util.ArrayList;
24
25
26 /**
27  * various type mangling/demangling routines
28  *
29  * This reflects the general type id mess in Java. We support the following:
30  *
31  *  builtin type: byte - T_BOOLEAN and the like
32  *  type name: String - according to JLS 6.7 ("int", "x.Y[]")
33  *  type signature: String - like JNI ("I", "[Lx/Y;")
34  *  type classname: String - e.g. "int", "[I", "x.Y", "[Lx.Y;"
35  */
36 public class Types {
37
38   // these have the same values as the BCEL Constants since we don't want to break compiled code
39   public static final byte T_NONE      = 0; // illegal type
40   
41   public static final byte T_BOOLEAN   = 4;
42   public static final byte T_BYTE      = 8;
43   public static final byte T_CHAR      = 5;
44   public static final byte T_SHORT     = 9;
45   public static final byte T_INT       = 10;
46   public static final byte T_LONG      = 11;
47   public static final byte T_FLOAT     = 6;
48   public static final byte T_DOUBLE    = 7;
49   public static final byte T_REFERENCE = 14;
50   public static final byte T_ARRAY     = 13;  // <2do> do we need this in addition to T_REFERENCE?
51   public static final byte T_VOID      = 12;
52
53   
54   public static byte[] getArgumentTypes (String signature) {
55     int i;
56     int j;
57     int nArgs;
58
59     for (i = 1, nArgs = 0; signature.charAt(i) != ')'; nArgs++) {
60       i += getTypeLength(signature, i);
61     }
62
63     byte[] args = new byte[nArgs];
64
65     for (i = 1, j = 0; j < nArgs; j++) {
66       int    end = i + getTypeLength(signature, i);
67       String arg = signature.substring(i, end);
68       i = end;
69
70       args[j] = getBuiltinTypeFromSignature(arg);
71     }
72
73     return args;
74   }
75
76   // TODO: Fix for Groovy's model-checking
77   // TODO: We return the generic type name whenever possible (the one between '<' and '>')
78   // TODO: To do this we fixed the implementation of getTypeLength
79   public static String[] getArgumentTypeNames (String signature) {
80     int len = signature.length();
81
82     if ((len > 1) && (signature.charAt(1) == ')')) {
83       return new String[0]; // 'no args' shortcut
84     }
85     
86     ArrayList<String> a = new ArrayList<String>();
87
88     for (int i = 1; signature.charAt(i) != ')';) {
89       int end = i + getTypeLength(signature,i);
90       String arg = signature.substring(i, end);
91       i = end;
92
93       a.add(getTypeName(arg));
94     }
95
96     String[] typeNames = new String[a.size()];
97     a.toArray(typeNames);
98     
99     return typeNames;
100   }
101
102   public static String dequalify (String typeName){
103     int idx = typeName.lastIndexOf('.');
104     if (idx > 0) {
105       return typeName.substring(idx + 1);
106     } else {
107       return typeName;
108     }    
109   }
110   
111   public static String getDequalifiedMethodSignature (String mName){
112     int idx = mName.indexOf('(');
113     String sig = mName.substring(idx);
114     
115     return mName.substring(0, idx) + getDequalifiedArgumentSignature(sig);
116   }
117   
118   public static String getDequalifiedArgumentSignature (String sig){
119     String[] argTypes = getArgumentTypeNames(sig);
120     StringBuilder sb = new StringBuilder();
121     sb.append('(');
122     for (int i=0; i<argTypes.length; i++){
123       if (i>0){
124         sb.append(',');
125       }
126       sb.append(dequalify(argTypes[i]));
127     }
128     sb.append(')');
129     return sb.toString();
130   }
131   
132   public static String getDequalifiedTypeName (String sig){
133     String tn = getTypeName(sig);
134     return dequalify(tn);
135   }
136   
137   public static String getArgumentSignature (String[] typeNames, boolean qualified){
138     StringBuilder sb = new StringBuilder();
139     sb.append('(');
140     for (int i=0; i<typeNames.length; i++){
141       if (i>0){
142         sb.append(',');
143       }
144       
145       String tn = getTypeName(typeNames[i]);
146       if (!qualified){
147         int idx = tn.lastIndexOf('.');
148         if (idx >0){
149           tn = tn.substring(idx+1);
150         }
151       }
152       
153       sb.append( tn);
154     }
155     sb.append(')');
156     return sb.toString();
157   }
158   
159   /**
160    * get size in stack slots (ints), excluding this
161    */
162   public static int getArgumentsSize (String sig) {
163     int  n = 0;
164     for (int i = 1; sig.charAt(i) != ')'; i++) {
165       switch (sig.charAt(i)) {
166       case 'L':
167         do i++; while (sig.charAt(i) != ';');
168         n++;
169         break;
170       case '[':
171         do i++; while (sig.charAt(i) == '[');
172         if (sig.charAt(i) == 'L') {
173           do i++; while (sig.charAt(i) != ';');
174         }
175         n++;
176         break;
177       case 'J':
178       case 'D':
179         // the two-slot types
180         n += 2;
181         break;
182       default:
183         // just one slot entry
184         n++;
185       }
186     }
187     return n;
188   }
189
190   public static String getArrayElementType (String type) {
191     if (type.charAt(0) != '[') {
192       throw new JPFException("not an array type: " + type);
193     }
194
195     return type.substring(1);
196   }
197
198   public static String getComponentTerminal (String type) {
199     if (type.charAt(0) != '[') {
200       throw new JPFException("not an array type: " + type);
201     }
202
203     if(isReferenceSignature(type)) {
204       return type.substring(type.indexOf('L') + 1 , type.indexOf(';'));
205     } else {
206       return type.substring(type.lastIndexOf('[') + 1);
207     }
208   }
209
210   public static byte getBuiltinTypeFromSignature (String signature) {
211     switch (signature.charAt(0)) {
212     case 'B':
213       return T_BYTE;
214
215     case 'C':
216       return T_CHAR;
217
218     case 'D':
219       return T_DOUBLE;
220
221     case 'F':
222       return T_FLOAT;
223
224     case 'I':
225       return T_INT;
226
227     case 'J':
228       return T_LONG;
229
230     case 'L':
231       return T_REFERENCE;
232
233     case 'S':
234       return T_SHORT;
235
236     case 'V':
237       return T_VOID;
238
239     case 'Z':
240       return T_BOOLEAN;
241
242     case '[':
243       return T_ARRAY;
244     }
245
246     throw new JPFException("invalid type string: " + signature);
247   }
248
249   /**
250    * get the argument type part of the signature out of a
251    * JNI mangled method name.
252    * Note this is not the complete signature, since we don't have a
253    * return type (which is superfluous since it's not overloading,
254    * but unfortunately part of the signature in the class file)
255    */
256   public static String getJNISignature (String mangledName) {
257     int    i = mangledName.indexOf("__");
258     String sig = null;
259
260     if (i > 0) {
261       int k = 0;      
262       int r = mangledName.indexOf("__", i+2); // maybe there is a return type part
263       boolean gotReturnType = false;
264       int len = mangledName.length();
265       char[] buf = new char[len + 2];
266
267       buf[k++] = '(';
268
269       for (i += 2; i < len; i++) {
270
271         if (i == r) { // here comes the return type part (that's not JNI, only MJI
272           if ((i + 2) < len) {
273             i++;
274             buf[k++] = ')';
275             gotReturnType = true;
276             continue;
277           } else {
278             break;
279           }
280         }
281         
282         char c = mangledName.charAt(i);
283         if (c == '_') {
284           i++;
285
286           if (i < len) {
287             c = mangledName.charAt(i);
288
289             switch (c) {
290             case '1':
291               buf[k++] = '_';
292
293               break;
294
295             case '2':
296               buf[k++] = ';';
297
298               break;
299
300             case '3':
301               buf[k++] = '[';
302
303               break;
304
305             default:
306               buf[k++] = '/';
307               buf[k++] = c;
308             }
309           } else {
310             buf[k++] = '/';
311           }
312         } else {
313           buf[k++] = c;
314         }
315       }
316
317       if (!gotReturnType) {
318         // if there was no return type spec, assume 'void'
319         buf[k++] = ')';
320         buf[k++] = 'V';
321       }
322         
323       sig = new String(buf, 0, k);
324     }
325
326     // Hmm, maybe we should return "()V" instead of null, but that seems a bit too assuming
327     return sig;
328   }
329
330   public static String getJNIMangledMethodName (Method m) {
331     String      name = m.getName();
332     Class<?>[]    pt = m.getParameterTypes();
333     StringBuilder  s = new StringBuilder(name.length() + (pt.length * 16));
334
335     s.append(name);
336     s.append("__");
337
338     // <2do> not very efficient, but we don't care for now
339     for (int i = 0; i < pt.length; i++) {
340       s.append(getJNITypeCode(pt[i].getName()));
341     }
342
343     // the return type part, which is not in JNI, but is required for
344     // handling covariant return types
345     Class<?> rt = m.getReturnType();
346     s.append("__");
347     s.append(getJNITypeCode(rt.getName()));
348     
349     return s.toString();
350   }
351
352   public static String getJNIMangledMethodName (String cls, String name,
353                                                 String signature) {
354     StringBuilder s = new StringBuilder(signature.length() + 10);
355     int           i;
356     char          c;
357     int           slen = signature.length();
358     
359     if (cls != null) {
360       s.append(cls.replace('.', '_'));
361     }
362
363     s.append(name);
364     s.append("__");
365
366     // as defined in the JNI specs
367     for (i = 1; i<slen; i++) {
368       c = signature.charAt(i);
369       switch (c) {
370       case '/':
371         s.append('_');
372         break;
373
374       case '_':
375         s.append("_1");
376         break;
377
378       case ';':
379         s.append("_2");
380         break;
381
382       case '[':
383         s.append("_3");
384         break;
385
386       case ')':
387         // the return type part - note this is not JNI, but saves us a lot of trouble with
388         // the covariant return types of Java 1.5        
389         s.append("__");
390         break;
391         
392       default:
393         s.append(c);
394       }
395     }
396
397     return s.toString();
398   }
399
400   /**
401    * return the name part of a JNI mangled method name (which is of
402    * course not completely safe - you should only use it if you know
403    * this is a JNI name)
404    */
405   public static String getJNIMethodName (String mangledName) {
406     // note that's the first '__' group, which marks the beginning of the arg types
407     int i = mangledName.indexOf("__");
408
409     if (i > 0) {
410       return mangledName.substring(0, i);
411     } else {
412       return mangledName;
413     }
414   }
415
416   /**
417    * type is supposed to be Class.getName conforming, i.e.
418    * 
419    * int    -> int
420    * int[]  -> [I
421    * String -> java/lang/String
422    * String[] -> [Ljava/lang/String;
423    * String[][] -> [[Ljava/lang/String;
424    * 
425    * <2do> this is really not very efficient
426    */
427   public static String getJNITypeCode (String type) {
428     StringBuilder sb = new StringBuilder(32);
429     int l = type.length() - 1;
430     int i;
431
432     // Class.getName arrays "[...type"
433     for ( i=0; type.charAt(i) == '['; i++){
434       sb.append("_3");
435     }
436     
437     // conventional arrays "type[]..."
438     for (; type.charAt(l) == ']'; l -= 2) {
439       sb.append("_3");
440     }
441
442     type = type.substring(i, l + 1);
443
444     if (type.equals("int") || type.equals("I")) {
445       sb.append('I');
446     } else if (type.equals("long") || type.equals("J")) {
447       sb.append('J');
448     } else if (type.equals("boolean") || type.equals("Z")) {
449       sb.append('Z');
450     } else if (type.equals("char") || type.equals("C")) {
451       sb.append('C');
452     } else if (type.equals("byte")  || type.equals("B")) {
453       sb.append('B');
454     } else if (type.equals("short") || type.equals("S")) {
455       sb.append('S');
456     } else if (type.equals("double") || type.equals("D")) {
457       sb.append('D');
458     } else if (type.equals("float") || type.equals("F")) {
459       sb.append('F');
460     } else if (type.equals("void") || type.equals("V")) {  // for return types
461       sb.append('V');
462     } else { // reference type
463       if (type.charAt(0) != 'L'){
464         sb.append('L');
465       }
466
467       l = type.length();
468       for (i=0; i < l; i++) {
469         char c = type.charAt(i);
470
471         switch (c) {
472         case '.':
473           sb.append('_');
474           break;
475
476         case '_':
477           sb.append("_1");
478           break;
479           
480         case ';':
481           break;
482           
483         default:
484           sb.append(c);
485         }
486       }
487
488       sb.append("_2");
489       
490     }
491
492     return sb.toString();
493   }
494
495   // this includes the return type part
496   public static int getNumberOfStackSlots (String signature, boolean isStatic) {
497     int nArgSlots = 0;
498     int n = isStatic ? 0 : 1;
499     int sigLen = signature.length();
500
501     for (int i = 1; i < sigLen; i++) {
502       switch (signature.charAt(i)) {
503       case ')' : // end of arg part, but there still might be a return type
504         nArgSlots = n;
505         n = 0;
506         break;
507       case 'L':   // reference = 1 slot
508         i = signature.indexOf(';', i);
509         n++;
510         break;
511       case '[':
512         do i++; while (signature.charAt(i) == '[');
513         if (signature.charAt(i) == 'L') {
514           i = signature.indexOf(';', i);
515         }
516         n++;
517         break;
518       case 'J':
519       case 'D':
520         n+=2;
521         break;
522       default:
523         n++;
524       }
525     }
526     
527     return Math.max(n, nArgSlots);
528   }
529   
530   public static int getNumberOfArguments (String signature) {
531     int  i,n;
532     int sigLen = signature.length();
533
534     for (i = 1, n = 0; i<sigLen; n++) {
535       switch (signature.charAt(i)) {
536       case ')' :
537         return n;
538       case 'L':
539         do i++; while (signature.charAt(i) != ';');
540         break;
541
542       case '[':
543         do i++; while (signature.charAt(i) == '[');
544         if (signature.charAt(i) == 'L') {
545           do i++; while (signature.charAt(i) != ';');
546         }
547         break;
548
549       default:
550         // just a single type char
551       }
552
553       i++;
554     }
555
556     assert (false) : "malformed signature: " + signature;
557     return n; // that would be a malformed signature
558   }
559
560   public static boolean isReferenceSignature(String signature){
561     return signature.charAt(signature.length()-1) == ';';
562   }
563
564   public static boolean isReference (String type) {
565     int t = getBuiltinTypeFromSignature(type);
566
567     return (t == T_ARRAY) || (t == T_REFERENCE);
568   }
569
570   public static boolean isArray (String type) {
571     int t = getBuiltinTypeFromSignature(type);
572
573     return (t == T_ARRAY);
574   }
575
576   public static byte getReturnBuiltinType (String signature) {
577     int i = signature.indexOf(')');
578
579     return getBuiltinTypeFromSignature(signature.substring(i + 1));
580   }
581
582   public static String getReturnTypeSignature(String signature){
583     int i = signature.indexOf(')');
584     return signature.substring(i + 1);
585   }
586
587   public static String getReturnTypeName (String signature){
588     int i = signature.indexOf(')');
589     return getTypeName(signature.substring(i+1));
590   }
591
592   public static String getGenericReturnTypeName (String signature){
593     int i = signature.indexOf(')');
594     return getTypeName(signature.substring(i+1));
595   }
596   
597   public static String getTypeSignature (String type, boolean asDotNotation) {
598     String  t = null;
599     int arrayDim = 0;
600     
601     type = asDotNotation ? type.replace('/', '.') : type.replace('.', '/');
602     
603     if ((type.charAt(0) == '[') || (type.endsWith(";"))) {  // [[[L...;
604       t = type;
605       
606     } else {
607       
608       while (type.endsWith("[]")) { // type[][][]
609         type = type.substring(0, type.length() - 2);
610         arrayDim++;
611       }
612       
613       if (type.equals("byte")) {
614         t = "B";
615       } else if (type.equals("char")) {
616         t = "C";
617       } else if (type.equals("short")) {
618         t = "S";
619       } else if (type.equals("int")) {
620         t = "I";
621       } else if (type.equals("float")) {
622         t = "F";
623       } else if (type.equals("long")) {
624         t = "J";
625       } else if (type.equals("double")) {
626         t = "D";
627       } else if (type.equals("boolean")) {
628         t = "Z";
629       } else if (type.equals("void")) {
630         t = "V";
631       } else if (type.endsWith(";")) {
632         t = type;
633         
634       } else {
635         t = "L" + type + ';';
636       }
637       
638       while (arrayDim-- > 0) {
639         t = "[" + t;
640       }
641     }
642
643     return t;
644   }
645
646   public static byte getBuiltinType(String typeName){
647       if (typeName.equals("byte")) {
648         return T_BYTE;
649       } else if (typeName.equals("char")) {
650         return T_CHAR;
651       } else if (typeName.equals("short")) {
652         return T_SHORT;
653       } else if (typeName.equals("int")) {
654         return T_INT;
655       } else if (typeName.equals("float")) {
656         return T_FLOAT;
657       } else if (typeName.equals("long")) {
658         return T_LONG;
659       } else if (typeName.equals("double")) {
660         return T_DOUBLE;
661       } else if (typeName.equals("boolean")) {
662         return T_BOOLEAN;
663       } else if (typeName.equals("void")) {
664         return T_VOID;
665       } else {
666         if (typeName.charAt(typeName.length()-1) == ']'){
667           return T_ARRAY;
668         } else {
669           return T_REFERENCE;
670         }
671       }
672   }
673
674   public static String getBoxedType (byte type) {
675           switch (type) {
676           case Types.T_BOOLEAN:
677                   return "Boolean";
678           case Types.T_BYTE:
679                   return "Byte";
680           case Types.T_CHAR:
681                   return "Character";
682           case Types.T_SHORT:
683                   return "Short";
684           case Types.T_INT:
685                   return "Integer";
686           case Types.T_LONG:
687                   return "Long";
688           case Types.T_FLOAT:
689                   return "Float";
690           case Types.T_DOUBLE:
691                   return "Double";
692           default:
693                   return null;
694           }
695   }
696   
697   public static byte getUnboxedType (String typeName){
698     if (typeName.startsWith("java.lang.")){
699       typeName = typeName.substring(10);
700       if (typeName.equals("Boolean")){
701         return T_BOOLEAN;
702       } else if (typeName.equals("Byte")){
703         return T_BYTE;
704       } else if (typeName.equals("Character")){
705         return T_CHAR;
706       } else if (typeName.equals("Short")){
707         return T_SHORT;
708       } else if (typeName.equals("Integer")){
709         return T_INT;
710       } else if (typeName.equals("Long")){
711         return T_LONG;
712       } else if (typeName.equals("Float")){
713         return T_FLOAT;
714       } else if (typeName.equals("Double")){
715         return T_DOUBLE;
716       }
717     }
718     
719     // everything else can't be a box type
720     if (typeName.charAt(0) == '[' || typeName.charAt(typeName.length()-1) == ']'){
721       return T_ARRAY;
722     } else {
723       return T_REFERENCE;
724     }
725   }
726   
727   public static String getClassNameFromSignature (String signature){
728     if (signature.charAt(signature.length()-1) == ';'){ // reference
729       return signature.replace('/', '.');
730
731     } else { // builtin
732       switch (signature.charAt(0)){
733         case 'Z': return "boolean";
734         case 'B': return "byte";
735         case 'C': return "char";
736         case 'S': return "short";
737         case 'I': return "int";
738         case 'J': return "long";
739         case 'F': return "float";
740         case 'D': return "double";
741         default:
742           throw new JPFException("illegal type signature: " + signature);
743       }
744     }
745   }
746
747   /**
748    * get the canonical representation of a type name, which happens to be
749    *  (1) the name of the builtin type (e.g. "int")
750    *  (2) the normal dot name for ordinary classes (e.g. "java.lang.String")
751    *  (3) the coded dot name for arrays (e.g. "[B", "[[C", or "[Ljava.lang.String;")
752    *  
753    * not sure if we need to support internal class names (which use '/'
754    * instead of '.' as separators
755    *  
756    * no idea what's the logic behind this, but let's implement it
757    */
758   public static String getClassNameFromTypeName (String typeName) {
759     typeName = typeName.replace('/','.');
760     int n = typeName.length()-1;
761     
762     if (typeName.charAt(0) == '['){ // the "[<type>" notation
763       if (typeName.charAt(1) == 'L'){
764         if (typeName.charAt(n) != ';'){
765           typeName = typeName + ';';
766         }
767       }
768       
769       return typeName;
770     }
771     
772     int i=typeName.indexOf('[');
773     if (i>0){ // the sort of "<type>[]"
774       StringBuilder sb = new StringBuilder();
775       sb.append('[');
776       for (int j=i; (j=typeName.indexOf('[',j+1)) >0;){
777         sb.append('[');
778       }
779       
780       typeName = typeName.substring(0,i);
781       if (isBasicType(typeName)){
782         sb.append( getTypeSignature(typeName, true));
783       } else {
784         sb.append('L');
785         sb.append(typeName);
786         sb.append(';');
787       }
788       
789       return sb.toString();
790     }
791     
792     if (typeName.charAt(n) == ';') {
793       return typeName.substring(1,n);
794     }
795     
796     return typeName;
797   }
798
799   
800   public static boolean isTypeCode (String t) {
801     char c = t.charAt(0);
802
803     if (c == '[') {
804       return true;
805     }
806
807     if ((t.length() == 1) &&
808             ((c == 'B') || (c == 'I') || (c == 'S') || (c == 'C') ||
809               (c == 'F') || (c == 'J') || (c == 'D') || (c == 'Z'))) {
810       return true;
811     }
812
813     if (t.endsWith(";")) {
814       return true;
815     }
816
817     return false;
818   }
819
820   public static boolean isBasicType (String typeName){
821     return ("boolean".equals(typeName) ||
822         "byte".equals(typeName) ||
823         "char".equals(typeName) ||
824         "int".equals(typeName) ||
825         "long".equals(typeName) ||
826         "double".equals(typeName) ||
827         "short".equals(typeName) ||
828         "float".equals(typeName));
829   }
830
831   public static byte getTypeCode (String signature){
832     char c = signature.charAt(0);
833
834     switch (c) {
835       case 'B':
836         return T_BYTE;
837
838       case 'C':
839         return T_CHAR;
840
841       case 'D':
842         return T_DOUBLE;
843
844       case 'F':
845         return T_FLOAT;
846
847       case 'I':
848         return T_INT;
849
850       case 'J':
851         return T_LONG;
852
853       case 'L':
854         return T_REFERENCE;
855
856       case 'S':
857         return T_SHORT;
858
859       case 'V':
860         return T_VOID;
861
862       case 'Z':
863         return T_BOOLEAN;
864
865       case '[':
866         return T_ARRAY;
867
868       default:
869         throw new JPFException("unknow typecode: " + signature);
870     }
871   }
872   
873   /**
874    * return the qualified signature name according to JLS 6.7 (e.g. "int", "x.Y[]")
875    */
876   public static String getTypeName (String signature) {
877     int  len = signature.length();
878     char c = signature.charAt(0);
879
880     if (len == 1) {
881       switch (c) {
882       case 'B':
883         return "byte";
884
885       case 'C':
886         return "char";
887
888       case 'D':
889         return "double";
890
891       case 'F':
892         return "float";
893
894       case 'I':
895         return "int";
896
897       case 'J':
898         return "long";
899
900       case 'S':
901         return "short";
902
903       case 'V':
904         return "void";
905
906       case 'Z':
907         return "boolean";
908       }
909     }
910
911     if (c == '[') {
912       return getTypeName(signature.substring(1)) + "[]";
913     }
914
915     int len1 = len-1;
916     if (signature.charAt(len1) == ';') {
917       // TODO: Fix for Groovy's model-checking
918       // TODO: Cleaning up the generic type part inside '<' and '>'
919       return signature.substring(1, len1).replace('/', '.').
920               replaceAll(";L", ", ").
921               replace("<L","<").
922               replace(";>", ">").
923               replaceAll("<T", "<");
924     }
925
926
927
928     throw new JPFException("invalid type string: " + signature);
929   }
930
931   /** thoses are according to the arrayType codes of the newarray JVMS definition */
932   public static String getElementDescriptorOfType (int arrayType){
933     switch (arrayType){
934       case 4: return "Z";
935       case 5: return "C";
936       case 6: return "F";
937       case 7: return "D";
938       case 8: return "B";
939       case 9: return "S";
940       case 10: return "I";
941       case 11: return "J";
942     }
943     return null;
944   }
945
946   /**
947    * what would be the info size in bytes, not words
948    * (we ignore 64bit machines for now)
949    */
950   public static int getTypeSizeInBytes (String signature) {
951     switch (signature.charAt(0)) {
952       case 'V':
953         return 0;
954         
955       case 'Z': // that's a stretch, but we assume boolean uses the smallest addressable size
956       case 'B':
957         return 1;
958         
959       case 'S':
960       case 'C':
961         return 2;
962         
963       case 'L':
964       case '[':
965       case 'F':
966       case 'I':
967         return 4;
968         
969       case 'D':
970       case 'J':
971         return 8;
972     }
973
974     throw new JPFException("invalid type string: " + signature);
975   }
976   
977   public static int getTypeSize (String signature) {
978     switch (signature.charAt(0)) {
979     case 'V':
980       return 0;
981
982     case 'B':
983     case 'C':
984     case 'F':
985     case 'I':
986     case 'L':
987     case 'S':
988     case 'Z':
989     case '[':
990       return 1;
991
992     case 'D':
993     case 'J':
994       return 2;
995     }
996
997     throw new JPFException("invalid type string: " + signature);
998   }
999
1000   public static int getTypeSize (byte typeCategory){
1001     if (typeCategory == T_LONG || typeCategory == T_DOUBLE){
1002       return 2;
1003     } else {
1004       return 1;
1005     }
1006   }
1007   
1008   public static String asTypeName (String type) {
1009     if (type.startsWith("[") || type.endsWith(";")) {
1010       return getTypeName(type);
1011     }
1012
1013     return type;
1014   }
1015
1016   public static int booleanToInt (boolean b) {
1017     return b ? 1 : 0;
1018   }
1019
1020   public static long doubleToLong (double d) {
1021     return Double.doubleToLongBits(d);
1022   }
1023
1024   public static int floatToInt (float f) {
1025     return Float.floatToIntBits(f);
1026   }
1027
1028   public static int hiDouble (double d) {
1029     return hiLong(Double.doubleToLongBits(d));
1030   }
1031
1032   public static int hiLong (long l) {
1033     return (int) (l >> 32);
1034   }
1035
1036   public static boolean instanceOf (String type, String ofType) {
1037     int bType = getBuiltinTypeFromSignature(type);
1038
1039     if ((bType == T_ARRAY) && ofType.equals("Ljava/lang/Object;")) {
1040       return true;
1041     }
1042
1043     int bOfType = getBuiltinTypeFromSignature(ofType);
1044
1045     if (bType != bOfType) {
1046       return false;
1047     }
1048
1049     switch (bType) {
1050     case T_ARRAY:
1051       return instanceOf(type.substring(1), ofType.substring(1));
1052
1053     case T_REFERENCE:
1054       ClassInfo ci = ClassLoaderInfo.getCurrentResolvedClassInfo(getTypeName(type));
1055       return ci.isInstanceOf(getTypeName(ofType));
1056
1057     default:
1058       return true;
1059     }
1060   }
1061
1062   public static boolean intToBoolean (int i) {
1063     return i != 0;
1064   }
1065
1066   public static float intToFloat (int i) {
1067     return Float.intBitsToFloat(i);
1068   }
1069
1070   public static double intsToDouble (int l, int h) {
1071     long bits = ((long) h << 32) | (/*(long)*/ l & 0xFFFFFFFFL);
1072     return Double.longBitsToDouble(bits);
1073   }
1074
1075   public static long intsToLong (int l, int h) {
1076     return ((long) h << 32) | (/*(long)*/ l & 0xFFFFFFFFL);
1077   }
1078
1079   public static int loDouble (double d) {
1080     return loLong(Double.doubleToLongBits(d));
1081   }
1082
1083   public static int loLong (long l) {
1084     return (int) (l & 0xFFFFFFFFL);
1085   }
1086
1087   public static double longToDouble (long l) {
1088     return Double.longBitsToDouble(l);
1089   }
1090
1091   private static int getTypeLength (String signature, int idx) {
1092     switch (signature.charAt(idx)) {
1093     case 'B':
1094     case 'C':
1095     case 'D':
1096     case 'F':
1097     case 'I':
1098     case 'J':
1099     case 'S':
1100     case 'V':
1101     case 'Z':
1102       return 1;
1103
1104     case '[':
1105       return 1 + getTypeLength(signature, idx + 1);
1106
1107     case 'L':
1108
1109       int semicolon = signature.indexOf(';', idx);
1110       // TODO: Fix for Groovy's model-checking
1111       // Check if this is a generic!
1112       String currParam = signature.substring(idx,semicolon);
1113       int genericStart = currParam.indexOf('<');
1114       if (genericStart != -1) {
1115         if (currParam.charAt(genericStart + 1) == '*') {
1116           // Need to offset with idx to anticipate for array types (idx is incremented for array types)
1117           semicolon = genericStart + idx + 3;
1118         } else {
1119           int generic = signature.indexOf('>', semicolon);
1120           if (generic != -1) {
1121             // Advance one character past the ';'
1122             semicolon = generic + 1;
1123           }
1124         }
1125       }
1126
1127       if (semicolon == -1) {
1128         throw new JPFException("invalid type signature: " +
1129                                          signature);
1130       }
1131
1132       return semicolon - idx + 1;
1133     }
1134
1135     throw new JPFException("invalid type signature");
1136   }
1137
1138   /**
1139    * return the JPF internal representation of a method signature that is given
1140    * in dot-notation (like javap),
1141    *
1142    *  e.g.  "int foo(int[],java.lang.String)" -> "foo([ILjava/lang/String;)I"
1143    *
1144    */
1145   public static String getSignatureName (String methodDecl) {
1146
1147     StringBuffer sb = new StringBuffer(128);
1148     String retType = null;
1149
1150     int i = methodDecl.indexOf('(');
1151     if (i>0){
1152
1153       //--- name and return type
1154       String[] a = methodDecl.substring(0, i).split(" ");
1155       if (a.length > 0){
1156         sb.append(a[a.length-1]);
1157
1158         if (a.length > 1){
1159           retType = getTypeSignature(a[a.length-2], false);
1160         }
1161       }
1162
1163       //--- argument types
1164       int j = methodDecl.lastIndexOf(')');
1165       if (j > 0){
1166         sb.append('(');
1167         for (String type : methodDecl.substring(i+1,j).split(",")){
1168           if (!type.isEmpty()){
1169             type = type.trim();
1170             if (!type.isEmpty()){
1171               sb.append( getTypeSignature(type,false));
1172             }
1173           }
1174         }
1175         sb.append(')');
1176
1177         if (retType != null){
1178           sb.append(retType);
1179         }
1180
1181         return sb.toString();
1182       }
1183     }
1184
1185     throw new JPFException("invalid method declaration: " + methodDecl);
1186   }
1187
1188   // TODO: Fix for Groovy's model-checking
1189   public static String[] getGenericTypeVariableNames(String signature) {
1190     int pos = 0;
1191     int marker = 0;
1192     ArrayList<String> typeVarNames = new ArrayList<>();
1193
1194     while (pos < signature.length()) {
1195       if (pos > 0) {
1196         // Start from ';' if this is not the first type variable name
1197         marker = signature.indexOf(';', pos);
1198         // Break if this is the end of the type variable names
1199         if (signature.charAt(marker + 1) == '>')
1200           break;
1201       }
1202       int colon = signature.indexOf(':', pos);
1203       String typeVarName = signature.substring(marker + 1, colon);
1204       typeVarNames.add(typeVarName);
1205       pos = colon + 1;
1206     }
1207
1208     String[] arrTypeVarNames = new String[typeVarNames.size()];
1209     typeVarNames.toArray(arrTypeVarNames);
1210
1211     return arrTypeVarNames;
1212   }
1213
1214   public static String[] getParameterizedTypes(String signature) {
1215     int pos = signature.indexOf('<', 0);
1216     if (pos == -1)
1217       return new String[0];
1218     ArrayList<String> typeVarNames = new ArrayList<>();
1219
1220     while (pos < signature.length()) {
1221       String typeVarName = "";
1222       int comma = signature.indexOf(',', pos);
1223       if (comma == -1) {
1224         int closing = signature.lastIndexOf('>', signature.length());
1225         typeVarName = signature.substring(pos + 1, closing);
1226         pos = signature.length();
1227       } else {
1228         typeVarName = signature.substring(pos + 1, comma);
1229         pos = comma + 1;
1230       }
1231       typeVarNames.add(typeVarName);
1232     }
1233
1234     String[] arrTypeVarNames = new String[typeVarNames.size()];
1235     typeVarNames.toArray(arrTypeVarNames);
1236
1237     return arrTypeVarNames;
1238   }
1239
1240   public static String getGenericClassName(String signature) {
1241     int opening = signature.indexOf('<');
1242     if (opening == -1)
1243       return signature;
1244     else
1245       return signature.substring(0, opening);
1246   }
1247
1248   public static String getArrayClassName(String signature) {
1249     int opening = signature.indexOf('[');
1250     if (opening == -1)
1251       return signature;
1252     else
1253       return signature.substring(0, opening);
1254   }
1255
1256   public static String getOwnerClassName(String signature) {
1257     int marker = signature.indexOf('$');
1258     if (marker == -1)
1259       return null;
1260     else
1261       return signature.substring(0, marker);
1262   }
1263
1264   public static boolean isGenericSignature(String signature) {
1265     if (signature == null || signature.equals(""))
1266       return false;
1267     int opening = signature.indexOf('<');
1268     return (opening != -1);
1269   }
1270
1271   public static boolean isParameterizedType(String signature) {
1272     return Types.isGenericSignature(signature);
1273   }
1274
1275   public static boolean isArraySignature(String signature) {
1276     if (signature == null || signature.equals(""))
1277       return false;
1278     int opening = signature.indexOf('[');
1279     return (opening != -1);
1280   }
1281
1282   public static boolean isTypeParameter(String parameterizedType, String signature) {
1283     if (signature == null || signature.equals(""))
1284       return false;
1285     String typeParamSig = parameterizedType.concat(":");
1286     return signature.contains(typeParamSig);
1287   }
1288
1289   public static boolean isWildcardType(String signature) {
1290     return (signature.startsWith("+L") ||
1291             signature.startsWith("-L") ||
1292             signature.startsWith("+")  ||
1293             signature.startsWith("-")  ||
1294             signature.equals("*"));
1295   }
1296
1297   public static String getWildcardType(String signature) {
1298     if (signature.equals("*")) {
1299       return "java.lang.Object";
1300     }
1301     return signature.replaceAll("\\+L|-L", "");
1302   }
1303
1304   public static String getTypeParameter(String signature) {
1305     if (signature == null || signature.equals(""))
1306       return signature;
1307
1308     if (signature.equals("*")) {
1309       return signature;
1310     }
1311
1312     String cleanSig = signature.replaceAll("\\+|-", "");
1313     if (cleanSig.length()%2 != 0) {
1314       // This is probably a class, e.g., +java.lang.Class
1315       return signature;
1316     }
1317
1318     // Check if this is not a class name, e.g., +java.lang.Class
1319     if (cleanSig.contains(".")) {
1320       return signature;
1321     }
1322
1323     // Just return the second half of the signature to get the Type parameter
1324     int halfPos = cleanSig.length()/2;
1325     //String firstHalf = cleanSig.substring(0, halfPos);
1326     String secondHalf = cleanSig.substring(halfPos, cleanSig.length());
1327     return secondHalf;
1328   }
1329   // TODO: Fix for Groovy's model-checking
1330 }