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. --- lib/Core/SpecialFunctionHandler.cpp | 27 +++++++++++++++++++++++---- 1 file changed, 23 insertions(+), 4 deletions(-) (limited to 'lib/Core/SpecialFunctionHandler.cpp') 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()), -- cgit 1.4.1