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

4 files changed, 28 insertions, 22 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);
       }