Skip to content

Commit

Permalink
Add option to generate XML test cases
Browse files Browse the repository at this point in the history
  • Loading branch information
@misonijnik
misonijnik committed Jul 9, 2024
1 parent 6e2efd1 commit f6d4fef
Show file tree
Hide file tree
Showing 2 changed files with 208 additions and 35 deletions.
19 changes: 19 additions & 0 deletions test/Feature/WriteXML.c
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,19 @@
// RUN: %clang %s -emit-llvm -g -c -o %t2.bc
// RUN: rm -rf %t.klee-out
// RUN: %klee --output-dir=%t.klee-out --exit-on-error --write-xml-tests --xml-metadata-programfile=WriteXML.c --xml-metadata-programhash=0 %t2.bc
// RUN: test -f %t.klee-out/test000001.xml
// RUN: test -f %t.klee-out/test000002.xml

#include <assert.h>
#include <stdio.h>

int main() {
if (klee_range(0, 2, "range")) {
assert(__LINE__ == 16);
printf("__LINE__ = %d\n", __LINE__);
} else {
assert(__LINE__ == 19);
printf("__LINE__ = %d\n", __LINE__);
}
return 0;
}
224 changes: 189 additions & 35 deletions tools/klee/main.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -84,6 +84,11 @@ namespace {
cl::desc("Do not generate any test files (default=false)"),
cl::cat(TestCaseCat));

cl::opt<bool> WriteKTests(
"write-ktests", cl::init(true),
cl::desc("Write .ktest files for each test case (default=true)"),
cl::cat(TestCaseCat));

cl::opt<bool>
WriteCVCs("write-cvcs",
cl::desc("Write .cvc files for each test case (default=false)"),
Expand Down Expand Up @@ -286,6 +291,26 @@ namespace {
cl::desc("Link the llvm libc++ library into the bitcode (default=false)"),
cl::init(false),
cl::cat(LinkCat));

/*** Test-Comp specific options ***/

cl::OptionCategory
TestCompCat("Options specific to Test-Comp",
"These are options specific to the Test-Comp competition.");

cl::opt<bool> WriteXMLTests("write-xml-tests",
cl::desc("Write XML-formated tests"),
cl::init(false), cl::cat(TestCompCat));

cl::opt<std::string>
XMLMetadataProgramFile("xml-metadata-programfile",
cl::desc("Original file name for xml metadata"),
cl::cat(TestCompCat));

cl::opt<std::string> XMLMetadataProgramHash(
"xml-metadata-programhash",
llvm::cl::desc("Test-Comp hash sum of original file for xml metadata"),
llvm::cl::cat(TestCompCat));
}

namespace klee {
Expand Down Expand Up @@ -330,6 +355,15 @@ class KleeHandler : public InterpreterHandler {
void processTestCase(const ExecutionState &state,
const char *errorMessage,
const char *errorSuffix);
bool writeTestCaseKTest(
const std::vector<std::pair<std::string, std::vector<unsigned char>>>
&out,
unsigned id);
void writeTestCaseXML(
bool isError,
const std::vector<std::pair<std::string, std::vector<unsigned char>>>
&assignments,
unsigned id);

std::string getOutputFilename(const std::string &filename);
std::unique_ptr<llvm::raw_fd_ostream> openOutputFile(const std::string &filename);
Expand Down Expand Up @@ -477,53 +511,127 @@ KleeHandler::openTestFile(const std::string &suffix, unsigned id) {
return openOutputFile(getTestFilename(suffix, id));
}

bool KleeHandler::writeTestCaseKTest(
const std::vector<std::pair<std::string, std::vector<unsigned char>>> &out,
unsigned id) {
KTest b;
b.numArgs = m_argc;
b.args = m_argv;
b.symArgvs = 0;
b.symArgvLen = 0;
b.numObjects = out.size();
b.objects = new KTestObject[b.numObjects];
assert(b.objects);
for (unsigned i = 0; i < b.numObjects; i++) {
KTestObject *o = &b.objects[i];
o->name = const_cast<char *>(out[i].first.c_str());
o->numBytes = out[i].second.size();
o->bytes = new unsigned char[o->numBytes];
assert(o->bytes);
std::copy(out[i].second.begin(), out[i].second.end(), o->bytes);
}
bool status = true;
if (!kTest_toFile(&b,
getOutputFilename(getTestFilename("ktest", id)).c_str())) {
status = false;
klee_warning("unable to write output test case, losing it");
}
for (unsigned i = 0; i < b.numObjects; i++)
delete[] b.objects[i].bytes;
delete[] b.objects;
return status;
}

void KleeHandler::writeTestCaseXML(
bool isError,
const std::vector<std::pair<std::string, std::vector<unsigned char>>>
&assignments,
unsigned id) {

// TODO: This is super specific to test-comp and assumes that the name is the
// type information
auto file = openTestFile("xml", id);
if (!file)
return;

*file << "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n";
*file << "<!DOCTYPE testcase PUBLIC \"+//IDN sosy-lab.org//DTD test-format "
"testcase 1.0//EN\" "
"\"https://sosy-lab.org/test-format/testcase-1.0.dtd\">\n";
*file << "<testcase";
if (isError)
*file << " coversError=\"true\"";
*file << ">\n";
for (auto &item : assignments) {
*file << "\t<input variable=\"" << item.first << "\" ";
*file << "type =\"";
// print type of the input
*file << item.first;
*file << "\">";
// Ignore the type
auto type_size_bytes = item.second.size() * 8;
llvm::APInt v(type_size_bytes, 0, false);
for (auto i = item.second.rbegin(), e = item.second.rend(); i != e; ++i) {
v <<= 8;
v |= *i;
}
// print value

// Check if this is an unsigned type
if (item.first.find("u") == 0) {
v.print(*file, false);
} else if (item.first.rfind("*") != std::string::npos) {
// Pointer types
v.print(*file, false);
} else if (item.first.find("float") == 0) {
llvm::APFloat(APFloatBase::IEEEhalf(), v).print(*file);
} else if (item.first.find("double") == 0) {
llvm::APFloat(APFloatBase::IEEEdouble(), v).print(*file);
} else if (item.first.rfind("_t") != std::string::npos) {
// arbitrary type, e.g. sector_t
v.print(*file, false);
} else if (item.first.find("_") == 0) {
// _Bool
v.print(*file, false);
} else {
// the rest must be signed
v.print(*file, true);
}
*file << "</input>\n";
}
*file << "</testcase>\n";
}

/* Outputs all files (.ktest, .kquery, .cov etc.) describing a test case */
void KleeHandler::processTestCase(const ExecutionState &state,
const char *errorMessage,
const char *errorSuffix) {
unsigned test_id = ++m_numTotalTests;
if (!WriteNone) {
std::vector< std::pair<std::string, std::vector<unsigned char> > > out;
bool success = m_interpreter->getSymbolicSolution(state, out);
std::vector<std::pair<std::string, std::vector<unsigned char>>> assignments;
bool success = m_interpreter->getSymbolicSolution(state, assignments);

if (!success)
klee_warning("unable to get symbolic solution, losing test case");

const auto start_time = time::getWallTime();

unsigned id = ++m_numTotalTests;
bool atLeastOneGenerated = false;

if (success) {
KTest b;
b.numArgs = m_argc;
b.args = m_argv;
b.symArgvs = 0;
b.symArgvLen = 0;
b.numObjects = out.size();
b.objects = new KTestObject[b.numObjects];
assert(b.objects);
for (unsigned i=0; i<b.numObjects; i++) {
KTestObject *o = &b.objects[i];
o->name = const_cast<char*>(out[i].first.c_str());
o->numBytes = out[i].second.size();
o->bytes = new unsigned char[o->numBytes];
assert(o->bytes);
std::copy(out[i].second.begin(), out[i].second.end(), o->bytes);
if (WriteKTests) {
if (writeTestCaseKTest(assignments, test_id)) {
atLeastOneGenerated = true;
}
}

if (!kTest_toFile(&b, getOutputFilename(getTestFilename("ktest", id)).c_str())) {
klee_warning("unable to write output test case, losing it");
} else {
++m_numGeneratedTests;
if (WriteXMLTests) {
writeTestCaseXML(errorMessage != nullptr, assignments, test_id);
atLeastOneGenerated = true;
}

for (unsigned i=0; i<b.numObjects; i++)
delete[] b.objects[i].bytes;
delete[] b.objects;
}

if (errorMessage) {
auto f = openTestFile(errorSuffix, id);
auto f = openTestFile(errorSuffix, test_id);
if (f)
*f << errorMessage;
}
Expand All @@ -532,18 +640,22 @@ void KleeHandler::processTestCase(const ExecutionState &state,
std::vector<unsigned char> concreteBranches;
m_pathWriter->readStream(m_interpreter->getPathStreamID(state),
concreteBranches);
auto f = openTestFile("path", id);
auto f = openTestFile("path", test_id);
if (f) {
for (const auto &branch : concreteBranches) {
*f << branch << '\n';
}
}
}

if (atLeastOneGenerated) {
++m_numGeneratedTests;
}

if (errorMessage || WriteKQueries) {
std::string constraints;
m_interpreter->getConstraintLog(state, constraints,Interpreter::KQUERY);
auto f = openTestFile("kquery", id);
auto f = openTestFile("kquery", test_id);
if (f)
*f << constraints;
}
Expand All @@ -553,15 +665,15 @@ void KleeHandler::processTestCase(const ExecutionState &state,
// SMT-LIBv2 not CVC which is a bit confusing
std::string constraints;
m_interpreter->getConstraintLog(state, constraints, Interpreter::STP);
auto f = openTestFile("cvc", id);
auto f = openTestFile("cvc", test_id);
if (f)
*f << constraints;
}

if (WriteSMT2s) {
std::string constraints;
m_interpreter->getConstraintLog(state, constraints, Interpreter::SMTLIB2);
auto f = openTestFile("smt2", id);
auto f = openTestFile("smt2", test_id);
if (f)
*f << constraints;
}
Expand All @@ -570,7 +682,7 @@ void KleeHandler::processTestCase(const ExecutionState &state,
std::vector<unsigned char> symbolicBranches;
m_symPathWriter->readStream(m_interpreter->getSymbolicPathStreamID(state),
symbolicBranches);
auto f = openTestFile("sym.path", id);
auto f = openTestFile("sym.path", test_id);
if (f) {
for (const auto &branch : symbolicBranches) {
*f << branch << '\n';
Expand All @@ -581,7 +693,7 @@ void KleeHandler::processTestCase(const ExecutionState &state,
if (WriteCov) {
std::map<const std::string*, std::set<unsigned> > cov;
m_interpreter->getCoveredLines(state, cov);
auto f = openTestFile("cov", id);
auto f = openTestFile("cov", test_id);
if (f) {
for (const auto &entry : cov) {
for (const auto &line : entry.second) {
Expand All @@ -596,7 +708,7 @@ void KleeHandler::processTestCase(const ExecutionState &state,

if (WriteTestInfo) {
time::Span elapsed_time(time::getWallTime() - start_time);
auto f = openTestFile("info", id);
auto f = openTestFile("info", test_id);
if (f)
*f << "Time to generate test case: " << elapsed_time << '\n';
}
Expand Down Expand Up @@ -1422,6 +1534,48 @@ int main(int argc, char **argv, char **envp) {
}

auto startTime = std::time(nullptr);

if (WriteXMLTests) {
// Write metadata.xml
auto meta_file = handler->openOutputFile("metadata.xml");
if (!meta_file)
klee_error("Could not write metadata.xml");

*meta_file
<< "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n";
*meta_file
<< "<!DOCTYPE test-metadata PUBLIC \"+//IDN sosy-lab.org//DTD "
"test-format test-metadata 1.0//EN\" "
"\"https://sosy-lab.org/test-format/test-metadata-1.0.dtd\">\n";
*meta_file << "<test-metadata>\n";
*meta_file << "\t<sourcecodelang>C</sourcecodelang>\n";
*meta_file << "\t<producer>" << PACKAGE_STRING << "</producer>\n";

// Assume with early exit a bug finding mode and otherwise coverage
if (OptExitOnError)
*meta_file << "\t<specification>COVER( init(main()), FQL(COVER "
"EDGES(@CALL(__VERIFIER_error))) )</specification>\n";
else
*meta_file << "\t<specification>COVER( init(main()), FQL(COVER "
"EDGES(@DECISIONEDGE)) )</specification>\n";

// Assume the input file resembles the original source file; just exchange
// extension
*meta_file << "\t<programfile>" << XMLMetadataProgramFile
<< ".c</programfile>\n";
*meta_file << "\t<programhash>" << XMLMetadataProgramHash
<< "</programhash>\n";
*meta_file << "\t<entryfunction>" << mainFn->getName().str()
<< "</entryfunction>\n";
*meta_file << "\t<architecture>"
<< finalModule->getDataLayout().getPointerSizeInBits()
<< "bit</architecture>\n";
std::stringstream t;
t << std::put_time(std::localtime(&startTime), "%Y-%m-%dT%H:%M:%SZ");
*meta_file << "\t<creationtime>" << t.str() << "</creationtime>\n";
*meta_file << "</test-metadata>\n";
}

{ // output clock info and start time
std::stringstream startInfo;
startInfo << time::getClockInfo()
Expand Down

0 comments on commit f6d4fef

Please sign in to comment.