klee Namespace Reference

Namespaces
namespace	bits32
namespace	bits64
namespace	expr
namespace	floats
namespace	ImpliedValue
namespace	ints
namespace	stats
namespace	time
namespace	util

Classes
struct	_Identity
struct	_Select1st
class	AddressSpace
class	Array
class	ArrayCache
	Provides an interface for creating and destroying Array objects. More...
struct	ArrayCmpFn
class	ArrayExprHash
class	ArrayExprHelper
struct	ArrayHashFn
class	ArrayReadExprVisitor
class	ArrayValueOptReplaceVisitor
class	Assignment
class	AssignmentEvaluator
class	AssignmentGenerator
class	AssignmentValidatingSolver
class	BatchingSearcher
class	BFSSearcher
class	BinaryExpr
class	BitArray
class	CallPathManager
class	CallPathNode
struct	CallSiteInfo
class	CastExpr
struct	Cell
struct	CleanupPhaseUnwindingInformation
class	CmpExpr
class	compressed_fd_ostream
class	ConcatExpr
class	ConstantArrayExprVisitor
class	ConstantArrayFinder
class	ConstantExpr
class	ConstraintManager
	Manages constraints, e.g. optimisation. More...
class	ConstraintSet
class	Context
	Context - Helper class for storing global information about a KLEE run. More...
class	DFSSearcher
class	DiscretePDF
class	DivCheckPass
class	DummySolverImpl
struct	EquivArrayCmpFn
class	ExecutionState
	ExecutionState representing a path under exploration. More...
struct	ExecutionStateIDCompare
class	Executor
class	Expr
	Class representing symbolic expressions. More...
class	ExprBuilder
	ExprBuilder - Base expression builder class. More...
class	ExprEvaluator
class	ExprHandle
class	ExprHashMap
class	ExprHolder
class	ExprOptimizer
class	ExprPPrinter
class	ExprRangeEvaluator
class	ExprRewriter
class	ExprSMTLIBPrinter
class	ExprVisitor
class	ExternalDispatcher
class	ExternalDispatcherImpl
class	ExtractExpr
class	FixedStack
class	FunctionAliasPass
struct	FunctionInfo
	FunctionInfo stores debug information for a KFunction. More...
class	generic_gep_type_iterator
class	ImmutableMap
class	ImmutableSet
class	ImmutableTree
class	IncompleteSolver
class	IndexCompatibilityExprVisitor
class	IndexTransformationExprVisitor
struct	InstructionInfo
	InstructionInfo stores debug information for a KInstruction. More...
class	InstructionInfoTable
class	InstructionOperandTypeCheckPass
class	InterleavedSearcher
class	Interpreter
class	InterpreterHandler
class	IntrinsicCleanerPass
class	IterativeDeepeningTimeSearcher
class	KCommandLine
class	KConstant
struct	KFunction
struct	KGEPInstruction
class	KInstIterator
struct	KInstruction
class	KleeIRMetaData
	Handles KLEE-specific LLVM IR meta-data. More...
class	KModule
class	LowerSwitchPass
class	MapOfSets
class	MemoryManager
class	MemoryObject
struct	MemoryObjectLT
	Function object ordering MemoryObject's by address. More...
class	MergeHandler
	Represents one klee_open_merge() call. Handles merging of states that branched from it. More...
class	MergingSearcher
class	MetaSMTSolver
class	NonConstantExpr
class	NotExpr
class	NotOptimizedExpr
class	ObjectState
class	OptNonePass
	Instruments every function that contains a KLEE function call as nonopt. More...
class	OvershiftCheckPass
class	PhiCleanerPass
class	PTree
class	PTreeNode
struct	Query
class	RaiseAsmPass
class	RandomPathSearcher
class	RandomSearcher
	RandomSearcher picks a state randomly. More...
class	ReadExpr
	Class representing a one byte read from an array. More...
class	ref
class	ReferenceCounter
	Reference counter to be used as part of a ref-managed struct or class. More...
class	RNG
class	Searcher
struct	SearchPhaseUnwindingInformation
class	SeedInfo
class	SelectExpr
	Class representing an if-then-else expression. More...
class	Solver
class	SolverImpl
	SolverImpl - Abstract base clase for solver implementations. More...
struct	SolverQueryMetaData
class	SpecialFunctionHandler
struct	StackFrame
class	StagedSolverImpl
class	Statistic
class	StatisticManager
class	StatisticRecord
class	StatsTracker
class	STPArrayExprHash
class	STPBuilder
class	STPSolver
	STPSolver - A complete solver based on STP. More...
struct	SwitchCaseCmp
class	SymbolicObjectFinder
class	Timer
class	TimerGroup
class	TimerStatIncrementer
class	TimingSolver
class	TreeOStream
class	TreeStreamWriter
class	UnwindingInformation
	Contains information related to unwinding (Itanium ABI/2-Phase unwinding) More...
class	UpdateList
	Class representing a complete list of updates into an array. More...
class	UpdateNode
	Class representing a byte update of an array. More...
struct	UpdateNodeCmpFn
struct	UpdateNodeHashFn
class	ValidatingSolver
class	WallTimer
class	WeightedRandomSearcher
class	Z3ArrayExprHash
class	Z3Builder
class	Z3NodeHandle
class	Z3Solver
	Z3Solver - A complete solver based on Z3. More...

Typedefs
typedef std::pair< const MemoryObject *, const ObjectState * >	ObjectPair
typedef std::vector< ObjectPair >	ResolutionList
typedef ImmutableMap< const MemoryObject *, ref< ObjectState >, MemoryObjectLT >	MemoryMap
typedef std::map< const llvm::Instruction *, std::map< const llvm::Function *, CallSiteInfo > >	CallSiteSummaryTable
typedef generic_gep_type_iterator	gep_type_iterator
typedef generic_gep_type_iterator< llvm::ExtractValueInst::idx_iterator >	ev_type_iterator
typedef generic_gep_type_iterator< llvm::InsertValueInst::idx_iterator >	iv_type_iterator
typedef generic_gep_type_iterator< llvm::SmallVector< unsigned, 4 >::const_iterator >	vce_type_iterator
typedef std::vector< std::pair< ref< ReadExpr >, ref< ConstantExpr > > >	ImpliedValueList
using	PTreeNodePtr = llvm::PointerIntPair< PTreeNode *, PtrBitCount, uint8_t >
typedef Z3NodeHandle< Z3_sort >	Z3SortHandle
typedef Z3NodeHandle< Z3_ast >	Z3ASTHandle
typedef unsigned	TreeStreamID
using	array2idx_ty = std::map< const Array *, std::vector< ref< Expr > > >
using	mapIndexOptimizedExpr_ty = std::map< ref< Expr >, std::vector< ref< Expr > > >
typedef std::unordered_set< ref< Expr >, klee::util::ExprHash, klee::util::ExprCmp >	ExprHashSet

Enumerations
enum	ArrayOptimizationType { NONE , ALL , INDEX , VALUE }
enum	QueryLoggingSolverType { ALL_KQUERY , ALL_SMTLIB , SOLVER_KQUERY , SOLVER_SMTLIB }
	The different query logging solvers that can be switched on/off. More...
enum	CoreSolverType {   STP_SOLVER , METASMT_SOLVER , DUMMY_SOLVER , Z3_SOLVER ,   NO_SOLVER }

Functions
llvm::raw_ostream &	operator<< (llvm::raw_ostream &os, const MemoryMap &mm)
cl::OptionCategory	DebugCat ("Debugging options", "These are debugging options.")
cl::OptionCategory	ExtCallsCat ("External call policy options", "These options impact external calls.")
cl::OptionCategory	SeedingCat ("Seeding options", "These options are related to the use of seeds to start exploration.")
cl::OptionCategory	TerminationCat ("State and overall termination options", "These options control termination of the overall KLEE " "execution and of individual states.")
cl::OptionCategory	TestGenCat ("Test generation options", "These options impact test generation.")
cl::opt< std::string >	MaxTime ("max-time", cl::desc("Halt execution after the specified duration. " "Set to 0s to disable (default=0s)"), cl::init("0s"), cl::cat(TerminationCat))
gep_type_iterator	gep_type_begin (const llvm::User *GEP)
gep_type_iterator	gep_type_end (const llvm::User *GEP)
gep_type_iterator	gep_type_begin (const llvm::User &GEP)
gep_type_iterator	gep_type_end (const llvm::User &GEP)
ev_type_iterator	ev_type_begin (const llvm::ExtractValueInst *EV)
ev_type_iterator	ev_type_end (const llvm::ExtractValueInst *EV)
iv_type_iterator	iv_type_begin (const llvm::InsertValueInst *IV)
iv_type_iterator	iv_type_end (const llvm::InsertValueInst *IV)
vce_type_iterator	vce_type_begin (const llvm::ConstantExpr *CE)
vce_type_iterator	vce_type_end (const llvm::ConstantExpr *CE)
template<typename ItTy >
generic_gep_type_iterator< ItTy >	gep_type_begin (llvm::Type *Op0, ItTy I, ItTy E)
template<typename ItTy >
generic_gep_type_iterator< ItTy >	gep_type_end (llvm::Type *Op0, ItTy I, ItTy E)
llvm::cl::OptionCategory	MergeCat ("Path merging options", "These options control path merging.")
llvm::cl::opt< bool >	UseMerge ("use-merge", llvm::cl::init(false), llvm::cl::desc("Enable support for path merging via klee_open_merge() and " "klee_close_merge() (default=false)"), llvm::cl::cat(klee::MergeCat))
llvm::cl::opt< bool >	DebugLogMerge ("debug-log-merge", llvm::cl::init(false), llvm::cl::desc("Debug information for path merging (default=false)"), llvm::cl::cat(klee::MergeCat))
llvm::cl::opt< bool >	UseIncompleteMerge ("use-incomplete-merge", llvm::cl::init(false), llvm::cl::desc("Heuristic-based path merging (default=false)"), llvm::cl::cat(klee::MergeCat))
llvm::cl::opt< bool >	DebugLogIncompleteMerge ("debug-log-incomplete-merge", llvm::cl::init(false), llvm::cl::desc("Debug information for incomplete path merging (default=false)"), llvm::cl::cat(klee::MergeCat))
uint64_t	computeMinDistToUncovered (const KInstruction *ki, uint64_t minDistAtRA)
bool	userSearcherRequiresMD2U ()
void	initializeSearchOptions ()
Searcher *	constructUserSearcher (Executor &executor)
llvm::cl::opt< ArrayOptimizationType >	OptimizeArray ("optimize-array", llvm::cl::values(clEnumValN(ALL, "all", "Combining index and value transformations"), clEnumValN(INDEX, "index", "Index-based transformation"), clEnumValN(VALUE, "value", "Value-based transformation at branch (both " "concrete and concrete/symbolic)")), llvm::cl::init(NONE), llvm::cl::desc("Optimize accesses to either concrete or concrete/symbolic " "arrays. (default=false)"), llvm::cl::cat(klee::SolvingCat))
llvm::cl::opt< double >	ArrayValueRatio ("array-value-ratio", llvm::cl::desc("Maximum ratio of unique values to array size for which the " "value-based transformations are applied."), llvm::cl::init(1.0), llvm::cl::value_desc("Unique Values / Array Size"), llvm::cl::cat(klee::SolvingCat))
llvm::cl::opt< double >	ArrayValueSymbRatio ("array-value-symb-ratio", llvm::cl::desc("Maximum ratio of symbolic values to array size for which " "the mixed value-based transformations are applied."), llvm::cl::init(1.0), llvm::cl::value_desc("Symbolic Values / Array Size"), llvm::cl::cat(klee::SolvingCat))
llvm::cl::OptionCategory	ExprCat ("Expression building and printing options", "These options impact the way expressions are build and printed.")
cl::OptionCategory	ModuleCat ("Module-related options", "These options affect the compile-time processing of the code.")
Solver *	createAssignmentValidatingSolver (Solver *s)
static uint32_t	ones (uint32_t x)
static uint32_t	ldz (uint32_t x)
static uint32_t	exp_base_2 (int32_t n)
void	ComputeMultConstants64 (uint64_t multiplicand, uint64_t &add, uint64_t &sub)
void	ComputeUDivConstants32 (uint32_t d, uint32_t &mprime, uint32_t &sh1, uint32_t &sh2)
void	ComputeSDivConstants32 (int32_t d, int32_t &mprime, int32_t &dsign, int32_t &shpost)
Solver *	constructSolverChain (Solver *coreSolver, std::string querySMT2LogPath, std::string baseSolverQuerySMT2LogPath, std::string queryKQueryLogPath, std::string baseSolverQueryKQueryLogPath)
Solver *	createCoreSolver (CoreSolverType cst)
Solver *	createDummySolver ()
Solver *	createMetaSMTSolver ()
cl::extrahelp	TimeFormatInfo ("\nTime format used by KLEE's options\n" "\n" " Time spans can be specified in two ways:\n" " 1. As positive real numbers representing seconds, e.g. '10', '3.5' " "but not 'INF', 'NaN', '1e3', '-4.5s'\n" " 2. As a sequence of natural numbers with specified units, e.g. " "'1h10min' (= '70min'), '5min10s' but not '3.5min', '8S'\n" " The following units are supported: h, min, s, ms, us, ns.\n")
cl::OptionCategory	SolvingCat ("Constraint solving options", "These options impact constraint solving.")
cl::opt< bool >	UseFastCexSolver ("use-fast-cex-solver", cl::init(false), cl::desc("Enable an experimental range-based solver (default=false)"), cl::cat(SolvingCat))
cl::opt< bool >	UseCexCache ("use-cex-cache", cl::init(true), cl::desc("Use the counterexample cache (default=true)"), cl::cat(SolvingCat))
cl::opt< bool >	UseBranchCache ("use-branch-cache", cl::init(true), cl::desc("Use the branch cache (default=true)"), cl::cat(SolvingCat))
cl::opt< bool >	UseIndependentSolver ("use-independent-solver", cl::init(true), cl::desc("Use constraint independence (default=true)"), cl::cat(SolvingCat))
cl::opt< bool >	DebugValidateSolver ("debug-validate-solver", cl::init(false), cl::desc("Crosscheck the results of the solver chain above the core solver " "with the results of the core solver (default=false)"), cl::cat(SolvingCat))
cl::opt< std::string >	MinQueryTimeToLog ("min-query-time-to-log", cl::desc("Set time threshold for queries logged in files. " "Only queries longer than threshold will be logged. (default=0s)"), cl::cat(SolvingCat))
cl::opt< bool >	LogTimedOutQueries ("log-timed-out-queries", cl::init(true), cl::desc("Log queries that timed out. (default=true)."), cl::cat(SolvingCat))
cl::opt< std::string >	MaxCoreSolverTime ("max-solver-time", cl::desc("Maximum amount of time for a single SMT query (default=0s (off)). " "Enables --use-forked-solver"), cl::cat(SolvingCat))
cl::opt< bool >	UseForkedCoreSolver ("use-forked-solver", cl::desc("Run the core SMT solver in a forked process (default=true)"), cl::init(true), cl::cat(SolvingCat))
cl::opt< bool >	CoreSolverOptimizeDivides ("solver-optimize-divides", cl::desc("Optimize constant divides into add/shift/multiplies before " "passing them to the core SMT solver (default=false)"), cl::init(false), cl::cat(SolvingCat))
cl::bits< QueryLoggingSolverType >	QueryLoggingOptions ("use-query-log", cl::desc("Log queries to a file. Multiple options can be specified " "separated by a comma. By default nothing is logged."), cl::values(clEnumValN(ALL_KQUERY, "all:kquery", "All queries in .kquery (KQuery) format"), clEnumValN(ALL_SMTLIB, "all:smt2", "All queries in .smt2 (SMT-LIBv2) format"), clEnumValN(SOLVER_KQUERY, "solver:kquery", "All queries reaching the solver in .kquery (KQuery) format"), clEnumValN(SOLVER_SMTLIB, "solver:smt2", "All queries reaching the solver in .smt2 (SMT-LIBv2) format")), cl::CommaSeparated, cl::cat(SolvingCat))
cl::opt< bool >	UseAssignmentValidatingSolver ("debug-assignment-validating-solver", cl::init(false), cl::desc("Debug the correctness of generated assignments (default=false)"), cl::cat(SolvingCat))
cl::opt< CoreSolverType >	CoreSolverToUse ("solver-backend", cl::desc("Specifiy the core solver backend to use"), cl::values(clEnumValN(STP_SOLVER, "stp", "STP" STP_IS_DEFAULT_STR), clEnumValN(METASMT_SOLVER, "metasmt", "metaSMT" METASMT_IS_DEFAULT_STR), clEnumValN(DUMMY_SOLVER, "dummy", "Dummy solver"), clEnumValN(Z3_SOLVER, "z3", "Z3" Z3_IS_DEFAULT_STR)), cl::init(DEFAULT_CORE_SOLVER), cl::cat(SolvingCat))
cl::opt< CoreSolverType >	DebugCrossCheckCoreSolverWith ("debug-crosscheck-core-solver", cl::desc("Specifiy a solver to use for crosschecking the results of the core solver"), cl::values(clEnumValN(STP_SOLVER, "stp", "STP"), clEnumValN(METASMT_SOLVER, "metasmt", "metaSMT"), clEnumValN(DUMMY_SOLVER, "dummy", "Dummy solver"), clEnumValN(Z3_SOLVER, "z3", "Z3"), clEnumValN(NO_SOLVER, "none", "Do not crosscheck (default)")), cl::init(NO_SOLVER), cl::cat(SolvingCat))
Solver *	createValidatingSolver (Solver *s, Solver *oracle)
cl::OptionCategory	MiscCat ("Miscellaneous options", "")
std::unique_ptr< llvm::raw_fd_ostream >	klee_open_output_file (const std::string &path, std::string &error)
template<class T >
llvm::raw_ostream &	operator<< (llvm::raw_ostream &os, const ref< T > &e)
template<class T >
std::stringstream &	operator<< (std::stringstream &os, const ref< T > &e)
bool	operator== (const Expr &lhs, const Expr &rhs)
bool	operator< (const Expr &lhs, const Expr &rhs)
bool	operator!= (const Expr &lhs, const Expr &rhs)
bool	operator> (const Expr &lhs, const Expr &rhs)
bool	operator<= (const Expr &lhs, const Expr &rhs)
bool	operator>= (const Expr &lhs, const Expr &rhs)
llvm::raw_ostream &	operator<< (llvm::raw_ostream &os, const Expr &e)
llvm::raw_ostream &	operator<< (llvm::raw_ostream &os, const Expr::Kind kind)
std::stringstream &	operator<< (std::stringstream &os, const Expr &e)
std::stringstream &	operator<< (std::stringstream &os, const Expr::Kind kind)
ExprBuilder *	createDefaultExprBuilder ()
ExprBuilder *	createConstantFoldingExprBuilder (ExprBuilder *Base)
ExprBuilder *	createSimplifyingExprBuilder (ExprBuilder *Base)
void	findReads (ref< Expr > e, bool visitUpdates, std::vector< ref< ReadExpr > > &result)
void	findSymbolicObjects (ref< Expr > e, std::vector< const Array * > &results)
template<typename InputIterator >
void	findSymbolicObjects (InputIterator begin, InputIterator end, std::vector< const Array * > &results)
Solver *	createCachingSolver (Solver *s)
Solver *	createCexCachingSolver (Solver *s)
Solver *	createFastCexSolver (Solver *s)
Solver *	createIndependentSolver (Solver *s)
Solver *	createKQueryLoggingSolver (Solver *s, std::string path, time::Span minQueryTimeToLog, bool logTimedOut)
Solver *	createSMTLIBLoggingSolver (Solver *s, std::string path, time::Span minQueryTimeToLog, bool logTimedOut)
void	klee_error (const char *msg,...) __attribute__((format(printf
void	klee_message (const char *msg,...) __attribute__((format(printf
void void	klee_message_to_file (const char *msg,...) __attribute__((format(printf
void void void	klee_warning (const char *msg,...) __attribute__((format(printf
void void void void	klee_warning_once (const void *id, const char *msg,...) __attribute__((format(printf
std::unique_ptr< llvm::Module >	linkModules (std::vector< std::unique_ptr< llvm::Module > > &modules, llvm::StringRef entryFunction, std::string &errorMsg)
llvm::Function *	getDirectCallTarget (const llvm::CallBase &cb, bool moduleIsFullyLinked)
bool	functionEscapes (const llvm::Function *f)
bool	loadFile (const std::string &libraryName, llvm::LLVMContext &context, std::vector< std::unique_ptr< llvm::Module > > &modules, std::string &errorMsg)
void	printVersion (llvm::raw_ostream &OS)

Variables
cl::opt< std::string >	MaxTime
static uint64_t *	gTheArgsP
llvm::cl::opt< bool >	UseMerge
llvm::cl::opt< bool >	DebugLogMerge
llvm::cl::opt< bool >	DebugLogIncompleteMerge
constexpr int	PtrBitCount = 3
llvm::cl::opt< bool >	UseIncompleteMerge
llvm::cl::OptionCategory	ExprCat
const char	ALL_QUERIES_SMT2_FILE_NAME [] ="all-queries.smt2"
const char	SOLVER_QUERIES_SMT2_FILE_NAME [] ="solver-queries.smt2"
const char	ALL_QUERIES_KQUERY_FILE_NAME [] ="all-queries.kquery"
const char	SOLVER_QUERIES_KQUERY_FILE_NAME [] ="solver-queries.kquery"
llvm::cl::opt< bool >	UseFastCexSolver
llvm::cl::opt< bool >	UseCexCache
llvm::cl::opt< bool >	UseBranchCache
llvm::cl::opt< bool >	UseIndependentSolver
llvm::cl::opt< bool >	DebugValidateSolver
llvm::cl::opt< std::string >	MinQueryTimeToLog
llvm::cl::opt< bool >	LogTimedOutQueries
llvm::cl::opt< std::string >	MaxCoreSolverTime
llvm::cl::opt< bool >	UseForkedCoreSolver
llvm::cl::opt< bool >	CoreSolverOptimizeDivides
llvm::cl::opt< bool >	UseAssignmentValidatingSolver
llvm::cl::bits< QueryLoggingSolverType >	QueryLoggingOptions
llvm::cl::opt< CoreSolverType >	CoreSolverToUse
llvm::cl::opt< CoreSolverType >	DebugCrossCheckCoreSolverWith
StatisticManager *	theStatisticManager = 0
const size_t	BUFSIZE = 128 * 1024
FILE *	klee_warning_file = NULL
FILE *	klee_message_file = NULL
void	noreturn
llvm::cl::OptionCategory	DebugCat
llvm::cl::OptionCategory	MergeCat
llvm::cl::OptionCategory	MiscCat
llvm::cl::OptionCategory	ModuleCat
llvm::cl::OptionCategory	SeedingCat
llvm::cl::OptionCategory	SolvingCat
llvm::cl::OptionCategory	TerminationCat
llvm::cl::OptionCategory	TestGenCat

Typedef Documentation

array2idx_ty

using klee::array2idx_ty = typedef std::map<const Array *, std::vector<ref<Expr> >>

Definition at line 28 of file ArrayExprOptimizer.h.

CallSiteSummaryTable

typedef std::map<const llvm::Instruction *, std::map<const llvm::Function *, CallSiteInfo> > klee::CallSiteSummaryTable

Definition at line 37 of file CallPathManager.h.

ev_type_iterator

typedef generic_gep_type_iterator<llvm::ExtractValueInst::idx_iterator> klee::ev_type_iterator

Definition at line 106 of file GetElementPtrTypeIterator.h.

ExprHashSet

typedef std::unordered_set<ref<Expr>, klee::util::ExprHash, klee::util::ExprCmp> klee::ExprHashSet

Definition at line 39 of file ExprHashMap.h.

gep_type_iterator

typedef generic_gep_type_iterator klee::gep_type_iterator

Definition at line 105 of file GetElementPtrTypeIterator.h.

ImpliedValueList

typedef std::vector< std::pair<ref<ReadExpr>, ref<ConstantExpr> > > klee::ImpliedValueList

Definition at line 30 of file ImpliedValue.h.

iv_type_iterator

typedef generic_gep_type_iterator<llvm::InsertValueInst::idx_iterator> klee::iv_type_iterator

Definition at line 107 of file GetElementPtrTypeIterator.h.

mapIndexOptimizedExpr_ty

using klee::mapIndexOptimizedExpr_ty = typedef std::map<ref<Expr>, std::vector<ref<Expr> >>

Definition at line 29 of file ArrayExprOptimizer.h.

MemoryMap

typedef ImmutableMap<const MemoryObject *, ref<ObjectState>, MemoryObjectLT> klee::MemoryMap

Definition at line 36 of file AddressSpace.h.

ObjectPair

typedef std::pair<const MemoryObject*, const ObjectState*> klee::ObjectPair

Definition at line 27 of file AddressSpace.h.

PTreeNodePtr

using klee::PTreeNodePtr = typedef llvm::PointerIntPair<PTreeNode *, PtrBitCount, uint8_t>

Definition at line 27 of file PTree.h.

ResolutionList

typedef std::vector<ObjectPair> klee::ResolutionList

Definition at line 28 of file AddressSpace.h.

TreeStreamID

typedef unsigned klee::TreeStreamID

Definition at line 18 of file TreeStream.h.

vce_type_iterator

typedef generic_gep_type_iterator<llvm::SmallVector<unsigned, 4>::const_iterator> klee::vce_type_iterator

Definition at line 108 of file GetElementPtrTypeIterator.h.

Z3ASTHandle

typedef Z3NodeHandle<Z3_ast> klee::Z3ASTHandle

Definition at line 91 of file Z3Builder.h.

Z3SortHandle

typedef Z3NodeHandle<Z3_sort> klee::Z3SortHandle

Definition at line 86 of file Z3Builder.h.

Enumeration Type Documentation

ArrayOptimizationType

enum klee::ArrayOptimizationType

Enumerator
NONE
ALL
INDEX
VALUE

Definition at line 26 of file ArrayExprOptimizer.h.

CoreSolverType

enum klee::CoreSolverType

Enumerator
STP_SOLVER
METASMT_SOLVER
DUMMY_SOLVER
Z3_SOLVER
NO_SOLVER

Definition at line 57 of file SolverCmdLine.h.

QueryLoggingSolverType

enum klee::QueryLoggingSolverType

The different query logging solvers that can be switched on/off.

Enumerator
ALL_KQUERY	Log all queries in .kquery (KQuery) format.
ALL_SMTLIB	Log all queries .smt2 (SMT-LIBv2) format.
SOLVER_KQUERY	Log queries passed to solver in .kquery (KQuery) format.
SOLVER_SMTLIB	Log queries passed to solver in .smt2 (SMT-LIBv2) format.

Definition at line 48 of file SolverCmdLine.h.

Function Documentation

ArrayValueRatio()

llvm::cl::opt< double > klee::ArrayValueRatio	(	"array-value-ratio"	,
		llvm::cl::desc("Maximum ratio of unique values to array size for which the " "value-based transformations are applied.")	,
		llvm::cl::init(1.0)	,
		llvm::cl::value_desc("Unique Values / Array Size")	,
		llvm::cl::cat(klee::SolvingCat)
	)

Referenced by klee::ExprOptimizer::buildConstantSelectExpr(), and klee::ExprOptimizer::buildMixedSelectExpr().

Here is the caller graph for this function:

ArrayValueSymbRatio()

llvm::cl::opt< double > klee::ArrayValueSymbRatio	(	"array-value-symb-ratio"	,
		llvm::cl::desc("Maximum ratio of symbolic values to array size for which " "the mixed value-based transformations are applied.")	,
		llvm::cl::init(1.0)	,
		llvm::cl::value_desc("Symbolic Values / Array Size")	,
		llvm::cl::cat(klee::SolvingCat)
	)

Referenced by klee::ExprOptimizer::getSelectOptExpr().

Here is the caller graph for this function:

computeMinDistToUncovered()

uint64_t klee::computeMinDistToUncovered	(	const KInstruction *	ki,
		uint64_t	minDistAtRA
	)

Definition at line 755 of file StatsTracker.cpp.

References klee::StatisticManager::getIndexedValue(), klee::InstructionInfo::id, klee::KInstruction::info, klee::stats::minDistToReturn, klee::stats::minDistToUncovered, and theStatisticManager.

Referenced by klee::StatsTracker::computeReachableUncovered(), klee::Executor::dumpStates(), klee::StatsTracker::framePushed(), and klee::WeightedRandomSearcher::getWeight().

Here is the call graph for this function:

Here is the caller graph for this function:

ComputeMultConstants64()

void klee::ComputeMultConstants64	(	uint64_t	x,
		uint64_t &	add_out,
		uint64_t &	sub_out
	)

ComputeMultConstants64 - Compute add and sub such that add-sub==x, while attempting to minimize the number of bits in add and sub combined.

Definition at line 82 of file ConstantDivision.cpp.

References add, klee::bits64::indexOfRightmostBit(), klee::bits64::indexOfSingleBit(), klee::bits64::isolateRightmostBit(), and klee::floats::sub().

Here is the call graph for this function:

ComputeSDivConstants32()

void klee::ComputeSDivConstants32	(	int32_t	d,
		int32_t &	mprime,
		int32_t &	dsign,
		int32_t &	shpost
	)

Compute the constants to perform a quicker equivalent of a division of some 32-bit signed integer n by a known constant d (also a 32-bit signed integer). The constants to compute n/d without explicit division will be stored in mprime, dsign, and shpost (signed 32-bit integers).

Parameters

	d	- denominator (divisor)
[out]	mprime
[out]	dsign
[out]	shpost

Definition at line 128 of file ConstantDivision.cpp.

References ABS, exp_base_2(), LOG2_CEIL, TWO_TO_THE_31_S64, TWO_TO_THE_32_U64, and XSIGN.

Here is the call graph for this function:

ComputeUDivConstants32()

void klee::ComputeUDivConstants32	(	uint32_t	d,
		uint32_t &	mprime,
		uint32_t &	sh1,
		uint32_t &	sh2
	)

Compute the constants to perform a quicker equivalent of a division of some 32-bit unsigned integer n by a known constant d (also a 32-bit unsigned integer). The constants to compute n/d without explicit division will be stored in mprime, sh1, and sh2 (unsigned 32-bit integers).

Parameters

	d	- denominator (divisor)
[out]	mprime
[out]	sh1
[out]	sh2

Definition at line 118 of file ConstantDivision.cpp.

References exp_base_2(), LOG2_CEIL, and TWO_TO_THE_32_U64.

Here is the call graph for this function:

constructSolverChain()

Solver * klee::constructSolverChain	(	Solver *	coreSolver,
		std::string	querySMT2LogPath,
		std::string	baseSolverQuerySMT2LogPath,
		std::string	queryKQueryLogPath,
		std::string	baseSolverQueryKQueryLogPath
	)

Definition at line 23 of file ConstructSolverChain.cpp.

References ALL_KQUERY, ALL_SMTLIB, createAssignmentValidatingSolver(), createCachingSolver(), createCexCachingSolver(), createCoreSolver(), createFastCexSolver(), createIndependentSolver(), createKQueryLoggingSolver(), createSMTLIBLoggingSolver(), createValidatingSolver(), DebugCrossCheckCoreSolverWith, DebugValidateSolver, klee_message(), LogTimedOutQueries, MinQueryTimeToLog, NO_SOLVER, QueryLoggingOptions, SOLVER_KQUERY, SOLVER_SMTLIB, UseAssignmentValidatingSolver, UseBranchCache, UseCexCache, UseFastCexSolver, and UseIndependentSolver.

Referenced by EvaluateInputAST(), and klee::Executor::Executor().

Here is the call graph for this function:

Here is the caller graph for this function:

constructUserSearcher()

Searcher * klee::constructUserSearcher

(

Executor &

executor

)

Definition at line 125 of file UserSearcher.cpp.

References klee::Executor::getHandler(), klee::InterpreterHandler::getInfoStream(), getNewSearcher(), klee::Searcher::printName(), klee::Executor::processTree, klee::Executor::setMergingSearcher(), klee::Executor::theRNG, and UseMerge.

Referenced by klee::Executor::run().

Here is the call graph for this function:

Here is the caller graph for this function:

CoreSolverOptimizeDivides()

cl::opt< bool > klee::CoreSolverOptimizeDivides	(	"solver-optimize-divides"	,
		cl::desc("Optimize constant divides into add/shift/multiplies before " "passing them to the core SMT solver (default=false)")	,
		cl::init(false)	,
		cl::cat(SolvingCat)
	)

CoreSolverToUse()

cl::opt< CoreSolverType > klee::CoreSolverToUse	(	"solver-backend"	,
		cl::desc("Specifiy the core solver backend to use")	,
		cl::values(clEnumValN(STP_SOLVER, "stp", "STP" STP_IS_DEFAULT_STR), clEnumValN(METASMT_SOLVER, "metasmt", "metaSMT" METASMT_IS_DEFAULT_STR), clEnumValN(DUMMY_SOLVER, "dummy", "Dummy solver"), clEnumValN(Z3_SOLVER, "z3", "Z3" Z3_IS_DEFAULT_STR))	,
		cl::init(DEFAULT_CORE_SOLVER)	,
		cl::cat(SolvingCat)
	)

createAssignmentValidatingSolver()

Solver * klee::createAssignmentValidatingSolver

(

Solver *

s

)

createAssignmentValidatingSolver - Create a solver that when requested for an assignment will check that the computed assignment satisfies the Query.

Parameters

s	- The underlying solver to use.

Definition at line 151 of file AssignmentValidatingSolver.cpp.

Referenced by constructSolverChain().

Here is the caller graph for this function:

createCachingSolver()

Solver * klee::createCachingSolver

(

Solver *

s

)

createCachingSolver - Create a solver which will cache the queries in memory (without eviction).

Parameters

s	- The underlying solver to use.

Definition at line 258 of file CachingSolver.cpp.

Referenced by constructSolverChain().

Here is the caller graph for this function:

createCexCachingSolver()

Solver * klee::createCexCachingSolver

(

Solver *

s

)

createCexCachingSolver - Create a counterexample caching solver. This is a more sophisticated cache which records counterexamples for a constraint set and uses subset/superset relations among constraints to try and quickly find satisfying assignments.

Parameters

s	- The underlying solver to use.

Definition at line 386 of file CexCachingSolver.cpp.

Referenced by constructSolverChain().

Here is the caller graph for this function:

createConstantFoldingExprBuilder()

ExprBuilder * klee::createConstantFoldingExprBuilder

(

ExprBuilder *

Base

)

createConstantFoldingExprBuilder - Create an expression builder which folds constant expressions.

Base - The base builder to use when constructing expressions.

Definition at line 1061 of file ExprBuilder.cpp.

Referenced by main().

Here is the caller graph for this function:

createCoreSolver()

Solver * klee::createCoreSolver

(

CoreSolverType

cst

)

Definition at line 25 of file CoreSolver.cpp.

References CoreSolverOptimizeDivides, createDummySolver(), createMetaSMTSolver(), DUMMY_SOLVER, klee_message(), METASMT_SOLVER, NO_SOLVER, STP_SOLVER, UseForkedCoreSolver, and Z3_SOLVER.

Referenced by constructSolverChain(), EvaluateInputAST(), and klee::Executor::Executor().

Here is the call graph for this function:

Here is the caller graph for this function:

createDefaultExprBuilder()

ExprBuilder * klee::createDefaultExprBuilder

(

)

createDefaultExprBuilder - Create an expression builder which does no folding.

Definition at line 1057 of file ExprBuilder.cpp.

Referenced by klee::ExprOptimizer::buildConstantSelectExpr(), klee::ExprOptimizer::buildMixedSelectExpr(), and main().

Here is the caller graph for this function:

createDummySolver()

Solver * klee::createDummySolver

(

)

createDummySolver - Create a dummy solver implementation which always fails.

Definition at line 62 of file DummySolver.cpp.

Referenced by createCoreSolver().

Here is the caller graph for this function:

createFastCexSolver()

Solver * klee::createFastCexSolver

(

Solver *

s

)

createFastCexSolver - Create a "fast counterexample solver", which tries to quickly compute a satisfying assignment for a constraint set using value propogation and range analysis.

Parameters

s	- The underlying solver to use.

Definition at line 1141 of file FastCexSolver.cpp.

Referenced by constructSolverChain().

Here is the caller graph for this function:

createIndependentSolver()

Solver * klee::createIndependentSolver

(

Solver *

s

)

createIndependentSolver - Create a solver which will eliminate any unnecessary constraints before propogating the query to the underlying solver.

Parameters

s	- The underlying solver to use.

Definition at line 560 of file IndependentSolver.cpp.

Referenced by constructSolverChain().

Here is the caller graph for this function:

createKQueryLoggingSolver()

Solver * klee::createKQueryLoggingSolver	(	Solver *	s,
		std::string	path,
		time::Span	minQueryTimeToLog,
		bool	logTimedOut
	)

createKQueryLoggingSolver - Create a solver which will forward all queries after writing them to the given path in .kquery format.

Definition at line 63 of file KQueryLoggingSolver.cpp.

Referenced by constructSolverChain().

Here is the caller graph for this function:

createMetaSMTSolver()

Solver * klee::createMetaSMTSolver

(

)

createMetaSMTSolver - Create a solver using the metaSMT backend set by the option MetaSMTBackend.

Referenced by createCoreSolver().

Here is the caller graph for this function:

createSimplifyingExprBuilder()

ExprBuilder * klee::createSimplifyingExprBuilder

(

ExprBuilder *

Base

)

createSimplifyingExprBuilder - Create an expression builder which attemps to fold redundant expressions and normalize expressions for improved caching.

Base - The base builder to use when constructing expressions.

Definition at line 1065 of file ExprBuilder.cpp.

Referenced by main().

Here is the caller graph for this function:

createSMTLIBLoggingSolver()

Solver * klee::createSMTLIBLoggingSolver	(	Solver *	s,
		std::string	path,
		time::Span	minQueryTimeToLog,
		bool	logTimedOut
	)

createSMTLIBLoggingSolver - Create a solver which will forward all queries after writing them to the given path in .smt2 format.

Definition at line 58 of file SMTLIBLoggingSolver.cpp.

Referenced by constructSolverChain().

Here is the caller graph for this function:

createValidatingSolver()

Solver * klee::createValidatingSolver	(	Solver *	s,
		Solver *	oracle
	)

createValidatingSolver - Create a solver which will validate all query results against an oracle, used for testing that an optimized solver has the same results as an unoptimized one. This solver will assert on any mismatches.

Parameters

s	- The primary underlying solver to use.
oracle	- The solver to check query results against.

Definition at line 139 of file ValidatingSolver.cpp.

Referenced by constructSolverChain().

Here is the caller graph for this function:

DebugCat()

cl::OptionCategory klee::DebugCat	(	"Debugging options"	,
		"These are debugging options."
	)

DebugCrossCheckCoreSolverWith()

cl::opt< CoreSolverType > klee::DebugCrossCheckCoreSolverWith	(	"debug-crosscheck-core-solver"	,
		cl::desc("Specifiy a solver to use for crosschecking the results of the core solver")	,
		cl::values(clEnumValN(STP_SOLVER, "stp", "STP"), clEnumValN(METASMT_SOLVER, "metasmt", "metaSMT"), clEnumValN(DUMMY_SOLVER, "dummy", "Dummy solver"), clEnumValN(Z3_SOLVER, "z3", "Z3"), clEnumValN(NO_SOLVER, "none", "Do not crosscheck (default)"))	,
		cl::init(NO_SOLVER)	,
		cl::cat(SolvingCat)
	)

DebugLogIncompleteMerge()

llvm::cl::opt< bool > klee::DebugLogIncompleteMerge	(	"debug-log-incomplete-merge"	,
		llvm::cl::init(false)	,
		llvm::cl::desc("Debug information for incomplete path merging (default=false)")	,
		llvm::cl::cat(klee::MergeCat)
	)

DebugLogMerge()

llvm::cl::opt< bool > klee::DebugLogMerge	(	"debug-log-merge"	,
		llvm::cl::init(false)	,
		llvm::cl::desc("Debug information for path merging (default=false)")	,
		llvm::cl::cat(klee::MergeCat)
	)

DebugValidateSolver()

cl::opt< bool > klee::DebugValidateSolver	(	"debug-validate-solver"	,
		cl::init(false)	,
		cl::desc("Crosscheck the results of the solver chain above the core solver " "with the results of the core solver (default=false)")	,
		cl::cat(SolvingCat)
	)

ev_type_begin()

ev_type_iterator klee::ev_type_begin ( const llvm::ExtractValueInst *  EV )

inline

Definition at line 125 of file GetElementPtrTypeIterator.h.

References klee::generic_gep_type_iterator< ItTy >::begin().

Referenced by klee::Executor::bindInstructionConstants().

Here is the call graph for this function:

Here is the caller graph for this function:

ev_type_end()

ev_type_iterator klee::ev_type_end ( const llvm::ExtractValueInst *  EV )

inline

Definition at line 129 of file GetElementPtrTypeIterator.h.

References klee::generic_gep_type_iterator< ItTy >::end().

Referenced by klee::Executor::bindInstructionConstants().

Here is the call graph for this function:

Here is the caller graph for this function:

exp_base_2()

static uint32_t klee::exp_base_2 ( int32_t  n )

static

Definition at line 65 of file ConstantDivision.cpp.

Referenced by ComputeSDivConstants32(), and ComputeUDivConstants32().

Here is the caller graph for this function:

ExprCat()

llvm::cl::OptionCategory klee::ExprCat	(	"Expression building and printing options"	,
		"These options impact the way expressions are build and printed."
	)

ExtCallsCat()

cl::OptionCategory klee::ExtCallsCat	(	"External call policy options"	,
		"These options impact external calls."
	)

findReads()

void klee::findReads	(	ref< Expr >	e,
		bool	visitUpdates,
		std::vector< ref< ReadExpr > > &	result
	)

Find all ReadExprs used in the expression DAG. If visitUpdates is true then this will including those reachable by traversing update lists. Note that this may be slow and return a large number of results.

Definition at line 19 of file ExprUtil.cpp.

References klee::ref< T >::get(), klee::Expr::getKid(), and klee::Expr::getNumKids().

Referenced by klee::ImpliedValue::checkForImpliedValues(), IndependentElementSet::IndependentElementSet(), and klee::SeedInfo::patchSeed().

Here is the call graph for this function:

Here is the caller graph for this function:

findSymbolicObjects() [1/2]

template<typename InputIterator >

void klee::findSymbolicObjects	(	InputIterator	begin,
		InputIterator	end,
		std::vector< const Array * > &	results
	)

Return a list of all unique symbolic objects referenced by the given expression range.

Definition at line 124 of file ExprUtil.cpp.

References klee::ExprVisitor::visit().

Here is the call graph for this function:

findSymbolicObjects() [2/2]

void klee::findSymbolicObjects	(	ref< Expr >	e,
		std::vector< const Array * > &	results
	)

Return a list of all unique symbolic objects referenced by the given expression.

Definition at line 132 of file ExprUtil.cpp.

References findSymbolicObjects().

Referenced by findSymbolicObjects(), and CexCachingSolver::getAssignment().

Here is the call graph for this function:

Here is the caller graph for this function:

functionEscapes()

bool klee::functionEscapes

(

const llvm::Function *

f

)

Return true iff the given Function value is used in something other than a direct call (or a constant expression that terminates in a direct call).

Referenced by klee::KModule::manifest(), and valueIsOnlyCalled().

Here is the caller graph for this function:

gep_type_begin() [1/3]

gep_type_iterator klee::gep_type_begin ( const llvm::User &  GEP )

inline

Definition at line 117 of file GetElementPtrTypeIterator.h.

References klee::generic_gep_type_iterator< ItTy >::begin().

Here is the call graph for this function:

gep_type_begin() [2/3]

gep_type_iterator klee::gep_type_begin ( const llvm::User *  GEP )

inline

Definition at line 110 of file GetElementPtrTypeIterator.h.

References klee::generic_gep_type_iterator< ItTy >::begin().

Referenced by klee::Executor::bindInstructionConstants(), and klee::Executor::evalConstantExpr().

Here is the call graph for this function:

Here is the caller graph for this function:

gep_type_begin() [3/3]

template<typename ItTy >

generic_gep_type_iterator< ItTy > klee::gep_type_begin ( llvm::Type *  Op0, ItTy  I, ItTy  E  )

inline

Definition at line 150 of file GetElementPtrTypeIterator.h.

References klee::generic_gep_type_iterator< ItTy >::begin().

Here is the call graph for this function:

gep_type_end() [1/3]

gep_type_iterator klee::gep_type_end ( const llvm::User &  GEP )

inline

Definition at line 121 of file GetElementPtrTypeIterator.h.

References klee::generic_gep_type_iterator< ItTy >::end().

Here is the call graph for this function:

gep_type_end() [2/3]

gep_type_iterator klee::gep_type_end ( const llvm::User *  GEP )

inline

Definition at line 114 of file GetElementPtrTypeIterator.h.

References klee::generic_gep_type_iterator< ItTy >::end().

Referenced by klee::Executor::bindInstructionConstants(), and klee::Executor::evalConstantExpr().

Here is the call graph for this function:

Here is the caller graph for this function:

gep_type_end() [3/3]

template<typename ItTy >

generic_gep_type_iterator< ItTy > klee::gep_type_end ( llvm::Type *  Op0, ItTy  I, ItTy  E  )

inline

Definition at line 156 of file GetElementPtrTypeIterator.h.

References klee::generic_gep_type_iterator< ItTy >::end().

Here is the call graph for this function:

getDirectCallTarget()

llvm::Function * klee::getDirectCallTarget	(	const llvm::CallBase &	cb,
		bool	moduleIsFullyLinked
	)

Return the Function* target of a Call or Invoke instruction, or null if it cannot be determined (should be only for indirect calls, although complicated constant expressions might be another possibility).

If moduleIsFullyLinked is set to true it will be assumed that the module containing the llvm::CallSite (llvm::CallBase on LLVM 8+) is fully linked. This assumption allows resolution of functions that are marked as overridable.

Referenced by klee::StatsTracker::computeReachableUncovered(), klee::Executor::getAllocationAlignment(), and instructionIsCoverable().

Here is the caller graph for this function:

initializeSearchOptions()

void klee::initializeSearchOptions

(

)

Definition at line 84 of file UserSearcher.cpp.

References klee_warning(), and UseMerge.

Referenced by klee::Executor::Executor().

Here is the call graph for this function:

Here is the caller graph for this function:

iv_type_begin()

iv_type_iterator klee::iv_type_begin ( const llvm::InsertValueInst *  IV )

inline

Definition at line 133 of file GetElementPtrTypeIterator.h.

References klee::generic_gep_type_iterator< ItTy >::begin().

Referenced by klee::Executor::bindInstructionConstants().

Here is the call graph for this function:

Here is the caller graph for this function:

iv_type_end()

iv_type_iterator klee::iv_type_end ( const llvm::InsertValueInst *  IV )

inline

Definition at line 137 of file GetElementPtrTypeIterator.h.

References klee::generic_gep_type_iterator< ItTy >::end().

Referenced by klee::Executor::bindInstructionConstants().

Here is the call graph for this function:

Here is the caller graph for this function:

klee_error()

void klee::klee_error	(	const char *	msg,
			...
	)

Print "KLEE: ERROR: " followed by the msg in printf format and a newline on stderr and to warnings.txt, then exit with an error.

Definition at line 145 of file ErrorHandling.cpp.

References errorPrefix, and klee_vmessage().

Referenced by klee::MemoryManager::allocateFixed(), klee::Executor::allocateGlobalObjects(), klee::Executor::callExternalFunction(), klee::KModule::checkModule(), klee::Executor::evalConstant(), klee::Executor::evalConstantExpr(), klee::Executor::Executor(), CexCachingSolver::getAssignment(), klee::PTree::getNextId(), klee::util::GetTotalMallocUsage(), klee::Executor::initializeGlobalObjects(), injectStaticConstructorsAndDestructors(), KleeHandler::KleeHandler(), klee::KModule::link(), linkWithUclibc(), main(), klee::MemoryManager::MemoryManager(), klee::KModule::optimiseAndPrepare(), preparePOSIX(), KleeHandler::processTestCase(), QueryLoggingSolver::QueryLoggingSolver(), klee::Executor::runFunctionAsMain(), klee::FunctionAliasPass::runOnModule(), klee::Executor::setModule(), klee::time::Span::Span(), klee::StatsTracker::StatsTracker(), valueIsOnlyCalled(), klee::StatsTracker::writeStatsHeader(), and klee::StatsTracker::writeStatsLine().

Here is the call graph for this function:

Here is the caller graph for this function:

klee_message()

void klee::klee_message	(	const char *	msg,
			...
	)

Print "KLEE: " followed by the msg in printf format and a newline on stderr and to messages.txt.

Definition at line 130 of file ErrorHandling.cpp.

References klee_vmessage().

Referenced by klee::KModule::addInternalFunction(), constructSolverChain(), createCoreSolver(), klee::Executor::doDumpStates(), klee::Executor::executeAlloc(), klee::Executor::Executor(), KleeHandler::KleeHandler(), main(), klee::MemoryManager::MemoryManager(), klee::Executor::run(), klee::FunctionAliasPass::runOnModule(), klee::BatchingSearcher::selectState(), klee::Executor::terminateStateOnError(), and klee::IterativeDeepeningTimeSearcher::update().

Here is the call graph for this function:

Here is the caller graph for this function:

klee_message_to_file()

void klee::klee_message_to_file	(	const char *	msg,
			...
	)

Print "KLEE: " followed by the msg in printf format and a newline to messages.txt.

Definition at line 138 of file ErrorHandling.cpp.

References klee_vmessage().

Here is the call graph for this function:

klee_open_output_file()

std::unique_ptr< llvm::raw_fd_ostream > klee::klee_open_output_file	(	const std::string &	path,
		std::string &	error
	)

Definition at line 24 of file FileHandling.cpp.

Referenced by klee::Executor::Executor(), KleeHandler::openOutputFile(), and QueryLoggingSolver::QueryLoggingSolver().

Here is the caller graph for this function:

klee_warning()

void klee::klee_warning	(	const char *	msg,
			...
	)

Print "KLEE: WARNING: " followed by the msg in printf format and a newline on stderr and to warnings.txt.

Definition at line 153 of file ErrorHandling.cpp.

References klee_vmessage(), and warningPrefix.

Referenced by klee::TimerGroup::add(), klee::Executor::addConstraint(), klee::KModule::addInternalFunction(), klee::MemoryManager::allocate(), klee::Executor::allocateGlobalObjects(), klee::Executor::callExternalFunction(), klee::Executor::checkMemoryUsage(), klee::FunctionAliasPass::checkType(), klee::Executor::executeCall(), klee::Executor::executeInstruction(), klee::ObjectState::flushToConcreteStore(), klee::Executor::getConstraintLog(), klee::Executor::getSymbolicSolution(), klee::time::getUserTime(), klee::AssignmentGenerator::helperGenerateAssignment(), klee::ExprOptimizer::optimizeExpr(), klee::Executor::run(), klee::RaiseAsmPass::runOnModule(), klee::FunctionAliasPass::runOnModule(), klee::StatsTracker::StatsTracker(), klee::Executor::toConstant(), klee::StatsTracker::writeStatsLine(), and klee::StatsTracker::~StatsTracker().

Here is the call graph for this function:

Here is the caller graph for this function:

klee_warning_once()

void klee::klee_warning_once	(	const void *	id,
		const char *	msg,
			...
	)

Print "KLEE: WARNING: " followed by the msg in printf format and a newline on stderr and to warnings.txt. However, the warning is only printed once for each unique (id, msg) pair (as pointers).

Definition at line 161 of file ErrorHandling.cpp.

References klee_vmessage(), and warningOncePrefix.

Referenced by klee::MemoryManager::allocate(), klee::Executor::branchingPermitted(), klee::Executor::callExternalFunction(), klee::Executor::evalConstant(), klee::Executor::executeCall(), klee::Executor::executeInstruction(), klee::Executor::getAllocationAlignment(), klee::SeedInfo::getNextInput(), klee::Executor::maxStaticPctChecks(), klee::ObjectState::read8(), klee::SpecialFunctionHandler::readStringAtAddress(), klee::IntrinsicCleanerPass::runOnBasicBlock(), klee::Executor::terminateState(), klee::Executor::toConstant(), and klee::ObjectState::write8().

Here is the call graph for this function:

Here is the caller graph for this function:

ldz()

static uint32_t klee::ldz ( uint32_t  x )

static

Definition at line 54 of file ConstantDivision.cpp.

References ones().

Here is the call graph for this function:

linkModules()

std::unique_ptr< llvm::Module > klee::linkModules	(	std::vector< std::unique_ptr< llvm::Module > > &	modules,
		llvm::StringRef	entryFunction,
		std::string &	errorMsg
	)

Links all the modules together into one and returns it.

All the modules which are used for resolving entities are freed, all the remaining ones are preserved.

Parameters

modules	List of modules to link together: if resolveOnly true, everything is linked against the first entry.
entryFunction	if set, missing functions of the module containing the entry function will be solved.

Returns

final module or null in this case errorMsg is set

Definition at line 146 of file ModuleUtil.cpp.

References GetAllUndefinedSymbols(), and linkTwoModules().

Referenced by klee::KModule::link(), linkTwoModules(), and main().

Here is the call graph for this function:

Here is the caller graph for this function:

loadFile()

bool klee::loadFile	(	const std::string &	libraryName,
		llvm::LLVMContext &	context,
		std::vector< std::unique_ptr< llvm::Module > > &	modules,
		std::string &	errorMsg
	)

Loads the file libraryName and reads all possible modules out of it.

Different file types are possible:

• .bc binary file
• .ll IR file
• .a archive containing .bc and .ll files

Parameters

libraryName	library to read
modules	contains extracted modules
errorMsg	contains the error description in case the file could not be loaded

Returns

true if successful otherwise false

Referenced by main(), klee::Executor::setModule(), and valueIsOnlyCalled().

Here is the caller graph for this function:

LogTimedOutQueries()

cl::opt< bool > klee::LogTimedOutQueries	(	"log-timed-out-queries"	,
		cl::init(true)	,
		cl::desc("Log queries that timed out. (default=true).")	,
		cl::cat(SolvingCat)
	)

MaxCoreSolverTime()

cl::opt< std::string > klee::MaxCoreSolverTime	(	"max-solver-time"	,
		cl::desc("Maximum amount of time for a single SMT query (default=0s (off)). " "Enables --use-forked-solver")	,
		cl::cat(SolvingCat)
	)

MaxTime()

cl::opt< std::string > klee::MaxTime	(	"max-time"	,
		cl::desc("Halt execution after the specified duration. " "Set to 0s to disable (default=0s)")	,
		cl::init("0s")	,
		cl::cat(TerminationCat)
	)

MergeCat()

llvm::cl::OptionCategory klee::MergeCat	(	"Path merging options"	,
		"These options control path merging."
	)

MinQueryTimeToLog()

cl::opt< std::string > klee::MinQueryTimeToLog	(	"min-query-time-to-log"	,
		cl::desc("Set time threshold for queries logged in files. " "Only queries longer than threshold will be logged. (default=0s)")	,
		cl::cat(SolvingCat)
	)

MiscCat()

cl::OptionCategory klee::MiscCat	(	"Miscellaneous options"	,
		""
	)

ModuleCat()

cl::OptionCategory klee::ModuleCat	(	"Module-related options"	,
		"These options affect the compile-time processing of the code."
	)

ones()

static uint32_t klee::ones ( uint32_t  x )

static

Definition at line 43 of file ConstantDivision.cpp.

Referenced by ldz().

Here is the caller graph for this function:

operator!=()

bool klee::operator!= ( const Expr &  lhs, const Expr &  rhs  )

inline

Definition at line 314 of file Expr.h.

operator<()

bool klee::operator< ( const Expr &  lhs, const Expr &  rhs  )

inline

Definition at line 310 of file Expr.h.

References klee::Expr::compare().

Here is the call graph for this function:

operator<<() [1/7]

llvm::raw_ostream & klee::operator<< ( llvm::raw_ostream &  os, const Expr &  e  )

inline

Definition at line 332 of file Expr.h.

References klee::Expr::print().

Here is the call graph for this function:

operator<<() [2/7]

llvm::raw_ostream & klee::operator<< ( llvm::raw_ostream &  os, const Expr::Kind  kind  )

inline

Definition at line 337 of file Expr.h.

References klee::Expr::printKind().

Here is the call graph for this function:

operator<<() [3/7]

llvm::raw_ostream & klee::operator<<	(	llvm::raw_ostream &	os,
		const MemoryMap &	mm
	)

Definition at line 141 of file ExecutionState.cpp.

References klee::ImmutableMap< K, D, CMP >::begin(), and klee::ImmutableMap< K, D, CMP >::end().

Here is the call graph for this function:

operator<<() [4/7]

template<class T >

llvm::raw_ostream & klee::operator<< ( llvm::raw_ostream &  os, const ref< T > &  e  )

inline

Definition at line 229 of file Ref.h.

operator<<() [5/7]

std::stringstream & klee::operator<< ( std::stringstream &  os, const Expr &  e  )

inline

Definition at line 342 of file Expr.h.

References klee::Expr::print().

Here is the call graph for this function:

operator<<() [6/7]

std::stringstream & klee::operator<< ( std::stringstream &  os, const Expr::Kind  kind  )

inline

Definition at line 350 of file Expr.h.

References klee::Expr::printKind().

Here is the call graph for this function:

operator<<() [7/7]

template<class T >

std::stringstream & klee::operator<< ( std::stringstream &  os, const ref< T > &  e  )

inline

Definition at line 235 of file Ref.h.

operator<=()

bool klee::operator<= ( const Expr &  lhs, const Expr &  rhs  )

inline

Definition at line 322 of file Expr.h.

operator==()

bool klee::operator== ( const Expr &  lhs, const Expr &  rhs  )

inline

Definition at line 306 of file Expr.h.

References klee::Expr::compare().

Here is the call graph for this function:

operator>()

bool klee::operator> ( const Expr &  lhs, const Expr &  rhs  )

inline

Definition at line 318 of file Expr.h.

operator>=()

bool klee::operator>= ( const Expr &  lhs, const Expr &  rhs  )

inline

Definition at line 326 of file Expr.h.

OptimizeArray()

llvm::cl::opt< ArrayOptimizationType > klee::OptimizeArray	(	"optimize-array"	,
		llvm::cl::values(clEnumValN(ALL, "all", "Combining index and value transformations"), clEnumValN(INDEX, "index", "Index-based transformation"), clEnumValN(VALUE, "value", "Value-based transformation at branch (both " "concrete and concrete/symbolic)"))	,
		llvm::cl::init(NONE)	,
		llvm::cl::desc("Optimize accesses to either concrete or concrete/symbolic " "arrays. (default=false)")	,
		llvm::cl::cat(klee::SolvingCat)
	)

Referenced by klee::ExprOptimizer::optimizeExpr().

Here is the caller graph for this function:

printVersion()

void klee::printVersion

(

llvm::raw_ostream &

OS

)

Definition at line 18 of file PrintVersion.cpp.

Referenced by main(), and parseArguments().

Here is the caller graph for this function:

QueryLoggingOptions()

cl::bits< QueryLoggingSolverType > klee::QueryLoggingOptions	(	"use-query-log"	,
		cl::desc("Log queries to a file. Multiple options can be specified " "separated by a comma. By default nothing is logged.")	,
		cl::values(clEnumValN(ALL_KQUERY, "all:kquery", "All queries in .kquery (KQuery) format"), clEnumValN(ALL_SMTLIB, "all:smt2", "All queries in .smt2 (SMT-LIBv2) format"), clEnumValN(SOLVER_KQUERY, "solver:kquery", "All queries reaching the solver in .kquery (KQuery) format"), clEnumValN(SOLVER_SMTLIB, "solver:smt2", "All queries reaching the solver in .smt2 (SMT-LIBv2) format"))	,
		cl::CommaSeparated	,
		cl::cat(SolvingCat)
	)

SeedingCat()

cl::OptionCategory klee::SeedingCat	(	"Seeding options"	,
		"These options are related to the use of seeds to start exploration."
	)

SolvingCat()

cl::OptionCategory klee::SolvingCat	(	"Constraint solving options"	,
		"These options impact constraint solving."
	)

TerminationCat()

cl::OptionCategory klee::TerminationCat	(	"State and overall termination options"	,
		"These options control termination of the overall KLEE " "execution and of individual states."
	)

TestGenCat()

cl::OptionCategory klee::TestGenCat	(	"Test generation options"	,
		"These options impact test generation."
	)

TimeFormatInfo()

cl::extrahelp klee::TimeFormatInfo	(	"\nTime format used by KLEE's options\n" "\n" " Time spans can be specified in two ways:\n" " 1. As positive real numbers representing	seconds,
		e.g. '10'	,
		'3.5' " "but not 'INF'	,
		'NaN'	,
		'1e3'	,
		'-4.5s'\n" " 2. As a sequence of natural numbers with specified	units,
		e.g. " " '1h10min'	='70min',
		'5min10s' but not '3.5min'	,
		'8S'\n" " The following units are supported:h	,
		min	,
		s	,
		ms	,
		us	,
		ns.\n"
	)

UseAssignmentValidatingSolver()

cl::opt< bool > klee::UseAssignmentValidatingSolver	(	"debug-assignment-validating-solver"	,
		cl::init(false)	,
		cl::desc("Debug the correctness of generated assignments (default=false)")	,
		cl::cat(SolvingCat)
	)

UseBranchCache()

cl::opt< bool > klee::UseBranchCache	(	"use-branch-cache"	,
		cl::init(true)	,
		cl::desc("Use the branch cache (default=true)")	,
		cl::cat(SolvingCat)
	)

UseCexCache()

cl::opt< bool > klee::UseCexCache	(	"use-cex-cache"	,
		cl::init(true)	,
		cl::desc("Use the counterexample cache (default=true)")	,
		cl::cat(SolvingCat)
	)

UseFastCexSolver()

cl::opt< bool > klee::UseFastCexSolver	(	"use-fast-cex-solver"	,
		cl::init(false)	,
		cl::desc("Enable an experimental range-based solver (default=false)")	,
		cl::cat(SolvingCat)
	)

UseForkedCoreSolver()

cl::opt< bool > klee::UseForkedCoreSolver	(	"use-forked-solver"	,
		cl::desc("Run the core SMT solver in a forked process (default=true)")	,
		cl::init(true)	,
		cl::cat(SolvingCat)
	)

UseIncompleteMerge()

llvm::cl::opt< bool > klee::UseIncompleteMerge	(	"use-incomplete-merge"	,
		llvm::cl::init(false)	,
		llvm::cl::desc("Heuristic-based path merging (default=false)")	,
		llvm::cl::cat(klee::MergeCat)
	)

UseIndependentSolver()

cl::opt< bool > klee::UseIndependentSolver	(	"use-independent-solver"	,
		cl::init(true)	,
		cl::desc("Use constraint independence (default=true)")	,
		cl::cat(SolvingCat)
	)

UseMerge()

llvm::cl::opt< bool > klee::UseMerge	(	"use-merge"	,
		llvm::cl::init(false)	,
		llvm::cl::desc("Enable support for path merging via klee_open_merge() and " "klee_close_merge() (default=false)")	,
		llvm::cl::cat(klee::MergeCat)
	)

userSearcherRequiresMD2U()

bool klee::userSearcherRequiresMD2U

(

)

Definition at line 97 of file UserSearcher.cpp.

Referenced by klee::Executor::setModule(), and klee::StatsTracker::StatsTracker().

Here is the caller graph for this function:

vce_type_begin()

vce_type_iterator klee::vce_type_begin ( const llvm::ConstantExpr *  CE )

inline

Definition at line 141 of file GetElementPtrTypeIterator.h.

References klee::generic_gep_type_iterator< ItTy >::begin().

Here is the call graph for this function:

vce_type_end()

vce_type_iterator klee::vce_type_end ( const llvm::ConstantExpr *  CE )

inline

Definition at line 145 of file GetElementPtrTypeIterator.h.

References klee::generic_gep_type_iterator< ItTy >::end().

Here is the call graph for this function:

Variable Documentation

ALL_QUERIES_KQUERY_FILE_NAME

const char klee::ALL_QUERIES_KQUERY_FILE_NAME[] ="all-queries.kquery"

Definition at line 24 of file Common.h.

Referenced by EvaluateInputAST(), and klee::Executor::Executor().

ALL_QUERIES_SMT2_FILE_NAME

const char klee::ALL_QUERIES_SMT2_FILE_NAME[] ="all-queries.smt2"

Definition at line 22 of file Common.h.

Referenced by EvaluateInputAST(), and klee::Executor::Executor().

BUFSIZE

const size_t klee::BUFSIZE = 128 * 1024

Definition at line 17 of file CompressionStream.h.

CoreSolverOptimizeDivides

llvm::cl::opt<bool> klee::CoreSolverOptimizeDivides

extern

Referenced by createCoreSolver().

CoreSolverToUse

llvm::cl::opt<CoreSolverType> klee::CoreSolverToUse

extern

Referenced by EvaluateInputAST(), and klee::Executor::Executor().

DebugCat

llvm::cl::OptionCategory klee::DebugCat

extern

DebugCrossCheckCoreSolverWith

llvm::cl::opt<CoreSolverType> klee::DebugCrossCheckCoreSolverWith

extern

Referenced by constructSolverChain().

DebugLogIncompleteMerge

llvm::cl::opt<bool> klee::DebugLogIncompleteMerge

extern

Referenced by klee::MergingSearcher::selectState().

DebugLogMerge

llvm::cl::opt<bool> klee::DebugLogMerge

extern

DebugValidateSolver

llvm::cl::opt<bool> klee::DebugValidateSolver

extern

Referenced by constructSolverChain().

ExprCat

llvm::cl::OptionCategory klee::ExprCat

extern

gTheArgsP

uint64_t* klee::gTheArgsP

static

Definition at line 213 of file ExternalDispatcher.cpp.

Referenced by klee::ExternalDispatcherImpl::createDispatcher(), and klee::ExternalDispatcherImpl::runProtectedCall().

klee_message_file

FILE * klee::klee_message_file = NULL

extern

Definition at line 27 of file ErrorHandling.cpp.

Referenced by klee_vmessage(), KleeHandler::KleeHandler(), and KleeHandler::~KleeHandler().

klee_warning_file

FILE * klee::klee_warning_file = NULL

extern

Definition at line 26 of file ErrorHandling.cpp.

Referenced by klee_vmessage(), KleeHandler::KleeHandler(), and KleeHandler::~KleeHandler().

LogTimedOutQueries

llvm::cl::opt<bool> klee::LogTimedOutQueries

extern

Referenced by constructSolverChain().

MaxCoreSolverTime

llvm::cl::opt<std::string> klee::MaxCoreSolverTime

extern

Referenced by EvaluateInputAST(), and klee::Executor::Executor().

MaxTime

cl::opt<std::string> klee::MaxTime

extern

Referenced by klee::Executor::Executor(), and main().

MergeCat

llvm::cl::OptionCategory klee::MergeCat

extern

MinQueryTimeToLog

llvm::cl::opt<std::string> klee::MinQueryTimeToLog

extern

Referenced by constructSolverChain().

MiscCat

llvm::cl::OptionCategory klee::MiscCat

extern

ModuleCat

llvm::cl::OptionCategory klee::ModuleCat

extern

noreturn

void klee::noreturn

Definition at line 29 of file ErrorHandling.h.

PtrBitCount

constexpr int klee::PtrBitCount = 3

constexpr

Definition at line 26 of file PTree.h.

Referenced by klee::PTree::getNextId().

QueryLoggingOptions

llvm::cl::bits<QueryLoggingSolverType> klee::QueryLoggingOptions

extern

Referenced by constructSolverChain().

SeedingCat

llvm::cl::OptionCategory klee::SeedingCat

extern

SOLVER_QUERIES_KQUERY_FILE_NAME

const char klee::SOLVER_QUERIES_KQUERY_FILE_NAME[] ="solver-queries.kquery"

Definition at line 25 of file Common.h.

Referenced by EvaluateInputAST(), and klee::Executor::Executor().

SOLVER_QUERIES_SMT2_FILE_NAME

const char klee::SOLVER_QUERIES_SMT2_FILE_NAME[] ="solver-queries.smt2"

Definition at line 23 of file Common.h.

Referenced by EvaluateInputAST(), and klee::Executor::Executor().

SolvingCat

llvm::cl::OptionCategory klee::SolvingCat

extern

Referenced by klee::KCommandLine::HideOptions().

TerminationCat

llvm::cl::OptionCategory klee::TerminationCat

extern

TestGenCat

llvm::cl::OptionCategory klee::TestGenCat

extern

theStatisticManager

StatisticManager * klee::theStatisticManager = 0

extern

Definition at line 57 of file Statistics.cpp.

Referenced by computeMinDistToUncovered(), klee::StatsTracker::computeReachableUncovered(), klee::Executor::dumpStates(), EvaluateInputAST(), getStatisticManager(), klee::Statistic::getValue(), klee::WeightedRandomSearcher::getWeight(), main(), klee::StatsTracker::markBranchVisited(), klee::Executor::maxStaticPctChecks(), klee::StatisticRecord::operator+=(), klee::Statistic::operator+=(), klee::StatisticRecord::operator=(), QueryLoggingSolver::startQuery(), klee::StatisticRecord::StatisticRecord(), klee::StatsTracker::StatsTracker(), klee::StatsTracker::stepInstruction(), klee::StatsTracker::updateStateStatistics(), klee::StatsTracker::writeIStats(), and klee::StatisticRecord::zero().

UseAssignmentValidatingSolver

llvm::cl::opt<bool> klee::UseAssignmentValidatingSolver

extern

Referenced by constructSolverChain().

UseBranchCache

llvm::cl::opt<bool> klee::UseBranchCache

extern

Referenced by constructSolverChain().

UseCexCache

llvm::cl::opt<bool> klee::UseCexCache

extern

Referenced by constructSolverChain().

UseFastCexSolver

llvm::cl::opt<bool> klee::UseFastCexSolver

extern

Referenced by constructSolverChain().

UseForkedCoreSolver

llvm::cl::opt<bool> klee::UseForkedCoreSolver

extern

Referenced by createCoreSolver(), and klee::Executor::Executor().

UseIncompleteMerge

llvm::cl::opt<bool> klee::UseIncompleteMerge

extern

Referenced by klee::MergingSearcher::selectState().

UseIndependentSolver

llvm::cl::opt<bool> klee::UseIndependentSolver

extern

Referenced by constructSolverChain().

UseMerge

llvm::cl::opt<bool> klee::UseMerge

extern

Referenced by constructUserSearcher(), and initializeSearchOptions().