diff options
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/kleaver/Makefile | 11 | ||||
| -rw-r--r-- | tools/kleaver/main.cpp | 89 | ||||
| -rw-r--r-- | tools/klee/Makefile | 14 | ||||
| -rw-r--r-- | tools/klee/main.cpp | 205 |
4 files changed, 182 insertions, 137 deletions
diff --git a/tools/kleaver/Makefile b/tools/kleaver/Makefile index b6ccc91f..b93e361d 100644 --- a/tools/kleaver/Makefile +++ b/tools/kleaver/Makefile @@ -20,3 +20,14 @@ LINK_COMPONENTS = support include $(LEVEL)/Makefile.common LIBS += -lstp + +ifeq ($(ENABLE_METASMT),1) + include $(METASMT_ROOT)/share/metaSMT/metaSMT.makefile + LD.Flags += -L$(METASMT_ROOT)/../../deps/Z3-4.1/lib \ + -L$(METASMT_ROOT)/../../deps/boolector-1.5.118/lib \ + -L$(METASMT_ROOT)/../../deps/minisat-git/lib/ \ + -L$(METASMT_ROOT)/../../deps/boost-1_52_0/lib + CXX.Flags += -DBOOST_HAS_GCC_TR1 + CXX.Flags := $(filter-out -fno-exceptions,$(CXX.Flags)) + LIBS += -lrt -lgomp -lboost_iostreams -lboost_thread -lboost_system -lmetaSMT -lz3 -lboolector -lminisat_core +endif \ No newline at end of file diff --git a/tools/kleaver/main.cpp b/tools/kleaver/main.cpp index accc48e4..abc37d4b 100644 --- a/tools/kleaver/main.cpp +++ b/tools/kleaver/main.cpp @@ -34,17 +34,35 @@ #undef PACKAGE_TARNAME #undef PACKAGE_VERSION -#if LLVM_VERSION_CODE < LLVM_VERSION(2, 9) -#include "llvm/System/Signals.h" -#else #include "llvm/Support/Signals.h" #include "llvm/Support/system_error.h" -#endif using namespace llvm; using namespace klee; using namespace klee::expr; +#ifdef SUPPORT_METASMT + +#include <metaSMT/DirectSolver_Context.hpp> +#include <metaSMT/backend/Z3_Backend.hpp> +#include <metaSMT/backend/Boolector.hpp> + +#define Expr VCExpr +#define Type VCType +#define STP STP_Backend +#include <metaSMT/backend/STP.hpp> +#undef Expr +#undef Type +#undef STP + +using namespace metaSMT; +using namespace metaSMT::solver; + +#endif /* SUPPORT_METASMT */ + + + + namespace { llvm::cl::opt<std::string> InputFile(llvm::cl::desc("<input query log>"), llvm::cl::Positional, @@ -211,7 +229,39 @@ static bool EvaluateInputAST(const char *Filename, return false; // FIXME: Support choice of solver. - Solver *coreSolver = UseDummySolver ? createDummySolver() : new STPSolver(UseForkedCoreSolver); + Solver *coreSolver = NULL; // + +#ifdef SUPPORT_METASMT + if (UseMetaSMT != METASMT_BACKEND_NONE) { + + std::string backend; + + switch (UseMetaSMT) { + case METASMT_BACKEND_STP: + backend = "STP"; + coreSolver = new MetaSMTSolver< DirectSolver_Context < STP_Backend > >(UseForkedCoreSolver, CoreSolverOptimizeDivides); + break; + case METASMT_BACKEND_Z3: + backend = "Z3"; + coreSolver = new MetaSMTSolver< DirectSolver_Context < Z3_Backend > >(UseForkedCoreSolver, CoreSolverOptimizeDivides); + break; + case METASMT_BACKEND_BOOLECTOR: + backend = "Boolector"; + coreSolver = new MetaSMTSolver< DirectSolver_Context < Boolector > >(UseForkedCoreSolver, CoreSolverOptimizeDivides); + break; + default: + assert(false); + break; + }; + std::cerr << "Starting MetaSMTSolver(" << backend << ") ...\n"; + } + else { + coreSolver = UseDummySolver ? createDummySolver() : new STPSolver(UseForkedCoreSolver); + } +#else + coreSolver = UseDummySolver ? createDummySolver() : new STPSolver(UseForkedCoreSolver); +#endif /* SUPPORT_METASMT */ + if (!UseDummySolver) { if (0 != MaxCoreSolverTime) { @@ -405,20 +455,12 @@ int main(int argc, char **argv) { std::string ErrorStr; -#if LLVM_VERSION_CODE < LLVM_VERSION(2, 9) - MemoryBuffer *MB = MemoryBuffer::getFileOrSTDIN(InputFile.c_str(), &ErrorStr); - if (!MB) { - std::cerr << argv[0] << ": error: " << ErrorStr << "\n"; - return 1; - } -#else OwningPtr<MemoryBuffer> MB; error_code ec=MemoryBuffer::getFileOrSTDIN(InputFile.c_str(), MB); if (ec) { std::cerr << argv[0] << ": error: " << ec.message() << "\n"; return 1; } -#endif ExprBuilder *Builder = 0; switch (BuilderKind) { @@ -438,45 +480,24 @@ int main(int argc, char **argv) { switch (ToolAction) { case PrintTokens: -#if LLVM_VERSION_CODE < LLVM_VERSION(2, 9) - PrintInputTokens(MB); -#else PrintInputTokens(MB.get()); -#endif break; case PrintAST: -#if LLVM_VERSION_CODE < LLVM_VERSION(2, 9) - success = PrintInputAST(InputFile=="-" ? "<stdin>" : InputFile.c_str(), MB, - Builder); -#else success = PrintInputAST(InputFile=="-" ? "<stdin>" : InputFile.c_str(), MB.get(), Builder); -#endif break; case Evaluate: -#if LLVM_VERSION_CODE < LLVM_VERSION(2, 9) - success = EvaluateInputAST(InputFile=="-" ? "<stdin>" : InputFile.c_str(), - MB, Builder); -#else success = EvaluateInputAST(InputFile=="-" ? "<stdin>" : InputFile.c_str(), MB.get(), Builder); -#endif break; case PrintSMTLIBv2: -#if LLVM_VERSION_CODE < LLVM_VERSION(2, 9) - success = printInputAsSMTLIBv2(InputFile=="-"? "<stdin>" : InputFile.c_str(), MB,Builder); -#else success = printInputAsSMTLIBv2(InputFile=="-"? "<stdin>" : InputFile.c_str(), MB.get(),Builder); -#endif break; default: std::cerr << argv[0] << ": error: Unknown program action!\n"; } delete Builder; -#if LLVM_VERSION_CODE < LLVM_VERSION(2, 9) - delete MB; -#endif llvm::llvm_shutdown(); return success ? 0 : 1; } diff --git a/tools/klee/Makefile b/tools/klee/Makefile index 01486fef..f050bf74 100644 --- a/tools/klee/Makefile +++ b/tools/klee/Makefile @@ -15,6 +15,20 @@ include $(LEVEL)/Makefile.config USEDLIBS = kleeCore.a kleeBasic.a kleeModule.a kleaverSolver.a kleaverExpr.a kleeSupport.a LINK_COMPONENTS = jit bitreader bitwriter ipo linker engine +ifeq ($(shell echo "$(LLVM_VERSION_MAJOR).$(LLVM_VERSION_MINOR) >= 3.3" | bc), 1) +LINK_COMPONENTS += irreader +endif include $(LEVEL)/Makefile.common LIBS += -lstp + +ifeq ($(ENABLE_METASMT),1) + include $(METASMT_ROOT)/share/metaSMT/metaSMT.makefile + LD.Flags += -L$(METASMT_ROOT)/../../deps/Z3-4.1/lib \ + -L$(METASMT_ROOT)/../../deps/boolector-1.5.118/lib \ + -L$(METASMT_ROOT)/../../deps/minisat-git/lib/ \ + -L$(METASMT_ROOT)/../../deps/boost-1_52_0/lib + CXX.Flags += -DBOOST_HAS_GCC_TR1 + CXX.Flags := $(filter-out -fno-exceptions,$(CXX.Flags)) + LIBS += -lrt -lgomp -lboost_iostreams -lboost_thread -lboost_system -lmetaSMT -lz3 -lboolector -lminisat_core +endif \ No newline at end of file diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp index 92e4df67..3616bfa6 100644 --- a/tools/klee/main.cpp +++ b/tools/klee/main.cpp @@ -13,18 +13,25 @@ #include "klee/Internal/Support/ModuleUtil.h" #include "klee/Internal/System/Time.h" +#if LLVM_VERSION_CODE > LLVM_VERSION(3, 2) +#include "llvm/IR/Constants.h" +#include "llvm/IR/Module.h" +#include "llvm/IR/Type.h" +#include "llvm/IR/InstrTypes.h" +#include "llvm/IR/Instruction.h" +#include "llvm/IR/Instructions.h" +#include "llvm/IR/LLVMContext.h" +#else #include "llvm/Constants.h" #include "llvm/Module.h" -#if LLVM_VERSION_CODE < LLVM_VERSION(2, 7) -#include "llvm/ModuleProvider.h" -#endif #include "llvm/Type.h" #include "llvm/InstrTypes.h" #include "llvm/Instruction.h" #include "llvm/Instructions.h" -#if LLVM_VERSION_CODE >= LLVM_VERSION(2, 7) #include "llvm/LLVMContext.h" +#include "llvm/Support/FileSystem.h" #endif +#include "llvm/Support/FileSystem.h" #include "llvm/Bitcode/ReaderWriter.h" #include "llvm/Support/CommandLine.h" #include "llvm/Support/ManagedStatic.h" @@ -41,27 +48,23 @@ #else #include "llvm/Support/TargetSelect.h" #endif -#if LLVM_VERSION_CODE < LLVM_VERSION(2, 9) -#include "llvm/System/Signals.h" -#else #include "llvm/Support/Signals.h" #include "llvm/Support/system_error.h" -#endif -#include <iostream> -#include <fstream> -#include <cerrno> + #include <dirent.h> +#include <signal.h> #include <unistd.h> -#include <errno.h> #include <sys/stat.h> #include <sys/wait.h> -#include <signal.h> +#include <cerrno> +#include <fstream> +#include <iomanip> #include <iostream> #include <iterator> -#include <fstream> #include <sstream> + using namespace llvm; using namespace klee; @@ -148,7 +151,12 @@ namespace { CheckDivZero("check-div-zero", cl::desc("Inject checks for division-by-zero"), cl::init(true)); - + + cl::opt<bool> + CheckOvershift("check-overshift", + cl::desc("Inject checks for overshift"), + cl::init(true)); + cl::opt<std::string> OutputDir("output-dir", cl::desc("Directory to write results in (defaults to klee-out-N)"), @@ -211,7 +219,7 @@ private: TreeStreamWriter *m_pathWriter, *m_symPathWriter; std::ostream *m_infoFile; - char m_outputDirectory[1024]; + sys::Path m_outputDirectory; unsigned m_testIndex; // number of tests written so far unsigned m_pathsExplored; // number of paths explored so far @@ -256,79 +264,86 @@ KleeHandler::KleeHandler(int argc, char **argv) m_pathWriter(0), m_symPathWriter(0), m_infoFile(0), + m_outputDirectory(), m_testIndex(0), m_pathsExplored(0), m_argc(argc), m_argv(argv) { - std::string theDir; if (OutputDir=="") { llvm::sys::Path directory(InputFile); - std::string dirname = ""; + std::stringstream dirname; directory.eraseComponent(); if (directory.isEmpty()) directory.set("."); - for (int i = 0; ; i++) { - char buf[256], tmp[64]; - sprintf(tmp, "klee-out-%d", i); - dirname = tmp; - sprintf(buf, "%s/%s", directory.c_str(), tmp); - theDir = buf; + for (int i = 0; i< INT_MAX ; i++) { + dirname << "klee-out-"; + dirname << i; + + m_outputDirectory = llvm::sys::Path(directory); // Copy + if (!m_outputDirectory.appendComponent(dirname.str())) + klee_error("Failed to append \"%s\" to \"%s\"", dirname.str().c_str(), directory.c_str()); - if (DIR *dir = opendir(theDir.c_str())) { - closedir(dir); - } else { - break; + bool isDir = true; + llvm::error_code e = llvm::sys::fs::exists(m_outputDirectory.str(), isDir); + if ( e != llvm::errc::success ) + klee_error("Failed to check if \"%s\" exists.", m_outputDirectory.str().c_str()); + + if (!isDir) + { + break; // Found an available directory name } + + // Warn the user if the klee-out-* exists but is not a directory + e = llvm::sys::fs::is_directory(m_outputDirectory.str(), isDir); + if ( e == llvm::errc::success && !isDir ) + klee_warning("A file \"%s\" exists, but it is not a directory", + m_outputDirectory.str().c_str()); + + dirname.str(""); // Clear + m_outputDirectory.clear(); } - std::cerr << "KLEE: output directory = \"" << dirname << "\"\n"; + if (m_outputDirectory.empty()) + klee_error("Failed to find available output directory in %s", dirname.str().c_str()); + + std::cerr << "KLEE: output directory = \"" << dirname.str() << "\"\n"; llvm::sys::Path klee_last(directory); - klee_last.appendComponent("klee-last"); - - if ((unlink(klee_last.c_str()) < 0) && (errno != ENOENT)) { - perror("Cannot unlink klee-last"); - assert(0 && "exiting."); - } + if(!klee_last.appendComponent("klee-last")) + klee_error("cannot create path name for klee-last"); + + if ((unlink(klee_last.c_str()) < 0) && (errno != ENOENT)) + klee_error("cannot unlink klee-last: %s", strerror(errno)); - if (symlink(dirname.c_str(), klee_last.c_str()) < 0) { - perror("Cannot make symlink"); - assert(0 && "exiting."); - } + if (symlink(dirname.str().c_str(), klee_last.c_str()) < 0) + klee_error("cannot create klee-last symlink: %s", strerror(errno)); + } else { - theDir = OutputDir; + if (!m_outputDirectory.set(OutputDir)) + klee_error("cannot use klee output directory: %s", OutputDir.c_str()); } - sys::Path p(theDir); -#if LLVM_VERSION_CODE < LLVM_VERSION(3, 1) - if (!p.isAbsolute()) { -#else - if (!sys::path::is_absolute(p.c_str())) { -#endif + if (!sys::path::is_absolute(m_outputDirectory.c_str())) { sys::Path cwd = sys::Path::GetCurrentDirectory(); - cwd.appendComponent(theDir); - p = cwd; - } - strcpy(m_outputDirectory, p.c_str()); + if(!cwd.appendComponent( m_outputDirectory.c_str())) + klee_error("cannot create absolute path name for output directory"); - if (mkdir(m_outputDirectory, 0775) < 0) { - std::cerr << "KLEE: ERROR: Unable to make output directory: \"" - << m_outputDirectory - << "\", refusing to overwrite.\n"; - exit(1); + m_outputDirectory = cwd; } - char fname[1024]; - snprintf(fname, sizeof(fname), "%s/warnings.txt", m_outputDirectory); - klee_warning_file = fopen(fname, "w"); - assert(klee_warning_file); + if (mkdir(m_outputDirectory.c_str(), 0775) < 0) + klee_error("cannot create directory \"%s\": %s", m_outputDirectory.c_str(), strerror(errno)); + + std::string file_path = getOutputFilename("warnings.txt"); + if ((klee_warning_file = fopen(file_path.c_str(), "w")) == NULL) + klee_error("cannot open file \"%s\": %s", file_path.c_str(), strerror(errno)); - snprintf(fname, sizeof(fname), "%s/messages.txt", m_outputDirectory); - klee_message_file = fopen(fname, "w"); - assert(klee_message_file); + file_path = getOutputFilename("messages.txt"); + if ((klee_message_file = fopen(file_path.c_str(), "w")) == NULL) + klee_error("cannot open file \"%s\": %s", file_path.c_str(), strerror(errno)); m_infoFile = openOutputFile("info"); } @@ -336,6 +351,8 @@ KleeHandler::KleeHandler(int argc, char **argv) KleeHandler::~KleeHandler() { if (m_pathWriter) delete m_pathWriter; if (m_symPathWriter) delete m_symPathWriter; + fclose(klee_warning_file); + fclose(klee_message_file); delete m_infoFile; } @@ -356,9 +373,12 @@ void KleeHandler::setInterpreter(Interpreter *i) { } std::string KleeHandler::getOutputFilename(const std::string &filename) { - char outfile[1024]; - sprintf(outfile, "%s/%s", m_outputDirectory, filename.c_str()); - return outfile; + sys::Path path(m_outputDirectory); + if(!path.appendComponent(filename)) { + klee_error("cannot create path name for \"%s\"", filename.c_str()); + } + + return path.str(); } std::ostream *KleeHandler::openOutputFile(const std::string &filename) { @@ -379,15 +399,13 @@ std::ostream *KleeHandler::openOutputFile(const std::string &filename) { } std::string KleeHandler::getTestFilename(const std::string &suffix, unsigned id) { - char filename[1024]; - sprintf(filename, "test%06d.%s", id, suffix.c_str()); - return getOutputFilename(filename); + std::stringstream filename; + filename << "test" << std::setfill('0') << std::setw(6) << id << '.' << suffix; + return filename.str(); } std::ostream *KleeHandler::openTestFile(const std::string &suffix, unsigned id) { - char filename[1024]; - sprintf(filename, "test%06d.%s", id, suffix.c_str()); - return openOutputFile(filename); + return openOutputFile(getTestFilename(suffix, id)); } @@ -429,7 +447,7 @@ void KleeHandler::processTestCase(const ExecutionState &state, std::copy(out[i].second.begin(), out[i].second.end(), o->bytes); } - if (!kTest_toFile(&b, getTestFilename("ktest", id).c_str())) { + if (!kTest_toFile(&b, getOutputFilename(getTestFilename("ktest", id)).c_str())) { klee_warning("unable to write output test case, losing it"); } @@ -544,11 +562,7 @@ void KleeHandler::getOutFiles(std::string path, } for (std::set<llvm::sys::Path>::iterator it = contents.begin(), ie = contents.end(); it != ie; ++it) { -#if LLVM_VERSION_CODE != LLVM_VERSION(2, 6) std::string f = it->str(); -#else - std::string f = it->toString(); -#endif if (f.substr(f.size()-6,f.size()) == ".ktest") { results.push_back(f); } @@ -723,7 +737,6 @@ static const char *modelledExternals[] = { "klee_warning_once", "klee_alias_function", "klee_stack_trace", - "llvm.dbg.stoppoint", #if LLVM_VERSION_CODE >= LLVM_VERSION(3, 1) "llvm.dbg.declare", "llvm.dbg.value", @@ -989,6 +1002,12 @@ static void replaceOrRenameFunction(llvm::Module *module, } static llvm::Module *linkWithUclibc(llvm::Module *mainModule) { + // Ensure that KLEE_UCLIBC exists + bool uclibcRootExists=false; + llvm::sys::fs::is_directory(KLEE_UCLIBC, uclibcRootExists); + if (!uclibcRootExists) + klee_error("Cannot link with uclibc. KLEE_UCLIBC (\"" KLEE_UCLIBC "\") is not a directory."); + Function *f; // force import of __uClibc_main mainModule->getOrInsertFunction("__uClibc_main", @@ -1183,28 +1202,7 @@ int main(int argc, char **argv, char **envp) { // Load the bytecode... std::string ErrorMsg; -#if LLVM_VERSION_CODE < LLVM_VERSION(2, 7) - ModuleProvider *MP = 0; - if (MemoryBuffer *Buffer = MemoryBuffer::getFileOrSTDIN(InputFile, &ErrorMsg)) { - MP = getBitcodeModuleProvider(Buffer, getGlobalContext(), &ErrorMsg); - if (!MP) delete Buffer; - } - - if (!MP) - klee_error("error loading program '%s': %s", InputFile.c_str(), ErrorMsg.c_str()); - - Module *mainModule = MP->materializeModule(); - MP->releaseModule(); - delete MP; -#else Module *mainModule = 0; -#if LLVM_VERSION_CODE < LLVM_VERSION(2, 9) - MemoryBuffer *Buffer = MemoryBuffer::getFileOrSTDIN(InputFile, &ErrorMsg); - if (Buffer) { - mainModule = getLazyBitcodeModule(Buffer, getGlobalContext(), &ErrorMsg); - if (!mainModule) delete Buffer; - } -#else OwningPtr<MemoryBuffer> BufferPtr; error_code ec=MemoryBuffer::getFileOrSTDIN(InputFile.c_str(), BufferPtr); if (ec) { @@ -1213,7 +1211,6 @@ int main(int argc, char **argv, char **envp) { } mainModule = getLazyBitcodeModule(BufferPtr.get(), getGlobalContext(), &ErrorMsg); -#endif if (mainModule) { if (mainModule->MaterializeAllPermanently(&ErrorMsg)) { delete mainModule; @@ -1223,7 +1220,6 @@ int main(int argc, char **argv, char **envp) { if (!mainModule) klee_error("error loading program '%s': %s", InputFile.c_str(), ErrorMsg.c_str()); -#endif if (WithPOSIXRuntime) { int r = initEnv(mainModule); @@ -1241,7 +1237,8 @@ int main(int argc, char **argv, char **envp) { #endif Interpreter::ModuleOptions Opts(LibraryDir.c_str(), /*Optimize=*/OptimizeModule, - /*CheckDivZero=*/CheckDivZero); + /*CheckDivZero=*/CheckDivZero, + /*CheckOvershift=*/CheckOvershift); switch (Libc) { case NoLibc: /* silence compiler warning */ @@ -1250,7 +1247,11 @@ int main(int argc, char **argv, char **envp) { case KleeLibc: { // FIXME: Find a reasonable solution for this. llvm::sys::Path Path(Opts.LibraryDir); +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3) + Path.appendComponent("klee-libc.bc"); +#else Path.appendComponent("libklee-libc.bca"); +#endif mainModule = klee::linkWithLibrary(mainModule, Path.c_str()); assert(mainModule && "unable to link with klee-libc"); break; @@ -1502,9 +1503,7 @@ int main(int argc, char **argv, char **envp) { std::cerr << stats.str(); handler->getInfoStream() << stats.str(); -#if LLVM_VERSION_CODE >= LLVM_VERSION(2, 9) BufferPtr.take(); -#endif delete handler; return 0; |