klee
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 "ExecutionState.h"
13
14#include "klee/Config/Version.h"
17#include "klee/Solver/Solver.h"
18
19#include "CoreStats.h"
20
21using namespace klee;
22using namespace llvm;
23
24/***/
25
26bool TimingSolver::evaluate(const ConstraintSet &constraints, ref<Expr> expr,
27 Solver::Validity &result,
28 SolverQueryMetaData &metaData) {
29 // Fast path, to avoid timer and OS overhead.
30 if (ConstantExpr *CE = dyn_cast<ConstantExpr>(expr)) {
31 result = CE->isTrue() ? Solver::True : Solver::False;
32 return true;
33 }
34
36
37 if (simplifyExprs)
38 expr = ConstraintManager::simplifyExpr(constraints, expr);
39
40 bool success = solver->evaluate(Query(constraints, expr), result);
41
42 metaData.queryCost += timer.delta();
43
44 return success;
45}
46
47bool TimingSolver::mustBeTrue(const ConstraintSet &constraints, ref<Expr> expr,
48 bool &result, SolverQueryMetaData &metaData) {
49 // Fast path, to avoid timer and OS overhead.
50 if (ConstantExpr *CE = dyn_cast<ConstantExpr>(expr)) {
51 result = CE->isTrue() ? true : false;
52 return true;
53 }
54
56
57 if (simplifyExprs)
58 expr = ConstraintManager::simplifyExpr(constraints, expr);
59
60 bool success = solver->mustBeTrue(Query(constraints, expr), result);
61
62 metaData.queryCost += timer.delta();
63
64 return success;
65}
66
68 bool &result, SolverQueryMetaData &metaData) {
69 return mustBeTrue(constraints, Expr::createIsZero(expr), result, metaData);
70}
71
72bool TimingSolver::mayBeTrue(const ConstraintSet &constraints, ref<Expr> expr,
73 bool &result, SolverQueryMetaData &metaData) {
74 bool res;
75 if (!mustBeFalse(constraints, expr, res, metaData))
76 return false;
77 result = !res;
78 return true;
79}
80
81bool TimingSolver::mayBeFalse(const ConstraintSet &constraints, ref<Expr> expr,
82 bool &result, SolverQueryMetaData &metaData) {
83 bool res;
84 if (!mustBeTrue(constraints, expr, res, metaData))
85 return false;
86 result = !res;
87 return true;
88}
89
90bool TimingSolver::getValue(const ConstraintSet &constraints, ref<Expr> expr,
91 ref<ConstantExpr> &result,
92 SolverQueryMetaData &metaData) {
93 // Fast path, to avoid timer and OS overhead.
94 if (ConstantExpr *CE = dyn_cast<ConstantExpr>(expr)) {
95 result = CE;
96 return true;
97 }
98
100
101 if (simplifyExprs)
102 expr = ConstraintManager::simplifyExpr(constraints, expr);
103
104 bool success = solver->getValue(Query(constraints, expr), result);
105
106 metaData.queryCost += timer.delta();
107
108 return success;
109}
110
112 const ConstraintSet &constraints, const std::vector<const Array *> &objects,
113 std::vector<std::vector<unsigned char>> &result,
114 SolverQueryMetaData &metaData) {
115 if (objects.empty())
116 return true;
117
119
120 bool success = solver->getInitialValues(
121 Query(constraints, ConstantExpr::alloc(0, Expr::Bool)), objects, result);
122
123 metaData.queryCost += timer.delta();
124
125 return success;
126}
127
128std::pair<ref<Expr>, ref<Expr>>
130 SolverQueryMetaData &metaData) {
132 auto result = solver->getRange(Query(constraints, expr));
133 metaData.queryCost += timer.delta();
134 return result;
135}
static ref< ConstantExpr > alloc(const llvm::APInt &v)
Definition: Expr.h:1065
static ref< Expr > simplifyExpr(const ConstraintSet &constraints, const ref< Expr > &expr)
Definition: Constraints.cpp:92
static ref< Expr > createIsZero(ref< Expr > e)
Definition: Expr.cpp:322
static const Width Bool
Definition: Expr.h:100
bool mayBeFalse(const ConstraintSet &, ref< Expr >, bool &result, SolverQueryMetaData &metaData)
bool getInitialValues(const ConstraintSet &, const std::vector< const Array * > &objects, std::vector< std::vector< unsigned char > > &result, SolverQueryMetaData &metaData)
bool getValue(const ConstraintSet &, ref< Expr > expr, ref< ConstantExpr > &result, SolverQueryMetaData &metaData)
bool mustBeFalse(const ConstraintSet &, ref< Expr >, bool &result, SolverQueryMetaData &metaData)
bool mayBeTrue(const ConstraintSet &, ref< Expr >, bool &result, SolverQueryMetaData &metaData)
bool mustBeTrue(const ConstraintSet &, ref< Expr >, bool &result, SolverQueryMetaData &metaData)
std::pair< ref< Expr >, ref< Expr > > getRange(const ConstraintSet &, ref< Expr > query, SolverQueryMetaData &metaData)
std::unique_ptr< Solver > solver
Definition: TimingSolver.h:29
Statistic solverTime
Definition: main.cpp:291
time::Span queryCost
Costs for all queries issued for this state.
Definition: Solver.h:29