From 812c08bbc64cb0d2f82f2f44e83c5da390ee1355 Mon Sep 17 00:00:00 2001 From: Nguyễn Gia Phong Date: Thu, 23 Nov 2023 20:03:22 +0900 Subject: Clean up interfaces Psychic now extract patch number directly from meta conditions. Previously it was under the assumption that a patch is triggered by multiple choices. Now we allow a patch to have multiple hunks and the possibility to combine multiple patches. Internally, the code relevant diff test generation is moved under Differentiator. --- include/klee/klee.h | 1 - lib/Core/Differentiator.cpp | 183 +++++++++++++++++++++++++----------- lib/Core/Differentiator.h | 12 +-- lib/Core/ExecutionState.cpp | 53 ----------- lib/Core/ExecutionState.h | 4 +- lib/Core/Executor.cpp | 15 ++- lib/Core/SpecialFunctionHandler.cpp | 16 ---- lib/Core/SpecialFunctionHandler.h | 1 - 8 files changed, 147 insertions(+), 138 deletions(-) diff --git a/include/klee/klee.h b/include/klee/klee.h index 04cb75c8..07528595 100644 --- a/include/klee/klee.h +++ b/include/klee/klee.h @@ -118,7 +118,6 @@ extern "C" { void klee_prefer_cex(void *object, uintptr_t condition); void klee_posix_prefer_cex(void *object, uintptr_t condition); void klee_mark_global(void *object); - void klee_mark_patch(uint64_t patch_number); /* Return a possible constant value for the input expression. This allows programs to forcibly concretize values on their own. */ diff --git a/lib/Core/Differentiator.cpp b/lib/Core/Differentiator.cpp index 20aa69c9..2609e832 100644 --- a/lib/Core/Differentiator.cpp +++ b/lib/Core/Differentiator.cpp @@ -11,12 +11,74 @@ #include +#include +#include +#include + llvm::cl::opt InputProgram{llvm::cl::desc(""), llvm::cl::Positional, llvm::cl::Required}; using namespace klee; +bool +isSymArg(const std::string& name) +{ + /// Match arg\d\d + 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(const std::string& name) +{ + /// Match for out!.*\d + return (name[0] == 'o' && name[1] == 'u' && name[2] == 't' && name[3] == '!' + && '0' <= name[name.size() - 1] && name[name.size() - 1] <= '9'); +} + +std::pair +Differentiator::extractPatchNumber(ref e) +{ + if (e.get()->getKind() == Expr::And) { + const auto& et = dyn_cast(e.get()); + const auto& l = extractPatchNumber(et->left); + const auto& r = extractPatchNumber(et->right); + // Optimized if ((__choose\d+) == 0) {} else if (\1 == \d+) + assert(!(l.first && r.first)); + return {l.first || r.first, l.first ? l.second : r.second}; + } + if (e.get()->getKind() != Expr::Eq) + return {false, 0u}; // expecting __choose\d+ == \d+ + const auto eq = dyn_cast(e.get()); + // Expr is unbalanced to the right, hence scalar must be on the left. + if (eq->left.get()->getKind() != Expr::Constant) + return {false, 0u}; + const auto constant = dyn_cast(eq->left.get()); + if (constant->isFalse()) // negation + return {false, 0u}; // could only be !(__choose.+) anyway if meta + + ReadExpr* read; + if (eq->right.get()->getKind() == Expr::Read) { + read = dyn_cast(eq->right.get()); + } else { + if (eq->right.get()->getKind() != Expr::Concat) + return {false, 0u}; + const auto concat = dyn_cast(eq->right.get()); + if (concat->getLeft().get()->getKind() != Expr::Read) + return {false, 0u}; + read = dyn_cast(concat->getLeft().get()); + } + + const auto& name = read->updates.root->name; + // Skip when it is not __choose\d.* + if (name.substr(0, 8) != "__choose" || '0' > name[8] || name[8] > '9') + return {false, 0u}; + return {true, constant->getZExtValue()}; +} + ExprCmbnVisitor::ExprCmbnVisitor(char rev, ArrayCache& ac) : revision(rev), arrayCache(ac) {} @@ -28,7 +90,7 @@ ExprCmbnVisitor::visitExprPost(const Expr& e) return ExprVisitor::Action::doChildren(); const auto load = dyn_cast(&e); const auto orig = load->updates.root; - if (!Differentiator::isSymOut(orig->name)) + if (!isSymOut(orig->name)) return ExprVisitor::Action::doChildren(); const auto a = this->arrayCache.CreateArray( orig->name + '!' + this->revision, @@ -39,13 +101,50 @@ ExprCmbnVisitor::visitExprPost(const Expr& e) return ExprVisitor::Action::changeTo(replacement); } -bool -Differentiator::isSymArg(const std::string& name) +Differentiator::Differentiator(std::unique_ptr* s, + time::Span& t, ArrayCache& ac) +: revisions{{0}}, prog{InputProgram.c_str()}, solver{s}, solverTimeout{t}, + arrayCache{ac}, visitorA{'a', ac}, visitorB{'b', ac} +{} + +Differentiator::Bytes +run(const std::uint64_t rev, const char* prog, + const Differentiator::TestArgs& argv) { - 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'); + int fildes[2]; + { + const auto err = pipe(fildes); + assert(!err); + } + posix_spawn_file_actions_t action; + posix_spawn_file_actions_init(&action); + posix_spawn_file_actions_addclose(&action, fildes[0]); + posix_spawn_file_actions_adddup2(&action, fildes[1], 1); + { + pid_t pid; + std::vector argp {prog}; + for (const auto& v : argv) + argp.push_back((const char *) v.data()); + argp.push_back(NULL); + std::ostringstream env; + env << "KLEE_META=" << rev; + char *const envp[] = {const_cast(env.str().c_str()), NULL}; + const auto err = posix_spawn(&pid, prog, &action, NULL, + const_cast(argp.data()), envp); + assert(!err); + } + close(fildes[1]); + + char buffer[128]; // output buffer for concrete execution + Differentiator::Bytes result; + for (unsigned char n; n = read(fildes[0], buffer, sizeof(buffer));) { + assert(n >= 0); + for (unsigned char i = 0; i < n; ++i) + result.push_back(buffer[i]); + } + posix_spawn_file_actions_destroy(&action); + result.push_back(0); // null termination + return result; } bool @@ -82,56 +181,26 @@ Differentiator::extract(ExecutionState* a, ExecutionState* b, } } uint8_t last = 0; - for (const auto& p : args) { - assert(p.first == last); - argv.push_back(p.second); + for (const auto& [rev, arg] : args) { + assert(rev == last); + argv.push_back(arg); last++; } } - - char buffer[128]; // output buffer for concrete execution - for (const auto& rev : this->envs) { - auto& envs = rev.second; - pid_t pid; - std::vector argp {this->prog.c_str()}; - for (const auto& v : argv) - argp.push_back((const char *) v.data()); - argp.push_back(NULL); - - int fildes[2]; - auto err = pipe(fildes); - assert(!err); - posix_spawn_file_actions_t action; - posix_spawn_file_actions_init(&action); - posix_spawn_file_actions_addclose(&action, fildes[0]); - posix_spawn_file_actions_adddup2(&action, fildes[1], 1); - char *const envp[] = {const_cast(envs.c_str()), NULL}; - err = posix_spawn(&pid, this->prog.c_str(), &action, NULL, - const_cast(argp.data()), - envs.empty() ? NULL : envp); - assert(!err); - close(fildes[1]); - for (unsigned char n; n = read(fildes[0], buffer, sizeof(buffer));) { - assert(n >= 0); - for (unsigned char i = 0; i < n; ++i) - outputs[rev.first].second.push_back(buffer[i]); - } - outputs[rev.first].second.push_back(0); // null termination - posix_spawn_file_actions_destroy(&action); - } + for (const auto& rev : this->revisions) + outputs[rev].second = run(rev, this->prog, argv); this->tests[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 + std::map revOut; + for (const auto& [rev, out] : outputs) { + const auto& [syms, concrete] = out; + for (const auto& [var, val] : syms) + revOut[var][val].insert(rev); + revOut[""][concrete].insert(rev); } - - for (auto& vp : revOut) - for (auto& p : vp.second) - for (auto& q : vp.second) { + for (const auto& [_, clusters] : revOut) + for (const auto& p : clusters) + for (const auto& q : clusters) { if (&p == &q) continue; for (std::uint64_t i : p.second) @@ -162,11 +231,11 @@ Differentiator::search(ExecutionState* latest) ConstraintSet cmbnSet; { std::set> combination; - for (auto const& constraint : state->constraints) + for (const auto& constraint : state->constraints) combination.insert(this->visitorA.visit(constraint)); - for (auto const& constraint : latest->constraints) + for (const auto& constraint : latest->constraints) combination.insert(this->visitorB.visit(constraint)); - for (auto const& constraint : combination) + for (const auto& constraint : combination) cmbnSet.push_back(constraint); } @@ -191,8 +260,10 @@ Differentiator::search(ExecutionState* latest) // FIXME: impossible to use visitor hash for (const auto& a : this->visitorA.outVars[name]) { - const auto ne = NotExpr::create(EqExpr::create(a.second, - this->visitorB.outVars[name][a.first])); + const auto& b = this->visitorB.outVars[name].find(a.first); + if (b == this->visitorB.outVars[name].end()) + continue; + const auto& ne = NotExpr::create(EqExpr::create(a.second, b->second)); if (distinction.get() == nullptr) distinction = ne; else diff --git a/lib/Core/Differentiator.h b/lib/Core/Differentiator.h index 1927f8d7..3743743c 100644 --- a/lib/Core/Differentiator.h +++ b/lib/Core/Differentiator.h @@ -41,10 +41,8 @@ struct Differentiator { typedef std::map, Bytes>> TestOuts; - /// Return if name matches arg\d\d - static bool isSymArg(const std::string&); - /// Return if name matches out!.*\d - static bool isSymOut(const std::string&); + /// Extract revision number from given condition if any + static std::pair extractPatchNumber(ref e); Differentiator(std::unique_ptr*, time::Span&, ArrayCache&); /// Extract differential test from concrete execution @@ -56,11 +54,11 @@ struct Differentiator { /// Log patch differentiation result void log(); - /// Environment variables corresponding to each revision - std::map envs; + /// Program revision numbers + std::set revisions; private: /// Program path for concrete execution. - std::string prog; + const char* prog; /// Exit states std::map e) { - if (e.get()->getKind() == Expr::And) { - const auto et = dyn_cast(e.get()); - const auto& left = extractMetaEnvVar(et->left); - const auto& right = extractMetaEnvVar(et->right); - // Optimized if ((__choose\d+) == 0) {} else if (\1 == \d+) - assert(left.empty() || right.empty()); - return left.empty() ? right : left; - } - if (e.get()->getKind() != Expr::Eq) - return ""; // expecting __choose\d+ == \d+ - const auto eq = dyn_cast(e.get()); - // Expr is unbalanced to the right, hence scalar must be on the left. - if (eq->left.get()->getKind() != Expr::Constant) - return ""; - const auto constant = dyn_cast(eq->left.get()); - if (constant->isFalse()) // negation - return ""; // could only be !(__choose.+) if has __choose - - ReadExpr* read; - if (eq->right.get()->getKind() == Expr::Read) { - read = dyn_cast(eq->right.get()); - } else { - if (eq->right.get()->getKind() != Expr::Concat) - return ""; - const auto concat = dyn_cast(eq->right.get()); - if (concat->getLeft().get()->getKind() != Expr::Read) - return ""; - read = dyn_cast(concat->getLeft().get()); - } - - const auto& name = read->updates.root->name; - // Skip when it is not __choose\d.* - if (name.substr(0, 8) != "__choose" || '0' > name[8] || name[8] > '9') - return ""; - std::string value; - constant->toString(value); - unsigned char count = 1; - while (count < name.size() - 8 && name[count + 8] != '_') - ++count; - return "__SWITCH" + name.substr(8, count) + "=" + value; -} - void ExecutionState::addConstraint(ref e) { - auto v = extractMetaEnvVar(e); - if (!v.empty()) { - this->patchLocs++; - if (!this->metaEnvVar.empty()) - return; // one revision at once - if (v.substr(v.size() - 2) != "=0") - this->metaEnvVar = v; - return; - } ConstraintManager c(constraints); c.addConstraint(e); } diff --git a/lib/Core/ExecutionState.h b/lib/Core/ExecutionState.h index 0af3c336..038c62e3 100644 --- a/lib/Core/ExecutionState.h +++ b/lib/Core/ExecutionState.h @@ -232,9 +232,6 @@ public: /// @ brief The patch number, starting from 1; 0 being the original. std::uint64_t patchNo = 0; - /// @ brief Environment variable for runtime metaprogram switching. - std::string metaEnvVar = ""; - /// @brief The numbers of times this state has run through Executor::stepInstruction std::uint64_t steppedInstructions = 0; @@ -316,6 +313,7 @@ struct ExecutionStatePathCondCompare { j = b->constraints.begin(); i < a->constraints.end() && j < b->constraints.end(); ++i, ++j) return *i < *j; + return false; } }; } diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index 4dd486b6..279d5f3a 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -1236,6 +1236,19 @@ Executor::StatePair Executor::fork(ExecutionState ¤t, ref condition, } void Executor::addConstraint(ExecutionState &state, ref condition) { + const auto& [isMeta, patchNo] = Differentiator::extractPatchNumber(condition); + if (isMeta) { + if (state.patchNo && patchNo != state.patchNo) { + terminateStateEarly(state, "ignore patch combination", + StateTerminationType::SilentExit); + return; + } + state.patchLocs++; + if (!state.patchNo) + differ.revisions.insert(state.patchNo = patchNo); + return; + } + if (ConstantExpr *CE = dyn_cast(condition)) { if (!CE->isTrue()) llvm::report_fatal_error("attempt to add invalid constraint"); @@ -4002,7 +4015,7 @@ void Executor::terminateStateOnError(ExecutionState &state, interpreterHandler->processTestCase(state, msg.str().c_str(), file_suffix); } - differ.search(&state); + differ.search(&state); // e.g. sanitiser error terminateState(state, terminationType); if (shouldExitOn(terminationType)) diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp index f80f6b65..b0c28fbc 100644 --- a/lib/Core/SpecialFunctionHandler.cpp +++ b/lib/Core/SpecialFunctionHandler.cpp @@ -109,7 +109,6 @@ static constexpr std::array handlerInfo = { add("klee_is_symbolic", handleIsSymbolic, true), add("klee_make_symbolic", handleMakeSymbolic, false), add("klee_mark_global", handleMarkGlobal, false), - add("klee_mark_patch", handleMarkPatch, false), add("klee_open_merge", handleOpenMerge, false), add("klee_close_merge", handleCloseMerge, false), add("klee_prefer_cex", handlePreferCex, false), @@ -841,18 +840,3 @@ void SpecialFunctionHandler::handleMarkGlobal(ExecutionState &state, mo->isGlobal = true; } } - -void SpecialFunctionHandler::handleMarkPatch(ExecutionState &state, - KInstruction *target, - std::vector> &arguments) { - assert(arguments.size() == 1 && - "invalid number of arguments to klee_mark_patch"); - assert(isa(arguments[0]) && - "expect constant patch number argument to klee_mark_patch"); - auto patchNo = cast(arguments[0])->getLimitedValue(); - if (state.patchNo && patchNo != state.patchNo) - executor.terminateStateEarly(state, "ignore patch combination", - StateTerminationType::SilentExit); - else - executor.differ.envs[state.patchNo = patchNo] = state.metaEnvVar; -} diff --git a/lib/Core/SpecialFunctionHandler.h b/lib/Core/SpecialFunctionHandler.h index be0bc7d2..3fdbf8f8 100644 --- a/lib/Core/SpecialFunctionHandler.h +++ b/lib/Core/SpecialFunctionHandler.h @@ -101,7 +101,6 @@ namespace klee { HANDLER(handleMalloc); HANDLER(handleMemalign); HANDLER(handleMarkGlobal); - HANDLER(handleMarkPatch); HANDLER(handleOpenMerge); HANDLER(handleCloseMerge); HANDLER(handleNew); -- cgit 1.4.1