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: package de.uka.ilkd.key.rule.metaconstruct;
009:
010: import java.util.*;
011:
012: import de.uka.ilkd.key.java.*;
013: import de.uka.ilkd.key.java.declaration.VariableSpecification;
014: import de.uka.ilkd.key.java.statement.LoopStatement;
015: import de.uka.ilkd.key.java.visitor.JavaASTVisitor;
016: import de.uka.ilkd.key.logic.*;
017: import de.uka.ilkd.key.logic.op.*;
018: import de.uka.ilkd.key.logic.sort.ArrayOfSort;
019: import de.uka.ilkd.key.logic.sort.Sort;
020: import de.uka.ilkd.key.proof.OpReplacer;
021: import de.uka.ilkd.key.rule.MatchConditions;
022: import de.uka.ilkd.key.rule.UpdateSimplifier;
023: import de.uka.ilkd.key.rule.inst.SVInstantiations;
024: import de.uka.ilkd.key.rule.updatesimplifier.Update;
025:
026: public class LocationDependentFunction extends AbstractMetaOperator {
027:
028: private static Term updTerm = null;
029: private static Term heapDepFuncTerm = null;
030:
031: public static Term getHeapDepFuncTermFor(Term term,
032: Services services) {
033: if (term.sub(0) == updTerm) {
034: return heapDepFuncTerm;
035: }
036: updTerm = term.sub(0);
037: ListOfProgramVariable pvs = collectRelevantPVs(term);
038: Term hdf = createHeapDependentFunctionTerm(pvs);
039: services.getNamespaces().functions().add(hdf.op());
040: Map map = AtPreEquations.getAtPreFunctions(updTerm);
041: OpReplacer or = new OpReplacer(map);
042: Term preUpdTerm = or.replace(updTerm);
043: if (!(updTerm.op() instanceof IUpdateOperator))
044: return hdf;
045: final Update upd = Update.createUpdate(preUpdTerm);
046: final UpdateFactory uf = new UpdateFactory(services,
047: new UpdateSimplifier());
048: heapDepFuncTerm = uf.prepend(upd, hdf);
049: return heapDepFuncTerm;
050: }
051:
052: public LocationDependentFunction() {
053: super (new Name("#locDepFunc"), 2);
054: }
055:
056: /* (non-Javadoc)
057: * @see de.uka.ilkd.key.logic.op.MetaOperator#calculate(de.uka.ilkd.key.logic.Term, de.uka.ilkd.key.rule.inst.SVInstantiations, de.uka.ilkd.key.java.Services)
058: */
059: public Term calculate(Term term, SVInstantiations svInst,
060: Services services) {
061: return getHeapDepFuncTermFor(term, services);
062: }
063:
064: private static Term createHeapDependentFunctionTerm(
065: ListOfProgramVariable l) {
066: Term[] subs = new Term[l.size()];
067: Sort[] subSorts = new Sort[l.size()];
068: int i = 0;
069: TermFactory tf = TermFactory.DEFAULT;
070: IteratorOfProgramVariable it = l.iterator();
071: while (it.hasNext()) {
072: ProgramVariable pv = it.next();
073: subs[i] = tf.createVariableTerm(pv);
074: subSorts[i++] = pv.sort();
075: }
076: ArrayOfSort aos = new ArrayOfSort(subSorts);
077: Function anon = new NonRigidHeapDependentFunction(new Name(
078: "anon"), Sort.FORMULA, aos);
079: return tf.createFunctionTerm(anon, subs);
080: }
081:
082: private static ListOfProgramVariable collectRelevantPVs(Term t) {
083: LoopStatement loop = getLoop(t.sub(1).javaBlock().program());
084: FreePVCollector pc = new FreePVCollector(loop);
085: pc.start();
086: return pc.result();
087: }
088:
089: private static LoopStatement getLoop(ProgramElement pe) {
090: if (pe instanceof LoopStatement) {
091: return (LoopStatement) pe;
092: }
093: if (pe instanceof StatementContainer) {
094: return getLoop(((StatementContainer) pe).getStatementAt(0));
095: }
096: //shouldn't happen.
097: return null;
098: }
099:
100: /* (non-Javadoc)
101: * @see de.uka.ilkd.key.logic.op.Operator#validTopLevel(de.uka.ilkd.key.logic.Term)
102: */
103: public boolean validTopLevel(Term term) {
104: return term.arity() == 2 && term.sub(1).sort() == Sort.FORMULA;
105: }
106:
107: /* (non-Javadoc)
108: * @see de.uka.ilkd.key.logic.op.Operator#sort(de.uka.ilkd.key.logic.Term[])
109: */
110: public Sort sort(Term[] term) {
111: return Sort.FORMULA;
112: }
113:
114: /* (non-Javadoc)
115: * @see de.uka.ilkd.key.logic.op.Operator#isRigid(de.uka.ilkd.key.logic.Term)
116: */
117: public boolean isRigid(Term term) {
118: return false;
119: }
120:
121: /** (non-Javadoc)
122: * by default meta operators do not match anything
123: * @see de.uka.ilkd.key.logic.op.Operator#match(SVSubstitute, de.uka.ilkd.key.rule.MatchConditions, de.uka.ilkd.key.java.Services)
124: */
125: public MatchConditions match(SVSubstitute subst,
126: MatchConditions mc, Services services) {
127: return null;
128: }
129:
130: /**
131: * Collects the local program variables which have free occurrences
132: * in a program.
133: */
134: private static class FreePVCollector extends JavaASTVisitor {
135: private ListOfProgramVariable declaredPVs = SLListOfProgramVariable.EMPTY_LIST;
136: private ListOfProgramVariable freePVs = SLListOfProgramVariable.EMPTY_LIST;
137:
138: public FreePVCollector(ProgramElement root) {
139: super (root);
140: }
141:
142: protected void doAction(ProgramElement node) {
143: node.visit(this );
144: }
145:
146: protected void doDefaultAction(SourceElement node) {
147: if (node instanceof ProgramVariable) {
148: ProgramVariable pv = (ProgramVariable) node;
149: if (!pv.isMember() && !declaredPVs.contains(pv)) {
150: freePVs = freePVs.prepend(pv);
151: }
152: } else if (node instanceof VariableSpecification) {
153: VariableSpecification vs = (VariableSpecification) node;
154: ProgramVariable pv = (ProgramVariable) vs
155: .getProgramVariable();
156: if (!pv.isMember()) {
157: assert !declaredPVs.contains(pv);
158: declaredPVs = declaredPVs.prepend(pv);
159:
160: //occurrence in the declaration itself does not count
161: assert freePVs.contains(pv);
162: freePVs = freePVs.removeFirst(pv);
163: }
164: }
165: }
166:
167: public ListOfProgramVariable result() {
168: //remove duplicates
169: ListOfProgramVariable result = SLListOfProgramVariable.EMPTY_LIST;
170: IteratorOfProgramVariable it = freePVs.iterator();
171: while (it.hasNext()) {
172: ProgramVariable pv = it.next();
173: if (!result.contains(pv)) {
174: result = result.prepend(pv);
175: }
176: }
177: return result;
178: }
179: }
180: }
|