From 60e89a2266abcca60bdd8a89ef1d9d9d25e8581c Mon Sep 17 00:00:00 2001 From: Aleksandr Misonizhnik Date: Tue, 24 Oct 2023 18:34:36 +0400 Subject: [PATCH] [fix] Generate test only for successful solution found --- lib/Core/Executor.cpp | 1 - tools/klee/main.cpp | 147 +++++++++++++++++++++--------------------- 2 files changed, 73 insertions(+), 75 deletions(-) diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index dd34b18d5d..0fbbcfe1f8 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -7180,7 +7180,6 @@ bool Executor::getSymbolicSolution(const ExecutionState &state, KTest &res) { } bool success = solver->getInitialValues(extendedConstraints.cs(), objects, values, state.queryMetaData); - Assignment assignment(objects, values); solver->setTimeout(time::Span()); if (!success) { klee_warning("unable to compute initial values (invalid constraints?)!"); diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp index 0e509a9c00..71e7f8623a 100644 --- a/tools/klee/main.cpp +++ b/tools/klee/main.cpp @@ -34,6 +34,7 @@ DISABLE_WARNING_DEPRECATED_DECLARATIONS #include "llvm/Bitcode/BitcodeReader.h" #include "llvm/IR/Constants.h" #include "llvm/IR/IRBuilder.h" +#include "llvm/IR/InstIterator.h" #include "llvm/IR/Instruction.h" #include "llvm/IR/LLVMContext.h" #include "llvm/IR/Type.h" @@ -62,7 +63,6 @@ DISABLE_WARNING_POP #include #include #include -#include #include using json = nlohmann::json; @@ -601,9 +601,8 @@ void KleeHandler::processTestCase(const ExecutionState &state, const auto start_time = time::getWallTime(); bool atLeastOneGenerated = false; - if (WriteKTests) { - - if (success) { + if (success) { + if (WriteKTests) { for (unsigned i = 0; i < ktest.uninitCoeff + 1; ++i) { if (!kTest_toFile( &ktest, @@ -620,49 +619,36 @@ void KleeHandler::processTestCase(const ExecutionState &state, } } - if (message) { - auto f = openTestFile(suffix, id); - if (f) - *f << message; - } - - if (m_pathWriter) { - std::vector concreteBranches; - m_pathWriter->readStream(m_interpreter->getPathStreamID(state), - concreteBranches); - auto f = openTestFile("path", id); - if (f) { - for (const auto &branch : concreteBranches) { - *f << branch << '\n'; - } + if (WriteXMLTests) { + for (unsigned i = 0; i < ktest.uninitCoeff + 1; ++i) { + writeTestCaseXML(message != nullptr, ktest, id, i); + atLeastOneGenerated = true; } } - } - if (message || WriteKQueries) { - std::string constraints; - m_interpreter->getConstraintLog(state, constraints, Interpreter::KQUERY); - auto f = openTestFile("kquery", id); - if (f) - *f << constraints; + for (unsigned i = 0; i < ktest.numObjects; i++) { + delete[] ktest.objects[i].bytes; + delete[] ktest.objects[i].pointers; + } + delete[] ktest.objects; } - if (WriteCVCs) { - // FIXME: If using Z3 as the core solver the emitted file is actually - // SMT-LIBv2 not CVC which is a bit confusing - std::string constraints; - m_interpreter->getConstraintLog(state, constraints, Interpreter::STP); - auto f = openTestFile("cvc", id); + if (message) { + auto f = openTestFile(suffix, id); if (f) - *f << constraints; + *f << message; } - if (WriteSMT2s) { - std::string constraints; - m_interpreter->getConstraintLog(state, constraints, Interpreter::SMTLIB2); - auto f = openTestFile("smt2", id); - if (f) - *f << constraints; + if (m_pathWriter) { + std::vector concreteBranches; + m_pathWriter->readStream(m_interpreter->getPathStreamID(state), + concreteBranches); + auto f = openTestFile("path", id); + if (f) { + for (const auto &branch : concreteBranches) { + *f << branch << '\n'; + } + } } if (m_symPathWriter) { @@ -677,48 +663,14 @@ void KleeHandler::processTestCase(const ExecutionState &state, } } - if (WriteKPaths) { - std::string blockPath; - m_interpreter->getBlockPath(state, blockPath); - auto f = openTestFile("kpath", id); - if (f) - *f << blockPath; - } - - if (WriteCov) { - std::map> cov; - m_interpreter->getCoveredLines(state, cov); - auto f = openTestFile("cov", id); - if (f) { - for (const auto &entry : cov) { - for (const auto &line : entry.second) { - *f << entry.first << ':' << line << '\n'; - } - } - } - } - - if (WriteXMLTests) { - for (unsigned i = 0; i < ktest.uninitCoeff + 1; ++i) { - writeTestCaseXML(message != nullptr, ktest, id, i); - atLeastOneGenerated = true; - } - } - if (atLeastOneGenerated) { ++m_numGeneratedTests; } - for (unsigned i = 0; i < ktest.numObjects; i++) { - delete[] ktest.objects[i].bytes; - delete[] ktest.objects[i].pointers; - } - delete[] ktest.objects; - if (m_numGeneratedTests == MaxTests) m_interpreter->setHaltExecution(HaltExecution::MaxTests); - if (!WriteXMLTests && WriteTestInfo) { + if (WriteTestInfo) { time::Span elapsed_time(time::getWallTime() - start_time); auto f = openTestFile("info", id); if (f) @@ -726,6 +678,53 @@ void KleeHandler::processTestCase(const ExecutionState &state, } } // if (!WriteNone) + if (WriteKQueries) { + std::string constraints; + m_interpreter->getConstraintLog(state, constraints, Interpreter::KQUERY); + auto f = openTestFile("kquery", id); + if (f) + *f << constraints; + } + + if (WriteCVCs) { + // FIXME: If using Z3 as the core solver the emitted file is actually + // SMT-LIBv2 not CVC which is a bit confusing + std::string constraints; + m_interpreter->getConstraintLog(state, constraints, Interpreter::STP); + auto f = openTestFile("cvc", id); + if (f) + *f << constraints; + } + + if (WriteSMT2s) { + std::string constraints; + m_interpreter->getConstraintLog(state, constraints, Interpreter::SMTLIB2); + auto f = openTestFile("smt2", id); + if (f) + *f << constraints; + } + + if (WriteKPaths) { + std::string blockPath; + m_interpreter->getBlockPath(state, blockPath); + auto f = openTestFile("kpath", id); + if (f) + *f << blockPath; + } + + if (WriteCov) { + std::map> cov; + m_interpreter->getCoveredLines(state, cov); + auto f = openTestFile("cov", id); + if (f) { + for (const auto &entry : cov) { + for (const auto &line : entry.second) { + *f << entry.first << ':' << line << '\n'; + } + } + } + } + if (isError && OptExitOnError) { m_interpreter->prepareForEarlyExit(); klee_error("EXITING ON ERROR:\n%s\n", message);