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;
012:
013: import java.util.HashMap;
014: import java.util.Map;
015:
016: import de.uka.ilkd.key.java.Services;
017: import de.uka.ilkd.key.java.abstraction.KeYJavaType;
018: import de.uka.ilkd.key.logic.op.*;
019: import de.uka.ilkd.key.logic.sort.Sort;
020: import de.uka.ilkd.key.rule.updatesimplifier.Update;
021: import de.uka.ilkd.key.util.Debug;
022:
023: /**
024: * Creates anonymising updates for sets of locations, i.e. (quantified) updates
025: * which assign uninterpreted functions to all locations of such a set.
026: */
027: public class AnonymisingUpdateFactory {
028: private static final TermBuilder TB = TermBuilder.DF;
029: private static final TermFactory TF = TermFactory.DEFAULT;
030: private final UpdateFactory uf;
031:
032: private final Term updateTarget = TB.func(new NonRigidFunction(
033: new Name("x"), Sort.FORMULA, new Sort[0]));
034:
035: public AnonymisingUpdateFactory(UpdateFactory uf) {
036: this .uf = uf;
037: }
038:
039: private static Term[] getSubTerms(Term term) {
040: int arity = term.arity();
041: Term[] result = new Term[arity];
042:
043: for (int i = 0; i < arity; i++) {
044: result[i] = term.sub(i);
045: }
046:
047: return result;
048: }
049:
050: private static Name getNewName(Services services, Name baseName) {
051: NamespaceSet namespaces = services.getNamespaces();
052:
053: int i = 0;
054: Name name;
055: do {
056: name = new Name(baseName + "_" + i++);
057: } while (namespaces.lookup(name) != null);
058:
059: return name;
060: }
061:
062: /**
063: * Determines the arguments sorts of the passed operator
064: * (helper for getUninterpretedFunction()).
065: */
066: private static Sort[] getArgumentSorts(Operator op,
067: Sort[] commonArguments, Services services) {
068: if (op.arity() == 0)
069: return commonArguments;
070:
071: final Sort[] result = new Sort[op.arity()
072: + commonArguments.length];
073: System.arraycopy(commonArguments, 0, result, op.arity(),
074: commonArguments.length);
075:
076: if (op instanceof ProgramVariable) {
077: Debug.assertTrue(op.arity() == 0);
078: } else if (op instanceof AccessOp) {
079: Sort integerSort = services.getTypeConverter()
080: .getIntegerLDT().targetSort();
081:
082: if (op instanceof AttributeOp) {
083: AttributeOp aop = (AttributeOp) op;
084: KeYJavaType kjt = ((ProgramVariable) aop.attribute())
085: .getContainerType();
086: if (services.getJavaInfo().rec2key()
087: .getSuperArrayType() == kjt
088: && "length".equals(aop.attribute().name()
089: .toString())) {
090: result[0] = services.getJavaInfo()
091: .getJavaLangObjectAsSort();
092: } else {
093: result[0] = kjt.getSort();
094: }
095: } else if (op instanceof ArrayOp) {
096: result[0] = ((ArrayOp) op).arraySort();
097: result[1] = integerSort;
098: } else {
099: Debug.fail("Unexpected location operator." + op);
100: }
101:
102: if (((AccessOp) op).isShadowed()) {
103: result[op.arity() - 1] = integerSort;
104: }
105: } else if (op instanceof Function) {
106: Function func = (Function) op;
107: for (int i = 0; i < op.arity(); i++) {
108: result[i] = func.argSort(i);
109: }
110: } else {
111: Debug.fail("Unsupported location operator." + op);
112: }
113:
114: return result;
115: }
116:
117: private static Term[] getArguments(Term locTerm,
118: Term[] commonArguments) {
119: final Operator op = locTerm.op();
120: if (op.arity() == 0)
121: return commonArguments;
122:
123: final Term[] argTerms = new Term[op.arity()
124: + commonArguments.length];
125: System.arraycopy(getSubTerms(locTerm), 0, argTerms, 0, op
126: .arity());
127: System.arraycopy(commonArguments, 0, argTerms, op.arity(),
128: commonArguments.length);
129: return argTerms;
130: }
131:
132: /**
133: * Gets an uninterpreted function for the passed location term
134: * (helper for createUninterpretedFunctions()).
135: */
136: private static RigidFunction getUninterpretedFunction(Term locTerm,
137: Sort[] commonArguments,
138: Map /*Operator -> RigidFunction*/functions,
139: Services services) {
140: RigidFunction result = (RigidFunction) functions.get(locTerm
141: .op());
142:
143: if (result == null) {
144: Name baseName = locTerm.op() instanceof AttributeOp ? ((AttributeOp) locTerm
145: .op()).attribute().name()
146: : locTerm.op() instanceof ArrayOp ? new Name("get")
147: : locTerm.op().name();
148:
149: if (baseName instanceof ProgramElementName) {
150: baseName = new Name(((ProgramElementName) baseName)
151: .getProgramName());
152: }
153:
154: result = new RigidFunction(getNewName(services, baseName),
155: locTerm.sort(), getArgumentSorts(locTerm.op(),
156: commonArguments, services));
157: services.getNamespaces().functions().add(result);
158: functions.put(locTerm.op(), result);
159: }
160:
161: return result;
162: }
163:
164: /**
165: * Creates suitable uninterpreted functions for the passed locations.
166: */
167: public static RigidFunction[] createUninterpretedFunctions(
168: LocationDescriptor[] locations, Sort[] commonArguments,
169: Services services) {
170: RigidFunction[] result = new RigidFunction[locations.length];
171: Map /*Operator -> RigidFunction*/functions = new HashMap();
172:
173: for (int i = 0; i < locations.length; i++) {
174: if (locations[i] instanceof BasicLocationDescriptor) {
175: BasicLocationDescriptor bloc = (BasicLocationDescriptor) locations[i];
176: result[i] = getUninterpretedFunction(bloc.getLocTerm(),
177: commonArguments, functions, services);
178: } else {
179: Debug
180: .assertTrue(
181: locations[i] instanceof EverythingLocationDescriptor
182: && commonArguments.length == 0,
183: "Modifies set {"
184: + locations[i]
185: + "} is not allowed in this situation "
186: + "(could be because of metavariables that have to be given as arguments,"
187: + "which is not supported for the modifier *)");
188: result[i] = null;
189: }
190: }
191:
192: return result;
193: }
194:
195: /**
196: * Creates suitable uninterpreted functions for the passed locations.
197: */
198: public static RigidFunction[] createUninterpretedFunctions(
199: LocationDescriptor[] locations, Services services) {
200: return createUninterpretedFunctions(locations, new Sort[0],
201: services);
202: }
203:
204: /**
205: * Creates the anonymising update for the passed locations using the passed
206: * uninterpreted functions (which must have the correct signature).
207: */
208: public Update createAnonymisingUpdate(
209: LocationDescriptor[] locations, Function[] functions,
210: Services services) {
211: return createAnonymisingUpdate(locations, functions,
212: new Term[0], services);
213: }
214:
215: private Update createAnonymisingUpdate(
216: LocationDescriptor[] locations, Function[] functions,
217: Term[] commonArguments, Services services) {
218: Debug.assertTrue(functions.length == locations.length);
219:
220: Update result = uf.skip();
221:
222: for (int i = 0; i < locations.length; i++) {
223: if (locations[i] instanceof BasicLocationDescriptor) {
224: BasicLocationDescriptor bloc = (BasicLocationDescriptor) locations[i];
225: final Term locTerm = bloc.getLocTerm();
226: final Term guardTerm = createGuard(bloc, services);
227:
228: //create elementary update
229: final Term[] argTerms = getArguments(locTerm,
230: commonArguments);
231:
232: Term valueTerm = TF.createFunctionTerm(functions[i],
233: argTerms);
234: Update elementaryUpdate = uf.elementaryUpdate(locTerm,
235: valueTerm);
236:
237: //create guarded update
238: Update guardedUpdate = uf.guard(guardTerm,
239: elementaryUpdate);
240:
241: //create quantified update
242: Update quantifiedUpdate = guardedUpdate;
243: IteratorOfQuantifiableVariable it = locTerm.freeVars()
244: .iterator();
245: while (it.hasNext()) {
246: quantifiedUpdate = uf.quantify(it.next(),
247: quantifiedUpdate);
248: }
249: //add update to result update
250: result = uf.parallel(result, quantifiedUpdate);
251: } else {
252: Debug
253: .assertTrue(locations[i] instanceof EverythingLocationDescriptor);
254:
255: //create anonym*ous* update
256: AnonymousUpdate ao = AnonymousUpdate
257: .getNewAnonymousOperator();
258: Term updateTerm = TF.createAnonymousUpdateTerm(ao, TF
259: .createJunctorTerm(Op.TRUE));
260: return Update.createUpdate(updateTerm);
261: }
262: }
263:
264: return result;
265: }
266:
267: private Term createGuard(BasicLocationDescriptor bloc,
268: Services services) {
269: final Term locTerm = bloc.getLocTerm();
270: Term guardTerm = bloc.getFormula();
271:
272: //optimisation: for location descriptors of the form
273: //"\for int x; \if(0 <= x & x < a.length) a[x]"
274: //(resulting e.g. from parsing "a[*]"),
275: //we skip the guard in order to simplify the result.
276: if (!(locTerm.op() instanceof ArrayOp && locTerm.sub(1).op() instanceof LogicVariable))
277: return guardTerm;
278:
279: ProgramVariable lengthPV = services.getJavaInfo()
280: .getArrayLength();
281: Function sub = services.getTypeConverter().getIntegerLDT()
282: .getArithSubstraction();
283:
284: Term varTerm = TB.var((LogicVariable) locTerm.sub(1).op());
285: Term lengthTerm = TB.dot(locTerm.sub(0), lengthPV);
286: Term lengthMinusOneTerm = TB.func(sub, lengthTerm, TB
287: .one(services));
288:
289: Term lowerBoundTerm = TB.leq(TB.zero(services), varTerm,
290: services);
291: Term upperBoundTerm1 = TB.lt(varTerm, lengthTerm, services);
292: Term upperBoundTerm2 = TB.leq(varTerm, lengthMinusOneTerm,
293: services);
294: if (guardTerm.equals(TB.and(lowerBoundTerm, upperBoundTerm1))
295: || guardTerm.equals(TB.and(lowerBoundTerm,
296: upperBoundTerm2))) {
297: guardTerm = TB.tt();
298: }
299:
300: return guardTerm;
301: }
302:
303: /**
304: * Creates the anonymising update for the passed locations using new
305: * uninterpreted functions.
306: */
307: public Update createAnonymisingUpdate(
308: SetOfLocationDescriptor locations, Services services) {
309: return createAnonymisingUpdate(locations, new Term[0], services);
310: }
311:
312: public Update createAnonymisingUpdate(
313: SetOfLocationDescriptor locations, Term[] commonArguments,
314: Services services) {
315: LocationDescriptor[] locationsArray = locations.toArray();
316: RigidFunction[] functions = createUninterpretedFunctions(
317: locationsArray, extractSorts(commonArguments), services);
318: return createAnonymisingUpdate(locationsArray, functions,
319: commonArguments, services);
320: }
321:
322: /**
323: * Creates the anonymising update for the passed locations using the passed
324: * uninterpreted functions (which must have the correct signature) and
325: * applies it to the passed target term.
326: */
327: public Term createAnonymisingUpdateTerm(
328: LocationDescriptor[] locations, Function[] functions,
329: Term targetTerm, Services services) {
330: return uf.prepend(createAnonymisingUpdate(locations, functions,
331: services), targetTerm);
332: }
333:
334: /**
335: * Creates the anonymising update for the passed locations using new
336: * uninterpreted functions and applies it to the passed target term.
337: */
338: public Term createAnonymisingUpdateTerm(
339: SetOfLocationDescriptor locations, Term targetTerm,
340: Services services) {
341: LocationDescriptor[] locationsArray = locations.toArray();
342: RigidFunction[] functions = createUninterpretedFunctions(
343: locationsArray, services);
344: return createAnonymisingUpdateTerm(locationsArray, functions,
345: targetTerm, services);
346: }
347:
348: /**
349: * Creates the anonymising update for the passed locations using new
350: * uninterpreted functions and applies it to the passed target term.
351: */
352: public Term createAnonymisingUpdateAsFor(
353: LocationDescriptor[] locationsArray,
354: Term[] commonArguments, Services services) {
355: RigidFunction[] functions = createUninterpretedFunctions(
356: locationsArray, extractSorts(commonArguments), services);
357: Update upd = createAnonymisingUpdate(locationsArray, functions,
358: commonArguments, services);
359: return uf.prepend(upd, updateTarget);
360: }
361:
362: private Sort[] extractSorts(Term[] argTerms) {
363: final Sort[] argSorts = new Sort[argTerms.length];
364: for (int i = 0; i != argTerms.length; ++i)
365: argSorts[i] = argTerms[i].sort();
366: return argSorts;
367: }
368: }
|