diff options
author | Nguyễn Gia Phong <mcsinyx@disroot.org> | 2023-03-30 19:47:11 +0900 |
---|---|---|
committer | Nguyễn Gia Phong <cnx@loang.net> | 2024-03-05 17:20:16 +0900 |
commit | 443992debf19fa09673ce4d493fc3de5e6beb536 (patch) | |
tree | 665855467f6a5e8d19e2cd5c4be998806d6d4af1 | |
parent | fe22b90764887ab69c20b1eccd773d47a8378b95 (diff) | |
download | klee-443992debf19fa09673ce4d493fc3de5e6beb536.tar.gz |
Implement differencial test structure
-rw-r--r-- | lib/Core/CMakeLists.txt | 1 | ||||
-rw-r--r-- | lib/Core/Differentiator.cpp | 70 | ||||
-rw-r--r-- | lib/Core/Differentiator.h | 43 |
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 */ |