 |
|
 |
|
| Files: |
1 |
|
Branches Taken: |
50.0% |
15 / 30 |
| Generated: |
2009-05-17 22:47 |
|
Branches Executed: |
53.3% |
16 / 30 |
| |
|
Line Coverage: |
98.0% |
48 / 49 |
| |
 |
|
 |
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/ExprEvaluator.h"
13 : #include "klee/util/ExprVisitor.h"
14 : #include "klee/Internal/Support/QueryLog.h"
15 : #include "klee/Internal/Support/Serialize.h"
16 : #include "klee/Internal/System/Time.h"
17 :
18 : #include "llvm/Support/CommandLine.h"
19 :
20 : #include <iostream>
21 : #include <iomanip>
22 : #include <fstream>
23 :
24 : using namespace klee;
25 : using namespace llvm;
26 : using namespace klee::serialize;
27 : using namespace klee::util;
28 :
29 : ///
30 :
31 3507: QueryLogEntry::QueryLogEntry(const QueryLogEntry &b)
32 : : exprs(b.exprs),
33 : type(b.type),
34 : query(b.query),
35 : instruction(b.instruction),
36 7014: objects(b.objects) {}
37 :
38 : QueryLogEntry::QueryLogEntry(const Query& _query,
39 : Type _type,
40 807: const std::vector<const MemoryObject*> *_objects)
41 : : exprs(_query.constraints.begin(), _query.constraints.end()),
42 4035: type(_type), query(_query.expr) {
43 807: Statistic *S = theStatisticManager->getStatisticByName("Instructions");
807: branch 0 taken
0: branch 1 not taken
807: branch 3 taken
807: branch 4 taken
44 807: instruction = S ? S->getValue() : 0;
147: branch 0 taken
660: branch 1 taken
660: branch 2 taken
660: branch 3 taken
45 807: if (_objects)
46 147: objects = *_objects;
47 807: }
48 :
49 : ///
50 :
51 : class LoggingSolver : public SolverImpl {
52 : Solver *solver;
53 : std::ofstream outstream;
54 : OutBinArchive archive;
55 : std::vector< QueryLogEntry > persistence;
56 :
57 807: QueryLogEntry &addEntry(const QueryLogEntry &e) {
58 807: persistence.push_back(e);
59 1614: return persistence.back();
60 : }
61 :
62 : public:
63 : LoggingSolver(Solver *_solver, std::string path);
64 : ~LoggingSolver();
65 :
66 : bool computeTruth(const Query&, bool &isValid);
67 : bool computeValidity(const Query&, Solver::Validity &result);
68 : bool computeValue(const Query&, ref<Expr> &result);
69 : bool computeInitialValues(const Query&,
70 : const std::vector<const MemoryObject*> &objects,
71 : std::vector< std::vector<unsigned char> > &values,
72 : bool &hasSolution);
73 : };
74 :
75 2: LoggingSolver::LoggingSolver(Solver *_solver, std::string path)
76 : : solver(_solver),
77 : outstream(path.c_str(), std::ios::trunc|std::ios::binary),
78 10: archive(outstream, "QUERY_LOG", 2) {
0: branch 0 not taken
2: branch 1 taken
0: branch 3 not taken
0: branch 4 not taken
79 4: assert(outstream.good() && "unable to open log file");
80 2: }
81 :
82 2: LoggingSolver::~LoggingSolver() {
83 2: persistence.clear();
2: branch 0 taken
0: branch 1 not taken
2: branch 4 taken
2: branch 5 taken
0: branch 8 not taken
0: branch 9 not taken
84 2: delete solver;
2: branch 3 taken
0: branch 4 not taken
0: branch 9 not taken
0: branch 10 not taken
0: branch 15 not taken
0: branch 16 not taken
85 4: }
86 :
87 : bool LoggingSolver::computeValidity(const Query& query,
88 132: Solver::Validity &result) {
89 132: archive << addEntry(QueryLogEntry(query, QueryLogEntry::Validity));
90 132: double startTime = getWallTime();
91 132: bool success = solver->impl->computeValidity(query, result);
92 264: archive << QueryLogResult(success, result, getWallTime() - startTime);
93 132: return success;
94 : }
95 :
96 445: bool LoggingSolver::computeTruth(const Query& query, bool &isValid) {
97 445: archive << addEntry(QueryLogEntry(query, QueryLogEntry::Truth));
98 445: double startTime = getWallTime();
99 445: bool success = solver->impl->computeTruth(query, isValid);
100 890: archive << QueryLogResult(success, isValid, getWallTime() - startTime);
101 445: return success;
102 : }
103 :
104 83: bool LoggingSolver::computeValue(const Query& query, ref<Expr> &result) {
105 83: archive << addEntry(QueryLogEntry(query, QueryLogEntry::Value));
106 83: double startTime = getWallTime();
107 83: bool success = solver->impl->computeValue(query, result);
0: branch 0 not taken
83: branch 1 taken
108 83: if (!success)
109 0: result = ref<Expr>(0, query.expr.getWidth());
110 : archive << QueryLogResult(success, result.getConstantValue(),
111 249: getWallTime() - startTime);
112 83: return success;
113 : }
114 :
115 : bool LoggingSolver::computeInitialValues(const Query& query,
116 : const std::vector<const MemoryObject*> &objects,
117 : std::vector< std::vector<unsigned char> > &values,
118 147: bool &hasSolution) {
119 147: archive << addEntry(QueryLogEntry(query, QueryLogEntry::Cex, &objects));
120 147: double startTime = getWallTime();
121 : bool success = solver->impl->computeInitialValues(query, objects,
122 147: values, hasSolution);
123 294: archive << QueryLogResult(success, hasSolution, getWallTime() - startTime);
124 147: return success;
125 : }
126 :
127 : ///
128 :
129 2: Solver *klee::createLoggingSolver(Solver *_solver, std::string path) {
130 4: return new Solver(new LoggingSolver(_solver, path));
103: branch 0 taken
0: branch 1 not taken
103: branch 2 taken
0: branch 3 not taken
131 206: }
Generated: 2009-05-17 22:47 by zcov