klee
 All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
main.cpp
Go to the documentation of this file.
1 #include "expr/Lexer.h"
2 #include "expr/Parser.h"
3 
4 #include "klee/Config/Version.h"
5 #include "klee/Constraints.h"
6 #include "klee/Expr.h"
7 #include "klee/ExprBuilder.h"
8 #include "klee/Solver.h"
9 #include "klee/SolverImpl.h"
10 #include "klee/Statistics.h"
11 #include "klee/CommandLine.h"
12 #include "klee/Common.h"
13 #include "klee/util/ExprPPrinter.h"
14 #include "klee/util/ExprVisitor.h"
15 
17 
18 #include "llvm/ADT/OwningPtr.h"
19 #include "llvm/ADT/StringExtras.h"
20 #include "llvm/Support/CommandLine.h"
21 #include "llvm/Support/ManagedStatic.h"
22 #include "llvm/Support/MemoryBuffer.h"
23 #include "llvm/Support/raw_ostream.h"
24 
25 #include <sys/stat.h>
26 #include <unistd.h>
27 
28 // FIXME: Ugh, this is gross. But otherwise our config.h conflicts with LLVMs.
29 #undef PACKAGE_BUGREPORT
30 #undef PACKAGE_NAME
31 #undef PACKAGE_STRING
32 #undef PACKAGE_TARNAME
33 #undef PACKAGE_VERSION
34 
35 #include "llvm/Support/Signals.h"
36 #include "llvm/Support/system_error.h"
37 
38 using namespace llvm;
39 using namespace klee;
40 using namespace klee::expr;
41 
42 #ifdef SUPPORT_METASMT
43 
44 #include <metaSMT/DirectSolver_Context.hpp>
45 #include <metaSMT/backend/Z3_Backend.hpp>
46 #include <metaSMT/backend/Boolector.hpp>
47 
48 #define Expr VCExpr
49 #define Type VCType
50 #define STP STP_Backend
51 #include <metaSMT/backend/STP.hpp>
52 #undef Expr
53 #undef Type
54 #undef STP
55 
56 using namespace metaSMT;
57 using namespace metaSMT::solver;
58 
59 #endif /* SUPPORT_METASMT */
60 
61 
62 
63 
64 namespace {
65  llvm::cl::opt<std::string>
66  InputFile(llvm::cl::desc("<input query log>"), llvm::cl::Positional,
67  llvm::cl::init("-"));
68 
69  enum ToolActions {
70  PrintTokens,
71  PrintAST,
72  PrintSMTLIBv2,
73  Evaluate
74  };
75 
76  static llvm::cl::opt<ToolActions>
77  ToolAction(llvm::cl::desc("Tool actions:"),
78  llvm::cl::init(Evaluate),
79  llvm::cl::values(
80  clEnumValN(PrintTokens, "print-tokens",
81  "Print tokens from the input file."),
82  clEnumValN(PrintSMTLIBv2, "print-smtlib",
83  "Print parsed input file as SMT-LIBv2 query."),
84  clEnumValN(PrintAST, "print-ast",
85  "Print parsed AST nodes from the input file."),
86  clEnumValN(Evaluate, "evaluate",
87  "Print parsed AST nodes from the input file."),
88  clEnumValEnd));
89 
90 
91  enum BuilderKinds {
92  DefaultBuilder,
93  ConstantFoldingBuilder,
94  SimplifyingBuilder
95  };
96 
97  static llvm::cl::opt<BuilderKinds>
98  BuilderKind("builder",
99  llvm::cl::desc("Expression builder:"),
100  llvm::cl::init(DefaultBuilder),
101  llvm::cl::values(
102  clEnumValN(DefaultBuilder, "default",
103  "Default expression construction."),
104  clEnumValN(ConstantFoldingBuilder, "constant-folding",
105  "Fold constant expressions."),
106  clEnumValN(SimplifyingBuilder, "simplify",
107  "Fold constants and simplify expressions."),
108  clEnumValEnd));
109 
110  cl::opt<bool>
111  UseDummySolver("use-dummy-solver",
112  cl::init(false));
113 
114  llvm::cl::opt<std::string> directoryToWriteQueryLogs("query-log-dir",llvm::cl::desc("The folder to write query logs to. Defaults is current working directory."),
115  llvm::cl::init("."));
116 
117 }
118 
119 static std::string getQueryLogPath(const char filename[])
120 {
121  //check directoryToWriteLogs exists
122  struct stat s;
123  if( !(stat(directoryToWriteQueryLogs.c_str(),&s) == 0 && S_ISDIR(s.st_mode)) )
124  {
125  llvm::errs() << "Directory to log queries \""
126  << directoryToWriteQueryLogs << "\" does not exist!"
127  << "\n";
128  exit(1);
129  }
130 
131  //check permissions okay
132  if( !( (s.st_mode & S_IWUSR) && getuid() == s.st_uid) &&
133  !( (s.st_mode & S_IWGRP) && getgid() == s.st_gid) &&
134  !( s.st_mode & S_IWOTH)
135  )
136  {
137  llvm::errs() << "Directory to log queries \""
138  << directoryToWriteQueryLogs << "\" is not writable!"
139  << "\n";
140  exit(1);
141  }
142 
143  std::string path=directoryToWriteQueryLogs;
144  path+="/";
145  path+=filename;
146  return path;
147 }
148 
149 static std::string escapedString(const char *start, unsigned length) {
150  std::string Str;
151  llvm::raw_string_ostream s(Str);
152  for (unsigned i=0; i<length; ++i) {
153  char c = start[i];
154  if (isprint(c)) {
155  s << c;
156  } else if (c == '\n') {
157  s << "\\n";
158  } else {
159  s << "\\x"
160  << hexdigit(((unsigned char) c >> 4) & 0xF)
161  << hexdigit((unsigned char) c & 0xF);
162  }
163  }
164  return s.str();
165 }
166 
167 static void PrintInputTokens(const MemoryBuffer *MB) {
168  Lexer L(MB);
169  Token T;
170  do {
171  L.Lex(T);
172  llvm::outs() << "(Token \"" << T.getKindName() << "\" "
173  << "\"" << escapedString(T.start, T.length) << "\" "
174  << T.length << " " << T.line << " " << T.column << ")\n";
175  } while (T.kind != Token::EndOfFile);
176 }
177 
178 static bool PrintInputAST(const char *Filename,
179  const MemoryBuffer *MB,
180  ExprBuilder *Builder) {
181  std::vector<Decl*> Decls;
182  Parser *P = Parser::Create(Filename, MB, Builder);
183  P->SetMaxErrors(20);
184 
185  unsigned NumQueries = 0;
186  while (Decl *D = P->ParseTopLevelDecl()) {
187  if (!P->GetNumErrors()) {
188  if (isa<QueryCommand>(D))
189  llvm::outs() << "# Query " << ++NumQueries << "\n";
190 
191  D->dump();
192  }
193  Decls.push_back(D);
194  }
195 
196  bool success = true;
197  if (unsigned N = P->GetNumErrors()) {
198  llvm::errs() << Filename << ": parse failure: " << N << " errors.\n";
199  success = false;
200  }
201 
202  for (std::vector<Decl*>::iterator it = Decls.begin(),
203  ie = Decls.end(); it != ie; ++it)
204  delete *it;
205 
206  delete P;
207 
208  return success;
209 }
210 
211 static bool EvaluateInputAST(const char *Filename,
212  const MemoryBuffer *MB,
213  ExprBuilder *Builder) {
214  std::vector<Decl*> Decls;
215  Parser *P = Parser::Create(Filename, MB, Builder);
216  P->SetMaxErrors(20);
217  while (Decl *D = P->ParseTopLevelDecl()) {
218  Decls.push_back(D);
219  }
220 
221  bool success = true;
222  if (unsigned N = P->GetNumErrors()) {
223  llvm::errs() << Filename << ": parse failure: " << N << " errors.\n";
224  success = false;
225  }
226 
227  if (!success)
228  return false;
229 
230  // FIXME: Support choice of solver.
231  Solver *coreSolver = NULL; //
232 
233 #ifdef SUPPORT_METASMT
234  if (UseMetaSMT != METASMT_BACKEND_NONE) {
235 
236  std::string backend;
237 
238  switch (UseMetaSMT) {
239  case METASMT_BACKEND_STP:
240  backend = "STP";
241  coreSolver = new MetaSMTSolver< DirectSolver_Context < STP_Backend > >(UseForkedCoreSolver, CoreSolverOptimizeDivides);
242  break;
243  case METASMT_BACKEND_Z3:
244  backend = "Z3";
245  coreSolver = new MetaSMTSolver< DirectSolver_Context < Z3_Backend > >(UseForkedCoreSolver, CoreSolverOptimizeDivides);
246  break;
247  case METASMT_BACKEND_BOOLECTOR:
248  backend = "Boolector";
249  coreSolver = new MetaSMTSolver< DirectSolver_Context < Boolector > >(UseForkedCoreSolver, CoreSolverOptimizeDivides);
250  break;
251  default:
252  assert(false);
253  break;
254  };
255  llvm::errs() << "Starting MetaSMTSolver(" << backend << ") ...\n";
256  }
257  else {
258  coreSolver = UseDummySolver ? createDummySolver() : new STPSolver(UseForkedCoreSolver);
259  }
260 #else
261  coreSolver = UseDummySolver ? createDummySolver() : new STPSolver(UseForkedCoreSolver);
262 #endif /* SUPPORT_METASMT */
263 
264 
265  if (!UseDummySolver) {
266  if (0 != MaxCoreSolverTime) {
268  }
269  }
270 
271  Solver *S = constructSolverChain(coreSolver,
276 
277  unsigned Index = 0;
278  for (std::vector<Decl*>::iterator it = Decls.begin(),
279  ie = Decls.end(); it != ie; ++it) {
280  Decl *D = *it;
281  if (QueryCommand *QC = dyn_cast<QueryCommand>(D)) {
282  llvm::outs() << "Query " << Index << ":\t";
283 
284  assert("FIXME: Support counterexample query commands!");
285  if (QC->Values.empty() && QC->Objects.empty()) {
286  bool result;
287  if (S->mustBeTrue(Query(ConstraintManager(QC->Constraints), QC->Query),
288  result)) {
289  llvm::outs() << (result ? "VALID" : "INVALID");
290  } else {
291  llvm::outs() << "FAIL (reason: "
292  << SolverImpl::getOperationStatusString(S->impl->getOperationStatusCode())
293  << ")";
294  }
295  } else if (!QC->Values.empty()) {
296  assert(QC->Objects.empty() &&
297  "FIXME: Support counterexamples for values and objects!");
298  assert(QC->Values.size() == 1 &&
299  "FIXME: Support counterexamples for multiple values!");
300  assert(QC->Query->isFalse() &&
301  "FIXME: Support counterexamples with non-trivial query!");
302  ref<ConstantExpr> result;
303  if (S->getValue(Query(ConstraintManager(QC->Constraints),
304  QC->Values[0]),
305  result)) {
306  llvm::outs() << "INVALID\n";
307  llvm::outs() << "\tExpr 0:\t" << result;
308  } else {
309  llvm::outs() << "FAIL (reason: "
310  << SolverImpl::getOperationStatusString(S->impl->getOperationStatusCode())
311  << ")";
312  }
313  } else {
314  std::vector< std::vector<unsigned char> > result;
315 
316  if (S->getInitialValues(Query(ConstraintManager(QC->Constraints),
317  QC->Query),
318  QC->Objects, result)) {
319  llvm::outs() << "INVALID\n";
320 
321  for (unsigned i = 0, e = result.size(); i != e; ++i) {
322  llvm::outs() << "\tArray " << i << ":\t"
323  << QC->Objects[i]->name
324  << "[";
325  for (unsigned j = 0; j != QC->Objects[i]->size; ++j) {
326  llvm::outs() << (unsigned) result[i][j];
327  if (j + 1 != QC->Objects[i]->size)
328  llvm::outs() << ", ";
329  }
330  llvm::outs() << "]";
331  if (i + 1 != e)
332  llvm::outs() << "\n";
333  }
334  } else {
336  if (SolverImpl::SOLVER_RUN_STATUS_TIMEOUT == retCode) {
337  llvm::outs() << " FAIL (reason: "
338  << SolverImpl::getOperationStatusString(retCode)
339  << ")";
340  }
341  else {
342  llvm::outs() << "VALID (counterexample request ignored)";
343  }
344  }
345  }
346 
347  llvm::outs() << "\n";
348  ++Index;
349  }
350  }
351 
352  for (std::vector<Decl*>::iterator it = Decls.begin(),
353  ie = Decls.end(); it != ie; ++it)
354  delete *it;
355  delete P;
356 
357  delete S;
358 
359  if (uint64_t queries = *theStatisticManager->getStatisticByName("Queries")) {
360  llvm::outs()
361  << "--\n"
362  << "total queries = " << queries << "\n"
363  << "total queries constructs = "
364  << *theStatisticManager->getStatisticByName("QueriesConstructs") << "\n"
365  << "valid queries = "
366  << *theStatisticManager->getStatisticByName("QueriesValid") << "\n"
367  << "invalid queries = "
368  << *theStatisticManager->getStatisticByName("QueriesInvalid") << "\n"
369  << "query cex = "
370  << *theStatisticManager->getStatisticByName("QueriesCEX") << "\n";
371  }
372 
373  return success;
374 }
375 
376 static bool printInputAsSMTLIBv2(const char *Filename,
377  const MemoryBuffer *MB,
378  ExprBuilder *Builder)
379 {
380  //Parse the input file
381  std::vector<Decl*> Decls;
382  Parser *P = Parser::Create(Filename, MB, Builder);
383  P->SetMaxErrors(20);
384  while (Decl *D = P->ParseTopLevelDecl())
385  {
386  Decls.push_back(D);
387  }
388 
389  bool success = true;
390  if (unsigned N = P->GetNumErrors())
391  {
392  llvm::errs() << Filename << ": parse failure: "
393  << N << " errors.\n";
394  success = false;
395  }
396 
397  if (!success)
398  return false;
399 
401  printer->setOutput(llvm::outs());
402 
403  unsigned int queryNumber = 0;
404  //Loop over the declarations
405  for (std::vector<Decl*>::iterator it = Decls.begin(), ie = Decls.end(); it != ie; ++it)
406  {
407  Decl *D = *it;
408  if (QueryCommand *QC = dyn_cast<QueryCommand>(D))
409  {
410  //print line break to separate from previous query
411  if(queryNumber!=0) llvm::outs() << "\n";
412 
413  //Output header for this query as a SMT-LIBv2 comment
414  llvm::outs() << ";SMTLIBv2 Query " << queryNumber << "\n";
415 
416  /* Can't pass ConstraintManager constructor directly
417  * as argument to Query object. Like...
418  * query(ConstraintManager(QC->Constraints),QC->Query);
419  *
420  * For some reason if constructed this way the first
421  * constraint in the constraint set is set to NULL and
422  * will later cause a NULL pointer dereference.
423  */
424  ConstraintManager constraintM(QC->Constraints);
425  Query query(constraintM,QC->Query);
426  printer->setQuery(query);
427 
428  if(!QC->Objects.empty())
429  printer->setArrayValuesToGet(QC->Objects);
430 
431  printer->generateOutput();
432 
433 
434  queryNumber++;
435  }
436  }
437 
438  //Clean up
439  for (std::vector<Decl*>::iterator it = Decls.begin(),
440  ie = Decls.end(); it != ie; ++it)
441  delete *it;
442  delete P;
443 
444  delete printer;
445 
446  return true;
447 }
448 
449 int main(int argc, char **argv) {
450  bool success = true;
451 
452  llvm::sys::PrintStackTraceOnErrorSignal();
453  llvm::cl::ParseCommandLineOptions(argc, argv);
454 
455  std::string ErrorStr;
456 
457  OwningPtr<MemoryBuffer> MB;
458  error_code ec=MemoryBuffer::getFileOrSTDIN(InputFile.c_str(), MB);
459  if (ec) {
460  llvm::errs() << argv[0] << ": error: " << ec.message() << "\n";
461  return 1;
462  }
463 
464  ExprBuilder *Builder = 0;
465  switch (BuilderKind) {
466  case DefaultBuilder:
467  Builder = createDefaultExprBuilder();
468  break;
469  case ConstantFoldingBuilder:
470  Builder = createDefaultExprBuilder();
471  Builder = createConstantFoldingExprBuilder(Builder);
472  break;
473  case SimplifyingBuilder:
474  Builder = createDefaultExprBuilder();
475  Builder = createConstantFoldingExprBuilder(Builder);
476  Builder = createSimplifyingExprBuilder(Builder);
477  break;
478  }
479 
480  switch (ToolAction) {
481  case PrintTokens:
482  PrintInputTokens(MB.get());
483  break;
484  case PrintAST:
485  success = PrintInputAST(InputFile=="-" ? "<stdin>" : InputFile.c_str(), MB.get(),
486  Builder);
487  break;
488  case Evaluate:
489  success = EvaluateInputAST(InputFile=="-" ? "<stdin>" : InputFile.c_str(),
490  MB.get(), Builder);
491  break;
492  case PrintSMTLIBv2:
493  success = printInputAsSMTLIBv2(InputFile=="-"? "<stdin>" : InputFile.c_str(), MB.get(),Builder);
494  break;
495  default:
496  llvm::errs() << argv[0] << ": error: Unknown program action!\n";
497  }
498 
499  delete Builder;
500  llvm::llvm_shutdown();
501  return success ? 0 : 1;
502 }
bool getValue(const Query &, ref< ConstantExpr > &result)
Definition: Solver.cpp:176
void setQuery(const Query &q)
unsigned line
The length of the token.
Definition: Lexer.h:55
StatisticManager * theStatisticManager
Definition: Statistics.cpp:57
ExprBuilder * createSimplifyingExprBuilder(ExprBuilder *Base)
ExprBuilder * createDefaultExprBuilder()
ExprSMTLIBPrinter * createSMTLIBPrinter()
const char ALL_QUERIES_SMT2_FILE_NAME[]
Definition: Common.h:20
ExprBuilder - Base expression builder class.
Definition: ExprBuilder.h:17
const char ALL_QUERIES_PC_FILE_NAME[]
Definition: Common.h:22
unsigned length
The beginning of the token string.
Definition: Lexer.h:54
Statistic queries
static bool EvaluateInputAST(const char *Filename, const MemoryBuffer *MB, ExprBuilder *Builder)
Definition: main.cpp:211
bool mustBeTrue(const Query &, bool &result)
Definition: Solver.cpp:144
void setOutput(llvm::raw_ostream &output)
static bool printInputAsSMTLIBv2(const char *Filename, const MemoryBuffer *MB, ExprBuilder *Builder)
Definition: main.cpp:376
Statistic * getStatisticByName(const std::string &name) const
Definition: Statistics.cpp:50
static std::string getQueryLogPath(const char filename[])
Definition: main.cpp:119
const char * getKindName() const
getKindName - The name of this token's kind.
Definition: Lexer.cpp:24
const char * start
The token kind.
Definition: Lexer.h:53
const char SOLVER_QUERIES_SMT2_FILE_NAME[]
Definition: Common.h:21
Decl - Base class for top level declarations.
Definition: Parser.h:41
llvm::cl::opt< double > MaxCoreSolverTime
Lexer - Interface for lexing tokens from a .pc language file.
Definition: Lexer.h:76
BuilderKinds
Definition: main.cpp:91
static void PrintInputTokens(const MemoryBuffer *MB)
Definition: main.cpp:167
SolverImpl * impl
Definition: Solver.h:64
unsigned column
The line number of the start of this token.
Definition: Lexer.h:56
llvm::cl::opt< bool > UseForkedCoreSolver
virtual void setCoreSolverTimeout(double timeout)
Definition: Solver.cpp:128
virtual void SetMaxErrors(unsigned N)=0
SetMaxErrors - Suppress anything beyond the first N errors.
int main(int argc, char **argv)
Definition: main.cpp:449
static std::string escapedString(const char *start, unsigned length)
Definition: main.cpp:149
virtual unsigned GetNumErrors() const =0
GetNumErrors - Return the number of encountered errors.
bool getInitialValues(const Query &, const std::vector< const Array * > &objects, std::vector< std::vector< unsigned char > > &result)
Definition: Solver.cpp:193
llvm::cl::opt< bool > CoreSolverOptimizeDivides
void setArrayValuesToGet(const std::vector< const Array * > &a)
Parser - Public interface for parsing a .pc language file.
Definition: Parser.h:206
const char SOLVER_QUERIES_PC_FILE_NAME[]
Definition: Common.h:23
ExprBuilder * createConstantFoldingExprBuilder(ExprBuilder *Base)
virtual SolverRunStatus getOperationStatusCode()=0
getOperationStatusCode - get the status of the last solver operation
virtual Decl * ParseTopLevelDecl()=0
Token & Lex(Token &Result)
Definition: Lexer.cpp:210
Solver * createDummySolver()
Definition: Solver.cpp:489
static bool PrintInputAST(const char *Filename, const MemoryBuffer *MB, ExprBuilder *Builder)
Definition: main.cpp:178
STPSolver - A complete solver based on STP.
Definition: Solver.h:203
ToolActions
Definition: main.cpp:69
Solver * constructSolverChain(Solver *coreSolver, std::string querySMT2LogPath, std::string baseSolverQuerySMT2LogPath, std::string queryPCLogPath, std::string baseSolverQueryPCLogPath)