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: // This file is part of KeY - Integrated Deductive Software Design
009: // Copyright (C) 2001-2005 Universitaet Karlsruhe, Germany
010: // Universitaet Koblenz-Landau, Germany
011: // Chalmers University of Technology, Sweden
012: //
013: // The KeY system is protected by the GNU General Public License.
014: // See LICENSE.TXT for details.
015: //
016: //
017:
018: package de.uka.ilkd.key.logic;
019:
020: import java.util.HashMap;
021:
022: import de.uka.ilkd.key.collection.IteratorOfString;
023: import de.uka.ilkd.key.collection.ListOfString;
024: import de.uka.ilkd.key.java.*;
025: import de.uka.ilkd.key.java.abstraction.KeYJavaType;
026: import de.uka.ilkd.key.java.declaration.LocalVariableDeclaration;
027: import de.uka.ilkd.key.java.declaration.VariableSpecification;
028: import de.uka.ilkd.key.java.expression.operator.CopyAssignment;
029: import de.uka.ilkd.key.java.reference.ExecutionContext;
030: import de.uka.ilkd.key.java.statement.EmptyStatement;
031: import de.uka.ilkd.key.java.statement.MethodFrame;
032: import de.uka.ilkd.key.java.visitor.JavaASTWalker;
033: import de.uka.ilkd.key.java.visitor.ProgramReplaceVisitor;
034: import de.uka.ilkd.key.logic.op.*;
035: import de.uka.ilkd.key.logic.sort.ArraySort;
036: import de.uka.ilkd.key.logic.sort.PrimitiveSort;
037: import de.uka.ilkd.key.logic.sort.ProgramSVSort;
038: import de.uka.ilkd.key.logic.sort.Sort;
039: import de.uka.ilkd.key.proof.Goal;
040: import de.uka.ilkd.key.proof.InstantiationProposer;
041: import de.uka.ilkd.key.proof.Node;
042: import de.uka.ilkd.key.proof.ProofSaver;
043: import de.uka.ilkd.key.rule.IteratorOfTacletGoalTemplate;
044: import de.uka.ilkd.key.rule.NewVarcond;
045: import de.uka.ilkd.key.rule.RewriteTacletGoalTemplate;
046: import de.uka.ilkd.key.rule.TacletApp;
047: import de.uka.ilkd.key.rule.inst.ContextInstantiationEntry;
048: import de.uka.ilkd.key.rule.inst.SVInstantiations;
049:
050: /**
051: * Responsible for program variable naming issues.
052: */
053: public abstract class VariableNamer implements InstantiationProposer {
054:
055: //-------------------------------------------------------------------------
056: //member variables
057: //-------------------------------------------------------------------------
058:
059: /**
060: * default basename for variable name proposals
061: */
062: private static final String DEFAULT_BASENAME = "var";
063:
064: /**
065: * name of the counter object used for temporary name proposals
066: */
067: private static final String TEMPCOUNTER_NAME = "VarNamerCnt";
068:
069: /**
070: * status of suggestive name proposing
071: */
072: private static boolean suggestive_off = true;
073:
074: /**
075: * pointer to services object
076: */
077: private final Services services;
078:
079: protected HashMap map = new HashMap();
080: protected HashMap renamingHistory = new HashMap();
081:
082: //-------------------------------------------------------------------------
083: //constructors
084: //-------------------------------------------------------------------------
085:
086: /**
087: * @param services pointer to services object
088: */
089: public VariableNamer(Services services) {
090: this .services = services;
091: }
092:
093: //-------------------------------------------------------------------------
094: //internal: general stuff
095: //-------------------------------------------------------------------------
096:
097: /**
098: * determines the passed ProgramElementName's basename and index (ignoring
099: * temporary indices)
100: */
101: protected BasenameAndIndex getBasenameAndIndex(
102: ProgramElementName name) {
103: BasenameAndIndex result = new BasenameAndIndex();
104:
105: if (name instanceof PermIndProgramElementName) {
106: result.basename = ((IndProgramElementName) name)
107: .getBaseName();
108: result.index = ((IndProgramElementName) name).getIndex();
109: } else if (name instanceof TempIndProgramElementName) {
110: result.basename = ((IndProgramElementName) name)
111: .getBaseName();
112: result.index = 0;
113: } else {
114: result.basename = name.toString();
115: result.index = 0;
116: }
117:
118: //for debugging
119: /*if(!(name instanceof IndProgramElementName)
120: && parseName(name.toString()) instanceof IndProgramElementName) {
121: System.out.println("VN Debug error: inspected name \"" + name
122: + "\" has " + name.getClass());
123: }*/
124:
125: return result;
126: }
127:
128: public HashMap getRenamingMap() {
129: return renamingHistory;
130: }
131:
132: /**
133: * returns the subterm containing a java block, or null
134: * (helper for getProgramFromPIO())
135: */
136: private Term findProgramInTerm(Term term) {
137: if (term.javaBlock() != JavaBlock.EMPTY_JAVABLOCK) {
138: return term;
139: }
140: for (int i = 0; i < term.arity(); i++) {
141: Term subterm = findProgramInTerm(term.sub(i));
142: if (subterm != null) {
143: return subterm;
144: }
145: }
146: return null;
147: }
148:
149: /**
150: * returns the program contained in a PosInOccurrence
151: */
152: protected ProgramElement getProgramFromPIO(PosInOccurrence pio) {
153: Term progTerm;
154: if (pio != null
155: && (progTerm = findProgramInTerm(pio.subTerm())) != null) {
156: return progTerm.javaBlock().program();
157: } else {
158: return new EmptyStatement();
159: }
160: }
161:
162: /**
163: * returns a NameCreationInfo representing the method stack of a
164: * PosInOccurrence
165: */
166: protected NameCreationInfo getMethodStack(PosInOccurrence posOfFind) {
167: ListOfProgramMethod list = SLListOfProgramMethod.EMPTY_LIST;
168:
169: SourceElement element = getProgramFromPIO(posOfFind);
170: while (element != element.getFirstElement()) {
171: element = element.getFirstElement();
172:
173: if (element instanceof MethodFrame) {
174: MethodFrame frame = (MethodFrame) element;
175: ProgramMethod method = frame.getProgramMethod();
176: if (method != null) {
177: list = list.append(method);
178: }
179: }
180: }
181:
182: return new MethodStackInfo(list);
183: }
184:
185: /**
186: * creates a ProgramElementName object to be used for permanent names
187: */
188: protected ProgramElementName createName(String basename, int index,
189: NameCreationInfo creationInfo) {
190: return new PermIndProgramElementName(basename, index,
191: creationInfo);
192: }
193:
194: //-------------------------------------------------------------------------
195: //internal: counter finding
196: //-------------------------------------------------------------------------
197:
198: /**
199: * returns the maximum counter value already associated with the passed
200: * basename in the passed list of global variables, or -1
201: */
202: protected int getMaxCounterInGlobals(String basename,
203: Globals globals) {
204: int result = -1;
205:
206: IteratorOfProgramElementName it = globals.iterator();
207: while (it.hasNext()) {
208: ProgramElementName name = it.next();
209: BasenameAndIndex bai = getBasenameAndIndex(name);
210: if (bai.basename.equals(basename) && bai.index > result) {
211: result = bai.index;
212: }
213: }
214:
215: return result;
216: }
217:
218: /**
219: * returns the maximum counter value already associated with the passed
220: * basename in the passed program (ignoring temporary counters), or -1
221: */
222: protected int getMaxCounterInProgram(String basename,
223: ProgramElement program, PosInProgram posOfDeclaration) {
224: class MyWalker extends CustomJavaASTWalker {
225: public String basename;
226: public int maxCounter = -1;
227:
228: public MyWalker(ProgramElement program,
229: PosInProgram posOfDeclaration) {
230: super (program, posOfDeclaration);
231: }
232:
233: protected void doAction(ProgramElement node) {
234: if (node instanceof ProgramVariable) {
235: ProgramVariable var = (ProgramVariable) node;
236: ProgramElementName name = var
237: .getProgramElementName();
238: if (!(name instanceof TempIndProgramElementName)) {
239: BasenameAndIndex bai = getBasenameAndIndex(name);
240: if (bai.basename.equals(basename)
241: && bai.index > maxCounter) {
242: maxCounter = bai.index;
243: }
244: }
245: }
246: }
247: }
248:
249: MyWalker walker = new MyWalker(program, posOfDeclaration);
250: walker.basename = basename;
251: walker.start();
252:
253: return walker.maxCounter;
254: }
255:
256: //-------------------------------------------------------------------------
257: //internal: uniqueness checking
258: //-------------------------------------------------------------------------
259:
260: /**
261: * tells whether a name is unique in the passed list of global variables
262: */
263: protected boolean isUniqueInGlobals(String name, Globals globals) {
264: IteratorOfProgramElementName it = globals.iterator();
265: while (it.hasNext()) {
266: ProgramElementName n = it.next();
267: if (n.toString().equals(name)) {
268: return false;
269: }
270: }
271: return true;
272: }
273:
274: /**
275: * tells whether a name is unique in the passed program
276: */
277: protected boolean isUniqueInProgram(String name,
278: ProgramElement program, PosInProgram posOfDeclaration) {
279: class MyWalker extends CustomJavaASTWalker {
280: public String nameToFind;
281: public boolean foundIt = false;
282:
283: public MyWalker(ProgramElement program,
284: PosInProgram posOfDeclaration) {
285: super (program, posOfDeclaration);
286: }
287:
288: protected void doAction(ProgramElement node) {
289: if (node instanceof ProgramVariable) {
290: ProgramVariable var = (ProgramVariable) node;
291: ProgramElementName varname = var
292: .getProgramElementName();
293: if (varname.getProgramName().equals(nameToFind)) {
294: foundIt = true;
295: }
296: }
297: }
298: }
299:
300: MyWalker walker = new MyWalker(program, posOfDeclaration);
301: walker.nameToFind = name;
302: walker.start();
303:
304: return !walker.foundIt;
305: }
306:
307: //-------------------------------------------------------------------------
308: //internal: uniform treatment of global variables
309: //-------------------------------------------------------------------------
310:
311: /**
312: * creates a Globals object for use with other internal methods
313: */
314: protected Globals wrapGlobals(ListOfNamed globals) {
315: return new GlobalsAsListOfNamed(globals);
316: }
317:
318: /**
319: * creates a Globals object for use with other internal methods
320: */
321: protected Globals wrapGlobals(SetOfProgramVariable globals) {
322: return new GlobalsAsSetOfProgramVariable(globals);
323: }
324:
325: //-------------------------------------------------------------------------
326: //interface: renaming
327: //-------------------------------------------------------------------------
328:
329: /**
330: * intended to be called when symbolically executing a variable declaration;
331: * resolves any naming conflicts between the new variable and other global
332: * variables by renaming the new variable and / or other variables
333: * @param var the new program variable
334: * @param goal the goal
335: * @param posOfFind the PosInOccurrence of the currently executed program
336: * @return the renamed version of the var parameter
337: */
338: public abstract ProgramVariable rename(ProgramVariable var,
339: Goal goal, PosInOccurrence posOfFind);
340:
341: //-------------------------------------------------------------------------
342: //internal: name proposals
343: //-------------------------------------------------------------------------
344:
345: /**
346: * proposes a base name for a given sort
347: */
348: private String getBaseNameProposal(Sort sort) {
349: String result;
350: String name = sort.name().toString();
351: if (sort instanceof PrimitiveSort) {
352: result = name.substring(0, 1);
353: } else if (sort instanceof ArraySort) {
354: result = DEFAULT_BASENAME;
355: } else {
356: int lastDotIndex = name.lastIndexOf('.');
357: if (lastDotIndex != -1) {
358: name = name.substring(lastDotIndex + 1);
359: }
360: result = name.substring(0, 1).toLowerCase()
361: + name.substring(1);
362: }
363:
364: return result;
365: }
366:
367: /**
368: * proposes a unique name for the instantiation of a schema variable
369: * (like getProposal(), but somewhat less nicely)
370: * @param basename desired base name, or null to use default
371: * @param sv the schema variable
372: * @param posOfFind the PosInOccurrence containing the name's target program
373: * @param posOfDeclaration the PosInProgram where the name will be declared
374: * (or null to just be pessimistic about the scope)
375: * @param previousProposals list of names which should be considered taken,
376: * or null
377: * @return the name proposal, or null if no proposal is available
378: */
379: protected ProgramElementName getNameProposalForSchemaVariable(
380: String basename, SortedSchemaVariable sv,
381: PosInOccurrence posOfFind, PosInProgram posOfDeclaration,
382: ListOfString previousProposals) {
383: ProgramElementName result = null;
384:
385: Sort svSort = sv.sort();
386: if (svSort == ProgramSVSort.VARIABLE) {
387: if (basename == null || "".equals(basename)) {
388: basename = DEFAULT_BASENAME;
389: }
390: int cnt = getMaxCounterInProgram(basename,
391: getProgramFromPIO(posOfFind), posOfDeclaration) + 1;
392:
393: result = createName(basename, cnt, null);
394:
395: //avoid using a previous proposal again
396: if (previousProposals != null) {
397: boolean collision;
398: do {
399: collision = false;
400: IteratorOfString it = previousProposals.iterator();
401: while (it.hasNext()) {
402: String s = it.next();
403: if (s.equals(result.toString())) {
404: result = createName(basename, ++cnt, null);
405: collision = true;
406: break;
407: }
408: }
409: } while (collision);
410: }
411: }
412:
413: return result;
414: }
415:
416: //-------------------------------------------------------------------------
417: //interface: name proposals
418: //-------------------------------------------------------------------------
419:
420: /**
421: * proposes a unique name; intended for use in places where the information
422: * required by getProposal() is not available
423: * @param basename desired base name, or null to use default
424: * @return the name proposal
425: */
426: public ProgramElementName getTemporaryNameProposal(String basename) {
427: if (basename == null || "".equals(basename)) {
428: basename = DEFAULT_BASENAME;
429: }
430: int cnt = services.getCounter(TEMPCOUNTER_NAME)
431: .getCountPlusPlus(null);
432: //using null as undo anchor should be okay, since the name which the
433: //the counter is used for is only temporary and will be changed
434: //before the variable enters the logic
435:
436: return new TempIndProgramElementName(basename, cnt, null);
437: }
438:
439: /**
440: * proposes a unique name for the instantiation of a schema variable
441: * @param app the taclet app
442: * @param var the schema variable to be instantiated
443: * @param services not used
444: * @param undoAnchor not used
445: * @param previousProposals list of names which should be considered taken,
446: * or null
447: * @return the name proposal, or null if no proposal is available
448: */
449: public String getProposal(TacletApp app, SchemaVariable var,
450: Services services, Node undoAnchor,
451: ListOfString previousProposals) {
452: //determine posOfDeclaration from TacletApp
453: ContextInstantiationEntry cie = app.instantiations()
454: .getContextInstantiation();
455: PosInProgram posOfDeclaration = (cie == null ? null : cie
456: .prefix());
457:
458: //determine a suitable base name
459: String basename = null;
460: NewVarcond nv = app.taclet().varDeclaredNew(var);
461: if (nv != null) {
462: Sort sort = nv.getSort();
463: if (sort != null) {
464: basename = getBaseNameProposal(sort);
465: } else {
466: SchemaVariable psv = nv.getPeerSchemaVariable();
467: Object inst = app.instantiations()
468: .getInstantiation(psv);
469: if (inst instanceof Expression) {
470: final ExecutionContext ec = app.instantiations()
471: .getExecutionContext();
472: if (ec != null) {
473: KeYJavaType kjt = ((Expression) inst)
474: .getKeYJavaType(this .services, ec);
475: basename = getBaseNameProposal(kjt.getSort());
476: } else {
477: // usually this should never be entered, but because of
478: // naming issues we do not want nullpointer exceptions
479: // 'u' for unknown
480: basename = "u";
481: }
482: }
483: }
484: }
485:
486: //get the proposal
487: ProgramElementName name = getNameProposalForSchemaVariable(
488: basename, (SortedSchemaVariable) var, app
489: .posInOccurrence(), posOfDeclaration,
490: previousProposals);
491: return (name == null ? null : name.toString());
492: }
493:
494: //-------------------------------------------------------------------------
495: //interface: uniqueness checking
496: //-------------------------------------------------------------------------
497:
498: /**
499: * tells whether a name for instantiating a schema variable is unique
500: * within its scope
501: * @param name the name to be checked
502: * @param sv the schema variable
503: * @param posOfFind the PosInOccurrence of the name's target program
504: * @param posOfDeclaration the PosInProgram where the name will be declared
505: * @return true if the name is unique or if its uniqueness cannot be
506: * checked, else false
507: */
508: public boolean isUniqueNameForSchemaVariable(String name,
509: SortedSchemaVariable sv, PosInOccurrence posOfFind,
510: PosInProgram posOfDeclaration) {
511: boolean result = true;
512:
513: Sort svSort = sv.sort();
514: if (svSort == ProgramSVSort.VARIABLE) {
515: result = isUniqueInProgram(name,
516: getProgramFromPIO(posOfFind), posOfDeclaration);
517: }
518:
519: return result;
520: }
521:
522: //-------------------------------------------------------------------------
523: //interface: name parsing
524: //-------------------------------------------------------------------------
525:
526: /**
527: * parses the passed string and creates a suitable program element name
528: * (this does *not* make the name unique - if that is necessary, use either
529: * getTemporaryNameProposal() or getProposal())
530: * @param name the name as a string
531: * @param creationInfo optional name creation info the name should carry
532: * @param comments any comments the name should carry
533: * @return the name as a ProgramElementName
534: */
535: public static ProgramElementName parseName(String name,
536: NameCreationInfo creationInfo, Comment[] comments) {
537: ProgramElementName result;
538:
539: int sepPos = name
540: .lastIndexOf(TempIndProgramElementName.SEPARATOR);
541: if (sepPos > 0) {
542: String basename = name.substring(0, sepPos);
543: int index = Integer.parseInt(name.substring(sepPos + 1));
544: result = new TempIndProgramElementName(basename, index,
545: creationInfo, comments);
546: } else {
547: sepPos = name
548: .lastIndexOf(PermIndProgramElementName.SEPARATOR);
549: if (sepPos > 0) {
550: try {
551: String basename = name.substring(0, sepPos);
552: int index = Integer.parseInt(name
553: .substring(sepPos + 1));
554: result = new PermIndProgramElementName(basename,
555: index, creationInfo, comments);
556: } catch (NumberFormatException e) {
557: result = new ProgramElementName(name, creationInfo,
558: comments);
559: }
560: } else {
561: result = new ProgramElementName(name, creationInfo,
562: comments);
563: }
564: }
565:
566: return result;
567: }
568:
569: public static ProgramElementName parseName(String name,
570: NameCreationInfo creationInfo) {
571: return parseName(name, creationInfo, new Comment[0]);
572: }
573:
574: public static ProgramElementName parseName(String name,
575: Comment[] comments) {
576: return parseName(name, null, comments);
577: }
578:
579: public static ProgramElementName parseName(String name) {
580: return parseName(name, null, new Comment[0]);
581: }
582:
583: //-------------------------------------------------------------------------
584: //interface: suggestive name proposals
585: //(taken from VarNameDeliverer.java, pretty much unchanged)
586: //-------------------------------------------------------------------------
587:
588: public static void setSuggestiveEnabled(boolean enabled) {
589: suggestive_off = !enabled;
590: }
591:
592: // precondition: sv.sort()==ProgramSVSort.VARIABLE
593: public String getSuggestiveNameProposalForProgramVariable(
594: SortedSchemaVariable sv, TacletApp app, Goal goal,
595: Services services, ListOfString previousProposals) {
596: if (suggestive_off) {
597: return getProposal(app, sv, services, null,
598: previousProposals);
599: }
600:
601: String proposal;
602: boolean found = false;
603: try {
604: IteratorOfTacletGoalTemplate templs = app.taclet()
605: .goalTemplates().iterator();
606: RewriteTacletGoalTemplate rwgt = null;
607: String name = "";
608: while (templs.hasNext() && !found) {
609: rwgt = (RewriteTacletGoalTemplate) templs.next();
610: Term t = findProgramInTerm(rwgt.replaceWith());
611: ContextStatementBlock c = (ContextStatementBlock) t
612: .executableJavaBlock().program();
613: if (c.getStatementAt(0) instanceof LocalVariableDeclaration) {
614: VariableSpecification v = ((LocalVariableDeclaration) c
615: .getStatementAt(0)).getVariables()
616: .getVariableSpecification(0);
617:
618: if (v.hasInitializer()) {
619: ProgramElement rhs = instantiateExpression(v
620: .getInitializer(),
621: app.instantiations(), services);
622: name = ProofSaver.printProgramElement(rhs);
623: break;
624: } else if (c.getStatementAt(1) instanceof CopyAssignment) {
625: CopyAssignment p2 = (CopyAssignment) c
626: .getStatementAt(1);
627: Expression lhs = p2.getExpressionAt(0);
628: if (lhs.equals(sv)) {
629: SortedSchemaVariable rhs = (SortedSchemaVariable) p2
630: .getExpressionAt(1);
631: name = app.instantiations()
632: .getInstantiation(rhs).toString();
633: break;
634: }
635: }
636: }
637:
638: }
639: if ("".equals(name))
640: throw new Exception();
641: proposal = "[" + name + "]";
642: } catch (Exception e) { // bad style, but this is really non-critical
643: //System.err.println(e);
644: //e.printStackTrace();
645: return getProposal(app, sv, services, null,
646: previousProposals);
647: }
648: return proposal;
649: }
650:
651: public String getSuggestiveNameProposalForSchemaVariable(
652: Expression e) {
653: if (suggestive_off) {
654: return getTemporaryNameProposal(DEFAULT_BASENAME)
655: .toString();
656: }
657: return "[" + ProofSaver.printProgramElement(e) + "]";
658: }
659:
660: private ProgramElement instantiateExpression(ProgramElement e,
661: SVInstantiations svInst, Services services) {
662: ProgramReplaceVisitor trans = new ProgramReplaceVisitor(e,
663: services, svInst, false);
664: trans.start();
665: return trans.result();
666: }
667:
668: //-------------------------------------------------------------------------
669: //inner classes
670: //-------------------------------------------------------------------------
671:
672: /**
673: * ProgramElementName carrying an additional index
674: */
675: private abstract static class IndProgramElementName extends
676: ProgramElementName {
677: private final String basename;
678: private final int index;
679:
680: IndProgramElementName(String name, String basename, int index,
681: NameCreationInfo creationInfo) {
682: super (name, creationInfo);
683: this .basename = basename.intern();
684: this .index = index;
685: }
686:
687: IndProgramElementName(String name, String basename, int index,
688: NameCreationInfo creationInfo, Comment[] comments) {
689: super (name, creationInfo, comments);
690: this .basename = basename.intern();
691: this .index = index;
692: }
693:
694: public String getBaseName() {
695: return basename;
696: }
697:
698: public int getIndex() {
699: return index;
700: }
701: }
702:
703: /**
704: * temporary indexed ProgramElementName
705: */
706: private static class TempIndProgramElementName extends
707: IndProgramElementName {
708: static final char SEPARATOR = '#';
709:
710: TempIndProgramElementName(String basename, int index,
711: NameCreationInfo creationInfo) {
712: super (basename + SEPARATOR + index, basename, index,
713: creationInfo);
714: }
715:
716: TempIndProgramElementName(String basename, int index,
717: NameCreationInfo creationInfo, Comment[] comments) {
718: super (basename + SEPARATOR + index, basename, index,
719: creationInfo, comments);
720: }
721: }
722:
723: /**
724: * regular indexed ProgramElementName
725: */
726: private static class PermIndProgramElementName extends
727: IndProgramElementName {
728: static final char SEPARATOR = '_';
729:
730: PermIndProgramElementName(String basename, int index,
731: NameCreationInfo creationInfo) {
732: super (
733: basename
734: + (index == 0 ? "" : SEPARATOR + "" + index),
735: basename, index, creationInfo);
736: }
737:
738: PermIndProgramElementName(String basename, int index,
739: NameCreationInfo creationInfo, Comment[] comments) {
740: super (
741: basename
742: + (index == 0 ? "" : SEPARATOR + "" + index),
743: basename, index, creationInfo, comments);
744: }
745: }
746:
747: /**
748: * wrapper for global variables coming as a ListOfNamed
749: */
750: private static class GlobalsAsListOfNamed implements Globals {
751: private ListOfNamed globals;
752:
753: public GlobalsAsListOfNamed(ListOfNamed globals) {
754: this .globals = globals;
755: }
756:
757: public IteratorOfProgramElementName iterator() {
758: return new AdapterOfIteratorOfNamed(globals.iterator());
759: }
760: }
761:
762: /**
763: * wrapper for global variables coming as a SetOfProgramVariable
764: */
765: private static class GlobalsAsSetOfProgramVariable implements
766: Globals {
767: private SetOfProgramVariable globals;
768:
769: public GlobalsAsSetOfProgramVariable(
770: SetOfProgramVariable globals) {
771: this .globals = globals;
772: }
773:
774: public IteratorOfProgramElementName iterator() {
775: return new AdapterOfIteratorOfProgramVariable(globals
776: .iterator());
777: }
778: }
779:
780: /**
781: * adapter from IteratorOfNamed to IteratorOfProgramElementName
782: */
783: private static class AdapterOfIteratorOfNamed implements
784: IteratorOfProgramElementName {
785: private IteratorOfNamed it;
786:
787: public AdapterOfIteratorOfNamed(IteratorOfNamed it) {
788: this .it = it;
789: }
790:
791: public boolean hasNext() {
792: return it.hasNext();
793: }
794:
795: public ProgramElementName next() {
796: return (ProgramElementName) (it.next().name());
797: }
798: }
799:
800: /**
801: * adapter from IteratorOfProgramVariable to IteratorOfProgramElementName
802: */
803: private static class AdapterOfIteratorOfProgramVariable implements
804: IteratorOfProgramElementName {
805: private IteratorOfProgramVariable it;
806:
807: public AdapterOfIteratorOfProgramVariable(
808: IteratorOfProgramVariable it) {
809: this .it = it;
810: }
811:
812: public boolean hasNext() {
813: return it.hasNext();
814: }
815:
816: public ProgramElementName next() {
817: return it.next().getProgramElementName();
818: }
819: }
820:
821: /**
822: * a customized JavaASTWalker
823: */
824: private abstract static class CustomJavaASTWalker extends
825: JavaASTWalker {
826: private ProgramElement declarationNode = null;
827: private int declarationScopeDepth = -2;
828: private int currentScopeDepth = -2;
829:
830: CustomJavaASTWalker(ProgramElement program,
831: PosInProgram posOfDeclaration) {
832: super (program);
833: if (posOfDeclaration != null) {
834: declarationNode = PosInProgram.getProgramAt(
835: posOfDeclaration, program);
836: }
837: }
838:
839: protected void walk(ProgramElement node) {
840: //ignore ExecutionContext and ProgramMethod branches;
841: //ignore anything rooted at a depth less or equal than the depth
842: //of the scope containing the declaration (except for this
843: //"declaration scope" itself);
844: if (node instanceof ExecutionContext
845: || node instanceof ProgramMethod) {
846: return;
847: } else if (node instanceof ScopeDefiningElement) {
848: currentScopeDepth = depth();
849: } else if (node == declarationNode) {
850: declarationScopeDepth = currentScopeDepth;
851: } else if (depth() <= declarationScopeDepth) {
852: return;
853: }
854:
855: super .walk(node);
856: }
857: }
858:
859: /**
860: * internal representation for global variables
861: */
862: protected static interface Globals {
863: public IteratorOfProgramElementName iterator();
864: }
865:
866: /**
867: * tuple of a basename and an index
868: */
869: protected static class BasenameAndIndex {
870: public String basename;
871: public int index;
872: }
873: }
|