From 76a2adef91dc987083e8e30f40c4143742e4e726 Mon Sep 17 00:00:00 2001
From: Martin Nowack <m.nowack@imperial.ac.uk>
Date: Tue, 27 Feb 2024 16:20:11 +0000
Subject: Add support to fully concretise objects if modified externally

Propagate ExternalCallPolicy to allow user-based selection.
---
 lib/Core/AddressSpace.cpp | 24 +++++++++++++++---------
 lib/Core/AddressSpace.h   | 12 ++++++++----
 lib/Core/Executor.cpp     |  6 ++++--
 3 files changed, 27 insertions(+), 15 deletions(-)

diff --git a/lib/Core/AddressSpace.cpp b/lib/Core/AddressSpace.cpp
index bb77f0fc..138119b1 100644
--- a/lib/Core/AddressSpace.cpp
+++ b/lib/Core/AddressSpace.cpp
@@ -318,14 +318,14 @@ void AddressSpace::copyOutConcrete(const MemoryObject *mo,
   std::memcpy(address, os->concreteStore, mo->size);
 }
 
-bool AddressSpace::copyInConcretes() {
+bool AddressSpace::copyInConcretes(bool concretize) {
   for (auto &obj : objects) {
     const MemoryObject *mo = obj.first;
 
     if (!mo->isUserSpecified) {
       const auto &os = obj.second;
 
-      if (!copyInConcrete(mo, os.get(), mo->address))
+      if (!copyInConcrete(mo, os.get(), mo->address, concretize))
         return false;
     }
   }
@@ -334,7 +334,7 @@ bool AddressSpace::copyInConcretes() {
 }
 
 bool AddressSpace::copyInConcrete(const MemoryObject *mo, const ObjectState *os,
-                                  uint64_t src_address) {
+                                  uint64_t src_address, bool concretize) {
   auto address = reinterpret_cast<std::uint8_t*>(src_address);
 
   // Don't do anything if the underlying representation has not been changed
@@ -357,12 +357,18 @@ bool AddressSpace::copyInConcrete(const MemoryObject *mo, const ObjectState *os,
     return true;
   }
 
-  // The object is partially symbolic, it needs to be updated byte-by-byte
-  // via object state's `write` function
-  for (size_t i = 0, ie = mo->size; i < ie; ++i) {
-    u_int8_t external_byte_value = *(address + i);
-    if (external_byte_value != wos->concreteStore[i])
-      wos->write8(i, external_byte_value);
+  // Check if object should be concretized
+  if (concretize) {
+    wos->makeConcrete();
+    std::memcpy(wos->concreteStore, address, mo->size);
+  } else {
+    // The object is partially symbolic, it needs to be updated byte-by-byte
+    // via object state's `write` function
+    for (size_t i = 0, ie = mo->size; i < ie; ++i) {
+      u_int8_t external_byte_value = *(address + i);
+      if (external_byte_value != wos->concreteStore[i])
+        wos->write8(i, external_byte_value);
+    }
   }
   return true;
 }
diff --git a/lib/Core/AddressSpace.h b/lib/Core/AddressSpace.h
index 37ae76f9..fa4fb940 100644
--- a/lib/Core/AddressSpace.h
+++ b/lib/Core/AddressSpace.h
@@ -138,18 +138,22 @@ namespace klee {
     /// potentially copied) if the memory values are different from
     /// the current concrete values.
     ///
-    /// \retval true The copy succeeded. 
-    /// \retval false The copy failed because a read-only object was modified.
-    bool copyInConcretes();
+    /// \param concretize fully concretize the object representation if changed
+    /// externally
+    /// \return true if copy succeeded, otherwise false (e.g. try to modify
+    /// read-only object)
+    bool copyInConcretes(bool concretize);
 
     /// Updates the memory object with the raw memory from the address
     ///
     /// @param mo The MemoryObject to update
     /// @param os The associated memory state containing the actual data
     /// @param src_address the address to copy from
+    /// @param concretize fully concretize the object representation if changed
+    /// externally
     /// @return
     bool copyInConcrete(const MemoryObject *mo, const ObjectState *os,
-                        uint64_t src_address);
+                        uint64_t src_address, bool concretize);
   };
 } // End klee namespace
 
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index 1af88d88..bc27c5f3 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -4126,7 +4126,8 @@ void Executor::callExternalFunction(ExecutionState &state, KInstruction *target,
     return;
   }
 
-  if (!state.addressSpace.copyInConcretes()) {
+  if (!state.addressSpace.copyInConcretes(ExternalCalls ==
+                                          ExternalCallPolicy::All)) {
     terminateStateOnExecError(state, "external modified read-only object",
                               StateTerminationType::External);
     return;
@@ -4143,7 +4144,8 @@ 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);
+                                    (uint64_t)&error,
+                                    ExternalCalls == ExternalCallPolicy::All);
 #endif
 
   Type *resultType = target->inst->getType();
-- 
cgit 1.4.1