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: //
012:
013: // This file is partially taken from the RECODER library, which is protected by
014: // the LGPL, and modified.
015:
016: package de.uka.ilkd.key.java.recoderext;
017:
018: import java.io.IOException;
019: import java.io.Reader;
020:
021: import recoder.ParserException;
022: import recoder.convenience.TreeWalker;
023: import recoder.java.*;
024: import recoder.java.SourceElement.Position;
025: import recoder.java.declaration.*;
026: import recoder.java.reference.MethodReference;
027: import recoder.java.reference.ReferencePrefix;
028: import recoder.java.reference.TypeReference;
029: import recoder.list.CommentArrayList;
030: import recoder.list.CommentMutableList;
031: import recoder.list.StatementMutableList;
032: import de.uka.ilkd.key.logic.Name;
033: import de.uka.ilkd.key.logic.Named;
034: import de.uka.ilkd.key.logic.Namespace;
035: import de.uka.ilkd.key.logic.op.SchemaVariable;
036: import de.uka.ilkd.key.logic.op.SortedSchemaVariable;
037: import de.uka.ilkd.key.logic.sort.ProgramSVSort;
038: import de.uka.ilkd.key.parser.schemajava.ParseException;
039: import de.uka.ilkd.key.parser.schemajava.SchemaJavaParser;
040:
041: public class SchemaJavaProgramFactory extends JavaProgramFactory {
042:
043: protected Namespace svns;
044:
045: /**
046: Protected constructor - use {@link #getInstance} instead.
047: */
048: protected SchemaJavaProgramFactory() {
049: }
050:
051: /**
052: The singleton instance of the program factory.
053: */
054: private static SchemaJavaProgramFactory theFactory = new SchemaJavaProgramFactory();
055:
056: /**
057: Returns the single instance of this class.
058: */
059: public static JavaProgramFactory getInstance() {
060: return theFactory;
061: }
062:
063: /**
064: * Create an {@link ImplicitIdentifier}.
065: */
066: public ImplicitIdentifier createImplicitIdentifier(String text) {
067: return new ImplicitIdentifier(text);
068: }
069:
070: public SpecialReferenceWrapper createThisReference(
071: TypeReference typeRef, Expression var) {
072: return new SpecialReferenceWrapper(typeRef,
073: (ReferencePrefix) var);
074: }
075:
076: public RMethodCallStatement createRMethodCallStatement(
077: ProgramVariableSVWrapper resVar, ExecutionContext esvw,
078: Statement st) {
079: return new RMethodCallStatement(resVar, esvw, st);
080: }
081:
082: public RMethodBodyStatement createRMethodBodyStatement(
083: TypeReference typeRef, ProgramVariableSVWrapper resVar,
084: MethodReference mr) {
085: return new RMethodBodyStatement(typeRef, resVar, mr);
086: }
087:
088: public RKeYMetaConstruct createRKeYMetaConstruct() {
089: return new RKeYMetaConstruct();
090: }
091:
092: public RKeYMetaConstructExpression createRKeYMetaConstructExpression() {
093: return new RKeYMetaConstructExpression();
094: }
095:
096: public RKeYMetaConstructType createRKeYMetaConstructType() {
097: return new RKeYMetaConstructType();
098: }
099:
100: public ContextStatementBlock createContextStatementBlock(
101: TypeSVWrapper typeRef, ExpressionSVWrapper var) {
102: return new ContextStatementBlock(typeRef, var);
103: }
104:
105: public ContextStatementBlock createContextStatementBlock(
106: ExecCtxtSVWrapper ec) {
107: return new ContextStatementBlock(ec);
108: }
109:
110: /**
111: * Create a {@link PassiveExpression}.
112: */
113: public PassiveExpression createPassiveExpression(Expression e) {
114: return new PassiveExpression(e);
115: }
116:
117: /**
118: * Create a {@link PassiveExpression}.
119: */
120: public PassiveExpression createPassiveExpression() {
121: return new PassiveExpression();
122: }
123:
124: public static void throwSortInvalid(SchemaVariable sv, String s)
125: throws ParseException {
126: throw new ParseException("Sort of declared schema variable "
127: + sv.name().toString() + " "
128: + ((SortedSchemaVariable) sv).sort().name().toString()
129: + " does not comply with expected type " + s
130: + " in Java program.");
131: }
132:
133: public boolean lookupSchemaVariableType(String s, ProgramSVSort sort) {
134: if (svns == null)
135: return false;
136: Named n = svns.lookup(new Name(s));
137: if (n != null && n instanceof SortedSchemaVariable) {
138: return ((SortedSchemaVariable) n).sort() == sort;
139: }
140: return false;
141: }
142:
143: public SchemaVariable lookupSchemaVariable(String s)
144: throws ParseException {
145: SchemaVariable sv = null;
146: Named n = svns.lookup(new Name(s));
147: if (n != null && n instanceof SchemaVariable) {
148: sv = (SchemaVariable) n;
149: } else {
150: throw new ParseException("Schema variable not declared: "
151: + s);
152: }
153: return sv;
154: }
155:
156: public StatementSVWrapper getStatementSV(String s)
157: throws ParseException {
158: SchemaVariable sv = lookupSchemaVariable(s);
159: if (!sv.isProgramSV()) {
160: throwSortInvalid(sv, "Statement");
161: }
162:
163: return new StatementSVWrapper(sv);
164: }
165:
166: public ExpressionSVWrapper getExpressionSV(String s)
167: throws ParseException {
168: SchemaVariable sv = lookupSchemaVariable(s);
169: if (!sv.isProgramSV()) {
170: throwSortInvalid(sv, "Expression");
171: }
172: return new ExpressionSVWrapper(sv);
173: }
174:
175: public LabelSVWrapper getLabelSV(String s) throws ParseException {
176: SchemaVariable sv = lookupSchemaVariable(s);
177: if (!sv.isProgramSV()) {
178: throwSortInvalid(sv, "Label");
179: }
180: return new LabelSVWrapper(sv);
181: }
182:
183: public JumpLabelSVWrapper getJumpLabelSV(String s)
184: throws ParseException {
185: SchemaVariable sv = lookupSchemaVariable(s);
186: if (!sv.isProgramSV()
187: || ((SortedSchemaVariable) sv).sort() != ProgramSVSort.LABEL) {
188: throwSortInvalid(sv, "Label");
189: }
190: return new JumpLabelSVWrapper(sv);
191: }
192:
193: public TypeSVWrapper getTypeSV(String s) throws ParseException {
194: SchemaVariable sv = lookupSchemaVariable(s);
195: if (!sv.isProgramSV()) {
196: throwSortInvalid(sv, "Type");
197: }
198: return new TypeSVWrapper(sv);
199: }
200:
201: public ExecCtxtSVWrapper getExecutionContextSV(String s)
202: throws ParseException {
203: SchemaVariable sv = lookupSchemaVariable(s);
204: if (!sv.isProgramSV()) {
205: throwSortInvalid(sv, "Type");
206: }
207: return new ExecCtxtSVWrapper(sv);
208: }
209:
210: public ProgramVariableSVWrapper getProgramVariableSV(String s)
211: throws ParseException {
212: SchemaVariable sv = lookupSchemaVariable(s);
213: if (!sv.isProgramSV()) {
214: throwSortInvalid(sv, "Program Variable");
215: }
216: return new ProgramVariableSVWrapper(sv);
217: }
218:
219: public CatchSVWrapper getCatchSV(String s) throws ParseException {
220: SchemaVariable sv = lookupSchemaVariable(s);
221: if (!sv.isProgramSV()) {
222: throwSortInvalid(sv, "Catch");
223: }
224: return new CatchSVWrapper(sv);
225: }
226:
227: /**
228: For internal reuse and synchronization.
229: */
230: private static SchemaJavaParser parser = new SchemaJavaParser(
231: System.in);
232:
233: private static final Position ZERO_POSITION = new Position(0, 0);
234:
235: private static void attachComment(Comment c, ProgramElement pe) {
236: ProgramElement dest = pe;
237: if (!c.isPrefixed()) {
238: NonTerminalProgramElement ppe = dest.getASTParent();
239: int i = 0;
240: if (ppe != null) {
241: for (; ppe.getChildAt(i) != dest; i++) {
242: }
243: }
244: if (i == 0) { // before syntactical parent
245: c.setPrefixed(true);
246: } else {
247: dest = ppe.getChildAt(i - 1);
248: while (dest instanceof NonTerminalProgramElement) {
249: ppe = (NonTerminalProgramElement) dest;
250: i = ppe.getChildCount();
251: if (i == 0) {
252: break;
253: }
254: dest = ppe.getChildAt(i - 1);
255: }
256: }
257: }
258: if (c instanceof SingleLineComment && c.isPrefixed()) {
259: Position p = dest.getFirstElement().getRelativePosition();
260: if (p.getLine() < 1) {
261: p.setLine(1);
262: dest.getFirstElement().setRelativePosition(p);
263: }
264: }
265: CommentMutableList cml = dest.getComments();
266: if (cml == null) {
267: dest.setComments(cml = new CommentArrayList());
268: }
269: cml.add(c);
270: }
271:
272: /**
273: Perform post work on the created element. Creates parent links
274: and assigns comments.
275: */
276: private static void postWork(ProgramElement pe) {
277: CommentMutableList comments = SchemaJavaParser.getComments();
278: int commentIndex = 0;
279: int commentCount = comments.size();
280: Position cpos = ZERO_POSITION;
281: Comment current = null;
282: if (commentIndex < commentCount) {
283: current = comments.getComment(commentIndex);
284: cpos = current.getFirstElement().getStartPosition();
285: }
286: TreeWalker tw = new TreeWalker(pe);
287: while (tw.next()) {
288: pe = tw.getProgramElement();
289: if (pe instanceof NonTerminalProgramElement) {
290: ((NonTerminalProgramElement) pe).makeParentRoleValid();
291: }
292: if (pe.getFirstElement() != null) {
293: Position pos = pe.getFirstElement().getStartPosition();
294: while ((commentIndex < commentCount)
295: && pos.compareTo(cpos) > 0) {
296: attachComment(current, pe);
297: commentIndex += 1;
298: if (commentIndex < commentCount) {
299: current = comments.getComment(commentIndex);
300: cpos = current.getFirstElement()
301: .getStartPosition();
302: }
303: }
304: }
305: }
306: if (commentIndex < commentCount) {
307: while (pe.getASTParent() != null) {
308: pe = pe.getASTParent();
309: }
310: CommentMutableList cml = pe.getComments();
311: if (cml == null) {
312: pe.setComments(cml = new CommentArrayList());
313: }
314: do {
315: current = comments.getComment(commentIndex);
316: current.setPrefixed(false);
317: cml.add(current);
318: commentIndex += 1;
319: } while (commentIndex < commentCount);
320: }
321: }
322:
323: /**
324: Parse a {@link CompilationUnit} from the given reader.
325: */
326: public CompilationUnit parseCompilationUnit(Reader in)
327: throws IOException, ParserException {
328: synchronized (parser) {
329: try {
330: SchemaJavaParser.initialize(in);
331: CompilationUnit res = SchemaJavaParser
332: .CompilationUnit();
333: postWork(res);
334: return res;
335: } catch (ParseException e) {
336: throw new ParserException();
337: }
338: }
339: }
340:
341: /**
342: Parse a {@link TypeDeclaration} from the given reader.
343: */
344: public TypeDeclaration parseTypeDeclaration(Reader in)
345: throws IOException, ParserException {
346: synchronized (parser) {
347: try {
348: SchemaJavaParser.initialize(in);
349: TypeDeclaration res = SchemaJavaParser
350: .TypeDeclaration();
351: postWork(res);
352: return res;
353: } catch (ParseException e) {
354: throw new ParserException();
355: }
356:
357: }
358: }
359:
360: /**
361: Parse a {@link FieldDeclaration} from the given reader.
362: */
363: public FieldDeclaration parseFieldDeclaration(Reader in)
364: throws IOException, ParserException {
365: synchronized (parser) {
366: try {
367: SchemaJavaParser.initialize(in);
368: FieldDeclaration res = SchemaJavaParser
369: .FieldDeclaration();
370: postWork(res);
371: return res;
372: } catch (ParseException e) {
373: throw new ParserException();
374: }
375:
376: }
377: }
378:
379: /**
380: Parse a {@link MethodDeclaration} from the given reader.
381: */
382: public MethodDeclaration parseMethodDeclaration(Reader in)
383: throws IOException, ParserException {
384: synchronized (parser) {
385: try {
386: SchemaJavaParser.initialize(in);
387: MethodDeclaration res = SchemaJavaParser
388: .MethodDeclaration();
389: postWork(res);
390: return res;
391: } catch (ParseException e) {
392: throw new ParserException();
393: }
394:
395: }
396: }
397:
398: /**
399: Parse a {@link MemberDeclaration} from the given reader.
400: */
401: public MemberDeclaration parseMemberDeclaration(Reader in)
402: throws IOException, ParserException {
403: synchronized (parser) {
404: try {
405: SchemaJavaParser.initialize(in);
406: MemberDeclaration res = SchemaJavaParser
407: .ClassBodyDeclaration();
408: postWork(res);
409: return res;
410: } catch (ParseException e) {
411: throw new ParserException();
412: }
413:
414: }
415: }
416:
417: /**
418: Parse a {@link ParameterDeclaration} from the given reader.
419: */
420: public ParameterDeclaration parseParameterDeclaration(Reader in)
421: throws IOException, ParserException {
422: synchronized (parser) {
423: try {
424: SchemaJavaParser.initialize(in);
425: ParameterDeclaration res = SchemaJavaParser
426: .FormalParameter();
427: postWork(res);
428: return res;
429: } catch (ParseException e) {
430: throw new ParserException();
431: }
432:
433: }
434: }
435:
436: /**
437: Parse a {@link ConstructorDeclaration} from the given reader.
438: */
439: public ConstructorDeclaration parseConstructorDeclaration(Reader in)
440: throws IOException, ParserException {
441: synchronized (parser) {
442: try {
443: SchemaJavaParser.initialize(in);
444: ConstructorDeclaration res = SchemaJavaParser
445: .ConstructorDeclaration();
446: postWork(res);
447: return res;
448: } catch (ParseException e) {
449: throw new ParserException();
450: }
451:
452: }
453: }
454:
455: /**
456: Parse a {@link TypeReference} from the given reader.
457: */
458: public TypeReference parseTypeReference(Reader in)
459: throws IOException, ParserException {
460: synchronized (parser) {
461: try {
462: SchemaJavaParser.initialize(in);
463: TypeReference res = SchemaJavaParser.ResultType();
464: postWork(res);
465: return res;
466: } catch (ParseException e) {
467: throw new ParserException();
468: }
469:
470: }
471: }
472:
473: /**
474: Parse an {@link Expression} from the given reader.
475: */
476: public Expression parseExpression(Reader in) throws IOException,
477: ParserException {
478: synchronized (parser) {
479: try {
480: SchemaJavaParser.initialize(in);
481: Expression res = SchemaJavaParser.Expression();
482: postWork(res);
483: return res;
484: } catch (ParseException e) {
485: throw new ParserException();
486: }
487:
488: }
489: }
490:
491: /**
492: Parse some {@link Statement}s from the given reader.
493: */
494: public StatementMutableList parseStatements(Reader in)
495: throws IOException, ParserException {
496: synchronized (parser) {
497: try {
498: SchemaJavaParser.initialize(in);
499: StatementMutableList res = SchemaJavaParser
500: .GeneralizedStatements();
501: for (int i = 0; i < res.size(); i += 1) {
502: postWork(res.getStatement(i));
503: }
504: return res;
505: } catch (ParseException e) {
506: throw new ParserException();
507: }
508:
509: }
510: }
511:
512: /**
513: * Parse a {@link StatementBlock} from the given string.
514: */
515: public StatementBlock parseStatementBlock(Reader in)
516: throws IOException, ParserException {
517: synchronized (parser) {
518: try {
519: SchemaJavaParser.initialize(in);
520: StatementBlock res = SchemaJavaParser.StartBlock();
521: postWork(res);
522: return res;
523: } catch (ParseException e) {
524: throw new ParserException(e.toString());
525: }
526:
527: }
528: }
529:
530: public void setSVNamespace(Namespace ns) {
531: svns = ns;
532: }
533:
534: }
|