From 55b8a71ae4365b00fcca28d7e9c543bcf15cd6cc Mon Sep 17 00:00:00 2001 From: Nguyễn Gia Phong Date: Thu, 2 May 2024 17:53:41 +0900 Subject: Refine support for stdio capture --- lib/Core/Differentiator.cpp | 54 ++++++++++++++++++++++++++------------------- lib/Core/Differentiator.h | 10 ++++----- lib/Core/Executor.cpp | 2 +- runtime/POSIX/fd_init.c | 2 +- 4 files changed, 38 insertions(+), 30 deletions(-) diff --git a/lib/Core/Differentiator.cpp b/lib/Core/Differentiator.cpp index 95c08bda..553df337 100644 --- a/lib/Core/Differentiator.cpp +++ b/lib/Core/Differentiator.cpp @@ -109,35 +109,41 @@ Differentiator::Differentiator(std::unique_ptr* s, Differentiator::Bytes run(const std::uint64_t rev, const char* prog, - const Differentiator::TestArgs& argv) + const Differentiator::TestInps& inputs) { - int fildes[2]; + int ind[2], outd[2]; { - const auto err = pipe(fildes); + auto err = pipe(ind); + assert(!err); + err = pipe(outd); 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); + posix_spawn_file_actions_adddup2(&action, ind[0], 0); + posix_spawn_file_actions_addclose(&action, ind[1]); + posix_spawn_file_actions_addclose(&action, outd[0]); + posix_spawn_file_actions_adddup2(&action, outd[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::vector argv {prog}; + for (const auto& v : inputs.first) + argv.push_back((const char *) v.data()); + argv.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); + const_cast(argv.data()), envp); assert(!err); } - close(fildes[1]); + write(ind[0], inputs.second.data(), inputs.second.size()); + close(ind[0]); + close(outd[1]); char buffer[128]; // output buffer for concrete execution Differentiator::Bytes result; - for (unsigned char n; n = read(fildes[0], buffer, sizeof(buffer));) { + for (unsigned char n; n = read(outd[0], buffer, sizeof(buffer));) { assert(n >= 0); for (unsigned char i = 0; i < n; ++i) result.push_back(buffer[i]); @@ -156,14 +162,14 @@ logBytes(const Differentiator::Bytes& buffer) } void -logArgs(const Differentiator::TestArgs& args) +logInputs(const Differentiator::TestInps& inputs) { llvm::errs() << "Args:"; - for (const auto& s : args) { + for (const auto& s : inputs.first) { llvm::errs() << ' '; logBytes(s); } - llvm::errs() << '\n'; + llvm::errs() << "\nStdin: " << inputs.second.data() << '\n'; } void @@ -188,7 +194,7 @@ Differentiator::extract(ExecutionState* a, ExecutionState* b, const std::vector& objects, const std::vector& values) { - TestArgs argv; + TestInps inputs; TestOuts outputs; { std::map args; @@ -200,18 +206,20 @@ Differentiator::extract(ExecutionState* a, ExecutionState* b, } 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]; + } else if (name == "stdin") { + inputs.second = values[i]; } } uint8_t last = 0; for (const auto& [rev, arg] : args) { assert(rev == last); - argv.push_back(arg); + inputs.first.push_back(arg); last++; } } for (const auto& rev : this->revisions) - outputs[rev].second = run(rev, this->prog, argv); - this->tests[argv] = outputs; + outputs[rev].second = run(rev, this->prog, inputs); + this->tests[inputs] = outputs; std::map revOut; for (const auto& [rev, out] : outputs) { @@ -228,7 +236,7 @@ Differentiator::extract(ExecutionState* a, ExecutionState* b, for (std::uint64_t i : p.second) for (std::uint64_t j : q.second) if (i < j) - this->done.emplace(std::make_pair(i, j), &this->tests[argv]); + this->done.emplace(std::make_pair(i, j), &this->tests[inputs]); } } @@ -314,7 +322,7 @@ Differentiator::search(ExecutionState* latest) void Differentiator::log() { - std::vector> clusterings; + std::vector> clusterings; for (auto& t : this->tests) { Clusters clusters; for (const auto& rev : this->revisions) { @@ -327,8 +335,8 @@ Differentiator::log() if (clusters.size() > 1) clusterings.push_back({std::move(t.first), std::move(clusters)}); } - for (const auto& [args, clusters] : clusterings) { - logArgs(args); + for (const auto& [inputs, clusters] : clusterings) { + logInputs(inputs); logClusters(clusters); llvm::errs() << '\n'; } diff --git a/lib/Core/Differentiator.h b/lib/Core/Differentiator.h index 11225ac7..98c15e92 100644 --- a/lib/Core/Differentiator.h +++ b/lib/Core/Differentiator.h @@ -35,8 +35,8 @@ private: struct Differentiator { /// Buffer of bytes typedef std::vector Bytes; - /// CLI arguments - typedef std::vector TestArgs; + /// argv stdin + typedef std::pair, Bytes> TestInps; /// :rev (:var val) stdout typedef std::map, @@ -59,6 +59,8 @@ struct Differentiator { /// Program revision numbers std::set revisions; + /// Differentiated pairs + std::map, TestOuts*> done; private: /// Program path for concrete execution. const char* prog; @@ -67,7 +69,7 @@ private: std::set> exits; /// Differential tests - std::map tests; + std::map tests; /// SMT solver "borrowed" from Executor std::unique_ptr* solver; /// SMT solving timeout @@ -76,8 +78,6 @@ private: ArrayCache& arrayCache; /// Symbolic output renamers ExprCmbnVisitor visitorA, visitorB; - /// Differentiated pairs - std::map, TestOuts*> done; }; } // namespace klee diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index 465100f4..34b3d7b8 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -1104,7 +1104,7 @@ Executor::StatePair Executor::fork(ExecutionState ¤t, ref condition, // Fix branch in only-replay-seed mode, if we don't have both true // and false seeds. - if (isSeeding && + if (isSeeding && !Differentiator::extractPatchNumber(condition).first && (current.forkDisabled || OnlyReplaySeeds) && res == Solver::Unknown) { bool trueSeed=false, falseSeed=false; diff --git a/runtime/POSIX/fd_init.c b/runtime/POSIX/fd_init.c index b93148ec..90c04a73 100644 --- a/runtime/POSIX/fd_init.c +++ b/runtime/POSIX/fd_init.c @@ -153,7 +153,7 @@ void klee_init_fds(unsigned n_files, unsigned file_length, __exe_fs.sym_stdout = malloc(sizeof(*__exe_fs.sym_stdout)); if (!__exe_fs.sym_stdout) klee_report_error(__FILE__, __LINE__, "out of memory in klee_init_env", "user.err"); - __create_new_dfile(__exe_fs.sym_stdout, stdout_length, "stdout", &s); + __create_new_dfile(__exe_fs.sym_stdout, stdout_length, "out!stdout!0", &s); __exe_env.fds[1].dfile = __exe_fs.sym_stdout; __exe_fs.stdout_writes = 0; } -- cgit 1.4.1