001: // This file is part of KeY - Integrated Deductive Software Design
002: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
003: // Universitaet Koblenz-Landau, Germany
004: // Chalmers University of Technology, Sweden
005: //
006: // The KeY system is protected by the GNU General Public License.
007: // See LICENSE.TXT for details.
008: //
009: //
010:
011: package de.uka.ilkd.key.java;
012:
013: import java.io.IOException;
014: import java.io.StringReader;
015: import java.util.HashMap;
016:
017: import de.uka.ilkd.key.java.abstraction.KeYJavaType;
018: import de.uka.ilkd.key.java.abstraction.PrimitiveType;
019: import de.uka.ilkd.key.java.declaration.LocalVariableDeclaration;
020: import de.uka.ilkd.key.java.declaration.Modifier;
021: import de.uka.ilkd.key.java.declaration.VariableSpecification;
022: import de.uka.ilkd.key.java.recoderext.*;
023: import de.uka.ilkd.key.java.reference.*;
024: import de.uka.ilkd.key.java.reference.ExecutionContext;
025: import de.uka.ilkd.key.java.statement.*;
026: import de.uka.ilkd.key.java.statement.MethodBodyStatement;
027: import de.uka.ilkd.key.logic.Namespace;
028: import de.uka.ilkd.key.logic.NamespaceSet;
029: import de.uka.ilkd.key.logic.ProgramElementName;
030: import de.uka.ilkd.key.logic.op.*;
031: import de.uka.ilkd.key.logic.sort.ProgramSVSort;
032: import de.uka.ilkd.key.rule.metaconstruct.*;
033: import de.uka.ilkd.key.util.Debug;
034: import de.uka.ilkd.key.util.ExtList;
035: import de.uka.ilkd.key.util.KeYRecoderExcHandler;
036:
037: public class SchemaRecoder2KeY extends Recoder2KeY implements
038: SchemaJavaReader {
039:
040: /** the namespace containing the program schema variables allowed here*/
041: protected Namespace svns;
042:
043: public static KeYJavaType typeSVType = new KeYJavaType(
044: PrimitiveType.PROGRAM_SV, ProgramSVSort.TYPE);
045:
046: /** caches access to methods for reflection */
047: private final static HashMap schemaCt2meth = new HashMap(400);
048:
049: /** caches constructor access for reflection */
050: private final static HashMap recClass2schemakeyClassCons = new HashMap(
051: 400);
052:
053: // could this be the servConf of the super class?
054: private static SchemaCrossReferenceServiceConfiguration schemaServConf = new SchemaCrossReferenceServiceConfiguration(
055: new KeYRecoderExcHandler());
056:
057: public SchemaRecoder2KeY(Services services, NamespaceSet nss) {
058: super (services, nss);
059: }
060:
061: /**
062: * returns the hashmap of a concrete RecodeR class to the constructor of its
063: * corresponding KeY class. Speeds up reflection.
064: * Attention must be overwritten by subclasses!
065: */
066: protected HashMap getKeYClassConstructorCache() {
067: return recClass2schemakeyClassCons;
068: }
069:
070: protected HashMap getMethodCache() {
071: return schemaCt2meth;
072: }
073:
074: public void setSVNamespace(Namespace svns) {
075: this .svns = svns;
076: }
077:
078: /** creates an empty RECODER compilation unit
079: * @return the recoder.java.CompilationUnit
080: */
081: public Context createEmptyContext() {
082: return new Context(schemaServConf,
083: new recoder.java.CompilationUnit(), schemaServConf
084: .getProgramFactory().createClassDeclaration(
085: null,
086: new ImplicitIdentifier(
087: "<KeYSpecialParsing>"), null,
088: null, null));
089: }
090:
091: public ProgramMetaConstruct convert(
092: de.uka.ilkd.key.java.recoderext.RKeYMetaConstruct mc) {
093:
094: ExtList list = new ExtList();
095: String mcName = mc.getName();
096: list.add(callConvert(mc.getChild()));
097: if ("#switch-to-if".equals(mcName)) {
098: return new SwitchToIf((SchemaVariable) list
099: .get(SchemaVariable.class));
100: } else if ("#unwind-loop".equals(mcName)) {
101: final ProgramSV[] labels = mc.getSV();
102: return new UnwindLoop(labels[0], labels[1],
103: (LoopStatement) list.get(LoopStatement.class));
104: } else if ("#unpack".equals(mcName)) {
105: return new Unpack((For) list.get(For.class));
106: } else if ("#do-break".equals(mcName)) {
107: return new DoBreak((LabeledStatement) list
108: .get(LabeledStatement.class));
109: } else if ("#expand-method-body".equals(mcName)) {
110: return new ExpandMethodBody((SchemaVariable) list
111: .get(SchemaVariable.class));
112: } else if ("#method-call".equals(mcName)
113: || "#method-call-contract".equals(mcName)) {
114: ProgramSV[] svw = mc.getSV();
115: ProgramSV execSV = null;
116: ProgramSV returnSV = null;
117: for (int i = 0; i < svw.length; i++) {
118: if (svw[i].sort() == ProgramSVSort.VARIABLE) {
119: returnSV = svw[i];
120: }
121: if (svw[i].sort() == ProgramSVSort.EXECUTIONCONTEXT) {
122: execSV = svw[i];
123: }
124: }
125: if ("#method-call".equals(mcName)) {
126: return new MethodCall(execSV, returnSV,
127: (Expression) list.get(Expression.class));
128: } else {
129: return new MethodCallContract(execSV, returnSV,
130: (Expression) list.get(Expression.class));
131: }
132: } else if ("#evaluate-arguments".equals(mcName)) {
133: return new EvaluateArgs((Expression) list
134: .get(Expression.class));
135: } else if ("#constructor-call".equals(mcName)) {
136: return new ConstructorCall(mc.getFirstSV().getSV(),
137: (Expression) list.get(Expression.class));
138: } else if ("#special-constructor-call".equals(mcName)) {
139: return new SpecialConstructorCall((Expression) list
140: .get(Expression.class));
141: } else if ("#post-work".equals(mcName)) {
142: return new PostWork((SchemaVariable) list
143: .get(SchemaVariable.class));
144: } else if ("#static-initialisation".equals(mcName)) {
145: return new StaticInitialisation((Expression) list
146: .get(Expression.class));
147: } else if ("#resolve-multiple-var-decl".equals(mcName)) {
148: return new MultipleVarDecl((SchemaVariable) list
149: .get(SchemaVariable.class));
150: } else if ("#array-post-declaration".equals(mcName)) {
151: return new ArrayPostDecl((SchemaVariable) list
152: .get(SchemaVariable.class));
153: } else if ("#init-array-creation".equals(mcName)) {
154: return new InitArrayCreation(mc.getFirstSV().getSV(),
155: (Expression) list.get(Expression.class));
156: } else if ("#init-array-creation-transient".equals(mcName)) {
157: return new InitArrayCreation(mc.getFirstSV().getSV(),
158: (Expression) list.get(Expression.class), true);
159: } else {
160: throw new ConvertException("Program meta construct "
161: + mc.toString() + " unknown.");
162: }
163: }
164:
165: public ProgramMetaConstruct convert(
166: de.uka.ilkd.key.java.recoderext.RKeYMetaConstructExpression mc) {
167: ExtList list = new ExtList();
168: String mcName = mc.getName();
169: list.add(callConvert(mc.getChild()));
170: if ("#create-object".equals(mcName)) {
171: return new CreateObject((Expression) list
172: .get(Expression.class));
173: } else if ("#isstatic".equals(mc.getName())) {
174: return new IsStatic((Expression) list.get(Expression.class));
175: } else if ("#length-reference".equals(mcName)) {
176: return new ArrayLength((Expression) list
177: .get(Expression.class));
178: } else {
179: throw new ConvertException("Program meta construct "
180: + mc.toString() + " unknown.");
181: }
182: }
183:
184: public ProgramMetaConstruct convert(
185: de.uka.ilkd.key.java.recoderext.RKeYMetaConstructType mc) {
186: ExtList list = new ExtList();
187: list.add(callConvert(mc.getChild()));
188: if ("#typeof".equals(mc.getName0())) {
189: return new TypeOf((Expression) list.get(Expression.class));
190: } else {
191: throw new ConvertException("Program meta construct "
192: + mc.toString() + " unknown.");
193: }
194: }
195:
196: public MethodFrame convert(
197: de.uka.ilkd.key.java.recoderext.RMethodCallStatement l) {
198: ProgramVariableSVWrapper svw = l.getVariableSV();
199: return new MethodFrame((IProgramVariable) (svw != null ? svw
200: .getSV() : null), (IExecutionContext) callConvert(l
201: .getExecutionContext()), (StatementBlock) callConvert(l
202: .getBody()));
203: }
204:
205: public MethodBodyStatement convert(
206: de.uka.ilkd.key.java.recoderext.RMethodBodyStatement l) {
207: final IProgramVariable resVar = (IProgramVariable) (l
208: .getResultVar() == null ? null : l.getResultVar()
209: .getSV());
210:
211: final TypeReference tr;
212: if (l.getBodySource() instanceof TypeSVWrapper) {
213: tr = (TypeReference) ((TypeSVWrapper) l.getBodySource())
214: .getSV();
215: } else {
216: tr = convert(l.getBodySource());
217: }
218:
219: return new MethodBodyStatement(tr, resVar, convert(l
220: .getMethodReference()));
221: }
222:
223: public ContextStatementBlock convert(
224: de.uka.ilkd.key.java.recoderext.ContextStatementBlock csb) {
225: ExtList children = collectChildren(csb);
226: return new ContextStatementBlock(children, csb
227: .getExecutionContext() == null ? null
228: : (IExecutionContext) callConvert(csb
229: .getExecutionContext()));
230: }
231:
232: public SchemaVariable convert(
233: de.uka.ilkd.key.java.recoderext.ExpressionSVWrapper svw) {
234:
235: return svw.getSV();
236: }
237:
238: public SchemaVariable convert(
239: de.uka.ilkd.key.java.recoderext.StatementSVWrapper svw) {
240:
241: return svw.getSV();
242: }
243:
244: public ThisReference convert(recoder.java.reference.ThisReference tr) {
245: return new ThisReference();
246: }
247:
248: public SuperReference convert(
249: recoder.java.reference.SuperReference sr) {
250: return new SuperReference();
251: }
252:
253: public SchemaVariable convert(
254: de.uka.ilkd.key.java.recoderext.LabelSVWrapper svw) {
255:
256: return svw.getSV();
257: }
258:
259: public SchemaVariable convert(
260: de.uka.ilkd.key.java.recoderext.TypeSVWrapper svw) {
261:
262: return svw.getSV();
263: }
264:
265: public SchemaVariable convert(
266: de.uka.ilkd.key.java.recoderext.ExecCtxtSVWrapper svw) {
267: return svw.getSV();
268: }
269:
270: public ExecutionContext convert(
271: de.uka.ilkd.key.java.recoderext.ExecutionContext ec) {
272: return new ExecutionContext((TypeReference) callConvert(ec
273: .getTypeReference()), (ReferencePrefix) callConvert(ec
274: .getRuntimeInstance()));
275: }
276:
277: public SchemaVariable convert(
278: de.uka.ilkd.key.java.recoderext.CatchSVWrapper svw) {
279: return svw.getSV();
280: }
281:
282: public SchemaVariable convert(
283: de.uka.ilkd.key.java.recoderext.ProgramVariableSVWrapper svw) {
284:
285: return svw.getSV();
286: }
287:
288: /**
289: * wraps a RECODER ClassDeclaration in a compilation unit
290: * @param classDecl the recoder.java.ClassDeclaration to wrap
291: * @param cUnit the recoder.java.CompilationUnit where the class is wrapped
292: * @return the enclosing recoder.java.CompilationUnit
293: */
294: protected recoder.java.CompilationUnit embedClass(
295: recoder.java.declaration.ClassDeclaration classDecl,
296: Context context) {
297:
298: recoder.java.CompilationUnit cUnit = context
299: .getCompilationUnitContext();
300:
301: // add class to compilation unit
302: recoder.list.TypeDeclarationMutableList typeDecls = cUnit
303: .getDeclarations();
304:
305: if (typeDecls == null) {
306: typeDecls = new recoder.list.TypeDeclarationArrayList(0);
307: } else {
308: typeDecls = (recoder.list.TypeDeclarationMutableList) typeDecls
309: .deepClone();
310: }
311: typeDecls.add(classDecl);
312:
313: recoder.java.CompilationUnit compUnitContext = (recoder.java.CompilationUnit) cUnit
314: .deepClone();
315:
316: compUnitContext.setDeclarations(typeDecls);
317: compUnitContext.makeParentRoleValid();
318: schemaServConf.getChangeHistory().attached(compUnitContext);
319: schemaServConf.getChangeHistory().updateModel();
320: return compUnitContext;
321: }
322:
323: /** parses a given JavaBlock using the context to determine the right
324: * references and returns a statement block of recoder.
325: * @param block a String describing a java block
326: * @param context recoder.java.CompilationUnit in which the block has
327: * to be interpreted
328: * @return the parsed and resolved recoder statement block
329: */
330: protected recoder.java.StatementBlock recoderBlock(String block,
331: Context context) {
332: recoder.java.StatementBlock bl = null;
333:
334: SchemaJavaProgramFactory factory = (SchemaJavaProgramFactory) schemaServConf
335: .getProgramFactory();
336: factory.setSVNamespace(svns);
337: try {
338: bl = factory.parseStatementBlock(new StringReader(block));
339: } catch (recoder.ParserException e) {
340: Debug.out("readSchemaJavaBlock(Reader,CompilationUnit)"
341: + " caused the " + "exception:\n", e);
342: Debug.printStackTrace(e);
343: throw new ConvertException("Parsing: \n **** BEGIN ****\n "
344: + block
345: + "\n **** END ****\n failed. Thrown Exception:"
346: + e.toString());
347: } catch (IOException ioe) {
348: Debug.out("readSchemaJavaBlock(Reader,CompilationUnit)"
349: + " caused the IO exception:\n", ioe);
350: Debug.printStackTrace(ioe);
351: throw new ConvertException(
352: "IO Error when parsing: \n **** BEGIN ****\n "
353: + block
354: + "\n **** END ****\n failed. Thrown IOException:"
355: + ioe.toString());
356: }
357:
358: embedClass(embedMethod(embedBlock(bl), context), context);
359:
360: return bl;
361: }
362:
363: /**
364: * converts a For.
365: * @param f the For of recoder
366: * @return the For of KeY
367: */
368: public For convert(recoder.java.statement.For f) {
369:
370: ILoopInit li;
371: IForUpdates ifu;
372: IGuard iGuard;
373: if (f.getInitializers() != null
374: && f.getInitializers().getLoopInitializer(0) instanceof de.uka.ilkd.key.java.recoderext.ExpressionSVWrapper) {
375: de.uka.ilkd.key.java.recoderext.ExpressionSVWrapper esvw = (de.uka.ilkd.key.java.recoderext.ExpressionSVWrapper) f
376: .getInitializers().getLoopInitializer(0); //brrrr!
377: li = (ProgramSV) esvw.getSV();
378: } else {
379: li = convertLoopInitializers(f);
380: }
381:
382: if (f.getGuard() instanceof de.uka.ilkd.key.java.recoderext.ExpressionSVWrapper) {
383: de.uka.ilkd.key.java.recoderext.ExpressionSVWrapper esvw = (de.uka.ilkd.key.java.recoderext.ExpressionSVWrapper) f
384: .getGuard();
385: iGuard = (ProgramSV) esvw.getSV();
386: } else {
387: iGuard = convertGuard(f);
388: }
389:
390: if (f.getUpdates() != null
391: && f.getUpdates().getExpression(0) instanceof de.uka.ilkd.key.java.recoderext.ExpressionSVWrapper) {
392: de.uka.ilkd.key.java.recoderext.ExpressionSVWrapper esvw = (de.uka.ilkd.key.java.recoderext.ExpressionSVWrapper) f
393: .getUpdates().getExpression(0);
394: ifu = (ProgramSV) esvw.getSV();
395: } else {
396: ifu = convertUpdates(f);
397: }
398:
399: return new For(li, iGuard, ifu, convertBody(f));
400: }
401:
402: protected VariableSpecification convertVarSpecWithSVType(
403: recoder.java.declaration.VariableSpecification recoderVarspec) {
404: VariableSpecification varspec = (VariableSpecification) rec2key()
405: .toKeY(recoderVarspec);
406: if (varspec == null) {
407: ExtList l = collectChildren(recoderVarspec);
408: ProgramElement pv = ProgramSVSort.VARIABLE.getSVWithSort(l,
409: ProgramElementName.class);
410: if (pv instanceof ProgramElementName) { //sth. like #type i;
411: KeYJavaType kjt = new KeYJavaType(typeSVType);
412: pv = new LocationVariable((ProgramElementName) pv, kjt);
413: }
414: ProgramElement init = ProgramSVSort.VARIABLEINIT
415: .getSVWithSort(l, Expression.class);
416: varspec = new VariableSpecification((IProgramVariable) pv,
417: recoderVarspec.getDimensions(), (Expression) init,
418: typeSVType, null);
419: insertToMap(recoderVarspec, varspec);
420: }
421: return varspec;
422: }
423:
424: public LocalVariableDeclaration convert(
425: recoder.java.declaration.LocalVariableDeclaration lvd) {
426: if (lvd.getTypeReference() instanceof TypeSVWrapper) {
427: recoder.list.VariableSpecificationList rspecs = lvd
428: .getVariables();
429: VariableSpecification[] varspecs = new VariableSpecification[rspecs
430: .size()];
431: for (int i = 0; i < rspecs.size(); i++) {
432: varspecs[i] = convertVarSpecWithSVType(rspecs
433: .getVariableSpecification(i));
434: }
435: SchemaVariable typesv = ((TypeSVWrapper) lvd
436: .getTypeReference()).getSV();
437:
438: recoder.list.ModifierList mods = lvd.getModifiers();
439: Modifier[] modifiers = new Modifier[mods == null ? 0 : mods
440: .size()];
441: for (int i = 0; i < modifiers.length; i++) {
442: modifiers[i] = (Modifier) callConvert(mods
443: .getModifier(i));
444: }
445:
446: return new LocalVariableDeclaration(modifiers,
447: (ProgramSV) typesv, varspecs);
448: } else {
449: return super .convert(lvd);
450: }
451: }
452:
453: /**
454: * convert a recoder TypeReference to a KeY TypeReference
455: * (checks dimension and hands it over)
456: */
457: public TypeReference convert(recoder.java.reference.TypeReference tr) {
458:
459: recoder.java.reference.ReferencePrefix rp = tr
460: .getReferencePrefix();
461:
462: recoder.java.reference.PackageReference prefix = null;
463: recoder.java.reference.PackageReference result = null;
464: while (rp != null) {
465: if (prefix == null) {
466: result = new recoder.java.reference.PackageReference(
467: ((recoder.java.reference.UncollatedReferenceQualifier) rp)
468: .getIdentifier());
469: prefix = result;
470: } else {
471: recoder.java.reference.PackageReference prefix2 = new recoder.java.reference.PackageReference(
472: ((recoder.java.reference.UncollatedReferenceQualifier) rp)
473: .getIdentifier());
474: prefix.setReferencePrefix(prefix2);
475: prefix = prefix2;
476: }
477:
478: if (rp instanceof recoder.java.reference.ReferenceSuffix) {
479: rp = ((recoder.java.reference.ReferenceSuffix) rp)
480: .getReferencePrefix();
481: } else {
482: rp = null;
483: }
484: }
485:
486: return new SchemaTypeReference(new ProgramElementName(tr
487: .getName()), tr.getDimensions(),
488: result != null ? convert(result) : null);
489: }
490:
491: /** convert a recoder VariableSpecification to a KeY
492: * VariableSpecification
493: * (checks dimension and hands it over and insert in hashmap)
494: */
495: public VariableSpecification convert(
496: recoder.java.declaration.VariableSpecification recoderVarspec) {
497:
498: if (!(recoderVarspec.getIdentifier() instanceof ProgramVariableSVWrapper)) {
499: return super .convert(recoderVarspec);
500: }
501: VariableSpecification varSpec = (VariableSpecification) rec2key()
502: .toKeY(recoderVarspec);
503: if (varSpec == null) {
504:
505: ExtList children = collectChildren(recoderVarspec);
506: IProgramVariable progvar = (IProgramVariable) children
507: .get(SchemaVariable.class);
508:
509: children.remove(progvar);
510: varSpec = new VariableSpecification(children, progvar,
511: recoderVarspec.getDimensions(), null);
512: insertToMap(recoderVarspec, varSpec);
513:
514: }
515: return varSpec;
516: }
517:
518: public Expression convert(recoder.java.reference.FieldReference fr) {
519:
520: ReferencePrefix prefix = null;
521: if (fr.getReferencePrefix() != null) {
522: prefix = (ReferencePrefix) callConvert(fr
523: .getReferencePrefix());
524: }
525:
526: SchemaVariable suffix = (SchemaVariable) callConvert(fr
527: .getIdentifier());
528:
529: return new SchematicFieldReference(suffix, prefix);
530: }
531:
532: public MethodReference convert(
533: recoder.java.reference.MethodReference mr) {
534:
535: // convert reference prefix
536: final ReferencePrefix prefix;
537: if (mr.getReferencePrefix() instanceof recoder.java.reference.UncollatedReferenceQualifier) {
538: // type references would be allowed
539: final recoder.java.reference.UncollatedReferenceQualifier uncoll = (recoder.java.reference.UncollatedReferenceQualifier) mr
540: .getReferencePrefix();
541: prefix = convert(new recoder.java.reference.TypeReference(
542: uncoll.getReferencePrefix(), uncoll.getIdentifier()));
543: } else {
544: if (mr.getReferencePrefix() != null) {
545: prefix = (ReferencePrefix) callConvert(mr
546: .getReferencePrefix());
547: } else {
548: prefix = null;
549: }
550: }
551: // convert MethodName
552: MethodName name = (MethodName) callConvert(mr.getIdentifier());
553:
554: // convert arguments
555: recoder.list.ExpressionMutableList recoderArgs = mr
556: .getArguments();
557: final Expression[] keyArgs;
558: if (recoderArgs != null) {
559: keyArgs = new Expression[recoderArgs.size()];
560: } else {
561: keyArgs = new Expression[0];
562: }
563: for (int i = 0, sz = keyArgs.length; i < sz; i++) {
564: keyArgs[i] = (Expression) callConvert(recoderArgs
565: .getExpression(i));
566: }
567:
568: return new MethodReference(new ArrayOfExpression(keyArgs),
569: name, prefix);
570: }
571:
572: public void parseSpecialClasses() {
573: }
574: }
|