diff options
-rw-r--r-- | include/klee/Internal/Module/KInstruction.h | 8 | ||||
-rw-r--r-- | lib/Core/Executor.cpp | 32 | ||||
-rw-r--r-- | lib/Core/ExternalDispatcher.cpp | 3 | ||||
-rw-r--r-- | lib/Module/KInstruction.cpp | 7 | ||||
-rw-r--r-- | lib/Module/ModuleUtil.cpp | 8 | ||||
-rw-r--r-- | lib/Solver/CoreSolver.cpp | 19 | ||||
-rw-r--r-- | lib/Support/ErrorHandling.cpp | 13 | ||||
-rw-r--r-- | test/Feature/LinkLLVMLib.c | 2 | ||||
-rw-r--r-- | test/Feature/MemoryLimit.c | 6 | ||||
-rw-r--r-- | test/Feature/Realloc.c | 2 | ||||
-rw-r--r-- | test/regression/2017-02-21-pathOS-id.c | 19 |
11 files changed, 80 insertions, 39 deletions
diff --git a/include/klee/Internal/Module/KInstruction.h b/include/klee/Internal/Module/KInstruction.h index 62f514ff..1cad98fd 100644 --- a/include/klee/Internal/Module/KInstruction.h +++ b/include/klee/Internal/Module/KInstruction.h @@ -11,7 +11,11 @@ #define KLEE_KINSTRUCTION_H #include "klee/Config/Version.h" +#include "klee/Internal/Module/InstructionInfoTable.h" + #include "llvm/Support/DataTypes.h" +#include "llvm/Support/raw_ostream.h" + #include <vector> namespace llvm { @@ -39,7 +43,9 @@ namespace klee { unsigned dest; public: - virtual ~KInstruction(); + virtual ~KInstruction(); + void printFileLine(llvm::raw_ostream &); + }; struct KGEPInstruction : KInstruction { diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index c5d294fb..95812dd7 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -976,14 +976,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 +1239,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 +1468,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) { diff --git a/lib/Core/ExternalDispatcher.cpp b/lib/Core/ExternalDispatcher.cpp index 01c5f935..984e3ab2 100644 --- a/lib/Core/ExternalDispatcher.cpp +++ b/lib/Core/ExternalDispatcher.cpp @@ -207,10 +207,11 @@ Function *ExternalDispatcher::createDispatcher(Function *target, Instruction *in std::vector<LLVM_TYPE_Q Type*> nullary; + // MCJIT functions need unique names, or wrong function can be called Function *dispatcher = Function::Create(FunctionType::get(Type::getVoidTy(ctx), nullary, false), GlobalVariable::ExternalLinkage, - "", + "dispatcher_" + target->getName().str(), dispatchModule); 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/ModuleUtil.cpp b/lib/Module/ModuleUtil.cpp index 94a37e08..83dc5045 100644 --- a/lib/Module/ModuleUtil.cpp +++ b/lib/Module/ModuleUtil.cpp @@ -266,9 +266,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; @@ -412,10 +412,10 @@ Module *klee::linkWithLibrary(Module *module, } else if (magic.is_object()) { OwningPtr<object::Binary> obj; - if (object::ObjectFile *o = dyn_cast<object::ObjectFile>(obj.get())) { + 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/Solver/CoreSolver.cpp b/lib/Solver/CoreSolver.cpp index 783047f8..d36a3219 100644 --- a/lib/Solver/CoreSolver.cpp +++ b/lib/Solver/CoreSolver.cpp @@ -8,6 +8,7 @@ //===----------------------------------------------------------------------===// #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" @@ -51,10 +52,10 @@ static klee::Solver *handleMetaSMT() { UseForkedCoreSolver, CoreSolverOptimizeDivides); break; default: - llvm_unreachable("Unrecognised metasmt backend"); + llvm_unreachable("Unrecognised MetaSMT backend"); break; }; - llvm::errs() << "Starting MetaSMTSolver(" << backend << ") ...\n"; + klee_message("Starting MetaSMTSolver(%s)", backend.c_str()); return coreSolver; } #endif /* ENABLE_METASMT */ @@ -65,32 +66,32 @@ 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"; + klee_message("Using MetaSMT solver backend"); return handleMetaSMT(); #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/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/test/Feature/LinkLLVMLib.c b/test/Feature/LinkLLVMLib.c index 95437094..34931409 100644 --- a/test/Feature/LinkLLVMLib.c +++ b/test/Feature/LinkLLVMLib.c @@ -3,7 +3,7 @@ // // RUN: %llvmgcc %s -g -emit-llvm -O0 -c -o %t2.bc -DLINK_LLVM_LIB_TEST_EXEC // RUN: rm -rf %t.klee-out -// RUN: %klee --link-llvm-lib %t1.a --output-dir=%t.klee-out --emit-all-errors %t2.bc 2>&1 | FileCheck %s +// RUN: %klee --link-llvm-lib %t1.a --output-dir=%t.klee-out --emit-all-errors --warnings-only-to-file=false %t2.bc 2>&1 | FileCheck %s #ifdef LINK_LLVM_LIB_TEST_EXEC extern void printint(int d); diff --git a/test/Feature/MemoryLimit.c b/test/Feature/MemoryLimit.c index fb9f2c86..ce4bc00f 100644 --- a/test/Feature/MemoryLimit.c +++ b/test/Feature/MemoryLimit.c @@ -4,17 +4,17 @@ // RUN: %llvmgcc -emit-llvm -DLITTLE_ALLOC -g -c %s -o %t.little.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --max-memory=20 %t.little.bc > %t.little.log 2> %t.little.err +// RUN: %klee --output-dir=%t.klee-out --max-memory=20 %t.little.bc > %t.little.log // RUN: not grep -q "MALLOC FAILED" %t.little.log // RUN: not grep -q "DONE" %t.little.log -// RUN: grep "WARNING: killing 1 states (over memory cap)" %t.little.err +// RUN: grep "WARNING: killing 1 states (over memory cap)" %t.klee-out/warnings.txt // RUN: %llvmgcc -emit-llvm -g -c %s -o %t.big.bc // RUN: rm -rf %t.klee-out // RUN: %klee --output-dir=%t.klee-out --max-memory=20 %t.big.bc > %t.big.log 2> %t.big.err // RUN: not grep -q "MALLOC FAILED" %t.big.log // RUN: not grep -q "DONE" %t.big.log -// RUN: grep "WARNING: killing 1 states (over memory cap)" %t.big.err +// RUN: grep "WARNING: killing 1 states (over memory cap)" %t.klee-out/warnings.txt #include <stdlib.h> #include <stdio.h> diff --git a/test/Feature/Realloc.c b/test/Feature/Realloc.c index 76016fb7..0a97dd78 100644 --- a/test/Feature/Realloc.c +++ b/test/Feature/Realloc.c @@ -1,6 +1,6 @@ // RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --exit-on-error %t1.bc 2>&1 | FileCheck %s +// RUN: %klee --output-dir=%t.klee-out --exit-on-error --warnings-only-to-file=false %t1.bc 2>&1 | FileCheck %s #include <assert.h> #include <stdlib.h> diff --git a/test/regression/2017-02-21-pathOS-id.c b/test/regression/2017-02-21-pathOS-id.c new file mode 100644 index 00000000..d3bffbe0 --- /dev/null +++ b/test/regression/2017-02-21-pathOS-id.c @@ -0,0 +1,19 @@ +// RUN: %llvmgcc %s -emit-llvm -g -O0 -c -o %t.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out -write-paths %t.bc 2> %t.log +// RUN: cat %t.klee-out/test000001.path | wc -l | grep -q 1 +// RUN: cat %t.klee-out/test000002.path | wc -l | grep -q 1 +// RUN: cat %t.klee-out/test000003.path | wc -l | grep -q 1 +// RUN: cat %t.klee-out/test000004.path | wc -l | grep -q 1 +int main(){ + int a, b; + klee_make_symbolic (&a, sizeof(int), "a"); + klee_make_symbolic (&b, sizeof(int), "b"); + klee_assume(a<2); + klee_assume(a>=0); + malloc(a); + if(b){ + b++;//do something + } + return b; +} |