Fixed bug 589

7 files changed, 36 insertions, 10 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 {