From 017a80509b16fd02d88219312d5e1d3adf831eff Mon Sep 17 00:00:00 2001 From: Nguyễn Gia Phong Date: Wed, 26 Apr 2023 19:11:34 +0900 Subject: Conclude concrete execution impl --- lib/Core/Differentiator.cpp | 2 +- lib/Core/Differentiator.h | 10 ++++-- lib/Core/ExecutionState.cpp | 7 ++-- lib/Core/Executor.cpp | 86 ++++++++++++++++++++++++++++----------------- lib/Core/Executor.h | 4 ++- 5 files changed, 70 insertions(+), 39 deletions(-) diff --git a/lib/Core/Differentiator.cpp b/lib/Core/Differentiator.cpp index b0fc8caf..c68ec6d1 100644 --- a/lib/Core/Differentiator.cpp +++ b/lib/Core/Differentiator.cpp @@ -34,7 +34,7 @@ std::string quoted(const std::string& s) { return ss.str(); } -inline char hex(char c) { +inline char hex(unsigned char c) { return (c < 10) ? '0' + c : 'a' + c - 10; } diff --git a/lib/Core/Differentiator.h b/lib/Core/Differentiator.h index 54a12ac7..1f9c7766 100644 --- a/lib/Core/Differentiator.h +++ b/lib/Core/Differentiator.h @@ -30,10 +30,14 @@ bool isSymArg(std::string); bool isSymOut(std::string); struct Differentiator { - uint64_t revA, revB; - std::map args; + std::uint64_t revA, revB; + // arg_k => v + std::map args; + // k => (out!k!a, out!k!b) std::map> outputs; - Differentiator(uint64_t a, uint64_t b) : revA{a}, revB{b} {} + // rev => stdout + std::map stdouts; + Differentiator(std::uint64_t a, std::uint64_t b) : revA{a}, revB{b} {} }; /// Write convenient representation for debugging diff --git a/lib/Core/ExecutionState.cpp b/lib/Core/ExecutionState.cpp index 9f81c907..b614f6e4 100644 --- a/lib/Core/ExecutionState.cpp +++ b/lib/Core/ExecutionState.cpp @@ -421,9 +421,12 @@ std::string extractMetaEnvVar(ref e) { } void ExecutionState::addConstraint(ref e) { - this->metaEnvVar = extractMetaEnvVar(e); - if (!this->metaEnvVar.empty()) + auto v = extractMetaEnvVar(e); + if (!v.empty()) { + if (v.substr(v.size() - 2) != "=0") + this->metaEnvVar = v; return; + } ConstraintManager c(constraints); c.addConstraint(e); } diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index e87caa97..1906427e 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -3604,6 +3604,9 @@ void Executor::doDumpStates() { for (const auto &state : states) terminateStateEarly(*state, "Execution halting.", StateTerminationType::Interrupted); updateStates(nullptr); + + for (const auto& t : this->diffTests) + llvm::errs() << t << '\n'; } void Executor::run(ExecutionState &initialState) { @@ -3805,16 +3808,17 @@ static std::string terminationTypeFileExtension(StateTerminationType type) { return ret; }; -void Executor::extractDifferentiator(uint64_t a, uint64_t b, const z3::model& m) { - auto test = Differentiator {a, b}; +void Executor::extractDifferentiator(ExecutionState* a, ExecutionState* b, + const z3::model& m) { + auto test = Differentiator {a->patchNo, b->patchNo}; 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] = ""; const auto& expr = m.eval(m[k]()); - for (uint8_t b = 0; b < this->symArgs[i]; ++b) { - const auto c = z3::select(expr, b).simplify().as_uint64(); + 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::max()); test.args[i].push_back((unsigned char) c); } @@ -3823,8 +3827,8 @@ void Executor::extractDifferentiator(uint64_t a, uint64_t b, const z3::model& m) const auto& expr = m.eval(m[k]()); std::string binary {""}; const auto size = this->symOuts[name.substr(0, name.size() - 2)]; - for (uint8_t b = 0; b < size; ++b) { - const auto c = z3::select(expr, b).simplify().as_uint64(); + for (uint8_t i = 0; i < size; ++i) { + const auto c = z3::select(expr, i).simplify().as_uint64(); assert(c <= std::numeric_limits::max()); binary.push_back((unsigned char) c); const auto& ident = name.substr(4, name.size() - 6); @@ -3835,6 +3839,44 @@ void Executor::extractDifferentiator(uint64_t a, uint64_t b, const z3::model& m) } } } + llvm::errs() << test << '\n'; + + char buffer[128]; + for (auto& rev : this->metaEnvVars) { + auto& envs = rev.second; + pid_t pid; + std::vector 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); + + 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->concreteProgram.c_str(), &action, NULL, + const_cast(args.data()), + envs.empty() ? NULL : envp); + assert(!err); + close(fildes[1]); + std::string out = ""; + for (ssize_t n; n = read(fildes[0], buffer, 127);) { + assert(n >= 0); + buffer[n] = 0; + out += buffer; + } + test.stdouts[rev.first] = out; + llvm::errs() << "rev " << rev.first << ' ' << out; + posix_spawn_file_actions_destroy(&action); + } this->diffTests.push_back(test); } @@ -3869,14 +3911,15 @@ void Executor::searchDifferentiators(ExecutionState* latest) { 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.c_str(), "r"); + const auto out = popen((command + " 2> /dev/null").c_str(), "r"); std::string formula; char buffer[128]; while (!feof(out)) - if (fgets(buffer, 128, out) != NULL) + if (fgets(buffer, 127, out) != NULL) formula += buffer; - assert(pclose(out) == 0); remove(smt2_name.c_str()); + if (pclose(out)) + continue; static z3::context c; static z3::solver s {c}; @@ -3884,30 +3927,8 @@ void Executor::searchDifferentiators(ExecutionState* latest) { s.from_string(formula.c_str()); if (s.check() != z3::sat) continue; - this->extractDifferentiator(latest->patchNo, state->patchNo, s.get_model()); + this->extractDifferentiator(latest, state, s.get_model()); assert(!this->diffTests.empty()); - - pid_t pid; - std::vector args {this->concreteProgram.c_str()}; - uint8_t last = 0; - for (const auto& p : this->diffTests.back().args) { - assert(p.first == last); - args.push_back(p.second.c_str()); - last++; - } - int fildes[2]; - auto err = pipe(fildes); - if (err) - llvm::errs() << "failed creating pipe\n"; - 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(latest->metaEnvVar.c_str()), - NULL}; - auto status = posix_spawn(&pid, this->concreteProgram.c_str(), - &action, NULL, - const_cast(args.data()), envp); break; } remove(last_smt2_name.c_str()); @@ -3921,6 +3942,7 @@ void Executor::terminateStateOnExit(ExecutionState &state) { terminationTypeFileExtension(StateTerminationType::Exit).c_str()); interpreterHandler->incPathsCompleted(); + metaEnvVars[state.patchNo] = state.metaEnvVar; getConstraintLog(state, state.formula, Interpreter::SMTLIB2); searchDifferentiators(&state); exitStates.insert(&state); diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h index 6a6b19c0..3b10fa27 100644 --- a/lib/Core/Executor.h +++ b/lib/Core/Executor.h @@ -117,6 +117,7 @@ private: std::unique_ptr memory; std::set states; std::set exitStates; + std::map metaEnvVars; std::vector diffTests; StatsTracker *statsTracker; TreeStreamWriter *pathWriter, *symPathWriter; @@ -432,7 +433,8 @@ private: llvm::Instruction** lastInstruction); /// Extract differencial test from SMT model - void extractDifferentiator(uint64_t, uint64_t, const z3::model&); + void extractDifferentiator(ExecutionState*, ExecutionState*, + const z3::model&); /// Compare with other exit states for possible differencial tests void searchDifferentiators(ExecutionState *state); -- cgit 1.4.1