Change Solver::getValue to make explicit that result is a ConstantExpr.

git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72860 91177308-0d34-0410-b5e6-96231b3b80d8

8 files changed, 37 insertions, 29 deletions

diff --git a/lib/Core/AddressSpace.cpp b/lib/Core/AddressSpace.cpp
index a4a65bd9..5b73a6f6 100644
--- a/lib/Core/AddressSpace.cpp
+++ b/lib/Core/AddressSpace.cpp
@@ -80,7 +80,7 @@ bool AddressSpace::resolveOne(ExecutionState &state,
 
     // try cheap search, will succeed for any inbounds pointer
 
-    ref<Expr> cex(0);
+    ref<ConstantExpr> cex;
     if (!solver->getValue(state, address, cex))
       return false;
     unsigned example = (unsigned) cex->getConstantValue();
@@ -187,7 +187,7 @@ bool AddressSpace::resolve(ExecutionState &state,
     // to hit the fast path with exactly 2 queries). we could also
     // just get this by inspection of the expr.
     
-    ref<Expr> cex(0);
+    ref<ConstantExpr> cex;
     if (!solver->getValue(state, p, cex))
       return true;
     unsigned example = (unsigned) cex->getConstantValue();
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index f567efc6..aa8681dc 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -623,7 +623,7 @@ void Executor::branch(ExecutionState &state,
            siie = seeds.end(); siit != siie; ++siit) {
       unsigned i;
       for (i=0; i<N; ++i) {
-        ref<Expr> res;
+        ref<ConstantExpr> res;
         bool success = 
           solver->getValue(state, siit->assignment.evaluate(conditions[i]), 
                            res);
@@ -680,7 +680,7 @@ Executor::fork(ExecutionState &current, ref<Expr> condition, bool isInternal) {
         (MaxStaticCPForkPct<1. &&
          cpn && (cpn->statistics.getValue(stats::solverTime) > 
                  stats::solverTime*MaxStaticCPSolvePct))) {
-      ref<Expr> value; 
+      ref<ConstantExpr> value; 
       bool success = solver->getValue(current, condition, value);
       assert(success && "FIXME: Unhandled solver failure");
       addConstraint(current, EqExpr::create(value, condition));
@@ -748,7 +748,7 @@ Executor::fork(ExecutionState &current, ref<Expr> condition, bool isInternal) {
     // Is seed extension still ok here?
     for (std::vector<SeedInfo>::iterator siit = it->second.begin(), 
            siie = it->second.end(); siit != siie; ++siit) {
-      ref<Expr> res;
+      ref<ConstantExpr> res;
       bool success = 
         solver->getValue(current, siit->assignment.evaluate(condition), res);
       assert(success && "FIXME: Unhandled solver failure");
@@ -813,7 +813,7 @@ Executor::fork(ExecutionState &current, ref<Expr> condition, bool isInternal) {
       std::vector<SeedInfo> &falseSeeds = seedMap[falseState];
       for (std::vector<SeedInfo>::iterator siit = seeds.begin(), 
              siie = seeds.end(); siit != siie; ++siit) {
-        ref<Expr> res;
+        ref<ConstantExpr> res;
         bool success = 
           solver->getValue(current, siit->assignment.evaluate(condition), res);
         assert(success && "FIXME: Unhandled solver failure");
@@ -998,7 +998,7 @@ ref<Expr> Executor::toUnique(const ExecutionState &state,
   ref<Expr> result = e;
 
   if (!isa<ConstantExpr>(e)) {
-    ref<Expr> value(0);
+    ref<ConstantExpr> value;
     bool isTrue = false;
 
     solver->setTimeout(stpTimeout);      
@@ -1020,7 +1020,7 @@ ref<Expr> Executor::toConstant(ExecutionState &state,
                                const char *reason) {
   e = state.constraints.simplifyExpr(e);
   if (!isa<ConstantExpr>(e)) {
-    ref<Expr> value;
+    ref<ConstantExpr> value;
     bool success = solver->getValue(state, e, value);
     assert(success && "FIXME: Unhandled solver failure");
     
@@ -1049,7 +1049,7 @@ void Executor::executeGetValue(ExecutionState &state,
   std::map< ExecutionState*, std::vector<SeedInfo> >::iterator it = 
     seedMap.find(&state);
   if (it==seedMap.end() || isa<ConstantExpr>(e)) {
-    ref<Expr> value;
+    ref<ConstantExpr> value;
     bool success = solver->getValue(state, e, value);
     assert(success && "FIXME: Unhandled solver failure");
     bindLocal(target, state, value);
@@ -1057,7 +1057,7 @@ void Executor::executeGetValue(ExecutionState &state,
     std::set< ref<Expr> > values;
     for (std::vector<SeedInfo>::iterator siit = it->second.begin(), 
            siie = it->second.end(); siit != siie; ++siit) {
-      ref<Expr> value;
+      ref<ConstantExpr> value;
       bool success = 
         solver->getValue(state, siit->assignment.evaluate(e), value);
       assert(success && "FIXME: Unhandled solver failure");
@@ -1529,7 +1529,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
          have already got a value. But in the end the caches should
          handle it for us, albeit with some overhead. */
       do {
-        ref<Expr> value;
+        ref<ConstantExpr> value;
         bool success = solver->getValue(*free, v, value);
         assert(success && "FIXME: Unhandled solver failure");
         StatePair res = fork(*free, EqExpr::create(v, value), true);
@@ -2347,7 +2347,7 @@ std::string Executor::getAddressInfo(ExecutionState &state,
   if (ConstantExpr *CE = dyn_cast<ConstantExpr>(address)) {
     example = CE->getConstantValue();
   } else {
-    ref<Expr> value;
+    ref<ConstantExpr> value;
     bool success = solver->getValue(state, address, value);
     assert(success && "FIXME: Unhandled solver failure");
     example = value->getConstantValue();
@@ -2513,7 +2513,7 @@ void Executor::callExternalFunction(ExecutionState &state,
   for (std::vector<ref<Expr> >::iterator ai = arguments.begin(), ae = arguments.end();
        ai!=ae; ++ai, ++i) {
     if (AllowExternalSymCalls) { // don't bother checking uniqueness
-      ref<Expr> ce;
+      ref<ConstantExpr> ce;
       bool success = solver->getValue(state, *ai, ce);
       assert(success && "FIXME: Unhandled solver failure");
       static_cast<ConstantExpr*>(ce.get())->toMemory((void*) &args[i]);
@@ -2652,14 +2652,15 @@ void Executor::executeAlloc(ExecutionState &state,
     // return argument first). This shows up in pcre when llvm
     // collapses the size expression with a select.
 
-    ref<Expr> example;
+    ref<ConstantExpr> example;
     bool success = solver->getValue(state, size, example);
     assert(success && "FIXME: Unhandled solver failure");
     
     // Try and start with a small example
     while (example->getConstantValue() > 128) {
-      ref<Expr> tmp = ConstantExpr::alloc(example->getConstantValue() >> 1, 
-                                          example->getWidth());
+      ref<ConstantExpr> tmp = 
+        ConstantExpr::alloc(example->getConstantValue() >> 1, 
+                            example->getWidth());
       bool res;
       bool success = solver->mayBeTrue(state, EqExpr::create(tmp, size), res);
       assert(success && "FIXME: Unhandled solver failure");      
@@ -2672,7 +2673,7 @@ void Executor::executeAlloc(ExecutionState &state,
     
     if (fixedSize.second) { 
       // Check for exactly two values
-      ref<Expr> tmp;
+      ref<ConstantExpr> tmp;
       bool success = solver->getValue(*fixedSize.second, size, tmp);
       assert(success && "FIXME: Unhandled solver failure");      
       bool res;
diff --git a/lib/Core/ImpliedValue.cpp b/lib/Core/ImpliedValue.cpp
index b8d44eea..6ad0f5d2 100644
--- a/lib/Core/ImpliedValue.cpp
+++ b/lib/Core/ImpliedValue.cpp
@@ -244,7 +244,7 @@ void ImpliedValue::checkForImpliedValues(Solver *S, ref<Expr> e,
   for (std::vector< ref<ReadExpr> >::iterator i = reads.begin(), 
          ie = reads.end(); i != ie; ++i) {
     ref<ReadExpr> var = *i;
-    ref<Expr> possible;
+    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);
diff --git a/lib/Core/SeedInfo.cpp b/lib/Core/SeedInfo.cpp
index 62b71e87..f328823b 100644
--- a/lib/Core/SeedInfo.cpp
+++ b/lib/Core/SeedInfo.cpp
@@ -98,7 +98,7 @@ void SeedInfo::patchSeed(const ExecutionState &state,
       bool success = solver->mustBeFalse(tmp, isSeed, res);
       assert(success && "FIXME: Unhandled solver failure");
       if (res) {
-        ref<Expr> value;
+        ref<ConstantExpr> value;
         bool success = solver->getValue(tmp, read, value);
         assert(success && "FIXME: Unhandled solver failure");            
         it2->second[i] = value->getConstantValue();
@@ -128,7 +128,7 @@ void SeedInfo::patchSeed(const ExecutionState &state,
       bool success = solver->mustBeFalse(tmp, isSeed, res);
       assert(success && "FIXME: Unhandled solver failure");
       if (res) {
-        ref<Expr> value;
+        ref<ConstantExpr> value;
         bool success = solver->getValue(tmp, read, value);
         assert(success && "FIXME: Unhandled solver failure");            
         it->second[i] = value->getConstantValue();
diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp
index 0ec9a5ac..ea2594eb 100644
--- a/lib/Core/SpecialFunctionHandler.cpp
+++ b/lib/Core/SpecialFunctionHandler.cpp
@@ -480,7 +480,7 @@ void SpecialFunctionHandler::handlePrintRange(ExecutionState &state,
   llvm::cerr << msg_str << ":" << arguments[1];
   if (!isa<ConstantExpr>(arguments[1])) {
     // FIXME: Pull into a unique value method?
-    ref<Expr> value;
+    ref<ConstantExpr> value;
     bool success = executor.solver->getValue(state, arguments[1], value);
     assert(success && "FIXME: Unhandled solver failure");
     bool res;
diff --git a/lib/Core/TimingSolver.cpp b/lib/Core/TimingSolver.cpp
index b26551cc..339c33b2 100644
--- a/lib/Core/TimingSolver.cpp
+++ b/lib/Core/TimingSolver.cpp
@@ -94,10 +94,10 @@ bool TimingSolver::mayBeFalse(const ExecutionState& state, ref<Expr> expr,
 }
 
 bool TimingSolver::getValue(const ExecutionState& state, ref<Expr> expr, 
-                            ref<Expr> &result) {
+                            ref<ConstantExpr> &result) {
   // Fast path, to avoid timer and OS overhead.
-  if (isa<ConstantExpr>(expr)) {
-    result = expr;
+  if (ConstantExpr *CE = dyn_cast<ConstantExpr>(expr)) {
+    result = CE;
     return true;
   }
   
diff --git a/lib/Core/TimingSolver.h b/lib/Core/TimingSolver.h
index 1287c2f3..b13879df 100644
--- a/lib/Core/TimingSolver.h
+++ b/lib/Core/TimingSolver.h
@@ -55,7 +55,8 @@ namespace klee {
 
     bool mayBeFalse(const ExecutionState&, ref<Expr>, bool &result);
 
-    bool getValue(const ExecutionState &, ref<Expr> expr, ref<Expr> &result);
+    bool getValue(const ExecutionState &, ref<Expr> expr, 
+                  ref<ConstantExpr> &result);
 
     bool getInitialValues(const ExecutionState&, 
                           const std::vector<const Array*> &objects,
diff --git a/lib/Solver/Solver.cpp b/lib/Solver/Solver.cpp
index 3db049cd..a673e9e7 100644
--- a/lib/Solver/Solver.cpp
+++ b/lib/Solver/Solver.cpp
@@ -110,14 +110,20 @@ bool Solver::mayBeFalse(const Query& query, bool &result) {
   return true;
 }
 
-bool Solver::getValue(const Query& query, ref<Expr> &result) {
+bool Solver::getValue(const Query& query, ref<ConstantExpr> &result) {
   // Maintain invariants implementation expect.
-  if (isa<ConstantExpr>(query.expr)) {
-    result = query.expr;
+  if (ConstantExpr *CE = dyn_cast<ConstantExpr>(query.expr)) {
+    result = CE;
     return true;
   }
 
-  return impl->computeValue(query, result);
+  // FIXME: Push ConstantExpr requirement down.
+  ref<Expr> tmp;
+  if (!impl->computeValue(query, tmp))
+    return false;
+  
+  result = cast<ConstantExpr>(tmp);
+  return true;
 }
 
 bool