[feat] Add options to store and rerun execution states during execution

Author: dim8art

include/klee/ADT/SeedFromFile.h

@@ -0,0 +1,19 @@
+#ifndef KLEE_SEED_FROM_FILE_H
+#include <string>
+
+class KTest;
+
+namespace klee {
+
+class SeedFromFile {
+public:
+  KTest *ktest;
+  unsigned maxInstructions;
+
+  SeedFromFile() {}
+  SeedFromFile(std::string _path);
+};
+
+} // namespace klee
+#define KLEE_SEED_FROM_FILE_H
+#endif

include/klee/Core/BranchTypes.h

@@ -25,7 +25,8 @@
   BTYPE(Realloc, 8U)                                                           \
   BTYPE(Free, 9U)                                                              \
   BTYPE(GetVal, 10U)                                                           \
-  BMARK(END, 10U)
+  BTYPE(InitialBranch, 11U)                                                    \
+  BMARK(END, 11U)
 /// \endcond
 
 /** @enum BranchType

include/klee/Core/Interpreter.h

@@ -10,6 +10,7 @@
 #define KLEE_INTERPRETER_H
 
 #include "TerminationTypes.h"
+#include "klee/ADT/SeedFromFile.h"
 #include "klee/Module/Annotation.h"
 
 #include "klee/Module/SarifReport.h"
@@ -200,18 +201,9 @@ class Interpreter {
   // to record the symbolic path (as a stream of '0' and '1' bytes).
   virtual void setSymbolicPathWriter(TreeStreamWriter *tsw) = 0;
 
-  // supply a test case to replay from. this can be used to drive the
-  // interpretation down a user specified path. use null to reset.
-  virtual void setReplayKTest(const struct KTest *out) = 0;
-
-  // supply a list of branch decisions specifying which direction to
-  // take on forks. this can be used to drive the interpretation down
-  // a user specified path. use null to reset.
-  virtual void setReplayPath(const std::vector<bool> *path) = 0;
-
   // supply a set of symbolic bindings that will be used as "seeds"
   // for the search. use null to reset.
-  virtual void useSeeds(const std::vector<struct KTest *> *seeds) = 0;
+  virtual void useSeeds(std::vector<SeedFromFile> seeds) = 0;
 
   virtual void runFunctionAsMain(llvm::Function *f, int argc, char **argv,
                                  char **envp) = 0;
@@ -237,6 +229,9 @@ class Interpreter {
   virtual void getConstraintLog(const ExecutionState &state, std::string &res,
                                 LogType logFormat = STP) = 0;
 
+  virtual void getSteppedInstructions(const ExecutionState &state,
+                                      unsigned &res) = 0;
+
   virtual bool getSymbolicSolution(const ExecutionState &state, KTest &res) = 0;
 
   virtual void addSARIFReport(const ExecutionState &state) = 0;

include/klee/Core/TerminationTypes.h

@@ -101,6 +101,7 @@ enum Reason {
   ErrorOnWhichShouldExit,
   Interrupt,
   MaxDepth,
+  MaxMemory,
   MaxStackFrames,
   MaxSolverTime,
   Unspecified

lib/ADT/CMakeLists.txt

@@ -7,7 +7,9 @@
 #
 #===------------------------------------------------------------------------===#
 add_library(kleeADT
+  SeedFromFile.cpp
   SparseStorage.cpp
+  SeedFromFile.cpp
 )
 
 llvm_config(kleeADT "${USE_LLVM_SHARED}" support)

lib/ADT/SeedFromFile.cpp

@@ -0,0 +1,14 @@
+#include "klee/ADT/SeedFromFile.h"
+#include "klee/ADT/KTest.h"
+
+#include <fstream>
+
+using namespace klee;
+
+SeedFromFile::SeedFromFile(std::string _path)
+    : ktest(kTest_fromFile((_path + "ktest").c_str())) {
+  std::ifstream seedInfoStream(_path + "seedinfo");
+  if (seedInfoStream.good()) {
+    seedInfoStream >> maxInstructions;
+  }
+}

lib/Basic/KTest.cpp

@@ -295,3 +295,13 @@ void kTest_free(KTest *bo) {
   free(bo->objects);
   free(bo);
 }
+
+unsigned getKTestMemoryUsage(KTest *ktest) {
+  size_t size = 0;
+  for (unsigned i = 0; i < ktest->numObjects; i++) {
+    size += std::strlen(ktest->objects[i].name) * sizeof(char);
+    size += ktest->objects[i].numBytes * sizeof(unsigned char);
+    size += ktest->objects[i].numPointers * sizeof(Pointer);
+  }
+  return size;
+}

lib/Core/ExecutionState.cpp

@@ -170,9 +170,9 @@ ExecutionState::ExecutionState(const ExecutionState &state)
       coveredNew(state.coveredNew), coveredNewError(state.coveredNewError),
       forkDisabled(state.forkDisabled), returnValue(state.returnValue),
       gepExprBases(state.gepExprBases), multiplexKF(state.multiplexKF),
-      prevTargets_(state.prevTargets_), targets_(state.targets_),
-      prevHistory_(state.prevHistory_), history_(state.history_),
-      isTargeted_(state.isTargeted_) {
+      isSeeded(state.isSeeded), prevTargets_(state.prevTargets_),
+      targets_(state.targets_), prevHistory_(state.prevHistory_),
+      history_(state.history_), isTargeted_(state.isTargeted_) {
   queryMetaData.id = state.id;
 }
 

lib/Core/ExecutionState.h

@@ -420,6 +420,8 @@ class ExecutionState {
   // Temp: to know which multiplex path this state has taken
   KFunction *multiplexKF = nullptr;
 
+  bool isSeeded = false;
+
 private:
   PersistentSet<ref<Target>> prevTargets_;
   PersistentSet<ref<Target>> targets_;
@@ -514,6 +516,11 @@ class ExecutionState {
 
   inline void setTargeted(bool targeted) { isTargeted_ = targeted; }
 
+  inline void setTargets(const PersistentSet<ref<Target>> &targets) {
+    targets_ = targets;
+    areTargetsChanged_ = true;
+  }
+
   inline void setTargets(const TargetHashSet &targets) {
     targets_ = PersistentSet<ref<Target>>();
     for (auto target : targets) {