#include <Interpreter.h>

Inheritance diagram for klee::Interpreter:

Collaboration diagram for klee::Interpreter:

Classes
struct	InterpreterOptions

struct	ModuleOptions

Public Types
enum	LogType { STP , KQUERY , SMTLIB2 }

Public Member Functions
virtual	~Interpreter ()

virtual llvm::Module *	setModule (std::vector< std::unique_ptr< llvm::Module > > &modules, const ModuleOptions &opts)=0

virtual void	setPathWriter (TreeStreamWriter *tsw)=0

virtual void	setSymbolicPathWriter (TreeStreamWriter *tsw)=0

virtual void	setReplayKTest (const struct KTest *out)=0

virtual void	setReplayPath (const std::vector< bool > *path)=0

virtual void	useSeeds (const std::vector< struct KTest * > *seeds)=0

virtual void	runFunctionAsMain (llvm::Function f, int argc, char argv, char *envp)=0

virtual void	setHaltExecution (bool value)=0

virtual void	setInhibitForking (bool value)=0

virtual void	prepareForEarlyExit ()=0

virtual unsigned	getPathStreamID (const ExecutionState &state)=0

virtual unsigned	getSymbolicPathStreamID (const ExecutionState &state)=0

virtual void	getConstraintLog (const ExecutionState &state, std::string &res, LogType logFormat=STP)=0

virtual bool	getSymbolicSolution (const ExecutionState &state, std::vector< std::pair< std::string, std::vector< unsigned char > > > &res)=0

virtual void	getCoveredLines (const ExecutionState &state, std::map< const std::string *, std::set< unsigned > > &res)=0

Static Public Member Functions
static Interpreter *	create (llvm::LLVMContext &ctx, const InterpreterOptions &_interpreterOpts, InterpreterHandler *ih)

Protected Member Functions
	Interpreter (const InterpreterOptions &_interpreterOpts)

Protected Attributes
const InterpreterOptions	interpreterOpts

Detailed Description

Definition at line 51 of file Interpreter.h.

Member Enumeration Documentation

◆ LogType

enum klee::Interpreter::LogType

Enumerator
STP
KQUERY
SMTLIB2

Definition at line 71 of file Interpreter.h.

Constructor & Destructor Documentation

◆ Interpreter()

klee::Interpreter::Interpreter ( const InterpreterOptions & _interpreterOpts )

inlineprotected

Definition at line 94 of file Interpreter.h.

◆ ~Interpreter()

virtual klee::Interpreter::~Interpreter ( )

inlinevirtual

Definition at line 99 of file Interpreter.h.

Member Function Documentation

◆ create()

Interpreter * Interpreter::create	(	llvm::LLVMContext &	ctx,
		const InterpreterOptions &	_interpreterOpts,
		InterpreterHandler *	ih
	)

static

Definition at line 4738 of file Executor.cpp.

◆ getConstraintLog()

virtual void klee::Interpreter::getConstraintLog	(	const ExecutionState &	state,
		std::string &	res,
		LogType	logFormat = `STP`
	)

pure virtual

Implemented in klee::Executor.

Referenced by KleeHandler::processTestCase().

Here is the caller graph for this function:

◆ getCoveredLines()

virtual void klee::Interpreter::getCoveredLines	(	const ExecutionState &	state,
		std::map< const std::string *, std::set< unsigned > > &	res
	)

pure virtual

Implemented in klee::Executor.

Referenced by KleeHandler::processTestCase().

Here is the caller graph for this function:

◆ getPathStreamID()

virtual unsigned klee::Interpreter::getPathStreamID ( const ExecutionState & state )

pure virtual

Implemented in klee::Executor.

Referenced by KleeHandler::processTestCase().

Here is the caller graph for this function:

◆ getSymbolicPathStreamID()

virtual unsigned klee::Interpreter::getSymbolicPathStreamID ( const ExecutionState & state )

pure virtual

Implemented in klee::Executor.

Referenced by KleeHandler::processTestCase().

Here is the caller graph for this function:

◆ getSymbolicSolution()

virtual bool klee::Interpreter::getSymbolicSolution	(	const ExecutionState &	state,
		std::vector< std::pair< std::string, std::vector< unsigned char > > > &	res
	)

pure virtual

Implemented in klee::Executor.

Referenced by KleeHandler::processTestCase().

Here is the caller graph for this function:

◆ prepareForEarlyExit()

virtual void klee::Interpreter::prepareForEarlyExit ( )

pure virtual

Implemented in klee::Executor.

Referenced by KleeHandler::processTestCase().

Here is the caller graph for this function:

◆ runFunctionAsMain()

virtual void klee::Interpreter::runFunctionAsMain	(	llvm::Function *	f,
		int	argc,
		char **	argv,
		char **	envp
	)

pure virtual

Implemented in klee::Executor.

Referenced by main().

Here is the caller graph for this function:

◆ setHaltExecution()

virtual void klee::Interpreter::setHaltExecution ( bool value )

pure virtual

Implemented in klee::Executor.

Referenced by halt_execution(), and KleeHandler::processTestCase().

Here is the caller graph for this function:

◆ setInhibitForking()

virtual void klee::Interpreter::setInhibitForking ( bool value )

pure virtual

Implemented in klee::Executor.

Referenced by stop_forking().

Here is the caller graph for this function:

◆ setModule()

virtual llvm::Module * klee::Interpreter::setModule	(	std::vector< std::unique_ptr< llvm::Module > > &	modules,
		const ModuleOptions &	opts
	)

pure virtual

Register the module to be executed.

Parameters

modules A list of modules that should form the final module

Returns: The final module after it has been optimized, checks inserted, and modified for interpretation.

Implemented in klee::Executor.

Referenced by main().

Here is the caller graph for this function:

◆ setPathWriter()

virtual void klee::Interpreter::setPathWriter ( TreeStreamWriter * tsw )

pure virtual

Implemented in klee::Executor.

Referenced by KleeHandler::setInterpreter().

Here is the caller graph for this function:

◆ setReplayKTest()

virtual void klee::Interpreter::setReplayKTest ( const struct KTest * out )

pure virtual

Implemented in klee::Executor.

Referenced by main().

Here is the caller graph for this function:

◆ setReplayPath()

virtual void klee::Interpreter::setReplayPath ( const std::vector< bool > * path )

pure virtual

Implemented in klee::Executor.

Referenced by main().

Here is the caller graph for this function:

◆ setSymbolicPathWriter()

virtual void klee::Interpreter::setSymbolicPathWriter ( TreeStreamWriter * tsw )

pure virtual

Implemented in klee::Executor.

Referenced by KleeHandler::setInterpreter().

Here is the caller graph for this function:

◆ useSeeds()

virtual void klee::Interpreter::useSeeds ( const std::vector< struct KTest * > * seeds )

pure virtual

Implemented in klee::Executor.

Referenced by main().

Here is the caller graph for this function:

Member Data Documentation

◆ interpreterOpts

const InterpreterOptions klee::Interpreter::interpreterOpts

protected

Definition at line 92 of file Interpreter.h.

Referenced by klee::Executor::executeMemoryOperation(), and klee::Executor::replaceReadWithSymbolic().

The documentation for this class was generated from the following files:

/Users/cristic/klee/include/klee/Core/Interpreter.h
/Users/cristic/klee/lib/Core/Executor.cpp

Classes

Public Types

Public Member Functions

Static Public Member Functions

Protected Member Functions

Protected Attributes

Detailed Description

Member Enumeration Documentation

◆ LogType

Constructor & Destructor Documentation

◆ Interpreter()

◆ ~Interpreter()

Member Function Documentation

◆ create()

◆ getConstraintLog()

◆ getCoveredLines()

◆ getPathStreamID()

◆ getSymbolicPathStreamID()

◆ getSymbolicSolution()

◆ prepareForEarlyExit()

◆ runFunctionAsMain()

◆ setHaltExecution()

◆ setInhibitForking()

◆ setModule()

◆ setPathWriter()

◆ setReplayKTest()

◆ setReplayPath()

◆ setSymbolicPathWriter()

◆ useSeeds()

Member Data Documentation

◆ interpreterOpts