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.unittest.simplify;
009:
010: import de.uka.ilkd.key.proof.decproc.*;
011: import de.uka.ilkd.key.unittest.simplify.ast.*;
012: import de.uka.ilkd.key.unittest.*;
013: import de.uka.ilkd.key.java.Services;
014: import de.uka.ilkd.key.collection.*;
015: import de.uka.ilkd.key.util.ExtList;
016: import de.uka.ilkd.key.parser.simplify.*;
017: import de.uka.ilkd.key.logic.*;
018:
019: import java.io.StringReader;
020: import java.util.*;
021:
022: public class SimplifyModelGenerator implements DecProdModelGenerator {
023:
024: private Services serv;
025: private HashMap string2class;
026: private HashMap term2class;
027: private HashSet intClasses;
028: private String initialCounterExample;
029: // first element has to be 0. Only positive values at even indices.
030: public static int modelLimit = 1;
031: private static final int[] genericTestValues = new int[] { 0, -1,
032: 1, -10, 10, -1000, 1000, -1000000, 1000000, -2000000000,
033: 2000000000 };
034: // Outputs of Simplify are stored in order to prevent Simplify
035: // from being called several times with the same formula -> saves execution
036: // time
037: private HashSet simplifyOutputs;
038: private ListOfString placeHoldersForClasses = SLListOfString.EMPTY_LIST;
039:
040: public SimplifyModelGenerator(DecisionProcedureSimplify dps,
041: Services serv, HashMap term2class, SetOfTerm locations) {
042:
043: this .serv = serv;
044: this .term2class = term2class;
045:
046: DecisionProcedureResult res = dps.run(true);
047: initialCounterExample = res.getText();
048: this .simplifyOutputs = new HashSet();
049: string2class = new HashMap();
050: IteratorOfTerm it = locations.iterator();
051: Vector v = new Vector();
052: SimplifyTranslation st = (SimplifyTranslation) res
053: .getTranslation();
054: try {
055: while (it.hasNext()) {
056: de.uka.ilkd.key.logic.Term t = it.next();
057: String s = st.translate(t, v).toString();
058: string2class.put(s, term2class.get(t));
059: }
060: } catch (SimplifyException e) {
061: System.err.println(e);
062: }
063: intClasses = new HashSet();
064: Iterator itc = term2class.values().iterator();
065: int index = initialCounterExample.indexOf("AND") + 4;
066: while (itc.hasNext() && index != 3) {
067: EquivalenceClass ec = (EquivalenceClass) itc.next();
068: try {
069: if (ec.isInt() && ec.getLocations().size() != 0
070: && !intClasses.contains(ec)) {
071: String ph = "(_placeHolder_" + intClasses.size()
072: + ")";
073: string2class.put(ph, ec);
074: placeHoldersForClasses = placeHoldersForClasses
075: .append(ph);
076: intClasses.add(ec);
077: de.uka.ilkd.key.logic.Term loc = ec.getLocations()
078: .iterator().next();
079: String eq = "(EQ " + ph + " "
080: + st.translate(loc, v) + ")\n";
081: initialCounterExample = initialCounterExample
082: .substring(0, index)
083: + eq
084: + initialCounterExample.substring(index);
085: }
086: } catch (SimplifyException e) {
087: System.err.println(e);
088: }
089: }
090: }
091:
092: public Set createModels() {
093: HashSet models = new HashSet();
094: int datCount = 1;
095: while (models.size() < modelLimit
096: && datCount <= genericTestValues.length) {
097: models.addAll(createModelsHelp(initialCounterExample,
098: new Model(term2class), datCount++));
099: simplifyOutputs.clear();
100: }
101: return models;
102: }
103:
104: public Set createModelsHelp(String counterEx, Model model,
105: int datCount) {
106: Set models = new HashSet();
107: if (counterEx.indexOf("Counterexample") == -1
108: || models.size() >= modelLimit) {
109: return models;
110: }
111: counterEx = counterEx.replaceAll("_ ", "_");
112: counterEx = removeIrrelevantSubformulas(counterEx);
113: if (simplifyOutputs.contains(counterEx)) {
114: ModelGenerator.cached++;
115: return models;
116: }
117: StringReader stream = new StringReader(counterEx);
118: SimplifyParser parser = new SimplifyParser(new SimplifyLexer(
119: stream), serv);
120: Conjunction c = null;
121: try {
122: c = parser.top();
123: } catch (Exception e) {
124: throw new RuntimeException(e);
125: }
126: removeNegativeArrayIndices(c);
127: Equation[] eqs = c.getEquations();
128: if (eqs.length == c.arity()) {
129: for (int i = 0; i < eqs.length; i++) {
130: de.uka.ilkd.key.unittest.simplify.ast.Term ft = eqs[i]
131: .sub(0);
132: EquivalenceClass ec = getEqvClass(ft);
133: if (ec != null && ec.getLocations().size() > 0
134: && eqs[i].sub(1) instanceof NumberTerm) {
135: model.setValue(ec, ((NumberTerm) eqs[i].sub(1))
136: .getValue());
137: }
138: }
139: if (model.size() == intClasses.size()) {
140: models.add(model);
141: } else {
142: for (int i = 0; i < eqs.length; i++) {
143: //set a subterm to an arbitrary value an test if
144: //the system of equations has a unique solution now.
145: for (int j = 0; j < datCount; j++) {
146: Equation e = createEquationForSubTerm(eqs[i],
147: genericTestValues[j]);
148: if (e != null) {
149: c.add(e);
150: models.addAll(createModelsHelp(simplify(c),
151: model.copy(), datCount));
152: if (models.size() >= modelLimit) {
153: return models;
154: }
155: c.removeLast();
156: }
157: }
158: }
159: }
160: } else {
161: LessEq[] leqs = c.getLessEq();
162: for (int i = 0; i < leqs.length; i++) {
163: for (int j = 0; j < datCount; j += 2) {
164: c.add(lessEqToEq(leqs[i], genericTestValues[j]));
165: models.addAll(createModelsHelp(simplify(c), model
166: .copy(), datCount));
167: if (models.size() >= modelLimit) {
168: return models;
169: }
170: c.removeLast();
171: }
172: }
173: Less[] les = c.getLess();
174: for (int i = 0; i < les.length; i++) {
175: for (int j = 2; j < datCount; j += 2) {
176: c.add(lessToEq(les[i], genericTestValues[j]));
177: models.addAll(createModelsHelp(simplify(c), model
178: .copy(), datCount));
179: if (models.size() >= modelLimit) {
180: return models;
181: }
182: c.removeLast();
183: }
184: }
185: Inequation[] neq = c.getInequations();
186: for (int i = 0; i < neq.length; i++) {
187: for (int j = 1; j < datCount; j++) {
188: c.add(ineqToEq(neq[i], genericTestValues[j]));
189: models.addAll(createModelsHelp(simplify(c), model
190: .copy(), datCount));
191: if (models.size() >= modelLimit) {
192: return models;
193: }
194: c.removeLast();
195: }
196: }
197: }
198: return models;
199: }
200:
201: private String simplify(Conjunction c) {
202: try {
203: return DecisionProcedureSimplify.execute("(NOT "
204: + c.toSimplify() + ")");
205: } catch (Exception e) {
206: throw new RuntimeException(e);
207: }
208: }
209:
210: private Equation createEquationForSubTerm(Equation eq, int x) {
211: Equation e = null;
212: for (int j = 0; j < 2; j++) {
213: if (!(eq.sub(1) instanceof NumberTerm)
214: && !(eq.sub(0) instanceof NumberTerm)) {
215: e = createEquationForSubTermHelp(eq, x);
216: } else {
217: e = createEquationForSubTermHelp(eq.sub(0), x);
218: if (e == null) {
219: e = createEquationForSubTermHelp(eq.sub(1), x);
220: }
221: }
222: if (e != null) {
223: return e;
224: }
225: }
226: return e;
227: }
228:
229: private void removeNegativeArrayIndices(Conjunction c) {
230: for (int i = 0; i < c.arity();) {
231: if (containsNegativeIndex(c.sub(i))) {
232: c.remove(c.sub(i));
233: } else {
234: i++;
235: }
236: }
237: }
238:
239: private boolean containsNegativeIndex(
240: de.uka.ilkd.key.unittest.simplify.ast.Term t) {
241: if (t.op().equals("ArrayOp")) {
242: if ((t.sub(1) instanceof NumberTerm)
243: && ((NumberTerm) t.sub(1)).getValue() < 0) {
244: return true;
245: }
246: }
247: for (int i = 0; i < t.arity(); i++) {
248: if (containsNegativeIndex(t.sub(i))) {
249: return true;
250: }
251: }
252: return false;
253: }
254:
255: private Equation createEquationForSubTermHelp(
256: de.uka.ilkd.key.unittest.simplify.ast.Term t, int x) {
257: for (int i = 0; i < t.arity(); i++) {
258: if ((t.sub(i) instanceof FunctionTerm)
259: && (((FunctionTerm) t.sub(i)).isArithmetic() || getEqvClass(t
260: .sub(i)) != null
261: && getEqvClass(t.sub(i)).isInt())) {
262: return new Equation(t.sub(i), new NumberTerm(x));
263: }
264: Equation e = createEquationForSubTermHelp(t.sub(i), x);
265: if (e != null) {
266: return e;
267: }
268: }
269: return null;
270: }
271:
272: private EquivalenceClass getEqvClass(
273: de.uka.ilkd.key.unittest.simplify.ast.Term t) {
274: if (t instanceof FunctionTerm) {
275: return (EquivalenceClass) string2class.get(t.toString());
276: }
277: return null;
278: }
279:
280: /**
281: * Removes uninterpreted predicatesand extracts the formula provided by
282: * Simplify.
283: */
284: private String removeIrrelevantSubformulas(String s) {
285: int index = s.indexOf("(AND");
286: index = s.indexOf("(", index + 1);
287: String result = "(AND ";
288: while (index < s.length() - 1 && index != -1) {
289: String op = s.substring(index + 1, index + 4);
290: if ((op.startsWith("<=") || op.startsWith("<")
291: || op.startsWith("EQ") || op.startsWith("NEQ"))
292: && s.substring(index, s.indexOf("\n", index) + 1)
293: .indexOf("_undef") == -1
294: && s.substring(index, s.indexOf("\n", index) + 1)
295: .indexOf("(null_") == -1
296: && s.substring(index + 4,
297: s.indexOf("\n", index) + 1).indexOf("<") == -1) {
298: result += " "
299: + s
300: .substring(index, s
301: .indexOf("\n", index) + 1);
302: }
303: index = s.indexOf("\n", index);
304: if (index == -1)
305: break;
306: index = s.indexOf("(", index + 1);
307: }
308: result += ")";
309: return result;
310: }
311:
312: private Equation lessEqToEq(LessEq t, int i) {
313: Equation eq = new Equation();
314: eq.setLeft(plus(t.sub(0), i));
315: eq.setRight(t.sub(1));
316: return eq;
317: }
318:
319: /**
320: * @param t term of the form a<b.
321: * @return a+i=b
322: */
323: private Equation lessToEq(Less t, int i) {
324: if (i < 0) {
325: i = -i;
326: }
327: Equation eq = new Equation();
328: eq.setLeft(plus(t.sub(0), i));
329: eq.setRight(t.sub(1));
330: return eq;
331: }
332:
333: private de.uka.ilkd.key.unittest.simplify.ast.Term plus(
334: de.uka.ilkd.key.unittest.simplify.ast.Term t, int i) {
335: if (i == 0) {
336: return t;
337: }
338: ExtList l = new ExtList();
339: l.add(t);
340: l.add(new NumberTerm(i));
341: return new FunctionTerm(
342: de.uka.ilkd.key.unittest.simplify.ast.Function.PLUS, l);
343: }
344:
345: private Equation ineqToEq(Inequation t, int i) {
346: Equation eq = new Equation();
347: eq.setLeft(t.sub(0));
348: eq.setRight(plus(t.sub(1), i));
349: return eq;
350: }
351:
352: }
|