about summary refs log tree commit diff homepage
path: root/lib/Core
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/Core
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/Core')
-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
5 files changed, 52 insertions, 48 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;