diff options
Diffstat (limited to 'lib/Core')
-rw-r--r-- | lib/Core/Executor.cpp | 61 | ||||
-rw-r--r-- | lib/Core/SpecialFunctionHandler.cpp | 27 | ||||
-rw-r--r-- | lib/Core/SpecialFunctionHandler.h | 1 |
3 files changed, 51 insertions, 38 deletions
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index 1b2bc15b..49e526f5 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -140,12 +140,6 @@ namespace { cl::desc("Dump test cases for all active states on exit (default=on)")); cl::opt<bool> - PreferCex("prefer-cex", - cl::init(false), - cl::desc("Prefer creation of tests with human readable bytes. Can also pair with klee_prefer_cex api " - "to customize range. Note: option is expensive when creating lots of tests (default=false)")); - - cl::opt<bool> RandomizeFork("randomize-fork", cl::init(false), cl::desc("Randomly swap the true and false states on a fork (default=off)")); @@ -3484,34 +3478,33 @@ bool Executor::getSymbolicSolution(const ExecutionState &state, solver->setTimeout(coreSolverTimeout); ExecutionState tmp(state); - if (PreferCex) { - // When the PreferCex is enabled, go through each byte in every test case and - // attempt to restrict it to the constraints contained in cexPreferences. - // (Note: usually this means trying to make it an ASCII character (0-127) - // and therefore human readable. It is also possible to customize the preferred - // constraints. See test/Features/PreferCex.c for an example) While this - // process can be very expensive, it can also make understanding individual - // test cases much easier. - for (unsigned i = 0; i != state.symbolics.size(); ++i) { - const MemoryObject *mo = state.symbolics[i].first; - std::vector< ref<Expr> >::const_iterator pi = - mo->cexPreferences.begin(), pie = mo->cexPreferences.end(); - for (; pi != pie; ++pi) { - bool mustBeTrue; - // Attempt to bound byte to constraints held in cexPreferences - bool success = solver->mustBeTrue(tmp, Expr::createIsZero(*pi), - mustBeTrue); - // If it isn't possible to constrain this particular byte in the desired - // way (normally this would mean that the byte can't be constrained to - // be between 0 and 127 without making the entire constraint list UNSAT) - // then just continue on to the next byte. - if (!success) break; - // If the particular constraint operated on in this iteration through - // the loop isn't implied then add it to the list of constraints. - if (!mustBeTrue) tmp.addConstraint(*pi); - } - if (pi!=pie) break; - } + + // Go through each byte in every test case and attempt to restrict + // it to the constraints contained in cexPreferences. (Note: + // usually this means trying to make it an ASCII character (0-127) + // and therefore human readable. It is also possible to customize + // the preferred constraints. See test/Features/PreferCex.c for + // an example) While this process can be very expensive, it can + // also make understanding individual test cases much easier. + for (unsigned i = 0; i != state.symbolics.size(); ++i) { + const MemoryObject *mo = state.symbolics[i].first; + std::vector< ref<Expr> >::const_iterator pi = + mo->cexPreferences.begin(), pie = mo->cexPreferences.end(); + for (; pi != pie; ++pi) { + bool mustBeTrue; + // Attempt to bound byte to constraints held in cexPreferences + bool success = solver->mustBeTrue(tmp, Expr::createIsZero(*pi), + mustBeTrue); + // If it isn't possible to constrain this particular byte in the desired + // way (normally this would mean that the byte can't be constrained to + // be between 0 and 127 without making the entire constraint list UNSAT) + // then just continue on to the next byte. + if (!success) break; + // If the particular constraint operated on in this iteration through + // the loop isn't implied then add it to the list of constraints. + if (!mustBeTrue) tmp.addConstraint(*pi); + } + if (pi!=pie) break; } std::vector< std::vector<unsigned char> > values; diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp index f06ae4f5..52abff5f 100644 --- a/lib/Core/SpecialFunctionHandler.cpp +++ b/lib/Core/SpecialFunctionHandler.cpp @@ -22,6 +22,8 @@ #include "Executor.h" #include "MemoryManager.h" +#include "klee/CommandLine.h" + #if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3) #include "llvm/IR/Module.h" #else @@ -34,6 +36,15 @@ using namespace llvm; using namespace klee; +namespace { + cl::opt<bool> + ReadablePosix("readable-posix-inputs", + cl::init(false), + cl::desc("Prefer creation of POSIX inputs (command-line arguments, files, etc.) with human readable bytes. " + "Note: option is expensive when creating lots of tests (default=false)")); +} + + /// \todo Almost all of the demands in this file should be replaced /// with terminateState calls. @@ -81,6 +92,7 @@ static SpecialFunctionHandler::HandlerInfo handlerInfo[] = { add("klee_mark_global", handleMarkGlobal, false), add("klee_merge", handleMerge, false), add("klee_prefer_cex", handlePreferCex, false), + add("klee_posix_prefer_cex", handlePosixPreferCex, false), add("klee_print_expr", handlePrintExpr, false), add("klee_print_range", handlePrintRange, false), add("klee_set_forking", handleSetForking, false), @@ -222,7 +234,7 @@ SpecialFunctionHandler::readStringAtAddress(ExecutionState &state, ref<ConstantExpr> address = cast<ConstantExpr>(addressExpr); if (!state.addressSpace.resolveOne(address, op)) assert(0 && "XXX out of bounds / multiple resolution unhandled"); - bool res; + bool res __attribute__ ((unused)); assert(executor.solver->mustBeTrue(state, EqExpr::create(address, op.first->getBaseExpr()), @@ -376,7 +388,7 @@ void SpecialFunctionHandler::handleAssume(ExecutionState &state, e = NeExpr::create(e, ConstantExpr::create(0, e->getWidth())); bool res; - bool success = executor.solver->mustBeFalse(state, e, res); + bool success __attribute__ ((unused)) = executor.solver->mustBeFalse(state, e, res); assert(success && "FIXME: Unhandled solver failure"); if (res) { executor.terminateStateOnError(state, @@ -416,6 +428,13 @@ void SpecialFunctionHandler::handlePreferCex(ExecutionState &state, rl[0].first.first->cexPreferences.push_back(cond); } +void SpecialFunctionHandler::handlePosixPreferCex(ExecutionState &state, + KInstruction *target, + std::vector<ref<Expr> > &arguments) { + if (ReadablePosix) + return handlePreferCex(state, target, arguments); +} + void SpecialFunctionHandler::handlePrintExpr(ExecutionState &state, KInstruction *target, std::vector<ref<Expr> > &arguments) { @@ -480,7 +499,7 @@ void SpecialFunctionHandler::handlePrintRange(ExecutionState &state, if (!isa<ConstantExpr>(arguments[1])) { // FIXME: Pull into a unique value method? ref<ConstantExpr> value; - bool success = executor.solver->getValue(state, arguments[1], value); + bool success __attribute__ ((unused)) = executor.solver->getValue(state, arguments[1], value); assert(success && "FIXME: Unhandled solver failure"); bool res; success = executor.solver->mustBeTrue(state, @@ -679,7 +698,7 @@ void SpecialFunctionHandler::handleMakeSymbolic(ExecutionState &state, // FIXME: Type coercion should be done consistently somewhere. bool res; - bool success = + bool success __attribute__ ((unused)) = executor.solver->mustBeTrue(*s, EqExpr::create(ZExtExpr::create(arguments[1], Context::get().getPointerWidth()), diff --git a/lib/Core/SpecialFunctionHandler.h b/lib/Core/SpecialFunctionHandler.h index d52b8fc5..2dfdde43 100644 --- a/lib/Core/SpecialFunctionHandler.h +++ b/lib/Core/SpecialFunctionHandler.h @@ -120,6 +120,7 @@ namespace klee { HANDLER(handleNew); HANDLER(handleNewArray); HANDLER(handlePreferCex); + HANDLER(handlePosixPreferCex); HANDLER(handlePrintExpr); HANDLER(handlePrintRange); HANDLER(handleRange); |