about summary refs log tree commit diff homepage
path: root/lib
diff options
context:
space:
mode:
authorDaniel Dunbar <daniel@zuster.org>2009-06-04 08:59:53 +0000
committerDaniel Dunbar <daniel@zuster.org>2009-06-04 08:59:53 +0000
commit92004d6524c7633aa1e014e5b727a39475652dda (patch)
treee68a45e3aa57b34a33f5f1dfbb496acb8bcebc9a /lib
parent21fb3bd80309b30ed2223e793003ac4744776dfb (diff)
downloadklee-92004d6524c7633aa1e014e5b727a39475652dda.tar.gz
Sink getConstantValue into ConstantExpr.
 - Propogate ConstantExpr to various places, or cast as appropriate.


git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72862 91177308-0d34-0410-b5e6-96231b3b80d8
Diffstat (limited to 'lib')
-rw-r--r--lib/Core/Executor.cpp74
-rw-r--r--lib/Core/Executor.h3
-rw-r--r--lib/Core/ImpliedValue.cpp10
-rw-r--r--lib/Core/ImpliedValue.h3
-rw-r--r--lib/Core/SpecialFunctionHandler.cpp10
-rw-r--r--lib/Expr/Constraints.cpp3
-rw-r--r--lib/Expr/Expr.cpp38
-rw-r--r--lib/Solver/CexCachingSolver.cpp2
-rw-r--r--lib/Solver/FastCexSolver.cpp7
-rw-r--r--lib/Solver/STPBuilder.cpp2
10 files changed, 78 insertions, 74 deletions
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index aa8681dc..21356af9 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -1015,31 +1015,31 @@ ref<Expr> Executor::toUnique(const ExecutionState &state,
 
 /* Concretize the given expression, and return a possible constant value. 
    'reason' is just a documentation string stating the reason for concretization. */
-ref<Expr> Executor::toConstant(ExecutionState &state, 
-                               ref<Expr> e,
-                               const char *reason) {
+ref<klee::ConstantExpr> 
+Executor::toConstant(ExecutionState &state, 
+                     ref<Expr> e,
+                     const char *reason) {
   e = state.constraints.simplifyExpr(e);
-  if (!isa<ConstantExpr>(e)) {
-    ref<ConstantExpr> value;
-    bool success = solver->getValue(state, e, value);
-    assert(success && "FIXME: Unhandled solver failure");
+  if (ConstantExpr *CE = dyn_cast<ConstantExpr>(e))
+    return CE;
+
+  ref<ConstantExpr> value;
+  bool success = solver->getValue(state, e, value);
+  assert(success && "FIXME: Unhandled solver failure");
     
-    std::ostringstream os;
-    os << "silently concretizing (reason: " << reason << ") expression " << e 
-       << " to value " << value 
-       << " (" << (*(state.pc)).info->file << ":" << (*(state.pc)).info->line << ")";
+  std::ostringstream os;
+  os << "silently concretizing (reason: " << reason << ") expression " << e 
+     << " to value " << value 
+     << " (" << (*(state.pc)).info->file << ":" << (*(state.pc)).info->line << ")";
       
-    if (AllExternalWarnings)
-      klee_warning(reason, os.str().c_str());
-    else
-      klee_warning_once(reason, "%s", os.str().c_str());
+  if (AllExternalWarnings)
+    klee_warning(reason, os.str().c_str());
+  else
+    klee_warning_once(reason, "%s", os.str().c_str());
 
-    addConstraint(state, EqExpr::create(e, value));
+  addConstraint(state, EqExpr::create(e, value));
     
-    return value;
-  } else {
-    return e;
-  }
+  return value;
 }
 
 void Executor::executeGetValue(ExecutionState &state,
@@ -1909,8 +1909,8 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
   case Instruction::FPTrunc: {
     FPTruncInst *fi = cast<FPTruncInst>(i);
     Expr::Width resultType = Expr::getWidthForLLVMType(fi->getType());
-    ref<Expr> arg = toConstant(state, eval(ki, 0, state).value,
-                               "floating point");
+    ref<ConstantExpr> arg = toConstant(state, eval(ki, 0, state).value,
+                                       "floating point");
     uint64_t value = floats::trunc(arg->getConstantValue(),
                                    resultType,
                                    arg->getWidth());
@@ -1921,8 +1921,8 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
   case Instruction::FPExt: {
     FPExtInst *fi = cast<FPExtInst>(i);
     Expr::Width resultType = Expr::getWidthForLLVMType(fi->getType());
-    ref<Expr> arg = toConstant(state, eval(ki, 0, state).value,
-                               "floating point");
+    ref<ConstantExpr> arg = toConstant(state, eval(ki, 0, state).value,
+                                       "floating point");
     uint64_t value = floats::ext(arg->getConstantValue(),
                                  resultType,
                                  arg->getWidth());
@@ -1933,8 +1933,8 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
   case Instruction::FPToUI: {
     FPToUIInst *fi = cast<FPToUIInst>(i);
     Expr::Width resultType = Expr::getWidthForLLVMType(fi->getType());
-    ref<Expr> arg = toConstant(state, eval(ki, 0, state).value,
-                               "floating point");
+    ref<ConstantExpr> arg = toConstant(state, eval(ki, 0, state).value,
+                                       "floating point");
     uint64_t value = floats::toUnsignedInt(arg->getConstantValue(),
                                            resultType,
                                            arg->getWidth());
@@ -1945,8 +1945,8 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
   case Instruction::FPToSI: {
     FPToSIInst *fi = cast<FPToSIInst>(i);
     Expr::Width resultType = Expr::getWidthForLLVMType(fi->getType());
-    ref<Expr> arg = toConstant(state, eval(ki, 0, state).value,
-                               "floating point");
+    ref<ConstantExpr> arg = toConstant(state, eval(ki, 0, state).value,
+                                       "floating point");
     uint64_t value = floats::toSignedInt(arg->getConstantValue(),
                                          resultType,
                                          arg->getWidth());
@@ -1957,8 +1957,8 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
   case Instruction::UIToFP: {
     UIToFPInst *fi = cast<UIToFPInst>(i);
     Expr::Width resultType = Expr::getWidthForLLVMType(fi->getType());
-    ref<Expr> arg = toConstant(state, eval(ki, 0, state).value,
-                               "floating point");
+    ref<ConstantExpr> arg = toConstant(state, eval(ki, 0, state).value,
+                                       "floating point");
     uint64_t value = floats::UnsignedIntToFP(arg->getConstantValue(),
                                              resultType);
     bindLocal(ki, state, ConstantExpr::alloc(value, resultType));
@@ -1968,8 +1968,8 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
   case Instruction::SIToFP: {
     SIToFPInst *fi = cast<SIToFPInst>(i);
     Expr::Width resultType = Expr::getWidthForLLVMType(fi->getType());
-    ref<Expr> arg = toConstant(state, eval(ki, 0, state).value,
-                               "floating point");
+    ref<ConstantExpr> arg = toConstant(state, eval(ki, 0, state).value,
+                                       "floating point");
     uint64_t value = floats::SignedIntToFP(arg->getConstantValue(),
                                            resultType,
                                            arg->getWidth());
@@ -1980,10 +1980,10 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
   case Instruction::FCmp: {
     FCmpInst *fi = cast<FCmpInst>(i);
     Expr::Width resultType = Expr::getWidthForLLVMType(fi->getType());
-    ref<Expr> left  = toConstant(state, eval(ki, 0, state).value, 
-                                 "floating point");
-    ref<Expr> right = toConstant(state, eval(ki, 1, state).value,
-                                 "floating point");
+    ref<ConstantExpr> left  = toConstant(state, eval(ki, 0, state).value, 
+                                         "floating point");
+    ref<ConstantExpr> right = toConstant(state, eval(ki, 1, state).value,
+                                         "floating point");
     uint64_t leftVal = left->getConstantValue();
     uint64_t rightVal = right->getConstantValue();
  
@@ -2804,7 +2804,7 @@ void Executor::executeMemoryOperation(ExecutionState &state,
   solver->setTimeout(stpTimeout);
   if (!state.addressSpace.resolveOne(state, solver, address, op, success)) {
     address = toConstant(state, address, "resolveOne failure");
-    success = state.addressSpace.resolveOne(address->getConstantValue(), op);
+    success = state.addressSpace.resolveOne(cast<ConstantExpr>(address)->getConstantValue(), op);
   }
   solver->setTimeout(0);
 
diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h
index ba65cf5a..013d3bb8 100644
--- a/lib/Core/Executor.h
+++ b/lib/Core/Executor.h
@@ -319,7 +319,8 @@ private:
   /// should generally be avoided.
   ///
   /// \param purpose An identify string to printed in case of concretization.
-  ref<Expr> toConstant(ExecutionState &state, ref<Expr> e, const char *purpose);
+  ref<klee::ConstantExpr> toConstant(ExecutionState &state, ref<Expr> e, 
+                                     const char *purpose);
 
   /// Bind a constant value for e to the given target. NOTE: This
   /// function may fork state if the state has multiple seeds.
diff --git a/lib/Core/ImpliedValue.cpp b/lib/Core/ImpliedValue.cpp
index 6ad0f5d2..e1daca2f 100644
--- a/lib/Core/ImpliedValue.cpp
+++ b/lib/Core/ImpliedValue.cpp
@@ -30,7 +30,8 @@ static void _getImpliedValue(ref<Expr> e,
                              ImpliedValueList &results) {
   switch (e->getKind()) {
   case Expr::Constant: {
-    assert(value == e->getConstantValue() && "error in implied value calculation");
+    assert(value == cast<ConstantExpr>(e)->getConstantValue() && 
+           "error in implied value calculation");
     break;
   }
 
@@ -203,14 +204,15 @@ void ImpliedValue::getImpliedValues(ref<Expr> e,
 void ImpliedValue::checkForImpliedValues(Solver *S, ref<Expr> e, 
                                          ref<ConstantExpr> value) {
   std::vector<ref<ReadExpr> > reads;
-  std::map<ref<ReadExpr>, ref<Expr> > found;
+  std::map<ref<ReadExpr>, ref<ConstantExpr> > found;
   ImpliedValueList results;
 
   getImpliedValues(e, value, results);
 
   for (ImpliedValueList::iterator i = results.begin(), ie = results.end();
        i != ie; ++i) {
-    std::map<ref<ReadExpr>, ref<Expr> >::iterator it = found.find(i->first);
+    std::map<ref<ReadExpr>, ref<ConstantExpr> >::iterator it = 
+      found.find(i->first);
     if (it != found.end()) {
       assert(it->second->getConstantValue() == i->second->getConstantValue() &&
              "I don't think so Scott");
@@ -247,7 +249,7 @@ void ImpliedValue::checkForImpliedValues(Solver *S, ref<Expr> e,
     ref<ConstantExpr> possible;
     bool success = S->getValue(Query(assume, var), possible);
     assert(success && "FIXME: Unhandled solver failure");    
-    std::map<ref<ReadExpr>, ref<Expr> >::iterator it = found.find(var);
+    std::map<ref<ReadExpr>, ref<ConstantExpr> >::iterator it = found.find(var);
     bool res;
     success = S->mustBeTrue(Query(assume, EqExpr::create(var, possible)), res);
     assert(success && "FIXME: Unhandled solver failure");    
diff --git a/lib/Core/ImpliedValue.h b/lib/Core/ImpliedValue.h
index cbc55dc5..6bdb6c66 100644
--- a/lib/Core/ImpliedValue.h
+++ b/lib/Core/ImpliedValue.h
@@ -26,7 +26,8 @@ namespace klee {
   class ReadExpr;
   class Solver;
 
-  typedef std::vector< std::pair<ref<ReadExpr>, ref<Expr> > > ImpliedValueList;
+  typedef std::vector< std::pair<ref<ReadExpr>, 
+                                 ref<ConstantExpr> > > ImpliedValueList;
   
   namespace ImpliedValue {        
     void getImpliedValues(ref<Expr> e, ref<ConstantExpr> cvalue, 
diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp
index ea2594eb..2ee73457 100644
--- a/lib/Core/SpecialFunctionHandler.cpp
+++ b/lib/Core/SpecialFunctionHandler.cpp
@@ -419,7 +419,7 @@ void SpecialFunctionHandler::handleUnderConstrained(ExecutionState &state,
   assert(isa<ConstantExpr>(arguments[0]) &&
    	 "symbolic argument given to klee_under_constrained!");
 
-  unsigned v = arguments[0]->getConstantValue();
+  unsigned v = cast<ConstantExpr>(arguments[0])->getConstantValue();
   llvm::cerr << "argument = " << v << " under=" << state.underConstrained << "\n";
   if(v) {
     assert(state.underConstrained == false &&
@@ -599,14 +599,14 @@ void SpecialFunctionHandler::handleCheckMemoryAccess(ExecutionState &state,
   } else {
     ObjectPair op;
 
-    if (!state.addressSpace.resolveOne(address->getConstantValue(), op)) {
+    if (!state.addressSpace.resolveOne(cast<ConstantExpr>(address)->getConstantValue(), op)) {
       executor.terminateStateOnError(state,
                                      "check_memory_access: memory error",
                                      "ptr.err",
                                      executor.getAddressInfo(state, address));
     } else {
       ref<Expr> chk = op.first->getBoundsCheckPointer(address, 
-                                                      size->getConstantValue());
+                                                      cast<ConstantExpr>(size)->getConstantValue());
       if (!cast<ConstantExpr>(chk)->getConstantValue()) {
         executor.terminateStateOnError(state,
                                        "check_memory_access: memory error",
@@ -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 = arguments[0]->getConstantValue();
-  uint64_t size = arguments[1]->getConstantValue();
+  uint64_t address = cast<ConstantExpr>(arguments[0])->getConstantValue();
+  uint64_t size = cast<ConstantExpr>(arguments[1])->getConstantValue();
   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/Constraints.cpp b/lib/Expr/Constraints.cpp
index 5869a852..8f89f88a 100644
--- a/lib/Expr/Constraints.cpp
+++ b/lib/Expr/Constraints.cpp
@@ -122,7 +122,8 @@ void ConstraintManager::addConstraintInternal(ref<Expr> e) {
 
   switch (e->getKind()) {
   case Expr::Constant:
-    assert(e->getConstantValue() && "attempt to add invalid (false) constraint");
+    assert(cast<ConstantExpr>(e)->getConstantValue() && 
+           "attempt to add invalid (false) constraint");
     break;
     
     // split to enable finer grained independence and other optimizations
diff --git a/lib/Expr/Expr.cpp b/lib/Expr/Expr.cpp
index f95369f4..c645f37c 100644
--- a/lib/Expr/Expr.cpp
+++ b/lib/Expr/Expr.cpp
@@ -189,11 +189,6 @@ unsigned ReadExpr::computeHash() {
   return hashValue;
 }
 
-uint64_t Expr::getConstantValue() const {
-  assert(getKind() == Constant);
-  return static_cast<const ConstantExpr*>(this)->asUInt64;
-}
-
 ref<Expr> Expr::createFromKind(Kind k, std::vector<CreateArg> args) {
   unsigned numArgs = args.size();
   
@@ -428,22 +423,26 @@ ref<Expr> SelectExpr::create(ref<Expr> c, ref<Expr> t, ref<Expr> f) {
 ref<Expr> ConcatExpr::create(const ref<Expr> &l, const ref<Expr> &r) {
   Expr::Width w = l->getWidth() + r->getWidth();
   
-  /* Constant folding */
-  if (l->getKind() == Expr::Constant && r->getKind() == Expr::Constant) {
-    // XXX: should fix this constant limitation soon
-    assert(w <= 64 && "ConcatExpr::create(): don't support concats describing constants greater than 64 bits yet");
-    
-    uint64_t res = (l->getConstantValue() << r->getWidth()) + r->getConstantValue();
-    return ConstantExpr::create(res, w);
+  // Fold concatenation of constants.
+  //
+  // FIXME: concat 0 x -> zext x ?
+  if (ConstantExpr *lCE = dyn_cast<ConstantExpr>(l)) {
+    if (ConstantExpr *rCE = dyn_cast<ConstantExpr>(r)) {
+      assert(w <= 64 && "ConcatExpr::create(): don't support concats describing constants greater than 64 bits yet");
+      
+      uint64_t res = (lCE->getConstantValue() << rCE->getWidth()) + 
+        rCE->getConstantValue();
+      return ConstantExpr::create(res, w);
+    }
   }
 
   // Merge contiguous Extracts
-  if (l->getKind() == Expr::Extract && r->getKind() == Expr::Extract) {
-    const ExtractExpr* ee_left = cast<ExtractExpr>(l);
-    const ExtractExpr* ee_right = cast<ExtractExpr>(r);
-    if (ee_left->expr == ee_right->expr &&
-	ee_right->offset + ee_right->width == ee_left->offset) {
-      return ExtractExpr::create(ee_left->expr, ee_right->offset, w);
+  if (ExtractExpr *ee_left = dyn_cast<ExtractExpr>(l)) {
+    if (ExtractExpr *ee_right = dyn_cast<ExtractExpr>(r)) {
+      if (ee_left->expr == ee_right->expr &&
+          ee_right->offset + ee_right->width == ee_left->offset) {
+        return ExtractExpr::create(ee_left->expr, ee_right->offset, w);
+      }
     }
   }
 
@@ -949,7 +948,8 @@ static ref<Expr> TryConstArrayOpt(const ref<ConstantExpr> &cl,
       return res;
     
     for (const UpdateNode *un = rd->updates.head; un; un = un->next) {
-      if (un->index != first_idx_match && un->value->getConstantValue() == ct) {
+      if (un->index != first_idx_match && 
+          cast<ConstantExpr>(un->value)->getConstantValue() == ct) {
 	ref<Expr> curr_eq = EqExpr::create(un->index, rd->index);
 	res = OrExpr::create(curr_eq, res);
       }
diff --git a/lib/Solver/CexCachingSolver.cpp b/lib/Solver/CexCachingSolver.cpp
index 1eaec4d9..9c233530 100644
--- a/lib/Solver/CexCachingSolver.cpp
+++ b/lib/Solver/CexCachingSolver.cpp
@@ -220,7 +220,7 @@ bool CexCachingSolver::computeValidity(const Query& query,
   assert(isa<ConstantExpr>(q) && 
          "assignment evaluation did not result in constant");
 
-  if (q->getConstantValue()) {
+  if (cast<ConstantExpr>(q)->getConstantValue()) {
     if (!getAssignment(query, a))
       return false;
     result = !a ? Solver::True : Solver::Unknown;
diff --git a/lib/Solver/FastCexSolver.cpp b/lib/Solver/FastCexSolver.cpp
index 1a1cfe62..6d9c8551 100644
--- a/lib/Solver/FastCexSolver.cpp
+++ b/lib/Solver/FastCexSolver.cpp
@@ -730,10 +730,9 @@ public:
   bool exprMustBeValue(ref<Expr> e, uint64_t value) {
     CexConstifier cc(objectValues);
     ref<Expr> v = cc.visit(e);
-    if (!isa<ConstantExpr>(v)) return false;
-    // XXX reenable once all reads and vars are fixed
-    //    assert(v.isConstant() && "not all values have been fixed");
-    return v->getConstantValue() == value;
+    if (ConstantExpr *CE = dyn_cast<ConstantExpr>(v))
+      return CE->getConstantValue() == value;
+    return false;
   }
 };
 
diff --git a/lib/Solver/STPBuilder.cpp b/lib/Solver/STPBuilder.cpp
index 88bdd2b0..5b3fdd60 100644
--- a/lib/Solver/STPBuilder.cpp
+++ b/lib/Solver/STPBuilder.cpp
@@ -449,7 +449,7 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
 
   switch (e->getKind()) {
   case Expr::Constant: {
-    uint64_t asUInt64 = e->getConstantValue();
+    uint64_t asUInt64 = cast<ConstantExpr>(e)->getConstantValue();
     *width_out = e->getWidth();
 
     if (*width_out > 64)