diff options
| -rw-r--r-- | lib/SMT/SMTParser.cpp | 51 | ||||
| -rw-r--r-- | lib/SMT/SMTParser.h | 21 | ||||
| -rw-r--r-- | lib/SMT/main.cpp | 2 | ||||
| -rw-r--r-- | lib/SMT/smtlib.lex | 1 | ||||
| -rw-r--r-- | lib/SMT/smtlib.y | 63 |
5 files changed, 110 insertions, 28 deletions
diff --git a/lib/SMT/SMTParser.cpp b/lib/SMT/SMTParser.cpp index 88d0a6c9..395241a0 100644 --- a/lib/SMT/SMTParser.cpp +++ b/lib/SMT/SMTParser.cpp @@ -14,6 +14,7 @@ #include <fstream> #include <cstring> #include <cassert> +#include <stack> using namespace std; using namespace klee; @@ -35,6 +36,10 @@ SMTParser::SMTParser(const std::string filename) : fileName(filename), bvSize(0), queryParsed(false) { is = new ifstream(filename.c_str()); + + // Initial empty environments + varEnvs.push(VarEnv()); + fvarEnvs.push(FVarEnv()); } void SMTParser::Init() { @@ -60,3 +65,49 @@ int SMTParser::Error(const string& s) { exit(1); return 0; } + +void SMTParser::PushVarEnv() { + cout << "Pushing new var env\n"; + varEnvs.push(VarEnv(varEnvs.top())); +} + +void SMTParser::PopVarEnv() { + cout << "Popping new var env\n"; + varEnvs.pop(); +} + +void SMTParser::AddVar(std::string name, ExprHandle val) { + cout << "Adding (" << name << ", " << val << ") to current var env.\n"; + varEnvs.top()[name] = val; +} + +ExprHandle SMTParser::GetVar(std::string name) { + VarEnv top = varEnvs.top(); + if (top.find(name) == top.end()) { + std::cerr << "Cannot find variable ?" << name << "\n"; + exit(1); + } + return top[name]; +} + + +void SMTParser::PushFVarEnv() { + fvarEnvs.push(FVarEnv(fvarEnvs.top())); +} + +void SMTParser::PopFVarEnv(void) { + fvarEnvs.pop(); +} + +void SMTParser::AddFVar(std::string name, ExprHandle val) { + fvarEnvs.top()[name] = val; +} + +ExprHandle SMTParser::GetFVar(std::string name) { + FVarEnv top = fvarEnvs.top(); + if (top.find(name) == top.end()) { + std::cerr << "Cannot find fvar $" << name << "\n"; + exit(1); + } + return top[name]; +} diff --git a/lib/SMT/SMTParser.h b/lib/SMT/SMTParser.h index edc1258f..ea5c34e5 100644 --- a/lib/SMT/SMTParser.h +++ b/lib/SMT/SMTParser.h @@ -16,7 +16,8 @@ #include <cassert> #include <iostream> #include <map> -#include <cstring> +#include <stack> +#include <string> namespace klee { namespace expr { @@ -53,6 +54,24 @@ class SMTParser : public klee::expr::Parser { void Init(void); int Error(const std::string& s); + + + 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 }; } diff --git a/lib/SMT/main.cpp b/lib/SMT/main.cpp index 4d2b8e0a..d5137782 100644 --- a/lib/SMT/main.cpp +++ b/lib/SMT/main.cpp @@ -13,4 +13,6 @@ int main(int argc, char** argv) { klee::expr::SMTParser smtParser(argv[1]); smtParser.Init(); + + cout << "Query: " << smtParser.query << "\n"; } diff --git a/lib/SMT/smtlib.lex b/lib/SMT/smtlib.lex index 0d955bf8..fb59316d 100644 --- a/lib/SMT/smtlib.lex +++ b/lib/SMT/smtlib.lex @@ -218,6 +218,7 @@ IDCHAR ({LETTER}|{DIGIT}|{OPCHAR}) "bvxor" { return BVXOR_TOK; } "bvxnor" { return BVXNOR_TOK; } +"=" { return EQ_TOK; } "bvcomp" { return BVCOMP_TOK; } "bvult" { return BVULT_TOK; } "bvule" { return BVULE_TOK; } diff --git a/lib/SMT/smtlib.y b/lib/SMT/smtlib.y index 12284d89..753b24b3 100644 --- a/lib/SMT/smtlib.y +++ b/lib/SMT/smtlib.y @@ -32,6 +32,7 @@ using namespace klee; using namespace klee::expr; // Define shortcuts for various things +#define PARSER SMTParser::parserTemp #define DONE SMTParser::parserTemp->done #define EXPR SMTParser::parserTemp->query #define ASSUMPTIONS SMTParser::parserTemp->assumptions @@ -98,8 +99,8 @@ int smtliberror(const char *s) %type <node> an_formula an_logical_formula an_atom prop_atom %type <node> an_term basic_term an_fun an_arithmetic_fun an_pred -%type <str> logic_name status attribute user_value annotation annotations - +%type <str> logic_name status attribute user_value annotation annotations +%type <str> var %token <str> NUMERAL_TOK %token <str> SYM_TOK @@ -170,6 +171,7 @@ int smtliberror(const char *s) %token BVXOR_TOK %token BVXNOR_TOK +%token EQ_TOK %token BVCOMP_TOK %token BVULT_TOK %token BVULE_TOK @@ -499,16 +501,21 @@ an_formula: { $$ = $1; } -/* - | LPAREN_TOK LET_TOK LPAREN_TOK var an_term RPAREN_TOK an_formula annotations RPAREN_TOK + + + | LPAREN_TOK LET_TOK LPAREN_TOK var an_term RPAREN_TOK + { + PARSER->PushVarEnv(); + PARSER->AddVar(*$4, $5); + } + an_formula RPAREN_TOK { - CVC3::Expr e(VC->listExpr(VC->listExpr(*$4, *$5))); - $$ = new CVC3::Expr(VC->listExpr("_LET", e, *$7)); - delete $4; - delete $5; - delete $7; - delete $8; + $$ = $8; + PARSER->PopVarEnv(); } + + +/* | LPAREN_TOK LET_TOK LPAREN_TOK var an_term RPAREN_TOK an_formula RPAREN_TOK { CVC3::Expr e(VC->listExpr(VC->listExpr(*$4, *$5))); @@ -517,15 +524,7 @@ an_formula: delete $5; delete $7; } - | LPAREN_TOK FLET_TOK LPAREN_TOK fvar an_formula RPAREN_TOK an_formula annotations RPAREN_TOK - { - CVC3::Expr e(VC->listExpr(VC->listExpr(*$4, *$5))); - $$ = new CVC3::Expr(VC->listExpr("_LET", e, *$7)); - delete $4; - delete $5; - delete $7; - delete $8; - } + | LPAREN_TOK FLET_TOK LPAREN_TOK fvar an_formula RPAREN_TOK an_formula RPAREN_TOK { CVC3::Expr e(VC->listExpr(VC->listExpr(*$4, *$5))); @@ -610,7 +609,16 @@ prop_atom: an_pred: - LPAREN_TOK BVULT_TOK an_term an_term RPAREN_TOK + LPAREN_TOK EQ_TOK an_term an_term RPAREN_TOK + { + $$ = EqExpr::create($3, $4); + } + | LPAREN_TOK EQ_TOK an_term an_term annotations RPAREN_TOK + { + $$ = EqExpr::create($3, $4); + } + + | LPAREN_TOK BVULT_TOK an_term an_term RPAREN_TOK { $$ = UltExpr::create($3, $4); } @@ -752,7 +760,7 @@ an_arithmetic_fun: { $$ = NULL; // XXX: unsupported } - | LPAREN_TOK BVSREM_TOK an_term an_term annotations RPAREN_TOK + | LPAREN_TOK BVSMOD_TOK an_term an_term annotations RPAREN_TOK { $$ = NULL; // XXX: unsupported } @@ -964,10 +972,12 @@ basic_term: { $$ = $1; } +*/ | var { - $$ = $1; + $$ = PARSER->GetVar(*$1); } +/* | fun_symb { if ($1->size() == 1) { @@ -1194,20 +1204,19 @@ attribute: } ; -/* + var: QUESTION_TOK SYM_TOK { - $$ = new CVC3::Expr(VC->idExpr(*$2)); - delete $2; + $$ = $2; } ; +/* fvar: DOLLAR_TOK SYM_TOK { - $$ = new CVC3::Expr(VC->idExpr(*$2)); - delete $2; + $$ = $2; } ; */ |