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.reference.PackageReference;
012: import de.uka.ilkd.key.java.statement.MethodFrame;
013: import de.uka.ilkd.key.java.visitor.JavaASTCollector;
014: import de.uka.ilkd.key.logic.*;
015: import de.uka.ilkd.key.logic.op.*;
016: import de.uka.ilkd.key.proof.*;
017: import de.uka.ilkd.key.visualization.*;
018:
019: import java.util.*;
020:
021: /**
022: * Generates a unittest from a proof or a node in a proof-tree.
023: */
024: public class UnitTestBuilder {
025:
026: private HashMap node2trace;
027:
028: private Services serv;
029: private Constraint uc;
030: // the nodes containing trace ends that have already been processed by the
031: // proof visualization
032: private HashSet traceEndNodes;
033: private PackageReference pr;
034: private int coverage;
035: // iff true only terminated traces are considered for test case generation
036: public static boolean requireCompleteExecution = false;
037:
038: public Namespace pvn;
039:
040: private String directory = null;
041:
042: public UnitTestBuilder(Services serv, Proof p) {
043: this .serv = serv;
044: node2trace = new HashMap();
045: uc = p.getUserConstraint().getConstraint();
046: traceEndNodes = new HashSet();
047: pvn = p.getNamespaces().programVariables();
048: }
049:
050: public UnitTestBuilder(Services serv, Proof p, String directory) {
051: this (serv, p);
052: this .directory = directory;
053: }
054:
055: /**
056: * Returns the program methods that are symbolically executed in the
057: * implementation under test <code>p</code>.
058: */
059: public SetOfProgramMethod getProgramMethods(Proof p) {
060: IteratorOfNode it = p.root().leavesIterator();
061: SetOfProgramMethod result = SetAsListOfProgramMethod.EMPTY_SET;
062: while (it.hasNext()) {
063: Node n = it.next();
064: ExecutionTraceModel[] tr = getTraces(n);
065: result = result.union(getProgramMethods(tr));
066: }
067: return result;
068: }
069:
070: public SetOfProgramMethod getProgramMethods(ListOfNode nodes) {
071: IteratorOfNode it = nodes.iterator();
072: SetOfProgramMethod result = SetAsListOfProgramMethod.EMPTY_SET;
073: while (it.hasNext()) {
074: Node n = it.next();
075: ExecutionTraceModel[] tr = getTraces(n);
076: result = result.union(getProgramMethods(tr));
077: }
078: return result;
079: }
080:
081: private ExecutionTraceModel[] getTraces(Node n) {
082: ExecutionTraceModel[] tr = (ExecutionTraceModel[]) node2trace
083: .get(n);
084: if (tr == null) {
085: ProofVisualization pv = new ProofVisualization(n, serv,
086: traceEndNodes, true);
087: tr = pv.getVisualizationModel().getExecutionTraces();
088: node2trace.put(n, tr);
089: }
090: return tr;
091: }
092:
093: private HashSet getStatements(ExecutionTraceModel[] tr) {
094: HashSet result = new HashSet();
095: for (int i = 0; i < tr.length; i++) {
096: result.addAll(tr[i].getExecutedStatementPositions());
097: }
098: return result;
099: }
100:
101: /**
102: * Creates unit tests for execution traces containing at least one
103: * of the methods in pms. Only execution traces on branches that end with
104: * one of the nodes iterated by <code>it</code> are considered.
105: */
106: private String createTestForNodes(IteratorOfNode it,
107: SetOfProgramMethod pms) {
108: TestGenerator tg = null;
109: String methodName = null;
110: Statement[] code = null;
111: Term oracle = null;
112: LinkedList mgs = new LinkedList();
113:
114: HashSet nodesAlreadyProcessed = new HashSet();
115:
116: SetOfProgramVariable pvs = null;
117:
118: // the statements occuring in the considered execution traces
119: HashSet statements = new HashSet();
120:
121: TestCodeExtractor tce = null;
122:
123: while (it.hasNext()) {
124: Node n = it.next();
125:
126: ExecutionTraceModel[] tr = getTraces(n);
127:
128: statements.addAll(getStatements(tr));
129: int maxRating = -1;
130:
131: // boolean traceFound = false;
132: for (int i = 0; i < tr.length; i++) {
133: if (tr[i].getRating() == 0
134: || (!tr[i].blockCompletelyExecuted() && requireCompleteExecution)
135: || (!tr[i].blockCompletelyExecuted())
136: && n.isClosed()
137: || tr[i].getProgramMethods(serv).union(pms)
138: .size() == tr[i]
139: .getProgramMethods(serv).size()
140: + pms.size()
141: || nodesAlreadyProcessed.contains(tr[i]
142: .getLastTraceElement().node())
143: || tr[i].getLastTraceElement()
144: .getPosOfModality().isInAntec()
145: || tr[i].getFirstContextTraceElement() == TraceElement.END /*||
146: tr[i].getType() != ExecutionTraceModel.TYPE1*/) {
147: continue;
148: }
149: // nodesAlreadyProcessed.add(tr[i].getLastTraceElement().node());
150: if (maxRating == -1
151: || tr[i].getRating() > tr[maxRating]
152: .getRating()) {
153: maxRating = i;
154: }
155: if (tg == null) {
156: tce = new TestCodeExtractor(tr[i], serv, pvn);
157: code = tce.extractTestCode();
158: JavaASTCollector coll = new JavaASTCollector(
159: new StatementBlock(code), MethodFrame.class);
160: coll.start();
161: if (coll.getNodes().size() == 0) {
162: tg = new TestGenerator(serv, "Test"
163: + tce.getFileName(), directory);
164: if (methodName == null) {
165: methodName = tce.getMethodName();
166: }
167: oracle = tce.getTermForOracle();
168: pvs = tce.getNewProgramVariables();
169: //tr[i].getFirstTraceElement().
170: //node().getGlobalProgVars().
171: //union(tce.getNewProgramVariables());
172: tce.getNewProgramVariables();
173: pr = tce.getPackage();
174: }
175: }
176: }
177: if (maxRating != -1) {
178: mgs.add(getModelGenerator(tr[maxRating], n));
179: nodesAlreadyProcessed.add(tr[maxRating]
180: .getLastTraceElement().node());
181: }
182: }
183: if (methodName == null) {
184: throw new UnitTestException(
185: "no suitable Execution Trace found");
186: }
187: computeStatementCoverage(statements, tce.getStatements());
188: tg.generateTestSuite(code, oracle, mgs, pvs, "test"
189: + methodName, pr);
190: return tg.getPath();
191: }
192:
193: /**
194: * Creates a Unittest for the node <code>n</code>. The testdata is derived
195: * only from <code>n</code>.
196: */
197: public String createTestForNode(Node n) {
198: ExecutionTraceModel[] tr = getTraces(n);
199: ListOfNode l = SLListOfNode.EMPTY_LIST.append(n);
200: return createTestForNodes(l.iterator(), getProgramMethods(tr));
201: }
202:
203: public String createTestForNodes(ListOfNode l) {
204: return createTestForNodes(l.iterator(), getProgramMethods(l));
205: }
206:
207: private void computeStatementCoverage(HashSet executedStatements,
208: HashSet sourceStatements) {
209: if (sourceStatements.size() == 0) {
210: coverage = -1;
211: } else {
212: int i = 0;
213: Iterator it = sourceStatements.iterator();
214: while (it.hasNext()) {
215: Statement s = (Statement) it.next();
216: if (executedStatements.contains(s.getPositionInfo()
217: .getStartPosition())) {
218: i++;
219: }
220: }
221: coverage = (100 * i) / sourceStatements.size();
222: }
223: }
224:
225: private boolean isInteresting(ExecutionTraceModel tr) {
226: return tr.getRating() != 0
227: && !tr.getLastTraceElement().getPosOfModality()
228: .isInAntec()
229: && (!requireCompleteExecution || tr
230: .blockCompletelyExecuted());
231: }
232:
233: private SetOfProgramMethod getProgramMethods(
234: ExecutionTraceModel[] traces) {
235: SetOfProgramMethod result = SetAsListOfProgramMethod.EMPTY_SET;
236: for (int i = 0; i < traces.length; i++) {
237: if (isInteresting(traces[i])) {
238: result = result
239: .union(traces[i].getProgramMethods(serv));
240: }
241: }
242: return result;
243: }
244:
245: /**
246: * Returns the percentage of covered statements.
247: */
248: public int getStatementCoverage() {
249: return coverage;
250: }
251:
252: /**
253: * Creates a Unittest for the proof <code>p</code>. The testdata is derived
254: * from the leaves of <code>p</code>'s proof tree.
255: */
256: public String createTestForProof(Proof p) {
257: IteratorOfNode it = p.root().leavesIterator();
258: return createTestForNodes(it, getProgramMethods(p));
259: }
260:
261: /**
262: * Creates a Unittest for those branches in the proof tree of
263: * <code>p</code> on which at least one of the program methods in pms is
264: * symbolically executed.
265: * The testdata is derived from the leaves of <code>p</code>'s proof tree.
266: */
267: public String createTestForProof(Proof p, SetOfProgramMethod pms) {
268: IteratorOfNode it = p.root().leavesIterator();
269: return createTestForNodes(it, pms);
270: }
271:
272: private ModelGenerator getModelGenerator(ExecutionTraceModel tr,
273: Node n) {
274: return new ModelGenerator(serv, uc, tr.getLastTraceElement()
275: .node(), tr.toString(), n);
276: }
277:
278: }
|