about summary refs log tree commit diff homepage
diff options
context:
space:
mode:
-rw-r--r--include/klee/Internal/Module/KInstruction.h8
-rw-r--r--lib/Core/Executor.cpp32
-rw-r--r--lib/Core/ExternalDispatcher.cpp3
-rw-r--r--lib/Module/KInstruction.cpp7
-rw-r--r--lib/Module/ModuleUtil.cpp8
-rw-r--r--lib/Solver/CoreSolver.cpp19
-rw-r--r--lib/Support/ErrorHandling.cpp13
-rw-r--r--test/Feature/LinkLLVMLib.c2
-rw-r--r--test/Feature/MemoryLimit.c6
-rw-r--r--test/Feature/Realloc.c2
-rw-r--r--test/regression/2017-02-21-pathOS-id.c19
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 &current, 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;
+}