about summary refs log tree commit diff homepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--include/klee/CommandLine.h12
-rw-r--r--lib/Basic/CmdLineOptions.cpp7
-rw-r--r--lib/Basic/ConstructSolverChain.cpp8
-rw-r--r--lib/Core/Executor.cpp30
-rw-r--r--test/regression/2015-08-05-invalid-fork.c24
-rw-r--r--tools/klee/main.cpp3
6 files changed, 45 insertions, 39 deletions
diff --git a/include/klee/CommandLine.h b/include/klee/CommandLine.h
index 6a72692d..64930bb2 100644
--- a/include/klee/CommandLine.h
+++ b/include/klee/CommandLine.h
@@ -40,11 +40,7 @@ enum QueryLoggingSolverType
     SOLVER_SMTLIB ///< Log queries passed to solver (optimised) in .smt2 (SMT-LIBv2) format
 };
 
-/* Using cl::list<> instead of cl::bits<> results in quite a bit of ugliness when it comes to checking
- * if an option is set. Unfortunately with gcc4.7 cl::bits<> is broken with LLVM2.9 and I doubt everyone
- * wants to patch their copy of LLVM just for these options.
- */
-extern llvm::cl::list<QueryLoggingSolverType> queryLoggingOptions;
+extern llvm::cl::bits<QueryLoggingSolverType> queryLoggingOptions;
 
 enum CoreSolverType {
   STP_SOLVER,
@@ -70,12 +66,6 @@ extern llvm::cl::opt<klee::MetaSMTBackendType> MetaSMTBackend;
 
 #endif /* ENABLE_METASMT */
 
-//A bit of ugliness so we can use cl::list<> like cl::bits<>, see queryLoggingOptions
-template <typename T>
-static bool optionIsSet(llvm::cl::list<T> &list, T option) {
-    return std::find(list.begin(), list.end(), option) != list.end();
-}
-
 }
 
 #endif	/* KLEE_COMMANDLINE_H */
diff --git a/lib/Basic/CmdLineOptions.cpp b/lib/Basic/CmdLineOptions.cpp
index 54087c21..324f349e 100644
--- a/lib/Basic/CmdLineOptions.cpp
+++ b/lib/Basic/CmdLineOptions.cpp
@@ -65,12 +65,7 @@ CoreSolverOptimizeDivides("solver-optimize-divides",
                  llvm::cl::desc("Optimize constant divides into add/shift/multiplies before passing to core SMT solver (default=off)"),
                  llvm::cl::init(false));
 
-
-/* Using cl::list<> instead of cl::bits<> results in quite a bit of ugliness when it comes to checking
- * if an option is set. Unfortunately with gcc4.7 cl::bits<> is broken with LLVM2.9 and I doubt everyone
- * wants to patch their copy of LLVM just for these options.
- */
-llvm::cl::list<QueryLoggingSolverType> queryLoggingOptions(
+llvm::cl::bits<QueryLoggingSolverType> queryLoggingOptions(
     "use-query-log",
     llvm::cl::desc("Log queries to a file. Multiple options can be specified separated by a comma. By default nothing is logged."),
     llvm::cl::values(
diff --git a/lib/Basic/ConstructSolverChain.cpp b/lib/Basic/ConstructSolverChain.cpp
index d00fcec1..50d81a25 100644
--- a/lib/Basic/ConstructSolverChain.cpp
+++ b/lib/Basic/ConstructSolverChain.cpp
@@ -23,14 +23,14 @@ Solver *constructSolverChain(Solver *coreSolver,
                              std::string baseSolverQueryKQueryLogPath) {
   Solver *solver = coreSolver;
 
-  if (optionIsSet(queryLoggingOptions, SOLVER_KQUERY)) {
+  if (queryLoggingOptions.isSet(SOLVER_KQUERY)) {
     solver = createKQueryLoggingSolver(solver, baseSolverQueryKQueryLogPath,
                                    MinQueryTimeToLog);
     klee_message("Logging queries that reach solver in .kquery format to %s\n",
                  baseSolverQueryKQueryLogPath.c_str());
   }
 
-  if (optionIsSet(queryLoggingOptions, SOLVER_SMTLIB)) {
+  if (queryLoggingOptions.isSet(SOLVER_SMTLIB)) {
     solver = createSMTLIBLoggingSolver(solver, baseSolverQuerySMT2LogPath,
                                        MinQueryTimeToLog);
     klee_message("Logging queries that reach solver in .smt2 format to %s\n",
@@ -55,14 +55,14 @@ Solver *constructSolverChain(Solver *coreSolver,
   if (DebugValidateSolver)
     solver = createValidatingSolver(solver, coreSolver);
 
-  if (optionIsSet(queryLoggingOptions, ALL_KQUERY)) {
+  if (queryLoggingOptions.isSet(ALL_KQUERY)) {
     solver = createKQueryLoggingSolver(solver, queryKQueryLogPath,
                                        MinQueryTimeToLog);
     klee_message("Logging all queries in .kquery format to %s\n",
                  queryKQueryLogPath.c_str());
   }
 
-  if (optionIsSet(queryLoggingOptions, ALL_SMTLIB)) {
+  if (queryLoggingOptions.isSet(ALL_SMTLIB)) {
     solver =
         createSMTLIBLoggingSolver(solver, querySMT2LogPath, MinQueryTimeToLog);
     klee_message("Logging all queries in .smt2 format to %s\n",
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index dd4c8f47..fac68b8d 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -120,7 +120,7 @@ namespace {
     FILE_COMPACT ///
   };
 
-  llvm::cl::list<PrintDebugInstructionsType> DebugPrintInstructions(
+  llvm::cl::bits<PrintDebugInstructionsType> DebugPrintInstructions(
       "debug-print-instructions",
       llvm::cl::desc("Log instructions during execution."),
       llvm::cl::values(
@@ -352,9 +352,9 @@ Executor::Executor(LLVMContext &ctx, const InterpreterOptions &opts,
   this->solver = new TimingSolver(solver, EqualitySubstitution);
   memory = new MemoryManager(&arrayCache);
 
-  if (optionIsSet(DebugPrintInstructions, FILE_ALL) ||
-      optionIsSet(DebugPrintInstructions, FILE_COMPACT) ||
-      optionIsSet(DebugPrintInstructions, FILE_SRC)) {
+  if (DebugPrintInstructions.isSet(FILE_ALL) ||
+      DebugPrintInstructions.isSet(FILE_COMPACT) ||
+      DebugPrintInstructions.isSet(FILE_SRC)) {
     std::string debug_file_name =
         interpreterHandler->getOutputFilename("instructions.txt");
     std::string ErrorInfo;
@@ -1136,19 +1136,19 @@ void Executor::executeGetValue(ExecutionState &state,
 
 void Executor::printDebugInstructions(ExecutionState &state) {
   // check do not print
-  if (DebugPrintInstructions.size() == 0)
+  if (DebugPrintInstructions.getBits() == 0)
 	  return;
 
   llvm::raw_ostream *stream = 0;
-  if (optionIsSet(DebugPrintInstructions, STDERR_ALL) ||
-      optionIsSet(DebugPrintInstructions, STDERR_SRC) ||
-      optionIsSet(DebugPrintInstructions, STDERR_COMPACT))
+  if (DebugPrintInstructions.isSet(STDERR_ALL) ||
+      DebugPrintInstructions.isSet(STDERR_SRC) ||
+      DebugPrintInstructions.isSet(STDERR_COMPACT))
     stream = &llvm::errs();
   else
     stream = &debugLogBuffer;
 
-  if (!optionIsSet(DebugPrintInstructions, STDERR_COMPACT) &&
-      !optionIsSet(DebugPrintInstructions, FILE_COMPACT)) {
+  if (!DebugPrintInstructions.isSet(STDERR_COMPACT) &&
+      !DebugPrintInstructions.isSet(FILE_COMPACT)) {
     (*stream) << "     ";
     state.pc->printFileLine(*stream);
     (*stream) << ":";
@@ -1156,14 +1156,14 @@ void Executor::printDebugInstructions(ExecutionState &state) {
 
   (*stream) << state.pc->info->assemblyLine;
 
-  if (optionIsSet(DebugPrintInstructions, STDERR_ALL) ||
-      optionIsSet(DebugPrintInstructions, FILE_ALL))
+  if (DebugPrintInstructions.isSet(STDERR_ALL) ||
+      DebugPrintInstructions.isSet(FILE_ALL))
     (*stream) << ":" << *(state.pc->inst);
   (*stream) << "\n";
 
-  if (optionIsSet(DebugPrintInstructions, FILE_ALL) ||
-      optionIsSet(DebugPrintInstructions, FILE_COMPACT) ||
-      optionIsSet(DebugPrintInstructions, FILE_SRC)) {
+  if (DebugPrintInstructions.isSet(FILE_ALL) ||
+      DebugPrintInstructions.isSet(FILE_COMPACT) ||
+      DebugPrintInstructions.isSet(FILE_SRC)) {
     debugLogBuffer.flush();
     (*debugInstFile) << debugLogBuffer.str();
     debugBufferString = "";
diff --git a/test/regression/2015-08-05-invalid-fork.c b/test/regression/2015-08-05-invalid-fork.c
new file mode 100644
index 00000000..7c35872c
--- /dev/null
+++ b/test/regression/2015-08-05-invalid-fork.c
@@ -0,0 +1,24 @@
+/* Reported by @kren1 in #262 
+   The test makes sure that the string "Should be printed once" 
+   is printed a single time. 
+*/
+
+// RUN: %llvmgcc %s -emit-llvm -g -O0 -c -o %t.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --output-dir=%t.klee-out %t.bc | FileCheck %s
+
+static int g_10 = 0x923607A9L;
+
+int main(int argc, char* argv[]) {
+  klee_make_symbolic(&g_10,sizeof(g_10), "g_10");
+  if (g_10 < (int)0x923607A9L) klee_silent_exit(0);
+  if (g_10 > (int)0x923607A9L) klee_silent_exit(0);
+
+  int b = 2;
+  int i = g_10 % (1 % g_10);
+  i || b;
+  printf("Should be printed once\n");
+  // CHECK: Should be printed once
+  // CHECK-NOT: Should be printed once
+  return 0;
+}
diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp
index 586c13ec..8e3431d3 100644
--- a/tools/klee/main.cpp
+++ b/tools/klee/main.cpp
@@ -1073,9 +1073,6 @@ static llvm::Module *linkWithUclibc(llvm::Module *mainModule, StringRef libDir)
   replaceOrRenameFunction(mainModule, "__libc_open", "open");
   replaceOrRenameFunction(mainModule, "__libc_fcntl", "fcntl");
 
-  // Take care of fortified functions
-  replaceOrRenameFunction(mainModule, "__fprintf_chk", "fprintf");
-
   // XXX we need to rearchitect so this can also be used with
   // programs externally linked with uclibc.
generated by cgit-pink 1.4.1 (git 2.36.1) at 2025-05-04 20:07:57 +0000