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

1 files changed, 15 insertions, 7 deletions

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);
       }