From 91c5d9967dbea3b4ca8163f9a2cc6cbffb323baf Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Fri, 11 Jun 2010 05:29:42 +0000 Subject: [PATCH] * Make GetUnsignedConst a member function of ASTNode. * In GetUnsignedConst check the position of the maximum bit only if the size is > , not >= git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@832 e59a4935-1847-0410-ae03-e826735625c1 --- src/AST/ASTNode.cpp | 25 +++++++++++++++++ src/AST/ASTNode.h | 3 ++ src/AST/ASTmisc.cpp | 28 ++----------------- .../CounterExample.cpp | 4 +-- src/printer/CPrinter.cpp | 20 ++++++------- src/printer/PLPrinter.cpp | 6 ++-- src/printer/SMTLIB1Printer.cpp | 6 ++-- src/printer/SMTLIB2Printer.cpp | 6 ++-- src/simplifier/consteval.cpp | 6 ++-- src/simplifier/simplifier.cpp | 6 ++-- src/to-sat/BitBlastNew.cpp | 4 +-- 11 files changed, 59 insertions(+), 55 deletions(-) diff --git a/src/AST/ASTNode.cpp b/src/AST/ASTNode.cpp index fe1dc41..09d43f1 100644 --- a/src/AST/ASTNode.cpp +++ b/src/AST/ASTNode.cpp @@ -159,6 +159,31 @@ namespace BEEV return ((ASTBVConst *) _int_node_ptr)->GetBVConst(); } //End of GetBVConst() + unsigned int ASTNode::GetUnsignedConst() const + { + const ASTNode& n = *this; + assert(BVCONST == n.GetKind()); + + if (sizeof(unsigned int) * 8 < n.GetValueWidth()) + { + // It may only contain a small value in a bit type, + // which fits nicely into an unsigned int. This is + // common for functions like: bvshl(bv1[128], + // bv1[128]) where both operands have the same type. + signed long maxBit = CONSTANTBV::Set_Max(n.GetBVConst()); + if (maxBit >= ((signed long) sizeof(unsigned int)) * 8) + { + n.LispPrint(cerr); //print the node so they can find it. + FatalError("GetUnsignedConst: cannot convert bvconst "\ + "of length greater than 32 to unsigned int"); + } + } + return (unsigned int) *((unsigned int *) n.GetBVConst()); + } //end of GetUnsignedConst + + + + void ASTNode::NFASTPrint(int l, int max, int prefix) const { //**************************************** diff --git a/src/AST/ASTNode.h b/src/AST/ASTNode.h index 3f4c6b0..013247d 100644 --- a/src/AST/ASTNode.h +++ b/src/AST/ASTNode.h @@ -335,6 +335,9 @@ namespace BEEV //Get the BVCONST value. CBV GetBVConst() const; + unsigned int GetUnsignedConst() const; + + /******************************************************************* * ASTNode is of type BV <==> ((indexwidth=0)&&(valuewidth>0))* * ASTNode is of type ARRAY <==> ((indexwidth>0)&&(valuewidth>0))* diff --git a/src/AST/ASTmisc.cpp b/src/AST/ASTmisc.cpp index b700eb5..23b3bc8 100644 --- a/src/AST/ASTmisc.cpp +++ b/src/AST/ASTmisc.cpp @@ -262,9 +262,9 @@ namespace BEEV FatalError("BVTypeCheck: should have exactly 3 args\n", n); if (!(BVCONST == n[1].GetKind() && BVCONST == n[2].GetKind())) FatalError("BVTypeCheck: indices should be BVCONST\n", n); - if (n.GetValueWidth() != GetUnsignedConst(n[1]) - GetUnsignedConst(n[2]) + 1) + if (n.GetValueWidth() != n[1].GetUnsignedConst() - n[2].GetUnsignedConst() + 1) FatalError("BVTypeCheck: length mismatch\n", n); - if (GetUnsignedConst(n[1]) >= n[0].GetValueWidth()) + if (n[1].GetUnsignedConst() >= n[0].GetValueWidth()) FatalError("BVTypeCheck: Top index of select is greater or equal to the bitwidth.\n", n); break; case BVLEFTSHIFT: @@ -351,30 +351,6 @@ namespace BEEV return true; } //End of TypeCheck function - //Return the unsigned constant value of the input 'n' - unsigned int GetUnsignedConst(const ASTNode n) - { - if(BVCONST != n.GetKind()){ - FatalError("GetUnsignedConst: cannot extract an "\ - "unsigned value from a non-bvconst"); - } - - if (sizeof(unsigned int) * 8 <= n.GetValueWidth()) - { - // It may only contain a small value in a bit type, - // which fits nicely into an unsigned int. This is - // common for functions like: bvshl(bv1[128], - // bv1[128]) where both operands have the same type. - signed long maxBit = CONSTANTBV::Set_Max(n.GetBVConst()); - if (maxBit >= ((signed long) sizeof(unsigned int)) * 8) - { - n.LispPrint(cerr); //print the node so they can find it. - FatalError("GetUnsignedConst: cannot convert bvconst "\ - "of length greater than 32 to unsigned int"); - } - } - return (unsigned int) *((unsigned int *) n.GetBVConst()); - } //end of GetUnsignedConst //if a is READ(Arr,const) or SYMBOL, and b is BVCONST then return 1 //if b is READ(Arr,const) or SYMBOL, and a is BVCONST then return -1 diff --git a/src/absrefine_counterexample/CounterExample.cpp b/src/absrefine_counterexample/CounterExample.cpp index e4ab1d0..be693a0 100644 --- a/src/absrefine_counterexample/CounterExample.cpp +++ b/src/absrefine_counterexample/CounterExample.cpp @@ -69,7 +69,7 @@ namespace BEEV v = _ASTNode_to_BitvectorMap[symbol]; //kk is the index of BVGETBIT - const unsigned int kk = GetUnsignedConst(s[1]); + const unsigned int kk = s[1].GetUnsignedConst(); //Collect the bits of 'symbol' and store in v. Store //in reverse order. @@ -868,7 +868,7 @@ namespace BEEV GetCounterExample(t, readexpr); //cout << "ASSERT( "; //cout << " = "; - out_int.push_back(GetUnsignedConst(val)); + out_int.push_back(val.GetUnsignedConst()); //cout << "\n"; } } diff --git a/src/printer/CPrinter.cpp b/src/printer/CPrinter.cpp index 99af73c..dce9d36 100644 --- a/src/printer/CPrinter.cpp +++ b/src/printer/CPrinter.cpp @@ -149,8 +149,8 @@ namespace printer // we only accept indices that are byte-aligned // (e.g., [15:8], [23:16]) // and round down to byte indices rather than bit indices - upper = GetUnsignedConst(c[1]); - lower = GetUnsignedConst(c[2]); + upper = c[1].GetUnsignedConst(); + lower = c[2].GetUnsignedConst(); assert(upper > lower); assert(lower % 8 == 0); assert((upper + 1) % 8 == 0); @@ -178,7 +178,7 @@ namespace printer os << "("; C_Print1(os, c[0], indentation, letize); os << " << "; - os << GetUnsignedConst(c[1]); + os << c[1].GetUnsignedConst(); os << ")"; break; case BVRIGHTSHIFT: @@ -187,7 +187,7 @@ namespace printer os << "("; C_Print1(os, c[0], indentation, letize); os << " >> "; - os << GetUnsignedConst(c[1]); + os << c[1].GetUnsignedConst(); os << ")"; break; case BVMULT: @@ -308,14 +308,14 @@ namespace printer // comparison if (LHSkind == BVEXTRACT) { - upper = GetUnsignedConst(c[0].GetChildren()[1]); - lower = GetUnsignedConst(c[0].GetChildren()[2]); + upper = c[0].GetChildren()[1].GetUnsignedConst(); + lower = c[0].GetChildren()[2].GetUnsignedConst(); num_bytes = (upper - lower + 1) / 8; } else if (RHSkind == BVEXTRACT) { - upper = GetUnsignedConst(c[1].GetChildren()[1]); - lower = GetUnsignedConst(c[1].GetChildren()[2]); + upper = c[1].GetChildren()[1].GetUnsignedConst(); + lower = c[1].GetChildren()[2].GetUnsignedConst(); num_bytes = (upper - lower + 1) / 8; } @@ -478,8 +478,8 @@ namespace printer // see if it's a BVEXTRACT, and if so, whether it's multi-byte if (it->second.GetKind() == BVEXTRACT) { - upper = GetUnsignedConst(it->second.GetChildren()[1]); - lower = GetUnsignedConst(it->second.GetChildren()[2]); + upper = it->second.GetChildren()[1].GetUnsignedConst(); + lower = it->second.GetChildren()[2].GetUnsignedConst(); num_bytes = (upper - lower + 1) / 8; assert(num_bytes > 0); } diff --git a/src/printer/PLPrinter.cpp b/src/printer/PLPrinter.cpp index d6c791e..499ac62 100644 --- a/src/printer/PLPrinter.cpp +++ b/src/printer/PLPrinter.cpp @@ -162,9 +162,9 @@ string functionToCVCName(const Kind k) { case BVEXTRACT: PL_Print1(os, c[0], indentation, letize); os << "["; - os << GetUnsignedConst(c[1]); + os << c[1].GetUnsignedConst(); os << ":"; - os << GetUnsignedConst(c[2]); + os << c[2].GetUnsignedConst(); os << "]"; break; case BVLEFTSHIFT: @@ -175,7 +175,7 @@ string functionToCVCName(const Kind k) { { FatalError("PL_Print1: The shift argument to a left shift must be a constant. Found:",c[1]); } - os << GetUnsignedConst(c[1]); + os << c[1].GetUnsignedConst(); os << ")"; os << "["; os << (c[0].GetValueWidth()-1); diff --git a/src/printer/SMTLIB1Printer.cpp b/src/printer/SMTLIB1Printer.cpp index d56f3b7..0d318e8 100644 --- a/src/printer/SMTLIB1Printer.cpp +++ b/src/printer/SMTLIB1Printer.cpp @@ -181,7 +181,7 @@ void printSMTLIB1VarDeclsToStream(ASTNodeSet& symbols, ostream& os) case BVSX: case BVZX: { - unsigned int amount = GetUnsignedConst(c[1]); + unsigned int amount = c[1].GetUnsignedConst(); if (BVZX == kind) os << "(zero_extend["; else @@ -194,8 +194,8 @@ void printSMTLIB1VarDeclsToStream(ASTNodeSet& symbols, ostream& os) break; case BVEXTRACT: { - unsigned int upper = GetUnsignedConst(c[1]); - unsigned int lower = GetUnsignedConst(c[2]); + unsigned int upper = c[1].GetUnsignedConst(); + unsigned int lower = c[2].GetUnsignedConst(); assert(upper >= lower); os << "(extract[" << upper << ":" << lower << "] "; SMTLIB1_Print1(os, c[0], indentation, letize); diff --git a/src/printer/SMTLIB2Printer.cpp b/src/printer/SMTLIB2Printer.cpp index 9f437c1..8d3b3fd 100644 --- a/src/printer/SMTLIB2Printer.cpp +++ b/src/printer/SMTLIB2Printer.cpp @@ -177,7 +177,7 @@ void printVarDeclsToStream(ASTNodeSet& symbols, ostream& os) case BVSX: case BVZX: { - unsigned int amount = GetUnsignedConst(c[1]); + unsigned int amount = c[1].GetUnsignedConst(); if (BVZX == kind) os << "((_ zero_extend "; else @@ -190,8 +190,8 @@ void printVarDeclsToStream(ASTNodeSet& symbols, ostream& os) break; case BVEXTRACT: { - unsigned int upper = GetUnsignedConst(c[1]); - unsigned int lower = GetUnsignedConst(c[2]); + unsigned int upper = c[1].GetUnsignedConst(); + unsigned int lower = c[2].GetUnsignedConst(); assert(upper >= lower); os << "((_ extract " << upper << " " << lower << ") "; SMTLIB2_Print1(os, c[0], indentation, letize); diff --git a/src/simplifier/consteval.cpp b/src/simplifier/consteval.cpp index d81f238..8fbab60 100644 --- a/src/simplifier/consteval.cpp +++ b/src/simplifier/consteval.cpp @@ -135,7 +135,7 @@ namespace BEEV // the shift is destructive, get a copy. CONSTANTBV::BitVector_Interval_Copy(output, tmp0, 0, 0, inputwidth); - unsigned int shift = GetUnsignedConst(shiftNode); + unsigned int shift = shiftNode.GetUnsignedConst(); if (k == BVLEFTSHIFT) CONSTANTBV::BitVector_Move_Left(output, shift); @@ -201,8 +201,8 @@ namespace BEEV { output = CONSTANTBV::BitVector_Create(inputwidth, true); tmp0 = children[0].GetBVConst(); - unsigned int hi = GetUnsignedConst(children[1]); - unsigned int low = GetUnsignedConst(children[2]); + unsigned int hi = children[1].GetUnsignedConst(); + unsigned int low = children[2].GetUnsignedConst(); unsigned int len = hi - low + 1; CONSTANTBV::BitVector_Destroy(output); diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp index d2a2680..4a5b504 100644 --- a/src/simplifier/simplifier.cpp +++ b/src/simplifier/simplifier.cpp @@ -2005,8 +2005,8 @@ namespace BEEV ASTNode zero = _bm->CreateBVConst(32, 0); //recall that the indices of BVEXTRACT are always 32 bits //long. therefore doing a GetBVUnsigned is ok. - unsigned int i_val = GetUnsignedConst(i); - unsigned int j_val = GetUnsignedConst(j); + unsigned int i_val = i.GetUnsignedConst(); + unsigned int j_val = j.GetUnsignedConst(); // a0[i:0] and len(a0)=i+1, then return a0 if (0 == j_val && a_len == a0.GetValueWidth()) @@ -2502,7 +2502,7 @@ namespace BEEV } else { - const unsigned int shift = GetUnsignedConst(b); + const unsigned int shift = b.GetUnsignedConst(); if (shift >= width) { output = _bm->CreateZeroConst(width); diff --git a/src/to-sat/BitBlastNew.cpp b/src/to-sat/BitBlastNew.cpp index 82420d4..c5b3650 100644 --- a/src/to-sat/BitBlastNew.cpp +++ b/src/to-sat/BitBlastNew.cpp @@ -223,8 +223,8 @@ const BBNodeVec BitBlasterNew::BBTerm(const ASTNode& term, BBNodeSet& support) { // with memo-ization. const BBNodeVec& bbkids = BBTerm(term[0], support); - const unsigned int high = GetUnsignedConst(term[1]); - const unsigned int low = GetUnsignedConst(term[2]); + const unsigned int high = term[1].GetUnsignedConst(); + const unsigned int low = term[2].GetUnsignedConst(); BBNodeVec::const_iterator bbkfit = bbkids.begin(); // I should have used pointers to BBNodeVec, to avoid this crock -- 2.47.3