Storage for symbolic execution paths to be resumed later. More...

#include <path_storage.h>

Inheritance diagram for path_storaget:

Collaboration diagram for path_storaget:

Classes
struct	patht
	Information saved at a conditional goto to resume execution. More...

Public Member Functions
virtual	~path_storaget ()=default

patht &	peek ()
	Reference to the next path to resume. More...

virtual void	clear ()=0
	Clear all saved paths. More...

virtual void	push (const patht &)=0
	Add a path to resume to the storage. More...

void	pop ()
	Remove the next path to resume from the storage. More...

virtual std::size_t	size () const =0
	How many paths does this storage contain? More...

bool	empty () const
	Is this storage empty? More...

std::size_t	get_unique_l1_index (const irep_idt &id, std::size_t minimum_index)
	Provide a unique L1 index for a given `id`, starting from `minimum_index`. More...

std::size_t	get_unique_l2_index (const irep_idt &id)

void	add_function_loops (const irep_idt &identifier, const goto_programt &body)
	Generates a loop analysis for the instructions in goto_programt and keys it against function ID. More...

std::shared_ptr< lexical_loopst >	get_loop_analysis (const irep_idt &function_id)

Public Attributes
symex_nondet_generatort	build_symex_nondet
	Counter for nondet objects, which require unique names. More...

std::unordered_map< irep_idt, local_safe_pointerst >	safe_pointers
	Map function identifiers to local_safe_pointerst instances. More...

incremental_dirtyt	dirty
	Local variables are considered 'dirty' if they've had an address taken and therefore may be referred to by a pointer. More...

Private Types
typedef std::unordered_map< irep_idt, std::size_t >	name_index_mapt

Private Member Functions
virtual patht &	private_peek ()=0

virtual void	private_pop ()=0

std::size_t	get_unique_index (name_index_mapt &unique_index_map, const irep_idt &id, std::size_t minimum_index)

Private Attributes
std::unordered_map< irep_idt, std::shared_ptr< lexical_loopst > >	loop_analysis_map

name_index_mapt	l1_indices
	Storage used by get_unique_index. More...

name_index_mapt	l2_indices

Detailed Description

Storage for symbolic execution paths to be resumed later.

This data structure supports saving partially-executed symbolic execution paths so that their execution can be halted and resumed later. The choice of which path should be resumed next is implemented by subtypes of this abstract class.

Definition at line 37 of file path_storage.h.

Member Typedef Documentation

◆ name_index_mapt

typedef std::unordered_map<irep_idt, std::size_t> path_storaget::name_index_mapt

private

Definition at line 145 of file path_storage.h.

Constructor & Destructor Documentation

◆ ~path_storaget()

virtual path_storaget::~path_storaget ( )

virtualdefault

Member Function Documentation

◆ add_function_loops()

void path_storaget::add_function_loops	(	const irep_idt &	identifier,
		const goto_programt &	body
	)

inline

Generates a loop analysis for the instructions in goto_programt and keys it against function ID.

Definition at line 120 of file path_storage.h.

◆ clear()

virtual void path_storaget::clear ( )

pure virtual

Clear all saved paths.

This is typically used because we want to terminate symbolic execution early. It doesn't matter too much in terms of memory usage since CBMC typically exits soon after we do that, however it's nice to have tests that check that the worklist is always empty when symex finishes.

Implemented in path_fifot, and path_lifot.

◆ empty()

bool path_storaget::empty ( ) const

inline

Is this storage empty?

Definition at line 88 of file path_storage.h.

◆ get_loop_analysis()

std::shared_ptr<lexical_loopst> path_storaget::get_loop_analysis ( const irep_idt & function_id )

inline

Definition at line 131 of file path_storage.h.

◆ get_unique_index()

std::size_t path_storaget::get_unique_index	(	name_index_mapt &	unique_index_map,
		const irep_idt &	id,
		std::size_t	minimum_index
	)

inlineprivate

Definition at line 147 of file path_storage.h.

◆ get_unique_l1_index()

std::size_t path_storaget::get_unique_l1_index	(	const irep_idt &	id,
		std::size_t	minimum_index
	)

inline

Provide a unique L1 index for a given id, starting from minimum_index.

Definition at line 104 of file path_storage.h.

◆ get_unique_l2_index()

std::size_t path_storaget::get_unique_l2_index ( const irep_idt & id )

inline

Definition at line 109 of file path_storage.h.

◆ peek()

patht& path_storaget::peek ( )

inline

Reference to the next path to resume.

Definition at line 60 of file path_storage.h.

◆ pop()

void path_storaget::pop ( )

inline

Remove the next path to resume from the storage.

Definition at line 78 of file path_storage.h.

◆ private_peek()

virtual patht& path_storaget::private_peek ( )

privatepure virtual

Implemented in path_fifot, and path_lifot.

◆ private_pop()

virtual void path_storaget::private_pop ( )

privatepure virtual

Implemented in path_fifot, and path_lifot.

◆ push()

virtual void path_storaget::push ( const patht & )

pure virtual

Add a path to resume to the storage.

Implemented in path_fifot, and path_lifot.

◆ size()

virtual std::size_t path_storaget::size ( ) const

pure virtual

How many paths does this storage contain?

Implemented in path_fifot, and path_lifot.

Member Data Documentation

◆ build_symex_nondet

symex_nondet_generatort path_storaget::build_symex_nondet

Counter for nondet objects, which require unique names.

Definition at line 94 of file path_storage.h.

◆ dirty

incremental_dirtyt path_storaget::dirty

Local variables are considered 'dirty' if they've had an address taken and therefore may be referred to by a pointer.

Definition at line 116 of file path_storage.h.

◆ l1_indices

name_index_mapt path_storaget::l1_indices

private

Storage used by get_unique_index.

Definition at line 161 of file path_storage.h.

◆ l2_indices

name_index_mapt path_storaget::l2_indices

private

Definition at line 162 of file path_storage.h.

◆ loop_analysis_map

std::unordered_map<irep_idt, std::shared_ptr<lexical_loopst> > path_storaget::loop_analysis_map

private

Definition at line 138 of file path_storage.h.

◆ safe_pointers

std::unordered_map<irep_idt, local_safe_pointerst> path_storaget::safe_pointers

Map function identifiers to local_safe_pointerst instances.

This is to identify derferences that are guaranteed to be safe in a given execution context, thus helping to avoid symex to follow spurious error-handling paths.

Definition at line 100 of file path_storage.h.

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

/home/runner/work/cbmc/cbmc/src/goto-symex/path_storage.h

Classes

Public Member Functions

Public Attributes

Private Types

Private Member Functions

Private Attributes

Detailed Description

Member Typedef Documentation

◆ name_index_mapt

Constructor & Destructor Documentation

◆ ~path_storaget()

Member Function Documentation

◆ add_function_loops()

◆ clear()

◆ empty()

◆ get_loop_analysis()

◆ get_unique_index()

◆ get_unique_l1_index()

◆ get_unique_l2_index()

◆ peek()

◆ pop()

◆ private_peek()

◆ private_pop()

◆ push()

◆ size()

Member Data Documentation

◆ build_symex_nondet

◆ dirty

◆ l1_indices

◆ l2_indices

◆ loop_analysis_map

◆ safe_pointers