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;
009:
010: import de.uka.ilkd.key.java.*;
011: import de.uka.ilkd.key.java.declaration.*;
012: import de.uka.ilkd.key.java.reference.*;
013: import de.uka.ilkd.key.java.statement.*;
014: import de.uka.ilkd.key.java.visitor.*;
015: import de.uka.ilkd.key.java.expression.operator.*;
016: import de.uka.ilkd.key.logic.op.*;
017: import de.uka.ilkd.key.logic.*;
018: import de.uka.ilkd.key.proof.*;
019: import de.uka.ilkd.key.visualization.*;
020:
021: import java.util.*;
022:
023: /**
024: * Extracts the code, for which we want to create a unittest, from a formula
025: * of the form: < updates> \\< code\\> post.
026: */
027: public class TestCodeExtractor {
028:
029: // private Term modTerm;
030: private Services serv;
031: private ExecutionTraceModel tr;
032:
033: private Statement[] testCode = null;
034: private Term post = null;
035: private PackageReference context = null;
036: private StatementBlock sb = null;
037:
038: // the name of the file the method under test is located in
039: private String fileName = null;
040: // the package of the containing class
041: // private String packageName = null;
042: // the method we want to test
043: private String methodName = null;
044: private static int testCounter = 0;
045: private Namespace newPVs = new Namespace();
046: private Namespace pvn;
047:
048: public TestCodeExtractor(ExecutionTraceModel tr, Services serv,
049: Namespace pvn) {
050: this .tr = tr;
051: this .serv = serv;
052: this .pvn = pvn;
053: }
054:
055: public Statement[] extractTestCode() {
056: if (testCode != null) {
057: return testCode;
058: }
059: Semisequent succ = getNodeForCodeExtraction(tr).sequent()
060: .succedent();
061: for (int i = 0; i < succ.size(); i++) {
062: Term current = succ.get(i).formula();
063: ListOfStatement statements = SLListOfStatement.EMPTY_LIST;
064: //TODO: Resolve data dependencies in simultaneous updates.
065: while (current.op() instanceof IUpdateOperator) {
066: statements = statements.append(getAssignments(current));
067: current = current.sub(current.op().arity() - 1);
068: }
069: if (current.op() instanceof Modality) {
070: post = current.sub(0);
071: sb = (StatementBlock) current.javaBlock().program();
072: collectUndeclaredVariables(sb);
073: statements = statements.append(flatten(sb));
074: testCode = statements.toArray();
075: return testCode;
076: }
077: }
078: throw new NotTranslatableException("Could not extract testcode");
079: }
080:
081: /**
082: * Collects variables not explicitely declared in the IUT.
083: */
084: private void collectUndeclaredVariables(StatementBlock sb) {
085: JavaASTCollector coll = new JavaASTCollector(sb,
086: ProgramVariable.class);
087: coll.start();
088: ListOfProgramElement l = coll.getNodes();
089: IteratorOfProgramElement it = l.iterator();
090: while (it.hasNext()) {
091: ProgramVariable pv = (ProgramVariable) it.next();
092: if (pvn.lookup(pv.name()) == pv) {
093: newPVs.add(pv);
094: }
095: }
096: coll = new JavaASTCollector(sb, LocalVariableDeclaration.class);
097: coll.start();
098: l = coll.getNodes();
099: it = l.iterator();
100: ListOfNamed lon = newPVs.allElements();
101: while (it.hasNext()) {
102: LocalVariableDeclaration lvd = (LocalVariableDeclaration) it
103: .next();
104: ArrayOfVariableSpecification vars = lvd.getVariables();
105: for (int i = 0; i < vars.size(); i++) {
106: IProgramVariable pv = vars.getVariableSpecification(i)
107: .getProgramVariable();
108: if (pvn.lookup(pv.name()) == pv) {
109: lon = lon.removeAll(pv);
110: }
111: }
112: }
113: newPVs = new Namespace();
114: while (!lon.isEmpty()) {
115: newPVs.add(lon.head());
116: lon = lon.tail();
117: }
118: }
119:
120: public HashSet getStatements() {
121: if (sb != null) {
122: return getStatements(sb);
123: }
124: return new HashSet();
125: }
126:
127: private HashSet getStatements(StatementBlock sbl) {
128: HashSet result = new HashSet();
129: for (int i = 0; i < sbl.getChildCount(); i++) {
130: Statement s = sbl.getStatementAt(i);
131: if (s instanceof StatementBlock) {
132: result.addAll(getStatements((StatementBlock) s));
133: } else if (s instanceof MethodBodyStatement) {
134: JavaASTCollector coll = new JavaASTCollector(
135: ((MethodBodyStatement) s).getBody(serv),
136: Statement.class);
137: coll.start();
138: ListOfProgramElement l = coll.getNodes();
139: IteratorOfProgramElement it = l.iterator();
140: while (it.hasNext()) {
141: Statement next = (Statement) it.next();
142: if (!(next instanceof StatementContainer)) {
143: result.add(next);
144: }
145: }
146: } else {
147: result.add(s);
148: }
149: }
150: return result;
151: }
152:
153: public Node getNodeForCodeExtraction(ExecutionTraceModel tr) {
154: Node node = tr.getFirstTraceElement().node();
155: while (!node.root()) {
156: node = node.parent();
157: }
158: while (node.childrenCount() == 1
159: && node != tr.getFirstTraceElement().node()) {
160: node = node.child(0);
161: }
162: return node;
163: }
164:
165: private ListOfStatement flatten(StatementBlock sb) {
166: ListOfStatement result = SLListOfStatement.EMPTY_LIST;
167: for (int i = 0; i < sb.getStatementCount(); i++) {
168: if (fileName == null) {
169: fileName = sb.getStatementAt(i).getPositionInfo()
170: .getFileName();
171: }
172: if (sb.getStatementAt(i) instanceof StatementBlock) {
173: result = result.append(flatten((StatementBlock) sb
174: .getStatementAt(i)));
175: } else if (sb.getStatementAt(i) instanceof MethodBodyStatement) {
176: result = result
177: .append(convertMBSToMethodCall((MethodBodyStatement) sb
178: .getStatementAt(i)));
179: } else {
180: result = result.append(sb.getStatementAt(i));
181: }
182: }
183: return result;
184: }
185:
186: /**
187: * Returns the formula from which an oracle for the extracted code can
188: * be created.
189: */
190: public Term getTermForOracle() {
191: if (post == null) {
192: extractTestCode();
193: }
194: return post;
195: }
196:
197: /**
198: * Returns the package the code under test is located in.
199: */
200: public PackageReference getPackage() {
201: if (context == null) {
202: extractTestCode();
203: }
204: return context;
205: }
206:
207: /**
208: * Transforms updates into assignment expressions.
209: */
210: private ListOfStatement getAssignments(Term t) {
211: ListOfStatement result = SLListOfStatement.EMPTY_LIST;
212: IUpdateOperator uop = (IUpdateOperator) t.op();
213: for (int i = 0; i < uop.locationCount(); i++) {
214: Expression l, r;
215: l = (Expression) convertToProgramElement(uop.location(t, i));
216: r = (Expression) convertToProgramElement(uop.value(t, i));
217: result = result.append(TestGenerator.assignmentOrSet(l, r,
218: serv));
219: }
220: return result;
221: }
222:
223: public Expression convertToProgramElement(Term t) {
224: t = TestGenerator.replaceConstants(t, serv, newPVs);
225: return serv.getTypeConverter().convertToProgramElement(t);
226: }
227:
228: /**
229: * Returns the program variables newly introduced as substitution for
230: * skolem constants and those found in the IUT.
231: */
232: public SetOfProgramVariable getNewProgramVariables() {
233: SetOfProgramVariable result = SetAsListOfProgramVariable.EMPTY_SET;
234: IteratorOfNamed it = newPVs.allElements().iterator();
235: while (it.hasNext()) {
236: result = result.add((ProgramVariable) it.next());
237: }
238: return result;
239: }
240:
241: private Statement convertMBSToMethodCall(MethodBodyStatement mbs) {
242: methodName = mbs.getProgramMethod(serv).getMethodDeclaration()
243: .getName();
244: String sortName = mbs.getProgramMethod(serv).getContainerType()
245: .getSort().name().toString();
246: fileName = sortName.substring(sortName.lastIndexOf(".") + 1,
247: sortName.length());
248: // if(sortName.lastIndexOf(".")!=-1){
249: // packageName = sortName.substring(0, sortName.lastIndexOf("."));
250: // }
251: MethodReference mr = new MethodReference(mbs.getArguments(),
252: new ProgramElementName(mbs.getProgramMethod(serv)
253: .getName()), mbs.getProgramMethod(serv)
254: .isStatic() ? new TypeRef(mbs.getProgramMethod(
255: serv).getContainerType()) : mbs
256: .getDesignatedContext());
257: context = mbs.getProgramMethod(serv).getContainerType()
258: .createPackagePrefix();
259: if (mbs.getResultVariable() != null) {
260: ProgramVariable rv = (ProgramVariable) mbs
261: .getResultVariable();
262: newPVs.add(rv);
263: return new CopyAssignment(rv, mr);
264: } else {
265: return mr;
266: }
267: }
268:
269: public String getFileName() {
270: return (fileName == null ? "Generic" : fileName)
271: + (testCounter++);
272: }
273:
274: // public String getPackageName(){
275: // return packageName;
276: // }
277:
278: public String getMethodName() {
279: return (methodName == null ? "code" : methodName);
280: }
281:
282: }
|