klee
 All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
klee Namespace Reference

Namespaces

 bits32
 
 bits64
 
 expr
 
 floats
 
 ImpliedValue
 
 ints
 
 stats
 
 util
 

Classes

struct  _Identity
 
struct  _Select1st
 
class  AddressSpace
 
class  Array
 
struct  ArrayCmpFn
 
class  ArrayExprHash
 
struct  ArrayHashFn
 
class  Assignment
 
class  AssignmentEvaluator
 
class  BatchingSearcher
 
class  BFSSearcher
 
class  BinaryExpr
 
class  BitArray
 
class  BumpMergingSearcher
 
class  CallPathManager
 
class  CallPathNode
 
struct  CallSiteInfo
 
class  CastExpr
 
struct  Cell
 
class  CmpExpr
 
class  ConcatExpr
 
class  ConstantExpr
 
class  ConstraintManager
 
class  Context
 Context - Helper class for storing global information about a KLEE run. More...
 
class  DFSSearcher
 
class  DiscretePDF
 
class  DivCheckPass
 
class  ExecutionState
 
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  ExprPPrinter
 
class  ExprRangeEvaluator
 
class  ExprSMTLIBLetPrinter
 
class  ExprSMTLIBPrinter
 
class  ExprVisitor
 
class  ExternalDispatcher
 
class  ExtractExpr
 
class  FixedStack
 
class  generic_gep_type_iterator
 
class  ImmutableMap
 
class  ImmutableSet
 
class  ImmutableTree
 
class  IncompleteSolver
 
struct  InstructionInfo
 
class  InstructionInfoTable
 
class  InterleavedSearcher
 
class  Interpreter
 
class  InterpreterHandler
 
class  IntrinsicCleanerPass
 
class  IterativeDeepeningTimeSearcher
 
class  KConstant
 
struct  KFunction
 
struct  KGEPInstruction
 
class  KInstIterator
 
struct  KInstruction
 
class  KModule
 
class  LowerSwitchPass
 
class  MapOfSets
 
class  MemoryManager
 
class  MemoryObject
 
struct  MemoryObjectLT
 Function object ordering MemoryObject's by address. More...
 
class  MergingSearcher
 
class  NonConstantExpr
 
class  NotExpr
 
class  NotOptimizedExpr
 
class  ObjectHolder
 
class  ObjectState
 
class  OvershiftCheckPass
 
class  PhiCleanerPass
 
class  PTree
 
class  PTreeNode
 
struct  Query
 
class  QueryLogEntry
 
class  QueryLogResult
 
class  RaiseAsmPass
 
class  RandomPathSearcher
 
class  RandomSearcher
 
class  ReadExpr
 Class representing a one byte read from an array. More...
 
class  ref
 
class  RNG
 
class  Searcher
 
class  SeedInfo
 
class  SelectExpr
 Class representing an if-then-else expression. More...
 
class  Solver
 
class  SolverImpl
 SolverImpl - Abstract base clase for solver implementations. More...
 
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  TimerStatIncrementer
 
class  TimingSolver
 
class  TreeOStream
 
class  TreeStreamWriter
 
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  UpdateReachableTimer
 
class  WallTimer
 
class  WeightedRandomSearcher
 
class  WriteIStatsTimer
 
class  WriteStatsTimer
 

Typedefs

typedef std::pair< const
MemoryObject *, const
ObjectState * > 
ObjectPair
 
typedef std::vector< ObjectPairResolutionList
 
typedef ImmutableMap< const
MemoryObject *, ObjectHolder,
MemoryObjectLT
MemoryMap
 
typedef std::map
< llvm::Instruction
*, std::map< llvm::Function
*, CallSiteInfo > > 
CallSiteSummaryTable
 
typedef std::vector< std::pair
< ref< ReadExpr >, ref
< ConstantExpr > > > 
ImpliedValueList
 
typedef unsigned TreeStreamID
 
typedef
std::tr1::unordered_set< ref
< Expr >, klee::util::ExprHash,
klee::util::ExprCmp
ExprHashSet
 
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
 

Enumerations

enum  QueryLoggingSolverType { ALL_PC, ALL_SMTLIB, SOLVER_PC, SOLVER_SMTLIB }
 The different query logging solvers that can switched on/off. More...
 

Functions

llvm::cl::opt< bool > UseFastCexSolver ("use-fast-cex-solver", llvm::cl::init(false), llvm::cl::desc("(default=off)"))
 
llvm::cl::opt< bool > UseCexCache ("use-cex-cache", llvm::cl::init(true), llvm::cl::desc("Use counterexample caching (default=on)"))
 
llvm::cl::opt< bool > UseCache ("use-cache", llvm::cl::init(true), llvm::cl::desc("Use validity caching (default=on)"))
 
llvm::cl::opt< bool > UseIndependentSolver ("use-independent-solver", llvm::cl::init(true), llvm::cl::desc("Use constraint independence (default=on)"))
 
llvm::cl::opt< bool > DebugValidateSolver ("debug-validate-solver", llvm::cl::init(false))
 
llvm::cl::opt< int > MinQueryTimeToLog ("min-query-time-to-log", llvm::cl::init(0), llvm::cl::value_desc("milliseconds"), llvm::cl::desc("Set time threshold (in ms) for queries logged in files. ""Only queries longer than threshold will be logged. (default=0). ""Set this param to a negative value to log timeouts only."))
 
llvm::cl::opt< double > MaxCoreSolverTime ("max-solver-time", llvm::cl::desc("Maximum amount of time for a single SMT query (default=0s (off)). Enables --use-forked-solver"), llvm::cl::init(0.0), llvm::cl::value_desc("seconds"))
 
llvm::cl::opt< bool > UseForkedCoreSolver ("use-forked-solver", llvm::cl::desc("Run the core SMT solver in a forked process (default=on)"), llvm::cl::init(true))
 
llvm::cl::opt< bool > CoreSolverOptimizeDivides ("solver-optimize-divides", llvm::cl::desc("Optimize constant divides into add/shift/multiplies before passing to core SMT solver (default=on)"), llvm::cl::init(true))
 
llvm::cl::list
< QueryLoggingSolverType
queryLoggingOptions ("use-query-log", llvm::cl::desc("Log queries to a file. Multiple options can be specified seperate by a comma. By default nothing is logged."), llvm::cl::values(clEnumValN(ALL_PC,"all:pc","All queries in .pc (KQuery) format"), clEnumValN(ALL_SMTLIB,"all:smt2","All queries in .smt2 (SMT-LIBv2) format"), clEnumValN(SOLVER_PC,"solver:pc","All queries reaching the solver in .pc (KQuery) format"), clEnumValN(SOLVER_SMTLIB,"solver:smt2","All queries reaching the solver in .smt2 (SMT-LIBv2) format"), clEnumValEnd), llvm::cl::CommaSeparated)
 
SolverconstructSolverChain (Solver *coreSolver, std::string querySMT2LogPath, std::string baseSolverQuerySMT2LogPath, std::string queryPCLogPath, std::string baseSolverQueryPCLogPath)
 
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
 
uint64_t computeMinDistToUncovered (const KInstruction *ki, uint64_t minDistAtRA)
 
bool userSearcherRequiresMD2U ()
 
SearcherconstructUserSearcher (Executor &executor)
 
ExprSMTLIBPrintercreateSMTLIBPrinter ()
 
static uint32_t ones (register uint32_t x)
 
static uint32_t ldz (register uint32_t x)
 
static uint32_t exp_base_2 (register 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)
 
template<typename T >
static bool optionIsSet (llvm::cl::list< T > list, T option)
 
llvm::raw_ostream & operator<< (llvm::raw_ostream &os, const MemoryMap &mm)
 
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)
 
ExprBuildercreateDefaultExprBuilder ()
 
ExprBuildercreateConstantFoldingExprBuilder (ExprBuilder *Base)
 
ExprBuildercreateSimplifyingExprBuilder (ExprBuilder *Base)
 
llvm::Module * linkWithLibrary (llvm::Module *module, const std::string &libraryName)
 Link a module with a specified bitcode archive. More...
 
llvm::Function * getDirectCallTarget (llvm::CallSite)
 
bool functionEscapes (const llvm::Function *f)
 
SolvercreateValidatingSolver (Solver *s, Solver *oracle)
 
SolvercreateCachingSolver (Solver *s)
 
SolvercreateCexCachingSolver (Solver *s)
 
SolvercreateFastCexSolver (Solver *s)
 
SolvercreateIndependentSolver (Solver *s)
 
SolvercreatePCLoggingSolver (Solver *s, std::string path, int minQueryTimeToLog)
 
SolvercreateSMTLIBLoggingSolver (Solver *s, std::string path, int minQueryTimeToLog)
 
SolvercreateDummySolver ()
 
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)
 
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_Q llvm::Type *Op0, ItTy I, ItTy E)
 
template<typename ItTy >
generic_gep_type_iterator< ItTy > gep_type_end (LLVM_TYPE_Q llvm::Type *Op0, ItTy I, ItTy E)
 
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)
 

Variables

FILE * klee_warning_file = NULL
 
FILE * klee_message_file = NULL
 
void noreturn
 
RNG theRNG
 
llvm::cl::opt< bool > UseFastCexSolver
 
llvm::cl::opt< bool > UseCexCache
 
llvm::cl::opt< bool > UseCache
 
llvm::cl::opt< bool > UseIndependentSolver
 
llvm::cl::opt< bool > DebugValidateSolver
 
llvm::cl::opt< int > MinQueryTimeToLog
 
llvm::cl::opt< double > MaxCoreSolverTime
 
llvm::cl::opt< bool > UseForkedCoreSolver
 
llvm::cl::opt< bool > CoreSolverOptimizeDivides
 
llvm::cl::list
< QueryLoggingSolverType
queryLoggingOptions
 
const char ALL_QUERIES_SMT2_FILE_NAME [] ="all-queries.smt2"
 
const char SOLVER_QUERIES_SMT2_FILE_NAME [] ="solver-queries.smt2"
 
const char ALL_QUERIES_PC_FILE_NAME [] ="all-queries.pc"
 
const char SOLVER_QUERIES_PC_FILE_NAME [] ="solver-queries.pc"
 
StatisticManagertheStatisticManager = 0
 

Typedef Documentation

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

Definition at line 35 of file CallPathManager.h.

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

Definition at line 109 of file GetElementPtrTypeIterator.h.

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

Definition at line 44 of file ExprHashMap.h.

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

Definition at line 27 of file ImpliedValue.h.

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

Definition at line 110 of file GetElementPtrTypeIterator.h.

Definition at line 34 of file AddressSpace.h.

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

Definition at line 24 of file AddressSpace.h.

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

Definition at line 27 of file AddressSpace.h.

typedef unsigned klee::TreeStreamID

Definition at line 18 of file TreeStream.h.

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

Definition at line 111 of file GetElementPtrTypeIterator.h.

Enumeration Type Documentation

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

Enumerator
ALL_PC 

Log all queries (un-optimised) in .pc (KQuery) format.

ALL_SMTLIB 

Log all queries (un-optimised) .smt2 (SMT-LIBv2) format.

SOLVER_PC 

Log queries passed to solver (optimised) in .pc (KQuery) format.

SOLVER_SMTLIB 

Log queries passed to solver (optimised) in .smt2 (SMT-LIBv2) format.

Definition at line 33 of file CommandLine.h.

Function Documentation

uint64_t klee::computeMinDistToUncovered ( const KInstruction ki,
uint64_t  minDistAtRA 
)
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 klee::bits64::indexOfRightmostBit(), klee::bits64::indexOfSingleBit(), and klee::bits64::isolateRightmostBit().

Referenced by klee::STPBuilder::constructMulByConstant().

Here is the call graph for this function:

Here is the caller graph for this function:

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.

Referenced by klee::STPBuilder::constructSDivByConstant().

Here is the call graph for this function:

Here is the caller graph for this function:

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.

Referenced by klee::STPBuilder::constructUDivByConstant().

Here is the call graph for this function:

Here is the caller graph for this function:

Solver * klee::constructSolverChain ( Solver *  coreSolver,
std::string  querySMT2LogPath,
std::string  baseSolverQuerySMT2LogPath,
std::string  queryPCLogPath,
std::string  baseSolverQueryPCLogPath 
)
Searcher * klee::constructUserSearcher ( Executor executor)

Definition at line 95 of file UserSearcher.cpp.

References klee::Executor::getHandler(), klee::InterpreterHandler::getInfoStream(), getNewSearcher(), and klee::Searcher::printName().

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

Here is the call graph for this function:

Here is the caller graph for this function:

llvm::cl::opt<bool> klee::CoreSolverOptimizeDivides ( "solver-optimize-divides"  ,
llvm::cl::  desc"Optimize constant divides into add/shift/multiplies before passing to core SMT solver (default=on)",
llvm::cl::  inittrue 
)
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 259 of file CachingSolver.cpp.

Referenced by constructSolverChain(), and klee::expr::SMTParser::Solve().

Here is the caller graph for this function:

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 365 of file CexCachingSolver.cpp.

Referenced by constructSolverChain(), and klee::expr::SMTParser::Solve().

Here is the caller graph for this function:

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:

ExprBuilder * klee::createDefaultExprBuilder ( )

createDefaultExprBuilder - Create an expression builder which does no folding.

Definition at line 1057 of file ExprBuilder.cpp.

Referenced by main().

Here is the caller graph for this function:

Solver * klee::createDummySolver ( )

createDummySolver - Create a dummy solver implementation which always fails.

Definition at line 489 of file Solver.cpp.

Referenced by EvaluateInputAST(), and klee::expr::SMTParser::Solve().

Here is the caller graph for this function:

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 1134 of file FastCexSolver.cpp.

Referenced by constructSolverChain(), and klee::expr::SMTParser::Solve().

Here is the caller graph for this function:

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 336 of file IndependentSolver.cpp.

Referenced by constructSolverChain(), and klee::expr::SMTParser::Solve().

Here is the caller graph for this function:

Solver * klee::createPCLoggingSolver ( Solver s,
std::string  path,
int  minQueryTimeToLog 
)

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

Definition at line 65 of file PCLoggingSolver.cpp.

Referenced by constructSolverChain(), and klee::expr::SMTParser::Solve().

Here is the caller graph for this function:

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:

Solver * klee::createSMTLIBLoggingSolver ( Solver s,
std::string  path,
int  minQueryTimeToLog 
)

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

Definition at line 63 of file SMTLIBLoggingSolver.cpp.

Referenced by constructSolverChain().

Here is the caller graph for this function:

ExprSMTLIBPrinter * klee::createSMTLIBPrinter ( )

Create a SMT-LIBv2 printer based on command line options The caller is responsible for deleting the printer

Definition at line 226 of file ExprSMTLIBLetPrinter.cpp.

References ExprSMTLIBOptions::useLetExpressions().

Referenced by klee::Executor::getConstraintLog(), printInputAsSMTLIBv2(), and SMTLIBLoggingSolver::SMTLIBLoggingSolver().

Here is the call graph for this function:

Here is the caller graph for this function:

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 450 of file Solver.cpp.

Referenced by constructSolverChain(), and klee::expr::SMTParser::Solve().

Here is the caller graph for this function:

llvm::cl::opt<bool> klee::DebugValidateSolver ( "debug-validate-solver"  ,
llvm::cl::  initfalse 
)
ev_type_iterator klee::ev_type_begin ( const llvm::ExtractValueInst *  EV)
inline

Definition at line 128 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_iterator klee::ev_type_end ( const llvm::ExtractValueInst *  EV)
inline

Definition at line 132 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:

static uint32_t klee::exp_base_2 ( register 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:

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 21 of file ExprUtil.cpp.

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

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:

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 118 of file ExprUtil.cpp.

Referenced by STPSolverImpl::computeValue(), and CexCachingSolver::getAssignment().

Here is the caller graph for this function:

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 110 of file ExprUtil.cpp.

References klee::ExprVisitor::visit().

Here is the call graph for this function:

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::prepare().

Here is the caller graph for this function:

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

Definition at line 113 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_iterator klee::gep_type_begin ( const llvm::User &  GEP)
inline

Definition at line 120 of file GetElementPtrTypeIterator.h.

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

Here is the call graph for this function:

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

Definition at line 154 of file GetElementPtrTypeIterator.h.

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

Here is the call graph for this function:

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

Definition at line 117 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_iterator klee::gep_type_end ( const llvm::User &  GEP)
inline

Definition at line 124 of file GetElementPtrTypeIterator.h.

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

Here is the call graph for this function:

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

Definition at line 160 of file GetElementPtrTypeIterator.h.

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

Here is the call graph for this function:

llvm::Function* klee::getDirectCallTarget ( llvm::CallSite  )

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).

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

Here is the caller graph for this function:

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

Definition at line 136 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_iterator klee::iv_type_end ( const llvm::InsertValueInst *  IV)
inline

Definition at line 140 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:

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 73 of file Common.cpp.

References klee_vmessage().

Referenced by klee::MemoryManager::allocateFixed(), klee::Executor::executeCall(), initEnv(), klee::Executor::initializeGlobals(), injectStaticConstructorsAndDestructors(), KleeHandler::KleeHandler(), main(), KleeHandler::openOutputFile(), klee::KModule::prepare(), and klee::Executor::runFunctionAsMain().

Here is the call graph for this function:

Here is the caller graph for this function:

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 58 of file Common.cpp.

References klee_vmessage().

Referenced by klee::KModule::addInternalFunction(), klee::Executor::executeAlloc(), klee::Executor::initializeGlobals(), inlineChecks(), KleeHandler::KleeHandler(), main(), klee::Executor::run(), and klee::Executor::terminateStateOnError().

Here is the call graph for this function:

Here is the caller graph for this function:

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 66 of file Common.cpp.

References klee_vmessage().

Here is the call graph for this function:

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 81 of file Common.cpp.

References klee_vmessage().

Referenced by klee::Executor::addConstraint(), klee::KModule::addInternalFunction(), klee::Executor::callExternalFunction(), klee::Executor::getConstraintLog(), klee::Executor::getSymbolicSolution(), klee::Executor::initializeGlobals(), inlineChecks(), klee::Executor::run(), and klee::Executor::toConstant().

Here is the call graph for this function:

Here is the caller graph for this function:

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 90 of file Common.cpp.

References klee_vmessage().

Referenced by klee::MemoryManager::allocate(), klee::Executor::callExternalFunction(), klee::Executor::executeCall(), klee::Executor::executeInstruction(), klee::Executor::fork(), klee::SeedInfo::getNextInput(), klee::ObjectState::read8(), 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:

static uint32_t klee::ldz ( register uint32_t  x)
static

Definition at line 54 of file ConstantDivision.cpp.

References ones().

Here is the call graph for this function:

llvm::Module* klee::linkWithLibrary ( llvm::Module *  module,
const std::string &  libraryName 
)

Link a module with a specified bitcode archive.

Referenced by main(), and klee::KModule::prepare().

Here is the caller graph for this function:

llvm::cl::opt<double> klee::MaxCoreSolverTime ( "max-solver-time"  ,
llvm::cl::  desc"Maximum amount of time for a single SMT query (default=0s (off)). Enables --use-forked-solver",
llvm::cl::  init0.0,
llvm::cl::  value_desc"seconds" 
)
llvm::cl::opt<int> klee::MinQueryTimeToLog ( "min-query-time-to-log"  ,
llvm::cl::  init0,
llvm::cl::  value_desc"milliseconds",
llvm::cl::  desc"Set time threshold (in ms) for queries logged in files. ""Only queries longer than threshold will be logged. (default=0). ""Set this param to a negative value to log timeouts only." 
)
static uint32_t klee::ones ( register uint32_t  x)
static

Definition at line 43 of file ConstantDivision.cpp.

Referenced by ldz().

Here is the caller graph for this function:

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

Definition at line 278 of file Expr.h.

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

Definition at line 274 of file Expr.h.

References klee::Expr::compare().

Here is the call graph for this function:

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

Definition at line 181 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:

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

Definition at line 114 of file Ref.h.

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

Definition at line 120 of file Ref.h.

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

Definition at line 296 of file Expr.h.

References klee::Expr::print().

Here is the call graph for this function:

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

Definition at line 303 of file Expr.h.

References klee::Expr::printKind().

Here is the call graph for this function:

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

Definition at line 309 of file Expr.h.

References klee::Expr::print().

Here is the call graph for this function:

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

Definition at line 317 of file Expr.h.

References klee::Expr::printKind().

Here is the call graph for this function:

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

Definition at line 286 of file Expr.h.

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

Definition at line 270 of file Expr.h.

References klee::Expr::compare().

Here is the call graph for this function:

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

Definition at line 282 of file Expr.h.

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

Definition at line 290 of file Expr.h.

template<typename T >
static bool klee::optionIsSet ( llvm::cl::list< T >  list,
option 
)
static

Definition at line 63 of file CommandLine.h.

Referenced by constructSolverChain().

Here is the caller graph for this function:

llvm::cl::list<QueryLoggingSolverType> klee::queryLoggingOptions ( "use-query-log"  ,
llvm::cl::  desc"Log queries to a file. Multiple options can be specified seperate by a comma. By default nothing is logged.",
llvm::cl::  valuesclEnumValN(ALL_PC,"all:pc","All queries in .pc (KQuery) format"), clEnumValN(ALL_SMTLIB,"all:smt2","All queries in .smt2 (SMT-LIBv2) format"), clEnumValN(SOLVER_PC,"solver:pc","All queries reaching the solver in .pc (KQuery) format"), clEnumValN(SOLVER_SMTLIB,"solver:smt2","All queries reaching the solver in .smt2 (SMT-LIBv2) format"), clEnumValEnd,
llvm::cl::CommaSeparated   
)
llvm::cl::opt<bool> klee::UseCache ( "use-cache"  ,
llvm::cl::  inittrue,
llvm::cl::  desc"Use validity caching (default=on)" 
)
llvm::cl::opt<bool> klee::UseCexCache ( "use-cex-cache"  ,
llvm::cl::  inittrue,
llvm::cl::  desc"Use counterexample caching (default=on)" 
)
llvm::cl::opt<bool> klee::UseFastCexSolver ( "use-fast-cex-solver"  ,
llvm::cl::  initfalse,
llvm::cl::  desc"(default=off)" 
)
llvm::cl::opt<bool> klee::UseForkedCoreSolver ( "use-forked-solver"  ,
llvm::cl::  desc"Run the core SMT solver in a forked process (default=on)",
llvm::cl::  inittrue 
)
llvm::cl::opt<bool> klee::UseIndependentSolver ( "use-independent-solver"  ,
llvm::cl::  inittrue,
llvm::cl::  desc"Use constraint independence (default=on)" 
)
bool klee::userSearcherRequiresMD2U ( )

Definition at line 68 of file UserSearcher.cpp.

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

Here is the caller graph for this function:

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

Definition at line 144 of file GetElementPtrTypeIterator.h.

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

Here is the call graph for this function:

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

Definition at line 148 of file GetElementPtrTypeIterator.h.

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

Here is the call graph for this function:

Variable Documentation

const char klee::ALL_QUERIES_PC_FILE_NAME[] ="all-queries.pc"

Definition at line 22 of file Common.h.

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

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

Definition at line 20 of file Common.h.

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

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

Referenced by constructSolverChain().

FILE * klee::klee_message_file = NULL

Definition at line 23 of file Common.cpp.

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

FILE * klee::klee_warning_file = NULL

Definition at line 22 of file Common.cpp.

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

llvm::cl::opt<double> klee::MaxCoreSolverTime

Referenced by EvaluateInputAST().

llvm::cl::opt<int> klee::MinQueryTimeToLog

Referenced by constructSolverChain().

void klee::noreturn

Definition at line 31 of file Common.h.

llvm::cl::list<QueryLoggingSolverType> klee::queryLoggingOptions

Referenced by constructSolverChain().

const char klee::SOLVER_QUERIES_PC_FILE_NAME[] ="solver-queries.pc"

Definition at line 23 of file Common.h.

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

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

Definition at line 21 of file Common.h.

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

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

Referenced by constructSolverChain().

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

Referenced by constructSolverChain().

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

Referenced by constructSolverChain().