 |
|
 |
|
| Files: |
1 |
|
Branches Taken: |
66.7% |
16 / 24 |
| Generated: |
2009-05-17 22:47 |
|
Branches Executed: |
91.7% |
22 / 24 |
| |
|
Line Coverage: |
90.0% |
54 / 60 |
| |
 |
|
 |
1 : /* -*- mode: c++; c-basic-offset: 2; -*- */
2 :
3 : #include "TimingSolver.h"
4 :
5 : #include "klee/ExecutionState.h"
6 : #include "klee/Solver.h"
7 : #include "klee/Statistics.h"
8 :
9 : #include "CoreStats.h"
10 :
11 : #include "llvm/System/Process.h"
12 :
13 : using namespace klee;
14 : using namespace llvm;
15 :
16 : /***/
17 :
18 : bool TimingSolver::evaluate(const ExecutionState& state, ref<Expr> expr,
19 848044: Solver::Validity &result) {
20 : // Fast path, to avoid timer and OS overhead.
846757: branch 0 taken
1287: branch 1 taken
21 848044: if (expr.isConstant()) {
840589: branch 0 taken
6168: branch 1 taken
22 846757: result = expr.getConstantValue() ? Solver::True : Solver::False;
23 846757: return true;
24 : }
25 :
26 : sys::TimeValue now(0,0),user(0,0),delta(0,0),sys(0,0);
27 1287: sys::Process::GetTimeUsage(now,user,sys);
28 :
1287: branch 0 taken
0: branch 1 not taken
29 1287: if (simplifyExprs)
30 1287: expr = state.constraints.simplifyExpr(expr);
31 :
32 3861: bool success = solver->evaluate(Query(state.constraints, expr), result);
33 :
34 1287: sys::Process::GetTimeUsage(delta,user,sys);
35 : delta -= now;
36 1287: stats::solverTime += delta.usec();
37 2574: state.queryCost += delta.usec()/1000000.;
38 :
39 1287: return success;
40 : }
41 :
42 : bool TimingSolver::mustBeTrue(const ExecutionState& state, ref<Expr> expr,
43 3407537: bool &result) {
44 : // Fast path, to avoid timer and OS overhead.
3406033: branch 0 taken
1504: branch 1 taken
45 3407537: if (expr.isConstant()) {
46 3406033: result = expr.getConstantValue() ? true : false;
47 3406033: return true;
48 : }
49 :
50 : sys::TimeValue now(0,0),user(0,0),delta(0,0),sys(0,0);
51 1504: sys::Process::GetTimeUsage(now,user,sys);
52 :
1504: branch 0 taken
0: branch 1 not taken
53 1504: if (simplifyExprs)
54 1504: expr = state.constraints.simplifyExpr(expr);
55 :
56 4512: bool success = solver->mustBeTrue(Query(state.constraints, expr), result);
57 :
58 1504: sys::Process::GetTimeUsage(delta,user,sys);
59 : delta -= now;
60 1504: stats::solverTime += delta.usec();
61 3008: state.queryCost += delta.usec()/1000000.;
62 :
63 1504: return success;
64 : }
65 :
66 : bool TimingSolver::mustBeFalse(const ExecutionState& state, ref<Expr> expr,
67 1064: bool &result) {
68 1064: return mustBeTrue(state, Expr::createNot(expr), result);
69 : }
70 :
71 : bool TimingSolver::mayBeTrue(const ExecutionState& state, ref<Expr> expr,
72 1034: bool &result) {
73 : bool res;
0: branch 2 not taken
1034: branch 3 taken
74 1034: if (!mustBeFalse(state, expr, res))
75 0: return false;
76 1034: result = !res;
77 1034: return true;
78 : }
79 :
80 : bool TimingSolver::mayBeFalse(const ExecutionState& state, ref<Expr> expr,
81 0: bool &result) {
82 : bool res;
0: branch 2 not taken
0: branch 3 not taken
83 0: if (!mustBeTrue(state, expr, res))
84 0: return false;
85 0: result = !res;
86 0: return true;
87 : }
88 :
89 : bool TimingSolver::getValue(const ExecutionState& state, ref<Expr> expr,
90 531: ref<Expr> &result) {
91 : // Fast path, to avoid timer and OS overhead.
99: branch 0 taken
432: branch 1 taken
92 531: if (expr.isConstant()) {
93 99: result = expr;
94 99: return true;
95 : }
96 :
97 : sys::TimeValue now(0,0),user(0,0),delta(0,0),sys(0,0);
98 432: sys::Process::GetTimeUsage(now,user,sys);
99 :
432: branch 0 taken
0: branch 1 not taken
100 432: if (simplifyExprs)
101 432: expr = state.constraints.simplifyExpr(expr);
102 :
103 1296: bool success = solver->getValue(Query(state.constraints, expr), result);
104 :
105 432: sys::Process::GetTimeUsage(delta,user,sys);
106 : delta -= now;
107 432: stats::solverTime += delta.usec();
108 864: state.queryCost += delta.usec()/1000000.;
109 :
110 432: return success;
111 : }
112 :
113 : bool
114 : TimingSolver::getInitialValues(const ExecutionState& state,
115 : const std::vector<const MemoryObject*>
116 : &objects,
117 : std::vector< std::vector<unsigned char> >
118 663: &result) {
29: branch 0 taken
634: branch 1 taken
119 663: if (objects.empty())
120 29: return true;
121 :
122 : sys::TimeValue now(0,0),user(0,0),delta(0,0),sys(0,0);
123 634: sys::Process::GetTimeUsage(now,user,sys);
124 :
125 : bool success = solver->getInitialValues(Query(state.constraints,
126 : ref<Expr>(0, Expr::Bool)),
127 1902: objects, result);
128 :
129 634: sys::Process::GetTimeUsage(delta,user,sys);
130 : delta -= now;
131 634: stats::solverTime += delta.usec();
132 1268: state.queryCost += delta.usec()/1000000.;
133 :
134 634: return success;
135 : }
136 :
137 : std::pair< ref<Expr>, ref<Expr> >
138 6: TimingSolver::getRange(const ExecutionState& state, ref<Expr> expr) {
139 24: return solver->getRange(Query(state.constraints, expr));
103: branch 0 taken
0: branch 1 not taken
103: branch 2 taken
0: branch 3 not taken
140 206: }
Generated: 2009-05-17 22:47 by zcov