about summary refs log tree commit diff homepage
path: root/lib/Core
diff options
context:
space:
mode:
authorCristian Cadar <c.cadar@imperial.ac.uk>2017-08-04 23:15:29 +0100
committerCristian Cadar <c.cadar@imperial.ac.uk>2017-08-07 11:06:34 +0100
commit75d0c41e361583cf922b6082b1cb13eee2811e33 (patch)
tree35f4cedcc4c835f0499ce333d36f810965372a5d /lib/Core
parenta4ed54c2b8228a30785c11d7542427a1bd1f7292 (diff)
downloadklee-75d0c41e361583cf922b6082b1cb13eee2811e33.tar.gz
Added checks for div/mod by zero and overshifts in constant expressions. Such div/mod by zero expressions would previously crash KLEE. Added two test cases, one for div/mod by zero, the other for overshift. This fixes the bug reported in #268.
Diffstat (limited to 'lib/Core')
-rw-r--r--lib/Core/ExecutorUtil.cpp24
1 files changed, 24 insertions, 0 deletions
diff --git a/lib/Core/ExecutorUtil.cpp b/lib/Core/ExecutorUtil.cpp
index 0a8f08ed..bd8aa200 100644
--- a/lib/Core/ExecutorUtil.cpp
+++ b/lib/Core/ExecutorUtil.cpp
@@ -126,6 +126,30 @@ namespace klee {
     if (numOperands > 1) op2 = evalConstant(ce->getOperand(1), ki);
     if (numOperands > 2) op3 = evalConstant(ce->getOperand(2), ki);
 
+    /* Checking for possible errors during constant folding */
+    switch (ce->getOpcode()) {
+    case Instruction::SDiv:
+    case Instruction::UDiv:
+    case Instruction::SRem:
+    case Instruction::URem:
+      if (op2->getLimitedValue() == 0) {
+	std::string msg("Division/modulo by zero during constant folding at location ");
+	llvm::raw_string_ostream os(msg);
+	os << (ki ? ki->printFileLine().c_str() : "[unknown]");
+	klee_error("%s", os.str().c_str());
+      }
+      break;
+    case Instruction::Shl:
+    case Instruction::LShr:
+    case Instruction::AShr:
+      if (op2->getLimitedValue() >= op1->getWidth()) {
+	std::string msg("Overshift during constant folding at location ");
+	llvm::raw_string_ostream os(msg);
+	os << (ki ? ki->printFileLine().c_str() : "[unknown]");
+	klee_error("%s", os.str().c_str());
+      }
+    }
+
     std::string msg("Unknown ConstantExpr type");
     llvm::raw_string_ostream os(msg);