about summary refs log tree commit diff homepage
diff options
context:
space:
mode:
Diffstat
-rwxr-xr-x.travis/testing-utils.sh6
-rw-r--r--Dockerfile3
-rw-r--r--include/klee/CommandLine.h10
-rw-r--r--include/klee/Internal/Support/ErrorHandling.h6
-rw-r--r--include/klee/Interpreter.h11
-rw-r--r--lib/Basic/CmdLineOptions.cpp13
-rw-r--r--lib/Basic/ConstructSolverChain.cpp102
-rw-r--r--lib/Module/KModule.cpp4
-rw-r--r--lib/Module/Optimize.cpp5
-rw-r--r--lib/Solver/CoreSolver.cpp4
-rw-r--r--runtime/POSIX/klee_init_env.c4
-rw-r--r--test/regression/2016-08-11-entry-point-internalize-pass.c7
-rw-r--r--test/regression/2016-08-12-empty-file.c10
-rw-r--r--tools/klee/main.cpp9
14 files changed, 118 insertions, 76 deletions
diff --git a/.travis/testing-utils.sh b/.travis/testing-utils.sh
index 27bd420d..b2f608db 100755
--- a/.travis/testing-utils.sh
+++ b/.travis/testing-utils.sh
@@ -4,9 +4,9 @@ set -e
 
 if [ "${LLVM_VERSION}" != "2.9" ]; then
     # Using LLVM3.4 all we need is vanilla GoogleTest :)
-    wget https://googletest.googlecode.com/files/gtest-1.7.0.zip
-    unzip gtest-1.7.0.zip
-    cd gtest-1.7.0/
+    wget https://github.com/google/googletest/archive/release-1.7.0.zip
+    unzip release-1.7.0.zip
+    cd googletest-release-1.7.0/
     cmake .
     make
     # Normally I wouldn't do something like this but hey we're running on a temporary virtual machine, so who cares?
diff --git a/Dockerfile b/Dockerfile
index ae5312d5..6ee9a9ac 100644
--- a/Dockerfile
+++ b/Dockerfile
@@ -136,4 +136,7 @@ RUN echo 'export PATH=$PATH:'${BUILD_DIR}'/klee/Release+Asserts/bin' >> /home/kl
 # Link klee to /usr/bin so that it can be used by docker run
 USER root
 RUN for exec in ${BUILD_DIR}/klee/Release+Asserts/bin/* ; do ln -s ${exec} /usr/bin/`basename ${exec}`; done
+
+# Link klee to the libkleeRuntest library needed by docker run
+RUN ln -s ${BUILD_DIR}/klee/Release+Asserts/lib/libkleeRuntest.so /usr/lib/libkleeRuntest.so.1.0
 USER klee
diff --git a/include/klee/CommandLine.h b/include/klee/CommandLine.h
index 00cdeebb..dc69de6e 100644
--- a/include/klee/CommandLine.h
+++ b/include/klee/CommandLine.h
@@ -44,9 +44,17 @@ enum QueryLoggingSolverType
  */
 extern llvm::cl::list<QueryLoggingSolverType> queryLoggingOptions;
 
-enum CoreSolverType { STP_SOLVER, METASMT_SOLVER, DUMMY_SOLVER, Z3_SOLVER };
+enum CoreSolverType {
+  STP_SOLVER,
+  METASMT_SOLVER,
+  DUMMY_SOLVER,
+  Z3_SOLVER,
+  NO_SOLVER
+};
 extern llvm::cl::opt<CoreSolverType> CoreSolverToUse;
 
+extern llvm::cl::opt<CoreSolverType> DebugCrossCheckCoreSolverWith;
+
 #ifdef ENABLE_METASMT
 
 enum MetaSMTBackendType
diff --git a/include/klee/Internal/Support/ErrorHandling.h b/include/klee/Internal/Support/ErrorHandling.h
index 330985e9..29451692 100644
--- a/include/klee/Internal/Support/ErrorHandling.h
+++ b/include/klee/Internal/Support/ErrorHandling.h
@@ -23,7 +23,7 @@ namespace klee {
 extern FILE *klee_warning_file;
 extern FILE *klee_message_file;
 
-/// Print "KLEE: ERROR" followed by the msg in printf format and a
+/// Print "KLEE: ERROR: " followed by the msg in printf format and a
 /// newline on stderr and to warnings.txt, then exit with an error.
 void klee_error(const char *msg, ...)
     __attribute__((format(printf, 1, 2), noreturn));
@@ -37,11 +37,11 @@ void klee_message(const char *msg, ...) __attribute__((format(printf, 1, 2)));
 void klee_message_to_file(const char *msg, ...)
     __attribute__((format(printf, 1, 2)));
 
-/// Print "KLEE: WARNING" followed by the msg in printf format and a
+/// Print "KLEE: WARNING: " followed by the msg in printf format and a
 /// newline on stderr and to warnings.txt.
 void klee_warning(const char *msg, ...) __attribute__((format(printf, 1, 2)));
 
-/// Print "KLEE: WARNING" followed by the msg in printf format and a
+/// Print "KLEE: WARNING: " followed by the msg in printf format and a
 /// newline on stderr and to warnings.txt. However, the warning is only
 /// printed once for each unique (id, msg) pair (as pointers).
 void klee_warning_once(const void *id, const char *msg, ...)
diff --git a/include/klee/Interpreter.h b/include/klee/Interpreter.h
index b40ad0d5..3a4d40b4 100644
--- a/include/klee/Interpreter.h
+++ b/include/klee/Interpreter.h
@@ -51,15 +51,16 @@ public:
   /// registering a module with the interpreter.
   struct ModuleOptions {
     std::string LibraryDir;
+    std::string EntryPoint;
     bool Optimize;
     bool CheckDivZero;
     bool CheckOvershift;
 
-    ModuleOptions(const std::string& _LibraryDir, 
-                  bool _Optimize, bool _CheckDivZero,
-                  bool _CheckOvershift)
-      : LibraryDir(_LibraryDir), Optimize(_Optimize), 
-        CheckDivZero(_CheckDivZero), CheckOvershift(_CheckOvershift) {}
+    ModuleOptions(const std::string &_LibraryDir,
+                  const std::string &_EntryPoint, bool _Optimize,
+                  bool _CheckDivZero, bool _CheckOvershift)
+        : LibraryDir(_LibraryDir), EntryPoint(_EntryPoint), Optimize(_Optimize),
+          CheckDivZero(_CheckDivZero), CheckOvershift(_CheckOvershift) {}
   };
 
   enum LogType
diff --git a/lib/Basic/CmdLineOptions.cpp b/lib/Basic/CmdLineOptions.cpp
index 20c190a5..399c27a2 100644
--- a/lib/Basic/CmdLineOptions.cpp
+++ b/lib/Basic/CmdLineOptions.cpp
@@ -139,6 +139,19 @@ llvm::cl::opt<CoreSolverType> CoreSolverToUse(
                      clEnumValN(Z3_SOLVER, "z3", "Z3" Z3_IS_DEFAULT_STR),
                      clEnumValEnd),
     llvm::cl::init(DEFAULT_CORE_SOLVER));
+
+llvm::cl::opt<CoreSolverType> DebugCrossCheckCoreSolverWith(
+    "debug-crosscheck-core-solver",
+    llvm::cl::desc(
+        "Specifiy a solver to use for cross checking with the core solver"),
+    llvm::cl::values(clEnumValN(STP_SOLVER, "stp", "stp"),
+                     clEnumValN(METASMT_SOLVER, "metasmt", "metaSMT"),
+                     clEnumValN(DUMMY_SOLVER, "dummy", "Dummy solver"),
+                     clEnumValN(Z3_SOLVER, "z3", "Z3"),
+                     clEnumValN(NO_SOLVER, "none",
+                                "Do not cross check (default)"),
+                     clEnumValEnd),
+    llvm::cl::init(NO_SOLVER));
 }
 #undef STP_IS_DEFAULT_STR
 #undef METASMT_IS_DEFAULT_STR
diff --git a/lib/Basic/ConstructSolverChain.cpp b/lib/Basic/ConstructSolverChain.cpp
index 59790551..2df87d51 100644
--- a/lib/Basic/ConstructSolverChain.cpp
+++ b/lib/Basic/ConstructSolverChain.cpp
@@ -1,4 +1,4 @@
-//===-- ConstructSolverChain.cpp ------------------------------------------------*- C++ -*-===//
+//===-- ConstructSolverChain.cpp ------------------------------------++ -*-===//
 //
 //                     The KLEE Symbolic Virtual Machine
 //
@@ -14,69 +14,59 @@
 #include "klee/CommandLine.h"
 #include "llvm/Support/raw_ostream.h"
 
-namespace klee
-{
-        Solver *constructSolverChain(Solver *coreSolver,
-                                     std::string querySMT2LogPath,
-                                     std::string baseSolverQuerySMT2LogPath,
-                                     std::string queryPCLogPath,
-                                     std::string baseSolverQueryPCLogPath)
-	{
-	  Solver *solver = coreSolver;
+namespace klee {
+Solver *constructSolverChain(Solver *coreSolver, std::string querySMT2LogPath,
+                             std::string baseSolverQuerySMT2LogPath,
+                             std::string queryPCLogPath,
+                             std::string baseSolverQueryPCLogPath) {
+  Solver *solver = coreSolver;
 
-	  if (optionIsSet(queryLoggingOptions, SOLVER_PC))
-	  {
-		solver = createPCLoggingSolver(solver,
-					       baseSolverQueryPCLogPath,
-					       MinQueryTimeToLog);
-		llvm::errs() << "Logging queries that reach solver in .pc format to "
-			  << baseSolverQueryPCLogPath.c_str() << "\n";
-	  }
+  if (optionIsSet(queryLoggingOptions, SOLVER_PC)) {
+    solver = createPCLoggingSolver(solver, baseSolverQueryPCLogPath,
+                                   MinQueryTimeToLog);
+    llvm::errs() << "Logging queries that reach solver in .pc format to "
+                 << baseSolverQueryPCLogPath.c_str() << "\n";
+  }
 
-	  if (optionIsSet(queryLoggingOptions, SOLVER_SMTLIB))
-	  {
-		solver = createSMTLIBLoggingSolver(solver,
-						   baseSolverQuerySMT2LogPath,
-						   MinQueryTimeToLog);
-		llvm::errs() << "Logging queries that reach solver in .smt2 format to "
-			  << baseSolverQuerySMT2LogPath.c_str() << "\n";
-	  }
+  if (optionIsSet(queryLoggingOptions, SOLVER_SMTLIB)) {
+    solver = createSMTLIBLoggingSolver(solver, baseSolverQuerySMT2LogPath,
+                                       MinQueryTimeToLog);
+    llvm::errs() << "Logging queries that reach solver in .smt2 format to "
+                 << baseSolverQuerySMT2LogPath.c_str() << "\n";
+  }
 
-	  if (UseFastCexSolver)
-		solver = createFastCexSolver(solver);
+  if (UseFastCexSolver)
+    solver = createFastCexSolver(solver);
 
-	  if (UseCexCache)
-		solver = createCexCachingSolver(solver);
+  if (UseCexCache)
+    solver = createCexCachingSolver(solver);
 
-	  if (UseCache)
-		solver = createCachingSolver(solver);
+  if (UseCache)
+    solver = createCachingSolver(solver);
 
-	  if (UseIndependentSolver)
-		solver = createIndependentSolver(solver);
+  if (UseIndependentSolver)
+    solver = createIndependentSolver(solver);
 
-	  if (DebugValidateSolver)
-		solver = createValidatingSolver(solver, coreSolver);
+  if (DebugValidateSolver)
+    solver = createValidatingSolver(solver, coreSolver);
 
-	  if (optionIsSet(queryLoggingOptions, ALL_PC))
-	  {
-		solver = createPCLoggingSolver(solver,
-					       queryPCLogPath,
-					       MinQueryTimeToLog);
-		llvm::errs() << "Logging all queries in .pc format to "
-			  << queryPCLogPath.c_str() << "\n";
-	  }
+  if (optionIsSet(queryLoggingOptions, ALL_PC)) {
+    solver = createPCLoggingSolver(solver, queryPCLogPath, MinQueryTimeToLog);
+    llvm::errs() << "Logging all queries in .pc format to "
+                 << queryPCLogPath.c_str() << "\n";
+  }
 
-	  if (optionIsSet(queryLoggingOptions, ALL_SMTLIB))
-	  {
-		solver = createSMTLIBLoggingSolver(solver,querySMT2LogPath,
-						   MinQueryTimeToLog);
-		llvm::errs() << "Logging all queries in .smt2 format to "
-			  << querySMT2LogPath.c_str() << "\n";
-	  }
-
-	  return solver;
-	}
+  if (optionIsSet(queryLoggingOptions, ALL_SMTLIB)) {
+    solver =
+        createSMTLIBLoggingSolver(solver, querySMT2LogPath, MinQueryTimeToLog);
+    llvm::errs() << "Logging all queries in .smt2 format to "
+                 << querySMT2LogPath.c_str() << "\n";
+  }
+  if (DebugCrossCheckCoreSolverWith != NO_SOLVER) {
+    Solver *oracleSolver = createCoreSolver(DebugCrossCheckCoreSolverWith);
+    solver = createValidatingSolver(/*s=*/solver, /*oracle=*/oracleSolver);
+  }
 
+  return solver;
+}
 }
-
-
diff --git a/lib/Module/KModule.cpp b/lib/Module/KModule.cpp
index 01165e94..57346a31 100644
--- a/lib/Module/KModule.cpp
+++ b/lib/Module/KModule.cpp
@@ -132,7 +132,7 @@ KModule::~KModule() {
 /***/
 
 namespace llvm {
-extern void Optimize(Module*);
+extern void Optimize(Module *, const std::string &EntryPoint);
 }
 
 // what a hack
@@ -308,7 +308,7 @@ void KModule::prepare(const Interpreter::ModuleOptions &opts,
   pm.run(*module);
 
   if (opts.Optimize)
-    Optimize(module);
+    Optimize(module, opts.EntryPoint);
 #if LLVM_VERSION_CODE < LLVM_VERSION(3, 3)
   // Force importing functions required by intrinsic lowering. Kind of
   // unfortunate clutter when we don't need them but we won't know
diff --git a/lib/Module/Optimize.cpp b/lib/Module/Optimize.cpp
index ce43cd96..3d9c8cc1 100644
--- a/lib/Module/Optimize.cpp
+++ b/lib/Module/Optimize.cpp
@@ -163,7 +163,7 @@ static void AddStandardCompilePasses(PassManager &PM) {
 /// Optimize - Perform link time optimizations. This will run the scalar
 /// optimizations, any loaded plugin-optimization modules, and then the
 /// inter-procedural optimizations if applicable.
-void Optimize(Module* M) {
+void Optimize(Module *M, const std::string &EntryPoint) {
 
   // Instantiate the pass manager to organize the passes.
   PassManager Passes;
@@ -192,7 +192,8 @@ void Optimize(Module* M) {
     // internal.
     if (!DisableInternalize) {
 #if LLVM_VERSION_CODE >= LLVM_VERSION(3, 2)
-      ModulePass *pass = createInternalizePass(std::vector<const char *>(1, "main"));
+      ModulePass *pass = createInternalizePass(
+          std::vector<const char *>(1, EntryPoint.c_str()));
 #else
       ModulePass *pass = createInternalizePass(true);
 #endif
diff --git a/lib/Solver/CoreSolver.cpp b/lib/Solver/CoreSolver.cpp
index 66328f30..783047f8 100644
--- a/lib/Solver/CoreSolver.cpp
+++ b/lib/Solver/CoreSolver.cpp
@@ -83,11 +83,15 @@ Solver *createCoreSolver(CoreSolverType cst) {
     return createDummySolver();
   case Z3_SOLVER:
 #ifdef ENABLE_Z3
+    llvm::errs() << "Using Z3 solver backend\n";
     return new Z3Solver();
 #else
     llvm::errs() << "Not compiled with Z3 support\n";
     return NULL;
 #endif
+  case NO_SOLVER:
+    llvm::errs() << "Invalid solver\n";
+    return NULL;
   default:
     llvm_unreachable("Unsupported CoreSolverType");
   }
diff --git a/runtime/POSIX/klee_init_env.c b/runtime/POSIX/klee_init_env.c
index 7ac9804c..1fa6adea 100644
--- a/runtime/POSIX/klee_init_env.c
+++ b/runtime/POSIX/klee_init_env.c
@@ -112,6 +112,10 @@ usage: (klee_init_env) [options] [program arguments]\n\
                               each with size N\n\
   -sym-stdin <N>            - Make stdin symbolic with size N.\n\
   -sym-stdout               - Make stdout symbolic.\n\
+  -save-all-writes          - Allow write operations to execute as expected\n\
+                              even if they exceed the file size. If set to 0, all\n\
+                              writes exceeding the initial file size are discarded.\n\
+                              Note: file offset is always incremented.\n\
   -max-fail <N>             - Allow up to N injected failures\n\
   -fd-fail                  - Shortcut for '-max-fail 1'\n\n");
   }
diff --git a/test/regression/2016-08-11-entry-point-internalize-pass.c b/test/regression/2016-08-11-entry-point-internalize-pass.c
new file mode 100644
index 00000000..4cd8ff8d
--- /dev/null
+++ b/test/regression/2016-08-11-entry-point-internalize-pass.c
@@ -0,0 +1,7 @@
+// RUN: %llvmgcc %s -emit-llvm -g -O0 -c -o %t.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --output-dir=%t.klee-out --entry-point=entry %t.bc
+
+int entry() {
+  return 0;
+}
diff --git a/test/regression/2016-08-12-empty-file.c b/test/regression/2016-08-12-empty-file.c
new file mode 100644
index 00000000..b9650278
--- /dev/null
+++ b/test/regression/2016-08-12-empty-file.c
@@ -0,0 +1,10 @@
+// RUN: %llvmgcc %s -emit-llvm -g -O0 -c -o %t.bc
+// RUN: rm -rf %t.klee-out
+// RUN: not %klee --output-dir=%t.klee-out %t.bc >%t1.log 2>&1
+// RUN: FileCheck -input-file=%t1.log -check-prefix=CHECK-MAIN-NOT-FOUND %s
+// RUN: rm -rf %t.klee-out
+// RUN: rm -rf %t1.log
+// RUN: not %klee --output-dir=%t.klee-out --posix-runtime %t.bc >%t1.log 2>&1
+// RUN: FileCheck -input-file=%t1.log -check-prefix=CHECK-MAIN-NOT-FOUND %s
+
+// CHECK-MAIN-NOT-FOUND: 'main' function not found in module.
diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp
index 3e469a6e..1eab170f 100644
--- a/tools/klee/main.cpp
+++ b/tools/klee/main.cpp
@@ -669,6 +669,9 @@ static int initEnv(Module *mainModule) {
   */
 
   Function *mainFn = mainModule->getFunction(EntryPoint);
+  if (!mainFn) {
+    klee_error("'%s' function not found in module.", EntryPoint.c_str());
+  }
 
   if (mainFn->arg_size() < 2) {
     klee_error("Cannot handle ""--posix-runtime"" when main() has less than two arguments.\n");
@@ -1276,7 +1279,6 @@ int main(int argc, char **argv, char **envp) {
   }
 #endif
 
-
   if (WithPOSIXRuntime) {
     int r = initEnv(mainModule);
     if (r != 0)
@@ -1284,7 +1286,7 @@ int main(int argc, char **argv, char **envp) {
   }
 
   std::string LibraryDir = KleeHandler::getRunTimeLibraryPath(argv[0]);
-  Interpreter::ModuleOptions Opts(LibraryDir.c_str(),
+  Interpreter::ModuleOptions Opts(LibraryDir.c_str(), EntryPoint,
                                   /*Optimize=*/OptimizeModule,
                                   /*CheckDivZero=*/CheckDivZero,
                                   /*CheckOvershift=*/CheckOvershift);
@@ -1331,8 +1333,7 @@ int main(int argc, char **argv, char **envp) {
   // locale and other data and then calls main.
   Function *mainFn = mainModule->getFunction(EntryPoint);
   if (!mainFn) {
-    llvm::errs() << "'" << EntryPoint << "' function not found in module.\n";
-    return -1;
+    klee_error("'%s' function not found in module.", EntryPoint.c_str());
   }
 
   // FIXME: Change me to std types.
generated by cgit-pink 1.4.1 (git 2.36.1) at 2024-11-27 22:15:14 +0000