Add option to store and rerun execution states during run

UnitTestBot · Jul 2, 2024 · 03b6802 · 03b6802
1 parent 4f237af
commit 03b6802
Show file tree

Hide file tree

Showing 20 changed files with 748 additions and 437 deletions.
diff --git a/include/klee/ADT/KTest.h b/include/klee/ADT/KTest.h
@@ -65,6 +65,7 @@ int kTest_toFile(const KTest *, const char *path);
 unsigned kTest_numBytes(KTest *);
 
 void kTest_free(KTest *);
+void test_kTest_free(KTest *);
 
 #ifdef __cplusplus
 }

diff --git a/include/klee/Core/BranchTypes.h b/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

diff --git a/include/klee/Core/Interpreter.h b/include/klee/Core/Interpreter.h
@@ -12,6 +12,7 @@
 #include "TerminationTypes.h"
 #include "klee/Module/Annotation.h"
 
+#include "klee/ADT/KTest.h"
 #include "klee/Module/SarifReport.h"
 
 #include <cstdint>
@@ -58,8 +59,11 @@ class InterpreterHandler {
 
   virtual void processTestCase(const ExecutionState &state, const char *message,
                                const char *suffix, bool isError = false) = 0;
-
   virtual ToolJson info() const = 0;
+
+  // used for writing .ktest files
+  virtual int argc() = 0;
+  virtual char **argv() = 0;
 };
 
 /// [File][Line][Column] -> Opcode
@@ -209,10 +213,6 @@ class Interpreter {
   // 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 runFunctionAsMain(llvm::Function *f, int argc, char **argv,
                                  char **envp) = 0;
 
@@ -237,7 +237,10 @@ class Interpreter {
   virtual void getConstraintLog(const ExecutionState &state, std::string &res,
                                 LogType logFormat = STP) = 0;
 
-  virtual bool getSymbolicSolution(const ExecutionState &state, KTest &res) = 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;
 

diff --git a/lib/Basic/KTest.cpp b/lib/Basic/KTest.cpp
@@ -9,10 +9,13 @@
 
 #include "klee/ADT/KTest.h"
 
+#include <cassert>
+#include <fstream>
 #include <stdint.h>
 #include <stdio.h>
 #include <stdlib.h>
 #include <string.h>
+#include <string>
 
 #define KTEST_VERSION 4
 #define KTEST_MAGIC_SIZE 5
@@ -295,3 +298,14 @@ void kTest_free(KTest *bo) {
   free(bo->objects);
   free(bo);
 }
+
+void test_kTest_free(KTest *bo) {
+  unsigned i;
+  for (i = 0; i < bo->numObjects; i++) {
+    free(bo->objects[i].name);
+    free(bo->objects[i].bytes);
+    free(bo->objects[i].pointers);
+  }
+  free(bo->objects);
+  free(bo);
+}
diff --git a/lib/Core/ExecutionState.cpp b/lib/Core/ExecutionState.cpp
@@ -178,7 +178,7 @@ ExecutionState::ExecutionState(const ExecutionState &state)
       gepExprBases(state.gepExprBases), multiplexKF(state.multiplexKF),
       prevTargets_(state.prevTargets_), targets_(state.targets_),
       prevHistory_(state.prevHistory_), history_(state.history_),
-      isTargeted_(state.isTargeted_) {
+      isTargeted_(state.isTargeted_), isSeeded(state.isSeeded) {
   queryMetaData.id = state.id;
 }
 

diff --git a/lib/Core/ExecutionState.h b/lib/Core/ExecutionState.h
@@ -151,6 +151,9 @@ struct ExecutionStack {
   inline const call_stack_ty &uniqueFrames() const { return uniqueFrames_; }
 
   void forceReturnLocation(const ref<CodeLocation> &location) {
+    if (callStack_.empty()) {
+      llvm::errs() << callStack_.size() << "\n";
+    }
     assert(!callStack_.empty() && "Call stack should contain at least one "
                                   "stack frame to force return location");
     std::optional<ref<CodeLocation>> &callStackReturnLocation =
@@ -300,6 +303,7 @@ class ExecutionState {
 public:
   using stack_ty = ExecutionStack;
 
+  bool isSeeded = false;
   // Execution - Control Flow specific
 
   /// @brief Pointer to initial instruction