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.logic.op;
012:
013: import java.io.IOException;
014:
015: import de.uka.ilkd.key.java.*;
016: import de.uka.ilkd.key.java.abstraction.KeYJavaType;
017: import de.uka.ilkd.key.java.annotation.Annotation;
018: import de.uka.ilkd.key.java.reference.ExecutionContext;
019: import de.uka.ilkd.key.java.reference.PackageReference;
020: import de.uka.ilkd.key.java.reference.ReferencePrefix;
021: import de.uka.ilkd.key.java.reference.TypeReference;
022: import de.uka.ilkd.key.java.visitor.Visitor;
023: import de.uka.ilkd.key.logic.Name;
024: import de.uka.ilkd.key.logic.ProgramConstruct;
025: import de.uka.ilkd.key.logic.ProgramElementName;
026: import de.uka.ilkd.key.logic.Term;
027: import de.uka.ilkd.key.logic.sort.ProgramSVSort;
028: import de.uka.ilkd.key.rule.MatchConditions;
029: import de.uka.ilkd.key.rule.inst.ProgramList;
030: import de.uka.ilkd.key.rule.inst.SVInstantiations;
031: import de.uka.ilkd.key.util.Debug;
032:
033: public class ProgramSV extends SortedSchemaVariable implements
034: ProgramConstruct, Location {
035:
036: private static final ProgramList EMPTY_LIST_INSTANTIATION = new ProgramList(
037: new ArrayOfProgramElement(new ProgramElement[0]));
038:
039: /**
040: * creates a new SchemaVariable used as a placeholder for program
041: * constructs
042: * @param name the Name of the SchemaVariable
043: * @param listSV a boolean which is true iff the schemavariable is
044: * allowed to match a list of program constructs
045: */
046: ProgramSV(Name name, ProgramSVSort s, boolean listSV) {
047: super (name, ProgramConstruct.class, s, listSV);
048: }
049:
050: /** returns true iff this SchemaVariable is used to match
051: * part of a program
052: * @return true iff this SchemaVariable is used to match
053: * part of a program
054: */
055: public boolean isProgramSV() {
056: return true;
057: }
058:
059: /** @return comments if the schemavariable stands for programm
060: * construct and has comments attached to it (not supported yet)
061: */
062: public Comment[] getComments() {
063: return new Comment[0];
064: }
065:
066: public SourceElement getFirstElement() {
067: return this ;
068: }
069:
070: public SourceElement getLastElement() {
071: return this ;
072: }
073:
074: /**
075: *@return the annotations.
076: */
077: public Annotation[] getAnnotations() {
078: return new Annotation[0];
079: }
080:
081: public int getAnnotationCount() {
082: return 0;
083: }
084:
085: /**
086: * Returns the start position of the primary token of this element.
087: * To get the start position of the syntactical first token,
088: * call the corresponding method of <CODE>getFirstElement()</CODE>.
089: * @return the start position of the primary token.
090: */
091: public Position getStartPosition() {
092: return Position.UNDEFINED;
093: }
094:
095: /**
096: * Returns the end position of the primary token of this element.
097: * To get the end position of the syntactical first token,
098: * call the corresponding method of <CODE>getLastElement()</CODE>.
099: * @return the end position of the primary token.
100: */
101: public Position getEndPosition() {
102: return Position.UNDEFINED;
103: }
104:
105: /**
106: * Returns the relative position (number of blank heading lines and
107: * columns) of the primary token of this element.
108: * To get the relative position of the syntactical first token,
109: * call the corresponding method of <CODE>getFirstElement()</CODE>.
110: * @return the relative position of the primary token.
111: */
112: public Position getRelativePosition() {
113: return Position.UNDEFINED;
114: }
115:
116: public PositionInfo getPositionInfo() {
117: return PositionInfo.UNDEFINED;
118: }
119:
120: public ReferencePrefix getReferencePrefix() {
121: return null;
122: }
123:
124: public ReferencePrefix setReferencePrefix(ReferencePrefix r) {
125: return this ;
126: }
127:
128: public int getDimensions() {
129: return 0;
130: }
131:
132: public int getTypeReferenceCount() {
133: return 0;
134: }
135:
136: public TypeReference getTypeReferenceAt(int index) {
137: return this ;
138: }
139:
140: public PackageReference getPackageReference() {
141: return null;
142: }
143:
144: public int getExpressionCount() {
145: return 0;
146: }
147:
148: public Expression getExpressionAt(int index) {
149: return null;
150: }
151:
152: public int getChildCount() {
153: return 0;
154: }
155:
156: public ProgramElement getChildAt(int index) {
157: return this ;
158: }
159:
160: public int getStatementCount() {
161: return 0;
162: }
163:
164: public int size() {
165: return 0;
166: }
167:
168: public ArrayOfExpression getUpdates() {
169: return null;
170: }
171:
172: public ArrayOfLoopInitializer getInits() {
173: return null;
174: }
175:
176: public Statement getStatementAt(int i) {
177: return this ;
178: }
179:
180: public ProgramElementName getProgramElementName() {
181: return new ProgramElementName(toString());
182: }
183:
184: public String getName() {
185: return name().toString();
186: }
187:
188: /** calls the corresponding method of a visitor in order to
189: * perform some action/transformation on this element
190: * @param v the Visitor
191: */
192: public void visit(Visitor v) {
193: v.performActionOnSchemaVariable(this );
194: }
195:
196: /** this pretty printer method is for the program pretty printer
197: * and needs not to be overwritten by ProgramSV but at the moment
198: * it is not
199: */
200: public void prettyPrint(PrettyPrinter w) throws IOException {
201: w.printSchemaVariable(this );
202: }
203:
204: public KeYJavaType getKeYJavaType() {
205: return null;
206: }
207:
208: public KeYJavaType getKeYJavaType(Services javaServ) {
209: return null;
210: }
211:
212: public KeYJavaType getKeYJavaType(Services javaServ,
213: ExecutionContext ec) {
214: return null;
215: }
216:
217: /* (non-Javadoc)
218: * @see de.uka.ilkd.key.logic.op.Operator#match(de.uka.ilkd.key.logic.op.Operator, de.uka.ilkd.key.rule.MatchConditions, de.uka.ilkd.key.java.Services)
219: */
220: public MatchConditions match(SVSubstitute substitute,
221: MatchConditions mc, Services services) {
222:
223: final ProgramSVSort svSort = (ProgramSVSort) sort();
224:
225: if (substitute instanceof Term
226: && svSort.canStandFor((Term) substitute)) {
227: return addInstantiation((Term) substitute, mc, services);
228: } else if (substitute instanceof ProgramElement
229: && svSort.canStandFor((ProgramElement) substitute, mc
230: .getInstantiations().getExecutionContext(),
231: services)) {
232: return addInstantiation((ProgramElement) substitute, mc,
233: services);
234: }
235: Debug.out("FAILED. Cannot match ProgramSV with given "
236: + "instantiation(template, orig)", this , substitute);
237: return null;
238: }
239:
240: /** toString */
241: public String toString() {
242: return toString("program " + sort().name());
243: }
244:
245: /**
246: * adds a found mapping from schema variable <code>var</code> to
247: * program element <code>pe</code> and returns the updated match
248: * conditions or null if mapping is not possible because of
249: * violating some variable condition
250: * @param pe the ProgramElement <code>var</code> is mapped to
251: * @param matchCond the MatchConditions to be updated
252: * @param services the Services provide access to the Java model
253: x * @return the updated match conditions including mapping
254: * <code>var</code> to <code>pe</code> or null if some variable
255: * condition would be hurt by the mapping
256: */
257: private MatchConditions addProgramInstantiation(ProgramElement pe,
258: MatchConditions matchCond, Services services) {
259: if (matchCond == null) {
260: return null;
261: }
262:
263: SVInstantiations insts = matchCond.getInstantiations();
264:
265: final Object foundInst = insts.getInstantiation(this );
266:
267: if (foundInst != null) {
268: final Object newInst;
269: if (foundInst instanceof Term) {
270: newInst = services.getTypeConverter()
271: .convertToLogicElement(pe,
272: insts.getExecutionContext());
273: } else {
274: newInst = pe;
275: }
276:
277: if (foundInst.equals(newInst)) {
278: return matchCond;
279: } else {
280: return null;
281: }
282: }
283:
284: insts = insts.add(this , pe);
285: return insts == null ? null : matchCond
286: .setInstantiations(insts);
287: }
288:
289: /**
290: * adds a found mapping from schema variable <code>var</code> to the
291: * list of program elements <code>list</code> and returns the updated
292: * match conditions or null if mapping is not possible because of
293: * violating some variable condition
294: * @param list the ProgramList <code>var</code> is mapped to
295: * @param matchCond the MatchConditions to be updated
296: * @param services the Services provide access to the Java model
297: * @return the updated match conditions including mapping
298: * <code>var</code> to <code>list</code> or null if some variable
299: * condition would be hurt by the mapping
300: */
301: private MatchConditions addProgramInstantiation(ProgramList list,
302: MatchConditions matchCond, Services services) {
303: if (matchCond == null) {
304: return null;
305: }
306:
307: SVInstantiations insts = matchCond.getInstantiations();
308: final ProgramList pl = (ProgramList) insts
309: .getInstantiation(this );
310: if (pl != null) {
311: if (pl.equals(list)) {
312: return matchCond;
313: } else {
314: return null;
315: }
316: }
317:
318: insts = insts.add(this , list);
319: return insts == null ? null : matchCond
320: .setInstantiations(insts);
321: }
322:
323: /**
324: * returns true, if the given SchemaVariable can stand for the
325: * ProgramElement
326: * @param match the ProgramElement to be matched
327: * @param services the Services object encapsulating information
328: * about the java datastructures like (static)types etc.
329: * @return true if the SchemaVariable can stand for the given element
330: */
331: private boolean check(ProgramElement match, ExecutionContext ec,
332: Services services) {
333: if (match == null) {
334: return false;
335: }
336: return ((ProgramSVSort) sort())
337: .canStandFor(match, ec, services);
338: }
339:
340: /**
341: *
342: */
343: public MatchConditions match(SourceData source,
344: MatchConditions matchCond) {
345: if (isListSV()) {
346: return matchListSV(source, matchCond);
347: }
348: final Services services = source.getServices();
349: final ProgramElement src = source.getSource();
350: Debug.out("Program match start (template, source)", this , src);
351:
352: final SVInstantiations instantiations = matchCond
353: .getInstantiations();
354:
355: final ExecutionContext ec = instantiations
356: .getExecutionContext();
357:
358: if (!check(src, ec, services)) {
359: Debug
360: .out("taclet: MATCH FAILED. Sort of SchemaVariable cannot "
361: + "stand for the program");
362: return null; //FAILED
363: }
364:
365: final Object instant = instantiations.getInstantiation(this );
366: if (instant == null
367: || instant.equals(src)
368: || (instant instanceof Term && ((Term) instant).op()
369: .equals(src))) {
370:
371: matchCond = addProgramInstantiation(src, matchCond,
372: services);
373:
374: if (matchCond == null) {
375: // FAILED due to incompatibility with already found matchings
376: // (e.g. generic sorts)
377: return null;
378: }
379: } else {
380: Debug.out("taclet: MATCH FAILED 3. Former match of "
381: + " SchemaVariable incompatible with "
382: + " the current match.");
383: return null; //FAILED mismatch
384: }
385: source.next();
386: return matchCond;
387: }
388:
389: private MatchConditions matchListSV(SourceData source,
390: MatchConditions matchCond) {
391: final Services services = source.getServices();
392: ProgramElement src = source.getSource();
393:
394: if (src == null) {
395: return addProgramInstantiation(EMPTY_LIST_INSTANTIATION,
396: matchCond, services);
397: }
398:
399: SVInstantiations instantiations = matchCond.getInstantiations();
400:
401: final ExecutionContext ec = instantiations
402: .getExecutionContext();
403:
404: final java.util.ArrayList matchedElements = new java.util.ArrayList();
405:
406: while (src != null) {
407: if (!check(src, ec, services)) {
408: Debug.out("taclet: Stopped list matching because of "
409: + "incompatible elements", this , src);
410: break;
411: }
412: matchedElements.add(src);
413: source.next();
414: src = source.getSource();
415: }
416:
417: Debug.out("Program list match: ", this , matchedElements);
418: return addProgramInstantiation(new ProgramList(
419: new ArrayOfProgramElement(matchedElements)), matchCond,
420: services);
421: }
422: }
|