From 33417e4b63377e2825811096aaca026847cf2e26 Mon Sep 17 00:00:00 2001 From: Eric Rizzi Date: Mon, 11 May 2015 10:34:05 -0400 Subject: Make use of prefer-cex optional rather than default Previously, default Klee would go through every byte in a test case and attempt to bound it to be between 0 and 127, making it human readable. While this may be useful when attempting to understand Klee, it also means that the time required to create large test suites was greatly increased. By making this behavior default off, unsuspecting users won't incur these additional costs. --- lib/Core/Executor.cpp | 22 +++++++++++++++++++--- 1 file changed, 19 insertions(+), 3 deletions(-) (limited to 'lib/Core/Executor.cpp') diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index 45876659..1b2bc15b 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -140,8 +140,10 @@ namespace { cl::desc("Dump test cases for all active states on exit (default=on)")); cl::opt - NoPreferCex("no-prefer-cex", - cl::init(false)); + 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 RandomizeFork("randomize-fork", @@ -3482,16 +3484,30 @@ bool Executor::getSymbolicSolution(const ExecutionState &state, solver->setTimeout(coreSolverTimeout); ExecutionState tmp(state); - if (!NoPreferCex) { + 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 >::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; -- cgit 1.4.1 From 16772a3c4f287aa7b4016be4ebbaa9e4ece6ca5a Mon Sep 17 00:00:00 2001 From: Cristian Cadar Date: Wed, 3 Jun 2015 19:32:14 +0100 Subject: Added an option --readable-posix-inputs which is used to turn on/off the CEX preferences added in the POSIX model. Removed option --prefer-cex which controlled all CEX preferences. --- include/klee/klee.h | 1 + lib/Core/Executor.cpp | 61 ++++++++++++++++--------------------- lib/Core/SpecialFunctionHandler.cpp | 27 +++++++++++++--- lib/Core/SpecialFunctionHandler.h | 1 + runtime/POSIX/fd_init.c | 28 ++++++++--------- runtime/POSIX/klee_init_env.c | 2 +- test/Feature/PreferCex.c | 2 +- tools/klee-replay/klee-replay.c | 4 +++ 8 files changed, 72 insertions(+), 54 deletions(-) (limited to 'lib/Core/Executor.cpp') diff --git a/include/klee/klee.h b/include/klee/klee.h index 032e5243..d0980395 100644 --- a/include/klee/klee.h +++ b/include/klee/klee.h @@ -110,6 +110,7 @@ extern "C" { void klee_warning(const char *message); void klee_warning_once(const char *message); void klee_prefer_cex(void *object, uintptr_t condition); + void klee_posix_prefer_cex(void *object, uintptr_t condition); void klee_mark_global(void *object); /* Return a possible constant value for the input expression. This 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 @@ -139,12 +139,6 @@ namespace { cl::init(true), cl::desc("Dump test cases for all active states on exit (default=on)")); - cl::opt - 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 RandomizeFork("randomize-fork", cl::init(false), @@ -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 >::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 >::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 > 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 + 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 address = cast(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 > &arguments) { + if (ReadablePosix) + return handlePreferCex(state, target, arguments); +} + void SpecialFunctionHandler::handlePrintExpr(ExecutionState &state, KInstruction *target, std::vector > &arguments) { @@ -480,7 +499,7 @@ void SpecialFunctionHandler::handlePrintRange(ExecutionState &state, if (!isa(arguments[1])) { // FIXME: Pull into a unique value method? ref 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); diff --git a/runtime/POSIX/fd_init.c b/runtime/POSIX/fd_init.c index d976b0b4..8b69fd04 100644 --- a/runtime/POSIX/fd_init.c +++ b/runtime/POSIX/fd_init.c @@ -74,20 +74,20 @@ static void __create_new_dfile(exe_disk_file_t *dfile, unsigned size, reasonable. */ klee_assume((s->st_blksize & ~0xFFFF) == 0); - klee_prefer_cex(s, !(s->st_mode & ~(S_IFMT | 0777))); - klee_prefer_cex(s, s->st_dev == defaults->st_dev); - klee_prefer_cex(s, s->st_rdev == defaults->st_rdev); - klee_prefer_cex(s, (s->st_mode&0700) == 0600); - klee_prefer_cex(s, (s->st_mode&0070) == 0020); - klee_prefer_cex(s, (s->st_mode&0007) == 0002); - klee_prefer_cex(s, (s->st_mode&S_IFMT) == S_IFREG); - klee_prefer_cex(s, s->st_nlink == 1); - klee_prefer_cex(s, s->st_uid == defaults->st_uid); - klee_prefer_cex(s, s->st_gid == defaults->st_gid); - klee_prefer_cex(s, s->st_blksize == 4096); - klee_prefer_cex(s, s->st_atime == defaults->st_atime); - klee_prefer_cex(s, s->st_mtime == defaults->st_mtime); - klee_prefer_cex(s, s->st_ctime == defaults->st_ctime); + klee_posix_prefer_cex(s, !(s->st_mode & ~(S_IFMT | 0777))); + klee_posix_prefer_cex(s, s->st_dev == defaults->st_dev); + klee_posix_prefer_cex(s, s->st_rdev == defaults->st_rdev); + klee_posix_prefer_cex(s, (s->st_mode&0700) == 0600); + klee_posix_prefer_cex(s, (s->st_mode&0070) == 0020); + klee_posix_prefer_cex(s, (s->st_mode&0007) == 0002); + klee_posix_prefer_cex(s, (s->st_mode&S_IFMT) == S_IFREG); + klee_posix_prefer_cex(s, s->st_nlink == 1); + klee_posix_prefer_cex(s, s->st_uid == defaults->st_uid); + klee_posix_prefer_cex(s, s->st_gid == defaults->st_gid); + klee_posix_prefer_cex(s, s->st_blksize == 4096); + klee_posix_prefer_cex(s, s->st_atime == defaults->st_atime); + klee_posix_prefer_cex(s, s->st_mtime == defaults->st_mtime); + klee_posix_prefer_cex(s, s->st_ctime == defaults->st_ctime); s->st_size = dfile->size; s->st_blocks = 8; diff --git a/runtime/POSIX/klee_init_env.c b/runtime/POSIX/klee_init_env.c index 2a6b6f68..cbcf31f4 100644 --- a/runtime/POSIX/klee_init_env.c +++ b/runtime/POSIX/klee_init_env.c @@ -67,7 +67,7 @@ static char *__get_sym_str(int numChars, char *name) { klee_make_symbolic(s, numChars+1, name); for (i=0; i diff --git a/tools/klee-replay/klee-replay.c b/tools/klee-replay/klee-replay.c index 73e2783e..6b4fb8f4 100644 --- a/tools/klee-replay/klee-replay.c +++ b/tools/klee-replay/klee-replay.c @@ -418,6 +418,10 @@ void klee_prefer_cex(void *buffer, uintptr_t condition) { ; } +void klee_posix_prefer_cex(void *buffer, uintptr_t condition) { + ; +} + void klee_make_symbolic(void *addr, size_t nbytes, const char *name) { /* XXX remove model version code once new tests gen'd */ if (obj_index >= input->numObjects) { -- cgit 1.4.1