aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorNguyễn Gia Phong <mcsinyx@disroot.org>2023-03-30 19:47:11 +0900
committerNguyễn Gia Phong <cnx@loang.net>2024-03-05 17:20:16 +0900
commit443992debf19fa09673ce4d493fc3de5e6beb536 (patch)
tree665855467f6a5e8d19e2cd5c4be998806d6d4af1
parentfe22b90764887ab69c20b1eccd773d47a8378b95 (diff)
downloadklee-443992debf19fa09673ce4d493fc3de5e6beb536.tar.gz
Implement differencial test structure
-rw-r--r--lib/Core/CMakeLists.txt1
-rw-r--r--lib/Core/Differentiator.cpp70
-rw-r--r--lib/Core/Differentiator.h43
3 files changed, 114 insertions, 0 deletions
diff --git a/lib/Core/CMakeLists.txt b/lib/Core/CMakeLists.txt
index 021c3ce7..534753eb 100644
--- a/lib/Core/CMakeLists.txt
+++ b/lib/Core/CMakeLists.txt
@@ -12,6 +12,7 @@ add_library(kleeCore
CallPathManager.cpp
Context.cpp
CoreStats.cpp
+ Differentiator.cpp
ExecutionState.cpp
ExecutionTree.cpp
ExecutionTreeWriter.cpp
diff --git a/lib/Core/Differentiator.cpp b/lib/Core/Differentiator.cpp
new file mode 100644
index 00000000..b0fc8caf
--- /dev/null
+++ b/lib/Core/Differentiator.cpp
@@ -0,0 +1,70 @@
+//===-- Differentiator.cpp ------------------------------------------------===//
+//
+// The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#include "Differentiator.h"
+
+#include <iomanip>
+#include <sstream>
+
+using namespace klee;
+
+namespace klee {
+bool isSymArg(std::string name) {
+ return (name.size() == 5 // string::starts_with requires C++20
+ && name[0] == 'a' && name[1] == 'r' && name[2] == 'g'
+ && '0' <= name[3] && name[3] <= '9'
+ && '0' <= name[4] && name[4] <= '9');
+}
+
+bool isSymOut(std::string name) {
+ // string::starts_with requires C++20
+ return (name[0] == 'o' && name[1] == 'u' && name[2] == 't' && name[3] == '!'
+ && '0' <= name[name.size() - 1] && name[name.size() - 1] <= '9');
+}
+
+std::string quoted(const std::string& s) {
+ std::stringstream ss;
+ ss << std::quoted(s);
+ return ss.str();
+}
+
+inline char hex(char c) {
+ return (c < 10) ? '0' + c : 'a' + c - 10;
+}
+
+void writeHex(llvm::raw_ostream& os, std::string s) {
+ for (const auto c : s)
+ os << "\\x" << hex(c >> 4) << hex(c & 0xf);
+}
+
+llvm::raw_ostream &operator<<(llvm::raw_ostream& os, const Differentiator& d) {
+ os << "{(";
+ uint8_t last = 0;
+ for (const auto& p : d.args) {
+ assert(p.first == last);
+ if (last)
+ os << " ";
+ os << quoted(p.second);
+ last++;
+ }
+ os << ") {";
+ last = 0;
+ for (const auto& p : d.outputs) {
+ os << (last ? " :" : ":") << p.first << " {"; os << d.revA << " ";
+ writeHex(os, p.second.first);
+ os << " " << d.revB << " ";
+ writeHex(os, p.second.second);
+ os << "}";
+ last++;
+ }
+ os << "}}";
+
+ return os;
+}
+}
diff --git a/lib/Core/Differentiator.h b/lib/Core/Differentiator.h
new file mode 100644
index 00000000..54a12ac7
--- /dev/null
+++ b/lib/Core/Differentiator.h
@@ -0,0 +1,43 @@
+//===-- Differentiator.h ----------------------------------------*- C++ -*-===//
+//
+// The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+//
+// Class to perform actual execution, hides implementation details from external
+// interpreter.
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef KLEE_DIFFERENTIATOR_H
+#define KLEE_DIFFERENTIATOR_H
+
+#include "llvm/Support/raw_ostream.h"
+
+#include <cstdint>
+#include <map>
+#include <string>
+
+namespace klee {
+
+/// Return if name matches arg\d\d
+bool isSymArg(std::string);
+
+/// Return if name matches out!.*\d
+bool isSymOut(std::string);
+
+struct Differentiator {
+ uint64_t revA, revB;
+ std::map<uint8_t, std::string> args;
+ std::map<std::string, std::pair<std::string, std::string>> outputs;
+ Differentiator(uint64_t a, uint64_t b) : revA{a}, revB{b} {}
+};
+
+/// Write convenient representation for debugging
+llvm::raw_ostream &operator<<(llvm::raw_ostream&, const Differentiator&);
+} // End klee namespace
+
+#endif /* KLEE_DIFFERENTIATOR_H */