0001: // This file is part of KeY - Integrated Deductive Software Design
0002: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
0003: // Universitaet Koblenz-Landau, Germany
0004: // Chalmers University of Technology, Sweden
0005: //
0006: // The KeY system is protected by the GNU General Public License.
0007: // See LICENSE.TXT for details.
0008: package de.uka.ilkd.key.unittest;
0009:
0010: import de.uka.ilkd.key.java.*;
0011: import de.uka.ilkd.key.java.declaration.*;
0012: import de.uka.ilkd.key.java.declaration.modifier.*;
0013: import de.uka.ilkd.key.java.expression.*;
0014: import de.uka.ilkd.key.java.expression.operator.*;
0015: import de.uka.ilkd.key.java.expression.literal.*;
0016: import de.uka.ilkd.key.java.reference.*;
0017: import de.uka.ilkd.key.java.abstraction.*;
0018: import de.uka.ilkd.key.java.statement.*;
0019: import de.uka.ilkd.key.java.visitor.*;
0020: import de.uka.ilkd.key.util.*;
0021: import de.uka.ilkd.key.visualdebugger.VisualDebugger;
0022: import de.uka.ilkd.key.logic.*;
0023: import de.uka.ilkd.key.logic.sort.*;
0024: import de.uka.ilkd.key.logic.op.*;
0025: import de.uka.ilkd.key.rule.soundness.TermProgramVariableCollector;
0026: import de.uka.ilkd.key.rule.UpdateSimplifier;
0027:
0028: import java.io.*;
0029: import java.util.*;
0030:
0031: /**
0032: * Generates a unittest for a given piece of code and a set of modelgenerators.
0033: */
0034: public class TestGenerator {
0035:
0036: private StringWriter w;
0037: private Services serv;
0038: private JavaInfo ji;
0039:
0040: private KeYJavaType testCase;
0041: private KeYJavaType testSuite;
0042: private KeYJavaType b;
0043: private KeYJavaType intType;
0044: private Type suiteType;
0045: private TypeRef testTypeRef;
0046: private String fileName;
0047: private String path = null;
0048:
0049: private Random rand;
0050:
0051: private MethodDeclaration suiteMethod;
0052:
0053: private int mcounter = 0;
0054:
0055: private MethodReference oracle = null;
0056:
0057: static int counter = 0;
0058:
0059: private HashMap translatedFormulas;
0060: private String directory = System.getProperty("user.home")
0061: + File.separator + "testFiles";
0062:
0063: // private HashMap array2length;
0064:
0065: /**
0066: * creates a TestGenerator instance for the given compilation unit
0067: * @param serv the Services
0068: * @param fileName the name of the unittest file this TestGenerator
0069: * creates.
0070: */
0071: public TestGenerator(Services serv, String fileName) {
0072: ji = serv.getJavaInfo();
0073: translatedFormulas = new HashMap();
0074: // array2length = new HashMap();
0075: this .fileName = fileName;
0076: w = new StringWriter();
0077: this .serv = serv;
0078: ExtList l = new ExtList();
0079: l.add(new ProgramElementName(fileName));
0080: suiteType = new ClassDeclaration(l, new ProgramElementName(
0081: fileName), false);
0082: KeYJavaType testType = new KeYJavaType(suiteType,
0083: new ClassInstanceSortImpl(new Name(fileName), false));
0084: testTypeRef = new TypeRef(testType);
0085: testCase = ji
0086: .getKeYJavaTypeByClassName("junit.framework.TestCase");
0087: testSuite = ji
0088: .getKeYJavaTypeByClassName("junit.framework.TestSuite");
0089: b = ji.getTypeByName("boolean");
0090: intType = ji.getTypeByName("int");
0091: suiteMethod = createSuiteMethod();
0092: rand = new Random();
0093: }
0094:
0095: public TestGenerator(Services serv, String fileName,
0096: String directory) {
0097: this (serv, fileName);
0098: if (directory != null)
0099: this .directory = directory;
0100: }
0101:
0102: /**
0103: * Creates the class declaration of the unit test that should be exported
0104: * to a file.
0105: */
0106: private ClassDeclaration createSuiteClass(ExtList l) {
0107: l.add(new Public());
0108: l.add(new Extends(new TypeRef(testCase)));
0109: l.add(new ProgramElementName(fileName));
0110: ClassDeclaration result = new ClassDeclaration(l,
0111: new ProgramElementName(fileName), false);
0112: // FieldReplaceVisitor frv = new FieldReplaceVisitor(result);
0113: // frv.start();
0114: return result;
0115: }
0116:
0117: private KeYJavaType getArrayTypeAndEnsureExistence(
0118: KeYJavaType baseType, int dim) {
0119: final JavaInfo ji = serv.getJavaInfo();
0120: Sort as = ArraySortImpl.getArraySortForDim(baseType.getSort(),
0121: dim, ji.getJavaLangObjectAsSort(), ji
0122: .getJavaLangCloneableAsSort(), ji
0123: .getJavaIoSerializableAsSort());
0124: KeYJavaType kjt = ji.getKeYJavaType(as);
0125: if (kjt == null || baseType.getSort().toString().equals("int")) {
0126: JavaBlock jb = ji.readJavaBlock("{" + as + " v;}");
0127: return ((VariableDeclaration) ((StatementBlock) jb
0128: .program()).getChildAt(0)).getTypeReference()
0129: .getKeYJavaType();
0130: }
0131: return kjt;
0132: }
0133:
0134: private KeYJavaType getBaseType(KeYJavaType arrayType) {
0135: return ((ArrayType) arrayType.getJavaType()).getBaseType()
0136: .getKeYJavaType();
0137: }
0138:
0139: /** Creates a method of the form:
0140: * public void <name>(){
0141: * < pv-decls for v0,...,vl >
0142: * testData0 = {d_00,...,d_0k};
0143: * ...
0144: * testDataj = {d_j0,...,d_jk};
0145: * for(int i=0; i<testData0.length; i++){
0146: * ...
0147: * l0 = testData0[i];
0148: * ...
0149: * lj = testDataj[i];
0150: * <code>
0151: * java.lang.StringBuffer buffer;
0152: * buffer = new java.lang.StringBuffer ();
0153: * boolean result = testOracle(v0,..., vl, buffer);
0154: * assertTrue (< String >, result);
0155: * }
0156: * }
0157: * Where < String > contains the assignments of l0,...,lj in this
0158: * iteration and the results the oracles for the subformulas of post
0159: * have provided so far.
0160: *
0161: */
0162: private MethodDeclaration createTestMethod(Statement code[],
0163: Term post,
0164: Expression[][] testLocation,
0165: Expression[][] testData,
0166: // ProgramVariable[] pvs,
0167: ProgramVariable[] pvsNotDecl, String name,
0168: ExtList children, ModelGenerator mg,
0169: EquivalenceClass[] testLocEqvs) {
0170: ListOfStatement s = SLListOfStatement.EMPTY_LIST;
0171: // declare and initialize program variables
0172: for (int i = 0; i < pvsNotDecl.length; i++) {
0173: VariableSpecification varSpec = null;
0174: if (pvsNotDecl[i].getKeYJavaType().getSort().extendsTrans(
0175: serv.getTypeConverter().getIntegerLDT()
0176: .targetSort())) {
0177: varSpec = new VariableSpecification(pvsNotDecl[i],
0178: new TypeCast(new IntLiteral(0), new TypeRef(
0179: pvsNotDecl[i].getKeYJavaType())),
0180: pvsNotDecl[i].getKeYJavaType());
0181: } else if (pvsNotDecl[i].getKeYJavaType().getSort() == b
0182: .getSort()) {
0183: varSpec = new VariableSpecification(pvsNotDecl[i],
0184: BooleanLiteral.TRUE, pvsNotDecl[i]
0185: .getKeYJavaType());
0186: } else {
0187: /* varSpec =
0188: new VariableSpecification(
0189: pvsNotDecl[i], new New(
0190: new Expression[0],
0191: new TypeRef(pvsNotDecl[i].getKeYJavaType()),
0192: null),
0193: pvsNotDecl[i].getKeYJavaType());*/
0194: varSpec = new VariableSpecification(pvsNotDecl[i],
0195: NullLiteral.NULL, pvsNotDecl[i]
0196: .getKeYJavaType());
0197: }
0198: LocalVariableDeclaration lvd = new LocalVariableDeclaration(
0199: new TypeRef(pvsNotDecl[i].getKeYJavaType()),
0200: varSpec);
0201: s = s.append(lvd);
0202: }
0203:
0204: // put test data in array
0205: ProgramVariable[] testArray = new ProgramVariable[testLocation.length];
0206: boolean singleTuple = singleTuple(testData);
0207: for (int i = 0; i < testData.length; i++) {
0208: KeYJavaType kjt = testLocEqvs[i].getKeYJavaType();
0209: if (singleTuple) {
0210: Expression testDatum;
0211: if (testData[i][0] != null) {
0212: testDatum = new TypeCast(testData[i][0],
0213: new TypeRef(kjt));
0214: } else {
0215: testDatum = new TypeCast(new IntLiteral(rand
0216: .nextInt()), new TypeRef(kjt));
0217: }
0218: testArray[i] = new LocationVariable(
0219: new ProgramElementName("testData" + i), kjt);
0220: VariableSpecification vs = new VariableSpecification(
0221: testArray[i], testDatum, kjt.getJavaType());
0222: s = s.append(new LocalVariableDeclaration(new TypeRef(
0223: kjt), vs));
0224: } else {
0225: KeYJavaType akjt = getArrayTypeAndEnsureExistence(kjt,
0226: 1);
0227: ExtList ai = new ExtList();
0228: for (int j = 0; j < testData[i].length; j++) {
0229: ExtList partj = new ExtList();
0230: if (testData[i][j] != null) {
0231: ai.add(new TypeCast(testData[i][j],
0232: new TypeRef(kjt)));
0233: } else {
0234: ai.add(new TypeCast(new IntLiteral(rand
0235: .nextInt()), new TypeRef(kjt)));
0236: }
0237: }
0238: testArray[i] = new LocationVariable(
0239: new ProgramElementName("testData" + i), akjt);
0240: ExtList aType = new ExtList();
0241: aType.add(new TypeRef(kjt));
0242: NewArray init = new NewArray(aType, kjt,
0243: new ArrayInitializer(ai), 1);
0244: VariableSpecification vs = new VariableSpecification(
0245: testArray[i], init, akjt.getJavaType());
0246: s = s.append(new LocalVariableDeclaration(new TypeRef(
0247: akjt), vs));
0248: }
0249: }
0250: ArrayOfExpression arg = new ArrayOfExpression();
0251: ExtList l = new ExtList();
0252: l.add(new ProgramElementName(name));
0253: l.add(new Public());
0254: Statement[] ib = new Statement[6 + code.length];
0255:
0256: ProgramVariable partCounter = new LocationVariable(
0257: new ProgramElementName("testDataCounter"), intType);
0258: ProgramVariable length = new LocationVariable(
0259: new ProgramElementName("length"), intType);
0260:
0261: // assignments of test data to locations + initialization of
0262: // object references
0263: ListOfStatement assignments = SLListOfStatement.EMPTY_LIST;
0264:
0265: // initialization of arrays and creation of test data assignments
0266: HashMap array2Cons = new HashMap();
0267: ListOfStatement testDataAssignments = SLListOfStatement.EMPTY_LIST;
0268: for (int i = 0; i < testData.length; i++) {
0269: for (int k = 0; k < testLocation[i].length; k++) {
0270: Expression testDat = singleTuple ? (Expression) testArray[i]
0271: : (Expression) new ArrayReference(testArray[i],
0272: new Expression[] { partCounter });
0273: if (testLocation[i][k] instanceof FieldReference
0274: && ((FieldReference) testLocation[i][k])
0275: .getProgramVariable().name().toString()
0276: .equals("length")) {
0277: KeYJavaType at = ((Expression) ((FieldReference) testLocation[i][k])
0278: .getReferencePrefix()).getKeYJavaType(serv,
0279: null);
0280: if (at.getSort() instanceof ArraySort) {
0281: NewArray ar = new NewArray(
0282: new Expression[] { testDat },
0283: new TypeRef(getBaseType(at)), at, null,
0284: 0);
0285: // array2length.put(((FieldReference) testLocation[i][k]).
0286: // getReferencePrefix().toString(),
0287: // testDat);
0288: array2Cons.put(
0289: ((FieldReference) testLocation[i][k])
0290: .getReferencePrefix()
0291: .toString(), ar);
0292: continue;
0293: }
0294: }
0295: IndexReplaceVisitor irv = new IndexReplaceVisitor(
0296: testLocation[i][k], testLocation, singleTuple,
0297: partCounter, testArray);
0298: irv.start();
0299: irv.result();
0300: testDataAssignments = testDataAssignments
0301: .append(assignmentOrSet((Expression) irv
0302: .result(), testDat, serv));
0303: }
0304: }
0305:
0306: // initialization of other object references
0307: EquivalenceClass[] nonPrim = mg
0308: .getNonPrimitiveLocationEqvClasses();
0309: HashMap loc2cons = new HashMap();
0310: LinkedList locationsOrdered = new LinkedList();
0311: for (int i = 0; i < nonPrim.length; i++) {
0312: SetOfTerm locs = nonPrim[i].getLocations();
0313: IteratorOfTerm itt = locs.iterator();
0314: if (!nonPrim[i].isNull()) {
0315: Term nonPrimLocTerm = itt.next();
0316: Expression loc1 = translateTerm(nonPrimLocTerm, null,
0317: null);
0318: Expression cons;
0319: if (nonPrimLocTerm.sort() instanceof ArraySort) {
0320: cons = (Expression) array2Cons.get(loc1.toString());
0321: if (cons == null) {
0322: KeYJavaType locKJT = nonPrim[i]
0323: .getKeYJavaType();
0324: cons = new NewArray(
0325: new Expression[] { new IntLiteral(20) },
0326: new TypeRef(getBaseType(locKJT)),
0327: locKJT, null, 0);
0328: }
0329: /* KeYJavaType locKJT =loc1.getKeYJavaType(serv, null);
0330: ExtList aType = new ExtList();
0331: aType.add(new TypeRef(locKJT));
0332: cons = new NewArray(aType, locKJT,
0333: new ArrayInitializer(new ExtList()),
0334: 0);*/
0335: } else {
0336: cons = new New(new Expression[0], new TypeRef(
0337: nonPrim[i].getKeYJavaType()), null);
0338: }
0339: if (locs.size() > 1) {
0340: ProgramVariable pv = new LocationVariable(
0341: new ProgramElementName("_init" + i),
0342: nonPrim[i].getKeYJavaType());
0343: VariableSpecification varSpec = new VariableSpecification(
0344: pv, cons, nonPrim[i].getKeYJavaType());
0345: assignments = assignments
0346: .append(new LocalVariableDeclaration(
0347: new TypeRef(nonPrim[i]
0348: .getKeYJavaType()), varSpec));
0349: loc2cons.put(loc1, pv);
0350: while (itt.hasNext()) {
0351: Expression loc2 = translateTerm(itt.next(),
0352: null, null);
0353: addOrdered(loc2, locationsOrdered);
0354: loc2cons.put(loc2, pv);
0355: }
0356: } else {
0357: loc2cons.put(loc1, cons);
0358: }
0359: addOrdered(loc1, locationsOrdered);
0360: } else {
0361: while (itt.hasNext()) {
0362: Term locTerm = itt.next();
0363: if (locTerm.op() != Op.NULL) {
0364: Expression loc2 = translateTerm(locTerm, null,
0365: null);
0366: addOrdered(loc2, locationsOrdered);
0367: loc2cons.put(loc2, NullLiteral.NULL);
0368: }
0369: }
0370: }
0371: }
0372: Iterator locIt = locationsOrdered.iterator();
0373: while (locIt.hasNext()) {
0374: Expression loc = (Expression) locIt.next();
0375: Expression cons = (Expression) loc2cons.get(loc);
0376: IndexReplaceVisitor irv = new IndexReplaceVisitor(loc,
0377: testLocation, singleTuple, partCounter, testArray);
0378: irv.start();
0379: irv.result();
0380: assignments = assignments.append(assignmentOrSet(
0381: (Expression) irv.result(), cons, serv));
0382: }
0383:
0384: assignments = assignments.append(testDataAssignments);
0385: // assignments = removeOutOfBounds(assignments);
0386: ib[0] = new StatementBlock(assignments.toArray());
0387:
0388: for (int i = 0; i < code.length; i++) {
0389: ib[i + 1] = code[i];
0390: }
0391:
0392: KeYJavaType sb = ji
0393: .getKeYJavaTypeByClassName("java.lang.StringBuffer");
0394: New cons = new New(new Expression[0], new TypeRef(sb), null);
0395: ProgramVariable buffer = new LocationVariable(
0396: new ProgramElementName("buffer"), sb);
0397: ib[code.length + 1] = new LocalVariableDeclaration(new TypeRef(
0398: sb), new VariableSpecification(buffer));
0399: ib[code.length + 2] = new CopyAssignment(buffer, cons);
0400:
0401: ProgramVariable result = new LocationVariable(
0402: new ProgramElementName("result"), b);
0403: ib[code.length + 3] = new LocalVariableDeclaration(new TypeRef(
0404: b), new VariableSpecification(result));
0405: MethodReference oracle = getOracle(post, buffer, children);
0406: ib[code.length + 4] = new CopyAssignment(result, oracle);
0407: ProgramMethod assertTrue = ji
0408: .getProgramMethod(
0409: testCase,
0410: "assertTrue",
0411: SLListOfKeYJavaType.EMPTY_LIST
0412: .append(
0413: ji
0414: .getKeYJavaTypeByClassName("java.lang.String"))
0415: .append(b), testCase);
0416: Expression failure = new StringLiteral(
0417: "\\nPost evaluated to false.\\n"
0418: + "Variable/Location Assignments:\\n");
0419: for (int i = 0; i < testLocation.length; i++) {
0420: for (int j = 0; j < testLocation[i].length; j++) {
0421: Expression assignment = new Plus(
0422: new StringLiteral(" "
0423: + testLocation[i][j].toString() + " = "),
0424: singleTuple ? (Expression) testArray[i]
0425: : (Expression) new ArrayReference(
0426: testArray[i],
0427: new Expression[] { partCounter }));
0428: failure = new Plus(failure, assignment);
0429: }
0430: }
0431: Expression str = new Plus(new StringLiteral(
0432: "\\nEvaluation of subformulas so far: "),
0433: new MethodReference(new ArrayOfExpression(),
0434: new ProgramElementName("toString"), buffer));
0435: str = new Plus(failure, str);
0436: ib[code.length + 5] = new MethodReference(
0437: new ArrayOfExpression(new Expression[] { str, result }),
0438: new ProgramElementName("assertTrue"), null);
0439:
0440: Statement body = new StatementBlock(ib);
0441:
0442: // nested loops for executing the tested code with every possible
0443: // combination of testdata in each partition
0444: if (!singleTuple) {
0445: /* for(int i=0; i<testData.length; i++){
0446: VariableSpecification counterSpec =
0447: new VariableSpecification(lCounter[i], new IntLiteral(0),
0448: intType);
0449: LocalVariableDeclaration counterDecl =
0450: new LocalVariableDeclaration(new TypeRef(intType),
0451: counterSpec);
0452: Expression guard =
0453: new LessThan(lCounter[i], new FieldReference(
0454: length, new ArrayReference(
0455: testArray[i],
0456: new Expression[]{partCounter})));
0457: Expression update = new PostIncrement(lCounter[i]);
0458: body = new For(new LoopInitializer[]{counterDecl}, guard,
0459: new Expression[]{update}, body);
0460: }*/
0461: // loop over the number of partitions
0462: // int partCount = testData.length==0? 1 : testData[0].length;
0463: VariableSpecification counterSpec = new VariableSpecification(
0464: partCounter, new IntLiteral(0), intType);
0465: LocalVariableDeclaration counterDecl = new LocalVariableDeclaration(
0466: new TypeRef(intType), counterSpec);
0467: Expression guard = new LessThan(partCounter,
0468: testData.length == 0 ? (Expression) new IntLiteral(
0469: 1) : (Expression) new FieldReference(
0470: length, testArray[0]));
0471: // Expression guard =
0472: // new LessThan(partCounter, new IntLiteral(partCount));
0473: Expression update = new PostIncrement(partCounter);
0474: body = new For(new LoopInitializer[] { counterDecl },
0475: guard, new Expression[] { update }, body);
0476: }
0477:
0478: s = s.append(body);
0479: StatementBlock mBody = new StatementBlock(s.toArray());
0480: FieldReplaceVisitor frv = new FieldReplaceVisitor(mBody);
0481: frv.start();
0482: l.add(frv.result());
0483: l.add(new Comment("\n Covered execution trace:\n"
0484: + mg.getExecutionTrace()));
0485: MethodDeclaration tm = new MethodDeclaration(l, false);
0486:
0487: if (VisualDebugger.isDebuggingMode()) {
0488: VisualDebugger.getVisualDebugger().addTestCase(fileName,
0489: name, mg.getOriginalNode());
0490: }
0491:
0492: return tm;
0493: }
0494:
0495: private void addOrdered(Expression e, LinkedList l) {
0496: for (int i = 0; i < l.size(); i++) {
0497: if (depth((Expression) l.get(i)) > depth(e)) {
0498: l.add(i, e);
0499: return;
0500: }
0501: }
0502: l.add(e);
0503: }
0504:
0505: private boolean singleTuple(Expression[][] e) {
0506: if (0 < e.length) {
0507: return e[0].length == 1;
0508: }
0509: return true;
0510: }
0511:
0512: /**
0513: * Returns the depth, i.e. the length of the reference prefix of an
0514: * expression.
0515: */
0516: private int depth(Expression e) {
0517: if ((e instanceof FieldReference)
0518: && (((FieldReference) e).getReferencePrefix() instanceof Expression)) {
0519: return 1 + depth((Expression) ((FieldReference) e)
0520: .getReferencePrefix());
0521: } else if ((e instanceof ArrayReference)
0522: && (((ArrayReference) e).getReferencePrefix() instanceof Expression)) {
0523: return depth((Expression) ((ArrayReference) e)
0524: .getReferencePrefix()) + 1;
0525: }
0526: return 0;
0527: }
0528:
0529: /**
0530: * Generates either an assignment statement lhs = rhs; or a method call
0531: * statement for the appropriate set method in the case that
0532: * lhs is a field reference.
0533: */
0534: public static Statement assignmentOrSet(Expression lhs,
0535: Expression rhs, Services serv) {
0536: if (lhs instanceof FieldReference) {
0537: ProgramVariable pv = ((FieldReference) lhs)
0538: .getProgramVariable();
0539: String typeName = pv.getKeYJavaType().getName();
0540: typeName = PrettyPrinter
0541: .getTypeNameForAccessMethods(typeName);
0542: KeYJavaType kjt = pv.getContainerType();
0543: String pvName = pv.name().toString();
0544: pvName = pvName.substring(pvName.lastIndexOf(":") + 1);
0545: String methodName = "_set" + pvName + typeName;
0546: ListOfKeYJavaType sig = SLListOfKeYJavaType.EMPTY_LIST;
0547: sig = sig.append(pv.getKeYJavaType());
0548: return new MethodReference(new ArrayOfExpression(rhs),
0549: new ProgramElementName(methodName),
0550: ((FieldReference) lhs).getReferencePrefix());
0551: }
0552: CopyAssignment ca = new CopyAssignment(lhs, rhs);
0553: if (lhs instanceof ArrayReference) {
0554: KeYJavaType ae = serv.getJavaInfo()
0555: .getKeYJavaTypeByClassName(
0556: "java.lang.ArrayIndexOutOfBoundsException");
0557: ParameterDeclaration pd = new ParameterDeclaration(
0558: new Modifier[0], new TypeRef(ae),
0559: new VariableSpecification(new LocationVariable(
0560: new ProgramElementName("e"), ae)), false);
0561: Branch c = new Catch(pd, new StatementBlock());
0562: return new Try(new StatementBlock(ca), new Branch[] { c });
0563: } else {
0564: return ca;
0565: }
0566: }
0567:
0568: /**
0569: * creates the method public static junit.framework.TestSuite suite () ...
0570: * which is needed for junit test suites.
0571: */
0572: private MethodDeclaration createSuiteMethod() {
0573: TypeRef testSuiteRef = new TypeRef(testSuite);
0574: ExtList l = new ExtList();
0575: l.add(new ProgramElementName("suite"));
0576: l.add(new Public());
0577: l.add(new Static());
0578: l.add(testSuiteRef);
0579: Statement[] s = new Statement[3];
0580:
0581: ProgramVariable suite = new LocationVariable(
0582: new ProgramElementName("suite"), testSuite);
0583: s[0] = new LocalVariableDeclaration(testSuiteRef,
0584: new VariableSpecification(suite));
0585: Expression[] arg = new Expression[1];
0586: arg[0] = new MetaClassReference(testTypeRef);
0587: New cons = new New(arg, testSuiteRef, null);
0588: s[1] = new CopyAssignment(suite, cons);
0589: s[2] = new Return(suite);
0590: StatementBlock mBody = new StatementBlock(s);
0591: FieldReplaceVisitor frv = new FieldReplaceVisitor(mBody);
0592: frv.start();
0593: l.add(frv.result());
0594: return new MethodDeclaration(l, false);
0595: }
0596:
0597: /**
0598: * Generates the testcase and writes it to a file.
0599: * @param code the piece of code that is tested by the generated unittest.
0600: * @param oracle a term representing the postcondition of
0601: * <code>code</code>. It is used to create a testoracle.
0602: * @param mgs List of ModelGenerators.
0603: * @param programVars program variables that have to be declared in the
0604: * method.
0605: * @param methodName the name of the testmethod created for
0606: * <code>code</code>within the test case.
0607: */
0608: public void generateTestSuite(Statement[] code, Term oracle,
0609: List mgs, SetOfProgramVariable programVars,
0610: String methodName, PackageReference pr) {
0611: UpdateSimplifier simplifier = new UpdateSimplifier();
0612: oracle = simplifier.simplify(oracle, serv);
0613: HashSet processedModels = new HashSet();
0614: int dm = 0;
0615: Iterator it = mgs.iterator();
0616: // ProgramVariable[] pva = null;
0617: ProgramVariable[] pvaNotDecl = null;
0618: while (it.hasNext()) {
0619: ModelGenerator mg = (ModelGenerator) it.next();
0620: programVars = programVars.union(mg.getProgramVariables());
0621: }
0622: pvaNotDecl = removeDublicates(programVars).toArray();
0623: it = mgs.iterator();
0624: ExtList l = new ExtList();
0625: l.add(suiteMethod);
0626: int testMCounter = 0;
0627: while (it.hasNext()) {
0628: ModelGenerator mg = (ModelGenerator) it.next();
0629: Model[] models = mg.createModels();
0630: int dublicate = 0;
0631: if (models.length - dublicate == 0 && mgs.size() != 1) {
0632: continue;
0633: }
0634: EquivalenceClass[] eqvArray = mg
0635: .getPrimitiveLocationEqvClasses();
0636: Expression[][] testLocation = new Expression[eqvArray.length][];
0637: Expression[][] testData = new Expression[eqvArray.length][models.length
0638: - dublicate];
0639: for (int i = 0; i < eqvArray.length; i++) {
0640: SetOfTerm locs = eqvArray[i].getLocations();
0641: testLocation[i] = new Expression[locs.size()];
0642: int k = 0;
0643: IteratorOfTerm itt = locs.iterator();
0644: while (itt.hasNext()) {
0645: Term testLoc = itt.next();
0646: testLocation[i][k++] = translateTerm(testLoc, null,
0647: null);
0648: }
0649: for (int j = 0; j < models.length - dublicate; j++) {
0650: testData[i][j] = models[j]
0651: .getValueAsExpression(eqvArray[i]);
0652: }
0653: }
0654: l.add(createTestMethod(code, oracle, testLocation,
0655: testData, pvaNotDecl,
0656: methodName + (testMCounter++), l, mg, eqvArray));
0657: }
0658:
0659: ClassDeclaration suite = createSuiteClass(l);
0660: PrettyPrinter pp = new PrettyPrinter(w, false, true);
0661: try {
0662: // write the file to disk
0663: pp.printClassDeclaration(suite);
0664: File dir = new File(directory);
0665: if (!dir.exists()) {
0666: dir.mkdirs();
0667: }
0668: File pcFile = new File(dir, fileName + ".java");
0669: path = pcFile.getAbsolutePath();
0670: FileWriter fw = new FileWriter(pcFile);
0671: BufferedWriter bw = new BufferedWriter(fw);
0672: bw.write(addImports(clean(w.toString()), pr));
0673: bw.close();
0674: } catch (IOException ioe) {
0675: }
0676: exportCodeUnderTest();
0677: }
0678:
0679: /**
0680: * Exports the code under test to files and adds get and set methods for
0681: * each field.
0682: */
0683: public void exportCodeUnderTest() {
0684: Set kjts = ji.getAllKeYJavaTypes();
0685: Iterator it = kjts.iterator();
0686: while (it.hasNext()) {
0687: KeYJavaType kjt = (KeYJavaType) it.next();
0688: if ((kjt.getJavaType() instanceof ClassDeclaration || kjt
0689: .getJavaType() instanceof InterfaceDeclaration)
0690: && ((TypeDeclaration) kjt.getJavaType())
0691: .getPositionInfo().getFileName() != null
0692: && ((TypeDeclaration) kjt.getJavaType())
0693: .getPositionInfo().getFileName().indexOf(
0694: "resources") == -1) {
0695:
0696: StringWriter sw = new StringWriter();
0697: PrettyPrinter pp = new PrettyPrinter(sw, false, true);
0698: try {
0699: // write the implementation under test to the testFiles
0700: // directory
0701: if (kjt.getJavaType() instanceof ClassDeclaration) {
0702: pp.printClassDeclaration((ClassDeclaration) kjt
0703: .getJavaType());
0704: } else {
0705: pp
0706: .printInterfaceDeclaration((InterfaceDeclaration) kjt
0707: .getJavaType());
0708: }
0709: String fn = ((TypeDeclaration) kjt.getJavaType())
0710: .getPositionInfo().getFileName();
0711:
0712: String header = getHeader(fn);
0713:
0714: File dir = new File(directory
0715: + fn.substring(0, fn
0716: .lastIndexOf(File.separator)));
0717: fn = fn
0718: .substring(fn.lastIndexOf(File.separator) + 1);
0719: if (!dir.exists()) {
0720: dir.mkdirs();
0721: }
0722: File pcFile = new File(dir, fn);
0723: FileWriter fw = new FileWriter(pcFile);
0724: BufferedWriter bw = new BufferedWriter(fw);
0725: bw.write(header);
0726: bw.write(clean(sw.toString()));
0727: bw.close();
0728: } catch (IOException ioe) {
0729: throw new UnitTestException(ioe);
0730: }
0731: }
0732: }
0733: }
0734:
0735: private String clean(String s) {
0736: while (s.indexOf(";.") != -1) {
0737: s = s.substring(0, s.indexOf(";."))
0738: + s.substring(s.indexOf(";.") + 1);
0739: }
0740: while (s.indexOf(";;") != -1) {
0741: s = s.substring(0, s.indexOf(";;"))
0742: + s.substring(s.indexOf(";;") + 1);
0743: }
0744: while (s.indexOf(";[") != -1) {
0745: s = s.substring(0, s.indexOf(";["))
0746: + s.substring(s.indexOf(";[") + 1);
0747: }
0748: while (s.indexOf(";]") != -1) {
0749: s = s.substring(0, s.indexOf(";]"))
0750: + s.substring(s.indexOf(";]") + 1);
0751: }
0752: return s;
0753: }
0754:
0755: /** Returns the header consisting of package and import statements
0756: * occuring in the file <code>fileName</code>.
0757: */
0758: private String getHeader(String fileName) {
0759: String result = "";
0760: String lineSeparator = System.getProperty("line.separator");
0761: BufferedReader reader;
0762: try {
0763: reader = new BufferedReader(new FileReader(fileName));
0764: String line;
0765: while ((line = reader.readLine()) != null) {
0766: result += line + lineSeparator;
0767: }
0768: reader.close();
0769: } catch (IOException ioe) {
0770: throw new UnitTestException(ioe);
0771: }
0772: int declIndex = result.indexOf("class ");
0773: if (declIndex == -1) {
0774: declIndex = result.indexOf("interface ");
0775: }
0776: result = result.substring(0, declIndex);
0777: result = result.substring(0, result.lastIndexOf(";") + 1);
0778: return result + "\n\n";
0779: }
0780:
0781: public SetOfProgramVariable removeDublicates(
0782: SetOfProgramVariable pvs) {
0783: HashSet names = new HashSet();
0784: IteratorOfProgramVariable it = pvs.iterator();
0785: SetOfProgramVariable result = SetAsListOfProgramVariable.EMPTY_SET;
0786: while (it.hasNext()) {
0787: ProgramVariable pv = it.next();
0788: if (names.add(pv.name().toString())) {
0789: result = result.add(pv);
0790: }
0791: }
0792: return result;
0793: }
0794:
0795: /**
0796: * Returns the path of the file generated by this instance.
0797: */
0798: public String getPath() {
0799: return path;
0800: }
0801:
0802: private String addImports(String classDec, PackageReference pr) {
0803: String imports = "import junit.framework.*;";
0804: if (pr != null) {
0805: imports += "\nimport " + pr + ".*;";
0806: }
0807: return imports + "\n\n" + classDec;
0808: }
0809:
0810: /** Creates a testoracle from the term <code>post</code>.
0811: * @param post the term used for creating a testoracle.
0812: * @param buffer a program variable of type StringBuffer.
0813: * @param children the children of the enclosing class. The MethodDeclarations
0814: * created by this method are added to <code>children</code>.
0815: */
0816: public MethodReference getOracle(Term post, ProgramVariable buffer,
0817: ExtList children) {
0818: if (oracle == null) {
0819: post = replaceConstants(post, serv, null);
0820: oracle = (MethodReference) getMethodReferenceForFormula(
0821: post, buffer, children);
0822: }
0823: return oracle;
0824: }
0825:
0826: /**
0827: * Returns the method reference the term post is translated to and creates
0828: * also the corresponding method declaration.
0829: */
0830: private Expression getMethodReferenceForFormula(Term post,
0831: ProgramVariable buffer, ExtList children) {
0832: if (post.sort() != Sort.FORMULA) {
0833: return translateTerm(post, buffer, children);
0834: }
0835: if (translatedFormulas.containsKey(post)) {
0836: return (Expression) translatedFormulas.get(post);
0837: }
0838: ExtList args = getArguments(post);
0839: args.add(buffer);
0840: LinkedList params = getParameterDeclarations(args);
0841: Statement[] mBody = buildMethodBodyFromFormula(post, buffer,
0842: children);
0843: MethodDeclaration md = buildMethodDeclaration(mBody,
0844: new TypeRef(b), "subformula", params);
0845: children.add(md);
0846: MethodReference mr = new MethodReference(args,
0847: new ProgramElementName(md.getName()), testTypeRef);
0848: translatedFormulas.put(post, mr);
0849: return mr;
0850: }
0851:
0852: /**
0853: * Creates the method body for the method the term post is translated to.
0854: */
0855: private Statement[] buildMethodBodyFromFormula(Term post,
0856: ProgramVariable buffer, ExtList children) {
0857: Statement[] s = new Statement[4];
0858: ProgramVariable result = new LocationVariable(
0859: new ProgramElementName("result"), b);
0860: s[0] = new LocalVariableDeclaration(new TypeRef(b),
0861: new VariableSpecification(result));
0862: Expression f = translateFormula(post, buffer, children);
0863: s[1] = new CopyAssignment(result, f);
0864: Plus str = new Plus(new StringLiteral("\\neval(" + post
0865: + ") = "), result);
0866: s[2] = new MethodReference(new ArrayOfExpression(str),
0867: new ProgramElementName("append"), buffer);
0868: s[3] = new Return(result);
0869: return s;
0870: }
0871:
0872: /**
0873: * Translates a term to a java expression.
0874: */
0875: private Expression translateTerm(Term t, ProgramVariable buffer,
0876: ExtList children) {
0877: Expression result = null;
0878: if (t.op() instanceof ProgramInLogic) {
0879: final ExtList tchildren = new ExtList();
0880: for (int i = 0; i < t.arity(); i++) {
0881: tchildren
0882: .add(translateTerm(t.sub(i), buffer, children));
0883: }
0884: return ((ProgramInLogic) t.op()).convertToProgram(t,
0885: tchildren);
0886: } else if (t.op() == Op.IF_THEN_ELSE) {
0887: ExtList l = new ExtList();
0888: l.add(getMethodReferenceForFormula(t.sub(0), buffer,
0889: children));
0890: l.add(translateTerm(t.sub(1), buffer, children));
0891: l.add(translateTerm(t.sub(2), buffer, children));
0892: result = new Conditional(l);
0893: result = new ParenthesizedExpression(result);
0894: } else if (t.op() instanceof Function) {
0895: String name = t.op().name().toString().intern();
0896: if (name.equals("add") || name.equals("jadd")
0897: || name.equals("addJint")) {
0898: result = new Plus(translateTerm(t.sub(0), buffer,
0899: children), translateTerm(t.sub(1), buffer,
0900: children));
0901: } else if (name.equals("sub") || name.equals("jsub")
0902: || name.equals("subJint")) {
0903: result = new Minus(translateTerm(t.sub(0), buffer,
0904: children), translateTerm(t.sub(1), buffer,
0905: children));
0906: } else if (name.equals("neg") || name.equals("jneg")
0907: || name.equals("negJint") || name.equals("neglit")) {
0908: result = new Negative(translateTerm(t.sub(0), buffer,
0909: children));
0910: } else if (name.equals("mul") || name.equals("jmul")
0911: || name.equals("mulJint")) {
0912: result = new Times(translateTerm(t.sub(0), buffer,
0913: children), translateTerm(t.sub(1), buffer,
0914: children));
0915: } else if (name.equals("div") || name.equals("jdiv")
0916: || name.equals("divJint")) {
0917: result = new Divide(translateTerm(t.sub(0), buffer,
0918: children), translateTerm(t.sub(1), buffer,
0919: children));
0920: } else if (name.equals("mod") || name.equals("jmod")
0921: || name.equals("modJint")) {
0922: result = new Modulo(translateTerm(t.sub(0), buffer,
0923: children), translateTerm(t.sub(1), buffer,
0924: children));
0925: } else if (name.equals("Z")) {
0926: result = translateTerm(t.sub(0), buffer, children);
0927: }
0928: if (result != null) {
0929: result = new ParenthesizedExpression(result);
0930: }
0931: }
0932: if (result == null) {
0933: result = convertToProgramElement(t);
0934: }
0935: return result;
0936: }
0937:
0938: /**
0939: * Translates a formula to a java expression, i.e. an oracle for the
0940: * is created
0941: * @param children the children of the enclosing class. The method
0942: * declarations created by this method are added to <code>
0943: * children</code>.
0944: */
0945: private Expression translateFormula(Term post,
0946: ProgramVariable buffer, ExtList children) {
0947: ExtList l = new ExtList();
0948: if (post.sort() != Sort.FORMULA) {
0949: return translateTerm(post, buffer, children);
0950: } else if (post.op() == Op.TRUE) {
0951: return BooleanLiteral.TRUE;
0952: } else if (post.op() == Op.FALSE) {
0953: return BooleanLiteral.FALSE;
0954: } else if (post.op() == Op.NOT) {
0955: l.add(new ParenthesizedExpression(translateFormula(post
0956: .sub(0), buffer, children)));
0957: return new LogicalNot(l);
0958: } else if (post.op() == Op.AND) {
0959: return new LogicalAnd(getMethodReferenceForFormula(post
0960: .sub(0), buffer, children),
0961: getMethodReferenceForFormula(post.sub(1), buffer,
0962: children));
0963: } else if (post.op() == Op.OR) {
0964: return new LogicalOr(getMethodReferenceForFormula(post
0965: .sub(0), buffer, children),
0966: getMethodReferenceForFormula(post.sub(1), buffer,
0967: children));
0968: } else if (post.op() == Op.IMP) {
0969: l.add(getMethodReferenceForFormula(post.sub(0), buffer,
0970: children));
0971: return new LogicalOr(new LogicalNot(l),
0972: getMethodReferenceForFormula(post.sub(1), buffer,
0973: children));
0974: } else if (post.op() instanceof Equality) {
0975: l.add(getMethodReferenceForFormula(post.sub(0), buffer,
0976: children));
0977: l.add(getMethodReferenceForFormula(post.sub(1), buffer,
0978: children));
0979: Equals eq = new Equals(l);
0980: return eq;
0981: } else if (post.op() == Op.IF_THEN_ELSE) {
0982: l.add(getMethodReferenceForFormula(post.sub(0), buffer,
0983: children));
0984: l.add(getMethodReferenceForFormula(post.sub(1), buffer,
0985: children));
0986: l.add(getMethodReferenceForFormula(post.sub(2), buffer,
0987: children));
0988: return new Conditional(l);
0989: } else if (post.op() == Op.ALL) {
0990: return translateQuantifiedTerm(true, post, buffer, children);
0991: } else if (post.op() == Op.EX) {
0992: return translateQuantifiedTerm(false, post, buffer,
0993: children);
0994: } else if (post.op().name().toString().equals("lt")) {
0995: return new LessThan(translateTerm(post.sub(0), buffer,
0996: children), translateTerm(post.sub(1), buffer,
0997: children));
0998: } else if (post.op().name().toString().equals("gt")) {
0999: l.add(translateTerm(post.sub(0), buffer, children));
1000: l.add(translateTerm(post.sub(1), buffer, children));
1001: return new GreaterThan(l);
1002: } else if (post.op().name().toString().equals("geq")) {
1003: l.add(translateTerm(post.sub(0), buffer, children));
1004: l.add(translateTerm(post.sub(1), buffer, children));
1005: return new GreaterOrEquals(l);
1006: } else if (post.op().name().toString().equals("leq")) {
1007: return new LessOrEquals(translateTerm(post.sub(0), buffer,
1008: children), translateTerm(post.sub(1), buffer,
1009: children));
1010: }
1011: throw new NotTranslatableException(
1012: "Test oracle could not be generated");
1013: }
1014:
1015: /**
1016: * Builds a method declaration with the provided name and type.
1017: * Field references o.a occuring in the method body are replaced
1018: * by methodcalls o._a().
1019: */
1020: private MethodDeclaration buildMethodDeclaration(Statement[] body,
1021: TypeRef type, String name, LinkedList params) {
1022: ExtList l = new ExtList();
1023: l.add(new ProgramElementName(name + (mcounter++)));
1024: l.add(new Private());
1025: l.add(new Static());
1026: l.addAll(params);
1027: l.add(type);
1028: StatementBlock mBody = new StatementBlock(body);
1029: FieldReplaceVisitor frv = new FieldReplaceVisitor(mBody);
1030: frv.start();
1031: l.add(frv.result());
1032: MethodDeclaration md = new MethodDeclaration(l, false);
1033: return md;
1034: }
1035:
1036: /**
1037: * Creates an oracle for a quantified formula, which is only possible for
1038: * some classes of quantified formulas. If <code>t</code> doesn't belong
1039: * to one of these classes a NotTranslatableException is thrown.
1040: */
1041: private Expression translateQuantifiedTerm(boolean all, Term t,
1042: ProgramVariable buffer, ExtList children) {
1043: de.uka.ilkd.key.logic.op.Operator junctor;
1044: Expression resInit;
1045: if (all) {
1046: junctor = Op.IMP;
1047: resInit = BooleanLiteral.TRUE;
1048: } else {
1049: junctor = Op.AND;
1050: resInit = BooleanLiteral.FALSE;
1051: }
1052: // if(true ) return BooleanLiteral.TRUE;
1053: Statement[] body = new Statement[4];
1054: Expression[] bounds = new Expression[] { null, null, null, null };
1055: LogicVariable lv = (LogicVariable) t.varsBoundHere(0)
1056: .lastQuantifiableVariable();
1057: if (t.varsBoundHere(0).size() > 1
1058: || !(lv.sort() == intType.getSort() || lv.sort()
1059: .toString().equals("jint"))) {
1060: throw new NotTranslatableException("quantified Term " + t);
1061: }
1062: ProgramVariable result = new LocationVariable(
1063: new ProgramElementName("result"), b);
1064: body[0] = new LocalVariableDeclaration(new TypeRef(b),
1065: new VariableSpecification(result, resInit, b
1066: .getJavaType()));
1067: KeYJavaType lvType = intType;
1068: ProgramVariable pv = new LocationVariable(
1069: new ProgramElementName("_" + lv.name() + (counter++)),
1070: lvType);
1071: Term sub0 = replaceLogicVariable(t.sub(0), lv, pv);
1072: if (sub0.op() == junctor && sub0.sub(0).op() == Op.AND) {
1073: Term range = sub0.sub(0);
1074: getBound(range.sub(0), bounds, pv, buffer, children);
1075: getBound(range.sub(1), bounds, pv, buffer, children);
1076: } else if (sub0.op() == junctor && sub0.sub(1).op() == junctor) {
1077: getBound(sub0.sub(0), bounds, pv, buffer, children);
1078: getBound(sub0.sub(1).sub(0), bounds, pv, buffer, children);
1079: } else {
1080: throw new NotTranslatableException("quantified Term " + t);
1081: }
1082:
1083: Statement loopBody = new CopyAssignment(result,
1084: all ? (Expression) new LogicalAnd(result,
1085: getMethodReferenceForFormula(sub0.sub(1),
1086: buffer, children))
1087: : (Expression) new LogicalOr(result,
1088: getMethodReferenceForFormula(sub0
1089: .sub(1), buffer, children)));
1090: VariableSpecification vs = new VariableSpecification(pv,
1091: bounds[0] != null ? bounds[0] : new Plus(bounds[1],
1092: new IntLiteral(1)), intType.getJavaType());
1093: LocalVariableDeclaration init = new LocalVariableDeclaration(
1094: new TypeRef(intType), vs);
1095: Expression guard = bounds[2] == null ? (Expression) new LessThan(
1096: pv, bounds[3])
1097: : (Expression) new LessOrEquals(pv, bounds[2]);
1098: Expression update = new PostIncrement(pv);
1099: body[1] = new For(new LoopInitializer[] { init }, guard,
1100: new Expression[] { update }, new StatementBlock(
1101: loopBody));
1102: Plus str = new Plus(new StringLiteral("\\neval(" + t + ") = "),
1103: result);
1104: body[2] = new MethodReference(new ArrayOfExpression(str),
1105: new ProgramElementName("append"), buffer);
1106: body[3] = new Return(result);
1107:
1108: ExtList args = getArguments(t);
1109: args.add(buffer);
1110: LinkedList params = getParameterDeclarations(args);
1111:
1112: MethodDeclaration md = buildMethodDeclaration(body,
1113: new TypeRef(b), "quantifierTerm", params);
1114: children.add(md);
1115: return new MethodReference(args, new ProgramElementName(md
1116: .getName()), testTypeRef);
1117: }
1118:
1119: /**
1120: * Returns the program variables occuring in t that are no atributes.
1121: */
1122: private ExtList getArguments(Term t) {
1123: SetOfProgramVariable programVars = SetAsListOfProgramVariable.EMPTY_SET;
1124: TermProgramVariableCollector pvColl = new TermProgramVariableCollector();
1125: t.execPreOrder(pvColl);
1126: Iterator itp = pvColl.result().iterator();
1127: while (itp.hasNext()) {
1128: ProgramVariable v = (ProgramVariable) itp.next();
1129: if (!v.isMember()) {
1130: programVars = programVars.add(v);
1131: }
1132: }
1133: programVars = removeDublicates(programVars);
1134: IteratorOfProgramVariable it = programVars.iterator();
1135: ExtList args = new ExtList();
1136: while (it.hasNext()) {
1137: args.add(it.next());
1138: }
1139: return args;
1140: }
1141:
1142: private LinkedList getParameterDeclarations(ExtList l) {
1143: LinkedList params = new LinkedList();
1144: Iterator it = l.iterator();
1145: while (it.hasNext()) {
1146: ProgramVariable arg = (ProgramVariable) it.next();
1147: params.add(new ParameterDeclaration(new Modifier[0],
1148: new TypeRef(arg.getKeYJavaType()),
1149: new VariableSpecification(arg), false));
1150: }
1151: return params;
1152: }
1153:
1154: /**
1155: * Trys to extract bounds for the quantified integer variable.
1156: */
1157: private void getBound(Term t, Expression[] bounds,
1158: ProgramVariable pv, ProgramVariable buffer, ExtList children) {
1159: int ex = 0, less = 1;
1160: if ((t.op().name().toString().equals("!") || t.op().name()
1161: .toString().equals("not"))
1162: && t.sub(0).op().name().toString().equals("lt")) {
1163: t = t.sub(0);
1164: less = 0;
1165: } else if (t.op().name().toString().equals("lt")) {
1166: ex = 1;
1167: } else if (t.op().name().toString().equals("leq")) {
1168: } else if (t.op().name().toString().equals("geq")) {
1169: less = 0;
1170: } else if (t.op().name().toString().equals("gt")) {
1171: ex = 1;
1172: less = 0;
1173: } else {
1174: throw new NotTranslatableException("bound " + t
1175: + " for quantified variable");
1176: }
1177: if (t.sub(0).op() == pv) {
1178: bounds[2 * less + ex] = translateTerm(t.sub(1), buffer,
1179: children);
1180: } else if (t.sub(1).op() == pv) {
1181: bounds[2 - 2 * less + ex] = translateTerm(t.sub(0), buffer,
1182: children);
1183: } else {
1184: throw new NotTranslatableException("bound " + t
1185: + " for quantified variable");
1186: }
1187: }
1188:
1189: /**
1190: * replaces all occurences of lv in t with pv.
1191: */
1192: private Term replaceLogicVariable(Term t, LogicVariable lv,
1193: ProgramVariable pv) {
1194: TermFactory tf = TermFactory.DEFAULT;
1195: Term result = null;
1196: if (t.op() == lv) {
1197: return tf.createVariableTerm(pv);
1198: } else {
1199: Term subTerms[] = new Term[t.arity()];
1200: ArrayOfQuantifiableVariable[] quantVars = new ArrayOfQuantifiableVariable[t
1201: .arity()];
1202: for (int i = 0; i < t.arity(); i++) {
1203: quantVars[i] = t.varsBoundHere(i);
1204: subTerms[i] = replaceLogicVariable(t.sub(i), lv, pv);
1205: }
1206: JavaBlock jb = t.javaBlock();
1207: result = tf.createTerm(t.op(), subTerms, quantVars, jb);
1208: }
1209: return result;
1210: }
1211:
1212: /**
1213: * Converts <code>t</code> to a ProgramElement. If <code>t</code> is
1214: * a (skolem)constant, a new identically named ProgramVariable of the
1215: * same sort is returned.
1216: */
1217: public Expression convertToProgramElement(Term t) {
1218: t = replaceConstants(t, serv, null);
1219: return serv.getTypeConverter().convertToProgramElement(t);
1220: }
1221:
1222: /**
1223: * Replaces rigid constants by program variables.
1224: */
1225: protected static Term replaceConstants(Term t, Services serv,
1226: Namespace newPVs) {
1227: TermFactory tf = TermFactory.DEFAULT;
1228: Term result = null;
1229: if (t.op() instanceof RigidFunction && t.arity() == 0
1230: && !"#".equals(t.op().name().toString())
1231: && !"TRUE".equals(t.op().name().toString())
1232: && !"FALSE".equals(t.op().name().toString())
1233: && t.op() != Op.NULL) {
1234: KeYJavaType kjt = serv.getJavaInfo().getKeYJavaType(
1235: t.sort().toString());
1236: if (t.sort().toString().startsWith("jint")) {
1237: kjt = serv.getJavaInfo().getKeYJavaType(
1238: t.sort().toString().substring(1));
1239: }
1240: ProgramVariable pv = new LocationVariable(
1241: new ProgramElementName(t.op().name().toString()),
1242: kjt);
1243: if (newPVs != null) {
1244: newPVs.add(pv);
1245: }
1246: return tf.createVariableTerm(pv);
1247: } else if (t.op() instanceof ProgramVariable) {
1248: if (newPVs != null
1249: && !((ProgramVariable) t.op()).isStatic()) {
1250: newPVs.add((ProgramVariable) t.op());
1251: }
1252: return t;
1253: } else {
1254: Term subTerms[] = new Term[t.arity()];
1255: ArrayOfQuantifiableVariable[] quantVars = new ArrayOfQuantifiableVariable[t
1256: .arity()];
1257: for (int i = 0; i < t.arity(); i++) {
1258: quantVars[i] = t.varsBoundHere(i);
1259: subTerms[i] = replaceConstants(t.sub(i), serv, newPVs);
1260: }
1261: JavaBlock jb = t.javaBlock();
1262: result = tf.createTerm(t.op(), subTerms, quantVars, jb);
1263: }
1264: return result;
1265: }
1266:
1267: }
|