Feature: implement single memory object resolution for symbolic addresses.

This feature implements tracking of and resolution of memory objects in the presence of
symbolic addresses.
For example, an expression like the following:
int x;
klee_make_symbolic(&x, sizeof(x), "x");

int* tmp = &b.y[x].z;

For a concrete array object "y", which is a member of struct "b", a symbolic offset "x" would normally be resolved to any matching
memory object - including the ones outside of the object "b".
This behaviour is consistent with symbex approach of exploring all execution paths.
However, from the point of view of security testing, we would only be interested to know if we are still
in-bounds or there is a buffer overflow.

The implemented feature creates and tracks (via the GEP instruction) the mapping between the current
symbolic offset and the base object it refers to: in our example we are able to tell that the reference
should happen within the object "b" (as the array "y" is inside the same memory blob). As a result, we are able to minimize
the symbolic exploration to only two paths: one within the bounds of "b", the other with a buffer overflow bug.

The feature is turned on via the single-object-resolution command line flag.

A new test case was implemented to illustrate how the feature works.

2 files changed, 133 insertions, 51 deletions

diff --git a/lib/Core/ExecutionState.h b/lib/Core/ExecutionState.h
index 20187166..833537f2 100644
--- a/lib/Core/ExecutionState.h
+++ b/lib/Core/ExecutionState.h
@@ -248,6 +248,10 @@ public:
   /// @brief Disables forking for this state. Set by user code
   bool forkDisabled = false;
 
+  /// @brief Mapping symbolic address expressions to concrete base addresses
+  typedef std::map<ref<Expr>, ref<ConstantExpr>> base_addrs_t;
+  base_addrs_t base_addrs;
+
 public:
 #ifdef KLEE_UNITTEST
   // provide this function only in the context of unittests
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index cf6ce777..b96ea843 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -466,6 +466,12 @@ cl::opt<bool> DebugCheckForImpliedValues(
     cl::desc("Debug the implied value optimization"),
     cl::cat(DebugCat));
 
+/*** Misc options ***/
+cl::opt<bool> SingleObjectResolution(
+    "single-object-resolution",
+    cl::desc("Try to resolve memory reads/writes to single objects "
+             "when offsets are symbolic (default=false)"),
+    cl::init(false), cl::cat(MiscCat));
 } // namespace
 
 // XXX hack
@@ -2784,6 +2790,26 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
     KGEPInstruction *kgepi = static_cast<KGEPInstruction*>(ki);
     ref<Expr> base = eval(ki, 0, state).value;
 
+    bool const_base = isa<ConstantExpr>(base);
+    bool update = false;
+    ref<ConstantExpr> original_base = 0;
+    ref<Expr> key = 0;
+    ref<ConstantExpr> value = 0;
+
+    if (SingleObjectResolution) {
+      ExecutionState::base_addrs_t::iterator base_it;
+      if (!const_base) {
+        base_it = state.base_addrs.find(base);
+        if (base_it != state.base_addrs.end()) {
+          update = true;
+          key = base_it->first;
+          value = base_it->second;
+        }
+      } else {
+        original_base = dyn_cast<ConstantExpr>(base);
+      }
+    }
+
     for (std::vector< std::pair<unsigned, uint64_t> >::iterator 
            it = kgepi->indices.begin(), ie = kgepi->indices.end(); 
          it != ie; ++it) {
@@ -2796,6 +2822,22 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
     if (kgepi->offset)
       base = AddExpr::create(base,
                              Expr::createPointer(kgepi->offset));
+
+    if (SingleObjectResolution) {
+      if (const_base && !isa<ConstantExpr>(base)) {
+        // the initial base address was a constant expression, the final is not:
+        // store the mapping between constant address and the non-const
+        // reference in the state
+        state.base_addrs[base] = original_base;
+      }
+
+      if (update) {
+        // we need to update the current entry with a new value
+        state.base_addrs[base] = value;
+        state.base_addrs.erase(key);
+      }
+    }
+
     bindLocal(ki, state, base);
     break;
   }
@@ -4305,71 +4347,107 @@ void Executor::executeMemoryOperation(ExecutionState &state,
 
   address = optimizer.optimizeExpr(address, true);
 
-  // fast path: single in-bounds resolution
   ObjectPair op;
   bool success;
   solver->setTimeout(coreSolverTimeout);
-  if (!state.addressSpace.resolveOne(state, solver.get(), address, op, success)) {
-    address = toConstant(state, address, "resolveOne failure");
-    success = state.addressSpace.resolveOne(cast<ConstantExpr>(address), op);
-  }
-  solver->setTimeout(time::Span());
-
-  if (success) {
-    const MemoryObject *mo = op.first;
 
-    if (MaxSymArraySize && mo->size >= MaxSymArraySize) {
-      address = toConstant(state, address, "max-sym-array-size");
+  bool resolveSingleObject = SingleObjectResolution;
+
+  if (resolveSingleObject && !isa<ConstantExpr>(address)) {
+    // Address is symbolic
+
+    resolveSingleObject = false;
+    ExecutionState::base_addrs_t::iterator base_it =
+        state.base_addrs.find(address);
+    if (base_it != state.base_addrs.end()) {
+      // Concrete address found in the map, now find the associated memory
+      // object
+      if (!state.addressSpace.resolveOne(state, solver.get(), base_it->second, op,
+                                         success) ||
+          !success) {
+        klee_warning("Failed to resolve concrete address from the base_addrs "
+                     "map to a memory object");
+      } else {
+        // We have resolved the stored concrete address to a memory object.
+        // Now let's see if we can prove an overflow - we are only interested in
+        // two cases: either we overflow and it's a bug or we don't and we carry
+        // on; in this mode we are not interested in trying out other memory
+        // objects
+        resolveSingleObject = true;
+      }
     }
-    
-    ref<Expr> offset = mo->getOffsetExpr(address);
-    ref<Expr> check = mo->getBoundsCheckOffset(offset, bytes);
-    check = optimizer.optimizeExpr(check, true);
+  } else {
+    resolveSingleObject = false;
+  }
 
-    bool inBounds;
-    solver->setTimeout(coreSolverTimeout);
-    bool success = solver->mustBeTrue(state.constraints, check, inBounds,
-                                      state.queryMetaData);
-    solver->setTimeout(time::Span());
-    if (!success) {
-      state.pc = state.prevPC;
-      terminateStateOnSolverError(state, "Query timed out (bounds check).");
-      return;
+  if (!resolveSingleObject) {
+    if (!state.addressSpace.resolveOne(state, solver.get(), address, op, success)) {
+      address = toConstant(state, address, "resolveOne failure");
+      success = state.addressSpace.resolveOne(cast<ConstantExpr>(address), op);
     }
+    solver->setTimeout(time::Span());
 
-    if (inBounds) {
-      const ObjectState *os = op.second;
-      if (isWrite) {
-        if (os->readOnly) {
-          terminateStateOnProgramError(state, "memory error: object read only",
-                                       StateTerminationType::ReadOnly);
-        } else {
-          ObjectState *wos = state.addressSpace.getWriteable(mo, os);
-          wos->write(offset, value);
-        }          
-      } else {
-        ref<Expr> result = os->read(offset, type);
-        
-        if (interpreterOpts.MakeConcreteSymbolic)
-          result = replaceReadWithSymbolic(state, result);
-        
-        bindLocal(target, state, result);
+    if (success) {
+      const MemoryObject *mo = op.first;
+
+      if (MaxSymArraySize && mo->size >= MaxSymArraySize) {
+        address = toConstant(state, address, "max-sym-array-size");
       }
 
-      return;
+      ref<Expr> offset = mo->getOffsetExpr(address);
+      ref<Expr> check = mo->getBoundsCheckOffset(offset, bytes);
+      check = optimizer.optimizeExpr(check, true);
+
+      bool inBounds;
+      solver->setTimeout(coreSolverTimeout);
+      bool success = solver->mustBeTrue(state.constraints, check, inBounds,
+                                        state.queryMetaData);
+      solver->setTimeout(time::Span());
+      if (!success) {
+        state.pc = state.prevPC;
+        terminateStateOnSolverError(state, "Query timed out (bounds check).");
+        return;
+      }
+
+      if (inBounds) {
+        const ObjectState *os = op.second;
+        if (isWrite) {
+          if (os->readOnly) {
+            terminateStateOnProgramError(state, "memory error: object read only",
+                                         StateTerminationType::ReadOnly);
+          } else {
+            ObjectState *wos = state.addressSpace.getWriteable(mo, os);
+            wos->write(offset, value);
+          }
+        } else {
+          ref<Expr> result = os->read(offset, type);
+
+          if (interpreterOpts.MakeConcreteSymbolic)
+            result = replaceReadWithSymbolic(state, result);
+
+          bindLocal(target, state, result);
+        }
+
+        return;
+      }
     }
-  } 
+  }
 
   // we are on an error path (no resolution, multiple resolution, one
-  // resolution with out of bounds)
+  // resolution with out of bounds), or we do a single object resolution
 
   address = optimizer.optimizeExpr(address, true);
-  ResolutionList rl;  
-  solver->setTimeout(coreSolverTimeout);
-  bool incomplete = state.addressSpace.resolve(state, solver.get(), address, rl,
-                                               0, coreSolverTimeout);
-  solver->setTimeout(time::Span());
-  
+  ResolutionList rl;
+  bool incomplete = false;
+
+  if (!resolveSingleObject) {
+    solver->setTimeout(coreSolverTimeout);
+    incomplete = state.addressSpace.resolve(state, solver.get(), address, rl, 0,
+                                            coreSolverTimeout);
+    solver->setTimeout(time::Span());
+  } else {
+    rl.push_back(op); // we already have the object pair, no need to look for it
+  }
   // XXX there is some query wasteage here. who cares?
   ExecutionState *unbound = &state;
   
@@ -4401,7 +4479,7 @@ void Executor::executeMemoryOperation(ExecutionState &state,
     if (!unbound)
       break;
   }
-  
+
   // XXX should we distinguish out of bounds and overlapped cases?
   if (unbound) {
     if (incomplete) {