klee: add exit-on-error-type parameter

It allows stopping the execution on some conditions like assertions.

The use is like:
klee -exit-on-error-type=Assert -exit-on-error-type=External file.llvm

This is especially useful in the SV-COMP.

A test to cover the new parameter was added too.

Signed-off-by: Jiri Slaby <jslaby@suse.cz>

1 files changed, 20 insertions, 24 deletions

diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp
index caec5e39..b44b0e1b 100644
--- a/lib/Core/SpecialFunctionHandler.cpp
+++ b/lib/Core/SpecialFunctionHandler.cpp
@@ -273,7 +273,7 @@ void SpecialFunctionHandler::handleAbort(ExecutionState &state,
                            KInstruction *target,
                            std::vector<ref<Expr> > &arguments) {
   assert(arguments.size()==0 && "invalid number of arguments to abort");
-  executor.terminateStateOnError(state, "abort failure", "abort.err");
+  executor.terminateStateOnError(state, "abort failure", Executor::Abort);
 }
 
 void SpecialFunctionHandler::handleExit(ExecutionState &state,
@@ -310,7 +310,7 @@ void SpecialFunctionHandler::handleAssert(ExecutionState &state,
   assert(arguments.size()==3 && "invalid number of arguments to _assert");  
   executor.terminateStateOnError(state,
 				 "ASSERTION FAIL: " + readStringAtAddress(state, arguments[0]),
-				 "assert.err");
+				 Executor::Assert);
 }
 
 void SpecialFunctionHandler::handleAssertFail(ExecutionState &state,
@@ -319,7 +319,7 @@ void SpecialFunctionHandler::handleAssertFail(ExecutionState &state,
   assert(arguments.size()==4 && "invalid number of arguments to __assert_fail");
   executor.terminateStateOnError(state,
 				 "ASSERTION FAIL: " + readStringAtAddress(state, arguments[0]),
-				 "assert.err");
+				 Executor::Assert);
 }
 
 void SpecialFunctionHandler::handleReportError(ExecutionState &state,
@@ -330,6 +330,7 @@ void SpecialFunctionHandler::handleReportError(ExecutionState &state,
   // arguments[0], arguments[1] are file, line
   executor.terminateStateOnError(state,
 				 readStringAtAddress(state, arguments[2]),
+				 Executor::ReportError,
 				 readStringAtAddress(state, arguments[3]).c_str());
 }
 
@@ -402,7 +403,7 @@ void SpecialFunctionHandler::handleAssume(ExecutionState &state,
     } else {
       executor.terminateStateOnError(state,
                                      "invalid klee_assume call (provably false)",
-                                     "user.err");
+                                     Executor::User);
     }
   } else {
     executor.addConstraint(state, e);
@@ -467,7 +468,7 @@ void SpecialFunctionHandler::handleSetForking(ExecutionState &state,
   } else {
     executor.terminateStateOnError(state, 
                                    "klee_set_forking requires a constant arg",
-                                   "user.err");
+                                   Executor::User);
   }
 }
 
@@ -623,14 +624,14 @@ void SpecialFunctionHandler::handleCheckMemoryAccess(ExecutionState &state,
   if (!isa<ConstantExpr>(address) || !isa<ConstantExpr>(size)) {
     executor.terminateStateOnError(state, 
                                    "check_memory_access requires constant args",
-                                   "user.err");
+				   Executor::User);
   } else {
     ObjectPair op;
 
     if (!state.addressSpace.resolveOne(cast<ConstantExpr>(address), op)) {
       executor.terminateStateOnError(state,
                                      "check_memory_access: memory error",
-                                     "ptr.err",
+				     Executor::Ptr, NULL,
                                      executor.getAddressInfo(state, address));
     } else {
       ref<Expr> chk = 
@@ -639,7 +640,7 @@ void SpecialFunctionHandler::handleCheckMemoryAccess(ExecutionState &state,
       if (!chk->isTrue()) {
         executor.terminateStateOnError(state,
                                        "check_memory_access: memory error",
-                                       "ptr.err",
+				       Executor::Ptr, NULL,
                                        executor.getAddressInfo(state, address));
       }
     }
@@ -700,9 +701,8 @@ void SpecialFunctionHandler::handleMakeSymbolic(ExecutionState &state,
     ExecutionState *s = it->second;
     
     if (old->readOnly) {
-      executor.terminateStateOnError(*s, 
-                                     "cannot make readonly object symbolic", 
-                                     "user.err");
+      executor.terminateStateOnError(*s, "cannot make readonly object symbolic",
+                                     Executor::User);
       return;
     } 
 
@@ -721,7 +721,7 @@ void SpecialFunctionHandler::handleMakeSymbolic(ExecutionState &state,
     } else {      
       executor.terminateStateOnError(*s, 
                                      "wrong size given to klee_make_symbolic[_name]", 
-                                     "user.err");
+                                     Executor::User);
     }
   }
 }
@@ -746,31 +746,27 @@ void SpecialFunctionHandler::handleMarkGlobal(ExecutionState &state,
 void SpecialFunctionHandler::handleAddOverflow(ExecutionState &state,
                                                KInstruction *target,
                                                std::vector<ref<Expr> > &arguments) {
-  executor.terminateStateOnError(state,
-                                 "overflow on unsigned addition",
-                                 "overflow.err");
+  executor.terminateStateOnError(state, "overflow on unsigned addition",
+                                 Executor::Overflow);
 }
 
 void SpecialFunctionHandler::handleSubOverflow(ExecutionState &state,
                                                KInstruction *target,
                                                std::vector<ref<Expr> > &arguments) {
-  executor.terminateStateOnError(state,
-                                 "overflow on unsigned subtraction",
-                                 "overflow.err");
+  executor.terminateStateOnError(state, "overflow on unsigned subtraction",
+                                 Executor::Overflow);
 }
 
 void SpecialFunctionHandler::handleMulOverflow(ExecutionState &state,
                                                KInstruction *target,
                                                std::vector<ref<Expr> > &arguments) {
-  executor.terminateStateOnError(state,
-                                 "overflow on unsigned multiplication",
-                                 "overflow.err");
+  executor.terminateStateOnError(state, "overflow on unsigned multiplication",
+                                 Executor::Overflow);
 }
 
 void SpecialFunctionHandler::handleDivRemOverflow(ExecutionState &state,
                                                KInstruction *target,
                                                std::vector<ref<Expr> > &arguments) {
-  executor.terminateStateOnError(state,
-                                 "overflow on division or remainder",
-                                 "overflow.err");
+  executor.terminateStateOnError(state, "overflow on division or remainder",
+                                 Executor::Overflow);
 }