From 570be9543a034d17591f91c9e46b593c9e4ad7f4 Mon Sep 17 00:00:00 2001
From: Nguyễn Gia Phong <mcsinyx@disroot.org>
Date: Thu, 30 Mar 2023 20:11:04 +0900
Subject: Implement differentiator extraction

---
 lib/Core/Executor.h | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)

(limited to 'lib/Core/Executor.h')

diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h
index 204638e8..8f2850fd 100644
--- a/lib/Core/Executor.h
+++ b/lib/Core/Executor.h
@@ -15,6 +15,7 @@
 #ifndef KLEE_EXECUTOR_H
 #define KLEE_EXECUTOR_H
 
+#include "Differentiator.h"
 #include "ExecutionState.h"
 #include "UserSearcher.h"
 
@@ -32,6 +33,9 @@
 #include "llvm/ADT/Twine.h"
 #include "llvm/Support/raw_ostream.h"
 
+#include <z3.h>
+#include <z3++.h>
+
 #include <map>
 #include <memory>
 #include <set>
@@ -113,6 +117,8 @@ private:
   std::unique_ptr<TimingSolver> solver;
   std::unique_ptr<MemoryManager> memory;
   std::set<ExecutionState*, ExecutionStateIDCompare> states;
+  std::set<ExecutionState*, ExecutionStateIDCompare> exitStates;
+  std::vector<Differentiator> diffTests;
   StatsTracker *statsTracker;
   TreeStreamWriter *pathWriter, *symPathWriter;
   SpecialFunctionHandler *specialFunctionHandler;
@@ -146,6 +152,12 @@ private:
   /// globals that have no representative object (e.g. aliases).
   std::map<const llvm::GlobalValue*, ref<ConstantExpr>> globalAddresses;
 
+  /// Size of symbolic arguments.
+  std::vector<size_t> symArgs;
+
+  /// Size of symbolic outputs.
+  std::map<std::string, size_t> symOuts;
+
   /// Map of legal function addresses to the corresponding Function.
   /// Used to validate and dereference function pointers.
   std::unordered_map<std::uint64_t, llvm::Function*> legalFunctions;
@@ -410,6 +422,12 @@ private:
   const InstructionInfo & getLastNonKleeInternalInstruction(const ExecutionState &state,
       llvm::Instruction** lastInstruction);
 
+  /// Extract differencial test from SMT model
+  void extractDifferentiator(uint64_t, uint64_t, const z3::model&);
+
+  /// Compare with other exit states for possible differencial tests
+  void searchDifferentiators(ExecutionState *state);
+
   /// Remove state from queue and delete state. This function should only be
   /// used in the termination functions below.
   void terminateState(ExecutionState &state);
-- 
cgit 1.4.1