diff options
Diffstat (limited to 'lib')
31 files changed, 1006 insertions, 256 deletions
diff --git a/lib/Basic/CmdLineOptions.cpp b/lib/Basic/CmdLineOptions.cpp index e55c4550..82cb01b2 100644 --- a/lib/Basic/CmdLineOptions.cpp +++ b/lib/Basic/CmdLineOptions.cpp @@ -82,6 +82,10 @@ llvm::cl::list<QueryLoggingSolverType> queryLoggingOptions( llvm::cl::CommaSeparated ); +llvm::cl::opt<bool> + UseAssignmentValidatingSolver("debug-assignment-validating-solver", + llvm::cl::init(false)); + #ifdef ENABLE_METASMT #ifdef METASMT_DEFAULT_BACKEND_IS_BTOR diff --git a/lib/Basic/ConstructSolverChain.cpp b/lib/Basic/ConstructSolverChain.cpp index 68e1b08b..d00fcec1 100644 --- a/lib/Basic/ConstructSolverChain.cpp +++ b/lib/Basic/ConstructSolverChain.cpp @@ -37,6 +37,9 @@ Solver *constructSolverChain(Solver *coreSolver, baseSolverQuerySMT2LogPath.c_str()); } + if (UseAssignmentValidatingSolver) + solver = createAssignmentValidatingSolver(solver); + if (UseFastCexSolver) solver = createFastCexSolver(solver); diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index 8a445aa3..5af31125 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -81,6 +81,7 @@ #include "llvm/ADT/StringExtras.h" #include "llvm/Support/CommandLine.h" #include "llvm/Support/ErrorHandling.h" +#include "llvm/Support/FileSystem.h" #include "llvm/Support/Process.h" #include "llvm/Support/raw_ostream.h" @@ -383,7 +384,13 @@ Executor::Executor(LLVMContext &ctx, const InterpreterOptions &opts, if (!DebugCompressInstructions) { #endif -#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 5) +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 6) + std::error_code ec; + debugInstFile = new llvm::raw_fd_ostream(debug_file_name.c_str(), ec, + llvm::sys::fs::OpenFlags::F_Text); + if (ec) + ErrorInfo = ec.message(); +#elif LLVM_VERSION_CODE >= LLVM_VERSION(3, 5) debugInstFile = new llvm::raw_fd_ostream(debug_file_name.c_str(), ErrorInfo, llvm::sys::fs::OpenFlags::F_Text); #else @@ -976,14 +983,18 @@ Executor::fork(ExecutionState ¤t, ref<Expr> condition, bool isInternal) { falseState->ptreeNode = res.first; trueState->ptreeNode = res.second; - if (!isInternal) { - if (pathWriter) { - falseState->pathOS = pathWriter->open(current.pathOS); + if (pathWriter) { + // Need to update the pathOS.id field of falseState, otherwise the same id + // is used for both falseState and trueState. + falseState->pathOS = pathWriter->open(current.pathOS); + if (!isInternal) { trueState->pathOS << "1"; falseState->pathOS << "0"; - } - if (symPathWriter) { - falseState->symPathOS = symPathWriter->open(current.symPathOS); + } + } + if (symPathWriter) { + falseState->symPathOS = symPathWriter->open(current.symPathOS); + if (!isInternal) { trueState->symPathOS << "1"; falseState->symPathOS << "0"; } @@ -1235,8 +1246,11 @@ void Executor::printDebugInstructions(ExecutionState &state) { stream = &debugLogBuffer; if (!optionIsSet(DebugPrintInstructions, STDERR_COMPACT) && - !optionIsSet(DebugPrintInstructions, FILE_COMPACT)) - printFileLine(state, state.pc, *stream); + !optionIsSet(DebugPrintInstructions, FILE_COMPACT)) { + (*stream) << " "; + state.pc->printFileLine(*stream); + (*stream) << ":"; + } (*stream) << state.pc->info->id; @@ -1461,15 +1475,6 @@ void Executor::transferToBasicBlock(BasicBlock *dst, BasicBlock *src, } } -void Executor::printFileLine(ExecutionState &state, KInstruction *ki, - llvm::raw_ostream &debugFile) { - const InstructionInfo &ii = *ki->info; - if (ii.file != "") - debugFile << " " << ii.file << ":" << ii.line << ":"; - else - debugFile << " [no debug info]:"; -} - /// Compute the true target of a function call, resolving LLVM and KLEE aliases /// and bitcasts. Function* Executor::getTargetFunction(Value *calledVal, ExecutionState &state) { @@ -1481,9 +1486,13 @@ Function* Executor::getTargetFunction(Value *calledVal, ExecutionState &state) { while (true) { if (GlobalValue *gv = dyn_cast<GlobalValue>(c)) { +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 6) + if (!Visited.insert(gv).second) + return 0; +#else if (!Visited.insert(gv)) return 0; - +#endif std::string alias = state.getFnAlias(gv->getName()); if (alias != "") { llvm::Module* currModule = kmodule->module; @@ -3082,7 +3091,6 @@ void Executor::callExternalFunction(ExecutionState &state, else klee_warning_once(function, "%s", os.str().c_str()); } - bool success = externalDispatcher->executeCall(function, target->inst, args); if (!success) { terminateStateOnError(state, "failed external call: " + function->getName(), @@ -3837,6 +3845,13 @@ size_t Executor::getAllocationAlignment(const llvm::Value *allocSite) const { "Returned alignment must be a power of two"); return alignment; } + +void Executor::prepareForEarlyExit() { + if (statsTracker) { + // Make sure stats get flushed out + statsTracker->done(); + } +} /// Interpreter *Interpreter::create(LLVMContext &ctx, const InterpreterOptions &opts, diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h index 7c18ae1f..c3f6e705 100644 --- a/lib/Core/Executor.h +++ b/lib/Core/Executor.h @@ -487,6 +487,8 @@ public: inhibitForking = value; } + void prepareForEarlyExit(); + /*** State accessor methods ***/ virtual unsigned getPathStreamID(const ExecutionState &state); diff --git a/lib/Core/ExternalDispatcher.cpp b/lib/Core/ExternalDispatcher.cpp index 01c5f935..df0dd9a9 100644 --- a/lib/Core/ExternalDispatcher.cpp +++ b/lib/Core/ExternalDispatcher.cpp @@ -11,19 +11,24 @@ #include "klee/Config/Version.h" #if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3) -#include "llvm/IR/Module.h" #include "llvm/IR/Constants.h" #include "llvm/IR/DerivedTypes.h" #include "llvm/IR/Instructions.h" #include "llvm/IR/LLVMContext.h" +#include "llvm/IR/Module.h" #else -#include "llvm/Module.h" #include "llvm/Constants.h" #include "llvm/DerivedTypes.h" #include "llvm/Instructions.h" #include "llvm/LLVMContext.h" +#include "llvm/Module.h" #endif +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 6) +#include "llvm/ExecutionEngine/MCJIT.h" +#else #include "llvm/ExecutionEngine/JIT.h" +#endif + #include "llvm/ExecutionEngine/GenericValue.h" #include "llvm/Support/DynamicLibrary.h" #include "llvm/Support/raw_ostream.h" @@ -55,12 +60,48 @@ extern "C" { static void sigsegv_handler(int signal, siginfo_t *info, void *context) { longjmp(escapeCallJmpBuf, 1); } +} +namespace klee { + +class ExternalDispatcherImpl { +private: + typedef std::map<const llvm::Instruction *, llvm::Function *> dispatchers_ty; + dispatchers_ty dispatchers; + llvm::Function *createDispatcher(llvm::Function *f, llvm::Instruction *i, + llvm::Module *module); + llvm::ExecutionEngine *executionEngine; + LLVMContext &ctx; + std::map<std::string, void *> preboundFunctions; + bool runProtectedCall(llvm::Function *f, uint64_t *args); + llvm::Module *singleDispatchModule; + std::vector<std::string> moduleIDs; + std::string &getFreshModuleID(); + +public: + ExternalDispatcherImpl(llvm::LLVMContext &ctx); + ~ExternalDispatcherImpl(); + bool executeCall(llvm::Function *function, llvm::Instruction *i, + uint64_t *args); + void *resolveSymbol(const std::string &name); +}; + +std::string &ExternalDispatcherImpl::getFreshModuleID() { + // We store the module IDs because `llvm::Module` constructor takes the + // module ID as a StringRef so it doesn't own the ID. Therefore we need to + // own the ID. + static uint64_t counter = 0; + std::string underlyingString; + llvm::raw_string_ostream ss(underlyingString); + ss << "ExternalDispatcherModule_" << counter; + moduleIDs.push_back(ss.str()); // moduleIDs now has a copy + ++counter; // Increment for next call + return moduleIDs.back(); } -void *ExternalDispatcher::resolveSymbol(const std::string &name) { +void *ExternalDispatcherImpl::resolveSymbol(const std::string &name) { assert(executionEngine); - + const char *str = name.c_str(); // We use this to validate that function names can be resolved so we @@ -74,10 +115,10 @@ void *ExternalDispatcher::resolveSymbol(const std::string &name) { void *addr = sys::DynamicLibrary::SearchForAddressOfSymbol(str); if (addr) return addr; - + // If it has an asm specifier and starts with an underscore we retry // without the underscore. I (DWD) don't know why. - if (name[0] == 1 && str[0]=='_') { + if (name[0] == 1 && str[0] == '_') { ++str; addr = sys::DynamicLibrary::SearchForAddressOfSymbol(str); } @@ -85,11 +126,24 @@ void *ExternalDispatcher::resolveSymbol(const std::string &name) { return addr; } -ExternalDispatcher::ExternalDispatcher(LLVMContext &ctx) { - dispatchModule = new Module("ExternalDispatcher", ctx); - +ExternalDispatcherImpl::ExternalDispatcherImpl(LLVMContext &ctx) : ctx(ctx) { std::string error; - executionEngine = ExecutionEngine::createJIT(dispatchModule, &error); + singleDispatchModule = new Module(getFreshModuleID(), ctx); +#if LLVM_VERSION_CODE < LLVM_VERSION(3, 6) + // Use old JIT + executionEngine = ExecutionEngine::createJIT(singleDispatchModule, &error); +#else + // Use MCJIT. + // The MCJIT JITs whole modules at a time rather than individual functions + // so we will let it manage the modules. + // Note that we don't do anything with `singleDispatchModule`. This is just + // so we can use the EngineBuilder API. + auto dispatchModuleUniq = std::unique_ptr<Module>(singleDispatchModule); + executionEngine = EngineBuilder(std::move(dispatchModuleUniq)) + .setEngineKind(EngineKind::JIT) + .create(); +#endif + if (!executionEngine) { llvm::errs() << "unable to make jit: " << error << "\n"; abort(); @@ -98,6 +152,10 @@ ExternalDispatcher::ExternalDispatcher(LLVMContext &ctx) { // If we have a native target, initialize it to ensure it is linked in and // usable by the JIT. llvm::InitializeNativeTarget(); +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 6) + llvm::InitializeNativeTargetAsmParser(); + llvm::InitializeNativeTargetAsmPrinter(); +#endif // from ExecutionEngine::create if (executionEngine) { @@ -107,61 +165,90 @@ ExternalDispatcher::ExternalDispatcher(LLVMContext &ctx) { } #ifdef WINDOWS - preboundFunctions["getpid"] = (void*) (long) getpid; - preboundFunctions["putchar"] = (void*) (long) putchar; - preboundFunctions["printf"] = (void*) (long) printf; - preboundFunctions["fprintf"] = (void*) (long) fprintf; - preboundFunctions["sprintf"] = (void*) (long) sprintf; + preboundFunctions["getpid"] = (void *)(long)getpid; + preboundFunctions["putchar"] = (void *)(long)putchar; + preboundFunctions["printf"] = (void *)(long)printf; + preboundFunctions["fprintf"] = (void *)(long)fprintf; + preboundFunctions["sprintf"] = (void *)(long)sprintf; #endif } -ExternalDispatcher::~ExternalDispatcher() { +ExternalDispatcherImpl::~ExternalDispatcherImpl() { delete executionEngine; + // NOTE: the `executionEngine` owns all modules so + // we don't need to delete any of them. } -bool ExternalDispatcher::executeCall(Function *f, Instruction *i, uint64_t *args) { +bool ExternalDispatcherImpl::executeCall(Function *f, Instruction *i, + uint64_t *args) { dispatchers_ty::iterator it = dispatchers.find(i); - Function *dispatcher; + if (it != dispatchers.end()) { + // Code already JIT'ed for this + return runProtectedCall(it->second, args); + } - if (it == dispatchers.end()) { + // Code for this not JIT'ed. Do this now. + Function *dispatcher; #ifdef WINDOWS - std::map<std::string, void*>::iterator it2 = - preboundFunctions.find(f->getName())); - - if (it2 != preboundFunctions.end()) { - // only bind once - if (it2->second) { - executionEngine->addGlobalMapping(f, it2->second); - it2->second = 0; - } + std::map<std::string, void *>::iterator it2 = + preboundFunctions.find(f->getName()); + + if (it2 != preboundFunctions.end()) { + // only bind once + if (it2->second) { + executionEngine->addGlobalMapping(f, it2->second); + it2->second = 0; } + } #endif - dispatcher = createDispatcher(f,i); - - dispatchers.insert(std::make_pair(i, dispatcher)); - - if (dispatcher) { - // Force the JIT execution engine to go ahead and build the function. This - // ensures that any errors or assertions in the compilation process will - // trigger crashes instead of being caught as aborts in the external - // function. - executionEngine->recompileAndRelinkFunction(dispatcher); - } + Module *dispatchModule = NULL; +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 6) + // The MCJIT generates whole modules at a time so for every call that we + // haven't made before we need to create a new Module. + dispatchModule = new Module(getFreshModuleID(), ctx); +#else + dispatchModule = this->singleDispatchModule; +#endif + dispatcher = createDispatcher(f, i, dispatchModule); + dispatchers.insert(std::make_pair(i, dispatcher)); + +// Force the JIT execution engine to go ahead and build the function. This +// ensures that any errors or assertions in the compilation process will +// trigger crashes instead of being caught as aborts in the external +// function. +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 6) + if (dispatcher) { + // The dispatchModule is now ready so tell MCJIT to generate the code for + // it. + auto dispatchModuleUniq = std::unique_ptr<Module>(dispatchModule); + executionEngine->addModule( + std::move(dispatchModuleUniq)); // MCJIT takes ownership + // Force code generation + uint64_t fnAddr = + executionEngine->getFunctionAddress(dispatcher->getName()); + executionEngine->finalizeObject(); + assert(fnAddr && "failed to get function address"); + (void)fnAddr; } else { - dispatcher = it->second; + // MCJIT didn't take ownership of the module so delete it. + delete dispatchModule; } - +#else + if (dispatcher) { + // Old JIT works on a function at a time so compile the function. + executionEngine->recompileAndRelinkFunction(dispatcher); + } +#endif return runProtectedCall(dispatcher, args); } // FIXME: This is not reentrant. static uint64_t *gTheArgsP; - -bool ExternalDispatcher::runProtectedCall(Function *f, uint64_t *args) { +bool ExternalDispatcherImpl::runProtectedCall(Function *f, uint64_t *args) { struct sigaction segvAction, segvActionOld; bool res; - + if (!f) return false; @@ -185,85 +272,87 @@ bool ExternalDispatcher::runProtectedCall(Function *f, uint64_t *args) { return res; } +// FIXME: This might have been relevant for the old JIT but the MCJIT +// has a completly different implementation so this comment below is +// likely irrelevant and misleading. +// // For performance purposes we construct the stub in such a way that the // arguments pointer is passed through the static global variable gTheArgsP in // this file. This is done so that the stub function prototype trivially matches // the special cases that the JIT knows how to directly call. If this is not // done, then the jit will end up generating a nullary stub just to call our // stub, for every single function call. -Function *ExternalDispatcher::createDispatcher(Function *target, Instruction *inst) { +Function *ExternalDispatcherImpl::createDispatcher(Function *target, + Instruction *inst, + Module *module) { if (!resolveSymbol(target->getName())) return 0; - LLVMContext &ctx = target->getContext(); CallSite cs; - if (inst->getOpcode()==Instruction::Call) { + if (inst->getOpcode() == Instruction::Call) { cs = CallSite(cast<CallInst>(inst)); } else { cs = CallSite(cast<InvokeInst>(inst)); } - Value **args = new Value*[cs.arg_size()]; + Value **args = new Value *[cs.arg_size()]; - std::vector<LLVM_TYPE_Q Type*> nullary; - - Function *dispatcher = Function::Create(FunctionType::get(Type::getVoidTy(ctx), - nullary, false), - GlobalVariable::ExternalLinkage, - "", - dispatchModule); + std::vector<LLVM_TYPE_Q Type *> nullary; + // MCJIT functions need unique names, or wrong function can be called. + // The module identifier is included because for the MCJIT we need + // unique function names across all `llvm::Modules`s. + std::string fnName = + "dispatcher_" + target->getName().str() + module->getModuleIdentifier(); + Function *dispatcher = + Function::Create(FunctionType::get(Type::getVoidTy(ctx), nullary, false), + GlobalVariable::ExternalLinkage, fnName, module); BasicBlock *dBB = BasicBlock::Create(ctx, "entry", dispatcher); // Get a Value* for &gTheArgsP, as an i64**. - Instruction *argI64sp = - new IntToPtrInst(ConstantInt::get(Type::getInt64Ty(ctx), - (uintptr_t) (void*) &gTheArgsP), - PointerType::getUnqual(PointerType::getUnqual(Type::getInt64Ty(ctx))), - "argsp", dBB); - Instruction *argI64s = new LoadInst(argI64sp, "args", dBB); - + Instruction *argI64sp = new IntToPtrInst( + ConstantInt::get(Type::getInt64Ty(ctx), (uintptr_t)(void *)&gTheArgsP), + PointerType::getUnqual(PointerType::getUnqual(Type::getInt64Ty(ctx))), + "argsp", dBB); + Instruction *argI64s = new LoadInst(argI64sp, "args", dBB); + // Get the target function type. - LLVM_TYPE_Q FunctionType *FTy = - cast<FunctionType>(cast<PointerType>(target->getType())->getElementType()); + LLVM_TYPE_Q FunctionType *FTy = cast<FunctionType>( + cast<PointerType>(target->getType())->getElementType()); // Each argument will be passed by writing it into gTheArgsP[i]. unsigned i = 0, idx = 2; - for (CallSite::arg_iterator ai = cs.arg_begin(), ae = cs.arg_end(); - ai!=ae; ++ai, ++i) { + for (CallSite::arg_iterator ai = cs.arg_begin(), ae = cs.arg_end(); ai != ae; + ++ai, ++i) { // Determine the type the argument will be passed as. This accomodates for // the corresponding code in Executor.cpp for handling calls to bitcasted // functions. - LLVM_TYPE_Q Type *argTy = (i < FTy->getNumParams() ? FTy->getParamType(i) : - (*ai)->getType()); - Instruction *argI64p = - GetElementPtrInst::Create(argI64s, - ConstantInt::get(Type::getInt32Ty(ctx), idx), - "", dBB); - - Instruction *argp = new BitCastInst(argI64p, PointerType::getUnqual(argTy), - "", dBB); + LLVM_TYPE_Q Type *argTy = + (i < FTy->getNumParams() ? FTy->getParamType(i) : (*ai)->getType()); + Instruction *argI64p = GetElementPtrInst::Create( + argI64s, ConstantInt::get(Type::getInt32Ty(ctx), idx), "", dBB); + + Instruction *argp = + new BitCastInst(argI64p, PointerType::getUnqual(argTy), "", dBB); args[i] = new LoadInst(argp, "", dBB); unsigned argSize = argTy->getPrimitiveSizeInBits(); - idx += ((!!argSize ? argSize : 64) + 63)/64; + idx += ((!!argSize ? argSize : 64) + 63) / 64; } - Constant *dispatchTarget = - dispatchModule->getOrInsertFunction(target->getName(), FTy, - target->getAttributes()); + Constant *dispatchTarget = module->getOrInsertFunction( + target->getName(), FTy, target->getAttributes()); #if LLVM_VERSION_CODE >= LLVM_VERSION(3, 0) - Instruction *result = CallInst::Create(dispatchTarget, - llvm::ArrayRef<Value *>(args, args+i), - "", dBB); + Instruction *result = CallInst::Create( + dispatchTarget, llvm::ArrayRef<Value *>(args, args + i), "", dBB); #else - Instruction *result = CallInst::Create(dispatchTarget, args, args+i, "", dBB); + Instruction *result = + CallInst::Create(dispatchTarget, args, args + i, "", dBB); #endif if (result->getType() != Type::getVoidTy(ctx)) { - Instruction *resp = - new BitCastInst(argI64s, PointerType::getUnqual(result->getType()), - "", dBB); + Instruction *resp = new BitCastInst( + argI64s, PointerType::getUnqual(result->getType()), "", dBB); new StoreInst(result, resp, dBB); } @@ -273,3 +362,18 @@ Function *ExternalDispatcher::createDispatcher(Function *target, Instruction *in return dispatcher; } + +ExternalDispatcher::ExternalDispatcher(llvm::LLVMContext &ctx) + : impl(new ExternalDispatcherImpl(ctx)) {} + +ExternalDispatcher::~ExternalDispatcher() { delete impl; } + +bool ExternalDispatcher::executeCall(llvm::Function *function, + llvm::Instruction *i, uint64_t *args) { + return impl->executeCall(function, i, args); +} + +void *ExternalDispatcher::resolveSymbol(const std::string &name) { + return impl->resolveSymbol(name); +} +} diff --git a/lib/Core/ExternalDispatcher.h b/lib/Core/ExternalDispatcher.h index 94363bab..c64dc7d8 100644 --- a/lib/Core/ExternalDispatcher.h +++ b/lib/Core/ExternalDispatcher.h @@ -10,42 +10,37 @@ #ifndef KLEE_EXTERNALDISPATCHER_H #define KLEE_EXTERNALDISPATCHER_H +#include "klee/Config/Version.h" + #include <map> -#include <string> +#include <memory> #include <stdint.h> +#include <string> namespace llvm { - class ExecutionEngine; - class Instruction; - class LLVMContext; - class Function; - class FunctionType; - class Module; +class Instruction; +class LLVMContext; +class Function; } namespace klee { - class ExternalDispatcher { - private: - typedef std::map<const llvm::Instruction*,llvm::Function*> dispatchers_ty; - dispatchers_ty dispatchers; - llvm::Module *dispatchModule; - llvm::ExecutionEngine *executionEngine; - std::map<std::string, void*> preboundFunctions; - - llvm::Function *createDispatcher(llvm::Function *f, llvm::Instruction *i); - bool runProtectedCall(llvm::Function *f, uint64_t *args); - - public: - ExternalDispatcher(llvm::LLVMContext &ctx); - ~ExternalDispatcher(); - - /* Call the given function using the parameter passing convention of - * ci with arguments in args[1], args[2], ... and writing the result - * into args[0]. - */ - bool executeCall(llvm::Function *function, llvm::Instruction *i, uint64_t *args); - void *resolveSymbol(const std::string &name); - }; +class ExternalDispatcherImpl; +class ExternalDispatcher { +private: + ExternalDispatcherImpl *impl; + +public: + ExternalDispatcher(llvm::LLVMContext &ctx); + ~ExternalDispatcher(); + + /* Call the given function using the parameter passing convention of + * ci with arguments in args[1], args[2], ... and writing the result + * into args[0]. + */ + bool executeCall(llvm::Function *function, llvm::Instruction *i, + uint64_t *args); + void *resolveSymbol(const std::string &name); +}; } #endif diff --git a/lib/Core/Memory.h b/lib/Core/Memory.h index d08bfb0c..4e5c8734 100644 --- a/lib/Core/Memory.h +++ b/lib/Core/Memory.h @@ -50,8 +50,6 @@ public: mutable bool isGlobal; bool isFixed; - /// true if created by us. - bool fake_object; bool isUserSpecified; MemoryManager *parent; @@ -96,7 +94,6 @@ public: isLocal(_isLocal), isGlobal(_isGlobal), isFixed(_isFixed), - fake_object(false), isUserSpecified(false), parent(_parent), allocSite(_allocSite) { diff --git a/lib/Core/Searcher.cpp b/lib/Core/Searcher.cpp index c787382f..d15226b3 100644 --- a/lib/Core/Searcher.cpp +++ b/lib/Core/Searcher.cpp @@ -539,7 +539,7 @@ ExecutionState &BatchingSearcher::selectState() { if (lastState) { double delta = util::getWallTime()-lastStartTime; if (delta>timeBudget*1.1) { - klee_message("KLEE: increased time budget from %f to %f\n", timeBudget, + klee_message("increased time budget from %f to %f\n", timeBudget, delta); timeBudget = delta; } @@ -613,7 +613,7 @@ void IterativeDeepeningTimeSearcher::update( if (baseSearcher->empty()) { time *= 2; - klee_message("KLEE: increased time budget to %f\n", time); + klee_message("increased time budget to %f\n", time); std::vector<ExecutionState *> ps(pausedStates.begin(), pausedStates.end()); baseSearcher->update(0, ps, std::vector<ExecutionState *>()); pausedStates.clear(); diff --git a/lib/Core/StatsTracker.cpp b/lib/Core/StatsTracker.cpp index ccf6e04d..b93796ec 100644 --- a/lib/Core/StatsTracker.cpp +++ b/lib/Core/StatsTracker.cpp @@ -168,7 +168,7 @@ static bool instructionIsCoverable(Instruction *i) { Instruction *prev = static_cast<Instruction *>(--it); if (isa<CallInst>(prev) || isa<InvokeInst>(prev)) { Function *target = - getDirectCallTarget(prev, /*moduleIsFullyLinked=*/true); + getDirectCallTarget(CallSite(prev), /*moduleIsFullyLinked=*/true); if (target && target->doesNotReturn()) return false; } @@ -206,13 +206,16 @@ StatsTracker::StatsTracker(Executor &_executor, std::string _objectFilename, if (!sys::path::is_absolute(objectFilename)) { SmallString<128> current(objectFilename); if(sys::fs::make_absolute(current)) { +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 6) + Twine current_twine(current.str()); // requires a twine for this + if (!sys::fs::exists(current_twine)) { +#elif LLVM_VERSION_CODE >= LLVM_VERSION(3, 5) + bool exists = false; + if (!sys::fs::exists(current.str(), exists)) { +#else bool exists = false; - -#if LLVM_VERSION_CODE < LLVM_VERSION(3, 5) error_code ec = sys::fs::exists(current.str(), exists); if (ec == errc::success && exists) { -#else - if (!sys::fs::exists(current.str(), exists)) { #endif objectFilename = current.c_str(); } diff --git a/lib/Expr/Assigment.cpp b/lib/Expr/Assigment.cpp index 635362d4..d788785a 100644 --- a/lib/Expr/Assigment.cpp +++ b/lib/Expr/Assigment.cpp @@ -22,4 +22,21 @@ void Assignment::dump() { llvm::errs() << "]\n"; } } + +void Assignment::createConstraintsFromAssignment( + std::vector<ref<Expr> > &out) const { + assert(out.size() == 0 && "out should be empty"); + for (bindings_ty::const_iterator it = bindings.begin(), ie = bindings.end(); + it != ie; ++it) { + const Array *array = it->first; + const std::vector<unsigned char> &values = it->second; + for (unsigned arrayIndex = 0; arrayIndex < array->size; ++arrayIndex) { + unsigned char value = values[arrayIndex]; + out.push_back(EqExpr::create( + ReadExpr::create(UpdateList(array, 0), + ConstantExpr::alloc(arrayIndex, array->getDomain())), + ConstantExpr::alloc(value, array->getRange()))); + } + } +} } diff --git a/lib/Module/KInstruction.cpp b/lib/Module/KInstruction.cpp index 799620c6..a32745b8 100644 --- a/lib/Module/KInstruction.cpp +++ b/lib/Module/KInstruction.cpp @@ -17,3 +17,10 @@ using namespace klee; KInstruction::~KInstruction() { delete[] operands; } + +void KInstruction::printFileLine(llvm::raw_ostream &debugFile) { + if (info->file != "") + debugFile << info->file << ":" << info->line; + else + debugFile << "[no debug info]"; +} diff --git a/lib/Module/KModule.cpp b/lib/Module/KModule.cpp index 08ec28ef..45dc34bf 100644 --- a/lib/Module/KModule.cpp +++ b/lib/Module/KModule.cpp @@ -158,8 +158,14 @@ static Function *getStubFunctionForCtorList(Module *m, if (arr) { for (unsigned i=0; i<arr->getNumOperands(); i++) { ConstantStruct *cs = cast<ConstantStruct>(arr->getOperand(i)); +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 5) + // There is a third *optional* element in global_ctor elements (``i8 + // @data``). + assert((cs->getNumOperands() == 2 || cs->getNumOperands() == 3) && + "unexpected element in ctor initializer list"); +#else assert(cs->getNumOperands()==2 && "unexpected element in ctor initializer list"); - +#endif Constant *fp = cs->getOperand(1); if (!fp->isNullValue()) { if (llvm::ConstantExpr *ce = dyn_cast<llvm::ConstantExpr>(fp)) @@ -513,8 +519,13 @@ static int getOperandNum(Value *v, return registerMap[inst]; } else if (Argument *a = dyn_cast<Argument>(v)) { return a->getArgNo(); +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 6) + // Metadata is no longer a Value + } else if (isa<BasicBlock>(v) || isa<InlineAsm>(v)) { +#else } else if (isa<BasicBlock>(v) || isa<InlineAsm>(v) || isa<MDNode>(v)) { +#endif return -1; } else { assert(isa<Constant>(v)); diff --git a/lib/Module/ModuleUtil.cpp b/lib/Module/ModuleUtil.cpp index 94a37e08..c7f1c6d9 100644 --- a/lib/Module/ModuleUtil.cpp +++ b/lib/Module/ModuleUtil.cpp @@ -212,15 +212,27 @@ static bool linkBCA(object::Archive* archive, Module* composite, std::string& er KLEE_DEBUG_WITH_TYPE("klee_linker", dbgs() << "Loading modules\n"); // Load all bitcode files in to memory so we can examine their symbols +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 5) + for (object::Archive::child_iterator AI = archive->child_begin(), + AE = archive->child_end(); AI != AE; ++AI) +#else for (object::Archive::child_iterator AI = archive->begin_children(), AE = archive->end_children(); AI != AE; ++AI) +#endif { StringRef memberName; +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 5) + ErrorOr<StringRef> memberNameErr = AI->getName(); + std::error_code ec = memberNameErr.getError(); + if (!ec) { + memberName = memberNameErr.get(); +#else error_code ec = AI->getName(memberName); if ( ec == errc::success ) { +#endif KLEE_DEBUG_WITH_TYPE("klee_linker", dbgs() << "Loading archive member " << memberName << "\n"); } else @@ -229,17 +241,29 @@ static bool linkBCA(object::Archive* archive, Module* composite, std::string& er return false; } +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 5) + ErrorOr<std::unique_ptr<llvm::object::Binary> > child = AI->getAsBinary(); + ec = child.getError(); +#else OwningPtr<object::Binary> child; ec = AI->getAsBinary(child); - if (ec != object::object_error::success) - { +#endif + if (ec) { // If we can't open as a binary object file its hopefully a bitcode file - +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 6) + ErrorOr<MemoryBufferRef> buff = AI->getMemoryBufferRef(); + ec = buff.getError(); +#elif LLVM_VERSION_CODE >= LLVM_VERSION(3, 5) + ErrorOr<std::unique_ptr<MemoryBuffer> > buffErr = AI->getMemoryBuffer(); + std::unique_ptr<MemoryBuffer> buff = nullptr; + ec = buffErr.getError(); + if (!ec) + buff = std::move(buffErr.get()); +#else OwningPtr<MemoryBuffer> buff; // Once this is destroyed will Module still be valid?? - Module *Result = 0; - - if (error_code ec = AI->getMemoryBuffer(buff)) - { + ec = AI->getMemoryBuffer(buff); +#endif + if (ec) { SS << "Failed to get MemoryBuffer: " <<ec.message(); SS.flush(); return false; @@ -247,10 +271,20 @@ static bool linkBCA(object::Archive* archive, Module* composite, std::string& er if (buff) { + Module *Result = 0; // FIXME: Maybe load bitcode file lazily? Then if we need to link, materialise the module +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 5) + ErrorOr<Module *> resultErr = parseBitcodeFile(buff.get(), + composite->getContext()); + ec = resultErr.getError(); + if (ec) + errorMessage = ec.message(); + else + Result = resultErr.get(); +#else Result = ParseBitcodeFile(buff.get(), composite->getContext(), &errorMessage); - +#endif if(!Result) { SS << "Loading module failed : " << errorMessage << "\n"; @@ -266,9 +300,9 @@ static bool linkBCA(object::Archive* archive, Module* composite, std::string& er } } - else if (object::ObjectFile *o = dyn_cast<object::ObjectFile>(child.get())) + else if (child.get()->isObject()) { - SS << "Object file " << o->getFileName().data() << + SS << "Object file " << child.get()->getFileName().data() << " in archive is not supported"; SS.flush(); return false; @@ -317,8 +351,11 @@ static bool linkBCA(object::Archive* archive, Module* composite, std::string& er KLEE_DEBUG_WITH_TYPE("klee_linker", dbgs() << "Found " << GV->getName() << " in " << M->getModuleIdentifier() << "\n"); - +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 6) + if (Linker::LinkModules(composite, M)) +#else if (Linker::LinkModules(composite, M, Linker::DestroySource, &errorMessage)) +#endif { // Linking failed SS << "Linking archive module with composite failed:" << errorMessage; @@ -371,36 +408,86 @@ Module *klee::linkWithLibrary(Module *module, libraryName.c_str()); } +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 5) + ErrorOr<std::unique_ptr<MemoryBuffer> > bufferErr = + MemoryBuffer::getFile(libraryName); + std::error_code ec = bufferErr.getError(); +#else OwningPtr<MemoryBuffer> Buffer; - if (error_code ec = MemoryBuffer::getFile(libraryName,Buffer)) { + error_code ec = MemoryBuffer::getFile(libraryName,Buffer); +#endif + if (ec) { klee_error("Link with library %s failed: %s", libraryName.c_str(), ec.message().c_str()); } +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 6) + MemoryBufferRef Buffer = bufferErr.get()->getMemBufferRef(); +#elif LLVM_VERSION_CODE >= LLVM_VERSION(3, 5) + MemoryBuffer *Buffer = bufferErr->get(); +#endif + +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 6) + sys::fs::file_magic magic = sys::fs::identify_magic(Buffer.getBuffer()); +#else sys::fs::file_magic magic = sys::fs::identify_magic(Buffer->getBuffer()); +#endif LLVMContext &Context = module->getContext(); std::string ErrorMessage; if (magic == sys::fs::file_magic::bitcode) { Module *Result = 0; +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 5) + ErrorOr<Module *> ResultErr = parseBitcodeFile(Buffer, Context); + if ((ec = ResultErr.getError())) { + ErrorMessage = ec.message(); +#else Result = ParseBitcodeFile(Buffer.get(), Context, &ErrorMessage); + if (!Result) { +#endif + klee_error("Link with library %s failed: %s", libraryName.c_str(), + ErrorMessage.c_str()); + } +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 5) + Result = ResultErr.get(); +#endif - if (!Result || Linker::LinkModules(module, Result, Linker::DestroySource, - &ErrorMessage)) +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 6) + if (Linker::LinkModules(module, Result)) { + ErrorMessage = "linking error"; +#else + if (Linker::LinkModules(module, Result, Linker::DestroySource, &ErrorMessage)) { +#endif klee_error("Link with library %s failed: %s", libraryName.c_str(), ErrorMessage.c_str()); + } delete Result; } else if (magic == sys::fs::file_magic::archive) { +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 6) + ErrorOr<std::unique_ptr<object::Binary> > arch = + object::createBinary(Buffer, &Context); + ec = arch.getError(); +#elif LLVM_VERSION_CODE >= LLVM_VERSION(3, 5) + ErrorOr<object::Binary *> arch = + object::createBinary(std::move(bufferErr.get()), &Context); + ec = arch.getError(); +#else OwningPtr<object::Binary> arch; - if (error_code ec = object::createBinary(Buffer.take(), arch)) + ec = object::createBinary(Buffer.take(), arch); +#endif + if (ec) klee_error("Link with library %s failed: %s", libraryName.c_str(), ec.message().c_str()); +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 6) + if (object::Archive *a = dyn_cast<object::Archive>(arch->get())) { +#else if (object::Archive *a = dyn_cast<object::Archive>(arch.get())) { +#endif // Handle in helper if (!linkBCA(a, module, ErrorMessage)) klee_error("Link with library %s failed: %s", libraryName.c_str(), @@ -411,11 +498,15 @@ Module *klee::linkWithLibrary(Module *module, } } else if (magic.is_object()) { +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 5) + std::unique_ptr<object::Binary> obj; +#else OwningPtr<object::Binary> obj; - if (object::ObjectFile *o = dyn_cast<object::ObjectFile>(obj.get())) { +#endif + if (obj.get()->isObject()) { klee_warning("Link with library: Object file %s in archive %s found. " "Currently not supported.", - o->getFileName().data(), libraryName.c_str()); + obj.get()->getFileName().data(), libraryName.c_str()); } } else { klee_error("Link with library %s failed: Unrecognized file type.", diff --git a/lib/Module/Optimize.cpp b/lib/Module/Optimize.cpp index 3d9c8cc1..c0f3f34c 100644 --- a/lib/Module/Optimize.cpp +++ b/lib/Module/Optimize.cpp @@ -172,15 +172,17 @@ void Optimize(Module *M, const std::string &EntryPoint) { if (VerifyEach) Passes.add(createVerifierPass()); -#if LLVM_VERSION_CODE <= LLVM_VERSION(3, 1) - // Add an appropriate TargetData instance for this module... - addPass(Passes, new TargetData(M)); -#elif LLVM_VERSION_CODE < LLVM_VERSION(3, 5) // Add an appropriate DataLayout instance for this module... +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 6) + DataLayoutPass *dlpass = new DataLayoutPass(); + dlpass->doInitialization(*M); + addPass(Passes, dlpass); +#elif LLVM_VERSION_CODE >= LLVM_VERSION(3, 5) + addPass(Passes, new DataLayoutPass(M)); +#elif LLVM_VERSION_CODE >= LLVM_VERSION(3, 2) addPass(Passes, new DataLayout(M)); #else - // Add an appropriate DataLayout instance for this module... - addPass(Passes, new DataLayoutPass(M)); + addPass(Passes, new TargetData(M)); #endif // DWD - Run the opt standard pass list as well. diff --git a/lib/Module/RaiseAsm.cpp b/lib/Module/RaiseAsm.cpp index af92b74b..5fc54ef1 100644 --- a/lib/Module/RaiseAsm.cpp +++ b/lib/Module/RaiseAsm.cpp @@ -24,6 +24,10 @@ #include "llvm/Support/raw_ostream.h" #include "llvm/Support/Host.h" #include "llvm/Target/TargetLowering.h" +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 6) +#include "llvm/Target/TargetMachine.h" +#include "llvm/Target/TargetSubtargetInfo.h" +#endif #if LLVM_VERSION_CODE < LLVM_VERSION(3, 0) #include "llvm/Target/TargetRegistry.h" #else @@ -99,15 +103,20 @@ bool RaiseAsmPass::runOnModule(Module &M) { klee_warning("Warning: unable to select native target: %s", Err.c_str()); TLI = 0; } else { -#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 1) +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 6) + TM = NativeTarget->createTargetMachine(HostTriple, "", "", TargetOptions()); + TLI = TM->getSubtargetImpl()->getTargetLowering(); +#elif LLVM_VERSION_CODE >= LLVM_VERSION(3, 1) TM = NativeTarget->createTargetMachine(HostTriple, "", "", TargetOptions()); + TLI = TM->getTargetLowering(); #elif LLVM_VERSION_CODE >= LLVM_VERSION(3, 0) TM = NativeTarget->createTargetMachine(HostTriple, "", ""); + TLI = TM->getTargetLowering(); #else TM = NativeTarget->createTargetMachine(HostTriple, ""); -#endif TLI = TM->getTargetLowering(); +#endif triple = llvm::Triple(HostTriple); } diff --git a/lib/Solver/AssignmentValidatingSolver.cpp b/lib/Solver/AssignmentValidatingSolver.cpp new file mode 100644 index 00000000..a4d97f54 --- /dev/null +++ b/lib/Solver/AssignmentValidatingSolver.cpp @@ -0,0 +1,158 @@ +//===-- AssignmentValidatingSolver.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/util/Assignment.h" +#include "klee/Constraints.h" +#include "klee/Solver.h" +#include "klee/SolverImpl.h" +#include <vector> + +namespace klee { + +class AssignmentValidatingSolver : public SolverImpl { +private: + Solver *solver; + void dumpAssignmentQuery(const Query &query, const Assignment &assignment); + +public: + AssignmentValidatingSolver(Solver *_solver) : solver(_solver) {} + ~AssignmentValidatingSolver() { delete solver; } + + bool computeValidity(const Query &, Solver::Validity &result); + bool computeTruth(const Query &, bool &isValid); + bool computeValue(const Query &, ref<Expr> &result); + bool computeInitialValues(const Query &, + const std::vector<const Array *> &objects, + std::vector<std::vector<unsigned char> > &values, + bool &hasSolution); + SolverRunStatus getOperationStatusCode(); + char *getConstraintLog(const Query &); + void setCoreSolverTimeout(double timeout); +}; + +// TODO: use computeInitialValues for all queries for more stress testing +bool AssignmentValidatingSolver::computeValidity(const Query &query, + Solver::Validity &result) { + return solver->impl->computeValidity(query, result); +} +bool AssignmentValidatingSolver::computeTruth(const Query &query, + bool &isValid) { + return solver->impl->computeTruth(query, isValid); +} +bool AssignmentValidatingSolver::computeValue(const Query &query, + ref<Expr> &result) { + return solver->impl->computeValue(query, result); +} + +bool AssignmentValidatingSolver::computeInitialValues( + const Query &query, const std::vector<const Array *> &objects, + std::vector<std::vector<unsigned char> > &values, bool &hasSolution) { + bool success = + solver->impl->computeInitialValues(query, objects, values, hasSolution); + if (!hasSolution) + return success; + + // Use `_allowFreeValues` so that if we are missing an assignment + // we can't compute a constant and flag this as a problem. + Assignment assignment(objects, values, /*_allowFreeValues=*/true); + // Check computed assignment satisfies query + for (ConstraintManager::const_iterator it = query.constraints.begin(), + ie = query.constraints.end(); + it != ie; ++it) { + ref<Expr> constraint = *it; + ref<Expr> constraintEvaluated = assignment.evaluate(constraint); + ConstantExpr *CE = dyn_cast<ConstantExpr>(constraintEvaluated); + if (CE == NULL) { + llvm::errs() << "Constraint did not evalaute to a constant:\n"; + llvm::errs() << "Constraint:\n" << constraint << "\n"; + llvm::errs() << "Evaluated Constraint:\n" << constraintEvaluated << "\n"; + llvm::errs() << "Assignment:\n"; + assignment.dump(); + dumpAssignmentQuery(query, assignment); + abort(); + } + if (CE->isFalse()) { + llvm::errs() << "Constraint evaluated to false when using assignment\n"; + llvm::errs() << "Constraint:\n" << constraint << "\n"; + llvm::errs() << "Assignment:\n"; + assignment.dump(); + dumpAssignmentQuery(query, assignment); + abort(); + } + } + + ref<Expr> queryExprEvaluated = assignment.evaluate(query.expr); + ConstantExpr *CE = dyn_cast<ConstantExpr>(queryExprEvaluated); + if (CE == NULL) { + llvm::errs() << "Query expression did not evalaute to a constant:\n"; + llvm::errs() << "Expression:\n" << query.expr << "\n"; + llvm::errs() << "Evaluated expression:\n" << queryExprEvaluated << "\n"; + llvm::errs() << "Assignment:\n"; + assignment.dump(); + dumpAssignmentQuery(query, assignment); + abort(); + } + // KLEE queries are validity queries. A counter example to + // ∀ x constraints(x) → query(x) + // exists therefore + // ¬∀ x constraints(x) → query(x) + // Which is equivalent to + // ∃ x constraints(x) ∧ ¬ query(x) + // This means for the assignment we get back query expression should evaluate + // to false. + if (CE->isTrue()) { + llvm::errs() + << "Query Expression evaluated to true when using assignment\n"; + llvm::errs() << "Expression:\n" << query.expr << "\n"; + llvm::errs() << "Assignment:\n"; + assignment.dump(); + dumpAssignmentQuery(query, assignment); + abort(); + } + + return success; +} + +void AssignmentValidatingSolver::dumpAssignmentQuery( + const Query &query, const Assignment &assignment) { + // Create a Query that is augmented with constraints that + // enforce the given assignment. + std::vector<ref<Expr> > constraints; + assignment.createConstraintsFromAssignment(constraints); + // Add Constraints from `query` + for (ConstraintManager::const_iterator it = query.constraints.begin(), + ie = query.constraints.end(); + it != ie; ++it) { + constraints.push_back(*it); + } + ConstraintManager augmentedConstraints(constraints); + Query augmentedQuery(augmentedConstraints, query.expr); + + // Ask the solver for the log for this query. + char *logText = solver->getConstraintLog(augmentedQuery); + llvm::errs() << "Query with assignment as constraints:\n" << logText << "\n"; + free(logText); +} + +SolverImpl::SolverRunStatus +AssignmentValidatingSolver::getOperationStatusCode() { + return solver->impl->getOperationStatusCode(); +} + +char *AssignmentValidatingSolver::getConstraintLog(const Query &query) { + return solver->impl->getConstraintLog(query); +} + +void AssignmentValidatingSolver::setCoreSolverTimeout(double timeout) { + return solver->impl->setCoreSolverTimeout(timeout); +} + +Solver *createAssignmentValidatingSolver(Solver *s) { + return new Solver(new AssignmentValidatingSolver(s)); +} +} diff --git a/lib/Solver/CMakeLists.txt b/lib/Solver/CMakeLists.txt index 1302db38..d9c393fb 100644 --- a/lib/Solver/CMakeLists.txt +++ b/lib/Solver/CMakeLists.txt @@ -7,6 +7,7 @@ # #===------------------------------------------------------------------------===# klee_add_component(kleaverSolver + AssignmentValidatingSolver.cpp CachingSolver.cpp CexCachingSolver.cpp ConstantDivision.cpp diff --git a/lib/Solver/CoreSolver.cpp b/lib/Solver/CoreSolver.cpp index 783047f8..438f38f6 100644 --- a/lib/Solver/CoreSolver.cpp +++ b/lib/Solver/CoreSolver.cpp @@ -7,90 +7,48 @@ // //===----------------------------------------------------------------------===// +#include "STPSolver.h" +#include "Z3Solver.h" +#include "MetaSMTSolver.h" #include "klee/CommandLine.h" +#include "klee/Internal/Support/ErrorHandling.h" #include "klee/Solver.h" #include "llvm/Support/ErrorHandling.h" #include "llvm/Support/raw_ostream.h" #include <string> -#ifdef ENABLE_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 klee; -using namespace metaSMT; -using namespace metaSMT::solver; - -static klee::Solver *handleMetaSMT() { - Solver *coreSolver = NULL; - std::string backend; - switch (MetaSMTBackend) { - 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: - llvm_unreachable("Unrecognised metasmt backend"); - break; - }; - llvm::errs() << "Starting MetaSMTSolver(" << backend << ") ...\n"; - return coreSolver; -} -#endif /* ENABLE_METASMT */ - namespace klee { Solver *createCoreSolver(CoreSolverType cst) { switch (cst) { case STP_SOLVER: #ifdef ENABLE_STP - llvm::errs() << "Using STP solver backend\n"; + klee_message("Using STP solver backend"); return new STPSolver(UseForkedCoreSolver, CoreSolverOptimizeDivides); #else - llvm::errs() << "Not compiled with STP support\n"; + klee_message("Not compiled with STP support"); return NULL; #endif case METASMT_SOLVER: #ifdef ENABLE_METASMT - llvm::errs() << "Using MetaSMT solver backend\n"; - return handleMetaSMT(); + klee_message("Using MetaSMT solver backend"); + return createMetaSMTSolver(); #else - llvm::errs() << "Not compiled with MetaSMT support\n"; + klee_message("Not compiled with MetaSMT support"); return NULL; #endif case DUMMY_SOLVER: return createDummySolver(); case Z3_SOLVER: #ifdef ENABLE_Z3 - llvm::errs() << "Using Z3 solver backend\n"; + klee_message("Using Z3 solver backend"); return new Z3Solver(); #else - llvm::errs() << "Not compiled with Z3 support\n"; + klee_message("Not compiled with Z3 support"); return NULL; #endif case NO_SOLVER: - llvm::errs() << "Invalid solver\n"; + klee_message("Invalid solver"); return NULL; default: llvm_unreachable("Unsupported CoreSolverType"); diff --git a/lib/Solver/MetaSMTSolver.cpp b/lib/Solver/MetaSMTSolver.cpp index a453de40..9b49f995 100644 --- a/lib/Solver/MetaSMTSolver.cpp +++ b/lib/Solver/MetaSMTSolver.cpp @@ -9,6 +9,7 @@ #include "klee/Config/config.h" #ifdef ENABLE_METASMT +#include "MetaSMTSolver.h" #include "MetaSMTBuilder.h" #include "klee/Constraints.h" #include "klee/Internal/Support/ErrorHandling.h" @@ -17,6 +18,8 @@ #include "klee/util/Assignment.h" #include "klee/util/ExprUtil.h" +#include "llvm/Support/ErrorHandling.h" + #include <metaSMT/DirectSolver_Context.hpp> #include <metaSMT/backend/Z3_Backend.hpp> #include <metaSMT/backend/Boolector.hpp> @@ -405,5 +408,36 @@ void MetaSMTSolver<SolverContext>::setCoreSolverTimeout(double timeout) { template class MetaSMTSolver<DirectSolver_Context<metaSMT::solver::Boolector> >; template class MetaSMTSolver<DirectSolver_Context<metaSMT::solver::Z3_Backend> >; template class MetaSMTSolver<DirectSolver_Context<metaSMT::solver::STP_Backend> >; + +Solver *createMetaSMTSolver() { + using metaSMT::DirectSolver_Context; + using namespace metaSMT::solver; + + Solver *coreSolver = NULL; + std::string backend; + switch (MetaSMTBackend) { + 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: + llvm_unreachable("Unrecognised MetaSMT backend"); + break; + }; + klee_message("Starting MetaSMTSolver(%s)", backend.c_str()); + return coreSolver; +} + } #endif // ENABLE_METASMT diff --git a/lib/Solver/MetaSMTSolver.h b/lib/Solver/MetaSMTSolver.h new file mode 100644 index 00000000..60d72383 --- /dev/null +++ b/lib/Solver/MetaSMTSolver.h @@ -0,0 +1,32 @@ +//===-- MetaSMTSolver.h +//---------------------------------------------------===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + +#ifndef KLEE_METASMTSOLVER_H +#define KLEE_METASMTSOLVER_H + +#include "klee/Solver.h" + +namespace klee { + +template <typename SolverContext> class MetaSMTSolver : public Solver { +public: + MetaSMTSolver(bool useForked, bool optimizeDivides); + virtual ~MetaSMTSolver(); + + virtual char *getConstraintLog(const Query &); + virtual void setCoreSolverTimeout(double timeout); +}; + +/// createMetaSMTSolver - Create a solver using the metaSMT backend set by +/// the option MetaSMTBackend. +Solver *createMetaSMTSolver(); +} + +#endif /* KLEE_METASMTSOLVER_H */ diff --git a/lib/Solver/QueryLoggingSolver.cpp b/lib/Solver/QueryLoggingSolver.cpp index a858a7d7..cf4966cd 100644 --- a/lib/Solver/QueryLoggingSolver.cpp +++ b/lib/Solver/QueryLoggingSolver.cpp @@ -42,7 +42,13 @@ QueryLoggingSolver::QueryLoggingSolver(Solver *_solver, std::string path, #ifdef HAVE_ZLIB_H if (!CreateCompressedQueryLog) { #endif -#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 5) +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 6) + std::error_code ec; + os = new llvm::raw_fd_ostream(path.c_str(), ec, + llvm::sys::fs::OpenFlags::F_Text); + if (ec) + ErrorInfo = ec.message(); +#elif LLVM_VERSION_CODE >= LLVM_VERSION(3, 5) os = new llvm::raw_fd_ostream(path.c_str(), ErrorInfo, llvm::sys::fs::OpenFlags::F_Text); #else diff --git a/lib/Solver/STPSolver.cpp b/lib/Solver/STPSolver.cpp index 5893c28e..d1b8cbdc 100644 --- a/lib/Solver/STPSolver.cpp +++ b/lib/Solver/STPSolver.cpp @@ -8,6 +8,7 @@ //===----------------------------------------------------------------------===// #include "klee/Config/config.h" #ifdef ENABLE_STP +#include "STPSolver.h" #include "STPBuilder.h" #include "klee/Solver.h" #include "klee/SolverImpl.h" diff --git a/lib/Solver/STPSolver.h b/lib/Solver/STPSolver.h new file mode 100644 index 00000000..cb68ed91 --- /dev/null +++ b/lib/Solver/STPSolver.h @@ -0,0 +1,39 @@ +//===-- STPSolver.h +//---------------------------------------------------===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + +#ifndef KLEE_STPSOLVER_H +#define KLEE_STPSOLVER_H + +#include "klee/Solver.h" + +namespace klee { +/// STPSolver - A complete solver based on STP. +class STPSolver : public Solver { +public: + /// STPSolver - Construct a new STPSolver. + /// + /// \param useForkedSTP - Whether STP should be run in a separate process + /// (required for using timeouts). + /// \param optimizeDivides - Whether constant division operations should + /// be optimized into add/shift/multiply operations. + STPSolver(bool useForkedSTP, bool optimizeDivides = true); + + /// getConstraintLog - Return the constraint log for the given state in CVC + /// format. + virtual char *getConstraintLog(const Query &); + + /// setCoreSolverTimeout - Set constraint solver timeout delay to the given + /// value; 0 + /// is off. + virtual void setCoreSolverTimeout(double timeout); +}; +} + +#endif /* KLEE_STPSOLVER_H */ diff --git a/lib/Solver/Z3Builder.cpp b/lib/Solver/Z3Builder.cpp index fc826c07..6c0653e8 100644 --- a/lib/Solver/Z3Builder.cpp +++ b/lib/Solver/Z3Builder.cpp @@ -11,10 +11,10 @@ #include "Z3Builder.h" #include "klee/Expr.h" +#include "klee/Internal/Support/ErrorHandling.h" #include "klee/Solver.h" -#include "klee/util/Bits.h" -#include "ConstantDivision.h" #include "klee/SolverStats.h" +#include "klee/util/Bits.h" #include "llvm/ADT/StringExtras.h" #include "llvm/Support/CommandLine.h" @@ -26,6 +26,21 @@ llvm::cl::opt<bool> UseConstructHashZ3( "use-construct-hash-z3", llvm::cl::desc("Use hash-consing during Z3 query construction."), llvm::cl::init(true)); + +// FIXME: This should be std::atomic<bool>. Need C++11 for that. +bool Z3InterationLogOpen = false; +} + +namespace klee { + +// Declared here rather than `Z3Builder.h` so they can be called in gdb. +template <> void Z3NodeHandle<Z3_sort>::dump() { + llvm::errs() << "Z3SortHandle:\n" << ::Z3_sort_to_string(context, node) + << "\n"; +} +template <> void Z3NodeHandle<Z3_ast>::dump() { + llvm::errs() << "Z3ASTHandle:\n" << ::Z3_ast_to_string(context, as_ast()) + << "\n"; } void custom_z3_error_handler(Z3_context ctx, Z3_error_code ec) { @@ -45,6 +60,9 @@ void custom_z3_error_handler(Z3_context ctx, Z3_error_code ec) { } llvm::errs() << "Error: Incorrect use of Z3. [" << ec << "] " << errorMsg << "\n"; + // NOTE: The current implementation of `Z3_close_log()` can be safely + // called even if the log isn't open. + Z3_close_log(); abort(); } @@ -55,8 +73,17 @@ void Z3ArrayExprHash::clear() { _array_hash.clear(); } -Z3Builder::Z3Builder(bool autoClearConstructCache) - : autoClearConstructCache(autoClearConstructCache) { +Z3Builder::Z3Builder(bool autoClearConstructCache, const char* z3LogInteractionFileArg) + : autoClearConstructCache(autoClearConstructCache), z3LogInteractionFile("") { + if (z3LogInteractionFileArg) + this->z3LogInteractionFile = std::string(z3LogInteractionFileArg); + if (z3LogInteractionFile.length() > 0) { + klee_message("Logging Z3 API interaction to \"%s\"", + z3LogInteractionFile.c_str()); + assert(!Z3InterationLogOpen && "interaction log should not already be open"); + Z3_open_log(z3LogInteractionFile.c_str()); + Z3InterationLogOpen = true; + } // FIXME: Should probably let the client pass in a Z3_config instead Z3_config cfg = Z3_mk_config(); // It is very important that we ask Z3 to let us manage memory so that @@ -75,6 +102,10 @@ Z3Builder::~Z3Builder() { clearConstructCache(); _arr_hash.clear(); Z3_del_context(ctx); + if (z3LogInteractionFile.length() > 0) { + Z3_close_log(); + Z3InterationLogOpen = false; + } } Z3SortHandle Z3Builder::getBvSort(unsigned width) { @@ -529,6 +560,7 @@ Z3ASTHandle Z3Builder::constructActual(ref<Expr> e, int *width_out) { if (srcWidth == 1) { return iteExpr(src, bvOne(*width_out), bvZero(*width_out)); } else { + assert(*width_out > srcWidth && "Invalid width_out"); return Z3ASTHandle(Z3_mk_concat(ctx, bvZero(*width_out - srcWidth), src), ctx); } @@ -621,12 +653,15 @@ Z3ASTHandle Z3Builder::constructActual(ref<Expr> e, int *width_out) { uint64_t divisor = CE->getZExtValue(); if (bits64::isPowerOfTwo(divisor)) { - unsigned bits = bits64::indexOfSingleBit(divisor); + // FIXME: This should be unsigned but currently needs to be signed to + // avoid signed-unsigned comparison in assert. + int bits = bits64::indexOfSingleBit(divisor); // special case for modding by 1 or else we bvExtract -1:0 if (bits == 0) { return bvZero(*width_out); } else { + assert(*width_out > bits && "invalid width_out"); return Z3ASTHandle(Z3_mk_concat(ctx, bvZero(*width_out - bits), bvExtract(left, bits - 1, 0)), ctx); @@ -816,4 +851,5 @@ Z3ASTHandle Z3Builder::constructActual(ref<Expr> e, int *width_out) { return getTrue(); } } +} #endif // ENABLE_Z3 diff --git a/lib/Solver/Z3Builder.h b/lib/Solver/Z3Builder.h index f3b2732b..a3473f82 100644 --- a/lib/Solver/Z3Builder.h +++ b/lib/Solver/Z3Builder.h @@ -81,19 +81,13 @@ template <> inline ::Z3_ast Z3NodeHandle<Z3_sort>::as_ast() { // instead to simplify our implementation but this seems cleaner. return ::Z3_sort_to_ast(context, node); } -template <> inline void Z3NodeHandle<Z3_sort>::dump() { - llvm::errs() << "Z3SortHandle:\n" << ::Z3_sort_to_string(context, node) - << "\n"; -} typedef Z3NodeHandle<Z3_sort> Z3SortHandle; +template <> void Z3NodeHandle<Z3_sort>::dump() __attribute__((used)); // Specialise for Z3_ast template <> inline ::Z3_ast Z3NodeHandle<Z3_ast>::as_ast() { return node; } -template <> inline void Z3NodeHandle<Z3_ast>::dump() { - llvm::errs() << "Z3ASTHandle:\n" << ::Z3_ast_to_string(context, as_ast()) - << "\n"; -} typedef Z3NodeHandle<Z3_ast> Z3ASTHandle; +template <> void Z3NodeHandle<Z3_ast>::dump() __attribute__((used)); class Z3ArrayExprHash : public ArrayExprHash<Z3ASTHandle> { @@ -171,11 +165,11 @@ private: Z3SortHandle getBvSort(unsigned width); Z3SortHandle getArraySort(Z3SortHandle domainSort, Z3SortHandle rangeSort); bool autoClearConstructCache; + std::string z3LogInteractionFile; public: Z3_context ctx; - - Z3Builder(bool autoClearConstructCache = true); + Z3Builder(bool autoClearConstructCache, const char *z3LogInteractionFile); ~Z3Builder(); Z3ASTHandle getTrue(); diff --git a/lib/Solver/Z3Solver.cpp b/lib/Solver/Z3Solver.cpp index 1cbca566..985c143d 100644 --- a/lib/Solver/Z3Solver.cpp +++ b/lib/Solver/Z3Solver.cpp @@ -8,13 +8,37 @@ //===----------------------------------------------------------------------===// #include "klee/Config/config.h" #include "klee/Internal/Support/ErrorHandling.h" +#include "klee/Internal/Support/FileHandling.h" #ifdef ENABLE_Z3 +#include "Z3Solver.h" #include "Z3Builder.h" #include "klee/Constraints.h" #include "klee/Solver.h" #include "klee/SolverImpl.h" #include "klee/util/Assignment.h" #include "klee/util/ExprUtil.h" +#include "llvm/Support/CommandLine.h" +#include "llvm/Support/raw_ostream.h" + +namespace { +// NOTE: Very useful for debugging Z3 behaviour. These files can be given to +// the z3 binary to replay all Z3 API calls using its `-log` option. +llvm::cl::opt<std::string> Z3LogInteractionFile( + "debug-z3-log-api-interaction", llvm::cl::init(""), + llvm::cl::desc("Log API interaction with Z3 to the specified path")); + +llvm::cl::opt<std::string> Z3QueryDumpFile( + "debug-z3-dump-queries", llvm::cl::init(""), + llvm::cl::desc("Dump Z3's representation of the query to the specified path")); + +llvm::cl::opt<bool> Z3ValidateModels( + "debug-z3-validate-models", llvm::cl::init(false), + llvm::cl::desc("When generating Z3 models validate these against the query")); + +llvm::cl::opt<unsigned> + Z3VerbosityLevel("debug-z3-verbosity", llvm::cl::init(0), + llvm::cl::desc("Z3 verbosity level (default=0)")); +} #include "llvm/Support/ErrorHandling.h" @@ -25,6 +49,7 @@ private: Z3Builder *builder; double timeout; SolverRunStatus runStatusCode; + llvm::raw_fd_ostream* dumpedQueriesFile; ::Z3_params solverParameters; // Parameter symbols ::Z3_symbol timeoutParamStrSymbol; @@ -33,6 +58,7 @@ private: const std::vector<const Array *> *objects, std::vector<std::vector<unsigned char> > *values, bool &hasSolution); +bool validateZ3Model(::Z3_solver &theSolver, ::Z3_model &theModel); public: Z3SolverImpl(); @@ -65,18 +91,47 @@ public: }; Z3SolverImpl::Z3SolverImpl() - : builder(new Z3Builder(/*autoClearConstructCache=*/false)), timeout(0.0), - runStatusCode(SOLVER_RUN_STATUS_FAILURE) { + : builder(new Z3Builder( + /*autoClearConstructCache=*/false, + /*z3LogInteractionFileArg=*/Z3LogInteractionFile.size() > 0 + ? Z3LogInteractionFile.c_str() + : NULL)), + timeout(0.0), runStatusCode(SOLVER_RUN_STATUS_FAILURE), + dumpedQueriesFile(0) { assert(builder && "unable to create Z3Builder"); solverParameters = Z3_mk_params(builder->ctx); Z3_params_inc_ref(builder->ctx, solverParameters); timeoutParamStrSymbol = Z3_mk_string_symbol(builder->ctx, "timeout"); setCoreSolverTimeout(timeout); + + if (!Z3QueryDumpFile.empty()) { + std::string error; + dumpedQueriesFile = klee_open_output_file(Z3QueryDumpFile, error); + if (!error.empty()) { + klee_error("Error creating file for dumping Z3 queries: %s", + error.c_str()); + } + klee_message("Dumping Z3 queries to \"%s\"", Z3QueryDumpFile.c_str()); + } + + // Set verbosity + if (Z3VerbosityLevel > 0) { + std::string underlyingString; + llvm::raw_string_ostream ss(underlyingString); + ss << Z3VerbosityLevel; + ss.flush(); + Z3_global_param_set("verbose", underlyingString.c_str()); + } } Z3SolverImpl::~Z3SolverImpl() { Z3_params_dec_ref(builder->ctx, solverParameters); delete builder; + + if (dumpedQueriesFile) { + dumpedQueriesFile->close(); + delete dumpedQueriesFile; + } } Z3Solver::Z3Solver() : Solver(new Z3SolverImpl()) {} @@ -91,10 +146,18 @@ void Z3Solver::setCoreSolverTimeout(double timeout) { char *Z3SolverImpl::getConstraintLog(const Query &query) { std::vector<Z3ASTHandle> assumptions; + // We use a different builder here because we don't want to interfere + // with the solver's builder because it may change the solver builder's + // cache. + // NOTE: The builder does not set `z3LogInteractionFile` to avoid conflicting + // with whatever the solver's builder is set to do. + Z3Builder temp_builder(/*autoClearConstructCache=*/false, + /*z3LogInteractionFile=*/NULL); + for (std::vector<ref<Expr> >::const_iterator it = query.constraints.begin(), ie = query.constraints.end(); it != ie; ++it) { - assumptions.push_back(builder->construct(*it)); + assumptions.push_back(temp_builder.construct(*it)); } ::Z3_ast *assumptionsArray = NULL; int numAssumptions = query.constraints.size(); @@ -111,10 +174,11 @@ char *Z3SolverImpl::getConstraintLog(const Query &query) { // the negation of the equivalent i.e. // ∃ X Constraints(X) ∧ ¬ query(X) Z3ASTHandle formula = Z3ASTHandle( - Z3_mk_not(builder->ctx, builder->construct(query.expr)), builder->ctx); + Z3_mk_not(temp_builder.ctx, temp_builder.construct(query.expr)), + temp_builder.ctx); ::Z3_string result = Z3_benchmark_to_smtlib_string( - builder->ctx, + temp_builder.ctx, /*name=*/"Emited by klee::Z3SolverImpl::getConstraintLog()", /*logic=*/"", /*status=*/"unknown", @@ -125,6 +189,12 @@ char *Z3SolverImpl::getConstraintLog(const Query &query) { if (numAssumptions) free(assumptionsArray); + + // We need to trigger a dereference before the `temp_builder` gets destroyed. + // We do this indirectly by emptying `assumptions` and assigning to + // `formula`. + assumptions.clear(); + formula = Z3ASTHandle(NULL, temp_builder.ctx); // Client is responsible for freeing the returned C-string return strdup(result); } @@ -165,12 +235,15 @@ bool Z3SolverImpl::computeInitialValues( bool Z3SolverImpl::internalRunSolver( const Query &query, const std::vector<const Array *> *objects, std::vector<std::vector<unsigned char> > *values, bool &hasSolution) { + TimerStatIncrementer t(stats::queryTime); - // TODO: Does making a new solver for each query have a performance - // impact vs making one global solver and using push and pop? - // TODO: is the "simple_solver" the right solver to use for - // best performance? - Z3_solver theSolver = Z3_mk_simple_solver(builder->ctx); + // NOTE: Z3 will switch to using a slower solver internally if push/pop are + // used so for now it is likely that creating a new solver each time is the + // right way to go until Z3 changes its behaviour. + // + // TODO: Investigate using a custom tactic as described in + // https://github.com/klee/klee/issues/653 + Z3_solver theSolver = Z3_mk_solver(builder->ctx); Z3_solver_inc_ref(builder->ctx, theSolver); Z3_solver_set_params(builder->ctx, theSolver, solverParameters); @@ -197,6 +270,15 @@ bool Z3SolverImpl::internalRunSolver( builder->ctx, theSolver, Z3ASTHandle(Z3_mk_not(builder->ctx, z3QueryExpr), builder->ctx)); + if (dumpedQueriesFile) { + *dumpedQueriesFile << "; start Z3 query\n"; + *dumpedQueriesFile << Z3_solver_to_string(builder->ctx, theSolver); + *dumpedQueriesFile << "(check-sat)\n"; + *dumpedQueriesFile << "(reset)\n"; + *dumpedQueriesFile << "; end Z3 query\n\n"; + dumpedQueriesFile->flush(); + } + ::Z3_lbool satisfiable = Z3_solver_check(builder->ctx, theSolver); runStatusCode = handleSolverResponse(theSolver, satisfiable, objects, values, hasSolution); @@ -271,6 +353,13 @@ SolverImpl::SolverRunStatus Z3SolverImpl::handleSolverResponse( values->push_back(data); } + // Validate the model if requested + if (Z3ValidateModels) { + bool success = validateZ3Model(theSolver, theModel); + if (!success) + abort(); + } + Z3_model_dec_ref(builder->ctx, theModel); return SolverImpl::SOLVER_RUN_STATUS_SUCCESS_SOLVABLE; } @@ -280,7 +369,8 @@ SolverImpl::SolverRunStatus Z3SolverImpl::handleSolverResponse( case Z3_L_UNDEF: { ::Z3_string reason = ::Z3_solver_get_reason_unknown(builder->ctx, theSolver); - if (strcmp(reason, "timeout") == 0 || strcmp(reason, "canceled") == 0) { + if (strcmp(reason, "timeout") == 0 || strcmp(reason, "canceled") == 0 || + strcmp(reason, "(resource limits reached)") == 0) { return SolverImpl::SOLVER_RUN_STATUS_TIMEOUT; } if (strcmp(reason, "unknown") == 0) { @@ -294,6 +384,54 @@ SolverImpl::SolverRunStatus Z3SolverImpl::handleSolverResponse( } } +bool Z3SolverImpl::validateZ3Model(::Z3_solver &theSolver, ::Z3_model &theModel) { + bool success = true; + ::Z3_ast_vector constraints = + Z3_solver_get_assertions(builder->ctx, theSolver); + Z3_ast_vector_inc_ref(builder->ctx, constraints); + + unsigned size = Z3_ast_vector_size(builder->ctx, constraints); + + for (unsigned index = 0; index < size; ++index) { + Z3ASTHandle constraint = Z3ASTHandle( + Z3_ast_vector_get(builder->ctx, constraints, index), builder->ctx); + + ::Z3_ast rawEvaluatedExpr; + bool successfulEval = + Z3_model_eval(builder->ctx, theModel, constraint, + /*model_completion=*/Z3_TRUE, &rawEvaluatedExpr); + assert(successfulEval && "Failed to evaluate model"); + + // Use handle to do ref-counting. + Z3ASTHandle evaluatedExpr(rawEvaluatedExpr, builder->ctx); + + Z3SortHandle sort = + Z3SortHandle(Z3_get_sort(builder->ctx, evaluatedExpr), builder->ctx); + assert(Z3_get_sort_kind(builder->ctx, sort) == Z3_BOOL_SORT && + "Evaluated expression has wrong sort"); + + Z3_lbool evaluatedValue = + Z3_get_bool_value(builder->ctx, evaluatedExpr); + if (evaluatedValue != Z3_L_TRUE) { + llvm::errs() << "Validating model failed:\n" + << "The expression:\n"; + constraint.dump(); + llvm::errs() << "evaluated to \n"; + evaluatedExpr.dump(); + llvm::errs() << "But should be true\n"; + success = false; + } + } + + if (!success) { + llvm::errs() << "Solver state:\n" << Z3_solver_to_string(builder->ctx, theSolver) << "\n"; + llvm::errs() << "Model:\n" << Z3_model_to_string(builder->ctx, theModel) << "\n"; + } + + Z3_ast_vector_dec_ref(builder->ctx, constraints); + return success; +} + SolverImpl::SolverRunStatus Z3SolverImpl::getOperationStatusCode() { return runStatusCode; } diff --git a/lib/Solver/Z3Solver.h b/lib/Solver/Z3Solver.h new file mode 100644 index 00000000..8dc97e06 --- /dev/null +++ b/lib/Solver/Z3Solver.h @@ -0,0 +1,34 @@ +//===-- Z3Solver.h +//---------------------------------------------------===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + +#ifndef KLEE_Z3SOLVER_H +#define KLEE_Z3SOLVER_H + +#include "klee/Solver.h" + +namespace klee { +/// Z3Solver - A solver complete solver based on Z3 +class Z3Solver : public Solver { +public: + /// Z3Solver - Construct a new Z3Solver. + Z3Solver(); + + /// Get the query in SMT-LIBv2 format. + /// \return A C-style string. The caller is responsible for freeing this. + virtual char *getConstraintLog(const Query &); + + /// setCoreSolverTimeout - Set constraint solver timeout delay to the given + /// value; 0 + /// is off. + virtual void setCoreSolverTimeout(double timeout); +}; +} + +#endif /* KLEE_Z3SOLVER_H */ diff --git a/lib/Support/CMakeLists.txt b/lib/Support/CMakeLists.txt index 4e44fbc6..7145930f 100644 --- a/lib/Support/CMakeLists.txt +++ b/lib/Support/CMakeLists.txt @@ -9,6 +9,7 @@ klee_add_component(kleeSupport CompressionStream.cpp ErrorHandling.cpp + FileHandling.cpp MemoryUsage.cpp PrintVersion.cpp RNG.cpp diff --git a/lib/Support/CompressionStream.cpp b/lib/Support/CompressionStream.cpp index eb208edf..36303878 100644 --- a/lib/Support/CompressionStream.cpp +++ b/lib/Support/CompressionStream.cpp @@ -10,9 +10,11 @@ #include "klee/Config/Version.h" #ifdef HAVE_ZLIB_H #include "klee/Internal/Support/CompressionStream.h" -#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3) +#if (LLVM_VERSION_CODE >= LLVM_VERSION(3, 3) \ + && LLVM_VERSION_CODE <= LLVM_VERSION(3, 4)) #include "llvm/Support/system_error.h" #else +#include "llvm/Support/FileSystem.h" #include <fcntl.h> #include <errno.h> #include <sys/types.h> @@ -27,9 +29,13 @@ compressed_fd_ostream::compressed_fd_ostream(const char *Filename, ErrorInfo = ""; #if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3) // Open file in binary mode +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 5) + std::error_code EC = + llvm::sys::fs::openFileForWrite(Filename, FD, llvm::sys::fs::F_None); +#elif LLVM_VERSION_CODE >= LLVM_VERSION(3, 3) llvm::error_code EC = llvm::sys::fs::openFileForWrite(Filename, FD, llvm::sys::fs::F_Binary); - +#endif if (EC) { ErrorInfo = EC.message(); FD = -1; diff --git a/lib/Support/ErrorHandling.cpp b/lib/Support/ErrorHandling.cpp index 7ca223e5..00647701 100644 --- a/lib/Support/ErrorHandling.cpp +++ b/lib/Support/ErrorHandling.cpp @@ -10,6 +10,7 @@ #include "klee/Internal/Support/ErrorHandling.h" #include "llvm/ADT/StringRef.h" #include "llvm/Support/raw_ostream.h" +#include "llvm/Support/CommandLine.h" #include <stdlib.h> #include <stdio.h> @@ -20,6 +21,7 @@ #include <set> using namespace klee; +using namespace llvm; FILE *klee::klee_warning_file = NULL; FILE *klee::klee_message_file = NULL; @@ -29,6 +31,13 @@ static const char *warningOncePrefix = "WARNING ONCE"; static const char *errorPrefix = "ERROR"; static const char *notePrefix = "NOTE"; +namespace { +cl::opt<bool> WarningsOnlyToFile( + "warnings-only-to-file", cl::init(false), + cl::desc("All warnings will be written to warnings.txt only. If disabled, " + "they are also written on screen.")); +} + static bool shouldSetColor(const char *pfx, const char *msg, const char *prefixToSearchFor) { if (pfx && strcmp(pfx, prefixToSearchFor) == 0) @@ -139,7 +148,7 @@ void klee::klee_error(const char *msg, ...) { void klee::klee_warning(const char *msg, ...) { va_list ap; va_start(ap, msg); - klee_vmessage(warningPrefix, false, msg, ap); + klee_vmessage(warningPrefix, WarningsOnlyToFile, msg, ap); va_end(ap); } @@ -160,7 +169,7 @@ void klee::klee_warning_once(const void *id, const char *msg, ...) { keys.insert(key); va_list ap; va_start(ap, msg); - klee_vmessage(warningOncePrefix, false, msg, ap); + klee_vmessage(warningOncePrefix, WarningsOnlyToFile, msg, ap); va_end(ap); } } diff --git a/lib/Support/FileHandling.cpp b/lib/Support/FileHandling.cpp new file mode 100644 index 00000000..092a1af0 --- /dev/null +++ b/lib/Support/FileHandling.cpp @@ -0,0 +1,43 @@ +//===-- FileHandling.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/Internal/Support/FileHandling.h" +#include "klee/Config/Version.h" +#include "klee/Config/config.h" +#include "klee/Internal/Support/ErrorHandling.h" + +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 5) +#include "llvm/Support/FileSystem.h" +#endif + +namespace klee { + +llvm::raw_fd_ostream *klee_open_output_file(std::string &path, + std::string &error) { + llvm::raw_fd_ostream *f; +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 6) + std::error_code ec; + f = new llvm::raw_fd_ostream(path.c_str(), ec, llvm::sys::fs::F_None); + if (ec) + error = ec.message(); +#elif LLVM_VERSION_CODE >= LLVM_VERSION(3, 5) + f = new llvm::raw_fd_ostream(path.c_str(), error, llvm::sys::fs::F_None); +#elif LLVM_VERSION_CODE >= LLVM_VERSION(3, 4) + f = new llvm::raw_fd_ostream(path.c_str(), error, llvm::sys::fs::F_Binary); +#else + f = new llvm::raw_fd_ostream(path.c_str(), error, + llvm::raw_fd_ostream::F_Binary); +#endif + if (!error.empty()) { + if (f) + delete f; + f = NULL; + } + return f; +} +} |