klee
 All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
QueryLoggingSolver.cpp
Go to the documentation of this file.
1 //===-- QueryLoggingSolver.cpp --------------------------------------------===//
2 
3 #include "QueryLoggingSolver.h"
5 #include "klee/Statistics.h"
6 
7 //
8 // The KLEE Symbolic Virtual Machine
9 //
10 // This file is distributed under the University of Illinois Open Source
11 // License. See LICENSE.TXT for details.
12 //
13 //===----------------------------------------------------------------------===//
14 
15 using namespace klee::util;
16 
18  std::string path,
19  const std::string& commentSign,
20  int queryTimeToLog)
21  : solver(_solver),
22  os(path.c_str(), ErrorInfo),
23  BufferString(""),
24  logBuffer(BufferString),
25  queryCount(0),
26  minQueryTimeToLog(queryTimeToLog),
27  startTime(0.0f),
28  lastQueryTime(0.0f),
29  queryCommentSign(commentSign) {
30  assert(0 != solver);
31 }
32 
34  delete solver;
35 }
36 
37 void QueryLoggingSolver::startQuery(const Query& query, const char* typeName,
38  const Query* falseQuery,
39  const std::vector<const Array*> *objects) {
40  Statistic *S = theStatisticManager->getStatisticByName("Instructions");
41  uint64_t instructions = S ? S->getValue() : 0;
42 
43  logBuffer << queryCommentSign << " Query " << queryCount++ << " -- "
44  << "Type: " << typeName << ", "
45  << "Instructions: " << instructions << "\n";
46 
47  printQuery(query, falseQuery, objects);
48 
50 
51 }
52 
53 void QueryLoggingSolver::finishQuery(bool success) {
55  logBuffer << queryCommentSign << " " << (success ? "OK" : "FAIL") << " -- "
56  << "Elapsed: " << lastQueryTime << "\n";
57 
58  if (false == success) {
59  logBuffer << queryCommentSign << " Failure reason: "
60  << SolverImpl::getOperationStatusString(solver->impl->getOperationStatusCode())
61  << "\n";
62  }
63 }
64 
66  logBuffer.flush();
67 
68  if ((0 == minQueryTimeToLog) ||
69  (static_cast<int>(lastQueryTime * 1000) > minQueryTimeToLog)) {
70  // we either do not limit logging queries or the query time
71  // is larger than threshold (in ms)
72 
73  if ((minQueryTimeToLog >= 0) ||
75  // we do additional check here to log only timeouts in case
76  // user specified negative value for minQueryTimeToLog param
77  os << logBuffer.str();
78  os.flush();
79  }
80  }
81 
82  // prepare the buffer for reuse
83  BufferString = "";
84 }
85 
86 bool QueryLoggingSolver::computeTruth(const Query& query, bool& isValid) {
87  startQuery(query, "Truth");
88 
89  bool success = solver->impl->computeTruth(query, isValid);
90 
91  finishQuery(success);
92 
93  if (success) {
94  logBuffer << queryCommentSign << " Is Valid: "
95  << (isValid ? "true" : "false") << "\n";
96  }
97  logBuffer << "\n";
98 
99  flushBuffer();
100 
101  return success;
102 }
103 
105  Solver::Validity& result) {
106  startQuery(query, "Validity");
107 
108  bool success = solver->impl->computeValidity(query, result);
109 
110  finishQuery(success);
111 
112  if (success) {
113  logBuffer << queryCommentSign << " Validity: "
114  << result << "\n";
115  }
116  logBuffer << "\n";
117 
118  flushBuffer();
119 
120  return success;
121 }
122 
123 bool QueryLoggingSolver::computeValue(const Query& query, ref<Expr>& result) {
124  Query withFalse = query.withFalse();
125  startQuery(query, "Value", &withFalse);
126 
127  bool success = solver->impl->computeValue(query, result);
128 
129  finishQuery(success);
130 
131  if (success) {
132  logBuffer << queryCommentSign << " Result: " << result << "\n";
133  }
134  logBuffer << "\n";
135 
136  flushBuffer();
137 
138  return success;
139 }
140 
142  const std::vector<const Array*>& objects,
143  std::vector<std::vector<unsigned char> >& values,
144  bool& hasSolution) {
145  startQuery(query, "InitialValues", 0, &objects);
146 
147  bool success = solver->impl->computeInitialValues(query, objects,
148  values, hasSolution);
149 
150  finishQuery(success);
151 
152  if (success) {
153  logBuffer << queryCommentSign << " Solvable: "
154  << (hasSolution ? "true" : "false") << "\n";
155  if (hasSolution) {
156  std::vector< std::vector<unsigned char> >::iterator
157  values_it = values.begin();
158 
159  for (std::vector<const Array*>::const_iterator i = objects.begin(),
160  e = objects.end(); i != e; ++i, ++values_it) {
161  const Array *array = *i;
162  std::vector<unsigned char> &data = *values_it;
163  logBuffer << queryCommentSign << " " << array->name << " = [";
164 
165  for (unsigned j = 0; j < array->size; j++) {
166  logBuffer << (int) data[j];
167 
168  if (j+1 < array->size) {
169  logBuffer << ",";
170  }
171  }
172  logBuffer << "]\n";
173  }
174  }
175  }
176  logBuffer << "\n";
177 
178  flushBuffer();
179 
180  return success;
181 }
182 
185 }
186 
188  return solver->impl->getConstraintLog(query);
189 }
190 
192  solver->impl->setCoreSolverTimeout(timeout);
193 }
194 
SolverRunStatus getOperationStatusCode()
getOperationStatusCode - get the status of the last solver operation
StatisticManager * theStatisticManager
Definition: Statistics.cpp:57
bool computeValidity(const Query &query, Solver::Validity &result)
unsigned size
Definition: Expr.h:605
bool computeTruth(const Query &query, bool &isValid)
implementation of the SolverImpl interface
Query withFalse() const
withFalse - Return a copy of the query with a false expression.
Definition: Solver.h:37
double getWallTime()
Definition: Time.cpp:24
bool computeValue(const Query &query, ref< Expr > &result)
uint64_t getValue() const
getValue - Get the current primary statistic value.
Definition: Statistics.cpp:82
virtual void setCoreSolverTimeout(double timeout)
Definition: SolverImpl.h:106
Statistic * getStatisticByName(const std::string &name) const
Definition: Statistics.cpp:50
virtual bool computeValidity(const Query &query, Solver::Validity &result)
Definition: Solver.cpp:73
virtual bool computeInitialValues(const Query &query, const std::vector< const Array * > &objects, std::vector< std::vector< unsigned char > > &values, bool &hasSolution)=0
const std::string name
Definition: Expr.h:603
QueryLoggingSolver(Solver *_solver, std::string path, const std::string &commentSign, int queryTimeToLog)
SolverImpl * impl
Definition: Solver.h:64
const std::string queryCommentSign
bool computeInitialValues(const Query &query, const std::vector< const Array * > &objects, std::vector< std::vector< unsigned char > > &values, bool &hasSolution)
char * getConstraintLog(const Query &)
llvm::raw_fd_ostream os
virtual SolverRunStatus getOperationStatusCode()=0
getOperationStatusCode - get the status of the last solver operation
virtual bool computeTruth(const Query &query, bool &isValid)=0
virtual void finishQuery(bool success)
virtual void startQuery(const Query &query, const char *typeName, const Query *falseQuery=0, const std::vector< const Array * > *objects=0)
virtual void printQuery(const Query &query, const Query *falseQuery=0, const std::vector< const Array * > *objects=0)=0
llvm::raw_string_ostream logBuffer
void setCoreSolverTimeout(double timeout)
virtual char * getConstraintLog(const Query &query)
Definition: SolverImpl.h:101
Statistic instructions
virtual bool computeValue(const Query &query, ref< Expr > &result)=0