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.

diff --git a/src/parser/antlr_input.h b/src/parser/antlr_input.h
index 68a62274d6dc408c5653cebea49471e4c4955112..a2fe99f52b7e632482ac6cb5a0e017616e6e552b 100644 (file)
--- 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 52fadae66e909aa88aa7a2d37f045145050a6c9e..8328306bec8829b16138d18b5b0905224285670f 100644 (file)
--- 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 398ac4bd08885d19ff4b7b3a639d2cba7f85f522..973e1c1736e5a564a6f15940f5f42d4422cc0d0f 100644 (file)
--- 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 <code>Expr</code>
    * 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 0203ed80609c2c89746914714fda4f1126fe037d..f4b36469b99b440ab80155951d39416cc3343e29 100644 (file)
--- 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 65d46220bce48a91700fd15bf572e243f0daf686..8b77362b28e298d0fbee88da7dd26a0d6a4c38bc 100644 (file)
--- 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 156ca083f6b6e51a91b6437bda50464909f63bb8..2dae4ef66de12429dd1293771078fd96b78c1c43 100644 (file)
--- 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 ce5c8284c4ad50fd60424b718827b72d275bf74e..11110e78a822d5eeaf1757742a613f8d3bcb474f 100644 (file)
--- 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 2ed8d69666a9c030b479df4601f4a91d707b1850..9b423dcad0cf54ac5f73f2588e4bb4f853f744c6 100644 (file)
--- 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 62959c7661fda88a2253dcbe471ae1481bcada6b..9b271a2c008c91fbfb5ce5570109ffd9bbcf4b61 100644 (file)
--- 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 40231853fdeccf256114eb863fbcd285a10cd77a..d52c7f59730bf54a49febd25ca57c00d595729a4 100644 (file)
--- 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 da9c67e31fd3548c4cbc50e53ea9e14d08622be9..13aa358cda23330d7c756aea79cb0c3117b3e4e4 100644 (file)
--- 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 */