From 58e47f72906773748183a141f314a21f5b970b0b Mon Sep 17 00:00:00 2001 From: Tianyi Liang Date: Tue, 21 Oct 2014 23:10:35 -0500 Subject: [PATCH] Fixed bug 589 --- src/theory/strings/regexp_operation.cpp | 10 +++- src/theory/strings/regexp_operation.h | 2 + src/theory/strings/theory_strings.cpp | 4 ++ src/theory/strings/theory_strings.h | 3 + .../strings/theory_strings_preprocess.cpp | 2 +- .../strings/theory_strings_rewriter.cpp | 24 ++++++-- src/theory/strings/theory_strings_rewriter.h | 1 + src/util/regexp.h | 57 +++++++++++++------ 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() <= RMAXINT, "Exceeded LONG_MAX in RegExpOpr::containC2"); unsigned y = n[0].getConst().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() <= RMAXINT, "Exceeded LONG_MAX in RegExpOpr::containC2"); unsigned y = n[0].getConst().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 #include #include +#include #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() <= RMAXINT, "Exceeded LONG_MAX in string model"); unsigned lvalue = lts[i].getConst().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() <= RMAXINT, "Exceeded LONG_MAX in string model"); unsigned lvalue = v.getConst().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() <= RMAXINT, "Exceeded LONG_MAX in string model"); StringEnumeratorLength sel(lts_values[i].getConst().getNumerator().toUnsignedInt()); for( unsigned j=0; j + 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().getNumerator().toUnsignedInt(); + unsigned len = t[ret].getConst().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().sgn()>=0 && node[2].getConst().sgn()>=0) { - int i = node[1].getConst().getNumerator().toUnsignedInt(); - int j = node[2].getConst().getNumerator().toUnsignedInt(); + CVC4::Rational sum(node[1].getConst() + node[2].getConst()); if( node[0].isConst() ) { - if( node[0].getConst().size() >= (unsigned) (i + j) ) { + CVC4::Rational size(node[0].getConst().size()); + if( size >= sum ) { + //because size is smaller than MAX_INT + size_t i = node[1].getConst().getNumerator().toUnsignedInt(); + size_t j = node[2].getConst().getNumerator().toUnsignedInt(); retNode = NodeManager::currentNM()->mkConst( node[0].getConst().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().size() >= (unsigned) (i + j) ) { + CVC4::Rational size2(node[0][0].getConst().size()); + if( size2 >= sum ) { + //because size2 is smaller than MAX_INT + size_t i = node[1].getConst().getNumerator().toUnsignedInt(); + size_t j = node[2].getConst().getNumerator().toUnsignedInt(); retNode = NodeManager::currentNM()->mkConst( node[0][0].getConst().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(); CVC4::String t = node[1].getConst(); - int i = node[2].getConst().getNumerator().toUnsignedInt(); + CVC4::Rational RMAXINT(LONG_MAX); + Assert(node[2].getConst() <= RMAXINT, "Number exceeds LONG_MAX in string index_of"); + std::size_t i = node[2].getConst().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() <= RMAXINT, "Exceeded LONG_MAX in string REGEXP_LOOP (1)"); unsigned l = node[1].getConst().getNumerator().toUnsignedInt(); std::vector< Node > vec_nodes; for(unsigned i=0; imkNode(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() <= RMAXINT, "Exceeded LONG_MAX in string REGEXP_LOOP (2)"); unsigned u = node[2].getConst().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 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 #include #include -#include "util/exception.h" +#include //#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= 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= 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= 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 ret_vec; std::vector::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 ret_vec; std::vector::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; -- 2.30.2