blob: fd1ec04451948ecf5867681373e37e88145942de (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
|
//===-- SMTParser.h -------------------------------------------------------===//
//
// The KLEE Symbolic Virtual Machine
//
// This file is distributed under the University of Illinois Open Source
// License. See LICENSE.TXT for details.
//
//===----------------------------------------------------------------------===//
#ifndef SMT_PARSER_H
#define SMT_PARSER_H
#include "expr/Parser.h"
#include <cassert>
#include <iostream>
#include <map>
#include <stack>
#include <string>
namespace klee {
class ExprBuilder;
namespace expr {
class SMTParser : public klee::expr::Parser {
private:
void *buf;
public:
/* For interacting w/ the actual parser, should make this nicer */
static SMTParser* parserTemp;
std::string fileName;
std::istream* is;
int lineNum;
bool done;
bool arraysEnabled;
std::vector<ExprHandle> assumptions;
klee::expr::ExprHandle satQuery;
int bvSize;
bool queryParsed;
klee::ExprBuilder *builder;
SMTParser(const std::string filename, ExprBuilder *builder);
virtual klee::expr::Decl *ParseTopLevelDecl();
bool Solve();
virtual void SetMaxErrors(unsigned N) { }
virtual unsigned GetNumErrors() const { return 1; }
virtual ~SMTParser() {}
void Parse(void);
int Error(const std::string& s);
int StringToInt(const std::string& s);
ExprHandle GetConstExpr(std::string val, uint8_t base, klee::Expr::Width w);
void DeclareExpr(std::string name, Expr::Width w);
ExprHandle CreateAnd(std::vector<ExprHandle>);
ExprHandle CreateOr(std::vector<ExprHandle>);
ExprHandle CreateXor(std::vector<ExprHandle>);
typedef std::map<const std::string, ExprHandle> VarEnv;
typedef std::map<const std::string, ExprHandle> FVarEnv;
std::stack<VarEnv> varEnvs;
std::stack<FVarEnv> fvarEnvs;
void PushVarEnv(void);
void PopVarEnv(void);
void AddVar(std::string name, ExprHandle val); // to current var env
ExprHandle GetVar(std::string name); // from current var env
void PushFVarEnv(void);
void PopFVarEnv(void);
void AddFVar(std::string name, ExprHandle val); // to current fvar env
ExprHandle GetFVar(std::string name); // from current fvar env
};
}
}
#endif
|
