 |
|
 |
|
| Files: |
1 |
|
Branches Taken: |
0.0% |
0 / 0 |
| Generated: |
2009-05-17 22:47 |
|
Branches Executed: |
0.0% |
0 / 0 |
| |
|
Line Coverage: |
88.9% |
8 / 9 |
| |
 |
|
 |
1 : //===- Solver.h - Constraint solver interface -------------------*- C++ -*-===//
2 :
3 : #ifndef KLEE_SOLVER_H
4 : #define KLEE_SOLVER_H
5 :
6 : #include "klee/Expr.h"
7 :
8 : #include <vector>
9 :
10 : namespace klee {
11 : class ConstraintManager;
12 : class Expr;
13 : class SolverImpl;
14 :
15 9094: struct Query {
16 : public:
17 : const ConstraintManager &constraints;
18 : ref<Expr> expr;
19 :
20 : Query(const ConstraintManager& _constraints, ref<Expr> _expr)
21 9094: : constraints(_constraints), expr(_expr) {
22 : }
23 :
24 : /// withExpr - Return a copy of the query with the given expression.
25 0: Query withExpr(ref<Expr> _expr) const {
26 810: return Query(constraints, _expr);
27 : }
28 :
29 : /// withFalse - Return a copy of the query with a false expression.
30 813: Query withFalse() const {
31 2439: return Query(constraints, ref<Expr>(0, Expr::Bool));
32 : }
33 :
34 : /// negateExpr - Return a copy of the query with the expression negated.
35 265: Query negateExpr() const {
36 810: return withExpr(Expr::createNot(expr));
37 : }
38 : };
39 :
40 : class Solver {
41 : // DO NOT IMPLEMENT.
42 : Solver(const Solver&);
43 : void operator=(const Solver&);
44 :
45 : public:
46 : enum Validity {
47 : True = 1,
48 : False = -1,
49 : Unknown = 0
50 : };
51 :
52 : public:
53 : /// validity_to_str - Return the name of given Validity enum value.
54 : static const char *validity_to_str(Validity v);
55 :
56 : public:
57 : SolverImpl *impl;
58 :
59 : public:
60 317: Solver(SolverImpl *_impl) : impl(_impl) {};
61 : ~Solver();
62 :
63 : /// evaluate - Determine the full validity of an expression in particular
64 : /// state.
65 : ////
66 : /// \param [out] result - The validity of the given expression (provably
67 : /// true, provably false, or neither).
68 : ///
69 : /// \return True on success.
70 : bool evaluate(const Query&, Validity &result);
71 :
72 : /// mustBeTrue - Determine if the expression is provably true.
73 : ///
74 : /// \param [out] result - On success, true iff the expresssion is provably
75 : /// false.
76 : ///
77 : /// \return True on success.
78 : bool mustBeTrue(const Query&, bool &result);
79 :
80 : /// mustBeFalse - Determine if the expression is provably false.
81 : ///
82 : /// \param [out] result - On success, true iff the expresssion is provably
83 : /// false.
84 : ///
85 : /// \return True on success.
86 : bool mustBeFalse(const Query&, bool &result);
87 :
88 : /// mayBeTrue - Determine if there is a valid assignment for the given state
89 : /// in which the expression evaluates to false.
90 : ///
91 : /// \param [out] result - On success, true iff the expresssion is true for
92 : /// some satisfying assignment.
93 : ///
94 : /// \return True on success.
95 : bool mayBeTrue(const Query&, bool &result);
96 :
97 : /// mayBeFalse - Determine if there is a valid assignment for the given
98 : /// state in which the expression evaluates to false.
99 : ///
100 : /// \param [out] result - On success, true iff the expresssion is false for
101 : /// some satisfying assignment.
102 : ///
103 : /// \return True on success.
104 : bool mayBeFalse(const Query&, bool &result);
105 :
106 : /// getValue - Compute one possible value for the given expression.
107 : ///
108 : /// \param [out] result - On success, a value for the expression in some
109 : /// satisying assignment.
110 : ///
111 : /// \return True on success.
112 : bool getValue(const Query&, ref<Expr> &result);
113 :
114 : /// getInitialValues - Compute the initial values for a list of objects.
115 : ///
116 : /// \param [out] result - On success, this vector will be filled in with an
117 : /// array of bytes for each given object (with length matching the object
118 : /// size). The bytes correspond to the initial values for the objects for
119 : /// some satisying assignment.
120 : ///
121 : /// \return True on success.
122 : ///
123 : /// NOTE: This function returns failure if there is no satisfying
124 : /// assignment.
125 : //
126 : // FIXME: This API is lame. We should probably just provide an API which
127 : // returns an Assignment object, then clients can get out whatever values
128 : // they want. This also allows us to optimize the representation.
129 : bool getInitialValues(const Query&,
130 : const std::vector<const MemoryObject*> &objects,
131 : std::vector< std::vector<unsigned char> > &result);
132 :
133 : /// getRange - Compute a tight range of possible values for a given
134 : /// expression.
135 : ///
136 : /// \return - A pair with (min, max) values for the expression.
137 : ///
138 : /// \post(mustBeTrue(min <= e <= max) &&
139 : /// mayBeTrue(min == e) &&
140 : /// mayBeTrue(max == e))
141 : //
142 : // FIXME: This should go into a helper class, and should handle failure.
143 : virtual std::pair< ref<Expr>, ref<Expr> > getRange(const Query&);
144 : };
145 :
146 : /// STPSolver - A complete solver based on STP.
147 : class STPSolver : public Solver {
148 : public:
149 : /// STPSolver - Construct a new STPSolver.
150 : ///
151 : /// \param useForkedSTP - Whether STP should be run in a separate process
152 : /// (required for using timeouts).
153 : STPSolver(bool useForkedSTP);
154 :
155 : /// getConstraintLog - Return the constraint log for the given state in CVC
156 : /// format.
157 : char *getConstraintLog(const Query&);
158 :
159 : /// setTimeout - Set constraint solver timeout delay to the given value; 0
160 : /// is off.
161 : void setTimeout(double timeout);
162 : };
163 :
164 : /* *** */
165 :
166 : /// createValidatingSolver - Create a solver which will validate all query
167 : /// results against an oracle, used for testing that an optimized solver has
168 : /// the same results as an unoptimized one. This solver will assert on any
169 : /// mismatches.
170 : ///
171 : /// \param s - The primary underlying solver to use.
172 : /// \param oracle - The solver to check query results against.
173 : Solver *createValidatingSolver(Solver *s, Solver *oracle);
174 :
175 : /// createCachingSolver - Create a solver which will cache the queries in
176 : /// memory (without eviction).
177 : ///
178 : /// \param s - The underlying solver to use.
179 : Solver *createCachingSolver(Solver *s);
180 :
181 : /// createCexCachingSolver - Create a counterexample caching solver. This is a
182 : /// more sophisticated cache which records counterexamples for a constraint
183 : /// set and uses subset/superset relations among constraints to try and
184 : /// quickly find satisfying assignments.
185 : ///
186 : /// \param s - The underlying solver to use.
187 : Solver *createCexCachingSolver(Solver *s);
188 :
189 : /// createFastCexSolver - Create a "fast counterexample solver", which tries
190 : /// to quickly compute a satisfying assignment for a constraint set using
191 : /// value propogation and range analysis.
192 : ///
193 : /// \param s - The underlying solver to use.
194 : Solver *createFastCexSolver(Solver *s);
195 :
196 : /// createIndependentSolver - Create a solver which will eliminate any
197 : /// unnecessary constraints before propogating the query to the underlying
198 : /// solver.
199 : ///
200 : /// \param s - The underlying solver to use.
201 : Solver *createIndependentSolver(Solver *s);
202 :
203 : /// createLoggingSolver - Create a solver which will forward all queries after
204 : /// writing them to the given path in .qlog format.
205 : Solver *createLoggingSolver(Solver *s, std::string path);
206 :
207 : /// createPCLoggingSolver - Create a solver which will forward all queries
208 : /// after writing them to the given path in .pc format.
209 : Solver *createPCLoggingSolver(Solver *s, std::string path);
210 :
211 : }
212 :
213 : #endif
Generated: 2009-05-17 22:47 by zcov