From 46b4c4885c0162893835081e2d9d731ca7a8341c Mon Sep 17 00:00:00 2001
From: Martin Nowack <m.nowack@imperial.ac.uk>
Date: Tue, 27 Feb 2024 15:59:00 +0000
Subject: Refactor `ObjectState::flushToConcreteStore` to use `toConstant`

Use existing `Executor::toConstant()` function to transform a symbolic
byte of an `ObjectState` to its concrete representation.

This will also add constraints if required.
---
 lib/Core/Executor.h |  1 +
 lib/Core/Memory.cpp | 23 ++++++++++-------------
 lib/Core/Memory.h   | 16 ++++++++++------
 3 files changed, 21 insertions(+), 19 deletions(-)

(limited to 'lib')

diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h
index 7be056a1..465751f6 100644
--- a/lib/Core/Executor.h
+++ b/lib/Core/Executor.h
@@ -94,6 +94,7 @@ class Executor : public Interpreter {
   friend class SpecialFunctionHandler;
   friend class StatsTracker;
   friend class MergeHandler;
+  friend class ObjectState;
   friend klee::Searcher *klee::constructUserSearcher(Executor &executor);
 
 public:
diff --git a/lib/Core/Memory.cpp b/lib/Core/Memory.cpp
index 0c9394bd..d77270f2 100644
--- a/lib/Core/Memory.cpp
+++ b/lib/Core/Memory.cpp
@@ -11,6 +11,7 @@
 
 #include "Context.h"
 #include "ExecutionState.h"
+#include "Executor.h"
 #include "MemoryManager.h"
 
 #include "klee/ADT/BitArray.h"
@@ -196,20 +197,16 @@ const UpdateList &ObjectState::getUpdates() const {
   return updates;
 }
 
-void ObjectState::flushToConcreteStore(TimingSolver *solver,
-                                       const ExecutionState &state) const {
+void ObjectState::flushToConcreteStore(Executor &executor,
+                                       ExecutionState &state, bool concretize) {
   for (unsigned i = 0; i < size; i++) {
-    if (!isByteConcrete(i)) {
-      ref<ConstantExpr> ce;
-      bool success = solver->getValue(state.constraints, read8(i), ce,
-                                      state.queryMetaData);
-      if (!success)
-        klee_warning("Solver timed out when getting a value for external call, "
-                     "byte %p+%u will have random value",
-                     (void *)object->address, i);
-      else
-        ce->toMemory(concreteStore + i);
-    }
+    if (isByteConcrete(i))
+      continue;
+    // Get a concrete value for the symbolic byte and write it to the memory
+    // object
+    ref<ConstantExpr> ce =
+        executor.toConstant(state, read8(i), "external call", concretize);
+    ce->toMemory(concreteStore + i);
   }
 }
 
diff --git a/lib/Core/Memory.h b/lib/Core/Memory.h
index 9a936746..3b365c20 100644
--- a/lib/Core/Memory.h
+++ b/lib/Core/Memory.h
@@ -29,6 +29,7 @@ namespace klee {
 class ArrayCache;
 class BitArray;
 class ExecutionState;
+class Executor;
 class MemoryManager;
 class Solver;
 
@@ -233,12 +234,15 @@ public:
   void write64(unsigned offset, uint64_t value);
   void print() const;
 
-  /*
-    Looks at all the symbolic bytes of this object, gets a value for them
-    from the solver and puts them in the concreteStore.
-  */
-  void flushToConcreteStore(TimingSolver *solver,
-                            const ExecutionState &state) const;
+  /// Generate concrete values for each symbolic byte of the object and put them
+  /// in the concrete store.
+  ///
+  /// \param executor
+  /// \param state
+  /// \param concretize if true, constraints for concretised bytes are added if
+  /// necessary
+  void flushToConcreteStore(Executor &executor, ExecutionState &state,
+                            bool concretize);
 
 private:
   const UpdateList &getUpdates() const;
-- 
cgit 1.4.1