about summary refs log tree commit diff homepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--include/klee/Expr.h28
-rw-r--r--lib/Core/Executor.cpp13
-rw-r--r--lib/Core/Memory.cpp4
-rw-r--r--lib/Core/SpecialFunctionHandler.cpp10
-rw-r--r--lib/Expr/Expr.cpp2
-rw-r--r--lib/Expr/Parser.cpp2
-rw-r--r--lib/Solver/FastCexSolver.cpp4
-rw-r--r--lib/Solver/IndependentSolver.cpp2
-rw-r--r--lib/Solver/STPBuilder.cpp91
-rw-r--r--lib/Solver/Solver.cpp2
10 files changed, 89 insertions, 69 deletions
diff --git a/include/klee/Expr.h b/include/klee/Expr.h
index 70d9abfc..69f9f1df 100644
--- a/include/klee/Expr.h
+++ b/include/klee/Expr.h
@@ -314,6 +314,21 @@ public:
 
   uint64_t getConstantValue() const { return value; }
 
+  /// getZExtValue - Return the constant value for a limited number of bits.
+  ///
+  /// This routine should be used in situations where the width of the constant
+  /// is known to be limited to a certain number of bits.
+  uint64_t getZExtValue(unsigned bits = 64) const {
+    assert(getWidth() <= bits && "Value may be out of range!");
+    return value;
+  }
+
+  /// getLimitedValue - If this value is smaller than the specified limit,
+  /// return it, otherwise return the limit value.
+  uint64_t getLimitedValue(uint64_t Limit = ~0ULL) const {
+    return (value > Limit) ? Limit :  getZExtValue();
+  }
+
   int compareContents(const Expr &b) const { 
     const ConstantExpr &cb = static_cast<const ConstantExpr&>(b);
     if (width != cb.width) return width < cb.width ? -1 : 1;
@@ -357,23 +372,24 @@ public:
   /* Utility Functions */
 
   /// isZero - Is this a constant zero.
-  bool isZero() const { return getConstantValue() == 0; }
+  bool isZero() const { return getZExtValue() == 0; }
+
+  /// isOne - Is this a constant one.
+  bool isOne() const { return getZExtValue() == 1; }
   
   /// isTrue - Is this the true expression.
   bool isTrue() const { 
-    assert(getWidth() == Expr::Bool && "Invalid isTrue() call!");
-    return getConstantValue() == 1;
+    return getZExtValue(1) == 1;
   }
 
   /// isFalse - Is this the false expression.
   bool isFalse() const {
-    assert(getWidth() == Expr::Bool && "Invalid isTrue() call!");
-    return getConstantValue() == 0;
+    return getZExtValue(1) == 0;
   }
 
   /// isAllOnes - Is this constant all ones.
   bool isAllOnes() const {
-    return getConstantValue() == bits64::maxValueOfNBits(getWidth());
+    return getZExtValue(getWidth()) == bits64::maxValueOfNBits(getWidth());
   }
 
   /* Constant Operations */
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index f12aec08..5b22b782 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -1413,7 +1413,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
       // Somewhat gross to create these all the time, but fine till we
       // switch to an internal rep.
       ConstantInt *ci = ConstantInt::get(si->getCondition()->getType(),
-                                         CE->getConstantValue());
+                                         CE->getZExtValue());
       unsigned index = si->findCaseValue(ci);
       transferToBasicBlock(si->getSuccessor(index), si->getParent(), state);
     } else {
@@ -2688,11 +2688,10 @@ void Executor::executeAlloc(ExecutionState &state,
     assert(success && "FIXME: Unhandled solver failure");
     (void) success;
     
-    // Try and start with a small example
-    while (example->getConstantValue() > 128) {
-      ref<ConstantExpr> tmp = 
-        ConstantExpr::alloc(example->getConstantValue() >> 1, 
-                            example->getWidth());
+    // Try and start with a small example.
+    Expr::Width W = example->getWidth();
+    while (example->Ugt(ConstantExpr::alloc(128, W))->isTrue()) {
+      ref<ConstantExpr> tmp = example->LShr(ConstantExpr::alloc(1, W));
       bool res;
       bool success = solver->mayBeTrue(state, EqExpr::create(tmp, size), res);
       assert(success && "FIXME: Unhandled solver failure");      
@@ -3225,7 +3224,7 @@ void Executor::doImpliedValueConcretization(ExecutionState &state,
         assert(!os->readOnly && 
                "not possible? read only object with static read?");
         ObjectState *wos = state.addressSpace.getWriteable(mo, os);
-        wos->write(CE->getConstantValue(), it->second);
+        wos->write(CE, it->second);
       }
     }
   }
diff --git a/lib/Core/Memory.cpp b/lib/Core/Memory.cpp
index d8cf0bdb..49198df8 100644
--- a/lib/Core/Memory.cpp
+++ b/lib/Core/Memory.cpp
@@ -187,7 +187,7 @@ const UpdateList &ObjectState::getUpdates() const {
       if (!Value)
         break;
 
-      Contents[Index->getConstantValue()] = Value;
+      Contents[Index->getZExtValue()] = Value;
     }
 
     // FIXME: We should unique these, there is no good reason to create multiple
@@ -400,7 +400,7 @@ void ObjectState::write8(unsigned offset, uint8_t value) {
 void ObjectState::write8(unsigned offset, ref<Expr> value) {
   // can happen when ExtractExpr special cases
   if (ConstantExpr *CE = dyn_cast<ConstantExpr>(value)) {
-    write8(offset, (uint8_t) CE->getConstantValue());
+    write8(offset, (uint8_t) CE->getZExtValue(8));
   } else {
     setKnownSymbolic(offset, value.get());
       
diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp
index 2ee73457..d2c68b77 100644
--- a/lib/Core/SpecialFunctionHandler.cpp
+++ b/lib/Core/SpecialFunctionHandler.cpp
@@ -198,7 +198,7 @@ SpecialFunctionHandler::readStringAtAddress(ExecutionState &state,
     cur = executor.toUnique(state, cur);
     assert(isa<ConstantExpr>(cur) && 
            "hit symbolic char while reading concrete string");
-    buf[i] = cast<ConstantExpr>(cur)->getConstantValue();
+    buf[i] = cast<ConstantExpr>(cur)->getZExtValue(8);
   }
   buf[i] = 0;
   
@@ -441,7 +441,7 @@ void SpecialFunctionHandler::handleSetForking(ExecutionState &state,
   ref<Expr> value = executor.toUnique(state, arguments[0]);
   
   if (ConstantExpr *CE = dyn_cast<ConstantExpr>(value)) {
-    state.forkDisabled = !CE->getConstantValue();
+    state.forkDisabled = CE->isZero();
   } else {
     executor.terminateStateOnError(state, 
                                    "klee_set_forking requires a constant arg",
@@ -607,7 +607,7 @@ void SpecialFunctionHandler::handleCheckMemoryAccess(ExecutionState &state,
     } else {
       ref<Expr> chk = op.first->getBoundsCheckPointer(address, 
                                                       cast<ConstantExpr>(size)->getConstantValue());
-      if (!cast<ConstantExpr>(chk)->getConstantValue()) {
+      if (!chk->isTrue()) {
         executor.terminateStateOnError(state,
                                        "check_memory_access: memory error",
                                        "ptr.err",
@@ -636,8 +636,8 @@ void SpecialFunctionHandler::handleDefineFixedObject(ExecutionState &state,
   assert(isa<ConstantExpr>(arguments[1]) &&
          "expect constant size argument to klee_define_fixed_object");
   
-  uint64_t address = cast<ConstantExpr>(arguments[0])->getConstantValue();
-  uint64_t size = cast<ConstantExpr>(arguments[1])->getConstantValue();
+  uint64_t address = cast<ConstantExpr>(arguments[0])->getZExtValue();
+  uint64_t size = cast<ConstantExpr>(arguments[1])->getZExtValue();
   MemoryObject *mo = executor.memory->allocateFixed(address, size, state.prevPC->inst);
   executor.bindObjectInState(state, mo, false);
   mo->isUserSpecified = true; // XXX hack;
diff --git a/lib/Expr/Expr.cpp b/lib/Expr/Expr.cpp
index be9051ab..fd43018f 100644
--- a/lib/Expr/Expr.cpp
+++ b/lib/Expr/Expr.cpp
@@ -815,7 +815,7 @@ static ref<Expr> MulExpr_createPartialR(const ref<ConstantExpr> &cl, Expr *r) {
 
   if (type == Expr::Bool) {
     return AndExpr_createPartialR(cl, r);
-  } else if (cl->getConstantValue() == 1) {
+  } else if (cl->isOne()) {
     return r;
   } else if (cl->isZero()) {
     return cl;
diff --git a/lib/Expr/Parser.cpp b/lib/Expr/Parser.cpp
index 1f2f8412..c9d401e0 100644
--- a/lib/Expr/Parser.cpp
+++ b/lib/Expr/Parser.cpp
@@ -1185,7 +1185,7 @@ IntegerResult ParserImpl::ParseIntegerConstant(Expr::Width Type) {
   if (!Res.isValid())
     return IntegerResult();
 
-  return cast<ConstantExpr>(Res.get())->getConstantValue();
+  return cast<ConstantExpr>(Res.get())->getZExtValue(Type);
 }
 
 ExprResult ParserImpl::ParseExtractParenExpr(const Token &Name,
diff --git a/lib/Solver/FastCexSolver.cpp b/lib/Solver/FastCexSolver.cpp
index af2666ab..8c2fcfe6 100644
--- a/lib/Solver/FastCexSolver.cpp
+++ b/lib/Solver/FastCexSolver.cpp
@@ -346,7 +346,7 @@ public:
     if (array.isConstantArray() && 
         index.isFixed() && 
         index.min() < array.size)
-      return ValueRange(array.constantValues[index.min()]->getConstantValue());
+      return ValueRange(array.constantValues[index.min()]->getZExtValue(8));
 
     return ValueRange(0, 255);
   }
@@ -1037,7 +1037,7 @@ FastCexSolver::computeInitialValues(const Query& query,
       ref<Expr> value = cd.evaluatePossible(read);
       
       if (ConstantExpr *CE = dyn_cast<ConstantExpr>(value)) {
-        data.push_back((unsigned char) CE->getConstantValue());
+        data.push_back((unsigned char) CE->getZExtValue(8));
       } else {
         // FIXME: When does this happen?
         return false;
diff --git a/lib/Solver/IndependentSolver.cpp b/lib/Solver/IndependentSolver.cpp
index 1f3ea798..3e19dbc6 100644
--- a/lib/Solver/IndependentSolver.cpp
+++ b/lib/Solver/IndependentSolver.cpp
@@ -104,7 +104,7 @@ public:
       if (!wholeObjects.count(array)) {
         if (ConstantExpr *CE = dyn_cast<ConstantExpr>(re->index)) {
           DenseSet<unsigned> &dis = elements[array];
-          dis.add((unsigned) CE->getConstantValue());
+          dis.add((unsigned) CE->getZExtValue(32));
         } else {
           elements_ty::iterator it2 = elements.find(array);
           if (it2!=elements.end())
diff --git a/lib/Solver/STPBuilder.cpp b/lib/Solver/STPBuilder.cpp
index 8680d0a8..3d6f789e 100644
--- a/lib/Solver/STPBuilder.cpp
+++ b/lib/Solver/STPBuilder.cpp
@@ -571,13 +571,13 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
     ExprHandle right = construct(me->right, width_out);
     assert(*width_out!=1 && "uncanonicalized mul");
 
-    if (ConstantExpr *CE = dyn_cast<ConstantExpr>(me->left)) {
-      return constructMulByConstant(right, *width_out, 
-                                    CE->getConstantValue());
-    } else {
-      ExprHandle left = construct(me->left, width_out);
-      return vc_bvMultExpr(vc, *width_out, left, right);
-    }
+    if (ConstantExpr *CE = dyn_cast<ConstantExpr>(me->left))
+      if (CE->getWidth() <= 64)
+        return constructMulByConstant(right, *width_out, 
+                                      CE->getZExtValue());
+
+    ExprHandle left = construct(me->left, width_out);
+    return vc_bvMultExpr(vc, *width_out, left, right);
   }
 
   case Expr::UDiv: {
@@ -586,15 +586,18 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
     assert(*width_out!=1 && "uncanonicalized udiv");
     
     if (ConstantExpr *CE = dyn_cast<ConstantExpr>(de->right)) {
-      uint64_t divisor = CE->getConstantValue();
+      if (CE->getWidth() <= 64) {
+        uint64_t divisor = CE->getConstantValue();
       
-      if (bits64::isPowerOfTwo(divisor)) {
-        return bvRightShift(left,
-                            bits64::indexOfSingleBit(divisor),
-                            getShiftBits(*width_out));
-      } else if (optimizeDivides) {
-        if (*width_out == 32) //only works for 32-bit division
-          return constructUDivByConstant( left, *width_out, (uint32_t)divisor );
+        if (bits64::isPowerOfTwo(divisor)) {
+          return bvRightShift(left,
+                              bits64::indexOfSingleBit(divisor),
+                              getShiftBits(*width_out));
+        } else if (optimizeDivides) {
+          if (*width_out == 32) //only works for 32-bit division
+            return constructUDivByConstant( left, *width_out, 
+                                            (uint32_t) divisor);
+        }
       }
     } 
 
@@ -607,13 +610,11 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
     ExprHandle left = construct(de->left, width_out);
     assert(*width_out!=1 && "uncanonicalized sdiv");
 
-    if (ConstantExpr *CE = dyn_cast<ConstantExpr>(de->right)) {
-      if (optimizeDivides) {
+    if (ConstantExpr *CE = dyn_cast<ConstantExpr>(de->right))
+      if (optimizeDivides)
 	if (*width_out == 32) //only works for 32-bit division
 	  return constructSDivByConstant( left, *width_out, 
-                                          CE->getConstantValue());
-      }
-    } 
+                                          CE->getZExtValue(32));
 
     // XXX need to test for proper handling of sign, not sure I
     // trust STP
@@ -627,30 +628,34 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
     assert(*width_out!=1 && "uncanonicalized urem");
     
     if (ConstantExpr *CE = dyn_cast<ConstantExpr>(de->right)) {
-      uint64_t divisor = CE->getConstantValue();
+      if (CE->getWidth() <= 64) {
+        uint64_t divisor = CE->getConstantValue();
+
+        if (bits64::isPowerOfTwo(divisor)) {
+          unsigned bits = bits64::indexOfSingleBit(divisor);
+
+          // special case for modding by 1 or else we bvExtract -1:0
+          if (bits == 0) {
+            return bvZero(*width_out);
+          } else {
+            return vc_bvConcatExpr(vc,
+                                   bvZero(*width_out - bits),
+                                   bvExtract(left, bits - 1, 0));
+          }
+        }
 
-      if (bits64::isPowerOfTwo(divisor)) {
-        unsigned bits = bits64::indexOfSingleBit(divisor);
+      // Use fast division to compute modulo without explicit division for
+      // constant divisor.
 
-        // special case for modding by 1 or else we bvExtract -1:0
-        if (bits == 0) {
-          return bvZero(*width_out);
-        } else {
-          return vc_bvConcatExpr(vc,
-                                 bvZero(*width_out - bits),
-                                 bvExtract(left, bits - 1, 0));
+        if (optimizeDivides) {
+          if (*width_out == 32) { //only works for 32-bit division
+            ExprHandle quotient = constructUDivByConstant( left, *width_out, (uint32_t)divisor );
+            ExprHandle quot_times_divisor = constructMulByConstant( quotient, *width_out, divisor );
+            ExprHandle rem = vc_bvMinusExpr( vc, *width_out, left, quot_times_divisor );
+            return rem;
+          }
         }
       }
-
-      //use fast division to compute modulo without explicit division for constant divisor
-      if (optimizeDivides) {
-	if (*width_out == 32) { //only works for 32-bit division
-	  ExprHandle quotient = constructUDivByConstant( left, *width_out, (uint32_t)divisor );
-	  ExprHandle quot_times_divisor = constructMulByConstant( quotient, *width_out, divisor );
-          ExprHandle rem = vc_bvMinusExpr( vc, *width_out, left, quot_times_divisor );
-	  return rem;
-	}
-      }
     }
     
     ExprHandle right = construct(de->right, width_out);
@@ -726,7 +731,7 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
     assert(*width_out!=1 && "uncanonicalized shl");
 
     if (ConstantExpr *CE = dyn_cast<ConstantExpr>(se->right)) {
-      return bvLeftShift(left, CE->getConstantValue(), 
+      return bvLeftShift(left, (unsigned) CE->getLimitedValue(), 
                          getShiftBits(*width_out));
     } else {
       int shiftWidth;
@@ -742,7 +747,7 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
     assert(*width_out!=1 && "uncanonicalized lshr");
 
     if (ConstantExpr *CE = dyn_cast<ConstantExpr>(lse->right)) {
-      return bvRightShift(left, (unsigned) CE->getConstantValue(), 
+      return bvRightShift(left, (unsigned) CE->getLimitedValue(), 
                           shiftBits);
     } else {
       int shiftWidth;
@@ -757,7 +762,7 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
     assert(*width_out!=1 && "uncanonicalized ashr");
     
     if (ConstantExpr *CE = dyn_cast<ConstantExpr>(ase->right)) {
-      unsigned shift = (unsigned) CE->getConstantValue();
+      unsigned shift = (unsigned) CE->getLimitedValue();
       ExprHandle signedBool = bvBoolExtract(left, *width_out-1);
       return constructAShrByConstant(left, shift, signedBool, 
                                      getShiftBits(*width_out));
diff --git a/lib/Solver/Solver.cpp b/lib/Solver/Solver.cpp
index 9e8e37bf..f8f9d690 100644
--- a/lib/Solver/Solver.cpp
+++ b/lib/Solver/Solver.cpp
@@ -158,7 +158,7 @@ std::pair< ref<Expr>, ref<Expr> > Solver::getRange(const Query& query) {
       min = 0, max = 1; break;
     }
   } else if (ConstantExpr *CE = dyn_cast<ConstantExpr>(e)) {
-    min = max = CE->getConstantValue();
+    min = max = CE->getZExtValue();
   } else {
     // binary search for # of useful bits
     uint64_t lo=0, hi=width, mid, bits=0;
generated by cgit-pink 1.4.1 (git 2.36.1) at 2024-12-04 17:55:13 +0000