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.rule;
012:
013: import de.uka.ilkd.key.java.visitor.ProgramSVCollector;
014: import de.uka.ilkd.key.logic.*;
015: import de.uka.ilkd.key.logic.op.*;
016: import de.uka.ilkd.key.rule.inst.SVInstantiations;
017: import de.uka.ilkd.key.rule.metaconstruct.WhileInvRule;
018: import de.uka.ilkd.key.rule.metaconstruct.WhileInvRuleWrapper;
019:
020: /**
021: * Collects all schemavariables occurring in the
022: * <code>\find, \assumes</code> part or goal description of a taclet.
023: * The addrule section is scanned optionally.
024: *
025: * Duplicates are not removed because the use of persistent
026: * datastructure and up to now we just have a SetAsList-implementaion
027: * causing to have O(sqr(n)) if it would used.
028: *
029: * For example, {@link de.uka.ilkd.key.rule.TacletApp} uses this class
030: * to determine all uninstantiated schemavariables.
031: */
032: public class TacletSchemaVariableCollector extends Visitor {
033:
034: /** collects all found variables */
035: protected ListOfSchemaVariable varList;
036: /** the instantiations needed for unwind loop constructs */
037: private SVInstantiations instantiations = SVInstantiations.EMPTY_SVINSTANTIATIONS;
038:
039: /** creates the Variable collector.
040: */
041: public TacletSchemaVariableCollector() {
042: varList = SLListOfSchemaVariable.EMPTY_LIST;
043: }
044:
045: /** creates the Variable collector.
046: * @param svInsts the SVInstantiations that have been already found
047: * (needed by unwind loop constructs to determine which labels are needed)
048: */
049: public TacletSchemaVariableCollector(SVInstantiations svInsts) {
050: varList = SLListOfSchemaVariable.EMPTY_LIST;
051: instantiations = svInsts;
052: }
053:
054: /** collects all SchemVariables that occur in the JavaBlock
055: * @param jb the JavaBlock where to look for Schemavariables
056: * @param vars the ListOfSchemaVariable where to add the found
057: * SchemaVariables
058: * @return the extended list of found schemavariables
059: */
060: protected ListOfSchemaVariable collectSVInProgram(JavaBlock jb,
061: ListOfSchemaVariable vars) {
062:
063: ProgramSVCollector prgSVColl = new ProgramSVCollector(jb
064: .program(), vars, instantiations);
065: prgSVColl.start();
066: return prgSVColl.getSchemaVariables();
067: }
068:
069: private ListOfSchemaVariable collectSVInProgram(Term t,
070: ListOfSchemaVariable vars) {
071:
072: ProgramSVCollector prgSVColl = new ProgramSVCollector(
073: new WhileInvRuleWrapper(t), vars, instantiations);
074: prgSVColl.start();
075: return prgSVColl.getSchemaVariables();
076: }
077:
078: private ListOfSchemaVariable collectSVInAttributeOp(AttributeOp op) {
079: ListOfSchemaVariable result = SLListOfSchemaVariable.EMPTY_LIST;
080: final IProgramVariable attribute = op.attribute();
081: if (attribute instanceof SchemaVariable) {
082: result = result.prepend((SchemaVariable) attribute);
083: }
084: return result;
085: }
086:
087: /**
088: * visits the Term in post order {@link Term#execPostOrder(Visitor)} and
089: * collects all found schema variables
090: * @param t the Term whose schema variables are collected
091: */
092: public void visit(Term t) {
093: final Operator op = t.op();
094: if (op instanceof Modality || op instanceof ModalOperatorSV) {
095: varList = collectSVInProgram(t.javaBlock(), varList);
096: } else if (op instanceof AttributeOp) {
097: varList = varList
098: .prepend(collectSVInAttributeOp((AttributeOp) op));
099: } else if (op instanceof QuanUpdateOperator) {
100: varList = collectSVInQuanUpdateOperator(op, varList);
101: } else if (op instanceof WhileInvRule) {
102: varList = collectSVInProgram(t, varList);
103: }
104:
105: for (int j = 0, ar = t.arity(); j < ar; j++) {
106: for (int i = 0, sz = t.varsBoundHere(j).size(); i < sz; i++) {
107: final QuantifiableVariable qVar = t.varsBoundHere(j)
108: .getQuantifiableVariable(i);
109: if (qVar instanceof SchemaVariable) {
110: varList = varList.prepend((SchemaVariable) qVar);
111: }
112: }
113: }
114:
115: if (op instanceof SchemaVariable) {
116: varList = varList.prepend((SchemaVariable) op);
117: }
118: }
119:
120: /**
121: * collects all schema variables occurring as part of a quantified update
122: * operator
123: * @param op the {@link QuanUpdateOperator} to be scanned for schemavariables
124: * @param vars the ListOfSchemaVariables with already found schema variables
125: * @return a list of schema variables containing the ones of <code>vars</code>
126: * together with the schema variables found in <code>op</code>
127: */
128: private ListOfSchemaVariable collectSVInQuanUpdateOperator(
129: final Operator op, ListOfSchemaVariable vars) {
130: ListOfSchemaVariable result = vars;
131: final QuanUpdateOperator quan = (QuanUpdateOperator) op;
132: for (int i = 0, locCount = quan.locationCount(); i < locCount; i++) {
133: final Location currentLocation = quan.location(i);
134: if (currentLocation instanceof SchemaVariable) {
135: result = result
136: .prepend((SchemaVariable) currentLocation);
137: } else if (currentLocation instanceof AttributeOp) {
138: result = result
139: .prepend(collectSVInAttributeOp((AttributeOp) currentLocation));
140: }
141: }
142: return result;
143: }
144:
145: /** @return iterator of the found Variables */
146: public IteratorOfSchemaVariable varIterator() {
147: return varList.iterator();
148: }
149:
150: /** @return number of the found variables */
151: public int size() {
152: return varList.size();
153: }
154:
155: /** @return true iff term contains the given variable */
156: public boolean contains(SchemaVariable var) {
157: return varList.contains(var);
158: }
159:
160: /** collects all variables in a Semisequent
161: * @param semiseq the Semisequent to visit
162: */
163: private void visit(Semisequent semiseq) {
164: IteratorOfConstrainedFormula it = semiseq.iterator();
165: while (it.hasNext()) {
166: it.next().formula().execPostOrder(this );
167: }
168: }
169:
170: /** goes through the given sequent an collects all vars found
171: * @param seq the Sequent to visit
172: */
173: public void visit(Sequent seq) {
174: visit(seq.antecedent());
175: visit(seq.succedent());
176: }
177:
178: /**
179: * collects all schema variables of a taclet
180: * @param taclet the Taclet where the variables have to be collected to
181: * @param visitAddrules a boolean that contols if the addrule sections are
182: * to be ignored (iff false) or if the visitor descends into them (iff true)
183: */
184: public void visit(Taclet taclet, boolean visitAddrules) {
185: visit(taclet.ifSequent());
186: visitFindPart(taclet);
187: visitGoalTemplates(taclet, visitAddrules);
188: }
189:
190: protected void visitFindPart(Taclet taclet) {
191: if (taclet instanceof FindTaclet) {
192: (((FindTaclet) taclet).find()).execPostOrder(this );
193: }
194: }
195:
196: protected void visitGoalTemplates(Taclet taclet,
197: boolean visitAddrules) {
198: IteratorOfTacletGoalTemplate it = taclet.goalTemplates()
199: .iterator();
200: while (it.hasNext()) {
201: TacletGoalTemplate gt = it.next();
202: visit(gt.sequent());
203: if (gt instanceof RewriteTacletGoalTemplate) {
204: ((RewriteTacletGoalTemplate) gt).replaceWith()
205: .execPostOrder(this );
206: } else {
207: if (gt instanceof AntecSuccTacletGoalTemplate) {
208: visit(((AntecSuccTacletGoalTemplate) gt)
209: .replaceWith());
210: }
211: }
212: if (visitAddrules) {
213: IteratorOfTaclet addruleIt = gt.rules().iterator();
214: while (addruleIt.hasNext()) {
215: visit(addruleIt.next(), true);
216: }
217: }
218: }
219: }
220:
221: /** collects all variables in a Taclet but ignores the variables that appear
222: * only in the addrule sections of the Taclet
223: * @param taclet the Taclet where the variables have to be collected to
224: */
225: public void visitWithoutAddrule(Taclet taclet) {
226: visit(taclet, false);
227: // varList = varList.prepend(taclet.addedRuleNameVars());
228: }
229:
230: }
|