1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
|
//===-- SolverImpl.h --------------------------------------------*- C++ -*-===//
//
// The KLEE Symbolic Virtual Machine
//
// This file is distributed under the University of Illinois Open Source
// License. See LICENSE.TXT for details.
//
//===----------------------------------------------------------------------===//
#ifndef KLEE_SOLVERIMPL_H
#define KLEE_SOLVERIMPL_H
#include "klee/System/Time.h"
#include "Solver.h"
#include <vector>
namespace klee {
class Array;
class ExecutionState;
class Expr;
struct Query;
/// SolverImpl - Abstract base clase for solver implementations.
class SolverImpl {
public:
SolverImpl() = default;
SolverImpl(const SolverImpl&) = delete;
SolverImpl& operator=(const SolverImpl&) = delete;
virtual ~SolverImpl();
enum SolverRunStatus { SOLVER_RUN_STATUS_SUCCESS_SOLVABLE,
SOLVER_RUN_STATUS_SUCCESS_UNSOLVABLE,
SOLVER_RUN_STATUS_FAILURE,
SOLVER_RUN_STATUS_TIMEOUT,
SOLVER_RUN_STATUS_FORK_FAILED,
SOLVER_RUN_STATUS_INTERRUPTED,
SOLVER_RUN_STATUS_UNEXPECTED_EXIT_CODE,
SOLVER_RUN_STATUS_WAITPID_FAILED };
/// computeValidity - Compute a full validity result for the
/// query.
///
/// The query expression is guaranteed to be non-constant and have
/// bool type.
///
/// SolverImpl provides a default implementation which uses
/// computeTruth. Clients should override this if a more efficient
/// implementation is available.
///
/// \param [out] result - if
/// \f[ \forall X constraints(X) \to query(X) \f]
/// then Solver::True,
/// else if
/// \f[ \forall X constraints(X) \to \lnot query(X) \f]
/// then Solver::False,
/// else
/// Solver::Unknown
///
/// \return True on success
virtual bool computeValidity(const Query& query, Solver::Validity &result);
/// computeTruth - Determine whether the given query expression is provably true
/// given the constraints.
///
/// The query expression is guaranteed to be non-constant and have
/// bool type.
///
/// This method should evaluate the logical formula:
///
/// \f[ \forall X constraints(X) \to query(X) \f]
///
/// Where \f$X\f$ is some assignment, \f$constraints(X)\f$ are the constraints
/// in the query and \f$query(X)\f$ is the query expression.
///
/// \param [out] isValid - On success, true iff the logical formula is true.
/// \return True on success
virtual bool computeTruth(const Query& query, bool &isValid) = 0;
/// computeValue - Compute a feasible value for the expression.
///
/// The query expression is guaranteed to be non-constant.
///
/// \return True on success
virtual bool computeValue(const Query& query, ref<Expr> &result) = 0;
/// \sa Solver::getInitialValues()
virtual bool computeInitialValues(const Query& query,
const std::vector<const Array*>
&objects,
std::vector< std::vector<unsigned char> >
&values,
bool &hasSolution) = 0;
/// getOperationStatusCode - get the status of the last solver operation
virtual SolverRunStatus getOperationStatusCode() = 0;
/// getOperationStatusString - get string representation of the operation
/// status code
static const char* getOperationStatusString(SolverRunStatus statusCode);
virtual std::string getConstraintLog(const Query &query) {
// dummy
return {};
}
virtual void setCoreSolverTimeout(time::Span timeout) {};
};
}
#endif /* KLEE_SOLVERIMPL_H */
|
