From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Fri, 22 Feb 2013 21:48:13 +0000 (-0500)
Subject: Disallow overflow in bitvector literals (parser only)
X-Git-Tag: cvc5-1.0.0~7396
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=56b7a4f494dfe069fc4cbdb1dcd05c23c9b59a1d;p=cvc5.git

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 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 <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 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 */