[feature] add symcretes

lib/Core/ExecutionState.cpp

@@ -135,6 +135,7 @@ ExecutionState::ExecutionState(const ExecutionState& state):
     symbolics(state.symbolics),
     cexPreferences(state.cexPreferences),
     arrayNames(state.arrayNames),
+    symcretes(state.symcretes),
     openMergeStack(state.openMergeStack),
     steppedInstructions(state.steppedInstructions),
     steppedMemoryInstructions(state.steppedMemoryInstructions),
@@ -210,6 +211,24 @@ void ExecutionState::addSymbolic(const MemoryObject *mo, const Array *array) {
   symbolics.emplace_back(ref<const MemoryObject>(mo), array);
 }
 
+bool ExecutionState::isSymcrete(const Array *array) {
+  return symcretes.bindings.count(array);
+}
+
+void ExecutionState::addSymcrete(
+    const Array *array, const std::vector<unsigned char> &concretisation) {
+  assert(array && array->isSymbolicArray() &&
+         "Cannot make concrete array symcrete");
+  assert(array->size == concretisation.size() &&
+         "Given concretisation does not fit the array");
+  assert(!isSymcrete(array) && "Array already symcrete");
+  symcretes.bindings[array] = concretisation;
+}
+
+ref<Expr> ExecutionState::evaluateWithSymcretes(ref<Expr> e) {
+  return symcretes.evaluate(e);
+}
+
 /**/
 
 llvm::raw_ostream &klee::operator<<(llvm::raw_ostream &os, const MemoryMap &mm) {

lib/Core/ExecutionState.h

@@ -17,6 +17,7 @@
 
 #include "klee/ADT/ImmutableSet.h"
 #include "klee/ADT/TreeStream.h"
+#include "klee/Expr/Assignment.h"
 #include "klee/Expr/Constraints.h"
 #include "klee/Expr/Expr.h"
 #include "klee/Expr/ExprHashMap.h"
@@ -209,6 +210,9 @@ class ExecutionState {
   /// @brief If not null, represents current targets to be reached
   std::unordered_map<ReachWithError, ref<Target> > *targetsOfCurrentKBlock = nullptr;
 
+  std::set<std::pair<const MemoryObject *, ref<ObjectState>>>
+      unaddressableSymbolics;
+
   /// Statistics and information
 
   /// @brief Metadata utilized and collected by solvers for this state
@@ -241,6 +245,9 @@ class ExecutionState {
   /// @brief Set of used array names for this state.  Used to avoid collisions.
   std::set<std::string> arrayNames;
 
+  /// @brief Symcrete concretisations for this state
+  Assignment symcretes;
+
   /// @brief The objects handling the klee_open_merge calls this state ran through
   std::vector<ref<MergeHandler>> openMergeStack;
 
@@ -301,6 +308,13 @@ class ExecutionState {
 
   void addSymbolic(const MemoryObject *mo, const Array *array);
 
+  bool isSymcrete(const Array *array);
+
+  void addSymcrete(const Array *array,
+                   const std::vector<unsigned char> &concretisation);
+
+  ref<Expr> evaluateWithSymcretes(ref<Expr> e);
+
   void addConstraint(ref<Expr> e);
   void addCexPreference(const ref<Expr> &cond);