aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/Core
diff options
context:
space:
mode:
Diffstat (limited to 'lib/Core')
-rw-r--r--lib/Core/CMakeLists.txt1
-rw-r--r--lib/Core/Differentiator.cpp23
-rw-r--r--lib/Core/Differentiator.h8
-rw-r--r--lib/Core/Executor.cpp73
-rw-r--r--lib/Core/Executor.h16
-rw-r--r--lib/Core/ExecutorUtil.cpp13
6 files changed, 80 insertions, 54 deletions
diff --git a/lib/Core/CMakeLists.txt b/lib/Core/CMakeLists.txt
index 5f392ec9..9005a1ff 100644
--- a/lib/Core/CMakeLists.txt
+++ b/lib/Core/CMakeLists.txt
@@ -12,7 +12,6 @@ add_library(kleeCore
CallPathManager.cpp
Context.cpp
CoreStats.cpp
- Differentiator.cpp
ExecutionState.cpp
Executor.cpp
ExecutorUtil.cpp
diff --git a/lib/Core/Differentiator.cpp b/lib/Core/Differentiator.cpp
index c68ec6d1..ea713ad4 100644
--- a/lib/Core/Differentiator.cpp
+++ b/lib/Core/Differentiator.cpp
@@ -15,18 +15,6 @@
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;
@@ -46,22 +34,19 @@ void writeHex(llvm::raw_ostream& os, std::string s) {
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)
+ for (const auto& s : d.args) {
+ if (last++)
os << " ";
- os << quoted(p.second);
- last++;
+ os << quoted(s);
}
os << ") {";
last = 0;
for (const auto& p : d.outputs) {
- os << (last ? " :" : ":") << p.first << " {"; os << d.revA << " ";
+ os << (last++ ? " :" : ":") << p.first << " {"; os << d.revA << " ";
writeHex(os, p.second.first);
os << " " << d.revB << " ";
writeHex(os, p.second.second);
os << "}";
- last++;
}
os << "}}";
diff --git a/lib/Core/Differentiator.h b/lib/Core/Differentiator.h
index b9aa1ba4..70e83848 100644
--- a/lib/Core/Differentiator.h
+++ b/lib/Core/Differentiator.h
@@ -23,16 +23,10 @@
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 {
std::uint64_t revA, revB;
// arg_k => v
- std::map<std::uint8_t, std::string> args;
+ std::vector<std::string> args;
// k => (out!k!a, out!k!b)
std::map<std::string, std::pair<std::string, std::string>> outputs;
// rev => stdout
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index 2b2fcec9..78c3d8d5 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -3479,8 +3479,34 @@ void Executor::doDumpStates() {
terminateStateEarly(*state, "Execution halting.", StateTerminationType::Interrupted);
updateStates(nullptr);
- for (const auto& t : this->diffTests)
- llvm::errs() << t << '\n';
+ std::set<uint64_t> revs;
+ for (const auto& p : this->metaEnvVars)
+ revs.insert(p.first);
+ for (const auto& t : this->diffTests) {
+ std::map<std::string, std::set<std::uint64_t>> stdoutClusters;
+ std::map<std::pair<std::string, std::string>,
+ std::set<std::uint64_t>> varClusters;
+ if (t.second.size() < this->metaEnvVars.size())
+ continue;
+ for (const auto& rev : t.second) {
+ for (const auto& var : rev.second.first)
+ varClusters[var].insert(rev.first);
+ stdoutClusters[rev.second.second].insert(rev.first);
+ if (stdoutClusters.size() > 1) {
+ llvm::errs() << "Args:";
+ for (const auto& s : t.first)
+ llvm::errs() << " \"" << s << '"';
+ llvm::errs() << '\n';
+ int i = 0;
+ for (const auto& so : stdoutClusters) {
+ llvm::errs() << i++ << " " << so.first;
+ for (const auto& r : so.second)
+ llvm::errs() << " " << r;
+ llvm::errs() << '\n';
+ }
+ }
+ }
+ }
}
void Executor::run(ExecutionState &initialState) {
@@ -3681,17 +3707,18 @@ static std::string terminationTypeFileExtension(StateTerminationType type) {
void Executor::extractDifferentiator(ExecutionState* a, ExecutionState* b,
const z3::model& m) {
- auto test = Differentiator {a->patchNo, b->patchNo};
+ std::map<std::uint8_t, std::string> args;
+ Executor::TestOuts outputs;
for (auto k = m.size(); k--;) {
const auto& name = m[k].name().str();
if (isSymArg(name)) {
const uint8_t i = std::atoi(name.c_str() + 3);
- test.args[i] = "";
+ args[i] = "";
const auto& expr = m.eval(m[k]());
for (uint8_t i = 0; i < this->symArgs[i]; ++i) {
const auto c = z3::select(expr, i).simplify().as_uint64();
assert(c <= std::numeric_limits<unsigned char>::max());
- test.args[i].push_back((unsigned char) c);
+ args[i].push_back((unsigned char) c);
}
} else if (isSymOut(name.substr(0, name.size() - 2))) {
// TODO: use arguments for all patches
@@ -3702,28 +3729,27 @@ void Executor::extractDifferentiator(ExecutionState* a, ExecutionState* b,
const auto c = z3::select(expr, i).simplify().as_uint64();
assert(c <= std::numeric_limits<unsigned char>::max());
binary.push_back((unsigned char) c);
- const auto& ident = name.substr(4, name.size() - 6);
- if (name[name.size() - 1] == 'a')
- test.outputs[ident].first = binary;
- else
- test.outputs[ident].second = binary;
}
+ const auto rev = ((name[name.size() - 1] == 'a') ? a : b)->patchNo;
+ outputs[rev].first[name.substr(4, name.size() - 6)] = binary;
}
}
- llvm::errs() << test << '\n';
+ Executor::TestArgs argv;
+ uint8_t last = 0;
+ for (const auto& p : args) {
+ assert(p.first == last);
+ argv.push_back(p.second);
+ last++;
+ }
char buffer[128];
- for (auto& rev : this->metaEnvVars) {
+ for (const auto& rev : this->metaEnvVars) {
auto& envs = rev.second;
pid_t pid;
- std::vector<const char*> args {this->concreteProgram.c_str()};
- uint8_t last = 0;
- for (const auto& p : test.args) {
- assert(p.first == last);
- args.push_back(p.second.c_str());
- last++;
- }
- args.push_back(NULL);
+ std::vector<const char*> argp {this->concreteProgram.c_str()};
+ for (const auto& s : argv)
+ argp.push_back(s.c_str());
+ argp.push_back(NULL);
int fildes[2];
auto err = pipe(fildes);
@@ -3734,7 +3760,7 @@ void Executor::extractDifferentiator(ExecutionState* a, ExecutionState* b,
posix_spawn_file_actions_adddup2(&action, fildes[1], 1);
char *const envp[] = {const_cast<char* const>(envs.c_str()), NULL};
err = posix_spawn(&pid, this->concreteProgram.c_str(), &action, NULL,
- const_cast<char* const *>(args.data()),
+ const_cast<char* const *>(argp.data()),
envs.empty() ? NULL : envp);
assert(!err);
close(fildes[1]);
@@ -3744,11 +3770,10 @@ void Executor::extractDifferentiator(ExecutionState* a, ExecutionState* b,
buffer[n] = 0;
out += buffer;
}
- test.stdouts[rev.first] = out;
- llvm::errs() << "rev " << rev.first << ' ' << out;
+ outputs[rev.first].second = out;
posix_spawn_file_actions_destroy(&action);
}
- this->diffTests.push_back(test);
+ this->diffTests[argv] = outputs;
}
std::string hash(std::string data) {
diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h
index af3a3778..89819157 100644
--- a/lib/Core/Executor.h
+++ b/lib/Core/Executor.h
@@ -15,7 +15,6 @@
#ifndef KLEE_EXECUTOR_H
#define KLEE_EXECUTOR_H
-#include "Differentiator.h"
#include "ExecutionState.h"
#include "UserSearcher.h"
@@ -109,6 +108,12 @@ public:
RNG theRNG;
private:
+ typedef std::vector<std::string> TestArgs;
+ /// :rev (:var val) stdout
+ typedef std::map<std::uint64_t,
+ std::pair<std::map<std::string, std::string>,
+ std::string>> TestOuts;
+
std::unique_ptr<KModule> kmodule;
InterpreterHandler *interpreterHandler;
Searcher *searcher;
@@ -119,7 +124,7 @@ private:
std::set<ExecutionState*, ExecutionStateIDCompare> states;
std::set<ExecutionState*, ExecutionStateIDCompare> exitStates;
std::map<std::uint64_t, std::string> metaEnvVars;
- std::vector<Differentiator> diffTests;
+ std::map<TestArgs, TestOuts> diffTests;
StatsTracker *statsTracker;
TreeStreamWriter *pathWriter, *symPathWriter;
SpecialFunctionHandler *specialFunctionHandler;
@@ -602,7 +607,12 @@ public:
MergingSearcher *getMergingSearcher() const { return mergingSearcher; };
void setMergingSearcher(MergingSearcher *ms) { mergingSearcher = ms; };
};
-
+
+/// Return if name matches arg\d\d
+bool isSymArg(std::string);
+
+/// Return if name matches out!.*\d
+bool isSymOut(std::string);
} // End klee namespace
#endif /* KLEE_EXECUTOR_H */
diff --git a/lib/Core/ExecutorUtil.cpp b/lib/Core/ExecutorUtil.cpp
index 09f58fd3..2c2c0018 100644
--- a/lib/Core/ExecutorUtil.cpp
+++ b/lib/Core/ExecutorUtil.cpp
@@ -274,4 +274,17 @@ namespace klee {
llvm_unreachable("Unsupported expression in evalConstantExpr");
return op1;
}
+
+ 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');
+ }
}
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-22 23:31:10 +0000