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.proof;
012:
013: import java.io.IOException;
014: import java.util.HashMap;
015: import java.util.Map;
016:
017: import de.uka.ilkd.key.collection.ListOfString;
018: import de.uka.ilkd.key.java.*;
019: import de.uka.ilkd.key.java.annotation.Annotation;
020: import de.uka.ilkd.key.java.annotation.LoopInvariantAnnotation;
021: import de.uka.ilkd.key.java.reference.*;
022: import de.uka.ilkd.key.java.statement.LoopStatement;
023: import de.uka.ilkd.key.java.statement.MethodFrame;
024: import de.uka.ilkd.key.java.visitor.JavaASTVisitor;
025: import de.uka.ilkd.key.logic.*;
026: import de.uka.ilkd.key.logic.op.*;
027: import de.uka.ilkd.key.pp.*;
028: import de.uka.ilkd.key.rule.*;
029:
030: public class LoopInvariantProposer implements InstantiationProposer {
031:
032: /**
033: * An instance of LoopInvariantProposer
034: */
035: public static final LoopInvariantProposer DEFAULT = new LoopInvariantProposer();
036:
037: /**
038: * Returns a proposal for the instantiation of <code>var</code>
039: * iff <code>app</code> is a TacletApp for a loop invariant taclet
040: * and <code>var</code> is the SchemaVariable representing the invariant
041: * and the loop on which the taclet matches contains a loop invariant
042: * annotation. Otherwise null is returned.
043: */
044: public String getProposal(TacletApp app, SchemaVariable var,
045: Services services, Node undoAnchor,
046: ListOfString previousProposals) {
047:
048: final Object inst = tryToInstantiate(app, var, services);
049: final LogicPrinter lp = new LogicPrinter(new ProgramPrinter(
050: null), NotationInfo.createInstance(), services);
051: String proposal;
052: try {
053: if (inst instanceof Term) {
054: lp.printTerm((Term) inst);
055: proposal = lp.toString();
056: } else if (inst instanceof ListOfTerm) {
057: lp.printTerm((ListOfTerm) inst);
058: proposal = lp.toString();
059: } else if (inst instanceof SetOfLocationDescriptor) {
060: lp
061: .printLocationDescriptors((SetOfLocationDescriptor) inst);
062: proposal = lp.toString();
063: } else if (var.name().toString().equals("#modifies")) {
064: lp
065: .printLocationDescriptors(SetAsListOfLocationDescriptor.EMPTY_SET
066: .add(EverythingLocationDescriptor.INSTANCE));
067: proposal = lp.toString();
068: } else {
069: proposal = null;
070: }
071: } catch (IOException e) {
072: proposal = null;
073: }
074:
075: return proposal;
076: }
077:
078: /**
079: * returns true if the rulesets contain the rule set loop invariant
080: */
081: public static boolean inLoopInvariantRuleSet(
082: IteratorOfRuleSet ruleSets) {
083: while (ruleSets.hasNext()) {
084: if (ruleSets.next().name().toString().equals(
085: "loop_invariant_proposal")) {
086: return true;
087: }
088: }
089: return false;
090: }
091:
092: private static Term getSelfTerm(Term term, Services services) {
093: final Services serv = services;
094:
095: //ignore updates
096: while (term.op() instanceof IUpdateOperator) {
097: term = term.sub(((IUpdateOperator) term.op()).targetPos());
098: }
099:
100: //the remaining term should contain a program
101: //(because this method is only called for apps of taclets
102: //in "loop_invariant_proposal")
103: final ProgramElement pe = term.javaBlock().program();
104:
105: //fetch "self" from innermost non-static method-frame
106: Term result = new JavaASTVisitor(pe) {
107: private Term result;
108:
109: protected void doAction(ProgramElement node) {
110: node.visit(this );
111: }
112:
113: protected void doDefaultAction(SourceElement node) {
114: if (node instanceof MethodFrame && result == null) {
115: MethodFrame mf = (MethodFrame) node;
116: ExecutionContext ec = (ExecutionContext) mf
117: .getExecutionContext();
118: ReferencePrefix rp = ec.getRuntimeInstance();
119: if (!(rp instanceof TypeReference) && rp != null) {
120: result = serv.getTypeConverter()
121: .convertToLogicElement(rp);
122: }
123: }
124: }
125:
126: public Term run() {
127: walk(pe);
128: return result;
129: }
130: }.run();
131:
132: return result;
133: }
134:
135: /**
136: * Returns an instantiation of <code>var</code>
137: * iff <code>app</code> is a TacletApp for a loop invariant taclet
138: * and <code>var</code> is the SchemaVariable representing the invariant
139: * and the loop on which the taclet matches contains a loop invariant
140: * annotation. Otherwise null is returned.
141: * Depending if the var looked for is a list schemavariable or a normal sv
142: * a list of terms or a term is returned
143: */
144: public Object tryToInstantiate(TacletApp app, SchemaVariable var,
145: Services services) {
146: Object inst = null;
147: if (app instanceof PosTacletApp
148: && inLoopInvariantRuleSet(app.taclet().ruleSets())) {
149: final PosInOccurrence pos = ((PosTacletApp) app)
150: .posInOccurrence();
151: final LoopInvariantAnnotation firstLoopInvAnnot = getFirstLoopInvariantAnnotation(pos
152: .subTerm());
153: if (firstLoopInvAnnot == null) {
154: return null;
155: }
156:
157: //prepare replacing the loop invariant's "self"-variable
158: //by the current "self" term
159: final Term selfTerm = getSelfTerm(pos.subTerm(), services);
160: Map map = new HashMap();
161: map.put(TermBuilder.DF.var(firstLoopInvAnnot.getSelfVar()),
162: selfTerm);
163: OpReplacer or = new OpReplacer(map);
164:
165: //determine instantiation
166: final String varName = var.name().toString();
167: if (varName.equals("inv")
168: && firstLoopInvAnnot.invariant() != null) {
169: inst = or.replace(firstLoopInvAnnot.invariant());
170: } else if (varName.equals("#modifies")
171: && firstLoopInvAnnot.assignable() != null) {
172: inst = or.replace(firstLoopInvAnnot.assignable());
173: } else if (var.name().toString().equals("post")
174: && firstLoopInvAnnot.post() != null) {
175: inst = or.replace(firstLoopInvAnnot.post());
176: } else if (varName.equals("variant")
177: && firstLoopInvAnnot.variant() != null) {
178: inst = or.replace(firstLoopInvAnnot.variant());
179: } else if (varName.equals("#old")) {
180: inst = convertToListOfTerm(firstLoopInvAnnot.olds());
181: }
182: }
183:
184: return inst;
185: }
186:
187: private LoopInvariantAnnotation getFirstLoopInvariantAnnotation(
188: Term t) {
189: final Annotation[] a = getFirstLoopStatement(t)
190: .getAnnotations();
191:
192: for (int i = 0; i < a.length; i++) {
193: if (a[i] instanceof LoopInvariantAnnotation) {
194: return (LoopInvariantAnnotation) a[i];
195: }
196: }
197: return null;
198: }
199:
200: private ListOfTerm convertToListOfTerm(ArrayOfTerm array) {
201: ListOfTerm result = SLListOfTerm.EMPTY_LIST;
202: for (int i = array.size() - 1; i >= 0; i--) {
203: result = result.prepend(array.getTerm(i));
204: }
205: return result;
206: }
207:
208: private LoopStatement getFirstLoopStatement(Term t) {
209: while (t.op() instanceof IUpdateOperator) {
210: t = ((IUpdateOperator) t.op()).target(t);
211: }
212: return getLoopHelp(t.javaBlock().program());
213: }
214:
215: private LoopStatement getLoopHelp(ProgramElement pe) {
216: if (pe instanceof LoopStatement) {
217: return (LoopStatement) pe;
218: }
219: if (pe instanceof StatementContainer) {
220: return getLoopHelp(((StatementContainer) pe)
221: .getStatementAt(0));
222: }
223: //shouldn't happen.
224: return null;
225: }
226: }
|