about summary refs log tree commit diff homepage
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 */