klee
 All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
SMTParser.h
Go to the documentation of this file.
1 //===-- SMTParser.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 
11 #ifndef SMT_PARSER_H
12 #define SMT_PARSER_H
13 
14 #include "expr/Parser.h"
15 
16 #include <map>
17 #include <stack>
18 #include <string>
19 
20 namespace klee {
21  class ExprBuilder;
22 
23 namespace expr {
24 
25 class SMTParser : public klee::expr::Parser {
26  private:
27  void *buf;
28 
29  public:
30  /* For interacting w/ the actual parser, should make this nicer */
32  std::string fileName;
33  std::istream* is;
34  int lineNum;
35  bool done;
37 
38  std::vector<ExprHandle> assumptions;
40 
41  int bvSize;
43 
45 
46  SMTParser(const std::string filename, ExprBuilder *builder);
47 
49  bool Solve();
50 
51  virtual void SetMaxErrors(unsigned N) { }
52 
53  virtual unsigned GetNumErrors() const { return 1; }
54 
55  virtual ~SMTParser() {}
56 
57  void Parse(void);
58 
59  int Error(const std::string& s);
60 
61  int StringToInt(const std::string& s);
62  ExprHandle GetConstExpr(std::string val, uint8_t base, klee::Expr::Width w);
63 
64  void DeclareExpr(std::string name, Expr::Width w);
65 
66  ExprHandle CreateAnd(std::vector<ExprHandle>);
67  ExprHandle CreateOr(std::vector<ExprHandle>);
68  ExprHandle CreateXor(std::vector<ExprHandle>);
69 
70 
71  typedef std::map<const std::string, ExprHandle> VarEnv;
72  typedef std::map<const std::string, ExprHandle> FVarEnv;
73 
74  std::stack<VarEnv> varEnvs;
75  std::stack<FVarEnv> fvarEnvs;
76 
77  void PushVarEnv(void);
78  void PopVarEnv(void);
79  void AddVar(std::string name, ExprHandle val); // to current var env
80  ExprHandle GetVar(std::string name); // from current var env
81 
82  void PushFVarEnv(void);
83  void PopFVarEnv(void);
84  void AddFVar(std::string name, ExprHandle val); // to current fvar env
85  ExprHandle GetFVar(std::string name); // from current fvar env
86 };
87 
88 }
89 }
90 
91 #endif
92 
ExprHandle GetFVar(std::string name)
Definition: SMTParser.cpp:238
ExprHandle CreateOr(std::vector< ExprHandle >)
Definition: SMTParser.cpp:132
virtual void SetMaxErrors(unsigned N)
SetMaxErrors - Suppress anything beyond the first N errors.
Definition: SMTParser.h:51
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
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
std::map< const std::string, ExprHandle > VarEnv
Definition: SMTParser.h:71
SMTParser(const std::string filename, ExprBuilder *builder)
Definition: SMTParser.cpp:37
int StringToInt(const std::string &s)
Definition: SMTParser.cpp:111
virtual ~SMTParser()
Definition: SMTParser.h:55
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
std::vector< ExprHandle > assumptions
Definition: SMTParser.h:38
ExprHandle CreateXor(std::vector< ExprHandle >)
Definition: SMTParser.cpp:144
klee::ExprBuilder * builder
Definition: SMTParser.h:44
std::string fileName
Definition: SMTParser.h:32
unsigned Width
The type of an expression is simply its width, in bits.
Definition: Expr.h:94
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
std::stack< VarEnv > varEnvs
Definition: SMTParser.h:74
Parser - Public interface for parsing a .pc language file.
Definition: Parser.h:206
ExprHandle GetVar(std::string name)
Definition: SMTParser.cpp:210
virtual unsigned GetNumErrors() const
GetNumErrors - Return the number of encountered errors.
Definition: SMTParser.h:53