klee
 All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
QueryLoggingSolver.h
Go to the documentation of this file.
1 //===-- QueryLoggingSolver.h ---------------------------------------------------===//
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 #ifndef KLEE_QUERYLOGGINGSOLVER_H
11 #define KLEE_QUERYLOGGINGSOLVER_H
12 
13 #include "klee/Solver.h"
14 #include "klee/SolverImpl.h"
15 #include "llvm/Support/raw_ostream.h"
16 #include <fstream>
17 #include <sstream>
18 
19 using namespace klee;
20 
26 
27 protected:
29  std::string ErrorInfo;
30  llvm::raw_fd_ostream os;
31  // @brief Buffer used by logBuffer
32  std::string BufferString;
33  // @brief buffer to store logs before flushing to file
34  llvm::raw_string_ostream logBuffer;
35  unsigned queryCount;
36  int minQueryTimeToLog; // we log to file only those queries
37  // which take longer than the specified time (ms);
38  // if this param is negative, log only those queries
39  // on which the solver has timed out
40 
41  double startTime;
42  double lastQueryTime;
43  const std::string queryCommentSign; // sign representing commented lines
44  // in given a query format
45 
46  virtual void startQuery(const Query& query, const char* typeName,
47  const Query* falseQuery = 0,
48  const std::vector<const Array*>* objects = 0);
49 
50  virtual void finishQuery(bool success);
51 
54  void flushBuffer(void);
55 
56  virtual void printQuery(const Query& query,
57  const Query* falseQuery = 0,
58  const std::vector<const Array*>* objects = 0) = 0;
59 
60 public:
61  QueryLoggingSolver(Solver *_solver,
62  std::string path,
63  const std::string& commentSign,
64  int queryTimeToLog);
65 
66  virtual ~QueryLoggingSolver();
67 
69  bool computeTruth(const Query& query, bool &isValid);
70  bool computeValidity(const Query& query, Solver::Validity &result);
71  bool computeValue(const Query& query, ref<Expr> &result);
72  bool computeInitialValues(const Query& query,
73  const std::vector<const Array*> &objects,
74  std::vector< std::vector<unsigned char> > &values,
75  bool &hasSolution);
76  SolverRunStatus getOperationStatusCode();
77  char *getConstraintLog(const Query&);
78  void setCoreSolverTimeout(double timeout);
79 };
80 
81 #endif /* KLEE_QUERYLOGGINGSOLVER_H */
82 
SolverImpl - Abstract base clase for solver implementations.
Definition: SolverImpl.h:22
const std::string queryCommentSign
llvm::raw_fd_ostream os
llvm::raw_string_ostream logBuffer