diff options
| -rw-r--r-- | lib/SMT/SMTParser.cpp | 27 | ||||
| -rw-r--r-- | lib/SMT/SMTParser.h | 20 | ||||
| -rw-r--r-- | lib/SMT/parser_temp.h | 90 | ||||
| -rw-r--r-- | lib/SMT/smtlib.lex | 30 | ||||
| -rw-r--r-- | lib/SMT/smtlib.y | 24 |
5 files changed, 53 insertions, 138 deletions
diff --git a/lib/SMT/SMTParser.cpp b/lib/SMT/SMTParser.cpp index b87bbdbc..a66c2bf4 100644 --- a/lib/SMT/SMTParser.cpp +++ b/lib/SMT/SMTParser.cpp @@ -7,7 +7,6 @@ // //===----------------------------------------------------------------------===// -#include "parser_temp.h" #include "SMTParser.h" #include "expr/Parser.h" @@ -26,19 +25,22 @@ extern void smtlib_switchToBuffer(void *); extern int smtlib_bufSize(void); extern void smtlib_setInteractive(bool); -namespace CVC3 { - ParserTemp* parserTemp; +SMTParser* SMTParser::parserTemp = NULL; + +SMTParser::SMTParser(const std::string filename) : fileName(filename), + lineNum(0), + done(false), + expr(NULL), + bvSize(0), + queryParsed(false) { + is = new ifstream(filename.c_str()); } void SMTParser::Init() { cout << "Initializing parser\n"; - void *buf = smtlib_createBuffer(smtlib_bufSize()); + SMTParser::parserTemp = this; - CVC3::parserTemp = new CVC3::ParserTemp(); - CVC3::parserTemp->fileName = fname; - CVC3::parserTemp->is = new ifstream(fname.c_str()); - CVC3::parserTemp->interactive = false; - + void *buf = smtlib_createBuffer(smtlib_bufSize()); smtlib_switchToBuffer(buf); smtlib_setInteractive(false); smtlibparse(); @@ -47,3 +49,10 @@ void SMTParser::Init() { Decl* SMTParser::ParseTopLevelDecl() { return NULL; } + +// XXX: give more info +int SMTParser::Error(const string& s) { + std::cerr << "error: " << s << "\n"; + exit(1); + return 0; +} diff --git a/lib/SMT/SMTParser.h b/lib/SMT/SMTParser.h index 5abbee7b..35a0b00e 100644 --- a/lib/SMT/SMTParser.h +++ b/lib/SMT/SMTParser.h @@ -11,7 +11,6 @@ #ifndef SMT_PARSER_H #define SMT_PARSER_H -#include "parser_temp.h" #include "expr/Parser.h" #include <cassert> @@ -23,12 +22,21 @@ namespace klee { namespace expr { class SMTParser : public klee::expr::Parser { - private: - std::string fname; - void *buf; + private: + void *buf; public: - SMTParser(const std::string filename) : fname(filename) {} + /* For interacting w/ the actual parser, should make this nicer */ + static SMTParser* parserTemp; + std::string fileName; + std::istream* is; + int lineNum; + bool done; + klee::expr::ExprHandle expr; + int bvSize; + bool queryParsed; + + SMTParser(const std::string filename); virtual klee::expr::Decl *ParseTopLevelDecl(); @@ -39,6 +47,8 @@ class SMTParser : public klee::expr::Parser { virtual ~SMTParser() {} void Init(void); + + int Error(const std::string& s); }; } diff --git a/lib/SMT/parser_temp.h b/lib/SMT/parser_temp.h deleted file mode 100644 index ce0eecc8..00000000 --- a/lib/SMT/parser_temp.h +++ /dev/null @@ -1,90 +0,0 @@ -/*****************************************************************************/ -/*! - * \file parser_temp.h - * - * Author: Sergey Berezin - * - * Created: Wed Feb 5 17:53:02 2003 - * - * <hr> - * - * License to use, copy, modify, sell and/or distribute this software - * and its documentation for any purpose is hereby granted without - * royalty, subject to the terms and conditions defined in the \ref - * LICENSE file provided with this distribution. - * - * <hr> - * - * A class used to communicate with the actual parser. No one else - * should use it. - */ -/*****************************************************************************/ - -#ifndef _cvc3__parser_temp_h_ -#define _cvc3__parser_temp_h_ - -#include "expr/Parser.h" - -#include <sstream> -#include <vector> -#include <iostream> - -namespace CVC3 { - - class ParserTemp { - private: - // Counter for uniqueID of bound variables - int d_uid; - // The main prompt when running interactive - std::string prompt1; - // The interactive prompt in the middle of a multi-line command - std::string prompt2; - // The currently used prompt - std::string prompt; - public: - std::istream* is; - // The current input line - int lineNum; - // File name - std::string fileName; - // The last parsed Expr - klee::expr::ExprHandle expr; - // Whether we are done or not - bool done; - // Whether we are running interactive - bool interactive; - // Whether arrays are enabled for smt-lib format - bool arrFlag; - // Whether bit-vectors are enabled for smt-lib format - bool bvFlag; - // Size of bit-vectors for smt-lib format - int bvSize; - // Did we encounter a formula query (smtlib) - bool queryParsed; - // Default constructor - ParserTemp() : d_uid(0), prompt1("CVC> "), prompt2("- "), - prompt("CVC> "), lineNum(1), done(false), arrFlag(false), queryParsed(false) { } - // Parser error handling (implemented in parser.cpp) - int error(const std::string& s) { - // FIXME: Fail better? - std::cerr << "error: " << s << "\n"; - exit(1); - return 0; - } - // Get the next uniqueID as a string - std::string uniqueID() { - std::ostringstream ss; - ss << d_uid++; - return ss.str(); - } - // Get the current prompt - std::string getPrompt() { return prompt; } - // Set the prompt to the main one - void setPrompt1() { prompt = prompt1; } - // Set the prompt to the secondary one - void setPrompt2() { prompt = prompt2; } - }; - -} // end of namespace CVC3 - -#endif diff --git a/lib/SMT/smtlib.lex b/lib/SMT/smtlib.lex index 9f01c437..24acf56c 100644 --- a/lib/SMT/smtlib.lex +++ b/lib/SMT/smtlib.lex @@ -20,12 +20,11 @@ /*****************************************************************************/ #include <iostream> -#include "parser_temp.h" +#include "SMTParser.h" #include "smtlib_parser.h" -namespace CVC3 { - extern ParserTemp* parserTemp; -} +using namespace klee; +using namespace klee::expr; extern int smtlib_inputLine; extern char *smtlibtext; @@ -35,17 +34,8 @@ extern int smtliberror (const char *msg); static int smtlibinput(std::istream& is, char* buf, int size) { int res; if(is) { - // If interactive, read line by line; otherwise read as much as we - // can gobble - if(CVC3::parserTemp->interactive) { - // Print the current prompt - std::cout << CVC3::parserTemp->getPrompt() << std::flush; - // Set the prompt to "middle of the command" one - CVC3::parserTemp->setPrompt2(); - // Read the line - is.getline(buf, size-1); - } else // Set the terminator char to 0 - is.getline(buf, size-1, 0); + // Set the terminator char to 0 + is.getline(buf, size-1, 0); // If failbit is set, but eof is not, it means the line simply // didn't fit; so we clear the state and keep on reading. bool partialStr = is.fail() && !is.eof(); @@ -66,13 +56,13 @@ static int smtlibinput(std::istream& is, char* buf, int size) { // Redefine the input buffer function to read from an istream #define YY_INPUT(buf,result,max_size) \ - result = smtlibinput(*CVC3::parserTemp->is, buf, max_size); + result = smtlibinput(*SMTParser::parserTemp->is, buf, max_size); int smtlib_bufSize() { return YY_BUF_SIZE; } YY_BUFFER_STATE smtlib_buf_state() { return YY_CURRENT_BUFFER; } /* some wrappers for methods that need to refer to a struct. - These are used by CVC3::Parser. */ + These are used by SMTParser. */ void *smtlib_createBuffer(int sz) { return (void *)smtlib_create_buffer(NULL, sz); } @@ -125,7 +115,7 @@ OPCHAR (['\.\_]) IDCHAR ({LETTER}|{DIGIT}|{OPCHAR}) %% -[\n] { CVC3::parserTemp->lineNum++; } +[\n] { SMTParser::parserTemp->lineNum++; } [ \t\r\f] { /* skip whitespace */ } {DIGIT}+"\."{DIGIT}+ { smtliblval.str = new std::string(smtlibtext); return NUMERAL_TOK; } @@ -134,7 +124,7 @@ IDCHAR ({LETTER}|{DIGIT}|{OPCHAR}) ";" { BEGIN COMMENT; } <COMMENT>"\n" { BEGIN INITIAL; /* return to normal mode */ - CVC3::parserTemp->lineNum++; } + SMTParser::parserTemp->lineNum++; } <COMMENT>. { /* stay in comment mode */ } <INITIAL>"\"" { BEGIN STRING_LITERAL; @@ -163,7 +153,7 @@ IDCHAR ({LETTER}|{DIGIT}|{OPCHAR}) return USER_VAL_TOK; } <USER_VALUE>"\n" { _string_lit.insert(_string_lit.end(),'\n'); - CVC3::parserTemp->lineNum++; } + SMTParser::parserTemp->lineNum++; } <USER_VALUE>. { _string_lit.insert(_string_lit.end(),*smtlibtext); } "true" { return TRUE_TOK; } diff --git a/lib/SMT/smtlib.y b/lib/SMT/smtlib.y index 40413345..422c28ad 100644 --- a/lib/SMT/smtlib.y +++ b/lib/SMT/smtlib.y @@ -23,25 +23,21 @@ commands in SMT-LIB language. */ -#include "parser_temp.h" #include "SMTParser.h" #include "klee/Expr.h" +#include <sstream> + using namespace klee; using namespace klee::expr; -// Exported shared data -namespace CVC3 { - extern ParserTemp* parserTemp; -} // Define shortcuts for various things -#define TMP CVC3::parserTemp -#define EXPR CVC3::parserTemp->expr -//#define VC (CVC3::parserTemp->vc) -#define ARRAYSENABLED (CVC3::parserTemp->arrFlag) -#define BVENABLED (CVC3::parserTemp->bvFlag) -#define BVSIZE (CVC3::parserTemp->bvSize) -#define QUERYPARSED CVC3::parserTemp->queryParsed +#define TMP SMTParser::parserTemp +#define EXPR SMTParser::parserTemp->expr +#define ARRAYSENABLED (SMTParser::parserTemp->arrFlag) +#define BVENABLED (SMTParser::parserTemp->bvFlag) +#define BVSIZE (SMTParser::parserTemp->bvSize) +#define QUERYPARSED SMTParser::parserTemp->queryParsed // Suppress the bogus warning suppression in bison (it generates // compile error) @@ -53,9 +49,9 @@ extern int smtliblex(void); int smtliberror(const char *s) { std::ostringstream ss; - ss << CVC3::parserTemp->fileName << ":" << CVC3::parserTemp->lineNum + ss << SMTParser::parserTemp->fileName << ":" << SMTParser::parserTemp->lineNum << ": " << s; - return CVC3::parserTemp->error(ss.str()); + return SMTParser::parserTemp->Error(ss.str()); } |