diff options
| -rw-r--r-- | lib/Core/Executor.cpp | 607 |
1 files changed, 315 insertions, 292 deletions
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index c7d88c2c..9b2c1b0a 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -8,8 +8,11 @@ //===----------------------------------------------------------------------===// #include "Executor.h" + +#include "../Expr/ArrayExprOptimizer.h" #include "Context.h" #include "CoreStats.h" +#include "ExecutorTimerInfo.h" #include "ExternalDispatcher.h" #include "ImpliedValue.h" #include "Memory.h" @@ -21,21 +24,11 @@ #include "StatsTracker.h" #include "TimingSolver.h" #include "UserSearcher.h" -#include "ExecutorTimerInfo.h" - -#include "klee/ExecutionState.h" -#include "klee/Expr.h" -#include "klee/Interpreter.h" -#include "klee/TimerStatIncrementer.h" -#include "klee/SolverCmdLine.h" #include "klee/Common.h" -#include "klee/util/Assignment.h" -#include "klee/util/ExprPPrinter.h" -#include "klee/util/ExprSMTLIBPrinter.h" -#include "klee/util/ExprUtil.h" -#include "klee/util/GetElementPtrTypeIterator.h" #include "klee/Config/Version.h" +#include "klee/ExecutionState.h" +#include "klee/Expr.h" #include "klee/Internal/ADT/KTest.h" #include "klee/Internal/ADT/RNG.h" #include "klee/Internal/Module/Cell.h" @@ -46,12 +39,19 @@ #include "klee/Internal/Support/FileHandling.h" #include "klee/Internal/Support/FloatEvaluation.h" #include "klee/Internal/Support/ModuleUtil.h" -#include "klee/Internal/System/Time.h" #include "klee/Internal/System/MemoryUsage.h" +#include "klee/Internal/System/Time.h" +#include "klee/Interpreter.h" #include "klee/OptionCategories.h" +#include "klee/SolverCmdLine.h" #include "klee/SolverStats.h" +#include "klee/TimerStatIncrementer.h" +#include "klee/util/Assignment.h" +#include "klee/util/ExprPPrinter.h" +#include "klee/util/ExprSMTLIBPrinter.h" +#include "klee/util/ExprUtil.h" +#include "klee/util/GetElementPtrTypeIterator.h" -#include "../Expr/ArrayExprOptimizer.h" #include "llvm/ADT/SmallPtrSet.h" #include "llvm/ADT/StringExtras.h" #include "llvm/IR/Attributes.h" @@ -76,307 +76,330 @@ #include "llvm/IR/CallSite.h" #endif -#include <cassert> #include <algorithm> +#include <cassert> +#include <cerrno> +#include <cxxabi.h> +#include <fstream> #include <iomanip> #include <iosfwd> -#include <fstream> #include <sstream> -#include <vector> #include <string> - #include <sys/mman.h> - -#include <errno.h> -#include <cxxabi.h> +#include <vector> using namespace llvm; using namespace klee; - namespace { - /*** Test generation options ***/ - - cl::OptionCategory TestGenCat("Test generation options", - "These options impact test generation."); - - cl::opt<bool> - DumpStatesOnHalt("dump-states-on-halt", - cl::init(true), - cl::desc("Dump test cases for all active states on exit (default=true)"), - cl::cat(TestGenCat)); - - cl::opt<bool> - OnlyOutputStatesCoveringNew("only-output-states-covering-new", - cl::init(false), - cl::desc("Only output test cases covering new code (default=false)."), - cl::cat(TestGenCat)); - - cl::opt<bool> - EmitAllErrors("emit-all-errors", - cl::init(false), - cl::desc("Generate tests cases for all errors " - "(default=false, i.e. one per (error,instruction) pair)"), - cl::cat(TestGenCat)); - - +/*** Test generation options ***/ + +cl::OptionCategory TestGenCat("Test generation options", + "These options impact test generation."); + +cl::opt<bool> DumpStatesOnHalt( + "dump-states-on-halt", + cl::init(true), + cl::desc("Dump test cases for all active states on exit (default=true)"), + cl::cat(TestGenCat)); + +cl::opt<bool> OnlyOutputStatesCoveringNew( + "only-output-states-covering-new", + cl::init(false), + cl::desc("Only output test cases covering new code (default=false)"), + cl::cat(TestGenCat)); + +cl::opt<bool> EmitAllErrors( + "emit-all-errors", cl::init(false), + cl::desc("Generate tests cases for all errors " + "(default=false, i.e. one per (error,instruction) pair)"), + cl::cat(TestGenCat)); + + +/* Constraint solving options */ + +cl::opt<unsigned> MaxSymArraySize( + "max-sym-array-size", + cl::desc( + "If a symbolic array exceeds this size (in bytes), symbolic addresses " + "into this array are concretized. Set to 0 to disable (default=0)"), + cl::init(0), + cl::cat(SolvingCat)); + +cl::opt<bool> + SimplifySymIndices("simplify-sym-indices", + cl::init(false), + cl::desc("Simplify symbolic accesses using equalities " + "from other constraints (default=false)"), + cl::cat(SolvingCat)); - /* Constraint solving options */ +cl::opt<bool> + EqualitySubstitution("equality-substitution", cl::init(true), + cl::desc("Simplify equality expressions before " + "querying the solver (default=true)"), + cl::cat(SolvingCat)); - cl::opt<unsigned> - MaxSymArraySize("max-sym-array-size", - cl::desc("If a symbolic array exceeds this size (in bytes), symbolic addresses into this array are concretized. Set to 0 to disable (default=0)"), - cl::init(0), - cl::cat(SolvingCat)); +/*** External call policy options ***/ - cl::opt<bool> - SimplifySymIndices("simplify-sym-indices", - cl::init(false), - cl::desc("Simplify symbolic accesses using equalities from other constraints (default=false)"), - cl::cat(SolvingCat)); +cl::OptionCategory ExtCallsCat("External call policy options", + "These options impact external calls."); - cl::opt<bool> - EqualitySubstitution("equality-substitution", - cl::init(true), - cl::desc("Simplify equality expressions before querying the solver (default=true)"), - cl::cat(SolvingCat)); +enum class ExternalCallPolicy { + None, // No external calls allowed + Concrete, // Only external calls with concrete arguments allowed + All, // All external calls allowed +}; - - /*** External call policy options ***/ +cl::opt<ExternalCallPolicy> ExternalCalls( + "external-calls", + cl::desc("Specify the external call policy"), + cl::values( + clEnumValN( + ExternalCallPolicy::None, "none", + "No external function calls are allowed. Note that KLEE always " + "allows some external calls with concrete arguments to go through " + "(in particular printf and puts), regardless of this option."), + clEnumValN(ExternalCallPolicy::Concrete, "concrete", + "Only external function calls with concrete arguments are " + "allowed (default)"), + clEnumValN(ExternalCallPolicy::All, "all", + "All external function calls are allowed. This concretizes " + "any symbolic arguments in calls to external functions.") + KLEE_LLVM_CL_VAL_END), + cl::init(ExternalCallPolicy::Concrete), + cl::cat(ExtCallsCat)); + +cl::opt<bool> SuppressExternalWarnings( + "suppress-external-warnings", + cl::init(false), + cl::desc("Supress warnings about calling external functions."), + cl::cat(ExtCallsCat)); + +cl::opt<bool> AllExternalWarnings( + "all-external-warnings", + cl::init(false), + cl::desc("Issue a warning everytime an external call is made, " + "as opposed to once per function (default=false)"), + cl::cat(ExtCallsCat)); + +/*** Seeding options ***/ + +cl::OptionCategory SeedingCat( + "Seeding options", + "These options are related to the use of seeds to start exploration."); + +cl::opt<bool> AlwaysOutputSeeds( + "always-output-seeds", + cl::init(true), + cl::desc( + "Dump test cases even if they are driven by seeds only (default=true)"), + cl::cat(SeedingCat)); + +cl::opt<bool> OnlyReplaySeeds( + "only-replay-seeds", + cl::init(false), + cl::desc("Discard states that do not have a seed (default=false)."), + cl::cat(SeedingCat)); + +cl::opt<bool> OnlySeed("only-seed", + cl::init(false), + cl::desc("Stop execution after seeding is done without " + "doing regular search (default=false)."), + cl::cat(SeedingCat)); + +cl::opt<bool> + AllowSeedExtension("allow-seed-extension", + cl::init(false), + cl::desc("Allow extra (unbound) values to become " + "symbolic during seeding (default=false)."), + cl::cat(SeedingCat)); + +cl::opt<bool> ZeroSeedExtension( + "zero-seed-extension", + cl::init(false), + cl::desc( + "Use zero-filled objects if matching seed not found (default=false)"), + cl::cat(SeedingCat)); + +cl::opt<bool> AllowSeedTruncation( + "allow-seed-truncation", + cl::init(false), + cl::desc("Allow smaller buffers than in seeds (default=false)."), + cl::cat(SeedingCat)); + +cl::opt<bool> NamedSeedMatching( + "named-seed-matching", + cl::init(false), + cl::desc("Use names to match symbolic objects to inputs (default=false)."), + cl::cat(SeedingCat)); + +cl::opt<std::string> + SeedTime("seed-time", + cl::desc("Amount of time to dedicate to seeds, before normal " + "search (default=0s (off))"), + cl::cat(SeedingCat)); + + +/*** Termination criteria options ***/ + +cl::OptionCategory + TerminationCat("State and overall termination options", + "These options control termination of the overall KLEE " + "execution and of individual states."); + +cl::list<Executor::TerminateReason> ExitOnErrorType( + "exit-on-error-type", + cl::desc( + "Stop execution after reaching a specified condition (default=false)"), + cl::values( + clEnumValN(Executor::Abort, "Abort", "The program crashed"), + clEnumValN(Executor::Assert, "Assert", "An assertion was hit"), + clEnumValN(Executor::BadVectorAccess, "BadVectorAccess", + "Vector accessed out of bounds"), + clEnumValN(Executor::Exec, "Exec", + "Trying to execute an unexpected instruction"), + clEnumValN(Executor::External, "External", + "External objects referenced"), + clEnumValN(Executor::Free, "Free", "Freeing invalid memory"), + clEnumValN(Executor::Model, "Model", "Memory model limit hit"), + clEnumValN(Executor::Overflow, "Overflow", "An overflow occurred"), + clEnumValN(Executor::Ptr, "Ptr", "Pointer error"), + clEnumValN(Executor::ReadOnly, "ReadOnly", "Write to read-only memory"), + clEnumValN(Executor::ReportError, "ReportError", + "klee_report_error called"), + clEnumValN(Executor::User, "User", "Wrong klee_* functions invocation"), + clEnumValN(Executor::Unhandled, "Unhandled", + "Unhandled instruction hit") KLEE_LLVM_CL_VAL_END), + cl::ZeroOrMore, + cl::cat(TerminationCat)); + +cl::opt<unsigned long long> MaxInstructions( + "max-instructions", + cl::desc("Stop execution after this many instructions. Set to 0 to disable (default=0)"), + cl::init(0), + cl::cat(TerminationCat)); + +cl::opt<unsigned> + MaxForks("max-forks", + cl::desc("Only fork this many times. Set to -1 to disable (default=-1)"), + cl::init(~0u), + cl::cat(TerminationCat)); + +cl::opt<unsigned> MaxDepth( + "max-depth", + cl::desc("Only allow this many symbolic branches. Set to 0 to disable (default=0)"), + cl::init(0), + cl::cat(TerminationCat)); + +cl::opt<unsigned> MaxMemory("max-memory", + cl::desc("Refuse to fork when above this amount of " + "memory (in MB) (default=2000)"), + cl::init(2000), + cl::cat(TerminationCat)); + +cl::opt<bool> MaxMemoryInhibit( + "max-memory-inhibit", + cl::desc( + "Inhibit forking at memory cap (vs. random terminate) (default=true)"), + cl::init(true), + cl::cat(TerminationCat)); + +cl::opt<unsigned> RuntimeMaxStackFrames( + "max-stack-frames", + cl::desc("Terminate a state after this many stack frames. Set to 0 to " + "disable (default=8192)"), + cl::init(8192), + cl::cat(TerminationCat)); + +cl::opt<std::string> MaxInstructionTime( + "max-instruction-time", + cl::desc("Allow a single instruction to take only this much time. Enables " + "--use-forked-solver. Set to 0s to disable (default=0s)"), + cl::cat(TerminationCat)); + +cl::opt<double> MaxStaticForkPct( + "max-static-fork-pct", cl::init(1.), + cl::desc("Maximum percentage spent by an instruction forking out of the " + "forking of all instructions (default=1.0 (always))"), + cl::cat(TerminationCat)); + +cl::opt<double> MaxStaticSolvePct( + "max-static-solve-pct", cl::init(1.), + cl::desc("Maximum percentage of solving time that can be spent by a single " + "instruction over total solving time for all instructions " + "(default=1.0 (always))"), + cl::cat(TerminationCat)); + +cl::opt<double> MaxStaticCPForkPct( + "max-static-cpfork-pct", cl::init(1.), + cl::desc("Maximum percentage spent by an instruction of a call path " + "forking out of the forking of all instructions in the call path " + "(default=1.0 (always))"), + cl::cat(TerminationCat)); + +cl::opt<double> MaxStaticCPSolvePct( + "max-static-cpsolve-pct", cl::init(1.), + cl::desc("Maximum percentage of solving time that can be spent by a single " + "instruction of a call path over total solving time for all " + "instructions (default=1.0 (always))"), + cl::cat(TerminationCat)); + +/*** Debugging options ***/ + +cl::OptionCategory DebugCat("Debugging options", + "These are debugging options."); + +/// The different query logging solvers that can switched on/off +enum PrintDebugInstructionsType { + STDERR_ALL, /// + STDERR_SRC, + STDERR_COMPACT, + FILE_ALL, /// + FILE_SRC, /// + FILE_COMPACT /// +}; - cl::OptionCategory ExtCallsCat("External call policy options", - "These options impact external calls."); - - enum class ExternalCallPolicy { - None, // No external calls allowed - Concrete, // Only external calls with concrete arguments allowed - All, // All external calls allowed - }; - - cl::opt<ExternalCallPolicy> - ExternalCalls("external-calls", - cl::desc("Specify the external call policy"), - cl::values(clEnumValN(ExternalCallPolicy::None, "none", "No external function calls are allowed. Note that KLEE always allows some external calls with concrete arguments to go through (in particular printf and puts), regardless of this option."), - clEnumValN(ExternalCallPolicy::Concrete, "concrete", "Only external function calls with concrete arguments are allowed (default)"), - clEnumValN(ExternalCallPolicy::All, "all", "All external function calls are allowed. This concretizes any symbolic arguments in calls to external functions.") - KLEE_LLVM_CL_VAL_END), - cl::init(ExternalCallPolicy::Concrete), - cl::cat(ExtCallsCat)); - - cl::opt<bool> - SuppressExternalWarnings("suppress-external-warnings", - cl::init(false), - cl::desc("Supress warnings about calling external functions."), - cl::cat(ExtCallsCat)); - - cl::opt<bool> - AllExternalWarnings("all-external-warnings", - cl::init(false), - cl::desc("Issue a warning everytime an external call is made, " - "as opposed to once per function (default=false)"), - cl::cat(ExtCallsCat)); - - - /*** Seeding options ***/ - - cl::OptionCategory SeedingCat("Seeding options", - "These options are related to the use of seeds to start exploration."); - - cl::opt<bool> - AlwaysOutputSeeds("always-output-seeds", - cl::init(true), - cl::desc("Dump test cases even if they are driven by seeds only (default=true)"), - cl::cat(SeedingCat)); - - cl::opt<bool> - OnlyReplaySeeds("only-replay-seeds", - cl::init(false), - cl::desc("Discard states that do not have a seed (default=false)."), - cl::cat(SeedingCat)); - - cl::opt<bool> - OnlySeed("only-seed", - cl::init(false), - cl::desc("Stop execution after seeding is done without doing regular search (default=false)."), - cl::cat(SeedingCat)); - - cl::opt<bool> - AllowSeedExtension("allow-seed-extension", - cl::init(false), - cl::desc("Allow extra (unbound) values to become symbolic during seeding (default=false)."), - cl::cat(SeedingCat)); - - cl::opt<bool> - ZeroSeedExtension("zero-seed-extension", - cl::init(false), - cl::desc("Use zero-filled objects if matching seed not found (default=false)"), - cl::cat(SeedingCat)); - - cl::opt<bool> - AllowSeedTruncation("allow-seed-truncation", - cl::init(false), - cl::desc("Allow smaller buffers than in seeds (default=false)."), - cl::cat(SeedingCat)); - - cl::opt<bool> - NamedSeedMatching("named-seed-matching", - cl::init(false), - cl::desc("Use names to match symbolic objects to inputs (default=false)."), - cl::cat(SeedingCat)); - - cl::opt<std::string> - SeedTime("seed-time", - cl::desc("Amount of time to dedicate to seeds, before normal search (default=0s (off))"), - cl::cat(SeedingCat)); - - - /*** Termination criteria options ***/ - - cl::OptionCategory TerminationCat("State and overall termination options", - "These options control termination of the overall KLEE execution and of individual states."); - - cl::list<Executor::TerminateReason> - ExitOnErrorType("exit-on-error-type", - cl::desc("Stop execution after reaching a specified condition (default=false)"), - cl::values( - clEnumValN(Executor::Abort, "Abort", "The program crashed"), - clEnumValN(Executor::Assert, "Assert", "An assertion was hit"), - clEnumValN(Executor::BadVectorAccess, "BadVectorAccess", "Vector accessed out of bounds"), - clEnumValN(Executor::Exec, "Exec", "Trying to execute an unexpected instruction"), - clEnumValN(Executor::External, "External", "External objects referenced"), - clEnumValN(Executor::Free, "Free", "Freeing invalid memory"), - clEnumValN(Executor::Model, "Model", "Memory model limit hit"), - clEnumValN(Executor::Overflow, "Overflow", "An overflow occurred"), - clEnumValN(Executor::Ptr, "Ptr", "Pointer error"), - clEnumValN(Executor::ReadOnly, "ReadOnly", "Write to read-only memory"), - clEnumValN(Executor::ReportError, "ReportError", "klee_report_error called"), - clEnumValN(Executor::User, "User", "Wrong klee_* functions invocation"), - clEnumValN(Executor::Unhandled, "Unhandled", "Unhandled instruction hit") - KLEE_LLVM_CL_VAL_END), - cl::ZeroOrMore, - cl::cat(TerminationCat)); - - cl::opt<unsigned long long> - MaxInstructions("max-instructions", - cl::desc("Stop execution after this many instructions (default=0 (off))"), - cl::init(0), - cl::cat(TerminationCat)); - - cl::opt<unsigned> - MaxForks("max-forks", - cl::desc("Only fork this many times (default=-1 (off))"), - cl::init(~0u), - cl::cat(TerminationCat)); - - cl::opt<unsigned> - MaxDepth("max-depth", - cl::desc("Only allow this many symbolic branches (default=0 (off))"), - cl::init(0), - cl::cat(TerminationCat)); - - cl::opt<unsigned> - MaxMemory("max-memory", - cl::desc("Refuse to fork when above this amount of memory (in MB, default=2000)"), - cl::init(2000), - cl::cat(TerminationCat)); - - cl::opt<bool> - MaxMemoryInhibit("max-memory-inhibit", - cl::desc("Inhibit forking at memory cap (vs. random terminate) (default=true)"), - cl::init(true), - cl::cat(TerminationCat)); - - cl::opt<unsigned> RuntimeMaxStackFrames("max-stack-frames", - cl::desc("Terminate a state after this many stack frames (default=8192). Disable check with 0."), - cl::init(8192), - cl::cat(TerminationCat)); - - cl::opt<std::string> - MaxInstructionTime("max-instruction-time", - cl::desc("Allow a single instruction to take only this much time (default=0s (off)). Enables --use-forked-solver"), - cl::cat(TerminationCat)); - - cl::opt<double> - MaxStaticForkPct("max-static-fork-pct", - cl::init(1.), - cl::desc("Maximum percentage spent by an instruction forking out of the forking of all instructions (default=1.0 (always))"), - cl::cat(TerminationCat)); - - cl::opt<double> - MaxStaticSolvePct("max-static-solve-pct", - cl::init(1.), - cl::desc("Maximum percentage of solving time that can be spent by a single instruction over total solving time for all instructions (default=1.0 (always))"), - cl::cat(TerminationCat)); - - cl::opt<double> - MaxStaticCPForkPct("max-static-cpfork-pct", - cl::init(1.), - cl::desc("Maximum percentage spent by an instruction of a call path forking out of the forking of all instructions in the call path (default=1.0 (always))"), - cl::cat(TerminationCat)); - - cl::opt<double> - MaxStaticCPSolvePct("max-static-cpsolve-pct", - cl::init(1.), - cl::desc("Maximum percentage of solving time that can be spent by a single instruction of a call path over total solving time for all instructions (default=1.0 (always))"), - cl::cat(TerminationCat)); - - - /*** Debugging options ***/ - - cl::OptionCategory DebugCat("Debugging options", - "These are debugging options."); - - /// The different query logging solvers that can switched on/off - enum PrintDebugInstructionsType { - STDERR_ALL, /// - STDERR_SRC, - STDERR_COMPACT, - FILE_ALL, /// - FILE_SRC, /// - FILE_COMPACT /// - }; - - llvm::cl::bits<PrintDebugInstructionsType> DebugPrintInstructions( - "debug-print-instructions", - llvm::cl::desc("Log instructions during execution."), - llvm::cl::values( - clEnumValN(STDERR_ALL, "all:stderr", "Log all instructions to stderr " - "in format [src, inst_id, " - "llvm_inst]"), - clEnumValN(STDERR_SRC, "src:stderr", - "Log all instructions to stderr in format [src, inst_id]"), - clEnumValN(STDERR_COMPACT, "compact:stderr", - "Log all instructions to stderr in format [inst_id]"), - clEnumValN(FILE_ALL, "all:file", "Log all instructions to file " - "instructions.txt in format [src, " - "inst_id, llvm_inst]"), - clEnumValN(FILE_SRC, "src:file", "Log all instructions to file " - "instructions.txt in format [src, " - "inst_id]"), - clEnumValN(FILE_COMPACT, "compact:file", - "Log all instructions to file instructions.txt in format " - "[inst_id]") - KLEE_LLVM_CL_VAL_END), - llvm::cl::CommaSeparated, - cl::cat(DebugCat)); +llvm::cl::bits<PrintDebugInstructionsType> DebugPrintInstructions( + "debug-print-instructions", + llvm::cl::desc("Log instructions during execution."), + llvm::cl::values( + clEnumValN(STDERR_ALL, "all:stderr", + "Log all instructions to stderr " + "in format [src, inst_id, " + "llvm_inst]"), + clEnumValN(STDERR_SRC, "src:stderr", + "Log all instructions to stderr in format [src, inst_id]"), + clEnumValN(STDERR_COMPACT, "compact:stderr", + "Log all instructions to stderr in format [inst_id]"), + clEnumValN(FILE_ALL, "all:file", + "Log all instructions to file " + "instructions.txt in format [src, " + "inst_id, llvm_inst]"), + clEnumValN(FILE_SRC, "src:file", + "Log all instructions to file " + "instructions.txt in format [src, " + "inst_id]"), + clEnumValN(FILE_COMPACT, "compact:file", + "Log all instructions to file instructions.txt in format " + "[inst_id]") KLEE_LLVM_CL_VAL_END), + llvm::cl::CommaSeparated, + cl::cat(DebugCat)); #ifdef HAVE_ZLIB_H - cl::opt<bool> - DebugCompressInstructions("debug-compress-instructions", - cl::init(false), - cl::desc("Compress the logged instructions in gzip format (default=false)."), - cl::cat(DebugCat)); +cl::opt<bool> DebugCompressInstructions( + "debug-compress-instructions", cl::init(false), + cl::desc( + "Compress the logged instructions in gzip format (default=false)."), + cl::cat(DebugCat)); #endif - cl::opt<bool> - DebugCheckForImpliedValues("debug-check-for-implied-values", - cl::init(false), - cl::desc("Debug the implied value optimization"), - cl::cat(DebugCat)); - -} +cl::opt<bool> DebugCheckForImpliedValues( + "debug-check-for-implied-values", cl::init(false), + cl::desc("Debug the implied value optimization"), + cl::cat(DebugCat)); +} // namespace namespace klee { RNG theRNG; |