2 * Copyright (C) 2014, United States Government, as represented by the
3 * Administrator of the National Aeronautics and Space Administration.
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
10 * http://www.apache.org/licenses/LICENSE-2.0.
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.
18 package gov.nasa.jpf.vm;
20 import gov.nasa.jpf.JPFException;
22 import java.lang.reflect.Method;
23 import java.util.ArrayList;
27 * various type mangling/demangling routines
29 * This reflects the general type id mess in Java. We support the following:
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;"
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
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;
54 public static byte[] getArgumentTypes (String signature) {
59 for (i = 1, nArgs = 0; signature.charAt(i) != ')'; nArgs++) {
60 i += getTypeLength(signature, i);
63 byte[] args = new byte[nArgs];
65 for (i = 1, j = 0; j < nArgs; j++) {
66 int end = i + getTypeLength(signature, i);
67 String arg = signature.substring(i, end);
70 args[j] = getBuiltinTypeFromSignature(arg);
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();
82 if ((len > 1) && (signature.charAt(1) == ')')) {
83 return new String[0]; // 'no args' shortcut
86 ArrayList<String> a = new ArrayList<String>();
88 for (int i = 1; signature.charAt(i) != ')';) {
89 int end = i + getTypeLength(signature,i);
90 String arg = signature.substring(i, end);
93 a.add(getTypeName(arg));
96 String[] typeNames = new String[a.size()];
102 public static String dequalify (String typeName){
103 int idx = typeName.lastIndexOf('.');
105 return typeName.substring(idx + 1);
111 public static String getDequalifiedMethodSignature (String mName){
112 int idx = mName.indexOf('(');
113 String sig = mName.substring(idx);
115 return mName.substring(0, idx) + getDequalifiedArgumentSignature(sig);
118 public static String getDequalifiedArgumentSignature (String sig){
119 String[] argTypes = getArgumentTypeNames(sig);
120 StringBuilder sb = new StringBuilder();
122 for (int i=0; i<argTypes.length; i++){
126 sb.append(dequalify(argTypes[i]));
129 return sb.toString();
132 public static String getDequalifiedTypeName (String sig){
133 String tn = getTypeName(sig);
134 return dequalify(tn);
137 public static String getArgumentSignature (String[] typeNames, boolean qualified){
138 StringBuilder sb = new StringBuilder();
140 for (int i=0; i<typeNames.length; i++){
145 String tn = getTypeName(typeNames[i]);
147 int idx = tn.lastIndexOf('.');
149 tn = tn.substring(idx+1);
156 return sb.toString();
160 * get size in stack slots (ints), excluding this
162 public static int getArgumentsSize (String sig) {
164 for (int i = 1; sig.charAt(i) != ')'; i++) {
165 switch (sig.charAt(i)) {
167 do i++; while (sig.charAt(i) != ';');
171 do i++; while (sig.charAt(i) == '[');
172 if (sig.charAt(i) == 'L') {
173 do i++; while (sig.charAt(i) != ';');
179 // the two-slot types
183 // just one slot entry
190 public static String getArrayElementType (String type) {
191 if (type.charAt(0) != '[') {
192 throw new JPFException("not an array type: " + type);
195 return type.substring(1);
198 public static String getComponentTerminal (String type) {
199 if (type.charAt(0) != '[') {
200 throw new JPFException("not an array type: " + type);
203 if(isReferenceSignature(type)) {
204 return type.substring(type.indexOf('L') + 1 , type.indexOf(';'));
206 return type.substring(type.lastIndexOf('[') + 1);
210 public static byte getBuiltinTypeFromSignature (String signature) {
211 switch (signature.charAt(0)) {
246 throw new JPFException("invalid type string: " + signature);
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)
256 public static String getJNISignature (String mangledName) {
257 int i = mangledName.indexOf("__");
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];
269 for (i += 2; i < len; i++) {
271 if (i == r) { // here comes the return type part (that's not JNI, only MJI
275 gotReturnType = true;
282 char c = mangledName.charAt(i);
287 c = mangledName.charAt(i);
317 if (!gotReturnType) {
318 // if there was no return type spec, assume 'void'
323 sig = new String(buf, 0, k);
326 // Hmm, maybe we should return "()V" instead of null, but that seems a bit too assuming
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));
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()));
343 // the return type part, which is not in JNI, but is required for
344 // handling covariant return types
345 Class<?> rt = m.getReturnType();
347 s.append(getJNITypeCode(rt.getName()));
352 public static String getJNIMangledMethodName (String cls, String name,
354 StringBuilder s = new StringBuilder(signature.length() + 10);
357 int slen = signature.length();
360 s.append(cls.replace('.', '_'));
366 // as defined in the JNI specs
367 for (i = 1; i<slen; i++) {
368 c = signature.charAt(i);
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
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)
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("__");
410 return mangledName.substring(0, i);
417 * type is supposed to be Class.getName conforming, i.e.
421 * String -> java/lang/String
422 * String[] -> [Ljava/lang/String;
423 * String[][] -> [[Ljava/lang/String;
425 * <2do> this is really not very efficient
427 public static String getJNITypeCode (String type) {
428 StringBuilder sb = new StringBuilder(32);
429 int l = type.length() - 1;
432 // Class.getName arrays "[...type"
433 for ( i=0; type.charAt(i) == '['; i++){
437 // conventional arrays "type[]..."
438 for (; type.charAt(l) == ']'; l -= 2) {
442 type = type.substring(i, l + 1);
444 if (type.equals("int") || type.equals("I")) {
446 } else if (type.equals("long") || type.equals("J")) {
448 } else if (type.equals("boolean") || type.equals("Z")) {
450 } else if (type.equals("char") || type.equals("C")) {
452 } else if (type.equals("byte") || type.equals("B")) {
454 } else if (type.equals("short") || type.equals("S")) {
456 } else if (type.equals("double") || type.equals("D")) {
458 } else if (type.equals("float") || type.equals("F")) {
460 } else if (type.equals("void") || type.equals("V")) { // for return types
462 } else { // reference type
463 if (type.charAt(0) != 'L'){
468 for (i=0; i < l; i++) {
469 char c = type.charAt(i);
492 return sb.toString();
495 // this includes the return type part
496 public static int getNumberOfStackSlots (String signature, boolean isStatic) {
498 int n = isStatic ? 0 : 1;
499 int sigLen = signature.length();
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
507 case 'L': // reference = 1 slot
508 i = signature.indexOf(';', i);
512 do i++; while (signature.charAt(i) == '[');
513 if (signature.charAt(i) == 'L') {
514 i = signature.indexOf(';', i);
527 return Math.max(n, nArgSlots);
530 public static int getNumberOfArguments (String signature) {
532 int sigLen = signature.length();
534 for (i = 1, n = 0; i<sigLen; n++) {
535 switch (signature.charAt(i)) {
539 do i++; while (signature.charAt(i) != ';');
543 do i++; while (signature.charAt(i) == '[');
544 if (signature.charAt(i) == 'L') {
545 do i++; while (signature.charAt(i) != ';');
550 // just a single type char
556 assert (false) : "malformed signature: " + signature;
557 return n; // that would be a malformed signature
560 public static boolean isReferenceSignature(String signature){
561 return signature.charAt(signature.length()-1) == ';';
564 public static boolean isReference (String type) {
565 int t = getBuiltinTypeFromSignature(type);
567 return (t == T_ARRAY) || (t == T_REFERENCE);
570 public static boolean isArray (String type) {
571 int t = getBuiltinTypeFromSignature(type);
573 return (t == T_ARRAY);
576 public static byte getReturnBuiltinType (String signature) {
577 int i = signature.indexOf(')');
579 return getBuiltinTypeFromSignature(signature.substring(i + 1));
582 public static String getReturnTypeSignature(String signature){
583 int i = signature.indexOf(')');
584 return signature.substring(i + 1);
587 public static String getReturnTypeName (String signature){
588 int i = signature.indexOf(')');
589 return getTypeName(signature.substring(i+1));
592 public static String getGenericReturnTypeName (String signature){
593 int i = signature.indexOf(')');
594 return getTypeName(signature.substring(i+1));
597 public static String getTypeSignature (String type, boolean asDotNotation) {
601 type = asDotNotation ? type.replace('/', '.') : type.replace('.', '/');
603 if ((type.charAt(0) == '[') || (type.endsWith(";"))) { // [[[L...;
608 while (type.endsWith("[]")) { // type[][][]
609 type = type.substring(0, type.length() - 2);
613 if (type.equals("byte")) {
615 } else if (type.equals("char")) {
617 } else if (type.equals("short")) {
619 } else if (type.equals("int")) {
621 } else if (type.equals("float")) {
623 } else if (type.equals("long")) {
625 } else if (type.equals("double")) {
627 } else if (type.equals("boolean")) {
629 } else if (type.equals("void")) {
631 } else if (type.endsWith(";")) {
635 t = "L" + type + ';';
638 while (arrayDim-- > 0) {
646 public static byte getBuiltinType(String typeName){
647 if (typeName.equals("byte")) {
649 } else if (typeName.equals("char")) {
651 } else if (typeName.equals("short")) {
653 } else if (typeName.equals("int")) {
655 } else if (typeName.equals("float")) {
657 } else if (typeName.equals("long")) {
659 } else if (typeName.equals("double")) {
661 } else if (typeName.equals("boolean")) {
663 } else if (typeName.equals("void")) {
666 if (typeName.charAt(typeName.length()-1) == ']'){
674 public static String getBoxedType (byte type) {
676 case Types.T_BOOLEAN:
697 public static byte getUnboxedType (String typeName){
698 if (typeName.startsWith("java.lang.")){
699 typeName = typeName.substring(10);
700 if (typeName.equals("Boolean")){
702 } else if (typeName.equals("Byte")){
704 } else if (typeName.equals("Character")){
706 } else if (typeName.equals("Short")){
708 } else if (typeName.equals("Integer")){
710 } else if (typeName.equals("Long")){
712 } else if (typeName.equals("Float")){
714 } else if (typeName.equals("Double")){
719 // everything else can't be a box type
720 if (typeName.charAt(0) == '[' || typeName.charAt(typeName.length()-1) == ']'){
727 public static String getClassNameFromSignature (String signature){
728 if (signature.charAt(signature.length()-1) == ';'){ // reference
729 return signature.replace('/', '.');
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";
742 throw new JPFException("illegal type signature: " + signature);
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;")
753 * not sure if we need to support internal class names (which use '/'
754 * instead of '.' as separators
756 * no idea what's the logic behind this, but let's implement it
758 public static String getClassNameFromTypeName (String typeName) {
759 typeName = typeName.replace('/','.');
760 int n = typeName.length()-1;
762 if (typeName.charAt(0) == '['){ // the "[<type>" notation
763 if (typeName.charAt(1) == 'L'){
764 if (typeName.charAt(n) != ';'){
765 typeName = typeName + ';';
772 int i=typeName.indexOf('[');
773 if (i>0){ // the sort of "<type>[]"
774 StringBuilder sb = new StringBuilder();
776 for (int j=i; (j=typeName.indexOf('[',j+1)) >0;){
780 typeName = typeName.substring(0,i);
781 if (isBasicType(typeName)){
782 sb.append( getTypeSignature(typeName, true));
789 return sb.toString();
792 if (typeName.charAt(n) == ';') {
793 return typeName.substring(1,n);
800 public static boolean isTypeCode (String t) {
801 char c = t.charAt(0);
807 if ((t.length() == 1) &&
808 ((c == 'B') || (c == 'I') || (c == 'S') || (c == 'C') ||
809 (c == 'F') || (c == 'J') || (c == 'D') || (c == 'Z'))) {
813 if (t.endsWith(";")) {
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));
831 public static byte getTypeCode (String signature){
832 char c = signature.charAt(0);
869 throw new JPFException("unknow typecode: " + signature);
874 * return the qualified signature name according to JLS 6.7 (e.g. "int", "x.Y[]")
876 public static String getTypeName (String signature) {
877 int len = signature.length();
878 char c = signature.charAt(0);
912 return getTypeName(signature.substring(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", ", ").
923 replaceAll("<T", "<");
928 throw new JPFException("invalid type string: " + signature);
931 /** thoses are according to the arrayType codes of the newarray JVMS definition */
932 public static String getElementDescriptorOfType (int arrayType){
947 * what would be the info size in bytes, not words
948 * (we ignore 64bit machines for now)
950 public static int getTypeSizeInBytes (String signature) {
951 switch (signature.charAt(0)) {
955 case 'Z': // that's a stretch, but we assume boolean uses the smallest addressable size
974 throw new JPFException("invalid type string: " + signature);
977 public static int getTypeSize (String signature) {
978 switch (signature.charAt(0)) {
997 throw new JPFException("invalid type string: " + signature);
1000 public static int getTypeSize (byte typeCategory){
1001 if (typeCategory == T_LONG || typeCategory == T_DOUBLE){
1008 public static String asTypeName (String type) {
1009 if (type.startsWith("[") || type.endsWith(";")) {
1010 return getTypeName(type);
1016 public static int booleanToInt (boolean b) {
1020 public static long doubleToLong (double d) {
1021 return Double.doubleToLongBits(d);
1024 public static int floatToInt (float f) {
1025 return Float.floatToIntBits(f);
1028 public static int hiDouble (double d) {
1029 return hiLong(Double.doubleToLongBits(d));
1032 public static int hiLong (long l) {
1033 return (int) (l >> 32);
1036 public static boolean instanceOf (String type, String ofType) {
1037 int bType = getBuiltinTypeFromSignature(type);
1039 if ((bType == T_ARRAY) && ofType.equals("Ljava/lang/Object;")) {
1043 int bOfType = getBuiltinTypeFromSignature(ofType);
1045 if (bType != bOfType) {
1051 return instanceOf(type.substring(1), ofType.substring(1));
1054 ClassInfo ci = ClassLoaderInfo.getCurrentResolvedClassInfo(getTypeName(type));
1055 return ci.isInstanceOf(getTypeName(ofType));
1062 public static boolean intToBoolean (int i) {
1066 public static float intToFloat (int i) {
1067 return Float.intBitsToFloat(i);
1070 public static double intsToDouble (int l, int h) {
1071 long bits = ((long) h << 32) | (/*(long)*/ l & 0xFFFFFFFFL);
1072 return Double.longBitsToDouble(bits);
1075 public static long intsToLong (int l, int h) {
1076 return ((long) h << 32) | (/*(long)*/ l & 0xFFFFFFFFL);
1079 public static int loDouble (double d) {
1080 return loLong(Double.doubleToLongBits(d));
1083 public static int loLong (long l) {
1084 return (int) (l & 0xFFFFFFFFL);
1087 public static double longToDouble (long l) {
1088 return Double.longBitsToDouble(l);
1091 private static int getTypeLength (String signature, int idx) {
1092 switch (signature.charAt(idx)) {
1105 return 1 + getTypeLength(signature, idx + 1);
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;
1119 int generic = signature.indexOf('>', semicolon);
1120 if (generic != -1) {
1121 // Advance one character past the ';'
1122 semicolon = generic + 1;
1127 if (semicolon == -1) {
1128 throw new JPFException("invalid type signature: " +
1132 return semicolon - idx + 1;
1135 throw new JPFException("invalid type signature");
1139 * return the JPF internal representation of a method signature that is given
1140 * in dot-notation (like javap),
1142 * e.g. "int foo(int[],java.lang.String)" -> "foo([ILjava/lang/String;)I"
1145 public static String getSignatureName (String methodDecl) {
1147 StringBuffer sb = new StringBuffer(128);
1148 String retType = null;
1150 int i = methodDecl.indexOf('(');
1153 //--- name and return type
1154 String[] a = methodDecl.substring(0, i).split(" ");
1156 sb.append(a[a.length-1]);
1159 retType = getTypeSignature(a[a.length-2], false);
1163 //--- argument types
1164 int j = methodDecl.lastIndexOf(')');
1167 for (String type : methodDecl.substring(i+1,j).split(",")){
1168 if (!type.isEmpty()){
1170 if (!type.isEmpty()){
1171 sb.append( getTypeSignature(type,false));
1177 if (retType != null){
1181 return sb.toString();
1185 throw new JPFException("invalid method declaration: " + methodDecl);
1188 // TODO: Fix for Groovy's model-checking
1189 public static String[] getGenericTypeVariableNames(String signature) {
1192 ArrayList<String> typeVarNames = new ArrayList<>();
1194 while (pos < signature.length()) {
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) == '>')
1202 int colon = signature.indexOf(':', pos);
1203 String typeVarName = signature.substring(marker + 1, colon);
1204 typeVarNames.add(typeVarName);
1208 String[] arrTypeVarNames = new String[typeVarNames.size()];
1209 typeVarNames.toArray(arrTypeVarNames);
1211 return arrTypeVarNames;
1214 // TODO: Fix for Groovy's model-checking
1215 public static String[] getParameterizedTypes(String signature) {
1216 int pos = signature.indexOf('<', 0);
1218 return new String[0];
1219 ArrayList<String> typeVarNames = new ArrayList<>();
1221 while (pos < signature.length()) {
1222 String typeVarName = "";
1223 int comma = signature.indexOf(',', pos);
1225 int closing = signature.lastIndexOf('>', signature.length());
1226 typeVarName = signature.substring(pos + 1, closing);
1227 pos = signature.length();
1229 typeVarName = signature.substring(pos + 1, comma);
1232 typeVarNames.add(typeVarName);
1235 String[] arrTypeVarNames = new String[typeVarNames.size()];
1236 typeVarNames.toArray(arrTypeVarNames);
1238 return arrTypeVarNames;
1241 public static String getGenericClassName(String signature) {
1242 int opening = signature.indexOf('<');
1246 return signature.substring(0, opening);
1249 public static String getArrayClassName(String signature) {
1250 int opening = signature.indexOf('[');
1254 return signature.substring(0, opening);
1257 public static String getOwnerClassName(String signature) {
1258 int marker = signature.indexOf('$');
1262 return signature.substring(0, marker);
1265 public static boolean isGenericSignature(String signature) {
1266 if (signature == null || signature.equals(""))
1268 int opening = signature.indexOf('<');
1269 return (opening != -1);
1272 public static boolean isParameterizedType(String signature) {
1273 return Types.isGenericSignature(signature);
1276 public static boolean isArraySignature(String signature) {
1277 if (signature == null || signature.equals(""))
1279 int opening = signature.indexOf('[');
1280 return (opening != -1);
1283 public static boolean isTypeParameter(String parameterizedType, String signature) {
1284 if (signature == null || signature.equals(""))
1286 String typeParamSig = parameterizedType.concat(":");
1287 return signature.contains(typeParamSig);
1290 public static boolean isWildcardType(String signature) {
1291 return (signature.startsWith("+L") ||
1292 signature.startsWith("-L") ||
1293 signature.startsWith("+") ||
1294 signature.startsWith("-") ||
1295 signature.equals("*"));
1298 public static String getWildcardType(String signature) {
1299 if (signature.equals("*")) {
1300 return "java.lang.Object";
1302 return signature.replaceAll("\\+L|-L", "");
1305 public static String getTypeParameter(String signature) {
1306 if (signature == null || signature.equals(""))
1309 if (signature.equals("*")) {
1313 String cleanSig = signature.replaceAll("\\+|-", "");
1314 // This kind of signature should be a repetition of its class' type parameter, e.g., TT for Class<T>
1315 if (cleanSig.length()%2 != 0) {
1316 // This is probably a class, e.g., +java.lang.Class
1320 // Check that the first and the second halves are the same, e.g., TT for Class<T>
1321 int halfPos = cleanSig.length()/2;
1322 String firstHalf = cleanSig.substring(0, halfPos);
1323 String secondHalf = cleanSig.substring(halfPos, cleanSig.length());
1324 if (firstHalf.equals(secondHalf)) {
1327 // This is probably a class, e.g., +java.lang.Class
1331 // TODO: Fix for Groovy's model-checking