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:
0011: package de.uka.ilkd.key.java;
0012:
0013: import java.io.*;
0014: import java.lang.reflect.Constructor;
0015: import java.lang.reflect.InvocationTargetException;
0016: import java.lang.reflect.Method;
0017: import java.net.URL;
0018: import java.util.HashMap;
0019: import java.util.Iterator;
0020: import java.util.LinkedList;
0021:
0022: import org.apache.log4j.Logger;
0023:
0024: import recoder.abstraction.ClassType;
0025: import recoder.bytecode.ClassFile;
0026: import recoder.list.ClassTypeList;
0027: import recoder.list.ExpressionMutableList;
0028: import recoder.list.LoopInitializerMutableList;
0029: import recoder.service.ChangeHistory;
0030: import de.uka.ilkd.key.java.abstraction.*;
0031: import de.uka.ilkd.key.java.declaration.*;
0032: import de.uka.ilkd.key.java.declaration.modifier.*;
0033: import de.uka.ilkd.key.java.expression.ArrayInitializer;
0034: import de.uka.ilkd.key.java.expression.Literal;
0035: import de.uka.ilkd.key.java.expression.ParenthesizedExpression;
0036: import de.uka.ilkd.key.java.expression.PassiveExpression;
0037: import de.uka.ilkd.key.java.expression.literal.*;
0038: import de.uka.ilkd.key.java.expression.operator.*;
0039: import de.uka.ilkd.key.java.recoderext.*;
0040: import de.uka.ilkd.key.java.reference.*;
0041: import de.uka.ilkd.key.java.reference.ExecutionContext;
0042: import de.uka.ilkd.key.java.statement.*;
0043: import de.uka.ilkd.key.java.statement.CatchAllStatement;
0044: import de.uka.ilkd.key.java.statement.MethodBodyStatement;
0045: import de.uka.ilkd.key.logic.*;
0046: import de.uka.ilkd.key.logic.op.*;
0047: import de.uka.ilkd.key.logic.sort.*;
0048: import de.uka.ilkd.key.proof.init.KeYUserProblemFile;
0049: import de.uka.ilkd.key.util.Debug;
0050: import de.uka.ilkd.key.util.ExtList;
0051: import de.uka.ilkd.key.util.KeYResourceManager;
0052:
0053: public class Recoder2KeY implements JavaReader {
0054:
0055: static Logger logger = Logger
0056: .getLogger(Recoder2KeY.class.getName());
0057: //static String javaSrcDir = "sun_src_1.3.1_11-b02";
0058: //static String javaSrcDir = "sun_src_1.4.2_03";
0059: static String javaSrcDir = "JavaRedux_1.4.2";
0060:
0061: /** caches access to methods for reflection */
0062: private final static HashMap ct2meth = new HashMap(400);
0063:
0064: /** caches constructor access for reflection */
0065: private final static HashMap recClass2keyClassCons = new HashMap(
0066: 400);
0067:
0068: /**
0069: * mapping from recoder.abstraction.Type to KeYJavaType
0070: */
0071: protected HashMap type2KeYType = new HashMap();
0072:
0073: /**
0074: * methodsDeclaring contains the recoder method declarations as keys
0075: * that have been started to convert but are not yet finished.
0076: * The mapped value is the reference to the later completed
0077: * ProgramMethod.
0078: */
0079: protected HashMap methodsDeclaring = new HashMap();
0080:
0081: /**
0082: * Hashmap from
0083: * <code>recoder.java.declaration.FieldSpecification</code> to
0084: * <code>ProgramVariable</code>; this is necessary to avoid cycles
0085: * when converting initializers. Access to this map is performed
0086: * via the method
0087: * <code>getProgramVariableForFieldSpecification</code>
0088: */
0089: protected HashMap fieldSpecificationMapping = new HashMap();
0090:
0091: protected KeYRecoderMapping rec2key;
0092: protected TypeConverter typeConverter;
0093: protected KeYCrossReferenceServiceConfiguration servConf;
0094: protected Services services;
0095:
0096: private NamespaceSet namespaces = new NamespaceSet();
0097:
0098: private static int interactCounter = 0;
0099: private String currentClass = null;
0100: private boolean parsingLibs = false;
0101:
0102: private boolean inLoopInit = false;
0103: String fileName;
0104:
0105: /**
0106: * builder class for implicit array methods
0107: */
0108: private CreateArrayMethodBuilder arrayMethodBuilder;
0109:
0110: /**
0111: * builder class for implicit transient array methods
0112: */
0113: private CreateTransientArrayMethodBuilder transientArrayMethodBuilder;
0114:
0115: public Recoder2KeY(KeYCrossReferenceServiceConfiguration servConf,
0116: KeYRecoderMapping rec2key, NamespaceSet nss,
0117: TypeConverter tc) {
0118: this (servConf, null, rec2key, nss, tc);
0119: }
0120:
0121: public Recoder2KeY(Services services, NamespaceSet nss) {
0122: this (
0123: services.getJavaInfo().getKeYProgModelInfo()
0124: .getServConf(), null, services.getJavaInfo()
0125: .rec2key(), nss, services.getTypeConverter());
0126: }
0127:
0128: private Recoder2KeY(KeYCrossReferenceServiceConfiguration servConf,
0129: String classPath, KeYRecoderMapping rec2key,
0130: NamespaceSet nss, TypeConverter tc) {
0131: this .servConf = servConf;
0132: this .typeConverter = tc;
0133: this .rec2key = rec2key;
0134: this .services = tc.getServices();
0135: if (classPath != null) {
0136: servConf.getProjectSettings().setProperty(
0137: recoder.io.PropertyNames.INPUT_PATH, classPath);
0138: }
0139:
0140: if (servConf.getProjectSettings()
0141: .ensureSystemClassesAreInPath()) {
0142: } else {
0143: if (System.getProperty("os.name").toLowerCase().indexOf(
0144: "mac") != -1) {
0145: String inputPath = servConf.getProjectSettings()
0146: .getProperty(
0147: recoder.io.PropertyNames.INPUT_PATH);
0148: if (inputPath == null) {
0149: inputPath = ".";
0150: }
0151:
0152: final String javaHome = System.getProperty("java.home");
0153:
0154: inputPath += File.pathSeparator + javaHome
0155: + File.separator + ".." + File.separator
0156: + "Classes" + File.separator + "classes.jar";
0157: inputPath += File.pathSeparator + javaHome
0158: + File.separator + ".." + File.separator
0159: + "Classes" + File.separator + "ui.jar";
0160:
0161: servConf.getProjectSettings().setProperty(
0162: recoder.io.PropertyNames.INPUT_PATH, inputPath);
0163:
0164: if (!servConf.getProjectSettings()
0165: .ensureSystemClassesAreInPath()) {
0166: System.err
0167: .println("System classes not found on default Mac places.");
0168: }
0169:
0170: } else {
0171: System.err.println("System classes not found in path.");
0172: }
0173: }
0174: namespaces = nss;
0175: }
0176:
0177: private void initArrayMethodBuilder() {
0178: final KeYJavaType integerType = getKeYJavaType(servConf
0179: .getNameInfo().getIntType());
0180: final KeYJavaType byteType = getKeYJavaType(servConf
0181: .getNameInfo().getByteType());
0182: final KeYJavaType objectType = javaInfo().getJavaLangObject();
0183: arrayMethodBuilder = new CreateArrayMethodBuilder(integerType,
0184: objectType);
0185: transientArrayMethodBuilder = new CreateTransientArrayMethodBuilder(
0186: integerType, objectType, byteType);
0187: }
0188:
0189: private void parsingLibs(boolean v) {
0190: parsingLibs = v;
0191: }
0192:
0193: private JavaInfo javaInfo() {
0194: return typeConverter != null ? typeConverter.getServices()
0195: .getJavaInfo() : null;
0196: }
0197:
0198: public KeYCrossReferenceServiceConfiguration getServiceConfiguration() {
0199: return servConf;
0200: }
0201:
0202: public KeYRecoderMapping rec2key() {
0203: return rec2key;
0204: }
0205:
0206: /**
0207: * wraps a RECODER StatementBlock in a method
0208: * @param block the recoder.java.StatementBlock to wrap
0209: * @return the enclosing recoder.java.MethodDeclaration
0210: */
0211: protected recoder.java.declaration.MethodDeclaration embedBlock(
0212: recoder.java.StatementBlock block) {
0213:
0214: /*
0215: MethodDeclaration(modifiers,return type,Identifier, parameters,
0216: throws, StatementBlock)
0217: */
0218: recoder.java.declaration.MethodDeclaration mdecl = new recoder.java.declaration.MethodDeclaration(
0219: null, null, new ImplicitIdentifier(
0220: "<virtual_method_for_parsing>"), null, null,
0221: block);
0222: mdecl.makeParentRoleValid();
0223: return mdecl;
0224: }
0225:
0226: /**
0227: * wraps a RECODER MethodDeclaration in a class
0228: * @param mdecl the recoder.java.declaration.MethodDeclaration to wrap
0229: * @param context the recoder.java.declaration.ClassDeclaration
0230: * where the method has to be embedded
0231: * @return the enclosing recoder.java.declaration.ClassDeclaration
0232: */
0233: protected recoder.java.declaration.ClassDeclaration embedMethod(
0234: recoder.java.declaration.MethodDeclaration mdecl,
0235: Context context) {
0236:
0237: recoder.java.declaration.ClassDeclaration classContext = context
0238: .getClassContext();
0239:
0240: // add method to memberdeclaration list
0241: recoder.list.MemberDeclarationMutableList memberList = classContext
0242: .getMembers();
0243:
0244: if (memberList == null) {
0245: memberList = new recoder.list.MemberDeclarationArrayList(1);
0246: classContext.setMembers(memberList);
0247: }
0248:
0249: for (int i = 0, sz = memberList.size(); i < sz; i++) {
0250: if (memberList.getMemberDeclaration(i) instanceof recoder.java.declaration.MethodDeclaration) {
0251: recoder.java.declaration.MethodDeclaration olddecl = (recoder.java.declaration.MethodDeclaration) memberList
0252: .getMemberDeclaration(i);
0253: if (olddecl.getName().equals(mdecl.getName())) {
0254: memberList.remove(i);
0255: }
0256: }
0257: }
0258: memberList.add(mdecl);
0259:
0260: // add method to class
0261:
0262: classContext.setProgramModelInfo(servConf
0263: .getCrossReferenceSourceInfo());
0264: classContext.makeParentRoleValid();
0265: return classContext;
0266: }
0267:
0268: protected recoder.list.CompilationUnitMutableList recoderCompilationUnits(
0269: String[] cUnitStrings) {
0270: recoder.util.Debug.setLevel(500);
0271: parseSpecialClasses();
0272: recoder.list.CompilationUnitMutableList cUnits = new recoder.list.CompilationUnitArrayList();
0273: int current = 0;
0274: try {
0275: for (int i = 0; i < cUnitStrings.length; i++) {
0276: current = i;
0277: Debug.out("Reading ", cUnitStrings[i]);
0278: cUnits.add(servConf.getProgramFactory()
0279: .parseCompilationUnit(
0280: new StringReader(cUnitStrings[i])));
0281: }
0282: // run cross referencer
0283: final ChangeHistory changeHistory = servConf
0284: .getChangeHistory();
0285: for (int i = 0, sz = cUnits.size(); i < sz; i++) {
0286: current = i;
0287: cUnits.getCompilationUnit(i).makeAllParentRolesValid();
0288: changeHistory.attached(cUnits.getCompilationUnit(i));
0289: }
0290:
0291: if (changeHistory.needsUpdate()) {
0292: changeHistory.updateModel();
0293: }
0294: // transform program
0295:
0296: transformModel(cUnits);
0297: } catch (IOException ioe) {
0298: Debug.out("recoder2key: IO Error when reading"
0299: + "compilation unit (unit, exception) ",
0300: cUnitStrings[current], ioe);
0301: reportError(
0302: "IOError reading java program "
0303: + cUnitStrings[current]
0304: + ". May be file not found or missing permissions.",
0305: ioe);
0306: } catch (recoder.ParserException pe) {
0307: Debug.out("recoder2key: Recoder Parser Error when"
0308: + "reading a comiplation unit (unit, exception)",
0309: cUnitStrings[current], pe);
0310: if (pe.getCause() != null) {
0311: reportError(pe.getCause().getMessage(), pe.getCause());
0312: } else {
0313: reportError(pe.getMessage(), pe);
0314: }
0315: }
0316: return cUnits;
0317: }
0318:
0319: protected recoder.list.CompilationUnitMutableList recoderCompilationUnitsAsFiles(
0320: String[] cUnitStrings) {
0321: recoder.list.CompilationUnitMutableList cUnits = new recoder.list.CompilationUnitArrayList();
0322: parseSpecialClasses();
0323: try {
0324: cUnits = servConf.getProgramFactory()
0325: .parseCompilationUnits(cUnitStrings);
0326: final ChangeHistory changeHistory = servConf
0327: .getChangeHistory();
0328: for (int i = 0, sz = cUnits.size(); i < sz; i++) {
0329: cUnits.getCompilationUnit(i).makeAllParentRolesValid();
0330: changeHistory.attached(cUnits.getCompilationUnit(i));
0331: }
0332:
0333: if (changeHistory.needsUpdate()) {
0334: changeHistory.updateModel();
0335: }
0336:
0337: // transform program
0338: transformModel(cUnits);
0339: } catch (recoder.service.AmbiguousDeclarationException ade) {
0340: reportError(ade.getMessage(), ade);
0341: } catch (recoder.ParserException pe) {
0342: reportError(pe.getMessage(), pe);
0343: }
0344: return cUnits;
0345: }
0346:
0347: /**
0348: * adds a special compilation unit containing references to types that
0349: * have to be available in Recoder and KeY form, e.g. Exceptions
0350: * TODO
0351: */
0352: private recoder.list.CompilationUnitMutableList parseSpecial(
0353: boolean parseLibs) {
0354: recoder.ProgramFactory pf = servConf.getProgramFactory();
0355: recoder.list.CompilationUnitMutableList rcuList = new recoder.list.CompilationUnitArrayList();
0356: recoder.java.CompilationUnit rcu = null;
0357: URL jlURL = KeYResourceManager.getManager().getResourceFile(
0358: Recoder2KeY.class, javaSrcDir + "/" + "JAVALANG.TXT");
0359: if (logger.isDebugEnabled()) {
0360: logger.debug(jlURL.toString());
0361: }
0362: try {
0363: BufferedReader r = new BufferedReader(
0364: new InputStreamReader(jlURL.openStream()));
0365: for (String jl = r.readLine(); (jl != null); jl = r
0366: .readLine()) {
0367: if ((jl.charAt(0) == '#') || (jl.length() == 0)) {
0368: continue;
0369: }
0370: if ((jl.charAt(0) == '+')) {
0371: if (parseLibs) {
0372: jl = jl.substring(1);
0373: } else {
0374: continue;
0375: }
0376: }
0377: jl = jl.trim();
0378: URL jlf = KeYResourceManager.getManager()
0379: .getResourceFile(Recoder2KeY.class,
0380: javaSrcDir + "/" + jl);
0381: Reader f = new BufferedReader(new InputStreamReader(jlf
0382: .openStream()));
0383: rcu = pf.parseCompilationUnit(f);
0384: rcu.makeAllParentRolesValid();
0385: rcuList.add(rcu);
0386: if (logger.isDebugEnabled()) {
0387: logger.debug("parsed: " + jl);
0388: }
0389: }
0390:
0391: // parse a special default class
0392: rcu = pf.parseCompilationUnit(new StringReader(
0393: "public class "
0394: + JavaInfo.DEFAULT_EXECUTION_CONTEXT_CLASS
0395: + " {}"));
0396: rcu.makeAllParentRolesValid();
0397: rcuList.add(rcu);
0398: } catch (recoder.ParserException e) {
0399: e.printStackTrace(System.out);
0400: System.err
0401: .println("recoder2key: Error while parsing specials");
0402: System.err.println("recoder2key: Try to continue...");
0403: } catch (IOException e) {
0404: e.printStackTrace(System.out);
0405: System.err
0406: .println("recoder2key: Error while parsing specials");
0407: System.err
0408: .println("recoder2key: someone messed up with the resources");
0409: }
0410: return rcuList;
0411: }
0412:
0413: /**
0414: * if not parsed yet the special classes are read in and converted
0415: */
0416: public void parseSpecialClasses() {
0417: if (rec2key.parsedSpecial()) {
0418: return;
0419: }
0420: parsingLibs(true);
0421:
0422: final recoder.list.CompilationUnitMutableList specialClasses = parseSpecial(KeYUserProblemFile.parseLibSpecs);
0423: final ChangeHistory changeHistory = servConf.getChangeHistory();
0424: for (int i = 0, sz = specialClasses.size(); i < sz; i++) {
0425: specialClasses.getCompilationUnit(i)
0426: .makeAllParentRolesValid();
0427: changeHistory
0428: .attached(specialClasses.getCompilationUnit(i));
0429: }
0430:
0431: if (changeHistory.needsUpdate()) {
0432: changeHistory.updateModel();
0433: }
0434:
0435: transformModel(specialClasses);
0436:
0437: for (int i = 0, sz = specialClasses.size(); i < sz; i++) {
0438: callConvert(specialClasses.getCompilationUnit(i));
0439: }
0440:
0441: rec2key().parsedSpecial(true);
0442: parsingLibs(false);
0443: }
0444:
0445: public CompilationUnit[] readCompilationUnitsAsFiles(
0446: String[] cUnitStrings) {
0447: recoder.list.CompilationUnitMutableList cUnits = recoderCompilationUnitsAsFiles(cUnitStrings);
0448: CompilationUnit[] result = new CompilationUnit[cUnits.size()];
0449: for (int i = 0, sz = cUnits.size(); i < sz; i++) {
0450: Debug.out("R2K: ", cUnitStrings[i]);
0451: currentClass = cUnitStrings[i];
0452: result[i] = convert(cUnits.getCompilationUnit(i));
0453: currentClass = null;
0454: }
0455: return result;
0456: }
0457:
0458: public CompilationUnit readCompilationUnit(String cUnitString) {
0459: final recoder.java.CompilationUnit cc = recoderCompilationUnits(
0460: new String[] { cUnitString }).getCompilationUnit(0);
0461: return (CompilationUnit) callConvert(cc);
0462: }
0463:
0464: private String trim(String s) {
0465: if (s.length() > 150)
0466: return s.substring(0, 150) + "[...]";
0467: return s;
0468: }
0469:
0470: /**
0471: * tries to parse recoders exception position information
0472: */
0473: protected int[] extractPositionInfo(String errorMessage) {
0474: if (errorMessage == null || errorMessage.indexOf('@') == -1) {
0475: return new int[0];
0476: }
0477: String pos = errorMessage
0478: .substring(errorMessage.indexOf("@") + 1);
0479: pos = pos.substring(0, pos.indexOf(" "));
0480: int line = -1;
0481: int column = -1;
0482: try {
0483: line = Integer.parseInt(pos.substring(0, pos.indexOf('/')));
0484: column = Integer.parseInt(pos
0485: .substring(pos.indexOf('/') + 1));
0486: } catch (NumberFormatException nfe) {
0487: Debug.out("recoder2key:unresolved reference at " + "line:"
0488: + line + " column:" + column);
0489: return new int[0];
0490: } catch (StringIndexOutOfBoundsException siexc) {
0491: return new int[0];
0492: }
0493: return new int[] { line, column };
0494: }
0495:
0496: protected void reportError(String message, Throwable e) {
0497: // Attention: this highly depends on Recoders exception messages!
0498: int[] pos = extractPositionInfo(e.toString());
0499: final RuntimeException rte;
0500: if (pos.length > 0) {
0501: rte = new PosConvertException(message, pos[0], pos[1]);
0502: } else {
0503: if (e instanceof recoder.parser.ParseException) {
0504: rte = new ConvertException(
0505: (recoder.parser.ParseException) e);
0506: } else if (e instanceof de.uka.ilkd.key.parser.proofjava.ParseException) {
0507: rte = new ConvertException(
0508: (de.uka.ilkd.key.parser.proofjava.ParseException) e);
0509: } else {
0510: rte = new ConvertException(message);
0511: }
0512: }
0513: throw (RuntimeException) rte.initCause(e);
0514: }
0515:
0516: /**
0517: * parses a given JavaBlock using the context to determine the right
0518: * references and returns a statement block of recoder.
0519: * @param block a String describing a java block
0520: * @param context recoder.java.CompilationUnit in which the block has
0521: * to be interpreted
0522: * @return the parsed and resolved recoder statement block
0523: */
0524: protected recoder.java.StatementBlock recoderBlock(String block,
0525: Context context) {
0526: recoder.java.StatementBlock bl = null;
0527: parseSpecialClasses();
0528: try {
0529: bl = servConf.getProgramFactory().parseStatementBlock(
0530: new StringReader(block));
0531: bl.makeAllParentRolesValid();
0532: embedMethod(embedBlock(bl), context);
0533: context.getCompilationUnitContext().makeParentRoleValid();
0534: servConf.getCrossReferenceSourceInfo().register(bl);
0535: servConf.getChangeHistory().attached(
0536: context.getCompilationUnitContext());
0537: servConf.getChangeHistory().updateModel();
0538: } catch (de.uka.ilkd.key.util.ExceptionHandlerException e) {
0539: if (e.getCause() != null) {
0540: reportError(e.getCause().getMessage(), e.getCause());
0541: } else {
0542: reportError(e.getMessage(), e);
0543: }
0544: } catch (recoder.service.UnresolvedReferenceException e) {
0545: reportError("Could not resolve reference:"
0546: + e.getUnresolvedReference(), e);
0547: } catch (recoder.parser.ParseException e) {
0548: if (e.getCause() != null) {
0549: reportError(e.getCause().getMessage(), e.getCause());
0550: } else {
0551: reportError(e.getMessage(), e);
0552: }
0553: } catch (recoder.ModelException e) {
0554: if (e.getCause() != null) {
0555: reportError(e.getCause().getMessage(), e.getCause());
0556: } else {
0557: reportError(e.getMessage(), e);
0558: }
0559: } catch (recoder.ParserException e) {
0560: if (e.getCause() != null) {
0561: reportError(e.getCause().getMessage(), e.getCause());
0562: } else {
0563: reportError(e.getMessage(), e);
0564: }
0565: } catch (IOException e) {
0566: Debug.out("recoder2key: IOException detected. "
0567: + "(parsed program, IOException)", block, e);
0568: if (block.length() > 20)
0569: block = block.substring(0, 20) + "...";
0570: reportError("Could not access data stream "
0571: + "(e.g. file not found, wrong permissions) "
0572: + "when reading " + block + ": "
0573: + trim(e.getMessage()), e);
0574: } catch (NullPointerException e) {
0575: //to retrieve a more precise message we would need to patch Recoder
0576: reportError("Recoder parser threw exception in block:\n"
0577: + block
0578: + "\n Probably a misspelled identifier name.", e);
0579: } catch (Exception e) {
0580: reportError(e.getMessage(), e);
0581: }
0582: return bl;
0583: }
0584:
0585: /** parses a given JavaBlock using the context to determine the right
0586: * references
0587: * @param block a String describing a java block
0588: * @param context recoder.java.CompilationUnit in which the block has
0589: * to be interprested
0590: * @return the parsed and resolved JavaBlock
0591: */
0592: public JavaBlock readBlock(String block, Context context) {
0593:
0594: recoder.java.StatementBlock sb = recoderBlock(block, context);
0595: JavaBlock jb = JavaBlock
0596: .createJavaBlock((StatementBlock) callConvert(sb));
0597: return jb;
0598: }
0599:
0600: /** parses a given JavaBlock using the context to determine the right
0601: * references using an empty context
0602: * @param block a String describing a java block
0603: * @return the parsed and resolved JavaBlock
0604: */
0605: public JavaBlock readBlockWithEmptyContext(String block) {
0606: return readBlock(block, createEmptyContext());
0607: }
0608:
0609: public JavaBlock readBlockWithProgramVariables(Namespace varns,
0610: String s) {
0611: IteratorOfNamed it = varns.allElements().iterator();
0612: ListOfProgramVariable pvs = SLListOfProgramVariable.EMPTY_LIST;
0613: while (it.hasNext()) {
0614: Named n = it.next();
0615: if (n instanceof ProgramVariable) {
0616: pvs = pvs.prepend((ProgramVariable) n);
0617: }
0618: }
0619: return readBlock(s, createContext(pvs));
0620: }
0621:
0622: protected void insertToMap(recoder.ModelElement r, ModelElement k) {
0623:
0624: if (r != null) {
0625: rec2key.put(r, k);
0626: } else {
0627: // commented out because they caused an exception (they were thrown at array references)
0628: // Debug.out("Rec2Key.insertToMap : Omitting entry (r = " + r + " -> k = " + k + ")");
0629: // Debug.out("Maybe there is a bug !!");
0630: }
0631: }
0632:
0633: /**
0634: * returns the hashmap of a concrete RecodeR class to the constructor of its
0635: * corresponding KeY class. Speeds up reflection.
0636: * Attention must be overwritten by subclasses!
0637: */
0638: protected HashMap getKeYClassConstructorCache() {
0639: return recClass2keyClassCons;
0640: }
0641:
0642: /**
0643: * returns the hashmap of a concrete Java AST class to its
0644: * corresponding convert method. Speeds up reflection.
0645: * Attention must be overwritten by subclasses!
0646: */
0647: protected HashMap getMethodCache() {
0648: return ct2meth;
0649: }
0650:
0651: /** determines the right convert method using reflection
0652: * @param pe the recoder.java.JavaProgramElement to be converted
0653: * @return the converted element
0654: */
0655: protected Object callConvert(recoder.java.ProgramElement pe) {
0656:
0657: assert pe != null;
0658:
0659: final HashMap methodCache = getMethodCache();
0660: final Class contextClass = pe.getClass();
0661: Method m = (Method) methodCache.get(contextClass);
0662:
0663: if (m == null) {
0664: Class[] context = new Class[] { contextClass };
0665:
0666: final LinkedList l = new LinkedList();
0667: while (m == null && context[0] != null) {
0668: l.add(contextClass);
0669: try {
0670: m = getClass().getMethod("convert", context);
0671: } catch (NoSuchMethodException nsme) {
0672: context[0] = context[0].getSuperclass();
0673: Debug.out("recoder2key: method not found. "
0674: + "Next try with ", context[0]);
0675: }
0676: }
0677: assert m != null : "Could not find convert method";
0678: final Iterator it = l.iterator();
0679: while (it.hasNext()) {
0680: methodCache.put(it.next(), m);
0681: }
0682: }
0683:
0684: Object o = null;
0685: try {
0686: o = m.invoke(this , new Object[] { pe });
0687: } catch (IllegalAccessException iae) {
0688: Debug.out("recoder2key: cannot access method ", iae);
0689: throw new ConvertException(
0690: "recoder2key: cannot access method" + iae);
0691: } catch (IllegalArgumentException iarg) {
0692: Debug.out("recoder2key: wrong method arguments ", iarg);
0693: throw new ConvertException(
0694: "recoder2key: wrong method arguments" + iarg);
0695: } catch (InvocationTargetException ite) {
0696: Debug.out("recoder2key: called method threw exception ",
0697: ite.getTargetException());
0698: if (ite.getTargetException() instanceof ConvertException) {
0699: throw (ConvertException) ite.getTargetException();
0700: } else {
0701: //ite.getTargetException().printStackTrace();
0702: throw new ConvertException(
0703: "recoder2key: called method " + m
0704: + " threw exception:"
0705: + ite.getTargetException());
0706: }
0707: }
0708:
0709: if ((currentClass != null) && (o instanceof Statement)
0710: && !(o instanceof SchemaVariable)) {
0711: ((JavaProgramElement) o).setParentClass(currentClass);
0712: }
0713:
0714: return o;
0715: }
0716:
0717: /**
0718: * constructs the name of the corresponding KeYClass
0719: * @param recoderClass Class that is the original recoder
0720: * @return String containing the KeY-Classname
0721: */
0722: protected String getKeYName(Class recoderClass) {
0723: // value of recoderPrefixLength is: "recoder.".length()
0724: final int recoderPrefixLength = 8;
0725:
0726: return "de.uka.ilkd.key."
0727: + recoderClass.getName().substring(recoderPrefixLength);
0728: }
0729:
0730: /** gets the KeY-Class related to the recoder one
0731: * @param recoderClass the original Class
0732: * @return the related KeY Class
0733: */
0734: protected Class getKeYClass(Class recoderClass) {
0735: try {
0736: return Class.forName(getKeYName(recoderClass));
0737: } catch (ClassNotFoundException cnfe) {
0738: Debug.out("There is an AST class missing at KeY.", cnfe);
0739: throw new ConvertException(
0740: "There is an AST class missing at KeY. " + cnfe);
0741: } catch (ExceptionInInitializerError initErr) {
0742: Debug.out("recoder2key: Failed initializing class ",
0743: initErr);
0744: Debug.fail();
0745: } catch (LinkageError le) {
0746: Debug.out("recoder2key: Linking class failed.", le);
0747: Debug.fail();
0748: }
0749: return null;
0750: }
0751:
0752: /** determines the right standard constructor of the KeYClass
0753: * @param recoderClass the Class of the recoder AST object
0754: * @return the Constructor of the right KeY-Class
0755: */
0756: protected Constructor getKeYClassConstructor(Class recoderClass) {
0757: Constructor result = null;
0758: try {
0759: result = (Constructor) getKeYClassConstructorCache().get(
0760: recoderClass);
0761: if (result == null) {
0762: result = getKeYClass(recoderClass).getConstructor(
0763: new Class[] { ExtList.class });
0764: getKeYClassConstructorCache().put(recoderClass, result);
0765: }
0766: } catch (NoSuchMethodException nsme) {
0767: Debug.out("recoder2key: constructor not found. ", nsme);
0768: } catch (SecurityException se) {
0769: Debug.out("recoder2key: access denied. ", se);
0770: }
0771: return result;
0772: }
0773:
0774: /** collects children and adds their converted KeY-counterpart to
0775: * the list of childrem
0776: * @param pe the NonTerminalProgramElement that needs its
0777: * children before being converted
0778: * @return the list of children after conversion
0779: */
0780: protected ExtList collectChildren(
0781: recoder.java.NonTerminalProgramElement pe) {
0782: ExtList children = new ExtList();
0783: for (int i = 0, childCount = pe.getChildCount(); i < childCount; i++) {
0784: children.add(callConvert(pe.getChildAt(i)));
0785: }
0786: recoder.list.CommentList l = pe.getComments();
0787: if (l != null) {
0788: for (int i = 0, sz = l.size(); i < sz; i++) {
0789: children.add(convert(l.getComment(i)));
0790: }
0791: }
0792: children.add(positionInfo(pe));
0793: return children;
0794: }
0795:
0796: /** collects comments and adds their converted KeY-counterpart to
0797: * the list of childrem
0798: * @param pe the ProgramElement that needs its
0799: * comments before being converted
0800: * @return the list of comments after conversion
0801: */
0802: protected ExtList collectComments(recoder.java.ProgramElement pe) {
0803: ExtList children = new ExtList();
0804: recoder.list.CommentList l = pe.getComments();
0805: if (l != null) {
0806: for (int i = 0, sz = l.size(); i < sz; i++) {
0807: children.add(convert(l.getComment(i)));
0808: }
0809: }
0810: return children;
0811: }
0812:
0813: protected PositionInfo positionInfo(recoder.java.SourceElement se) {
0814: Position relPos = new Position(se.getRelativePosition()
0815: .getLine(), se.getRelativePosition().getColumn());
0816: Position startPos = new Position(se.getStartPosition()
0817: .getLine(), se.getStartPosition().getColumn());
0818: Position endPos = new Position(se.getEndPosition().getLine(),
0819: se.getEndPosition().getColumn());
0820: if ((!inLoopInit))
0821: return new PositionInfo(relPos, startPos, endPos,
0822: currentClass);
0823: else
0824: return new PositionInfo(relPos, startPos, endPos);
0825:
0826: }
0827:
0828: /**
0829: * the standard case.
0830: * @param pe the recoder.java.ProgramElement to be converted
0831: * @return the converted de.uka.ilkd.key.java.JavaProgramElement
0832: */
0833: public ProgramElement convert(recoder.java.JavaProgramElement pe) {
0834: ProgramElement result = null;
0835: ExtList parameter;
0836:
0837: if (pe instanceof recoder.java.JavaNonTerminalProgramElement) {
0838: parameter = collectChildren((recoder.java.JavaNonTerminalProgramElement) pe);
0839: } else {
0840: parameter = new ExtList();
0841: }
0842: try {
0843: result = (ProgramElement) getKeYClassConstructor(
0844: pe.getClass()).newInstance(
0845: new Object[] { parameter });
0846: } catch (InstantiationException e) {
0847: Debug.out("recoder2key: invocation of constructor failed.",
0848: e);
0849: } catch (InvocationTargetException ite) {
0850: Debug.out("recoder2key: invocation of constructor failed.",
0851: ite.getTargetException());
0852: } catch (IllegalAccessException iae) {
0853: Debug.out("recoder2key: access denied.", iae);
0854: } catch (IllegalArgumentException iae) {
0855: Debug.out("recoder2key: illegal arguments.", iae);
0856: }
0857: return result;
0858: }
0859:
0860: // ------------------- operators ----------------------
0861:
0862: public Instanceof convert(
0863: recoder.java.expression.operator.Instanceof rio) {
0864: return new Instanceof((Expression) callConvert(rio
0865: .getExpressionAt(0)), (TypeReference) callConvert(rio
0866: .getTypeReference()));
0867:
0868: }
0869:
0870: /**
0871: * converts the passive expression of the recoder extensions
0872: * to the KeYDependance
0873: */
0874: public PassiveExpression convert(
0875: de.uka.ilkd.key.java.recoderext.PassiveExpression pass) {
0876: return new PassiveExpression(collectChildren(pass));
0877: }
0878:
0879: /**
0880: * converts the parenthesized expression to the KeYDependance
0881: */
0882: public ParenthesizedExpression convert(
0883: recoder.java.expression.ParenthesizedExpression x) {
0884: // first we need to collect all children
0885: Debug
0886: .assertTrue(!(x instanceof de.uka.ilkd.key.java.recoderext.PassiveExpression));
0887: return new ParenthesizedExpression(collectChildren(x));
0888: }
0889:
0890: /**
0891: * converts the recoder.java.Comment to the KeYDependance
0892: */
0893: public Comment convert(recoder.java.Comment rc) {
0894: return new Comment(rc.getText());
0895: }
0896:
0897: /**
0898: * converts the recoder.java.expression.operator.NewArray
0899: * node to the KeYDependance
0900: */
0901: public NewArray convert(
0902: recoder.java.expression.operator.NewArray newArr) {
0903: // first we need to collect all children
0904: ExtList children = collectChildren(newArr);
0905: // now we have to extract the array initializer
0906: // is stored separately and must not appear in the children list
0907: ArrayInitializer arrInit = (ArrayInitializer) children
0908: .get(ArrayInitializer.class);
0909: children.remove(arrInit);
0910:
0911: recoder.abstraction.Type javaType = servConf
0912: .getCrossReferenceSourceInfo().getType(newArr);
0913:
0914: return new NewArray(children, getKeYJavaType(javaType),
0915: arrInit, newArr.getDimensions());
0916: }
0917:
0918: /**
0919: * converts the recoder.java.expression.operator.CopyAssignment
0920: * node to the KeYDependance
0921: */
0922: public CopyAssignment convert(
0923: recoder.java.expression.operator.CopyAssignment ass) {
0924: return new CopyAssignment(collectChildren(ass));
0925: }
0926:
0927: /**
0928: * converts the recoder.java.expression.operator.PostIncrement
0929: * node to the KeYDependance
0930: */
0931: public PostIncrement convert(
0932: recoder.java.expression.operator.PostIncrement postInc) {
0933: return new PostIncrement(collectChildren(postInc));
0934: }
0935:
0936: /**
0937: * converts the recoder.java.expression.operator.PreIncrement
0938: * node to the KeYDependance
0939: */
0940: public PreIncrement convert(
0941: recoder.java.expression.operator.PreIncrement preInc) {
0942: return new PreIncrement(collectChildren(preInc));
0943: }
0944:
0945: /**
0946: * converts the recoder.java.expression.operator.PostDecrement
0947: * node to the KeYDependance
0948: */
0949: public PostDecrement convert(
0950: recoder.java.expression.operator.PostDecrement postDec) {
0951: return new PostDecrement(collectChildren(postDec));
0952: }
0953:
0954: /**
0955: * converts the recoder.java.expression.operator.PreDecrement
0956: * node to the KeYDependance
0957: */
0958: public PreDecrement convert(
0959: recoder.java.expression.operator.PreDecrement preDec) {
0960: return new PreDecrement(collectChildren(preDec));
0961: }
0962:
0963: /**
0964: * converts the recoder.java.expression.operator.Minus
0965: * node to the KeYDependance
0966: */
0967: public Minus convert(recoder.java.expression.operator.Minus minus) {
0968: return new Minus(collectChildren(minus));
0969: }
0970:
0971: /**
0972: * converts the recoder.java.expression.operator.Plus
0973: * node to the KeYDependance
0974: */
0975: public Plus convert(recoder.java.expression.operator.Plus plus) {
0976: return new Plus(collectChildren(plus));
0977: }
0978:
0979: /**
0980: * converts the recoder.java.expression.operator.Times
0981: * node to the KeYDependance
0982: */
0983: public Times convert(recoder.java.expression.operator.Times times) {
0984: return new Times(collectChildren(times));
0985: }
0986:
0987: /**
0988: * converts the recoder.java.expression.operator.Divide
0989: * node to the KeYDependance
0990: */
0991: public Divide convert(recoder.java.expression.operator.Divide div) {
0992: return new Divide(collectChildren(div));
0993: }
0994:
0995: /**
0996: * converts the recoder.java.expression.operator.PlusAssignment
0997: * node to the KeYDependance
0998: */
0999: public PlusAssignment convert(
1000: recoder.java.expression.operator.PlusAssignment plus) {
1001: return new PlusAssignment(collectChildren(plus));
1002: }
1003:
1004: /**
1005: * converts the recoder.java.expression.operator.MinusAssignment
1006: * node to the KeYDependance
1007: */
1008: public MinusAssignment convert(
1009: recoder.java.expression.operator.MinusAssignment minus) {
1010: return new MinusAssignment(collectChildren(minus));
1011: }
1012:
1013: /**
1014: * converts the recoder.java.expression.operator.TimesAssignment
1015: * node to the KeYDependance
1016: */
1017: public TimesAssignment convert(
1018: recoder.java.expression.operator.TimesAssignment times) {
1019: return new TimesAssignment(collectChildren(times));
1020: }
1021:
1022: /**
1023: * converts the recoder.java.expression.operator.DivideAssignment
1024: * node to the KeYDependance
1025: */
1026: public DivideAssignment convert(
1027: recoder.java.expression.operator.DivideAssignment div) {
1028: return new DivideAssignment(collectChildren(div));
1029: }
1030:
1031: /**
1032: * converts the recoder.java.expression.operator.LessThan
1033: * node to the KeYDependance
1034: */
1035: public LessThan convert(recoder.java.expression.operator.LessThan op) {
1036: return new LessThan(collectChildren(op));
1037: }
1038:
1039: /**
1040: * converts the recoder.java.expression.operator.LessOrEquals
1041: * node to the KeYDependance
1042: */
1043: public LessOrEquals convert(
1044: recoder.java.expression.operator.LessOrEquals op) {
1045: return new LessOrEquals(collectChildren(op));
1046: }
1047:
1048: /**
1049: * converts the recoder.java.expression.operator.GreaterThan
1050: * node to the KeYDependance
1051: */
1052: public GreaterThan convert(
1053: recoder.java.expression.operator.GreaterThan op) {
1054: return new GreaterThan(collectChildren(op));
1055: }
1056:
1057: /**
1058: * converts the recoder.java.expression.operator.GreaterOrEquals
1059: * node to the KeYDependance
1060: */
1061: public GreaterOrEquals convert(
1062: recoder.java.expression.operator.GreaterOrEquals op) {
1063: return new GreaterOrEquals(collectChildren(op));
1064: }
1065:
1066: /**
1067: * converts the recoder.java.expression.operator.Equals
1068: * node to the KeYDependance
1069: */
1070: public Equals convert(recoder.java.expression.operator.Equals op) {
1071: return new Equals(collectChildren(op));
1072: }
1073:
1074: /**
1075: * converts the recoder.java.expression.operator.NotEquals
1076: * node to the KeYDependance
1077: */
1078: public NotEquals convert(
1079: recoder.java.expression.operator.NotEquals op) {
1080: return new NotEquals(collectChildren(op));
1081: }
1082:
1083: /**
1084: * converts the recoder.java.expression.operator.LogicalNot
1085: * node to the KeYDependance
1086: */
1087: public LogicalNot convert(
1088: recoder.java.expression.operator.LogicalNot op) {
1089: return new LogicalNot(collectChildren(op));
1090: }
1091:
1092: /**
1093: * converts the recoder.java.expression.operator.LogicalAnd
1094: * node to the KeYDependance
1095: */
1096: public LogicalAnd convert(
1097: recoder.java.expression.operator.LogicalAnd op) {
1098: return new LogicalAnd(collectChildren(op));
1099: }
1100:
1101: /**
1102: * converts the recoder.java.expression.operator.LogicalOr
1103: * node to the KeYDependance
1104: */
1105: public LogicalOr convert(
1106: recoder.java.expression.operator.LogicalOr op) {
1107: return new LogicalOr(collectChildren(op));
1108: }
1109:
1110: /** convert a recoder ArrayInitializer to a KeY array initializer*/
1111: public ArrayInitializer convert(
1112: recoder.java.expression.ArrayInitializer ai) {
1113: return new ArrayInitializer(collectChildren(ai));
1114: }
1115:
1116: //------------------- literals --------------------------------------
1117:
1118: /** convert a recoder IntLiteral to a KeY IntLiteral */
1119: public IntLiteral convert(
1120: recoder.java.expression.literal.IntLiteral intLit) {
1121: // if there are comments to take into consideration
1122: // change parameter to ExtList
1123: return new IntLiteral(intLit.getValue());
1124: }
1125:
1126: /** convert a recoder BooleanLiteral to a KeY BooleanLiteral */
1127: public BooleanLiteral convert(
1128: recoder.java.expression.literal.BooleanLiteral booleanLit) {
1129:
1130: // if there are comments to take into consideration
1131: // change parameter to ExtList
1132: return (booleanLit.getValue() ? BooleanLiteral.TRUE
1133: : BooleanLiteral.FALSE);
1134: }
1135:
1136: /** convert a recoder StringLiteral to a KeY StringLiteral */
1137: public StringLiteral convert(
1138: recoder.java.expression.literal.StringLiteral stringLit) {
1139:
1140: // if there are comments to take into consideration
1141: // change parameter to ExtList
1142: return new StringLiteral(stringLit.getValue());
1143: }
1144:
1145: /** convert a recoder DoubleLiteral to a KeY DoubleLiteral */
1146: public DoubleLiteral convert(
1147: recoder.java.expression.literal.DoubleLiteral doubleLit) {
1148:
1149: // if there are comments to take into consideration
1150: // change parameter to ExtList
1151: return new DoubleLiteral(doubleLit.getValue());
1152: }
1153:
1154: /** convert a recoder FloatLiteral to a KeY FloatLiteral */
1155: public FloatLiteral convert(
1156: recoder.java.expression.literal.FloatLiteral floatLit) {
1157:
1158: // if there are comments to take into consideration
1159: // change parameter to ExtList
1160: return new FloatLiteral(floatLit.getValue());
1161: }
1162:
1163: /** convert a recoder LongLiteral to a KeY LongLiteral */
1164: public LongLiteral convert(
1165: recoder.java.expression.literal.LongLiteral longLit) {
1166:
1167: // if there are comments to take into consideration
1168: // change parameter to ExtList
1169: return new LongLiteral(longLit.getValue());
1170: }
1171:
1172: /** convert a recoder CharLiteral to a KeY CharLiteral */
1173: public CharLiteral convert(
1174: recoder.java.expression.literal.CharLiteral charLit) {
1175:
1176: // if there are comments to take into consideration
1177: // change parameter to ExtList
1178:
1179: return new CharLiteral(charLit.getValue());
1180: }
1181:
1182: /** convert a recoder NullLiteral to a KeY NullLiteral */
1183: public NullLiteral convert(
1184: recoder.java.expression.literal.NullLiteral nullLit) {
1185:
1186: recoder.abstraction.Type javaType = getServiceConfiguration()
1187: .getCrossReferenceSourceInfo().getType(nullLit);
1188: getKeYJavaType(javaType);
1189: // if there are comments to take into consideration
1190: // change parameter to ExtList
1191: return NullLiteral.NULL;
1192: }
1193:
1194: //----------------------------------------------------------
1195:
1196: /** convert a recoder EmptyStatement to a KeY EmptyStatement*/
1197: public EmptyStatement convert(
1198: recoder.java.statement.EmptyStatement eStmnt) {
1199: // may change if comments are implemented, then
1200: // new EmptyStatement(children);
1201: return new EmptyStatement();
1202: }
1203:
1204: /** converts a recoder throw statement to a KeY throw statement*/
1205: public Throw convert(recoder.java.statement.Throw stmntThrow) {
1206: return new Throw(collectChildren(stmntThrow));
1207: }
1208:
1209: /** converts a recoder if statement to a KeY if statement*/
1210: public If convert(recoder.java.statement.If stmntIf) {
1211: return new If(collectChildren(stmntIf));
1212: }
1213:
1214: /** converts a recoder then statement to a KeY then statement*/
1215: public Then convert(recoder.java.statement.Then stmntThen) {
1216: return new Then(collectChildren(stmntThen));
1217: }
1218:
1219: /** converts a recoder else statement to a KeY else statement*/
1220: public Else convert(recoder.java.statement.Else stmntElse) {
1221: return new Else(collectChildren(stmntElse));
1222: }
1223:
1224: /** convert a recoder EmptyStatement to a KeY EmptyStatement*/
1225: public ProgramElementName convert(recoder.java.Identifier id) {
1226: return VariableNamer.parseName(id.getText(),
1227: (Comment[]) collectComments(id).collect(Comment.class));
1228: }
1229:
1230: /** convert a recoder EmptyStatement to a KeY EmptyStatement*/
1231: public ProgramElementName convert(ImplicitIdentifier id) {
1232:
1233: return new ProgramElementName(id.getText(),
1234: (Comment[]) collectComments(id).collect(Comment.class));
1235: }
1236:
1237: /** convert a recoder StamentBlock to a KeY StatementBlock*/
1238: public StatementBlock convert(recoder.java.StatementBlock block) {
1239: return new StatementBlock(collectChildren(block));
1240: }
1241:
1242: /** convert a recoder StamentBlock to a KeY StatementBlock*/
1243: public SynchronizedBlock convert(
1244: recoder.java.statement.SynchronizedBlock block) {
1245: return new SynchronizedBlock(collectChildren(block));
1246: }
1247:
1248: /** convert a recoder return statement to a KeY return statement */
1249: public Return convert(recoder.java.statement.Return stmntReturn) {
1250: return new Return(collectChildren(stmntReturn));
1251: }
1252:
1253: /** convert a recoder try statement to a KeY try statement */
1254: public Try convert(recoder.java.statement.Try stmntTry) {
1255: return new Try(collectChildren(stmntTry));
1256: }
1257:
1258: /** convert a recoder catch statement to a KeY catch statement */
1259: public Catch convert(recoder.java.statement.Catch stmntCatch) {
1260: return new Catch(collectChildren(stmntCatch));
1261: }
1262:
1263: /** convert a recoder finally statement to a KeY finally statement */
1264: public Finally convert(recoder.java.statement.Finally stmntFinally) {
1265: return new Finally(collectChildren(stmntFinally));
1266: }
1267:
1268: /** convert a recoderext MethodFrameStatement to a KeY MethodFrameStatement*/
1269: public MethodFrame convert(
1270: de.uka.ilkd.key.java.recoderext.MethodCallStatement rmcs) {
1271: ProgramVariable resVar = null;
1272: if (rmcs.getResultVariable() != null) {
1273: recoder.java.Expression rvar = rmcs.getResultVariable();
1274: if (rvar instanceof recoder.java.reference.VariableReference) {
1275: resVar = convert((recoder.java.reference.VariableReference) rvar);
1276: } else if (rvar instanceof recoder.java.reference.UncollatedReferenceQualifier) {
1277: try {
1278: resVar = (ProgramVariable) callConvert(rvar);
1279: } catch (ClassCastException e) {
1280: throw new ConvertException(
1281: "recoder2key: Expression is not a variable reference.");
1282: }
1283: }
1284: }
1285: StatementBlock block = null;
1286: if (rmcs.getBody() != null) {
1287: block = (StatementBlock) callConvert(rmcs.getBody());
1288: }
1289:
1290: return new MethodFrame(resVar, convert(rmcs
1291: .getExecutionContext()), block);
1292: }
1293:
1294: /** convert a recoderext MethodBodyStatement to a KeY MethodBodyStatement*/
1295: public MethodBodyStatement convert(
1296: de.uka.ilkd.key.java.recoderext.MethodBodyStatement rmbs) {
1297:
1298: final TypeReference bodySource = convert(rmbs.getBodySource());
1299: final IProgramVariable resultVar = rmbs.getResultVariable() != null ? (IProgramVariable) callConvert(rmbs
1300: .getResultVariable())
1301: : null;
1302: final ReferencePrefix invocationTarget = (ReferencePrefix) callConvert(rmbs
1303: .getReferencePrefix());
1304: final ProgramElementName methodName = convert(rmbs
1305: .getMethodName());
1306:
1307: final ExpressionMutableList args = rmbs.getArguments();
1308: final Expression[] keyArgs;
1309: if (args != null) {
1310: keyArgs = new Expression[args.size()];
1311: for (int i = 0, sz = args.size(); i < sz; i++) {
1312: keyArgs[i] = (Expression) callConvert(args
1313: .getExpression(i));
1314: }
1315: } else {
1316: keyArgs = new Expression[0];
1317: }
1318:
1319: final MethodReference mr = new MethodReference(
1320: new ArrayOfExpression(keyArgs), methodName,
1321: invocationTarget);
1322:
1323: return new MethodBodyStatement(bodySource, resultVar, mr);
1324: }
1325:
1326: public CatchAllStatement convert(
1327: de.uka.ilkd.key.java.recoderext.CatchAllStatement cas) {
1328: return new CatchAllStatement((StatementBlock) callConvert(cas
1329: .getStatementAt(0)),
1330: (ParameterDeclaration) callConvert(cas
1331: .getParameterDeclarationAt(0)));
1332: }
1333:
1334: // ------------------- modifiers ----------------------
1335:
1336: /**
1337: * converts the recoder public modifier to the KeY modifier
1338: */
1339: public Public convert(recoder.java.declaration.modifier.Public m) {
1340: return new Public(collectComments(m));
1341: }
1342:
1343: /**
1344: * converts the recoder protected modifier to the KeY modifier
1345: */
1346: public Protected convert(
1347: recoder.java.declaration.modifier.Protected m) {
1348: return new Protected(collectComments(m));
1349: }
1350:
1351: /**
1352: * converts the recoder private modifier to the KeY modifier
1353: */
1354: public Private convert(recoder.java.declaration.modifier.Private m) {
1355: return new Private(collectComments(m));
1356: }
1357:
1358: /**
1359: * converts the recoder static modifier to the KeY modifier
1360: */
1361: public Static convert(recoder.java.declaration.modifier.Static m) {
1362: return new Static(collectComments(m));
1363: }
1364:
1365: /**
1366: * converts the recoder abstract modifier to the KeY modifier
1367: */
1368: public Abstract convert(recoder.java.declaration.modifier.Abstract m) {
1369: return new Abstract(collectComments(m));
1370: }
1371:
1372: /**
1373: * converts the recoder final modifier to the KeY modifier
1374: */
1375: public Final convert(recoder.java.declaration.modifier.Final m) {
1376: return new Final(collectComments(m));
1377: }
1378:
1379: /**
1380: * converts the recoder native modifier to the KeY modifier
1381: */
1382: public Native convert(recoder.java.declaration.modifier.Native m) {
1383: return new Native(collectComments(m));
1384: }
1385:
1386: /**
1387: * converts the recoder transient modifier to the KeY modifier
1388: */
1389: public Transient convert(
1390: recoder.java.declaration.modifier.Transient m) {
1391: return new Transient(collectComments(m));
1392: }
1393:
1394: /**
1395: * converts the recoder synchronized modifier to the KeY modifier
1396: */
1397: public Synchronized convert(
1398: recoder.java.declaration.modifier.Synchronized m) {
1399: return new Synchronized(collectComments(m));
1400: }
1401:
1402: //------------------- declaration ---------------------
1403:
1404: public CompilationUnit convert(recoder.java.CompilationUnit cu) {
1405: return new CompilationUnit(collectChildren(cu));
1406: }
1407:
1408: public ClassInitializer convert(
1409: recoder.java.declaration.ClassInitializer ci) {
1410: return new ClassInitializer(collectChildren(ci));
1411: }
1412:
1413: public PackageSpecification convert(
1414: recoder.java.PackageSpecification ps) {
1415: return new PackageSpecification(collectChildren(ps));
1416: }
1417:
1418: public Throws convert(recoder.java.declaration.Throws t) {
1419: return new Throws(collectChildren(t));
1420: }
1421:
1422: public Extends convert(recoder.java.declaration.Extends e) {
1423: return new Extends(collectChildren(e));
1424: }
1425:
1426: public Implements convert(recoder.java.declaration.Implements e) {
1427: return new Implements(collectChildren(e));
1428: }
1429:
1430: public ClassDeclaration convert(
1431: recoder.java.declaration.ClassDeclaration td) {
1432:
1433: KeYJavaType kjt = getKeYJavaType(td);
1434: ExtList classMembers = collectChildren(td);
1435:
1436: ClassDeclaration keYClassDecl = new ClassDeclaration(
1437: classMembers, new ProgramElementName(td.getFullName()),
1438: parsingLibs);
1439:
1440: kjt.setJavaType(keYClassDecl);
1441: return keYClassDecl;
1442: }
1443:
1444: public InterfaceDeclaration convert(
1445: recoder.java.declaration.InterfaceDeclaration td) {
1446:
1447: KeYJavaType kjt = getKeYJavaType(td);
1448: ExtList members = collectChildren(td);
1449: InterfaceDeclaration keYInterfaceDecl = new InterfaceDeclaration(
1450: members, new ProgramElementName(td.getFullName()),
1451: parsingLibs);
1452: kjt.setJavaType(keYInterfaceDecl);
1453:
1454: return keYInterfaceDecl;
1455: }
1456:
1457: /**
1458: * converts a recoder LocalVariableDeclaration to a KeY
1459: * LocalVariableDeclaration
1460: * (especially the declaration type of its parent is determined
1461: * and handed over)
1462: */
1463: public LocalVariableDeclaration convert(
1464: recoder.java.declaration.LocalVariableDeclaration lvd) {
1465: return new LocalVariableDeclaration(collectChildren(lvd));
1466: }
1467:
1468: /**
1469: * converts a recoder ParameterDeclaration to a KeY
1470: * ParameterDeclaration
1471: * (especially the declaration type of its parent is determined
1472: * and handed over)
1473: */
1474: public ParameterDeclaration convert(
1475: recoder.java.declaration.ParameterDeclaration pd) {
1476: return new ParameterDeclaration(
1477: collectChildren(pd),
1478: pd.getASTParent() instanceof recoder.java.declaration.InterfaceDeclaration);
1479: }
1480:
1481: /** convert a recoder FieldDeclaration to a KeY
1482: * FieldDeclaration
1483: * (especially the declaration type of its parent is determined
1484: * and handed over)
1485: */
1486: public FieldDeclaration convert(
1487: recoder.java.declaration.FieldDeclaration fd) {
1488: return new FieldDeclaration(
1489: collectChildren(fd),
1490: fd.getASTParent() instanceof recoder.java.declaration.InterfaceDeclaration);
1491: }
1492:
1493: /** convert a recoder ConstructorDeclaration to a KeY
1494: * ProgramMethod
1495: * (especially the declaration type of its parent is determined
1496: * and handed over)
1497: */
1498: public ProgramMethod convert(
1499: recoder.java.declaration.ConstructorDeclaration cd) {
1500: ConstructorDeclaration consDecl = new ConstructorDeclaration(
1501: collectChildren(cd),
1502: cd.getASTParent() instanceof recoder.java.declaration.InterfaceDeclaration);
1503: recoder.abstraction.ClassType cont = servConf
1504: .getCrossReferenceSourceInfo().getContainingClassType(
1505: (recoder.abstraction.Member) cd);
1506:
1507: ProgramMethod result = new ProgramMethod(consDecl,
1508: getKeYJavaType(cont),
1509: getKeYJavaType(cd.getReturnType()), positionInfo(cd));
1510: insertToMap(cd, result);
1511: return result;
1512: }
1513:
1514: /** convert a recoder DefaultConstructor to a KeY
1515: * ProgramMethod
1516: * (especially the declaration type of its parent is determined
1517: * and handed over)
1518: */
1519: public ProgramMethod convert(
1520: recoder.abstraction.DefaultConstructor dc) {
1521: ExtList children = new ExtList();
1522: children.add(new ProgramElementName(dc.getName()));
1523: ConstructorDeclaration consDecl = new ConstructorDeclaration(
1524: children, dc.getContainingClassType().isInterface());
1525: recoder.abstraction.ClassType cont = dc
1526: .getContainingClassType();
1527: ProgramMethod result = new ProgramMethod(consDecl,
1528: getKeYJavaType(cont),
1529: getKeYJavaType(dc.getReturnType()),
1530: PositionInfo.UNDEFINED);
1531: insertToMap(dc, result);
1532: return result;
1533: }
1534:
1535: public TypeCast convert(recoder.java.expression.operator.TypeCast c) {
1536: return new TypeCast((Expression) callConvert(c
1537: .getExpressionAt(0)), (TypeReference) callConvert(c
1538: .getTypeReference()));
1539: }
1540:
1541: private KeYJavaType lookup(recoder.abstraction.Type t) {
1542: return (KeYJavaType) rec2key.toKeY(t);
1543: }
1544:
1545: private boolean isObject(recoder.abstraction.ClassType ct) {
1546: return "java.lang.Object".equals(ct.getFullName())
1547: || "Object".equals(ct.getName());
1548: }
1549:
1550: private Sort createObjectSort(recoder.abstraction.ClassType ct,
1551: SetOfSort super s) {
1552: final boolean abstractOrInterface = ct.isAbstract()
1553: || ct.isInterface();
1554: return new ClassInstanceSortImpl(new Name(ct.getFullName()),
1555: super s, abstractOrInterface);
1556: }
1557:
1558: private SetOfSort directSuperSorts(
1559: recoder.abstraction.ClassType classType) {
1560:
1561: recoder.list.ClassTypeList super s = classType.getSupertypes();
1562: SetOfSort ss = SetAsListOfSort.EMPTY_SET;
1563: for (int i = 0; i < super s.size(); i++) {
1564: ss = ss.add(getKeYJavaType(super s.getClassType(i))
1565: .getSort());
1566: }
1567:
1568: if (ss == SetAsListOfSort.EMPTY_SET && !isObject(classType)) {
1569: ss = ss.add(javaInfo().getJavaLangObjectAsSort());
1570: }
1571: return ss;
1572: }
1573:
1574: private KeYJavaType getKeYJavaType(recoder.abstraction.Type t) {
1575: if (t == null) {
1576: return null; //this can originate from 'void'
1577: }
1578: KeYJavaType kjt = lookup(t);
1579:
1580: if (kjt != null) {
1581: return kjt;
1582: }
1583: // create a new KeYJavaType
1584: Sort s = null;
1585: if (t instanceof recoder.abstraction.PrimitiveType) {
1586: s = typeConverter.getPrimitiveSort(PrimitiveType
1587: .getPrimitiveType(t.getFullName()));
1588: if (s == null) {
1589: s = new PrimitiveSort(new Name(t.getFullName()));
1590: namespaces.sorts().add(s);
1591: Debug.out("create primitive sort not backed by LDT", s);
1592: }
1593: addKeYJavaType(t, s);
1594: } else if (t instanceof recoder.abstraction.NullType) {
1595: s = Sort.NULL;
1596: addKeYJavaType(t, s);
1597: } else if (t instanceof recoder.abstraction.ClassType) {
1598: recoder.abstraction.ClassType ct = (recoder.abstraction.ClassType) t;
1599: if (ct.isInterface()) {
1600: s = createObjectSort(ct, directSuperSorts(ct).add(
1601: javaInfo().getJavaLangObjectAsSort()));
1602: } else {
1603: s = createObjectSort(ct, directSuperSorts(ct));
1604: }
1605: recoder.list.ConstructorList cl = t.getProgramModelInfo()
1606: .getConstructors((recoder.abstraction.ClassType) t);
1607: addKeYJavaType(t, s);
1608: if (cl.size() == 1
1609: && (cl.getConstructor(0) instanceof recoder.abstraction.DefaultConstructor)) {
1610: convert((recoder.abstraction.DefaultConstructor) cl
1611: .getConstructor(0));
1612: }
1613: } else if (t instanceof recoder.abstraction.ArrayType) {
1614: recoder.abstraction.Type bt = ((recoder.abstraction.ArrayType) t)
1615: .getBaseType();
1616:
1617: kjt = getKeYJavaType(bt);
1618:
1619: s = ArraySortImpl.getArraySort(kjt.getSort(), javaInfo()
1620: .getJavaLangObjectAsSort(), javaInfo()
1621: .getJavaLangCloneableAsSort(), javaInfo()
1622: .getJavaIoSerializableAsSort());
1623: addKeYJavaType(t, s);
1624: }
1625: return lookup(t);
1626: }
1627:
1628: private KeYJavaType addKeYJavaType(recoder.abstraction.Type t,
1629: Sort s) {
1630: KeYJavaType result = null;
1631: if (!(t instanceof recoder.java.declaration.TypeDeclaration)) {
1632: Type type = null;
1633: if (t instanceof recoder.abstraction.PrimitiveType) {
1634: type = PrimitiveType.getPrimitiveType(t.getFullName());
1635: result = typeConverter.getKeYJavaType(type);
1636: if (result == null) {
1637: Debug.out(
1638: "recoder2key: create new KeYJavaType for",
1639: t);
1640: Debug.out("recoder2key: this should not happen");
1641: result = new KeYJavaType(type, s);
1642: }
1643: } else if (t instanceof recoder.abstraction.NullType) {
1644: type = NullType.JAVA_NULL;
1645: if (namespaces.sorts().lookup(s.name()) == null) {
1646: setUpSort(s);
1647: }
1648: result = new KeYJavaType(type, s);
1649: } else if (t instanceof ClassFile) {
1650: setUpSort(s);
1651: result = new KeYJavaType(s);
1652: insertToMap(t, result);
1653: type = createTypeDeclaration((ClassFile) t);
1654:
1655: return (KeYJavaType) rec2key.toKeY(t);
1656: } else if (t instanceof recoder.abstraction.ArrayType) {
1657: setUpSort(s);
1658: result = new KeYJavaType(s);
1659: } else {
1660: Debug.out("recoder2key: unknown type", t);
1661: Debug.fail();
1662: result = new KeYJavaType();
1663: }
1664: } else {
1665: setUpSort(s);
1666: result = new KeYJavaType(s);
1667: }
1668: insertToMap(t, result);
1669:
1670: // delayed creation of virtual array declarations
1671: // to avoid cycles
1672: if (t instanceof recoder.abstraction.ArrayType) {
1673: result.setJavaType(createArrayType(
1674: getKeYJavaType(((recoder.abstraction.ArrayType) t)
1675: .getBaseType()), (KeYJavaType) rec2key
1676: .toKeY(t)));
1677: }
1678:
1679: return (KeYJavaType) rec2key.toKeY(t); //usually this equals result,
1680: //sometimes however, there is a 'legacy' type in the mapping,
1681: //which has priority
1682: }
1683:
1684: private TypeDeclaration createTypeDeclaration(ClassFile cf) {
1685: final KeYJavaType classType = getKeYJavaType(cf);
1686:
1687: final Modifier[] modifiers = getModifiers(cf);
1688: final ProgramElementName name = new ProgramElementName(cf
1689: .getName());
1690: final ProgramElementName fullname = new ProgramElementName(cf
1691: .getFullName());
1692:
1693: ClassTypeList super type = cf.getSupertypes();
1694:
1695: TypeReference[] implements Types = null;
1696: TypeReference extendType = null;
1697:
1698: LinkedList implements List = new LinkedList();
1699: if (super type != null) {
1700: for (int i = 0; i < super type.size(); i++) {
1701: recoder.abstraction.ClassType ct = super type
1702: .getClassType(i);
1703: final KeYJavaType kjt = getKeYJavaType(ct);
1704: final TypeReference tr = new TypeRef(
1705: new ProgramElementName(ct.getFullName()), 0,
1706: null, kjt);
1707: if (ct.isInterface()) {
1708: implements List.add(tr);
1709: } else {
1710: Debug.assertTrue(extendType == null);
1711: extendType = tr;
1712: }
1713: }
1714: implements Types = (TypeReference[]) implements List
1715: .toArray(new TypeReference[implements List.size()]);
1716: }
1717:
1718: final Extends ext = (extendType == null ? null : new Extends(
1719: extendType));
1720:
1721: final Implements impl = implements Types == null ? null
1722: : new Implements(implements Types);
1723:
1724: final boolean parentIsInterface = cf.getContainingClassType() != null ? cf
1725: .getContainingClassType().isInterface()
1726: : false;
1727:
1728: // for the moment no members
1729:
1730: MemberDeclaration[] members = new MemberDeclaration[0];
1731:
1732: TypeDeclaration td;
1733: if (cf.isInterface()) {
1734: td = new InterfaceDeclaration(modifiers, name, fullname,
1735: ext, members, true);
1736: } else {
1737: td = new ClassDeclaration(modifiers, name, ext, fullname,
1738: impl, members, parentIsInterface, true);
1739: }
1740: classType.setJavaType(td);
1741: return td;
1742: }
1743:
1744: /**
1745: * retrieve the modiefiers of <tt>cf</tt>
1746: * @param cf the ByteCodeElement whose modifiers are determined
1747: * @return cf's modifiers
1748: */
1749: private Modifier[] getModifiers(recoder.bytecode.ByteCodeElement cf) {
1750: LinkedList mods = new LinkedList();
1751: if (cf.isNative()) {
1752: mods.add(new Native());
1753: }
1754: if (cf.isAbstract()) {
1755: mods.add(new Abstract());
1756: }
1757: if (cf.isPublic()) {
1758: mods.add(new Public());
1759: } else if (cf.isPrivate()) {
1760: mods.add(new Private());
1761: } else if (cf.isProtected()) {
1762: mods.add(new Protected());
1763: }
1764: if (cf.isFinal()) {
1765: mods.add(new Final());
1766: }
1767: if (cf.isSynchronized()) {
1768: mods.add(new Synchronized());
1769: }
1770: return (Modifier[]) mods.toArray(new Modifier[mods.size()]);
1771: }
1772:
1773: /**
1774: * Insert sorts into the namespace, add symbols that may have been
1775: * defined by a sort to the function namespace (e.g. functions for
1776: * collection sorts)
1777: */
1778: protected void setUpSort(Sort s) {
1779: namespaces.sorts().add(s);
1780: if (s instanceof NonCollectionSort) {
1781: NonCollectionSort ns = (NonCollectionSort) s;
1782: namespaces.sorts().add(ns.getSetSort());
1783: namespaces.sorts().add(ns.getSequenceSort());
1784: namespaces.sorts().add(ns.getBagSort());
1785: }
1786: if (s instanceof SortDefiningSymbols) {
1787: ((SortDefiningSymbols) s).addDefinedSymbols(namespaces
1788: .functions(), namespaces.sorts());
1789: }
1790: }
1791:
1792: // ----------------- references ----------------------------------- //
1793:
1794: /**
1795: * converts an execution context
1796: */
1797: public ExecutionContext convert(
1798: de.uka.ilkd.key.java.recoderext.ExecutionContext ec) {
1799:
1800: return new ExecutionContext(collectChildren(ec));
1801:
1802: }
1803:
1804: /**
1805: * converts a recoder this constructor reference.
1806: * @return the this reference in the KeY data structures
1807: */
1808: public ThisConstructorReference convert(
1809: recoder.java.reference.ThisConstructorReference tcr) {
1810:
1811: return new ThisConstructorReference(collectChildren(tcr));
1812: }
1813:
1814: /**
1815: * converts a SpecialConstructorReference.
1816: * Special handling because the initializing
1817: * Expressions and the ReferencePrefix accessPath might not be disjunct.
1818: */
1819: public SuperConstructorReference convert(
1820: recoder.java.reference.SuperConstructorReference scr) {
1821:
1822: ExtList children = collectChildren(scr);
1823: ReferencePrefix prefix = null;
1824: int prefixPos = scr.getIndexOfChild(scr.getReferencePrefix());
1825: if (prefixPos != -1) {
1826: prefix = (ReferencePrefix) children.get(prefixPos);
1827: children.remove(prefixPos);
1828: }
1829: return new SuperConstructorReference(children, prefix);
1830: }
1831:
1832: public ThisReference convert(recoder.java.reference.ThisReference tr) {
1833:
1834: ExtList children = collectChildren(tr);
1835: ReferencePrefix prefix = null;
1836:
1837: int prefixPos = tr.getIndexOfChild(tr.getReferencePrefix());
1838: if (prefixPos != -1) {
1839: prefix = (ReferencePrefix) children.get(prefixPos);
1840: children.remove(prefixPos);
1841: }
1842: return new ThisReference((TypeReference) prefix);
1843: }
1844:
1845: public SuperReference convert(
1846: recoder.java.reference.SuperReference sr) {
1847:
1848: ExtList children = collectChildren(sr);
1849:
1850: int prefixPos = sr.getIndexOfChild(sr.getReferencePrefix());
1851: if (prefixPos != -1) {
1852: children.remove(prefixPos);
1853: }
1854:
1855: return new SuperReference(children);
1856: }
1857:
1858: /** convert a recoder VariableSpecification to a KeY
1859: * VariableSpecification
1860: * (checks dimension and hands it over and insert in hashmap)
1861: */
1862: public VariableSpecification convert(
1863: recoder.java.declaration.VariableSpecification recoderVarSpec) {
1864:
1865: VariableSpecification varSpec = (VariableSpecification) rec2key
1866: .toKeY(recoderVarSpec);
1867:
1868: if (varSpec == null) {
1869: recoder.abstraction.Type recoderType = (servConf
1870: .getSourceInfo()).getType(recoderVarSpec);
1871:
1872: final ProgramElementName name = VariableNamer
1873: .parseName(recoderVarSpec.getName());
1874: final ProgramVariable pv = new LocationVariable(name,
1875: getKeYJavaType(recoderType));
1876: varSpec = new VariableSpecification(
1877: collectChildren(recoderVarSpec), pv, recoderVarSpec
1878: .getDimensions(), pv.getKeYJavaType());
1879:
1880: insertToMap(recoderVarSpec, varSpec);
1881: }
1882: return varSpec;
1883: }
1884:
1885: /** convert a recoder MethodDeclaration to a KeY
1886: * ProgramMethod
1887: * (especially the declaration type of its parent is determined
1888: * and handed over)
1889: */
1890: public ProgramMethod convert(
1891: recoder.java.declaration.MethodDeclaration md) {
1892: ProgramMethod result = null;
1893:
1894: // methodsDeclaring contains the recoder method declarations as keys
1895: // that have been started to convert but are not yet finished.
1896: // The mapped value is the reference to the later completed
1897: // ProgramMethod.
1898: if (methodsDeclaring.containsKey(md)) {
1899: // a recursive call from a method reference
1900: return (ProgramMethod) methodsDeclaring.get(md);
1901: //reference that will later be set.
1902: }
1903: methodsDeclaring.put(md, result);
1904: if (!rec2key.mapped(md)) {
1905: final MethodDeclaration methDecl = new MethodDeclaration(
1906: collectChildren(md),
1907: md.getASTParent() instanceof recoder.java.declaration.InterfaceDeclaration);
1908: recoder.abstraction.ClassType cont = servConf
1909: .getCrossReferenceSourceInfo()
1910: .getContainingClassType(
1911: (recoder.abstraction.Member) md);
1912:
1913: result = new ProgramMethod(methDecl, getKeYJavaType(cont),
1914: getKeYJavaType(md.getReturnType()),
1915: positionInfo(md));
1916:
1917: insertToMap(md, result);
1918: }
1919: methodsDeclaring.remove(md);
1920: result = (ProgramMethod) rec2key.toKeY(md);
1921: return result;
1922: }
1923:
1924: /**
1925: * convert a recoder FieldSpecification to a KeY FieldSpecification
1926: * (checks dimension and hands it over and insert in hash map)
1927: */
1928: public FieldSpecification convert(
1929: recoder.java.declaration.FieldSpecification recoderVarSpec) {
1930:
1931: if (recoderVarSpec == null) { //%%%%%%%%%%%%%
1932: return new FieldSpecification();
1933: }
1934:
1935: FieldSpecification varSpec = (FieldSpecification) rec2key
1936: .toKeY(recoderVarSpec);
1937:
1938: if (varSpec == null) {
1939: recoder.abstraction.Type recoderType = (servConf
1940: .getSourceInfo()).getType(recoderVarSpec);
1941:
1942: ProgramVariable pv = getProgramVariableForFieldSpecification(recoderVarSpec);
1943:
1944: if (recoderVarSpec.getIdentifier() instanceof ImplicitIdentifier) {
1945: // the modelled field is an implicit one, we have to handle this one
1946: // explicit
1947: varSpec = new ImplicitFieldSpecification(pv,
1948: getKeYJavaType(recoderType));
1949: } else {
1950: varSpec = new FieldSpecification(
1951: collectChildren(recoderVarSpec), pv,
1952: recoderVarSpec.getDimensions(),
1953: getKeYJavaType(recoderType));
1954: }
1955: insertToMap(recoderVarSpec, varSpec);
1956: }
1957:
1958: return varSpec;
1959: }
1960:
1961: protected ProgramVariable getProgramVariableForFieldSpecification(
1962: recoder.java.declaration.FieldSpecification recoderVarSpec) {
1963:
1964: if (recoderVarSpec == null) { //%%%%%%%%%%%%%
1965: return null;
1966: }
1967:
1968: ProgramVariable pv = (ProgramVariable) fieldSpecificationMapping
1969: .get(recoderVarSpec);
1970:
1971: if (pv == null) {
1972: VariableSpecification varSpec = (VariableSpecification) rec2key
1973: .toKeY(recoderVarSpec);
1974: if (varSpec == null) {
1975: recoder.abstraction.Type recoderType = (servConf
1976: .getSourceInfo()).getType(recoderVarSpec);
1977: final ClassType recContainingClassType = recoderVarSpec
1978: .getContainingClassType();
1979: final ProgramElementName pen = new ProgramElementName(
1980: recoderVarSpec.getName(),
1981: recContainingClassType.getFullName());
1982:
1983: final Literal compileTimeConstant = getCompileTimeConstantInitializer(recoderVarSpec);
1984:
1985: if (compileTimeConstant == null) {
1986: pv = new LocationVariable(pen,
1987: getKeYJavaType(recoderType),
1988: getKeYJavaType(recContainingClassType),
1989: recoderVarSpec.isStatic());
1990: } else {
1991: pv = new ProgramConstant(pen,
1992: getKeYJavaType(recoderType),
1993: getKeYJavaType(recContainingClassType),
1994: recoderVarSpec.isStatic(),
1995: compileTimeConstant);
1996: }
1997: } else {
1998: pv = (ProgramVariable) varSpec.getProgramVariable();
1999: }
2000: fieldSpecificationMapping.put(recoderVarSpec, pv);
2001: }
2002:
2003: return pv;
2004: }
2005:
2006: /**
2007: * @return a literal constant representing the value of the
2008: * initializer of <code>recoderVarSpec</code>, if the variable is
2009: * a compile-time constant, and <code>null</code> otherwise
2010: */
2011: private Literal getCompileTimeConstantInitializer(
2012: recoder.java.declaration.FieldSpecification recoderVarSpec) {
2013:
2014: // Necessary condition: the field is static and final
2015: if (!recoderVarSpec.isFinal() || !recoderVarSpec.isStatic())
2016: return null;
2017:
2018: recoder.java.Expression init = recoderVarSpec.getInitializer();
2019:
2020: if (init != null) {
2021: recoder.service.ConstantEvaluator ce = new recoder.service.DefaultConstantEvaluator(
2022: getServiceConfiguration());
2023: recoder.service.ConstantEvaluator.EvaluationResult er = new recoder.service.ConstantEvaluator.EvaluationResult();
2024:
2025: if (ce.isCompileTimeConstant(init, er))
2026: return getLiteralFor(er);
2027: }
2028:
2029: return null;
2030: }
2031:
2032: /**
2033: * @return a literal constant representing the value of
2034: * <code>p_er</code>
2035: */
2036: private Literal getLiteralFor(
2037: recoder.service.ConstantEvaluator.EvaluationResult p_er) {
2038: switch (p_er.getTypeCode()) {
2039: case recoder.service.ConstantEvaluator.BOOLEAN_TYPE:
2040: return BooleanLiteral.getBooleanLiteral(p_er.getBoolean());
2041: case recoder.service.ConstantEvaluator.CHAR_TYPE:
2042: return new CharLiteral(p_er.getChar());
2043: case recoder.service.ConstantEvaluator.DOUBLE_TYPE:
2044: return new DoubleLiteral(p_er.getDouble());
2045: case recoder.service.ConstantEvaluator.FLOAT_TYPE:
2046: return new FloatLiteral(p_er.getFloat());
2047: case recoder.service.ConstantEvaluator.BYTE_TYPE:
2048: return new IntLiteral(p_er.getByte());
2049: case recoder.service.ConstantEvaluator.SHORT_TYPE:
2050: return new IntLiteral(p_er.getShort());
2051: case recoder.service.ConstantEvaluator.INT_TYPE:
2052: return new IntLiteral(p_er.getInt());
2053: case recoder.service.ConstantEvaluator.LONG_TYPE:
2054: return new LongLiteral(p_er.getLong());
2055: case recoder.service.ConstantEvaluator.STRING_TYPE:
2056: if (p_er.getString() == null)
2057: return NullLiteral.NULL;
2058: return new StringLiteral(p_er.getString());
2059: default:
2060: Debug.out("Don't know how to handle type "
2061: + p_er.getTypeCode() + " of " + p_er);
2062: }
2063: return null;
2064: }
2065:
2066: /**
2067: * convert a recoder TypeReference to a KeY TypeReference
2068: * (checks dimension and hands it over)
2069: */
2070: public TypeReference convert(recoder.java.reference.TypeReference tr) {
2071:
2072: recoder.abstraction.Type rType = servConf.getSourceInfo()
2073: .getType(tr);
2074: if (rType == null)
2075: return null; // because of 'void'
2076:
2077: KeYJavaType kjt = getKeYJavaType(rType);
2078: ExtList children = collectChildren(tr);
2079: TypeReference result = new TypeRef(children, kjt, tr
2080: .getDimensions());
2081: return result;
2082: }
2083:
2084: /**
2085: * if an UncollatedReferenceQualifier appears throw a
2086: * ConvertExceception because these qualifiers have to be resolved
2087: * by running the CrossReferencer
2088: */
2089: public ProgramElement convert(
2090: recoder.java.reference.UncollatedReferenceQualifier urq) {
2091: recoder.java.ProgramElement pe = servConf
2092: .getCrossReferenceSourceInfo().resolveURQ(urq);
2093: if (pe != null
2094: && !(pe instanceof recoder.java.reference.UncollatedReferenceQualifier)) {
2095: return (ProgramElement) callConvert(pe);
2096: }
2097: throw new PosConvertException("recoder2key: Qualifier "
2098: + urq.getName() + " not resolvable.", urq
2099: .getFirstElement().getStartPosition().getLine(), urq
2100: .getFirstElement().getStartPosition().getColumn() - 1);
2101: }
2102:
2103: protected recoder.java.declaration.VariableSpecification getRecoderVarSpec(
2104: recoder.java.reference.VariableReference vr) {
2105: return servConf.getSourceInfo().getVariableSpecification(
2106: servConf.getSourceInfo().getVariable(vr));
2107: }
2108:
2109: /**
2110: * converts a recoder variable reference. A ProgramVariable is created
2111: * replacing the variable reference.
2112: * @param vr the recoder variable reference.
2113: */
2114: public ProgramVariable convert(
2115: recoder.java.reference.VariableReference vr) {
2116:
2117: final recoder.java.declaration.VariableSpecification recoderVarspec = getRecoderVarSpec(vr);
2118:
2119: if (!rec2key.mapped(recoderVarspec)) {
2120: insertToMap(recoderVarspec, convert(recoderVarspec));
2121: }
2122:
2123: return (ProgramVariable) ((VariableSpecification) rec2key
2124: .toKeY(recoderVarspec)).getProgramVariable();
2125: }
2126:
2127: public BinaryAnd convert(
2128: recoder.java.expression.operator.BinaryAnd b) {
2129: return new BinaryAnd(collectChildren(b));
2130: }
2131:
2132: public BinaryOr convert(recoder.java.expression.operator.BinaryOr b) {
2133: return new BinaryOr(collectChildren(b));
2134: }
2135:
2136: public BinaryXOr convert(
2137: recoder.java.expression.operator.BinaryXOr b) {
2138: return new BinaryXOr(collectChildren(b));
2139: }
2140:
2141: public BinaryNot convert(
2142: recoder.java.expression.operator.BinaryNot b) {
2143: return new BinaryNot(collectChildren(b));
2144: }
2145:
2146: public BinaryAndAssignment convert(
2147: recoder.java.expression.operator.BinaryAndAssignment b) {
2148: return new BinaryAndAssignment(collectChildren(b));
2149: }
2150:
2151: public BinaryOrAssignment convert(
2152: recoder.java.expression.operator.BinaryOrAssignment b) {
2153: return new BinaryOrAssignment(collectChildren(b));
2154: }
2155:
2156: public BinaryXOrAssignment convert(
2157: recoder.java.expression.operator.BinaryXOrAssignment b) {
2158: return new BinaryXOrAssignment(collectChildren(b));
2159: }
2160:
2161: public ShiftLeft convert(
2162: recoder.java.expression.operator.ShiftLeft b) {
2163: return new ShiftLeft(collectChildren(b));
2164: }
2165:
2166: public ShiftRight convert(
2167: recoder.java.expression.operator.ShiftRight b) {
2168: return new ShiftRight(collectChildren(b));
2169: }
2170:
2171: public UnsignedShiftRight convert(
2172: recoder.java.expression.operator.UnsignedShiftRight b) {
2173: return new UnsignedShiftRight(collectChildren(b));
2174: }
2175:
2176: public ShiftLeftAssignment convert(
2177: recoder.java.expression.operator.ShiftLeftAssignment b) {
2178: return new ShiftLeftAssignment(collectChildren(b));
2179: }
2180:
2181: public ShiftRightAssignment convert(
2182: recoder.java.expression.operator.ShiftRightAssignment b) {
2183: return new ShiftRightAssignment(collectChildren(b));
2184: }
2185:
2186: public UnsignedShiftRightAssignment convert(
2187: recoder.java.expression.operator.UnsignedShiftRightAssignment b) {
2188: return new UnsignedShiftRightAssignment(collectChildren(b));
2189: }
2190:
2191: public Negative convert(recoder.java.expression.operator.Negative b) {
2192: return new Negative(collectChildren(b));
2193: }
2194:
2195: public Positive convert(recoder.java.expression.operator.Positive b) {
2196: return new Positive(collectChildren(b));
2197: }
2198:
2199: public Modulo convert(recoder.java.expression.operator.Modulo b) {
2200: return new Modulo(collectChildren(b));
2201: }
2202:
2203: public ModuloAssignment convert(
2204: recoder.java.expression.operator.ModuloAssignment b) {
2205: return new ModuloAssignment(collectChildren(b));
2206: }
2207:
2208: public Conditional convert(
2209: recoder.java.expression.operator.Conditional b) {
2210: return new Conditional(collectChildren(b));
2211: }
2212:
2213: /**
2214: * converts a recoder array length reference to a usual KeY field
2215: * reference
2216: */
2217: public FieldReference convert(
2218: recoder.java.reference.ArrayLengthReference alr) {
2219: recoder.abstraction.Type recoderType = servConf
2220: .getCrossReferenceSourceInfo().getType(
2221: alr.getReferencePrefix());
2222: ArrayDeclaration ad = (ArrayDeclaration) getKeYJavaType(
2223: recoderType).getJavaType();
2224:
2225: final ProgramVariable length = find("length", filterField(ad
2226: .length()));
2227: // the invocation of callConvert should work well as each array
2228: // length reference must have a reference prefix (at least this
2229: // is what i think)
2230: return new FieldReference(length,
2231: (ReferencePrefix) callConvert(alr.getReferencePrefix()));
2232: }
2233:
2234: /**
2235: * converts a recoder package reference to the KeY package reference
2236: * @param pr the recoder package reference reference.
2237: */
2238: public PackageReference convert(
2239: recoder.java.reference.PackageReference pr) {
2240: return new PackageReference(collectChildren(pr));
2241: }
2242:
2243: /**
2244: * converts a recoder field reference. A ProgramVariable is created
2245: * replacing the field reference.
2246: * @param fr the recoder field reference.
2247: */
2248: public Expression convert(recoder.java.reference.FieldReference fr) {
2249: ProgramVariable pv;
2250:
2251: recoder.java.declaration.FieldSpecification recoderVarSpec = (recoder.java.declaration.FieldSpecification) getRecoderVarSpec(fr);
2252:
2253: ReferencePrefix prefix = null;
2254:
2255: if (fr.getReferencePrefix() != null) {
2256: prefix = (ReferencePrefix) callConvert(fr
2257: .getReferencePrefix());
2258: }
2259:
2260: if (recoderVarSpec == null) {
2261: // null means only bytecode available for this
2262: // field %%%
2263: recoder.abstraction.Field recField = servConf
2264: .getSourceInfo().getField(fr);
2265: recoder.abstraction.Type recoderType = servConf
2266: .getByteCodeInfo().getType(recField);
2267: recoder.java.declaration.FieldSpecification fs = new recoder.java.declaration.FieldSpecification(
2268: fr.getIdentifier());
2269: pv = new LocationVariable(new ProgramElementName(fs
2270: .getName(), recField.getContainingClassType()
2271: .getFullName()), getKeYJavaType(recoderType),
2272: getKeYJavaType(recField.getContainingClassType()),
2273: recField.isStatic());
2274: insertToMap(fs, new FieldSpecification(pv));
2275: return new FieldReference(pv, prefix);
2276: }
2277:
2278: pv = getProgramVariableForFieldSpecification(recoderVarSpec);
2279:
2280: if (!pv.isMember()) {
2281: // in case of a cut, induction rule or s.th. else recoder will resolve
2282: // all variables of the created context as field references but
2283: // in fact they are references to local variables, so we have
2284: // to fix it here
2285: // same applies for variables declared in program variables
2286: // section
2287: return pv;
2288: }
2289:
2290: return new FieldReference(pv, prefix);
2291: }
2292:
2293: /**
2294: * converts a recoder method reference. A
2295: * de.uka.ilkd.key.logic.op.ProgramMethod is created
2296: * replacing the method reference.
2297: * @param mr the recoder method reference.
2298: * @return the Method the KeY Dependance
2299: */
2300: public MethodReference convert(
2301: recoder.java.reference.MethodReference mr) {
2302: recoder.service.SourceInfo sourceInfo = servConf
2303: .getSourceInfo();
2304: recoder.abstraction.Method method = sourceInfo.getMethod(mr);
2305:
2306: final ProgramMethod pm;
2307: if (!rec2key.mapped(method)) {
2308: if (method instanceof recoder.java.declaration.MethodDeclaration) {
2309: // method reference before method decl, also recursive calls.
2310: // do not use:
2311: final String oldCurrent = currentClass;
2312: final String className = ((recoder.java.declaration.MethodDeclaration) method)
2313: .getMemberParent().getFullName();
2314: recoder.io.DataLocation loc = servConf
2315: .getSourceFileRepository().findSourceFile(
2316: className);
2317: if (loc instanceof recoder.io.DataFileLocation) {
2318: currentClass = ((recoder.io.DataFileLocation) loc)
2319: .getFile().getAbsolutePath();
2320: } else {
2321: currentClass = (loc == null ? null : "" + loc);
2322: }
2323: pm = convert((recoder.java.declaration.MethodDeclaration) method);
2324: // because of cycles when reading recursive programs
2325: currentClass = oldCurrent;
2326: } else {
2327: // bytecode currently we do nothing
2328: pm = null;
2329: }
2330: } else {
2331: pm = (ProgramMethod) rec2key.toKeY(method);
2332: }
2333:
2334: ExtList children = collectChildren(mr);
2335: // convert reference prefix separately
2336: ReferencePrefix prefix = null;
2337: int prefixPos = mr.getIndexOfChild(mr.getReferencePrefix());
2338: if (prefixPos != -1) {
2339: prefix = (ReferencePrefix) children.get(prefixPos);
2340: children.remove(prefixPos);
2341: }
2342:
2343: return new MethodReference(children,
2344: pm == null ? new ProgramElementName(mr.getName()) : pm
2345: .getProgramElementName(), prefix,
2346: positionInfo(mr));
2347: }
2348:
2349: //--------------Special treatment because of ambiguities ----------
2350:
2351: public LabeledStatement convert(
2352: recoder.java.statement.LabeledStatement l) {
2353:
2354: ExtList children = collectChildren(l);
2355: Label lab = null;
2356: int labPos = l.getIndexOfChild(l.getIdentifier());
2357: if (labPos != -1) {
2358: lab = (Label) children.get(labPos);
2359: children.remove(labPos);
2360: }
2361: return new LabeledStatement(children, lab, positionInfo(l));
2362: }
2363:
2364: /**
2365: * converts a For.
2366: * @param f the For of recoder
2367: * @return the For of KeY
2368: */
2369: public For convert(recoder.java.statement.For f) {
2370: return new For(convertLoopInitializers(f), convertGuard(f),
2371: convertUpdates(f), convertBody(f), collectComments(f),
2372: positionInfo(f));
2373: }
2374:
2375: /**
2376: * converts a While.
2377: * @param w the While of recoder
2378: * @return the While of KeY
2379: */
2380: public While convert(recoder.java.statement.While w) {
2381: return new While(convertGuard(w).getExpression(),
2382: convertBody(w), positionInfo(w), collectComments(w));
2383: }
2384:
2385: /**
2386: * converts a Do.
2387: * @param d the Do of recoder
2388: * @return the Do of KeY
2389: */
2390: public Do convert(recoder.java.statement.Do d) {
2391: return new Do(convertGuard(d).getExpression(), convertBody(d),
2392: collectComments(d), positionInfo(d));
2393: }
2394:
2395: /**
2396: * helper for convert(x) with x a LoopStatement. Converts the body of x.
2397: */
2398: protected Statement convertBody(
2399: recoder.java.statement.LoopStatement ls) {
2400: Object body = null;
2401: if (ls.getBody() != null) {
2402: body = callConvert(ls.getBody());
2403: }
2404: return (Statement) body;
2405: }
2406:
2407: /**
2408: * helper for convert(x) with x a LoopStatement. Converts the guard of x.
2409: */
2410: protected Guard convertGuard(recoder.java.statement.LoopStatement ls) {
2411: Object guard = null;
2412: if (ls.getGuard() != null) {
2413: guard = callConvert(ls.getGuard());
2414: }
2415: return new Guard((Expression) guard);
2416: }
2417:
2418: /**
2419: * helper for convert(x) with x a LoopStatement. Converts the updates of x.
2420: */
2421: protected ForUpdates convertUpdates(
2422: recoder.java.statement.LoopStatement ls) {
2423: final ExtList updates = new ExtList();
2424: final ExpressionMutableList recLoopUpdates = ls.getUpdates();
2425: inLoopInit = true;
2426: if (recLoopUpdates != null) {
2427: for (int i = 0, sz = recLoopUpdates.size(); i < sz; i++) {
2428: updates
2429: .add(callConvert(recLoopUpdates
2430: .getExpression(i)));
2431: }
2432: inLoopInit = false;
2433: return new ForUpdates(updates, positionInfo(ls));
2434: }
2435: return null;
2436: }
2437:
2438: /**
2439: * helper for convert(x) with x a LoopStatement. Converts the loop
2440: * initializers of x.
2441: */
2442: protected LoopInit convertLoopInitializers(
2443: recoder.java.statement.LoopStatement ls) {
2444:
2445: final LoopInit loopInit;
2446:
2447: final LoopInitializerMutableList initializers = ls
2448: .getInitializers();
2449: if (initializers != null) {
2450: final LoopInitializer[] result = new LoopInitializer[initializers
2451: .size()];
2452: for (int i = 0, sz = initializers.size(); i < sz; i++) {
2453: inLoopInit = true;
2454: result[i] = (LoopInitializer) callConvert(initializers
2455: .getLoopInitializer(i));
2456: inLoopInit = false;
2457: }
2458: loopInit = new LoopInit(result);
2459: } else {
2460: loopInit = null;
2461: }
2462: return loopInit;
2463: }
2464:
2465: /**
2466: * converts an ArrayReference. Special handling because the initializing
2467: * Expressions and the ReferencePrefix accessPath might not be disjunct.
2468: */
2469: public ArrayReference convert(
2470: recoder.java.reference.ArrayReference ar) {
2471: ExtList children = collectChildren(ar);
2472: ReferencePrefix prefix = null;
2473:
2474: int prefixPos = ar.getIndexOfChild(ar.getReferencePrefix());
2475: if (prefixPos != -1) {
2476: prefix = (ReferencePrefix) children.get(prefixPos);
2477: children.remove(prefixPos);
2478: }
2479: return new ArrayReference(children, prefix);
2480: }
2481:
2482: /**
2483: * convert Breaks
2484: */
2485: public Break convert(recoder.java.statement.Break b) {
2486: return new Break(collectChildren(b));
2487: }
2488:
2489: /** convert Assert */
2490: public Assert convert(recoder.java.statement.Assert a) {
2491: final Expression message;
2492: if (a.getMessage() != null) {
2493: message = (Expression) callConvert(a.getMessage());
2494: } else {
2495: message = null;
2496: }
2497: return new Assert((Expression) callConvert(a.getCondition()),
2498: message, positionInfo(a));
2499: }
2500:
2501: /**
2502: * converts a Case.
2503: * Special handling because the initializing
2504: * Expression and Statements might not be disjunct.
2505: */
2506: public Case convert(recoder.java.statement.Case c) {
2507: ExtList children = collectChildren(c);
2508: Expression expr = null;
2509: int exprPos = c.getIndexOfChild(c.getExpression());
2510: if (exprPos != -1) {
2511: expr = (Expression) children.get(exprPos);
2512: children.remove(exprPos);
2513: }
2514: return new Case(children, expr, positionInfo(c));
2515: }
2516:
2517: /**
2518: * converts a New.
2519: * Special handling because the ReferencePrefix and the TypeReference
2520: * might not be disjunct.
2521: */
2522: public New convert(recoder.java.expression.operator.New n) {
2523:
2524: final recoder.list.ExpressionMutableList args = n
2525: .getArguments();
2526: final recoder.java.reference.ReferencePrefix rp = n
2527: .getReferencePrefix();
2528: final recoder.java.reference.TypeReference tr = n
2529: .getTypeReference();
2530:
2531: Expression[] arguments = new Expression[args != null ? args
2532: .size() : 0];
2533: for (int i = 0; i < arguments.length; i++) {
2534: arguments[i] = (Expression) callConvert(args
2535: .getExpression(i));
2536: }
2537: if (rp == null) {
2538: return new New(arguments, (TypeReference) callConvert(tr),
2539: (ReferencePrefix) null);
2540: } else {
2541: return new New(arguments, (TypeReference) callConvert(tr),
2542: (ReferencePrefix) callConvert(rp));
2543: }
2544: }
2545:
2546: //-----------------------------------------------------------
2547:
2548: public Import convert(recoder.java.Import im) {
2549: return new Import(collectChildren(im), im.isMultiImport());
2550: }
2551:
2552: private recoder.java.declaration.ClassDeclaration interactClassDecl() {
2553: recoder.java.declaration.ClassDeclaration classContext = new recoder.java.declaration.ClassDeclaration(
2554: null, new ImplicitIdentifier(
2555: "<virtual_class_for_parsing" + interactCounter
2556: + ">"), null, null, null);
2557: interactCounter++;
2558: classContext.setProgramModelInfo(servConf
2559: .getCrossReferenceSourceInfo());
2560: return classContext;
2561: }
2562:
2563: /** creates an empty RECODER compilation unit
2564: * @return the recoder.java.CompilationUnit
2565: */
2566: public Context createEmptyContext() {
2567: recoder.java.declaration.ClassDeclaration classContext = interactClassDecl();
2568: return new Context(servConf, classContext);
2569: }
2570:
2571: private VariableSpecification lookupVarSpec(ProgramVariable pv) {
2572: Iterator it = rec2key.elemsKeY().iterator();
2573: while (it.hasNext()) {
2574: Object o = it.next();
2575: if ((o instanceof VariableSpecification)
2576: && ((VariableSpecification) o).getProgramVariable() == pv) {
2577:
2578: return (VariableSpecification) o;
2579: }
2580: }
2581: return null;
2582: }
2583:
2584: private recoder.java.reference.TypeReference name2typeReference(
2585: String typeName) {
2586:
2587: recoder.java.reference.PackageReference pr = null;
2588: String baseType = TypeNameTranslator.getBaseType(typeName);
2589: int idx = baseType.indexOf('.');
2590: int lastIndex = 0;
2591: while (idx != -1) {
2592: pr = new recoder.java.reference.PackageReference(pr,
2593: new recoder.java.Identifier(baseType.substring(
2594: lastIndex, idx)));
2595: lastIndex = idx + 1;
2596: idx = baseType.indexOf('.', lastIndex);
2597: }
2598:
2599: recoder.java.Identifier typeId;
2600: if (baseType.charAt(0) == '<') {
2601: typeId = new ImplicitIdentifier(baseType
2602: .substring(lastIndex));
2603: } else {
2604: typeId = new recoder.java.Identifier(baseType
2605: .substring(lastIndex));
2606: }
2607: recoder.java.reference.TypeReference result = new recoder.java.reference.TypeReference(
2608: pr, typeId);
2609: result
2610: .setDimensions(TypeNameTranslator
2611: .getDimensions(typeName));
2612: return result;
2613: }
2614:
2615: public void addProgramVariablesToClassContext(
2616: recoder.java.declaration.ClassDeclaration classContext,
2617: ListOfProgramVariable vars,
2618: recoder.service.CrossReferenceSourceInfo csi) {
2619:
2620: HashMap names2var = new HashMap();
2621: IteratorOfProgramVariable it = vars.iterator();
2622: java.util.HashSet names = new java.util.HashSet();
2623: recoder.list.MemberDeclarationMutableList list = classContext
2624: .getMembers();
2625: if (list == null) {
2626: list = new recoder.list.MemberDeclarationArrayList();
2627: classContext.setMembers(list);
2628: }
2629: l: while (it.hasNext()) {
2630: VariableSpecification keyVarSpec;
2631: ProgramVariable var = it.next();
2632: if (names.contains(var.name().toString())) {
2633: continue l;
2634: }
2635: names.add(var.name().toString());
2636: keyVarSpec = lookupVarSpec(var);
2637: if (keyVarSpec == null) {
2638: keyVarSpec = new FieldSpecification(var);
2639: }
2640:
2641: if (var.getKeYJavaType() == null) {
2642: throw new IllegalArgumentException("Variable " + var
2643: + " has no type");
2644: }
2645:
2646: String typeName = "";
2647: Type javaType = var.getKeYJavaType().getJavaType();
2648: typeName = javaType.getFullName();
2649:
2650: recoder.java.declaration.FieldDeclaration recVar = new recoder.java.declaration.FieldDeclaration(
2651: null, name2typeReference(typeName),
2652: new ExtendedIdentifier(keyVarSpec.getName()), null);
2653:
2654: list.add(recVar);
2655: classContext.makeAllParentRolesValid();
2656: recoder.java.declaration.VariableSpecification rvarspec = recVar
2657: .getVariables().getVariableSpecification(0);
2658: names2var.put(var.name().toString(), rvarspec);
2659:
2660: rvarspec.setProgramModelInfo(csi);
2661: insertToMap(recVar.getVariables().getVariableSpecification(
2662: 0), keyVarSpec);
2663: }
2664:
2665: ((KeYCrossReferenceSourceInfo) csi).setNames2Vars(names2var);
2666: servConf.getChangeHistory().updateModel();
2667: }
2668:
2669: public Context createContext(ListOfProgramVariable pvs) {
2670: return createContext(pvs, servConf
2671: .getCrossReferenceSourceInfo());
2672: }
2673:
2674: public Context createContext(ListOfProgramVariable vars,
2675: recoder.service.CrossReferenceSourceInfo csi) {
2676: recoder.java.declaration.ClassDeclaration classContext = interactClassDecl();
2677: addProgramVariablesToClassContext(classContext, vars, csi);
2678: return new Context(servConf, classContext);
2679: }
2680:
2681: // invoke model transformers
2682: protected void transformModel(
2683: recoder.list.CompilationUnitMutableList cUnits) {
2684: RecoderModelTransformer[] transformer = new RecoderModelTransformer[] {
2685: new ImplicitFieldAdder(servConf, cUnits),
2686: new InstanceAllocationMethodBuilder(servConf, cUnits),
2687: new ConstructorNormalformBuilder(servConf, cUnits),
2688: new ClassPreparationMethodBuilder(servConf, cUnits),
2689: new ClassInitializeMethodBuilder(servConf, cUnits),
2690: new PrepareObjectBuilder(servConf, cUnits),
2691: new CreateBuilder(servConf, cUnits),
2692: new CreateObjectBuilder(servConf, cUnits),
2693: new JVMIsTransientMethodBuilder(servConf, cUnits) };
2694:
2695: final ChangeHistory cHistory = servConf.getChangeHistory();
2696: for (int i = 0; i < transformer.length; i++) {
2697: if (logger.isDebugEnabled()) {
2698: logger.debug("current transformer : "
2699: + transformer[i].toString());
2700: }
2701: transformer[i].execute();
2702: }
2703: if (cHistory.needsUpdate()) {
2704: cHistory.updateModel();
2705: }
2706: }
2707:
2708: /**
2709: * retrieves a field with the given name out of the list
2710: * @param name a String with the name of the field to be looked for
2711: * @param fields the ListOfField where we have to look for the field
2712: * @return the program variable of the given name or null if not
2713: * found
2714: */
2715: protected ProgramVariable find(String name, ListOfField fields) {
2716: IteratorOfField it = fields.iterator();
2717: while (it.hasNext()) {
2718: Field field = it.next();
2719: if (name.equals(field.getName())) {
2720: return (ProgramVariable) ((FieldSpecification) field)
2721: .getProgramVariable();
2722: }
2723: }
2724: return null;
2725: }
2726:
2727: /**
2728: * extracts all field specifications out of the given
2729: * list. Therefore it descends into field declarations.
2730: * @param list the ExtList with the members of a type declaration
2731: * @return a ListOfField the includes all field specifications found
2732: * int the field declaration of the given list
2733: */
2734: private ListOfField filterField(ExtList list) {
2735: ListOfField result = SLListOfField.EMPTY_LIST;
2736: Iterator it = list.iterator();
2737: while (it.hasNext()) {
2738: Object pe = it.next();
2739: if (pe instanceof FieldDeclaration) {
2740: result = result
2741: .prepend(filterField((FieldDeclaration) pe));
2742: }
2743: }
2744: return result;
2745: }
2746:
2747: /**
2748: * extracts all fields out of fielddeclaration
2749: * @param field the FieldDeclaration of which the field
2750: * specifications have to be extracted
2751: * @return a ListOfField the includes all field specifications found
2752: * int the field declaration of the given list
2753: */
2754: protected ListOfField filterField(FieldDeclaration field) {
2755: ListOfField result = SLListOfField.EMPTY_LIST;
2756: ArrayOfFieldSpecification spec = field.getFieldSpecifications();
2757: for (int i = spec.size() - 1; i >= 0; i--) {
2758: result = result.prepend(spec.getFieldSpecification(i));
2759: }
2760: return result;
2761: }
2762:
2763: // array type creation
2764:
2765: /**
2766: * creates an implicit field of the given name and type
2767: * @param name a String with the name of the implicit field
2768: * @param typeRef a TypeReference refering to the type as which the
2769: * new field has to be declared
2770: * @param isStatic a boolean that forces a field to become static or
2771: * non static
2772: * @return the new created FieldDeclaration <br></br>
2773: * </code>private (static) typeRef name</code>
2774: */
2775: private FieldDeclaration createImplicitArrayField(String name,
2776: TypeReference typeRef, boolean isStatic, KeYJavaType prefix) {
2777:
2778: ImplicitFieldSpecification varSpec = new ImplicitFieldSpecification(
2779: new LocationVariable(new ProgramElementName(name,
2780: prefix.getSort().name().toString()), typeRef
2781: .getKeYJavaType(), prefix, isStatic), typeRef
2782: .getKeYJavaType());
2783: // no recoder dependance
2784: // insertToMap(recoderVarSpec, varSpec);
2785: Modifier[] modifiers = new Modifier[isStatic ? 2 : 1];
2786: modifiers[0] = new Private();
2787: if (isStatic) {
2788: modifiers[1] = new Static();
2789: }
2790: return new FieldDeclaration(modifiers, typeRef,
2791: new FieldSpecification[] { varSpec }, false);
2792: }
2793:
2794: /**
2795: * Adds several implicit fields and methods to given list of members.
2796: * @param members an ExtList with the members of parent
2797: * @param parent the KeYJavaType of the array to be enriched by its
2798: * implicit members
2799: * @param baseType the KeYJavaType of the parent's element type
2800: */
2801: private void addImplicitArrayMembers(ExtList members,
2802: KeYJavaType parent, KeYJavaType baseType,
2803: ProgramVariable len) {
2804:
2805: final Type base = baseType.getJavaType();
2806: final int dimension = base instanceof ArrayType ? ((ArrayType) base)
2807: .getDimension() + 1
2808: : 1;
2809: TypeRef parentReference = new TypeRef(new ProgramElementName(""
2810: + parent.getSort().name()), dimension, null, parent);
2811: KeYJavaType integerType = getKeYJavaType(servConf.getNameInfo()
2812: .getIntType());
2813:
2814: members.add(createImplicitArrayField(
2815: ImplicitFieldAdder.IMPLICIT_NEXT_TO_CREATE,
2816: new TypeRef(integerType), true, parent));
2817:
2818: final recoder.service.NameInfo nameInfo = servConf
2819: .getNameInfo();
2820:
2821: TypeReference booleanArrayTypeRef;
2822: if (base == PrimitiveType.JAVA_BOOLEAN && dimension == 1) {
2823: booleanArrayTypeRef = parentReference;
2824: } else {
2825: booleanArrayTypeRef = new TypeRef(getKeYJavaType(nameInfo
2826: .getArrayType(nameInfo.getBooleanType())), 1);
2827: }
2828: members.add(createImplicitArrayField(
2829: ImplicitFieldAdder.IMPLICT_ARRAY_TRA_INITIALIZED,
2830: booleanArrayTypeRef, false, parent));
2831:
2832: // add methods
2833: // the only situation where base can be null is in case of a
2834: // reference type
2835: Expression defaultValue = (base != null ? base
2836: .getDefaultValue() : NullLiteral.NULL);
2837:
2838: ListOfField fields = filterField(members);
2839:
2840: ProgramVariable length = len;//find("length", fields);
2841:
2842: if (arrayMethodBuilder == null) {
2843: initArrayMethodBuilder();
2844: }
2845: final ProgramMethod prepare = arrayMethodBuilder
2846: .getPrepareArrayMethod(parentReference, length,
2847: defaultValue, fields);
2848:
2849: members.add(arrayMethodBuilder
2850: .getArrayInstanceAllocatorMethod(parentReference));
2851: members.add(prepare);
2852: members.add(arrayMethodBuilder.getCreateArrayHelperMethod(
2853: parentReference, length, fields));
2854: members.add(arrayMethodBuilder.getCreateArrayMethod(
2855: parentReference, prepare, fields));
2856: members.add(transientArrayMethodBuilder
2857: .getCreateTransientArrayHelperMethod(parentReference,
2858: length, fields));
2859: members.add(transientArrayMethodBuilder
2860: .getCreateTransientArrayMethod(parentReference, length,
2861: prepare, fields));
2862: }
2863:
2864: /**
2865: * creates the field declaration for the public final integer field
2866: * <code>length</code>
2867: */
2868: private FieldDeclaration createSuperArrayType() {
2869: KeYJavaType integerType = getKeYJavaType(servConf.getNameInfo()
2870: .getIntType());
2871:
2872: final KeYJavaType super ArrayType = new KeYJavaType();
2873: rec2key.setSuperArrayType(super ArrayType);
2874: FieldSpecification specLength = new FieldSpecification(
2875: new LocationVariable(new ProgramElementName("length"),
2876: integerType, super ArrayType, false));
2877: FieldDeclaration f = new FieldDeclaration(new Modifier[] {
2878: new Public(), new Final() }, new TypeRef(integerType),
2879: new FieldSpecification[] { specLength }, false);
2880: super ArrayType.setJavaType(new SuperArrayDeclaration(f));
2881: return f;
2882: }
2883:
2884: public ArrayDeclaration createArrayType(KeYJavaType baseType,
2885: KeYJavaType arrayType) {
2886: ExtList members = new ExtList();
2887: if (rec2key().getSuperArrayType() == null) {
2888: createSuperArrayType(); // we want to have exactly one
2889: // length attribute for this R2K
2890: // instance (resolving
2891: // a.length=a.length might get
2892: // impossible otherwise),
2893: // therefore we introduce a 'super
2894: // array class' which contains the
2895: // length attribute
2896: }
2897: final FieldDeclaration length = ((SuperArrayDeclaration) rec2key()
2898: .getSuperArrayType().getJavaType()).length();
2899: final TypeReference baseTypeRef;
2900:
2901: if (baseType.getJavaType() != null) {
2902: baseTypeRef = new TypeRef(baseType);
2903: } else {
2904: baseTypeRef = new TypeRef(new ProgramElementName(baseType
2905: .getSort().name().toString()), 0, null, baseType);
2906: }
2907: members.add(baseTypeRef);
2908: addImplicitArrayMembers(members, arrayType, baseType,
2909: (ProgramVariable) length.getFieldSpecifications()
2910: .getFieldSpecification(0).getProgramVariable());
2911:
2912: return new ArrayDeclaration(members, baseTypeRef, rec2key()
2913: .getSuperArrayType());
2914: }
2915:
2916: }
|