More ConstantExpr tweaks.

 - We can safely assume for now that array indices are within 32-bits (we will
   enforce this even on 64-bit targets).

 - We can also safely assume that address fit in 64-bits.

 - Always look up function pointers using 64-bits.

 - Protect a few other places by explicit checks that the type is <= 64-bits,
   when we can fallback to a safe path.


git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73328 91177308-0d34-0410-b5e6-96231b3b80d8

6 files changed, 66 insertions, 53 deletions

diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index 2be099bd..a5ec8daa 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -438,7 +438,7 @@ void Executor::initializeGlobals(ExecutionState &state) {
       addr = Expr::createPointer(0);
     } else {
       addr = Expr::createPointer((unsigned long) (void*) f);
-      legalFunctions.insert(f);
+      legalFunctions.insert((uint64_t) (unsigned long) (void*) f);
     }
     
     globalAddresses.insert(std::make_pair(f, addr));
@@ -1554,14 +1554,13 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
         (void) success;
         StatePair res = fork(*free, EqExpr::create(v, value), true);
         if (res.first) {
-          void *addr = (void*) (unsigned long) value->getConstantValue();
-          std::set<void*>::iterator it = legalFunctions.find(addr);
-          if (it != legalFunctions.end()) {
+          uint64_t addr = value->getZExtValue();
+          if (legalFunctions.count(addr)) {
             f = (Function*) addr;
 
             // Don't give warning on unique resolution
             if (res.second || !first)
-              klee_warning_once(addr, 
+              klee_warning_once((void*) (unsigned long) addr, 
                                 "resolved symbolic function pointer to: %s",
                                 f->getName().c_str());
 
@@ -2373,13 +2372,13 @@ std::string Executor::getAddressInfo(ExecutionState &state,
   info << "\taddress: " << address << "\n";
   uint64_t example;
   if (ConstantExpr *CE = dyn_cast<ConstantExpr>(address)) {
-    example = CE->getConstantValue();
+    example = CE->getZExtValue();
   } else {
     ref<ConstantExpr> value;
     bool success = solver->getValue(state, address, value);
     assert(success && "FIXME: Unhandled solver failure");
     (void) success;
-    example = value->getConstantValue();
+    example = value->getZExtValue();
     info << "\texample: " << example << "\n";
     std::pair< ref<Expr>, ref<Expr> > res = solver->getRange(state, address);
     info << "\trange: [" << res.first << ", " << res.second <<"]\n";
@@ -2650,9 +2649,8 @@ void Executor::executeAlloc(ExecutionState &state,
                             const ObjectState *reallocFrom) {
   size = toUnique(state, size);
   if (ConstantExpr *CE = dyn_cast<ConstantExpr>(size)) {
-    MemoryObject *mo = 
-      memory->allocate(CE->getConstantValue(), isLocal, false, 
-                       state.prevPC->inst);
+    MemoryObject *mo = memory->allocate(CE->getZExtValue(), isLocal, false, 
+                                        state.prevPC->inst);
     if (!mo) {
       bindLocal(target, state, ConstantExpr::alloc(0, kMachinePointerType));
     } else {
diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h
index 4dd89f2a..9cfcf627 100644
--- a/lib/Core/Executor.h
+++ b/lib/Core/Executor.h
@@ -135,8 +135,8 @@ private:
   std::map<const llvm::GlobalValue*, ref<Expr> > globalAddresses;
 
   /// The set of legal function addresses, used to validate function
-  /// pointers.
-  std::set<void*> legalFunctions;
+  /// pointers. We use the actual Function* address as the function address.
+  std::set<uint64_t> legalFunctions;
 
   /// When non-null the bindings that will be used for calls to
   /// klee_make_symbolic in order replay.
diff --git a/lib/Core/Memory.cpp b/lib/Core/Memory.cpp
index 49198df8..05c226d3 100644
--- a/lib/Core/Memory.cpp
+++ b/lib/Core/Memory.cpp
@@ -430,7 +430,7 @@ void ObjectState::write8(ref<Expr> offset, ref<Expr> value) {
 
 ref<Expr> ObjectState::read(ref<Expr> offset, Expr::Width width) const {
   if (ConstantExpr *CE = dyn_cast<ConstantExpr>(offset)) {
-    return read((unsigned) CE->getConstantValue(), width);
+    return read(CE->getZExtValue(32), width);
   } else { 
     switch (width) {
     default: assert(0 && "invalid type");
@@ -619,7 +619,7 @@ ref<Expr> ObjectState::read64(ref<Expr> offset) const {
 void ObjectState::write(ref<Expr> offset, ref<Expr> value) {
   Expr::Width w = value->getWidth();
   if (ConstantExpr *CE = dyn_cast<ConstantExpr>(offset)) {
-    write(CE->getConstantValue(), value);
+    write(CE->getZExtValue(32), value);
   } else {
     switch(w) {
     case  Expr::Bool:  write1(offset, value); break;
@@ -635,7 +635,7 @@ void ObjectState::write(ref<Expr> offset, ref<Expr> value) {
 void ObjectState::write(unsigned offset, ref<Expr> value) {
   Expr::Width w = value->getWidth();
   if (ConstantExpr *CE = dyn_cast<ConstantExpr>(value)) {
-    uint64_t val = CE->getConstantValue();
+    uint64_t val = CE->getZExtValue();
     switch(w) {
     case  Expr::Bool:
     case  Expr::Int8:  write8(offset, val); break;
diff --git a/lib/Core/SeedInfo.cpp b/lib/Core/SeedInfo.cpp
index dc3ff931..b540d271 100644
--- a/lib/Core/SeedInfo.cpp
+++ b/lib/Core/SeedInfo.cpp
@@ -79,7 +79,7 @@ void SeedInfo::patchSeed(const ExecutionState &state,
     ReadExpr *re = it->get();
     if (ConstantExpr *CE = dyn_cast<ConstantExpr>(re->index)) {
       directReads.insert(std::make_pair(re->updates.root, 
-                                        (unsigned) CE->getConstantValue()));
+                                        (unsigned) CE->getZExtValue(32)));
     }
   }
   
@@ -93,7 +93,9 @@ void SeedInfo::patchSeed(const ExecutionState &state,
     // If not in bindings then this can't be a violation?
     Assignment::bindings_ty::iterator it2 = assignment.bindings.find(array);
     if (it2 != assignment.bindings.end()) {
-      ref<Expr> isSeed = EqExpr::create(read, ConstantExpr::alloc(it2->second[i], Expr::Int8));
+      ref<Expr> isSeed = EqExpr::create(read, 
+                                        ConstantExpr::alloc(it2->second[i], 
+                                                            Expr::Int8));
       bool res;
       bool success = solver->mustBeFalse(tmp, isSeed, res);
       assert(success && "FIXME: Unhandled solver failure");
@@ -103,8 +105,10 @@ void SeedInfo::patchSeed(const ExecutionState &state,
         bool success = solver->getValue(tmp, read, value);
         assert(success && "FIXME: Unhandled solver failure");            
         (void) success;
-        it2->second[i] = value->getConstantValue();
-        tmp.addConstraint(EqExpr::create(read, ConstantExpr::alloc(it2->second[i], Expr::Int8)));
+        it2->second[i] = value->getZExtValue(8);
+        tmp.addConstraint(EqExpr::create(read, 
+                                         ConstantExpr::alloc(it2->second[i], 
+                                                             Expr::Int8)));
       } else {
         tmp.addConstraint(isSeed);
       }
@@ -126,7 +130,9 @@ void SeedInfo::patchSeed(const ExecutionState &state,
     for (unsigned i=0; i<array->size; ++i) {
       ref<Expr> read = ReadExpr::create(UpdateList(array, 0),
                                         ConstantExpr::alloc(i, Expr::Int32));
-      ref<Expr> isSeed = EqExpr::create(read, ConstantExpr::alloc(it->second[i], Expr::Int8));
+      ref<Expr> isSeed = EqExpr::create(read, 
+                                        ConstantExpr::alloc(it->second[i], 
+                                                            Expr::Int8));
       bool res;
       bool success = solver->mustBeFalse(tmp, isSeed, res);
       assert(success && "FIXME: Unhandled solver failure");
@@ -136,8 +142,10 @@ void SeedInfo::patchSeed(const ExecutionState &state,
         bool success = solver->getValue(tmp, read, value);
         assert(success && "FIXME: Unhandled solver failure");            
         (void) success;
-        it->second[i] = value->getConstantValue();
-        tmp.addConstraint(EqExpr::create(read, ConstantExpr::alloc(it->second[i], Expr::Int8)));
+        it->second[i] = value->getZExtValue(8);
+        tmp.addConstraint(EqExpr::create(read, 
+                                         ConstantExpr::alloc(it->second[i], 
+                                                             Expr::Int8)));
       } else {
         tmp.addConstraint(isSeed);
       }
diff --git a/lib/Solver/FastCexSolver.cpp b/lib/Solver/FastCexSolver.cpp
index 8c2fcfe6..e9f40a49 100644
--- a/lib/Solver/FastCexSolver.cpp
+++ b/lib/Solver/FastCexSolver.cpp
@@ -453,17 +453,19 @@ public:
       // FIXME: This is imprecise, we need to look through the existing writes
       // to see if this is an initial read or not.
       if (ConstantExpr *CE = dyn_cast<ConstantExpr>(re->index)) {
-        if (CE->getConstantValue() < array->size) {
+        uint64_t index = CE->getZExtValue();
+
+        if (index < array->size) {
           // If the range is fixed, just set that; even if it conflicts with the
           // previous range it should be a better guess.
           if (range.isFixed()) {
-            cod.setPossibleValue(CE->getConstantValue(), range.min());
+            cod.setPossibleValue(index, range.min());
           } else {
-            CexValueData cvd = cod.getPossibleValues(CE->getConstantValue());
+            CexValueData cvd = cod.getPossibleValues(index);
             CexValueData tmp = cvd.set_intersection(range);
 
             if (!tmp.isEmpty())
-              cod.setPossibleValues(CE->getConstantValue(), tmp);
+              cod.setPossibleValues(index, tmp);
           }
         }
       } else {
@@ -637,23 +639,26 @@ public:
       BinaryExpr *be = cast<BinaryExpr>(e);
       if (range.isFixed()) {
         if (ConstantExpr *CE = dyn_cast<ConstantExpr>(be->left)) {
-          uint64_t value = CE->getConstantValue();
-          if (range.min()) {
-            propogatePossibleValue(be->right, value);
-          } else {
-            if (value==0) {
-              propogatePossibleValues(be->right, 
-                               CexValueData(1,
-                                            ints::sext(1, 
-                                                       be->right->getWidth(),
-                                                       1)));
+          // FIXME: Handle large widths?
+          if (CE->getWidth() <= 64) {
+            uint64_t value = CE->getZExtValue();
+            if (range.min()) {
+              propogatePossibleValue(be->right, value);
             } else {
-              // XXX heuristic / lossy, could be better to pick larger range?
-              propogatePossibleValues(be->right, CexValueData(0, value-1));
+              CexValueData range;
+              if (value==0) {
+                range = CexValueData(1, 
+                                     bits64::maxValueOfNBits(CE->getWidth()));
+              } else {
+                // FIXME: heuristic / lossy, could be better to pick larger
+                // range?
+                range = CexValueData(0, value - 1);
+              }
+              propogatePossibleValues(be->right, range);
             }
+          } else {
+            // XXX what now
           }
-        } else {
-          // XXX what now
         }
       }
       break;
@@ -833,15 +838,17 @@ public:
       BinaryExpr *be = cast<BinaryExpr>(e);
       if (range.isFixed()) {
         if (ConstantExpr *CE = dyn_cast<ConstantExpr>(be->left)) {
-          uint64_t value = CE->getConstantValue();
-          if (range.min()) {
-            // If the equality is true, then propogate the value.
-            propogateExactValue(be->right, value);
-          } else {
-            // If the equality is false and the comparison is of booleans, then
-            // we can infer the value to propogate.
-            if (be->right->getWidth() == Expr::Bool) {
-              propogateExactValue(be->right, !value);
+          // FIXME: Handle large widths?
+          if (CE->getWidth() <= 64) {
+            uint64_t value = CE->getZExtValue();
+            if (range.min()) {
+              // If the equality is true, then propogate the value.
+              propogateExactValue(be->right, value);
+            } else {
+              // If the equality is false and the comparison is of booleans,
+              // then we can infer the value to propogate.
+              if (be->right->getWidth() == Expr::Bool)
+                propogateExactValue(be->right, !value);
             }
           }
         }
diff --git a/lib/Solver/STPBuilder.cpp b/lib/Solver/STPBuilder.cpp
index 3d6f789e..2c03c483 100644
--- a/lib/Solver/STPBuilder.cpp
+++ b/lib/Solver/STPBuilder.cpp
@@ -587,7 +587,7 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
     
     if (ConstantExpr *CE = dyn_cast<ConstantExpr>(de->right)) {
       if (CE->getWidth() <= 64) {
-        uint64_t divisor = CE->getConstantValue();
+        uint64_t divisor = CE->getZExtValue();
       
         if (bits64::isPowerOfTwo(divisor)) {
           return bvRightShift(left,
@@ -629,7 +629,7 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
     
     if (ConstantExpr *CE = dyn_cast<ConstantExpr>(de->right)) {
       if (CE->getWidth() <= 64) {
-        uint64_t divisor = CE->getConstantValue();
+        uint64_t divisor = CE->getZExtValue();
 
         if (bits64::isPowerOfTwo(divisor)) {
           unsigned bits = bits64::indexOfSingleBit(divisor);
@@ -644,8 +644,8 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
           }
         }
 
-      // Use fast division to compute modulo without explicit division for
-      // constant divisor.
+        // Use fast division to compute modulo without explicit division for
+        // constant divisor.
 
         if (optimizeDivides) {
           if (*width_out == 32) { //only works for 32-bit division