From 56b7a4f494dfe069fc4cbdb1dcd05c23c9b59a1d Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Fri, 22 Feb 2013 16:48:13 -0500 Subject: [PATCH] Disallow overflow in bitvector literals (parser only) * For example, (_ bv5 1) is now an error instead of being silently truncated. * Probably inappropriate for 1.0.x because it changes exception specifications. --- src/parser/antlr_input.h | 9 ++++++++- src/parser/cvc/cvc_input.cpp | 6 ++---- src/parser/cvc/cvc_input.h | 6 ++---- src/parser/input.h | 6 ++---- src/parser/parser.cpp | 16 ++++------------ src/parser/smt1/smt1_input.cpp | 6 ++---- src/parser/smt1/smt1_input.h | 6 ++---- src/parser/smt2/smt2_input.cpp | 6 ++---- src/parser/smt2/smt2_input.h | 6 ++---- src/parser/tptp/tptp_input.cpp | 6 ++---- src/parser/tptp/tptp_input.h | 6 ++---- 11 files changed, 30 insertions(+), 49 deletions(-) diff --git a/src/parser/antlr_input.h b/src/parser/antlr_input.h index 68a62274d..a2fe99f52 100644 --- a/src/parser/antlr_input.h +++ b/src/parser/antlr_input.h @@ -285,7 +285,14 @@ inline Rational AntlrInput::tokenToRational(pANTLR3_COMMON_TOKEN token) { inline BitVector AntlrInput::tokenToBitvector(pANTLR3_COMMON_TOKEN number, pANTLR3_COMMON_TOKEN size) { std::string number_str = tokenTextSubstr(number, 2); - return BitVector(tokenToUnsigned(size), Integer(number_str)); + unsigned sz = tokenToUnsigned(size); + Integer val(number_str); + if(val.modByPow2(sz) != val) { + std::stringstream ss; + ss << "Overflow in bitvector construction (specified bitvector size " << sz << " too small to hold value " << tokenText(number) << ")"; + throw std::invalid_argument(ss.str()); + } + return BitVector(sz, val); } }/* CVC4::parser namespace */ diff --git a/src/parser/cvc/cvc_input.cpp b/src/parser/cvc/cvc_input.cpp index 52fadae66..8328306be 100644 --- a/src/parser/cvc/cvc_input.cpp +++ b/src/parser/cvc/cvc_input.cpp @@ -56,13 +56,11 @@ CvcInput::~CvcInput() { d_pCvcParser->free(d_pCvcParser); } -Command* CvcInput::parseCommand() - throw (ParserException, TypeCheckingException) { +Command* CvcInput::parseCommand() { return d_pCvcParser->parseCommand(d_pCvcParser); } -Expr CvcInput::parseExpr() - throw (ParserException, TypeCheckingException) { +Expr CvcInput::parseExpr() { return d_pCvcParser->parseExpr(d_pCvcParser); } diff --git a/src/parser/cvc/cvc_input.h b/src/parser/cvc/cvc_input.h index 398ac4bd0..973e1c173 100644 --- a/src/parser/cvc/cvc_input.h +++ b/src/parser/cvc/cvc_input.h @@ -63,16 +63,14 @@ protected: * * @throws ParserException if an error is encountered during parsing. */ - Command* parseCommand() - throw(ParserException, TypeCheckingException); + Command* parseCommand(); /** Parse an expression from the input. Returns a null Expr * if there is no expression there to parse. * * @throws ParserException if an error is encountered during parsing. */ - Expr parseExpr() - throw(ParserException, TypeCheckingException); + Expr parseExpr(); private: diff --git a/src/parser/input.h b/src/parser/input.h index 0203ed806..f4b36469b 100644 --- a/src/parser/input.h +++ b/src/parser/input.h @@ -168,8 +168,7 @@ protected: * * @throws ParserException if an error is encountered during parsing. */ - virtual Command* parseCommand() - throw (ParserException, TypeCheckingException) = 0; + virtual Command* parseCommand() = 0; /** * Issue a warning to the user, with source file, line, and column info. @@ -188,8 +187,7 @@ protected: * * @throws ParserException if an error is encountered during parsing. */ - virtual Expr parseExpr() - throw (ParserException, TypeCheckingException) = 0; + virtual Expr parseExpr() = 0; /** Set the Parser object for this input. */ virtual void setParser(Parser& parser) = 0; diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index 65d46220b..8b77362b2 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -462,15 +462,9 @@ Command* Parser::nextCommand() throw(ParserException) { } catch(ParserException& e) { setDone(); throw; - } catch(Exception& e) { + } catch(exception& e) { setDone(); - stringstream ss; - // set the language of the stream, otherwise if it contains - // Exprs or Types it prints in the AST language - OutputLanguage outlang = - language::toOutputLanguage(d_input->getLanguage()); - ss << Expr::setlanguage(outlang) << e; - parseError( ss.str() ); + parseError(e.what()); } } } @@ -490,11 +484,9 @@ Expr Parser::nextExpression() throw(ParserException) { } catch(ParserException& e) { setDone(); throw; - } catch(Exception& e) { + } catch(exception& e) { setDone(); - stringstream ss; - ss << e; - parseError( ss.str() ); + parseError(e.what()); } } Debug("parser") << "nextExpression() => " << result << std::endl; diff --git a/src/parser/smt1/smt1_input.cpp b/src/parser/smt1/smt1_input.cpp index 156ca083f..2dae4ef66 100644 --- a/src/parser/smt1/smt1_input.cpp +++ b/src/parser/smt1/smt1_input.cpp @@ -57,13 +57,11 @@ Smt1Input::~Smt1Input() { d_pSmt1Parser->free(d_pSmt1Parser); } -Command* Smt1Input::parseCommand() - throw (ParserException, TypeCheckingException) { +Command* Smt1Input::parseCommand() { return d_pSmt1Parser->parseCommand(d_pSmt1Parser); } -Expr Smt1Input::parseExpr() - throw (ParserException, TypeCheckingException) { +Expr Smt1Input::parseExpr() { return d_pSmt1Parser->parseExpr(d_pSmt1Parser); } diff --git a/src/parser/smt1/smt1_input.h b/src/parser/smt1/smt1_input.h index ce5c8284c..11110e78a 100644 --- a/src/parser/smt1/smt1_input.h +++ b/src/parser/smt1/smt1_input.h @@ -66,8 +66,7 @@ protected: * * @throws ParserException if an error is encountered during parsing. */ - Command* parseCommand() - throw(ParserException, TypeCheckingException); + Command* parseCommand(); /** * Parse an expression from the input. Returns a null @@ -75,8 +74,7 @@ protected: * * @throws ParserException if an error is encountered during parsing. */ - Expr parseExpr() - throw(ParserException, TypeCheckingException); + Expr parseExpr(); private: diff --git a/src/parser/smt2/smt2_input.cpp b/src/parser/smt2/smt2_input.cpp index 2ed8d6966..9b423dcad 100644 --- a/src/parser/smt2/smt2_input.cpp +++ b/src/parser/smt2/smt2_input.cpp @@ -58,13 +58,11 @@ Smt2Input::~Smt2Input() { d_pSmt2Parser->free(d_pSmt2Parser); } -Command* Smt2Input::parseCommand() - throw (ParserException, TypeCheckingException) { +Command* Smt2Input::parseCommand() { return d_pSmt2Parser->parseCommand(d_pSmt2Parser); } -Expr Smt2Input::parseExpr() - throw (ParserException, TypeCheckingException) { +Expr Smt2Input::parseExpr() { return d_pSmt2Parser->parseExpr(d_pSmt2Parser); } diff --git a/src/parser/smt2/smt2_input.h b/src/parser/smt2/smt2_input.h index 62959c766..9b271a2c0 100644 --- a/src/parser/smt2/smt2_input.h +++ b/src/parser/smt2/smt2_input.h @@ -75,8 +75,7 @@ protected: * * @throws ParserException if an error is encountered during parsing. */ - Command* parseCommand() - throw(ParserException, TypeCheckingException); + Command* parseCommand(); /** * Parse an expression from the input. Returns a null @@ -84,8 +83,7 @@ protected: * * @throws ParserException if an error is encountered during parsing. */ - Expr parseExpr() - throw(ParserException, TypeCheckingException); + Expr parseExpr(); };/* class Smt2Input */ diff --git a/src/parser/tptp/tptp_input.cpp b/src/parser/tptp/tptp_input.cpp index 40231853f..d52c7f597 100644 --- a/src/parser/tptp/tptp_input.cpp +++ b/src/parser/tptp/tptp_input.cpp @@ -58,13 +58,11 @@ TptpInput::~TptpInput() { d_pTptpParser->free(d_pTptpParser); } -Command* TptpInput::parseCommand() - throw (ParserException, TypeCheckingException) { +Command* TptpInput::parseCommand() { return d_pTptpParser->parseCommand(d_pTptpParser); } -Expr TptpInput::parseExpr() - throw (ParserException, TypeCheckingException) { +Expr TptpInput::parseExpr() { return d_pTptpParser->parseExpr(d_pTptpParser); } diff --git a/src/parser/tptp/tptp_input.h b/src/parser/tptp/tptp_input.h index da9c67e31..13aa358cd 100644 --- a/src/parser/tptp/tptp_input.h +++ b/src/parser/tptp/tptp_input.h @@ -75,8 +75,7 @@ protected: * * @throws ParserException if an error is encountered during parsing. */ - Command* parseCommand() - throw(ParserException, TypeCheckingException); + Command* parseCommand(); /** * Parse an expression from the input. Returns a null @@ -84,8 +83,7 @@ protected: * * @throws ParserException if an error is encountered during parsing. */ - Expr parseExpr() - throw(ParserException, TypeCheckingException); + Expr parseExpr(); };/* class TptpInput */ -- 2.30.2