about summary refs log tree commit diff homepage
path: root/stp
diff options
context:
space:
mode:
authorDaniel Dunbar <daniel@zuster.org>2009-08-01 21:40:15 +0000
committerDaniel Dunbar <daniel@zuster.org>2009-08-01 21:40:15 +0000
commit01a78cc5898a21310fdfadc13c0c702086721d8c (patch)
treedfc334f928f8a5fccfa6f2312ba3287136b57119 /stp
parentbe3fdc136766cb4f2c1fa5b785f3ce74e52f5565 (diff)
downloadklee-01a78cc5898a21310fdfadc13c0c702086721d8c.tar.gz
Rewrite constant initialization to be more portable and readable.
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@77809 91177308-0d34-0410-b5e6-96231b3b80d8
Diffstat (limited to 'stp')
-rw-r--r--stp/AST/AST.cpp34
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