0001: // This file is part of KeY - Integrated Deductive Software Design
0002: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
0003: // Universitaet Koblenz-Landau, Germany
0004: // Chalmers University of Technology, Sweden
0005: //
0006: // The KeY system is protected by the GNU General Public License.
0007: // See LICENSE.TXT for details.
0008: //
0009: //
0010: package de.uka.ilkd.key.java;
0011:
0012: import java.util.HashMap;
0013: import java.util.HashSet;
0014: import java.util.Iterator;
0015: import java.util.Set;
0016:
0017: import de.uka.ilkd.key.java.abstraction.*;
0018: import de.uka.ilkd.key.java.declaration.*;
0019: import de.uka.ilkd.key.java.expression.literal.NullLiteral;
0020: import de.uka.ilkd.key.java.reference.ExecutionContext;
0021: import de.uka.ilkd.key.java.reference.TypeRef;
0022: import de.uka.ilkd.key.java.reference.TypeReference;
0023: import de.uka.ilkd.key.logic.*;
0024: import de.uka.ilkd.key.logic.ldt.*;
0025: import de.uka.ilkd.key.logic.op.*;
0026: import de.uka.ilkd.key.logic.sort.ArraySort;
0027: import de.uka.ilkd.key.logic.sort.IteratorOfSort;
0028: import de.uka.ilkd.key.logic.sort.ObjectSort;
0029: import de.uka.ilkd.key.logic.sort.Sort;
0030: import de.uka.ilkd.key.util.Debug;
0031: import de.uka.ilkd.key.util.LRUCache;
0032:
0033: /**
0034: * an instance serves as representation of a Java model underlying a DL
0035: * formula. This class provides calls to access the elements of the Java
0036: * model using the KeY datastructures only. Implementation specific
0037: * details like the use of Recoder is hidden in the field of type
0038: * {@link KeYProgModelInfo}. This class can be extended to provide further
0039: * services.
0040: */
0041: public class JavaInfo {
0042:
0043: public class CacheKey {
0044: Object o1;
0045: Object o2;
0046:
0047: public CacheKey(KeYJavaType k1, KeYJavaType k2) {
0048: assert k1 != null && k2 != null;
0049: o1 = k1;
0050: o2 = k2;
0051: }
0052:
0053: public boolean equals(Object o) {
0054: if (o instanceof CacheKey) {
0055: final CacheKey snd = (CacheKey) o;
0056: return snd.o1.equals(o1) && snd.o2.equals(o2);
0057: }
0058: return false;
0059: }
0060:
0061: public int hashCode() {
0062: return o1.hashCode() + o2.hashCode();
0063: }
0064:
0065: }
0066:
0067: private Services services;
0068: private KeYProgModelInfo kpmi;
0069: private String javaSourcePath;
0070:
0071: /**
0072: * the type of null
0073: */
0074: private KeYJavaType nullType = null;
0075:
0076: /**
0077: * as accessed very often caches:
0078: * KeYJavaType of
0079: * java.lang.Object, java.lang.Clonable, java.io.Serializable
0080: * in </em>in this order</em>
0081: */
0082: private KeYJavaType[] commonTypes = new KeYJavaType[3];
0083:
0084: //some caches for the getKeYJavaType methods.
0085: private HashMap sort2KJTCache = null;
0086: private HashMap type2KJTCache = null;
0087: private HashMap name2KJTCache = null;
0088: private HashMap sName2KJTCache = null;
0089:
0090: private LRUCache commonSubtypeCache = new LRUCache(200);
0091:
0092: private int nameCachedSize = 0;
0093: private int sNameCachedSize = 0;
0094: private int sortCachedSize = 0;
0095:
0096: /**
0097: * The default execution context is for the case of program statements on
0098: * the top level. It is equivalent to a static class belonging the default
0099: * package. This should only be used when using KeY in academic mode, if
0100: * the verification conditions are generated they "must" start with a
0101: * {@link de.uka.ilkd.key.java.statement.MethodBodyStatement} or a
0102: * {@link de.uka.ilkd.key.java.statement.MethodFrame}, which contains a
0103: * valid execution context.
0104: */
0105: private ExecutionContext defaultExecutionContext;
0106:
0107: /**
0108: * a term with the constant 'null'
0109: */
0110: private Term nullConst = null;
0111: private boolean commonTypesCacheValid;
0112:
0113: /** caches the predicate used to express a lega java state */
0114: private Function legalHeapStructure;
0115:
0116: /** caches the arrays' length attribute*/
0117: private ProgramVariable length;
0118:
0119: /** the name of the class used as default execution context */
0120: static final String DEFAULT_EXECUTION_CONTEXT_CLASS = "<Default>";
0121:
0122: /**
0123: * creates a new JavaInfo object by giving a KeYProgModelInfo to access
0124: * the Recoder SourceInfo and using the given {@link Services} object.
0125: */
0126: JavaInfo(KeYProgModelInfo kpmi, Services s) {
0127: this .kpmi = kpmi;
0128: services = s;
0129: }
0130:
0131: private JavaInfo(JavaInfo proto, Services s) {
0132: this (proto.getKeYProgModelInfo().copy(), s);
0133: nullType = proto.getNullType();
0134: nullConst = proto.getNullConst();
0135: }
0136:
0137: /**
0138: * returns the underlying KeYProgModelInfo providing access to the
0139: * Recoder structures.
0140: */
0141: public KeYProgModelInfo getKeYProgModelInfo() {
0142: return kpmi;
0143: }
0144:
0145: void setKeYProgModelInfo(KeYProgModelInfo kpmi) {
0146: this .kpmi = kpmi;
0147: }
0148:
0149: /**
0150: * convenience method that returns the Recoder-to-KeY mapping underlying
0151: * the KeYProgModelInfo of this JavaInfo
0152: */
0153: public KeYRecoderMapping rec2key() {
0154: return getKeYProgModelInfo().rec2key();
0155: }
0156:
0157: /**
0158: * copies this JavaInfo and uses the given Services object as the
0159: * Services object of the copied JavaInfo
0160: * @param serv the Services the copy will use and vice versa
0161: * @return a copy of the JavaInfo
0162: */
0163: public JavaInfo copy(Services serv) {
0164: return new JavaInfo(this , serv);
0165: }
0166:
0167: /**
0168: * Don't make this method public, use <code>Services</code>
0169: * instead
0170: *
0171: * returns the TypeConverter to translate program parts to their
0172: * logic equivalent
0173: */
0174: private TypeConverter getTypeConverter() {
0175: return services.getTypeConverter();
0176: }
0177:
0178: /**
0179: * returns the services associated with this JavaInfo
0180: */
0181: public Services getServices() {
0182: return services;
0183: }
0184:
0185: //------------------- common services ----------------------
0186:
0187: /**
0188: * returns the predicate expressing that we are in a state reachable by executing a
0189: * a java program
0190: */
0191: public Function getInReachableState() {
0192: if (legalHeapStructure == null) {
0193: legalHeapStructure = (Function) services.getNamespaces()
0194: .lookup(new Name("inReachableState"));
0195: if (legalHeapStructure == null) {
0196: throw new RuntimeException(
0197: "Legal pointer structure predicate not found.");
0198: }
0199: }
0200: return legalHeapStructure;
0201: }
0202:
0203: /**
0204: * returns the full name of a given {@link
0205: * de.uka.ilkd.key.java.abstraction.KeYJavaType}.
0206: * @param t the KeYJavaType including the package prefix
0207: * @return the full name
0208: */
0209: public String getFullName(KeYJavaType t) {
0210: return kpmi.getFullName(t);
0211: }
0212:
0213: /**
0214: * creates a new TypeReference for the given KeYJavaType
0215: */
0216: public TypeReference createTypeReference(KeYJavaType kjt) {
0217: return new TypeRef(kjt);
0218: }
0219:
0220: public void resetCaches() {
0221: sort2KJTCache = null;
0222: type2KJTCache = null;
0223: name2KJTCache = null;
0224: sName2KJTCache = null;
0225: nameCachedSize = 0;
0226: sNameCachedSize = 0;
0227: sortCachedSize = 0;
0228: }
0229:
0230: /**
0231: * looks up the fully qualifying name given by a String
0232: * in the list of all available
0233: * KeYJavaTypes in the Java model
0234: * @param fullName the String
0235: * @return the KeYJavaType with the name of the String
0236: */
0237: public KeYJavaType getTypeByName(String fullName) {
0238: fullName = translateArrayType(fullName);
0239: if (name2KJTCache == null
0240: || kpmi.rec2key().size() > nameCachedSize) {
0241: buildNameCache();
0242: }
0243: return (KeYJavaType) name2KJTCache.get(fullName);
0244: }
0245:
0246: /**
0247: * caches all known types using their qualified name as retrieval key
0248: */
0249: private void buildNameCache() {
0250: nameCachedSize = kpmi.rec2key().size();
0251: name2KJTCache = new HashMap();
0252: Iterator it = (kpmi.allElements()).iterator();
0253: while (it.hasNext()) {
0254: Object o = it.next();
0255: if (o != null && o instanceof KeYJavaType) {
0256: final KeYJavaType oKJT = (KeYJavaType) o;
0257: if (oKJT.getJavaType() instanceof ArrayType) {
0258: final ArrayType at = (ArrayType) oKJT.getJavaType();
0259: name2KJTCache.put(at.getFullName(), oKJT);
0260: name2KJTCache.put(at
0261: .getAlternativeNameRepresentation(), oKJT);
0262: } else {
0263: name2KJTCache.put(getFullName(oKJT), oKJT);
0264: }
0265: }
0266: }
0267: }
0268:
0269: /**
0270: * checks if name refers to a package
0271: * @param name a String with the name to be checked
0272: * @return true iff name refers to a package
0273: */
0274: public boolean isPackage(String name) {
0275: return kpmi.isPackage(name);
0276: }
0277:
0278: /**
0279: * Translates things like int[], jint[] into [I, etc.
0280: */
0281: private String translateArrayType(String s) {
0282: if ("jbyte[]".equals(s) || "byte[]".equals(s))
0283: return "[B";
0284: else if ("jint[]".equals(s) || "int[]".equals(s))
0285: return "[I";
0286: else if ("jlong[]".equals(s) || "long[]".equals("s"))
0287: return "[J";
0288: else if ("jshort[]".equals(s) || "short[]".equals(s))
0289: return "[S";
0290: else if ("jchar[]".equals(s) || "char[]".equals(s))
0291: return "[C";
0292: // Strangely, this one is not n
0293: // else if ("boolean[]".equals(s))
0294: // return "[Z";
0295: // Not sure if these are needed, commented out for efficiency
0296: // else if ("char[]".equals(s))
0297: // return "[C";
0298: // else if ("double[]".equals(s))
0299: // return "[D";
0300: // else if ("float[]".equals(s))
0301: // return "[F";
0302: return s;
0303: }
0304:
0305: /**
0306: * looks up a KeYJavaType with given name. If the name is a fully
0307: * qualifying name with package prefix an element with this full name is
0308: * taken. If the name does not contain a full package prefix some
0309: * KeYJavaType with this short name is taken.
0310: * @param className the name to look for (either full or short)
0311: * @return a class matching the name
0312: */
0313: public KeYJavaType getTypeByClassName(String className) {
0314: KeYJavaType result = getTypeByName(className);
0315: className = translateArrayType(className);
0316: /* TODO: get rid of this short name thing; introduce second parameter
0317: with the context in which to look for
0318: */
0319: if (result == null) {
0320: final int dotpos = className.lastIndexOf(".");
0321: String shortName = className.substring(dotpos + 1);
0322: if (sName2KJTCache == null) {
0323: buildShortNameCache();
0324: }
0325: result = (KeYJavaType) sName2KJTCache.get(shortName);
0326: }
0327: if (result != null) {
0328: Debug.out("javaInfo: type found (className, type):",
0329: className, result);
0330: } else {
0331: //this is for the case that the cache has been established to early
0332: //(i.e. when not all types were known)
0333: if (kpmi.rec2key().size() > sNameCachedSize) {
0334: sName2KJTCache = null;
0335: return getTypeByClassName(className);
0336: }
0337: Debug.out("javaInfo: type not found. Looked for:",
0338: className);
0339: throw new RuntimeException("TYPE NOT FOUND: " + className);
0340: }
0341: return result;
0342: }
0343:
0344: /**
0345: * caches all known types according to their short name
0346: */
0347: private void buildShortNameCache() {
0348: sName2KJTCache = new HashMap();
0349: sNameCachedSize = kpmi.rec2key().size();
0350: final HashSet duplicates = new HashSet();
0351: final Iterator it = kpmi.allElements().iterator();
0352: while (it.hasNext()) {
0353: Object o = it.next();
0354: if (o != null && o instanceof KeYJavaType) {
0355: KeYJavaType t = (KeYJavaType) o;
0356: String name = getFullName(t);
0357: //TODO array types [[I vs. int[]
0358: int pos = name.lastIndexOf(".");
0359: final String shortName = name.substring(pos + 1);
0360: if (!sName2KJTCache.containsKey(shortName)
0361: && !duplicates.contains(shortName)) {
0362: sName2KJTCache.put(shortName, o);
0363: } else {
0364: duplicates.add(shortName);
0365: sName2KJTCache.remove(shortName);
0366: }
0367: }
0368: }
0369: }
0370:
0371: /**
0372: * returns a type declaration with the full name of the given String fullName
0373: */
0374: public TypeDeclaration getTypeDeclaration(String fullName) {
0375: return (TypeDeclaration) getTypeByName(fullName).getJavaType();
0376: }
0377:
0378: /**
0379: * returns all known KeYJavaTypes of the current
0380: * program type model
0381: * @return all known KeYJavaTypes of the current
0382: * program type model
0383: */
0384: public Set getAllKeYJavaTypes() {
0385: final Set result = new HashSet();
0386: final Iterator it = kpmi.allElements().iterator();
0387: while (it.hasNext()) {
0388: final Object o = it.next();
0389: if (o instanceof KeYJavaType) {
0390: result.add(o);
0391: }
0392: }
0393: return result;
0394: }
0395:
0396: /**
0397: * returns a primitive KeYJavaType matching the given typename making use
0398: * of the LDTs of the current type converter in the services.
0399: */
0400: public KeYJavaType getPrimitiveKeYJavaType(String typename) {
0401: ListOfLDT models = getTypeConverter().getModels();
0402: final IteratorOfLDT ldtIterator = models.iterator();
0403: while (ldtIterator.hasNext()) {
0404: final LDT model = ldtIterator.next();
0405: if (model.javaType() != null
0406: && model.javaType().getFullName().equals(typename)) {
0407: return model.getKeYJavaType(model.javaType());
0408: }
0409: }
0410: return null;
0411: }
0412:
0413: /**
0414: * returns a KeYJavaType (either primitive of object type) having the
0415: * full name of the given String fullName
0416: * @param fullName a String with the type name to lookup
0417: */
0418: public KeYJavaType getKeYJavaType(String fullName) {
0419: KeYJavaType result = getPrimitiveKeYJavaType(fullName);
0420: return (result == null ? (KeYJavaType) getTypeByName(fullName)
0421: : result);
0422: }
0423:
0424: /**
0425: * this is an alias for getTypeByClassName
0426: */
0427: public KeYJavaType getKeYJavaTypeByClassName(String className) {
0428: return getTypeByClassName(className);
0429: }
0430:
0431: /**
0432: * returns true iff the given subType KeYJavaType is a sub type of the
0433: * given KeYJavaType superType.
0434: */
0435: public boolean isSubtype(KeYJavaType subType, KeYJavaType super Type) {
0436: return kpmi.isSubtype(subType, super Type);
0437: }
0438:
0439: /**
0440: * returns a KeYJavaType having the given sort
0441: */
0442: public KeYJavaType getKeYJavaType(Sort sort) {
0443: if (sort2KJTCache == null
0444: || kpmi.rec2key().size() > sortCachedSize) {
0445: sortCachedSize = kpmi.rec2key().size();
0446: sort2KJTCache = new HashMap();
0447: Iterator it = (kpmi.allElements()).iterator();
0448: while (it.hasNext()) {
0449: Object o = it.next();
0450: if (o != null && o instanceof KeYJavaType) {
0451: sort2KJTCache.put(((KeYJavaType) o).getSort(), o);
0452: }
0453: }
0454: }
0455: return (KeYJavaType) sort2KJTCache.get(sort);
0456: }
0457:
0458: /** returns the KeYJavaType of the expression if it can be
0459: * determined else null is returned
0460: */
0461: public KeYJavaType getPrimitiveKeYJavaType(Expression e) {
0462: return getTypeConverter().getKeYJavaType(e);
0463: }
0464:
0465: /**
0466: * returns all ObjectSorts of the underlying Java model
0467: * @return a namespace containing the object sorts
0468: */
0469: public Namespace getObjectSorts() {
0470: Iterator it = kpmi.allObjectSorts().iterator();
0471: Namespace ns = new Namespace();
0472: while (it.hasNext()) {
0473: ns.add((Named) it.next());
0474: }
0475: return ns;
0476: }
0477:
0478: /**
0479: * returns the KeYJavaType belonging to the given Type t
0480: */
0481: public KeYJavaType getKeYJavaType(Type t) {
0482: if (t instanceof PrimitiveType) {
0483: return getTypeConverter().getKeYJavaType(t);
0484: } else {
0485: if (type2KJTCache == null) {
0486: type2KJTCache = new HashMap();
0487: final Iterator it = (kpmi.allElements()).iterator();
0488: while (it.hasNext()) {
0489: Object o = it.next();
0490: if (o instanceof KeYJavaType) {
0491: type2KJTCache.put(((KeYJavaType) o)
0492: .getJavaType(), o);
0493: }
0494: }
0495: }
0496: return (KeYJavaType) type2KJTCache.get(t);
0497: }
0498: }
0499:
0500: /**
0501: * returns all methods from the given Type
0502: */
0503: public ListOfMethod getAllMethods(KeYJavaType kjt) {
0504: return kpmi.getAllMethods(kjt);
0505: }
0506:
0507: /**
0508: * returns all locally declared methods from the given Type
0509: */
0510: public ListOfMethod getMethods(KeYJavaType kjt) {
0511: return kpmi.getMethods(kjt);
0512: }
0513:
0514: /**
0515: * returns all methods from the given Type as ProgramMethods
0516: */
0517: public ListOfProgramMethod getAllProgramMethods(KeYJavaType kjt) {
0518: return kpmi.getAllProgramMethods(kjt);
0519: }
0520:
0521: /**
0522: * returns all methods declared in the given Type as ProgramMethods
0523: */
0524: public ListOfProgramMethod getAllProgramMethodsLocallyDeclared(
0525: KeYJavaType kjt) {
0526: return kpmi.getAllProgramMethodsLocallyDeclared(kjt);
0527: }
0528:
0529: /**
0530: * returns the program methods defined in the given KeYJavaType with name
0531: * m and the list of types as signature of the method
0532: * @param classType the KeYJavaType of the class where to look for the
0533: * method
0534: * @param methodName the name of the method
0535: * @param signature a ListOfType with the arguments types
0536: * @param context the KeYJavaType of the class context from <em>where</em>
0537: * the method is called
0538: * @return a matching program method
0539: */
0540: public ProgramMethod getProgramMethod(KeYJavaType classType,
0541: String methodName, ListOfType signature, KeYJavaType context) {
0542: return kpmi.getProgramMethod(classType, methodName, signature,
0543: context);
0544: }
0545:
0546: /**
0547: * returns the program methods defined in the given KeYJavaType with name
0548: * m and the list of types as signature of the method
0549: * @param ct the KeYJavaType of the class where to look for the
0550: * method
0551: * @param methodName the name of the method
0552: * @param signature a ListOfKeYJavaType with the arguments types
0553: * @param context the KeYJavaType of the class context from <em>where</em>
0554: * the method is called
0555: * @return a matching program method
0556: */
0557: public ProgramMethod getProgramMethod(KeYJavaType ct,
0558: String methodName, ListOfKeYJavaType signature,
0559: KeYJavaType context) {
0560: return kpmi
0561: .getProgramMethod(ct, methodName, signature, context);
0562: }
0563:
0564: public Term getProgramMethodTerm(Term prefix, String methodName,
0565: Term[] args, String className) {
0566: ListOfKeYJavaType sig = SLListOfKeYJavaType.EMPTY_LIST;
0567: Term[] subs = new Term[args.length + 1];
0568: subs[0] = prefix;
0569: for (int i = 1; i < subs.length; i++) {
0570: Term t = args[i - 1];
0571: sig = sig.append(getServices().getTypeConverter()
0572: .getKeYJavaType(t));
0573: subs[i] = t;
0574: }
0575: className = translateArrayType(className);
0576: KeYJavaType clType = getKeYJavaTypeByClassName(className);
0577: ProgramMethod pm = getProgramMethod(clType, methodName, sig,
0578: clType);
0579: if (pm == null) {
0580: throw new IllegalArgumentException("Program method "
0581: + methodName + " in " + className + " not found.");
0582: }
0583: if (pm.isStatic()) {
0584: Term[] newSubs = new Term[subs.length - 1];
0585: System.arraycopy(subs, 1, newSubs, 0, newSubs.length);
0586: subs = newSubs;
0587: }
0588: if (pm.getKeYJavaType() == null) {
0589: throw new IllegalArgumentException("Program method "
0590: + methodName + " in " + className + " must have"
0591: + " a non-void type.");
0592: }
0593: return TermFactory.DEFAULT.createFunctionTerm(pm, subs);
0594: }
0595:
0596: /**
0597: * returns all direct supertypes (local declared types in extends and
0598: * implements) if extends is not given explict java.lang.Object is added
0599: * (it is not added for interfaces)
0600: */
0601: public ListOfKeYJavaType getDirectSuperTypes(KeYJavaType type) {
0602: final ClassType javaType = (ClassType) type.getJavaType();
0603:
0604: ListOfKeYJavaType localSupertypes = javaType.getSupertypes();
0605:
0606: if (!javaType.isInterface()) {
0607: final IteratorOfKeYJavaType it = localSupertypes.iterator();
0608: boolean found = false;
0609: while (it.hasNext()) {
0610: KeYJavaType keYType = it.next();
0611: if (!((ClassType) keYType.getJavaType()).isInterface()) {
0612: found = true;
0613: break;
0614: }
0615: }
0616: if (!found) {
0617: localSupertypes = localSupertypes
0618: .prepend(getJavaLangObject());
0619: }
0620:
0621: }
0622: return localSupertypes;
0623: }
0624:
0625: /**
0626: * retrieves the direct extended superclass for the given class
0627: * @param type the KeYJavaType of the type whose superclass
0628: * has to be determined
0629: * @return KeYJavaType of the extended supertype
0630: */
0631: public KeYJavaType getSuperclass(KeYJavaType type) {
0632: KeYJavaType result = null;
0633: final ClassType javaType = (ClassType) type.getJavaType();
0634:
0635: if (javaType.isInterface()) {
0636: return null;
0637: }
0638:
0639: final ListOfKeYJavaType localSupertypes = javaType
0640: .getSupertypes();
0641: final IteratorOfKeYJavaType it = localSupertypes.iterator();
0642: while (result == null && it.hasNext()) {
0643: final KeYJavaType keYType = it.next();
0644: if (!((ClassType) keYType.getJavaType()).isInterface()) {
0645: result = keYType;
0646: }
0647: }
0648:
0649: if (result == null) {
0650: result = getJavaLangObject();
0651: }
0652:
0653: return result;
0654: }
0655:
0656: /**
0657: * returns the program method defined in the KeYJavaType of the program
0658: * variable clv, with the name m, and the KeYJavaTypes of the given array
0659: * of program variables as signatures.
0660: * @param classType the KeYJavaType of the class where to look for the
0661: * method
0662: * @param methodName the name of the method
0663: * @param args an array of ProgramVariables as the arguments of the
0664: * method
0665: * @param context the KeYJavaType of the class context from <em>where</em>
0666: * the method is called
0667: * @return a matching program method
0668: */
0669: public ProgramMethod getProgramMethod(KeYJavaType classType,
0670: String methodName, ProgramVariable[] args,
0671: KeYJavaType context) {
0672: ListOfType types = SLListOfType.EMPTY_LIST;
0673: for (int i = args.length - 1; i >= 0; i--) {
0674: types = types.prepend(args[i].getKeYJavaType());
0675: }
0676: return getProgramMethod(classType, methodName, types, context);
0677: }
0678:
0679: /** gets an array of expression and returns a list of types */
0680: private ListOfKeYJavaType getKeYJavaTypes(ArrayOfExpression args) {
0681: ListOfKeYJavaType result = SLListOfKeYJavaType.EMPTY_LIST;
0682: if (args != null) {
0683: for (int i = args.size() - 1; i >= 0; i--) {
0684: final Expression argument = args.getExpression(i);
0685: result = result.prepend(getTypeConverter()
0686: .getKeYJavaType(argument));
0687: }
0688: }
0689: return result;
0690: }
0691:
0692: /**
0693: * retrieves the signature according to the given expressions
0694: * @param arguments ArrayOfExpression of which we try to construct a
0695: * signature
0696: * @return the signature
0697: */
0698: public ListOfKeYJavaType createSignature(ArrayOfExpression arguments) {
0699: return getKeYJavaTypes(arguments);
0700: }
0701:
0702: /**
0703: * retrieves all attributes locally declared in class <tt>cl</tt>
0704: * (inclusive the implicit attributes)
0705: * The returned list is in source code order.
0706: * @param classDecl the ClassDeclaration whose attributes shall be collected
0707: * @return all attributes declared in class <tt>cl</tt>
0708: */
0709: public ListOfField getAllFields(ClassDeclaration classDecl) {
0710: return filterLocalDeclaredFields(classDecl, Filter.TRUE);
0711: }
0712:
0713: /**
0714: * retrieves all implicit attributes locally declared in the given class
0715: * The returned list is in source code order.
0716: * @param cl the ClassDeclaration where to look for the implicit
0717: * attributes
0718: * @return all implicit attributes declared in <tt>cl</tt>
0719: */
0720: public ListOfField getImplicitFields(ClassDeclaration cl) {
0721: return filterLocalDeclaredFields(cl, Filter.IMPLICITFIELD);
0722: }
0723:
0724: /**
0725: * retrieves all attributes locally declared in class <tt>cl</tt>
0726: * (inclusive the implicit attributes) satisfying the given filter
0727: * The returned list is in source code order.
0728: * @param classDecl the ClassDeclaration whose attributes shall be collected
0729: * @param filter the Filter to be satisifed by the attributes to
0730: * be returned
0731: * @return all attributes declared in class <tt>cl</tt> satisfying the
0732: * given filter
0733: */
0734: private ListOfField filterLocalDeclaredFields(
0735: ClassDeclaration classDecl, Filter filter) {
0736: ListOfField fields = SLListOfField.EMPTY_LIST;
0737: final ArrayOfMemberDeclaration members = classDecl.getMembers();
0738: for (int i = members.size() - 1; i >= 0; i--) {
0739: final MemberDeclaration member = members
0740: .getMemberDeclaration(i);
0741: if (member instanceof FieldDeclaration) {
0742: final ArrayOfFieldSpecification specs = ((FieldDeclaration) member)
0743: .getFieldSpecifications();
0744: for (int j = specs.size() - 1; j >= 0; j--) {
0745: final FieldSpecification fieldSpec = specs
0746: .getFieldSpecification(j);
0747: if (filter.isSatisfiedBy(fieldSpec)) {
0748: fields = fields.prepend(fieldSpec);
0749: }
0750: }
0751: }
0752: }
0753: return fields;
0754: }
0755:
0756: //----------------- parsing services --------------------------
0757:
0758: /**
0759: * reads a Java block given as a string java as it was in the given
0760: * TypeDeclaration asIn.
0761: */
0762: public JavaBlock readJavaBlock(String java, TypeDeclaration asIn) {
0763: ClassDeclaration cd = null;
0764: if (asIn instanceof ClassDeclaration) {
0765: cd = (ClassDeclaration) asIn;
0766: } else {
0767: Debug
0768: .out("Reading Java Block from an InterfaceDeclaration:"
0769: + " Not yet implemented.");
0770: }
0771: final NamespaceSet nss = services.getNamespaces().copy();
0772: nss.startProtocol();
0773: final JavaBlock block = kpmi.readBlock(java, cd, nss);
0774: // if we are here everything is fine nad wen can add the
0775: // changes (may be new array types)
0776: services.getNamespaces().addProtocolled(nss);
0777: return block;
0778: }
0779:
0780: /**
0781: * reads a Java block given as a String
0782: */
0783: public JavaBlock readJavaBlock(String java) {
0784: NamespaceSet nss = services.getNamespaces().copy();
0785: nss.startProtocol();
0786: final JavaBlock block = kpmi.readJavaBlock(java, nss);
0787: // if we are here everything is fine nad wen can add the
0788: // changes (may be new array types)
0789: services.getNamespaces().addProtocolled(nss);
0790: return block;
0791: }
0792:
0793: /**
0794: * reads a Java statement not necessarily a block
0795: */
0796: public ProgramElement readJava(String java) {
0797: return ((StatementBlock) readJavaBlock("{" + java + "}")
0798: .program()).getChildAt(0);
0799: }
0800:
0801: /**
0802: * returns a term representing 'null' in logic
0803: */
0804: public Term getNullTerm() {
0805: return getTypeConverter().convertToLogicElement(
0806: NullLiteral.NULL);
0807: }
0808:
0809: /**
0810: * retrieves a field with the given name out of the list
0811: * @param programName a String with the name of the field to be looked for
0812: * @param fields the ListOfField where we have to look for the field
0813: * @return the program variable of the given name or null if not
0814: * found
0815: */
0816: private final ProgramVariable find(String programName,
0817: ListOfField fields) {
0818: IteratorOfField it = fields.iterator();
0819: while (it.hasNext()) {
0820: Field field = it.next();
0821: if (programName.equals(field.getProgramName())) {
0822: return (ProgramVariable) ((FieldSpecification) field)
0823: .getProgramVariable();
0824: }
0825: }
0826: return null;
0827: }
0828:
0829: /**
0830: * extracts all fields out of fielddeclaration
0831: * @param field the FieldDeclaration of which the field
0832: * specifications have to be extracted
0833: * @return a ListOfField the includes all field specifications found
0834: * int the field declaration of the given list
0835: */
0836: private final ListOfField getFields(FieldDeclaration field) {
0837: ListOfField result = SLListOfField.EMPTY_LIST;
0838: final ArrayOfFieldSpecification spec = field
0839: .getFieldSpecifications();
0840: for (int i = spec.size() - 1; i >= 0; i--) {
0841: result = result.prepend(spec.getFieldSpecification(i));
0842: }
0843: return result;
0844: }
0845:
0846: /**
0847: * extracts all field specifications out of the given
0848: * list. Therefore it descends into field declarations.
0849: * @param list the ArrayOfMemberDeclaration with the members of a
0850: * type declaration
0851: * @return a ListOfField the includes all field specifications found
0852: * int the field declaration of the given list
0853: */
0854: private ListOfField getFields(ArrayOfMemberDeclaration list) {
0855: ListOfField result = SLListOfField.EMPTY_LIST;
0856: for (int i = list.size() - 1; i >= 0; i--) {
0857: final MemberDeclaration pe = list.getMemberDeclaration(i);
0858: if (pe instanceof FieldDeclaration) {
0859: result = result
0860: .append(getFields((FieldDeclaration) pe));
0861: }
0862: }
0863: return result;
0864: }
0865:
0866: /**
0867: * returns the programvariable for the specified attribute. The attribute
0868: * has to be fully qualified, i.e. <tt>declarationType::attributeName</tt>
0869: * @param fullyQualifiedName the String with the fully qualified attribute
0870: * name
0871: * @return an attribute program variable of the given name
0872: * @throws IllegalArgumentException if the given name is not fully
0873: * qualified
0874: */
0875: public ProgramVariable getAttribute(String fullyQualifiedName) {
0876: final int idx = fullyQualifiedName.indexOf("::");
0877:
0878: if (idx == -1) {
0879: throw new IllegalArgumentException(fullyQualifiedName
0880: + " is not a fully qualified attribute name");
0881: }
0882:
0883: return getAttribute(fullyQualifiedName.substring(idx + 2),
0884: fullyQualifiedName.substring(0, idx));
0885: }
0886:
0887: /**
0888: * returns the programvariable for the specified attribute declared in
0889: * the specified class
0890: * @param programName the String with the name of the attribute
0891: * @param qualifiedClassName the String with the full (inclusive package) qualified
0892: * class name
0893: * @return the attribute program variable of the given name
0894: * @throws IllegalArgumentException if the qualified class name is empty or
0895: * null
0896: */
0897: public ProgramVariable getAttribute(String programName,
0898: String qualifiedClassName) {
0899: if (qualifiedClassName == null
0900: || qualifiedClassName.length() == 0) {
0901: throw new IllegalArgumentException(
0902: "Missing qualified classname");
0903: }
0904: return getAttribute(programName,
0905: getKeYJavaTypeByClassName(qualifiedClassName));
0906: }
0907:
0908: /**
0909: * returns the program variable representing the attribute of the given
0910: * name declared locally in class <tt>classType</tt>
0911: * @return the attribute of the given name declared in <tt>classType</tt>
0912: */
0913: public ProgramVariable getAttribute(final String name,
0914: KeYJavaType classType) {
0915: if (classType.getJavaType() instanceof ArrayDeclaration) {
0916: ProgramVariable res = find(name,
0917: getFields(((ArrayDeclaration) classType
0918: .getJavaType()).getMembers()));
0919: if (res == null) {
0920: return getAttribute(name, getJavaLangObject());
0921: }
0922: return res;
0923: } else {
0924: final ListOfField list = kpmi
0925: .getAllFieldsLocallyDeclaredIn(classType);
0926: final IteratorOfField it = list.iterator();
0927: while (it.hasNext()) {
0928: final Field f = it.next();
0929: if (f != null
0930: && (f.getName().equals(name) || f
0931: .getProgramName().equals(name))) {
0932: return (ProgramVariable) ((VariableSpecification) f)
0933: .getProgramVariable();
0934: }
0935: }
0936: }
0937: return null;
0938: }
0939:
0940: /**
0941: * returns an attribute named <tt>attributeName</tt> declared locally
0942: * in object type <tt>s</tt>
0943: */
0944: public ProgramVariable getAttribute(String attributeName,
0945: ObjectSort s) {
0946: return getAttribute(attributeName, getKeYJavaType(s));
0947: }
0948:
0949: /**
0950: * returns a list of all attributes with the given program name
0951: * declared in one of <tt>type</tt>'s sub- or supertype including
0952: * its own attributes
0953: * <strong>Attention:</strong>
0954: * The type must not denote the null type
0955: * </ol>
0956: *
0957: * @param programName the String with name of the attribute as declared
0958: * in a program
0959: * @param type the KeYJavaType specifying the part of the hierarchy
0960: * where to look for
0961: * @return list of found attributes with name <tt>programName</tt>
0962: */
0963: public ListOfProgramVariable getAllAttributes(String programName,
0964: KeYJavaType type) {
0965:
0966: ListOfProgramVariable result = SLListOfProgramVariable.EMPTY_LIST;
0967:
0968: if (!(type.getSort() instanceof ObjectSort)) {
0969: return result;
0970: }
0971:
0972: if (type.getJavaType() instanceof ArrayType) {
0973: ProgramVariable var = find(programName,
0974: getFields(((ArrayDeclaration) type.getJavaType())
0975: .getMembers()));
0976: if (var != null) {
0977: result = result.prepend(var);
0978: }
0979: var = getAttribute(programName, getJavaLangObject());
0980: if (var != null) {
0981: result = result.prepend(var);
0982: }
0983: return result;
0984: }
0985:
0986: // the assert statements below are not for fun, some methods rely
0987: // on the correct order
0988: ListOfKeYJavaType hierarchie = kpmi.getAllSubtypes(type);
0989: assert !hierarchie.contains(type);
0990:
0991: hierarchie = hierarchie.prepend(kpmi.getAllSupertypes(type));
0992: assert hierarchie.head() == type;
0993:
0994: final IteratorOfKeYJavaType it = hierarchie.iterator();
0995: while (it.hasNext()) {
0996: KeYJavaType st = it.next();
0997: if (st != null) {
0998: final ProgramVariable var = getAttribute(programName,
0999: st);
1000: if (var != null) {
1001: result = result.prepend(var);
1002: }
1003: }
1004: }
1005:
1006: return result;
1007: }
1008:
1009: private void fillCommonTypesCache() {
1010: if (commonTypesCacheValid)
1011: return;
1012: final String[] fullNames = { "java.lang.Object",
1013: "java.lang.Cloneable", "java.lang.Serializable" };
1014:
1015: for (int i = 0; i < fullNames.length; i++) {
1016: commonTypes[i] = getKeYJavaTypeByClassName(fullNames[i]);
1017: }
1018: commonTypesCacheValid = true;
1019: }
1020:
1021: /**
1022: * returns the KeYJavaType for class <tt>java.lang.Object</tt>
1023: */
1024: public KeYJavaType getJavaLangObject() {
1025: if (commonTypes[0] == null) {
1026: commonTypes[0] = getKeYJavaTypeByClassName("java.lang.Object");
1027: }
1028: return commonTypes[0];
1029: }
1030:
1031: /**
1032: * returns the KeYJavaType for class java.lang.Clonable
1033: */
1034: public KeYJavaType getJavaLangCloneable() {
1035: if (commonTypes[1] == null) {
1036: commonTypes[1] = getKeYJavaTypeByClassName("java.lang.Cloneable");
1037: }
1038: return commonTypes[1];
1039: }
1040:
1041: /**
1042: * returns the KeYJavaType for class <tt>java.io.Serializable</tt>
1043: */
1044: public KeYJavaType getJavaIoSerializable() {
1045: if (commonTypes[2] == null) {
1046: commonTypes[2] = getKeYJavaTypeByClassName("java.io.Serializable");
1047: }
1048: return commonTypes[2];
1049: }
1050:
1051: /**
1052: * returns the KeYJavaType for class java.lang.Object
1053: */
1054: public Sort getJavaLangObjectAsSort() {
1055: return getJavaLangObject().getSort();
1056: }
1057:
1058: /**
1059: * returns the KeYJavaType for class java.lang.Cloneable
1060: */
1061: public Sort getJavaLangCloneableAsSort() {
1062: return getJavaLangCloneable().getSort();
1063: }
1064:
1065: /**
1066: * returns the KeYJavaType for class java.io.Serializable
1067: */
1068: public Sort getJavaIoSerializableAsSort() {
1069: return getJavaIoSerializable().getSort();
1070: }
1071:
1072: /**
1073: * tests if sort represents java.lang.Object, java.lang.Cloneable or
1074: * java.io.Serializable
1075: */
1076: public boolean isAJavaCommonSort(Sort sort) {
1077: if (!commonTypesCacheValid) {
1078: fillCommonTypesCache();
1079: }
1080: for (int i = 0; i < commonTypes.length; i++) {
1081: if (commonTypes[i].getSort() == sort) {
1082: return true;
1083: }
1084: }
1085: return false;
1086: }
1087:
1088: /**
1089: * returns the KeYJavaType representing the type of 'null'
1090: */
1091: public KeYJavaType getNullType() {
1092: if (nullType == null) {
1093: nullType = getKeYJavaTypeByClassName("null");
1094: Debug.assertTrue(nullType != null,
1095: "we should already have it in the map");
1096: }
1097: return nullType;
1098: }
1099:
1100: /**
1101: * returns the default execution context. This is equiavlent to executing the program
1102: * in a static method of a class placed in the default package
1103: * @return the default execution context
1104: */
1105: public ExecutionContext getDefaultExecutionContext() {
1106: if (defaultExecutionContext == null) {
1107: // ensure that default classes are available
1108: if (!kpmi.rec2key().parsedSpecial()) {
1109: readJava("{}");
1110: }
1111: final KeYJavaType kjt = getKeYJavaTypeByClassName(DEFAULT_EXECUTION_CONTEXT_CLASS);
1112: defaultExecutionContext = new ExecutionContext(new TypeRef(
1113: kjt), null);
1114: }
1115: return defaultExecutionContext;
1116: }
1117:
1118: /**
1119: * returns a term representing the null constant in logic
1120: */
1121: public Term getNullConst() {
1122: if (nullConst == null) {
1123: nullConst = TermFactory.DEFAULT.createFunctionTerm(Op.NULL);
1124: }
1125: return nullConst;
1126: }
1127:
1128: /**
1129: * returns all proper subtypes of a given type
1130: * @param type the KeYJavaType whose subtypes are returned
1131: * @return list of all subtypes
1132: */
1133: public ListOfKeYJavaType getAllSubtypes(KeYJavaType type) {
1134: return kpmi.getAllSubtypes(type);
1135: }
1136:
1137: /**
1138: * returns all supertypes of a given type
1139: * @param type the KeYJavaType whose supertypes are returned
1140: * @return list of all supertypes
1141: */
1142: public ListOfKeYJavaType getAllSupertypes(KeYJavaType type) {
1143: if (type.getJavaType() instanceof ArrayType) {
1144: ListOfKeYJavaType arraySupertypes = SLListOfKeYJavaType.EMPTY_LIST;
1145: final IteratorOfSort it = ((ArraySort) type.getSort())
1146: .extendsSorts().iterator();
1147: while (it.hasNext()) {
1148: arraySupertypes.append(getKeYJavaType(it.next()));
1149: }
1150: return arraySupertypes;
1151: }
1152: return kpmi.getAllSupertypes(type);
1153: }
1154:
1155: /**
1156: * looks up for a field of the given program name
1157: * visible <em>in</em> the specified class type belonging to the type
1158: * or one of its supertypes
1159: *
1160: * @param programName the String containing the name of the
1161: * field to be looked up. The name is in short notation,
1162: * i.e. not fully qualified
1163: * @param classType the KeYJavaType of the class used as context
1164: * @return the field of the given name
1165: */
1166: public ProgramVariable lookupVisibleAttribute(String programName,
1167: KeYJavaType classType) {
1168: return find(programName, kpmi.getAllVisibleFields(classType));
1169: }
1170:
1171: public void setJavaSourcePath(String path) {
1172: javaSourcePath = path;
1173: }
1174:
1175: public String getJavaSourcePath() {
1176: return javaSourcePath;
1177: }
1178:
1179: /**
1180: * returns the list of all common subtypes of types <tt>k1</tt> and <tt>k2</tt>
1181: * (inclusive one of them if they are equal or subtypes themselves)
1182: * attention: <tt>Null</tt> is not a jav atype only a logic sort, i.e.
1183: * if <tt>null</tt> is the only element shared between <tt>k1</tt> and <tt>k2</tt>
1184: * the returned list will be empty
1185: *
1186: * @param k1 the first KeYJavaType denoting a class type
1187: * @param k2 the second KeYJavaType denoting a classtype
1188: * @return the list of common subtypes of types <tt>k1</tt> and <tt>k2</tt>
1189: */
1190: public ListOfKeYJavaType getCommonSubtypes(KeYJavaType k1,
1191: KeYJavaType k2) {
1192: final CacheKey ck = new CacheKey(k1, k2);
1193: ListOfKeYJavaType result = (ListOfKeYJavaType) commonSubtypeCache
1194: .get(ck);
1195:
1196: if (result != null) {
1197: return result;
1198: }
1199:
1200: result = SLListOfKeYJavaType.EMPTY_LIST;
1201:
1202: if (k1.getSort().extendsTrans(k2.getSort())) {
1203: result = getAllSubtypes(k1).prepend(k1);
1204: } else if (k2.getSort().extendsTrans(k1.getSort())) {
1205: result = getAllSubtypes(k2).prepend(k2);
1206: } else {
1207: final ListOfKeYJavaType l1 = getAllSubtypes(k1);
1208: final ListOfKeYJavaType l2 = getAllSubtypes(k2);
1209:
1210: final IteratorOfKeYJavaType it = l1.iterator();
1211:
1212: while (it.hasNext()) {
1213: final KeYJavaType next = it.next();
1214: if (l2.contains(next)) {
1215: result = result.prepend(next);
1216: }
1217: }
1218: }
1219:
1220: commonSubtypeCache.put(ck, result);
1221: return result;
1222: }
1223:
1224: /** returns the length attribute for arrays */
1225: public ProgramVariable getArrayLength() {
1226: if (length == null) {
1227: final SuperArrayDeclaration sad = (SuperArrayDeclaration) rec2key()
1228: .getSuperArrayType().getJavaType();
1229: length = (ProgramVariable) sad.length().getVariables()
1230: .getVariableSpecification(0).getProgramVariable();
1231: assert "length".equals(length.name().toString()) : "Wrong array length";
1232: }
1233:
1234: return length;
1235: }
1236:
1237: /**
1238: * inner class used to filter certain types of program elements
1239: */
1240: static abstract class Filter {
1241:
1242: /** the universally satisfied filter */
1243: final static Filter TRUE = new Filter() {
1244:
1245: public boolean isSatisfiedBy(ProgramElement pe) {
1246: return true;
1247: }
1248: };
1249:
1250: /** this filter is satisfied if the given program element is an
1251: * instanceof ImplicitFieldSpecification
1252: */
1253: final static Filter IMPLICITFIELD = new Filter() {
1254:
1255: public boolean isSatisfiedBy(ProgramElement pe) {
1256: return pe instanceof ImplicitFieldSpecification;
1257: }
1258: };
1259:
1260: /**
1261: * decides whether the given program element fulfills the filter condition
1262: * or not
1263: * @param pe the ProgramElement to be filtered
1264: * @return true iff program element <tt>pe</tt> satisfies the filter
1265: * condition
1266: */
1267: public abstract boolean isSatisfiedBy(ProgramElement pe);
1268: }
1269:
1270: }
|