run VerifierPass after optimization and instrumentation

4 files changed, 27 insertions, 29 deletions

diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index 3a5202ac..70561216 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -527,6 +527,7 @@ Executor::setModule(std::vector<std::unique_ptr<llvm::Module>> &modules,
   preservedFunctions.push_back("memmove");
 
   kmodule->optimiseAndPrepare(opts, preservedFunctions);
+  kmodule->checkModule();
 
   // 4.) Manifest the module
   kmodule->manifest(interpreterHandler, StatsTracker::useStatistics());
diff --git a/lib/Module/KModule.cpp b/lib/Module/KModule.cpp
index 4817b6cc..3ce95a9e 100644
--- a/lib/Module/KModule.cpp
+++ b/lib/Module/KModule.cpp
@@ -41,6 +41,7 @@
 #include "llvm/Support/CallSite.h"
 #else
 #include "llvm/IR/CallSite.h"
+#include "llvm/IR/Verifier.h"
 #include "llvm/Linker/Linker.h"
 #endif
 
@@ -105,6 +106,12 @@ namespace {
   DebugPrintEscapingFunctions("debug-print-escaping-functions", 
                               cl::desc("Print functions whose address is taken (default=false)"),
 			      cl::cat(ModuleCat));
+
+  // Don't run VerifierPass when checking module
+  cl::opt<bool>
+  DontVerify("disable-verify",
+             cl::desc("Do not verify the module integrity (default=false)"),
+             cl::init(false), cl::cat(klee::ModuleCat));
 }
 
 /***/
@@ -282,19 +289,9 @@ void KModule::optimiseAndPrepare(
   case eSwitchTypeLLVM:  pm3.add(createLowerSwitchPass()); break;
   default: klee_error("invalid --switch-type");
   }
-  InstructionOperandTypeCheckPass *operandTypeCheckPass =
-      new InstructionOperandTypeCheckPass();
   pm3.add(new IntrinsicCleanerPass(*targetData));
   pm3.add(new PhiCleanerPass());
-  pm3.add(operandTypeCheckPass);
   pm3.run(*module);
-
-  // Enforce the operand type invariants that the Executor expects.  This
-  // implicitly depends on the "Scalarizer" pass to be run in order to succeed
-  // in the presence of vector instructions.
-  if (!operandTypeCheckPass->checkPassed()) {
-    klee_error("Unexpected instruction operand types detected");
-  }
 }
 
 void KModule::manifest(InterpreterHandler *ih, bool forceSourceOutput) {
@@ -360,6 +357,24 @@ void KModule::manifest(InterpreterHandler *ih, bool forceSourceOutput) {
   }
 }
 
+void KModule::checkModule() {
+  InstructionOperandTypeCheckPass *operandTypeCheckPass =
+      new InstructionOperandTypeCheckPass();
+
+  LegacyLLVMPassManagerTy pm;
+  if (!DontVerify)
+    pm.add(createVerifierPass());
+  pm.add(operandTypeCheckPass);
+  pm.run(*module);
+
+  // Enforce the operand type invariants that the Executor expects.  This
+  // implicitly depends on the "Scalarizer" pass to be run in order to succeed
+  // in the presence of vector instructions.
+  if (!operandTypeCheckPass->checkPassed()) {
+    klee_error("Unexpected instruction operand types detected");
+  }
+}
+
 KConstant* KModule::getKConstant(const Constant *c) {
   auto it = constantMap.find(c);
   if (it != constantMap.end())
diff --git a/lib/Module/ModuleUtil.cpp b/lib/Module/ModuleUtil.cpp
index 399e5577..5c9aad1a 100644
--- a/lib/Module/ModuleUtil.cpp
+++ b/lib/Module/ModuleUtil.cpp
@@ -33,12 +33,10 @@
 #include "llvm/Support/SourceMgr.h"
 
 #if LLVM_VERSION_CODE < LLVM_VERSION(3, 5)
-#include "llvm/Analysis/Verifier.h"
 #include "llvm/Assembly/AssemblyAnnotationWriter.h"
 #include "llvm/Linker.h"
 #else
 #include "llvm/IR/AssemblyAnnotationWriter.h"
-#include "llvm/IR/Verifier.h"
 #include "llvm/Linker/Linker.h"
 #endif
 
@@ -599,9 +597,3 @@ std::unique_ptr<llvm::Module> module(ParseIR(Buffer.take(), Err, context));
   modules.push_back(std::move(module));
   return true;
 }
-
-void klee::checkModule(llvm::Module *m) {
-  LegacyLLVMPassManagerTy pm;
-  pm.add(createVerifierPass());
-  pm.run(*m);
-}
diff --git a/lib/Module/Optimize.cpp b/lib/Module/Optimize.cpp
index d55fd0c3..22b9a16a 100644
--- a/lib/Module/Optimize.cpp
+++ b/lib/Module/Optimize.cpp
@@ -56,12 +56,6 @@
 
 using namespace llvm;
 
-// Don't verify at the end
-static cl::opt<bool>
-    DontVerify("disable-verify", cl::ReallyHidden,
-               cl::desc("Do not verify the module integrity (default=false)"),
-               cl::init(false), cl::cat(klee::ModuleCat));
-
 static cl::opt<bool>
     DisableInline("disable-inlining",
                   cl::desc("Do not run the inliner pass (default=false)"),
@@ -74,7 +68,7 @@ static cl::opt<bool> DisableInternalize(
 
 static cl::opt<bool> VerifyEach(
     "verify-each",
-    cl::desc("Verify intermediate results of all passes (default=false)"),
+    cl::desc("Verify intermediate results of all optimization passes (default=false)"),
     cl::init(false),
     cl::cat(klee::ModuleCat));
 
@@ -317,10 +311,6 @@ void Optimize(Module *M, llvm::ArrayRef<const char *> preservedFunctions) {
   addPass(Passes, createAggressiveDCEPass());
   addPass(Passes, createGlobalDCEPass());
 
-  // Make sure everything is still good.
-  if (!DontVerify)
-    Passes.add(createVerifierPass());
-
   // Run our queue of passes all at once now, efficiently.
   Passes.run(*M);
 }