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

UnitTestBot · Oct 30, 2024 · 341ca93 · 341ca93
1 parent 400abb9
commit 341ca93
Show file tree

Hide file tree

Showing 21 changed files with 238 additions and 950 deletions.
diff --git a/.github/workflows/build.yaml b/.github/workflows/build.yaml
@@ -5,7 +5,7 @@ on:
   pull_request:
     branches: [main, utbot-main]
   push:
-   branches: [main, utbot-main, testheheh]
+    branches: [main, utbot-main, testheheh]
   workflow_dispatch:
     inputs:
       warnings_as_errors:

diff --git a/include/klee/ADT/KTest.h b/include/klee/ADT/KTest.h
@@ -66,7 +66,7 @@ unsigned kTest_numBytes(KTest *);
 
 void kTest_free(KTest *);
 
-unsigned getkTestMemoryUsage(KTest *ktest);
+unsigned getKTestMemoryUsage(KTest *ktest);
 #ifdef __cplusplus
 }
 #endif

diff --git a/include/klee/ADT/SeedFromFile.h b/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
diff --git a/include/klee/Core/Interpreter.h b/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"
@@ -58,11 +59,8 @@ 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;
+  virtual ToolJson info() const = 0;
 };
 
 /// [File][Line][Column] -> Opcode
@@ -212,6 +210,10 @@ 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(std::vector<SeedFromFile> seeds) = 0;
+
   virtual void runFunctionAsMain(llvm::Function *f, int argc, char **argv,
                                  char **envp) = 0;
 
@@ -239,7 +241,7 @@ class Interpreter {
   virtual void getSteppedInstructions(const ExecutionState &state,
                                       unsigned &res) = 0;
 
-  virtual bool getSymbolicSolution(const ExecutionState &state, KTest *res) = 0;
+  virtual bool getSymbolicSolution(const ExecutionState &state, KTest &res) = 0;
 
   virtual void addSARIFReport(const ExecutionState &state) = 0;
 

diff --git a/lib/ADT/CMakeLists.txt b/lib/ADT/CMakeLists.txt
@@ -8,6 +8,7 @@
 #===------------------------------------------------------------------------===#
 add_library(kleeADT
   SparseStorage.cpp
+  SeedFromFile.cpp
 )
 
 llvm_config(kleeADT "${USE_LLVM_SHARED}" support)

diff --git a/lib/ADT/SeedFromFile.cpp b/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;
+  }
+}
diff --git a/lib/Basic/KTest.cpp b/lib/Basic/KTest.cpp
@@ -13,7 +13,6 @@
 #include <cstdio>
 #include <cstdlib>
 #include <cstring>
-#include <fstream>
 
 #define KTEST_VERSION 4
 #define KTEST_MAGIC_SIZE 5
@@ -297,7 +296,7 @@ void kTest_free(KTest *bo) {
   free(bo);
 }
 
-unsigned getkTestMemoryUsage(KTest *ktest) {
+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);