From 6bf8f3676f7048c19f849435fdd7dbd43bd91301 Mon Sep 17 00:00:00 2001 From: Nguyễn Gia Phong Date: Thu, 11 May 2023 17:41:34 +0900 Subject: Avoid resolving combined SMT formulae --- lib/Core/ExecutionState.h | 6 +++ lib/Core/Executor.cpp | 113 +++++++++++++++++++++++++++++++--------------- lib/Core/Executor.h | 6 ++- 3 files changed, 87 insertions(+), 38 deletions(-) diff --git a/lib/Core/ExecutionState.h b/lib/Core/ExecutionState.h index 1a3f42e7..93ed8214 100644 --- a/lib/Core/ExecutionState.h +++ b/lib/Core/ExecutionState.h @@ -305,6 +305,12 @@ struct ExecutionStateIDCompare { return a->getID() < b->getID(); } }; + +struct ExecutionStateFormulaCompare { + bool operator()(const ExecutionState *a, const ExecutionState *b) const { + return a->formula < b->formula; + } +}; } #endif /* KLEE_EXECUTIONSTATE_H */ diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index b21ee913..6be77eb1 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -3902,7 +3902,27 @@ void Executor::extractDifferentiator(ExecutionState* a, ExecutionState* b, outputs[rev.first].second = out; posix_spawn_file_actions_destroy(&action); } + //const auto& p = this->diffTests.insert(std::make_pair(argv, outputs)); this->diffTests[argv] = outputs; + // :var :val cluster + std::map>> revOut; + for (auto& o : outputs) { + for (auto& var : o.second.first) + revOut[var.first][var.second].insert(o.first); + revOut[""][o.second.second].insert(o.first); // stdout + } + + for (auto& vp : revOut) + for (auto& p : vp.second) + for (auto& q : vp.second) { + if (&p == &q) + continue; + for (std::uint64_t i : p.second) + for (std::uint64_t j : q.second) + if (i < j) + this->decided.emplace(std::make_pair(i, j), + &this->diffTests[argv]); + } } std::string hash(std::string data) { @@ -3918,43 +3938,62 @@ void Executor::searchDifferentiators(ExecutionState* latest) { last_smt2_file.open(last_smt2_name); last_smt2_file << latest->formula; last_smt2_file.close(); - for (const auto& state : this->exitStates) { - // TODO: skip moar and order - if (state->patchNo == latest->patchNo) - continue; - auto smt2_name = hash(state->formula) + ".smt2"; - if (smt2_name == last_smt2_name) - continue; - - // File I/O is expensive but SMT solving is even more expensive (-; - // Seriously though, FIXME: implement symbdiff natively - std::ofstream smt2_file; - smt2_file.open(smt2_name); - smt2_file << state->formula; - smt2_file.close(); - - auto command = "symbdiff " + smt2_name + " " + last_smt2_name; - for (const auto& out : this->symOuts) - command += " " + std::to_string(out.second); - const auto out = popen((command + " 2> /dev/null").c_str(), "r"); - std::string formula; - char buffer[128]; - while (!feof(out)) - if (fgets(buffer, 127, out) != NULL) - formula += buffer; - remove(smt2_name.c_str()); - if (pclose(out)) - continue; - static z3::context c; - static z3::solver s {c}; - s.reset(); - s.from_string(formula.c_str()); - if (s.check() != z3::sat) + std::hash hashFn; + for (const auto& rev : this->exitStates) { + if (rev.first == latest->patchNo) continue; - this->extractDifferentiator(latest, state, s.get_model()); - assert(!this->diffTests.empty()); - break; + if (rev.first < latest->patchNo) { + if (this->decided.find(std::make_pair(rev.first, latest->patchNo)) + != this->decided.end()) + continue; + } else { + if (this->decided.find(std::make_pair(latest->patchNo, rev.first)) + != this->decided.end()) + continue; + } + for (const auto& state : rev.second) { + auto hashPair = std::make_pair(hashFn(state->formula), + hashFn(latest->formula)); + if (hashPair.first == hashPair.second || this->compared[hashPair]) + continue; + this->compared[hashPair] = true; + hashPair = {hashFn(latest->formula), hashFn(state->formula)}; + if (this->compared[hashPair]) + continue; + this->compared[hashPair] = true; + + // File I/O is expensive but SMT solving is even more expensive (-; + // Seriously though, FIXME: implement symbdiff natively + const auto& smt2_name = hash(state->formula) + ".smt2"; + std::ofstream smt2_file; + smt2_file.open(smt2_name); + smt2_file << state->formula; + smt2_file.close(); + + auto command = "symbdiff " + smt2_name + " " + last_smt2_name; + for (const auto& out : this->symOuts) + command += " " + std::to_string(out.second); + const auto out = popen((command + " 2> /dev/null").c_str(), "r"); + std::string formula; + char buffer[128]; + while (!feof(out)) + if (fgets(buffer, 127, out) != NULL) + formula += buffer; + remove(smt2_name.c_str()); + if (pclose(out)) + continue; + + static z3::context c; + static z3::solver s {c}; + s.reset(); + s.from_string(formula.c_str()); + if (s.check() != z3::sat) + continue; + this->extractDifferentiator(latest, state, s.get_model()); + assert(!this->diffTests.empty()); + break; + } } remove(last_smt2_name.c_str()); } @@ -3969,8 +4008,8 @@ void Executor::terminateStateOnExit(ExecutionState &state) { interpreterHandler->incPathsCompleted(); metaEnvVars[state.patchNo] = state.metaEnvVar; getConstraintLog(state, state.formula, Interpreter::SMTLIB2); - searchDifferentiators(&state); - exitStates.insert(&state); + if (exitStates[state.patchNo].insert(&state).second) + searchDifferentiators(&state); terminateState(state, StateTerminationType::Exit); } diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h index 4928a5ab..bb65b9ad 100644 --- a/lib/Core/Executor.h +++ b/lib/Core/Executor.h @@ -121,9 +121,13 @@ private: std::unique_ptr solver; std::unique_ptr memory; std::set states; - std::set exitStates; + std::map> exitStates; std::map metaEnvVars; std::map diffTests; + std::map, TestOuts*> decided; + std::map, bool> compared; StatsTracker *statsTracker; TreeStreamWriter *pathWriter, *symPathWriter; SpecialFunctionHandler *specialFunctionHandler; -- cgit 1.4.1