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: * Created on 16.12.2004
011: */
012: package de.uka.ilkd.key.rule.updatesimplifier;
013:
014: import java.util.ArrayList;
015: import java.util.HashMap;
016: import java.util.HashSet;
017: import java.util.List;
018:
019: import de.uka.ilkd.key.java.Services;
020: import de.uka.ilkd.key.java.visitor.ProgramVariableCollector;
021: import de.uka.ilkd.key.logic.JavaBlock;
022: import de.uka.ilkd.key.logic.ProgramElementName;
023: import de.uka.ilkd.key.logic.Term;
024: import de.uka.ilkd.key.logic.op.*;
025: import de.uka.ilkd.key.rule.AbstractUpdateRule;
026: import de.uka.ilkd.key.rule.UpdateSimplifier;
027: import de.uka.ilkd.key.util.Debug;
028:
029: /**
030: * This simplification rule merges two updates and (optional)
031: * some assignment pairs with no influence on the fromula
032: * are removed
033: */
034: public class ApplyOnModality extends AbstractUpdateRule {
035:
036: /** marker that all program variables have to be protected */
037: private final static Object PROTECT_ALL = new Object();
038:
039: /** marker that all heap locations have to be protected */
040: private final static Object PROTECT_HEAP = new Object();
041:
042: private boolean deletionEnabled;
043:
044: private static HashMap protectedVarsCache = new HashMap();
045:
046: /**
047: * @param updateSimplifier
048: * @param deletionEnabled a boolean flag indictaing if effectless
049: * updates shall be deleted
050: */
051: public ApplyOnModality(UpdateSimplifier updateSimplifier,
052: boolean deletionEnabled) {
053: super (updateSimplifier);
054: this .deletionEnabled = deletionEnabled;
055: }
056:
057: /* (non-Javadoc)
058: * @see de.uka.ilkd.key.rule.IUpdateRule#isApplicable(de.uka.ilkd.key.rule.updatesimplifier.Update, de.uka.ilkd.key.logic.Term)
059: */
060: public boolean isApplicable(Update update, Term target) {
061: return target.op() instanceof Modality;
062: }
063:
064: /*
065: * (non-Javadoc)
066: *
067: * @see de.uka.ilkd.key.rule.IUpdateRule#apply(de.uka.ilkd.key.rule.updatesimplifier.Update,
068: * de.uka.ilkd.key.logic.Term)
069: */
070: public Term apply(Update update, Term target, Services services) {
071:
072: final ArrayOfAssignmentPair pairs = deletionEnabled ? new ArrayOfAssignmentPair(
073: remove(update, target))
074: : update.getAllAssignmentPairs();
075:
076: return pairs.size() == 0 ? target
077: : UpdateSimplifierTermFactory.DEFAULT.createUpdateTerm(
078: pairs, target);
079: }
080:
081: /**
082: * removes assignmentpairs updating locations which are not
083: * used in the tail of the formula
084: * @author bubel
085: */
086: public AssignmentPair[] remove(Update up, Term target) {
087: final ArrayOfAssignmentPair pairs = up.getAllAssignmentPairs();
088: final HashSet protectedProgVars = collectProgramVariables(target);
089: final List result = new ArrayList(pairs.size());
090:
091: for (int i = 0, size = pairs.size(); i < size; i++) {
092: final AssignmentPair pair = pairs.getAssignmentPair(i);
093: final Location loc = pair.location();
094:
095: if (protectedLocation(loc, protectedProgVars))
096: result.add(pair);
097: }
098: return (AssignmentPair[]) result
099: .toArray(new AssignmentPair[result.size()]);
100: }
101:
102: /**
103: * @param loc
104: * @param protectedProgVars
105: * @return
106: */
107: private boolean protectedLocation(Location loc,
108: HashSet protectedProgVars) {
109: // currently it would be safe to comment the PROTECTED_HEAP part out as
110: // heap locations are generally not thrown away. But in principle one can think
111: // of a more finegrained control
112: return protectedProgVars.contains(PROTECT_ALL)
113: || (protectedProgVars.contains(PROTECT_HEAP) && isHeapLocation(loc))
114: || (isHeapLocation(loc)
115: || protectedProgVars.contains(loc) || loc
116: .name().equals(
117: new ProgramElementName(
118: "<transactionCounter>")));
119: }
120:
121: /**
122: * returns true if the location is a heap location, i.e. a static or instance field or
123: * an array operator
124: * @param loc the Location to test
125: * @return true iff the location denotes a heap location
126: */
127: private boolean isHeapLocation(Location loc) {
128: return !(loc instanceof ProgramVariable)
129: || ((ProgramVariable) loc).isMember();
130: }
131:
132: /**
133: * collects all local program variables
134: * @param target
135: * @return
136: */
137: private HashSet collectProgramVariables(Term target) {
138: if (protectedVarsCache.containsKey(target)) {
139: return (HashSet) protectedVarsCache.get(target);
140: }
141: HashSet foundProgVars = new HashSet();
142:
143: final Operator targetOp = target.op();
144:
145: if (targetOp instanceof ProgramVariable) {
146: foundProgVars.add(targetOp);
147: } else if (targetOp instanceof NonRigidHeapDependentFunction) {
148: foundProgVars.add(PROTECT_HEAP);
149: } else if (targetOp == Op.COMPUTE_SPEC_OP
150: || (targetOp instanceof NonRigidFunction && !(targetOp instanceof ProgramMethod))) {
151: foundProgVars.add(PROTECT_ALL);
152: return foundProgVars;
153: }
154:
155: if (target.javaBlock() != JavaBlock.EMPTY_JAVABLOCK) {
156: ProgramVariableCollector pvc = new ProgramVariableCollector(
157: target.javaBlock().program(), true);
158: pvc.start();
159: foundProgVars.addAll(pvc.result());
160: }
161:
162: for (int i = 0; i < target.arity(); i++) {
163: foundProgVars
164: .addAll(collectProgramVariables(target.sub(i)));
165: }
166:
167: if (protectedVarsCache.size() >= 1000) {
168: protectedVarsCache.clear();
169: }
170:
171: protectedVarsCache.put(target, foundProgVars);
172: return foundProgVars;
173: }
174:
175: public Term matchingCondition(Update update, Term target,
176: Services services) {
177: // a modality is not a location
178: Debug
179: .fail("matchingCondition(...) must not be called for target "
180: + target);
181: return null; // unreachable
182: }
183: }
|