diff options
Diffstat (limited to 'lib/Core/Executor.cpp')
-rw-r--r-- | lib/Core/Executor.cpp | 194 |
1 files changed, 88 insertions, 106 deletions
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index e5a6bc9c..73dc21fa 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -3421,8 +3421,8 @@ void Executor::updateStates(ExecutionState *current) { if (it3 != seedMap.end()) seedMap.erase(it3); executionTree->remove(es->executionTreeNode); - if (es->formula.empty()) - delete es; + // FIXME: collect garbage + // delete es; } removedStates.clear(); } @@ -3595,6 +3595,16 @@ bool Executor::checkMemoryUsage() { return false; } +std::string quoted(const char* s) { + std::stringstream ss; + ss << std::quoted(s); + return ss.str(); +} + +inline char hex(unsigned char c) { + return (c < 10) ? '0' + c : 'a' + c - 10; +} + void Executor::doDumpStates() { if (!DumpStatesOnHalt || states.empty()) { interpreterHandler->incPathsExplored(states.size()); @@ -3610,23 +3620,22 @@ void Executor::doDumpStates() { 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::map<TestVal, std::set<std::uint64_t>> stdoutClusters; + std::map<std::pair<std::string, TestVal>, 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); + // TODO: improve output format if (stdoutClusters.size() > 1) { llvm::errs() << "Args:"; for (const auto& s : t.first) - llvm::errs() << " \"" << s << '"'; + llvm::errs() << " \"" << quoted((const char *) s.data()) << '"'; llvm::errs() << '\n'; int i = 0; for (const auto& so : stdoutClusters) { - llvm::errs() << i++ << " " << so.first; + llvm::errs() << i++ << " " << so.first.data(); for (const auto& r : so.second) llvm::errs() << " " << r; llvm::errs() << '\n'; @@ -3836,40 +3845,28 @@ static std::string terminationTypeFileExtension(StateTerminationType type) { }; void Executor::extractDifferentiator(ExecutionState* a, ExecutionState* b, - const z3::model& m) { - std::map<std::uint8_t, std::string> args; + std::vector<const Array*> objects, + std::vector<TestVal> values) { + Executor::TestArgs argv; 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); - 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()); - args[i].push_back((unsigned char) c); - } - } else if (isSymOut(name.substr(0, name.size() - 2))) { - // TODO: use arguments for all patches - const auto& expr = m.eval(m[k]()); - std::string binary {""}; - const auto size = this->symOuts[name.substr(0, name.size() - 2)]; - for (uint8_t i = 0; i < size; ++i) { - const auto c = z3::select(expr, i).simplify().as_uint64(); - assert(c <= std::numeric_limits<unsigned char>::max()); - binary.push_back((unsigned char) c); + { + std::map<std::uint8_t, TestVal> args; + for (unsigned i = 0; i < objects.size(); ++i) { + const auto& name = objects[i]->name; + if (isSymArg(name)) { + args[std::atoi(name.c_str() + 3)] = values[i]; + args[std::atoi(name.c_str() + 3)].push_back(0); // null termination + } else if (isSymOut(name.substr(0, name.size() - 2))) { + const auto rev = ((name[name.size() - 1] == 'a') ? a : b)->patchNo; + outputs[rev].first[name.substr(4, name.size() - 6)] = values[i]; } - const auto rev = ((name[name.size() - 1] == 'a') ? a : b)->patchNo; - outputs[rev].first[name.substr(4, name.size() - 6)] = binary; } - } - Executor::TestArgs argv; - uint8_t last = 0; - for (const auto& p : args) { - assert(p.first == last); - argv.push_back(p.second); - last++; + uint8_t last = 0; + for (const auto& p : args) { + assert(p.first == last); + argv.push_back(p.second); + last++; + } } char buffer[128]; @@ -3877,8 +3874,8 @@ void Executor::extractDifferentiator(ExecutionState* a, ExecutionState* b, auto& envs = rev.second; pid_t pid; std::vector<const char*> argp {this->concreteProgram.c_str()}; - for (const auto& s : argv) - argp.push_back(s.c_str()); + for (const auto& v : argv) + argp.push_back((const char *) v.data()); argp.push_back(NULL); int fildes[2]; @@ -3894,19 +3891,17 @@ void Executor::extractDifferentiator(ExecutionState* a, ExecutionState* b, 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; + for (const unsigned char c : buffer) + outputs[rev.first].second.push_back(c); } - 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<std::string, std::map<std::string, std::set<std::uint64_t>>> revOut; + std::map<std::string, std::map<TestVal, std::set<std::uint64_t>>> revOut; for (auto& o : outputs) { for (auto& var : o.second.first) revOut[var.first][var.second].insert(o.first); @@ -3926,21 +3921,7 @@ void Executor::extractDifferentiator(ExecutionState* a, ExecutionState* b, } } -std::string hash(std::string data) { - std::stringstream stream; - stream << std::hex << std::setw(16) << std::setfill('0') - << std::hash<std::string>{}(data); - return stream.str(); -} - void Executor::searchDifferentiators(ExecutionState* latest) { - auto last_smt2_name = hash(latest->formula) + ".smt2"; - std::ofstream last_smt2_file; - last_smt2_file.open(last_smt2_name); - last_smt2_file << latest->formula; - last_smt2_file.close(); - - std::hash<std::string> hashFn; for (const auto& rev : this->exitStates) { if (rev.first == latest->patchNo) continue; @@ -3954,55 +3935,58 @@ void Executor::searchDifferentiators(ExecutionState* latest) { continue; } for (const auto& state : rev.second) { - // TODO: implement symbdiff natively - std::set<ref<Expr>> combination; - for (auto const& constraint : state->constraints) - combination.insert(this->visitorA.visit(constraint)); - for (auto const& constraint : latest->constraints) - combination.insert(this->visitorB.visit(constraint)); - - 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 (-; - 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; + ConstraintSet cmbnSet; + { + std::set<ref<Expr>> combination; + for (auto const& constraint : state->constraints) + combination.insert(this->visitorA.visit(constraint)); + for (auto const& constraint : latest->constraints) + combination.insert(this->visitorB.visit(constraint)); + for (auto const& constraint : combination) + cmbnSet.push_back(constraint); + } + + std::vector<const Array*> objects; + // FIXME: what if diff symbolics + for (const auto& sym : state->symbolics) { + if (isSymArg(sym.second->name)) { + objects.push_back(sym.second); + continue; + } + if (!isSymOut(sym.second->name)) + continue; + objects.push_back(arrayCache.CreateArray(sym.second->name + "!a", + sym.second->size)); + objects.push_back(arrayCache.CreateArray(sym.second->name + "!b", + sym.second->size)); + + ref<Expr> distinction; + // FIXME: impossible to use visitor hash + for (const auto& a : this->visitorA.outVars[sym.second->name]) { + const auto ne = NotExpr::create(EqExpr::create(a.second, + this->visitorB.outVars[sym.second->name][a.first])); + if (distinction.get() == nullptr) + distinction = ne; + else + distinction = OrExpr::create(ne, distinction); + } + assert(distinction.get() != nullptr); + cmbnSet.push_back(distinction); + } - static z3::context c; - static z3::solver s {c}; - s.reset(); - s.from_string(formula.c_str()); - if (s.check() != z3::sat) + this->solver->setTimeout(coreSolverTimeout); + std::vector<TestVal> values; + bool success = this->solver->getInitialValues(cmbnSet, objects, values, + state->queryMetaData); + solver->setTimeout(time::Span()); + if (!success) continue; - this->extractDifferentiator(latest, state, s.get_model()); + this->extractDifferentiator(latest, state, objects, values); assert(!this->diffTests.empty()); - break; + llvm::errs() << latest->patchNo << ' ' << state->patchNo << '\n'; + break; // one diff test per termination for now } } - remove(last_smt2_name.c_str()); } void Executor::terminateStateOnExit(ExecutionState &state) { @@ -4014,7 +3998,6 @@ void Executor::terminateStateOnExit(ExecutionState &state) { interpreterHandler->incPathsCompleted(); metaEnvVars[state.patchNo] = state.metaEnvVar; - getConstraintLog(state, state.formula, Interpreter::SMTLIB2); if (exitStates[state.patchNo].insert(&state).second) searchDifferentiators(&state); terminateState(state, StateTerminationType::Exit); @@ -4143,7 +4126,6 @@ void Executor::terminateStateOnError(ExecutionState &state, } metaEnvVars[state.patchNo] = state.metaEnvVar; - getConstraintLog(state, state.formula, Interpreter::SMTLIB2); if (exitStates[state.patchNo].insert(&state).second) searchDifferentiators(&state); terminateState(state, terminationType); |