klee
 All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
TimingSolver.cpp
Go to the documentation of this file.
1 //===-- TimingSolver.cpp --------------------------------------------------===//
2 //
3 // The KLEE Symbolic Virtual Machine
4 //
5 // This file is distributed under the University of Illinois Open Source
6 // License. See LICENSE.TXT for details.
7 //
8 //===----------------------------------------------------------------------===//
9 
10 #include "TimingSolver.h"
11 
12 #include "klee/Config/Version.h"
13 #include "klee/ExecutionState.h"
14 #include "klee/Solver.h"
15 #include "klee/Statistics.h"
16 
17 #include "CoreStats.h"
18 
19 #include "llvm/Support/Process.h"
20 
21 using namespace klee;
22 using namespace llvm;
23 
24 /***/
25 
27  Solver::Validity &result) {
28  // Fast path, to avoid timer and OS overhead.
29  if (ConstantExpr *CE = dyn_cast<ConstantExpr>(expr)) {
30  result = CE->isTrue() ? Solver::True : Solver::False;
31  return true;
32  }
33 
34  sys::TimeValue now(0,0),user(0,0),delta(0,0),sys(0,0);
35  sys::Process::GetTimeUsage(now,user,sys);
36 
37  if (simplifyExprs)
38  expr = state.constraints.simplifyExpr(expr);
39 
40  bool success = solver->evaluate(Query(state.constraints, expr), result);
41 
42  sys::Process::GetTimeUsage(delta,user,sys);
43  delta -= now;
44  stats::solverTime += delta.usec();
45  state.queryCost += delta.usec()/1000000.;
46 
47  return success;
48 }
49 
51  bool &result) {
52  // Fast path, to avoid timer and OS overhead.
53  if (ConstantExpr *CE = dyn_cast<ConstantExpr>(expr)) {
54  result = CE->isTrue() ? true : false;
55  return true;
56  }
57 
58  sys::TimeValue now(0,0),user(0,0),delta(0,0),sys(0,0);
59  sys::Process::GetTimeUsage(now,user,sys);
60 
61  if (simplifyExprs)
62  expr = state.constraints.simplifyExpr(expr);
63 
64  bool success = solver->mustBeTrue(Query(state.constraints, expr), result);
65 
66  sys::Process::GetTimeUsage(delta,user,sys);
67  delta -= now;
68  stats::solverTime += delta.usec();
69  state.queryCost += delta.usec()/1000000.;
70 
71  return success;
72 }
73 
75  bool &result) {
76  return mustBeTrue(state, Expr::createIsZero(expr), result);
77 }
78 
80  bool &result) {
81  bool res;
82  if (!mustBeFalse(state, expr, res))
83  return false;
84  result = !res;
85  return true;
86 }
87 
89  bool &result) {
90  bool res;
91  if (!mustBeTrue(state, expr, res))
92  return false;
93  result = !res;
94  return true;
95 }
96 
98  ref<ConstantExpr> &result) {
99  // Fast path, to avoid timer and OS overhead.
100  if (ConstantExpr *CE = dyn_cast<ConstantExpr>(expr)) {
101  result = CE;
102  return true;
103  }
104 
105  sys::TimeValue now(0,0),user(0,0),delta(0,0),sys(0,0);
106  sys::Process::GetTimeUsage(now,user,sys);
107 
108  if (simplifyExprs)
109  expr = state.constraints.simplifyExpr(expr);
110 
111  bool success = solver->getValue(Query(state.constraints, expr), result);
112 
113  sys::Process::GetTimeUsage(delta,user,sys);
114  delta -= now;
115  stats::solverTime += delta.usec();
116  state.queryCost += delta.usec()/1000000.;
117 
118  return success;
119 }
120 
121 bool
123  const std::vector<const Array*>
124  &objects,
125  std::vector< std::vector<unsigned char> >
126  &result) {
127  if (objects.empty())
128  return true;
129 
130  sys::TimeValue now(0,0),user(0,0),delta(0,0),sys(0,0);
131  sys::Process::GetTimeUsage(now,user,sys);
132 
133  bool success = solver->getInitialValues(Query(state.constraints,
135  objects, result);
136 
137  sys::Process::GetTimeUsage(delta,user,sys);
138  delta -= now;
139  stats::solverTime += delta.usec();
140  state.queryCost += delta.usec()/1000000.;
141 
142  return success;
143 }
144 
145 std::pair< ref<Expr>, ref<Expr> >
147  return solver->getRange(Query(state.constraints, expr));
148 }
bool getInitialValues(const ExecutionState &, const std::vector< const Array * > &objects, std::vector< std::vector< unsigned char > > &result)
static ref< Expr > createIsZero(ref< Expr > e)
Definition: Expr.cpp:305
bool mayBeFalse(const ExecutionState &, ref< Expr >, bool &result)
bool mayBeTrue(const ExecutionState &, ref< Expr >, bool &result)
bool mustBeFalse(const ExecutionState &, ref< Expr >, bool &result)
static ref< ConstantExpr > alloc(const llvm::APInt &v)
Definition: Expr.h:398
Statistic solverTime
bool mustBeTrue(const ExecutionState &, ref< Expr >, bool &result)
ref< Expr > simplifyExpr(ref< Expr > e) const
Definition: Constraints.cpp:95
ConstraintManager constraints
static const Width Bool
Definition: Expr.h:97
std::pair< ref< Expr >, ref< Expr > > getRange(const ExecutionState &, ref< Expr > query)
bool getValue(const ExecutionState &, ref< Expr > expr, ref< ConstantExpr > &result)
bool evaluate(const ExecutionState &, ref< Expr >, Solver::Validity &result)