 |
|
 |
|
| Files: |
1 |
|
Branches Taken: |
60.0% |
24 / 40 |
| Generated: |
2009-05-17 22:47 |
|
Branches Executed: |
80.0% |
32 / 40 |
| |
|
Line Coverage: |
86.9% |
53 / 61 |
| |
 |
|
 |
1 : /* -*- mode: c++; c-basic-offset: 2; -*- */
2 :
3 : #include "klee/Solver.h"
4 :
5 : // FIXME: This should not be here.
6 : #include "klee/ExecutionState.h"
7 : #include "klee/Expr.h"
8 : // FIXME: This should not be here.
9 : #include "klee/Memory.h"
10 : #include "klee/SolverImpl.h"
11 : #include "klee/Statistics.h"
12 : #include "klee/util/ExprPPrinter.h"
13 : #include "klee/Internal/Support/QueryLog.h"
14 : #include "klee/Internal/System/Time.h"
15 :
16 : #include "llvm/Support/CommandLine.h"
17 :
18 : #include <fstream>
19 :
20 : using namespace klee;
21 : using namespace llvm;
22 : using namespace klee::util;
23 :
24 : ///
25 :
26 : class PCLoggingSolver : public SolverImpl {
27 : Solver *solver;
28 : std::ofstream os;
29 : ExprPPrinter *printer;
30 : unsigned queryCount;
31 : double startTime;
32 :
33 17: void startQuery(const Query& query, const char *typeName) {
34 17: Statistic *S = theStatisticManager->getStatisticByName("Instructions");
17: branch 0 taken
0: branch 1 not taken
35 17: uint64_t instructions = S ? S->getValue() : 0;
36 : os << "# Query " << queryCount++ << " -- "
37 : << "Type: " << typeName << ", "
38 51: << "Instructions: " << instructions << "\n";
39 17: printer->printQuery(os, query.constraints, query.expr);
40 :
41 17: startTime = getWallTime();
42 17: }
43 :
44 17: void finishQuery(bool success) {
45 17: double delta = getWallTime() - startTime;
46 : os << "# " << (success ? "OK" : "FAIL") << " -- "
17: branch 0 taken
0: branch 1 not taken
47 34: << "Elapsed: " << delta << "\n";
48 17: }
49 :
50 : public:
51 : PCLoggingSolver(Solver *_solver, std::string path)
52 : : solver(_solver),
53 : os(path.c_str(), std::ios::trunc),
54 : printer(ExprPPrinter::create(os)),
55 3: queryCount(0) {
56 : }
57 1: ~PCLoggingSolver() {
1: branch 0 taken
0: branch 1 not taken
1: branch 3 taken
1: branch 4 taken
58 1: delete printer;
1: branch 0 taken
0: branch 1 not taken
1: branch 4 taken
1: branch 5 taken
59 1: delete solver;
1: branch 2 taken
0: branch 3 not taken
0: branch 7 not taken
0: branch 8 not taken
60 1: }
61 :
62 12: bool computeTruth(const Query& query, bool &isValid) {
63 12: startQuery(query, "Truth");
64 12: bool success = solver->impl->computeTruth(query, isValid);
65 12: finishQuery(success);
12: branch 0 taken
0: branch 1 not taken
66 12: if (success)
4: branch 0 taken
8: branch 1 taken
67 12: os << "# Is Valid: " << (isValid ? "true" : "false") << "\n";
68 12: os << "\n";
69 12: return success;
70 : }
71 :
72 0: bool computeValidity(const Query& query, Solver::Validity &result) {
73 0: startQuery(query, "Validity");
74 0: bool success = solver->impl->computeValidity(query, result);
75 0: finishQuery(success);
0: branch 0 not taken
0: branch 1 not taken
76 0: if (success)
77 0: os << "# Validity: " << result << "\n";
78 0: os << "\n";
79 0: return success;
80 : }
81 :
82 4: bool computeValue(const Query& query, ref<Expr> &result) {
83 4: startQuery(query, "Value");
84 4: bool success = solver->impl->computeValue(query, result);
85 4: finishQuery(success);
4: branch 0 taken
0: branch 1 not taken
86 4: if (success)
87 8: os << "# Result: " << result << "\n";
88 4: os << "\n";
89 4: return success;
90 : }
91 :
92 : bool computeInitialValues(const Query& query,
93 : const std::vector<const MemoryObject*> &objects,
94 : std::vector< std::vector<unsigned char> > &values,
95 1: bool &hasSolution) {
96 : // FIXME: Add objects to output.
97 1: startQuery(query, "InitialValues");
98 : bool success = solver->impl->computeInitialValues(query, objects,
99 1: values, hasSolution);
100 1: finishQuery(success);
1: branch 0 taken
0: branch 1 not taken
101 1: if (success) {
1: branch 0 taken
0: branch 1 not taken
102 1: os << "# Solvable: " << (hasSolution ? "true" : "false") << "\n";
1: branch 0 taken
0: branch 1 not taken
103 1: if (hasSolution) {
104 : std::vector< std::vector<unsigned char> >::iterator
105 : values_it = values.begin();
5: branch 0 taken
1: branch 1 taken
106 6: for (std::vector<const MemoryObject*>::const_iterator
107 : i = objects.begin(), e = objects.end(); i != e; ++i, ++values_it) {
108 5: const MemoryObject *obj = *i;
109 5: std::vector<unsigned char> &data = *values_it;
110 10: os << "# arr" << obj->id << " = [";
20: branch 0 taken
5: branch 1 taken
111 25: for (unsigned j=0; j<obj->size; j++) {
112 20: os << (int) data[j];
15: branch 0 taken
5: branch 1 taken
113 20: if (j+1<obj->size)
114 15: os << ",";
115 : }
116 5: os << "]\n";
117 : }
118 : }
119 : }
120 1: os << "\n";
121 1: return success;
122 : }
123 : };
124 :
125 : ///
126 :
127 1: Solver *klee::createPCLoggingSolver(Solver *_solver, std::string path) {
128 3: return new Solver(new PCLoggingSolver(_solver, path));
103: branch 0 taken
0: branch 1 not taken
103: branch 2 taken
0: branch 3 not taken
129 206: }
Generated: 2009-05-17 22:47 by zcov