Fixed bug 589

8 files changed, 76 insertions, 27 deletions

diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp
index e769eb712..69b089c84 100644
--- a/src/theory/strings/regexp_operation.cpp
+++ b/src/theory/strings/regexp_operation.cpp
@@ -21,18 +21,20 @@ namespace CVC4 {
 namespace theory {
 namespace strings {
 
-RegExpOpr::RegExpOpr() {
+RegExpOpr::RegExpOpr()
+  : d_card( 256 ),
+  RMAXINT( LONG_MAX )
+{
   d_emptyString = NodeManager::currentNM()->mkConst( ::CVC4::String("") );
   d_true = NodeManager::currentNM()->mkConst( true );
   d_false = NodeManager::currentNM()->mkConst( false );
+  d_emptySingleton = NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, d_emptyString );
   d_zero = NodeManager::currentNM()->mkConst( ::CVC4::Rational(0) );
   d_one = NodeManager::currentNM()->mkConst( ::CVC4::Rational(1) );
-  d_emptySingleton = NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, d_emptyString );
   std::vector< Node > nvec;
   d_emptyRegexp = NodeManager::currentNM()->mkNode( kind::REGEXP_EMPTY, nvec );
   d_sigma = NodeManager::currentNM()->mkNode( kind::REGEXP_SIGMA, nvec );
   d_sigma_star = NodeManager::currentNM()->mkNode( kind::REGEXP_STAR, d_sigma );
-  d_card = 256;
 }
 
 int RegExpOpr::gcd ( int a, int b ) {
@@ -1284,6 +1286,7 @@ Node RegExpOpr::intersectInternal( Node r1, Node r2, std::map< unsigned, std::se
 
 bool RegExpOpr::containC2(unsigned cnt, Node n) {
   if(n.getKind() == kind::REGEXP_RV) {
+    Assert(n[0].getConst<Rational>() <= RMAXINT, "Exceeded LONG_MAX in RegExpOpr::containC2");
     unsigned y = n[0].getConst<Rational>().getNumerator().toUnsignedInt();
     return cnt == y;
   } else if(n.getKind() == kind::REGEXP_CONCAT) {
@@ -1322,6 +1325,7 @@ void RegExpOpr::convert2(unsigned cnt, Node n, Node &r1, Node &r2) {
     r1 = d_emptySingleton;
     r2 = d_emptySingleton;
   } else if(n.getKind() == kind::REGEXP_RV) {
+    Assert(n[0].getConst<Rational>() <= RMAXINT, "Exceeded LONG_MAX in RegExpOpr::containC2");
     unsigned y = n[0].getConst<Rational>().getNumerator().toUnsignedInt();
     r1 = d_emptySingleton;
     if(cnt == y) {
diff --git a/src/theory/strings/regexp_operation.h b/src/theory/strings/regexp_operation.h
index 2ae578cd6..ce3093528 100644
--- a/src/theory/strings/regexp_operation.h
+++ b/src/theory/strings/regexp_operation.h
@@ -22,6 +22,7 @@
 #include <vector>
 #include <set>
 #include <algorithm>
+#include <climits>
 #include "util/hash.h"
 #include "util/regexp.h"
 #include "theory/theory.h"
@@ -46,6 +47,7 @@ private:
   Node d_emptyRegexp;
   Node d_zero;
   Node d_one;
+  CVC4::Rational RMAXINT;
 
   char d_char_start;
   char d_char_end;
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index e0916974e..e8bf87a17 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -35,6 +35,7 @@ namespace strings {
 
 TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo)
   : Theory(THEORY_STRINGS, c, u, out, valuation, logicInfo),
+  RMAXINT(LONG_MAX),
   d_notify( *this ),
   d_equalityEngine(d_notify, c, "theory::strings::TheoryStrings"),
   d_conflict(c, false),
@@ -284,6 +285,7 @@ void TheoryStrings::collectModelInfo( TheoryModel* m, bool fullModel ) {
     Trace("strings-model") << " } (length is " << lts[i] << ")" << std::endl;
     if( lts[i].isConst() ) {
       lts_values.push_back( lts[i] );
+      Assert(lts[i].getConst<Rational>() <= RMAXINT, "Exceeded LONG_MAX in string model");
       unsigned lvalue = lts[i].getConst<Rational>().getNumerator().toUnsignedInt();
       values_used[ lvalue ] = true;
     }else{
@@ -292,6 +294,7 @@ void TheoryStrings::collectModelInfo( TheoryModel* m, bool fullModel ) {
         Node v = d_valuation.getModelValue(lts[i]);
         Trace("strings-model") << "Model value for " << lts[i] << " is " << v << std::endl;
         lts_values.push_back( v );
+        Assert(v.getConst<Rational>() <= RMAXINT, "Exceeded LONG_MAX in string model");
         unsigned lvalue =  v.getConst<Rational>().getNumerator().toUnsignedInt();
         values_used[ lvalue ] = true;
       }else{
@@ -346,6 +349,7 @@ void TheoryStrings::collectModelInfo( TheoryModel* m, bool fullModel ) {
 
 
       //use type enumerator
+      Assert(lts_values[i].getConst<Rational>() <= RMAXINT, "Exceeded LONG_MAX in string model");
       StringEnumeratorLength sel(lts_values[i].getConst<Rational>().getNumerator().toUnsignedInt());
       for( unsigned j=0; j<pure_eq.size(); j++ ){
         Assert( !sel.isFinished() );
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index 797c1bd29..95eba27bc 100644
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -27,6 +27,8 @@
 #include "context/cdchunk_list.h"
 #include "context/cdhashset.h"
 
+#include <climits>
+
 namespace CVC4 {
 namespace theory {
 namespace strings {
@@ -125,6 +127,7 @@ private:
   Node d_false;
   Node d_zero;
   Node d_one;
+  CVC4::Rational RMAXINT;
   // Options
   bool d_opt_fmf;
   bool d_opt_regexp_gcd;
diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index 6e7ca6d95..71db11fe1 100644
--- a/src/theory/strings/theory_strings_preprocess.cpp
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@ -126,7 +126,7 @@ int StringsPreprocess::checkFixLenVar( Node t ) {
     }
   }
   if(ret != 2) {
-    int len = t[ret].getConst<Rational>().getNumerator().toUnsignedInt();
+    unsigned len = t[ret].getConst<Rational>().getNumerator().toUnsignedInt();
     if(len < 2) {
       ret = 2;
     }
diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index e37cabfb6..c952a7b3c 100644
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -382,16 +382,23 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) {
       retNode = NodeManager::currentNM()->mkConst( ::CVC4::String("") );
     } else if( node[1].isConst() && node[2].isConst() ) {
       if(node[1].getConst<Rational>().sgn()>=0 && node[2].getConst<Rational>().sgn()>=0) {
-        int i = node[1].getConst<Rational>().getNumerator().toUnsignedInt();
-        int j = node[2].getConst<Rational>().getNumerator().toUnsignedInt();
+        CVC4::Rational sum(node[1].getConst<Rational>() + node[2].getConst<Rational>());
         if( node[0].isConst() ) {
-          if( node[0].getConst<String>().size() >= (unsigned) (i + j) ) {
+          CVC4::Rational size(node[0].getConst<String>().size());
+          if( size >= sum ) {
+            //because size is smaller than MAX_INT
+            size_t i = node[1].getConst<Rational>().getNumerator().toUnsignedInt();
+            size_t j = node[2].getConst<Rational>().getNumerator().toUnsignedInt();
             retNode = NodeManager::currentNM()->mkConst( node[0].getConst<String>().substr(i, j) );
           } else {
             retNode = NodeManager::currentNM()->mkConst( ::CVC4::String("") );
           }
         } else if(node[0].getKind() == kind::STRING_CONCAT && node[0][0].isConst()) {
-          if( node[0][0].getConst<String>().size() >= (unsigned) (i + j) ) {
+          CVC4::Rational size2(node[0][0].getConst<String>().size());
+          if( size2 >= sum ) {
+            //because size2 is smaller than MAX_INT
+            size_t i = node[1].getConst<Rational>().getNumerator().toUnsignedInt();
+            size_t j = node[2].getConst<Rational>().getNumerator().toUnsignedInt();
             retNode = NodeManager::currentNM()->mkConst( node[0][0].getConst<String>().substr(i, j) );
           }
         }
@@ -451,10 +458,12 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) {
     if( node[0].isConst() && node[1].isConst() && node[2].isConst() ) {
       CVC4::String s = node[0].getConst<String>();
       CVC4::String t = node[1].getConst<String>();
-      int i = node[2].getConst<Rational>().getNumerator().toUnsignedInt();
+      CVC4::Rational RMAXINT(LONG_MAX);
+      Assert(node[2].getConst<Rational>() <= RMAXINT, "Number exceeds LONG_MAX in string index_of");
+      std::size_t i = node[2].getConst<Rational>().getNumerator().toUnsignedInt();
       std::size_t ret = s.find(t, i);
       if( ret != std::string::npos ) {
-        retNode = NodeManager::currentNM()->mkConst( ::CVC4::Rational((int) ret) );
+        retNode = NodeManager::currentNM()->mkConst( ::CVC4::Rational((unsigned) ret) );
       } else {
         retNode = NodeManager::currentNM()->mkConst( ::CVC4::Rational(-1) );
       }
@@ -634,6 +643,8 @@ RewriteResponse TheoryStringsRewriter::preRewrite(TNode node) {
     if(r.getKind() == kind::REGEXP_STAR) {
       retNode = r;
     } else {
+      CVC4::Rational RMAXINT(LONG_MAX);
+      Assert(node[1].getConst<Rational>() <= RMAXINT, "Exceeded LONG_MAX in string REGEXP_LOOP (1)");
       unsigned l = node[1].getConst<Rational>().getNumerator().toUnsignedInt();
       std::vector< Node > vec_nodes;
       for(unsigned i=0; i<l; i++) {
@@ -642,6 +653,7 @@ RewriteResponse TheoryStringsRewriter::preRewrite(TNode node) {
       if(node.getNumChildren() == 3) {
         Node n = vec_nodes.size()==0 ? NodeManager::currentNM()->mkNode(kind::STRING_TO_REGEXP, NodeManager::currentNM()->mkConst(CVC4::String("")))
           : vec_nodes.size()==1 ? r : prerewriteConcatRegExp(NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT, vec_nodes));
+        Assert(node[2].getConst<Rational>() <= RMAXINT, "Exceeded LONG_MAX in string REGEXP_LOOP (2)");
         unsigned u = node[2].getConst<Rational>().getNumerator().toUnsignedInt();
         if(u <= l) {
           retNode = n;
diff --git a/src/theory/strings/theory_strings_rewriter.h b/src/theory/strings/theory_strings_rewriter.h
index d33254e1b..9d04f107f 100644
--- a/src/theory/strings/theory_strings_rewriter.h
+++ b/src/theory/strings/theory_strings_rewriter.h
@@ -23,6 +23,7 @@
 #include "theory/rewriter.h"
 #include "theory/type_enumerator.h"
 #include "expr/attribute.h"
+#include <climits>
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/util/regexp.h b/src/util/regexp.h
index e75ca1fad..2b7bfa303 100644
--- a/src/util/regexp.h
+++ b/src/util/regexp.h
@@ -24,8 +24,9 @@
 #include <string>
 #include <set>
 #include <sstream>
-#include "util/exception.h"
+#include <cassert>
 //#include "util/integer.h"
+#include "util/exception.h"
 #include "util/hash.h"
 
 namespace CVC4 {
@@ -65,7 +66,7 @@ private:
     } else if (c >= 'a' && c <= 'f') {
       return c - 'a' + 10;
     } else {
-      //Assert(c >= 'A' && c <= 'F');
+      assert(c >= 'A' && c <= 'F');
       return c - 'A' + 10;
     }
   }
@@ -151,14 +152,34 @@ public:
     }
   }
 
-  bool strncmp(const String &y, unsigned int n) const {
-    for(unsigned int i=0; i<n; ++i)
+  bool strncmp(const String &y, const std::size_t np) const {
+    std::size_t n = np;
+    std::size_t b = (d_str.size() >= y.d_str.size()) ? d_str.size() : y.d_str.size();
+    std::size_t s = (d_str.size() <= y.d_str.size()) ? d_str.size() : y.d_str.size();
+    if(n > s) {
+      if(b == s) {
+        n = s;
+      } else {
+        return false;
+      }
+    }
+    for(std::size_t i=0; i<n; ++i)
       if(d_str[i] != y.d_str[i]) return false;
     return true;
   }
 
-  bool rstrncmp(const String &y, unsigned int n) const {
-    for(unsigned int i=0; i<n; ++i)
+  bool rstrncmp(const String &y, const std::size_t np) const {
+    std::size_t n = np;
+    std::size_t b = (d_str.size() >= y.d_str.size()) ? d_str.size() : y.d_str.size();
+    std::size_t s = (d_str.size() <= y.d_str.size()) ? d_str.size() : y.d_str.size();
+    if(n > s) {
+      if(b == s) {
+        n = s;
+      } else {
+        return false;
+      }
+    }
+    for(std::size_t i=0; i<n; ++i)
       if(d_str[d_str.size() - i - 1] != y.d_str[y.d_str.size() - i - 1]) return false;
     return true;
   }
@@ -167,8 +188,8 @@ public:
     return ( d_str.size() == 0 );
   }
 
-  unsigned int operator[] (const unsigned int i) const {
-  //Assert( i < d_str.size() && i >= 0);
+  unsigned int operator[] (const std::size_t i) const {
+    assert( i < d_str.size() );
     return d_str[i];
   }
   /*
@@ -208,19 +229,19 @@ public:
     return true;
   }
 
-  std::size_t find(const String &y, const int start = 0) const {
-    if(d_str.size() < y.d_str.size() + (std::size_t) start) return std::string::npos;
-    if(y.d_str.size() == 0) return (std::size_t) start;
+  std::size_t find(const String &y, const std::size_t start = 0) const {
+    if(d_str.size() < y.d_str.size() + start) return std::string::npos;
+    if(y.d_str.size() == 0) return start;
     if(d_str.size() == 0) return std::string::npos;
     std::size_t ret = std::string::npos;
-    for(int i = start; i <= (int) d_str.size() - (int) y.d_str.size(); i++) {
+    for(std::size_t i = start; i <= d_str.size() - y.d_str.size(); i++) {
       if(d_str[i] == y.d_str[0]) {
         std::size_t j=0;
         for(; j<y.d_str.size(); j++) {
           if(d_str[i+j] != y.d_str[j]) break;
         }
         if(j == y.d_str.size()) {
-          ret = (std::size_t) i;
+          ret = i;
           break;
         }
       }
@@ -241,23 +262,25 @@ public:
     }
   }
 
-  String substr(unsigned i) const {
+  String substr(std::size_t i) const {
+    assert(i <= d_str.size());
     std::vector<unsigned int> ret_vec;
     std::vector<unsigned int>::const_iterator itr = d_str.begin() + i;
     ret_vec.insert(ret_vec.end(), itr, d_str.end());
     return String(ret_vec);
   }
-  String substr(unsigned i, unsigned j) const {
+  String substr(std::size_t i, std::size_t j) const {
+    assert(i+j <= d_str.size());
     std::vector<unsigned int> ret_vec;
     std::vector<unsigned int>::const_iterator itr = d_str.begin() + i;
     ret_vec.insert( ret_vec.end(), itr, itr + j );
     return String(ret_vec);
   }
 
-  String prefix(unsigned i) const {
+  String prefix(std::size_t i) const {
     return substr(0, i);
   }
-  String suffix(unsigned i) const {
+  String suffix(std::size_t i) const {
     return substr(d_str.size() - i, i);
   }
   std::size_t overlap(String &y) const;