Commit 975fdba7 authored by Cristian Cadar's avatar Cristian Cadar Committed by Dan Liew
Browse files

Patch by Dan Liew: "Added SMTLIBLoggingSolver for logging queries in SMT-LIBv2 format."

git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@166564 91177308-0d34-0410-b5e6-96231b3b80d8

Conflicts:
	include/klee/Solver.h
parent 9aaaf2ce
......@@ -222,6 +222,10 @@ namespace klee {
/// involve FP comparisons.
Solver *createFPRewritingSolver(Solver *s);
/// createSMTLIBLoggingSolver - Create a solver which will forward all queries
/// after writing them to the given path in .smt2 format.
Solver *createSMTLIBLoggingSolver(Solver *s, std::string path);
/// createDummySolver - Create a dummy solver implementation which always
/// fails.
Solver *createDummySolver();
......
//===-- SMTLIBLoggingSolver.cpp -----------------------------------------------===//
//
// The KLEE Symbolic Virtual Machine
//
// This file is distributed under the University of Illinois Open Source
// License. See LICENSE.TXT for details.
//
//===----------------------------------------------------------------------===//
#include "klee/Solver.h"
#include "klee/Expr.h"
#include "klee/SolverImpl.h"
#include "klee/Statistics.h"
#include "klee/util/ExprSMTLIBLetPrinter.h"
#include "klee/Internal/Support/QueryLog.h"
#include "klee/Internal/System/Time.h"
#include "llvm/Support/CommandLine.h"
#include <fstream>
using namespace klee;
using namespace llvm;
using namespace klee::util;
///This SolverImpl will log queries to a file in the SMTLIBv2 format
///and pass the query down to the underlying solver.
///
///This is basically just a "copy" of PCLoggingSolver with a few modifications.
class SMTLIBLoggingSolver : public SolverImpl
{
Solver *solver;
std::ofstream os;
ExprSMTLIBPrinter* printer;
unsigned queryCount;
double startTime;
void startQuery(const Query& query, const char *typeName, const std::vector<const Array*>* objects=NULL)
{
Statistic *S = theStatisticManager->getStatisticByName("Instructions");
uint64_t instructions = S ? S->getValue() : 0;
os << ";SMTLIBv2 Query " << queryCount++ << " -- "
<< "Type: " << typeName << ", "
<< "Instructions: " << instructions << "\n";
printer->setQuery(query);
if(objects!=NULL)
printer->setArrayValuesToGet(*objects);
printer->generateOutput();
os << "\n";
startTime = getWallTime();
}
void finishQuery(bool success)
{
double delta = getWallTime() - startTime;
os << "; " << (success ? "OK" : "FAIL") << " -- "
<< "Elapsed: " << delta << "\n";
}
public:
SMTLIBLoggingSolver(Solver *_solver, std::string path)
: solver(_solver),
os(path.c_str(), std::ios::trunc),
printer(),
queryCount(0),
startTime(0)
{
//Setup the printer
printer = createSMTLIBPrinter();
printer->setOutput(os);
}
~SMTLIBLoggingSolver()
{
delete printer;
delete solver;
}
bool computeTruth(const Query& query, bool &isValid)
{
startQuery(query, "Truth");
bool success = solver->impl->computeTruth(query, isValid);
finishQuery(success);
if (success)
os << "; Is Valid: " << (isValid ? "true" : "false") << "\n";
os << "\n";
return success;
}
bool computeValidity(const Query& query, Solver::Validity &result)
{
startQuery(query, "Validity");
bool success = solver->impl->computeValidity(query, result);
finishQuery(success);
if (success)
os << "; Validity: " << result << "\n";
os << "\n";
return success;
}
bool computeValue(const Query& query, ref<Expr> &result)
{
startQuery(query.withFalse(), "Value");
bool success = solver->impl->computeValue(query, result);
finishQuery(success);
if (success)
os << "; Result: " << result << "\n";
os << "\n";
return success;
}
bool computeInitialValues(const Query& query,
const std::vector<const Array*> &objects,
std::vector< std::vector<unsigned char> > &values,
bool &hasSolution)
{
startQuery(query, "InitialValues", &objects);
bool success = solver->impl->computeInitialValues(query, objects,
values, hasSolution);
finishQuery(success);
if (success)
{
os << "; Solvable: " << (hasSolution ? "true" : "false") << "\n";
if (hasSolution)
{
std::vector< std::vector<unsigned char> >::iterator
values_it = values.begin();
for (std::vector<const Array*>::const_iterator i = objects.begin(),
e = objects.end(); i != e; ++i, ++values_it)
{
const Array *array = *i;
std::vector<unsigned char> &data = *values_it;
os << "; " << array->name << " = [";
for (unsigned j = 0; j < array->size; j++)
{
os << (int) data[j];
if (j+1 < array->size)
os << ",";
}
os << "]\n";
}
}
}
os << "\n";
return success;
}
};
Solver* klee::createSMTLIBLoggingSolver(Solver *_solver, std::string path)
{
return new Solver(new SMTLIBLoggingSolver(_solver, path));
}
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment