diff options
| -rw-r--r-- | stp/AST/AST.cpp | 34 |
1 files changed, 13 insertions, 21 deletions
diff --git a/stp/AST/AST.cpp b/stp/AST/AST.cpp index ab290395..87541877 100644 --- a/stp/AST/AST.cpp +++ b/stp/AST/AST.cpp @@ -749,31 +749,23 @@ namespace BEEV { //Create a ASTBVConst node ASTNode BeevMgr::CreateBVConst(unsigned int width, unsigned long long int bvconst){ - if(width > (sizeof(unsigned long long int)<<3) || width <= 0) + if(width == 0 || width > (sizeof(unsigned long long int)<<3)) FatalError("CreateBVConst: trying to create a bvconst of width: ", ASTUndefined, width); - CBV bv = CONSTANTBV::BitVector_Create(width, true); - unsigned long c_val = (0x00000000ffffffffLL) & bvconst; - unsigned int copied = 0; - - // sizeof(unsigned long) returns the number of bytes in unsigned - // long. In order to convert it to bits, we need to shift left by - // 3. Hence, sizeof(unsigned long) << 3 - - //The algo below works as follows: It starts by copying the - //lower-order bits of the input "bvconst" in chunks of size = - //number of bits in unsigned long. The variable "copied" keeps - //track of the number of chunks copied so far - - while(copied + (sizeof(unsigned long)<<3) < width){ - CONSTANTBV::BitVector_Chunk_Store(bv, sizeof(unsigned long)<<3,copied,c_val); - bvconst = bvconst >> (sizeof(unsigned long) << 3); - c_val = (0x00000000ffffffffLL) & bvconst; - copied += sizeof(unsigned long) << 3; + + // Copy bvconst in using at most MaxChunkSize chunks, starting with the + // least significant bits. + const uint32_t MaxChunkSize = 32; + for (unsigned offset = 0; offset != width;) { + uint32_t numbits = std::min(MaxChunkSize, width - offset); + uint32_t mask = ~0 >> (32 - numbits); + CONSTANTBV::BitVector_Chunk_Store(bv, numbits, offset, + (bvconst >> offset) & mask); + offset += numbits; } - CONSTANTBV::BitVector_Chunk_Store(bv,width - copied,copied,c_val); - return CreateBVConst(bv,width); + + return CreateBVConst(bv, width); } //Create a ASTBVConst node from std::string |