Replace assertions of types on LLVM instructions in the Executor with a

pass that checks these assertions. This improves several things.

* This pass provides more friendly messages than assertions in that it
just emits a warning and carries on checking the rest of the
instructions.

* The takes the checks outside of the Executor's hot path and so avoids
checking the same instruction multiple times. Now each instruction
is only checked once just before execution starts.

The disadvantage of this approach is the check for invariants we expect
to hold have been pulled far away from where we expect them to hold.
After discussion with @ccadar and @MartinNowack it was decided we will
take this hit to readability for better performance and simpler code in
the Executor.

5 files changed, 213 insertions, 110 deletions

diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index 96181a3d..884f388d 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -1922,12 +1922,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
 
     // Special instructions
   case Instruction::Select: {
-    assert(i->getOperand(0)->getType()->isIntegerTy() &&
-           "Invalid operand type");
-    assert((i->getOperand(1)->getType() == i->getOperand(2)->getType()) &&
-           "true and false operands to Select have mismatching types");
-    // NOTE: We are do not check that operands 1 and 2 are not of vector type
-    // because the scalarizer pass might not remove these.
+    // NOTE: It is not required that operands 1 and 2 be of scalar type.
     ref<Expr> cond = eval(ki, 0, state).value;
     ref<Expr> tExpr = eval(ki, 1, state).value;
     ref<Expr> fExpr = eval(ki, 2, state).value;
@@ -1943,10 +1938,6 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
     // Arithmetic / logical
 
   case Instruction::Add: {
-    assert(i->getOperand(0)->getType()->isIntegerTy() &&
-           "Invalid operand type");
-    assert(i->getOperand(1)->getType()->isIntegerTy() &&
-           "Invalid operand type");
     ref<Expr> left = eval(ki, 0, state).value;
     ref<Expr> right = eval(ki, 1, state).value;
     bindLocal(ki, state, AddExpr::create(left, right));
@@ -1954,10 +1945,6 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
   }
 
   case Instruction::Sub: {
-    assert(i->getOperand(0)->getType()->isIntegerTy() &&
-           "Invalid operand type");
-    assert(i->getOperand(1)->getType()->isIntegerTy() &&
-           "Invalid operand type");
     ref<Expr> left = eval(ki, 0, state).value;
     ref<Expr> right = eval(ki, 1, state).value;
     bindLocal(ki, state, SubExpr::create(left, right));
@@ -1965,10 +1952,6 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
   }
  
   case Instruction::Mul: {
-    assert(i->getOperand(0)->getType()->isIntegerTy() &&
-           "Invalid operand type");
-    assert(i->getOperand(1)->getType()->isIntegerTy() &&
-           "Invalid operand type");
     ref<Expr> left = eval(ki, 0, state).value;
     ref<Expr> right = eval(ki, 1, state).value;
     bindLocal(ki, state, MulExpr::create(left, right));
@@ -1976,10 +1959,6 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
   }
 
   case Instruction::UDiv: {
-    assert(i->getOperand(0)->getType()->isIntegerTy() &&
-           "Invalid operand type");
-    assert(i->getOperand(1)->getType()->isIntegerTy() &&
-           "Invalid operand type");
     ref<Expr> left = eval(ki, 0, state).value;
     ref<Expr> right = eval(ki, 1, state).value;
     ref<Expr> result = UDivExpr::create(left, right);
@@ -1988,10 +1967,6 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
   }
 
   case Instruction::SDiv: {
-    assert(i->getOperand(0)->getType()->isIntegerTy() &&
-           "Invalid operand type");
-    assert(i->getOperand(1)->getType()->isIntegerTy() &&
-           "Invalid operand type");
     ref<Expr> left = eval(ki, 0, state).value;
     ref<Expr> right = eval(ki, 1, state).value;
     ref<Expr> result = SDivExpr::create(left, right);
@@ -2000,10 +1975,6 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
   }
 
   case Instruction::URem: {
-    assert(i->getOperand(0)->getType()->isIntegerTy() &&
-           "Invalid operand type");
-    assert(i->getOperand(1)->getType()->isIntegerTy() &&
-           "Invalid operand type");
     ref<Expr> left = eval(ki, 0, state).value;
     ref<Expr> right = eval(ki, 1, state).value;
     ref<Expr> result = URemExpr::create(left, right);
@@ -2012,10 +1983,6 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
   }
 
   case Instruction::SRem: {
-    assert(i->getOperand(0)->getType()->isIntegerTy() &&
-           "Invalid operand type");
-    assert(i->getOperand(1)->getType()->isIntegerTy() &&
-           "Invalid operand type");
     ref<Expr> left = eval(ki, 0, state).value;
     ref<Expr> right = eval(ki, 1, state).value;
     ref<Expr> result = SRemExpr::create(left, right);
@@ -2024,10 +1991,6 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
   }
 
   case Instruction::And: {
-    assert(i->getOperand(0)->getType()->isIntegerTy() &&
-           "Invalid operand type");
-    assert(i->getOperand(1)->getType()->isIntegerTy() &&
-           "Invalid operand type");
     ref<Expr> left = eval(ki, 0, state).value;
     ref<Expr> right = eval(ki, 1, state).value;
     ref<Expr> result = AndExpr::create(left, right);
@@ -2036,10 +1999,6 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
   }
 
   case Instruction::Or: {
-    assert(i->getOperand(0)->getType()->isIntegerTy() &&
-           "Invalid operand type");
-    assert(i->getOperand(1)->getType()->isIntegerTy() &&
-           "Invalid operand type");
     ref<Expr> left = eval(ki, 0, state).value;
     ref<Expr> right = eval(ki, 1, state).value;
     ref<Expr> result = OrExpr::create(left, right);
@@ -2048,10 +2007,6 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
   }
 
   case Instruction::Xor: {
-    assert(i->getOperand(0)->getType()->isIntegerTy() &&
-           "Invalid operand type");
-    assert(i->getOperand(1)->getType()->isIntegerTy() &&
-           "Invalid operand type");
     ref<Expr> left = eval(ki, 0, state).value;
     ref<Expr> right = eval(ki, 1, state).value;
     ref<Expr> result = XorExpr::create(left, right);
@@ -2060,10 +2015,6 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
   }
 
   case Instruction::Shl: {
-    assert(i->getOperand(0)->getType()->isIntegerTy() &&
-           "Invalid operand type");
-    assert(i->getOperand(1)->getType()->isIntegerTy() &&
-           "Invalid operand type");
     ref<Expr> left = eval(ki, 0, state).value;
     ref<Expr> right = eval(ki, 1, state).value;
     ref<Expr> result = ShlExpr::create(left, right);
@@ -2072,10 +2023,6 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
   }
 
   case Instruction::LShr: {
-    assert(i->getOperand(0)->getType()->isIntegerTy() &&
-           "Invalid operand type");
-    assert(i->getOperand(1)->getType()->isIntegerTy() &&
-           "Invalid operand type");
     ref<Expr> left = eval(ki, 0, state).value;
     ref<Expr> right = eval(ki, 1, state).value;
     ref<Expr> result = LShrExpr::create(left, right);
@@ -2084,10 +2031,6 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
   }
 
   case Instruction::AShr: {
-    assert(i->getOperand(0)->getType()->isIntegerTy() &&
-           "Invalid operand type");
-    assert(i->getOperand(1)->getType()->isIntegerTy() &&
-           "Invalid operand type");
     ref<Expr> left = eval(ki, 0, state).value;
     ref<Expr> right = eval(ki, 1, state).value;
     ref<Expr> result = AShrExpr::create(left, right);
@@ -2098,12 +2041,6 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
     // Compare
 
   case Instruction::ICmp: {
-    assert((i->getOperand(0)->getType()->isIntegerTy() ||
-            i->getOperand(0)->getType()->isPointerTy()) &&
-           "Invalid operand type");
-    assert((i->getOperand(1)->getType()->isIntegerTy() ||
-            i->getOperand(1)->getType()->isPointerTy()) &&
-           "Invalid operand type");
     CmpInst *ci = cast<CmpInst>(i);
     ICmpInst *ii = cast<ICmpInst>(ci);
 
@@ -2243,8 +2180,6 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
 
     // Conversion
   case Instruction::Trunc: {
-    assert(i->getOperand(0)->getType()->isIntegerTy() &&
-           "Invalid operand type");
     CastInst *ci = cast<CastInst>(i);
     ref<Expr> result = ExtractExpr::create(eval(ki, 0, state).value,
                                            0,
@@ -2253,8 +2188,6 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
     break;
   }
   case Instruction::ZExt: {
-    assert(i->getOperand(0)->getType()->isIntegerTy() &&
-           "Invalid operand type");
     CastInst *ci = cast<CastInst>(i);
     ref<Expr> result = ZExtExpr::create(eval(ki, 0, state).value,
                                         getWidthForLLVMType(ci->getType()));
@@ -2262,8 +2195,6 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
     break;
   }
   case Instruction::SExt: {
-    assert(i->getOperand(0)->getType()->isIntegerTy() &&
-           "Invalid operand type");
     CastInst *ci = cast<CastInst>(i);
     ref<Expr> result = SExtExpr::create(eval(ki, 0, state).value,
                                         getWidthForLLVMType(ci->getType()));
@@ -2272,8 +2203,6 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
   }
 
   case Instruction::IntToPtr: {
-    assert(i->getOperand(0)->getType()->isIntegerTy() &&
-           "Invalid operand type");
     CastInst *ci = cast<CastInst>(i);
     Expr::Width pType = getWidthForLLVMType(ci->getType());
     ref<Expr> arg = eval(ki, 0, state).value;
@@ -2281,8 +2210,6 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
     break;
   }
   case Instruction::PtrToInt: {
-    assert(i->getOperand(0)->getType()->isPointerTy() &&
-           "Invalid operand type");
     CastInst *ci = cast<CastInst>(i);
     Expr::Width iType = getWidthForLLVMType(ci->getType());
     ref<Expr> arg = eval(ki, 0, state).value;
@@ -2299,10 +2226,6 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
     // Floating point instructions
 
   case Instruction::FAdd: {
-    assert(i->getOperand(0)->getType()->isFloatingPointTy() &&
-           "Invalid operand type");
-    assert(i->getOperand(1)->getType()->isFloatingPointTy() &&
-           "Invalid operand type");
     ref<ConstantExpr> left = toConstant(state, eval(ki, 0, state).value,
                                         "floating point");
     ref<ConstantExpr> right = toConstant(state, eval(ki, 1, state).value,
@@ -2323,10 +2246,6 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
   }
 
   case Instruction::FSub: {
-    assert(i->getOperand(0)->getType()->isFloatingPointTy() &&
-           "Invalid operand type");
-    assert(i->getOperand(1)->getType()->isFloatingPointTy() &&
-           "Invalid operand type");
     ref<ConstantExpr> left = toConstant(state, eval(ki, 0, state).value,
                                         "floating point");
     ref<ConstantExpr> right = toConstant(state, eval(ki, 1, state).value,
@@ -2346,10 +2265,6 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
   }
 
   case Instruction::FMul: {
-    assert(i->getOperand(0)->getType()->isFloatingPointTy() &&
-           "Invalid operand type");
-    assert(i->getOperand(1)->getType()->isFloatingPointTy() &&
-           "Invalid operand type");
     ref<ConstantExpr> left = toConstant(state, eval(ki, 0, state).value,
                                         "floating point");
     ref<ConstantExpr> right = toConstant(state, eval(ki, 1, state).value,
@@ -2370,10 +2285,6 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
   }
 
   case Instruction::FDiv: {
-    assert(i->getOperand(0)->getType()->isFloatingPointTy() &&
-           "Invalid operand type");
-    assert(i->getOperand(1)->getType()->isFloatingPointTy() &&
-           "Invalid operand type");
     ref<ConstantExpr> left = toConstant(state, eval(ki, 0, state).value,
                                         "floating point");
     ref<ConstantExpr> right = toConstant(state, eval(ki, 1, state).value,
@@ -2394,10 +2305,6 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
   }
 
   case Instruction::FRem: {
-    assert(i->getOperand(0)->getType()->isFloatingPointTy() &&
-           "Invalid operand type");
-    assert(i->getOperand(1)->getType()->isFloatingPointTy() &&
-           "Invalid operand type");
     ref<ConstantExpr> left = toConstant(state, eval(ki, 0, state).value,
                                         "floating point");
     ref<ConstantExpr> right = toConstant(state, eval(ki, 1, state).value,
@@ -2418,8 +2325,6 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
   }
 
   case Instruction::FPTrunc: {
-    assert(i->getOperand(0)->getType()->isFloatingPointTy() &&
-           "Invalid operand type");
     FPTruncInst *fi = cast<FPTruncInst>(i);
     Expr::Width resultType = getWidthForLLVMType(fi->getType());
     ref<ConstantExpr> arg = toConstant(state, eval(ki, 0, state).value,
@@ -2441,8 +2346,6 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
   }
 
   case Instruction::FPExt: {
-    assert(i->getOperand(0)->getType()->isFloatingPointTy() &&
-           "Invalid operand type");
     FPExtInst *fi = cast<FPExtInst>(i);
     Expr::Width resultType = getWidthForLLVMType(fi->getType());
     ref<ConstantExpr> arg = toConstant(state, eval(ki, 0, state).value,
@@ -2463,8 +2366,6 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
   }
 
   case Instruction::FPToUI: {
-    assert(i->getOperand(0)->getType()->isFloatingPointTy() &&
-           "Invalid operand type");
     FPToUIInst *fi = cast<FPToUIInst>(i);
     Expr::Width resultType = getWidthForLLVMType(fi->getType());
     ref<ConstantExpr> arg = toConstant(state, eval(ki, 0, state).value,
@@ -2486,8 +2387,6 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
   }
 
   case Instruction::FPToSI: {
-    assert(i->getOperand(0)->getType()->isFloatingPointTy() &&
-           "Invalid operand type");
     FPToSIInst *fi = cast<FPToSIInst>(i);
     Expr::Width resultType = getWidthForLLVMType(fi->getType());
     ref<ConstantExpr> arg = toConstant(state, eval(ki, 0, state).value,
@@ -2509,8 +2408,6 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
   }
 
   case Instruction::UIToFP: {
-    assert(i->getOperand(0)->getType()->isIntegerTy() &&
-           "Invalid operand type");
     UIToFPInst *fi = cast<UIToFPInst>(i);
     Expr::Width resultType = getWidthForLLVMType(fi->getType());
     ref<ConstantExpr> arg = toConstant(state, eval(ki, 0, state).value,
@@ -2527,8 +2424,6 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
   }
 
   case Instruction::SIToFP: {
-    assert(i->getOperand(0)->getType()->isIntegerTy() &&
-           "Invalid operand type");
     SIToFPInst *fi = cast<SIToFPInst>(i);
     Expr::Width resultType = getWidthForLLVMType(fi->getType());
     ref<ConstantExpr> arg = toConstant(state, eval(ki, 0, state).value,
@@ -2545,10 +2440,6 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
   }
 
   case Instruction::FCmp: {
-    assert(i->getOperand(0)->getType()->isFloatingPointTy() &&
-           "Invalid operand type");
-    assert(i->getOperand(1)->getType()->isFloatingPointTy() &&
-           "Invalid operand type");
     FCmpInst *fi = cast<FCmpInst>(i);
     ref<ConstantExpr> left = toConstant(state, eval(ki, 0, state).value,
                                         "floating point");
diff --git a/lib/Module/CMakeLists.txt b/lib/Module/CMakeLists.txt
index fc481780..c1a5d809 100644
--- a/lib/Module/CMakeLists.txt
+++ b/lib/Module/CMakeLists.txt
@@ -9,6 +9,7 @@
 klee_add_component(kleeModule
   Checks.cpp
   InstructionInfoTable.cpp
+  InstructionOperandTypeCheckPass.cpp
   IntrinsicCleaner.cpp
   KInstruction.cpp
   KModule.cpp
diff --git a/lib/Module/InstructionOperandTypeCheckPass.cpp b/lib/Module/InstructionOperandTypeCheckPass.cpp
new file mode 100644
index 00000000..449eea48
--- /dev/null
+++ b/lib/Module/InstructionOperandTypeCheckPass.cpp
@@ -0,0 +1,184 @@
+//===-- InstructionOperandTypeCheckPass.cpp ---------------------*- C++ -*-===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+#include "Passes.h"
+#include "klee/Config/Version.h"
+#include "klee/Internal/Support/ErrorHandling.h"
+#include "llvm/Support/raw_ostream.h"
+
+using namespace llvm;
+
+namespace {
+
+void printOperandWarning(const char *expected, const Instruction *i,
+                         LLVM_TYPE_Q Type *ty, unsigned opNum) {
+  std::string msg;
+  llvm::raw_string_ostream ss(msg);
+  ss << "Found unexpected type (" << *ty << ") at operand " << opNum
+     << ". Expected " << expected << " in " << *i;
+  i->print(ss);
+  ss.flush();
+  klee::klee_warning("%s", msg.c_str());
+}
+
+bool checkOperandTypeIsScalarInt(const Instruction *i, unsigned opNum) {
+  assert(opNum < i->getNumOperands());
+  LLVM_TYPE_Q llvm::Type *ty = i->getOperand(opNum)->getType();
+  if (!(ty->isIntegerTy())) {
+    printOperandWarning("scalar integer", i, ty, opNum);
+    return false;
+  }
+  return true;
+}
+
+bool checkOperandTypeIsScalarIntOrPointer(const Instruction *i,
+                                          unsigned opNum) {
+  assert(opNum < i->getNumOperands());
+  LLVM_TYPE_Q llvm::Type *ty = i->getOperand(opNum)->getType();
+  if (!(ty->isIntegerTy() || ty->isPointerTy())) {
+    printOperandWarning("scalar integer or pointer", i, ty, opNum);
+    return false;
+  }
+  return true;
+}
+
+bool checkOperandTypeIsScalarPointer(const Instruction *i, unsigned opNum) {
+  assert(opNum < i->getNumOperands());
+  LLVM_TYPE_Q llvm::Type *ty = i->getOperand(opNum)->getType();
+  if (!(ty->isPointerTy())) {
+    printOperandWarning("scalar pointer", i, ty, opNum);
+    return false;
+  }
+  return true;
+}
+
+bool checkOperandTypeIsScalarFloat(const Instruction *i, unsigned opNum) {
+  assert(opNum < i->getNumOperands());
+  LLVM_TYPE_Q llvm::Type *ty = i->getOperand(opNum)->getType();
+  if (!(ty->isFloatingPointTy())) {
+    printOperandWarning("scalar float", i, ty, opNum);
+    return false;
+  }
+  return true;
+}
+
+bool checkOperandsHaveSameType(const Instruction *i, unsigned opNum0,
+                               unsigned opNum1) {
+  assert(opNum0 < i->getNumOperands());
+  assert(opNum1 < i->getNumOperands());
+  LLVM_TYPE_Q llvm::Type *ty0 = i->getOperand(opNum0)->getType();
+  LLVM_TYPE_Q llvm::Type *ty1 = i->getOperand(opNum1)->getType();
+  if (!(ty0 == ty1)) {
+    std::string msg;
+    llvm::raw_string_ostream ss(msg);
+    ss << "Found mismatched type (" << *ty0 << " != " << *ty1
+       << ") for operands" << opNum0 << " and " << opNum1
+       << ". Expected operand types to match in " << *i;
+    i->print(ss);
+    ss.flush();
+    klee::klee_warning("%s", msg.c_str());
+    return false;
+  }
+  return true;
+}
+
+bool checkInstruction(const Instruction *i) {
+  switch (i->getOpcode()) {
+  case Instruction::Select: {
+    // Note we do not enforce that operand 1 and 2 are scalar because the
+    // scalarizer pass might not remove these. This could be selecting which
+    // vector operand to feed to another instruction. The Executor can handle
+    // this so case so this is not a problem
+    return checkOperandTypeIsScalarInt(i, 0) &
+           checkOperandsHaveSameType(i, 1, 2);
+  }
+  // Integer arithmetic, logical and shifting
+  // TODO: When we upgrade to newer LLVM use LLVM_FALLTHROUGH
+  case Instruction::Add:
+  case Instruction::Sub:
+  case Instruction::Mul:
+  case Instruction::UDiv:
+  case Instruction::SDiv:
+  case Instruction::URem:
+  case Instruction::SRem:
+  case Instruction::And:
+  case Instruction::Or:
+  case Instruction::Xor:
+  case Instruction::Shl:
+  case Instruction::LShr:
+  case Instruction::AShr: {
+    return checkOperandTypeIsScalarInt(i, 0) &
+           checkOperandTypeIsScalarInt(i, 1);
+  }
+  // Integer comparison
+  case Instruction::ICmp: {
+    return checkOperandTypeIsScalarIntOrPointer(i, 0) &
+           checkOperandTypeIsScalarIntOrPointer(i, 1);
+  }
+  // Integer Conversion
+  case Instruction::Trunc:
+  case Instruction::ZExt:
+  case Instruction::SExt:
+  case Instruction::IntToPtr: {
+    return checkOperandTypeIsScalarInt(i, 0);
+  }
+  case Instruction::PtrToInt: {
+    return checkOperandTypeIsScalarPointer(i, 0);
+  }
+  // TODO: Figure out if Instruction::BitCast needs checking
+  // Floating point arithmetic
+  case Instruction::FAdd:
+  case Instruction::FSub:
+  case Instruction::FMul:
+  case Instruction::FDiv:
+  case Instruction::FRem: {
+    return checkOperandTypeIsScalarFloat(i, 0) &
+           checkOperandTypeIsScalarFloat(i, 1);
+  }
+  // Floating point conversion
+  case Instruction::FPTrunc:
+  case Instruction::FPExt:
+  case Instruction::FPToUI:
+  case Instruction::FPToSI: {
+    return checkOperandTypeIsScalarFloat(i, 0);
+  }
+  case Instruction::UIToFP:
+  case Instruction::SIToFP: {
+    return checkOperandTypeIsScalarInt(i, 0);
+  }
+  // Floating point comparison
+  case Instruction::FCmp: {
+    return checkOperandTypeIsScalarFloat(i, 0) &
+           checkOperandTypeIsScalarFloat(i, 1);
+  }
+  default:
+    // Treat all other instructions as conforming
+    return true;
+  }
+}
+}
+
+namespace klee {
+
+char InstructionOperandTypeCheckPass::ID = 0;
+
+bool InstructionOperandTypeCheckPass::runOnModule(Module &M) {
+  instructionOperandsConform = true;
+  for (Module::iterator fi = M.begin(), fe = M.end(); fi != fe; ++fi) {
+    for (Function::iterator bi = fi->begin(), be = fi->end(); bi != be; ++bi) {
+      for (BasicBlock::iterator ii = bi->begin(), ie = bi->end(); ii != ie;
+           ++ii) {
+        Instruction *i = static_cast<Instruction *>(ii);
+        instructionOperandsConform &= checkInstruction(i);
+      }
+    }
+  }
+
+  return false;
+}
+}
diff --git a/lib/Module/KModule.cpp b/lib/Module/KModule.cpp
index bee9a0b4..215b2275 100644
--- a/lib/Module/KModule.cpp
+++ b/lib/Module/KModule.cpp
@@ -390,9 +390,19 @@ void KModule::prepare(const Interpreter::ModuleOptions &opts,
   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");
+  }
 #if LLVM_VERSION_CODE < LLVM_VERSION(3, 3)
   // For cleanliness see if we can discard any of the functions we
   // forced to import.
diff --git a/lib/Module/Passes.h b/lib/Module/Passes.h
index 293766c1..2ac57b9b 100644
--- a/lib/Module/Passes.h
+++ b/lib/Module/Passes.h
@@ -189,6 +189,23 @@ private:
 llvm::FunctionPass *createScalarizerPass();
 #endif
 
+/// InstructionOperandTypeCheckPass - Type checks the types of instruction
+/// operands to check that they conform to invariants expected by the Executor.
+///
+/// This is a ModulePass because other pass types are not meant to maintain
+/// state between calls.
+class InstructionOperandTypeCheckPass : public llvm::ModulePass {
+private:
+  bool instructionOperandsConform;
+
+public:
+  static char ID;
+  InstructionOperandTypeCheckPass()
+      : llvm::ModulePass(ID), instructionOperandsConform(true) {}
+  // TODO: Add `override` when we switch to C++11
+  bool runOnModule(llvm::Module &M);
+  bool checkPassed() const { return instructionOperandsConform; }
+};
 }
 
 #endif