feat: Reintroduce concrete store (#197)

Author: ocelaiwo

lib/Core/AddressSpace.cpp

@@ -18,6 +18,7 @@
 #include "klee/Statistics/TimerStatIncrementer.h"
 
 #include "CoreStats.h"
+#include <cstring>
 
 namespace klee {
 llvm::cl::OptionCategory
@@ -384,15 +385,15 @@ bool AddressSpace::resolve(ExecutionState &state, TimingSolver *solver,
 // transparently avoid screwing up symbolics (if the byte is symbolic
 // then its concrete cache byte isn't being used) but is just a hack.
 
-void AddressSpace::copyOutConcretes(const Assignment &assignment) {
+void AddressSpace::copyOutConcretes() {
   for (const auto &object : objects) {
     auto &mo = object.first;
     auto &os = object.second;
     if (ref<ConstantExpr> sizeExpr =
             dyn_cast<ConstantExpr>(mo->getSizeExpr())) {
       if (!mo->isUserSpecified && !os->readOnly &&
           sizeExpr->getZExtValue() != 0) {
-        copyOutConcrete(mo, os.get(), assignment);
+        copyOutConcrete(mo, os.get());
       }
     }
   }
@@ -407,27 +408,19 @@ ref<ConstantExpr> toConstantExpr(ref<Expr> expr) {
 }
 
 void AddressSpace::copyOutConcrete(const MemoryObject *mo,
-                                   const ObjectState *os,
-                                   const Assignment &assignment) const {
-  if (ref<ConstantExpr> addressExpr =
-          dyn_cast<ConstantExpr>(mo->getBaseExpr())) {
-    auto address =
-        reinterpret_cast<std::uint8_t *>(addressExpr->getZExtValue());
-    AssignmentEvaluator evaluator(assignment, false);
-    if (ref<ConstantExpr> sizeExpr =
-            dyn_cast<ConstantExpr>(mo->getSizeExpr())) {
-      size_t moSize = sizeExpr->getZExtValue();
-      std::vector<uint8_t> concreteStore(moSize);
-      for (size_t i = 0; i < moSize; i++) {
-        auto byte = evaluator.visit(os->readValue8(i));
-        concreteStore[i] = cast<ConstantExpr>(byte)->getZExtValue(Expr::Int8);
-      }
-      std::memcpy(address, concreteStore.data(), moSize);
+                                   const ObjectState *os) const {
+
+  if (auto addressExpr = dyn_cast<ConstantExpr>(mo->getBaseExpr())) {
+    if (auto sizeExpr = dyn_cast<ConstantExpr>(mo->getSizeExpr())) {
+      auto address =
+          reinterpret_cast<std::uint8_t *>(addressExpr->getZExtValue());
+      auto size = sizeExpr->getZExtValue();
+      std::memcpy(address, os->valueOS.concreteStore->data(), size);
     }
   }
 }
 
-bool AddressSpace::copyInConcretes(const Assignment &assignment) {
+bool AddressSpace::copyInConcretes() {
   for (auto &obj : objects) {
     const MemoryObject *mo = obj.first;
 
@@ -436,8 +429,7 @@ bool AddressSpace::copyInConcretes(const Assignment &assignment) {
 
       if (ref<ConstantExpr> arrayConstantAddress =
               dyn_cast<ConstantExpr>(mo->getBaseExpr())) {
-        if (!copyInConcrete(mo, os.get(), arrayConstantAddress->getZExtValue(),
-                            assignment))
+        if (!copyInConcrete(mo, os.get(), arrayConstantAddress->getZExtValue()))
           return false;
       }
     }
@@ -447,24 +439,17 @@ bool AddressSpace::copyInConcretes(const Assignment &assignment) {
 }
 
 bool AddressSpace::copyInConcrete(const MemoryObject *mo, const ObjectState *os,
-                                  uint64_t src_address,
-                                  const Assignment &assignment) {
-  AssignmentEvaluator evaluator(assignment, false);
+                                  uint64_t src_address) {
   auto address = reinterpret_cast<std::uint8_t *>(src_address);
-  size_t moSize =
-      cast<ConstantExpr>(evaluator.visit(mo->getSizeExpr()))->getZExtValue();
-  std::vector<uint8_t> concreteStore(moSize);
-  for (size_t i = 0; i < moSize; i++) {
-    auto byte = evaluator.visit(os->readValue8(i));
-    concreteStore[i] = cast<ConstantExpr>(byte)->getZExtValue(8);
-  }
-  if (memcmp(address, concreteStore.data(), moSize) != 0) {
+  size_t moSize = cast<ConstantExpr>(mo->getSizeExpr())->getZExtValue();
+
+  if (memcmp(address, os->valueOS.concreteStore->data(), moSize) != 0) {
     if (os->readOnly) {
       return false;
     } else {
       ObjectState *wos = getWriteable(mo, os);
       for (size_t i = 0; i < moSize; i++) {
-        wos->write(i, ConstantExpr::create(address[i], Expr::Int8));
+        wos->write8(i, address[i]);
       }
     }
   }

lib/Core/AddressSpace.h

@@ -13,7 +13,6 @@
 #include "Memory.h"
 
 #include "klee/ADT/ImmutableMap.h"
-#include "klee/Expr/Assignment.h"
 #include "klee/Expr/Expr.h"
 #include "klee/System/Time.h"
 
@@ -139,10 +138,9 @@ class AddressSpace {
   /// actual system memory location they were allocated at.
   /// Returns the (hypothetical) number of pages needed provided each written
   /// object occupies (at least) a single page.
-  void copyOutConcretes(const Assignment &assignment);
+  void copyOutConcretes();
 
-  void copyOutConcrete(const MemoryObject *mo, const ObjectState *os,
-                       const Assignment &assignment) const;
+  void copyOutConcrete(const MemoryObject *mo, const ObjectState *os) const;
 
   /// \brief Obtain an ObjectState suitable for writing.
   ///
@@ -164,7 +162,7 @@ class AddressSpace {
   ///
   /// \retval true The copy succeeded.
   /// \retval false The copy failed because a read-only object was modified.
-  bool copyInConcretes(const Assignment &assignment);
+  bool copyInConcretes();
 
   /// Updates the memory object with the raw memory from the address
   ///
@@ -175,7 +173,7 @@ class AddressSpace {
   /// externally
   /// @return
   bool copyInConcrete(const MemoryObject *mo, const ObjectState *os,
-                      uint64_t src_address, const Assignment &assignment);
+                      uint64_t src_address);
 };
 } // namespace klee
 

lib/Core/Executor.cpp

@@ -1140,7 +1140,7 @@ void Executor::initializeGlobalObjects(ExecutionState &state) {
       if (v.isConstant()) {
         os->setReadOnly(true);
         // initialise constant memory that may be used with external calls
-        state.addressSpace.copyOutConcrete(mo, os, {});
+        state.addressSpace.copyOutConcrete(mo, os);
       }
     }
   }
@@ -5252,15 +5252,31 @@ void Executor::callExternalFunction(ExecutionState &state, KInstruction *target,
                                                 // uniqueness
         ref<Expr> arg = *ai;
         if (auto pointer = dyn_cast<PointerExpr>(arg)) {
-          arg = pointer->getValue();
-        }
-        arg = optimizer.optimizeExpr(arg, true);
-        ref<ConstantExpr> ce = evaluator.visit(arg);
-        ce->toMemory(&args[wordIndex]);
-        if (ExternalCalls == ExternalCallPolicy::All) {
-          addConstraint(state, EqExpr::create(ce, arg));
+          ref<ConstantExpr> base = evaluator.visit(pointer->getBase());
+          ref<ConstantExpr> value = evaluator.visit(pointer->getValue());
+          value->toMemory(&args[wordIndex]);
+          ref<ConstantPointerExpr> const_pointer =
+              ConstantPointerExpr::create(base, value);
+          ObjectPair op;
+          if (state.addressSpace.resolveOne(const_pointer, op) &&
+              !op.second->readOnly) {
+            auto *os = state.addressSpace.getWriteable(op.first, op.second);
+            os->flushToConcreteStore(model);
+          }
+          if (ExternalCalls == ExternalCallPolicy::All) {
+            addConstraint(state,
+                          EqExpr::create(const_pointer->getValue(), arg));
+          }
+          wordIndex += (value->getWidth() + 63) / 64;
+        } else {
+          arg = optimizer.optimizeExpr(arg, true);
+          ref<ConstantExpr> ce = evaluator.visit(arg);
+          ce->toMemory(&args[wordIndex]);
+          if (ExternalCalls == ExternalCallPolicy::All) {
+            addConstraint(state, EqExpr::create(ce, arg));
+          }
+          wordIndex += (ce->getWidth() + 63) / 64;
         }
-        wordIndex += (ce->getWidth() + 63) / 64;
       } else {
         ref<Expr> arg = toUnique(state, *ai);
         if (ConstantExpr *ce = dyn_cast<ConstantExpr>(arg)) {
@@ -5296,7 +5312,7 @@ void Executor::callExternalFunction(ExecutionState &state, KInstruction *target,
   solver->getInitialValues(state.constraints.cs(), arrays, values,
                            state.queryMetaData);
   Assignment assignment(arrays, values);
-  state.addressSpace.copyOutConcretes(assignment);
+  state.addressSpace.copyOutConcretes();
 #ifndef WINDOWS
   // Update external errno state with local state value
   ObjectPair result;
@@ -5364,7 +5380,7 @@ void Executor::callExternalFunction(ExecutionState &state, KInstruction *target,
     return;
   }
 
-  if (!state.addressSpace.copyInConcretes(assignment)) {
+  if (!state.addressSpace.copyInConcretes()) {
     terminateStateOnExecError(state, "external modified read-only object",
                               StateTerminationType::External);
     return;
@@ -5374,7 +5390,7 @@ void Executor::callExternalFunction(ExecutionState &state, KInstruction *target,
   // Update errno memory object with the errno value from the call
   int error = externalDispatcher->getLastErrno();
   state.addressSpace.copyInConcrete(result.first, result.second,
-                                    (uint64_t)&error, assignment);
+                                    (uint64_t)&error);
 #endif
 
   Type *resultType = target->inst()->getType();