klee
 All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
SMTParser.cpp
Go to the documentation of this file.
1 //===-- SMTParser.cpp -----------------------------------------------------===//
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 #include "SMTParser.h"
11 
12 #include "klee/ExprBuilder.h"
13 #include "klee/Solver.h"
14 #include "klee/Constraints.h"
15 #include "expr/Parser.h"
16 
17 #include <fstream>
18 #include <string>
19 #include <sstream>
20 #include <cassert>
21 #include <stack>
22 
23 //#define DEBUG
24 
25 using namespace klee;
26 using namespace klee::expr;
27 
28 extern int smtlibparse();
29 extern void *smtlib_createBuffer(int);
30 extern void smtlib_deleteBuffer(void *);
31 extern void smtlib_switchToBuffer(void *);
32 extern int smtlib_bufSize(void);
33 extern void smtlib_setInteractive(bool);
34 
36 
37 SMTParser::SMTParser(const std::string _filename,
38  ExprBuilder* _builder) : fileName(_filename),
39  lineNum(1),
40  done(false),
41  satQuery(NULL),
42  bvSize(0),
43  queryParsed(false),
44  builder(_builder) {
45  is = new ifstream(fileName.c_str());
46 
47  // Initial empty environments
48  varEnvs.push(VarEnv());
49  fvarEnvs.push(FVarEnv());
50 }
51 
53  SMTParser::parserTemp = this;
54 
57  smtlib_setInteractive(false);
58  smtlibparse();
59  //xcout << "Parsed successfully.\n";
60 }
61 
64  std::vector<ExprHandle>(),
65  std::vector<const Array*>());
66 }
67 
69  // FIXME: Support choice of solver.
70  bool UseDummySolver = false, UseFastCexSolver = true, UseSTPQueryPCLog = true;
71  Solver *S, *STP = S =
72  UseDummySolver ? createDummySolver() : new STPSolver(true);
73  if (UseSTPQueryPCLog)
74  S = createPCLoggingSolver(S, "stp-queries.pc");
75  if (UseFastCexSolver)
76  S = createFastCexSolver(S);
78  S = createCachingSolver(S);
80  if (0)
81  S = createValidatingSolver(S, STP);
82 
83  Decl *D = this->ParseTopLevelDecl();
84  if (QueryCommand *QC = dyn_cast<QueryCommand>(D)) {
85  //llvm::cout << "Query " << ":\t";
86 
87  assert("FIXME: Support counterexample query commands!");
88  if (QC->Values.empty() && QC->Objects.empty()) {
89  bool result;
90  if (S->mustBeTrue(Query(ConstraintManager(QC->Constraints), QC->Query),
91  result)) {
92  //std::cout << (result ? "VALID" : "INVALID") << "\n";
93  return result;
94  }
95  }
96  }
97  llvm::cout << "FAIL";
98  exit(1);
99 }
100 
101 
102 // XXX: give more info
103 int SMTParser::Error(const string& msg) {
104  llvm::errs() << SMTParser::parserTemp->fileName << ":"
105  << SMTParser::parserTemp->lineNum << ": " << msg << "\n";
106  exit(1);
107  return 0;
108 }
109 
110 
111 int SMTParser::StringToInt(const std::string& s) {
112  std::stringstream str(s);
113  int x;
114  str >> x;
115  assert(str);
116  return x;
117 }
118 
119 
120 ExprHandle SMTParser::CreateAnd(std::vector<ExprHandle> kids) {
121  unsigned n_kids = kids.size();
122  assert(n_kids);
123  if (n_kids == 1)
124  return kids[0];
125 
126  ExprHandle r = builder->And(kids[n_kids-2], kids[n_kids-1]);
127  for (int i=n_kids-3; i>=0; i--)
128  r = builder->And(kids[i], r);
129  return r;
130 }
131 
132 ExprHandle SMTParser::CreateOr(std::vector<ExprHandle> kids) {
133  unsigned n_kids = kids.size();
134  assert(n_kids);
135  if (n_kids == 1)
136  return kids[0];
137 
138  ExprHandle r = builder->Or(kids[n_kids-2], kids[n_kids-1]);
139  for (int i=n_kids-3; i>=0; i--)
140  r = builder->Or(kids[i], r);
141  return r;
142 }
143 
144 ExprHandle SMTParser::CreateXor(std::vector<ExprHandle> kids) {
145  unsigned n_kids = kids.size();
146  assert(n_kids);
147  if (n_kids == 1)
148  return kids[0];
149 
150  ExprHandle r = builder->Xor(kids[n_kids-2], kids[n_kids-1]);
151  for (int i=n_kids-3; i>=0; i--)
152  r = builder->Xor(kids[i], r);
153  return r;
154 }
155 
156 
157 void SMTParser::DeclareExpr(std::string name, Expr::Width w) {
158  // for now, only allow variables which are multiples of 8
159  if (w % 8 != 0) {
160  cout << "BitVec not multiple of 8 (" << w << "). Need to update code.\n";
161  exit(1);
162  }
163 
164 #ifdef DEBUG
165  std::cout << "Declaring " << name << " of width " << w << "\n";
166 #endif
167 
168  Array *arr = new Array(name, w / 8);
169 
170  ref<Expr> *kids = new ref<Expr>[w/8];
171  for (unsigned i=0; i < w/8; i++)
172  kids[i] = builder->Read(UpdateList(arr, NULL),
173  builder->Constant(i, 32));
174  ref<Expr> var = ConcatExpr::createN(w/8, kids); // XXX: move to builder?
175  delete [] kids;
176 
177  AddVar(name, var);
178 }
179 
180 
181 ExprHandle SMTParser::GetConstExpr(std::string val, uint8_t base, klee::Expr::Width w) {
182  assert(base == 2 || base == 10 || base == 16);
183  llvm::APInt ap(w, val.c_str(), val.length(), base);
184 
185  return klee::ConstantExpr::alloc(ap);
186 }
187 
188 
190 #ifdef DEBUG
191  cout << "Pushing new var env\n";
192 #endif
193  varEnvs.push(VarEnv(varEnvs.top()));
194 }
195 
197 #ifdef DEBUG
198  cout << "Popping var env\n";
199 #endif
200  varEnvs.pop();
201 }
202 
203 void SMTParser::AddVar(std::string name, ExprHandle val) {
204 #ifdef DEBUG
205  cout << "Adding (" << name << ", " << val << ") to current var env.\n";
206 #endif
207  varEnvs.top()[name] = val;
208 }
209 
210 ExprHandle SMTParser::GetVar(std::string name) {
211  VarEnv top = varEnvs.top();
212  if (top.find(name) == top.end()) {
213  llvm::errs() << "Cannot find variable ?" << name << "\n";
214  exit(1);
215  }
216  return top[name];
217 }
218 
219 
221  fvarEnvs.push(FVarEnv(fvarEnvs.top()));
222 }
223 
225 #ifdef DEBUG
226  cout << "Popping fvar env\n";
227 #endif
228  fvarEnvs.pop();
229 }
230 
231 void SMTParser::AddFVar(std::string name, ExprHandle val) {
232 #ifdef DEBUG
233  cout << "Adding (" << name << ", " << val << ") to current fvar env.\n";
234 #endif
235  fvarEnvs.top()[name] = val;
236 }
237 
238 ExprHandle SMTParser::GetFVar(std::string name) {
239  FVarEnv top = fvarEnvs.top();
240  if (top.find(name) == top.end()) {
241  llvm::errs() << "Cannot find fvar $" << name << "\n";
242  exit(1);
243  }
244  return top[name];
245 }
ExprHandle GetFVar(std::string name)
Definition: SMTParser.cpp:238
ExprHandle CreateOr(std::vector< ExprHandle >)
Definition: SMTParser.cpp:132
void smtlib_switchToBuffer(void *)
void PushFVarEnv(void)
Definition: SMTParser.cpp:220
ExprHandle GetConstExpr(std::string val, uint8_t base, klee::Expr::Width w)
Definition: SMTParser.cpp:181
void AddVar(std::string name, ExprHandle val)
Definition: SMTParser.cpp:203
Solver * createFastCexSolver(Solver *s)
klee::expr::ExprHandle satQuery
Definition: SMTParser.h:39
ExprHandle CreateAnd(std::vector< ExprHandle >)
Definition: SMTParser.cpp:120
ExprBuilder - Base expression builder class.
Definition: ExprBuilder.h:17
std::stack< FVarEnv > fvarEnvs
Definition: SMTParser.h:75
virtual klee::expr::Decl * ParseTopLevelDecl()
Definition: SMTParser.cpp:62
void DeclareExpr(std::string name, Expr::Width w)
Definition: SMTParser.cpp:157
int smtlib_bufSize(void)
std::map< const std::string, ExprHandle > VarEnv
Definition: SMTParser.h:71
Class representing a complete list of updates into an array.
Definition: Expr.h:655
Solver * createCachingSolver(Solver *s)
static ref< Expr > createN(unsigned nKids, const ref< Expr > kids[])
Shortcuts to create larger concats. The chain returned is unbalanced to the right.
Definition: Expr.cpp:582
bool mustBeTrue(const Query &, bool &result)
Definition: Solver.cpp:144
SMTParser(const std::string filename, ExprBuilder *builder)
Definition: SMTParser.cpp:37
int StringToInt(const std::string &s)
Definition: SMTParser.cpp:111
Decl - Base class for top level declarations.
Definition: Parser.h:41
int Error(const std::string &s)
Definition: SMTParser.cpp:103
void AddFVar(std::string name, ExprHandle val)
Definition: SMTParser.cpp:231
void * smtlib_createBuffer(int)
std::vector< ExprHandle > assumptions
Definition: SMTParser.h:38
ExprHandle CreateXor(std::vector< ExprHandle >)
Definition: SMTParser.cpp:144
virtual ref< Expr > Not(const ref< Expr > &LHS)=0
klee::ExprBuilder * builder
Definition: SMTParser.h:44
std::string fileName
Definition: SMTParser.h:32
int smtlibparse()
unsigned Width
The type of an expression is simply its width, in bits.
Definition: Expr.h:94
static ref< ConstantExpr > alloc(const llvm::APInt &v)
Definition: Expr.h:398
virtual ref< Expr > Constant(const llvm::APInt &Value)=0
Solver * createIndependentSolver(Solver *s)
virtual ref< Expr > And(const ref< Expr > &LHS, const ref< Expr > &RHS)=0
std::istream * is
Definition: SMTParser.h:33
static SMTParser * parserTemp
Definition: SMTParser.h:31
std::map< const std::string, ExprHandle > FVarEnv
Definition: SMTParser.h:72
llvm::cl::opt< bool > UseFastCexSolver
Solver * createValidatingSolver(Solver *s, Solver *oracle)
Definition: Solver.cpp:450
std::stack< VarEnv > varEnvs
Definition: SMTParser.h:74
ExprHandle GetVar(std::string name)
Definition: SMTParser.cpp:210
Solver * createPCLoggingSolver(Solver *s, std::string path, int minQueryTimeToLog)
virtual ref< Expr > Xor(const ref< Expr > &LHS, const ref< Expr > &RHS)=0
Solver * createDummySolver()
Definition: Solver.cpp:489
Solver * createCexCachingSolver(Solver *s)
STPSolver - A complete solver based on STP.
Definition: Solver.h:203
void smtlib_setInteractive(bool)
virtual ref< Expr > Or(const ref< Expr > &LHS, const ref< Expr > &RHS)=0
virtual ref< Expr > Read(const UpdateList &Updates, const ref< Expr > &Index)=0
void smtlib_deleteBuffer(void *)